(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)

Set Asymmetric Patterns.
Unset Standard Proposition Elimination Names.

Require Export ZArith.
Require Export Omega.



(**********************************************************************

                         CONFIGURATION

 **********************************************************************)

Section CONFIGURATION.

Definition counter := Z.

Record Config : Set := mkconfig {co : counter}.

Variable x : Z.

Definition mk_init_config := mkconfig x.

End CONFIGURATION.


(**********************************************************************

                         TRANSITIONS

 **********************************************************************)

Section TRANSITIONS.

Definition decrement_trans (c : Config) := mkconfig (co c - 1)%Z.

Definition divide_trans (c : Config) := mkconfig (Zeven.Zdiv2 (co c)).


Inductive transition (c : Config) : Set :=
  | decrement : (co c > 0)%Z -> Zeven.Zodd (co c) -> transition c
  | divide : (co c > 0)%Z -> Zeven.Zeven (co c) -> transition c.

Definition next_config (c : Config) (t : transition c) :=
  match t with
  | decrement h1 h2 => decrement_trans c
  | divide h1 h2 => divide_trans c
  end.

Variable x : Z.

Inductive legal : Config -> Prop :=
  | begin : legal (mk_init_config x)
  | after :
      forall (c : Config) (t : transition c),
      legal c -> legal (next_config c t).


End TRANSITIONS.


(* positive *)

Lemma Zdiv2_positive :
 forall x : Z, Zeven.Zeven x -> (x >= 0)%Z -> (Zeven.Zdiv2 x >= 0)%Z.
Proof.
(* Goal: forall (x : Z) (_ : Zeven x) (_ : Z.gt x Z0), Z.gt x (Z.div2 x) *)
  simple destruct x.
(* Goal: Z.gt (co (mkconfig x)) Z0 *)
(* Goal: legal (co (decrement_trans (mkconfig x))) c *)
  simpl in |- *.
(* Goal: Z.le Z0 x *)
  omega.
  
(* Goal: Z.gt (co (mkconfig x)) Z0 *)
(* Goal: legal (co (decrement_trans (mkconfig x))) c *)
  simpl in |- *.
(* Goal: forall (p : positive) (_ : match p with | xI p0 => False | xO p0 => True | xH => False end) (_ : Z.gt (Zpos p) Z0), Z.gt (Zpos p) match p with | xI p0 => Zpos (Pos.div2 p) | xO p0 => Zpos (Pos.div2 p) | xH => Z0 end *)
(* Goal: forall (p : positive) (_ : Zeven (Zneg p)) (_ : Z.gt (Zneg p) Z0), Z.gt (Zneg p) (Z.div2 (Zneg p)) *)
  simple destruct p.
(* Goal: forall (_ : Zeven (co c)) (_ : True), False *)
  intuition.
  
(* Goal: Z.gt (co (mkconfig x)) Z0 *)
(* Goal: legal (co (decrement_trans (mkconfig x))) c *)
  simpl in |- *.
(* Goal: forall (c : Config) (_ : Z.le (co c) Z0), not (@ex (transition c) (fun _ : transition c => True)) *)
  intros.
(* Goal: legal (co (divide_trans (mkconfig x))) c *)
  auto.
  
(* Goal: forall (_ : Zeven (co c)) (_ : True), False *)
  intuition.
  
(* Goal: Z.gt (co (mkconfig x)) Z0 *)
(* Goal: legal (co (decrement_trans (mkconfig x))) c *)
  simpl in |- *.
(* Goal: forall (p : positive) (_ : match p with | xI p0 => False | xO p0 => True | xH => False end) (_ : Z.gt (Zpos p) Z0), Z.gt (Zpos p) match p with | xI p0 => Zpos (Pos.div2 p) | xO p0 => Zpos (Pos.div2 p) | xH => Z0 end *)
(* Goal: forall (p : positive) (_ : Zeven (Zneg p)) (_ : Z.gt (Zneg p) Z0), Z.gt (Zneg p) (Z.div2 (Zneg p)) *)
  simple destruct p.
(* Goal: forall (_ : Zeven (co c)) (_ : True), False *)
  intuition.
  
