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.