Require Export autom.
Require Export constr.

Definition A_Etat (t x : nat) := Etat t x = A.
Definition B_Etat (t x : nat) := Etat t x = B.
Definition C_Etat (t x : nat) := Etat t x = C.
Definition G_Etat (t x : nat) := Etat t x = G.
Definition L_Etat (t x : nat) := Etat t x = L.
Definition F_Etat (t x : nat) := Etat t x = F.

Inductive A_basic (t x cote : nat) : Prop :=
make_A_basic :
deux < cote ->
Diag t x cote L_Etat A_Etat L_Etat ->
Diag (S t) x cote L_Etat A_Etat L_Etat -> A_basic t x cote.
Inductive B_basic (t x cote : nat) : Prop :=
make_B_basic :
deux < cote ->
Diag' t x cote L_Etat G_Etat B_Etat L_Etat ->
Diag (S t) x cote L_Etat B_Etat L_Etat -> B_basic t x cote.
Inductive C_basic (t x cote : nat) : Prop :=
make_C_basic :
un < cote ->
Diag t x cote L_Etat C_Etat L_Etat ->
Diag (S t) x cote L_Etat C_Etat L_Etat -> C_basic t x cote.

Section construction2.

Notation rec3 := (Rec3 _ _ _ _) (only parsing).

Variable t x cote : nat.

Lemma A_A :
A_basic t x cote ->
L_Etat (S (S t)) (x + cote) ->
L_Etat (S (S (S t))) (x + cote) -> A_basic (S (S t)) x cote.
intros H; elim H; clear H; intros.
apply (Rec3 _ _ _ _ (make_A_basic (S (S t)) x cote)); auto with v62.
apply DDD with (P := L_Etat) (Q := A_Etat) (P' := L_Etat) (Q' := A_Etat);
auto with v62.
unfold loi, L_Etat, A_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

unfold loi, L_Etat, A_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

unfold loi_droite, L_Etat, A_Etat in |- *; intros t0 x0; case x0; intros;
simpl in |- *; rewrite H4; rewrite H5; auto with v62.
case (Etat t0 n); auto with v62.

unfold loi, L_Etat, A_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

unfold loi, L_Etat, A_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

clear H0; intros H0;
apply DDD with (P := L_Etat) (Q := A_Etat) (P' := L_Etat) (Q' := A_Etat);
auto with v62.
unfold loi, L_Etat, A_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

unfold loi, L_Etat, A_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

unfold loi_droite, L_Etat, A_Etat in |- *; intros t0 x0; case x0; intros;
simpl in |- *; rewrite H4; rewrite H5; auto with v62.
case (Etat t0 n); auto with v62.

unfold loi, L_Etat, A_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

unfold loi, L_Etat, A_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.
Qed.

