Apply ordinal_ind to the current goal.
Let α be given.
Assume Ha: ordinal α.
Apply Ha to the current goal.
Assume Ha1 Ha2.
Assume IH: ∀β ∈ α, ∀x ∈ SNoS_ β, SNoLev (- x) ⊆ SNoLev x.
Let x be given.
Assume Hx: x ∈ SNoS_ α.
Apply SNoS_E2 α Ha x Hx to the current goal.
Assume Hx1: SNoLev x ∈ α.
Assume Hx2: ordinal (SNoLev x).
Assume Hx3: SNo x.
Assume Hx4: SNo_ (SNoLev x) x.
Set L to be the term {- z|z ∈ SNoR x}.
Set R to be the term {- w|w ∈ SNoL x}.
We prove the intermediate claim LLR: SNoCutP L R.
An exact proof term for the current goal is minus_SNo_SNoCutP x Hx3.
We will prove SNoLev (- x) ⊆ SNoLev x.
rewrite the current goal using minus_SNo_eq x Hx3 (from left to right).
We will prove SNoLev (SNoCut L R) ⊆ SNoLev x.
Apply SNoCutP_SNoCut_impred L R LLR to the current goal.
Assume H2: SNo (SNoCut L R).
Assume H3: SNoLev (SNoCut L R) ∈ ordsucc ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))).
Assume _ _ _.
We prove the intermediate claim L3: ordinal ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))).
Apply ordinal_binunion to the current goal.
Apply ordinal_famunion to the current goal.
Let w be given.
Assume Hw: w ∈ L.
We will prove ordinal (ordsucc (SNoLev w)).
Apply ReplE_impred (SNoR x) (λz ⇒ - z) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoR x.
Assume Hwu: w = - u.
Apply SNoR_E x Hx3 u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev x.
Assume Hu3: x < u.
Apply ordinal_ordsucc to the current goal.
We will prove ordinal (SNoLev w).
Apply SNoLev_ordinal to the current goal.
We will prove SNo w.
rewrite the current goal using Hwu (from left to right).
An exact proof term for the current goal is SNo_minus_SNo u Hu1.
Apply ordinal_famunion to the current goal.
Let w be given.
Assume Hw: w ∈ R.
We will prove ordinal (ordsucc (SNoLev w)).
Apply ReplE_impred (SNoL x) (λz ⇒ - z) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL x.
Assume Hwu: w = - u.
Apply SNoL_E x Hx3 u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev x.
Assume Hu3: u < x.
Apply ordinal_ordsucc to the current goal.
We will prove ordinal (SNoLev w).
Apply SNoLev_ordinal to the current goal.
We will prove SNo w.
rewrite the current goal using Hwu (from left to right).
An exact proof term for the current goal is SNo_minus_SNo u Hu1.
We prove the intermediate claim L3a: TransSet ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))).
Apply L3 to the current goal.
Assume H _.
An exact proof term for the current goal is H.
Let β be given.
Assume Hb: β ∈ SNoLev (SNoCut L R).
We prove the intermediate claim Lb: β ∈ ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))).
Apply ordsuccE ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))) (SNoLev (SNoCut L R)) H3 to the current goal.
Assume H4.
An exact proof term for the current goal is L3a (SNoLev (SNoCut L R)) H4 β Hb.
Assume H4.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is Hb.
We will prove β ∈ SNoLev x.
Apply binunionE (⋃x ∈ Lordsucc (SNoLev x)) (⋃y ∈ Rordsucc (SNoLev y)) β Lb to the current goal.
Assume H4: β ∈ ⋃x ∈ Lordsucc (SNoLev x).
Apply famunionE L (λx ⇒ ordsucc (SNoLev x)) β H4 to the current goal.
Let w be given.
Assume Hw.
Apply Hw to the current goal.
Assume Hw1: w ∈ L.
Assume Hw2: β ∈ ordsucc (SNoLev w).
We will prove β ∈ SNoLev x.
Apply ReplE_impred (SNoR x) (λz ⇒ - z) w Hw1 to the current goal.
Let u be given.
Assume Hu: u ∈ SNoR x.
Assume Hwu: w = - u.
Apply SNoR_E x Hx3 u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev x.
Assume Hu3: x < u.
We prove the intermediate claim Lu: u ∈ SNoS_ (ordsucc (SNoLev u)).
An exact proof term for the current goal is SNoS_SNoLev u Hu1.
We prove the intermediate claim LsLu: ordsucc (SNoLev u) ∈ α.
Apply ordinal_ordsucc_In_eq (SNoLev x) (SNoLev u) Hx2 Hu2 to the current goal.
Assume H2: ordsucc (SNoLev u) ∈ SNoLev x.
An exact proof term for the current goal is Ha1 (SNoLev x) Hx1 (ordsucc (SNoLev u)) H2.
Assume H2: SNoLev x = ordsucc (SNoLev u).
rewrite the current goal using H2 (from right to left).
An exact proof term for the current goal is Hx1.
We prove the intermediate claim IHu: SNoLev (- u) ⊆ SNoLev u.
An exact proof term for the current goal is IH (ordsucc (SNoLev u)) LsLu u Lu.
We prove the intermediate claim LLu: ordinal (SNoLev u).
An exact proof term for the current goal is SNoLev_ordinal u Hu1.
We prove the intermediate claim Lmu: SNo (- u).
An exact proof term for the current goal is SNo_minus_SNo u Hu1.
We prove the intermediate claim LLmu: ordinal (SNoLev (- u)).
An exact proof term for the current goal is SNoLev_ordinal (- u) Lmu.
We prove the intermediate claim LsLw: ordinal (ordsucc (SNoLev w)).
Apply ordinal_ordsucc to the current goal.
rewrite the current goal using Hwu (from left to right).
An exact proof term for the current goal is LLmu.
We prove the intermediate claim Lb: ordinal β.
An exact proof term for the current goal is ordinal_Hered (ordsucc (SNoLev w)) LsLw β Hw2.
Apply ordinal_In_Or_Subq β (SNoLev x) Lb Hx2 to the current goal.
Assume H5: β ∈ SNoLev x.
An exact proof term for the current goal is H5.
Assume H5: SNoLev x ⊆ β.
We will prove False.
We prove the intermediate claim LLub: SNoLev u ∈ β.
An exact proof term for the current goal is H5 (SNoLev u) Hu2.
Apply ordsuccE (SNoLev w) β Hw2 to the current goal.
rewrite the current goal using Hwu (from left to right).
Assume H5: β ∈ SNoLev (- u).
Apply In_no2cycle (SNoLev u) β LLub to the current goal.
We will prove β ∈ SNoLev u.
An exact proof term for the current goal is IHu β H5.
rewrite the current goal using Hwu (from left to right).
Assume H5: β = SNoLev (- u).
Apply In_irref (SNoLev u) to the current goal.
Apply IHu (SNoLev u) to the current goal.
We will prove SNoLev u ∈ SNoLev (- u).
rewrite the current goal using H5 (from right to left).
An exact proof term for the current goal is LLub.
Assume H4: β ∈ ⋃y ∈ Rordsucc (SNoLev y).
Apply famunionE R (λx ⇒ ordsucc (SNoLev x)) β H4 to the current goal.
Let w be given.
Assume Hw.
Apply Hw to the current goal.
Assume Hw1: w ∈ R.
Assume Hw2: β ∈ ordsucc (SNoLev w).
We will prove β ∈ SNoLev x.
Apply ReplE_impred (SNoL x) (λz ⇒ - z) w Hw1 to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL x.
Assume Hwu: w = - u.
Apply SNoL_E x Hx3 u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev x.
Assume Hu3: u < x.
We prove the intermediate claim Lu: u ∈ SNoS_ (ordsucc (SNoLev u)).
An exact proof term for the current goal is SNoS_SNoLev u Hu1.
We prove the intermediate claim LsLu: ordsucc (SNoLev u) ∈ α.
Apply ordinal_ordsucc_In_eq (SNoLev x) (SNoLev u) Hx2 Hu2 to the current goal.
Assume H2: ordsucc (SNoLev u) ∈ SNoLev x.
An exact proof term for the current goal is Ha1 (SNoLev x) Hx1 (ordsucc (SNoLev u)) H2.
Assume H2: SNoLev x = ordsucc (SNoLev u).
rewrite the current goal using H2 (from right to left).
An exact proof term for the current goal is Hx1.
We prove the intermediate claim IHu: SNoLev (- u) ⊆ SNoLev u.
An exact proof term for the current goal is IH (ordsucc (SNoLev u)) LsLu u Lu.
We prove the intermediate claim LLu: ordinal (SNoLev u).
An exact proof term for the current goal is SNoLev_ordinal u Hu1.
We prove the intermediate claim Lmu: SNo (- u).
An exact proof term for the current goal is SNo_minus_SNo u Hu1.
We prove the intermediate claim LLmu: ordinal (SNoLev (- u)).
An exact proof term for the current goal is SNoLev_ordinal (- u) Lmu.
We prove the intermediate claim LsLw: ordinal (ordsucc (SNoLev w)).
Apply ordinal_ordsucc to the current goal.
rewrite the current goal using Hwu (from left to right).
An exact proof term for the current goal is LLmu.
We prove the intermediate claim Lb: ordinal β.
An exact proof term for the current goal is ordinal_Hered (ordsucc (SNoLev w)) LsLw β Hw2.
Apply ordinal_In_Or_Subq β (SNoLev x) Lb Hx2 to the current goal.
Assume H5: β ∈ SNoLev x.
An exact proof term for the current goal is H5.
Assume H5: SNoLev x ⊆ β.
We will prove False.
We prove the intermediate claim LLub: SNoLev u ∈ β.
An exact proof term for the current goal is H5 (SNoLev u) Hu2.
Apply ordsuccE (SNoLev w) β Hw2 to the current goal.
rewrite the current goal using Hwu (from left to right).
Assume H5: β ∈ SNoLev (- u).
Apply In_no2cycle (SNoLev u) β LLub to the current goal.
We will prove β ∈ SNoLev u.
An exact proof term for the current goal is IHu β H5.
rewrite the current goal using Hwu (from left to right).
Assume H5: β = SNoLev (- u).
Apply In_irref (SNoLev u) to the current goal.
Apply IHu (SNoLev u) to the current goal.
We will prove SNoLev u ∈ SNoLev (- u).
rewrite the current goal using H5 (from right to left).
An exact proof term for the current goal is LLub.
∎