Let X, m, e and x be given.
Assume HmO: m ∈ ω.
Assume HxX: x ∈ X.
Assume HtermUI: ∀k : set, k ∈ ordsucc (ordsucc m) → apply_fun (apply_fun e k) x ∈ unit_interval.
We prove the intermediate claim HmNat: nat_p m.
An exact proof term for the current goal is (omega_nat_p m HmO).
We prove the intermediate claim HsmNat: nat_p (ordsucc m).
An exact proof term for the current goal is (nat_ordsucc m HmNat).
Set step to be the term (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)).
Set stepS to be the term (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun (swap_last_two e m) k) x)).
We prove the intermediate claim Hprefix: ∀k : set, k ∈ m → apply_fun (swap_last_two e m) k = apply_fun e k.
Let k be given.
Assume HkM: k ∈ m.
We prove the intermediate claim HkDom: k ∈ ordsucc (ordsucc m).
An exact proof term for the current goal is (ordsuccI1 (ordsucc m) k (ordsuccI1 m k HkM)).
We prove the intermediate claim Happ: apply_fun (swap_last_two e m) k = if k = m then apply_fun e (ordsucc m) else if k = ordsucc m then apply_fun e m else apply_fun e k.
An exact proof term for the current goal is (swap_last_two_apply e m k HkDom).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim Hkm: ¬ (k = m).
Assume Heq: k = m.
We prove the intermediate claim Hmm: m ∈ m.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is HkM.
An exact proof term for the current goal is ((In_irref m) Hmm).
rewrite the current goal using (If_i_0 (k = m) (apply_fun e (ordsucc m)) (if k = ordsucc m then apply_fun e m else apply_fun e k) Hkm) (from left to right).
We prove the intermediate claim Hksm: ¬ (k = ordsucc m).
Assume Heq: k = ordsucc m.
We prove the intermediate claim HkIn: ordsucc m ∈ m.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is HkM.
We prove the intermediate claim HmOrd: ordinal m.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal m HmO).
We prove the intermediate claim HmTrans: TransSet m.
An exact proof term for the current goal is (ordinal_TransSet m HmOrd).
We prove the intermediate claim Hsub: ordsucc m ⊆ m.
An exact proof term for the current goal is (HmTrans (ordsucc m) HkIn).
We prove the intermediate claim Hmm: m ∈ m.
An exact proof term for the current goal is (Hsub m (ordsuccI2 m)).
An exact proof term for the current goal is ((In_irref m) Hmm).
rewrite the current goal using (If_i_0 (k = ordsucc m) (apply_fun e m) (apply_fun e k) Hksm) (from left to right).
Use reflexivity.
We prove the intermediate claim Hsum_m: nat_primrec 0 step m = nat_primrec 0 stepS m.
We prove the intermediate claim HmNat2: nat_p m.
An exact proof term for the current goal is HmNat.
We prove the intermediate claim Heq: ∀k : set, k ∈ m → apply_fun e k = apply_fun (swap_last_two e m) k.
Let k be given.
Assume HkM: k ∈ m.
Use symmetry.
An exact proof term for the current goal is (Hprefix k HkM).
An exact proof term for the current goal is (nat_primrec_sum_congr_on X m e (swap_last_two e m) x HmNat2 HxX Heq).
We prove the intermediate claim Hterm_m_UI: apply_fun (apply_fun e m) x ∈ unit_interval.
An exact proof term for the current goal is (HtermUI m (ordsuccI1 (ordsucc m) m (ordsuccI2 m))).
We prove the intermediate claim Hterm_sm_UI: apply_fun (apply_fun e (ordsucc m)) x ∈ unit_interval.
An exact proof term for the current goal is (HtermUI (ordsucc m) (ordsuccI2 (ordsucc m))).
We prove the intermediate claim Hterm_m_R: apply_fun (apply_fun e m) x ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R (apply_fun (apply_fun e m) x) Hterm_m_UI).
We prove the intermediate claim Hterm_sm_R: apply_fun (apply_fun e (ordsucc m)) x ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R (apply_fun (apply_fun e (ordsucc m)) x) Hterm_sm_UI).
We prove the intermediate claim Hsum_m_R: nat_primrec 0 step m ∈ R.
We prove the intermediate claim HmO2: m ∈ ω.
An exact proof term for the current goal is HmO.
We prove the intermediate claim HtermR: ∀k : set, k ∈ m → apply_fun (apply_fun e k) x ∈ R.
Let k be given.
Assume HkM: k ∈ m.
We prove the intermediate claim HkDom: k ∈ ordsucc (ordsucc m).
An exact proof term for the current goal is (ordsuccI1 (ordsucc m) k (ordsuccI1 m k HkM)).
An exact proof term for the current goal is (unit_interval_sub_R (apply_fun (apply_fun e k) x) (HtermUI k HkDom)).
We prove the intermediate claim Hterm0: ∀k : set, k ∈ m → Rle 0 (apply_fun (apply_fun e k) x).
Let k be given.
Assume HkM: k ∈ m.
We prove the intermediate claim HkDom: k ∈ ordsucc (ordsucc m).
An exact proof term for the current goal is (ordsuccI1 (ordsucc m) k (ordsuccI1 m k HkM)).
An exact proof term for the current goal is (unit_interval_Rle0 (apply_fun (apply_fun e k) x) (HtermUI k HkDom)).
An exact proof term for the current goal is (andEL (nat_primrec 0 step m ∈ R) (Rle 0 (nat_primrec 0 step m)) (nat_primrec_sum_Rle0_of_Rle0_terms X m e x HmO2 HxX HtermR Hterm0)).
We prove the intermediate claim Hsum_m_S: SNo (nat_primrec 0 step m).
An exact proof term for the current goal is (real_SNo (nat_primrec 0 step m) Hsum_m_R).
We prove the intermediate claim Hterm_m_S: SNo (apply_fun (apply_fun e m) x).
An exact proof term for the current goal is (real_SNo (apply_fun (apply_fun e m) x) Hterm_m_R).
We prove the intermediate claim Hterm_sm_S: SNo (apply_fun (apply_fun e (ordsucc m)) x).
An exact proof term for the current goal is (real_SNo (apply_fun (apply_fun e (ordsucc m)) x) Hterm_sm_R).
rewrite the current goal using (nat_primrec_S 0 step (ordsucc m) HsmNat) (from left to right).
rewrite the current goal using (nat_primrec_S 0 step m HmNat) (from left to right).
rewrite the current goal using (nat_primrec_S 0 stepS (ordsucc m) HsmNat) (from left to right).
rewrite the current goal using (nat_primrec_S 0 stepS m HmNat) (from left to right).
rewrite the current goal using Hsum_m (from right to left).
We prove the intermediate claim Hswap_m: apply_fun (swap_last_two e m) m = apply_fun e (ordsucc m).
An exact proof term for the current goal is (swap_last_two_at_m e m HmNat).
We prove the intermediate claim Hswap_sm: apply_fun (swap_last_two e m) (ordsucc m) = apply_fun e m.
An exact proof term for the current goal is (swap_last_two_at_sm e m HmNat).
rewrite the current goal using Hswap_sm (from left to right).
rewrite the current goal using Hswap_m (from left to right).
We prove the intermediate claim Hcom3: add_SNo (add_SNo (nat_primrec 0 step m) (apply_fun (apply_fun e (ordsucc m)) x)) (apply_fun (apply_fun e m) x) = add_SNo (add_SNo (nat_primrec 0 step m) (apply_fun (apply_fun e m) x)) (apply_fun (apply_fun e (ordsucc m)) x).
An exact proof term for the current goal is (add_SNo_com_3b_1_2 (nat_primrec 0 step m) (apply_fun (apply_fun e (ordsucc m)) x) (apply_fun (apply_fun e m) x) Hsum_m_S Hterm_sm_S Hterm_m_S).
rewrite the current goal using Hcom3 (from left to right).
Use reflexivity.
∎