Require Import bib.

Section automates.

Section definitions.

Parameter N : nat.
Axiom necessaire : deux < definitions.N.

Inductive Couleur : Set :=
  | A : Couleur
  | B : Couleur
  | C : Couleur
  | L : Couleur
  | G : Couleur
  | F : Couleur.

Definition Transition_A_A (c2 : Couleur) :=
  match c2 return Couleur with
  | A =>
       A
      
  | B => B
      
  | C => C
      
  | L => A
      
  | G => B
      
  | F => F
  end.

Definition Transition_B_A (c2 : Couleur) :=
  match c2 return Couleur with
  | A =>
       F
      
  | B => G
      
  | C => C
      
  | L => G
      
  | G => C
      
  | F => F
  end.

Definition Transition_L_A (c2 : Couleur) :=
  match c2 return Couleur with
  | A =>
       A
      
  | B => L
      
  | C => G
      
  | L => A
      
  | G => F
      
  | F => F
  end.

Definition Transition_A_B (c2 : Couleur) :=
  match c2 return Couleur with
  | A =>
       B
      
  | B => B
      
  | C => L
      
  | L => G
      
  | G => F
      
  | F => F
  end.

Definition Transition_B_B (c2 : Couleur) :=
  match c2 return Couleur with
  | A =>
       A
      
  | B => B
      
  | C => C
      
  | L => G
      
  | G => B
      
  | F => F
  end.

Definition Transition_C_B (c2 : Couleur) :=
  match c2 return Couleur with
  | A =>
       A
      
  | B => F
      
  | C => F
      
  | L => L
      
  | G => L
      
  | F => F
  end.

Definition Transition_L_B (c2 : Couleur) :=
  match c2 return Couleur with
  | A =>
       G
      
  | B => B
      
  | C => L
      
  | L => F
      
  | G => B
      
  | F => F
  end.

Definition Transition_G_B (c2 : Couleur) :=
  match c2 return Couleur with
  | A =>
       C
      
  | B => F
      
  | C => B
      
  | L => C
      
  | G => G
      
  | F => F
  end.

Definition Transition_B_C (c2 : Couleur) :=
  match c2 return Couleur with
  | A =>
       F
      
  | B => F
      
  | C => C
      
  | L => C
      
  | G => G
      
  | F => F
  end.

Definition Transition_C_C (c2 : Couleur) :=
  match c2 return Couleur with
  | A =>
       A
      
  | B => B
      
  | C => C
      
  | L => C
      
  | G => B
      
  | F => F
  end.

Definition Transition_L_C (c2 : Couleur) :=
  match c2 return Couleur with
  | A =>
       A
      
  | B => G
      
  | C => C
      
  | L => C
      
  | G => G
      
  | F => F
  end.

Definition Transition_A_L (c2 : Couleur) :=
  match c2 return Couleur with
  | A =>
       L
      
  | B => L
      
  | C => L
      
  | L => G
      
  | G => C
      
  | F => F
  end.

Definition Transition_C_L (c2 : Couleur) :=
  match c2 return Couleur with
  | A =>
       L
      
  | B => L
      
  | C => L
      
  | L => A
      
  | G => G
      
  | F => F
  end.

Definition Transition_G_L (c2 : Couleur) :=
  match c2 return Couleur with
  | A =>
       L
      
  | B => L
      
  | C => L
      
  | L => C
      
  | G => A
      
  | F => F
  end.

Definition Transition__G_L (c0 : Couleur) :=
  match c0 return Couleur with
  | A =>
       B
      
  | B => B
      
  | C => A
      
  | L => A
      
  | G => B
      
  | F => F
  end.

Definition Transition__G_G (c0 : Couleur) :=
  match c0 return Couleur with
  | A =>
       F
      
  | B => G
      
  | C => A
      
  | L => F
      
  | G => F
      
  | F => F
  end.

Definition Transition_A (c0 c2 : Couleur) :=
  match c0 return Couleur with
  | A =>
       Transition_A_A c2
      
  | B => Transition_B_A c2
      
  | C => A
      
  | L => Transition_L_A c2
      
  | G => C
      
  | F => F
  end.

