Library hydras.Epsilon0.Paths

Transition systems associated with canonical sequences

P. Casteran, University of Bordeaux and Labri

After J. Ketonen and R. Solovay's paper " Rapidly Growing Ramsey Functions" in Annals of mathematics, Mar. 1981

TODO: Check wether the predicates ...PathS... are still useful

From hydras Require Import DecPreOrder Canon MoreLists First_toggle OrdNotations.
Import Relations Relation_Operators.
From Coq Require Import Lia.

Set Implicit Arguments.
Open Scope t1_scope.

relations associated with canonical sequences

Definition transition_S i : relation T1 :=
  fun alpha beta ⇒ alpha ≠ zero ∧ beta = canon alpha (S i).

Definition transition i : relation T1 :=
  match i with 0 ⇒ fun _ _ ⇒ False | S j ⇒ transition_S j end.

Definition bounded_transitionS (n:nat) alpha beta :=
  ∃ i:nat , (i ≤ n)%nat ∧ transition_S i alpha beta.

Paths inside epsilon_0

In this module, we study paths; i.e. sequences generated by the relations associated with the canonS i functions. In module O2H we show how pathes are related to hydra battles. Thus, the various classes of battles are described by predicates on pathes.

path_toS beta s alpha : pathS alpha s beta :

beta is reachable from alpha through the sequences s of indices ( zeros are ignored)

Note that only beta can be equal to zero

Inductive path_to (beta: T1) : list nat → T1 → Prop :=
| path_to_1 : ∀ (i:nat) alpha ,
    i ≠ 0 → transition i alpha beta → path_to beta (i ::nil) alpha
| path_to_cons : ∀ i alpha s gamma,
    i ≠ 0 → transition i alpha gamma →
    path_to beta s gamma → path_to beta (i ::s) alpha.

Definition path alpha s beta := path_to beta s alpha.

tries to solve a goal of the form (path_to beta s alpha)

Ltac path_tac :=
  repeat (match goal with
          | [ |- path_to ?b (?x :: ?y :: ?s) ?a ] ⇒
            (eright; [discriminate
                    | split;[discriminate | reflexivity]
                    | cbn])
          | [ |- path_to ?b (?x :: nil) ?a ] ⇒
                   (eleft; [discriminate |
                            split;cbn ; [discriminate | reflexivity]])

                 end).
Example ex_path1: path_to T1omega (2::2::2::nil) (T1omega × 2).

Example ex_path2: path_to T1omega (3::4::5::6::nil) (T1omega × 2).

Example ex_path3: path_to zero (interval 3 14) (T1omega × 2).

Example ex_path4: path_to zero (List.repeat 3 8) (T1omega × 2).

path_toS beta s alpha : pathS alpha s beta :

beta is reachable from alpha through the sequence of indices (shift s)

Note that only beta can be equal to zero

Lemma path_to_not_nil alpha s beta : path_to beta s alpha → s ≠ nil.

Inductive path_toS (beta: T1) : list nat → T1 → Prop :=
| path_toS_1 : ∀ (i:nat) alpha, transition_S i alpha beta →
                                      path_toS beta (i ::nil) alpha
| path_toS_cons : ∀ i alpha s gamma,
    transition_S i alpha gamma →
    path_toS beta s gamma →
    path_toS beta (i ::s) alpha.

Definition pathS alpha s beta := path_toS beta s alpha.

Accessibility (without traces)

Definition acc_from alpha beta := ∃ s , path_to beta s alpha.

following a path

useful helper ?

