Require Export basic.

Section bord_gauche.

Notation rec2 := (Rec2 _ _ _) (only parsing).

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

Notation rec5 := (Rec5' _ _ _ _ _ _) (only parsing).

Section n_end.

Inductive un_end (t x : nat) : Prop :=
    make_un_end : G_Etat t x → G_Etat (S t) x → un_end t x.

Inductive deux_end (t x : nat) : Prop :=
    make_deux_end :
      C_Etat t (S x) → B_Etat (S t) (S x) → un_end (S t) x → deux_end t x.

Inductive trois_end (t x : nat) : Prop :=
    make_trois_end :
      A_Etat t (S (S x)) →
      G_Etat (S t) (S (S x)) → deux_end (S t) x → trois_end t x.

Inductive quatre_end (t x : nat) : Prop :=
    make_quatre_end :
      L_Etat t (S (S (S x))) →
      L_Etat (S t) (S (S (S x))) → trois_end (S t) x → quatre_end t x.

Inductive cinq_end (t x : nat) : Prop :=
    make_cinq_end :
      L_Etat t (S (S (S (S x)))) →
      L_Etat (S t) (S (S (S (S x)))) →
      G_Etat (S t) (S (S (S x))) →
      B_Etat (S (S t)) (S (S (S x))) → trois_end (S (S t)) x → cinq_end t x.

End n_end.

Section end_GG.

Lemma un_GG : ∀ t x : nat, un_end t x → G_Etat t x ∧ G_Etat (S t) x.
intros; elim H; auto with v62.
Qed.

Lemma deux_GG :
 ∀ t x : nat, deux_end t x → G_Etat (S t) x ∧ G_Etat (S (S t)) x.
intros; apply un_GG; elim H; auto with v62.
Qed.

Lemma trois_GG :
 ∀ t x : nat,
 trois_end t x → G_Etat (S (S t)) x ∧ G_Etat (S (S (S t))) x.
intros; apply deux_GG; elim H; auto with v62.
Qed.

Lemma quatre_GG :
 ∀ t x : nat,
 quatre_end t x → G_Etat (S (S (S t))) x ∧ G_Etat (S (S (S (S t)))) x.
intros; apply trois_GG; elim H; auto with v62.
Qed.

Lemma cinq_GG :
 ∀ t x : nat,
 cinq_end t x → G_Etat (S (S (S (S t)))) x ∧ G_Etat (S (S (S (S (S t))))) x.
intros; apply trois_GG; elim H; auto with v62.
Qed.

End end_GG.

Section premier_end.

Lemma un_deux :
 ∀ t x : nat,
 un_end t x →
 C_Etat (S t) (S x) → B_Etat (S (S t)) (S x) → deux_end (S t) x.
intros t x H; elim H; clear H; intros; apply make_deux_end; auto with v62.
apply (Rec2 _ _ _ (make_un_end (S (S t)) x)).
apply GC_G; auto with v62.

intros; apply GB_G; auto with v62.
Qed.

Lemma deux_trois :
 ∀ t x : nat,
 deux_end t x →
 A_Etat (S t) (S (S x)) → G_Etat (S (S t)) (S (S x)) → trois_end (S t) x.
intros t x H; elim H; clear H; intros; apply make_trois_end; auto with v62.
apply (Rec3 _ _ _ _ (un_deux (S t) x)); auto with v62; elim H1; clear H1;
 intros.
apply (GBA_dollarC (S t) x); auto with v62.

apply (GC_dollarB (S (S t)) x); auto with v62.
Qed.

Lemma deux_quatre :
 ∀ t x : nat,
 deux_end t x →
 L_Etat t (S (S x)) →
 L_Etat t (S (S (S x))) → L_Etat (S t) (S (S (S x))) → quatre_end t x.
intros t x H; elim H; unfold B_Etat, C_Etat, L_Etat in |- *; intros;
 apply make_quatre_end; auto with v62.
apply (Rec3 _ _ _ _ (deux_trois t x)); auto with v62.
unfold A_Etat in |- *; rewrite un_pas; rewrite H0; rewrite H3; rewrite H4;
 auto with v62.

unfold A_Etat, G_Etat in |- *; intros; rewrite un_pas; rewrite H1; rewrite H6;
 rewrite H5; auto with v62.
Qed.

Lemma trois_quatre :
 ∀ t x : nat,
 trois_end t x →
 L_Etat (S t) (S (S (S x))) →
 L_Etat (S (S t)) (S (S (S x))) → trois_end (S (S t)) x.
intros t x H; elim H; clear H; unfold A_Etat, L_Etat, G_Etat in |- *; intros.
apply (Rec3 _ _ _ _ (deux_trois (S t) x)); auto with v62; elim H1; clear H1;
 unfold A_Etat, B_Etat, C_Etat, G_Etat in |- *; intros;
 rewrite un_pas.
rewrite H0; rewrite H1; rewrite H2; auto with v62.

rewrite H3; rewrite H4; rewrite H6; auto with v62.
Qed.

Lemma trois_cinq :
 ∀ t x : nat,
 trois_end t x →
 G_Etat (S t) (S (S (S x))) →
 B_Etat (S (S t)) (S (S (S x))) → trois_end (S (S t)) x.
intros t x H; elim H; clear H; unfold A_Etat, B_Etat, G_Etat in |- *; intros.
apply (Rec3 _ _ _ _ (deux_trois (S t) x)); auto with v62; elim H1; clear H1;
 unfold A_Etat, B_Etat, C_Etat, G_Etat, un, deux in |- *;
 intros; rewrite un_pas.
rewrite H0; rewrite H1; rewrite H2; auto with v62.

rewrite H3; rewrite H4; rewrite H6; auto with v62.
Qed.

End premier_end.

Section idem_end.

Lemma quatre_quatre :
 ∀ t x : nat,
 quatre_end t x →
 L_Etat (S (S t)) (S (S (S x))) →
 L_Etat (S (S (S t))) (S (S (S x))) → quatre_end (S (S t)) x.
intros t x H; elim H; clear H; intros; apply make_quatre_end; auto with v62.
apply trois_quatre; auto with v62.
Qed.

Lemma cinq_cinq :
 ∀ t x : nat,
 cinq_end t x →
 L_Etat (S (S t)) (S (S (S (S x)))) →
 L_Etat (S (S (S t))) (S (S (S (S x)))) → cinq_end (S (S t)) x.
intros t x H; elim H; clear H; unfold L_Etat, B_Etat, G_Etat in |- *; intros.
apply (Rec5' _ _ _ _ _ _ (make_cinq_end (S (S t)) x));
 unfold B_Etat, G_Etat, L_Etat in |- *; auto with v62.
elim H3; clear H H0 H1 H3; unfold A_Etat, G_Etat in |- *; intros;
 rewrite un_pas.
rewrite H; rewrite H2; rewrite H4; auto with v62.

elim H3; clear H H0 H1 H3; unfold G_Etat in |- *; intros; rewrite un_pas.
rewrite H0; rewrite H6; rewrite H5; auto with v62.

intros; apply trois_cinq; auto with v62.
Qed.

End idem_end.

Section suivant_end.

Lemma quatre_cinq :
 ∀ t x : nat,
 quatre_end t x →
 L_Etat (S t) (S (S (S (S x)))) →
 L_Etat (S (S t)) (S (S (S (S x)))) → cinq_end (S t) x.
intros t x H; elim H; clear H; unfold L_Etat, B_Etat, G_Etat in |- *; intros.
apply (Rec5' _ _ _ _ _ _ (make_cinq_end (S t) x)).
unfold L_Etat in |- *; auto with v62.

unfold L_Etat in |- *; auto with v62.

elim H1; clear H H1; unfold A_Etat, L_Etat, G_Etat in |- *; intros;
 rewrite un_pas.
rewrite H; rewrite H0; rewrite H2; auto with v62.

elim H1; clear H H1; unfold B_Etat, L_Etat, G_Etat in |- *; intros;
 rewrite un_pas.
rewrite H1; rewrite H6; rewrite H3; auto with v62.

intros; apply trois_cinq; auto with v62.
Qed.

Lemma cinq_quatre :
 ∀ t x : nat,
 cinq_end t x →
 L_Etat (S t) (x + cinq) →
 L_Etat (S (S t)) (x + cinq) →
 C_basic (S t) (x + trois) deux ∧ quatre_end (S (S (S t))) x.
intros t x H; elim H; clear H; unfold L_Etat, B_Etat, G_Etat in |- *;
 rewrite plus_trois; rewrite plus_cinq; intros; apply and_impl.
elim H3; clear H H3; unfold A_Etat, G_Etat in |- *; intros;
 apply (Rec3 _ _ _ _ (make_C_basic (S t) (S (S (S x))) deux)).
auto with v62.

apply (Rec3 _ _ _ _ (deux_Diag L_Etat C_Etat (S t) (S (S (S x))))).
unfold L_Etat in |- *; auto with v62.

unfold C_Etat in |- *; rewrite un_pas.
rewrite H1; rewrite H0; rewrite H4; auto with v62.

elim H6; clear H6; unfold A_Etat, L_Etat, C_Etat in |- *; intros;
 rewrite un_pas.
rewrite H; rewrite H2; rewrite H9; auto with v62.

clear H H0 H1 H4; intros H;
 apply (Rec3 _ _ _ _ (deux_Diag L_Etat C_Etat (S (S t)) (S (S (S x)))));
 elim H; clear H; unfold L_Etat, C_Etat in |- *; do 2 rewrite plus_deux;
 intros.
auto with v62.

rewrite un_pas.
generalize (H1 1 1); repeat rewrite plus_un; intros.
rewrite H2; rewrite H5; rewrite H7; auto with v62.

rewrite un_pas; rewrite H3; rewrite H4; rewrite H7; auto with v62.

clear H H0 H1 H2 H4 H5; intros H; elim H; intros.
elim H1; elim H2; clear H H0 H1 H2; intros.
generalize H2; generalize H7; clear H H0 H1 H2 H4 H5 H6 H7;
 do 2 rewrite plus_deux; intros; apply make_quatre_end;
 auto with v62.
apply trois_quatre; auto with v62.
Qed.

End suivant_end.

End bord_gauche.