Apply ordinal_ind to the current goal.
Let alpha be given.
Assume Ha: ordinal alpha.
Apply Ha to the current goal.
Assume Ha1 Ha2.
Assume IH: ∀beta ∈ alpha, ∀x ∈ SNoS_ beta, SNoLev (- x) ⊆ SNoLev x.
Let x be given.
Assume Hx: x ∈ SNoS_ alpha.
Apply SNoS_E2 alpha Ha x Hx to the current goal.
Assume Hx1: SNoLev x ∈ alpha.
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 beta be given.
Assume Hb: beta ∈ SNoLev (SNoCut L R).
We prove the intermediate claim Lb: beta ∈ ((⋃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 beta 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 beta ∈ SNoLev x.
Apply binunionE (⋃x ∈ Lordsucc (SNoLev x)) (⋃y ∈ Rordsucc (SNoLev y)) beta Lb to the current goal.
Assume H4: beta ∈ ⋃x ∈ Lordsucc (SNoLev x).
Apply famunionE L (λx ⇒ ordsucc (SNoLev x)) beta H4 to the current goal.
Let w be given.
Assume Hw.
Apply Hw to the current goal.
Assume Hw1: w ∈ L.
Assume Hw2: beta ∈ ordsucc (SNoLev w).
We will prove beta ∈ 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) ∈ alpha.
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 beta.
An exact proof term for the current goal is ordinal_Hered (ordsucc (SNoLev w)) LsLw beta Hw2.
Apply ordinal_In_Or_Subq beta (SNoLev x) Lb Hx2 to the current goal.
Assume H5: beta ∈ SNoLev x.
An exact proof term for the current goal is H5.
Assume H5: SNoLev x ⊆ beta.
We will prove False.
We prove the intermediate claim LLub: SNoLev u ∈ beta.
An exact proof term for the current goal is H5 (SNoLev u) Hu2.
Apply ordsuccE (SNoLev w) beta Hw2 to the current goal.
rewrite the current goal using Hwu (from left to right).
Assume H5: beta ∈ SNoLev (- u).
Apply In_no2cycle (SNoLev u) beta LLub to the current goal.
We will prove beta ∈ SNoLev u.
An exact proof term for the current goal is IHu beta H5.
rewrite the current goal using Hwu (from left to right).
Assume H5: beta = 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: beta ∈ ⋃y ∈ Rordsucc (SNoLev y).
Apply famunionE R (λx ⇒ ordsucc (SNoLev x)) beta H4 to the current goal.
Let w be given.
Assume Hw.
Apply Hw to the current goal.
Assume Hw1: w ∈ R.
Assume Hw2: beta ∈ ordsucc (SNoLev w).
We will prove beta ∈ 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) ∈ alpha.
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 beta.
An exact proof term for the current goal is ordinal_Hered (ordsucc (SNoLev w)) LsLw beta Hw2.
Apply ordinal_In_Or_Subq beta (SNoLev x) Lb Hx2 to the current goal.
Assume H5: beta ∈ SNoLev x.
An exact proof term for the current goal is H5.
Assume H5: SNoLev x ⊆ beta.
We will prove False.
We prove the intermediate claim LLub: SNoLev u ∈ beta.
An exact proof term for the current goal is H5 (SNoLev u) Hu2.
Apply ordsuccE (SNoLev w) beta Hw2 to the current goal.
rewrite the current goal using Hwu (from left to right).
Assume H5: beta ∈ SNoLev (- u).
Apply In_no2cycle (SNoLev u) beta LLub to the current goal.
We will prove beta ∈ SNoLev u.
An exact proof term for the current goal is IHu beta H5.
rewrite the current goal using Hwu (from left to right).
Assume H5: beta = 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.
∎