Let X, n, e, i and x be given.
Assume HnO: n ∈ ω.
Assume HiN: i ∈ n.
Assume HsiN: ordsucc i ∈ n.
Assume HxX: x ∈ X.
Assume HtermUI: ∀k : set, k ∈ n → apply_fun (apply_fun e k) x ∈ unit_interval.
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
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_adjacent e i n) k) x)).
Set base to be the term ordsucc (ordsucc i).
We prove the intermediate claim Hprefix: ∀k : set, k ∈ i → apply_fun (swap_adjacent e i n) k = apply_fun e k.
Let k be given.
Assume HkI: k ∈ i.
We prove the intermediate claim HkDom: k ∈ n.
An exact proof term for the current goal is (ordinal_TransSet n (ordinal_Hered ω omega_ordinal n HnO) i HiN k HkI).
We prove the intermediate claim Happ: apply_fun (swap_adjacent e i n) k = if k = i then apply_fun e (ordsucc i) else if k = ordsucc i then apply_fun e i else apply_fun e k.
An exact proof term for the current goal is (swap_adjacent_apply e i n k HkDom).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim Hki: ¬ (k = i).
Assume Heq: k = i.
We prove the intermediate claim Hii: i ∈ i.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is HkI.
An exact proof term for the current goal is ((In_irref i) Hii).
rewrite the current goal using (If_i_0 (k = i) (apply_fun e (ordsucc i)) (if k = ordsucc i then apply_fun e i else apply_fun e k) Hki) (from left to right).
We prove the intermediate claim Hksi: ¬ (k = ordsucc i).
Assume Heq: k = ordsucc i.
We prove the intermediate claim HsiIn: ordsucc i ∈ i.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is HkI.
We prove the intermediate claim HiOrd: ordinal i.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal i (omega_TransSet n HnO i HiN)).
We prove the intermediate claim HiTrans: TransSet i.
An exact proof term for the current goal is (ordinal_TransSet i HiOrd).
We prove the intermediate claim Hsub: ordsucc i ⊆ i.
An exact proof term for the current goal is (HiTrans (ordsucc i) HsiIn).
We prove the intermediate claim Hii: i ∈ i.
An exact proof term for the current goal is (Hsub i (ordsuccI2 i)).
An exact proof term for the current goal is ((In_irref i) Hii).
rewrite the current goal using (If_i_0 (k = ordsucc i) (apply_fun e i) (apply_fun e k) Hksi) (from left to right).
Use reflexivity.
We prove the intermediate claim Hsum_i: nat_primrec 0 stepS i = nat_primrec 0 step i.
We prove the intermediate claim HiOrd: ordinal i.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal i (omega_TransSet n HnO i HiN)).
We prove the intermediate claim HiNat: nat_p i.
An exact proof term for the current goal is (omega_nat_p i (omega_TransSet n HnO i HiN)).
We prove the intermediate claim Heq: ∀k : set, k ∈ i → apply_fun (swap_adjacent e i n) k = apply_fun e k.
Let k be given.
Assume HkI: k ∈ i.
An exact proof term for the current goal is (Hprefix k HkI).
An exact proof term for the current goal is (nat_primrec_sum_congr_on X i (swap_adjacent e i n) e x HiNat HxX Heq).
Set P to be the term (λt : set ⇒ t ∈ ordsucc n → (base ⊆ t → nat_primrec 0 stepS t = nat_primrec 0 step t)).
We prove the intermediate claim HP0: P 0.
Assume H0In: 0 ∈ ordsucc n.
Assume Hsub: base ⊆ 0.
Apply FalseE to the current goal.
We prove the intermediate claim Hb: ordsucc i ∈ base.
An exact proof term for the current goal is (ordsuccI2 (ordsucc i)).
We prove the intermediate claim Hb0: ordsucc i ∈ 0.
An exact proof term for the current goal is (Hsub (ordsucc i) Hb).
An exact proof term for the current goal is (EmptyE (ordsucc i) Hb0).
We prove the intermediate claim HPS: ∀t : set, nat_p t → P t → P (ordsucc t).
Let t be given.
Assume HtNat: nat_p t.
Assume IH: P t.
Assume HtSIn: ordsucc t ∈ ordsucc n.
Assume Hsub: base ⊆ ordsucc t.
We will prove nat_primrec 0 stepS (ordsucc t) = nat_primrec 0 step (ordsucc t).
Apply (xm (t = ordsucc i)) to the current goal.
Assume HtEq: t = ordsucc i.
rewrite the current goal using HtEq (from left to right).
We prove the intermediate claim HiNat: nat_p i.
An exact proof term for the current goal is (omega_nat_p i (omega_TransSet n HnO i HiN)).
We prove the intermediate claim HsiNat: nat_p (ordsucc i).
An exact proof term for the current goal is (nat_ordsucc i HiNat).
rewrite the current goal using (nat_primrec_S 0 step (ordsucc i) HsiNat) (from left to right).
rewrite the current goal using (nat_primrec_S 0 step i HiNat) (from left to right).
rewrite the current goal using (nat_primrec_S 0 stepS (ordsucc i) HsiNat) (from left to right).
rewrite the current goal using (nat_primrec_S 0 stepS i HiNat) (from left to right).
rewrite the current goal using Hsum_i (from left to right).
We prove the intermediate claim HsiDom: ordsucc i ∈ n.
An exact proof term for the current goal is HsiN.
We prove the intermediate claim HiDom: i ∈ n.
An exact proof term for the current goal is HiN.
We prove the intermediate claim Happ_i: apply_fun (swap_adjacent e i n) i = apply_fun e (ordsucc i).
We prove the intermediate claim Hsa: apply_fun (swap_adjacent e i n) i = if i = i then apply_fun e (ordsucc i) else if i = ordsucc i then apply_fun e i else apply_fun e i.
An exact proof term for the current goal is (swap_adjacent_apply e i n i HiDom).
rewrite the current goal using Hsa (from left to right).
We prove the intermediate claim Hii: i = i.
Use reflexivity.
rewrite the current goal using (If_i_1 (i = i) (apply_fun e (ordsucc i)) (if i = ordsucc i then apply_fun e i else apply_fun e i) Hii) (from left to right).
Use reflexivity.
We prove the intermediate claim Happ_si: apply_fun (swap_adjacent e i n) (ordsucc i) = apply_fun e i.
An exact proof term for the current goal is (swap_adjacent_at_succ e i n HsiDom).
rewrite the current goal using Happ_si (from left to right).
rewrite the current goal using Happ_i (from left to right).
We prove the intermediate claim Hsum_i_R: nat_primrec 0 step i ∈ R.
We prove the intermediate claim HiO: i ∈ ω.
An exact proof term for the current goal is (omega_TransSet n HnO i HiN).
We prove the intermediate claim HtermR: ∀k : set, k ∈ i → apply_fun (apply_fun e k) x ∈ R.
Let k be given.
Assume HkI: k ∈ i.
We prove the intermediate claim HkN: k ∈ n.
An exact proof term for the current goal is (ordinal_TransSet n (ordinal_Hered ω omega_ordinal n HnO) i HiN k HkI).
An exact proof term for the current goal is (unit_interval_sub_R (apply_fun (apply_fun e k) x) (HtermUI k HkN)).
We prove the intermediate claim Hterm0: ∀k : set, k ∈ i → Rle 0 (apply_fun (apply_fun e k) x).
Let k be given.
Assume HkI: k ∈ i.
We prove the intermediate claim HkN: k ∈ n.
An exact proof term for the current goal is (ordinal_TransSet n (ordinal_Hered ω omega_ordinal n HnO) i HiN k HkI).
An exact proof term for the current goal is (unit_interval_Rle0 (apply_fun (apply_fun e k) x) (HtermUI k HkN)).
An exact proof term for the current goal is (andEL (nat_primrec 0 step i ∈ R) (Rle 0 (nat_primrec 0 step i)) (nat_primrec_sum_Rle0_of_Rle0_terms X i e x HiO HxX HtermR Hterm0)).
We prove the intermediate claim Hsum_i_S: SNo (nat_primrec 0 step i).
An exact proof term for the current goal is (real_SNo (nat_primrec 0 step i) Hsum_i_R).
We prove the intermediate claim Hterm_i_R: apply_fun (apply_fun e i) x ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R (apply_fun (apply_fun e i) x) (HtermUI i HiN)).
We prove the intermediate claim Hterm_si_R: apply_fun (apply_fun e (ordsucc i)) x ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R (apply_fun (apply_fun e (ordsucc i)) x) (HtermUI (ordsucc i) HsiN)).
We prove the intermediate claim Hterm_i_S: SNo (apply_fun (apply_fun e i) x).
An exact proof term for the current goal is (real_SNo (apply_fun (apply_fun e i) x) Hterm_i_R).
We prove the intermediate claim Hterm_si_S: SNo (apply_fun (apply_fun e (ordsucc i)) x).
An exact proof term for the current goal is (real_SNo (apply_fun (apply_fun e (ordsucc i)) x) Hterm_si_R).
We prove the intermediate claim Hcom3: add_SNo (add_SNo (nat_primrec 0 step i) (apply_fun (apply_fun e (ordsucc i)) x)) (apply_fun (apply_fun e i) x) = add_SNo (add_SNo (nat_primrec 0 step i) (apply_fun (apply_fun e i) x)) (apply_fun (apply_fun e (ordsucc i)) x).
An exact proof term for the current goal is (add_SNo_com_3b_1_2 (nat_primrec 0 step i) (apply_fun (apply_fun e (ordsucc i)) x) (apply_fun (apply_fun e i) x) Hsum_i_S Hterm_si_S Hterm_i_S).
rewrite the current goal using Hcom3 (from left to right).
Use reflexivity.
Assume HtNeq: ¬ (t = ordsucc i).
We prove the intermediate claim HsiInSucc: ordsucc i ∈ ordsucc t.
An exact proof term for the current goal is (Hsub (ordsucc i) (ordsuccI2 (ordsucc i))).
We prove the intermediate claim Hcase: ordsucc i ∈ t ∨ ordsucc i = t.
An exact proof term for the current goal is (ordsuccE t (ordsucc i) HsiInSucc).
We prove the intermediate claim HsiInT: ordsucc i ∈ t.
Apply (Hcase (ordsucc i ∈ t)) to the current goal.
Assume H: ordsucc i ∈ t.
An exact proof term for the current goal is H.
Assume Heq: ordsucc i = t.
Apply FalseE to the current goal.
We prove the intermediate claim Heq2: t = ordsucc i.
Use symmetry.
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (HtNeq Heq2).
We prove the intermediate claim HtInN: t ∈ n.
We prove the intermediate claim HstIn: ordsucc t ∈ n ∨ ordsucc t = n.
An exact proof term for the current goal is (ordsuccE n (ordsucc t) HtSIn).
Apply (HstIn (t ∈ n)) to the current goal.
Assume HstInN: ordsucc t ∈ n.
We prove the intermediate claim HnOrd: ordinal n.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal n HnO).
We prove the intermediate claim HnTrans: TransSet n.
An exact proof term for the current goal is (ordinal_TransSet n HnOrd).
We prove the intermediate claim Hsub: ordsucc t ⊆ n.
An exact proof term for the current goal is (HnTrans (ordsucc t) HstInN).
An exact proof term for the current goal is (Hsub t (ordsuccI2 t)).
Assume HstEq: ordsucc t = n.
rewrite the current goal using HstEq (from right to left).
An exact proof term for the current goal is (ordsuccI2 t).
We prove the intermediate claim HtOrd: ordinal t.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal t (omega_TransSet n HnO t HtInN)).
We prove the intermediate claim HtTrans: TransSet t.
An exact proof term for the current goal is (ordinal_TransSet t HtOrd).
We prove the intermediate claim HbaseSubT: base ⊆ t.
Let z be given.
Assume Hz: z ∈ base.
Apply (xm (z = ordsucc i)) to the current goal.
Assume Heq: z = ordsucc i.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HsiInT.
Assume Hneq: ¬ (z = ordsucc i).
We prove the intermediate claim HzInSucc: z ∈ ordsucc (ordsucc i).
An exact proof term for the current goal is Hz.
We prove the intermediate claim HzInOr: z ∈ ordsucc i ∨ z = ordsucc i.
An exact proof term for the current goal is (ordsuccE (ordsucc i) z HzInSucc).
We prove the intermediate claim HzInOi: z ∈ ordsucc i.
Apply (HzInOr (z ∈ ordsucc i)) to the current goal.
Assume H: z ∈ ordsucc i.
An exact proof term for the current goal is H.
Assume Heq: z = ordsucc i.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hneq Heq).
We prove the intermediate claim HsubOi: ordsucc i ⊆ t.
An exact proof term for the current goal is (HtTrans (ordsucc i) HsiInT).
An exact proof term for the current goal is (HsubOi z HzInOi).
We prove the intermediate claim Heq_t: nat_primrec 0 stepS t = nat_primrec 0 step t.
An exact proof term for the current goal is (IH (ordsuccI1 n t HtInN) HbaseSubT).
rewrite the current goal using (nat_primrec_S 0 step t HtNat) (from left to right).
rewrite the current goal using (nat_primrec_S 0 stepS t HtNat) (from left to right).
rewrite the current goal using Heq_t (from left to right).
We prove the intermediate claim HtDom: t ∈ n.
An exact proof term for the current goal is HtInN.
We prove the intermediate claim HtNeqI: ¬ (t = i).
Assume Heq: t = i.
We prove the intermediate claim HsiInI: ordsucc i ∈ i.
rewrite the current goal using Heq (from right to left) at position 2.
An exact proof term for the current goal is HsiInT.
We prove the intermediate claim HiOrd: ordinal i.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal i (omega_TransSet n HnO i HiN)).
We prove the intermediate claim HiTrans: TransSet i.
An exact proof term for the current goal is (ordinal_TransSet i HiOrd).
We prove the intermediate claim Hsub: ordsucc i ⊆ i.
An exact proof term for the current goal is (HiTrans (ordsucc i) HsiInI).
We prove the intermediate claim Hii: i ∈ i.
An exact proof term for the current goal is (Hsub i (ordsuccI2 i)).
An exact proof term for the current goal is ((In_irref i) Hii).
We prove the intermediate claim HtNeqSi: ¬ (t = ordsucc i).
Assume Heq: t = ordsucc i.
An exact proof term for the current goal is (HtNeq Heq).
We prove the intermediate claim Hsame: apply_fun (swap_adjacent e i n) t = apply_fun e t.
rewrite the current goal using (swap_adjacent_apply e i n t HtDom) (from left to right).
rewrite the current goal using (If_i_0 (t = i) (apply_fun e (ordsucc i)) (if t = ordsucc i then apply_fun e i else apply_fun e t) HtNeqI) (from left to right).
rewrite the current goal using (If_i_0 (t = ordsucc i) (apply_fun e i) (apply_fun e t) HtNeqSi) (from left to right).
Use reflexivity.
rewrite the current goal using Hsame (from left to right).
Use reflexivity.
We prove the intermediate claim HPn: P n.
An exact proof term for the current goal is (nat_ind P HP0 HPS n HnNat).
We prove the intermediate claim HnIn: n ∈ ordsucc n.
An exact proof term for the current goal is (ordsuccI2 n).
We prove the intermediate claim HbaseSubN: base ⊆ n.
We prove the intermediate claim HnOrd: ordinal n.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal n HnO).
We prove the intermediate claim HnTrans: TransSet n.
An exact proof term for the current goal is (ordinal_TransSet n HnOrd).
We prove the intermediate claim HsubOi: ordsucc i ⊆ n.
An exact proof term for the current goal is (HnTrans (ordsucc i) HsiN).
Let z be given.
Assume Hz: z ∈ base.
Apply (xm (z = ordsucc i)) to the current goal.
Assume Heq: z = ordsucc i.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HsiN.
Assume Hneq: ¬ (z = ordsucc i).
We prove the intermediate claim HzInOr: z ∈ ordsucc i ∨ z = ordsucc i.
An exact proof term for the current goal is (ordsuccE (ordsucc i) z Hz).
We prove the intermediate claim HzInOi: z ∈ ordsucc i.
Apply (HzInOr (z ∈ ordsucc i)) to the current goal.
Assume H: z ∈ ordsucc i.
An exact proof term for the current goal is H.
Assume Heq: z = ordsucc i.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hneq Heq).
An exact proof term for the current goal is (HsubOi z HzInOi).
An exact proof term for the current goal is (HPn HnIn HbaseSubN).
∎