Beginning of Section SurrealAdd
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
(*** $I sig/Part1.mgs ***)
(*** $I sig/Part2.mgs ***)
(*** $I sig/Part3.mgs ***)
(*** $I sig/Part4.mgs ***)
(*** Part 5 ***)
L11
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.
L15
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:
Proof not loaded.
L71
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:
Proof not loaded.
L532
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:
Proof not loaded.
L542
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:
Proof not loaded.
L551
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:
Proof not loaded.
L559
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:
Proof not loaded.
L564
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:
Proof not loaded.
L629
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:
Proof not loaded.
L641
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:
Proof not loaded.
L707
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:
Proof not loaded.
L719
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:
Proof not loaded.
L732
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:
Proof not loaded.
L745
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:
Proof not loaded.
L760
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:
Proof not loaded.
L773
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:
Proof not loaded.
L781
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:
Proof not loaded.
L882
Theorem. (add_SNo_0L)
∀x, SNo x → 0 + x = x
In Proofgold the corresponding term root is 107598... and proposition id is 446bad...
Proof:
Proof not loaded.
L945
Theorem. (add_SNo_0R)
∀x, SNo x → x + 0 = x
In Proofgold the corresponding term root is d8a186... and proposition id is 1a7fa1...
Proof:
Proof not loaded.
L951
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:
Proof not loaded.
L1126
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:
Proof not loaded.
L1136
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:
Proof not loaded.
L1176
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:
Proof not loaded.
L1208
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:
Proof not loaded.
L1273
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:
Proof not loaded.
L1425
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:
Proof not loaded.
L1446
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:
Proof not loaded.
L1470
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:
Proof not loaded.
L1487
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:
Proof not loaded.
L1516
Theorem. (add_SNo_In_omega)
∀n m ∈ ω, n + m ∈ ω
In Proofgold the corresponding term root is f45cbb... and proposition id is eb6375...
Proof:
Proof not loaded.
L1525
Theorem. (add_SNo_1_1_2)
1 + 1 = 2
In Proofgold the corresponding term root is bbc448... and proposition id is 2b8298...
Proof:
Proof not loaded.
L1530
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:
Proof not loaded.
L1687
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:
Proof not loaded.
L1844
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:
Proof not loaded.
L2260
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:
Proof not loaded.
L2287
Theorem. (minus_SNo_0)
- 0 = 0
In Proofgold the corresponding term root is 77bc67... and proposition id is 3fcc57...
Proof:
Proof not loaded.
L2295
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:
Proof not loaded.
L2325
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:
Proof not loaded.
L2333
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:
Proof not loaded.
L2697
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:
Proof not loaded.
L2727
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:
Proof not loaded.
L2736
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:
Proof not loaded.
L2742
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:
Proof not loaded.
L2751
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:
Proof not loaded.
L2757
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:
Proof not loaded.
L2773
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:
Proof not loaded.
L2780
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:
Proof not loaded.
L2790
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:
Proof not loaded.
L2800
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:
Proof not loaded.
L2810
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:
Proof not loaded.
L2822
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:
Proof not loaded.
L2836
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:
Proof not loaded.
L2844
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:
Proof not loaded.
L2852
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:
Proof not loaded.
L2860
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:
Proof not loaded.
L2869
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:
Proof not loaded.
L2880
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:
Proof not loaded.
L2887
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:
Proof not loaded.
L2895
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:
Proof not loaded.
L2905
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:
Proof not loaded.
L2916
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:
Proof not loaded.
L2926
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:
Proof not loaded.
L2936
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:
Proof not loaded.
L2945
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:
Proof not loaded.
L2954
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:
Proof not loaded.
L2984
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:
Proof not loaded.
L2997
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:
Proof not loaded.
L3010
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:
Proof not loaded.
L3041
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:
Proof not loaded.
L3064
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:
Proof not loaded.
L3081
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:
Proof not loaded.
L3115
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:
Proof not loaded.
L3175
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:
Proof not loaded.
L3183
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:
Proof not loaded.
L3196
Theorem. (add_SNo_1_ordsucc)
∀n ∈ ω, n + 1 = ordsucc n
In Proofgold the corresponding term root is ec6cad... and proposition id is 85f670...
Proof:
Proof not loaded.
L3206
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:
Proof not loaded.
L3214
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:
Proof not loaded.
L3222
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:
Proof not loaded.
L3229
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:
Proof not loaded.
L3255
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:
Proof not loaded.
L3264
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:
Proof not loaded.
L3273
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:
Proof not loaded.
L3281
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:
Proof not loaded.
L3688
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:
Proof not loaded.
L3700
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:
Proof not loaded.
L3712
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:
Proof not loaded.
L3879
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:
Proof not loaded.
L4046
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:
Proof not loaded.
L4069
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:
Proof not loaded.
L4085
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:
Proof not loaded.
L4095
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:
Proof not loaded.
L4104
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:
Proof not loaded.
End of Section SurrealAdd