Let X, n, e, x and r be given.
Assume HnO: n ∈ ω.
Assume HxX: x ∈ X.
Assume HtermR: ∀k : set, k ∈ n → apply_fun (apply_fun e k) x ∈ R.
Assume HrR: r ∈ R.
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 step' to be the term (λk acc : set ⇒ add_SNo acc (mul_SNo (apply_fun (apply_fun e k) x) r)).
Set P to be the term (λm : set ⇒ m ∈ ordsucc n → (nat_primrec 0 step m ∈ R ∧ nat_primrec 0 step' m ∈ R ∧ mul_SNo (nat_primrec 0 step m) r = nat_primrec 0 step' m)).
We prove the intermediate claim HP0: P 0.
Assume H0: 0 ∈ ordsucc n.
rewrite the current goal using (nat_primrec_0 0 step) (from left to right).
rewrite the current goal using (nat_primrec_0 0 step') (from left to right).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is real_0.
An exact proof term for the current goal is real_0.
We prove the intermediate claim HrS: SNo r.
An exact proof term for the current goal is (real_SNo r HrR).
An exact proof term for the current goal is (mul_SNo_zeroL r HrS).
We prove the intermediate claim HPS: ∀m : set, nat_p m → P m → P (ordsucc m).
Let m be given.
Assume HmNat: nat_p m.
Assume IH: P m.
Assume HmS: ordsucc m ∈ ordsucc n.
We prove the intermediate claim Hsub: ordsucc m ⊆ n.
An exact proof term for the current goal is (nat_ordsucc_trans n HnNat (ordsucc m) HmS).
We prove the intermediate claim HmInN: m ∈ n.
An exact proof term for the current goal is (Hsub m (ordsuccI2 m)).
We prove the intermediate claim HmInSuccN: m ∈ ordsucc n.
An exact proof term for the current goal is (ordsuccI1 n m HmInN).
We prove the intermediate claim HrS: SNo r.
An exact proof term for the current goal is (real_SNo r HrR).
We prove the intermediate claim HtermRm: apply_fun (apply_fun e m) x ∈ R.
An exact proof term for the current goal is (HtermR m HmInN).
We prove the intermediate claim HtermSm: 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) HtermRm).
We prove the intermediate claim HmulR: mul_SNo (apply_fun (apply_fun e m) x) r ∈ R.
An exact proof term for the current goal is (real_mul_SNo (apply_fun (apply_fun e m) x) HtermRm r HrR).
We prove the intermediate claim HmulS: SNo (mul_SNo (apply_fun (apply_fun e m) x) r).
An exact proof term for the current goal is (real_SNo (mul_SNo (apply_fun (apply_fun e m) x) r) HmulR).
We prove the intermediate claim HIHcore: (nat_primrec 0 step m ∈ R ∧ nat_primrec 0 step' m ∈ R) ∧ mul_SNo (nat_primrec 0 step m) r = nat_primrec 0 step' m.
An exact proof term for the current goal is (IH HmInSuccN).
We prove the intermediate claim HIHab: nat_primrec 0 step m ∈ R ∧ nat_primrec 0 step' m ∈ R.
An exact proof term for the current goal is (andEL (nat_primrec 0 step m ∈ R ∧ nat_primrec 0 step' m ∈ R) (mul_SNo (nat_primrec 0 step m) r = nat_primrec 0 step' m) HIHcore).
We prove the intermediate claim HsumRm: nat_primrec 0 step m ∈ R.
An exact proof term for the current goal is (andEL (nat_primrec 0 step m ∈ R) (nat_primrec 0 step' m ∈ R) HIHab).
We prove the intermediate claim HsumR'm: nat_primrec 0 step' m ∈ R.
An exact proof term for the current goal is (andER (nat_primrec 0 step m ∈ R) (nat_primrec 0 step' m ∈ R) HIHab).
We prove the intermediate claim HeqIH: mul_SNo (nat_primrec 0 step m) r = nat_primrec 0 step' m.
An exact proof term for the current goal is (andER (nat_primrec 0 step m ∈ R ∧ nat_primrec 0 step' m ∈ R) (mul_SNo (nat_primrec 0 step m) r = nat_primrec 0 step' m) HIHcore).
We prove the intermediate claim HsumSm: SNo (nat_primrec 0 step m).
An exact proof term for the current goal is (real_SNo (nat_primrec 0 step m) HsumRm).
We will prove ((nat_primrec 0 step (ordsucc m) ∈ R ∧ nat_primrec 0 step' (ordsucc m) ∈ R) ∧ mul_SNo (nat_primrec 0 step (ordsucc m)) r = nat_primrec 0 step' (ordsucc m)).
Apply andI to the current goal.
Apply andI to the current goal.
rewrite the current goal using (nat_primrec_S 0 step m HmNat) (from left to right).
An exact proof term for the current goal is (real_add_SNo (nat_primrec 0 step m) HsumRm (apply_fun (apply_fun e m) x) HtermRm).
rewrite the current goal using (nat_primrec_S 0 step' m HmNat) (from left to right).
An exact proof term for the current goal is (real_add_SNo (nat_primrec 0 step' m) HsumR'm (mul_SNo (apply_fun (apply_fun e m) x) r) HmulR).
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 step' m HmNat) (from left to right).
We prove the intermediate claim Hlhs: mul_SNo (add_SNo (nat_primrec 0 step m) (apply_fun (apply_fun e m) x)) r = add_SNo (mul_SNo (nat_primrec 0 step m) r) (mul_SNo (apply_fun (apply_fun e m) x) r).
An exact proof term for the current goal is (mul_SNo_distrR (nat_primrec 0 step m) (apply_fun (apply_fun e m) x) r HsumSm HtermSm HrS).
rewrite the current goal using Hlhs (from left to right).
rewrite the current goal using HeqIH (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).
An exact proof term for the current goal is (andER (nat_primrec 0 step n ∈ R ∧ nat_primrec 0 step' n ∈ R) (mul_SNo (nat_primrec 0 step n) r = nat_primrec 0 step' n) (HPn HnIn)).
∎