Fixpoint gnawS (alpha : T1) (s: list nat) :=
  match s with
    | nil ⇒ alpha
    | (i::s') ⇒ gnawS (canon alpha (S i)) s'
  end.

Fixpoint gnaw (alpha : T1) (s: list nat) :=
  match s with
    | nil ⇒ alpha
    | (0::s') ⇒ gnaw alpha s'
    | (S i :: s') ⇒ gnaw (canon alpha (S i)) s'
  end.

Fixpoint standard_gnaw (i:nat)(alpha : T1)(l:nat): T1 :=
  match l with
  | 0 ⇒ alpha
  | S m ⇒ standard_gnaw (S i) (canon alpha i) m
  end.

alpha ---> beta in KP n

Definition KP_arrowS n := clos_trans_1n T1 (bounded_transitionS n).

Paths with constant index

Definition const_pathS i :=
  clos_trans_1n T1 (fun alpha beta ⇒ alpha ≠ zero ∧
                                      beta = canon alpha (S i)).

Definition const_path i alpha beta :=
  match i with
    0 ⇒ False
  | S j ⇒ const_pathS j alpha beta
  end.

Lemma const_pathSE i alpha beta: const_pathS i alpha beta ↔
                                  const_path (S i) alpha beta.

Definition const_pathS_eps i := clos_refl _ (const_path (S i)).

standard paths

Inductive standard_path_toS (j:nat)( beta : T1): nat → T1 → Prop :=
  stdS_1 : ∀ i alpha,
    alpha ≠ zero →
    beta = canon alpha (S i) → j = i →
    standard_path_toS j beta i alpha
| stdS_S : ∀ i alpha,
    standard_path_toS j beta (S i) (canon alpha (S i)) →
    standard_path_toS j beta i alpha.

Definition standard_pathS i alpha j beta :=
  standard_path_toS j beta i alpha.

Inductive standard_path_to (j:nat)(beta : T1): nat → T1 → Prop :=
| std_1 : ∀ i alpha,
    alpha ≠ zero →
    beta = canon alpha i → j = i → i ≠ 0 →
    standard_path_to j beta i alpha
| std_S : ∀ i alpha,
    standard_path_to j beta (S i) (canon alpha i) →
    standard_path_to j beta i alpha.

Definition standard_path i alpha j beta :=
  standard_path_to j beta i alpha.

Lemma path_to_interval_inv_le alpha beta i j :
  path_to beta (interval i j) alpha →
  (i ≤ j)%nat.

Bridge Lemmas

Lemma gnawS_gnaw s alpha :
  gnawS alpha s = gnaw alpha (shift s).

Lemma gnaw_gnawS s alpha :
  gnaw alpha s = gnawS alpha (unshift s).

Lemma path_toS_path_to alpha s beta :
  path_toS beta s alpha ↔
  path_to beta (shift s) alpha.

Lemma path_to_path_toS :
  ∀ alpha s beta, path_to beta s alpha →
                        path_toS beta (unshift s) alpha.

Lemma path_to_path_toS_iff :
  ∀ alpha s beta, ¬ In 0 s → path_to beta s alpha ↔
                        path_toS beta (unshift s) alpha.

Lemma path_toS_nf beta s alpha: path_toS beta s alpha → nf alpha → nf beta.

Lemma path_acc_from alpha s beta:
    path alpha s beta → acc_from alpha beta.

Lemma path_toS_gnawS : ∀ s alpha beta, path_toS beta s alpha →
                                              beta = gnawS alpha s.

Composition/decomposition of paths

Lemma path_toS_app beta t gamma :
    path_toS gamma t beta → ∀ alpha s, path_toS beta s alpha →
                                             path_toS gamma (s ++t)%list alpha.

Lemma path_to_app beta t gamma :
    path_to gamma t beta → ∀ alpha s, path_to beta s alpha →
                                             path_to gamma (s ++t)%list alpha.

Lemma path_toS_decompose gamma s alpha :
  ∀ beta t u, s = t ++u →
                    path_toS beta t alpha → path_toS gamma u beta →
                    path_toS gamma s alpha.

Lemma path_to_decompose gamma alpha beta s t u :
  s = t ++ u →
  path_to beta t alpha → path_to gamma u beta →
  path_to gamma s alpha.

Ltac path_decompose x :=
  match goal with |- path_to ?a (interval ?from ?to) ?b ⇒
                  rewrite (interval_app from x to);
                  [eapply path_to_app | try lia | try lia]
  end.

Lemma path_toS_appR : ∀ u gamma alpha,
    path_toS gamma u alpha →
    ∀ s t, s ≠ nil → t ≠ nil → u = s ++ t →
                ∃ beta ,
                  path_toS beta s alpha ∧ path_toS gamma t beta.

Lemma path_to_appR : ∀ u gamma alpha,
    path_to gamma u alpha →
    ∀ s t, s ≠ nil → t ≠ nil → u = s ++ t → ¬ In 0 u →
                ∃ beta ,
                  path_to beta s alpha ∧ path_to gamma t beta.

Lemma path_toS_zero_but_last : ∀ x u alpha,
    path_toS zero (x ::u) alpha → u ≠ nil →
    path_toS one (but_last x u) alpha.

Lemma path_toS_zero_one : ∀ x alpha,
    path_toS zero (x ::nil) alpha → alpha = one.

Lemma path_toS_zero_inv x u alpha :
  path_toS zero (x ::u) alpha → {alpha = one ∧ u = nil } +
                                {u ≠ nil ∧ path_toS one
                                                      (but_last x u)
                                                      alpha }.

Lemma path_toS_zero alpha s : ¬ path_toS alpha s zero.

Lemma path_to_zero alpha s: ¬ path_to alpha s zero.

todo : use this lemma to remove useless hypotheses

Lemma path_to_not_In_zero : ∀ alpha s beta,
    path_to beta s alpha → ¬ In 0 s.

Lemma path_toS_tail alpha s beta :
    path_toS beta s alpha →
    ∀ gamma n, nf (T1.cons gamma n alpha) →
                    path_toS (T1.cons gamma n beta) s (T1.cons gamma n alpha).

Lemma path_to_tail alpha s beta :
  path_to beta s alpha →
  ∀ gamma n, nf (T1.cons gamma n alpha) →
                  path_to (T1.cons gamma n beta) s (T1.cons gamma n alpha).

Lemma path_toS_mult alpha s i : nf alpha →
    path_toS zero s (T1.phi0 alpha) →
    path_toS (T1.cons alpha i zero) s (T1.cons alpha (S i) zero).

Lemma path_to_mult alpha s i :
  nf alpha →
  path_to zero s (T1.phi0 alpha) →
  path_to (T1.cons alpha i zero) s (T1.cons alpha (S i) zero).

Properties of gnaw

Lemma gnaw_nf : ∀ s alpha, nf alpha → nf (gnaw alpha s).

Lemma gnaw_zero : ∀ s, gnaw 0 s = 0.

Lemma gnawS_zero : ∀ s, gnawS zero s = zero.

Lemma gnawS_nf : ∀ s alpha, nf alpha → nf (gnawS alpha s).

Lemma gnaw_succ: ∀ alpha i s, nf alpha →
                                    gnaw (T1.succ alpha) (S i ::s) =
                                    gnaw alpha s.

Lemma gnaw_rw i s alpha : gnaw alpha (S i ::s) = gnaw (canon alpha (S i)) s.

Lemma gnawS_to_path_toS : ∀ s alpha beta,
    beta = gnawS alpha s → beta ≠ zero → s ≠ nil →
    path_toS beta s alpha.

Lemma gnaw_to_path_to : ∀ s alpha beta,
    beta = gnaw alpha s → ¬ In 0 s → beta ≠ zero → s ≠ nil →
    path_to beta s alpha.

Lemma gnaw_app : ∀ s s' alpha,
                   gnaw alpha (s ++ s') = gnaw (gnaw alpha s) s'.

Lemma gnawS_app : ∀ s s' alpha,
                   gnawS alpha (s ++ s') = gnawS (gnawS alpha s) s'.

Lemma gnaws_rw i s alpha : gnawS alpha (i ::s) = gnawS (canon alpha (S i)) s.

Lemma gnawS_lim1 (i:nat)(s: list nat) (lambda : T1) :
  nf lambda → T1limit lambda →
  gnawS (T1.cons lambda 0 T1.zero) (i ::s) =
  gnawS (T1.cons (canon lambda (S i)) 0 T1.zero) s.

Lemma gnawS_lim2 (i n:nat)(s: list nat) (lambda : T1) :
  nf lambda → T1limit lambda →
  gnawS (T1.cons lambda (S n) T1.zero) (i ::s) =
  gnawS (T1.cons lambda n (T1.cons (canon lambda (S i)) 0 T1.zero)) s.

Lemma gnawS_succ_eqn1 i s gamma :
  nf gamma → gnawS (T1.cons (T1.succ gamma) 0 T1.zero) (i ::s) =
              gnawS (T1.cons gamma i T1.zero) s.

Lemma gnawS_succ_eqn2 :
  ∀ i n s gamma, nf gamma →
                      gnawS (T1.cons (T1.succ gamma) (S n) zero) (i ::s) =
                      gnawS (T1.cons (T1.succ gamma) n
                                     (T1.cons gamma i T1.zero)) s.

Lemma gnawS_tail :
  ∀ i s alpha n beta,
                  nf (T1.cons alpha n beta) →
                  beta ≠ T1.zero →
                  gnawS (T1.cons alpha n beta) (i ::s) =
                  gnawS (T1.cons alpha n (canon beta (S i))) s.

Lemma gnawS_SSn (i:nat) s :
  ∀ alpha n ,
    nf alpha →
    gnawS (T1.cons alpha (S n) T1.zero) (i ::s) =
    gnawS (T1.cons alpha n (canon (T1.cons alpha 0 zero) (S i))) s.

Lemma gnawS_cut1 : ∀ s alpha n beta,
                    nf (T1.cons alpha n beta) →
                    gnawS (T1.cons alpha n beta) s = T1.zero →
                    ∃ s1 s2 , s = s1 ++ s2 ∧
                                  gnawS beta s1 = zero ∧
                                  gnawS (T1.cons alpha n T1.zero) s2 = zero.

Lemma gnawS_cut2 : ∀ s alpha n ,
                   nf alpha →
                   gnawS (T1.cons alpha (S n) T1.zero) s = zero →
                   ∃ s1 s2 , s = s1 ++ s2 ∧
                                 gnawS (T1.phi0 alpha) s1 = zero ∧
                                 gnawS (T1.cons alpha n T1.zero) s2 = zero.

Lemma path_to_gnaw : ∀ s alpha beta,
    path_to beta s alpha →
    beta = gnaw alpha s.

Lemma gnawS_path_toS : ∀ s alpha , s ≠ nil → gnawS alpha s ≠ zero →
                                        path_toS (gnawS alpha s) s alpha.

Lemma gnaw_path_to : ∀ s alpha , s ≠ nil → ¬ In 0 s →
                                      gnaw alpha s ≠ zero →
                                      path_to (gnaw alpha s) s alpha.

Properties of acc_from

Lemma acc_from_trans : ∀ alpha beta gamma,
    acc_from alpha beta → acc_from beta gamma → acc_from alpha gamma.

Lemma LT_path_toS (alpha beta : T1) :
  beta t1 < alpha → {s : list nat | path_toS beta s alpha }.

Lemma LT_path_to (alpha beta : T1) :
  beta t1 < alpha → {s : list nat | path_to beta s alpha }.

Lemma LT_acc_from (alpha beta : T1) :
  beta t1 < alpha → acc_from alpha beta.

Lemma path_toS_LT beta s alpha:
  path_toS beta s alpha → nf alpha → beta t1 < alpha.

Lemma path_to_LT beta s alpha :
  path_to beta s alpha → nf alpha → beta t1 < alpha.

Lemma acc_from_LT (alpha beta : T1) :
  acc_from alpha beta → nf alpha → beta t1 < alpha.

Paths with constant index: lemmas

Lemma const_pathS_repeat i : ∀ alpha beta,
    const_path (S i) alpha beta →
    ∃ n:nat , path_toS beta (repeat i (S n)) alpha.

Lemma const_pathS_repeatR i : ∀ n alpha beta,
    path_toS beta (repeat i (S n)) alpha →
    const_path (S i) alpha beta.

Lemma const_pathS_nf : ∀ n alpha beta,
    const_pathS n alpha beta →
    nf alpha → nf beta.

Lemma const_pathS_zero n alpha : ¬ const_path (S n) zero alpha.

Lemma const_pathS_LT i alpha beta:
                                     nf alpha →
                                     const_path (S i) alpha beta →
                                     beta t1 < alpha.

Lemma const_path_LT i :
  ∀ alpha beta,
      nf alpha → const_path i alpha beta →
    beta t1 < alpha.

Lemma const_pathS_LE i : ∀ alpha beta,
    nf alpha → const_path (S i) alpha beta → beta t1 ≤ alpha.

Lemma const_pathS_inv : ∀ n alpha beta,
    const_path (S n) alpha beta →
    beta = canon alpha (S n) ∨
    const_path (S n) (canon alpha (S n)) beta.

Lemma const_pathS_inv_strong : ∀ n alpha beta,
    const_path (S n) alpha beta →
    {beta = canon alpha (S n)} +
    {const_path (S n) (canon alpha (S n)) beta }.

Lemma const_pathS_trans : ∀ n alpha beta gamma,
    const_path (S n) alpha beta →
    const_path (S n) beta gamma →
    const_path (S n) alpha gamma.

Lemma const_pathS_eps_trans : ∀ i alpha beta gamma,
    const_pathS_eps i alpha beta →
    const_pathS_eps i beta gamma →
    const_pathS_eps i alpha gamma .

Lemma const_pathS_eps_LE_2 : ∀ n alpha beta,
    nf alpha → nf beta →
    const_pathS_eps n alpha beta →
    beta t1 ≤ alpha.

Lemma Proposition_2_3a:
  ∀ n alpha , nf alpha → alpha ≠ zero →
                   ∀ beta gamma, LT gamma beta →
                                        const_pathS n alpha gamma →
                                        const_pathS n alpha beta →
                                        const_pathS n beta gamma.

Lemma KS_thm_2_4_lemma1 : ∀ i alpha n beta beta',
    nf (T1.cons alpha n beta) →
    beta ≠ zero →
    const_pathS i beta beta' →
    const_pathS i (T1.cons alpha n beta)
            (T1.cons alpha n beta').

Lemma const_pathS_first_step : ∀ i alpha beta,
    const_pathS i alpha beta →
    {beta = canon alpha (S i) } +
    {const_pathS i (canon alpha (S i)) beta }.

Lemma KS_thm_2_4_lemma1' : ∀ i alpha n beta ,
    nf alpha → alpha ≠ zero →
    const_pathS i (T1.phi0 alpha) beta →
    const_pathS i (T1.cons alpha (S n) zero)
                (T1.cons alpha n beta).

Lemma KS_thm_2_4_lemma2 (n:nat)(alpha:T1) :
  nf alpha → alpha ≠ zero → const_pathS n alpha zero.

Lemma KS_thm_2_4_lemma3_0 : ∀ i alpha n,
    nf alpha →
    const_pathS i (T1.cons alpha (S n) zero)
            (T1.cons alpha n zero).

Lemma KS_thm_2_4_lemma3 : ∀ i n p alpha ,
    nf alpha → n < p →
    const_pathS i (T1.cons alpha p zero)
            (T1.cons alpha n zero).

Lemma KS_thm_2_4_lemma4 : ∀ i alpha,
    nf alpha →
    const_pathS i (T1.phi0 (succ alpha)) (T1.phi0 alpha).

Lemma KS_thm_2_4_lemma5 : ∀ i alpha beta,
    const_pathS i alpha beta → nf alpha →
    alpha ≠ zero →
    const_pathS i (T1.phi0 alpha) (T1.phi0 beta).

Theorem KS_thm_2_4 (lambda : T1) :
  nf lambda → T1limit lambda →
  ∀ i j, (i < j)%nat →
              const_path 1 (canon lambda (S j)) (canon lambda (S i)).

Corollary 12 of KS

Corollary Cor12 (alpha : T1) : nf alpha →
                ∀ beta i n, beta t1 < alpha →
                                 i < n →
                                 const_path (S i) alpha beta →
                                 const_path (S n) alpha beta.

Corollary Cor12_1 (alpha : T1) :
  nf alpha →
  ∀ beta i n, beta t1 < alpha →
                   i ≤ n →
                   const_path (S i) alpha beta →
                   const_path (S n) alpha beta.
Corollary Cor12_2 (alpha : T1) :
    nf alpha →
    ∀ beta i n,
      i ≤ n →
      const_pathS_eps i alpha beta →
      const_pathS_eps n alpha beta.

Corollary Cor12_3 (alpha : T1) :
  nf alpha →
  ∀ beta i n, beta t1 < alpha →
                   i ≤ n →
                   const_path i alpha beta →
                   const_path n alpha beta.

Lemma const_pathS_eps_zero n alpha :
   const_pathS_eps n zero alpha → alpha = zero.

Lemma Lemma2_6_1 (alpha : T1) :
  nf alpha →
  ∀ beta, beta t1 < alpha →
               {n :nat | const_path (S n) alpha beta }.

Lemma small_lemma (i:nat) (beta : T1) : ∀ alpha,
      const_pathS i alpha beta →
      nf alpha →
      beta t1 ≤ canon alpha (S i).

Lemma L2_6_2 (p: nat) :
  ∀ alpha, nf alpha →
                ∀ beta, const_pathS p alpha beta →
                             T1.succ beta t1 < alpha →
                             const_pathS (S p) alpha (T1.succ beta).

Section Lemma_4_3_Proof.
  Variables alpha beta : T1.
  Hypothesis H00 : alpha ≠ zero.
  Hypothesis nf1 : nf alpha.
  Hypothesis nf2 : nf beta.
  Variables n0 n1 n2: nat.
  Hypothesis H0: (n0 ≤n2)%nat.
  Hypothesis H1: (n1 ≤n2)%nat.
  Hypothesis H4: const_pathS_eps n0 alpha beta.

  Remark R4_3_1: const_pathS_eps n2 alpha beta.

  Remark R4_3_2 : const_pathS_eps n2 beta (canon beta (S n1)).

  Remark R4_3_3: const_pathS_eps n2 alpha (canon beta (S n1)).

  Remark R4_3_4 : (canon beta (S n1) t1 ≤ canon alpha (S n2))%t1.

  Lemma Lemma_4_3_0 :
    const_pathS_eps n2 (canon alpha (S n2)) (canon beta (S n1)).

End Lemma_4_3_Proof.

Lemma Lemma_4_3 :
  ∀ alpha beta : T1,
    nf alpha →
    nf beta →
    ∀ n0 n1 n2 : nat,
      (n0 ≤ n2)%nat →
      (n1 ≤ n2)%nat →
      const_pathS_eps n0 alpha beta →
      const_pathS_eps n2 (canon alpha (S n2)) (canon beta (S n1)).

Lemma const_pathS_LT' (i : nat) (alpha beta : T1) (H:nf alpha):
  const_pathS i alpha beta → alpha = zero ∨ beta t1 < alpha.

Lemma Lemma_4_4_1 : ∀ s n alpha beta (Ha : nf alpha)
                           (Hb : nf beta),
                      sorted_ge n s →
                      const_pathS_eps n alpha beta →
                      const_pathS_eps (simple_last n s)
                              (gnawS alpha s) (gnawS beta s).

Lemma KP_arrowS_zero n beta : KP_arrowS n zero beta → beta = zero.

Lemma KP_5_iii n alpha beta: nf alpha → nf beta →
                              const_pathS n alpha beta ↔
                              KP_arrowS n alpha beta.

Lemma Lemma_4_4_0 :
  ∀ n p alpha beta (Halpha : alpha ≠ T1.zero),
    nf alpha → nf beta → (n ≤ p)%nat →
    const_pathS_eps n alpha beta →
    const_pathS_eps p (canon alpha (S p)) (canon beta (S p)).

Lemma standard_path_shift i alpha j beta :
  standard_pathS i alpha j beta →
  standard_path (S i) alpha (S j) beta.

Lemma standard_path_unshift_0 i alpha j beta :
   standard_path i alpha j beta → ∀ k l,
      i = S k → j = S l →
  standard_pathS k alpha l beta.

Lemma standard_path_unshift i alpha j beta :
  standard_path (S i) alpha (S j) beta →
  standard_pathS i alpha j beta.

Lemma standard_path_toS_le_inv : ∀ j beta i alpha,
    standard_path_toS j beta i alpha → (i ≤ j)%nat.

Lemma standard_path_to_le_inv : ∀ j beta i alpha,
    standard_path_to j beta i alpha → (i ≤ j)%nat.

Lemma standard_path_toS_zero : ∀ j beta i alpha,
    standard_path_toS j beta i alpha → alpha ≠ zero.

Lemma standard_path_origin : ∀ j beta i alpha,
   standard_path_to j beta i alpha → alpha ≠ zero.

Lemma standard_pathS_path_toS :
  ∀ i alpha j beta, standard_pathS i alpha j beta →
                         (i ≤ j)%nat →
                         path_toS beta (interval i j) alpha.

Lemma standard_path_path_to i alpha j beta :
  standard_path i alpha j beta → i ≠ 0 →
  (i ≤ j)%nat →
  path_to beta (interval i j) alpha.

Lemma standard_gnaw_zero l i : standard_gnaw i zero l = zero.

Lemma standard_gnaw_iota_from i alpha l :
  i ≠ 0 →
  standard_gnaw i alpha l = gnaw alpha (iota_from i l).

Lemma standard_gnaw_plus : ∀ (t1 t2 i:nat)(alpha : T1) ,
    standard_gnaw i alpha (t1 + t2)%nat =
    standard_gnaw (t1 +i)%nat (standard_gnaw i alpha t1) t2.

Lemma standard_path_LE : ∀ j beta i alpha,
    standard_path i alpha j beta → (i ≤ j)%nat.

Lemma standard_path_to_nf : ∀ i alpha j beta,
    standard_path_to j beta i alpha → nf alpha → nf beta.

Lemma standard_path_zero : ∀ i j alpha beta,
    standard_path i alpha j beta →
    alpha = zero →
    beta = zero.

Lemma standard_path_lt2 : ∀ i alpha j beta,
    (0 < i)%nat → zero t1 < alpha →
    standard_path_to j beta i alpha →
    beta t1 < alpha.

Lemma standard_path_compose j beta k gamma :
  standard_path (S j) beta k gamma →
  ∀ i alpha, standard_path i alpha j beta →
                   standard_path i alpha k gamma.

Lemma standard_gnaw_S_zero : ∀ i n alpha ,
      standard_gnaw n alpha i = zero → standard_gnaw n alpha (S i)=zero.

Lemma standard_gnaw_to_path : ∀ t alpha i,
    alpha ≠ zero → i ≠ 0 →
    standard_gnaw i alpha t ≠ zero →
    standard_path i alpha (t + i)%nat
                  (standard_gnaw i alpha (S t)).

Lemma standard_gnaw_nf l : ∀ i alpha,
  nf alpha → nf (standard_gnaw i alpha l).

Lemma standard_path_equiv_1 :
  ∀ i j alpha beta, standard_path i alpha j beta →
                         beta = standard_gnaw i alpha (S j - i)%nat.

Lemma standard_path_equiv_2 :
  ∀ l i alpha, i ≠ 0 →
                    let beta := standard_gnaw i alpha (S l)
                    in beta ≠ zero →
                       standard_path i alpha (l + i)%nat beta.

Lemma path_to_S_iota_from :
  ∀ l i alpha beta,
    path_toS beta (iota_from i (S l)) alpha →
    standard_path_toS (l + i)%nat beta i alpha.

Lemma path_to_S_standard_pathS :
  ∀ i j alpha beta, (i ≤ j)%nat →
    path_toS beta (interval i j) alpha →
    standard_pathS i alpha j beta.

Lemma path_toS_standardS_equiv i j alpha beta :
  (i ≤ j)%nat → path_toS beta (interval i j) alpha ↔
    standard_pathS i alpha j beta.

Lemma path_to_standard_equiv i j alpha beta :
  i ≠ 0 → (i ≤ j)%nat → path_to beta (interval i j) alpha ↔
    standard_path i alpha j beta.

Lemma standard_pathS_app i alpha j beta k gamma :
  (i ≤ j)%nat → (j ≤ k)%nat →
  standard_pathS i alpha j beta → standard_pathS (S j) beta k gamma →
  standard_pathS i alpha k gamma.

Lemma cons_standard_pathS : ∀ alpha n beta ,
    nf (T1.cons alpha n beta) → ∀ gamma i j,
    standard_pathS i beta j gamma → gamma ≠ 0 →
    standard_pathS i (T1.cons alpha n beta) j (T1.cons alpha n gamma).

Lemma cons_standard_path : ∀ alpha n beta ,
    nf (T1.cons alpha n beta) → ∀ gamma i j,
    standard_path i beta j gamma → gamma ≠ 0 → i ≠ 0 →
    standard_path i (T1.cons alpha n beta) j (T1.cons alpha n gamma).

Lemma flatten : ∀ (i:nat) alpha (j:nat) beta,
     standard_path i alpha j beta →
    nf alpha → zero t1 < alpha → (0 < i)%nat →
    const_path j alpha beta.

Lemma standard_gnaw_to_zero :
  ∀ alpha , nf alpha → ∀ i,
      {p :nat | standard_gnaw i alpha p = zero }.

Lemma standard_path_to_zero:
  ∀ alpha i, nf alpha → alpha ≠ zero →
                   {j : nat | standard_path (S i) alpha j zero }.
Lemma standard_gnaw_2_zero :
  ∀ alpha i, nf alpha →
                   {t : nat | standard_gnaw i alpha t = zero }.

This section is dedicated to the proof of Lemma p 300 of KS We associate to any path from alpha to beta with a constant index a path from alpha to beta with a sequence of indices n+1, n+2, n+3, ...

Section Constant_to_standard_Proof.
  Variables (alpha beta: T1) (n : nat).
  Hypotheses (Halpha: nf alpha) (Hpos : zero t1 < beta)
             (Hpa : const_pathS n alpha beta).

  Remark Rem0 : beta t1 < alpha.

  Remark Rem1 : {k :nat &
                   {gamma : T1 |
                    standard_path (S n) alpha k gamma ∧
                    gamma t1 < alpha }}.

  Remark Rem01 : zero t1 < alpha.

  Remark Rem02 : alpha ≠ zero.

  Remark Rem2 : {t : nat | standard_gnaw (S n) alpha t t1 < beta }.

  Let t := proj1_sig Rem2.

  Remark Rem03 : (standard_gnaw (S n) alpha t t1 < beta)%t1.

  Let P (i:nat) := compare (standard_gnaw (S n) alpha i) beta ≠ Datatypes.Lt.

  Remark Rem04 : P 0.

  Remark Rem05 : ¬ P t.

  Remark Rem06 : (0 < t)%nat.

  Instance P_dec i : Decision (P i).

  Let l_def := first_toggle P P_dec 0 t Rem06 Rem04 Rem05.

  Let l := proj1_sig l_def.

  Let gamma := standard_gnaw (S n) alpha l.

  Remark Rem08 :
    (0 ≤ l)%nat ∧
    (l < t)%nat ∧
    (∀ i : nat,
        (0 ≤ i)%nat →
        (i ≤ l)%nat → P i ) ∧ ¬ P (S l).

  Remark Rem09 : (l < t)%nat.

  Remark Rem10 : P l.

  Remark Rem11 : ¬ P (S l).

  Remark R12 : const_pathS (l +n) alpha beta.

  Remark R13 : (0 < l)%nat → gamma ≠ zero →
               standard_path (S n) alpha ((l + n)) gamma.

  Remark R14 : l = 0 → gamma = alpha.

  Remark R15 : gamma ≠ zero →
               (0 < l)%nat → const_path (n + l) alpha gamma.

  Let m := Nat.pred (n + l).

  Lemma m_def : (0 < l)%nat → (n + l = S m)%nat.

  Remark R16 : (0 < l)%nat → const_path (n + l) alpha beta.

   Remark R17 : (0 < l)%nat → const_pathS (n +l) alpha beta.

  Remark R18 : gamma ≠ zero → (0 < l)%nat → const_pathS (n +l) alpha gamma.

  Remark R19 : beta t1 ≤ gamma.

  Remark R20 : gamma ≠ zero → (0 < l)%nat → beta t1 < gamma →
               const_pathS (n +l) gamma beta.

  Remark R21 : gamma ≠ zero → (0 < l)%nat →
               gamma = beta ∨ const_pathS (n +l) gamma beta.

  Let delta := canon gamma (S (n + l))%nat.

  Remark R22 : delta = standard_gnaw (S n) alpha (S l).

  Remark R23 : const_pathS (n +l) gamma beta →
               {beta = delta }+{const_pathS (n + l) delta beta }.

  Remark R24 : const_pathS (n +l) gamma beta → beta t1 ≤ delta.

   Remark R25 : delta t1 < beta.

   Remark R26 : ¬ const_pathS (n +l) gamma beta.

   Remark R27 : gamma ≠ zero → (0 < l)%nat → gamma = beta.

   Remark R28 : l = 0 → (beta t1 ≤ delta)%t1.

  Remark R29 : l ≠ 0.

  Remark R30 : gamma ≠ zero → gamma = beta.

  Remark R31_0 : gamma ≠ zero → beta = standard_gnaw (S n) alpha l.

  Lemma gamma_positive : gamma ≠ zero.

  Remark R31 : beta = standard_gnaw (S n) alpha l.

  Lemma constant_to_standard_0 :
    {l : nat | standard_gnaw (S n) alpha l = beta }.

End Constant_to_standard_Proof.

Lemma constant_to_standard (alpha beta : T1) (n : nat):
    nf alpha → const_pathS n alpha beta →
    {l : nat | standard_gnaw (S n) alpha l = beta }.

Lemma constant_to_standard_path
  (alpha beta : T1) (i : nat):
  nf alpha → const_pathS i alpha beta → zero t1 < alpha →
  {j :nat | standard_path (S i) alpha j beta }.
Corollary LT_to_standard_path (alpha beta : T1) :
  beta t1 < alpha →
  {n : nat & {j :nat | standard_path (S n) alpha j beta }}.

Adaptation to E0

Definition Canon_plus (i:nat)( alpha beta:E0)
  := const_path i (cnf alpha) (cnf beta).

Lemma Canon_plus_inv n alpha beta :
  Canon_plus (S n) alpha beta →
  beta = Canon alpha (S n) ∨
  Canon_plus (S n) (Canon alpha (S n)) beta.

Theorem KS_thm_2_4_E0 :
  ∀ lambda,
    E0limit lambda →
    ∀ i j, (i < j)%nat →
                Canon_plus 1 (Canon lambda (S j))
                       (Canon lambda (S i)).

Corollary Cor12_E0 : ∀ alpha beta i n,
    E0lt beta alpha → (i ≤ n)%nat →
    Canon_plus (S i) alpha beta →
    Canon_plus (S n) alpha beta.

Lemma Canon_mono1 alpha i j : E0limit alpha → (i < j)% nat →
                              (Canon alpha i o < Canon alpha j)%e0.

Lemma CanonS_plus_1 alpha beta k i :
  beta ≠ E0zero → alpha ≠ E0zero →
  (beta o < E0_phi0 alpha)%e0 →
  (Canon (Omega_term alpha i + beta)%e0 (S k) =
   (Omega_term alpha i + (Canon beta (S k)))%e0).

Lemma CanonS_Phi0_Succ_eqn i gamma:
  Canon (E0_phi0 (E0_succ gamma)) (S i) = Omega_term gamma i.

Lemma Lemma2_6_1_E0 (alpha beta: E0) :
    (beta o < alpha)%e0 →
    {n :nat | Canon_plus (S n) alpha beta }.

Lemmas used by F_alpha

Lemma Canon_plus_first_step: ∀ i alpha beta,
    Canon_plus (S i) (E0_succ alpha) beta →
    alpha = beta ∨ Canon_plus (S i) alpha beta.

Lemma Canon_plus_first_step_lim:
  ∀ i alpha beta, E0limit alpha →
                       Canon_plus (S i) alpha beta →
                       beta = Canon alpha (S i) ∨
                       Canon_plus (S i) (Canon alpha (S i)) beta.