(* Goal: Z.gt (co (mkconfig x)) Z0 *)
(* Goal: legal (co (decrement_trans (mkconfig x))) c *)
  simpl in |- *.
(* Goal: forall (_ : Zeven (co c)) (_ : True), False *)
  intuition.
  
(* Goal: forall (_ : Zeven (co c)) (_ : True), False *)
  intuition.
Qed.

Lemma x_gt_Zdiv2 :
 forall x : Z, Zeven.Zeven x -> (x > 0)%Z -> (x > Zeven.Zdiv2 x)%Z.
Proof.
(* Goal: forall (x : Z) (_ : Zeven x) (_ : Z.gt x Z0), Z.gt x (Z.div2 x) *)
  simple destruct x.
(* Goal: Z.gt (co (mkconfig x)) Z0 *)
(* Goal: legal (co (decrement_trans (mkconfig x))) c *)
  simpl in |- *.
(* Goal: legal (co (divide_trans (mkconfig x))) c *)
  auto.
  
(* Goal: Z.gt (co (mkconfig x)) Z0 *)
(* Goal: legal (co (decrement_trans (mkconfig x))) c *)
  simpl in |- *.
(* Goal: forall (p : positive) (_ : match p with | xI p0 => False | xO p0 => True | xH => False end) (_ : Z.gt (Zpos p) Z0), Z.gt (Zpos p) match p with | xI p0 => Zpos (Pos.div2 p) | xO p0 => Zpos (Pos.div2 p) | xH => Z0 end *)
(* Goal: forall (p : positive) (_ : Zeven (Zneg p)) (_ : Z.gt (Zneg p) Z0), Z.gt (Zneg p) (Z.div2 (Zneg p)) *)
  simple destruct p.
(* Goal: forall (_ : Zeven (co c)) (_ : True), False *)
  intuition.
  
(* Goal: Z.gt (co (mkconfig x)) Z0 *)
(* Goal: legal (co (decrement_trans (mkconfig x))) c *)
  simpl in |- *.
(* Goal: forall (c : Config) (_ : Z.le (co c) Z0), not (@ex (transition c) (fun _ : transition c => True)) *)
  intros.
(* Goal: forall _ : Z.gt (Zpos (xO p0)) Z0, Z.gt (Z.mul (Zpos (xO xH)) (Zpos p0)) (Zpos p0) *)
(* Goal: forall (_ : False) (_ : Z.gt (Zpos xH) Z0), Z.gt (Zpos xH) Z0 *)
(* Goal: forall (p : positive) (_ : Zeven (Zneg p)) (_ : Z.gt (Zneg p) Z0), Z.gt (Zneg p) (Z.div2 (Zneg p)) *)
  rewrite BinInt.Zpos_xO.
(* Goal: Z.gt (Z.mul (Zpos (xO xH)) (Zpos p0)) (Zpos p0) *)
(* Goal: forall (_ : False) (_ : Z.gt (Zpos xH) Z0), Z.gt (Zpos xH) Z0 *)
(* Goal: forall (p : positive) (_ : Zeven (Zneg p)) (_ : Z.gt (Zneg p) Z0), Z.gt (Zneg p) (Z.div2 (Zneg p)) *)
  generalize H0.
(* Goal: forall _ : Z.gt (Zpos (xO p0)) Z0, Z.gt (Z.mul (Zpos (xO xH)) (Zpos p0)) (Zpos p0) *)
(* Goal: forall (_ : False) (_ : Z.gt (Zpos xH) Z0), Z.gt (Zpos xH) Z0 *)
(* Goal: forall (p : positive) (_ : Zeven (Zneg p)) (_ : Z.gt (Zneg p) Z0), Z.gt (Zneg p) (Z.div2 (Zneg p)) *)
  rewrite BinInt.Zpos_xO.
(* Goal: forall (_ : Z.gt (co c) Z0) (_ : Zeven (co c)) (_ : True), False *)
  intro.
(* Goal: Z.le Z0 x *)
  omega.
  
(* Goal: legal (co (divide_trans (mkconfig x))) c *)
  auto.
  
