Set P to be the term λx y ⇒ SNo (x + y) ∧ (∀u ∈ SNoL x, u + y < x + y) ∧ (∀u ∈ SNoR x, x + y < u + y) ∧ (∀u ∈ SNoL y, x + u < x + y) ∧ (∀u ∈ SNoR y, x + y < x + u) ∧ SNoCutP ({w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}) ({z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y}) of type set → set → prop.
We prove the intermediate claim LPE: ∀x y, P x y → ∀p : prop, (SNo (x + y) → (∀u ∈ SNoL x, u + y < x + y) → (∀u ∈ SNoR x, x + y < u + y) → (∀u ∈ SNoL y, x + u < x + y) → (∀u ∈ SNoR y, x + y < x + u) → p) → p.
Let x and y be given.
Assume Hxy.
Let p be given.
Assume Hp.
Apply Hxy to the current goal.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume H1 H2 H3 H4 H5 _.
An exact proof term for the current goal is Hp H1 H2 H3 H4 H5.
We will prove ∀x y, SNo x → SNo y → P x y.
Apply SNoLev_ind2 to the current goal.
Let x and y be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume IHx: ∀w ∈ SNoS_ (SNoLev x), P w y.
Assume IHy: ∀z ∈ SNoS_ (SNoLev y), P x z.
Assume IHxy: ∀w ∈ SNoS_ (SNoLev x), ∀z ∈ SNoS_ (SNoLev y), P w z.
We prove the intermediate claim LLx: ordinal (SNoLev x).
An exact proof term for the current goal is SNoLev_ordinal x Hx.
We prove the intermediate claim LLxa: TransSet (SNoLev x).
An exact proof term for the current goal is ordinal_TransSet (SNoLev x) LLx.
We prove the intermediate claim LLy: ordinal (SNoLev y).
An exact proof term for the current goal is SNoLev_ordinal y Hy.
We prove the intermediate claim LLya: TransSet (SNoLev y).
An exact proof term for the current goal is ordinal_TransSet (SNoLev y) LLy.
Set L1 to be the term {w + y|w ∈ SNoL x}.
Set L2 to be the term {x + w|w ∈ SNoL y}.
Set L to be the term L1 ∪ L2.
Set R1 to be the term {z + y|z ∈ SNoR x}.
Set R2 to be the term {x + z|z ∈ SNoR y}.
Set R to be the term R1 ∪ R2.
We prove the intermediate claim IHLx: ∀w ∈ SNoL x, P w y.
Let w be given.
Assume Hw: w ∈ SNoL x.
Apply SNoL_E x Hx w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev x.
Assume Hw3: w < x.
We prove the intermediate claim Lw: w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 w x Hw1 Hx Hw2.
An exact proof term for the current goal is IHx w Lw.
We prove the intermediate claim IHRx: ∀w ∈ SNoR x, P w y.
Let w be given.
Assume Hw: w ∈ SNoR x.
Apply SNoR_E x Hx w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev x.
Assume Hw3: x < w.
We prove the intermediate claim Lw: w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 w x Hw1 Hx Hw2.
An exact proof term for the current goal is IHx w Lw.
We prove the intermediate claim IHLy: ∀w ∈ SNoL y, P x w.
Let w be given.
Assume Hw: w ∈ SNoL y.
Apply SNoL_E y Hy w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev y.
Assume Hw3: w < y.
We prove the intermediate claim Lw: w ∈ SNoS_ (SNoLev y).
An exact proof term for the current goal is SNoS_I2 w y Hw1 Hy Hw2.
An exact proof term for the current goal is IHy w Lw.
We prove the intermediate claim IHRy: ∀w ∈ SNoR y, P x w.
Let w be given.
Assume Hw: w ∈ SNoR y.
Apply SNoR_E y Hy w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev y.
Assume Hw3: y < w.
We prove the intermediate claim Lw: w ∈ SNoS_ (SNoLev y).
An exact proof term for the current goal is SNoS_I2 w y Hw1 Hy Hw2.
An exact proof term for the current goal is IHy w Lw.
We prove the intermediate claim LLR: SNoCutP L R.
We will prove (∀w ∈ L, SNo w) ∧ (∀z ∈ R, SNo z) ∧ (∀w ∈ L, ∀z ∈ R, w < z).
Apply and3I to the current goal.
Let w be given.
Assume Hw: w ∈ L1 ∪ L2.
We will prove SNo w.
Apply binunionE L1 L2 w Hw to the current goal.
Assume Hw: w ∈ {w + y|w ∈ SNoL x}.
Apply ReplE_impred (SNoL x) (λz ⇒ z + y) w Hw to the current goal.
Let z be given.
Assume Hz: z ∈ SNoL x.
Assume Hwz: w = z + y.
Apply LPE z y (IHLx z Hz) to the current goal.
Assume H2: SNo (z + y).
Assume _ _ _ _.
We will prove SNo w.
rewrite the current goal using Hwz (from left to right).
An exact proof term for the current goal is H2.
Assume Hw: w ∈ {x + w|w ∈ SNoL y}.
Apply ReplE_impred (SNoL y) (λz ⇒ x + z) w Hw to the current goal.
Let z be given.
Assume Hz: z ∈ SNoL y.
Assume Hwz: w = x + z.
Apply LPE x z (IHLy z Hz) to the current goal.
Assume H2: SNo (x + z).
Assume _ _ _ _.
We will prove SNo w.
rewrite the current goal using Hwz (from left to right).
An exact proof term for the current goal is H2.
Let w be given.
Assume Hw: w ∈ R1 ∪ R2.
We will prove SNo w.
Apply binunionE R1 R2 w Hw to the current goal.
Assume Hw: w ∈ {z + y|z ∈ SNoR x}.
Apply ReplE_impred (SNoR x) (λz ⇒ z + y) w Hw to the current goal.
Let z be given.
Assume Hz: z ∈ SNoR x.
Assume Hwz: w = z + y.
Apply LPE z y (IHRx z Hz) to the current goal.
Assume H2: SNo (z + y).
Assume _ _ _ _.
We will prove SNo w.
rewrite the current goal using Hwz (from left to right).
An exact proof term for the current goal is H2.
Assume Hw: w ∈ {x + z|z ∈ SNoR y}.
Apply ReplE_impred (SNoR y) (λz ⇒ x + z) w Hw to the current goal.
Let z be given.
Assume Hz: z ∈ SNoR y.
Assume Hwz: w = x + z.
Apply LPE x z (IHRy z Hz) to the current goal.
Assume H2: SNo (x + z).
Assume _ _ _ _.
We will prove SNo w.
rewrite the current goal using Hwz (from left to right).
An exact proof term for the current goal is H2.
Let w be given.
Assume Hw: w ∈ L.
Let z be given.
Assume Hz: z ∈ R.
We will prove w < z.
Apply binunionE L1 L2 w Hw to the current goal.
Assume Hw: w ∈ {w + y|w ∈ SNoL x}.
Apply ReplE_impred (SNoL x) (λz ⇒ z + y) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL x.
Assume Hwu: w = u + y.
Apply SNoL_E x Hx 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 Lux: u ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 u x Hu1 Hx Hu2.
Apply LPE u y (IHLx u Hu) to the current goal.
Assume IHu1: SNo (u + y).
Assume IHu2: ∀z ∈ SNoL u, z + y < u + y.
Assume IHu3: ∀z ∈ SNoR u, u + y < z + y.
Assume IHu4: ∀z ∈ SNoL y, u + z < u + y.
Assume IHu5: ∀z ∈ SNoR y, u + y < u + z.
We will prove w < z.
rewrite the current goal using Hwu (from left to right).
We will prove u + y < z.
Apply binunionE R1 R2 z Hz to the current goal.
Assume Hz: z ∈ {z + y|z ∈ SNoR x}.
Apply ReplE_impred (SNoR x) (λz ⇒ z + y) z Hz to the current goal.
Let v be given.
Assume Hv: v ∈ SNoR x.
Assume Hzv: z = v + y.
Apply SNoR_E x Hx v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev x.
Assume Hv3: x < v.
Apply LPE v y (IHRx v Hv) to the current goal.
Assume IHv1: SNo (v + y).
Assume IHv2: ∀u ∈ SNoL v, u + y < v + y.
Assume IHv3: ∀u ∈ SNoR v, v + y < u + y.
Assume IHv4: ∀u ∈ SNoL y, v + u < v + y.
Assume IHv5: ∀u ∈ SNoR y, v + y < v + u.
rewrite the current goal using Hzv (from left to right).
We will prove u + y < v + y.
We prove the intermediate claim Luv: u < v.
An exact proof term for the current goal is SNoLt_tra u x v Hu1 Hx Hv1 Hu3 Hv3.
Apply SNoLtE u v Hu1 Hv1 Luv to the current goal.
Let q be given.
Assume Hq1: SNo q.
Assume Hq2: SNoLev q ∈ SNoLev u ∩ SNoLev v.
Assume _ _.
Assume Hq5: u < q.
Assume Hq6: q < v.
Assume _ _.
Apply binintersectE (SNoLev u) (SNoLev v) (SNoLev q) Hq2 to the current goal.
Assume Hq2u Hq2v.
We prove the intermediate claim Lqx: SNoLev q ∈ SNoLev x.
An exact proof term for the current goal is LLxa (SNoLev u) Hu2 (SNoLev q) Hq2u.
We prove the intermediate claim Lqx2: q ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 q x Hq1 Hx Lqx.
We prove the intermediate claim Lqy: SNo (q + y).
Apply LPE q y (IHx q Lqx2) to the current goal.
Assume IHq1 _ _ _ _.
An exact proof term for the current goal is IHq1.
Apply SNoLt_tra (u + y) (q + y) (v + y) IHu1 Lqy IHv1 to the current goal.
We will prove u + y < q + y.
Apply IHu3 to the current goal.
We will prove q ∈ SNoR u.
An exact proof term for the current goal is SNoR_I u Hu1 q Hq1 Hq2u Hq5.
We will prove q + y < v + y.
Apply IHv2 to the current goal.
We will prove q ∈ SNoL v.
An exact proof term for the current goal is SNoL_I v Hv1 q Hq1 Hq2v Hq6.
Assume Huv: SNoLev u ∈ SNoLev v.
Assume _ _.
We will prove u + y < v + y.
Apply IHv2 to the current goal.
We will prove u ∈ SNoL v.
An exact proof term for the current goal is SNoL_I v Hv1 u Hu1 Huv Luv.
Assume Hvu: SNoLev v ∈ SNoLev u.
Assume _ _.
We will prove u + y < v + y.
Apply IHu3 to the current goal.
We will prove v ∈ SNoR u.
An exact proof term for the current goal is SNoR_I u Hu1 v Hv1 Hvu Luv.
Assume Hz: z ∈ {x + z|z ∈ SNoR y}.
Apply ReplE_impred (SNoR y) (λz ⇒ x + z) z Hz to the current goal.
Let v be given.
Assume Hv: v ∈ SNoR y.
Assume Hzv: z = x + v.
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev y.
Assume Hv3: y < v.
We prove the intermediate claim Lvy: v ∈ SNoS_ (SNoLev y).
An exact proof term for the current goal is SNoS_I2 v y Hv1 Hy Hv2.
Apply LPE x v (IHRy v Hv) to the current goal.
Assume IHv1: SNo (x + v).
Assume IHv2: ∀u ∈ SNoL x, u + v < x + v.
Assume IHv3: ∀u ∈ SNoR x, x + v < u + v.
Assume IHv4: ∀u ∈ SNoL v, x + u < x + v.
Assume IHv5: ∀u ∈ SNoR v, x + v < x + u.
rewrite the current goal using Hzv (from left to right).
We will prove u + y < x + v.
Apply LPE u v (IHxy u Lux v Lvy) to the current goal.
Assume IHuv1: SNo (u + v).
Assume _ _ _ _.
We will prove u + y < x + v.
Apply SNoLt_tra (u + y) (u + v) (x + v) IHu1 IHuv1 IHv1 to the current goal.
We will prove u + y < u + v.
Apply IHu5 to the current goal.
We will prove v ∈ SNoR y.
An exact proof term for the current goal is SNoR_I y Hy v Hv1 Hv2 Hv3.
We will prove u + v < x + v.
Apply IHv2 to the current goal.
We will prove u ∈ SNoL x.
An exact proof term for the current goal is SNoL_I x Hx u Hu1 Hu2 Hu3.
Assume Hw: w ∈ {x + w|w ∈ SNoL y}.
Apply ReplE_impred (SNoL y) (λz ⇒ x + z) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL y.
Assume Hwu: w = x + u.
Apply SNoL_E y Hy u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev y.
Assume Hu3: u < y.
We prove the intermediate claim Luy: u ∈ SNoS_ (SNoLev y).
An exact proof term for the current goal is SNoS_I2 u y Hu1 Hy Hu2.
Apply LPE x u (IHLy u Hu) to the current goal.
Assume IHu1: SNo (x + u).
Assume IHu2: ∀z ∈ SNoL x, z + u < x + u.
Assume IHu3: ∀z ∈ SNoR x, x + u < z + u.
Assume IHu4: ∀z ∈ SNoL u, x + z < x + u.
Assume IHu5: ∀z ∈ SNoR u, x + u < x + z.
We will prove w < z.
rewrite the current goal using Hwu (from left to right).
We will prove x + u < z.
Apply binunionE R1 R2 z Hz to the current goal.
Assume Hz: z ∈ {z + y|z ∈ SNoR x}.
Apply ReplE_impred (SNoR x) (λz ⇒ z + y) z Hz to the current goal.
Let v be given.
Assume Hv: v ∈ SNoR x.
Assume Hzv: z = v + y.
Apply SNoR_E x Hx v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev x.
Assume Hv3: x < v.
We prove the intermediate claim Lvx: v ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 v x Hv1 Hx Hv2.
Apply LPE v y (IHRx v Hv) to the current goal.
Assume IHv1: SNo (v + y).
Assume IHv2: ∀u ∈ SNoL v, u + y < v + y.
Assume IHv3: ∀u ∈ SNoR v, v + y < u + y.
Assume IHv4: ∀u ∈ SNoL y, v + u < v + y.
Assume IHv5: ∀u ∈ SNoR y, v + y < v + u.
rewrite the current goal using Hzv (from left to right).
We will prove x + u < v + y.
Apply LPE v u (IHxy v Lvx u Luy) to the current goal.
Assume IHvu1: SNo (v + u).
Assume _ _ _ _.
We will prove x + u < v + y.
Apply SNoLt_tra (x + u) (v + u) (v + y) IHu1 IHvu1 IHv1 to the current goal.
We will prove x + u < v + u.
Apply IHu3 to the current goal.
We will prove v ∈ SNoR x.
An exact proof term for the current goal is SNoR_I x Hx v Hv1 Hv2 Hv3.
We will prove v + u < v + y.
Apply IHv4 to the current goal.
We will prove u ∈ SNoL y.
An exact proof term for the current goal is SNoL_I y Hy u Hu1 Hu2 Hu3.
Assume Hz: z ∈ {x + z|z ∈ SNoR y}.
Apply ReplE_impred (SNoR y) (λz ⇒ x + z) z Hz to the current goal.
Let v be given.
Assume Hv: v ∈ SNoR y.
Assume Hzv: z = x + v.
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev y.
Assume Hv3: y < v.
Apply LPE x v (IHRy v Hv) to the current goal.
Assume IHv1: SNo (x + v).
Assume IHv2: ∀u ∈ SNoL x, u + v < x + v.
Assume IHv3: ∀u ∈ SNoR x, x + v < u + v.
Assume IHv4: ∀u ∈ SNoL v, x + u < x + v.
Assume IHv5: ∀u ∈ SNoR v, x + v < x + u.
rewrite the current goal using Hzv (from left to right).
We will prove x + u < x + v.
We prove the intermediate claim Luv: u < v.
An exact proof term for the current goal is SNoLt_tra u y v Hu1 Hy Hv1 Hu3 Hv3.
Apply SNoLtE u v Hu1 Hv1 Luv to the current goal.
Let q be given.
Assume Hq1: SNo q.
Assume Hq2: SNoLev q ∈ SNoLev u ∩ SNoLev v.
Assume _ _.
Assume Hq5: u < q.
Assume Hq6: q < v.
Assume _ _.
Apply binintersectE (SNoLev u) (SNoLev v) (SNoLev q) Hq2 to the current goal.
Assume Hq2u Hq2v.
We prove the intermediate claim Lqy: SNoLev q ∈ SNoLev y.
An exact proof term for the current goal is LLya (SNoLev v) Hv2 (SNoLev q) Hq2v.
We prove the intermediate claim Lqy2: q ∈ SNoS_ (SNoLev y).
An exact proof term for the current goal is SNoS_I2 q y Hq1 Hy Lqy.
We prove the intermediate claim Lxq: SNo (x + q).
Apply LPE x q (IHy q Lqy2) to the current goal.
Assume IHq1 _ _ _ _.
An exact proof term for the current goal is IHq1.
We will prove x + u < x + v.
Apply SNoLt_tra (x + u) (x + q) (x + v) IHu1 Lxq IHv1 to the current goal.
We will prove x + u < x + q.
Apply IHu5 to the current goal.
We will prove q ∈ SNoR u.
An exact proof term for the current goal is SNoR_I u Hu1 q Hq1 Hq2u Hq5.
We will prove x + q < x + v.
Apply IHv4 to the current goal.
We will prove q ∈ SNoL v.
An exact proof term for the current goal is SNoL_I v Hv1 q Hq1 Hq2v Hq6.
Assume Huv: SNoLev u ∈ SNoLev v.
Assume _ _.
We will prove x + u < x + v.
Apply IHv4 to the current goal.
We will prove u ∈ SNoL v.
An exact proof term for the current goal is SNoL_I v Hv1 u Hu1 Huv Luv.
Assume Hvu: SNoLev v ∈ SNoLev u.
Assume _ _.
We will prove x + u < x + v.
Apply IHu5 to the current goal.
We will prove v ∈ SNoR u.
An exact proof term for the current goal is SNoR_I u Hu1 v Hv1 Hvu Luv.
We will prove P x y.
We will prove SNo (x + y) ∧ (∀u ∈ SNoL x, u + y < x + y) ∧ (∀u ∈ SNoR x, x + y < u + y) ∧ (∀u ∈ SNoL y, x + u < x + y) ∧ (∀u ∈ SNoR y, x + y < x + u) ∧ SNoCutP L R.
We prove the intermediate claim LNLR: SNo (SNoCut L R).
An exact proof term for the current goal is SNoCutP_SNo_SNoCut L R LLR.
Apply andI to the current goal.
rewrite the current goal using add_SNo_eq x Hx y Hy (from left to right).
Apply and5I to the current goal.
We will prove SNo (SNoCut L R).
An exact proof term for the current goal is LNLR.
We will prove ∀u ∈ SNoL x, u + y < SNoCut L R.
Let u be given.
Assume Hu: u ∈ SNoL x.
We will prove u + y < SNoCut L R.
Apply SNoL_E x Hx 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 LuyL: u + y ∈ L.
We will prove u + y ∈ L1 ∪ L2.
Apply binunionI1 to the current goal.
We will prove u + y ∈ {w + y|w ∈ SNoL x}.
Apply ReplI (SNoL x) (λw ⇒ w + y) u to the current goal.
We will prove u ∈ SNoL x.
An exact proof term for the current goal is Hu.
We will prove u + y < SNoCut L R.
An exact proof term for the current goal is SNoCutP_SNoCut_L L R LLR (u + y) LuyL.
We will prove ∀u ∈ SNoR x, SNoCut L R < u + y.
Let u be given.
Assume Hu: u ∈ SNoR x.
We will prove SNoCut L R < u + y.
Apply SNoR_E x Hx 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 LuyR: u + y ∈ R.
We will prove u + y ∈ R1 ∪ R2.
Apply binunionI1 to the current goal.
We will prove u + y ∈ {z + y|z ∈ SNoR x}.
Apply ReplI (SNoR x) (λw ⇒ w + y) u to the current goal.
We will prove u ∈ SNoR x.
An exact proof term for the current goal is Hu.
We will prove SNoCut L R < u + y.
An exact proof term for the current goal is SNoCutP_SNoCut_R L R LLR (u + y) LuyR.
We will prove ∀u ∈ SNoL y, x + u < SNoCut L R.
Let u be given.
Assume Hu: u ∈ SNoL y.
We will prove x + u < SNoCut L R.
Apply SNoL_E y Hy u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev y.
Assume Hu3: u < y.
We prove the intermediate claim LxuL: x + u ∈ L.
We will prove x + u ∈ L1 ∪ L2.
Apply binunionI2 to the current goal.
We will prove x + u ∈ {x + w|w ∈ SNoL y}.
Apply ReplI (SNoL y) (λw ⇒ x + w) u to the current goal.
We will prove u ∈ SNoL y.
An exact proof term for the current goal is Hu.
We will prove x + u < SNoCut L R.
An exact proof term for the current goal is SNoCutP_SNoCut_L L R LLR (x + u) LxuL.
We will prove ∀u ∈ SNoR y, SNoCut L R < x + u.
Let u be given.
Assume Hu: u ∈ SNoR y.
We will prove SNoCut L R < x + u.
Apply SNoR_E y Hy u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev y.
Assume Hu3: y < u.
We prove the intermediate claim LxuR: x + u ∈ R.
We will prove x + u ∈ R1 ∪ R2.
Apply binunionI2 to the current goal.
We will prove x + u ∈ {x + z|z ∈ SNoR y}.
Apply ReplI (SNoR y) (λz ⇒ x + z) u to the current goal.
We will prove u ∈ SNoR y.
An exact proof term for the current goal is Hu.
We will prove SNoCut L R < x + u.
An exact proof term for the current goal is SNoCutP_SNoCut_R L R LLR (x + u) LxuR.
An exact proof term for the current goal is LLR.
∎