Beginning of Section SurrealMinus
Definition. We define minus_SNo to be SNo_rec_i (λx m ⇒ SNoCut {m z|z ∈ SNoR x} {m w|w ∈ SNoL x}) of type set → set.
In Proofgold the corresponding term root is 268a6c... and object id is 8a6d85...
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use ≤ as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Theorem. (minus_SNo_eq)
∀x, SNo x → - x = SNoCut {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}
In Proofgold the corresponding term root is c9793e... and proposition id is 570cba...
Proof:
We prove the intermediate claim L1: ∀x, SNo x → ∀g h : set → set, (∀w ∈ SNoS_ (SNoLev x), g w = h w) → SNoCut {g z|z ∈ SNoR x} {g w|w ∈ SNoL x} = SNoCut {h z|z ∈ SNoR x} {h w|w ∈ SNoL x}.
Let x be given.
Assume Hx: SNo x.
Let g and h be given.
Assume Hgh: ∀w ∈ SNoS_ (SNoLev x), g w = h w.
We will prove SNoCut {g z|z ∈ SNoR x} {g w|w ∈ SNoL x} = SNoCut {h z|z ∈ SNoR x} {h w|w ∈ SNoL x}.
We prove the intermediate claim L1a: {g z|z ∈ SNoR x} = {h z|z ∈ SNoR x}.
Apply ReplEq_ext to the current goal.
Let z be given.
Assume Hz: z ∈ SNoR x.
We will prove g z = h z.
Apply Hgh 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 prove the intermediate claim L1b: {g w|w ∈ SNoL x} = {h w|w ∈ SNoL x}.
Apply ReplEq_ext to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL x.
We will prove g w = h w.
Apply Hgh 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.
rewrite the current goal using L1a (from left to right).
rewrite the current goal using L1b (from left to right).
Use reflexivity.
An exact proof term for the current goal is SNo_rec_i_eq (λx m ⇒ SNoCut {m z|z ∈ SNoR x} {m w|w ∈ SNoL x}) L1.
∎
Theorem. (minus_SNo_prop1)
∀x, SNo x → SNo (- x) ∧ (∀u ∈ SNoL x, - x < - u) ∧ (∀u ∈ SNoR x, - u < - x) ∧ SNoCutP {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}
In Proofgold the corresponding term root is 7c0e82... and proposition id is f0b75f...
Proof:
Apply SNoLev_ind to the current goal.
Let x be given.
Assume Hx: SNo x.
Assume IH: ∀w ∈ SNoS_ (SNoLev x), SNo (- w) ∧ (∀u ∈ SNoL w, - w < - u) ∧ (∀u ∈ SNoR w, - u < - w) ∧ SNoCutP {- z|z ∈ SNoR w} {- v|v ∈ SNoL w}.
We prove the intermediate claim IHLx: ∀w ∈ SNoL x, SNo (- w) ∧ (∀u ∈ SNoL w, - w < - u) ∧ (∀u ∈ SNoR w, - u < - 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.
Apply IH w Lw to the current goal.
Assume H _.
An exact proof term for the current goal is H.
We prove the intermediate claim IHRx: ∀z ∈ SNoR x, SNo (- z) ∧ (∀u ∈ SNoL z, - z < - u) ∧ (∀u ∈ SNoR z, - u < - z).
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.
Apply IH w Lw to the current goal.
Assume H _.
An exact proof term for the current goal is H.
Set L to be the term {- z|z ∈ SNoR x}.
Set R to be the term {- w|w ∈ SNoL x}.
We prove the intermediate claim LLR: SNoCutP L R.
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 ∈ L.
We will prove SNo w.
Apply ReplE_impred (SNoR x) (λz ⇒ - z) w Hw to the current goal.
Let z be given.
Assume Hz: z ∈ SNoR x.
Assume Hwz: w = - z.
Apply IHRx z Hz to the current goal.
Assume H2.
Apply H2 to the current goal.
Assume H2: SNo (- 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 z be given.
Assume Hz: z ∈ R.
We will prove SNo z.
Apply ReplE_impred (SNoL x) (λw ⇒ - w) z Hz to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL x.
Assume Hzw: z = - w.
Apply IHLx w Hw to the current goal.
Assume H2.
Apply H2 to the current goal.
Assume H2: SNo (- w).
Assume _ _.
We will prove SNo z.
rewrite the current goal using Hzw (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.
Apply ReplE_impred (SNoR x) (λz ⇒ - z) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoR x.
Assume Hwu: w = - u.
Apply SNoR_E x Hx u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev x.
Assume Hu3: x < u.
Apply SNoLev_prop u Hu1 to the current goal.
Assume Hu1a: ordinal (SNoLev u).
Assume Hu1b: SNo_ (SNoLev u) u.
Apply ReplE_impred (SNoL x) (λw ⇒ - w) z Hz to the current goal.
Let v be given.
Assume Hv: v ∈ SNoL x.
Assume Hzv: z = - v.
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 SNoLev_prop v Hv1 to the current goal.
Assume Hv1a: ordinal (SNoLev v).
Assume Hv1b: SNo_ (SNoLev v) v.
Apply IHLx v Hv to the current goal.
Assume H2.
Apply H2 to the current goal.
Assume H2: SNo (- v).
Assume H3: ∀u ∈ SNoL v, - v < - u.
Assume H4: ∀u ∈ SNoR v, - u < - v.
Apply IHRx u Hu to the current goal.
Assume H5.
Apply H5 to the current goal.
Assume H5: SNo (- u).
Assume H6: ∀v ∈ SNoL u, - u < - v.
Assume H7: ∀v ∈ SNoR u, - v < - u.
We will prove w < z.
rewrite the current goal using Hwu (from left to right).
rewrite the current goal using Hzv (from left to right).
We will prove - u < - v.
We prove the intermediate claim Lvu: v < u.
An exact proof term for the current goal is SNoLt_tra v x u Hv1 Hx Hu1 Hv3 Hu3.
Apply SNoLtE v u Hv1 Hu1 Lvu to the current goal.
Let z be given.
Assume Hz: SNo z.
Assume Hz1: SNoLev z ∈ SNoLev v ∩ SNoLev u.
Assume Hz2: SNoEq_ (SNoLev z) z v.
Assume Hz3: SNoEq_ (SNoLev z) z u.
Assume Hz4: v < z.
Assume Hz5: z < u.
Assume Hz6: SNoLev z ∉ v.
Assume Hz7: SNoLev z ∈ u.
Apply SNoLev_prop z Hz to the current goal.
Assume Hza: ordinal (SNoLev z).
Assume Hzb: SNo_ (SNoLev z) z.
Apply binintersectE (SNoLev v) (SNoLev u) (SNoLev z) Hz1 to the current goal.
Assume Hz1a: SNoLev z ∈ SNoLev v.
Assume Hz1b: SNoLev z ∈ SNoLev u.
We prove the intermediate claim LzLx: z ∈ SNoS_ (SNoLev x).
Apply SNoS_I2 z x Hz Hx to the current goal.
We will prove SNoLev z ∈ SNoLev x.
Apply SNoLev_ordinal x Hx to the current goal.
Assume Hx2: TransSet (SNoLev x).
Assume _.
An exact proof term for the current goal is Hx2 (SNoLev u) Hu2 (SNoLev z) Hz1b.
We prove the intermediate claim Lmz: SNo (- z).
Apply IH z LzLx 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.
We will prove - u < - v.
Apply SNoLt_tra (- u) (- z) (- v) H5 Lmz H2 to the current goal.
We will prove - u < - z.
Apply H6 to the current goal.
We will prove z ∈ SNoL u.
We will prove z ∈ {x ∈ SNoS_ (SNoLev u)|x < u}.
Apply SepI to the current goal.
We will prove z ∈ SNoS_ (SNoLev u).
Apply SNoS_I2 z u Hz Hu1 Hz1b to the current goal.
We will prove z < u.
An exact proof term for the current goal is Hz5.
We will prove - z < - v.
Apply H4 to the current goal.
We will prove z ∈ SNoR v.
We will prove z ∈ {x ∈ SNoS_ (SNoLev v)|v < x}.
Apply SepI to the current goal.
We will prove z ∈ SNoS_ (SNoLev v).
An exact proof term for the current goal is SNoS_I2 z v Hz Hv1 Hz1a.
We will prove v < z.
An exact proof term for the current goal is Hz4.
Assume H8: SNoLev v ∈ SNoLev u.
Assume H9: SNoEq_ (SNoLev v) v u.
Assume H10: SNoLev v ∈ u.
We will prove - u < - v.
Apply H6 to the current goal.
We will prove v ∈ SNoL u.
We will prove v ∈ {x ∈ SNoS_ (SNoLev u)|x < u}.
Apply SepI to the current goal.
We will prove v ∈ SNoS_ (SNoLev u).
An exact proof term for the current goal is SNoS_I2 v u Hv1 Hu1 H8.
We will prove v < u.
An exact proof term for the current goal is Lvu.
Assume H8: SNoLev u ∈ SNoLev v.
Assume H9: SNoEq_ (SNoLev u) v u.
Assume H10: SNoLev u ∉ v.
We will prove - u < - v.
Apply H4 to the current goal.
We will prove u ∈ SNoR v.
We will prove u ∈ {x ∈ SNoS_ (SNoLev v)|v < x}.
Apply SepI to the current goal.
We will prove u ∈ SNoS_ (SNoLev v).
An exact proof term for the current goal is SNoS_I2 u v Hu1 Hv1 H8.
We will prove v < u.
An exact proof term for the current goal is Lvu.
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 minus_SNo_eq x Hx (from left to right).
Apply and3I 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, SNoCut L R < - u.
Let u be given.
Assume Hu: u ∈ SNoL x.
We will prove SNoCut L R < - 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 LmuR: - u ∈ R.
Apply ReplI to the current goal.
We will prove u ∈ SNoL x.
An exact proof term for the current goal is Hu.
We will prove SNoCut L R < - u.
An exact proof term for the current goal is SNoCutP_SNoCut_R L R LLR (- u) LmuR.
We will prove ∀u ∈ SNoR x, - u < SNoCut L R.
Let u be given.
Assume Hu: u ∈ SNoR x.
We will prove - u < SNoCut L R.
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 LmuL: - u ∈ L.
Apply ReplI to the current goal.
We will prove u ∈ SNoR x.
An exact proof term for the current goal is Hu.
We will prove - u < SNoCut L R.
An exact proof term for the current goal is SNoCutP_SNoCut_L L R LLR (- u) LmuL.
We will prove SNoCutP L R.
An exact proof term for the current goal is LLR.
∎
Theorem. (SNo_minus_SNo)
∀x, SNo x → SNo (- x)
In Proofgold the corresponding term root is 5cf7d9... and proposition id is 744cc2...
Proof:
Let x be given.
Assume Hx.
Apply minus_SNo_prop1 x Hx 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. (minus_SNo_Lt_contra)
∀x y, SNo x → SNo y → x < y → - y < - x
In Proofgold the corresponding term root is 5ce52d... and proposition id is 3ebf6e...
Proof:
Let x and y be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume Hxy: x < y.
Apply minus_SNo_prop1 x Hx to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: SNo (- x).
Assume H2: ∀u ∈ SNoL x, - x < - u.
Assume H3: ∀u ∈ SNoR x, - u < - x.
Assume _.
Apply minus_SNo_prop1 y Hy to the current goal.
Assume H4.
Apply H4 to the current goal.
Assume H4.
Apply H4 to the current goal.
Assume H4: SNo (- y).
Assume H5: ∀u ∈ SNoL y, - y < - u.
Assume H6: ∀u ∈ SNoR y, - u < - y.
Assume _.
Apply SNoLtE x y Hx Hy Hxy to the current goal.
Let z be given.
Assume Hz: SNo z.
Assume Hz1: SNoLev z ∈ SNoLev x ∩ SNoLev y.
Assume Hz2: SNoEq_ (SNoLev z) z x.
Assume Hz3: SNoEq_ (SNoLev z) z y.
Assume Hz4: x < z.
Assume Hz5: z < y.
Assume Hz6: SNoLev z ∉ x.
Assume Hz7: SNoLev z ∈ y.
Apply binintersectE (SNoLev x) (SNoLev y) (SNoLev z) Hz1 to the current goal.
Assume Hz1x Hz1y.
We will prove - y < - x.
Apply SNoLt_tra (- y) (- z) (- x) H4 (SNo_minus_SNo z Hz) H1 to the current goal.
We will prove - y < - z.
Apply H5 z to the current goal.
We will prove z ∈ SNoL y.
We will prove z ∈ {x ∈ SNoS_ (SNoLev y)|x < y}.
Apply SepI to the current goal.
We will prove z ∈ SNoS_ (SNoLev y).
An exact proof term for the current goal is SNoS_I2 z y Hz Hy Hz1y.
We will prove z < y.
An exact proof term for the current goal is Hz5.
We will prove - z < - x.
Apply H3 z to the current goal.
We will prove z ∈ SNoR x.
We will prove z ∈ {z ∈ SNoS_ (SNoLev x)|x < z}.
Apply SepI to the current goal.
We will prove z ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 z x Hz Hx Hz1x.
We will prove x < z.
An exact proof term for the current goal is Hz4.
Assume H7: SNoLev x ∈ SNoLev y.
Assume H8: SNoEq_ (SNoLev x) x y.
Assume H9: SNoLev x ∈ y.
Apply H5 x to the current goal.
We will prove x ∈ SNoL y.
We will prove x ∈ {x ∈ SNoS_ (SNoLev y)|x < y}.
Apply SepI to the current goal.
We will prove x ∈ SNoS_ (SNoLev y).
An exact proof term for the current goal is SNoS_I2 x y Hx Hy H7.
We will prove x < y.
An exact proof term for the current goal is Hxy.
Assume H7: SNoLev y ∈ SNoLev x.
Assume H8: SNoEq_ (SNoLev y) x y.
Assume H9: SNoLev y ∉ x.
We will prove - y < - x.
Apply H3 y to the current goal.
We will prove y ∈ SNoR x.
We will prove y ∈ {y ∈ SNoS_ (SNoLev x)|x < y}.
Apply SepI to the current goal.
We will prove y ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 y x Hy Hx H7.
We will prove x < y.
An exact proof term for the current goal is Hxy.
∎
Theorem. (minus_SNo_Le_contra)
∀x y, SNo x → SNo y → x ≤ y → - y ≤ - x
In Proofgold the corresponding term root is c1b225... and proposition id is f8c896...
Proof:
Let x and y be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume Hxy: x ≤ y.
Apply SNoLeE x y Hx Hy Hxy to the current goal.
Assume H1: x < y.
We will prove - y ≤ - x.
Apply SNoLtLe to the current goal.
We will prove - y < - x.
An exact proof term for the current goal is minus_SNo_Lt_contra x y Hx Hy H1.
Assume H1: x = y.
We will prove - y ≤ - x.
rewrite the current goal using H1 (from left to right).
We will prove - y ≤ - y.
Apply SNoLe_ref to the current goal.
∎
Theorem. (minus_SNo_SNoCutP)
∀x, SNo x → SNoCutP {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}
In Proofgold the corresponding term root is 99c6fc... and proposition id is 5ad5e4...
Proof:
Let x be given.
Assume Hx: SNo x.
Apply minus_SNo_prop1 x Hx to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume _ _ _ H1.
An exact proof term for the current goal is H1.
∎
Theorem. (minus_SNo_SNoCutP_gen)
∀L R, SNoCutP L R → SNoCutP {- z|z ∈ R} {- w|w ∈ L}
In Proofgold the corresponding term root is e7650d... and proposition id is 687fea...
Proof:
Let L and R be given.
Assume HLR: SNoCutP L R.
Apply HLR to the current goal.
Assume H.
Apply H to the current goal.
Assume HLR1: ∀x ∈ L, SNo x.
Assume HLR2: ∀y ∈ R, SNo y.
Assume HLR3: ∀x ∈ L, ∀y ∈ R, x < y.
Set Lm to be the term {- z|z ∈ R}.
Set Rm to be the term {- w|w ∈ L}.
We will prove (∀w ∈ Lm, SNo w) ∧ (∀z ∈ Rm, SNo z) ∧ (∀w ∈ Lm, ∀z ∈ Rm, w < z).
Apply and3I to the current goal.
Let w be given.
Assume Hw: w ∈ Lm.
We will prove SNo w.
Apply ReplE_impred R (λz ⇒ - z) w Hw to the current goal.
Let z be given.
Assume Hz: z ∈ R.
Assume Hwz: w = - z.
rewrite the current goal using Hwz (from left to right).
We will prove SNo (- z).
Apply SNo_minus_SNo to the current goal.
Apply HLR2 to the current goal.
An exact proof term for the current goal is Hz.
Let z be given.
Assume Hz: z ∈ Rm.
We will prove SNo z.
Apply ReplE_impred L (λw ⇒ - w) z Hz to the current goal.
Let w be given.
Assume Hw: w ∈ L.
Assume Hzw: z = - w.
rewrite the current goal using Hzw (from left to right).
We will prove SNo (- w).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is HLR1 w Hw.
Let w be given.
Assume Hw: w ∈ Lm.
Let z be given.
Assume Hz: z ∈ Rm.
Apply ReplE_impred R (λz ⇒ - z) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ R.
Assume Hwu: w = - u.
Apply ReplE_impred L (λw ⇒ - w) z Hz to the current goal.
Let v be given.
Assume Hv: v ∈ L.
Assume Hzv: z = - v.
We will prove w < z.
rewrite the current goal using Hwu (from left to right).
rewrite the current goal using Hzv (from left to right).
We will prove - u < - v.
Apply minus_SNo_Lt_contra v u (HLR1 v Hv) (HLR2 u Hu) to the current goal.
We will prove v < u.
An exact proof term for the current goal is HLR3 v Hv u Hu.
∎
Theorem. (minus_SNo_Lev_lem1)
∀alpha, ordinal alpha → ∀x ∈ SNoS_ alpha, SNoLev (- x) ⊆ SNoLev x
In Proofgold the corresponding term root is 14986a... and proposition id is afc115...
Proof:
Apply ordinal_ind to the current goal.
Let alpha be given.
Assume Ha: ordinal alpha.
Apply Ha to the current goal.
Assume Ha1 Ha2.
Assume IH: ∀beta ∈ alpha, ∀x ∈ SNoS_ beta, SNoLev (- x) ⊆ SNoLev x.
Let x be given.
Assume Hx: x ∈ SNoS_ alpha.
Apply SNoS_E2 alpha Ha x Hx to the current goal.
Assume Hx1: SNoLev x ∈ alpha.
Assume Hx2: ordinal (SNoLev x).
Assume Hx3: SNo x.
Assume Hx4: SNo_ (SNoLev x) x.
Set L to be the term {- z|z ∈ SNoR x}.
Set R to be the term {- w|w ∈ SNoL x}.
We prove the intermediate claim LLR: SNoCutP L R.
An exact proof term for the current goal is minus_SNo_SNoCutP x Hx3.
We will prove SNoLev (- x) ⊆ SNoLev x.
rewrite the current goal using minus_SNo_eq x Hx3 (from left to right).
We will prove SNoLev (SNoCut L R) ⊆ SNoLev x.
Apply SNoCutP_SNoCut_impred L R LLR to the current goal.
Assume H2: SNo (SNoCut L R).
Assume H3: SNoLev (SNoCut L R) ∈ ordsucc ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))).
Assume _ _ _.
We prove the intermediate claim L3: ordinal ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))).
Apply ordinal_binunion to the current goal.
Apply ordinal_famunion to the current goal.
Let w be given.
Assume Hw: w ∈ L.
We will prove ordinal (ordsucc (SNoLev w)).
Apply ReplE_impred (SNoR x) (λz ⇒ - z) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoR x.
Assume Hwu: w = - u.
Apply SNoR_E x Hx3 u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev x.
Assume Hu3: x < u.
Apply ordinal_ordsucc to the current goal.
We will prove ordinal (SNoLev w).
Apply SNoLev_ordinal to the current goal.
We will prove SNo w.
rewrite the current goal using Hwu (from left to right).
An exact proof term for the current goal is SNo_minus_SNo u Hu1.
Apply ordinal_famunion to the current goal.
Let w be given.
Assume Hw: w ∈ R.
We will prove ordinal (ordsucc (SNoLev w)).
Apply ReplE_impred (SNoL x) (λz ⇒ - z) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL x.
Assume Hwu: w = - u.
Apply SNoL_E x Hx3 u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev x.
Assume Hu3: u < x.
Apply ordinal_ordsucc to the current goal.
We will prove ordinal (SNoLev w).
Apply SNoLev_ordinal to the current goal.
We will prove SNo w.
rewrite the current goal using Hwu (from left to right).
An exact proof term for the current goal is SNo_minus_SNo u Hu1.
We prove the intermediate claim L3a: TransSet ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))).
Apply L3 to the current goal.
Assume H _.
An exact proof term for the current goal is H.
Let beta be given.
Assume Hb: beta ∈ SNoLev (SNoCut L R).
We prove the intermediate claim Lb: beta ∈ ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))).
Apply ordsuccE ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))) (SNoLev (SNoCut L R)) H3 to the current goal.
Assume H4.
An exact proof term for the current goal is L3a (SNoLev (SNoCut L R)) H4 beta Hb.
Assume H4.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is Hb.
We will prove beta ∈ SNoLev x.
Apply binunionE (⋃x ∈ Lordsucc (SNoLev x)) (⋃y ∈ Rordsucc (SNoLev y)) beta Lb to the current goal.
Assume H4: beta ∈ ⋃x ∈ Lordsucc (SNoLev x).
Apply famunionE L (λx ⇒ ordsucc (SNoLev x)) beta H4 to the current goal.
Let w be given.
Assume Hw.
Apply Hw to the current goal.
Assume Hw1: w ∈ L.
Assume Hw2: beta ∈ ordsucc (SNoLev w).
We will prove beta ∈ SNoLev x.
Apply ReplE_impred (SNoR x) (λz ⇒ - z) w Hw1 to the current goal.
Let u be given.
Assume Hu: u ∈ SNoR x.
Assume Hwu: w = - u.
Apply SNoR_E x Hx3 u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev x.
Assume Hu3: x < u.
We prove the intermediate claim Lu: u ∈ SNoS_ (ordsucc (SNoLev u)).
An exact proof term for the current goal is SNoS_SNoLev u Hu1.
We prove the intermediate claim LsLu: ordsucc (SNoLev u) ∈ alpha.
Apply ordinal_ordsucc_In_eq (SNoLev x) (SNoLev u) Hx2 Hu2 to the current goal.
Assume H2: ordsucc (SNoLev u) ∈ SNoLev x.
An exact proof term for the current goal is Ha1 (SNoLev x) Hx1 (ordsucc (SNoLev u)) H2.
Assume H2: SNoLev x = ordsucc (SNoLev u).
rewrite the current goal using H2 (from right to left).
An exact proof term for the current goal is Hx1.
We prove the intermediate claim IHu: SNoLev (- u) ⊆ SNoLev u.
An exact proof term for the current goal is IH (ordsucc (SNoLev u)) LsLu u Lu.
We prove the intermediate claim LLu: ordinal (SNoLev u).
An exact proof term for the current goal is SNoLev_ordinal u Hu1.
We prove the intermediate claim Lmu: SNo (- u).
An exact proof term for the current goal is SNo_minus_SNo u Hu1.
We prove the intermediate claim LLmu: ordinal (SNoLev (- u)).
An exact proof term for the current goal is SNoLev_ordinal (- u) Lmu.
We prove the intermediate claim LsLw: ordinal (ordsucc (SNoLev w)).
Apply ordinal_ordsucc to the current goal.
rewrite the current goal using Hwu (from left to right).
An exact proof term for the current goal is LLmu.
We prove the intermediate claim Lb: ordinal beta.
An exact proof term for the current goal is ordinal_Hered (ordsucc (SNoLev w)) LsLw beta Hw2.
Apply ordinal_In_Or_Subq beta (SNoLev x) Lb Hx2 to the current goal.
Assume H5: beta ∈ SNoLev x.
An exact proof term for the current goal is H5.
Assume H5: SNoLev x ⊆ beta.
We will prove False.
We prove the intermediate claim LLub: SNoLev u ∈ beta.
An exact proof term for the current goal is H5 (SNoLev u) Hu2.
Apply ordsuccE (SNoLev w) beta Hw2 to the current goal.
rewrite the current goal using Hwu (from left to right).
Assume H5: beta ∈ SNoLev (- u).
Apply In_no2cycle (SNoLev u) beta LLub to the current goal.
We will prove beta ∈ SNoLev u.
An exact proof term for the current goal is IHu beta H5.
rewrite the current goal using Hwu (from left to right).
Assume H5: beta = SNoLev (- u).
Apply In_irref (SNoLev u) to the current goal.
Apply IHu (SNoLev u) to the current goal.
We will prove SNoLev u ∈ SNoLev (- u).
rewrite the current goal using H5 (from right to left).
An exact proof term for the current goal is LLub.
Assume H4: beta ∈ ⋃y ∈ Rordsucc (SNoLev y).
Apply famunionE R (λx ⇒ ordsucc (SNoLev x)) beta H4 to the current goal.
Let w be given.
Assume Hw.
Apply Hw to the current goal.
Assume Hw1: w ∈ R.
Assume Hw2: beta ∈ ordsucc (SNoLev w).
We will prove beta ∈ SNoLev x.
Apply ReplE_impred (SNoL x) (λz ⇒ - z) w Hw1 to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL x.
Assume Hwu: w = - u.
Apply SNoL_E x Hx3 u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev x.
Assume Hu3: u < x.
We prove the intermediate claim Lu: u ∈ SNoS_ (ordsucc (SNoLev u)).
An exact proof term for the current goal is SNoS_SNoLev u Hu1.
We prove the intermediate claim LsLu: ordsucc (SNoLev u) ∈ alpha.
Apply ordinal_ordsucc_In_eq (SNoLev x) (SNoLev u) Hx2 Hu2 to the current goal.
Assume H2: ordsucc (SNoLev u) ∈ SNoLev x.
An exact proof term for the current goal is Ha1 (SNoLev x) Hx1 (ordsucc (SNoLev u)) H2.
Assume H2: SNoLev x = ordsucc (SNoLev u).
rewrite the current goal using H2 (from right to left).
An exact proof term for the current goal is Hx1.
We prove the intermediate claim IHu: SNoLev (- u) ⊆ SNoLev u.
An exact proof term for the current goal is IH (ordsucc (SNoLev u)) LsLu u Lu.
We prove the intermediate claim LLu: ordinal (SNoLev u).
An exact proof term for the current goal is SNoLev_ordinal u Hu1.
We prove the intermediate claim Lmu: SNo (- u).
An exact proof term for the current goal is SNo_minus_SNo u Hu1.
We prove the intermediate claim LLmu: ordinal (SNoLev (- u)).
An exact proof term for the current goal is SNoLev_ordinal (- u) Lmu.
We prove the intermediate claim LsLw: ordinal (ordsucc (SNoLev w)).
Apply ordinal_ordsucc to the current goal.
rewrite the current goal using Hwu (from left to right).
An exact proof term for the current goal is LLmu.
We prove the intermediate claim Lb: ordinal beta.
An exact proof term for the current goal is ordinal_Hered (ordsucc (SNoLev w)) LsLw beta Hw2.
Apply ordinal_In_Or_Subq beta (SNoLev x) Lb Hx2 to the current goal.
Assume H5: beta ∈ SNoLev x.
An exact proof term for the current goal is H5.
Assume H5: SNoLev x ⊆ beta.
We will prove False.
We prove the intermediate claim LLub: SNoLev u ∈ beta.
An exact proof term for the current goal is H5 (SNoLev u) Hu2.
Apply ordsuccE (SNoLev w) beta Hw2 to the current goal.
rewrite the current goal using Hwu (from left to right).
Assume H5: beta ∈ SNoLev (- u).
Apply In_no2cycle (SNoLev u) beta LLub to the current goal.
We will prove beta ∈ SNoLev u.
An exact proof term for the current goal is IHu beta H5.
rewrite the current goal using Hwu (from left to right).
Assume H5: beta = SNoLev (- u).
Apply In_irref (SNoLev u) to the current goal.
Apply IHu (SNoLev u) to the current goal.
We will prove SNoLev u ∈ SNoLev (- u).
rewrite the current goal using H5 (from right to left).
An exact proof term for the current goal is LLub.
∎
Theorem. (minus_SNo_Lev_lem2)
∀x, SNo x → SNoLev (- x) ⊆ SNoLev x
In Proofgold the corresponding term root is 879020... and proposition id is 19cf80...
Proof:
Let x be given.
Assume Hx: SNo x.
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 LsLx: ordinal (ordsucc (SNoLev x)).
An exact proof term for the current goal is ordinal_ordsucc (SNoLev x) LLx.
We prove the intermediate claim LxsLx: x ∈ SNoS_ (ordsucc (SNoLev x)).
An exact proof term for the current goal is SNoS_SNoLev x Hx.
An exact proof term for the current goal is minus_SNo_Lev_lem1 (ordsucc (SNoLev x)) LsLx x LxsLx.
∎
Theorem. (minus_SNo_invol)
∀x, SNo x → - - x = x
In Proofgold the corresponding term root is 44bfe8... and proposition id is cc64ee...
Proof:
Apply SNo_ind to the current goal.
Let L and R be given.
Assume HLR: SNoCutP L R.
Assume IHL: ∀x ∈ L, - - x = x.
Assume IHR: ∀y ∈ R, - - y = y.
Apply HLR to the current goal.
Assume H.
Apply H to the current goal.
Assume HLR1: ∀x ∈ L, SNo x.
Assume HLR2: ∀y ∈ R, SNo y.
Assume HLR3: ∀x ∈ L, ∀y ∈ R, x < y.
We prove the intermediate claim LCLR: SNo (SNoCut L R).
An exact proof term for the current goal is SNoCutP_SNo_SNoCut L R HLR.
We prove the intermediate claim LmCLR: SNo (- SNoCut L R).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is LCLR.
We prove the intermediate claim LmmCLR: SNo (- - SNoCut L R).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is LmCLR.
We prove the intermediate claim L1: SNoLev (SNoCut L R) ⊆ SNoLev (- - SNoCut L R) ∧ SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) (- - SNoCut L R).
Apply SNoCutP_SNoCut_fst to the current goal.
An exact proof term for the current goal is HLR.
We will prove SNo (- - SNoCut L R).
An exact proof term for the current goal is LmmCLR.
We will prove ∀x ∈ L, x < - - SNoCut L R.
Let x be given.
Assume Hx.
rewrite the current goal using IHL x Hx (from right to left).
We prove the intermediate claim Lx: SNo x.
An exact proof term for the current goal is HLR1 x Hx.
We prove the intermediate claim Lmx: SNo (- x).
An exact proof term for the current goal is SNo_minus_SNo x Lx.
We will prove - - x < - - SNoCut L R.
Apply minus_SNo_Lt_contra (- SNoCut L R) (- x) LmCLR Lmx to the current goal.
We will prove - SNoCut L R < - x.
Apply minus_SNo_Lt_contra x (SNoCut L R) Lx LCLR to the current goal.
We will prove x < SNoCut L R.
An exact proof term for the current goal is SNoCutP_SNoCut_L L R HLR x Hx.
We will prove ∀y ∈ R, - - SNoCut L R < y.
Let y be given.
Assume Hy.
rewrite the current goal using IHR y Hy (from right to left).
We prove the intermediate claim Ly: SNo y.
An exact proof term for the current goal is HLR2 y Hy.
We prove the intermediate claim Lmy: SNo (- y).
An exact proof term for the current goal is SNo_minus_SNo y Ly.
We will prove - - SNoCut L R < - - y.
Apply minus_SNo_Lt_contra (- y) (- SNoCut L R) Lmy LmCLR to the current goal.
We will prove - y < - SNoCut L R.
Apply minus_SNo_Lt_contra (SNoCut L R) y LCLR Ly to the current goal.
We will prove SNoCut L R < y.
An exact proof term for the current goal is SNoCutP_SNoCut_R L R HLR y Hy.
Apply L1 to the current goal.
Assume L1a: SNoLev (SNoCut L R) ⊆ SNoLev (- - SNoCut L R).
Assume L1b: SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) (- - SNoCut L R).
We will prove - - SNoCut L R = SNoCut L R.
Use symmetry.
Apply SNo_eq to the current goal.
An exact proof term for the current goal is LCLR.
An exact proof term for the current goal is LmmCLR.
We will prove SNoLev (SNoCut L R) = SNoLev (- - SNoCut L R).
Apply set_ext to the current goal.
We will prove SNoLev (SNoCut L R) ⊆ SNoLev (- - SNoCut L R).
An exact proof term for the current goal is L1a.
We will prove SNoLev (- - SNoCut L R) ⊆ SNoLev (SNoCut L R).
Apply Subq_tra (SNoLev (- - SNoCut L R)) (SNoLev (- SNoCut L R)) (SNoLev (SNoCut L R)) to the current goal.
We will prove SNoLev (- - SNoCut L R) ⊆ SNoLev (- SNoCut L R).
Apply minus_SNo_Lev_lem2 (- SNoCut L R) LmCLR to the current goal.
We will prove SNoLev (- SNoCut L R) ⊆ SNoLev (SNoCut L R).
Apply minus_SNo_Lev_lem2 (SNoCut L R) LCLR to the current goal.
We will prove SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) (- - SNoCut L R).
An exact proof term for the current goal is L1b.
∎
Theorem. (minus_SNo_Lev)
∀x, SNo x → SNoLev (- x) = SNoLev x
In Proofgold the corresponding term root is f65499... and proposition id is 476ae5...
Proof:
Let x be given.
Assume Hx.
Apply set_ext to the current goal.
We will prove SNoLev (- x) ⊆ SNoLev x.
An exact proof term for the current goal is minus_SNo_Lev_lem2 x Hx.
We will prove SNoLev x ⊆ SNoLev (- x).
rewrite the current goal using minus_SNo_invol x Hx (from right to left) at position 1.
We will prove SNoLev (- - x) ⊆ SNoLev (- x).
An exact proof term for the current goal is minus_SNo_Lev_lem2 (- x) (SNo_minus_SNo x Hx).
∎
Theorem. (minus_SNo_SNo_)
∀alpha, ordinal alpha → ∀x, SNo_ alpha x → SNo_ alpha (- x)
In Proofgold the corresponding term root is 84605f... and proposition id is 14bd6d...
Proof:
Let alpha be given.
Assume Ha.
Let x be given.
Assume Hx: SNo_ alpha x.
We prove the intermediate claim Lx: SNo x.
An exact proof term for the current goal is SNo_SNo alpha Ha x Hx.
We prove the intermediate claim Lxa: SNoLev x = alpha.
An exact proof term for the current goal is SNoLev_uniq2 alpha Ha x Hx.
We prove the intermediate claim Lmxa: SNoLev (- x) = alpha.
rewrite the current goal using minus_SNo_Lev x Lx (from left to right).
An exact proof term for the current goal is Lxa.
We will prove SNo_ alpha (- x).
rewrite the current goal using Lmxa (from right to left).
We will prove SNo_ (SNoLev (- x)) (- x).
Apply SNoLev_ to the current goal.
We will prove SNo (- x).
An exact proof term for the current goal is SNo_minus_SNo x Lx.
∎
Theorem. (minus_SNo_SNoS_)
∀alpha, ordinal alpha → ∀x, x ∈ SNoS_ alpha → - x ∈ SNoS_ alpha
In Proofgold the corresponding term root is 12f1a5... and proposition id is e10c92...
Proof:
Let alpha be given.
Assume Ha.
Let x be given.
Assume Hx: x ∈ SNoS_ alpha.
Apply SNoS_E2 alpha Ha x Hx to the current goal.
Assume Hx1: SNoLev x ∈ alpha.
Assume Hx2: ordinal (SNoLev x).
Assume Hx3: SNo x.
Assume Hx4: SNo_ (SNoLev x) x.
We prove the intermediate claim Lbmx: SNo_ (SNoLev x) (- x).
An exact proof term for the current goal is minus_SNo_SNo_ (SNoLev x) Hx2 x Hx4.
An exact proof term for the current goal is SNoS_I alpha Ha (- x) (SNoLev x) Hx1 Lbmx.
∎
Theorem. (minus_SNoCut_eq_lem)
∀v, SNo v → ∀L R, SNoCutP L R → v = SNoCut L R → - v = SNoCut {- z|z ∈ R} {- w|w ∈ L}
In Proofgold the corresponding term root is 29069a... and proposition id is 11eb03...
Proof:
Apply SNoLev_ind to the current goal.
Let v be given.
Assume Hv: SNo v.
Assume IHv: ∀u ∈ SNoS_ (SNoLev v), ∀L R, SNoCutP L R → u = SNoCut L R → - u = SNoCut {- z|z ∈ R} {- w|w ∈ L}.
Let L and R be given.
Assume HLR: SNoCutP L R.
Apply HLR to the current goal.
Assume HLR1.
Apply HLR1 to the current goal.
Assume HLR1: ∀x ∈ L, SNo x.
Assume HLR2: ∀y ∈ R, SNo y.
Assume HLR3: ∀x ∈ L, ∀y ∈ R, x < y.
Assume HvLR: v = SNoCut L R.
Set mL to be the term {- w|w ∈ L}.
Set mR to be the term {- z|z ∈ R}.
Set mLv to be the term {- w|w ∈ SNoL v}.
Set mRv to be the term {- z|z ∈ SNoR v}.
We prove the intermediate claim L1: SNo (SNoCut L R).
An exact proof term for the current goal is SNoCutP_SNo_SNoCut L R HLR.
We prove the intermediate claim L2: SNoCutP mR mL.
An exact proof term for the current goal is minus_SNo_SNoCutP_gen L R HLR.
Apply SNoCutP_SNoCut_impred mR mL L2 to the current goal.
Assume H1: SNo (SNoCut mR mL).
Assume H2: SNoLev (SNoCut mR mL) ∈ ordsucc ((⋃x ∈ mRordsucc (SNoLev x)) ∪ (⋃y ∈ mLordsucc (SNoLev y))).
Assume H3: ∀x ∈ mR, x < SNoCut mR mL.
Assume H4: ∀y ∈ mL, SNoCut mR mL < y.
Assume H5: ∀z, SNo z → (∀x ∈ mR, x < z) → (∀y ∈ mL, z < y) → SNoLev (SNoCut mR mL) ⊆ SNoLev z ∧ SNoEq_ (SNoLev (SNoCut mR mL)) (SNoCut mR mL) z.
We prove the intermediate claim L3: ∀x ∈ mR, x < - v.
Let x be given.
Assume Hx: x ∈ mR.
Apply ReplE_impred R minus_SNo x Hx to the current goal.
Let z be given.
Assume Hz: z ∈ R.
Assume Hxz: x = - z.
We will prove x < - v.
rewrite the current goal using Hxz (from left to right).
We will prove - z < - v.
Apply minus_SNo_Lt_contra v z Hv (HLR2 z Hz) to the current goal.
We will prove v < z.
rewrite the current goal using HvLR (from left to right).
We will prove SNoCut L R < z.
An exact proof term for the current goal is SNoCutP_SNoCut_R L R HLR z Hz.
We prove the intermediate claim L4: ∀y ∈ mL, - v < y.
Let y be given.
Assume Hy: y ∈ mL.
Apply ReplE_impred L minus_SNo y Hy to the current goal.
Let w be given.
Assume Hw: w ∈ L.
Assume Hyw: y = - w.
We will prove - v < y.
rewrite the current goal using Hyw (from left to right).
We will prove - v < - w.
Apply minus_SNo_Lt_contra w v (HLR1 w Hw) Hv to the current goal.
We will prove w < v.
rewrite the current goal using HvLR (from left to right).
We will prove w < SNoCut L R.
An exact proof term for the current goal is SNoCutP_SNoCut_L L R HLR w Hw.
Apply H5 (- v) (SNo_minus_SNo v Hv) L3 L4 to the current goal.
Assume H6: SNoLev (SNoCut mR mL) ⊆ SNoLev (- v).
Assume H7: SNoEq_ (SNoLev (SNoCut mR mL)) (SNoCut mR mL) (- v).
We prove the intermediate claim L5: ordinal (SNoLev (SNoCut mR mL)).
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is H1.
We prove the intermediate claim L6: ordinal (SNoLev (- v)).
Apply SNoLev_ordinal to the current goal.
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hv.
Apply ordinal_In_Or_Subq (SNoLev (SNoCut mR mL)) (SNoLev (- v)) L5 L6 to the current goal.
Assume H8: SNoLev (SNoCut mR mL) ∈ SNoLev (- v).
We will prove False.
We prove the intermediate claim L7: SNoCut mR mL ∈ SNoS_ (SNoLev v).
Apply SNoS_I2 to the current goal.
We will prove SNo (SNoCut mR mL).
An exact proof term for the current goal is H1.
We will prove SNo v.
An exact proof term for the current goal is Hv.
We will prove SNoLev (SNoCut mR mL) ∈ SNoLev v.
rewrite the current goal using minus_SNo_Lev v Hv (from right to left).
An exact proof term for the current goal is H8.
We prove the intermediate claim LIH: - SNoCut mR mL = SNoCut {- z|z ∈ mL} {- w|w ∈ mR}.
An exact proof term for the current goal is IHv (SNoCut mR mL) L7 mR mL L2 (λq H ⇒ H).
We prove the intermediate claim L8: {- z|z ∈ mL} = L.
Apply Repl_invol_eq (λx ⇒ x ∈ L) minus_SNo to the current goal.
Let x be given.
Assume Hx: x ∈ L.
We will prove - - x = x.
An exact proof term for the current goal is minus_SNo_invol x (HLR1 x Hx).
Let x be given.
Assume Hx: x ∈ L.
An exact proof term for the current goal is Hx.
We prove the intermediate claim L9: {- z|z ∈ mR} = R.
Apply Repl_invol_eq (λy ⇒ y ∈ R) minus_SNo to the current goal.
Let y be given.
Assume Hy: y ∈ R.
We will prove - - y = y.
An exact proof term for the current goal is minus_SNo_invol y (HLR2 y Hy).
Let y be given.
Assume Hy: y ∈ R.
An exact proof term for the current goal is Hy.
We prove the intermediate claim L10: - SNoCut mR mL = v.
rewrite the current goal using LIH (from left to right).
rewrite the current goal using L8 (from left to right).
rewrite the current goal using L9 (from left to right).
Use symmetry.
An exact proof term for the current goal is HvLR.
Apply In_irref (SNoLev v) to the current goal.
We will prove SNoLev v ∈ SNoLev v.
rewrite the current goal using L10 (from right to left) at position 1.
We will prove SNoLev (- SNoCut mR mL) ∈ SNoLev v.
rewrite the current goal using minus_SNo_Lev (SNoCut mR mL) H1 (from left to right).
rewrite the current goal using minus_SNo_Lev v Hv (from right to left).
An exact proof term for the current goal is H8.
Assume H8: SNoLev (- v) ⊆ SNoLev (SNoCut mR mL).
We will prove - v = SNoCut mR mL.
Use symmetry.
Apply SNo_eq (SNoCut mR mL) (- v) H1 (SNo_minus_SNo v Hv) to the current goal.
We will prove SNoLev (SNoCut mR mL) = SNoLev (- v).
Apply set_ext to the current goal.
An exact proof term for the current goal is H6.
An exact proof term for the current goal is H8.
We will prove SNoEq_ (SNoLev (SNoCut mR mL)) (SNoCut mR mL) (- v).
An exact proof term for the current goal is H7.
∎
Theorem. (minus_SNoCut_eq)
∀L R, SNoCutP L R → - SNoCut L R = SNoCut {- z|z ∈ R} {- w|w ∈ L}
In Proofgold the corresponding term root is 083ffe... and proposition id is 54736f...
Proof:
Let L and R be given.
Assume HLR.
An exact proof term for the current goal is minus_SNoCut_eq_lem (SNoCut L R) (SNoCutP_SNo_SNoCut L R HLR) L R HLR (λq H ⇒ H).
∎
Theorem. (minus_SNo_Lt_contra1)
∀x y, SNo x → SNo y → - x < y → - y < x
In Proofgold the corresponding term root is 226757... and proposition id is 298729...
Proof:
Let x and y be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume Hxy: - x < y.
We will prove - y < x.
rewrite the current goal using minus_SNo_invol x Hx (from right to left).
We will prove - y < - - x.
Apply minus_SNo_Lt_contra (- x) y (SNo_minus_SNo x Hx) Hy to the current goal.
We will prove - x < y.
An exact proof term for the current goal is Hxy.
∎
Theorem. (minus_SNo_Lt_contra2)
∀x y, SNo x → SNo y → x < - y → y < - x
In Proofgold the corresponding term root is c6f2da... and proposition id is f41968...
Proof:
Let x and y be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume Hxy: x < - y.
We will prove y < - x.
rewrite the current goal using minus_SNo_invol y Hy (from right to left).
We will prove - - y < - x.
Apply minus_SNo_Lt_contra x (- y) Hx (SNo_minus_SNo y Hy) to the current goal.
We will prove x < - y.
An exact proof term for the current goal is Hxy.
∎
Theorem. (mordinal_SNoLev_min_2)
∀alpha, ordinal alpha → ∀z, SNo z → SNoLev z ∈ ordsucc alpha → - alpha ≤ z
In Proofgold the corresponding term root is 2766c7... and proposition id is a96d68...
Proof:
Let alpha be given.
Assume Ha.
Let z be given.
Assume Hz: SNo z.
Assume H1: SNoLev z ∈ ordsucc alpha.
We prove the intermediate claim Lz1: SNo (- z).
An exact proof term for the current goal is SNo_minus_SNo z Hz.
We prove the intermediate claim Lz2: SNoLev (- z) ∈ ordsucc alpha.
rewrite the current goal using minus_SNo_Lev z Hz (from left to right).
An exact proof term for the current goal is H1.
We will prove - alpha ≤ z.
rewrite the current goal using minus_SNo_invol z Hz (from right to left).
We will prove - alpha ≤ - - z.
Apply minus_SNo_Le_contra (- z) alpha Lz1 (ordinal_SNo alpha Ha) to the current goal.
We will prove - z ≤ alpha.
An exact proof term for the current goal is ordinal_SNoLev_max_2 alpha Ha (- z) Lz1 Lz2.
∎
Theorem. (minus_SNo_SNoS_omega)
∀x ∈ SNoS_ ω, - x ∈ SNoS_ ω
In Proofgold the corresponding term root is daeba5... and proposition id is 0c19f5...
Proof:
Let x be given.
Assume Hx.
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_I ω omega_ordinal (- x) (SNoLev (- x)) to the current goal.
We will prove SNoLev (- x) ∈ ω.
rewrite the current goal using minus_SNo_Lev x Hx3 (from left to right).
We will prove SNoLev x ∈ ω.
An exact proof term for the current goal is Hx1.
We will prove SNo_ (SNoLev (- x)) (- x).
Apply SNoLev_ to the current goal.
An exact proof term for the current goal is SNo_minus_SNo x Hx3.
∎
Theorem. (SNoL_minus_SNoR)
∀x, SNo x → SNoL (- x) = {- w|w ∈ SNoR x}
In Proofgold the corresponding term root is 084b2d... and proposition id is 8b2b92...
Proof:
Let x be given.
Assume Hx.
We prove the intermediate claim Lmx: SNo (- x).
An exact proof term for the current goal is SNo_minus_SNo x Hx.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ SNoL (- x).
Apply SNoL_E (- x) Lmx z Hz to the current goal.
Assume Hz1: SNo z.
rewrite the current goal using minus_SNo_Lev x Hx (from left to right).
Assume Hz2: SNoLev z ∈ SNoLev x.
Assume Hz3: z < - x.
We will prove z ∈ {- w|w ∈ SNoR x}.
rewrite the current goal using minus_SNo_invol z Hz1 (from right to left).
Apply ReplI to the current goal.
We will prove - z ∈ SNoR x.
Apply SNoR_I x Hx (- z) (SNo_minus_SNo z Hz1) to the current goal.
We will prove SNoLev (- z) ∈ SNoLev x.
rewrite the current goal using minus_SNo_Lev z Hz1 (from left to right).
An exact proof term for the current goal is Hz2.
We will prove x < - z.
Apply minus_SNo_Lt_contra2 z x Hz1 Hx to the current goal.
An exact proof term for the current goal is Hz3.
Let z be given.
Assume Hz: z ∈ {- w|w ∈ SNoR x}.
Apply ReplE_impred (SNoR x) minus_SNo z Hz to the current goal.
Let w be given.
Assume Hw: w ∈ SNoR x.
Assume Hzw: z = - w.
We will prove z ∈ SNoL (- x).
rewrite the current goal using Hzw (from left to right).
We will prove - w ∈ SNoL (- 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.
Apply SNoL_I (- x) Lmx (- w) (SNo_minus_SNo w Hw1) to the current goal.
We will prove SNoLev (- w) ∈ SNoLev (- x).
rewrite the current goal using minus_SNo_Lev w Hw1 (from left to right).
rewrite the current goal using minus_SNo_Lev x Hx (from left to right).
An exact proof term for the current goal is Hw2.
We will prove - w < - x.
Apply minus_SNo_Lt_contra x w Hx Hw1 to the current goal.
An exact proof term for the current goal is Hw3.
∎
End of Section SurrealMinus