(* Goal: forall (p : positive) (_ : Zeven (Zneg p)) (_ : Z.gt (Zneg p) Z0), Z.gt (Zneg p) (Z.div2 (Zneg p)) *)
  discriminate.
Qed.



Lemma counter_remains_positive_or_null :
 forall (x : Z) (c : Config), (x >= 0)%Z -> legal x c -> (co c >= 0)%Z.
Proof.
(* Goal: forall (c : Config) (_ : Z.le (co c) Z0), not (@ex (transition c) (fun _ : transition c => True)) *)
  intros.
(* Goal: False *)
  elim H0.
(* Goal: Z.gt (co (mkconfig x)) Z0 *)
(* Goal: legal (co (decrement_trans (mkconfig x))) c *)
  simpl in |- *.
(* Goal: legal (co (divide_trans (mkconfig x))) c *)
  auto.
  
(* Goal: forall (c : Config) (t : transition c), Z.gt (co c) (co (next_config c t)) *)
  simple induction t.
(* Goal: Z.gt (co (mkconfig x)) Z0 *)
(* Goal: legal (co (decrement_trans (mkconfig x))) c *)
  simpl in |- *.
(* Goal: forall (c : Config) (_ : Z.le (co c) Z0), not (@ex (transition c) (fun _ : transition c => True)) *)
  intros.
(* Goal: Z.le Z0 x *)
  omega.
  
(* Goal: Z.gt (co (mkconfig x)) Z0 *)
(* Goal: legal (co (decrement_trans (mkconfig x))) c *)
  simpl in |- *.
(* Goal: forall (c : Config) (_ : Z.le (co c) Z0), not (@ex (transition c) (fun _ : transition c => True)) *)
  intros.
(* Goal: Z.ge (Z.div2 (co c0)) Z0 *)
  apply Zdiv2_positive.
(* Goal: legal (co (divide_trans (mkconfig x))) c *)
  auto.
  
(* Goal: legal (co (divide_trans (mkconfig x))) c *)
  auto.
      
Qed.

Lemma decreasing_measure :
 forall (c : Config) (t : transition c), (co c > co (next_config c t))%Z.
Proof.
(* Goal: forall (c : Config) (t : transition c), Z.gt (co c) (co (next_config c t)) *)
  simple induction t.
(* Goal: forall (c : Config) (_ : Z.le (co c) Z0), not (@ex (transition c) (fun _ : transition c => True)) *)
  simpl in |- *; intros.
(* Goal: Z.le Z0 x *)
  omega.
(* Goal: Z.gt (co (mkconfig x)) Z0 *)
(* Goal: legal (co (decrement_trans (mkconfig x))) c *)
  simpl in |- *.
(* Goal: forall (c : Config) (_ : Z.le (co c) Z0), not (@ex (transition c) (fun _ : transition c => True)) *)
  intros.
(* Goal: Z.gt (co c) (Z.div2 (co c)) *)
  apply x_gt_Zdiv2.
(* Goal: legal (co (divide_trans (mkconfig x))) c *)
  auto.
(* Goal: legal (co (divide_trans (mkconfig x))) c *)
  auto.
Qed.


Lemma liveness :
 forall (x : Z) (c : Config),
 legal x c ->
 (co c > 0)%Z -> exists t : transition c, legal x (next_config c t).
Proof.
(* Goal: forall (c : Config) (_ : Z.le (co c) Z0), not (@ex (transition c) (fun _ : transition c => True)) *)
  intros.
(* Goal: @ex (transition c) (fun t : transition c => legal x (next_config c t)) *)
  generalize (Zeven.Zeven_odd_dec (co c)).
(* Goal: forall (_ : Z.gt (co c) Z0) (_ : Zeven (co c)) (_ : True), False *)
  intro.
(* Goal: @ex (transition c) (fun t : transition c => legal x (next_config c t)) *)
  elim H1.
(* Goal: forall (_ : Z.gt (co c) Z0) (_ : Zeven (co c)) (_ : True), False *)
  intro.
