We will
prove equip {x ∈ SNoS_ ω|SNoLev x = 0} (2 ^ 0).
rewrite the current goal using
exp_SNo_nat_0 2 SNo_2 (from left to right).
We will prove equip {x ∈ SNoS_ ω|SNoLev x = 0} 1.
Apply equip_sym to the current goal.
We will prove ∃f : set → set, bij 1 {x ∈ SNoS_ ω|SNoLev x = 0} f.
Set f to be the term λi : set ⇒ 0.
We use f to witness the existential quantifier.
Apply bijI to the current goal.
Let i be given.
We will
prove 0 ∈ {x ∈ SNoS_ ω|SNoLev x = 0}.
Apply SepI to the current goal.
We will
prove 0 ∈ SNoS_ ω.
Apply SNoS_I ω omega_ordinal 0 0 (nat_p_omega 0 nat_0) to the current goal.
We will prove SNo_ 0 0.
An exact proof term for the current goal is ordinal_SNo_ 0 ordinal_Empty.
We will prove SNoLev 0 = 0.
An exact proof term for the current goal is SNoLev_0.
Let i be given.
Let j be given.
Assume Hij: 0 = 0.
We will prove i = j.
Apply cases_1 i Hi to the current goal.
Apply cases_1 j Hj to the current goal.
We will prove 0 = 0.
An exact proof term for the current goal is Hij.
Let x be given.
Apply SepE (SNoS_ ω) (λx ⇒ SNoLev x = 0) x Hx to the current goal.
Assume Hx2: SNoLev x = 0.
Apply SNoS_E2 ω omega_ordinal x Hx1 to the current goal.
Assume Hx1b: ordinal (SNoLev x).
Assume Hx1c: SNo x.
Assume Hx1d: SNo_ (SNoLev x) x.
We prove the intermediate claim L1: x = 0.
Use symmetry.
Apply SNo_eq 0 x SNo_0 Hx1c to the current goal.
We will prove SNoLev 0 = SNoLev x.
rewrite the current goal using SNoLev_0 (from left to right).
Use symmetry.
An exact proof term for the current goal is Hx2.
We will prove SNoEq_ (SNoLev 0) 0 x.
rewrite the current goal using SNoLev_0 (from left to right).
Let alpha be given.
We will prove False.
An exact proof term for the current goal is EmptyE alpha Ha.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is In_0_1.
We will prove 0 = x.
Use symmetry.
An exact proof term for the current goal is L1.
Let n be given.
Assume Hn.
We will
prove equip {x ∈ SNoS_ ω|SNoLev x = ordsucc n} (2 ^ ordsucc n).
rewrite the current goal using
exp_SNo_nat_S 2 SNo_2 n Hn (from left to right).
We will
prove equip {x ∈ SNoS_ ω|SNoLev x = ordsucc n} (2 * 2 ^ n).
rewrite the current goal using add_SNo_1_1_2 (from right to left) at position 1.
We will
prove equip {x ∈ SNoS_ ω|SNoLev x = ordsucc n} ((1 + 1) * 2 ^ n).
We will
prove equip {x ∈ SNoS_ ω|SNoLev x = ordsucc n} (2 ^ n + 2 ^ n).
We prove the intermediate
claim L2n1:
nat_p (2 ^ n).
We prove the intermediate
claim L2n2:
ordinal (2 ^ n).
Apply nat_p_ordinal to the current goal.
An exact proof term for the current goal is L2n1.
We prove the intermediate
claim L2n3:
SNo (2 ^ n).
Apply ordinal_SNo to the current goal.
An exact proof term for the current goal is L2n2.
We prove the intermediate
claim L2n2n1:
nat_p (2 ^ n + 2 ^ n).
Apply omega_nat_p to the current goal.
Apply add_SNo_In_omega to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is L2n1.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is L2n1.
We prove the intermediate
claim L2n2n2:
ordinal (2 ^ n + 2 ^ n).
Apply nat_p_ordinal to the current goal.
An exact proof term for the current goal is L2n2n1.
We prove the intermediate
claim L2n2n3:
SNo (2 ^ n + 2 ^ n).
Apply ordinal_SNo to the current goal.
An exact proof term for the current goal is L2n2n2.
We prove the intermediate
claim L2npLt2n2n:
∀m, SNo m → m < 2 ^ n → 2 ^ n + m < 2 ^ n + 2 ^ n.
Let m be given.
Assume Hm H1.
An
exact proof term for the current goal is
add_SNo_Lt2 (2 ^ n) m (2 ^ n) L2n3 Hm L2n3 H1.
We prove the intermediate
claim L2nLt2n2n:
2 ^ n < 2 ^ n + 2 ^ n.
rewrite the current goal using
add_SNo_0R (2 ^ n) L2n3 (from right to left) at position 1.
We will
prove 2 ^ n + 0 < 2 ^ n + 2 ^ n.
Apply L2npLt2n2n 0 SNo_0 to the current goal.
An
exact proof term for the current goal is
exp_SNo_nat_pos 2 SNo_2 SNoLt_0_2 n Hn.
Apply IHn to the current goal.
Let f be given.
Apply bijE {x ∈ SNoS_ ω|SNoLev x = n} (2 ^ n) f Hf to the current goal.
We prove the intermediate
claim L2:
∀x ∈ {x ∈ SNoS_ ω|SNoLev x = ordsucc n}, ∀p : prop, (SNo x → SNoLev x = ordsucc n → (x ∩ SNoElts_ n) ∈ {x ∈ SNoS_ ω|SNoLev x = n} → SNo (x ∩ SNoElts_ n) → SNoLev (x ∩ SNoElts_ n) = n → p) → p.
Let x be given.
Assume Hx.
Apply SepE (SNoS_ ω) (λx ⇒ SNoLev x = ordsucc n) x Hx to the current goal.
Assume Hx HxSn.
Apply SNoS_E2 ω omega_ordinal x Hx to the current goal.
Assume Hx2: ordinal (SNoLev x).
Assume Hx3: SNo x.
Assume Hx4: SNo_ (SNoLev x) x.
Let p be given.
Assume Hp.
We prove the intermediate
claim L2a:
n ∈ SNoLev x.
rewrite the current goal using HxSn (from left to right).
Apply ordsuccI2 to the current goal.
We prove the intermediate claim L2b: SNoLev (x ∩ SNoElts_ n) = n.
An exact proof term for the current goal is restr_SNoLev x Hx3 n L2a.
Apply Hp to the current goal.
An exact proof term for the current goal is Hx3.
An exact proof term for the current goal is HxSn.
Apply SepI to the current goal.
We will
prove (x ∩ SNoElts_ n) ∈ SNoS_ ω.
Apply SNoS_I ω omega_ordinal (x ∩ SNoElts_ n) n (nat_p_omega n Hn) to the current goal.
We will prove SNo_ n (x ∩ SNoElts_ n).
An exact proof term for the current goal is restr_SNo_ x Hx3 n L2a.
We will prove SNoLev (x ∩ SNoElts_ n) = n.
An exact proof term for the current goal is L2b.
An exact proof term for the current goal is restr_SNo x Hx3 n L2a.
An exact proof term for the current goal is L2b.
We prove the intermediate
claim Lf:
∀u ∈ {x ∈ SNoS_ ω|SNoLev x = ordsucc n}, ∀p : prop, (nat_p (f (u ∩ SNoElts_ n)) → ordinal (f (u ∩ SNoElts_ n)) → SNo (f (u ∩ SNoElts_ n)) → f (u ∩ SNoElts_ n) < 2 ^ n → p) → p.
Let u be given.
Assume Hu.
Let p be given.
Assume Hp.
Apply L2 u Hu to the current goal.
Assume Hu0a: SNo u.
Assume Hu0b: SNoLev u = ordsucc n.
Assume Hu2: SNo (u ∩ SNoElts_ n).
Assume Hu3: SNoLev (u ∩ SNoElts_ n) = n.
We prove the intermediate
claim Lf1a:
f (u ∩ SNoElts_ n) ∈ 2 ^ n.
An exact proof term for the current goal is Hf1 (u ∩ SNoElts_ n) Hu1.
We prove the intermediate claim Lf1b: nat_p (f (u ∩ SNoElts_ n)).
An
exact proof term for the current goal is
nat_p_trans (2 ^ n) L2n1 (f (u ∩ SNoElts_ n)) Lf1a.
We prove the intermediate claim Lf1c: ordinal (f (u ∩ SNoElts_ n)).
An exact proof term for the current goal is nat_p_ordinal (f (u ∩ SNoElts_ n)) Lf1b.
Apply Hp to the current goal.
An exact proof term for the current goal is Lf1b.
An exact proof term for the current goal is Lf1c.
Apply ordinal_SNo to the current goal.
An exact proof term for the current goal is Lf1c.
Apply ordinal_In_SNoLt to the current goal.
We will
prove ordinal (2 ^ n).
An exact proof term for the current goal is L2n2.
We will
prove f (u ∩ SNoElts_ n) ∈ 2 ^ n.
An exact proof term for the current goal is Lf1a.
We prove the intermediate
claim Lg:
∃g : set → set, (∀x, n ∈ x → g x = f (x ∩ SNoElts_ n)) ∧ (∀x, n ∉ x → g x = 2 ^ n + f (x ∩ SNoElts_ n)).
We use
(λx ⇒ if n ∈ x then f (x ∩ SNoElts_ n) else 2 ^ n + f (x ∩ SNoElts_ n)) to
witness the existential quantifier.
Apply andI to the current goal.
Let x be given.
An
exact proof term for the current goal is
If_i_1 (n ∈ x) (f (x ∩ SNoElts_ n)) (2 ^ n + f (x ∩ SNoElts_ n)) H1.
Let x be given.
Assume H1: n ∉ x.
An
exact proof term for the current goal is
If_i_0 (n ∈ x) (f (x ∩ SNoElts_ n)) (2 ^ n + f (x ∩ SNoElts_ n)) H1.
Apply Lg to the current goal.
Let g be given.
Assume H.
Apply H to the current goal.
We will
prove ∃g : set → set, bij {x ∈ SNoS_ ω|SNoLev x = ordsucc n} (2 ^ n + 2 ^ n) g.
We use g to witness the existential quantifier.
Apply bijI to the current goal.
Let u be given.
We will
prove g u ∈ 2 ^ n + 2 ^ n.
Apply L2 u Hu to the current goal.
Assume Hu0a: SNo u.
Assume Hu0b: SNoLev u = ordsucc n.
Assume Hu2: SNo (u ∩ SNoElts_ n).
Assume Hu3: SNoLev (u ∩ SNoElts_ n) = n.
Apply Lf u Hu to the current goal.
Assume Lfu1: nat_p (f (u ∩ SNoElts_ n)).
Assume Lfu2: ordinal (f (u ∩ SNoElts_ n)).
Assume Lfu3: SNo (f (u ∩ SNoElts_ n)).
Apply xm (n ∈ u) to the current goal.
rewrite the current goal using Hg1 u H1 (from left to right).
We will
prove f (u ∩ SNoElts_ n) ∈ 2 ^ n + 2 ^ n.
Apply ordinal_SNoLt_In (f (u ∩ SNoElts_ n)) (2 ^ n + 2 ^ n) Lfu2 L2n2n2 to the current goal.
We will
prove f (u ∩ SNoElts_ n) < 2 ^ n + 2 ^ n.
An
exact proof term for the current goal is
SNoLt_tra (f (u ∩ SNoElts_ n)) (2 ^ n) (2 ^ n + 2 ^ n) Lfu3 L2n3 L2n2n3 Lfu4 L2nLt2n2n.
Assume H1: n ∉ u.
rewrite the current goal using Hg2 u H1 (from left to right).
We will
prove 2 ^ n + f (u ∩ SNoElts_ n) ∈ 2 ^ n + 2 ^ n.
Apply ordinal_SNoLt_In (2 ^ n + f (u ∩ SNoElts_ n)) (2 ^ n + 2 ^ n) (add_SNo_ordinal_ordinal (2 ^ n) L2n2 (f (u ∩ SNoElts_ n)) Lfu2) L2n2n2 to the current goal.
We will
prove 2 ^ n + f (u ∩ SNoElts_ n) < 2 ^ n + 2 ^ n.
An exact proof term for the current goal is L2npLt2n2n (f (u ∩ SNoElts_ n)) Lfu3 Lfu4.
Let u be given.
Let v be given.
Apply L2 u Hu to the current goal.
Assume Hu0a: SNo u.
Assume Hu0b: SNoLev u = ordsucc n.
Assume Hu2: SNo (u ∩ SNoElts_ n).
Assume Hu3: SNoLev (u ∩ SNoElts_ n) = n.
Apply Lf u Hu to the current goal.
Assume Lfu1: nat_p (f (u ∩ SNoElts_ n)).
Assume Lfu2: ordinal (f (u ∩ SNoElts_ n)).
Assume Lfu3: SNo (f (u ∩ SNoElts_ n)).
Apply L2 v Hv to the current goal.
Assume Hv0a: SNo v.
Assume Hv0b: SNoLev v = ordsucc n.
Assume Hv2: SNo (v ∩ SNoElts_ n).
Assume Hv3: SNoLev (v ∩ SNoElts_ n) = n.
Apply Lf v Hv to the current goal.
Assume Lfv1: nat_p (f (v ∩ SNoElts_ n)).
Assume Lfv2: ordinal (f (v ∩ SNoElts_ n)).
Assume Lfv3: SNo (f (v ∩ SNoElts_ n)).
We prove the intermediate
claim LnLu:
n ∈ SNoLev u.
rewrite the current goal using Hu0b (from left to right).
Apply ordsuccI2 to the current goal.
We prove the intermediate
claim LnLv:
n ∈ SNoLev v.
rewrite the current goal using Hv0b (from left to right).
Apply ordsuccI2 to the current goal.
Apply xm (n ∈ u) to the current goal.
rewrite the current goal using Hg1 u H1 (from left to right).
Apply xm (n ∈ v) to the current goal.
rewrite the current goal using Hg1 v H2 (from left to right).
Assume Hguv: f (u ∩ SNoElts_ n) = f (v ∩ SNoElts_ n).
We will prove u = v.
We prove the intermediate claim Luv: u ∩ SNoElts_ n = v ∩ SNoElts_ n.
An exact proof term for the current goal is Hf2 (u ∩ SNoElts_ n) Hu1 (v ∩ SNoElts_ n) Hv1 Hguv.
Apply SNo_eq u v Hu0a Hv0a to the current goal.
We will prove SNoLev u = SNoLev v.
rewrite the current goal using Hv0b (from left to right).
An exact proof term for the current goal is Hu0b.
We will prove SNoEq_ (SNoLev u) u v.
rewrite the current goal using Hu0b (from left to right).
We will prove SNoEq_ (ordsucc n) u v.
Let i be given.
Apply ordsuccE n i Hi to the current goal.
We will
prove i ∈ u ↔ i ∈ v.
Apply iff_trans (i ∈ u) (i ∈ u ∩ SNoElts_ n) (i ∈ v) to the current goal.
We will
prove i ∈ u ↔ i ∈ u ∩ SNoElts_ n.
Apply iff_sym to the current goal.
An exact proof term for the current goal is restr_SNoEq u ?? n LnLu i H3.
We will
prove i ∈ u ∩ SNoElts_ n ↔ i ∈ v.
rewrite the current goal using Luv (from left to right).
We will
prove i ∈ v ∩ SNoElts_ n ↔ i ∈ v.
An exact proof term for the current goal is restr_SNoEq v ?? n LnLv i H3.
Assume H3: i = n.
rewrite the current goal using H3 (from left to right).
Apply iffI to the current goal.
Assume _.
An exact proof term for the current goal is H2.
Assume _.
An exact proof term for the current goal is H1.
Assume H2: n ∉ v.
rewrite the current goal using Hg2 v H2 (from left to right).
We will prove False.
Apply SNoLt_irref (2 ^ n) to the current goal.
We will
prove 2 ^ n < 2 ^ n.
Apply SNoLeLt_tra (2 ^ n) (2 ^ n + f (v ∩ SNoElts_ n)) (2 ^ n) L2n3 (SNo_add_SNo (2 ^ n) (f (v ∩ SNoElts_ n)) L2n3 Lfv3) L2n3 to the current goal.
We will
prove 2 ^ n ≤ 2 ^ n + f (v ∩ SNoElts_ n).
rewrite the current goal using
add_SNo_0R (2 ^ n) L2n3 (from right to left) at position 1.
We will
prove 2 ^ n + 0 ≤ 2 ^ n + f (v ∩ SNoElts_ n).
Apply add_SNo_Le2 (2 ^ n) 0 (f (v ∩ SNoElts_ n)) L2n3 SNo_0 Lfv3 to the current goal.
We will prove 0 ≤ f (v ∩ SNoElts_ n).
An exact proof term for the current goal is omega_nonneg (f (v ∩ SNoElts_ n)) (nat_p_omega (f (v ∩ SNoElts_ n)) Lfv1).
We will
prove 2 ^ n + f (v ∩ SNoElts_ n) < 2 ^ n.
rewrite the current goal using Hguv (from right to left).
An exact proof term for the current goal is Lfu4.
Assume H1: n ∉ u.
rewrite the current goal using Hg2 u H1 (from left to right).
Apply xm (n ∈ v) to the current goal.
rewrite the current goal using Hg1 v H2 (from left to right).
We will prove False.
Apply SNoLt_irref (2 ^ n) to the current goal.
We will
prove 2 ^ n < 2 ^ n.
Apply SNoLeLt_tra (2 ^ n) (2 ^ n + f (u ∩ SNoElts_ n)) (2 ^ n) L2n3 (SNo_add_SNo (2 ^ n) (f (u ∩ SNoElts_ n)) L2n3 Lfu3) L2n3 to the current goal.
We will
prove 2 ^ n ≤ 2 ^ n + f (u ∩ SNoElts_ n).
rewrite the current goal using
add_SNo_0R (2 ^ n) L2n3 (from right to left) at position 1.
We will
prove 2 ^ n + 0 ≤ 2 ^ n + f (u ∩ SNoElts_ n).
Apply add_SNo_Le2 (2 ^ n) 0 (f (u ∩ SNoElts_ n)) L2n3 SNo_0 Lfu3 to the current goal.
We will prove 0 ≤ f (u ∩ SNoElts_ n).
An exact proof term for the current goal is omega_nonneg (f (u ∩ SNoElts_ n)) (nat_p_omega (f (u ∩ SNoElts_ n)) Lfu1).
We will
prove 2 ^ n + f (u ∩ SNoElts_ n) < 2 ^ n.
rewrite the current goal using Hguv (from left to right).
An exact proof term for the current goal is Lfv4.
Assume H2: n ∉ v.
rewrite the current goal using Hg2 v H2 (from left to right).
We will prove u = v.
We prove the intermediate claim Luv: u ∩ SNoElts_ n = v ∩ SNoElts_ n.
Apply Hf2 (u ∩ SNoElts_ n) Hu1 (v ∩ SNoElts_ n) Hv1 to the current goal.
We will prove f (u ∩ SNoElts_ n) = f (v ∩ SNoElts_ n).
An
exact proof term for the current goal is
add_SNo_cancel_L (2 ^ n) (f (u ∩ SNoElts_ n)) (f (v ∩ SNoElts_ n)) L2n3 Lfu3 Lfv3 Hguv.
Apply SNo_eq u v Hu0a Hv0a to the current goal.
We will prove SNoLev u = SNoLev v.
rewrite the current goal using Hv0b (from left to right).
An exact proof term for the current goal is Hu0b.
We will prove SNoEq_ (SNoLev u) u v.
rewrite the current goal using Hu0b (from left to right).
We will prove SNoEq_ (ordsucc n) u v.
Let i be given.
Apply ordsuccE n i Hi to the current goal.
We will
prove i ∈ u ↔ i ∈ v.
Apply iff_trans (i ∈ u) (i ∈ u ∩ SNoElts_ n) (i ∈ v) to the current goal.
We will
prove i ∈ u ↔ i ∈ u ∩ SNoElts_ n.
Apply iff_sym to the current goal.
An exact proof term for the current goal is restr_SNoEq u ?? n LnLu i H3.
We will
prove i ∈ u ∩ SNoElts_ n ↔ i ∈ v.
rewrite the current goal using Luv (from left to right).
We will
prove i ∈ v ∩ SNoElts_ n ↔ i ∈ v.
An exact proof term for the current goal is restr_SNoEq v ?? n LnLv i H3.
Assume H3: i = n.
rewrite the current goal using H3 (from left to right).
Apply iffI to the current goal.
We will prove False.
An exact proof term for the current goal is H1 H4.
We will prove False.
An exact proof term for the current goal is H2 H4.
We will
prove ∀m ∈ 2 ^ n + 2 ^ n, ∃u ∈ {x ∈ SNoS_ ω|SNoLev x = ordsucc n}, g u = m.
Let m be given.
We prove the intermediate claim Lm1: nat_p m.
An
exact proof term for the current goal is
nat_p_trans (2 ^ n + 2 ^ n) L2n2n1 m Hm.
We prove the intermediate claim Lm2: SNo m.
An exact proof term for the current goal is nat_p_SNo m Lm1.
Apply add_SNo_omega_In_cases m (2 ^ n) (nat_p_omega (2 ^ n) L2n1) (2 ^ n) L2n1 Hm to the current goal.
Apply Hf3 m H1 to the current goal.
Let u be given.
Assume H.
Apply H to the current goal.
Assume Hu2: f u = m.
Apply SepE (SNoS_ ω) (λx ⇒ SNoLev x = n) u Hu1 to the current goal.
Assume Hu4: SNoLev u = n.
Apply SNoS_E2 ω omega_ordinal u Hu3 to the current goal.
Assume Hu3a Hu3b Hu3c Hu3d.
We prove the intermediate claim Lu1: SNo (SNo_extend1 u).
An exact proof term for the current goal is SNo_extend1_SNo u ??.
We prove the intermediate claim Lu2: SNoLev (SNo_extend1 u) = ordsucc n.
rewrite the current goal using Hu4 (from right to left).
An exact proof term for the current goal is SNo_extend1_SNoLev u ??.
We prove the intermediate
claim Lu3:
n ∈ SNo_extend1 u.
rewrite the current goal using Hu4 (from right to left).
An exact proof term for the current goal is SNo_extend1_In u ??.
We use (SNo_extend1 u) to witness the existential quantifier.
Apply andI to the current goal.
We will
prove SNo_extend1 u ∈ {x ∈ SNoS_ ω|SNoLev x = ordsucc n}.
Apply SepI to the current goal.
Apply SNoS_I ω omega_ordinal (SNo_extend1 u) (ordsucc n) to the current goal.
We will
prove ordsucc n ∈ ω.
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is nat_p_omega n Hn.
We will prove SNo_ (ordsucc n) (SNo_extend1 u).
rewrite the current goal using Hu4 (from right to left).
We will prove SNo_ (ordsucc (SNoLev u)) (SNo_extend1 u).
An exact proof term for the current goal is SNo_extend1_SNo_ u ??.
We will prove SNoLev (SNo_extend1 u) = ordsucc n.
An exact proof term for the current goal is Lu2.
We will prove g (SNo_extend1 u) = m.
rewrite the current goal using Hg1 (SNo_extend1 u) Lu3 (from left to right).
We will prove f (SNo_extend1 u ∩ SNoElts_ n) = m.
rewrite the current goal using Hu4 (from right to left).
We will prove f (SNo_extend1 u ∩ SNoElts_ (SNoLev u)) = m.
rewrite the current goal using SNo_extend1_restr_eq u Hu3c (from right to left).
An exact proof term for the current goal is Hu2.
Apply Hf3 (m + - 2 ^ n) H1 to the current goal.
Let u be given.
Assume H.
Apply H to the current goal.
Apply SepE (SNoS_ ω) (λx ⇒ SNoLev x = n) u Hu1 to the current goal.
Assume Hu4: SNoLev u = n.
Apply SNoS_E2 ω omega_ordinal u Hu3 to the current goal.
Assume Hu3a Hu3b Hu3c Hu3d.
We prove the intermediate claim Lu1: SNo (SNo_extend0 u).
An exact proof term for the current goal is SNo_extend0_SNo u ??.
We prove the intermediate claim Lu2: SNoLev (SNo_extend0 u) = ordsucc n.
rewrite the current goal using Hu4 (from right to left).
An exact proof term for the current goal is SNo_extend0_SNoLev u ??.
We prove the intermediate claim Lu3: n ∉ SNo_extend0 u.
rewrite the current goal using Hu4 (from right to left).
An exact proof term for the current goal is SNo_extend0_nIn u ??.
We use (SNo_extend0 u) to witness the existential quantifier.
Apply andI to the current goal.
We will
prove SNo_extend0 u ∈ {x ∈ SNoS_ ω|SNoLev x = ordsucc n}.
Apply SepI to the current goal.
Apply SNoS_I ω omega_ordinal (SNo_extend0 u) (ordsucc n) to the current goal.
We will
prove ordsucc n ∈ ω.
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is nat_p_omega n Hn.
We will prove SNo_ (ordsucc n) (SNo_extend0 u).
rewrite the current goal using Hu4 (from right to left).
We will prove SNo_ (ordsucc (SNoLev u)) (SNo_extend0 u).
An exact proof term for the current goal is SNo_extend0_SNo_ u ??.
We will prove SNoLev (SNo_extend0 u) = ordsucc n.
An exact proof term for the current goal is Lu2.
We will prove g (SNo_extend0 u) = m.
rewrite the current goal using Hg2 (SNo_extend0 u) Lu3 (from left to right).
We will
prove 2 ^ n + f (SNo_extend0 u ∩ SNoElts_ n) = m.
rewrite the current goal using Hu4 (from right to left) at position 2.
We will
prove 2 ^ n + f (SNo_extend0 u ∩ SNoElts_ (SNoLev u)) = m.
rewrite the current goal using SNo_extend0_restr_eq u Hu3c (from right to left).
We will
prove 2 ^ n + f u = m.
rewrite the current goal using Hu2 (from left to right).
We will
prove 2 ^ n + (m + - 2 ^ n) = m.
rewrite the current goal using
add_SNo_com (2 ^ n) (m + - 2 ^ n) L2n3 (SNo_add_SNo m (- 2 ^ n) Lm2 (SNo_minus_SNo (2 ^ n) L2n3)) (from left to right).
We will
prove (m + - 2 ^ n) + 2 ^ n = m.
rewrite the current goal using
add_SNo_assoc m (- 2 ^ n) (2 ^ n) Lm2 (SNo_minus_SNo (2 ^ n) L2n3) L2n3 (from right to left).
We will
prove m + (- 2 ^ n + 2 ^ n) = m.
rewrite the current goal using
add_SNo_minus_SNo_linv (2 ^ n) L2n3 (from left to right).
An exact proof term for the current goal is add_SNo_0R m Lm2.