Definition Transition_B (c0 c2 : Couleur) :=
  match c0 return Couleur with
  | A =>
       Transition_A_B c2
      
  | B => Transition_B_B c2
      
  | C => Transition_C_B c2
      
  | L => Transition_L_B c2
      
  | G => Transition_G_B c2
      
  | F => F
  end.

Definition Transition_C (c0 c2 : Couleur) :=
  match c0 return Couleur with
  | A =>
       B
      
  | B => Transition_B_C c2
      
  | C => Transition_C_C c2
      
  | L => Transition_L_C c2
      
  | G => B
      
  | F => F
  end.

Definition Transition_L (c0 c2 : Couleur) :=
  match c0 return Couleur with
  | A =>
       Transition_A_L c2
      
  | B => L
      
  | C => Transition_C_L c2
      
  | L => L
      
  | G => Transition_G_L c2
      
  | F => L
  end.

Definition Transition_G (c0 c2 : Couleur) :=
  match c2 return Couleur with
  | A =>
       G
      
  | B => G
      
  | C => G
      
  | L => Transition__G_L c0
      
  | G => Transition__G_G c0
      
  | F => G
  end.

Definition Transition (c0 c1 c2 : Couleur) :=
  match c1 return Couleur with
  | A =>
       Transition_A c0 c2
      
  | B => Transition_B c0 c2
      
  | C => Transition_C c0 c2
      
  | L => Transition_L c0 c2
      
  | G => Transition_G c0 c2
      
  | F => F
  end.

Notation Ifdec := (ifdec _ _ _) (only parsing).

Fixpoint Etat (t : nat) : nat -> Couleur :=
  fun x : nat =>
  match t return Couleur with
  | O =>
      
      match x return Couleur with
      | O =>
           G
          
      | S x' =>
          ifdec _ _ _ (eq_nat_dec (S definitions.N) (S x')) G
            (ifdec _ _ _ (eq_nat_dec (S (S definitions.N)) (S x')) C L)
      end
      
  | S t' =>
      match x return Couleur with
      | O =>
           Transition L (Etat t' 0) (Etat t' 1)
          
      | S x' => Transition (Etat t' x') (Etat t' (S x')) (Etat t' (S (S x')))
      end
  end.

End definitions.

Section cas_general.

Lemma un_pas :
 forall t x : nat,
 Etat (S t) (S x) = Transition (Etat t x) (Etat t (S x)) (Etat t (S (S x))).
intro; simpl in |- *; auto with v62.
Qed.

Lemma demi_pas :
 forall t : nat, Etat (S t) 0 = Transition L (Etat t 0) (Etat t 1).
intro; simpl in |- *; auto with v62.
Qed.

End cas_general.

Section base.

Lemma G00 : Etat 0 0 = G.
simpl in |- *; auto with v62.
Qed.

Lemma G0N : Etat 0 (S automates.N) = G.
simpl in |- *; apply Ifdec_left; auto with v62.
Qed.

Lemma C0N1 : Etat 0 (S (S automates.N)) = C.
simpl in |- *; rewrite Ifdec_right; auto with v62.
apply Ifdec_left; auto with v62.
Qed.

Lemma base_L : forall x : nat, 0 < x -> x < S automates.N -> Etat 0 x = L.
intros x Hlt; rewrite (S_pred x); auto with v62.
intros; simpl in |- *; rewrite Ifdec_right.
apply Ifdec_right.
apply sym_not_equal; apply lt_not_eq; auto with v62.

apply sym_not_equal; apply lt_not_eq; auto with v62.
Qed.

Lemma basedollar_L : forall x : nat, S (S automates.N) < x -> Etat 0 x = L.
intros; rewrite (S_pred x); auto with v62.
intros; simpl in |- *; rewrite Ifdec_right.
apply Ifdec_right.
apply lt_not_eq; auto with v62.

apply lt_not_eq; auto with v62.

apply lt_trans with (m := S automates.N); auto with v62.
Qed.

End base.

End automates.