(* Goal: @ex (transition c) (fun t : transition c => legal x (next_config c t)) *)
(* Goal: forall _ : Zodd (co c), @ex (transition c) (fun t : transition c => legal x (next_config c t)) *)
  split with (divide c H0 a).
(* Goal: legal x (next_config (mkconfig x) (divide (mkconfig x) H2 H3)) *)
(* Goal: @eq Config (next_config (mkconfig x) (divide (mkconfig x) H2 H3)) (divide_trans (mkconfig x)) *)
(* Goal: Zeven (co (mkconfig x)) *)
(* Goal: Z.gt (co (mkconfig x)) Z0 *)
(* Goal: legal (co (divide_trans (mkconfig x))) c *)
  apply after.
(* Goal: legal (co (divide_trans (mkconfig x))) c *)
  auto.
  
(* Goal: forall (_ : Z.gt (co c) Z0) (_ : Zeven (co c)) (_ : True), False *)
  intro.
(* Goal: @ex (transition c) (fun t : transition c => legal x (next_config c t)) *)
  split with (decrement c H0 b).
(* Goal: legal x (next_config (mkconfig x) (divide (mkconfig x) H2 H3)) *)
(* Goal: @eq Config (next_config (mkconfig x) (divide (mkconfig x) H2 H3)) (divide_trans (mkconfig x)) *)
(* Goal: Zeven (co (mkconfig x)) *)
(* Goal: Z.gt (co (mkconfig x)) Z0 *)
(* Goal: legal (co (divide_trans (mkconfig x))) c *)
  apply after.
(* Goal: legal (co (divide_trans (mkconfig x))) c *)
  auto.
Qed.

Lemma blocked :
 forall c : Config, (co c <= 0)%Z -> ~ (exists t : transition c, True).
Proof.
(* Goal: forall (c : Config) (_ : Z.le (co c) Z0), not (@ex (transition c) (fun _ : transition c => True)) *)
  intros.
(* Goal: forall (_ : Z.gt (co c) Z0) (_ : Zeven (co c)) (_ : True), False *)
  unfold not in |- *; intro.
(* Goal: False *)
  elim H0.
(* Goal: forall (_ : Z.gt (co c) Z0) (_ : Zeven (co c)) (_ : True), False *)
  intro.
(* Goal: forall _ : True, False *)
  elim x.
(* Goal: forall (_ : Z.gt (co c) Z0) (_ : Zeven (co c)) (_ : True), False *)
  intro.
(* Goal: forall (_ : Zeven (co c)) (_ : True), False *)
  intuition.
  
(* Goal: forall (_ : Z.gt (co c) Z0) (_ : Zeven (co c)) (_ : True), False *)
  intro.
(* Goal: forall (_ : Zeven (co c)) (_ : True), False *)
  intuition.
Qed.

Lemma recur2 :
 forall P : nat -> Prop,
 (forall n : nat, (forall p : nat, p < n -> P p) -> P n) ->
 forall m : nat, P m.
Proof.
(* Goal: forall (P : forall _ : nat, Prop) (_ : forall (n : nat) (_ : forall (p : nat) (_ : lt p n), P p), P n) (m : nat), P m *)
intros; apply H; elim m.
(* Goal: forall (p : nat) (_ : lt p O), P p *)
(* Goal: forall (n : nat) (_ : forall (p : nat) (_ : lt p n), P p) (p : nat) (_ : lt p (S n)), P p *)
intros; absurd (p < 0); auto with arith.

(* Goal: forall (n : nat) (_ : forall (p : nat) (_ : lt p n), P p) (p : nat) (_ : lt p (S n)), P p *)
intros; case (le_lt_eq_dec p n).
(* Goal: forall _ : lt p n, P p *)
(* Goal: forall _ : @eq nat p n, P p *)
 auto with arith.
(* Goal: forall _ : lt p n, P p *)
(* Goal: forall _ : @eq nat p n, P p *)
 auto with arith.
(* Goal: legal (co (divide_trans (mkconfig x))) c *)
intro; rewrite e; apply H; auto.
Qed.

Lemma natgen_ind :
 forall P : Z -> Prop,
 (forall x : Z,
  (0 <= x)%Z -> (forall y : Z, (0 <= y)%Z -> (y < x)%Z -> P y) -> P x) ->
 forall x : Z, (0 <= x)%Z -> P x.
