Library hydras.Hydra.Epsilon0_Needed_Std

Pierre Castéran, LaBRI and University of Bordeaux

We prove that the impossibility result of Epsilon0_Needed_Free still holds for "standard" battles

From hydras Require Import Epsilon0_Needed_Generic.
Import Hydra_Lemmas Epsilon0 Canon Paths Relation_Operators O2H.
Import Hydra_Definitions.

Open Scope t1_scope.

Section Impossibility_Proof.

  Context (mu: T1)
          (m : Hydra → T1)
          (Var : Hvariant T1_wf standard m)
          (Hy : BoundedVariant Var mu).

  Let big_h := big_h mu.
  Let small_h := small_h mu m.

  Lemma m_ge : m big_h t1 ≤ m small_h.

Proof of the inequality m small_h t1< m big_h

The measure is strictly decreasing along any round

  Lemma Lvar : ∀ h h0 i,
      h ≠ head →
      battle_rel standard i h h0 → m h0 t1 < m h.

Application to standard battles

Lemma m_decrease : ∀ j h0 i h,
h ≠ head → rounds standard i h j h0 → m h0 t1 < m h.

Conversion of ordinal inequalities into standard battles

  Lemma LT_to_standard_battle :
    ∀ alpha beta,
      beta t1 < alpha →
      ∃ n i , rounds standard n (iota alpha) i (iota beta).
  Remark Rem3 : beta_h mu m t1 < mu.

  Remark Rem4 : ∃ n i ,
      rounds standard n (iota mu) i (iota (beta_h mu m)).

  Remark Hmu : nf mu.

  Lemma m_lt : m small_h t1 < m big_h.

End of the proof