Library hydras.Epsilon0.F_omega
About F_ omega
From hydras Require Import Iterates F_alpha E0 Ack AckNotPR.
From Coq Require Import ArithRing Lia Arith.
Import Exp2.
Open Scope nat_scope.
Lemma Ack_iterate_rw n p : Ack (S n) (S p) = iterate (Ack n) (S (S p)) 1.
Lemma F_iterate_rw n p : F_ (S n) (S p) = iterate (F_ n) (S (S p)) (S p).
Lemma L02 p: 2 ≤ p → 2 × p + 3 ≤ exp2 p × p.
Section inductive_step.
Variable n: nat.
Hypothesis Hn : ∀ p, 2 ≤ p → Ack n p ≤ F_ n p.
Lemma L: ∀ p, 2 ≤ p → Ack (S n) p ≤ F_ (S n) p.
End inductive_step.
Lemma L2 : ∀ n, 2 ≤ n → ∀ p, 2 ≤ p →
Ack n p ≤ F_ n p.
Lemma F_vs_Ack n : 2 ≤ n → Ack n n ≤ F_ E0_omega n.
Import primRec extEqualNat.
Section F_omega_notPR.
Context (F_omega_PR : isPR 1 (F_ E0_omega)).
Lemma F_omega_not_PR : False.
End F_omega_notPR.
Section F_alpha_notPR.
Variable alpha: E0.
Section case_lt.
Hypothesis Halpha : E0_omega o< alpha.
Remark R5: ∃ N, ∀ k, N ≤ k → F_ E0_omega k < F_ alpha k.
Context (H: isPR 1 (F_ alpha)).
Remark R00 : F_ alpha >> fun n ⇒ Ack n n.
Lemma FF : False.
End case_lt.
Hypothesis H : E0_omega o≤ alpha.
Context (H0: isPR 1 (F_ alpha)).
Lemma F_alpha_not_PR: False.
End F_alpha_notPR.
#[export] Instance F_0_isPR : isPR 1 (F_ 0).
Section step.
Variable n: nat.
Hypothesis Hn : isPR 1 (F_ n).
Let F := fun a b ⇒ nat_rec (fun _ ⇒ nat) a (fun x y ⇒ F_ n y) b.
Remark L00: ∀ i, F_ (E0_succ n) i = F i (S i) .
#[local] Instance R01 : isPR 2 F.
#[local] Instance R02 : isPR 1 (fun i ⇒ F i (S i)).
#[local] Instance R03 : isPR 1 (F_ (S n)).
End step.
#[export] Instance F_n_PR (n:nat) : isPR 1 (F_ n).
Keep in mind that isPR is of sort Set, so not and iff
cannot be used