Proof.
(* Goal: forall (P : forall _ : Z, Prop) (_ : forall (x : Z) (_ : Z.le Z0 x) (_ : forall (y : Z) (_ : Z.le Z0 y) (_ : Z.lt y x), P y), P x) (x : Z) (_ : Z.le Z0 x), P x *)
intros; apply Z_of_nat_prop.
(* Goal: forall n : nat, P (Z.of_nat n) *)
(* Goal: Z.le Z0 x *)
intro; apply recur2 with (P := fun n : nat => P (Z_of_nat n)).
(* Goal: forall (n : nat) (_ : forall (p : nat) (_ : lt p n), P (Z.of_nat p)), P (Z.of_nat n) *)
(* Goal: Z.le Z0 x *)
intros; apply H.
(* Goal: Z.le Z0 x *)
omega.

intro; intro;
 apply Z_of_nat_prop with (P := fun y : Z => (y < Z_of_nat n0)%Z -> P y).
(* Goal: Z.le Z0 x *)
intros; apply H1; omega.

(* Goal: Z.ge x Z0 *)
trivial.

(* Goal: Z.ge x Z0 *)
trivial.
Qed.

Lemma rec2_princ :
 forall P : Z -> Prop,
 P 0%Z ->
 (forall x : Z, Zeven.Zeven x -> (x > 0)%Z -> P (Zeven.Zdiv2 x) -> P x) ->
 (forall x : Z, Zeven.Zodd x -> (x > 0)%Z -> P (x - 1)%Z -> P x) ->
 forall x : Z, (x >= 0)%Z -> P x.
Proof.
(* Goal: forall (c : Config) (_ : Z.le (co c) Z0), not (@ex (transition c) (fun _ : transition c => True)) *)
intros; apply natgen_ind; intros.
(* Goal: forall (_ : Z.gt (co c) Z0) (_ : Zeven (co c)) (_ : True), False *)
case (Z_le_lt_eq_dec 0 x0 H3); intro.
(* Goal: forall (_ : Z.gt (co c) Z0) (_ : Zeven (co c)) (_ : True), False *)
case (Zeven.Zeven_odd_dec x0); intro.
(* Goal: P x0 *)
(* Goal: P x0 *)
(* Goal: P x0 *)
(* Goal: Z.le Z0 x *)
apply H0.
(* Goal: legal (co (divide_trans (mkconfig x))) c *)
auto.

(* Goal: Z.le Z0 x *)
omega.

(* Goal: P (Z.div2 x0) *)
(* Goal: P x0 *)
(* Goal: P x0 *)
(* Goal: Z.le Z0 x *)
apply H4.
(* Goal: Z.le Z0 (Z.div2 x0) *)
(* Goal: Z.lt (Z.div2 x0) x0 *)
(* Goal: P x0 *)
(* Goal: P x0 *)
(* Goal: Z.le Z0 x *)
apply Zge_le; apply Zdiv2_positive; [ trivial | omega ].

(* Goal: Z.lt (Z.div2 x0) x0 *)
(* Goal: P x0 *)
(* Goal: P x0 *)
(* Goal: Z.le Z0 x *)
apply Zgt_lt; apply x_gt_Zdiv2; [ trivial | omega ].

(* Goal: P x0 *)
(* Goal: P x0 *)
(* Goal: Z.le Z0 x *)
apply H1.
(* Goal: Z.ge x Z0 *)
trivial.

(* Goal: Z.le Z0 x *)
omega.

(* Goal: Z.le Z0 x *)
apply H4; omega.

(* Goal: Z.ge x Z0 *)
rewrite <- e; trivial.

(* Goal: Z.le Z0 x *)
omega.
Qed.

Lemma legal_x_x : forall x : Z, legal x (mkconfig x).
Proof.
(* Goal: Z.ge x Z0 *)
intro; generalize (begin x); unfold mk_init_config in |- *; trivial.
Qed.

