Beginning of Section Int
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 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Primitive. The name int is a term of type set.
In Proofgold the corresponding term root is 90ee85... and object id is 331669...
L13
Axiom. (int_SNo_cases) We take the following as an axiom:
∀p : set → prop, (∀n ∈ ω, p n) → (∀n ∈ ω, p (- n)) → ∀x ∈ int, p x
In Proofgold the corresponding term root is 60107a... and proposition id is 14278d...
L14
Axiom. (int_3_cases) We take the following as an axiom:
∀n ∈ int, ∀p : prop, (∀m ∈ ω, n = - ordsucc m → p) → (n = 0 → p) → (∀m ∈ ω, n = ordsucc m → p) → p
In Proofgold the corresponding term root is 67b16d... and proposition id is 5c24db...
L15
Axiom. (int_SNo) We take the following as an axiom:
∀x ∈ int, SNo x
In Proofgold the corresponding term root is 19fdd2... and proposition id is 6089ec...
L16
Axiom. (Subq_omega_int) We take the following as an axiom:
ω ⊆ int
In Proofgold the corresponding term root is 405dda... and proposition id is b1bb2b...
L17
Axiom. (int_minus_SNo_omega) We take the following as an axiom:
∀n ∈ ω, - n ∈ int
In Proofgold the corresponding term root is 869503... and proposition id is 3a2593...
L18
Axiom. (int_add_SNo_lem) We take the following as an axiom:
∀n ∈ ω, ∀m, nat_p m → - n + m ∈ int
In Proofgold the corresponding term root is 8f0047... and proposition id is aab9d5...
L19
Axiom. (int_add_SNo) We take the following as an axiom:
∀x y ∈ int, x + y ∈ int
In Proofgold the corresponding term root is d66975... and proposition id is 1036d9...
L20
Axiom. (int_minus_SNo) We take the following as an axiom:
∀x ∈ int, - x ∈ int
In Proofgold the corresponding term root is 00e714... and proposition id is b2c591...
L21
Axiom. (int_mul_SNo) We take the following as an axiom:
∀x y ∈ int, x * y ∈ int
In Proofgold the corresponding term root is a7bc92... and proposition id is f40564...
End of Section Int
Beginning of Section SurrealAbs
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 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Primitive. The name abs_SNo is a term of type set → set.
In Proofgold the corresponding term root is 34f6dc... and object id is 2990e5...
L29
Axiom. (nonneg_abs_SNo) We take the following as an axiom:
∀x, 0 ≤ x → abs_SNo x = x
In Proofgold the corresponding term root is 330ed1... and proposition id is 1ed323...
L30
Axiom. (not_nonneg_abs_SNo) We take the following as an axiom:
∀x, ¬ (0 ≤ x) → abs_SNo x = - x
In Proofgold the corresponding term root is bc755d... and proposition id is b29f70...
L31
Axiom. (abs_SNo_0) We take the following as an axiom:
abs_SNo 0 = 0
In Proofgold the corresponding term root is c0c559... and proposition id is 35a655...
L32
Axiom. (pos_abs_SNo) We take the following as an axiom:
∀x, 0 < x → abs_SNo x = x
In Proofgold the corresponding term root is 32e626... and proposition id is 88568f...
L33
Axiom. (neg_abs_SNo) We take the following as an axiom:
∀x, SNo x → x < 0 → abs_SNo x = - x
In Proofgold the corresponding term root is d1245a... and proposition id is f858cb...
L34
Axiom. (SNo_abs_SNo) We take the following as an axiom:
∀x, SNo x → SNo (abs_SNo x)
In Proofgold the corresponding term root is 7266a7... and proposition id is 1c9c46...
L35
Axiom. (abs_SNo_Lev) We take the following as an axiom:
∀x, SNo x → SNoLev (abs_SNo x) = SNoLev x
In Proofgold the corresponding term root is fe5907... and proposition id is 24d266...
L36
Axiom. (abs_SNo_minus) We take the following as an axiom:
∀x, SNo x → abs_SNo (- x) = abs_SNo x
In Proofgold the corresponding term root is 977106... and proposition id is 2c0d4c...
L37
Axiom. (abs_SNo_dist_swap) We take the following as an axiom:
∀x y, SNo x → SNo y → abs_SNo (x + - y) = abs_SNo (y + - x)
In Proofgold the corresponding term root is 73d709... and proposition id is fd708c...
L38
Axiom. (SNo_triangle) We take the following as an axiom:
∀x y, SNo x → SNo y → abs_SNo (x + y) ≤ abs_SNo x + abs_SNo y
In Proofgold the corresponding term root is f7ed3b... and proposition id is db0357...
L39
Axiom. (SNo_triangle2) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → abs_SNo (x + - z) ≤ abs_SNo (x + - y) + abs_SNo (y + - z)
In Proofgold the corresponding term root is d54ddd... and proposition id is 8a76af...
End of Section SurrealAbs
Beginning of Section SNoMaxMin
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 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use ≤ as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
L49
Definition. We define SNo_max_of to be λX x ⇒ x ∈ X ∧ SNo x ∧ ∀y ∈ X, SNo y → y ≤ x of type set → set → prop.
In Proofgold the corresponding term root is 9570d4... and object id is 0e9f0e...
L50
Definition. We define SNo_min_of to be λX x ⇒ x ∈ X ∧ SNo x ∧ ∀y ∈ X, SNo y → x ≤ y of type set → set → prop.
In Proofgold the corresponding term root is 5eb8d7... and object id is 144946...
L51
Axiom. (minus_SNo_max_min) We take the following as an axiom:
∀X y, (∀x ∈ X, SNo x) → SNo_max_of X y → SNo_min_of {- x|x ∈ X} (- y)
In Proofgold the corresponding term root is 2403cf... and proposition id is f6c519...
L52
Axiom. (minus_SNo_max_min') We take the following as an axiom:
∀X y, (∀x ∈ X, SNo x) → SNo_max_of {- x|x ∈ X} y → SNo_min_of X (- y)
In Proofgold the corresponding term root is 544581... and proposition id is b07737...
L53
Axiom. (minus_SNo_min_max) We take the following as an axiom:
∀X y, (∀x ∈ X, SNo x) → SNo_min_of X y → SNo_max_of {- x|x ∈ X} (- y)
In Proofgold the corresponding term root is d435c2... and proposition id is fbf599...
L54
Axiom. (double_SNo_max_1) We take the following as an axiom:
∀x y, SNo x → SNo_max_of (SNoL x) y → ∀z, SNo z → x < z → y + z < x + x → ∃w ∈ SNoR z, y + w = x + x
In Proofgold the corresponding term root is 3155e8... and proposition id is d66034...
L55
Axiom. (double_SNo_min_1) We take the following as an axiom:
∀x y, SNo x → SNo_min_of (SNoR x) y → ∀z, SNo z → z < x → x + x < y + z → ∃w ∈ SNoL z, y + w = x + x
In Proofgold the corresponding term root is fa7d8b... and proposition id is 084f04...
L56
Axiom. (finite_max_exists) We take the following as an axiom:
∀X, (∀x ∈ X, SNo x) → finite X → X ≠ 0 → ∃x, SNo_max_of X x
In Proofgold the corresponding term root is 182021... and proposition id is 9baa0b...
L57
Axiom. (finite_min_exists) We take the following as an axiom:
∀X, (∀x ∈ X, SNo x) → finite X → X ≠ 0 → ∃x, SNo_min_of X x
In Proofgold the corresponding term root is efc9f1... and proposition id is 25808a...
L58
Axiom. (SNoS_omega_SNoL_max_exists) We take the following as an axiom:
∀x ∈ SNoS_ ω, SNoL x = 0 ∨ ∃y, SNo_max_of (SNoL x) y
In Proofgold the corresponding term root is 4539ed... and proposition id is faaae1...
L59
Axiom. (SNoS_omega_SNoR_min_exists) We take the following as an axiom:
∀x ∈ SNoS_ ω, SNoR x = 0 ∨ ∃y, SNo_min_of (SNoR x) y
In Proofgold the corresponding term root is b0aa0c... and proposition id is baaae8...
End of Section SNoMaxMin
Beginning of Section DiadicRationals
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 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use ≤ as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
L69
Axiom. (nonneg_diadic_rational_p_SNoS_omega) We take the following as an axiom:
∀k ∈ ω, ∀n, nat_p n → eps_ k * n ∈ SNoS_ ω
In Proofgold the corresponding term root is 9323b5... and proposition id is d9b318...
L70
Definition. We define diadic_rational_p to be λx ⇒ ∃k ∈ ω, ∃m ∈ int, x = eps_ k * m of type set → prop.
In Proofgold the corresponding term root is a02ca9... and object id is 25bca1...
L71
Axiom. (diadic_rational_p_SNoS_omega) We take the following as an axiom:
∀x, diadic_rational_p x → x ∈ SNoS_ ω
In Proofgold the corresponding term root is b7e7af... and proposition id is 3dea67...
L72
Axiom. (int_diadic_rational_p) We take the following as an axiom:
∀m ∈ int, diadic_rational_p m
In Proofgold the corresponding term root is 88ce9c... and proposition id is 8a4cf7...
L73
Axiom. (omega_diadic_rational_p) We take the following as an axiom:
∀m ∈ ω, diadic_rational_p m
In Proofgold the corresponding term root is 40b048... and proposition id is c250b0...
L74
Axiom. (eps_diadic_rational_p) We take the following as an axiom:
∀k ∈ ω, diadic_rational_p (eps_ k)
In Proofgold the corresponding term root is d306dc... and proposition id is cc1098...
L75
Axiom. (minus_SNo_diadic_rational_p) We take the following as an axiom:
∀x, diadic_rational_p x → diadic_rational_p (- x)
In Proofgold the corresponding term root is bb6f7d... and proposition id is bc4825...
L76
Axiom. (mul_SNo_diadic_rational_p) We take the following as an axiom:
∀x y, diadic_rational_p x → diadic_rational_p y → diadic_rational_p (x * y)
In Proofgold the corresponding term root is ed6a37... and proposition id is e4ff6e...
L77
Axiom. (add_SNo_diadic_rational_p) We take the following as an axiom:
∀x y, diadic_rational_p x → diadic_rational_p y → diadic_rational_p (x + y)
In Proofgold the corresponding term root is bd7ab2... and proposition id is 4e6254...
L78
Axiom. (SNoS_omega_diadic_rational_p_lem) We take the following as an axiom:
∀n, nat_p n → ∀x, SNo x → SNoLev x = n → diadic_rational_p x
In Proofgold the corresponding term root is 85a5ea... and proposition id is bf97d9...
L79
Axiom. (SNoS_omega_diadic_rational_p) We take the following as an axiom:
∀x ∈ SNoS_ ω, diadic_rational_p x
In Proofgold the corresponding term root is a9c764... and proposition id is 963bd5...
L80
Axiom. (mul_SNo_SNoS_omega) We take the following as an axiom:
∀x y ∈ SNoS_ ω, x * y ∈ SNoS_ ω
In Proofgold the corresponding term root is d17aa1... and proposition id is 768371...
End of Section DiadicRationals