Beginning of Section SurrealAdd
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Definition. We define add_SNo to be SNo_rec2 (λx y a ⇒ SNoCut ({a w y|w ∈ SNoL x} ∪ {a x w|w ∈ SNoL y}) ({a z y|z ∈ SNoR x} ∪ {a x z|z ∈ SNoR y})) of type set → set → set.
In Proofgold the corresponding term root is 127d04... and object id is f62f9a...
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Theorem. (add_SNo_eq)
∀x, SNo x → ∀y, SNo y → x + y = SNoCut ({w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}) ({z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y})
In Proofgold the corresponding term root is 0c1128... and proposition id is 437a9c...
Proof:
Set F to be the term λx y a ⇒ SNoCut ({a w y|w ∈ SNoL x} ∪ {a x w|w ∈ SNoL y}) ({a z y|z ∈ SNoR x} ∪ {a x z|z ∈ SNoR y}) of type set → set → (set → set → set) → set.
We prove the intermediate claim L1: ∀x, SNo x → ∀y, SNo y → ∀g h : set → set → set, (∀w ∈ SNoS_ (SNoLev x), ∀z, SNo z → g w z = h w z) → (∀z ∈ SNoS_ (SNoLev y), g x z = h x z) → F x y g = F x y h.
Let x be given.
Assume Hx: SNo x.
Let y be given.
Assume Hy: SNo y.
Let g and h be given.
Assume Hgh1: ∀w ∈ SNoS_ (SNoLev x), ∀z, SNo z → g w z = h w z.
Assume Hgh2: ∀z ∈ SNoS_ (SNoLev y), g x z = h x z.
We will prove F x y g = F x y h.
We prove the intermediate claim L1a: {g w y|w ∈ SNoL x} = {h w y|w ∈ SNoL x}.
Apply ReplEq_ext to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL x.
We will prove g w y = h w y.
Apply Hgh1 to the current goal.
We will prove w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoL_SNoS x Hx w Hw.
We will prove SNo y.
An exact proof term for the current goal is Hy.
We prove the intermediate claim L1b: {g x w|w ∈ SNoL y} = {h x w|w ∈ SNoL y}.
Apply ReplEq_ext to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL y.
We will prove g x w = h x w.
Apply Hgh2 to the current goal.
We will prove w ∈ SNoS_ (SNoLev y).
An exact proof term for the current goal is SNoL_SNoS y Hy w Hw.
We prove the intermediate claim L1c: {g z y|z ∈ SNoR x} = {h z y|z ∈ SNoR x}.
Apply ReplEq_ext to the current goal.
Let z be given.
Assume Hz: z ∈ SNoR x.
We will prove g z y = h z y.
Apply Hgh1 to the current goal.
We will prove z ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoR_SNoS x Hx z Hz.
We will prove SNo y.
An exact proof term for the current goal is Hy.
We prove the intermediate claim L1d: {g x z|z ∈ SNoR y} = {h x z|z ∈ SNoR y}.
Apply ReplEq_ext to the current goal.
Let z be given.
Assume Hz: z ∈ SNoR y.
We will prove g x z = h x z.
Apply Hgh2 to the current goal.
We will prove z ∈ SNoS_ (SNoLev y).
An exact proof term for the current goal is SNoR_SNoS y Hy z Hz.
We will prove SNoCut ({g w y|w ∈ SNoL x} ∪ {g x w|w ∈ SNoL y}) ({g z y|z ∈ SNoR x} ∪ {g x z|z ∈ SNoR y}) = SNoCut ({h w y|w ∈ SNoL x} ∪ {h x w|w ∈ SNoL y}) ({h z y|z ∈ SNoR x} ∪ {h x z|z ∈ SNoR y}).
rewrite the current goal using L1a (from left to right).
rewrite the current goal using L1b (from left to right).
rewrite the current goal using L1c (from left to right).
rewrite the current goal using L1d (from left to right).
Use reflexivity.
An exact proof term for the current goal is SNo_rec2_eq F L1.
∎
Theorem. (add_SNo_prop1)
∀x y, SNo x → SNo 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})
In Proofgold the corresponding term root is f3ece7... and proposition id is 5a879f...
Proof:
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.
∎
Theorem. (SNo_add_SNo)
∀x y, SNo x → SNo y → SNo (x + y)
In Proofgold the corresponding term root is c4a9a6... and proposition id is a57095...
Proof:
Let x and y be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Apply add_SNo_prop1 x y Hx Hy 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 H _ _ _ _ _.
An exact proof term for the current goal is H.
∎
Theorem. (SNo_add_SNo_3)
∀x y z, SNo x → SNo y → SNo z → SNo (x + y + z)
In Proofgold the corresponding term root is f6ef07... and proposition id is f2d78c...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz.
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hx.
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Hz.
∎
Theorem. (SNo_add_SNo_3c)
∀x y z, SNo x → SNo y → SNo z → SNo (x + y + - z)
In Proofgold the corresponding term root is 104eb9... and proposition id is 833be8...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz.
Apply SNo_add_SNo_3 to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hy.
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hz.
∎
Theorem. (SNo_add_SNo_4)
∀x y z w, SNo x → SNo y → SNo z → SNo w → SNo (x + y + z + w)
In Proofgold the corresponding term root is d71f0e... and proposition id is 42037e...
Proof:
Let x, y, z and w be given.
Assume Hx Hy Hz Hw.
An exact proof term for the current goal is SNo_add_SNo_3 x y (z + w) Hx Hy (SNo_add_SNo z w Hz Hw).
∎
Theorem. (add_SNo_Lt1)
∀x y z, SNo x → SNo y → SNo z → x < z → x + y < z + y
In Proofgold the corresponding term root is 92232f... and proposition id is cb0738...
Proof:
Let x, y and z be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume Hz: SNo z.
Assume Hxz: x < z.
Apply add_SNo_prop1 x y Hx Hy 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: SNo (x + y).
Assume _.
Assume H2: ∀u ∈ SNoR x, x + y < u + y.
Assume _ _ _.
Apply add_SNo_prop1 z y Hz Hy 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 H3: SNo (z + y).
Assume H4: ∀u ∈ SNoL z, u + y < z + y.
Assume _ _ _ _.
Apply SNoLtE x z Hx Hz Hxz to the current goal.
Let w be given.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev x ∩ SNoLev z.
Assume _ _.
Assume Hw5: x < w.
Assume Hw6: w < z.
Assume _ _.
Apply binintersectE (SNoLev x) (SNoLev z) (SNoLev w) Hw2 to the current goal.
Assume Hw2x Hw2z.
We will prove x + y < z + y.
Apply SNoLt_tra (x + y) (w + y) (z + y) H1 (SNo_add_SNo w y Hw1 Hy) H3 to the current goal.
We will prove x + y < w + y.
Apply H2 to the current goal.
We will prove w ∈ SNoR x.
Apply SNoR_I x Hx w Hw1 to the current goal.
We will prove SNoLev w ∈ SNoLev x.
An exact proof term for the current goal is Hw2x.
We will prove x < w.
An exact proof term for the current goal is Hw5.
We will prove w + y < z + y.
Apply H4 to the current goal.
We will prove w ∈ SNoL z.
Apply SNoL_I z Hz w Hw1 to the current goal.
We will prove SNoLev w ∈ SNoLev z.
An exact proof term for the current goal is Hw2z.
We will prove w < z.
An exact proof term for the current goal is Hw6.
Assume Hxz1: SNoLev x ∈ SNoLev z.
Assume _ _.
We will prove x + y < z + y.
Apply H4 to the current goal.
We will prove x ∈ SNoL z.
Apply SNoL_I z Hz x Hx to the current goal.
We will prove SNoLev x ∈ SNoLev z.
An exact proof term for the current goal is Hxz1.
We will prove x < z.
An exact proof term for the current goal is Hxz.
Assume Hzx: SNoLev z ∈ SNoLev x.
Assume _ _.
We will prove x + y < z + y.
Apply H2 to the current goal.
We will prove z ∈ SNoR x.
Apply SNoR_I x Hx z Hz to the current goal.
We will prove SNoLev z ∈ SNoLev x.
An exact proof term for the current goal is Hzx.
We will prove x < z.
An exact proof term for the current goal is Hxz.
∎
Theorem. (add_SNo_Le1)
∀x y z, SNo x → SNo y → SNo z → x ≤ z → x + y ≤ z + y
In Proofgold the corresponding term root is d8f37e... and proposition id is abcf72...
Proof:
Let x, y and z be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume Hz: SNo z.
Assume Hxz: x ≤ z.
We will prove x + y ≤ z + y.
Apply SNoLeE x z Hx Hz Hxz to the current goal.
Assume H1: x < z.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is add_SNo_Lt1 x y z Hx Hy Hz H1.
Assume H1: x = z.
rewrite the current goal using H1 (from left to right).
Apply SNoLe_ref to the current goal.
∎
Theorem. (add_SNo_Lt2)
∀x y z, SNo x → SNo y → SNo z → y < z → x + y < x + z
In Proofgold the corresponding term root is 6ad464... and proposition id is 6f0941...
Proof:
Let x, y and z be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume Hz: SNo z.
Assume Hyz: y < z.
Apply add_SNo_prop1 x y Hx Hy 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: SNo (x + y).
Assume _ _ _.
Assume H2: ∀u ∈ SNoR y, x + y < x + u.
Assume _.
Apply add_SNo_prop1 x z Hx Hz 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 H3: SNo (x + z).
Assume _ _.
Assume H4: ∀u ∈ SNoL z, x + u < x + z.
Assume _ _.
Apply SNoLtE y z Hy Hz Hyz to the current goal.
Let w be given.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev y ∩ SNoLev z.
Assume _ _.
Assume Hw5: y < w.
Assume Hw6: w < z.
Assume _ _.
Apply binintersectE (SNoLev y) (SNoLev z) (SNoLev w) Hw2 to the current goal.
Assume Hw2y Hw2z.
We will prove x + y < x + z.
Apply SNoLt_tra (x + y) (x + w) (x + z) H1 (SNo_add_SNo x w Hx Hw1) H3 to the current goal.
We will prove x + y < x + w.
Apply H2 to the current goal.
We will prove w ∈ SNoR y.
Apply SNoR_I y Hy w Hw1 to the current goal.
We will prove SNoLev w ∈ SNoLev y.
An exact proof term for the current goal is Hw2y.
We will prove y < w.
An exact proof term for the current goal is Hw5.
We will prove x + w < x + z.
Apply H4 to the current goal.
We will prove w ∈ SNoL z.
Apply SNoL_I z Hz w Hw1 to the current goal.
We will prove SNoLev w ∈ SNoLev z.
An exact proof term for the current goal is Hw2z.
We will prove w < z.
An exact proof term for the current goal is Hw6.
Assume Hyz1: SNoLev y ∈ SNoLev z.
Assume _ _.
We will prove x + y < x + z.
Apply H4 to the current goal.
We will prove y ∈ SNoL z.
Apply SNoL_I z Hz y Hy to the current goal.
We will prove SNoLev y ∈ SNoLev z.
An exact proof term for the current goal is Hyz1.
We will prove y < z.
An exact proof term for the current goal is Hyz.
Assume Hzy: SNoLev z ∈ SNoLev y.
Assume _ _.
We will prove x + y < x + z.
Apply H2 to the current goal.
We will prove z ∈ SNoR y.
Apply SNoR_I y Hy z Hz to the current goal.
We will prove SNoLev z ∈ SNoLev y.
An exact proof term for the current goal is Hzy.
We will prove y < z.
An exact proof term for the current goal is Hyz.
∎
Theorem. (add_SNo_Le2)
∀x y z, SNo x → SNo y → SNo z → y ≤ z → x + y ≤ x + z
In Proofgold the corresponding term root is 14975e... and proposition id is 3f52ba...
Proof:
Let x, y and z be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume Hz: SNo z.
Assume Hyz: y ≤ z.
We will prove x + y ≤ x + z.
Apply SNoLeE y z Hy Hz Hyz to the current goal.
Assume H1: y < z.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is add_SNo_Lt2 x y z Hx Hy Hz H1.
Assume H1: y = z.
rewrite the current goal using H1 (from left to right).
Apply SNoLe_ref to the current goal.
∎
Theorem. (add_SNo_Lt3a)
∀x y z w, SNo x → SNo y → SNo z → SNo w → x < z → y ≤ w → x + y < z + w
In Proofgold the corresponding term root is b2215f... and proposition id is 18ff91...
Proof:
Let x, y, z and w be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume Hz: SNo z.
Assume Hw: SNo w.
Assume Hxz: x < z.
Assume Hyw: y ≤ w.
Apply SNoLtLe_tra (x + y) (z + y) (z + w) (SNo_add_SNo x y Hx Hy) (SNo_add_SNo z y Hz Hy) (SNo_add_SNo z w Hz Hw) to the current goal.
We will prove x + y < z + y.
An exact proof term for the current goal is add_SNo_Lt1 x y z Hx Hy Hz Hxz.
We will prove z + y ≤ z + w.
An exact proof term for the current goal is add_SNo_Le2 z y w Hz Hy Hw Hyw.
∎
Theorem. (add_SNo_Lt3b)
∀x y z w, SNo x → SNo y → SNo z → SNo w → x ≤ z → y < w → x + y < z + w
In Proofgold the corresponding term root is 5b4f92... and proposition id is 8fe0d9...
Proof:
Let x, y, z and w be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume Hz: SNo z.
Assume Hw: SNo w.
Assume Hxz: x ≤ z.
Assume Hyw: y < w.
Apply SNoLeLt_tra (x + y) (z + y) (z + w) (SNo_add_SNo x y Hx Hy) (SNo_add_SNo z y Hz Hy) (SNo_add_SNo z w Hz Hw) to the current goal.
We will prove x + y ≤ z + y.
An exact proof term for the current goal is add_SNo_Le1 x y z Hx Hy Hz Hxz.
We will prove z + y < z + w.
An exact proof term for the current goal is add_SNo_Lt2 z y w Hz Hy Hw Hyw.
∎
Theorem. (add_SNo_Lt3)
∀x y z w, SNo x → SNo y → SNo z → SNo w → x < z → y < w → x + y < z + w
In Proofgold the corresponding term root is 7141a8... and proposition id is 55bdab...
Proof:
Let x, y, z and w be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume Hz: SNo z.
Assume Hw: SNo w.
Assume Hxz: x < z.
Assume Hyw: y < w.
Apply add_SNo_Lt3a x y z w Hx Hy Hz Hw Hxz to the current goal.
We will prove y ≤ w.
Apply SNoLtLe to the current goal.
We will prove y < w.
An exact proof term for the current goal is Hyw.
∎
Theorem. (add_SNo_Le3)
∀x y z w, SNo x → SNo y → SNo z → SNo w → x ≤ z → y ≤ w → x + y ≤ z + w
In Proofgold the corresponding term root is 0be637... and proposition id is be66ca...
Proof:
Let x, y, z and w be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume Hz: SNo z.
Assume Hw: SNo w.
Assume Hxz: x ≤ z.
Assume Hyw: y ≤ w.
Apply SNoLe_tra (x + y) (z + y) (z + w) (SNo_add_SNo x y Hx Hy) (SNo_add_SNo z y Hz Hy) (SNo_add_SNo z w Hz Hw) to the current goal.
We will prove x + y ≤ z + y.
An exact proof term for the current goal is add_SNo_Le1 x y z Hx Hy Hz Hxz.
We will prove z + y ≤ z + w.
An exact proof term for the current goal is add_SNo_Le2 z y w Hz Hy Hw Hyw.
∎
Theorem. (add_SNo_SNoCutP)
∀x y, SNo x → SNo y → SNoCutP ({w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}) ({z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y})
In Proofgold the corresponding term root is e2b7d7... and proposition id is f86b1a...
Proof:
Let x and y be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Apply add_SNo_prop1 x y Hx Hy to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
∎
Theorem. (add_SNo_com)
∀x y, SNo x → SNo y → x + y = y + x
In Proofgold the corresponding term root is 548814... and proposition id is f017e5...
Proof:
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), w + y = y + w.
Assume IHy: ∀z ∈ SNoS_ (SNoLev y), x + z = z + x.
Assume IHxy: ∀w ∈ SNoS_ (SNoLev x), ∀z ∈ SNoS_ (SNoLev y), w + z = z + w.
We prove the intermediate claim IHLx: ∀w ∈ SNoL x, w + y = y + w.
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, w + y = y + w.
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, x + w = w + x.
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, x + w = w + x.
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 will prove x + y = y + x.
Set Lxy1 to be the term {w + y|w ∈ SNoL x}.
Set Lxy2 to be the term {x + w|w ∈ SNoL y}.
Set Rxy1 to be the term {z + y|z ∈ SNoR x}.
Set Rxy2 to be the term {x + z|z ∈ SNoR y}.
rewrite the current goal using add_SNo_eq x Hx y Hy (from left to right).
We will prove (SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2)) = y + x.
Set Lyx1 to be the term {w + x|w ∈ SNoL y}.
Set Lyx2 to be the term {y + w|w ∈ SNoL x}.
Set Ryx1 to be the term {z + x|z ∈ SNoR y}.
Set Ryx2 to be the term {y + z|z ∈ SNoR x}.
rewrite the current goal using add_SNo_eq y Hy x Hx (from left to right).
We will prove (SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2)) = (SNoCut (Lyx1 ∪ Lyx2) (Ryx1 ∪ Ryx2)).
We prove the intermediate claim Lxy1yx2: Lxy1 = Lyx2.
We will prove {w + y|w ∈ SNoL x} = {y + w|w ∈ SNoL x}.
Apply ReplEq_ext (SNoL x) (λw ⇒ w + y) (λw ⇒ y + w) to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL x.
We will prove w + y = y + w.
An exact proof term for the current goal is IHLx w Hw.
We prove the intermediate claim Lxy2yx1: Lxy2 = Lyx1.
We will prove {x + w|w ∈ SNoL y} = {w + x|w ∈ SNoL y}.
Apply ReplEq_ext (SNoL y) (λw ⇒ x + w) (λw ⇒ w + x) to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL y.
We will prove x + w = w + x.
An exact proof term for the current goal is IHLy w Hw.
We prove the intermediate claim Rxy1yx2: Rxy1 = Ryx2.
We will prove {w + y|w ∈ SNoR x} = {y + w|w ∈ SNoR x}.
Apply ReplEq_ext (SNoR x) (λw ⇒ w + y) (λw ⇒ y + w) to the current goal.
Let w be given.
Assume Hw: w ∈ SNoR x.
We will prove w + y = y + w.
An exact proof term for the current goal is IHRx w Hw.
We prove the intermediate claim Rxy2yx1: Rxy2 = Ryx1.
We will prove {x + w|w ∈ SNoR y} = {w + x|w ∈ SNoR y}.
Apply ReplEq_ext (SNoR y) (λw ⇒ x + w) (λw ⇒ w + x) to the current goal.
Let w be given.
Assume Hw: w ∈ SNoR y.
We will prove x + w = w + x.
An exact proof term for the current goal is IHRy w Hw.
rewrite the current goal using Lxy1yx2 (from left to right).
rewrite the current goal using Lxy2yx1 (from left to right).
rewrite the current goal using Rxy1yx2 (from left to right).
rewrite the current goal using Rxy2yx1 (from left to right).
We will prove (SNoCut (Lyx2 ∪ Lyx1) (Ryx2 ∪ Ryx1)) = (SNoCut (Lyx1 ∪ Lyx2) (Ryx1 ∪ Ryx2)).
rewrite the current goal using binunion_com Lyx2 Lyx1 (from left to right).
rewrite the current goal using binunion_com Ryx2 Ryx1 (from left to right).
Use reflexivity.
∎
Theorem. (add_SNo_0L)
∀x, SNo x → 0 + x = x
In Proofgold the corresponding term root is 107598... and proposition id is 446bad...
Proof:
Apply SNoLev_ind to the current goal.
Let x be given.
Assume Hx: SNo x.
Assume IH: ∀w ∈ SNoS_ (SNoLev x), 0 + w = w.
We will prove 0 + x = x.
rewrite the current goal using add_SNo_eq 0 SNo_0 x Hx (from left to right).
We will prove SNoCut ({w + x|w ∈ SNoL 0} ∪ {0 + w|w ∈ SNoL x}) ({w + x|w ∈ SNoR 0} ∪ {0 + w|w ∈ SNoR x}) = x.
We prove the intermediate claim L1: {w + x|w ∈ SNoL 0} ∪ {0 + w|w ∈ SNoL x} = SNoL x.
rewrite the current goal using SNoL_0 (from left to right).
We will prove {w + x|w ∈ Empty} ∪ {0 + w|w ∈ SNoL x} = SNoL x.
rewrite the current goal using Repl_Empty (λw ⇒ w + x) (from left to right).
We will prove Empty ∪ {0 + w|w ∈ SNoL x} = SNoL x.
rewrite the current goal using binunion_idl (from left to right).
We will prove {0 + w|w ∈ SNoL x} = SNoL x.
Apply set_ext to the current goal.
Let u be given.
Assume Hu: u ∈ {0 + w|w ∈ SNoL x}.
Apply ReplE_impred (SNoL x) (λw ⇒ 0 + w) u Hu to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL x.
Assume H1: u = 0 + w.
We will prove u ∈ SNoL x.
rewrite the current goal using H1 (from left to right).
We will prove 0 + w ∈ SNoL x.
rewrite the current goal using IH w (SNoL_SNoS_ x w Hw) (from left to right).
We will prove w ∈ SNoL x.
An exact proof term for the current goal is Hw.
Let u be given.
Assume Hu: u ∈ SNoL x.
We will prove u ∈ {0 + w|w ∈ SNoL x}.
rewrite the current goal using IH u (SNoL_SNoS_ x u Hu) (from right to left).
We will prove 0 + u ∈ {0 + w|w ∈ SNoL x}.
An exact proof term for the current goal is ReplI (SNoL x) (λw ⇒ 0 + w) u Hu.
We prove the intermediate claim L2: {w + x|w ∈ SNoR 0} ∪ {0 + w|w ∈ SNoR x} = SNoR x.
rewrite the current goal using SNoR_0 (from left to right).
We will prove {w + x|w ∈ Empty} ∪ {0 + w|w ∈ SNoR x} = SNoR x.
rewrite the current goal using Repl_Empty (λw ⇒ w + x) (from left to right).
We will prove Empty ∪ {0 + w|w ∈ SNoR x} = SNoR x.
rewrite the current goal using binunion_idl (from left to right).
We will prove {0 + w|w ∈ SNoR x} = SNoR x.
Apply set_ext to the current goal.
Let u be given.
Assume Hu: u ∈ {0 + w|w ∈ SNoR x}.
Apply ReplE_impred (SNoR x) (λw ⇒ 0 + w) u Hu to the current goal.
Let w be given.
Assume Hw: w ∈ SNoR x.
Assume H1: u = 0 + w.
We will prove u ∈ SNoR x.
rewrite the current goal using H1 (from left to right).
We will prove 0 + w ∈ SNoR x.
rewrite the current goal using IH w (SNoR_SNoS_ x w Hw) (from left to right).
We will prove w ∈ SNoR x.
An exact proof term for the current goal is Hw.
Let u be given.
Assume Hu: u ∈ SNoR x.
We will prove u ∈ {0 + w|w ∈ SNoR x}.
rewrite the current goal using IH u (SNoR_SNoS_ x u Hu) (from right to left).
We will prove 0 + u ∈ {0 + w|w ∈ SNoR x}.
An exact proof term for the current goal is ReplI (SNoR x) (λw ⇒ 0 + w) u Hu.
rewrite the current goal using L1 (from left to right).
rewrite the current goal using L2 (from left to right).
We will prove SNoCut (SNoL x) (SNoR x) = x.
Use symmetry.
An exact proof term for the current goal is SNo_eta x Hx.
∎
Theorem. (add_SNo_0R)
∀x, SNo x → x + 0 = x
In Proofgold the corresponding term root is d8a186... and proposition id is 1a7fa1...
Proof:
Let x be given.
Assume Hx: SNo x.
rewrite the current goal using add_SNo_com x 0 Hx SNo_0 (from left to right).
An exact proof term for the current goal is add_SNo_0L x Hx.
∎
Theorem. (add_SNo_minus_SNo_linv)
∀x, SNo x → - x + x = 0
In Proofgold the corresponding term root is 424719... and proposition id is 44e251...
Proof:
Apply SNoLev_ind to the current goal.
Let x be given.
Assume Hx: SNo x.
Assume IH: ∀w ∈ SNoS_ (SNoLev x), - w + w = 0.
We will prove - x + x = 0.
We prove the intermediate claim Lmx: SNo (- x).
An exact proof term for the current goal is SNo_minus_SNo x Hx.
Set L1 to be the term {w + x|w ∈ SNoL (- x)}.
Set L2 to be the term {- x + w|w ∈ SNoL x}.
Set R1 to be the term {z + x|z ∈ SNoR (- x)}.
Set R2 to be the term {- x + z|z ∈ SNoR x}.
Set L to be the term L1 ∪ L2.
Set R to be the term R1 ∪ R2.
rewrite the current goal using add_SNo_eq (- x) Lmx x Hx (from left to right).
We will prove SNoCut L R = 0.
We prove the intermediate claim LLR: SNoCutP L R.
An exact proof term for the current goal is add_SNo_SNoCutP (- x) x Lmx Hx.
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.
We prove the intermediate claim Lfst: SNoLev (SNoCut L R) ⊆ SNoLev 0 ∧ SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) 0.
Apply SNoCutP_SNoCut_fst L R LLR 0 SNo_0 to the current goal.
We will prove ∀w ∈ L, w < 0.
Let w be given.
Assume Hw: w ∈ L.
Apply binunionE L1 L2 w Hw to the current goal.
Assume Hw: w ∈ {w + x|w ∈ SNoL (- x)}.
Apply ReplE_impred (SNoL (- x)) (λz ⇒ z + x) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL (- x).
Assume Hwu: w = u + x.
Apply SNoL_E (- x) Lmx 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 Lmu: SNo (- u).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hu1.
We prove the intermediate claim Lmuu: - u + u = 0.
Apply IH to the current goal.
We will prove u ∈ SNoS_ (SNoLev x).
Apply SNoS_I2 u x Hu1 Hx to the current goal.
We will prove SNoLev u ∈ SNoLev x.
rewrite the current goal using minus_SNo_Lev x Hx (from right to left).
We will prove SNoLev u ∈ SNoLev (- x).
An exact proof term for the current goal is Hu2.
We prove the intermediate claim Lxmu: x < - u.
rewrite the current goal using minus_SNo_invol x Hx (from right to left).
We will prove - - x < - u.
Apply minus_SNo_Lt_contra u (- x) Hu1 Lmx to the current goal.
We will prove u < - x.
An exact proof term for the current goal is Hu3.
We will prove w < 0.
rewrite the current goal using Hwu (from left to right).
We will prove u + x < 0.
rewrite the current goal using add_SNo_com u x Hu1 Hx (from left to right).
We will prove x + u < 0.
rewrite the current goal using Lmuu (from right to left).
We will prove x + u < - u + u.
Apply add_SNo_Lt1 x u (- u) Hx Hu1 Lmu to the current goal.
We will prove x < - u.
An exact proof term for the current goal is Lxmu.
Assume Hw: w ∈ {- x + w|w ∈ SNoL x}.
Apply ReplE_impred (SNoL x) (λz ⇒ - x + z) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL x.
Assume Hwu: w = - x + u.
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 Lmu: SNo (- u).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hu1.
We prove the intermediate claim Lmuu: - u + u = 0.
Apply IH to the current goal.
We will prove u ∈ SNoS_ (SNoLev x).
Apply SNoS_I2 u x Hu1 Hx to the current goal.
We will prove SNoLev u ∈ SNoLev x.
An exact proof term for the current goal is Hu2.
We prove the intermediate claim Lmxmu: - x < - u.
Apply minus_SNo_Lt_contra u x Hu1 Hx to the current goal.
We will prove u < x.
An exact proof term for the current goal is Hu3.
We will prove w < 0.
rewrite the current goal using Hwu (from left to right).
We will prove - x + u < 0.
rewrite the current goal using Lmuu (from right to left).
We will prove - x + u < - u + u.
Apply add_SNo_Lt1 (- x) u (- u) Lmx Hu1 Lmu to the current goal.
We will prove - x < - u.
An exact proof term for the current goal is Lmxmu.
We will prove ∀z ∈ R, 0 < z.
Let z be given.
Assume Hz: z ∈ R.
Apply binunionE R1 R2 z Hz to the current goal.
Assume Hz: z ∈ {z + x|z ∈ SNoR (- x)}.
Apply ReplE_impred (SNoR (- x)) (λz ⇒ z + x) z Hz to the current goal.
Let v be given.
Assume Hv: v ∈ SNoR (- x).
Assume Hzv: z = v + x.
Apply SNoR_E (- x) Lmx 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 Lmv: SNo (- v).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hv1.
We prove the intermediate claim Lmvv: - v + v = 0.
Apply IH to the current goal.
We will prove v ∈ SNoS_ (SNoLev x).
Apply SNoS_I2 v x Hv1 Hx to the current goal.
We will prove SNoLev v ∈ SNoLev x.
rewrite the current goal using minus_SNo_Lev x Hx (from right to left).
We will prove SNoLev v ∈ SNoLev (- x).
An exact proof term for the current goal is Hv2.
We prove the intermediate claim Lmvx: - v < x.
rewrite the current goal using minus_SNo_invol x Hx (from right to left).
We will prove - v < - - x.
Apply minus_SNo_Lt_contra (- x) v Lmx Hv1 to the current goal.
We will prove - x < v.
An exact proof term for the current goal is Hv3.
We will prove 0 < z.
rewrite the current goal using Hzv (from left to right).
We will prove 0 < v + x.
rewrite the current goal using add_SNo_com v x Hv1 Hx (from left to right).
We will prove 0 < x + v.
rewrite the current goal using Lmvv (from right to left).
We will prove - v + v < x + v.
Apply add_SNo_Lt1 (- v) v x Lmv Hv1 Hx to the current goal.
We will prove - v < x.
An exact proof term for the current goal is Lmvx.
Assume Hz: z ∈ {- x + z|z ∈ SNoR x}.
Apply ReplE_impred (SNoR x) (λz ⇒ - x + z) z Hz to the current goal.
Let v be given.
Assume Hv: v ∈ SNoR x.
Assume Hzv: z = - x + v.
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 Lmv: SNo (- v).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hv1.
We prove the intermediate claim Lmvv: - v + v = 0.
Apply IH to the current goal.
We will prove v ∈ SNoS_ (SNoLev x).
Apply SNoS_I2 v x Hv1 Hx to the current goal.
We will prove SNoLev v ∈ SNoLev x.
An exact proof term for the current goal is Hv2.
We prove the intermediate claim Lmvmx: - v < - x.
Apply minus_SNo_Lt_contra x v Hx Hv1 to the current goal.
We will prove x < v.
An exact proof term for the current goal is Hv3.
We will prove 0 < z.
rewrite the current goal using Hzv (from left to right).
We will prove 0 < - x + v.
rewrite the current goal using Lmvv (from right to left).
We will prove - v + v < - x + v.
Apply add_SNo_Lt1 (- v) v (- x) Lmv Hv1 Lmx to the current goal.
We will prove - v < - x.
An exact proof term for the current goal is Lmvmx.
Apply Lfst to the current goal.
Assume H1: SNoLev (SNoCut L R) ⊆ SNoLev 0.
Assume H2: SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) 0.
Apply SNo_eq (SNoCut L R) 0 LNLR SNo_0 to the current goal.
We will prove SNoLev (SNoCut L R) = SNoLev 0.
Apply set_ext to the current goal.
An exact proof term for the current goal is H1.
rewrite the current goal using ordinal_SNoLev 0 ordinal_Empty (from left to right).
We will prove 0 ⊆ SNoLev (SNoCut L R).
Apply Subq_Empty to the current goal.
We will prove SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) 0.
An exact proof term for the current goal is H2.
∎
Theorem. (add_SNo_minus_SNo_rinv)
∀x, SNo x → x + - x = 0
In Proofgold the corresponding term root is 9e8c44... and proposition id is b2f9cf...
Proof:
Let x be given.
Assume Hx: SNo x.
We prove the intermediate claim Lmx: SNo (- x).
An exact proof term for the current goal is SNo_minus_SNo x Hx.
We will prove x + - x = 0.
rewrite the current goal using add_SNo_com x (- x) Hx Lmx (from left to right).
We will prove - x + x = 0.
An exact proof term for the current goal is add_SNo_minus_SNo_linv x Hx.
∎
Theorem. (add_SNo_ordinal_SNoCutP)
∀alpha, ordinal alpha → ∀beta, ordinal beta → SNoCutP ({x + beta|x ∈ SNoS_ alpha} ∪ {alpha + x|x ∈ SNoS_ beta}) Empty
In Proofgold the corresponding term root is 2823e4... and proposition id is 507eab...
Proof:
Let alpha be given.
Assume Ha: ordinal alpha.
Let beta be given.
Assume Hb: ordinal beta.
Set Lo1 to be the term {x + beta|x ∈ SNoS_ alpha}.
Set Lo2 to be the term {alpha + x|x ∈ SNoS_ beta}.
We will prove (∀x ∈ Lo1 ∪ Lo2, SNo x) ∧ (∀y ∈ Empty, SNo y) ∧ (∀x ∈ Lo1 ∪ Lo2, ∀y ∈ Empty, x < y).
Apply and3I to the current goal.
Let w be given.
Assume Hw: w ∈ Lo1 ∪ Lo2.
Apply binunionE Lo1 Lo2 w Hw to the current goal.
Assume H1: w ∈ Lo1.
Apply ReplE_impred (SNoS_ alpha) (λx ⇒ x + beta) w H1 to the current goal.
Let x be given.
Assume Hx: x ∈ SNoS_ alpha.
Assume H2: w = x + beta.
Apply SNoS_E2 alpha Ha x Hx to the current goal.
Assume _ _.
Assume Hx2: SNo x.
Assume _.
We will prove SNo w.
rewrite the current goal using H2 (from left to right).
We will prove SNo (x + beta).
An exact proof term for the current goal is SNo_add_SNo x beta Hx2 (ordinal_SNo beta Hb).
Assume H1: w ∈ Lo2.
Apply ReplE_impred (SNoS_ beta) (λx ⇒ alpha + x) w H1 to the current goal.
Let x be given.
Assume Hx: x ∈ SNoS_ beta.
Assume H2: w = alpha + x.
Apply SNoS_E2 beta Hb x Hx to the current goal.
Assume _ _.
Assume Hx2: SNo x.
Assume _.
We will prove SNo w.
rewrite the current goal using H2 (from left to right).
We will prove SNo (alpha + x).
An exact proof term for the current goal is SNo_add_SNo alpha x (ordinal_SNo alpha Ha) Hx2.
Let y be given.
Assume Hy: y ∈ Empty.
We will prove False.
An exact proof term for the current goal is EmptyE y Hy.
Let x be given.
Assume _.
Let y be given.
Assume Hy: y ∈ Empty.
We will prove False.
An exact proof term for the current goal is EmptyE y Hy.
∎
Theorem. (add_SNo_ordinal_eq)
∀alpha, ordinal alpha → ∀beta, ordinal beta → alpha + beta = SNoCut ({x + beta|x ∈ SNoS_ alpha} ∪ {alpha + x|x ∈ SNoS_ beta}) Empty
In Proofgold the corresponding term root is cfe1f5... and proposition id is ee8e7c...
Proof:
Let alpha be given.
Assume Ha: ordinal alpha.
Let beta be given.
Assume Hb: ordinal beta.
Set Lo1 to be the term {x + beta|x ∈ SNoS_ alpha}.
Set Lo2 to be the term {alpha + x|x ∈ SNoS_ beta}.
We will prove alpha + beta = SNoCut (Lo1 ∪ Lo2) Empty.
We prove the intermediate claim La: SNo alpha.
An exact proof term for the current goal is ordinal_SNo alpha Ha.
We prove the intermediate claim Lb: SNo beta.
An exact proof term for the current goal is ordinal_SNo beta Hb.
rewrite the current goal using add_SNo_eq alpha La beta Lb (from left to right).
We will prove SNoCut ({x + beta|x ∈ SNoL alpha} ∪ {alpha + x|x ∈ SNoL beta}) ({x + beta|x ∈ SNoR alpha} ∪ {alpha + x|x ∈ SNoR beta}) = SNoCut (Lo1 ∪ Lo2) Empty.
rewrite the current goal using ordinal_SNoL alpha Ha (from left to right).
rewrite the current goal using ordinal_SNoL beta Hb (from left to right).
We will prove SNoCut (Lo1 ∪ Lo2) ({x + beta|x ∈ SNoR alpha} ∪ {alpha + x|x ∈ SNoR beta}) = SNoCut (Lo1 ∪ Lo2) Empty.
rewrite the current goal using ordinal_SNoR alpha Ha (from left to right).
rewrite the current goal using ordinal_SNoR beta Hb (from left to right).
We will prove SNoCut (Lo1 ∪ Lo2) ({x + beta|x ∈ Empty} ∪ {alpha + x|x ∈ Empty}) = SNoCut (Lo1 ∪ Lo2) Empty.
rewrite the current goal using Repl_Empty (from left to right).
rewrite the current goal using Repl_Empty (from left to right).
We will prove SNoCut (Lo1 ∪ Lo2) (Empty ∪ Empty) = SNoCut (Lo1 ∪ Lo2) Empty.
rewrite the current goal using binunion_idl (from left to right).
Use reflexivity.
∎
Theorem. (add_SNo_ordinal_ordinal)
∀alpha, ordinal alpha → ∀beta, ordinal beta → ordinal (alpha + beta)
In Proofgold the corresponding term root is e9309a... and proposition id is ee9c23...
Proof:
Let alpha be given.
Assume Ha: ordinal alpha.
Let beta be given.
Assume Hb: ordinal beta.
We prove the intermediate claim La: SNo alpha.
An exact proof term for the current goal is ordinal_SNo alpha Ha.
We prove the intermediate claim Lb: SNo beta.
An exact proof term for the current goal is ordinal_SNo beta Hb.
We prove the intermediate claim Lab1: SNo (alpha + beta).
An exact proof term for the current goal is SNo_add_SNo alpha beta La Lb.
We prove the intermediate claim Lab2: ordinal (SNoLev (alpha + beta)).
An exact proof term for the current goal is SNoLev_ordinal (alpha + beta) Lab1.
We will prove ordinal (alpha + beta).
Apply SNo_max_ordinal (alpha + beta) Lab1 to the current goal.
We will prove ∀y ∈ SNoS_ (SNoLev (alpha + beta)), y < alpha + beta.
Let y be given.
Assume Hy: y ∈ SNoS_ (SNoLev (alpha + beta)).
Apply SNoS_E2 (SNoLev (alpha + beta)) Lab2 y Hy to the current goal.
Assume Hy1: SNoLev y ∈ SNoLev (alpha + beta).
Assume Hy2: ordinal (SNoLev y).
Assume Hy3: SNo y.
Assume Hy4: SNo_ (SNoLev y) y.
Set Lo1 to be the term {x + beta|x ∈ SNoS_ alpha}.
Set Lo2 to be the term {alpha + x|x ∈ SNoS_ beta}.
Apply SNoLt_trichotomy_or y (alpha + beta) Hy3 Lab1 to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: y < alpha + beta.
An exact proof term for the current goal is H1.
Assume H1: y = alpha + beta.
We will prove False.
Apply In_irref (SNoLev y) to the current goal.
rewrite the current goal using H1 (from left to right) at position 2.
An exact proof term for the current goal is Hy1.
Assume H1: alpha + beta < y.
We will prove False.
Apply add_SNo_ordinal_SNoCutP alpha Ha beta Hb to the current goal.
Assume H2.
Apply H2 to the current goal.
Assume H2: ∀x ∈ Lo1 ∪ Lo2, SNo x.
Assume _ _.
Apply SNoCutP_SNoCut (Lo1 ∪ Lo2) Empty (add_SNo_ordinal_SNoCutP alpha Ha beta Hb) to the current goal.
Assume H3.
Apply H3 to the current goal.
Assume H3.
Apply H3 to the current goal.
Assume _.
Assume H3: ∀x ∈ Lo1 ∪ Lo2, x < SNoCut (Lo1 ∪ Lo2) Empty.
Assume _.
Assume H4: ∀z, SNo z → (∀x ∈ Lo1 ∪ Lo2, x < z) → (∀y ∈ Empty, z < y) → SNoLev (SNoCut (Lo1 ∪ Lo2) Empty) ⊆ SNoLev z ∧ SNoEq_ (SNoLev (SNoCut (Lo1 ∪ Lo2) Empty)) (SNoCut (Lo1 ∪ Lo2) Empty) z.
We prove the intermediate claim L1: SNoLev (alpha + beta) ⊆ SNoLev y ∧ SNoEq_ (SNoLev (alpha + beta)) (alpha + beta) y.
rewrite the current goal using add_SNo_ordinal_eq alpha Ha beta Hb (from left to right).
Apply H4 y Hy3 to the current goal.
Let w be given.
Assume Hw: w ∈ Lo1 ∪ Lo2.
We will prove w < y.
Apply SNoLt_tra w (alpha + beta) y (H2 w Hw) Lab1 Hy3 to the current goal.
We will prove w < alpha + beta.
rewrite the current goal using add_SNo_ordinal_eq alpha Ha beta Hb (from left to right).
An exact proof term for the current goal is H3 w Hw.
We will prove alpha + beta < y.
An exact proof term for the current goal is H1.
Let w be given.
Assume Hw: w ∈ Empty.
We will prove False.
An exact proof term for the current goal is EmptyE w Hw.
Apply L1 to the current goal.
Assume H5: SNoLev (alpha + beta) ⊆ SNoLev y.
Assume _.
Apply In_irref (SNoLev y) to the current goal.
Apply H5 to the current goal.
An exact proof term for the current goal is Hy1.
∎
Theorem. (add_SNo_ordinal_SL)
∀alpha, ordinal alpha → ∀beta, ordinal beta → ordsucc alpha + beta = ordsucc (alpha + beta)
In Proofgold the corresponding term root is d55bd8... and proposition id is 61ae57...
Proof:
Let alpha be given.
Assume Ha: ordinal alpha.
Apply ordinal_ind to the current goal.
Let beta be given.
Assume Hb: ordinal beta.
Assume IH: ∀delta ∈ beta, ordsucc alpha + delta = ordsucc (alpha + delta).
We prove the intermediate claim La: SNo alpha.
An exact proof term for the current goal is ordinal_SNo alpha Ha.
We prove the intermediate claim Lb: SNo beta.
An exact proof term for the current goal is ordinal_SNo beta Hb.
We prove the intermediate claim Lab: ordinal (alpha + beta).
An exact proof term for the current goal is add_SNo_ordinal_ordinal alpha Ha beta Hb.
We prove the intermediate claim LSa: ordinal (ordsucc alpha).
Apply ordinal_ordsucc to the current goal.
An exact proof term for the current goal is Ha.
We prove the intermediate claim LSa2: SNo (ordsucc alpha).
Apply ordinal_SNo to the current goal.
An exact proof term for the current goal is LSa.
We prove the intermediate claim LSab: ordinal (ordsucc alpha + beta).
An exact proof term for the current goal is add_SNo_ordinal_ordinal (ordsucc alpha) LSa beta Hb.
Set Lo1 to be the term {x + beta|x ∈ SNoS_ (ordsucc alpha)}.
Set Lo2 to be the term {ordsucc alpha + x|x ∈ SNoS_ beta}.
Apply SNoCutP_SNoCut (Lo1 ∪ Lo2) Empty (add_SNo_ordinal_SNoCutP (ordsucc alpha) LSa beta Hb) to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume _.
rewrite the current goal using add_SNo_ordinal_eq (ordsucc alpha) LSa beta Hb (from right to left).
Assume H1: ∀x ∈ Lo1 ∪ Lo2, x < ordsucc alpha + beta.
Assume _.
Assume H2: ∀z, SNo z → (∀x ∈ Lo1 ∪ Lo2, x < z) → (∀y ∈ Empty, z < y) → SNoLev (ordsucc alpha + beta) ⊆ SNoLev z ∧ SNoEq_ (SNoLev (ordsucc alpha + beta)) (ordsucc alpha + beta) z.
We prove the intermediate claim L1: alpha + beta ∈ ordsucc alpha + beta.
Apply ordinal_SNoLt_In (alpha + beta) (ordsucc alpha + beta) Lab LSab to the current goal.
We will prove alpha + beta < ordsucc alpha + beta.
Apply H1 to the current goal.
We will prove alpha + beta ∈ Lo1 ∪ Lo2.
Apply binunionI1 to the current goal.
We will prove alpha + beta ∈ {x + beta|x ∈ SNoS_ (ordsucc alpha)}.
Apply ReplI (SNoS_ (ordsucc alpha)) (λx ⇒ x + beta) alpha to the current goal.
We will prove alpha ∈ SNoS_ (ordsucc alpha).
Apply SNoS_I (ordsucc alpha) LSa alpha alpha (ordsuccI2 alpha) to the current goal.
We will prove SNo_ alpha alpha.
An exact proof term for the current goal is ordinal_SNo_ alpha Ha.
Apply ordinal_ordsucc_In_eq (ordsucc alpha + beta) (alpha + beta) LSab L1 to the current goal.
Assume H3: ordsucc (alpha + beta) ∈ ordsucc alpha + beta.
We will prove False.
Set z to be the term ordsucc (alpha + beta).
We prove the intermediate claim Lz: ordinal z.
An exact proof term for the current goal is ordinal_ordsucc (alpha + beta) Lab.
We prove the intermediate claim Lz1: TransSet z.
An exact proof term for the current goal is ordinal_TransSet z Lz.
We prove the intermediate claim Lz2: SNo z.
Apply ordinal_SNo to the current goal.
An exact proof term for the current goal is Lz.
We prove the intermediate claim L2: SNoLev (ordsucc alpha + beta) ⊆ SNoLev z ∧ SNoEq_ (SNoLev (ordsucc alpha + beta)) (ordsucc alpha + beta) z.
Apply H2 z (ordinal_SNo z Lz) to the current goal.
Let w be given.
Assume Hw: w ∈ Lo1 ∪ Lo2.
We will prove w < z.
Apply binunionE Lo1 Lo2 w Hw to the current goal.
Assume H4: w ∈ Lo1.
Apply ReplE_impred (SNoS_ (ordsucc alpha)) (λx ⇒ x + beta) w H4 to the current goal.
Let x be given.
Assume Hx: x ∈ SNoS_ (ordsucc alpha).
Assume Hwx: w = x + beta.
Apply SNoS_E2 (ordsucc alpha) LSa x Hx to the current goal.
Assume Hx1: SNoLev x ∈ ordsucc alpha.
Assume Hx2: ordinal (SNoLev x).
Assume Hx3: SNo x.
Assume Hx4: SNo_ (SNoLev x) x.
We will prove w < z.
rewrite the current goal using Hwx (from left to right).
We will prove x + beta < z.
We prove the intermediate claim LLxb: ordinal (SNoLev x + beta).
An exact proof term for the current goal is add_SNo_ordinal_ordinal (SNoLev x) Hx2 beta Hb.
We prove the intermediate claim LLxb2: SNo (SNoLev x + beta).
Apply ordinal_SNo to the current goal.
An exact proof term for the current goal is LLxb.
Apply SNoLeLt_tra (x + beta) (SNoLev x + beta) z (SNo_add_SNo x beta Hx3 Lb) LLxb2 Lz2 to the current goal.
We will prove x + beta ≤ SNoLev x + beta.
Apply add_SNo_Le1 x beta (SNoLev x) Hx3 Lb (ordinal_SNo (SNoLev x) Hx2) to the current goal.
We will prove x ≤ SNoLev x.
An exact proof term for the current goal is ordinal_SNoLev_max_2 (SNoLev x) Hx2 x Hx3 (ordsuccI2 (SNoLev x)).
We will prove SNoLev x + beta < z.
Apply SNoLeLt_tra (SNoLev x + beta) (alpha + beta) z LLxb2 (ordinal_SNo (alpha + beta) Lab) Lz2 to the current goal.
We will prove SNoLev x + beta ≤ alpha + beta.
Apply add_SNo_Le1 (SNoLev x) beta alpha (ordinal_SNo (SNoLev x) Hx2) Lb La to the current goal.
We will prove SNoLev x ≤ alpha.
Apply ordinal_Subq_SNoLe (SNoLev x) alpha Hx2 Ha to the current goal.
We will prove SNoLev x ⊆ alpha.
Apply ordsuccE alpha (SNoLev x) Hx1 to the current goal.
Assume H5: SNoLev x ∈ alpha.
Apply Ha to the current goal.
Assume Ha1 _.
An exact proof term for the current goal is Ha1 (SNoLev x) H5.
Assume H5: SNoLev x = alpha.
rewrite the current goal using H5 (from left to right).
Apply Subq_ref to the current goal.
We will prove alpha + beta < z.
An exact proof term for the current goal is ordinal_In_SNoLt z Lz (alpha + beta) (ordsuccI2 (alpha + beta)).
Assume H4: w ∈ Lo2.
Apply ReplE_impred (SNoS_ beta) (λx ⇒ ordsucc alpha + x) w H4 to the current goal.
Let x be given.
Assume Hx: x ∈ SNoS_ beta.
Assume Hwx: w = ordsucc alpha + x.
Apply SNoS_E2 beta Hb x Hx to the current goal.
Assume Hx1: SNoLev x ∈ beta.
Assume Hx2: ordinal (SNoLev x).
Assume Hx3: SNo x.
Assume Hx4: SNo_ (SNoLev x) x.
We will prove w < z.
rewrite the current goal using Hwx (from left to right).
We will prove ordsucc alpha + x < z.
We prove the intermediate claim IHLx: ordsucc alpha + SNoLev x = ordsucc (alpha + SNoLev x).
An exact proof term for the current goal is IH (SNoLev x) Hx1.
We prove the intermediate claim LSax: SNo (ordsucc alpha + x).
An exact proof term for the current goal is SNo_add_SNo (ordsucc alpha) x LSa2 Hx3.
We prove the intermediate claim LaLx: ordinal (alpha + SNoLev x).
An exact proof term for the current goal is add_SNo_ordinal_ordinal alpha Ha (SNoLev x) Hx2.
We prove the intermediate claim LSaLx: ordinal (ordsucc alpha + SNoLev x).
An exact proof term for the current goal is add_SNo_ordinal_ordinal (ordsucc alpha) LSa (SNoLev x) Hx2.
We prove the intermediate claim LSaLx2: SNo (ordsucc alpha + SNoLev x).
Apply ordinal_SNo to the current goal.
An exact proof term for the current goal is LSaLx.
Apply SNoLeLt_tra (ordsucc alpha + x) (ordsucc alpha + SNoLev x) z LSax LSaLx2 Lz2 to the current goal.
We will prove ordsucc alpha + x ≤ ordsucc alpha + SNoLev x.
Apply add_SNo_Le2 (ordsucc alpha) x (SNoLev x) LSa2 Hx3 (ordinal_SNo (SNoLev x) Hx2) to the current goal.
We will prove x ≤ SNoLev x.
An exact proof term for the current goal is ordinal_SNoLev_max_2 (SNoLev x) Hx2 x Hx3 (ordsuccI2 (SNoLev x)).
We will prove ordsucc alpha + SNoLev x < z.
rewrite the current goal using IHLx (from left to right).
We will prove ordsucc (alpha + SNoLev x) < ordsucc (alpha + beta).
Apply ordinal_In_SNoLt z Lz (ordsucc (alpha + SNoLev x)) to the current goal.
We will prove ordsucc (alpha + SNoLev x) ∈ ordsucc (alpha + beta).
Apply ordinal_ordsucc_In (alpha + beta) Lab to the current goal.
We will prove alpha + SNoLev x ∈ alpha + beta.
Apply ordinal_SNoLt_In (alpha + SNoLev x) (alpha + beta) LaLx Lab to the current goal.
We will prove alpha + SNoLev x < alpha + beta.
Apply add_SNo_Lt2 alpha (SNoLev x) beta La (ordinal_SNo (SNoLev x) Hx2) Lb to the current goal.
We will prove SNoLev x < beta.
Apply ordinal_In_SNoLt beta Hb (SNoLev x) to the current goal.
We will prove SNoLev x ∈ beta.
An exact proof term for the current goal is Hx1.
Let w be given.
Assume Hw: w ∈ Empty.
We will prove False.
An exact proof term for the current goal is EmptyE w Hw.
Apply L2 to the current goal.
rewrite the current goal using ordinal_SNoLev (ordsucc alpha + beta) LSab (from left to right).
rewrite the current goal using ordinal_SNoLev z Lz (from left to right).
Assume H4: ordsucc alpha + beta ⊆ z.
Assume _.
Apply In_irref z to the current goal.
Apply H4 to the current goal.
We will prove z ∈ ordsucc alpha + beta.
An exact proof term for the current goal is H3.
Assume H3: ordsucc alpha + beta = ordsucc (alpha + beta).
An exact proof term for the current goal is H3.
∎
Theorem. (add_SNo_ordinal_SR)
∀alpha, ordinal alpha → ∀beta, ordinal beta → alpha + ordsucc beta = ordsucc (alpha + beta)
In Proofgold the corresponding term root is e7378a... and proposition id is 0c1a6d...
Proof:
Let alpha be given.
Assume Ha: ordinal alpha.
Let beta be given.
Assume Hb: ordinal beta.
We prove the intermediate claim La: SNo alpha.
An exact proof term for the current goal is ordinal_SNo alpha Ha.
We prove the intermediate claim Lb: SNo beta.
An exact proof term for the current goal is ordinal_SNo beta Hb.
We prove the intermediate claim La: SNo alpha.
An exact proof term for the current goal is ordinal_SNo alpha Ha.
We prove the intermediate claim LSb: ordinal (ordsucc beta).
Apply ordinal_ordsucc to the current goal.
An exact proof term for the current goal is Hb.
We prove the intermediate claim LSb2: SNo (ordsucc beta).
An exact proof term for the current goal is ordinal_SNo (ordsucc beta) LSb.
rewrite the current goal using add_SNo_com alpha (ordsucc beta) La LSb2 (from left to right).
We will prove ordsucc beta + alpha = ordsucc (alpha + beta).
rewrite the current goal using add_SNo_ordinal_SL beta Hb alpha Ha (from left to right).
We will prove ordsucc (beta + alpha) = ordsucc (alpha + beta).
rewrite the current goal using add_SNo_com beta alpha Lb La (from left to right).
Use reflexivity.
∎
Theorem. (add_SNo_ordinal_InL)
∀alpha, ordinal alpha → ∀beta, ordinal beta → ∀gamma ∈ alpha, gamma + beta ∈ alpha + beta
In Proofgold the corresponding term root is 09a829... and proposition id is 5acda8...
Proof:
Let alpha be given.
Assume Ha.
Let beta be given.
Assume Hb.
Let gamma be given.
Assume Hc.
We prove the intermediate claim Lc: ordinal gamma.
An exact proof term for the current goal is ordinal_Hered alpha Ha gamma Hc.
We prove the intermediate claim Lab: ordinal (alpha + beta).
Apply add_SNo_ordinal_ordinal to the current goal.
An exact proof term for the current goal is Ha.
An exact proof term for the current goal is Hb.
We prove the intermediate claim Lcb: ordinal (gamma + beta).
Apply add_SNo_ordinal_ordinal to the current goal.
An exact proof term for the current goal is Lc.
An exact proof term for the current goal is Hb.
We will prove gamma + beta ∈ alpha + beta.
Apply ordinal_SNoLt_In (gamma + beta) (alpha + beta) Lcb Lab to the current goal.
We will prove gamma + beta < alpha + beta.
Apply add_SNo_Lt1 to the current goal.
Apply ordinal_SNo to the current goal.
An exact proof term for the current goal is Lc.
Apply ordinal_SNo to the current goal.
An exact proof term for the current goal is Hb.
Apply ordinal_SNo to the current goal.
An exact proof term for the current goal is Ha.
An exact proof term for the current goal is ordinal_In_SNoLt alpha Ha gamma Hc.
∎
Theorem. (add_SNo_ordinal_InR)
∀alpha, ordinal alpha → ∀beta, ordinal beta → ∀gamma ∈ beta, alpha + gamma ∈ alpha + beta
In Proofgold the corresponding term root is d291f4... and proposition id is 0f42b5...
Proof:
Let alpha be given.
Assume Ha: ordinal alpha.
Let beta be given.
Assume Hb: ordinal beta.
Let gamma be given.
Assume Hc: gamma ∈ beta.
We prove the intermediate claim La: SNo alpha.
An exact proof term for the current goal is ordinal_SNo alpha Ha.
We prove the intermediate claim Lb: SNo beta.
An exact proof term for the current goal is ordinal_SNo beta Hb.
We prove the intermediate claim Lc: ordinal gamma.
An exact proof term for the current goal is ordinal_Hered beta Hb gamma Hc.
We prove the intermediate claim Lc2: SNo gamma.
An exact proof term for the current goal is ordinal_SNo gamma Lc.
rewrite the current goal using add_SNo_com alpha gamma La Lc2 (from left to right).
rewrite the current goal using add_SNo_com alpha beta La Lb (from left to right).
An exact proof term for the current goal is add_SNo_ordinal_InL beta Hb alpha Ha gamma Hc.
∎
Theorem. (add_nat_add_SNo)
∀n m ∈ ω, add_nat n m = n + m
In Proofgold the corresponding term root is 1701fc... and proposition id is 9df659...
Proof:
Let n be given.
Assume Hn: n ∈ ω.
We prove the intermediate claim Ln1: nat_p n.
An exact proof term for the current goal is omega_nat_p n Hn.
We prove the intermediate claim Ln2: ordinal n.
An exact proof term for the current goal is nat_p_ordinal n Ln1.
We prove the intermediate claim Ln3: SNo n.
An exact proof term for the current goal is ordinal_SNo n Ln2.
We prove the intermediate claim L1: ∀m, nat_p m → add_nat n m = n + m.
Apply nat_ind to the current goal.
We will prove add_nat n 0 = n + 0.
rewrite the current goal using add_SNo_0R n Ln3 (from left to right).
We will prove add_nat n 0 = n.
An exact proof term for the current goal is add_nat_0R n.
Let m be given.
Assume Hm: nat_p m.
Assume IH: add_nat n m = n + m.
We will prove add_nat n (ordsucc m) = n + (ordsucc m).
rewrite the current goal using add_SNo_ordinal_SR n Ln2 m (nat_p_ordinal m Hm) (from left to right).
We will prove add_nat n (ordsucc m) = ordsucc (n + m).
rewrite the current goal using IH (from right to left).
We will prove add_nat n (ordsucc m) = ordsucc (add_nat n m).
An exact proof term for the current goal is add_nat_SR n m Hm.
Let m be given.
Assume Hm: m ∈ ω.
We will prove add_nat n m = n + m.
An exact proof term for the current goal is L1 m (omega_nat_p m Hm).
∎
Theorem. (add_SNo_In_omega)
∀n m ∈ ω, n + m ∈ ω
In Proofgold the corresponding term root is f45cbb... and proposition id is eb6375...
Proof:
Let n be given.
Assume Hn.
Let m be given.
Assume Hm.
rewrite the current goal using add_nat_add_SNo n Hn m Hm (from right to left).
Apply nat_p_omega to the current goal.
Apply add_nat_p to the current goal.
Apply omega_nat_p to the current goal.
An exact proof term for the current goal is Hn.
Apply omega_nat_p to the current goal.
An exact proof term for the current goal is Hm.
∎
Theorem. (add_SNo_1_1_2)
1 + 1 = 2
In Proofgold the corresponding term root is bbc448... and proposition id is 2b8298...
Proof:
rewrite the current goal using add_nat_add_SNo 1 (nat_p_omega 1 nat_1) 1 (nat_p_omega 1 nat_1) (from right to left).
An exact proof term for the current goal is add_nat_1_1_2.
∎
Theorem. (add_SNo_SNoL_interpolate)
∀x y, SNo x → SNo y → ∀u ∈ SNoL (x + y), (∃v ∈ SNoL x, u ≤ v + y) ∨ (∃v ∈ SNoL y, u ≤ x + v)
In Proofgold the corresponding term root is 971363... and proposition id is 3cafc1...
Proof:
Let x and y be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
We prove the intermediate claim Lxy: SNo (x + y).
An exact proof term for the current goal is SNo_add_SNo x y Hx Hy.
We prove the intermediate claim LI: ∀u, SNo u → SNoLev u ∈ SNoLev (x + y) → u < x + y → (∃v ∈ SNoL x, u ≤ v + y) ∨ (∃v ∈ SNoL y, u ≤ x + v).
Apply SNoLev_ind to the current goal.
Let u be given.
Assume Hu1: SNo u.
Assume IH: ∀z ∈ SNoS_ (SNoLev u), SNoLev z ∈ SNoLev (x + y) → z < x + y → (∃v ∈ SNoL x, z ≤ v + y) ∨ (∃v ∈ SNoL y, z ≤ x + v).
Assume Hu2: SNoLev u ∈ SNoLev (x + y).
Assume Hu3: u < x + y.
Apply dneg to the current goal.
Assume HNC: ¬ ((∃v ∈ SNoL x, u ≤ v + y) ∨ (∃v ∈ SNoL y, u ≤ x + v)).
Apply SNoLt_irref u to the current goal.
We will prove u < u.
Apply SNoLtLe_tra u (x + y) u Hu1 Lxy Hu1 Hu3 to the current goal.
We will prove x + y ≤ u.
Set Lxy1 to be the term {w + y|w ∈ SNoL x}.
Set Lxy2 to be the term {x + w|w ∈ SNoL y}.
Set Rxy1 to be the term {z + y|z ∈ SNoR x}.
Set Rxy2 to be the term {x + z|z ∈ SNoR y}.
rewrite the current goal using add_SNo_eq x Hx y Hy (from left to right).
We will prove SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2) ≤ u.
rewrite the current goal using SNo_eta u Hu1 (from left to right).
We will prove SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2) ≤ SNoCut (SNoL u) (SNoR u).
Apply SNoCut_Le (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2) (SNoL u) (SNoR u) to the current goal.
An exact proof term for the current goal is add_SNo_SNoCutP x y Hx Hy.
An exact proof term for the current goal is SNoCutP_SNoL_SNoR u Hu1.
rewrite the current goal using SNo_eta u Hu1 (from right to left).
We will prove ∀w ∈ Lxy1 ∪ Lxy2, w < u.
Let w be given.
Assume Hw: w ∈ Lxy1 ∪ Lxy2.
Apply binunionE Lxy1 Lxy2 w Hw to the current goal.
Assume Hw2: w ∈ Lxy1.
We will prove w < u.
Apply ReplE_impred (SNoL x) (λw ⇒ w + y) w Hw2 to the current goal.
Let v be given.
Assume Hv: v ∈ SNoL x.
Assume Hwv: w = v + y.
Apply SNoL_E x Hx v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev x.
Assume Hv3: v < x.
rewrite the current goal using Hwv (from left to right).
We will prove v + y < u.
We prove the intermediate claim Lvy: SNo (v + y).
An exact proof term for the current goal is SNo_add_SNo v y Hv1 Hy.
Apply SNoLtLe_or (v + y) u Lvy Hu1 to the current goal.
Assume H1: v + y < u.
An exact proof term for the current goal is H1.
Assume H1: u ≤ v + y.
We will prove False.
Apply HNC to the current goal.
Apply orIL to the current goal.
We use v to witness the existential quantifier.
Apply andI to the current goal.
We will prove v ∈ SNoL x.
An exact proof term for the current goal is Hv.
We will prove u ≤ v + y.
An exact proof term for the current goal is H1.
Assume Hw2: w ∈ Lxy2.
We will prove w < u.
Apply ReplE_impred (SNoL y) (λw ⇒ x + w) w Hw2 to the current goal.
Let v be given.
Assume Hv: v ∈ SNoL y.
Assume Hwv: w = x + v.
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev y.
Assume Hv3: v < y.
rewrite the current goal using Hwv (from left to right).
We will prove x + v < u.
We prove the intermediate claim Lxv: SNo (x + v).
An exact proof term for the current goal is SNo_add_SNo x v Hx Hv1.
Apply SNoLtLe_or (x + v) u Lxv Hu1 to the current goal.
Assume H1: x + v < u.
An exact proof term for the current goal is H1.
Assume H1: u ≤ x + v.
We will prove False.
Apply HNC to the current goal.
Apply orIR to the current goal.
We use v to witness the existential quantifier.
Apply andI to the current goal.
We will prove v ∈ SNoL y.
An exact proof term for the current goal is Hv.
We will prove u ≤ x + v.
An exact proof term for the current goal is H1.
rewrite the current goal using add_SNo_eq x Hx y Hy (from right to left).
We will prove ∀z ∈ SNoR u, x + y < z.
Let z be given.
Assume Hz: z ∈ SNoR u.
Apply SNoR_E u Hu1 z Hz to the current goal.
Assume Hz1: SNo z.
Assume Hz2: SNoLev z ∈ SNoLev u.
Assume Hz3: u < z.
Apply SNoLt_trichotomy_or (x + y) z Lxy Hz1 to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: x + y < z.
An exact proof term for the current goal is H1.
Assume H1: x + y = z.
We will prove False.
Apply In_no2cycle (SNoLev z) (SNoLev u) Hz2 to the current goal.
We will prove SNoLev u ∈ SNoLev z.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hu2.
Assume H1: z < x + y.
We will prove False.
We prove the intermediate claim Lz1: z ∈ SNoS_ (SNoLev u).
An exact proof term for the current goal is SNoR_SNoS_ u z Hz.
We prove the intermediate claim Lz2: SNoLev z ∈ SNoLev (x + y).
Apply SNoLev_ordinal (x + y) Lxy to the current goal.
Assume Hxy1 _.
An exact proof term for the current goal is Hxy1 (SNoLev u) Hu2 (SNoLev z) Hz2.
Apply IH z Lz1 Lz2 H1 to the current goal.
Assume H2: ∃v ∈ SNoL x, z ≤ v + y.
Apply H2 to the current goal.
Let v be given.
Assume H3.
Apply H3 to the current goal.
Assume Hv: v ∈ SNoL x.
Assume H3: z ≤ v + y.
Apply SNoL_E x Hx v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev x.
Assume Hv3: v < x.
Apply HNC to the current goal.
Apply orIL to the current goal.
We use v to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv.
We will prove u ≤ v + y.
Apply SNoLe_tra u z (v + y) Hu1 Hz1 (SNo_add_SNo v y Hv1 Hy) to the current goal.
We will prove u ≤ z.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hz3.
We will prove z ≤ v + y.
An exact proof term for the current goal is H3.
Assume H2: ∃v ∈ SNoL y, z ≤ x + v.
Apply H2 to the current goal.
Let v be given.
Assume H3.
Apply H3 to the current goal.
Assume Hv: v ∈ SNoL y.
Assume H3: z ≤ x + v.
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev y.
Assume Hv3: v < y.
Apply HNC to the current goal.
Apply orIR to the current goal.
We use v to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv.
We will prove u ≤ x + v.
Apply SNoLe_tra u z (x + v) Hu1 Hz1 (SNo_add_SNo x v Hx Hv1) to the current goal.
We will prove u ≤ z.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hz3.
We will prove z ≤ x + v.
An exact proof term for the current goal is H3.
Let u be given.
Assume Hu: u ∈ SNoL (x + y).
Apply SNoL_E (x + y) Lxy u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev (x + y).
Assume Hu3: u < x + y.
An exact proof term for the current goal is LI u Hu1 Hu2 Hu3.
∎
Theorem. (add_SNo_SNoR_interpolate)
∀x y, SNo x → SNo y → ∀u ∈ SNoR (x + y), (∃v ∈ SNoR x, v + y ≤ u) ∨ (∃v ∈ SNoR y, x + v ≤ u)
In Proofgold the corresponding term root is 928f71... and proposition id is 31fa94...
Proof:
Let x and y be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
We prove the intermediate claim Lxy: SNo (x + y).
An exact proof term for the current goal is SNo_add_SNo x y Hx Hy.
We prove the intermediate claim LI: ∀u, SNo u → SNoLev u ∈ SNoLev (x + y) → x + y < u → (∃v ∈ SNoR x, v + y ≤ u) ∨ (∃v ∈ SNoR y, x + v ≤ u).
Apply SNoLev_ind to the current goal.
Let u be given.
Assume Hu1: SNo u.
Assume IH: ∀z ∈ SNoS_ (SNoLev u), SNoLev z ∈ SNoLev (x + y) → x + y < z → (∃v ∈ SNoR x, v + y ≤ z) ∨ (∃v ∈ SNoR y, x + v ≤ z).
Assume Hu2: SNoLev u ∈ SNoLev (x + y).
Assume Hu3: x + y < u.
Apply dneg to the current goal.
Assume HNC: ¬ ((∃v ∈ SNoR x, v + y ≤ u) ∨ (∃v ∈ SNoR y, x + v ≤ u)).
Apply SNoLt_irref u to the current goal.
We will prove u < u.
Apply (λH : u ≤ x + y ⇒ SNoLeLt_tra u (x + y) u Hu1 Lxy Hu1 H Hu3) to the current goal.
We will prove u ≤ x + y.
Set Lxy1 to be the term {w + y|w ∈ SNoL x}.
Set Lxy2 to be the term {x + w|w ∈ SNoL y}.
Set Rxy1 to be the term {z + y|z ∈ SNoR x}.
Set Rxy2 to be the term {x + z|z ∈ SNoR y}.
rewrite the current goal using add_SNo_eq x Hx y Hy (from left to right).
We will prove u ≤ SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2).
rewrite the current goal using SNo_eta u Hu1 (from left to right).
We will prove SNoCut (SNoL u) (SNoR u) ≤ SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2).
Apply SNoCut_Le (SNoL u) (SNoR u) (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2) to the current goal.
An exact proof term for the current goal is SNoCutP_SNoL_SNoR u Hu1.
An exact proof term for the current goal is add_SNo_SNoCutP x y Hx Hy.
rewrite the current goal using add_SNo_eq x Hx y Hy (from right to left).
We will prove ∀z ∈ SNoL u, z < x + y.
Let z be given.
Assume Hz: z ∈ SNoL u.
Apply SNoL_E u Hu1 z Hz to the current goal.
Assume Hz1: SNo z.
Assume Hz2: SNoLev z ∈ SNoLev u.
Assume Hz3: z < u.
Apply SNoLt_trichotomy_or z (x + y) Hz1 Lxy to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: z < x + y.
An exact proof term for the current goal is H1.
Assume H1: z = x + y.
We will prove False.
Apply In_no2cycle (SNoLev z) (SNoLev u) Hz2 to the current goal.
We will prove SNoLev u ∈ SNoLev z.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hu2.
Assume H1: x + y < z.
We will prove False.
We prove the intermediate claim Lz1: z ∈ SNoS_ (SNoLev u).
An exact proof term for the current goal is SNoL_SNoS_ u z Hz.
We prove the intermediate claim Lz2: SNoLev z ∈ SNoLev (x + y).
Apply SNoLev_ordinal (x + y) Lxy to the current goal.
Assume Hxy1 _.
An exact proof term for the current goal is Hxy1 (SNoLev u) Hu2 (SNoLev z) Hz2.
Apply IH z Lz1 Lz2 H1 to the current goal.
Assume H2: ∃v ∈ SNoR x, v + y ≤ z.
Apply H2 to the current goal.
Let v be given.
Assume H3.
Apply H3 to the current goal.
Assume Hv: v ∈ SNoR x.
Assume H3: v + y ≤ z.
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 HNC to the current goal.
Apply orIL to the current goal.
We use v to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv.
We will prove v + y ≤ u.
Apply SNoLe_tra (v + y) z u (SNo_add_SNo v y Hv1 Hy) Hz1 Hu1 to the current goal.
We will prove v + y ≤ z.
An exact proof term for the current goal is H3.
We will prove z ≤ u.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hz3.
Assume H2: ∃v ∈ SNoR y, x + v ≤ z.
Apply H2 to the current goal.
Let v be given.
Assume H3.
Apply H3 to the current goal.
Assume Hv: v ∈ SNoR y.
Assume H3: x + v ≤ z.
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 HNC to the current goal.
Apply orIR to the current goal.
We use v to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv.
We will prove x + v ≤ u.
Apply SNoLe_tra (x + v) z u (SNo_add_SNo x v Hx Hv1) Hz1 Hu1 to the current goal.
We will prove x + v ≤ z.
An exact proof term for the current goal is H3.
We will prove z ≤ u.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hz3.
rewrite the current goal using SNo_eta u Hu1 (from right to left).
We will prove ∀w ∈ Rxy1 ∪ Rxy2, u < w.
Let w be given.
Assume Hw: w ∈ Rxy1 ∪ Rxy2.
Apply binunionE Rxy1 Rxy2 w Hw to the current goal.
Assume Hw2: w ∈ Rxy1.
We will prove u < w.
Apply ReplE_impred (SNoR x) (λw ⇒ w + y) w Hw2 to the current goal.
Let v be given.
Assume Hv: v ∈ SNoR x.
Assume Hwv: w = 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.
rewrite the current goal using Hwv (from left to right).
We will prove u < v + y.
We prove the intermediate claim Lvy: SNo (v + y).
An exact proof term for the current goal is SNo_add_SNo v y Hv1 Hy.
Apply SNoLtLe_or u (v + y) Hu1 Lvy to the current goal.
Assume H1: u < v + y.
An exact proof term for the current goal is H1.
Assume H1: v + y ≤ u.
We will prove False.
Apply HNC to the current goal.
Apply orIL to the current goal.
We use v to witness the existential quantifier.
Apply andI to the current goal.
We will prove v ∈ SNoR x.
An exact proof term for the current goal is Hv.
We will prove v + y ≤ u.
An exact proof term for the current goal is H1.
Assume Hw2: w ∈ Rxy2.
We will prove u < w.
Apply ReplE_impred (SNoR y) (λw ⇒ x + w) w Hw2 to the current goal.
Let v be given.
Assume Hv: v ∈ SNoR y.
Assume Hwv: w = 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.
rewrite the current goal using Hwv (from left to right).
We will prove u < x + v.
We prove the intermediate claim Lxv: SNo (x + v).
An exact proof term for the current goal is SNo_add_SNo x v Hx Hv1.
Apply SNoLtLe_or u (x + v) Hu1 Lxv to the current goal.
Assume H1: u < x + v.
An exact proof term for the current goal is H1.
Assume H1: x + v ≤ u.
We will prove False.
Apply HNC to the current goal.
Apply orIR to the current goal.
We use v to witness the existential quantifier.
Apply andI to the current goal.
We will prove v ∈ SNoR y.
An exact proof term for the current goal is Hv.
We will prove x + v ≤ u.
An exact proof term for the current goal is H1.
Let u be given.
Assume Hu: u ∈ SNoR (x + y).
Apply SNoR_E (x + y) Lxy u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev (x + y).
Assume Hu3: x + y < u.
An exact proof term for the current goal is LI u Hu1 Hu2 Hu3.
∎
Theorem. (add_SNo_assoc)
∀x y z, SNo x → SNo y → SNo z → x + (y + z) = (x + y) + z
In Proofgold the corresponding term root is 39b331... and proposition id is bc15ad...
Proof:
Set P to be the term λx y z ⇒ x + (y + z) = (x + y) + z of type set → set → set → prop.
Apply SNoLev_ind3 to the current goal.
Let x, y and z be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume Hz: SNo z.
Assume IH1: ∀u ∈ SNoS_ (SNoLev x), P u y z.
Assume IH2: ∀v ∈ SNoS_ (SNoLev y), P x v z.
Assume IH3: ∀w ∈ SNoS_ (SNoLev z), P x y w.
Assume IH4: ∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), P u v z.
Assume IH5: ∀u ∈ SNoS_ (SNoLev x), ∀w ∈ SNoS_ (SNoLev z), P u y w.
Assume IH6: ∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), P x v w.
Assume IH7: ∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), P u v w.
We will prove x + (y + z) = (x + y) + z.
We prove the intermediate claim Lxy: SNo (x + y).
An exact proof term for the current goal is SNo_add_SNo x y Hx Hy.
We prove the intermediate claim Lyz: SNo (y + z).
An exact proof term for the current goal is SNo_add_SNo y z Hy Hz.
Set Lxyz1 to be the term {w + (y + z)|w ∈ SNoL x}.
Set Lxyz2 to be the term {x + w|w ∈ SNoL (y + z)}.
Set Rxyz1 to be the term {w + (y + z)|w ∈ SNoR x}.
Set Rxyz2 to be the term {x + w|w ∈ SNoR (y + z)}.
Set Lxyz3 to be the term {w + z|w ∈ SNoL (x + y)}.
Set Lxyz4 to be the term {(x + y) + w|w ∈ SNoL z}.
Set Rxyz3 to be the term {w + z|w ∈ SNoR (x + y)}.
Set Rxyz4 to be the term {(x + y) + w|w ∈ SNoR z}.
rewrite the current goal using add_SNo_eq x Hx (y + z) Lyz (from left to right).
rewrite the current goal using add_SNo_eq (x + y) Lxy z Hz (from left to right).
We will prove (SNoCut (Lxyz1 ∪ Lxyz2) (Rxyz1 ∪ Rxyz2)) = (SNoCut (Lxyz3 ∪ Lxyz4) (Rxyz3 ∪ Rxyz4)).
We prove the intermediate claim Lxyz12: SNoCutP (Lxyz1 ∪ Lxyz2) (Rxyz1 ∪ Rxyz2).
An exact proof term for the current goal is add_SNo_SNoCutP x (y + z) Hx Lyz.
We prove the intermediate claim Lxyz34: SNoCutP (Lxyz3 ∪ Lxyz4) (Rxyz3 ∪ Rxyz4).
An exact proof term for the current goal is add_SNo_SNoCutP (x + y) z Lxy Hz.
Apply SNoCut_ext to the current goal.
An exact proof term for the current goal is Lxyz12.
An exact proof term for the current goal is Lxyz34.
We will prove ∀w ∈ Lxyz1 ∪ Lxyz2, w < SNoCut (Lxyz3 ∪ Lxyz4) (Rxyz3 ∪ Rxyz4).
rewrite the current goal using add_SNo_eq (x + y) Lxy z Hz (from right to left).
We will prove ∀w ∈ Lxyz1 ∪ Lxyz2, w < (x + y) + z.
Let w be given.
Assume Hw: w ∈ Lxyz1 ∪ Lxyz2.
Apply binunionE Lxyz1 Lxyz2 w Hw to the current goal.
Assume Hw: w ∈ Lxyz1.
Apply ReplE_impred (SNoL x) (λw ⇒ w + (y + z)) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL x.
Assume Hwu: w = u + (y + z).
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 will prove w < (x + y) + z.
rewrite the current goal using Hwu (from left to right).
We will prove u + (y + z) < (x + y) + z.
We prove the intermediate claim IH1u: u + (y + z) = (u + y) + z.
An exact proof term for the current goal is IH1 u (SNoL_SNoS_ x u Hu).
rewrite the current goal using IH1u (from left to right).
We will prove (u + y) + z < (x + y) + z.
Apply add_SNo_Lt1 (u + y) z (x + y) (SNo_add_SNo u y Hu1 Hy) Hz Lxy to the current goal.
We will prove u + y < x + y.
Apply add_SNo_Lt1 u y x Hu1 Hy Hx to the current goal.
We will prove u < x.
An exact proof term for the current goal is Hu3.
Assume Hw: w ∈ Lxyz2.
Apply ReplE_impred (SNoL (y + z)) (λw ⇒ x + w) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL (y + z).
Assume Hwu: w = x + u.
Apply SNoL_E (y + z) Lyz u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev (y + z).
Assume Hu3: u < y + z.
rewrite the current goal using Hwu (from left to right).
We will prove x + u < (x + y) + z.
Apply add_SNo_SNoL_interpolate y z Hy Hz u Hu to the current goal.
Assume H1: ∃v ∈ SNoL y, u ≤ v + z.
Apply H1 to the current goal.
Let v be given.
Assume H2.
Apply H2 to the current goal.
Assume Hv: v ∈ SNoL y.
Assume H2: u ≤ v + z.
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev y.
Assume Hv3: v < y.
We prove the intermediate claim IH2v: x + (v + z) = (x + v) + z.
An exact proof term for the current goal is IH2 v (SNoL_SNoS_ y v Hv).
We will prove x + u < (x + y) + z.
Apply SNoLeLt_tra (x + u) (x + (v + z)) ((x + y) + z) (SNo_add_SNo x u Hx Hu1) (SNo_add_SNo x (v + z) Hx (SNo_add_SNo v z Hv1 Hz)) (SNo_add_SNo (x + y) z Lxy Hz) to the current goal.
We will prove x + u ≤ x + (v + z).
Apply add_SNo_Le2 x u (v + z) Hx Hu1 (SNo_add_SNo v z Hv1 Hz) to the current goal.
We will prove u ≤ v + z.
An exact proof term for the current goal is H2.
We will prove x + (v + z) < (x + y) + z.
rewrite the current goal using IH2v (from left to right).
We will prove (x + v) + z < (x + y) + z.
Apply add_SNo_Lt1 (x + v) z (x + y) (SNo_add_SNo x v Hx Hv1) Hz Lxy to the current goal.
We will prove x + v < x + y.
Apply add_SNo_Lt2 x v y Hx Hv1 Hy to the current goal.
We will prove v < y.
An exact proof term for the current goal is Hv3.
Assume H1: ∃v ∈ SNoL z, u ≤ y + v.
Apply H1 to the current goal.
Let v be given.
Assume H2.
Apply H2 to the current goal.
Assume Hv: v ∈ SNoL z.
Assume H2: u ≤ y + v.
Apply SNoL_E z Hz v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev z.
Assume Hv3: v < z.
We prove the intermediate claim IH3v: x + (y + v) = (x + y) + v.
An exact proof term for the current goal is IH3 v (SNoL_SNoS_ z v Hv).
We will prove x + u < (x + y) + z.
Apply SNoLeLt_tra (x + u) (x + (y + v)) ((x + y) + z) (SNo_add_SNo x u Hx Hu1) (SNo_add_SNo x (y + v) Hx (SNo_add_SNo y v Hy Hv1)) (SNo_add_SNo (x + y) z Lxy Hz) to the current goal.
We will prove x + u ≤ x + (y + v).
Apply add_SNo_Le2 x u (y + v) Hx Hu1 (SNo_add_SNo y v Hy Hv1) to the current goal.
We will prove u ≤ y + v.
An exact proof term for the current goal is H2.
We will prove x + (y + v) < (x + y) + z.
rewrite the current goal using IH3v (from left to right).
We will prove (x + y) + v < (x + y) + z.
Apply add_SNo_Lt2 (x + y) v z Lxy Hv1 Hz to the current goal.
We will prove v < z.
An exact proof term for the current goal is Hv3.
We will prove ∀v ∈ Rxyz1 ∪ Rxyz2, SNoCut (Lxyz3 ∪ Lxyz4) (Rxyz3 ∪ Rxyz4) < v.
rewrite the current goal using add_SNo_eq (x + y) Lxy z Hz (from right to left).
We will prove ∀v ∈ Rxyz1 ∪ Rxyz2, (x + y) + z < v.
Let v be given.
Assume Hv: v ∈ Rxyz1 ∪ Rxyz2.
Apply binunionE Rxyz1 Rxyz2 v Hv to the current goal.
Assume Hv: v ∈ Rxyz1.
Apply ReplE_impred (SNoR x) (λw ⇒ w + (y + z)) v Hv to the current goal.
Let u be given.
Assume Hu: u ∈ SNoR x.
Assume Hvu: v = u + (y + z).
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 will prove (x + y) + z < v.
rewrite the current goal using Hvu (from left to right).
We will prove (x + y) + z < u + (y + z).
We prove the intermediate claim IH1u: u + (y + z) = (u + y) + z.
An exact proof term for the current goal is IH1 u (SNoR_SNoS_ x u Hu).
rewrite the current goal using IH1u (from left to right).
We will prove (x + y) + z < (u + y) + z.
Apply add_SNo_Lt1 (x + y) z (u + y) Lxy Hz (SNo_add_SNo u y Hu1 Hy) to the current goal.
We will prove x + y < u + y.
Apply add_SNo_Lt1 x y u Hx Hy Hu1 to the current goal.
We will prove x < u.
An exact proof term for the current goal is Hu3.
Assume Hv: v ∈ Rxyz2.
Apply ReplE_impred (SNoR (y + z)) (λw ⇒ x + w) v Hv to the current goal.
Let u be given.
Assume Hu: u ∈ SNoR (y + z).
Assume Hvu: v = x + u.
Apply SNoR_E (y + z) Lyz u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev (y + z).
Assume Hu3: y + z < u.
rewrite the current goal using Hvu (from left to right).
We will prove (x + y) + z < x + u.
Apply add_SNo_SNoR_interpolate y z Hy Hz u Hu to the current goal.
Assume H1: ∃v ∈ SNoR y, v + z ≤ u.
Apply H1 to the current goal.
Let v be given.
Assume H2.
Apply H2 to the current goal.
Assume Hv: v ∈ SNoR y.
Assume H2: v + z ≤ u.
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 IH2v: x + (v + z) = (x + v) + z.
An exact proof term for the current goal is IH2 v (SNoR_SNoS_ y v Hv).
We will prove (x + y) + z < x + u.
Apply SNoLtLe_tra ((x + y) + z) (x + (v + z)) (x + u) (SNo_add_SNo (x + y) z Lxy Hz) (SNo_add_SNo x (v + z) Hx (SNo_add_SNo v z Hv1 Hz)) (SNo_add_SNo x u Hx Hu1) to the current goal.
We will prove (x + y) + z < x + (v + z).
rewrite the current goal using IH2v (from left to right).
We will prove (x + y) + z < (x + v) + z.
Apply add_SNo_Lt1 (x + y) z (x + v) Lxy Hz (SNo_add_SNo x v Hx Hv1) to the current goal.
We will prove x + y < x + v.
Apply add_SNo_Lt2 x y v Hx Hy Hv1 to the current goal.
We will prove y < v.
An exact proof term for the current goal is Hv3.
We will prove x + (v + z) ≤ x + u.
Apply add_SNo_Le2 x (v + z) u Hx (SNo_add_SNo v z Hv1 Hz) Hu1 to the current goal.
We will prove v + z ≤ u.
An exact proof term for the current goal is H2.
Assume H1: ∃v ∈ SNoR z, y + v ≤ u.
Apply H1 to the current goal.
Let v be given.
Assume H2.
Apply H2 to the current goal.
Assume Hv: v ∈ SNoR z.
Assume H2: y + v ≤ u.
Apply SNoR_E z Hz v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev z.
Assume Hv3: z < v.
We prove the intermediate claim IH3v: x + (y + v) = (x + y) + v.
An exact proof term for the current goal is IH3 v (SNoR_SNoS_ z v Hv).
We will prove (x + y) + z < x + u.
Apply SNoLtLe_tra ((x + y) + z) (x + (y + v)) (x + u) (SNo_add_SNo (x + y) z Lxy Hz) (SNo_add_SNo x (y + v) Hx (SNo_add_SNo y v Hy Hv1)) (SNo_add_SNo x u Hx Hu1) to the current goal.
We will prove (x + y) + z < x + (y + v).
rewrite the current goal using IH3v (from left to right).
We will prove (x + y) + z < (x + y) + v.
Apply add_SNo_Lt2 (x + y) z v Lxy Hz Hv1 to the current goal.
We will prove z < v.
An exact proof term for the current goal is Hv3.
We will prove x + (y + v) ≤ x + u.
Apply add_SNo_Le2 x (y + v) u Hx (SNo_add_SNo y v Hy Hv1) Hu1 to the current goal.
We will prove y + v ≤ u.
An exact proof term for the current goal is H2.
We will prove ∀w ∈ Lxyz3 ∪ Lxyz4, w < SNoCut (Lxyz1 ∪ Lxyz2) (Rxyz1 ∪ Rxyz2).
rewrite the current goal using add_SNo_eq x Hx (y + z) Lyz (from right to left).
We will prove ∀w ∈ Lxyz3 ∪ Lxyz4, w < x + (y + z).
Let w be given.
Assume Hw: w ∈ Lxyz3 ∪ Lxyz4.
Apply binunionE Lxyz3 Lxyz4 w Hw to the current goal.
Assume Hw: w ∈ Lxyz3.
Apply ReplE_impred (SNoL (x + y)) (λw ⇒ w + z) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL (x + y).
Assume Hwu: w = u + z.
Apply SNoL_E (x + y) Lxy u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev (x + y).
Assume Hu3: u < x + y.
rewrite the current goal using Hwu (from left to right).
We will prove u + z < x + (y + z).
Apply add_SNo_SNoL_interpolate x y Hx Hy u Hu to the current goal.
Assume H1: ∃v ∈ SNoL x, u ≤ v + y.
Apply H1 to the current goal.
Let v be given.
Assume H2.
Apply H2 to the current goal.
Assume Hv: v ∈ SNoL x.
Assume H2: u ≤ v + y.
Apply SNoL_E x Hx v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev x.
Assume Hv3: v < x.
We prove the intermediate claim IH1v: v + (y + z) = (v + y) + z.
An exact proof term for the current goal is IH1 v (SNoL_SNoS_ x v Hv).
We will prove u + z < x + (y + z).
Apply SNoLeLt_tra (u + z) ((v + y) + z) (x + (y + z)) (SNo_add_SNo u z Hu1 Hz) (SNo_add_SNo (v + y) z (SNo_add_SNo v y Hv1 Hy) Hz) (SNo_add_SNo x (y + z) Hx Lyz) to the current goal.
We will prove u + z ≤ (v + y) + z.
Apply add_SNo_Le1 u z (v + y) Hu1 Hz (SNo_add_SNo v y Hv1 Hy) to the current goal.
We will prove u ≤ v + y.
An exact proof term for the current goal is H2.
We will prove (v + y) + z < x + (y + z).
rewrite the current goal using IH1v (from right to left).
We will prove v + (y + z) < x + (y + z).
Apply add_SNo_Lt1 v (y + z) x Hv1 Lyz Hx to the current goal.
We will prove v < x.
An exact proof term for the current goal is Hv3.
Assume H1: ∃v ∈ SNoL y, u ≤ x + v.
Apply H1 to the current goal.
Let v be given.
Assume H2.
Apply H2 to the current goal.
Assume Hv: v ∈ SNoL y.
Assume H2: u ≤ x + v.
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev y.
Assume Hv3: v < y.
We prove the intermediate claim IH2v: x + (v + z) = (x + v) + z.
An exact proof term for the current goal is IH2 v (SNoL_SNoS_ y v Hv).
We will prove u + z < x + (y + z).
Apply SNoLeLt_tra (u + z) ((x + v) + z) (x + (y + z)) (SNo_add_SNo u z Hu1 Hz) (SNo_add_SNo (x + v) z (SNo_add_SNo x v Hx Hv1) Hz) (SNo_add_SNo x (y + z) Hx Lyz) to the current goal.
We will prove u + z ≤ (x + v) + z.
Apply add_SNo_Le1 u z (x + v) Hu1 Hz (SNo_add_SNo x v Hx Hv1) to the current goal.
We will prove u ≤ x + v.
An exact proof term for the current goal is H2.
We will prove (x + v) + z < x + (y + z).
rewrite the current goal using IH2v (from right to left).
We will prove x + (v + z) < x + (y + z).
Apply add_SNo_Lt2 x (v + z) (y + z) Hx (SNo_add_SNo v z Hv1 Hz) Lyz to the current goal.
We will prove v + z < y + z.
Apply add_SNo_Lt1 v z y Hv1 Hz Hy to the current goal.
We will prove v < y.
An exact proof term for the current goal is Hv3.
Assume Hw: w ∈ Lxyz4.
Apply ReplE_impred (SNoL z) (λw ⇒ (x + y) + w) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL z.
Assume Hwu: w = (x + y) + u.
Apply SNoL_E z Hz u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev z.
Assume Hu3: u < z.
We will prove w < x + (y + z).
rewrite the current goal using Hwu (from left to right).
We will prove (x + y) + u < x + (y + z).
We prove the intermediate claim IH3u: x + (y + u) = (x + y) + u.
An exact proof term for the current goal is IH3 u (SNoL_SNoS_ z u Hu).
rewrite the current goal using IH3u (from right to left).
We will prove x + (y + u) < x + (y + z).
Apply add_SNo_Lt2 x (y + u) (y + z) Hx (SNo_add_SNo y u Hy Hu1) Lyz to the current goal.
We will prove y + u < y + z.
Apply add_SNo_Lt2 y u z Hy Hu1 Hz to the current goal.
We will prove u < z.
An exact proof term for the current goal is Hu3.
We will prove ∀v ∈ Rxyz3 ∪ Rxyz4, SNoCut (Lxyz1 ∪ Lxyz2) (Rxyz1 ∪ Rxyz2) < v.
rewrite the current goal using add_SNo_eq x Hx (y + z) Lyz (from right to left).
We will prove ∀v ∈ Rxyz3 ∪ Rxyz4, x + (y + z) < v.
Let v be given.
Assume Hv: v ∈ Rxyz3 ∪ Rxyz4.
Apply binunionE Rxyz3 Rxyz4 v Hv to the current goal.
Assume Hv: v ∈ Rxyz3.
Apply ReplE_impred (SNoR (x + y)) (λw ⇒ w + z) v Hv to the current goal.
Let u be given.
Assume Hu: u ∈ SNoR (x + y).
Assume Hvu: v = u + z.
Apply SNoR_E (x + y) Lxy u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev (x + y).
Assume Hu3: x + y < u.
rewrite the current goal using Hvu (from left to right).
We will prove x + (y + z) < u + z.
Apply add_SNo_SNoR_interpolate x y Hx Hy u Hu to the current goal.
Assume H1: ∃v ∈ SNoR x, v + y ≤ u.
Apply H1 to the current goal.
Let v be given.
Assume H2.
Apply H2 to the current goal.
Assume Hv: v ∈ SNoR x.
Assume H2: v + y ≤ u.
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 IH1v: v + (y + z) = (v + y) + z.
An exact proof term for the current goal is IH1 v (SNoR_SNoS_ x v Hv).
We will prove x + (y + z) < u + z.
Apply SNoLtLe_tra (x + (y + z)) ((v + y) + z) (u + z) (SNo_add_SNo x (y + z) Hx Lyz) (SNo_add_SNo (v + y) z (SNo_add_SNo v y Hv1 Hy) Hz) (SNo_add_SNo u z Hu1 Hz) to the current goal.
We will prove x + (y + z) < (v + y) + z.
rewrite the current goal using IH1v (from right to left).
We will prove x + (y + z) < v + (y + z).
Apply add_SNo_Lt1 x (y + z) v Hx Lyz Hv1 to the current goal.
We will prove x < v.
An exact proof term for the current goal is Hv3.
We will prove (v + y) + z ≤ u + z.
Apply add_SNo_Le1 (v + y) z u (SNo_add_SNo v y Hv1 Hy) Hz Hu1 to the current goal.
We will prove v + y ≤ u.
An exact proof term for the current goal is H2.
Assume H1: ∃v ∈ SNoR y, x + v ≤ u.
Apply H1 to the current goal.
Let v be given.
Assume H2.
Apply H2 to the current goal.
Assume Hv: v ∈ SNoR y.
Assume H2: x + v ≤ u.
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 IH2v: x + (v + z) = (x + v) + z.
An exact proof term for the current goal is IH2 v (SNoR_SNoS_ y v Hv).
We will prove x + (y + z) < u + z.
Apply SNoLtLe_tra (x + (y + z)) ((x + v) + z) (u + z) (SNo_add_SNo x (y + z) Hx Lyz) (SNo_add_SNo (x + v) z (SNo_add_SNo x v Hx Hv1) Hz) (SNo_add_SNo u z Hu1 Hz) to the current goal.
We will prove x + (y + z) < (x + v) + z.
rewrite the current goal using IH2v (from right to left).
We will prove x + (y + z) < x + (v + z).
Apply add_SNo_Lt2 x (y + z) (v + z) Hx Lyz (SNo_add_SNo v z Hv1 Hz) to the current goal.
We will prove y + z < v + z.
Apply add_SNo_Lt1 y z v Hy Hz Hv1 to the current goal.
We will prove y < v.
An exact proof term for the current goal is Hv3.
We will prove (x + v) + z ≤ u + z.
Apply add_SNo_Le1 (x + v) z u (SNo_add_SNo x v Hx Hv1) Hz Hu1 to the current goal.
We will prove x + v ≤ u.
An exact proof term for the current goal is H2.
Assume Hv: v ∈ Rxyz4.
Apply ReplE_impred (SNoR z) (λw ⇒ (x + y) + w) v Hv to the current goal.
Let u be given.
Assume Hu: u ∈ SNoR z.
Assume Hvu: v = (x + y) + u.
Apply SNoR_E z Hz u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev z.
Assume Hu3: z < u.
We will prove x + (y + z) < v.
rewrite the current goal using Hvu (from left to right).
We will prove x + (y + z) < (x + y) + u.
We prove the intermediate claim IH3u: x + (y + u) = (x + y) + u.
An exact proof term for the current goal is IH3 u (SNoR_SNoS_ z u Hu).
rewrite the current goal using IH3u (from right to left).
We will prove x + (y + z) < x + (y + u).
Apply add_SNo_Lt2 x (y + z) (y + u) Hx Lyz (SNo_add_SNo y u Hy Hu1) to the current goal.
We will prove y + z < y + u.
Apply add_SNo_Lt2 y z u Hy Hz Hu1 to the current goal.
We will prove z < u.
An exact proof term for the current goal is Hu3.
∎
Theorem. (add_SNo_cancel_L)
∀x y z, SNo x → SNo y → SNo z → x + y = x + z → y = z
In Proofgold the corresponding term root is 014096... and proposition id is 781256...
Proof:
Let x, y and z be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume Hz: SNo z.
Assume Hxyz: x + y = x + z.
We prove the intermediate claim Lmx: SNo (- x).
An exact proof term for the current goal is SNo_minus_SNo x Hx.
We prove the intermediate claim L1: - x + (x + y) = y.
rewrite the current goal using add_SNo_assoc (- x) x y Lmx Hx Hy (from left to right).
We will prove (- x + x) + y = y.
rewrite the current goal using add_SNo_minus_SNo_linv x Hx (from left to right).
We will prove 0 + y = y.
An exact proof term for the current goal is add_SNo_0L y Hy.
We prove the intermediate claim L2: - x + (x + z) = z.
rewrite the current goal using add_SNo_assoc (- x) x z Lmx Hx Hz (from left to right).
We will prove (- x + x) + z = z.
rewrite the current goal using add_SNo_minus_SNo_linv x Hx (from left to right).
We will prove 0 + z = z.
An exact proof term for the current goal is add_SNo_0L z Hz.
rewrite the current goal using L1 (from right to left).
rewrite the current goal using Hxyz (from left to right).
An exact proof term for the current goal is L2.
∎
Theorem. (minus_SNo_0)
- 0 = 0
In Proofgold the corresponding term root is 77bc67... and proposition id is 3fcc57...
Proof:
Apply add_SNo_cancel_L 0 (- 0) 0 SNo_0 (SNo_minus_SNo 0 SNo_0) SNo_0 to the current goal.
We will prove 0 + - 0 = 0 + 0.
Use transitivity with and 0.
An exact proof term for the current goal is add_SNo_minus_SNo_rinv 0 SNo_0.
Use symmetry.
An exact proof term for the current goal is add_SNo_0L 0 SNo_0.
∎
Theorem. (minus_add_SNo_distr)
∀x y, SNo x → SNo y → - (x + y) = (- x) + (- y)
In Proofgold the corresponding term root is 57ec9d... and proposition id is da8d5a...
Proof:
Let x and y be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
We prove the intermediate claim Lmx: SNo (- x).
An exact proof term for the current goal is SNo_minus_SNo x Hx.
We prove the intermediate claim Lmy: SNo (- y).
An exact proof term for the current goal is SNo_minus_SNo y Hy.
We prove the intermediate claim Lxy: SNo (x + y).
An exact proof term for the current goal is SNo_add_SNo x y Hx Hy.
We prove the intermediate claim L1: (x + y) + - (x + y) = (x + y) + ((- x) + (- y)).
rewrite the current goal using add_SNo_minus_SNo_rinv (x + y) Lxy (from left to right).
We will prove 0 = (x + y) + ((- x) + (- y)).
rewrite the current goal using add_SNo_assoc (x + y) (- x) (- y) Lxy Lmx Lmy (from left to right).
We will prove 0 = ((x + y) + (- x)) + (- y).
rewrite the current goal using add_SNo_com x y Hx Hy (from left to right).
We will prove 0 = ((y + x) + - x) + - y.
rewrite the current goal using add_SNo_assoc y x (- x) Hy Hx Lmx (from right to left).
We will prove 0 = (y + (x + - x)) + - y.
rewrite the current goal using add_SNo_minus_SNo_rinv x Hx (from left to right).
We will prove 0 = (y + 0) + - y.
rewrite the current goal using add_SNo_0R y Hy (from left to right).
We will prove 0 = y + - y.
rewrite the current goal using add_SNo_minus_SNo_rinv y Hy (from left to right).
We will prove 0 = 0.
Use reflexivity.
An exact proof term for the current goal is add_SNo_cancel_L (x + y) (- (x + y)) ((- x) + (- y)) Lxy (SNo_minus_SNo (x + y) Lxy) (SNo_add_SNo (- x) (- y) Lmx Lmy) L1.
∎
Theorem. (minus_add_SNo_distr_3)
∀x y z, SNo x → SNo y → SNo z → - (x + y + z) = - x + - y + - z
In Proofgold the corresponding term root is b074ac... and proposition id is 94dbf3...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz.
Use transitivity with and - x + - (y + z).
An exact proof term for the current goal is minus_add_SNo_distr x (y + z) Hx (SNo_add_SNo y z Hy Hz).
Use f_equal.
We will prove - (y + z) = - y + - z.
An exact proof term for the current goal is minus_add_SNo_distr y z Hy Hz.
∎
Theorem. (add_SNo_Lev_bd)
∀x y, SNo x → SNo y → SNoLev (x + y) ⊆ SNoLev x + SNoLev y
In Proofgold the corresponding term root is 0f257c... and proposition id is 0680ef...
Proof:
Set P to be the term λx y ⇒ SNoLev (x + y) ⊆ SNoLev x + SNoLev y of type set → set → prop.
Apply SNoLev_ind2 to the current goal.
Let x and y be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
We prove the intermediate claim Lxy: SNo (x + y).
An exact proof term for the current goal is SNo_add_SNo x y Hx Hy.
We prove the intermediate claim LLxLy: ordinal (SNoLev x + SNoLev y).
Apply add_SNo_ordinal_ordinal to the current goal.
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is Hx.
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is Hy.
Assume IH1: ∀w ∈ SNoS_ (SNoLev x), P w y.
Assume IH2: ∀z ∈ SNoS_ (SNoLev y), P x z.
Assume IH3: ∀w ∈ SNoS_ (SNoLev x), ∀z ∈ SNoS_ (SNoLev y), P w z.
We will prove SNoLev (x + y) ⊆ SNoLev x + SNoLev y.
Set Lxy1 to be the term {w + y|w ∈ SNoL x}.
Set Lxy2 to be the term {x + w|w ∈ SNoL y}.
Set Rxy1 to be the term {z + y|z ∈ SNoR x}.
Set Rxy2 to be the term {x + z|z ∈ SNoR y}.
rewrite the current goal using add_SNo_eq x Hx y Hy (from left to right).
We will prove SNoLev (SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2)) ⊆ SNoLev x + SNoLev y.
We prove the intermediate claim L1: SNoCutP (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2).
An exact proof term for the current goal is add_SNo_SNoCutP x y Hx Hy.
Apply SNoCutP_SNoCut_impred (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2) L1 to the current goal.
Assume H1: SNo (SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2)).
Assume H2: SNoLev (SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2)) ∈ ordsucc ((⋃x ∈ (Lxy1 ∪ Lxy2)ordsucc (SNoLev x)) ∪ (⋃y ∈ (Rxy1 ∪ Rxy2)ordsucc (SNoLev y))).
Assume _ _ _.
We prove the intermediate claim Lxy1E: ∀u ∈ Lxy1, ∀p : set → prop, (∀w ∈ SNoS_ (SNoLev x), u = w + y → SNo w → SNoLev w ∈ SNoLev x → w < x → p (w + y)) → p u.
Let u be given.
Assume Hu.
Let p be given.
Assume Hp.
Apply ReplE_impred (SNoL x) (λw ⇒ w + y) u Hu to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL x.
Assume Huw: u = w + y.
rewrite the current goal using Huw (from left to right).
Apply SNoL_E x Hx w Hw to the current goal.
We prove the intermediate claim Lw: w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoL_SNoS_ x w Hw.
An exact proof term for the current goal is Hp w Lw Huw.
We prove the intermediate claim Lxy2E: ∀u ∈ Lxy2, ∀p : set → prop, (∀w ∈ SNoS_ (SNoLev y), u = x + w → SNo w → SNoLev w ∈ SNoLev y → w < y → p (x + w)) → p u.
Let u be given.
Assume Hu.
Let p be given.
Assume Hp.
Apply ReplE_impred (SNoL y) (λw ⇒ x + w) u Hu to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL y.
Assume Huw: u = x + w.
rewrite the current goal using Huw (from left to right).
Apply SNoL_E y Hy w Hw to the current goal.
We prove the intermediate claim Lw: w ∈ SNoS_ (SNoLev y).
An exact proof term for the current goal is SNoL_SNoS_ y w Hw.
An exact proof term for the current goal is Hp w Lw Huw.
We prove the intermediate claim Rxy1E: ∀u ∈ Rxy1, ∀p : set → prop, (∀w ∈ SNoS_ (SNoLev x), u = w + y → SNo w → SNoLev w ∈ SNoLev x → x < w → p (w + y)) → p u.
Let u be given.
Assume Hu.
Let p be given.
Assume Hp.
Apply ReplE_impred (SNoR x) (λw ⇒ w + y) u Hu to the current goal.
Let w be given.
Assume Hw: w ∈ SNoR x.
Assume Huw: u = w + y.
rewrite the current goal using Huw (from left to right).
Apply SNoR_E x Hx w Hw to the current goal.
We prove the intermediate claim Lw: w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoR_SNoS_ x w Hw.
An exact proof term for the current goal is Hp w Lw Huw.
We prove the intermediate claim Rxy2E: ∀u ∈ Rxy2, ∀p : set → prop, (∀w ∈ SNoS_ (SNoLev y), u = x + w → SNo w → SNoLev w ∈ SNoLev y → y < w → p (x + w)) → p u.
Let u be given.
Assume Hu.
Let p be given.
Assume Hp.
Apply ReplE_impred (SNoR y) (λw ⇒ x + w) u Hu to the current goal.
Let w be given.
Assume Hw: w ∈ SNoR y.
Assume Huw: u = x + w.
rewrite the current goal using Huw (from left to right).
Apply SNoR_E y Hy w Hw to the current goal.
We prove the intermediate claim Lw: w ∈ SNoS_ (SNoLev y).
An exact proof term for the current goal is SNoR_SNoS_ y w Hw.
An exact proof term for the current goal is Hp w Lw Huw.
We prove the intermediate claim Lxy1E2: ∀u ∈ Lxy1, SNo u.
Let u be given.
Assume Hu.
Apply Lxy1E u Hu to the current goal.
Let w be given.
Assume Hw1 Hw2 Hw3 Hw4 Hw5.
We will prove SNo (w + y).
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hw3.
An exact proof term for the current goal is Hy.
We prove the intermediate claim Lxy2E2: ∀u ∈ Lxy2, SNo u.
Let u be given.
Assume Hu.
Apply Lxy2E u Hu to the current goal.
Let w be given.
Assume Hw1 Hw2 Hw3 Hw4 Hw5.
We will prove SNo (x + w).
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hw3.
We prove the intermediate claim Rxy1E2: ∀u ∈ Rxy1, SNo u.
Let u be given.
Assume Hu.
Apply Rxy1E u Hu to the current goal.
Let w be given.
Assume Hw1 Hw2 Hw3 Hw4 Hw5.
We will prove SNo (w + y).
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hw3.
An exact proof term for the current goal is Hy.
We prove the intermediate claim Rxy2E2: ∀u ∈ Rxy2, SNo u.
Let u be given.
Assume Hu.
Apply Rxy2E u Hu to the current goal.
Let w be given.
Assume Hw1 Hw2 Hw3 Hw4 Hw5.
We will prove SNo (x + w).
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hw3.
We prove the intermediate claim L2: ordinal ((⋃u ∈ (Lxy1 ∪ Lxy2)ordsucc (SNoLev u)) ∪ (⋃u ∈ (Rxy1 ∪ Rxy2)ordsucc (SNoLev u))).
Apply ordinal_binunion to the current goal.
Apply ordinal_famunion (Lxy1 ∪ Lxy2) (λu ⇒ ordsucc (SNoLev u)) to the current goal.
Let u be given.
Assume Hu: u ∈ Lxy1 ∪ Lxy2.
We will prove ordinal (ordsucc (SNoLev u)).
Apply ordinal_ordsucc to the current goal.
Apply SNoLev_ordinal to the current goal.
We will prove SNo u.
Apply binunionE Lxy1 Lxy2 u Hu to the current goal.
Assume Hu.
An exact proof term for the current goal is Lxy1E2 u Hu.
Assume Hu.
An exact proof term for the current goal is Lxy2E2 u Hu.
Apply ordinal_famunion (Rxy1 ∪ Rxy2) (λu ⇒ ordsucc (SNoLev u)) to the current goal.
Let u be given.
Assume Hu: u ∈ Rxy1 ∪ Rxy2.
We will prove ordinal (ordsucc (SNoLev u)).
Apply ordinal_ordsucc to the current goal.
Apply SNoLev_ordinal to the current goal.
We will prove SNo u.
Apply binunionE Rxy1 Rxy2 u Hu to the current goal.
Assume Hu.
An exact proof term for the current goal is Rxy1E2 u Hu.
Assume Hu.
An exact proof term for the current goal is Rxy2E2 u Hu.
We prove the intermediate claim L3: SNoLev (SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2)) ⊆ (⋃u ∈ (Lxy1 ∪ Lxy2)ordsucc (SNoLev u)) ∪ (⋃u ∈ (Rxy1 ∪ Rxy2)ordsucc (SNoLev u)).
Apply TransSet_In_ordsucc_Subq to the current goal.
We will prove TransSet ((⋃u ∈ (Lxy1 ∪ Lxy2)ordsucc (SNoLev u)) ∪ (⋃u ∈ (Rxy1 ∪ Rxy2)ordsucc (SNoLev u))).
Apply L2 to the current goal.
Assume H _.
An exact proof term for the current goal is H.
An exact proof term for the current goal is H2.
We prove the intermediate claim L4: ((⋃u ∈ (Lxy1 ∪ Lxy2)ordsucc (SNoLev u)) ∪ (⋃u ∈ (Rxy1 ∪ Rxy2)ordsucc (SNoLev u))) ⊆ SNoLev x + SNoLev y.
Apply binunion_Subq_min to the current goal.
We will prove (⋃u ∈ (Lxy1 ∪ Lxy2)ordsucc (SNoLev u)) ⊆ SNoLev x + SNoLev y.
Let v be given.
Assume Hv: v ∈ (⋃u ∈ (Lxy1 ∪ Lxy2)ordsucc (SNoLev u)).
Apply famunionE_impred (Lxy1 ∪ Lxy2) (λu ⇒ ordsucc (SNoLev u)) v Hv to the current goal.
Let u be given.
Assume Hu: u ∈ Lxy1 ∪ Lxy2.
Apply binunionE Lxy1 Lxy2 u Hu to the current goal.
Assume Hu: u ∈ Lxy1.
Apply Lxy1E u Hu to the current goal.
Let w be given.
Assume Hw1: w ∈ SNoS_ (SNoLev x).
Assume Hw2: u = w + y.
Assume Hw3: SNo w.
Assume Hw4: SNoLev w ∈ SNoLev x.
Assume Hw5: w < x.
Assume Hw6: v ∈ ordsucc (SNoLev (w + y)).
We will prove v ∈ SNoLev x + SNoLev y.
We prove the intermediate claim Lv: ordinal v.
Apply ordinal_Hered (ordsucc (SNoLev (w + y))) to the current goal.
We will prove ordinal (ordsucc (SNoLev (w + y))).
Apply ordinal_ordsucc to the current goal.
Apply SNoLev_ordinal to the current goal.
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hw3.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Hw6.
Apply ordinal_In_Or_Subq v (SNoLev x + SNoLev y) Lv LLxLy to the current goal.
Assume H1: v ∈ SNoLev x + SNoLev y.
An exact proof term for the current goal is H1.
Assume H1: SNoLev x + SNoLev y ⊆ v.
We will prove False.
We prove the intermediate claim LIHw: SNoLev (w + y) ⊆ SNoLev w + SNoLev y.
Apply IH1 to the current goal.
We will prove w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is Hw1.
We prove the intermediate claim L4a: SNoLev w + SNoLev y ∈ SNoLev x + SNoLev y.
Apply add_SNo_ordinal_InL to the current goal.
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is Hx.
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Hw4.
We prove the intermediate claim L4b: SNoLev w + SNoLev y ⊆ SNoLev x + SNoLev y.
Apply LLxLy to the current goal.
Assume H _.
An exact proof term for the current goal is H (SNoLev w + SNoLev y) L4a.
We prove the intermediate claim L4c: v ⊆ SNoLev (w + y).
Apply ordinal_In_Or_Subq (SNoLev (w + y)) v (SNoLev_ordinal (w + y) (SNo_add_SNo w y Hw3 Hy)) Lv to the current goal.
Assume H2: SNoLev (w + y) ∈ v.
We will prove False.
Apply ordsuccE (SNoLev (w + y)) v Hw6 to the current goal.
Assume H3: v ∈ SNoLev (w + y).
An exact proof term for the current goal is In_no2cycle (SNoLev (w + y)) v H2 H3.
Assume H3: v = SNoLev (w + y).
Apply In_irref v to the current goal.
rewrite the current goal using H3 (from left to right) at position 1.
An exact proof term for the current goal is H2.
Assume H2: v ⊆ SNoLev (w + y).
An exact proof term for the current goal is H2.
Apply In_irref (SNoLev w + SNoLev y) to the current goal.
We will prove (SNoLev w + SNoLev y) ∈ (SNoLev w + SNoLev y).
Apply LIHw to the current goal.
We will prove (SNoLev w + SNoLev y) ∈ SNoLev (w + y).
Apply L4c to the current goal.
We will prove (SNoLev w + SNoLev y) ∈ v.
Apply H1 to the current goal.
We will prove (SNoLev w + SNoLev y) ∈ SNoLev x + SNoLev y.
An exact proof term for the current goal is L4a.
Assume Hu: u ∈ Lxy2.
Apply Lxy2E u Hu to the current goal.
Let w be given.
Assume Hw1: w ∈ SNoS_ (SNoLev y).
Assume Hw2: u = x + w.
Assume Hw3: SNo w.
Assume Hw4: SNoLev w ∈ SNoLev y.
Assume Hw5: w < y.
Assume Hw6: v ∈ ordsucc (SNoLev (x + w)).
We will prove v ∈ SNoLev x + SNoLev y.
We prove the intermediate claim Lv: ordinal v.
Apply ordinal_Hered (ordsucc (SNoLev (x + w))) to the current goal.
We will prove ordinal (ordsucc (SNoLev (x + w))).
Apply ordinal_ordsucc to the current goal.
Apply SNoLev_ordinal to the current goal.
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hw3.
An exact proof term for the current goal is Hw6.
Apply ordinal_In_Or_Subq v (SNoLev x + SNoLev y) Lv LLxLy to the current goal.
Assume H1: v ∈ SNoLev x + SNoLev y.
An exact proof term for the current goal is H1.
Assume H1: SNoLev x + SNoLev y ⊆ v.
We will prove False.
We prove the intermediate claim LIHw: SNoLev (x + w) ⊆ SNoLev x + SNoLev w.
Apply IH2 to the current goal.
We will prove w ∈ SNoS_ (SNoLev y).
An exact proof term for the current goal is Hw1.
We prove the intermediate claim L4a: SNoLev x + SNoLev w ∈ SNoLev x + SNoLev y.
Apply add_SNo_ordinal_InR to the current goal.
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is Hx.
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Hw4.
We prove the intermediate claim L4b: SNoLev x + SNoLev w ⊆ SNoLev x + SNoLev y.
Apply LLxLy to the current goal.
Assume H _.
An exact proof term for the current goal is H (SNoLev x + SNoLev w) L4a.
We prove the intermediate claim L4c: v ⊆ SNoLev (x + w).
Apply ordinal_In_Or_Subq (SNoLev (x + w)) v (SNoLev_ordinal (x + w) (SNo_add_SNo x w Hx Hw3)) Lv to the current goal.
Assume H2: SNoLev (x + w) ∈ v.
We will prove False.
Apply ordsuccE (SNoLev (x + w)) v Hw6 to the current goal.
Assume H3: v ∈ SNoLev (x + w).
An exact proof term for the current goal is In_no2cycle (SNoLev (x + w)) v H2 H3.
Assume H3: v = SNoLev (x + w).
Apply In_irref v to the current goal.
rewrite the current goal using H3 (from left to right) at position 1.
An exact proof term for the current goal is H2.
Assume H2: v ⊆ SNoLev (x + w).
An exact proof term for the current goal is H2.
Apply In_irref (SNoLev x + SNoLev w) to the current goal.
We will prove (SNoLev x + SNoLev w) ∈ (SNoLev x + SNoLev w).
Apply LIHw to the current goal.
We will prove (SNoLev x + SNoLev w) ∈ SNoLev (x + w).
Apply L4c to the current goal.
We will prove (SNoLev x + SNoLev w) ∈ v.
Apply H1 to the current goal.
We will prove (SNoLev x + SNoLev w) ∈ SNoLev x + SNoLev y.
An exact proof term for the current goal is L4a.
We will prove (⋃u ∈ (Rxy1 ∪ Rxy2)ordsucc (SNoLev u)) ⊆ SNoLev x + SNoLev y.
Let v be given.
Assume Hv: v ∈ (⋃u ∈ (Rxy1 ∪ Rxy2)ordsucc (SNoLev u)).
Apply famunionE_impred (Rxy1 ∪ Rxy2) (λu ⇒ ordsucc (SNoLev u)) v Hv to the current goal.
Let u be given.
Assume Hu: u ∈ Rxy1 ∪ Rxy2.
Apply binunionE Rxy1 Rxy2 u Hu to the current goal.
Assume Hu: u ∈ Rxy1.
Apply Rxy1E u Hu to the current goal.
Let w be given.
Assume Hw1: w ∈ SNoS_ (SNoLev x).
Assume Hw2: u = w + y.
Assume Hw3: SNo w.
Assume Hw4: SNoLev w ∈ SNoLev x.
Assume Hw5: x < w.
Assume Hw6: v ∈ ordsucc (SNoLev (w + y)).
We will prove v ∈ SNoLev x + SNoLev y.
We prove the intermediate claim Lv: ordinal v.
Apply ordinal_Hered (ordsucc (SNoLev (w + y))) to the current goal.
We will prove ordinal (ordsucc (SNoLev (w + y))).
Apply ordinal_ordsucc to the current goal.
Apply SNoLev_ordinal to the current goal.
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hw3.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Hw6.
Apply ordinal_In_Or_Subq v (SNoLev x + SNoLev y) Lv LLxLy to the current goal.
Assume H1: v ∈ SNoLev x + SNoLev y.
An exact proof term for the current goal is H1.
Assume H1: SNoLev x + SNoLev y ⊆ v.
We will prove False.
We prove the intermediate claim LIHw: SNoLev (w + y) ⊆ SNoLev w + SNoLev y.
Apply IH1 to the current goal.
We will prove w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is Hw1.
We prove the intermediate claim L4a: SNoLev w + SNoLev y ∈ SNoLev x + SNoLev y.
Apply add_SNo_ordinal_InL to the current goal.
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is Hx.
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Hw4.
We prove the intermediate claim L4b: SNoLev w + SNoLev y ⊆ SNoLev x + SNoLev y.
Apply LLxLy to the current goal.
Assume H _.
An exact proof term for the current goal is H (SNoLev w + SNoLev y) L4a.
We prove the intermediate claim L4c: v ⊆ SNoLev (w + y).
Apply ordinal_In_Or_Subq (SNoLev (w + y)) v (SNoLev_ordinal (w + y) (SNo_add_SNo w y Hw3 Hy)) Lv to the current goal.
Assume H2: SNoLev (w + y) ∈ v.
We will prove False.
Apply ordsuccE (SNoLev (w + y)) v Hw6 to the current goal.
Assume H3: v ∈ SNoLev (w + y).
An exact proof term for the current goal is In_no2cycle (SNoLev (w + y)) v H2 H3.
Assume H3: v = SNoLev (w + y).
Apply In_irref v to the current goal.
rewrite the current goal using H3 (from left to right) at position 1.
An exact proof term for the current goal is H2.
Assume H2: v ⊆ SNoLev (w + y).
An exact proof term for the current goal is H2.
Apply In_irref (SNoLev w + SNoLev y) to the current goal.
We will prove (SNoLev w + SNoLev y) ∈ (SNoLev w + SNoLev y).
Apply LIHw to the current goal.
We will prove (SNoLev w + SNoLev y) ∈ SNoLev (w + y).
Apply L4c to the current goal.
We will prove (SNoLev w + SNoLev y) ∈ v.
Apply H1 to the current goal.
We will prove (SNoLev w + SNoLev y) ∈ SNoLev x + SNoLev y.
An exact proof term for the current goal is L4a.
Assume Hu: u ∈ Rxy2.
Apply Rxy2E u Hu to the current goal.
Let w be given.
Assume Hw1: w ∈ SNoS_ (SNoLev y).
Assume Hw2: u = x + w.
Assume Hw3: SNo w.
Assume Hw4: SNoLev w ∈ SNoLev y.
Assume Hw5: y < w.
Assume Hw6: v ∈ ordsucc (SNoLev (x + w)).
We will prove v ∈ SNoLev x + SNoLev y.
We prove the intermediate claim Lv: ordinal v.
Apply ordinal_Hered (ordsucc (SNoLev (x + w))) to the current goal.
We will prove ordinal (ordsucc (SNoLev (x + w))).
Apply ordinal_ordsucc to the current goal.
Apply SNoLev_ordinal to the current goal.
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hw3.
An exact proof term for the current goal is Hw6.
Apply ordinal_In_Or_Subq v (SNoLev x + SNoLev y) Lv LLxLy to the current goal.
Assume H1: v ∈ SNoLev x + SNoLev y.
An exact proof term for the current goal is H1.
Assume H1: SNoLev x + SNoLev y ⊆ v.
We will prove False.
We prove the intermediate claim LIHw: SNoLev (x + w) ⊆ SNoLev x + SNoLev w.
Apply IH2 to the current goal.
We will prove w ∈ SNoS_ (SNoLev y).
An exact proof term for the current goal is Hw1.
We prove the intermediate claim L4a: SNoLev x + SNoLev w ∈ SNoLev x + SNoLev y.
Apply add_SNo_ordinal_InR to the current goal.
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is Hx.
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is Hw4.
We prove the intermediate claim L4b: SNoLev x + SNoLev w ⊆ SNoLev x + SNoLev y.
Apply LLxLy to the current goal.
Assume H _.
An exact proof term for the current goal is H (SNoLev x + SNoLev w) L4a.
We prove the intermediate claim L4c: v ⊆ SNoLev (x + w).
Apply ordinal_In_Or_Subq (SNoLev (x + w)) v (SNoLev_ordinal (x + w) (SNo_add_SNo x w Hx Hw3)) Lv to the current goal.
Assume H2: SNoLev (x + w) ∈ v.
We will prove False.
Apply ordsuccE (SNoLev (x + w)) v Hw6 to the current goal.
Assume H3: v ∈ SNoLev (x + w).
An exact proof term for the current goal is In_no2cycle (SNoLev (x + w)) v H2 H3.
Assume H3: v = SNoLev (x + w).
Apply In_irref v to the current goal.
rewrite the current goal using H3 (from left to right) at position 1.
An exact proof term for the current goal is H2.
Assume H2: v ⊆ SNoLev (x + w).
An exact proof term for the current goal is H2.
Apply In_irref (SNoLev x + SNoLev w) to the current goal.
We will prove (SNoLev x + SNoLev w) ∈ (SNoLev x + SNoLev w).
Apply LIHw to the current goal.
We will prove (SNoLev x + SNoLev w) ∈ SNoLev (x + w).
Apply L4c to the current goal.
We will prove (SNoLev x + SNoLev w) ∈ v.
Apply H1 to the current goal.
We will prove (SNoLev x + SNoLev w) ∈ SNoLev x + SNoLev y.
An exact proof term for the current goal is L4a.
An exact proof term for the current goal is Subq_tra (SNoLev (SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2))) ((⋃u ∈ (Lxy1 ∪ Lxy2)ordsucc (SNoLev u)) ∪ (⋃u ∈ (Rxy1 ∪ Rxy2)ordsucc (SNoLev u))) (SNoLev x + SNoLev y) L3 L4.
∎
Theorem. (add_SNo_SNoS_omega)
∀x y ∈ SNoS_ ω, x + y ∈ SNoS_ ω
In Proofgold the corresponding term root is 931103... and proposition id is 6d16aa...
Proof:
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
Apply SNoS_E2 ω omega_ordinal 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.
Apply SNoS_E2 ω omega_ordinal y Hy to the current goal.
Assume Hy1: SNoLev y ∈ ω.
Assume Hy2: ordinal (SNoLev y).
Assume Hy3: SNo y.
Assume Hy4: SNo_ (SNoLev y) y.
Apply SNoS_I ω omega_ordinal (x + y) (SNoLev (x + y)) to the current goal.
We will prove SNoLev (x + y) ∈ ω.
We prove the intermediate claim LLxy: ordinal (SNoLev (x + y)).
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is SNo_add_SNo x y Hx3 Hy3.
Apply ordinal_In_Or_Subq (SNoLev (x + y)) ω LLxy omega_ordinal to the current goal.
Assume H1.
An exact proof term for the current goal is H1.
Assume H1: ω ⊆ SNoLev (x + y).
Apply In_irref (SNoLev x + SNoLev y) to the current goal.
We will prove (SNoLev x + SNoLev y) ∈ (SNoLev x + SNoLev y).
Apply add_SNo_Lev_bd x y Hx3 Hy3 to the current goal.
We will prove (SNoLev x + SNoLev y) ∈ SNoLev (x + y).
Apply H1 to the current goal.
We will prove (SNoLev x + SNoLev y) ∈ ω.
An exact proof term for the current goal is add_SNo_In_omega (SNoLev x) Hx1 (SNoLev y) Hy1.
We will prove SNo_ (SNoLev (x + y)) (x + y).
Apply SNoLev_ to the current goal.
An exact proof term for the current goal is SNo_add_SNo x y Hx3 Hy3.
∎
Theorem. (add_SNo_minus_R2)
∀x y, SNo x → SNo y → (x + y) + - y = x
In Proofgold the corresponding term root is 3e7b33... and proposition id is 91f4ef...
Proof:
Let x and y be given.
Assume Hx Hy.
Use transitivity with x + (y + - y), and x + 0.
Use symmetry.
An exact proof term for the current goal is add_SNo_assoc x y (- y) Hx Hy (SNo_minus_SNo y Hy).
Use f_equal.
An exact proof term for the current goal is add_SNo_minus_SNo_rinv y Hy.
An exact proof term for the current goal is add_SNo_0R x Hx.
∎
Theorem. (add_SNo_minus_R2')
∀x y, SNo x → SNo y → (x + - y) + y = x
In Proofgold the corresponding term root is 4f9468... and proposition id is 43b4d1...
Proof:
Let x and y be given.
Assume Hx Hy.
rewrite the current goal using minus_SNo_invol y Hy (from right to left) at position 2.
An exact proof term for the current goal is add_SNo_minus_R2 x (- y) Hx (SNo_minus_SNo y Hy).
∎
Theorem. (add_SNo_minus_L2)
∀x y, SNo x → SNo y → - x + (x + y) = y
In Proofgold the corresponding term root is 2cd65e... and proposition id is 598ee6...
Proof:
Let x and y be given.
Assume Hx Hy.
rewrite the current goal using add_SNo_com (- x) (x + y) (SNo_minus_SNo x Hx) (SNo_add_SNo x y Hx Hy) (from left to right).
We will prove (x + y) + - x = y.
rewrite the current goal using add_SNo_com x y Hx Hy (from left to right).
We will prove (y + x) + - x = y.
An exact proof term for the current goal is add_SNo_minus_R2 y x Hy Hx.
∎
Theorem. (add_SNo_minus_L2')
∀x y, SNo x → SNo y → x + (- x + y) = y
In Proofgold the corresponding term root is 632a4d... and proposition id is a8450d...
Proof:
Let x and y be given.
Assume Hx Hy.
rewrite the current goal using minus_SNo_invol x Hx (from right to left) at position 1.
An exact proof term for the current goal is add_SNo_minus_L2 (- x) y (SNo_minus_SNo x Hx) Hy.
∎
Theorem. (add_SNo_Lt1_cancel)
∀x y z, SNo x → SNo y → SNo z → x + y < z + y → x < z
In Proofgold the corresponding term root is e5c11e... and proposition id is 2ec8ae...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz H1.
We will prove x < z.
We prove the intermediate claim L1: (x + y) + - y = x.
An exact proof term for the current goal is add_SNo_minus_R2 x y Hx Hy.
We prove the intermediate claim L2: (z + y) + - y = z.
An exact proof term for the current goal is add_SNo_minus_R2 z y Hz Hy.
rewrite the current goal using L1 (from right to left).
rewrite the current goal using L2 (from right to left).
We will prove (x + y) + - y < (z + y) + - y.
An exact proof term for the current goal is add_SNo_Lt1 (x + y) (- y) (z + y) (SNo_add_SNo x y Hx Hy) (SNo_minus_SNo y Hy) (SNo_add_SNo z y Hz Hy) H1.
∎
Theorem. (add_SNo_Lt2_cancel)
∀x y z, SNo x → SNo y → SNo z → x + y < x + z → y < z
In Proofgold the corresponding term root is 9ecfc8... and proposition id is d4afbd...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz.
rewrite the current goal using add_SNo_com x y Hx Hy (from left to right).
rewrite the current goal using add_SNo_com x z Hx Hz (from left to right).
An exact proof term for the current goal is add_SNo_Lt1_cancel y x z Hy Hx Hz.
∎
Theorem. (add_SNo_assoc_4)
∀x y z w, SNo x → SNo y → SNo z → SNo w → x + y + z + w = (x + y + z) + w
In Proofgold the corresponding term root is b9919a... and proposition id is f2ec8c...
Proof:
Let x, y, z and w be given.
Assume Hx Hy Hz Hw.
Use transitivity with (x + y) + z + w, and ((x + y) + z) + w.
An exact proof term for the current goal is add_SNo_assoc x y (z + w) Hx Hy (SNo_add_SNo z w Hz Hw).
An exact proof term for the current goal is add_SNo_assoc (x + y) z w (SNo_add_SNo x y Hx Hy) Hz Hw.
Use f_equal.
Use symmetry.
An exact proof term for the current goal is add_SNo_assoc x y z Hx Hy Hz.
∎
Theorem. (add_SNo_com_3_0_1)
∀x y z, SNo x → SNo y → SNo z → x + y + z = y + x + z
In Proofgold the corresponding term root is 53adb5... and proposition id is 3c9cc8...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz.
rewrite the current goal using add_SNo_assoc x y z Hx Hy Hz (from left to right).
rewrite the current goal using add_SNo_assoc y x z Hy Hx Hz (from left to right).
Use f_equal.
An exact proof term for the current goal is add_SNo_com x y Hx Hy.
∎
Theorem. (add_SNo_com_3b_1_2)
∀x y z, SNo x → SNo y → SNo z → (x + y) + z = (x + z) + y
In Proofgold the corresponding term root is 2ccf2b... and proposition id is f2dd80...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz.
rewrite the current goal using add_SNo_assoc x y z Hx Hy Hz (from right to left).
rewrite the current goal using add_SNo_assoc x z y Hx Hz Hy (from right to left).
Use f_equal.
An exact proof term for the current goal is add_SNo_com y z Hy Hz.
∎
Theorem. (add_SNo_com_4_inner_mid)
∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + y) + (z + w) = (x + z) + (y + w)
In Proofgold the corresponding term root is 635cb7... and proposition id is e25ee6...
Proof:
Let x, y, z and w be given.
Assume Hx Hy Hz Hw.
rewrite the current goal using add_SNo_assoc (x + y) z w (SNo_add_SNo x y Hx Hy) Hz Hw (from left to right).
We will prove ((x + y) + z) + w = (x + z) + (y + w).
rewrite the current goal using add_SNo_com_3b_1_2 x y z Hx Hy Hz (from left to right).
We will prove ((x + z) + y) + w = (x + z) + (y + w).
Use symmetry.
An exact proof term for the current goal is add_SNo_assoc (x + z) y w (SNo_add_SNo x z Hx Hz) Hy Hw.
∎
Theorem. (add_SNo_rotate_3_1)
∀x y z, SNo x → SNo y → SNo z → x + y + z = z + x + y
In Proofgold the corresponding term root is 51654e... and proposition id is 340640...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz.
We will prove x + (y + z) = z + (x + y).
Use transitivity with x + (z + y), (x + z) + y, and (z + x) + y.
Use f_equal.
An exact proof term for the current goal is add_SNo_com y z Hy Hz.
An exact proof term for the current goal is add_SNo_assoc x z y Hx Hz Hy.
Use f_equal.
An exact proof term for the current goal is add_SNo_com x z Hx Hz.
Use symmetry.
An exact proof term for the current goal is add_SNo_assoc z x y Hz Hx Hy.
∎
Theorem. (add_SNo_rotate_4_1)
∀x y z w, SNo x → SNo y → SNo z → SNo w → x + y + z + w = w + x + y + z
In Proofgold the corresponding term root is 4bc7aa... and proposition id is ce0a6b...
Proof:
Let x, y, z and w be given.
Assume Hx Hy Hz Hw.
rewrite the current goal using add_SNo_rotate_3_1 y z w Hy Hz Hw (from left to right).
We will prove x + w + y + z = w + x + y + z.
An exact proof term for the current goal is add_SNo_com_3_0_1 x w (y + z) Hx Hw (SNo_add_SNo y z Hy Hz).
∎
Theorem. (add_SNo_rotate_5_1)
∀x y z w v, SNo x → SNo y → SNo z → SNo w → SNo v → x + y + z + w + v = v + x + y + z + w
In Proofgold the corresponding term root is 4b4b64... and proposition id is 0714aa...
Proof:
Let x, y, z, w and v be given.
Assume Hx Hy Hz Hw Hv.
rewrite the current goal using add_SNo_rotate_4_1 y z w v Hy Hz Hw Hv (from left to right).
We will prove x + v + y + z + w = v + x + y + z + w.
An exact proof term for the current goal is add_SNo_com_3_0_1 x v (y + z + w) Hx Hv (SNo_add_SNo_3 y z w Hy Hz Hw).
∎
Theorem. (add_SNo_rotate_5_2)
∀x y z w v, SNo x → SNo y → SNo z → SNo w → SNo v → x + y + z + w + v = w + v + x + y + z
In Proofgold the corresponding term root is 33b5cc... and proposition id is fec9d0...
Proof:
Let x, y, z, w and v be given.
Assume Hx Hy Hz Hw Hv.
Use transitivity with and (v + x + y + z + w).
An exact proof term for the current goal is add_SNo_rotate_5_1 x y z w v Hx Hy Hz Hw Hv.
An exact proof term for the current goal is add_SNo_rotate_5_1 v x y z w Hv Hx Hy Hz Hw.
∎
Theorem. (add_SNo_minus_SNo_prop2)
∀x y, SNo x → SNo y → x + - x + y = y
In Proofgold the corresponding term root is 632a4d... and proposition id is a8450d...
Proof:
Let x and y be given.
Assume Hx Hy.
rewrite the current goal using add_SNo_assoc x (- x) y Hx (SNo_minus_SNo x Hx) Hy (from left to right).
We will prove (x + - x) + y = y.
rewrite the current goal using add_SNo_minus_SNo_rinv x Hx (from left to right).
We will prove 0 + y = y.
An exact proof term for the current goal is add_SNo_0L y Hy.
∎
Theorem. (add_SNo_minus_SNo_prop3)
∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + y + z) + (- z + w) = x + y + w
In Proofgold the corresponding term root is 038fdd... and proposition id is 0d4f24...
Proof:
Let x, y, z and w be given.
Assume Hx Hy Hz Hw.
rewrite the current goal using add_SNo_assoc x y z Hx Hy Hz (from left to right).
We will prove ((x + y) + z) + (- z + w) = x + y + w.
rewrite the current goal using add_SNo_assoc (x + y) z (- z + w) (SNo_add_SNo x y Hx Hy) Hz (SNo_add_SNo (- z) w (SNo_minus_SNo z Hz) Hw) (from right to left).
We will prove (x + y) + (z + - z + w) = x + y + w.
rewrite the current goal using add_SNo_minus_L2' z w Hz Hw (from left to right).
We will prove (x + y) + w = x + y + w.
Use symmetry.
An exact proof term for the current goal is add_SNo_assoc x y w Hx Hy Hw.
∎
Theorem. (add_SNo_minus_SNo_prop4)
∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + y + z) + (w + - z) = x + y + w
In Proofgold the corresponding term root is 930324... and proposition id is 4c3067...
Proof:
Let x, y, z and w be given.
Assume Hx Hy Hz Hw.
rewrite the current goal using add_SNo_com w (- z) Hw (SNo_minus_SNo z Hz) (from left to right).
We will prove (x + y + z) + (- z + w) = x + y + w.
An exact proof term for the current goal is add_SNo_minus_SNo_prop3 x y z w Hx Hy Hz Hw.
∎
Theorem. (add_SNo_minus_SNo_prop5)
∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + y + - z) + (z + w) = x + y + w
In Proofgold the corresponding term root is bdfd3f... and proposition id is eeb587...
Proof:
Let x, y, z and w be given.
Assume Hx Hy Hz Hw.
We will prove (x + y + - z) + (z + w) = x + y + w.
rewrite the current goal using minus_SNo_invol z Hz (from right to left) at position 2.
We will prove (x + y + - z) + (- - z + w) = x + y + w.
An exact proof term for the current goal is add_SNo_minus_SNo_prop3 x y (- z) w Hx Hy (SNo_minus_SNo z Hz) Hw.
∎
Theorem. (add_SNo_minus_Lt1)
∀x y z, SNo x → SNo y → SNo z → x + - y < z → x < z + y
In Proofgold the corresponding term root is 643876... and proposition id is 4033dc...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz H1.
Apply add_SNo_Lt1_cancel x (- y) (z + y) Hx (SNo_minus_SNo y Hy) (SNo_add_SNo z y Hz Hy) to the current goal.
We will prove x + - y < (z + y) + - y.
rewrite the current goal using add_SNo_assoc z y (- y) Hz Hy (SNo_minus_SNo y Hy) (from right to left).
rewrite the current goal using add_SNo_minus_SNo_rinv y Hy (from left to right).
rewrite the current goal using add_SNo_0R z Hz (from left to right).
An exact proof term for the current goal is H1.
∎
Theorem. (add_SNo_minus_Lt2)
∀x y z, SNo x → SNo y → SNo z → z < x + - y → z + y < x
In Proofgold the corresponding term root is 76c543... and proposition id is 362145...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz H1.
Apply add_SNo_Lt1_cancel (z + y) (- y) x (SNo_add_SNo z y Hz Hy) (SNo_minus_SNo y Hy) Hx to the current goal.
We will prove (z + y) + - y < x + - y.
rewrite the current goal using add_SNo_assoc z y (- y) Hz Hy (SNo_minus_SNo y Hy) (from right to left).
We will prove z + y + - y < x + - y.
rewrite the current goal using add_SNo_minus_SNo_rinv y Hy (from left to right).
rewrite the current goal using add_SNo_0R z Hz (from left to right).
An exact proof term for the current goal is H1.
∎
Theorem. (add_SNo_minus_Lt1b)
∀x y z, SNo x → SNo y → SNo z → x < z + y → x + - y < z
In Proofgold the corresponding term root is 5012b1... and proposition id is 0b5cca...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz H1.
Apply add_SNo_Lt1_cancel (x + - y) y z (SNo_add_SNo x (- y) Hx (SNo_minus_SNo y Hy)) Hy Hz to the current goal.
We will prove (x + - y) + y < z + y.
rewrite the current goal using add_SNo_assoc x (- y) y Hx (SNo_minus_SNo y Hy) Hy (from right to left).
rewrite the current goal using add_SNo_minus_SNo_linv y Hy (from left to right).
rewrite the current goal using add_SNo_0R x Hx (from left to right).
An exact proof term for the current goal is H1.
∎
Theorem. (add_SNo_minus_Lt2b)
∀x y z, SNo x → SNo y → SNo z → z + y < x → z < x + - y
In Proofgold the corresponding term root is 24d1a6... and proposition id is 684192...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz H1.
Apply add_SNo_Lt1_cancel z y (x + - y) Hz Hy (SNo_add_SNo x (- y) Hx (SNo_minus_SNo y Hy)) to the current goal.
We will prove z + y < (x + - y) + y.
rewrite the current goal using add_SNo_assoc x (- y) y Hx (SNo_minus_SNo y Hy) Hy (from right to left).
rewrite the current goal using add_SNo_minus_SNo_linv y Hy (from left to right).
rewrite the current goal using add_SNo_0R x Hx (from left to right).
An exact proof term for the current goal is H1.
∎
Theorem. (add_SNo_minus_Lt1b3)
∀x y z w, SNo x → SNo y → SNo z → SNo w → x + y < w + z → x + y + - z < w
In Proofgold the corresponding term root is 218e4f... and proposition id is 8ea4a7...
Proof:
Let x, y, z and w be given.
Assume Hx Hy Hz Hw H1.
We will prove x + y + - z < w.
rewrite the current goal using add_SNo_assoc x y (- z) Hx Hy (SNo_minus_SNo z Hz) (from left to right).
We will prove (x + y) + - z < w.
Apply add_SNo_minus_Lt1b (x + y) z w (SNo_add_SNo x y Hx Hy) Hz Hw to the current goal.
An exact proof term for the current goal is H1.
∎
Theorem. (add_SNo_minus_Lt2b3)
∀x y z w, SNo x → SNo y → SNo z → SNo w → w + z < x + y → w < x + y + - z
In Proofgold the corresponding term root is d9462b... and proposition id is 4bf575...
Proof:
Let x, y, z and w be given.
Assume Hx Hy Hz Hw H1.
We will prove w < x + y + - z.
rewrite the current goal using add_SNo_assoc x y (- z) Hx Hy (SNo_minus_SNo z Hz) (from left to right).
We will prove w < (x + y) + - z.
Apply add_SNo_minus_Lt2b (x + y) z w (SNo_add_SNo x y Hx Hy) Hz Hw to the current goal.
An exact proof term for the current goal is H1.
∎
Theorem. (add_SNo_minus_Lt_lem)
∀x y z u v w, SNo x → SNo y → SNo z → SNo u → SNo v → SNo w → x + y + w < u + v + z → x + y + - z < u + v + - w
In Proofgold the corresponding term root is da9f29... and proposition id is d29d2a...
Proof:
Let x, y, z, u, v and w be given.
Assume Hx Hy Hz Hu Hv Hw H1.
We prove the intermediate claim Lmz: SNo (- z).
An exact proof term for the current goal is SNo_minus_SNo z Hz.
We prove the intermediate claim Lmw: SNo (- w).
An exact proof term for the current goal is SNo_minus_SNo w Hw.
We prove the intermediate claim Lxy: SNo (x + y).
An exact proof term for the current goal is SNo_add_SNo x y Hx Hy.
We prove the intermediate claim Luv: SNo (u + v).
An exact proof term for the current goal is SNo_add_SNo u v Hu Hv.
rewrite the current goal using add_SNo_assoc x y (- z) Hx Hy Lmz (from left to right).
rewrite the current goal using add_SNo_assoc u v (- w) Hu Hv Lmw (from left to right).
We will prove (x + y) + - z < (u + v) + - w.
Apply add_SNo_minus_Lt2b (u + v) w ((x + y) + - z) Luv Hw (SNo_add_SNo (x + y) (- z) Lxy Lmz) to the current goal.
We will prove ((x + y) + - z) + w < u + v.
rewrite the current goal using add_SNo_assoc (x + y) (- z) w Lxy Lmz Hw (from right to left).
We will prove (x + y) + - z + w < u + v.
rewrite the current goal using add_SNo_com (- z) w Lmz Hw (from left to right).
We will prove (x + y) + w + - z < u + v.
rewrite the current goal using add_SNo_assoc (x + y) w (- z) Lxy Hw Lmz (from left to right).
We will prove ((x + y) + w) + - z < u + v.
Apply add_SNo_minus_Lt1b ((x + y) + w) z (u + v) (SNo_add_SNo (x + y) w Lxy Hw) Hz Luv to the current goal.
We will prove (x + y) + w < (u + v) + z.
rewrite the current goal using add_SNo_assoc x y w Hx Hy Hw (from right to left).
rewrite the current goal using add_SNo_assoc u v z Hu Hv Hz (from right to left).
An exact proof term for the current goal is H1.
∎
Theorem. (add_SNo_minus_Le2)
∀x y z, SNo x → SNo y → SNo z → z ≤ x + - y → z + y ≤ x
In Proofgold the corresponding term root is 85af84... and proposition id is 86b40b...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz H1.
Apply SNoLeE z (x + - y) Hz (SNo_add_SNo x (- y) Hx (SNo_minus_SNo y Hy)) H1 to the current goal.
Assume H2.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is add_SNo_minus_Lt2 x y z Hx Hy Hz H2.
Assume H2: z = x + - y.
We will prove z + y ≤ x.
rewrite the current goal using H2 (from left to right).
We will prove (x + - y) + y ≤ x.
rewrite the current goal using add_SNo_minus_R2' x y Hx Hy (from left to right).
Apply SNoLe_ref to the current goal.
∎
Theorem. (add_SNo_minus_Le2b)
∀x y z, SNo x → SNo y → SNo z → z + y ≤ x → z ≤ x + - y
In Proofgold the corresponding term root is 688ef9... and proposition id is d815dd...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz H1.
Apply SNoLeE (z + y) x (SNo_add_SNo z y Hz Hy) Hx H1 to the current goal.
Assume H2.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is add_SNo_minus_Lt2b x y z Hx Hy Hz H2.
Assume H2: z + y = x.
We will prove z ≤ x + - y.
rewrite the current goal using H2 (from right to left).
We will prove z ≤ (z + y) + - y.
rewrite the current goal using add_SNo_minus_R2 z y Hz Hy (from left to right).
Apply SNoLe_ref to the current goal.
∎
Theorem. (add_SNo_Lt_subprop2)
∀x y z w u v, SNo x → SNo y → SNo z → SNo w → SNo u → SNo v → x + u < z + v → y + v < w + u → x + y < z + w
In Proofgold the corresponding term root is 848909... and proposition id is 7f1b50...
Proof:
Let x, y, z, w, u and v be given.
Assume Hx Hy Hz Hw Hu Hv H1 H2.
Apply add_SNo_Lt1_cancel (x + y) (u + v) (z + w) (SNo_add_SNo x y Hx Hy) (SNo_add_SNo u v Hu Hv) (SNo_add_SNo z w Hz Hw) to the current goal.
We will prove (x + y) + (u + v) < (z + w) + (u + v).
rewrite the current goal using add_SNo_com_4_inner_mid x y u v Hx Hy Hu Hv (from left to right).
We will prove (x + u) + (y + v) < (z + w) + (u + v).
We prove the intermediate claim L1: (z + w) + (u + v) = (z + v) + (w + u).
rewrite the current goal using add_SNo_assoc z w (u + v) Hz Hw (SNo_add_SNo u v Hu Hv) (from right to left).
rewrite the current goal using add_SNo_assoc z v (w + u) Hz Hv (SNo_add_SNo w u Hw Hu) (from right to left).
We will prove z + (w + (u + v)) = z + (v + (w + u)).
Use f_equal.
We will prove w + u + v = v + w + u.
An exact proof term for the current goal is add_SNo_rotate_3_1 w u v Hw Hu Hv.
rewrite the current goal using L1 (from left to right).
We will prove (x + u) + (y + v) < (z + v) + (w + u).
An exact proof term for the current goal is add_SNo_Lt3 (x + u) (y + v) (z + v) (w + u) (SNo_add_SNo x u Hx Hu) (SNo_add_SNo y v Hy Hv) (SNo_add_SNo z v Hz Hv) (SNo_add_SNo w u Hw Hu) H1 H2.
∎
Theorem. (add_SNo_Lt_subprop3a)
∀x y z w u a, SNo x → SNo y → SNo z → SNo w → SNo u → SNo a → x + z < w + a → y + a < u → x + y + z < w + u
In Proofgold the corresponding term root is 43322d... and proposition id is cde0c9...
Proof:
Let x, y, z, w, u and a be given.
Assume Hx Hy Hz Hw Hu Ha H1 H2.
Apply SNoLt_tra (x + y + z) (y + w + a) (w + u) (SNo_add_SNo x (y + z) Hx (SNo_add_SNo y z Hy Hz)) (SNo_add_SNo y (w + a) Hy (SNo_add_SNo w a Hw Ha)) (SNo_add_SNo w u Hw Hu) to the current goal.
We will prove x + y + z < y + w + a.
rewrite the current goal using add_SNo_com_3_0_1 x y z Hx Hy Hz (from left to right).
We will prove y + x + z < y + w + a.
Apply add_SNo_Lt2 y (x + z) (w + a) Hy (SNo_add_SNo x z Hx Hz) (SNo_add_SNo w a Hw Ha) to the current goal.
An exact proof term for the current goal is H1.
We will prove y + w + a < w + u.
rewrite the current goal using add_SNo_rotate_3_1 w a y Hw Ha Hy (from right to left).
We will prove w + a + y < w + u.
Apply add_SNo_Lt2 w (a + y) u Hw (SNo_add_SNo a y Ha Hy) Hu to the current goal.
We will prove a + y < u.
rewrite the current goal using add_SNo_com a y Ha Hy (from left to right).
An exact proof term for the current goal is H2.
∎
Theorem. (add_SNo_Lt_subprop3b)
∀x y w u v a, SNo x → SNo y → SNo w → SNo u → SNo v → SNo a → x + a < w + v → y < a + u → x + y < w + u + v
In Proofgold the corresponding term root is 9d5c37... and proposition id is b197b1...
Proof:
Let x, y, w, u, v and a be given.
Assume Hx Hy Hw Hu Hv Ha H1 H2.
rewrite the current goal using add_SNo_com x y Hx Hy (from left to right).
We will prove y + x < w + u + v.
rewrite the current goal using add_SNo_rotate_3_1 u v w Hu Hv Hw (from right to left).
We will prove y + x < u + v + w.
rewrite the current goal using add_SNo_0R x Hx (from right to left).
We will prove y + x + 0 < u + v + w.
Apply add_SNo_Lt_subprop3a y x 0 u (v + w) a Hy Hx SNo_0 Hu (SNo_add_SNo v w Hv Hw) Ha to the current goal.
We will prove y + 0 < u + a.
rewrite the current goal using add_SNo_0R y Hy (from left to right).
rewrite the current goal using add_SNo_com u a Hu Ha (from left to right).
An exact proof term for the current goal is H2.
We will prove x + a < v + w.
rewrite the current goal using add_SNo_com v w Hv Hw (from left to right).
An exact proof term for the current goal is H1.
∎
Theorem. (add_SNo_Lt_subprop3c)
∀x y z w u a b c, SNo x → SNo y → SNo z → SNo w → SNo u → SNo a → SNo b → SNo c → x + a < b + c → y + c < u → b + z < w + a → x + y + z < w + u
In Proofgold the corresponding term root is 184614... and proposition id is f8cf2b...
Proof:
Let x, y, z, w, u, a, b and c be given.
Assume Hx Hy Hz Hw Hu Ha Hb Hc H1 H2 H3.
We prove the intermediate claim L1: x + z < c + w.
Apply add_SNo_Lt_subprop2 x z c w a b Hx Hz Hc Hw Ha Hb to the current goal.
We will prove x + a < c + b.
rewrite the current goal using add_SNo_com c b Hc Hb (from left to right).
An exact proof term for the current goal is H1.
We will prove z + b < w + a.
rewrite the current goal using add_SNo_com z b Hz Hb (from left to right).
An exact proof term for the current goal is H3.
We prove the intermediate claim Lxz: SNo (x + z).
An exact proof term for the current goal is SNo_add_SNo x z Hx Hz.
We prove the intermediate claim Lcw: SNo (c + w).
An exact proof term for the current goal is SNo_add_SNo c w Hc Hw.
Apply SNoLt_tra (x + y + z) (c + w + y) (w + u) to the current goal.
An exact proof term for the current goal is SNo_add_SNo x (y + z) Hx (SNo_add_SNo y z Hy Hz).
An exact proof term for the current goal is SNo_add_SNo c (w + y) Hc (SNo_add_SNo w y Hw Hy).
An exact proof term for the current goal is SNo_add_SNo w u Hw Hu.
We will prove x + y + z < c + w + y.
rewrite the current goal using add_SNo_com y z Hy Hz (from left to right).
We will prove x + z + y < c + w + y.
rewrite the current goal using add_SNo_assoc x z y Hx Hz Hy (from left to right).
rewrite the current goal using add_SNo_assoc c w y Hc Hw Hy (from left to right).
An exact proof term for the current goal is add_SNo_Lt1 (x + z) y (c + w) Lxz Hy Lcw L1.
We will prove c + w + y < w + u.
rewrite the current goal using add_SNo_rotate_3_1 w y c Hw Hy Hc (from right to left).
We will prove w + y + c < w + u.
Apply add_SNo_Lt2 w (y + c) u Hw (SNo_add_SNo y c Hy Hc) Hu to the current goal.
We will prove y + c < u.
An exact proof term for the current goal is H2.
∎
Theorem. (add_SNo_Lt_subprop3d)
∀x y w u v a b c, SNo x → SNo y → SNo w → SNo u → SNo v → SNo a → SNo b → SNo c → x + a < b + v → y < c + u → b + c < w + a → x + y < w + u + v
In Proofgold the corresponding term root is a447c6... and proposition id is a1520a...
Proof:
Let x, y, w, u, v, a, b and c be given.
Assume Hx Hy Hw Hu Hv Ha Hb Hc H1 H2 H3.
We prove the intermediate claim L1: b + y < w + u + a.
An exact proof term for the current goal is add_SNo_Lt_subprop3b b y w u a c Hb Hy Hw Hu Ha Hc H3 H2.
We prove the intermediate claim Lxy: SNo (x + y).
An exact proof term for the current goal is SNo_add_SNo x y Hx Hy.
We prove the intermediate claim Lwuv: SNo (w + u + v).
An exact proof term for the current goal is SNo_add_SNo w (u + v) Hw (SNo_add_SNo u v Hu Hv).
We prove the intermediate claim Lwua: SNo (w + u + a).
An exact proof term for the current goal is SNo_add_SNo w (u + a) Hw (SNo_add_SNo u a Hu Ha).
We prove the intermediate claim Lby: SNo (b + y).
An exact proof term for the current goal is SNo_add_SNo b y Hb Hy.
Apply add_SNo_Lt1_cancel (x + y) b (w + u + v) Lxy Hb Lwuv to the current goal.
We will prove (x + y) + b < (w + u + v) + b.
Apply SNoLt_tra ((x + y) + b) (x + w + u + a) ((w + u + v) + b) (SNo_add_SNo (x + y) b Lxy Hb) (SNo_add_SNo x (w + u + a) Hx Lwua) (SNo_add_SNo (w + u + v) b Lwuv Hb) to the current goal.
We will prove (x + y) + b < x + w + u + a.
rewrite the current goal using add_SNo_assoc x y b Hx Hy Hb (from right to left).
We will prove x + y + b < x + w + u + a.
rewrite the current goal using add_SNo_com y b Hy Hb (from left to right).
We will prove x + b + y < x + w + u + a.
Apply add_SNo_Lt2 x (b + y) (w + u + a) Hx Lby Lwua to the current goal.
We will prove b + y < w + u + a.
An exact proof term for the current goal is L1.
We will prove x + w + u + a < (w + u + v) + b.
We prove the intermediate claim L2: x + w + u + a = (w + u) + (x + a).
Use transitivity with (x + w + u) + a, (w + u + x) + a, and w + u + x + a.
An exact proof term for the current goal is add_SNo_assoc_4 x w u a Hx Hw Hu Ha.
Use f_equal.
Use symmetry.
An exact proof term for the current goal is add_SNo_rotate_3_1 w u x Hw Hu Hx.
Use symmetry.
An exact proof term for the current goal is add_SNo_assoc_4 w u x a Hw Hu Hx Ha.
We will prove w + u + x + a = (w + u) + (x + a).
An exact proof term for the current goal is add_SNo_assoc w u (x + a) Hw Hu (SNo_add_SNo x a Hx Ha).
We prove the intermediate claim L3: (w + u + v) + b = (w + u) + b + v.
Use transitivity with ((w + u) + v) + b, and (w + u) + (v + b).
Use f_equal.
An exact proof term for the current goal is add_SNo_assoc w u v Hw Hu Hv.
Use symmetry.
An exact proof term for the current goal is add_SNo_assoc (w + u) v b (SNo_add_SNo w u Hw Hu) Hv Hb.
Use f_equal.
An exact proof term for the current goal is add_SNo_com v b Hv Hb.
rewrite the current goal using L2 (from left to right).
rewrite the current goal using L3 (from left to right).
We will prove (w + u) + (x + a) < (w + u) + (b + v).
Apply add_SNo_Lt2 (w + u) (x + a) (b + v) (SNo_add_SNo w u Hw Hu) (SNo_add_SNo x a Hx Ha) (SNo_add_SNo b v Hb Hv) to the current goal.
An exact proof term for the current goal is H1.
∎
Theorem. (ordinal_ordsucc_SNo_eq)
∀alpha, ordinal alpha → ordsucc alpha = 1 + alpha
In Proofgold the corresponding term root is f0596d... and proposition id is 36bf6d...
Proof:
Let alpha be given.
Assume Ha.
rewrite the current goal using add_SNo_0L alpha (ordinal_SNo alpha Ha) (from right to left) at position 1.
We will prove ordsucc (0 + alpha) = 1 + alpha.
Use symmetry.
An exact proof term for the current goal is add_SNo_ordinal_SL 0 ordinal_Empty alpha Ha.
∎
Theorem. (add_SNo_3a_2b)
∀x y z w u, SNo x → SNo y → SNo z → SNo w → SNo u → (x + y + z) + (w + u) = (u + y + z) + (w + x)
In Proofgold the corresponding term root is d5c6f9... and proposition id is f24a27...
Proof:
Let x, y, z, w and u be given.
Assume Hx Hy Hz Hw Hu.
rewrite the current goal using add_SNo_com (x + y + z) (w + u) (SNo_add_SNo_3 x y z Hx Hy Hz) (SNo_add_SNo w u Hw Hu) (from left to right).
We will prove (w + u) + (x + y + z) = (u + y + z) + (w + x).
rewrite the current goal using add_SNo_com_4_inner_mid w u x (y + z) Hw Hu Hx (SNo_add_SNo y z Hy Hz) (from left to right).
We will prove (w + x) + (u + y + z) = (u + y + z) + (w + x).
An exact proof term for the current goal is add_SNo_com (w + x) (u + y + z) (SNo_add_SNo w x Hw Hx) (SNo_add_SNo_3 u y z Hu Hy Hz).
∎
Theorem. (add_SNo_1_ordsucc)
∀n ∈ ω, n + 1 = ordsucc n
In Proofgold the corresponding term root is ec6cad... and proposition id is 85f670...
Proof:
Let n be given.
Assume Hn.
rewrite the current goal using add_nat_add_SNo n Hn 1 (nat_p_omega 1 nat_1) (from right to left).
We will prove add_nat n 1 = ordsucc n.
rewrite the current goal using add_nat_SR n 0 nat_0 (from left to right).
We will prove ordsucc (add_nat n 0) = ordsucc n.
rewrite the current goal using add_nat_0R (from left to right).
Use reflexivity.
∎
Theorem. (add_SNo_eps_Lt)
∀x, SNo x → ∀n ∈ ω, x < x + eps_ n
In Proofgold the corresponding term root is dfe40b... and proposition id is d492a4...
Proof:
Let x be given.
Assume Hx.
Let n be given.
Assume Hn.
rewrite the current goal using add_SNo_0R x Hx (from right to left) at position 1.
We will prove x + 0 < x + eps_ n.
Apply add_SNo_Lt2 x 0 (eps_ n) Hx SNo_0 (SNo_eps_ n Hn) to the current goal.
An exact proof term for the current goal is SNo_eps_pos n Hn.
∎
Theorem. (add_SNo_eps_Lt')
∀x y, SNo x → SNo y → ∀n ∈ ω, x < y → x < y + eps_ n
In Proofgold the corresponding term root is 281ca0... and proposition id is 943874...
Proof:
Let x and y be given.
Assume Hx Hy.
Let n be given.
Assume Hn.
Assume Hxy.
Apply SNoLt_tra x y (y + eps_ n) Hx Hy (SNo_add_SNo y (eps_ n) Hy (SNo_eps_ n Hn)) Hxy to the current goal.
We will prove y < y + eps_ n.
An exact proof term for the current goal is add_SNo_eps_Lt y Hy n Hn.
∎
Theorem. (SNoLt_minus_pos)
∀x y, SNo x → SNo y → x < y → 0 < y + - x
In Proofgold the corresponding term root is fff649... and proposition id is 2c799f...
Proof:
Let x and y be given.
Assume Hx Hy Hxy.
Apply add_SNo_minus_Lt2b y x 0 Hy Hx SNo_0 to the current goal.
We will prove 0 + x < y.
rewrite the current goal using add_SNo_0L x Hx (from left to right).
An exact proof term for the current goal is Hxy.
∎
Theorem. (add_SNo_omega_In_cases)
∀m, ∀n ∈ ω, ∀k, nat_p k → m ∈ n + k → m ∈ n ∨ m + - n ∈ k
In Proofgold the corresponding term root is 3eee93... and proposition id is 584cf6...
Proof:
Let m and n be given.
Assume Hn.
We prove the intermediate claim Ln: SNo n.
Apply omega_SNo to the current goal.
An exact proof term for the current goal is Hn.
Apply nat_ind to the current goal.
We will prove m ∈ n + 0 → m ∈ n ∨ m + - n ∈ 0.
rewrite the current goal using add_SNo_0R n Ln (from left to right).
Assume H1.
Apply orIL to the current goal.
An exact proof term for the current goal is H1.
Let k be given.
Assume Hk.
Assume IHk: m ∈ n + k → m ∈ n ∨ m + - n ∈ k.
rewrite the current goal using add_SNo_1_ordsucc k (nat_p_omega k Hk) (from right to left) at position 1.
rewrite the current goal using add_SNo_assoc n k 1 Ln (nat_p_SNo k Hk) SNo_1 (from left to right).
rewrite the current goal using add_SNo_1_ordsucc (n + k) (add_SNo_In_omega n Hn k (nat_p_omega k Hk)) (from left to right).
Assume H1: m ∈ ordsucc (n + k).
Apply ordsuccE (n + k) m H1 to the current goal.
Assume H2: m ∈ n + k.
Apply IHk H2 to the current goal.
Assume H3: m ∈ n.
Apply orIL to the current goal.
An exact proof term for the current goal is H3.
Assume H3: m + - n ∈ k.
Apply orIR to the current goal.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is H3.
Assume H2: m = n + k.
Apply orIR to the current goal.
rewrite the current goal using H2 (from left to right).
We will prove (n + k) + - n ∈ ordsucc k.
rewrite the current goal using add_SNo_com (n + k) (- n) (SNo_add_SNo n k Ln (nat_p_SNo k Hk)) (SNo_minus_SNo n Ln) (from left to right).
rewrite the current goal using add_SNo_minus_L2 n k Ln (nat_p_SNo k Hk) (from left to right).
Apply ordsuccI2 to the current goal.
∎
Theorem. (add_SNo_Lt4)
∀x y z w u v, SNo x → SNo y → SNo z → SNo w → SNo u → SNo v → x < w → y < u → z < v → x + y + z < w + u + v
In Proofgold the corresponding term root is 7e45aa... and proposition id is c85ce6...
Proof:
Let x, y, z, w, u and v be given.
Assume Hx Hy Hz Hw Hu Hv Hxw Hyu Hzv.
We will prove x + y + z < w + u + v.
Apply add_SNo_Lt3 x (y + z) w (u + v) Hx (SNo_add_SNo y z Hy Hz) Hw (SNo_add_SNo u v Hu Hv) Hxw to the current goal.
We will prove y + z < u + v.
An exact proof term for the current goal is add_SNo_Lt3 y z u v Hy Hz Hu Hv Hyu Hzv.
∎
Theorem. (add_SNo_3_3_3_Lt1)
∀x y z w u, SNo x → SNo y → SNo z → SNo w → SNo u → x + y < z + w → x + y + u < z + w + u
In Proofgold the corresponding term root is 5889f8... and proposition id is fa11ed...
Proof:
Let x, y, z, w and u be given.
Assume Hx Hy Hz Hw Hu H1.
rewrite the current goal using add_SNo_assoc x y u Hx Hy Hu (from left to right).
rewrite the current goal using add_SNo_assoc z w u Hz Hw Hu (from left to right).
We will prove (x + y) + u < (z + w) + u.
An exact proof term for the current goal is add_SNo_Lt1 (x + y) u (z + w) (SNo_add_SNo x y Hx Hy) Hu (SNo_add_SNo z w Hz Hw) H1.
∎
Theorem. (add_SNo_3_2_3_Lt1)
∀x y z w u, SNo x → SNo y → SNo z → SNo w → SNo u → y + x < z + w → x + u + y < z + w + u
In Proofgold the corresponding term root is c05b73... and proposition id is e4013b...
Proof:
Let x, y, z, w and u be given.
Assume Hx Hy Hz Hw Hu H1.
rewrite the current goal using add_SNo_rotate_3_1 x u y Hx Hu Hy (from left to right).
We will prove y + x + u < z + w + u.
An exact proof term for the current goal is add_SNo_3_3_3_Lt1 y x z w u Hy Hx Hz Hw Hu H1.
∎
Theorem. (add_SNoCutP_lem)
∀Lx Rx Ly Ry x y, SNoCutP Lx Rx → SNoCutP Ly Ry → x = SNoCut Lx Rx → y = SNoCut Ly Ry → SNoCutP ({w + y|w ∈ Lx} ∪ {x + w|w ∈ Ly}) ({z + y|z ∈ Rx} ∪ {x + z|z ∈ Ry}) ∧ x + y = SNoCut ({w + y|w ∈ Lx} ∪ {x + w|w ∈ Ly}) ({z + y|z ∈ Rx} ∪ {x + z|z ∈ Ry})
In Proofgold the corresponding term root is 956a83... and proposition id is 171607...
Proof:
Let Lx, Rx, Ly, Ry, x and y be given.
Assume HLRx HLRy Hxe Hye.
Apply HLRx to the current goal.
Assume H.
Apply H to the current goal.
Assume HLRx1: ∀w ∈ Lx, SNo w.
Assume HLRx2: ∀z ∈ Rx, SNo z.
Assume HLRx3: ∀w ∈ Lx, ∀z ∈ Rx, w < z.
Apply HLRy to the current goal.
Assume H.
Apply H to the current goal.
Assume HLRy1: ∀w ∈ Ly, SNo w.
Assume HLRy2: ∀z ∈ Ry, SNo z.
Assume HLRy3: ∀w ∈ Ly, ∀z ∈ Ry, w < z.
Set Lx' to be the term {w + y|w ∈ Lx}.
Set Ly' to be the term {x + w|w ∈ Ly}.
Set Rx' to be the term {z + y|z ∈ Rx}.
Set Ry' to be the term {x + z|z ∈ Ry}.
Apply SNoCutP_SNoCut_impred Lx Rx HLRx to the current goal.
rewrite the current goal using Hxe (from right to left).
Assume Hx1: SNo x.
Assume Hx2: SNoLev x ∈ ordsucc ((⋃w ∈ Lxordsucc (SNoLev w)) ∪ (⋃z ∈ Rxordsucc (SNoLev z))).
Assume Hx3: ∀w ∈ Lx, w < x.
Assume Hx4: ∀z ∈ Rx, x < z.
Assume Hx5: (∀u, SNo u → (∀w ∈ Lx, w < u) → (∀z ∈ Rx, u < z) → SNoLev x ⊆ SNoLev u ∧ SNoEq_ (SNoLev x) x u).
Apply SNoCutP_SNoCut_impred Ly Ry HLRy to the current goal.
rewrite the current goal using Hye (from right to left).
Assume Hy1: SNo y.
Assume Hy2: SNoLev y ∈ ordsucc ((⋃w ∈ Lyordsucc (SNoLev w)) ∪ (⋃z ∈ Ryordsucc (SNoLev z))).
Assume Hy3: ∀w ∈ Ly, w < y.
Assume Hy4: ∀z ∈ Ry, y < z.
Assume Hy5: (∀u, SNo u → (∀w ∈ Ly, w < u) → (∀z ∈ Ry, u < z) → SNoLev y ⊆ SNoLev u ∧ SNoEq_ (SNoLev y) y u).
We prove the intermediate claim L1: SNoCutP (Lx' ∪ Ly') (Rx' ∪ Ry').
We will prove (∀w ∈ Lx' ∪ Ly', SNo w) ∧ (∀z ∈ Rx' ∪ Ry', SNo z) ∧ (∀w ∈ Lx' ∪ Ly', ∀z ∈ Rx' ∪ Ry', w < z).
Apply and3I to the current goal.
Let w be given.
Apply binunionE' to the current goal.
Assume Hw: w ∈ Lx'.
Apply ReplE_impred Lx (λw ⇒ w + y) w Hw to the current goal.
Let w' be given.
Assume Hw': w' ∈ Lx.
Assume Hwe: w = w' + y.
rewrite the current goal using Hwe (from left to right).
An exact proof term for the current goal is SNo_add_SNo w' y (HLRx1 w' Hw') Hy1.
Assume Hw: w ∈ Ly'.
Apply ReplE_impred Ly (λw ⇒ x + w) w Hw to the current goal.
Let w' be given.
Assume Hw': w' ∈ Ly.
Assume Hwe: w = x + w'.
rewrite the current goal using Hwe (from left to right).
An exact proof term for the current goal is SNo_add_SNo x w' Hx1 (HLRy1 w' Hw').
Let z be given.
Apply binunionE' to the current goal.
Assume Hz: z ∈ Rx'.
Apply ReplE_impred Rx (λz ⇒ z + y) z Hz to the current goal.
Let z' be given.
Assume Hz': z' ∈ Rx.
Assume Hze: z = z' + y.
rewrite the current goal using Hze (from left to right).
An exact proof term for the current goal is SNo_add_SNo z' y (HLRx2 z' Hz') Hy1.
Assume Hz: z ∈ Ry'.
Apply ReplE_impred Ry (λz ⇒ x + z) z Hz to the current goal.
Let z' be given.
Assume Hz': z' ∈ Ry.
Assume Hze: z = x + z'.
rewrite the current goal using Hze (from left to right).
An exact proof term for the current goal is SNo_add_SNo x z' Hx1 (HLRy2 z' Hz').
Let w be given.
Apply binunionE' to the current goal.
Assume Hw: w ∈ Lx'.
Apply ReplE_impred Lx (λw ⇒ w + y) w Hw to the current goal.
Let w' be given.
Assume Hw': w' ∈ Lx.
We prove the intermediate claim Lw': SNo w'.
An exact proof term for the current goal is HLRx1 w' Hw'.
Assume Hwe: w = w' + y.
rewrite the current goal using Hwe (from left to right).
Let z be given.
Apply binunionE' to the current goal.
Assume Hz: z ∈ Rx'.
Apply ReplE_impred Rx (λz ⇒ z + y) z Hz to the current goal.
Let z' be given.
Assume Hz': z' ∈ Rx.
Assume Hze: z = z' + y.
We prove the intermediate claim Lz': SNo z'.
An exact proof term for the current goal is HLRx2 z' Hz'.
rewrite the current goal using Hze (from left to right).
We will prove w' + y < z' + y.
Apply add_SNo_Lt1 w' y z' Lw' Hy1 Lz' to the current goal.
We will prove w' < z'.
An exact proof term for the current goal is SNoLt_tra w' x z' Lw' Hx1 Lz' (Hx3 w' Hw') (Hx4 z' Hz').
Assume Hz: z ∈ Ry'.
Apply ReplE_impred Ry (λz ⇒ x + z) z Hz to the current goal.
Let z' be given.
Assume Hz': z' ∈ Ry.
Assume Hze: z = x + z'.
We prove the intermediate claim Lz': SNo z'.
An exact proof term for the current goal is HLRy2 z' Hz'.
rewrite the current goal using Hze (from left to right).
We will prove w' + y < x + z'.
Apply add_SNo_Lt3 w' y x z' Lw' Hy1 Hx1 Lz' to the current goal.
We will prove w' < x.
An exact proof term for the current goal is Hx3 w' Hw'.
We will prove y < z'.
An exact proof term for the current goal is Hy4 z' Hz'.
Assume Hw: w ∈ Ly'.
Apply ReplE_impred Ly (λw ⇒ x + w) w Hw to the current goal.
Let w' be given.
Assume Hw': w' ∈ Ly.
Assume Hwe: w = x + w'.
We prove the intermediate claim Lw': SNo w'.
An exact proof term for the current goal is HLRy1 w' Hw'.
rewrite the current goal using Hwe (from left to right).
Let z be given.
Apply binunionE' to the current goal.
Assume Hz: z ∈ Rx'.
Apply ReplE_impred Rx (λz ⇒ z + y) z Hz to the current goal.
Let z' be given.
Assume Hz': z' ∈ Rx.
Assume Hze: z = z' + y.
We prove the intermediate claim Lz': SNo z'.
An exact proof term for the current goal is HLRx2 z' Hz'.
rewrite the current goal using Hze (from left to right).
We will prove x + w' < z' + y.
Apply add_SNo_Lt3 x w' z' y Hx1 Lw' Lz' Hy1 to the current goal.
We will prove x < z'.
An exact proof term for the current goal is Hx4 z' Hz'.
We will prove w' < y.
An exact proof term for the current goal is Hy3 w' Hw'.
Assume Hz: z ∈ Ry'.
Apply ReplE_impred Ry (λz ⇒ x + z) z Hz to the current goal.
Let z' be given.
Assume Hz': z' ∈ Ry.
Assume Hze: z = x + z'.
We prove the intermediate claim Lz': SNo z'.
An exact proof term for the current goal is HLRy2 z' Hz'.
rewrite the current goal using Hze (from left to right).
We will prove x + w' < x + z'.
Apply add_SNo_Lt2 x w' z' Hx1 Lw' Lz' to the current goal.
We will prove w' < z'.
An exact proof term for the current goal is SNoLt_tra w' y z' Lw' Hy1 Lz' (Hy3 w' Hw') (Hy4 z' Hz').
Apply andI (SNoCutP (Lx' ∪ Ly') (Rx' ∪ Ry')) (x + y = SNoCut (Lx' ∪ Ly') (Rx' ∪ Ry')) L1 to the current goal.
We will prove x + y = SNoCut (Lx' ∪ Ly') (Rx' ∪ Ry').
rewrite the current goal using add_SNo_eq x Hx1 y Hy1 (from left to right).
We will prove SNoCut ({w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}) ({z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y}) = SNoCut (Lx' ∪ Ly') (Rx' ∪ Ry').
Set v to be the term SNoCut (Lx' ∪ Ly') (Rx' ∪ Ry').
Apply SNoCutP_SNoCut_impred (Lx' ∪ Ly') (Rx' ∪ Ry') L1 to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ ordsucc ((⋃w ∈ Lx' ∪ Ly'ordsucc (SNoLev w)) ∪ (⋃z ∈ Rx' ∪ Ry'ordsucc (SNoLev z))).
Assume Hv3: ∀w ∈ Lx' ∪ Ly', w < v.
Assume Hv4: ∀z ∈ Rx' ∪ Ry', v < z.
Assume Hv5: ∀u, SNo u → (∀w ∈ Lx' ∪ Ly', w < u) → (∀z ∈ Rx' ∪ Ry', u < z) → SNoLev v ⊆ SNoLev u ∧ SNoEq_ (SNoLev v) v u.
Apply SNoCut_ext ({w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}) ({z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y}) (Lx' ∪ Ly') (Rx' ∪ Ry') to the current goal.
An exact proof term for the current goal is add_SNo_SNoCutP x y Hx1 Hy1.
An exact proof term for the current goal is L1.
We will prove ∀w ∈ {w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}, w < v.
Let w be given.
Apply binunionE' to the current goal.
Assume Hw.
Apply ReplE_impred (SNoL x) (λw ⇒ w + y) w Hw to the current goal.
Let w' be given.
Assume Hw': w' ∈ SNoL x.
Assume Hwe: w = w' + y.
Apply SNoL_E x Hx1 w' Hw' to the current goal.
Assume Hw'1: SNo w'.
Assume Hw'2: SNoLev w' ∈ SNoLev x.
Assume Hw'3: w' < x.
We prove the intermediate claim L2: ∃w'' ∈ Lx, w' ≤ w''.
Apply dneg to the current goal.
Assume HC.
We prove the intermediate claim L2a: SNoLev x ⊆ SNoLev w' ∧ SNoEq_ (SNoLev x) x w'.
Apply Hx5 w' Hw'1 to the current goal.
We will prove ∀w'' ∈ Lx, w'' < w'.
Let w'' be given.
Assume Hw''1.
Apply SNoLtLe_or w'' w' (HLRx1 w'' Hw''1) Hw'1 to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume Hw''2: w' ≤ w''.
We will prove False.
Apply HC to the current goal.
We use w'' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw''1.
An exact proof term for the current goal is Hw''2.
We will prove ∀z ∈ Rx, w' < z.
Let z be given.
Assume Hz.
Apply SNoLt_tra w' x z Hw'1 Hx1 (HLRx2 z Hz) to the current goal.
We will prove w' < x.
An exact proof term for the current goal is Hw'3.
We will prove x < z.
An exact proof term for the current goal is Hx4 z Hz.
Apply L2a to the current goal.
Assume Hxw': SNoLev x ⊆ SNoLev w'.
Assume _.
Apply In_irref (SNoLev w') to the current goal.
We will prove SNoLev w' ∈ SNoLev w'.
Apply Hxw' to the current goal.
An exact proof term for the current goal is Hw'2.
Apply L2 to the current goal.
Let w'' be given.
Assume H.
Apply H to the current goal.
Assume Hw''1: w'' ∈ Lx.
Assume Hw''2: w' ≤ w''.
rewrite the current goal using Hwe (from left to right).
We will prove w' + y < v.
Apply SNoLeLt_tra (w' + y) (w'' + y) v (SNo_add_SNo w' y Hw'1 Hy1) (SNo_add_SNo w'' y (HLRx1 w'' Hw''1) Hy1) Hv1 to the current goal.
We will prove w' + y ≤ w'' + y.
Apply add_SNo_Le1 w' y w'' Hw'1 Hy1 (HLRx1 w'' Hw''1) to the current goal.
We will prove w' ≤ w''.
An exact proof term for the current goal is Hw''2.
We will prove w'' + y < v.
Apply Hv3 to the current goal.
We will prove w'' + y ∈ Lx' ∪ Ly'.
Apply binunionI1 to the current goal.
We will prove w'' + y ∈ Lx'.
An exact proof term for the current goal is ReplI Lx (λw ⇒ w + y) w'' Hw''1.
Assume Hw.
Apply ReplE_impred (SNoL y) (λw ⇒ x + w) w Hw to the current goal.
Let w' be given.
Assume Hw': w' ∈ SNoL y.
Assume Hwe: w = x + w'.
Apply SNoL_E y Hy1 w' Hw' to the current goal.
Assume Hw'1: SNo w'.
Assume Hw'2: SNoLev w' ∈ SNoLev y.
Assume Hw'3: w' < y.
We prove the intermediate claim L3: ∃w'' ∈ Ly, w' ≤ w''.
Apply dneg to the current goal.
Assume HC.
We prove the intermediate claim L3a: SNoLev y ⊆ SNoLev w' ∧ SNoEq_ (SNoLev y) y w'.
Apply Hy5 w' Hw'1 to the current goal.
We will prove ∀w'' ∈ Ly, w'' < w'.
Let w'' be given.
Assume Hw''1.
Apply SNoLtLe_or w'' w' (HLRy1 w'' Hw''1) Hw'1 to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume Hw''2: w' ≤ w''.
We will prove False.
Apply HC to the current goal.
We use w'' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw''1.
An exact proof term for the current goal is Hw''2.
We will prove ∀z ∈ Ry, w' < z.
Let z be given.
Assume Hz.
Apply SNoLt_tra w' y z Hw'1 Hy1 (HLRy2 z Hz) to the current goal.
We will prove w' < y.
An exact proof term for the current goal is Hw'3.
We will prove y < z.
An exact proof term for the current goal is Hy4 z Hz.
Apply L3a to the current goal.
Assume Hyw': SNoLev y ⊆ SNoLev w'.
Assume _.
Apply In_irref (SNoLev w') to the current goal.
We will prove SNoLev w' ∈ SNoLev w'.
Apply Hyw' to the current goal.
An exact proof term for the current goal is Hw'2.
Apply L3 to the current goal.
Let w'' be given.
Assume H.
Apply H to the current goal.
Assume Hw''1: w'' ∈ Ly.
Assume Hw''2: w' ≤ w''.
rewrite the current goal using Hwe (from left to right).
We will prove x + w' < v.
Apply SNoLeLt_tra (x + w') (x + w'') v (SNo_add_SNo x w' Hx1 Hw'1) (SNo_add_SNo x w'' Hx1 (HLRy1 w'' Hw''1)) Hv1 to the current goal.
We will prove x + w' ≤ x + w''.
Apply add_SNo_Le2 x w' w'' Hx1 Hw'1 (HLRy1 w'' Hw''1) to the current goal.
We will prove w' ≤ w''.
An exact proof term for the current goal is Hw''2.
We will prove x + w'' < v.
Apply Hv3 to the current goal.
We will prove x + w'' ∈ Lx' ∪ Ly'.
Apply binunionI2 to the current goal.
We will prove x + w'' ∈ Ly'.
An exact proof term for the current goal is ReplI Ly (λw ⇒ x + w) w'' Hw''1.
We will prove ∀z ∈ {z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y}, v < z.
Let z be given.
Apply binunionE' to the current goal.
Assume Hz.
Apply ReplE_impred (SNoR x) (λz ⇒ z + y) z Hz to the current goal.
Let z' be given.
Assume Hz': z' ∈ SNoR x.
Assume Hze: z = z' + y.
Apply SNoR_E x Hx1 z' Hz' to the current goal.
Assume Hz'1: SNo z'.
Assume Hz'2: SNoLev z' ∈ SNoLev x.
Assume Hz'3: x < z'.
We prove the intermediate claim L4: ∃z'' ∈ Rx, z'' ≤ z'.
Apply dneg to the current goal.
Assume HC.
We prove the intermediate claim L4a: SNoLev x ⊆ SNoLev z' ∧ SNoEq_ (SNoLev x) x z'.
Apply Hx5 z' Hz'1 to the current goal.
We will prove ∀w ∈ Lx, w < z'.
Let w be given.
Assume Hw.
Apply SNoLt_tra w x z' (HLRx1 w Hw) Hx1 Hz'1 to the current goal.
We will prove w < x.
An exact proof term for the current goal is Hx3 w Hw.
We will prove x < z'.
An exact proof term for the current goal is Hz'3.
We will prove ∀z'' ∈ Rx, z' < z''.
Let z'' be given.
Assume Hz''1.
Apply SNoLtLe_or z' z'' Hz'1 (HLRx2 z'' Hz''1) to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume Hz''2: z'' ≤ z'.
We will prove False.
Apply HC to the current goal.
We use z'' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz''1.
An exact proof term for the current goal is Hz''2.
Apply L4a to the current goal.
Assume Hxz': SNoLev x ⊆ SNoLev z'.
Assume _.
Apply In_irref (SNoLev z') to the current goal.
We will prove SNoLev z' ∈ SNoLev z'.
Apply Hxz' to the current goal.
An exact proof term for the current goal is Hz'2.
Apply L4 to the current goal.
Let z'' be given.
Assume H.
Apply H to the current goal.
Assume Hz''1: z'' ∈ Rx.
Assume Hz''2: z'' ≤ z'.
rewrite the current goal using Hze (from left to right).
We will prove v < z' + y.
Apply SNoLtLe_tra v (z'' + y) (z' + y) Hv1 (SNo_add_SNo z'' y (HLRx2 z'' Hz''1) Hy1) (SNo_add_SNo z' y Hz'1 Hy1) to the current goal.
We will prove v < z'' + y.
Apply Hv4 to the current goal.
We will prove z'' + y ∈ Rx' ∪ Ry'.
Apply binunionI1 to the current goal.
We will prove z'' + y ∈ Rx'.
An exact proof term for the current goal is ReplI Rx (λz ⇒ z + y) z'' Hz''1.
We will prove z'' + y ≤ z' + y.
Apply add_SNo_Le1 z'' y z' (HLRx2 z'' Hz''1) Hy1 Hz'1 to the current goal.
We will prove z'' ≤ z'.
An exact proof term for the current goal is Hz''2.
Assume Hz.
Apply ReplE_impred (SNoR y) (λz ⇒ x + z) z Hz to the current goal.
Let z' be given.
Assume Hz': z' ∈ SNoR y.
Assume Hze: z = x + z'.
Apply SNoR_E y Hy1 z' Hz' to the current goal.
Assume Hz'1: SNo z'.
Assume Hz'2: SNoLev z' ∈ SNoLev y.
Assume Hz'3: y < z'.
We prove the intermediate claim L5: ∃z'' ∈ Ry, z'' ≤ z'.
Apply dneg to the current goal.
Assume HC.
We prove the intermediate claim L5a: SNoLev y ⊆ SNoLev z' ∧ SNoEq_ (SNoLev y) y z'.
Apply Hy5 z' Hz'1 to the current goal.
We will prove ∀w ∈ Ly, w < z'.
Let w be given.
Assume Hw.
Apply SNoLt_tra w y z' (HLRy1 w Hw) Hy1 Hz'1 to the current goal.
We will prove w < y.
An exact proof term for the current goal is Hy3 w Hw.
We will prove y < z'.
An exact proof term for the current goal is Hz'3.
We will prove ∀z'' ∈ Ry, z' < z''.
Let z'' be given.
Assume Hz''1.
Apply SNoLtLe_or z' z'' Hz'1 (HLRy2 z'' Hz''1) to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume Hz''2: z'' ≤ z'.
We will prove False.
Apply HC to the current goal.
We use z'' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz''1.
An exact proof term for the current goal is Hz''2.
Apply L5a to the current goal.
Assume Hyz': SNoLev y ⊆ SNoLev z'.
Assume _.
Apply In_irref (SNoLev z') to the current goal.
We will prove SNoLev z' ∈ SNoLev z'.
Apply Hyz' to the current goal.
An exact proof term for the current goal is Hz'2.
Apply L5 to the current goal.
Let z'' be given.
Assume H.
Apply H to the current goal.
Assume Hz''1: z'' ∈ Ry.
Assume Hz''2: z'' ≤ z'.
rewrite the current goal using Hze (from left to right).
We will prove v < x + z'.
Apply SNoLtLe_tra v (x + z'') (x + z') Hv1 (SNo_add_SNo x z'' Hx1 (HLRy2 z'' Hz''1)) (SNo_add_SNo x z' Hx1 Hz'1) to the current goal.
We will prove v < x + z''.
Apply Hv4 to the current goal.
We will prove x + z'' ∈ Rx' ∪ Ry'.
Apply binunionI2 to the current goal.
We will prove x + z'' ∈ Ry'.
An exact proof term for the current goal is ReplI Ry (λz ⇒ x + z) z'' Hz''1.
We will prove x + z'' ≤ x + z'.
Apply add_SNo_Le2 x z'' z' Hx1 (HLRy2 z'' Hz''1) Hz'1 to the current goal.
We will prove z'' ≤ z'.
An exact proof term for the current goal is Hz''2.
rewrite the current goal using add_SNo_eq x Hx1 y Hy1 (from right to left).
We will prove ∀w ∈ Lx' ∪ Ly', w < x + y.
Let w be given.
Apply binunionE' to the current goal.
Assume Hw: w ∈ Lx'.
Apply ReplE_impred Lx (λw ⇒ w + y) w Hw to the current goal.
Let w' be given.
Assume Hw': w' ∈ Lx.
Assume Hwe: w = w' + y.
rewrite the current goal using Hwe (from left to right).
We will prove w' + y < x + y.
Apply add_SNo_Lt1 w' y x (HLRx1 w' Hw') Hy1 Hx1 to the current goal.
We will prove w' < x.
An exact proof term for the current goal is Hx3 w' Hw'.
Assume Hw: w ∈ Ly'.
Apply ReplE_impred Ly (λw ⇒ x + w) w Hw to the current goal.
Let w' be given.
Assume Hw': w' ∈ Ly.
Assume Hwe: w = x + w'.
rewrite the current goal using Hwe (from left to right).
We will prove x + w' < x + y.
Apply add_SNo_Lt2 x w' y Hx1 (HLRy1 w' Hw') Hy1 to the current goal.
We will prove w' < y.
An exact proof term for the current goal is Hy3 w' Hw'.
rewrite the current goal using add_SNo_eq x Hx1 y Hy1 (from right to left).
We will prove ∀z ∈ Rx' ∪ Ry', x + y < z.
Let z be given.
Apply binunionE' to the current goal.
Assume Hz: z ∈ Rx'.
Apply ReplE_impred Rx (λz ⇒ z + y) z Hz to the current goal.
Let z' be given.
Assume Hz': z' ∈ Rx.
Assume Hze: z = z' + y.
rewrite the current goal using Hze (from left to right).
We will prove x + y < z' + y.
Apply add_SNo_Lt1 x y z' Hx1 Hy1 (HLRx2 z' Hz') to the current goal.
We will prove x < z'.
An exact proof term for the current goal is Hx4 z' Hz'.
Assume Hz: z ∈ Ry'.
Apply ReplE_impred Ry (λz ⇒ x + z) z Hz to the current goal.
Let z' be given.
Assume Hz': z' ∈ Ry.
Assume Hze: z = x + z'.
rewrite the current goal using Hze (from left to right).
We will prove x + y < x + z'.
Apply add_SNo_Lt2 x y z' Hx1 Hy1 (HLRy2 z' Hz') to the current goal.
We will prove y < z'.
An exact proof term for the current goal is Hy4 z' Hz'.
∎
Theorem. (add_SNoCutP_gen)
∀Lx Rx Ly Ry x y, SNoCutP Lx Rx → SNoCutP Ly Ry → x = SNoCut Lx Rx → y = SNoCut Ly Ry → SNoCutP ({w + y|w ∈ Lx} ∪ {x + w|w ∈ Ly}) ({z + y|z ∈ Rx} ∪ {x + z|z ∈ Ry})
In Proofgold the corresponding term root is b23ebe... and proposition id is 0362c0...
Proof:
Let Lx, Rx, Ly, Ry, x and y be given.
Assume HLRx HLRy Hxe Hye.
Apply add_SNoCutP_lem Lx Rx Ly Ry x y HLRx HLRy Hxe Hye to the current goal.
Assume H _.
An exact proof term for the current goal is H.
∎
Theorem. (add_SNoCut_eq)
∀Lx Rx Ly Ry x y, SNoCutP Lx Rx → SNoCutP Ly Ry → x = SNoCut Lx Rx → y = SNoCut Ly Ry → x + y = SNoCut ({w + y|w ∈ Lx} ∪ {x + w|w ∈ Ly}) ({z + y|z ∈ Rx} ∪ {x + z|z ∈ Ry})
In Proofgold the corresponding term root is 0ce555... and proposition id is dbc2fa...
Proof:
Let Lx, Rx, Ly, Ry, x and y be given.
Assume HLRx HLRy Hxe Hye.
Apply add_SNoCutP_lem Lx Rx Ly Ry x y HLRx HLRy Hxe Hye to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
∎
Theorem. (add_SNo_SNoCut_L_interpolate)
∀Lx Rx Ly Ry x y, SNoCutP Lx Rx → SNoCutP Ly Ry → x = SNoCut Lx Rx → y = SNoCut Ly Ry → ∀u ∈ SNoL (x + y), (∃v ∈ Lx, u ≤ v + y) ∨ (∃v ∈ Ly, u ≤ x + v)
In Proofgold the corresponding term root is 0fc8ac... and proposition id is 8e8eb2...
Proof:
Let Lx, Rx, Ly, Ry, x and y be given.
Assume HLRx HLRy Hxe Hye.
Apply HLRx to the current goal.
Assume H.
Apply H to the current goal.
Assume HLRx1: ∀w ∈ Lx, SNo w.
Assume HLRx2: ∀z ∈ Rx, SNo z.
Assume HLRx3: ∀w ∈ Lx, ∀z ∈ Rx, w < z.
Apply HLRy to the current goal.
Assume H.
Apply H to the current goal.
Assume HLRy1: ∀w ∈ Ly, SNo w.
Assume HLRy2: ∀z ∈ Ry, SNo z.
Assume HLRy3: ∀w ∈ Ly, ∀z ∈ Ry, w < z.
Apply SNoCutP_SNoCut_impred Lx Rx HLRx to the current goal.
rewrite the current goal using Hxe (from right to left).
Assume Hx1: SNo x.
Assume Hx2: SNoLev x ∈ ordsucc ((⋃w ∈ Lxordsucc (SNoLev w)) ∪ (⋃z ∈ Rxordsucc (SNoLev z))).
Assume Hx3: ∀w ∈ Lx, w < x.
Assume Hx4: ∀z ∈ Rx, x < z.
Assume Hx5: (∀u, SNo u → (∀w ∈ Lx, w < u) → (∀z ∈ Rx, u < z) → SNoLev x ⊆ SNoLev u ∧ SNoEq_ (SNoLev x) x u).
Apply SNoCutP_SNoCut_impred Ly Ry HLRy to the current goal.
rewrite the current goal using Hye (from right to left).
Assume Hy1: SNo y.
Assume Hy2: SNoLev y ∈ ordsucc ((⋃w ∈ Lyordsucc (SNoLev w)) ∪ (⋃z ∈ Ryordsucc (SNoLev z))).
Assume Hy3: ∀w ∈ Ly, w < y.
Assume Hy4: ∀z ∈ Ry, y < z.
Assume Hy5: (∀u, SNo u → (∀w ∈ Ly, w < u) → (∀z ∈ Ry, u < z) → SNoLev y ⊆ SNoLev u ∧ SNoEq_ (SNoLev y) y u).
We prove the intermediate claim Lxy: SNo (x + y).
An exact proof term for the current goal is SNo_add_SNo x y Hx1 Hy1.
We prove the intermediate claim LI: ∀u, SNo u → SNoLev u ∈ SNoLev (x + y) → u < x + y → (∃v ∈ Lx, u ≤ v + y) ∨ (∃v ∈ Ly, u ≤ x + v).
Apply SNoLev_ind to the current goal.
Let u be given.
Assume Hu1: SNo u.
Assume IH: ∀z ∈ SNoS_ (SNoLev u), SNoLev z ∈ SNoLev (x + y) → z < x + y → (∃v ∈ Lx, z ≤ v + y) ∨ (∃v ∈ Ly, z ≤ x + v).
Assume Hu2: SNoLev u ∈ SNoLev (x + y).
Assume Hu3: u < x + y.
Apply dneg to the current goal.
Assume HNC: ¬ ((∃v ∈ Lx, u ≤ v + y) ∨ (∃v ∈ Ly, u ≤ x + v)).
Apply SNoLt_irref u to the current goal.
We will prove u < u.
Apply SNoLtLe_tra u (x + y) u Hu1 Lxy Hu1 Hu3 to the current goal.
We will prove x + y ≤ u.
Set Lxy1 to be the term {w + y|w ∈ Lx}.
Set Lxy2 to be the term {x + w|w ∈ Ly}.
Set Rxy1 to be the term {z + y|z ∈ Rx}.
Set Rxy2 to be the term {x + z|z ∈ Ry}.
rewrite the current goal using add_SNoCut_eq Lx Rx Ly Ry x y HLRx HLRy Hxe Hye (from left to right).
We will prove SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2) ≤ u.
rewrite the current goal using SNo_eta u Hu1 (from left to right).
We will prove SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2) ≤ SNoCut (SNoL u) (SNoR u).
Apply SNoCut_Le (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2) (SNoL u) (SNoR u) to the current goal.
An exact proof term for the current goal is add_SNoCutP_gen Lx Rx Ly Ry x y HLRx HLRy Hxe Hye.
An exact proof term for the current goal is SNoCutP_SNoL_SNoR u Hu1.
rewrite the current goal using SNo_eta u Hu1 (from right to left).
We will prove ∀w ∈ Lxy1 ∪ Lxy2, w < u.
Let w be given.
Assume Hw: w ∈ Lxy1 ∪ Lxy2.
Apply binunionE Lxy1 Lxy2 w Hw to the current goal.
Assume Hw2: w ∈ Lxy1.
We will prove w < u.
Apply ReplE_impred Lx (λw ⇒ w + y) w Hw2 to the current goal.
Let v be given.
Assume Hv: v ∈ Lx.
Assume Hwv: w = v + y.
rewrite the current goal using Hwv (from left to right).
We will prove v + y < u.
We prove the intermediate claim Lvy: SNo (v + y).
An exact proof term for the current goal is SNo_add_SNo v y (HLRx1 v Hv) Hy1.
Apply SNoLtLe_or (v + y) u Lvy Hu1 to the current goal.
Assume H1: v + y < u.
An exact proof term for the current goal is H1.
Assume H1: u ≤ v + y.
We will prove False.
Apply HNC to the current goal.
Apply orIL to the current goal.
We use v to witness the existential quantifier.
Apply andI to the current goal.
We will prove v ∈ Lx.
An exact proof term for the current goal is Hv.
We will prove u ≤ v + y.
An exact proof term for the current goal is H1.
Assume Hw2: w ∈ Lxy2.
We will prove w < u.
Apply ReplE_impred Ly (λw ⇒ x + w) w Hw2 to the current goal.
Let v be given.
Assume Hv: v ∈ Ly.
Assume Hwv: w = x + v.
rewrite the current goal using Hwv (from left to right).
We will prove x + v < u.
We prove the intermediate claim Lxv: SNo (x + v).
An exact proof term for the current goal is SNo_add_SNo x v Hx1 (HLRy1 v Hv).
Apply SNoLtLe_or (x + v) u Lxv Hu1 to the current goal.
Assume H1: x + v < u.
An exact proof term for the current goal is H1.
Assume H1: u ≤ x + v.
We will prove False.
Apply HNC to the current goal.
Apply orIR to the current goal.
We use v to witness the existential quantifier.
Apply andI to the current goal.
We will prove v ∈ Ly.
An exact proof term for the current goal is Hv.
We will prove u ≤ x + v.
An exact proof term for the current goal is H1.
rewrite the current goal using add_SNoCut_eq Lx Rx Ly Ry x y HLRx HLRy Hxe Hye (from right to left).
We will prove ∀z ∈ SNoR u, x + y < z.
Let z be given.
Assume Hz: z ∈ SNoR u.
Apply SNoR_E u Hu1 z Hz to the current goal.
Assume Hz1: SNo z.
Assume Hz2: SNoLev z ∈ SNoLev u.
Assume Hz3: u < z.
Apply SNoLt_trichotomy_or (x + y) z Lxy Hz1 to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: x + y < z.
An exact proof term for the current goal is H1.
Assume H1: x + y = z.
We will prove False.
Apply In_no2cycle (SNoLev z) (SNoLev u) Hz2 to the current goal.
We will prove SNoLev u ∈ SNoLev z.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hu2.
Assume H1: z < x + y.
We will prove False.
We prove the intermediate claim Lz1: z ∈ SNoS_ (SNoLev u).
An exact proof term for the current goal is SNoR_SNoS_ u z Hz.
We prove the intermediate claim Lz2: SNoLev z ∈ SNoLev (x + y).
Apply SNoLev_ordinal (x + y) Lxy to the current goal.
Assume Hxy1 _.
An exact proof term for the current goal is Hxy1 (SNoLev u) Hu2 (SNoLev z) Hz2.
Apply IH z Lz1 Lz2 H1 to the current goal.
Assume H2: ∃v ∈ Lx, z ≤ v + y.
Apply H2 to the current goal.
Let v be given.
Assume H3.
Apply H3 to the current goal.
Assume Hv: v ∈ Lx.
Assume H3: z ≤ v + y.
Apply HNC to the current goal.
Apply orIL to the current goal.
We use v to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv.
We will prove u ≤ v + y.
Apply SNoLe_tra u z (v + y) Hu1 Hz1 (SNo_add_SNo v y (HLRx1 v Hv) Hy1) to the current goal.
We will prove u ≤ z.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hz3.
We will prove z ≤ v + y.
An exact proof term for the current goal is H3.
Assume H2: ∃v ∈ Ly, z ≤ x + v.
Apply H2 to the current goal.
Let v be given.
Assume H3.
Apply H3 to the current goal.
Assume Hv: v ∈ Ly.
Assume H3: z ≤ x + v.
Apply HNC to the current goal.
Apply orIR to the current goal.
We use v to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv.
We will prove u ≤ x + v.
Apply SNoLe_tra u z (x + v) Hu1 Hz1 (SNo_add_SNo x v Hx1 (HLRy1 v Hv)) to the current goal.
We will prove u ≤ z.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hz3.
We will prove z ≤ x + v.
An exact proof term for the current goal is H3.
Let u be given.
Assume Hu: u ∈ SNoL (x + y).
Apply SNoL_E (x + y) Lxy u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev (x + y).
Assume Hu3: u < x + y.
An exact proof term for the current goal is LI u Hu1 Hu2 Hu3.
∎
Theorem. (add_SNo_SNoCut_R_interpolate)
∀Lx Rx Ly Ry x y, SNoCutP Lx Rx → SNoCutP Ly Ry → x = SNoCut Lx Rx → y = SNoCut Ly Ry → ∀u ∈ SNoR (x + y), (∃v ∈ Rx, v + y ≤ u) ∨ (∃v ∈ Ry, x + v ≤ u)
In Proofgold the corresponding term root is 189d80... and proposition id is 7ef92e...
Proof:
Let Lx, Rx, Ly, Ry, x and y be given.
Assume HLRx HLRy Hxe Hye.
Apply HLRx to the current goal.
Assume H.
Apply H to the current goal.
Assume HLRx1: ∀w ∈ Lx, SNo w.
Assume HLRx2: ∀z ∈ Rx, SNo z.
Assume HLRx3: ∀w ∈ Lx, ∀z ∈ Rx, w < z.
Apply HLRy to the current goal.
Assume H.
Apply H to the current goal.
Assume HLRy1: ∀w ∈ Ly, SNo w.
Assume HLRy2: ∀z ∈ Ry, SNo z.
Assume HLRy3: ∀w ∈ Ly, ∀z ∈ Ry, w < z.
Apply SNoCutP_SNoCut_impred Lx Rx HLRx to the current goal.
rewrite the current goal using Hxe (from right to left).
Assume Hx1: SNo x.
Assume Hx2: SNoLev x ∈ ordsucc ((⋃w ∈ Lxordsucc (SNoLev w)) ∪ (⋃z ∈ Rxordsucc (SNoLev z))).
Assume Hx3: ∀w ∈ Lx, w < x.
Assume Hx4: ∀z ∈ Rx, x < z.
Assume Hx5: (∀u, SNo u → (∀w ∈ Lx, w < u) → (∀z ∈ Rx, u < z) → SNoLev x ⊆ SNoLev u ∧ SNoEq_ (SNoLev x) x u).
Apply SNoCutP_SNoCut_impred Ly Ry HLRy to the current goal.
rewrite the current goal using Hye (from right to left).
Assume Hy1: SNo y.
Assume Hy2: SNoLev y ∈ ordsucc ((⋃w ∈ Lyordsucc (SNoLev w)) ∪ (⋃z ∈ Ryordsucc (SNoLev z))).
Assume Hy3: ∀w ∈ Ly, w < y.
Assume Hy4: ∀z ∈ Ry, y < z.
Assume Hy5: (∀u, SNo u → (∀w ∈ Ly, w < u) → (∀z ∈ Ry, u < z) → SNoLev y ⊆ SNoLev u ∧ SNoEq_ (SNoLev y) y u).
We prove the intermediate claim Lxy: SNo (x + y).
An exact proof term for the current goal is SNo_add_SNo x y Hx1 Hy1.
We prove the intermediate claim LI: ∀u, SNo u → SNoLev u ∈ SNoLev (x + y) → x + y < u → (∃v ∈ Rx, v + y ≤ u) ∨ (∃v ∈ Ry, x + v ≤ u).
Apply SNoLev_ind to the current goal.
Let u be given.
Assume Hu1: SNo u.
Assume IH: ∀z ∈ SNoS_ (SNoLev u), SNoLev z ∈ SNoLev (x + y) → x + y < z → (∃v ∈ Rx, v + y ≤ z) ∨ (∃v ∈ Ry, x + v ≤ z).
Assume Hu2: SNoLev u ∈ SNoLev (x + y).
Assume Hu3: x + y < u.
Apply dneg to the current goal.
Assume HNC: ¬ ((∃v ∈ Rx, v + y ≤ u) ∨ (∃v ∈ Ry, x + v ≤ u)).
Apply SNoLt_irref u to the current goal.
We will prove u < u.
Apply (λH : u ≤ x + y ⇒ SNoLeLt_tra u (x + y) u Hu1 Lxy Hu1 H Hu3) to the current goal.
We will prove u ≤ x + y.
Set Lxy1 to be the term {w + y|w ∈ Lx}.
Set Lxy2 to be the term {x + w|w ∈ Ly}.
Set Rxy1 to be the term {z + y|z ∈ Rx}.
Set Rxy2 to be the term {x + z|z ∈ Ry}.
rewrite the current goal using add_SNoCut_eq Lx Rx Ly Ry x y HLRx HLRy Hxe Hye (from left to right).
We will prove u ≤ SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2).
rewrite the current goal using SNo_eta u Hu1 (from left to right).
We will prove SNoCut (SNoL u) (SNoR u) ≤ SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2).
Apply SNoCut_Le (SNoL u) (SNoR u) (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2) to the current goal.
An exact proof term for the current goal is SNoCutP_SNoL_SNoR u Hu1.
An exact proof term for the current goal is add_SNoCutP_gen Lx Rx Ly Ry x y HLRx HLRy Hxe Hye.
rewrite the current goal using add_SNoCut_eq Lx Rx Ly Ry x y HLRx HLRy Hxe Hye (from right to left).
We will prove ∀z ∈ SNoL u, z < x + y.
Let z be given.
Assume Hz: z ∈ SNoL u.
Apply SNoL_E u Hu1 z Hz to the current goal.
Assume Hz1: SNo z.
Assume Hz2: SNoLev z ∈ SNoLev u.
Assume Hz3: z < u.
Apply SNoLt_trichotomy_or z (x + y) Hz1 Lxy to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: z < x + y.
An exact proof term for the current goal is H1.
Assume H1: z = x + y.
We will prove False.
Apply In_no2cycle (SNoLev z) (SNoLev u) Hz2 to the current goal.
We will prove SNoLev u ∈ SNoLev z.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hu2.
Assume H1: x + y < z.
We will prove False.
We prove the intermediate claim Lz1: z ∈ SNoS_ (SNoLev u).
An exact proof term for the current goal is SNoL_SNoS_ u z Hz.
We prove the intermediate claim Lz2: SNoLev z ∈ SNoLev (x + y).
Apply SNoLev_ordinal (x + y) Lxy to the current goal.
Assume Hxy1 _.
An exact proof term for the current goal is Hxy1 (SNoLev u) Hu2 (SNoLev z) Hz2.
Apply IH z Lz1 Lz2 H1 to the current goal.
Assume H2: ∃v ∈ Rx, v + y ≤ z.
Apply H2 to the current goal.
Let v be given.
Assume H3.
Apply H3 to the current goal.
Assume Hv: v ∈ Rx.
Assume H3: v + y ≤ z.
Apply HNC to the current goal.
Apply orIL to the current goal.
We use v to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv.
We will prove v + y ≤ u.
Apply SNoLe_tra (v + y) z u (SNo_add_SNo v y (HLRx2 v Hv) Hy1) Hz1 Hu1 to the current goal.
We will prove v + y ≤ z.
An exact proof term for the current goal is H3.
We will prove z ≤ u.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hz3.
Assume H2: ∃v ∈ Ry, x + v ≤ z.
Apply H2 to the current goal.
Let v be given.
Assume H3.
Apply H3 to the current goal.
Assume Hv: v ∈ Ry.
Assume H3: x + v ≤ z.
Apply HNC to the current goal.
Apply orIR to the current goal.
We use v to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv.
We will prove x + v ≤ u.
Apply SNoLe_tra (x + v) z u (SNo_add_SNo x v Hx1 (HLRy2 v Hv)) Hz1 Hu1 to the current goal.
We will prove x + v ≤ z.
An exact proof term for the current goal is H3.
We will prove z ≤ u.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hz3.
rewrite the current goal using SNo_eta u Hu1 (from right to left).
We will prove ∀w ∈ Rxy1 ∪ Rxy2, u < w.
Let w be given.
Assume Hw: w ∈ Rxy1 ∪ Rxy2.
Apply binunionE Rxy1 Rxy2 w Hw to the current goal.
Assume Hw2: w ∈ Rxy1.
We will prove u < w.
Apply ReplE_impred Rx (λw ⇒ w + y) w Hw2 to the current goal.
Let v be given.
Assume Hv: v ∈ Rx.
Assume Hwv: w = v + y.
rewrite the current goal using Hwv (from left to right).
We will prove u < v + y.
We prove the intermediate claim Lvy: SNo (v + y).
An exact proof term for the current goal is SNo_add_SNo v y (HLRx2 v Hv) Hy1.
Apply SNoLtLe_or u (v + y) Hu1 Lvy to the current goal.
Assume H1: u < v + y.
An exact proof term for the current goal is H1.
Assume H1: v + y ≤ u.
We will prove False.
Apply HNC to the current goal.
Apply orIL to the current goal.
We use v to witness the existential quantifier.
Apply andI to the current goal.
We will prove v ∈ Rx.
An exact proof term for the current goal is Hv.
We will prove v + y ≤ u.
An exact proof term for the current goal is H1.
Assume Hw2: w ∈ Rxy2.
We will prove u < w.
Apply ReplE_impred Ry (λw ⇒ x + w) w Hw2 to the current goal.
Let v be given.
Assume Hv: v ∈ Ry.
Assume Hwv: w = x + v.
rewrite the current goal using Hwv (from left to right).
We will prove u < x + v.
We prove the intermediate claim Lxv: SNo (x + v).
An exact proof term for the current goal is SNo_add_SNo x v Hx1 (HLRy2 v Hv).
Apply SNoLtLe_or u (x + v) Hu1 Lxv to the current goal.
Assume H1: u < x + v.
An exact proof term for the current goal is H1.
Assume H1: x + v ≤ u.
We will prove False.
Apply HNC to the current goal.
Apply orIR to the current goal.
We use v to witness the existential quantifier.
Apply andI to the current goal.
We will prove v ∈ Ry.
An exact proof term for the current goal is Hv.
We will prove x + v ≤ u.
An exact proof term for the current goal is H1.
Let u be given.
Assume Hu: u ∈ SNoR (x + y).
Apply SNoR_E (x + y) Lxy u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev (x + y).
Assume Hu3: x + y < u.
An exact proof term for the current goal is LI u Hu1 Hu2 Hu3.
∎
Theorem. (add_SNo_minus_Lt12b3)
∀x y z w u v, SNo x → SNo y → SNo z → SNo w → SNo u → SNo v → x + y + v < w + u + z → x + y + - z < w + u + - v
In Proofgold the corresponding term root is da9f29... and proposition id is d29d2a...
Proof:
Let x, y, z, w, u and v be given.
Assume Hx Hy Hz Hw Hu Hv.
Assume H1: x + y + v < w + u + z.
We will prove x + y + - z < w + u + - v.
We prove the intermediate claim Lmv: SNo (- v).
An exact proof term for the current goal is SNo_minus_SNo v Hv.
Apply add_SNo_minus_Lt1b3 x y z (w + u + - v) Hx Hy Hz (SNo_add_SNo_3 w u (- v) Hw Hu Lmv) to the current goal.
We will prove x + y < (w + u + - v) + z.
rewrite the current goal using add_SNo_assoc w u (- v) Hw Hu Lmv (from left to right).
We will prove x + y < ((w + u) + - v) + z.
rewrite the current goal using add_SNo_com_3b_1_2 (w + u) (- v) z (SNo_add_SNo w u Hw Hu) Lmv Hz (from left to right).
We will prove x + y < ((w + u) + z) + - v.
Apply add_SNo_minus_Lt2b ((w + u) + z) v (x + y) (SNo_add_SNo (w + u) z (SNo_add_SNo w u Hw Hu) Hz) Hv (SNo_add_SNo x y Hx Hy) to the current goal.
We will prove (x + y) + v < (w + u) + z.
rewrite the current goal using add_SNo_assoc x y v Hx Hy Hv (from right to left).
rewrite the current goal using add_SNo_assoc w u z Hw Hu Hz (from right to left).
An exact proof term for the current goal is H1.
∎
Theorem. (add_SNo_Le1_cancel)
∀x y z, SNo x → SNo y → SNo z → x + y ≤ z + y → x ≤ z
In Proofgold the corresponding term root is 01a9b8... and proposition id is 8bfac1...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz H1.
We will prove x ≤ z.
We prove the intermediate claim L1: (x + y) + - y = x.
An exact proof term for the current goal is add_SNo_minus_R2 x y Hx Hy.
We prove the intermediate claim L2: (z + y) + - y = z.
An exact proof term for the current goal is add_SNo_minus_R2 z y Hz Hy.
rewrite the current goal using L1 (from right to left).
rewrite the current goal using L2 (from right to left).
We will prove (x + y) + - y ≤ (z + y) + - y.
An exact proof term for the current goal is add_SNo_Le1 (x + y) (- y) (z + y) (SNo_add_SNo x y Hx Hy) (SNo_minus_SNo y Hy) (SNo_add_SNo z y Hz Hy) H1.
∎
Theorem. (add_SNo_minus_Le1b)
∀x y z, SNo x → SNo y → SNo z → x ≤ z + y → x + - y ≤ z
In Proofgold the corresponding term root is c8c038... and proposition id is 6a5e5e...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz H1.
Apply add_SNo_Le1_cancel (x + - y) y z (SNo_add_SNo x (- y) Hx (SNo_minus_SNo y Hy)) Hy Hz to the current goal.
We will prove (x + - y) + y ≤ z + y.
rewrite the current goal using add_SNo_assoc x (- y) y Hx (SNo_minus_SNo y Hy) Hy (from right to left).
rewrite the current goal using add_SNo_minus_SNo_linv y Hy (from left to right).
rewrite the current goal using add_SNo_0R x Hx (from left to right).
An exact proof term for the current goal is H1.
∎
Theorem. (add_SNo_minus_Le1b3)
∀x y z w, SNo x → SNo y → SNo z → SNo w → x + y ≤ w + z → x + y + - z ≤ w
In Proofgold the corresponding term root is 11c341... and proposition id is 6a25dd...
Proof:
Let x, y, z and w be given.
Assume Hx Hy Hz Hw H1.
We will prove x + y + - z ≤ w.
rewrite the current goal using add_SNo_assoc x y (- z) Hx Hy (SNo_minus_SNo z Hz) (from left to right).
We will prove (x + y) + - z ≤ w.
Apply add_SNo_minus_Le1b (x + y) z w (SNo_add_SNo x y Hx Hy) Hz Hw to the current goal.
An exact proof term for the current goal is H1.
∎
Theorem. (add_SNo_minus_Le12b3)
∀x y z w u v, SNo x → SNo y → SNo z → SNo w → SNo u → SNo v → x + y + v ≤ w + u + z → x + y + - z ≤ w + u + - v
In Proofgold the corresponding term root is 055445... and proposition id is d88d85...
Proof:
Let x, y, z, w, u and v be given.
Assume Hx Hy Hz Hw Hu Hv.
Assume H1: x + y + v ≤ w + u + z.
We will prove x + y + - z ≤ w + u + - v.
We prove the intermediate claim Lmv: SNo (- v).
An exact proof term for the current goal is SNo_minus_SNo v Hv.
Apply add_SNo_minus_Le1b3 x y z (w + u + - v) Hx Hy Hz (SNo_add_SNo_3 w u (- v) Hw Hu Lmv) to the current goal.
We will prove x + y ≤ (w + u + - v) + z.
rewrite the current goal using add_SNo_assoc w u (- v) Hw Hu Lmv (from left to right).
We will prove x + y ≤ ((w + u) + - v) + z.
rewrite the current goal using add_SNo_com_3b_1_2 (w + u) (- v) z (SNo_add_SNo w u Hw Hu) Lmv Hz (from left to right).
We will prove x + y ≤ ((w + u) + z) + - v.
Apply add_SNo_minus_Le2b ((w + u) + z) v (x + y) (SNo_add_SNo (w + u) z (SNo_add_SNo w u Hw Hu) Hz) Hv (SNo_add_SNo x y Hx Hy) to the current goal.
We will prove (x + y) + v ≤ (w + u) + z.
rewrite the current goal using add_SNo_assoc x y v Hx Hy Hv (from right to left).
rewrite the current goal using add_SNo_assoc w u z Hw Hu Hz (from right to left).
An exact proof term for the current goal is H1.
∎
End of Section SurrealAdd