Lemma simpl_config : forall c : Config, mkconfig (co c) = c.
Proof.
(* Goal: legal (co (divide_trans (mkconfig x))) c *)
simple induction c; auto.
Qed.

Lemma legal_trans :
 forall (x : Z) (c c' : Config), legal x c -> legal (co c) c' -> legal x c'.
Proof.
(* Goal: False *)
intros; elim H0.
(* Goal: Z.ge x Z0 *)
unfold mk_init_config in |- *; rewrite simpl_config; trivial.

(* Goal: Z.ge x Z0 *)
intros; apply after; trivial.
Qed.

Lemma legal_decrement :
 forall (x : Z) (c : Config),
 (x > 0)%Z -> Zeven.Zodd x -> legal (x - 1) c -> legal x c.
Proof.
(* Goal: forall (x : Z) (c : Config) (_ : Z.gt x Z0) (_ : Zodd x) (_ : legal (Z.sub x (Zpos xH)) c), legal x c *)
intros; apply legal_trans with (c := decrement_trans (mkconfig x)).
(* Goal: legal x (divide_trans (mkconfig x)) *)
(* Goal: legal (co (divide_trans (mkconfig x))) c *)
cut (co (mkconfig x) > 0)%Z.
(* Goal: forall _ : Z.gt (co (mkconfig x)) Z0, legal x (decrement_trans (mkconfig x)) *)
(* Goal: Z.gt (co (mkconfig x)) Z0 *)
(* Goal: legal (co (decrement_trans (mkconfig x))) c *)
intro; cut (Zeven.Zodd (co (mkconfig x))).
intro;
 replace (decrement_trans (mkconfig x)) with
  (next_config (mkconfig x) (decrement (mkconfig x) H2 H3)).
(* Goal: legal x (next_config (mkconfig x) (divide (mkconfig x) H2 H3)) *)
(* Goal: @eq Config (next_config (mkconfig x) (divide (mkconfig x) H2 H3)) (divide_trans (mkconfig x)) *)
(* Goal: Zeven (co (mkconfig x)) *)
(* Goal: Z.gt (co (mkconfig x)) Z0 *)
(* Goal: legal (co (divide_trans (mkconfig x))) c *)
apply after.
(* Goal: legal x (mkconfig x) *)
(* Goal: not (@ex (transition (mkconfig x)) (fun _ : transition (mkconfig x) => True)) *)
(* Goal: @ex Config (fun c : Config => and (legal x c) (not (@ex (transition c) (fun _ : transition c => True)))) *)
apply legal_x_x.

(* Goal: legal (co (divide_trans (mkconfig x))) c *)
auto.

(* Goal: legal (co (divide_trans (mkconfig x))) c *)
auto.

(* Goal: Z.gt (co (mkconfig x)) Z0 *)
(* Goal: legal (co (decrement_trans (mkconfig x))) c *)
simpl in |- *.
(* Goal: legal (co (divide_trans (mkconfig x))) c *)
auto.

(* Goal: legal (co (divide_trans (mkconfig x))) c *)
auto.
Qed.

Lemma legal_divide :
 forall (x : Z) (c : Config),
 (x > 0)%Z -> Zeven.Zeven x -> legal (Zeven.Zdiv2 x) c -> legal x c.
Proof.
(* Goal: forall (x : Z) (c : Config) (_ : Z.gt x Z0) (_ : Zeven x) (_ : legal (Z.div2 x) c), legal x c *)
intros; apply legal_trans with (c := divide_trans (mkconfig x)).
(* Goal: legal x (divide_trans (mkconfig x)) *)
(* Goal: legal (co (divide_trans (mkconfig x))) c *)
cut (co (mkconfig x) > 0)%Z.
(* Goal: forall _ : Z.gt (co (mkconfig x)) Z0, legal x (divide_trans (mkconfig x)) *)
(* Goal: Z.gt (co (mkconfig x)) Z0 *)
(* Goal: legal (co (divide_trans (mkconfig x))) c *)
intro; cut (Zeven.Zeven (co (mkconfig x))).
intro;
 replace (divide_trans (mkconfig x)) with
  (next_config (mkconfig x) (divide (mkconfig x) H2 H3)).
(* Goal: legal x (next_config (mkconfig x) (divide (mkconfig x) H2 H3)) *)
(* Goal: @eq Config (next_config (mkconfig x) (divide (mkconfig x) H2 H3)) (divide_trans (mkconfig x)) *)
(* Goal: Zeven (co (mkconfig x)) *)
(* Goal: Z.gt (co (mkconfig x)) Z0 *)
(* Goal: legal (co (divide_trans (mkconfig x))) c *)
apply after.
(* Goal: legal x (mkconfig x) *)
(* Goal: not (@ex (transition (mkconfig x)) (fun _ : transition (mkconfig x) => True)) *)
(* Goal: @ex Config (fun c : Config => and (legal x c) (not (@ex (transition c) (fun _ : transition c => True)))) *)
apply legal_x_x.

(* Goal: legal (co (divide_trans (mkconfig x))) c *)
auto.

(* Goal: legal (co (divide_trans (mkconfig x))) c *)
auto.

(* Goal: legal (co (divide_trans (mkconfig x))) c *)
auto.

(* Goal: legal (co (divide_trans (mkconfig x))) c *)
auto.
Qed.

Lemma fin_O : forall x : Z, (x >= 0)%Z -> legal x (mkconfig 0%Z).
Proof.
(* Goal: forall (x : Z) (_ : Z.ge x Z0), legal x (mkconfig Z0) *)
intros; apply rec2_princ with (P := fun x : Z => legal x (mkconfig 0%Z)).
(* Goal: legal x (mkconfig x) *)
(* Goal: not (@ex (transition (mkconfig x)) (fun _ : transition (mkconfig x) => True)) *)
(* Goal: @ex Config (fun c : Config => and (legal x c) (not (@ex (transition c) (fun _ : transition c => True)))) *)
apply legal_x_x.

(* Goal: legal (co (divide_trans (mkconfig x))) c *)
intros; apply legal_divide; auto.

(* Goal: legal (co (divide_trans (mkconfig x))) c *)
intros; apply legal_decrement; auto.

(* Goal: Z.ge x Z0 *)
trivial.
Qed.

Lemma termination :
 forall x : Z,
 exists c : Config, legal x c /\ ~ (exists t : transition c, True).
Proof.
(* Goal: forall (c : Config) (_ : Z.le (co c) Z0), not (@ex (transition c) (fun _ : transition c => True)) *)
intro; case (Z_lt_ge_dec x 0); intros.
(* Goal: @ex Config (fun c : Config => and (legal x c) (not (@ex (transition c) (fun _ : transition c => True)))) *)
(* Goal: @ex Config (fun c : Config => and (legal x c) (not (@ex (transition c) (fun _ : transition c => True)))) *)
split with (mkconfig x).
(* Goal: and (legal x (mkconfig x)) (not (@ex (transition (mkconfig x)) (fun _ : transition (mkconfig x) => True))) *)
(* Goal: @ex Config (fun c : Config => and (legal x c) (not (@ex (transition c) (fun _ : transition c => True)))) *)
split.
(* Goal: legal x (mkconfig x) *)
(* Goal: not (@ex (transition (mkconfig x)) (fun _ : transition (mkconfig x) => True)) *)
(* Goal: @ex Config (fun c : Config => and (legal x c) (not (@ex (transition c) (fun _ : transition c => True)))) *)
apply legal_x_x.

(* Goal: Z.le Z0 x *)
apply blocked; simpl in |- *; omega.

(* Goal: and (legal x (mkconfig x)) (not (@ex (transition (mkconfig x)) (fun _ : transition (mkconfig x) => True))) *)
(* Goal: @ex Config (fun c : Config => and (legal x c) (not (@ex (transition c) (fun _ : transition c => True)))) *)
split with (mkconfig 0%Z); split.
(* Goal: forall _ : lt p n, P p *)
(* Goal: forall _ : @eq nat p n, P p *)
apply fin_O; auto with arith.

(* Goal: not (@ex (transition (mkconfig Z0)) (fun _ : transition (mkconfig Z0) => True)) *)
apply blocked; simpl in |- *; auto with zarith.
Qed.
