Library hydras.Hydra.Battle_length

From hydras Require Import L_alpha.
From hydras Require Import Hydra_Lemmas Epsilon0_Needed_Free
     Epsilon0_Needed_Std Hydra_Termination O2H.
Import E0 Large_Sets Hprime Paths MoreLists.

Section Battle_length.

  Variable alpha : E0.
  Hypothesis Halpha : alpha ≠ E0zero.
  Variable k : nat.
  Hypothesis Hk : (1 ≤ k)%nat.
  Let l := L_ alpha (S k).

  Remark R0 : (S k < l)%nat.


  Remark R2 : mlarge (cnf alpha) (interval (S k) (Nat.pred l)).


  Remark R3 : path_toS zero
                       (unshift (interval (S k) (Nat.pred l)))
                       (cnf alpha).

  Remark R4 :
    trace_to (O2H.iota zero)
             (unshift (interval (S k) (Nat.pred l)))
             (O2H.iota (cnf alpha)).

  Lemma R5 : trace_to (O2H.iota zero)
                      (interval k (Nat.pred (Nat.pred l)))
                      (O2H.iota (cnf alpha)).

  Remark R6 : S (Nat.pred (Nat.pred l)) = (l-1)%nat.

  Lemma L06: rounds standard k (iota (cnf alpha)) (l-1)%nat
                     (iota zero).


  Lemma battle_length_std:
    battle_length standard k (iota (cnf alpha)) (l-k)%nat.
End Battle_length.


Definition l_std alpha k := (L_ alpha (S k) - k)%nat.

Lemma l_std_ok : ∀ alpha : E0,
    alpha ≠ E0zero →
    ∀ k : nat,
      1 ≤ k → battle_length standard k (iota (cnf alpha))
                              (l_std alpha k).