Require Import Arith.
Require Import Omega. Require Import Compare_dec.
Require Import Relations.
Require Import Wellfounded.
Require Import Max.

Require Import Tools.
Require Import More_nat.
Require Import AccP.
Require Import not_decreasing.
Require Import EPSILON0.
Require Import More_nat.

Set Implicit Arguments.



Inductive T2 : Set :=
  zero : T2
| cons : T2 → T2 → nat → T2 → T2.

Notation "[ x , y ]" := (cons x y 0 zero) (at level 0) :g0_scope.

Open Scope g0_scope.

Definition psi alpha beta := [alpha, beta].

Definition psi_term alpha :=
  match alpha with zero ⇒ zero
                 | cons a b n c ⇒ [a, b]
  end.

Definition one := [zero,zero].

Lemma psi_eq : ∀ a b, psi a b = [a,b].
Proof.
 trivial.
Qed.

Ltac fold_psi := rewrite <- psi_eq.
Ltac fold_psis := repeat fold_psi.

Definition finite p := match p with
                             0 ⇒ zero
                           | S q ⇒ cons zero zero q zero
                           end.

Notation "'F' n" := (finite n)(at level 29) : g0_scope.

Inductive is_finite: T2 → Set :=
 zero_finite : is_finite zero
|succ_finite : ∀ n, is_finite (cons zero zero n zero).

Hint Constructors is_finite : T2.

Definition omega := [zero,one].

Definition epsilon0 := [one,zero].

Definition epsilon alpha := [one, alpha].


Fixpoint T1_inj (c:T1) : T2 :=
 match c with EPSILON0.zero ⇒ zero
            | EPSILON0.cons a n b ⇒ cons zero (T1_inj a) n (T1_inj b)
 end.


Inductive ap : T2 → Prop :=
ap_intro : ∀ alpha beta, ap [alpha, beta].



Inductive lt : T2 → T2 → Prop :=
|
 lt_1 : ∀ alpha beta n gamma, zero < cons alpha beta n gamma
|
 lt_2 : ∀ alpha1 alpha2 beta1 beta2 n1 n2 gamma1 gamma2,
                alpha1 < alpha2 →
                beta1 < cons alpha2 beta2 0 zero →
               cons alpha1 beta1 n1 gamma1 <
               cons alpha2 beta2 n2 gamma2
|
 lt_3 : ∀ alpha1 beta1 beta2 n1 n2 gamma1 gamma2,
               beta1 < beta2 →
               cons alpha1 beta1 n1 gamma1 <
               cons alpha1 beta2 n2 gamma2

|
 lt_4 : ∀ alpha1 alpha2 beta1 beta2 n1 n2 gamma1 gamma2,
               alpha2 < alpha1 →
               cons alpha1 beta1 0 zero < beta2 →
               cons alpha1 beta1 n1 gamma1 <
               cons alpha2 beta2 n2 gamma2

|
lt_5 : ∀ alpha1 alpha2 beta1 n1 n2 gamma1 gamma2,
               alpha2 < alpha1 →
               cons alpha1 beta1 n1 gamma1 <
               cons alpha2 (cons alpha1 beta1 0 zero) n2 gamma2

|
lt_6 : ∀ alpha1 beta1 n1 n2 gamma1 gamma2, (n1 < n2)%nat →
                                    cons alpha1 beta1 n1 gamma1 <
                                    cons alpha1 beta1 n2 gamma2

|
  lt_7 : ∀ alpha1 beta1 n1 gamma1 gamma2, gamma1 < gamma2 →
                                      cons alpha1 beta1 n1 gamma1 <
                                      cons alpha1 beta1 n1 gamma2
where "o1 < o2" := (lt o1 o2): g0_scope.
Hint Constructors lt : T2.

Definition le t t' := t = t' ∨ t < t'.
Hint Unfold le : T2.

Notation "o1 <= o2" := (le o1 o2): g0_scope.

Definition tail c := match c with | zero ⇒ zero
                                  | cons a b n c ⇒ c
                             end.

Inductive nf : T2 → Prop :=
| zero_nf : nf zero
| single_nf : ∀ a b n, nf a → nf b → nf (cons a b n zero)
| cons_nf : ∀ a b n a' b' n' c',
                             [a', b'] < [a, b] →
                             nf a → nf b →
                             nf(cons a' b' n' c')→
                             nf(cons a b n (cons a' b' n' c')).
Hint Constructors nf : T2.

Fixpoint succ (a:T2) : T2 :=
 match a with zero ⇒ finite 1
             | cons zero zero n c ⇒ finite (S (S n))
             | cons a b n c ⇒ cons a b n (succ c)
 end.

Fixpoint pred (a:T2) : option T2 :=
 match a with zero ⇒ None
             | cons zero zero 0 zero ⇒ Some zero
             | cons zero zero (S n) zero ⇒
                  Some (cons zero zero n zero)
             | cons a b n c ⇒ (match (pred c) with
                                   Some c' ⇒ Some (cons a b n c')
                                  | None ⇒ None
                                  end)
 end.

Inductive lt_epsilon0 : T2 → Prop :=
  zero_lt_e0 : lt_epsilon0 zero
| cons_lt_e0 : ∀ b n c, lt_epsilon0 b →
                                lt_epsilon0 c →
                                lt_epsilon0 (cons zero b n c).