Lemma B_B :
B_basic t x cote ->
L_Etat (S (S t)) (x + cote) ->
L_Etat (S (S (S t))) (x + cote) -> B_basic (S (S t)) x cote.
intros H; elim H; clear H; intros.
apply (Rec3 _ _ _ _ (make_B_basic (S (S t)) x cote)); auto with v62.
apply
D'DD'
with
(P := L_Etat)
(Q := B_Etat)
(R := G_Etat)
(P' := L_Etat)
(Q' := B_Etat); auto with v62.
unfold loi, L_Etat, B_Etat, G_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

unfold loi, L_Etat, B_Etat, G_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

unfold loi_droite, L_Etat, B_Etat in |- *; intros t0 x0; case x0; intros;
simpl in |- *; rewrite H4; rewrite H5; auto with v62.
case (Etat t0 n); auto with v62.

unfold loi, L_Etat, B_Etat, G_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

unfold loi, L_Etat, B_Etat, G_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

unfold loi, L_Etat, B_Etat, G_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

clear H0; intros H0;
apply
DD'D
with
(P := L_Etat)
(Q := B_Etat)
(R' := G_Etat)
(P' := L_Etat)
(Q' := B_Etat); auto with v62.
unfold loi, L_Etat, B_Etat, G_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

unfold loi_droite, L_Etat, B_Etat in |- *; intros t0 x0; case x0; intros;
simpl in |- *; rewrite H4; rewrite H5; auto with v62.
case (Etat t0 n); auto with v62.

unfold loi, L_Etat, B_Etat, G_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

unfold loi, L_Etat, B_Etat, G_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.
Qed.

Lemma C_C :
C_basic t x cote ->
L_Etat (S (S t)) (x + cote) ->
L_Etat (S (S (S t))) (x + cote) -> C_basic (S (S t)) x cote.
intros H; elim H; clear H; intros.
apply (Rec3 _ _ _ _ (make_C_basic (S (S t)) x cote)); auto with v62.
apply DDD with (P := L_Etat) (Q := C_Etat) (P' := L_Etat) (Q' := C_Etat);
auto with v62.
unfold loi, L_Etat, C_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

unfold loi, L_Etat, C_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

unfold loi_droite, L_Etat, C_Etat in |- *; intros t0 x0; case x0; intros;
simpl in |- *; rewrite H4; rewrite H5; auto with v62.
case (Etat t0 n); auto with v62.

unfold loi, L_Etat, C_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

unfold loi, L_Etat, C_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

clear H0; intros H0;
apply DDD with (P := L_Etat) (Q := C_Etat) (P' := L_Etat) (Q' := C_Etat);
auto with v62.
unfold loi, L_Etat, C_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

unfold loi, L_Etat, C_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

unfold loi_droite, L_Etat, C_Etat in |- *; intros t0 x0; case x0; intros;
simpl in |- *; rewrite H4; rewrite H5; auto with v62.
case (Etat t0 n); auto with v62.

unfold loi, L_Etat, C_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

unfold loi, L_Etat, C_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.
Qed.

Lemma A_B :
A_basic t x cote ->
L_Etat (S t) (S x + cote) ->
L_Etat (S (S t)) (S x + cote) -> B_basic (S t) (S x) cote.
intros H; elim H; clear H; intros.
apply (Rec3 _ _ _ _ (make_B_basic (S t) (S x) cote)); auto with v62.
apply DD_D' with (P := L_Etat) (Q := A_Etat) (P' := L_Etat) (Q' := A_Etat);
auto with v62.
unfold loi, L_Etat, A_Etat, B_Etat, G_Etat in |- *; intros; simpl in |- *;
rewrite H4; rewrite H5; rewrite H6; auto with v62.

unfold loi, L_Etat, A_Etat, B_Etat, G_Etat in |- *; intros; simpl in |- *;
rewrite H4; rewrite H5; rewrite H6; auto with v62.

unfold loi, L_Etat, A_Etat, B_Etat, G_Etat in |- *; intros; simpl in |- *;
rewrite H4; rewrite H5; rewrite H6; auto with v62.

unfold loi, L_Etat, A_Etat, B_Etat, G_Etat in |- *; intros; simpl in |- *;
rewrite H4; rewrite H5; rewrite H6; auto with v62.

clear H0; intros H0;
apply
D_D'D
with
(P := L_Etat)
(Q := A_Etat)
(P' := L_Etat)
(Q' := B_Etat)
(R' := G_Etat); auto with v62.
unfold loi, L_Etat, A_Etat, B_Etat, G_Etat in |- *; intros; simpl in |- *;
rewrite H4; rewrite H5; rewrite H6; auto with v62.

unfold loi, L_Etat, A_Etat, B_Etat, G_Etat in |- *; intros; simpl in |- *;
rewrite H4; rewrite H5; rewrite H6; auto with v62.

unfold loi, L_Etat, A_Etat, B_Etat, G_Etat in |- *; intros; simpl in |- *;
rewrite H4; rewrite H5; rewrite H6; auto with v62.
Qed.

Lemma C_A :
C_basic t x cote ->
L_Etat (S t) (x + S cote) ->
L_Etat (S (S t)) (x + S cote) -> A_basic (S t) x (S cote).
intros H; elim H; clear H; intros.
apply (Rec3 _ _ _ _ (make_A_basic (S t) x (S cote))); auto with v62.
apply
DD_Ddollar with (P := L_Etat) (Q := C_Etat) (P' := L_Etat) (Q' := C_Etat);
auto with v62.
unfold loi, L_Etat, A_Etat, C_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

unfold loi_droite, L_Etat, A_Etat in |- *; intros t0 x0; case x0; intros;
simpl in |- *; rewrite H4; rewrite H5; auto with v62.
case (Etat t0 n); auto with v62.

unfold loi, L_Etat, A_Etat, C_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

unfold loi, L_Etat, A_Etat, C_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

clear H0; intros H0;
apply
D_DDdollar with (P := L_Etat) (Q := C_Etat) (P' := L_Etat) (Q' := A_Etat);
auto with v62.
unfold loi, L_Etat, A_Etat, C_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

unfold loi_droite, L_Etat, A_Etat in |- *; intros t0 x0; case x0; intros;
simpl in |- *; rewrite H4; rewrite H5; auto with v62.
case (Etat t0 n); auto with v62.

unfold loi, L_Etat, A_Etat, C_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

unfold loi, L_Etat, A_Etat, C_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.
Qed.

Lemma B_C :
B_basic t x cote ->
L_Etat (S t) (S x + cote) ->
L_Etat (S (S t)) (S x + cote) -> C_basic (S t) (S x) cote.
intros H; elim H; clear H; intros.
apply (Rec3 _ _ _ _ (make_C_basic (S t) (S x) cote)); auto with v62.
apply
D'D_D
with
(P := L_Etat)
(Q := B_Etat)
(R := G_Etat)
(P' := L_Etat)
(Q' := B_Etat); auto with v62.
unfold loi, L_Etat, B_Etat, C_Etat, G_Etat in |- *; intros; simpl in |- *;
rewrite H4; rewrite H5; rewrite H6; auto with v62.

unfold loi, L_Etat, B_Etat, C_Etat, G_Etat in |- *; intros; simpl in |- *;
rewrite H4; rewrite H5; rewrite H6; auto with v62.

unfold loi, L_Etat, B_Etat, C_Etat, G_Etat in |- *; intros; simpl in |- *;
rewrite H4; rewrite H5; rewrite H6; auto with v62.

clear H0; intros H0;
apply D_DD with (P := L_Etat) (Q := B_Etat) (P' := L_Etat) (Q' := C_Etat);
auto with v62.
unfold loi, L_Etat, B_Etat, C_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

unfold loi, L_Etat, B_Etat, C_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.

unfold loi, L_Etat, B_Etat, C_Etat in |- *; intros; simpl in |- *; rewrite H4;
rewrite H5; rewrite H6; auto with v62.
Qed.

End construction2.

Section sommet.

Lemma GA_G : forall t x : nat, G_Etat t x -> A_Etat t (S x) -> G_Etat (S t) x.
unfold A_Etat, G_Etat in |- *; intros t x; case x; intros.
rewrite demi_pas; rewrite H; rewrite H0; auto with v62.

rewrite un_pas; rewrite H; rewrite H0; auto with v62.
Qed.

Lemma GB_G : forall t x : nat, G_Etat t x -> B_Etat t (S x) -> G_Etat (S t) x.
unfold B_Etat, G_Etat in |- *; intros t x; case x; intros.
rewrite demi_pas; rewrite H; rewrite H0; auto with v62.

rewrite un_pas; rewrite H; rewrite H0; auto with v62.
Qed.

Lemma GC_G : forall t x : nat, G_Etat t x -> C_Etat t (S x) -> G_Etat (S t) x.
unfold C_Etat, G_Etat in |- *; intros t x; case x; intros.
rewrite demi_pas; rewrite H; rewrite H0; auto with v62.

rewrite un_pas; rewrite H; rewrite H0; auto with v62.
Qed.

Lemma GA_dollarC :
forall t x : nat, G_Etat t x -> A_Etat t (S x) -> C_Etat (S t) (S x).
unfold A_Etat, C_Etat, G_Etat in |- *; intros; rewrite un_pas; rewrite H;
rewrite H0; auto with v62.
Qed.

Lemma GBA_dollarC :
forall t x : nat,
G_Etat t x -> B_Etat t (S x) -> A_Etat t (S (S x)) -> C_Etat (S t) (S x).
unfold A_Etat, B_Etat, C_Etat, G_Etat in |- *; intros; rewrite un_pas;
rewrite H; rewrite H0; rewrite H1; auto with v62.
Qed.

Lemma GBG_dollarG :
forall t x : nat,
G_Etat t x -> B_Etat t (S x) -> G_Etat t (S (S x)) -> G_Etat (S t) (S x).
unfold B_Etat, G_Etat in |- *; intros; rewrite un_pas; rewrite H; rewrite H0;
rewrite H1; auto with v62.
Qed.

Lemma GBC_dollarB :
forall t x : nat,
G_Etat t x -> B_Etat t (S x) -> C_Etat t (S (S x)) -> B_Etat (S t) (S x).
unfold B_Etat, C_Etat, G_Etat in |- *; intros; rewrite un_pas; rewrite H;
rewrite H0; rewrite H1; auto with v62.
Qed.

Lemma GC_dollarB :
forall t x : nat, G_Etat t x -> C_Etat t (S x) -> B_Etat (S t) (S x).
unfold B_Etat, C_Etat, G_Etat in |- *; intros; rewrite un_pas; rewrite H;
rewrite H0; auto with v62.
Qed.

End sommet.