Primitive. The name Eps_i is a term of type (setprop)set.
Axiom. (Eps_i_ax) We take the following as an axiom:
∀P : setprop, ∀x : set, P xP (Eps_i P)
Definition. We define True to be ∀p : prop, pp of type prop.
Definition. We define False to be ∀p : prop, p of type prop.
Definition. We define not to be λA : propAFalse of type propprop.
Notation. We use ¬ as a prefix operator with priority 700 corresponding to applying term not.
Definition. We define and to be λA B : prop∀p : prop, (ABp)p of type proppropprop.
Notation. We use as an infix operator with priority 780 and which associates to the left corresponding to applying term and.
Definition. We define or to be λA B : prop∀p : prop, (Ap)(Bp)p of type proppropprop.
Notation. We use as an infix operator with priority 785 and which associates to the left corresponding to applying term or.
Definition. We define iff to be λA B : propand (AB) (BA) of type proppropprop.
Notation. We use as an infix operator with priority 805 and no associativity corresponding to applying term iff.
Beginning of Section Eq
Variable A : SType
Definition. We define eq to be λx y : A∀Q : AAprop, Q x yQ y x of type AAprop.
Definition. We define neq to be λx y : A¬ eq x y of type AAprop.
End of Section Eq
Notation. We use = as an infix operator with priority 502 and no associativity corresponding to applying term eq.
Notation. We use as an infix operator with priority 502 and no associativity corresponding to applying term neq.
Beginning of Section FE
Variable A B : SType
Axiom. (func_ext) We take the following as an axiom:
∀f g : AB, (∀x : A, f x = g x)f = g
End of Section FE
Beginning of Section Ex
Variable A : SType
Definition. We define ex to be λQ : Aprop∀P : prop, (∀x : A, Q xP)P of type (Aprop)prop.
End of Section Ex
Notation. We use x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using ex.
Axiom. (prop_ext) We take the following as an axiom:
∀p q : prop, iff p qp = q
Primitive. The name In is a term of type setsetprop.
Notation. We use as an infix operator with priority 500 and no associativity corresponding to applying term In. Furthermore, we may write xA, B to mean x : set, xAB.
Definition. We define Subq to be λA B ⇒ xA, x B of type setsetprop.
Notation. We use as an infix operator with priority 500 and no associativity corresponding to applying term Subq. Furthermore, we may write xA, B to mean x : set, xAB.
Axiom. (set_ext) We take the following as an axiom:
∀X Y : set, X YY XX = Y
Axiom. (In_ind) We take the following as an axiom:
∀P : setprop, (∀X : set, (xX, P x)P X)∀X : set, P X
Notation. We use x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using ex and handling ∈ or ⊆ ascriptions using and.
Primitive. The name Empty is a term of type set.
Axiom. (EmptyAx) We take the following as an axiom:
¬ x : set, x Empty
Primitive. The name is a term of type setset.
Axiom. (UnionEq) We take the following as an axiom:
∀X x, x X Y, x Y Y X
Primitive. The name 𝒫 is a term of type setset.
Axiom. (PowerEq) We take the following as an axiom:
∀X Y : set, Y 𝒫 X Y X
Primitive. The name Repl is a term of type set(setset)set.
Notation. {B| xA} is notation for Repl Ax . B).
Axiom. (ReplEq) We take the following as an axiom:
∀A : set, ∀F : setset, ∀y : set, y {F x|xA} xA, y = F x
Definition. We define TransSet to be λU : setxU, x U of type setprop.
Definition. We define Union_closed to be λU : set∀X : set, X U X U of type setprop.
Definition. We define Power_closed to be λU : set∀X : set, X U𝒫 X U of type setprop.
Definition. We define Repl_closed to be λU : set∀X : set, X U∀F : setset, (∀x : set, x XF x U){F x|xX} U of type setprop.
Definition. We define ZF_closed to be λU : setUnion_closed U Power_closed U Repl_closed U of type setprop.
Primitive. The name UnivOf is a term of type setset.
Axiom. (UnivOf_In) We take the following as an axiom:
∀N : set, N UnivOf N
Axiom. (UnivOf_TransSet) We take the following as an axiom:
∀N : set, TransSet (UnivOf N)
Axiom. (UnivOf_ZF_closed) We take the following as an axiom:
∀N : set, ZF_closed (UnivOf N)
Axiom. (UnivOf_Min) We take the following as an axiom:
∀N U : set, N UTransSet UZF_closed UUnivOf N U
Axiom. (FalseE) We take the following as an axiom:
False∀p : prop, p
Axiom. (TrueI) We take the following as an axiom:
True
Axiom. (andI) We take the following as an axiom:
∀A B : prop, ABA B
Axiom. (andEL) We take the following as an axiom:
∀A B : prop, A BA
Axiom. (andER) We take the following as an axiom:
∀A B : prop, A BB
Axiom. (orIL) We take the following as an axiom:
∀A B : prop, AA B
Axiom. (orIR) We take the following as an axiom:
∀A B : prop, BA B
Beginning of Section PropN
Variable P1 P2 P3 : prop
Axiom. (and3I) We take the following as an axiom:
P1P2P3P1 P2 P3
Axiom. (and3E) We take the following as an axiom:
P1 P2 P3(∀p : prop, (P1P2P3p)p)
Axiom. (or3I1) We take the following as an axiom:
P1P1 P2 P3
Axiom. (or3I2) We take the following as an axiom:
P2P1 P2 P3
Axiom. (or3I3) We take the following as an axiom:
P3P1 P2 P3
Axiom. (or3E) We take the following as an axiom:
P1 P2 P3(∀p : prop, (P1p)(P2p)(P3p)p)
Variable P4 : prop
Axiom. (and4I) We take the following as an axiom:
P1P2P3P4P1 P2 P3 P4
Variable P5 : prop
Axiom. (and5I) We take the following as an axiom:
P1P2P3P4P5P1 P2 P3 P4 P5
End of Section PropN
Axiom. (not_or_and_demorgan) We take the following as an axiom:
∀A B : prop, ¬ (A B)¬ A ¬ B
Axiom. (not_ex_all_demorgan_i) We take the following as an axiom:
∀P : setprop, (¬ x, P x)∀x, ¬ P x
Axiom. (iffI) We take the following as an axiom:
∀A B : prop, (AB)(BA)(A B)
Axiom. (iffEL) We take the following as an axiom:
∀A B : prop, (A B)AB
Axiom. (iffER) We take the following as an axiom:
∀A B : prop, (A B)BA
Axiom. (iff_refl) We take the following as an axiom:
∀A : prop, A A
Axiom. (iff_sym) We take the following as an axiom:
∀A B : prop, (A B)(B A)
Axiom. (iff_trans) We take the following as an axiom:
∀A B C : prop, (A B)(B C)(A C)
Axiom. (eq_i_tra) We take the following as an axiom:
∀x y z, x = yy = zx = z
Axiom. (f_eq_i) We take the following as an axiom:
∀f : setset, ∀x y, x = yf x = f y
Axiom. (neq_i_sym) We take the following as an axiom:
∀x y, x yy x
Definition. We define nIn to be λx X ⇒ ¬ In x X of type setsetprop.
Notation. We use as an infix operator with priority 502 and no associativity corresponding to applying term nIn.
Axiom. (Eps_i_ex) We take the following as an axiom:
∀P : setprop, (x, P x)P (Eps_i P)
Axiom. (pred_ext) We take the following as an axiom:
∀P Q : setprop, (∀x, P x Q x)P = Q
Axiom. (prop_ext_2) We take the following as an axiom:
∀p q : prop, (pq)(qp)p = q
Axiom. (Subq_ref) We take the following as an axiom:
∀X : set, X X
Axiom. (Subq_tra) We take the following as an axiom:
∀X Y Z : set, X YY ZX Z
Axiom. (Subq_contra) We take the following as an axiom:
∀X Y z : set, X Yz Yz X
Axiom. (EmptyE) We take the following as an axiom:
∀x : set, x Empty
Axiom. (Subq_Empty) We take the following as an axiom:
∀X : set, Empty X
Axiom. (Empty_Subq_eq) We take the following as an axiom:
∀X : set, X EmptyX = Empty
Axiom. (Empty_eq) We take the following as an axiom:
∀X : set, (∀x, x X)X = Empty
Axiom. (UnionI) We take the following as an axiom:
∀X x Y : set, x YY Xx X
Axiom. (UnionE) We take the following as an axiom:
∀X x : set, x XY : set, x Y Y X
Axiom. (UnionE_impred) We take the following as an axiom:
∀X x : set, x X∀p : prop, (∀Y : set, x YY Xp)p
Axiom. (PowerI) We take the following as an axiom:
∀X Y : set, Y XY 𝒫 X
Axiom. (PowerE) We take the following as an axiom:
∀X Y : set, Y 𝒫 XY X
Axiom. (Empty_In_Power) We take the following as an axiom:
∀X : set, Empty 𝒫 X
Axiom. (Self_In_Power) We take the following as an axiom:
∀X : set, X 𝒫 X
Axiom. (xm) We take the following as an axiom:
∀P : prop, P ¬ P
Axiom. (dneg) We take the following as an axiom:
∀P : prop, ¬ ¬ PP
Axiom. (not_all_ex_demorgan_i) We take the following as an axiom:
∀P : setprop, ¬ (∀x, P x)x, ¬ P x
Axiom. (eq_or_nand) We take the following as an axiom:
or = (λx y : prop¬ (¬ x ¬ y))
Primitive. The name exactly1of2 is a term of type proppropprop.
Axiom. (exactly1of2_I1) We take the following as an axiom:
∀A B : prop, A¬ Bexactly1of2 A B
Axiom. (exactly1of2_I2) We take the following as an axiom:
∀A B : prop, ¬ ABexactly1of2 A B
Axiom. (exactly1of2_E) We take the following as an axiom:
∀A B : prop, exactly1of2 A B∀p : prop, (A¬ Bp)(¬ ABp)p
Axiom. (exactly1of2_or) We take the following as an axiom:
∀A B : prop, exactly1of2 A BA B
Axiom. (ReplI) We take the following as an axiom:
∀A : set, ∀F : setset, ∀x : set, x AF x {F x|xA}
Axiom. (ReplE) We take the following as an axiom:
∀A : set, ∀F : setset, ∀y : set, y {F x|xA}xA, y = F x
Axiom. (ReplE_impred) We take the following as an axiom:
∀A : set, ∀F : setset, ∀y : set, y {F x|xA}∀p : prop, (∀x : set, x Ay = F xp)p
Axiom. (ReplE') We take the following as an axiom:
∀X, ∀f : setset, ∀p : setprop, (xX, p (f x))y{f x|xX}, p y
Axiom. (Repl_Empty) We take the following as an axiom:
∀F : setset, {F x|xEmpty} = Empty
Axiom. (ReplEq_ext_sub) We take the following as an axiom:
∀X, ∀F G : setset, (xX, F x = G x){F x|xX} {G x|xX}
Axiom. (ReplEq_ext) We take the following as an axiom:
∀X, ∀F G : setset, (xX, F x = G x){F x|xX} = {G x|xX}
Axiom. (Repl_inv_eq) We take the following as an axiom:
∀P : setprop, ∀f g : setset, (∀x, P xg (f x) = x)∀X, (xX, P x){g y|y{f x|xX}} = X
Axiom. (Repl_invol_eq) We take the following as an axiom:
∀P : setprop, ∀f : setset, (∀x, P xf (f x) = x)∀X, (xX, P x){f y|y{f x|xX}} = X
Primitive. The name If_i is a term of type propsetsetset.
Notation. if cond then T else E is notation corresponding to If_i type cond T E where type is the inferred type of T.
Axiom. (If_i_correct) We take the following as an axiom:
∀p : prop, ∀x y : set, p (if p then x else y) = x ¬ p (if p then x else y) = y
Axiom. (If_i_0) We take the following as an axiom:
∀p : prop, ∀x y : set, ¬ p(if p then x else y) = y
Axiom. (If_i_1) We take the following as an axiom:
∀p : prop, ∀x y : set, p(if p then x else y) = x
Axiom. (If_i_or) We take the following as an axiom:
∀p : prop, ∀x y : set, (if p then x else y) = x (if p then x else y) = y
Primitive. The name UPair is a term of type setsetset.
Notation. {x,y} is notation for UPair x y.
Axiom. (UPairE) We take the following as an axiom:
∀x y z : set, x {y,z}x = y x = z
Axiom. (UPairI1) We take the following as an axiom:
∀y z : set, y {y,z}
Axiom. (UPairI2) We take the following as an axiom:
∀y z : set, z {y,z}
Primitive. The name Sing is a term of type setset.
Notation. {x} is notation for Sing x.
Axiom. (SingI) We take the following as an axiom:
∀x : set, x {x}
Axiom. (SingE) We take the following as an axiom:
∀x y : set, y {x}y = x
Primitive. The name binunion is a term of type setsetset.
Notation. We use as an infix operator with priority 345 and which associates to the left corresponding to applying term binunion.
Axiom. (binunionI1) We take the following as an axiom:
∀X Y z : set, z Xz X Y
Axiom. (binunionI2) We take the following as an axiom:
∀X Y z : set, z Yz X Y
Axiom. (binunionE) We take the following as an axiom:
∀X Y z : set, z X Yz X z Y
Axiom. (binunionE') We take the following as an axiom:
∀X Y z, ∀p : prop, (z Xp)(z Yp)(z X Yp)
Axiom. (binunion_asso) We take the following as an axiom:
∀X Y Z : set, X (Y Z) = (X Y) Z
Axiom. (binunion_com_Subq) We take the following as an axiom:
∀X Y : set, X Y Y X
Axiom. (binunion_com) We take the following as an axiom:
∀X Y : set, X Y = Y X
Axiom. (binunion_idl) We take the following as an axiom:
∀X : set, Empty X = X
Axiom. (binunion_idr) We take the following as an axiom:
∀X : set, X Empty = X
Axiom. (binunion_Subq_1) We take the following as an axiom:
∀X Y : set, X X Y
Axiom. (binunion_Subq_2) We take the following as an axiom:
∀X Y : set, Y X Y
Axiom. (binunion_Subq_min) We take the following as an axiom:
∀X Y Z : set, X ZY ZX Y Z
Axiom. (Subq_binunion_eq) We take the following as an axiom:
∀X Y, (X Y) = (X Y = Y)
Definition. We define SetAdjoin to be λX y ⇒ X {y} of type setsetset.
Notation. We now use the set enumeration notation {...,...,...} in general. If 0 elements are given, then Empty is used to form the corresponding term. If 1 element is given, then Sing is used to form the corresponding term. If 2 elements are given, then UPair is used to form the corresponding term. If more than elements are given, then SetAdjoin is used to reduce to the case with one fewer elements.
Primitive. The name famunion is a term of type set(setset)set.
Notation. We use x [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using famunion.
Axiom. (famunionI) We take the following as an axiom:
∀X : set, ∀F : (setset), ∀x y : set, x Xy F xy xXF x
Axiom. (famunionE) We take the following as an axiom:
∀X : set, ∀F : (setset), ∀y : set, y (xXF x)xX, y F x
Axiom. (famunionE_impred) We take the following as an axiom:
∀X : set, ∀F : (setset), ∀y : set, y (xXF x)∀p : prop, (∀x, x Xy F xp)p
Axiom. (famunion_Empty) We take the following as an axiom:
∀F : setset, (xEmptyF x) = Empty
Beginning of Section SepSec
Variable X : set
Variable P : setprop
Let z : setEps_i (λz ⇒ z X P z)
Let F : setsetλx ⇒ if P x then x else z
Primitive. The name Sep is a term of type set.
End of Section SepSec
Notation. {xA | B} is notation for Sep Ax . B).
Axiom. (SepI) We take the following as an axiom:
∀X : set, ∀P : (setprop), ∀x : set, x XP xx {xX|P x}
Axiom. (SepE) We take the following as an axiom:
∀X : set, ∀P : (setprop), ∀x : set, x {xX|P x}x X P x
Axiom. (SepE1) We take the following as an axiom:
∀X : set, ∀P : (setprop), ∀x : set, x {xX|P x}x X
Axiom. (SepE2) We take the following as an axiom:
∀X : set, ∀P : (setprop), ∀x : set, x {xX|P x}P x
Axiom. (Sep_Subq) We take the following as an axiom:
∀X : set, ∀P : setprop, {xX|P x} X
Axiom. (Sep_In_Power) We take the following as an axiom:
∀X : set, ∀P : setprop, {xX|P x} 𝒫 X
Primitive. The name ReplSep is a term of type set(setprop)(setset)set.
Notation. {B| xA, C} is notation for ReplSep Ax . C) (λ x . B).
Axiom. (ReplSepI) We take the following as an axiom:
∀X : set, ∀P : setprop, ∀F : setset, ∀x : set, x XP xF x {F x|xX, P x}
Axiom. (ReplSepE) We take the following as an axiom:
∀X : set, ∀P : setprop, ∀F : setset, ∀y : set, y {F x|xX, P x}x : set, x X P x y = F x
Axiom. (ReplSepE_impred) We take the following as an axiom:
∀X : set, ∀P : setprop, ∀F : setset, ∀y : set, y {F x|xX, P x}∀p : prop, (xX, P xy = F xp)p
Primitive. The name binintersect is a term of type setsetset.
Notation. We use as an infix operator with priority 340 and which associates to the left corresponding to applying term binintersect.
Axiom. (binintersectI) We take the following as an axiom:
∀X Y z, z Xz Yz X Y
Axiom. (binintersectE) We take the following as an axiom:
∀X Y z, z X Yz X z Y
Axiom. (binintersectE1) We take the following as an axiom:
∀X Y z, z X Yz X
Axiom. (binintersectE2) We take the following as an axiom:
∀X Y z, z X Yz Y
Axiom. (binintersect_Subq_1) We take the following as an axiom:
∀X Y : set, X Y X
Axiom. (binintersect_Subq_2) We take the following as an axiom:
∀X Y : set, X Y Y
Axiom. (binintersect_Subq_eq_1) We take the following as an axiom:
∀X Y, X YX Y = X
Axiom. (binintersect_Subq_max) We take the following as an axiom:
∀X Y Z : set, Z XZ YZ X Y
Axiom. (binintersect_com_Subq) We take the following as an axiom:
∀X Y : set, X Y Y X
Axiom. (binintersect_com) We take the following as an axiom:
∀X Y : set, X Y = Y X
Primitive. The name setminus is a term of type setsetset.
Notation. We use as an infix operator with priority 350 and no associativity corresponding to applying term setminus.
Axiom. (setminusI) We take the following as an axiom:
∀X Y z, (z X)(z Y)z X Y
Axiom. (setminusE) We take the following as an axiom:
∀X Y z, (z X Y)z X z Y
Axiom. (setminusE1) We take the following as an axiom:
∀X Y z, (z X Y)z X
Axiom. (setminusE2) We take the following as an axiom:
∀X Y z, (z X Y)z Y
Axiom. (setminus_Subq) We take the following as an axiom:
∀X Y : set, X Y X
Axiom. (setminus_Subq_contra) We take the following as an axiom:
∀X Y Z : set, Z YX Y X Z
Axiom. (setminus_In_Power) We take the following as an axiom:
∀A U, A U 𝒫 A
Axiom. (In_irref) We take the following as an axiom:
∀x, x x
Axiom. (In_no2cycle) We take the following as an axiom:
∀x y, x yy xFalse
Primitive. The name ordsucc is a term of type setset.
Axiom. (ordsuccI1) We take the following as an axiom:
∀x : set, x ordsucc x
Axiom. (ordsuccI2) We take the following as an axiom:
∀x : set, x ordsucc x
Axiom. (ordsuccE) We take the following as an axiom:
∀x y : set, y ordsucc xy x y = x
Notation. Natural numbers 0,1,2,... are notation for the terms formed using Empty as 0 and forming successors with ordsucc.
Axiom. (neq_0_ordsucc) We take the following as an axiom:
∀a : set, 0 ordsucc a
Axiom. (neq_ordsucc_0) We take the following as an axiom:
∀a : set, ordsucc a 0
Axiom. (ordsucc_inj) We take the following as an axiom:
∀a b : set, ordsucc a = ordsucc ba = b
Axiom. (ordsucc_inj_contra) We take the following as an axiom:
∀a b : set, a bordsucc a ordsucc b
Axiom. (In_0_1) We take the following as an axiom:
0 1
Axiom. (In_0_2) We take the following as an axiom:
0 2
Axiom. (In_1_2) We take the following as an axiom:
1 2
Definition. We define nat_p to be λn : set∀p : setprop, p 0(∀x : set, p xp (ordsucc x))p n of type setprop.
Axiom. (nat_0) We take the following as an axiom:
nat_p 0
Axiom. (nat_ordsucc) We take the following as an axiom:
∀n : set, nat_p nnat_p (ordsucc n)
Axiom. (nat_1) We take the following as an axiom:
nat_p 1
Axiom. (nat_2) We take the following as an axiom:
nat_p 2
Axiom. (nat_0_in_ordsucc) We take the following as an axiom:
∀n, nat_p n0 ordsucc n
Axiom. (nat_ordsucc_in_ordsucc) We take the following as an axiom:
∀n, nat_p nmn, ordsucc m ordsucc n
Axiom. (nat_ind) We take the following as an axiom:
∀p : setprop, p 0(∀n, nat_p np np (ordsucc n))∀n, nat_p np n
Axiom. (nat_inv_impred) We take the following as an axiom:
∀p : setprop, p 0(∀n, nat_p np (ordsucc n))∀n, nat_p np n
Axiom. (nat_inv) We take the following as an axiom:
∀n, nat_p nn = 0 x, nat_p x n = ordsucc x
Axiom. (nat_complete_ind) We take the following as an axiom:
∀p : setprop, (∀n, nat_p n(mn, p m)p n)∀n, nat_p np n
Axiom. (nat_p_trans) We take the following as an axiom:
∀n, nat_p nmn, nat_p m
Axiom. (nat_trans) We take the following as an axiom:
∀n, nat_p nmn, m n
Axiom. (nat_ordsucc_trans) We take the following as an axiom:
∀n, nat_p nmordsucc n, m n
Axiom. (Union_ordsucc_eq) We take the following as an axiom:
∀n, nat_p n (ordsucc n) = n
Axiom. (cases_1) We take the following as an axiom:
i1, ∀p : setprop, p 0p i
Axiom. (cases_2) We take the following as an axiom:
i2, ∀p : setprop, p 0p 1p i
Axiom. (cases_3) We take the following as an axiom:
i3, ∀p : setprop, p 0p 1p 2p i
Axiom. (neq_0_1) We take the following as an axiom:
0 1
Axiom. (neq_1_0) We take the following as an axiom:
1 0
Axiom. (neq_0_2) We take the following as an axiom:
0 2
Axiom. (neq_2_0) We take the following as an axiom:
2 0
Axiom. (neq_1_2) We take the following as an axiom:
1 2
Axiom. (ZF_closed_E) We take the following as an axiom:
∀U, ZF_closed U∀p : prop, (Union_closed UPower_closed URepl_closed Up)p
Axiom. (ZF_Union_closed) We take the following as an axiom:
∀U, ZF_closed UXU, X U
Axiom. (ZF_Power_closed) We take the following as an axiom:
∀U, ZF_closed UXU, 𝒫 X U
Axiom. (ZF_Repl_closed) We take the following as an axiom:
∀U, ZF_closed UXU, ∀F : setset, (xX, F x U){F x|xX} U
Axiom. (ZF_UPair_closed) We take the following as an axiom:
∀U, ZF_closed Ux yU, {x,y} U
Axiom. (ZF_Sing_closed) We take the following as an axiom:
∀U, ZF_closed UxU, {x} U
Axiom. (ZF_binunion_closed) We take the following as an axiom:
∀U, ZF_closed UX YU, (X Y) U
Axiom. (ZF_ordsucc_closed) We take the following as an axiom:
∀U, ZF_closed UxU, ordsucc x U
Axiom. (nat_p_UnivOf_Empty) We take the following as an axiom:
∀n : set, nat_p nn UnivOf Empty
Primitive. The name ω is a term of type set.
Axiom. (omega_nat_p) We take the following as an axiom:
nω, nat_p n
Axiom. (nat_p_omega) We take the following as an axiom:
∀n : set, nat_p nn ω
Axiom. (omega_ordsucc) We take the following as an axiom:
nω, ordsucc n ω
Definition. We define ordinal to be λalpha : setTransSet alpha betaalpha, TransSet beta of type setprop.
Axiom. (ordinal_TransSet) We take the following as an axiom:
∀alpha : set, ordinal alphaTransSet alpha
Axiom. (ordinal_Empty) We take the following as an axiom:
ordinal Empty
Axiom. (ordinal_Hered) We take the following as an axiom:
∀alpha : set, ordinal alphabetaalpha, ordinal beta
Axiom. (TransSet_ordsucc) We take the following as an axiom:
∀X : set, TransSet XTransSet (ordsucc X)
Axiom. (ordinal_ordsucc) We take the following as an axiom:
∀alpha : set, ordinal alphaordinal (ordsucc alpha)
Axiom. (nat_p_ordinal) We take the following as an axiom:
∀n : set, nat_p nordinal n
Axiom. (ordinal_1) We take the following as an axiom:
ordinal 1
Axiom. (ordinal_2) We take the following as an axiom:
ordinal 2
Axiom. (omega_TransSet) We take the following as an axiom:
TransSet ω
Axiom. (omega_ordinal) We take the following as an axiom:
ordinal ω
Axiom. (ordsucc_omega_ordinal) We take the following as an axiom:
ordinal (ordsucc ω)
Axiom. (TransSet_ordsucc_In_Subq) We take the following as an axiom:
∀X : set, TransSet XxX, ordsucc x X
Axiom. (ordinal_ordsucc_In_Subq) We take the following as an axiom:
∀alpha, ordinal alphabetaalpha, ordsucc beta alpha
Axiom. (ordinal_trichotomy_or) We take the following as an axiom:
∀alpha beta : set, ordinal alphaordinal betaalpha beta alpha = beta beta alpha
Axiom. (ordinal_trichotomy_or_impred) We take the following as an axiom:
∀alpha beta : set, ordinal alphaordinal beta∀p : prop, (alpha betap)(alpha = betap)(beta alphap)p
Axiom. (ordinal_In_Or_Subq) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaalpha beta beta alpha
Axiom. (ordinal_linear) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaalpha beta beta alpha
Axiom. (ordinal_ordsucc_In_eq) We take the following as an axiom:
∀alpha beta, ordinal alphabeta alphaordsucc beta alpha alpha = ordsucc beta
Axiom. (ordinal_lim_or_succ) We take the following as an axiom:
∀alpha, ordinal alpha(betaalpha, ordsucc beta alpha) (betaalpha, alpha = ordsucc beta)
Axiom. (ordinal_ordsucc_In) We take the following as an axiom:
∀alpha, ordinal alphabetaalpha, ordsucc beta ordsucc alpha
Axiom. (ordinal_famunion) We take the following as an axiom:
∀X, ∀F : setset, (xX, ordinal (F x))ordinal (xXF x)
Axiom. (ordinal_binintersect) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaordinal (alpha beta)
Axiom. (ordinal_binunion) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaordinal (alpha beta)
Axiom. (ordinal_ind) We take the following as an axiom:
∀p : setprop, (∀alpha, ordinal alpha(betaalpha, p beta)p alpha)∀alpha, ordinal alphap alpha
Axiom. (least_ordinal_ex) We take the following as an axiom:
∀p : setprop, (alpha, ordinal alpha p alpha)alpha, ordinal alpha p alpha betaalpha, ¬ p beta
Definition. We define inj to be λX Y f ⇒ (uX, f u Y) (u vX, f u = f vu = v) of type setset(setset)prop.
Definition. We define bij to be λX Y f ⇒ (uX, f u Y) (u vX, f u = f vu = v) (wY, uX, f u = w) of type setset(setset)prop.
Axiom. (bijI) We take the following as an axiom:
∀X Y, ∀f : setset, (uX, f u Y)(u vX, f u = f vu = v)(wY, uX, f u = w)bij X Y f
Axiom. (bijE) We take the following as an axiom:
∀X Y, ∀f : setset, bij X Y f∀p : prop, ((uX, f u Y)(u vX, f u = f vu = v)(wY, uX, f u = w)p)p
Primitive. The name inv is a term of type set(setset)setset.
Axiom. (surj_rinv) We take the following as an axiom:
∀X Y, ∀f : setset, (wY, uX, f u = w)yY, inv X f y X f (inv X f y) = y
Axiom. (inj_linv) We take the following as an axiom:
∀X, ∀f : setset, (u vX, f u = f vu = v)xX, inv X f (f x) = x
Axiom. (bij_inv) We take the following as an axiom:
∀X Y, ∀f : setset, bij X Y fbij Y X (inv X f)
Axiom. (bij_id) We take the following as an axiom:
∀X, bij X X (λx ⇒ x)
Axiom. (bij_comp) We take the following as an axiom:
∀X Y Z : set, ∀f g : setset, bij X Y fbij Y Z gbij X Z (λx ⇒ g (f x))
Definition. We define equip to be λX Y : setf : setset, bij X Y f of type setsetprop.
Axiom. (equip_ref) We take the following as an axiom:
∀X, equip X X
Axiom. (equip_sym) We take the following as an axiom:
∀X Y, equip X Yequip Y X
Axiom. (equip_tra) We take the following as an axiom:
∀X Y Z, equip X Yequip Y Zequip X Z
Axiom. (equip_0_Empty) We take the following as an axiom:
∀X, equip X 0X = 0
Beginning of Section SchroederBernstein
Axiom. (KnasterTarski_set) We take the following as an axiom:
∀A, ∀F : setset, (U𝒫 A, F U 𝒫 A)(U V𝒫 A, U VF U F V)Y𝒫 A, F Y = Y
Axiom. (image_In_Power) We take the following as an axiom:
∀A B, ∀f : setset, (xA, f x B)U𝒫 A, {f x|xU} 𝒫 B
Axiom. (image_monotone) We take the following as an axiom:
∀f : setset, ∀U V, U V{f x|xU} {f x|xV}
Axiom. (setminus_antimonotone) We take the following as an axiom:
∀A U V, U VA V A U
Axiom. (SchroederBernstein) We take the following as an axiom:
∀A B, ∀f g : setset, inj A B finj B A gequip A B
End of Section SchroederBernstein
Beginning of Section PigeonHole
Axiom. (PigeonHole_nat) We take the following as an axiom:
∀n, nat_p n∀f : setset, (iordsucc n, f i n)¬ (i jordsucc n, f i = f ji = j)
Axiom. (PigeonHole_nat_bij) We take the following as an axiom:
∀n, nat_p n∀f : setset, (in, f i n)(i jn, f i = f ji = j)bij n n f
End of Section PigeonHole
Definition. We define finite to be λX ⇒ nω, equip X n of type setprop.
Axiom. (finite_ind) We take the following as an axiom:
∀p : setprop, p Empty(∀X y, finite Xy Xp Xp (X {y}))∀X, finite Xp X
Axiom. (finite_Empty) We take the following as an axiom:
finite 0
Axiom. (adjoin_finite) We take the following as an axiom:
∀X y, finite Xfinite (X {y})
Axiom. (binunion_finite) We take the following as an axiom:
∀X, finite X∀Y, finite Yfinite (X Y)
Axiom. (famunion_nat_finite) We take the following as an axiom:
∀X : setset, ∀n, nat_p n(in, finite (X i))finite (inX i)
Axiom. (Subq_finite) We take the following as an axiom:
∀X, finite X∀Y, Y Xfinite Y
Axiom. (TransSet_In_ordsucc_Subq) We take the following as an axiom:
∀x y, TransSet yx ordsucc yx y
Axiom. (exandE_i) We take the following as an axiom:
∀P Q : setprop, (x, P x Q x)∀r : prop, (∀x, P xQ xr)r
Axiom. (exandE_ii) We take the following as an axiom:
∀P Q : (setset)prop, (x : setset, P x Q x)∀p : prop, (∀x : setset, P xQ xp)p
Axiom. (exandE_iii) We take the following as an axiom:
∀P Q : (setsetset)prop, (x : setsetset, P x Q x)∀p : prop, (∀x : setsetset, P xQ xp)p
Axiom. (exandE_iiii) We take the following as an axiom:
∀P Q : (setsetsetset)prop, (x : setsetsetset, P x Q x)∀p : prop, (∀x : setsetsetset, P xQ xp)p
Beginning of Section Descr_ii
Variable P : (setset)prop
Primitive. The name Descr_ii is a term of type setset.
Hypothesis Pex : f : setset, P f
Hypothesis Puniq : ∀f g : setset, P fP gf = g
Axiom. (Descr_ii_prop) We take the following as an axiom:
End of Section Descr_ii
Beginning of Section Descr_iii
Variable P : (setsetset)prop
Primitive. The name Descr_iii is a term of type setsetset.
Hypothesis Pex : f : setsetset, P f
Hypothesis Puniq : ∀f g : setsetset, P fP gf = g
Axiom. (Descr_iii_prop) We take the following as an axiom:
End of Section Descr_iii
Beginning of Section Descr_Vo1
Variable P : Vo 1prop
Primitive. The name Descr_Vo1 is a term of type Vo 1.
Hypothesis Pex : f : Vo 1, P f
Hypothesis Puniq : ∀f g : Vo 1, P fP gf = g
Axiom. (Descr_Vo1_prop) We take the following as an axiom:
End of Section Descr_Vo1
Beginning of Section If_ii
Variable p : prop
Variable f g : setset
Primitive. The name If_ii is a term of type setset.
Axiom. (If_ii_1) We take the following as an axiom:
pIf_ii = f
Axiom. (If_ii_0) We take the following as an axiom:
¬ pIf_ii = g
End of Section If_ii
Beginning of Section If_iii
Variable p : prop
Variable f g : setsetset
Primitive. The name If_iii is a term of type setsetset.
Axiom. (If_iii_1) We take the following as an axiom:
pIf_iii = f
Axiom. (If_iii_0) We take the following as an axiom:
¬ pIf_iii = g
End of Section If_iii
Beginning of Section EpsilonRec_i
Variable F : set(setset)set
Primitive. The name In_rec_i is a term of type setset.
Hypothesis Fr : ∀X : set, ∀g h : setset, (xX, g x = h x)F X g = F X h
Axiom. (In_rec_i_eq) We take the following as an axiom:
∀X : set, In_rec_i X = F X In_rec_i
End of Section EpsilonRec_i
Beginning of Section EpsilonRec_ii
Variable F : set(set(setset))(setset)
Primitive. The name In_rec_ii is a term of type set(setset).
Hypothesis Fr : ∀X : set, ∀g h : set(setset), (xX, g x = h x)F X g = F X h
Axiom. (In_rec_ii_eq) We take the following as an axiom:
∀X : set, In_rec_ii X = F X In_rec_ii
End of Section EpsilonRec_ii
Beginning of Section EpsilonRec_iii
Variable F : set(set(setsetset))(setsetset)
Primitive. The name In_rec_iii is a term of type set(setsetset).
Hypothesis Fr : ∀X : set, ∀g h : set(setsetset), (xX, g x = h x)F X g = F X h
Axiom. (In_rec_iii_eq) We take the following as an axiom:
∀X : set, In_rec_iii X = F X In_rec_iii
End of Section EpsilonRec_iii
Beginning of Section NatRec
Variable z : set
Variable f : setsetset
Let F : set(setset)setλn g ⇒ if n n then f ( n) (g ( n)) else z
Definition. We define nat_primrec to be In_rec_i F of type setset.
Axiom. (nat_primrec_r) We take the following as an axiom:
∀X : set, ∀g h : setset, (xX, g x = h x)F X g = F X h
Axiom. (nat_primrec_0) We take the following as an axiom:
Axiom. (nat_primrec_S) We take the following as an axiom:
∀n : set, nat_p nnat_primrec (ordsucc n) = f n (nat_primrec n)
End of Section NatRec
Beginning of Section NatArith
Definition. We define add_nat to be λn m : setnat_primrec n (λ_ r ⇒ ordsucc r) m of type setsetset.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_nat.
Axiom. (add_nat_0R) We take the following as an axiom:
∀n : set, n + 0 = n
Axiom. (add_nat_SR) We take the following as an axiom:
∀n m : set, nat_p mn + ordsucc m = ordsucc (n + m)
Axiom. (add_nat_p) We take the following as an axiom:
∀n : set, nat_p n∀m : set, nat_p mnat_p (n + m)
Axiom. (add_nat_1_1_2) We take the following as an axiom:
1 + 1 = 2
Axiom. (add_nat_0L) We take the following as an axiom:
∀m : set, nat_p m0 + m = m
Axiom. (add_nat_SL) We take the following as an axiom:
∀n : set, nat_p n∀m : set, nat_p mordsucc n + m = ordsucc (n + m)
Axiom. (add_nat_com) We take the following as an axiom:
∀n : set, nat_p n∀m : set, nat_p mn + m = m + n
Axiom. (nat_Subq_add_ex) We take the following as an axiom:
∀n, nat_p n∀m, nat_p mn mk, nat_p k m = k + n
Definition. We define mul_nat to be λn m : setnat_primrec 0 (λ_ r ⇒ n + r) m of type setsetset.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_nat.
Axiom. (mul_nat_0R) We take the following as an axiom:
∀n : set, n * 0 = 0
Axiom. (mul_nat_SR) We take the following as an axiom:
∀n m : set, nat_p mn * ordsucc m = n + n * m
Axiom. (mul_nat_p) We take the following as an axiom:
∀n : set, nat_p n∀m : set, nat_p mnat_p (n * m)
End of Section NatArith
Definition. We define Inj1 to be In_rec_i (λX f ⇒ {0} {f x|xX}) of type setset.
Axiom. (Inj1_eq) We take the following as an axiom:
∀X : set, Inj1 X = {0} {Inj1 x|xX}
Axiom. (Inj1I1) We take the following as an axiom:
∀X : set, 0 Inj1 X
Axiom. (Inj1I2) We take the following as an axiom:
∀X x : set, x XInj1 x Inj1 X
Axiom. (Inj1E) We take the following as an axiom:
∀X y : set, y Inj1 Xy = 0 xX, y = Inj1 x
Axiom. (Inj1NE1) We take the following as an axiom:
∀x : set, Inj1 x 0
Axiom. (Inj1NE2) We take the following as an axiom:
∀x : set, Inj1 x {0}
Definition. We define Inj0 to be λX ⇒ {Inj1 x|xX} of type setset.
Axiom. (Inj0I) We take the following as an axiom:
∀X x : set, x XInj1 x Inj0 X
Axiom. (Inj0E) We take the following as an axiom:
∀X y : set, y Inj0 Xx : set, x X y = Inj1 x
Definition. We define Unj to be In_rec_i (λX f ⇒ {f x|xX {0}}) of type setset.
Axiom. (Unj_eq) We take the following as an axiom:
∀X : set, Unj X = {Unj x|xX {0}}
Axiom. (Unj_Inj1_eq) We take the following as an axiom:
∀X : set, Unj (Inj1 X) = X
Axiom. (Inj1_inj) We take the following as an axiom:
∀X Y : set, Inj1 X = Inj1 YX = Y
Axiom. (Unj_Inj0_eq) We take the following as an axiom:
∀X : set, Unj (Inj0 X) = X
Axiom. (Inj0_inj) We take the following as an axiom:
∀X Y : set, Inj0 X = Inj0 YX = Y
Axiom. (Inj0_0) We take the following as an axiom:
Inj0 0 = 0
Axiom. (Inj0_Inj1_neq) We take the following as an axiom:
∀X Y : set, Inj0 X Inj1 Y
Definition. We define setsum to be λX Y ⇒ {Inj0 x|xX} {Inj1 y|yY} of type setsetset.
Notation. We use + as an infix operator with priority 450 and which associates to the left corresponding to applying term setsum.
Axiom. (Inj0_setsum) We take the following as an axiom:
∀X Y x : set, x XInj0 x X + Y
Axiom. (Inj1_setsum) We take the following as an axiom:
∀X Y y : set, y YInj1 y X + Y
Axiom. (setsum_Inj_inv) We take the following as an axiom:
∀X Y z : set, z X + Y(xX, z = Inj0 x) (yY, z = Inj1 y)
Axiom. (Inj0_setsum_0L) We take the following as an axiom:
∀X : set, 0 + X = Inj0 X
Axiom. (Subq_1_Sing0) We take the following as an axiom:
1 {0}
Axiom. (eq_1_Sing0) We take the following as an axiom:
1 = {0}
Axiom. (Inj1_setsum_1L) We take the following as an axiom:
∀X : set, 1 + X = Inj1 X
Axiom. (nat_setsum1_ordsucc) We take the following as an axiom:
∀n : set, nat_p n1 + n = ordsucc n
Axiom. (setsum_0_0) We take the following as an axiom:
0 + 0 = 0
Axiom. (setsum_1_0_1) We take the following as an axiom:
1 + 0 = 1
Axiom. (setsum_1_1_2) We take the following as an axiom:
1 + 1 = 2
Beginning of Section pair_setsum
Let pair ≝ setsum
Definition. We define proj0 to be λZ ⇒ {Unj z|zZ, x : set, Inj0 x = z} of type setset.
Definition. We define proj1 to be λZ ⇒ {Unj z|zZ, y : set, Inj1 y = z} of type setset.
Axiom. (Inj0_pair_0_eq) We take the following as an axiom:
Inj0 = pair 0
Axiom. (Inj1_pair_1_eq) We take the following as an axiom:
Inj1 = pair 1
Axiom. (pairI0) We take the following as an axiom:
∀X Y x, x Xpair 0 x pair X Y
Axiom. (pairI1) We take the following as an axiom:
∀X Y y, y Ypair 1 y pair X Y
Axiom. (pairE) We take the following as an axiom:
∀X Y z, z pair X Y(xX, z = pair 0 x) (yY, z = pair 1 y)
Axiom. (pairE0) We take the following as an axiom:
∀X Y x, pair 0 x pair X Yx X
Axiom. (pairE1) We take the following as an axiom:
∀X Y y, pair 1 y pair X Yy Y
Axiom. (proj0I) We take the following as an axiom:
∀w u : set, pair 0 u wu proj0 w
Axiom. (proj0E) We take the following as an axiom:
∀w u : set, u proj0 wpair 0 u w
Axiom. (proj1I) We take the following as an axiom:
∀w u : set, pair 1 u wu proj1 w
Axiom. (proj1E) We take the following as an axiom:
∀w u : set, u proj1 wpair 1 u w
Axiom. (proj0_pair_eq) We take the following as an axiom:
∀X Y : set, proj0 (pair X Y) = X
Axiom. (proj1_pair_eq) We take the following as an axiom:
∀X Y : set, proj1 (pair X Y) = Y
Definition. We define Sigma to be λX Y ⇒ xX{pair x y|yY x} of type set(setset)set.
Notation. We use x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Sigma.
Axiom. (pair_Sigma) We take the following as an axiom:
∀X : set, ∀Y : setset, xX, yY x, pair x y xX, Y x
Axiom. (Sigma_eta_proj0_proj1) We take the following as an axiom:
∀X : set, ∀Y : setset, z(xX, Y x), pair (proj0 z) (proj1 z) = z proj0 z X proj1 z Y (proj0 z)
Axiom. (proj_Sigma_eta) We take the following as an axiom:
∀X : set, ∀Y : setset, z(xX, Y x), pair (proj0 z) (proj1 z) = z
Axiom. (proj0_Sigma) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)proj0 z X
Axiom. (proj1_Sigma) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)proj1 z Y (proj0 z)
Axiom. (pair_Sigma_E1) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀x y : set, pair x y (xX, Y x)y Y x
Axiom. (Sigma_E) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)xX, yY x, z = pair x y
Definition. We define setprod to be λX Y : setxX, Y of type setsetset.
Notation. We use as an infix operator with priority 440 and which associates to the left corresponding to applying term setprod.
Let lam : set(setset)setSigma
Definition. We define ap to be λf x ⇒ {proj1 z|zf, y : set, z = pair x y} of type setsetset.
Notation. When x is a set, a term x y is notation for ap x y.
Notation. λ xAB is notation for the set Sigma Ax : set ⇒ B).
Notation. We now use n-tuple notation (a0,...,an-1) for n ≥ 2 for λ i ∈ n . if i = 0 then a0 else ... if i = n-2 then an-2 else an-1.
Axiom. (lamI) We take the following as an axiom:
∀X : set, ∀F : setset, xX, yF x, pair x y λxX F x
Axiom. (lamE) We take the following as an axiom:
∀X : set, ∀F : setset, ∀z : set, z (λxX F x)xX, yF x, z = pair x y
Axiom. (apI) We take the following as an axiom:
∀f x y, pair x y fy f x
Axiom. (apE) We take the following as an axiom:
∀f x y, y f xpair x y f
Axiom. (beta) We take the following as an axiom:
∀X : set, ∀F : setset, ∀x : set, x X(λxX F x) x = F x
Axiom. (proj0_ap_0) We take the following as an axiom:
∀u, proj0 u = u 0
Axiom. (proj1_ap_1) We take the following as an axiom:
∀u, proj1 u = u 1
Axiom. (pair_ap_0) We take the following as an axiom:
∀x y : set, (pair x y) 0 = x
Axiom. (pair_ap_1) We take the following as an axiom:
∀x y : set, (pair x y) 1 = y
Axiom. (ap0_Sigma) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)(z 0) X
Axiom. (ap1_Sigma) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀z : set, z (xX, Y x)(z 1) (Y (z 0))
Definition. We define pair_p to be λu : setpair (u 0) (u 1) = u of type setprop.
Axiom. (pair_p_I) We take the following as an axiom:
∀x y, pair_p (pair x y)
Axiom. (Subq_2_UPair01) We take the following as an axiom:
Axiom. (tuple_pair) We take the following as an axiom:
∀x y : set, pair x y = (x,y)
Definition. We define Pi to be λX Y ⇒ {f𝒫 (xX, (Y x))|xX, f x Y x} of type set(setset)set.
Notation. We use x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Pi.
Axiom. (PiI) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀f : set, (uf, pair_p u u 0 X)(xX, f x Y x)f xX, Y x
Axiom. (lam_Pi) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀F : setset, (xX, F x Y x)(λxX F x) (xX, Y x)
Axiom. (ap_Pi) We take the following as an axiom:
∀X : set, ∀Y : setset, ∀f : set, ∀x : set, f (xX, Y x)x Xf x Y x
Definition. We define setexp to be λX Y : setyY, X of type setsetset.
Notation. We use :^: as an infix operator with priority 430 and which associates to the left corresponding to applying term setexp.
Axiom. (pair_tuple_fun) We take the following as an axiom:
pair = (λx y ⇒ (x,y))
Axiom. (lamI2) We take the following as an axiom:
∀X, ∀F : setset, xX, yF x, (x,y) λxX F x
Beginning of Section Tuples
Variable x0 x1 : set
Axiom. (tuple_2_0_eq) We take the following as an axiom:
(x0,x1) 0 = x0
Axiom. (tuple_2_1_eq) We take the following as an axiom:
(x0,x1) 1 = x1
End of Section Tuples
Axiom. (ReplEq_setprod_ext) We take the following as an axiom:
∀X Y, ∀F G : setsetset, (xX, yY, F x y = G x y){F (w 0) (w 1)|wX Y} = {G (w 0) (w 1)|wX Y}
Axiom. (tuple_2_Sigma) We take the following as an axiom:
∀X : set, ∀Y : setset, xX, yY x, (x,y) xX, Y x
Axiom. (tuple_2_setprod) We take the following as an axiom:
∀X : set, ∀Y : set, xX, yY, (x,y) X Y
End of Section pair_setsum
Notation. We use x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Sigma.
Notation. We use as an infix operator with priority 440 and which associates to the left corresponding to applying term setprod.
Notation. We use x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Pi.
Notation. We use :^: as an infix operator with priority 430 and which associates to the left corresponding to applying term setexp.
Primitive. The name DescrR_i_io_1 is a term of type (set(setprop)prop)set.
Primitive. The name DescrR_i_io_2 is a term of type (set(setprop)prop)setprop.
Axiom. (DescrR_i_io_12) We take the following as an axiom:
∀R : set(setprop)prop, (x, (y : setprop, R x y) (∀y z : setprop, R x yR x zy = z))R (DescrR_i_io_1 R) (DescrR_i_io_2 R)
Definition. We define PNoEq_ to be λalpha p q ⇒ betaalpha, p beta q beta of type set(setprop)(setprop)prop.
Axiom. (PNoEq_ref_) We take the following as an axiom:
∀alpha, ∀p : setprop, PNoEq_ alpha p p
Axiom. (PNoEq_sym_) We take the following as an axiom:
∀alpha, ∀p q : setprop, PNoEq_ alpha p qPNoEq_ alpha q p
Axiom. (PNoEq_tra_) We take the following as an axiom:
∀alpha, ∀p q r : setprop, PNoEq_ alpha p qPNoEq_ alpha q rPNoEq_ alpha p r
Axiom. (PNoEq_antimon_) We take the following as an axiom:
∀p q : setprop, ∀alpha, ordinal alphabetaalpha, PNoEq_ alpha p qPNoEq_ beta p q
Definition. We define PNoLt_ to be λalpha p q ⇒ betaalpha, PNoEq_ beta p q ¬ p beta q beta of type set(setprop)(setprop)prop.
Axiom. (PNoLt_E_) We take the following as an axiom:
∀alpha, ∀p q : setprop, PNoLt_ alpha p q∀R : prop, (∀beta, beta alphaPNoEq_ beta p q¬ p betaq betaR)R
Axiom. (PNoLt_irref_) We take the following as an axiom:
∀alpha, ∀p : setprop, ¬ PNoLt_ alpha p p
Axiom. (PNoLt_mon_) We take the following as an axiom:
∀p q : setprop, ∀alpha, ordinal alphabetaalpha, PNoLt_ beta p qPNoLt_ alpha p q
Axiom. (PNoLt_trichotomy_or_) We take the following as an axiom:
∀p q : setprop, ∀alpha, ordinal alphaPNoLt_ alpha p q PNoEq_ alpha p q PNoLt_ alpha q p
Axiom. (PNoLt_tra_) We take the following as an axiom:
∀alpha, ordinal alpha∀p q r : setprop, PNoLt_ alpha p qPNoLt_ alpha q rPNoLt_ alpha p r
Primitive. The name PNoLt is a term of type set(setprop)set(setprop)prop.
Axiom. (PNoLtI1) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, PNoLt_ (alpha beta) p qPNoLt alpha p beta q
Axiom. (PNoLtI2) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, alpha betaPNoEq_ alpha p qq alphaPNoLt alpha p beta q
Axiom. (PNoLtI3) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, beta alphaPNoEq_ beta p q¬ p betaPNoLt alpha p beta q
Axiom. (PNoLtE) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, PNoLt alpha p beta q∀R : prop, (PNoLt_ (alpha beta) p qR)(alpha betaPNoEq_ alpha p qq alphaR)(beta alphaPNoEq_ beta p q¬ p betaR)R
Axiom. (PNoLt_irref) We take the following as an axiom:
∀alpha, ∀p : setprop, ¬ PNoLt alpha p alpha p
Axiom. (PNoLt_trichotomy_or) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, ordinal alphaordinal betaPNoLt alpha p beta q alpha = beta PNoEq_ alpha p q PNoLt beta q alpha p
Axiom. (PNoLtEq_tra) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal beta∀p q r : setprop, PNoLt alpha p beta qPNoEq_ beta q rPNoLt alpha p beta r
Axiom. (PNoEqLt_tra) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal beta∀p q r : setprop, PNoEq_ alpha p qPNoLt alpha q beta rPNoLt alpha p beta r
Axiom. (PNoLt_tra) We take the following as an axiom:
∀alpha beta gamma, ordinal alphaordinal betaordinal gamma∀p q r : setprop, PNoLt alpha p beta qPNoLt beta q gamma rPNoLt alpha p gamma r
Definition. We define PNoLe to be λalpha p beta q ⇒ PNoLt alpha p beta q alpha = beta PNoEq_ alpha p q of type set(setprop)set(setprop)prop.
Axiom. (PNoLeI1) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, PNoLt alpha p beta qPNoLe alpha p beta q
Axiom. (PNoLeI2) We take the following as an axiom:
∀alpha, ∀p q : setprop, PNoEq_ alpha p qPNoLe alpha p alpha q
Axiom. (PNoLe_ref) We take the following as an axiom:
∀alpha, ∀p : setprop, PNoLe alpha p alpha p
Axiom. (PNoLe_antisym) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal beta∀p q : setprop, PNoLe alpha p beta qPNoLe beta q alpha palpha = beta PNoEq_ alpha p q
Axiom. (PNoLtLe_tra) We take the following as an axiom:
∀alpha beta gamma, ordinal alphaordinal betaordinal gamma∀p q r : setprop, PNoLt alpha p beta qPNoLe beta q gamma rPNoLt alpha p gamma r
Axiom. (PNoLeLt_tra) We take the following as an axiom:
∀alpha beta gamma, ordinal alphaordinal betaordinal gamma∀p q r : setprop, PNoLe alpha p beta qPNoLt beta q gamma rPNoLt alpha p gamma r
Axiom. (PNoEqLe_tra) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal beta∀p q r : setprop, PNoEq_ alpha p qPNoLe alpha q beta rPNoLe alpha p beta r
Axiom. (PNoLe_tra) We take the following as an axiom:
∀alpha beta gamma, ordinal alphaordinal betaordinal gamma∀p q r : setprop, PNoLe alpha p beta qPNoLe beta q gamma rPNoLe alpha p gamma r
Definition. We define PNo_downc to be λL alpha p ⇒ beta, ordinal beta q : setprop, L beta q PNoLe alpha p beta q of type (set(setprop)prop)set(setprop)prop.
Definition. We define PNo_upc to be λR alpha p ⇒ beta, ordinal beta q : setprop, R beta q PNoLe beta q alpha p of type (set(setprop)prop)set(setprop)prop.
Axiom. (PNoLe_downc) We take the following as an axiom:
∀L : set(setprop)prop, ∀alpha beta, ∀p q : setprop, ordinal alphaordinal betaPNo_downc L alpha pPNoLe beta q alpha pPNo_downc L beta q
Axiom. (PNo_downc_ref) We take the following as an axiom:
∀L : set(setprop)prop, ∀alpha, ordinal alpha∀p : setprop, L alpha pPNo_downc L alpha p
Axiom. (PNo_upc_ref) We take the following as an axiom:
∀R : set(setprop)prop, ∀alpha, ordinal alpha∀p : setprop, R alpha pPNo_upc R alpha p
Axiom. (PNoLe_upc) We take the following as an axiom:
∀R : set(setprop)prop, ∀alpha beta, ∀p q : setprop, ordinal alphaordinal betaPNo_upc R alpha pPNoLe alpha p beta qPNo_upc R beta q
Definition. We define PNoLt_pwise to be λL R ⇒ ∀gamma, ordinal gamma∀p : setprop, L gamma p∀delta, ordinal delta∀q : setprop, R delta qPNoLt gamma p delta q of type (set(setprop)prop)(set(setprop)prop)prop.
Axiom. (PNoLt_pwise_downc_upc) We take the following as an axiom:
∀L R : set(setprop)prop, PNoLt_pwise L RPNoLt_pwise (PNo_downc L) (PNo_upc R)
Definition. We define PNo_rel_strict_upperbd to be λL alpha p ⇒ betaalpha, ∀q : setprop, PNo_downc L beta qPNoLt beta q alpha p of type (set(setprop)prop)set(setprop)prop.
Definition. We define PNo_rel_strict_lowerbd to be λR alpha p ⇒ betaalpha, ∀q : setprop, PNo_upc R beta qPNoLt alpha p beta q of type (set(setprop)prop)set(setprop)prop.
Definition. We define PNo_rel_strict_imv to be λL R alpha p ⇒ PNo_rel_strict_upperbd L alpha p PNo_rel_strict_lowerbd R alpha p of type (set(setprop)prop)(set(setprop)prop)set(setprop)prop.
Axiom. (PNoEq_rel_strict_upperbd) We take the following as an axiom:
∀L : set(setprop)prop, ∀alpha, ordinal alpha∀p q : setprop, PNoEq_ alpha p qPNo_rel_strict_upperbd L alpha pPNo_rel_strict_upperbd L alpha q
Axiom. (PNo_rel_strict_upperbd_antimon) We take the following as an axiom:
∀L : set(setprop)prop, ∀alpha, ordinal alpha∀p : setprop, betaalpha, PNo_rel_strict_upperbd L alpha pPNo_rel_strict_upperbd L beta p
Axiom. (PNoEq_rel_strict_lowerbd) We take the following as an axiom:
∀R : set(setprop)prop, ∀alpha, ordinal alpha∀p q : setprop, PNoEq_ alpha p qPNo_rel_strict_lowerbd R alpha pPNo_rel_strict_lowerbd R alpha q
Axiom. (PNo_rel_strict_lowerbd_antimon) We take the following as an axiom:
∀R : set(setprop)prop, ∀alpha, ordinal alpha∀p : setprop, betaalpha, PNo_rel_strict_lowerbd R alpha pPNo_rel_strict_lowerbd R beta p
Axiom. (PNoEq_rel_strict_imv) We take the following as an axiom:
∀L R : set(setprop)prop, ∀alpha, ordinal alpha∀p q : setprop, PNoEq_ alpha p qPNo_rel_strict_imv L R alpha pPNo_rel_strict_imv L R alpha q
Axiom. (PNo_rel_strict_imv_antimon) We take the following as an axiom:
∀L R : set(setprop)prop, ∀alpha, ordinal alpha∀p : setprop, betaalpha, PNo_rel_strict_imv L R alpha pPNo_rel_strict_imv L R beta p
Definition. We define PNo_rel_strict_uniq_imv to be λL R alpha p ⇒ PNo_rel_strict_imv L R alpha p ∀q : setprop, PNo_rel_strict_imv L R alpha qPNoEq_ alpha p q of type (set(setprop)prop)(set(setprop)prop)set(setprop)prop.
Definition. We define PNo_rel_strict_split_imv to be λL R alpha p ⇒ PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta delta alpha) PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta delta = alpha) of type (set(setprop)prop)(set(setprop)prop)set(setprop)prop.
Axiom. (PNo_extend0_eq) We take the following as an axiom:
∀alpha, ∀p : setprop, PNoEq_ alpha p (λdelta ⇒ p delta delta alpha)
Axiom. (PNo_extend1_eq) We take the following as an axiom:
∀alpha, ∀p : setprop, PNoEq_ alpha p (λdelta ⇒ p delta delta = alpha)
Axiom. (PNo_rel_imv_ex) We take the following as an axiom:
∀L R : set(setprop)prop, PNoLt_pwise L R∀alpha, ordinal alpha(p : setprop, PNo_rel_strict_uniq_imv L R alpha p) (taualpha, p : setprop, PNo_rel_strict_split_imv L R tau p)
Definition. We define PNo_lenbdd to be λalpha L ⇒ ∀beta, ∀p : setprop, L beta pbeta alpha of type set(set(setprop)prop)prop.
Axiom. (PNo_lenbdd_strict_imv_extend0) We take the following as an axiom:
∀L R : set(setprop)prop, ∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha R∀p : setprop, PNo_rel_strict_imv L R alpha pPNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta delta alpha)
Axiom. (PNo_lenbdd_strict_imv_extend1) We take the following as an axiom:
∀L R : set(setprop)prop, ∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha R∀p : setprop, PNo_rel_strict_imv L R alpha pPNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta delta = alpha)
Axiom. (PNo_lenbdd_strict_imv_split) We take the following as an axiom:
∀L R : set(setprop)prop, ∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha R∀p : setprop, PNo_rel_strict_imv L R alpha pPNo_rel_strict_split_imv L R alpha p
Axiom. (PNo_rel_imv_bdd_ex) We take the following as an axiom:
∀L R : set(setprop)prop, PNoLt_pwise L R∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha Rbetaordsucc alpha, p : setprop, PNo_rel_strict_split_imv L R beta p
Definition. We define PNo_strict_upperbd to be λL alpha p ⇒ ∀beta, ordinal beta∀q : setprop, L beta qPNoLt beta q alpha p of type (set(setprop)prop)set(setprop)prop.
Definition. We define PNo_strict_lowerbd to be λR alpha p ⇒ ∀beta, ordinal beta∀q : setprop, R beta qPNoLt alpha p beta q of type (set(setprop)prop)set(setprop)prop.
Definition. We define PNo_strict_imv to be λL R alpha p ⇒ PNo_strict_upperbd L alpha p PNo_strict_lowerbd R alpha p of type (set(setprop)prop)(set(setprop)prop)set(setprop)prop.
Axiom. (PNoEq_strict_upperbd) We take the following as an axiom:
∀L : set(setprop)prop, ∀alpha, ordinal alpha∀p q : setprop, PNoEq_ alpha p qPNo_strict_upperbd L alpha pPNo_strict_upperbd L alpha q
Axiom. (PNoEq_strict_lowerbd) We take the following as an axiom:
∀R : set(setprop)prop, ∀alpha, ordinal alpha∀p q : setprop, PNoEq_ alpha p qPNo_strict_lowerbd R alpha pPNo_strict_lowerbd R alpha q
Axiom. (PNoEq_strict_imv) We take the following as an axiom:
∀L R : set(setprop)prop, ∀alpha, ordinal alpha∀p q : setprop, PNoEq_ alpha p qPNo_strict_imv L R alpha pPNo_strict_imv L R alpha q
Axiom. (PNo_strict_upperbd_imp_rel_strict_upperbd) We take the following as an axiom:
∀L : set(setprop)prop, ∀alpha, ordinal alphabetaordsucc alpha, ∀p : setprop, PNo_strict_upperbd L alpha pPNo_rel_strict_upperbd L beta p
Axiom. (PNo_strict_lowerbd_imp_rel_strict_lowerbd) We take the following as an axiom:
∀R : set(setprop)prop, ∀alpha, ordinal alphabetaordsucc alpha, ∀p : setprop, PNo_strict_lowerbd R alpha pPNo_rel_strict_lowerbd R beta p
Axiom. (PNo_strict_imv_imp_rel_strict_imv) We take the following as an axiom:
∀L R : set(setprop)prop, ∀alpha, ordinal alphabetaordsucc alpha, ∀p : setprop, PNo_strict_imv L R alpha pPNo_rel_strict_imv L R beta p
Axiom. (PNo_rel_split_imv_imp_strict_imv) We take the following as an axiom:
∀L R : set(setprop)prop, ∀alpha, ordinal alpha∀p : setprop, PNo_rel_strict_split_imv L R alpha pPNo_strict_imv L R alpha p
Axiom. (PNo_lenbdd_strict_imv_ex) We take the following as an axiom:
∀L R : set(setprop)prop, PNoLt_pwise L R∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha Rbetaordsucc alpha, p : setprop, PNo_strict_imv L R beta p
Definition. We define PNo_least_rep to be λL R beta p ⇒ ordinal beta PNo_strict_imv L R beta p gammabeta, ∀q : setprop, ¬ PNo_strict_imv L R gamma q of type (set(setprop)prop)(set(setprop)prop)set(setprop)prop.
Definition. We define PNo_least_rep2 to be λL R beta p ⇒ PNo_least_rep L R beta p ∀x, x beta¬ p x of type (set(setprop)prop)(set(setprop)prop)set(setprop)prop.
Axiom. (PNo_strict_imv_pred_eq) We take the following as an axiom:
∀L R : set(setprop)prop, PNoLt_pwise L R∀alpha, ordinal alpha∀p q : setprop, PNo_least_rep L R alpha pPNo_strict_imv L R alpha qbetaalpha, p beta q beta
Axiom. (PNo_lenbdd_least_rep2_exuniq2) We take the following as an axiom:
∀L R : set(setprop)prop, PNoLt_pwise L R∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha Rbeta, (p : setprop, PNo_least_rep2 L R beta p) (∀p q : setprop, PNo_least_rep2 L R beta pPNo_least_rep2 L R beta qp = q)
Primitive. The name PNo_bd is a term of type (set(setprop)prop)(set(setprop)prop)set.
Primitive. The name PNo_pred is a term of type (set(setprop)prop)(set(setprop)prop)setprop.
Axiom. (PNo_bd_pred_lem) We take the following as an axiom:
∀L R : set(setprop)prop, PNoLt_pwise L R∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha RPNo_least_rep2 L R (PNo_bd L R) (PNo_pred L R)
Axiom. (PNo_bd_pred) We take the following as an axiom:
∀L R : set(setprop)prop, PNoLt_pwise L R∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha RPNo_least_rep L R (PNo_bd L R) (PNo_pred L R)
Axiom. (PNo_bd_In) We take the following as an axiom:
∀L R : set(setprop)prop, PNoLt_pwise L R∀alpha, ordinal alphaPNo_lenbdd alpha LPNo_lenbdd alpha RPNo_bd L R ordsucc alpha
Beginning of Section TaggedSets
Let tag : setsetλalpha ⇒ SetAdjoin alpha {1}
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.
Axiom. (not_TransSet_Sing1) We take the following as an axiom:
Axiom. (not_ordinal_Sing1) We take the following as an axiom:
Axiom. (tagged_not_ordinal) We take the following as an axiom:
∀y, ¬ ordinal (y ')
Axiom. (tagged_notin_ordinal) We take the following as an axiom:
∀alpha y, ordinal alpha(y ') alpha
Axiom. (tagged_eqE_Subq) We take the following as an axiom:
∀alpha beta, ordinal alphaalpha ' = beta 'alpha beta
Axiom. (tagged_eqE_eq) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaalpha ' = beta 'alpha = beta
Axiom. (tagged_ReplE) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betabeta ' {gamma '|gammaalpha}beta alpha
Axiom. (ordinal_notin_tagged_Repl) We take the following as an axiom:
∀alpha Y, ordinal alphaalpha {y '|yY}
Definition. We define SNoElts_ to be λalpha ⇒ alpha {beta '|betaalpha} of type setset.
Axiom. (SNoElts_mon) We take the following as an axiom:
∀alpha beta, alpha betaSNoElts_ alpha SNoElts_ beta
Definition. We define SNo_ to be λalpha x ⇒ x SNoElts_ alpha betaalpha, exactly1of2 (beta ' x) (beta x) of type setsetprop.
Definition. We define PSNo to be λalpha p ⇒ {betaalpha|p beta} {beta '|betaalpha, ¬ p beta} of type set(setprop)set.
Axiom. (PNoEq_PSNo) We take the following as an axiom:
∀alpha, ordinal alpha∀p : setprop, PNoEq_ alpha (λbeta ⇒ beta PSNo alpha p) p
Axiom. (SNo_PSNo) We take the following as an axiom:
∀alpha, ordinal alpha∀p : setprop, SNo_ alpha (PSNo alpha p)
Axiom. (SNo_PSNo_eta_) We take the following as an axiom:
∀alpha x, ordinal alphaSNo_ alpha xx = PSNo alpha (λbeta ⇒ beta x)
Primitive. The name SNo is a term of type setprop.
Axiom. (SNo_SNo) We take the following as an axiom:
∀alpha, ordinal alpha∀z, SNo_ alpha zSNo z
Primitive. The name SNoLev is a term of type setset.
Axiom. (SNoLev_uniq_Subq) We take the following as an axiom:
∀x alpha beta, ordinal alphaordinal betaSNo_ alpha xSNo_ beta xalpha beta
Axiom. (SNoLev_uniq) We take the following as an axiom:
∀x alpha beta, ordinal alphaordinal betaSNo_ alpha xSNo_ beta xalpha = beta
Axiom. (SNoLev_prop) We take the following as an axiom:
∀x, SNo xordinal (SNoLev x) SNo_ (SNoLev x) x
Axiom. (SNoLev_ordinal) We take the following as an axiom:
∀x, SNo xordinal (SNoLev x)
Axiom. (SNoLev_) We take the following as an axiom:
∀x, SNo xSNo_ (SNoLev x) x
Axiom. (SNo_PSNo_eta) We take the following as an axiom:
∀x, SNo xx = PSNo (SNoLev x) (λbeta ⇒ beta x)
Axiom. (SNoLev_PSNo) We take the following as an axiom:
∀alpha, ordinal alpha∀p : setprop, SNoLev (PSNo alpha p) = alpha
Axiom. (SNo_Subq) We take the following as an axiom:
∀x y, SNo xSNo ySNoLev x SNoLev y(alphaSNoLev x, alpha x alpha y)x y
Definition. We define SNoEq_ to be λalpha x y ⇒ PNoEq_ alpha (λbeta ⇒ beta x) (λbeta ⇒ beta y) of type setsetsetprop.
Axiom. (SNoEq_I) We take the following as an axiom:
∀alpha x y, (betaalpha, beta x beta y)SNoEq_ alpha x y
Axiom. (SNo_eq) We take the following as an axiom:
∀x y, SNo xSNo ySNoLev x = SNoLev ySNoEq_ (SNoLev x) x yx = y
End of Section TaggedSets
Definition. We define SNoLt to be λx y ⇒ PNoLt (SNoLev x) (λbeta ⇒ beta x) (SNoLev y) (λbeta ⇒ beta y) of type setsetprop.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Definition. We define SNoLe to be λx y ⇒ PNoLe (SNoLev x) (λbeta ⇒ beta x) (SNoLev y) (λbeta ⇒ beta y) of type setsetprop.
Notation. We use as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Axiom. (SNoLtLe) We take the following as an axiom:
∀x y, x < yx y
Axiom. (SNoLeE) We take the following as an axiom:
∀x y, SNo xSNo yx yx < y x = y
Axiom. (SNoEq_sym_) We take the following as an axiom:
∀alpha x y, SNoEq_ alpha x ySNoEq_ alpha y x
Axiom. (SNoEq_tra_) We take the following as an axiom:
∀alpha x y z, SNoEq_ alpha x ySNoEq_ alpha y zSNoEq_ alpha x z
Axiom. (SNoLtE) We take the following as an axiom:
∀x y, SNo xSNo yx < y∀p : prop, (∀z, SNo zSNoLev z SNoLev x SNoLev ySNoEq_ (SNoLev z) z xSNoEq_ (SNoLev z) z yx < zz < ySNoLev z xSNoLev z yp)(SNoLev x SNoLev ySNoEq_ (SNoLev x) x ySNoLev x yp)(SNoLev y SNoLev xSNoEq_ (SNoLev y) x ySNoLev y xp)p
Axiom. (SNoLtI2) We take the following as an axiom:
∀x y, SNoLev x SNoLev ySNoEq_ (SNoLev x) x ySNoLev x yx < y
Axiom. (SNoLtI3) We take the following as an axiom:
∀x y, SNoLev y SNoLev xSNoEq_ (SNoLev y) x ySNoLev y xx < y
Axiom. (SNoLt_irref) We take the following as an axiom:
∀x, ¬ SNoLt x x
Axiom. (SNoLt_trichotomy_or) We take the following as an axiom:
∀x y, SNo xSNo yx < y x = y y < x
Axiom. (SNoLt_trichotomy_or_impred) We take the following as an axiom:
∀x y, SNo xSNo y∀p : prop, (x < yp)(x = yp)(y < xp)p
Axiom. (SNoLt_tra) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx < yy < zx < z
Axiom. (SNoLe_ref) We take the following as an axiom:
∀x, SNoLe x x
Axiom. (SNoLe_antisym) We take the following as an axiom:
∀x y, SNo xSNo yx yy xx = y
Axiom. (SNoLtLe_tra) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx < yy zx < z
Axiom. (SNoLeLt_tra) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx yy < zx < z
Axiom. (SNoLe_tra) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx yy zx z
Axiom. (SNoLtLe_or) We take the following as an axiom:
∀x y, SNo xSNo yx < y y x
Axiom. (SNoLt_PSNo_PNoLt) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, ordinal alphaordinal betaPSNo alpha p < PSNo beta qPNoLt alpha p beta q
Axiom. (PNoLt_SNoLt_PSNo) We take the following as an axiom:
∀alpha beta, ∀p q : setprop, ordinal alphaordinal betaPNoLt alpha p beta qPSNo alpha p < PSNo beta q
Definition. We define SNoCut to be λL R ⇒ PSNo (PNo_bd (λalpha p ⇒ ordinal alpha PSNo alpha p L) (λalpha p ⇒ ordinal alpha PSNo alpha p R)) (PNo_pred (λalpha p ⇒ ordinal alpha PSNo alpha p L) (λalpha p ⇒ ordinal alpha PSNo alpha p R)) of type setsetset.
Definition. We define SNoCutP to be λL R ⇒ (xL, SNo x) (yR, SNo y) (xL, yR, x < y) of type setsetprop.
Axiom. (SNoCutP_SNoCut) We take the following as an axiom:
∀L R, SNoCutP L RSNo (SNoCut L R) SNoLev (SNoCut L R) ordsucc ((xLordsucc (SNoLev x)) (yRordsucc (SNoLev y))) (xL, x < SNoCut L R) (yR, SNoCut L R < y) (∀z, SNo z(xL, x < z)(yR, z < y)SNoLev (SNoCut L R) SNoLev z SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) z)
Axiom. (SNoCutP_SNoCut_impred) We take the following as an axiom:
∀L R, SNoCutP L R∀p : prop, (SNo (SNoCut L R)SNoLev (SNoCut L R) ordsucc ((xLordsucc (SNoLev x)) (yRordsucc (SNoLev y)))(xL, x < SNoCut L R)(yR, SNoCut L R < y)(∀z, SNo z(xL, x < z)(yR, z < y)SNoLev (SNoCut L R) SNoLev z SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) z)p)p
Axiom. (SNoCutP_L_0) We take the following as an axiom:
∀L, (xL, SNo x)SNoCutP L 0
Axiom. (SNoCutP_0_R) We take the following as an axiom:
∀R, (xR, SNo x)SNoCutP 0 R
Axiom. (SNoCutP_0_0) We take the following as an axiom:
SNoCutP 0 0
Definition. We define SNoS_ to be λalpha ⇒ {x𝒫 (SNoElts_ alpha)|betaalpha, SNo_ beta x} of type setset.
Axiom. (SNoS_E) We take the following as an axiom:
∀alpha, ordinal alphaxSNoS_ alpha, betaalpha, SNo_ beta x
Beginning of Section TaggedSets2
Let tag : setsetλalpha ⇒ SetAdjoin alpha {1}
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.
Axiom. (SNoS_I) We take the following as an axiom:
∀alpha, ordinal alpha∀x, betaalpha, SNo_ beta xx SNoS_ alpha
Axiom. (SNoS_I2) We take the following as an axiom:
∀x y, SNo xSNo ySNoLev x SNoLev yx SNoS_ (SNoLev y)
Axiom. (SNoS_Subq) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaalpha betaSNoS_ alpha SNoS_ beta
Axiom. (SNoLev_uniq2) We take the following as an axiom:
∀alpha, ordinal alpha∀x, SNo_ alpha xSNoLev x = alpha
Axiom. (SNoS_E2) We take the following as an axiom:
∀alpha, ordinal alphaxSNoS_ alpha, ∀p : prop, (SNoLev x alphaordinal (SNoLev x)SNo xSNo_ (SNoLev x) xp)p
Axiom. (SNoS_In_neq) We take the following as an axiom:
∀w, SNo wxSNoS_ (SNoLev w), x w
Axiom. (SNoS_SNoLev) We take the following as an axiom:
∀z, SNo zz SNoS_ (ordsucc (SNoLev z))
Definition. We define SNoL to be λz ⇒ {xSNoS_ (SNoLev z)|x < z} of type setset.
Definition. We define SNoR to be λz ⇒ {ySNoS_ (SNoLev z)|z < y} of type setset.
Axiom. (SNoCutP_SNoL_SNoR) We take the following as an axiom:
∀z, SNo zSNoCutP (SNoL z) (SNoR z)
Axiom. (SNoL_E) We take the following as an axiom:
∀x, SNo xwSNoL x, ∀p : prop, (SNo wSNoLev w SNoLev xw < xp)p
Axiom. (SNoR_E) We take the following as an axiom:
∀x, SNo xzSNoR x, ∀p : prop, (SNo zSNoLev z SNoLev xx < zp)p
Axiom. (SNoL_SNoS_) We take the following as an axiom:
∀z, SNoL z SNoS_ (SNoLev z)
Axiom. (SNoR_SNoS_) We take the following as an axiom:
∀z, SNoR z SNoS_ (SNoLev z)
Axiom. (SNoL_SNoS) We take the following as an axiom:
∀x, SNo xwSNoL x, w SNoS_ (SNoLev x)
Axiom. (SNoR_SNoS) We take the following as an axiom:
∀x, SNo xzSNoR x, z SNoS_ (SNoLev x)
Axiom. (SNoL_I) We take the following as an axiom:
∀z, SNo z∀x, SNo xSNoLev x SNoLev zx < zx SNoL z
Axiom. (SNoR_I) We take the following as an axiom:
∀z, SNo z∀y, SNo ySNoLev y SNoLev zz < yy SNoR z
Axiom. (SNo_eta) We take the following as an axiom:
∀z, SNo zz = SNoCut (SNoL z) (SNoR z)
Axiom. (SNoCutP_SNo_SNoCut) We take the following as an axiom:
∀L R, SNoCutP L RSNo (SNoCut L R)
Axiom. (SNoCutP_SNoCut_L) We take the following as an axiom:
∀L R, SNoCutP L RxL, x < SNoCut L R
Axiom. (SNoCutP_SNoCut_R) We take the following as an axiom:
∀L R, SNoCutP L RyR, SNoCut L R < y
Axiom. (SNoCutP_SNoCut_fst) We take the following as an axiom:
∀L R, SNoCutP L R∀z, SNo z(xL, x < z)(yR, z < y)SNoLev (SNoCut L R) SNoLev z SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) z
Axiom. (SNoCut_Le) We take the following as an axiom:
∀L1 R1 L2 R2, SNoCutP L1 R1SNoCutP L2 R2(wL1, w < SNoCut L2 R2)(zR2, SNoCut L1 R1 < z)SNoCut L1 R1 SNoCut L2 R2
Axiom. (SNoCut_ext) We take the following as an axiom:
∀L1 R1 L2 R2, SNoCutP L1 R1SNoCutP L2 R2(wL1, w < SNoCut L2 R2)(zR1, SNoCut L2 R2 < z)(wL2, w < SNoCut L1 R1)(zR2, SNoCut L1 R1 < z)SNoCut L1 R1 = SNoCut L2 R2
Axiom. (SNoLt_SNoL_or_SNoR_impred) We take the following as an axiom:
∀x y, SNo xSNo yx < y∀p : prop, (zSNoL y, z SNoR xp)(x SNoL yp)(y SNoR xp)p
Axiom. (SNoL_or_SNoR_impred) We take the following as an axiom:
∀x y, SNo xSNo y∀p : prop, (x = yp)(zSNoL y, z SNoR xp)(x SNoL yp)(y SNoR xp)(zSNoR y, z SNoL xp)(x SNoR yp)(y SNoL xp)p
Axiom. (ordinal_SNo_) We take the following as an axiom:
∀alpha, ordinal alphaSNo_ alpha alpha
Axiom. (ordinal_SNo) We take the following as an axiom:
∀alpha, ordinal alphaSNo alpha
Axiom. (ordinal_SNoLev) We take the following as an axiom:
∀alpha, ordinal alphaSNoLev alpha = alpha
Axiom. (ordinal_SNoLev_max) We take the following as an axiom:
∀alpha, ordinal alpha∀z, SNo zSNoLev z alphaz < alpha
Axiom. (ordinal_SNoL) We take the following as an axiom:
∀alpha, ordinal alphaSNoL alpha = SNoS_ alpha
Axiom. (ordinal_SNoR) We take the following as an axiom:
∀alpha, ordinal alphaSNoR alpha = Empty
Axiom. (nat_p_SNo) We take the following as an axiom:
∀n, nat_p nSNo n
Axiom. (omega_SNo) We take the following as an axiom:
Axiom. (omega_SNoS_omega) We take the following as an axiom:
Axiom. (ordinal_In_SNoLt) We take the following as an axiom:
∀alpha, ordinal alphabetaalpha, beta < alpha
Axiom. (ordinal_SNoLev_max_2) We take the following as an axiom:
∀alpha, ordinal alpha∀z, SNo zSNoLev z ordsucc alphaz alpha
Axiom. (ordinal_Subq_SNoLe) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaalpha betaalpha beta
Axiom. (ordinal_SNoLt_In) We take the following as an axiom:
∀alpha beta, ordinal alphaordinal betaalpha < betaalpha beta
Axiom. (omega_nonneg) We take the following as an axiom:
Axiom. (SNo_0) We take the following as an axiom:
Axiom. (SNo_1) We take the following as an axiom:
Axiom. (SNo_2) We take the following as an axiom:
Axiom. (SNoLev_0) We take the following as an axiom:
Axiom. (SNoCut_0_0) We take the following as an axiom:
Axiom. (SNoL_0) We take the following as an axiom:
Axiom. (SNoR_0) We take the following as an axiom:
Axiom. (SNoL_1) We take the following as an axiom:
Axiom. (SNoR_1) We take the following as an axiom:
Axiom. (SNo_max_SNoLev) We take the following as an axiom:
∀x, SNo x(ySNoS_ (SNoLev x), y < x)SNoLev x = x
Axiom. (SNo_max_ordinal) We take the following as an axiom:
∀x, SNo x(ySNoS_ (SNoLev x), y < x)ordinal x
Axiom. (pos_low_eq_one) We take the following as an axiom:
∀x, SNo x0 < xSNoLev x 1x = 1
Definition. We define SNo_extend0 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λdelta ⇒ delta x delta SNoLev x) of type setset.
Definition. We define SNo_extend1 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λdelta ⇒ delta x delta = SNoLev x) of type setset.
Axiom. (SNo_extend0_SNo_) We take the following as an axiom:
∀x, SNo xSNo_ (ordsucc (SNoLev x)) (SNo_extend0 x)
Axiom. (SNo_extend1_SNo_) We take the following as an axiom:
∀x, SNo xSNo_ (ordsucc (SNoLev x)) (SNo_extend1 x)
Axiom. (SNo_extend0_SNo) We take the following as an axiom:
∀x, SNo xSNo (SNo_extend0 x)
Axiom. (SNo_extend1_SNo) We take the following as an axiom:
∀x, SNo xSNo (SNo_extend1 x)
Axiom. (SNo_extend0_SNoLev) We take the following as an axiom:
∀x, SNo xSNoLev (SNo_extend0 x) = ordsucc (SNoLev x)
Axiom. (SNo_extend1_SNoLev) We take the following as an axiom:
∀x, SNo xSNoLev (SNo_extend1 x) = ordsucc (SNoLev x)
Axiom. (SNo_extend0_nIn) We take the following as an axiom:
∀x, SNo xSNoLev x SNo_extend0 x
Axiom. (SNo_extend1_In) We take the following as an axiom:
∀x, SNo xSNoLev x SNo_extend1 x
Axiom. (SNo_extend0_SNoEq) We take the following as an axiom:
∀x, SNo xSNoEq_ (SNoLev x) (SNo_extend0 x) x
Axiom. (SNo_extend1_SNoEq) We take the following as an axiom:
∀x, SNo xSNoEq_ (SNoLev x) (SNo_extend1 x) x
Axiom. (SNoLev_0_eq_0) We take the following as an axiom:
∀x, SNo xSNoLev x = 0x = 0
Definition. We define eps_ to be λn ⇒ {0} {(ordsucc m) '|mn} of type setset.
Axiom. (eps_ordinal_In_eq_0) We take the following as an axiom:
∀n alpha, ordinal alphaalpha eps_ nalpha = 0
Axiom. (eps_0_1) We take the following as an axiom:
Axiom. (SNo__eps_) We take the following as an axiom:
Axiom. (SNo_eps_) We take the following as an axiom:
Axiom. (SNo_eps_1) We take the following as an axiom:
Axiom. (SNoLev_eps_) We take the following as an axiom:
Axiom. (SNo_eps_SNoS_omega) We take the following as an axiom:
Axiom. (SNo_eps_decr) We take the following as an axiom:
Axiom. (SNo_eps_pos) We take the following as an axiom:
Axiom. (SNo_pos_eps_Lt) We take the following as an axiom:
∀n, nat_p nxSNoS_ (ordsucc n), 0 < xeps_ n < x
Axiom. (SNo_pos_eps_Le) We take the following as an axiom:
∀n, nat_p nxSNoS_ (ordsucc (ordsucc n)), 0 < xeps_ n x
Axiom. (eps_SNo_eq) We take the following as an axiom:
∀n, nat_p nxSNoS_ (ordsucc n), 0 < xSNoEq_ (SNoLev x) (eps_ n) xmn, x = eps_ m
Axiom. (eps_SNoCutP) We take the following as an axiom:
Axiom. (eps_SNoCut) We take the following as an axiom:
End of Section TaggedSets2
Axiom. (SNo_etaE) We take the following as an axiom:
∀z, SNo z∀p : prop, (∀L R, SNoCutP L R(xL, SNoLev x SNoLev z)(yR, SNoLev y SNoLev z)z = SNoCut L Rp)p
Axiom. (SNo_ind) We take the following as an axiom:
∀P : setprop, (∀L R, SNoCutP L R(xL, P x)(yR, P y)P (SNoCut L R))∀z, SNo zP z
Beginning of Section SurrealRecI
Variable F : set(setset)set
Let default : setEps_i (λ_ ⇒ True)
Let G : set(setsetset)setsetλalpha g ⇒ If_ii (ordinal alpha) (λz : setif z SNoS_ (ordsucc alpha) then F z (λw ⇒ g (SNoLev w) w) else default) (λz : setdefault)
Primitive. The name SNo_rec_i is a term of type setset.
Hypothesis Fr : ∀z, SNo z∀g h : setset, (wSNoS_ (SNoLev z), g w = h w)F z g = F z h
Axiom. (SNo_rec_i_eq) We take the following as an axiom:
∀z, SNo zSNo_rec_i z = F z SNo_rec_i
End of Section SurrealRecI
Beginning of Section SurrealRecII
Variable F : set(set(setset))(setset)
Let default : (setset)Descr_ii (λ_ ⇒ True)
Let G : set(setset(setset))set(setset)λalpha g ⇒ If_iii (ordinal alpha) (λz : setIf_ii (z SNoS_ (ordsucc alpha)) (F z (λw ⇒ g (SNoLev w) w)) default) (λz : setdefault)
Primitive. The name SNo_rec_ii is a term of type set(setset).
Hypothesis Fr : ∀z, SNo z∀g h : set(setset), (wSNoS_ (SNoLev z), g w = h w)F z g = F z h
Axiom. (SNo_rec_ii_eq) We take the following as an axiom:
∀z, SNo zSNo_rec_ii z = F z SNo_rec_ii
End of Section SurrealRecII
Beginning of Section SurrealRec2
Variable F : setset(setsetset)set
Let G : set(setsetset)set(setset)setλw f z g ⇒ F w z (λx y ⇒ if x = w then g y else f x y)
Let H : set(setsetset)setsetλw f z ⇒ if SNo z then SNo_rec_i (G w f) z else Empty
Primitive. The name SNo_rec2 is a term of type setsetset.
Hypothesis Fr : ∀w, SNo w∀z, SNo z∀g h : setsetset, (xSNoS_ (SNoLev w), ∀y, SNo yg x y = h x y)(ySNoS_ (SNoLev z), g w y = h w y)F w z g = F w z h
Axiom. (SNo_rec2_G_prop) We take the following as an axiom:
∀w, SNo w∀f k : setsetset, (xSNoS_ (SNoLev w), f x = k x)∀z, SNo z∀g h : setset, (uSNoS_ (SNoLev z), g u = h u)G w f z g = G w k z h
Axiom. (SNo_rec2_eq_1) We take the following as an axiom:
∀w, SNo w∀f : setsetset, ∀z, SNo zSNo_rec_i (G w f) z = G w f z (SNo_rec_i (G w f))
Axiom. (SNo_rec2_eq) We take the following as an axiom:
∀w, SNo w∀z, SNo zSNo_rec2 w z = F w z SNo_rec2
End of Section SurrealRec2
Axiom. (SNo_ordinal_ind) We take the following as an axiom:
∀P : setprop, (∀alpha, ordinal alphaxSNoS_ alpha, P x)(∀x, SNo xP x)
Axiom. (SNo_ordinal_ind2) We take the following as an axiom:
∀P : setsetprop, (∀alpha, ordinal alpha∀beta, ordinal betaxSNoS_ alpha, ySNoS_ beta, P x y)(∀x y, SNo xSNo yP x y)
Axiom. (SNo_ordinal_ind3) We take the following as an axiom:
∀P : setsetsetprop, (∀alpha, ordinal alpha∀beta, ordinal beta∀gamma, ordinal gammaxSNoS_ alpha, ySNoS_ beta, zSNoS_ gamma, P x y z)(∀x y z, SNo xSNo ySNo zP x y z)
Axiom. (SNoLev_ind) We take the following as an axiom:
∀P : setprop, (∀x, SNo x(wSNoS_ (SNoLev x), P w)P x)(∀x, SNo xP x)
Axiom. (SNoLev_ind2) We take the following as an axiom:
∀P : setsetprop, (∀x y, SNo xSNo y(wSNoS_ (SNoLev x), P w y)(zSNoS_ (SNoLev y), P x z)(wSNoS_ (SNoLev x), zSNoS_ (SNoLev y), P w z)P x y)∀x y, SNo xSNo yP x y
Axiom. (SNoLev_ind3) We take the following as an axiom:
∀P : setsetsetprop, (∀x y z, SNo xSNo ySNo z(uSNoS_ (SNoLev x), P u y z)(vSNoS_ (SNoLev y), P x v z)(wSNoS_ (SNoLev z), P x y w)(uSNoS_ (SNoLev x), vSNoS_ (SNoLev y), P u v z)(uSNoS_ (SNoLev x), wSNoS_ (SNoLev z), P u y w)(vSNoS_ (SNoLev y), wSNoS_ (SNoLev z), P x v w)(uSNoS_ (SNoLev x), vSNoS_ (SNoLev y), wSNoS_ (SNoLev z), P u v w)P x y z)∀x y z, SNo xSNo ySNo zP x y z
Axiom. (SNo_omega) We take the following as an axiom:
SNo ω
Axiom. (SNoLt_0_1) We take the following as an axiom:
0 < 1
Axiom. (SNoLt_0_2) We take the following as an axiom:
0 < 2
Axiom. (SNoLt_1_2) We take the following as an axiom:
1 < 2
Axiom. (restr_SNo_) We take the following as an axiom:
∀x, SNo xalphaSNoLev x, SNo_ alpha (x SNoElts_ alpha)
Axiom. (restr_SNo) We take the following as an axiom:
∀x, SNo xalphaSNoLev x, SNo (x SNoElts_ alpha)
Axiom. (restr_SNoLev) We take the following as an axiom:
∀x, SNo xalphaSNoLev x, SNoLev (x SNoElts_ alpha) = alpha
Axiom. (restr_SNoEq) We take the following as an axiom:
∀x, SNo xalphaSNoLev x, SNoEq_ alpha (x SNoElts_ alpha) x
Axiom. (SNo_extend0_restr_eq) We take the following as an axiom:
∀x, SNo xx = SNo_extend0 x SNoElts_ (SNoLev x)
Axiom. (SNo_extend1_restr_eq) We take the following as an axiom:
∀x, SNo xx = SNo_extend1 x SNoElts_ (SNoLev x)
Beginning of Section SurrealMinus
Primitive. The name minus_SNo is a term of type setset.
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.
Axiom. (minus_SNo_eq) We take the following as an axiom:
∀x, SNo x- x = SNoCut {- z|zSNoR x} {- w|wSNoL x}
Axiom. (minus_SNo_prop1) We take the following as an axiom:
∀x, SNo xSNo (- x) (uSNoL x, - x < - u) (uSNoR x, - u < - x) SNoCutP {- z|zSNoR x} {- w|wSNoL x}
Axiom. (SNo_minus_SNo) We take the following as an axiom:
∀x, SNo xSNo (- x)
Axiom. (minus_SNo_Lt_contra) We take the following as an axiom:
∀x y, SNo xSNo yx < y- y < - x
Axiom. (minus_SNo_Le_contra) We take the following as an axiom:
∀x y, SNo xSNo yx y- y - x
Axiom. (minus_SNo_SNoCutP) We take the following as an axiom:
∀x, SNo xSNoCutP {- z|zSNoR x} {- w|wSNoL x}
Axiom. (minus_SNo_SNoCutP_gen) We take the following as an axiom:
∀L R, SNoCutP L RSNoCutP {- z|zR} {- w|wL}
Axiom. (minus_SNo_Lev_lem1) We take the following as an axiom:
∀alpha, ordinal alphaxSNoS_ alpha, SNoLev (- x) SNoLev x
Axiom. (minus_SNo_Lev_lem2) We take the following as an axiom:
∀x, SNo xSNoLev (- x) SNoLev x
Axiom. (minus_SNo_invol) We take the following as an axiom:
∀x, SNo x- - x = x
Axiom. (minus_SNo_Lev) We take the following as an axiom:
∀x, SNo xSNoLev (- x) = SNoLev x
Axiom. (minus_SNo_SNo_) We take the following as an axiom:
∀alpha, ordinal alpha∀x, SNo_ alpha xSNo_ alpha (- x)
Axiom. (minus_SNo_SNoS_) We take the following as an axiom:
∀alpha, ordinal alpha∀x, x SNoS_ alpha- x SNoS_ alpha
Axiom. (minus_SNoCut_eq_lem) We take the following as an axiom:
∀v, SNo v∀L R, SNoCutP L Rv = SNoCut L R- v = SNoCut {- z|zR} {- w|wL}
Axiom. (minus_SNoCut_eq) We take the following as an axiom:
∀L R, SNoCutP L R- SNoCut L R = SNoCut {- z|zR} {- w|wL}
Axiom. (minus_SNo_Lt_contra1) We take the following as an axiom:
∀x y, SNo xSNo y- x < y- y < x
Axiom. (minus_SNo_Lt_contra2) We take the following as an axiom:
∀x y, SNo xSNo yx < - yy < - x
Axiom. (mordinal_SNoLev_min_2) We take the following as an axiom:
∀alpha, ordinal alpha∀z, SNo zSNoLev z ordsucc alpha- alpha z
Axiom. (minus_SNo_SNoS_omega) We take the following as an axiom:
Axiom. (SNoL_minus_SNoR) We take the following as an axiom:
∀x, SNo xSNoL (- x) = {- w|wSNoR x}
End of Section SurrealMinus
Beginning of Section SurrealAdd
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Primitive. The name add_SNo is a term of type setsetset.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Axiom. (add_SNo_eq) We take the following as an axiom:
∀x, SNo x∀y, SNo yx + y = SNoCut ({w + y|wSNoL x} {x + w|wSNoL y}) ({z + y|zSNoR x} {x + z|zSNoR y})
Axiom. (add_SNo_prop1) We take the following as an axiom:
∀x y, SNo xSNo ySNo (x + y) (uSNoL x, u + y < x + y) (uSNoR x, x + y < u + y) (uSNoL y, x + u < x + y) (uSNoR y, x + y < x + u) SNoCutP ({w + y|wSNoL x} {x + w|wSNoL y}) ({z + y|zSNoR x} {x + z|zSNoR y})
Axiom. (SNo_add_SNo) We take the following as an axiom:
∀x y, SNo xSNo ySNo (x + y)
Axiom. (SNo_add_SNo_3) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zSNo (x + y + z)
Axiom. (SNo_add_SNo_3c) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zSNo (x + y + - z)
Axiom. (SNo_add_SNo_4) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo wSNo (x + y + z + w)
Axiom. (add_SNo_Lt1) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx < zx + y < z + y
Axiom. (add_SNo_Le1) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx zx + y z + y
Axiom. (add_SNo_Lt2) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zy < zx + y < x + z
Axiom. (add_SNo_Le2) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zy zx + y x + z
Axiom. (add_SNo_Lt3a) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo wx < zy wx + y < z + w
Axiom. (add_SNo_Lt3b) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo wx zy < wx + y < z + w
Axiom. (add_SNo_Lt3) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo wx < zy < wx + y < z + w
Axiom. (add_SNo_Le3) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo wx zy wx + y z + w
Axiom. (add_SNo_SNoCutP) We take the following as an axiom:
∀x y, SNo xSNo ySNoCutP ({w + y|wSNoL x} {x + w|wSNoL y}) ({z + y|zSNoR x} {x + z|zSNoR y})
Axiom. (add_SNo_com) We take the following as an axiom:
∀x y, SNo xSNo yx + y = y + x
Axiom. (add_SNo_0L) We take the following as an axiom:
∀x, SNo x0 + x = x
Axiom. (add_SNo_0R) We take the following as an axiom:
∀x, SNo xx + 0 = x
Axiom. (add_SNo_minus_SNo_linv) We take the following as an axiom:
∀x, SNo x- x + x = 0
Axiom. (add_SNo_minus_SNo_rinv) We take the following as an axiom:
∀x, SNo xx + - x = 0
Axiom. (add_SNo_ordinal_SNoCutP) We take the following as an axiom:
∀alpha, ordinal alpha∀beta, ordinal betaSNoCutP ({x + beta|xSNoS_ alpha} {alpha + x|xSNoS_ beta}) Empty
Axiom. (add_SNo_ordinal_eq) We take the following as an axiom:
∀alpha, ordinal alpha∀beta, ordinal betaalpha + beta = SNoCut ({x + beta|xSNoS_ alpha} {alpha + x|xSNoS_ beta}) Empty
Axiom. (add_SNo_ordinal_ordinal) We take the following as an axiom:
∀alpha, ordinal alpha∀beta, ordinal betaordinal (alpha + beta)
Axiom. (add_SNo_ordinal_SL) We take the following as an axiom:
∀alpha, ordinal alpha∀beta, ordinal betaordsucc alpha + beta = ordsucc (alpha + beta)
Axiom. (add_SNo_ordinal_SR) We take the following as an axiom:
∀alpha, ordinal alpha∀beta, ordinal betaalpha + ordsucc beta = ordsucc (alpha + beta)
Axiom. (add_SNo_ordinal_InL) We take the following as an axiom:
∀alpha, ordinal alpha∀beta, ordinal betagammaalpha, gamma + beta alpha + beta
Axiom. (add_SNo_ordinal_InR) We take the following as an axiom:
∀alpha, ordinal alpha∀beta, ordinal betagammabeta, alpha + gamma alpha + beta
Axiom. (add_nat_add_SNo) We take the following as an axiom:
Axiom. (add_SNo_In_omega) We take the following as an axiom:
Axiom. (add_SNo_1_1_2) We take the following as an axiom:
1 + 1 = 2
Axiom. (add_SNo_SNoL_interpolate) We take the following as an axiom:
∀x y, SNo xSNo yuSNoL (x + y), (vSNoL x, u v + y) (vSNoL y, u x + v)
Axiom. (add_SNo_SNoR_interpolate) We take the following as an axiom:
∀x y, SNo xSNo yuSNoR (x + y), (vSNoR x, v + y u) (vSNoR y, x + v u)
Axiom. (add_SNo_assoc) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx + (y + z) = (x + y) + z
Axiom. (add_SNo_cancel_L) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx + y = x + zy = z
Axiom. (minus_SNo_0) We take the following as an axiom:
- 0 = 0
Axiom. (minus_add_SNo_distr) We take the following as an axiom:
∀x y, SNo xSNo y- (x + y) = (- x) + (- y)
Axiom. (minus_add_SNo_distr_3) We take the following as an axiom:
∀x y z, SNo xSNo ySNo z- (x + y + z) = - x + - y + - z
Axiom. (add_SNo_Lev_bd) We take the following as an axiom:
∀x y, SNo xSNo ySNoLev (x + y) SNoLev x + SNoLev y
Axiom. (add_SNo_SNoS_omega) We take the following as an axiom:
Axiom. (add_SNo_minus_R2) We take the following as an axiom:
∀x y, SNo xSNo y(x + y) + - y = x
Axiom. (add_SNo_minus_R2') We take the following as an axiom:
∀x y, SNo xSNo y(x + - y) + y = x
Axiom. (add_SNo_minus_L2) We take the following as an axiom:
∀x y, SNo xSNo y- x + (x + y) = y
Axiom. (add_SNo_minus_L2') We take the following as an axiom:
∀x y, SNo xSNo yx + (- x + y) = y
Axiom. (add_SNo_Lt1_cancel) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx + y < z + yx < z
Axiom. (add_SNo_Lt2_cancel) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx + y < x + zy < z
Axiom. (add_SNo_assoc_4) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo wx + y + z + w = (x + y + z) + w
Axiom. (add_SNo_com_3_0_1) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx + y + z = y + x + z
Axiom. (add_SNo_com_3b_1_2) We take the following as an axiom:
∀x y z, SNo xSNo ySNo z(x + y) + z = (x + z) + y
Axiom. (add_SNo_com_4_inner_mid) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo w(x + y) + (z + w) = (x + z) + (y + w)
Axiom. (add_SNo_rotate_3_1) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx + y + z = z + x + y
Axiom. (add_SNo_rotate_4_1) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo wx + y + z + w = w + x + y + z
Axiom. (add_SNo_rotate_5_1) We take the following as an axiom:
∀x y z w v, SNo xSNo ySNo zSNo wSNo vx + y + z + w + v = v + x + y + z + w
Axiom. (add_SNo_rotate_5_2) We take the following as an axiom:
∀x y z w v, SNo xSNo ySNo zSNo wSNo vx + y + z + w + v = w + v + x + y + z
Axiom. (add_SNo_minus_SNo_prop3) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo w(x + y + z) + (- z + w) = x + y + w
Axiom. (add_SNo_minus_SNo_prop4) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo w(x + y + z) + (w + - z) = x + y + w
Axiom. (add_SNo_minus_SNo_prop5) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo w(x + y + - z) + (z + w) = x + y + w
Axiom. (add_SNo_minus_Lt1) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx + - y < zx < z + y
Axiom. (add_SNo_minus_Lt2) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zz < x + - yz + y < x
Axiom. (add_SNo_minus_Lt1b) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx < z + yx + - y < z
Axiom. (add_SNo_minus_Lt2b) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zz + y < xz < x + - y
Axiom. (add_SNo_minus_Lt1b3) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo wx + y < w + zx + y + - z < w
Axiom. (add_SNo_minus_Lt2b3) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo ww + z < x + yw < x + y + - z
Axiom. (add_SNo_minus_Lt_lem) We take the following as an axiom:
∀x y z u v w, SNo xSNo ySNo zSNo uSNo vSNo wx + y + w < u + v + zx + y + - z < u + v + - w
Axiom. (add_SNo_minus_Le2) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zz x + - yz + y x
Axiom. (add_SNo_minus_Le2b) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zz + y xz x + - y
Axiom. (add_SNo_Lt_subprop2) We take the following as an axiom:
∀x y z w u v, SNo xSNo ySNo zSNo wSNo uSNo vx + u < z + vy + v < w + ux + y < z + w
Axiom. (add_SNo_Lt_subprop3a) We take the following as an axiom:
∀x y z w u a, SNo xSNo ySNo zSNo wSNo uSNo ax + z < w + ay + a < ux + y + z < w + u
Axiom. (add_SNo_Lt_subprop3b) We take the following as an axiom:
∀x y w u v a, SNo xSNo ySNo wSNo uSNo vSNo ax + a < w + vy < a + ux + y < w + u + v
Axiom. (add_SNo_Lt_subprop3c) We take the following as an axiom:
∀x y z w u a b c, SNo xSNo ySNo zSNo wSNo uSNo aSNo bSNo cx + a < b + cy + c < ub + z < w + ax + y + z < w + u
Axiom. (add_SNo_Lt_subprop3d) We take the following as an axiom:
∀x y w u v a b c, SNo xSNo ySNo wSNo uSNo vSNo aSNo bSNo cx + a < b + vy < c + ub + c < w + ax + y < w + u + v
Axiom. (ordinal_ordsucc_SNo_eq) We take the following as an axiom:
∀alpha, ordinal alphaordsucc alpha = 1 + alpha
Axiom. (add_SNo_3a_2b) We take the following as an axiom:
∀x y z w u, SNo xSNo ySNo zSNo wSNo u(x + y + z) + (w + u) = (u + y + z) + (w + x)
Axiom. (add_SNo_1_ordsucc) We take the following as an axiom:
Axiom. (add_SNo_eps_Lt) We take the following as an axiom:
∀x, SNo xnω, x < x + eps_ n
Axiom. (add_SNo_eps_Lt') We take the following as an axiom:
∀x y, SNo xSNo ynω, x < yx < y + eps_ n
Axiom. (SNoLt_minus_pos) We take the following as an axiom:
∀x y, SNo xSNo yx < y0 < y + - x
Axiom. (add_SNo_omega_In_cases) We take the following as an axiom:
∀m, nω, ∀k, nat_p km n + km n m + - n k
Axiom. (add_SNo_Lt4) We take the following as an axiom:
∀x y z w u v, SNo xSNo ySNo zSNo wSNo uSNo vx < wy < uz < vx + y + z < w + u + v
Axiom. (add_SNo_3_3_3_Lt1) We take the following as an axiom:
∀x y z w u, SNo xSNo ySNo zSNo wSNo ux + y < z + wx + y + u < z + w + u
Axiom. (add_SNo_3_2_3_Lt1) We take the following as an axiom:
∀x y z w u, SNo xSNo ySNo zSNo wSNo uy + x < z + wx + u + y < z + w + u
End of Section SurrealAdd
Beginning of Section SurrealMul
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.
Definition. We define mul_SNo to be SNo_rec2 (λx y m ⇒ SNoCut ({m (w 0) y + m x (w 1) + - m (w 0) (w 1)|wSNoL x SNoL y} {m (z 0) y + m x (z 1) + - m (z 0) (z 1)|zSNoR x SNoR y}) ({m (w 0) y + m x (w 1) + - m (w 0) (w 1)|wSNoL x SNoR y} {m (z 0) y + m x (z 1) + - m (z 0) (z 1)|zSNoR x SNoL y})) of type setsetset.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Axiom. (mul_SNo_eq) We take the following as an axiom:
∀x, SNo x∀y, SNo yx * y = SNoCut ({(w 0) * y + x * (w 1) + - (w 0) * (w 1)|wSNoL x SNoL y} {(z 0) * y + x * (z 1) + - (z 0) * (z 1)|zSNoR x SNoR y}) ({(w 0) * y + x * (w 1) + - (w 0) * (w 1)|wSNoL x SNoR y} {(z 0) * y + x * (z 1) + - (z 0) * (z 1)|zSNoR x SNoL y})
Axiom. (mul_SNo_eq_2) We take the following as an axiom:
∀x y, SNo xSNo y∀p : prop, (∀L R, (∀u, u L(∀q : prop, (w0SNoL x, w1SNoL y, u = w0 * y + x * w1 + - w0 * w1q)(z0SNoR x, z1SNoR y, u = z0 * y + x * z1 + - z0 * z1q)q))(w0SNoL x, w1SNoL y, w0 * y + x * w1 + - w0 * w1 L)(z0SNoR x, z1SNoR y, z0 * y + x * z1 + - z0 * z1 L)(∀u, u R(∀q : prop, (w0SNoL x, z1SNoR y, u = w0 * y + x * z1 + - w0 * z1q)(z0SNoR x, w1SNoL y, u = z0 * y + x * w1 + - z0 * w1q)q))(w0SNoL x, z1SNoR y, w0 * y + x * z1 + - w0 * z1 R)(z0SNoR x, w1SNoL y, z0 * y + x * w1 + - z0 * w1 R)x * y = SNoCut L Rp)p
Axiom. (mul_SNo_prop_1) We take the following as an axiom:
∀x, SNo x∀y, SNo y∀p : prop, (SNo (x * y)(uSNoL x, vSNoL y, u * y + x * v < x * y + u * v)(uSNoR x, vSNoR y, u * y + x * v < x * y + u * v)(uSNoL x, vSNoR y, x * y + u * v < u * y + x * v)(uSNoR x, vSNoL y, x * y + u * v < u * y + x * v)p)p
Axiom. (SNo_mul_SNo) We take the following as an axiom:
∀x y, SNo xSNo ySNo (x * y)
Axiom. (SNo_mul_SNo_lem) We take the following as an axiom:
∀x y u v, SNo xSNo ySNo uSNo vSNo (u * y + x * v + - (u * v))
Axiom. (SNo_mul_SNo_3) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zSNo (x * y * z)
Axiom. (mul_SNo_eq_3) We take the following as an axiom:
∀x y, SNo xSNo y∀p : prop, (∀L R, SNoCutP L R(∀u, u L(∀q : prop, (w0SNoL x, w1SNoL y, u = w0 * y + x * w1 + - w0 * w1q)(z0SNoR x, z1SNoR y, u = z0 * y + x * z1 + - z0 * z1q)q))(w0SNoL x, w1SNoL y, w0 * y + x * w1 + - w0 * w1 L)(z0SNoR x, z1SNoR y, z0 * y + x * z1 + - z0 * z1 L)(∀u, u R(∀q : prop, (w0SNoL x, z1SNoR y, u = w0 * y + x * z1 + - w0 * z1q)(z0SNoR x, w1SNoL y, u = z0 * y + x * w1 + - z0 * w1q)q))(w0SNoL x, z1SNoR y, w0 * y + x * z1 + - w0 * z1 R)(z0SNoR x, w1SNoL y, z0 * y + x * w1 + - z0 * w1 R)x * y = SNoCut L Rp)p
Axiom. (mul_SNo_Lt) We take the following as an axiom:
∀x y u v, SNo xSNo ySNo uSNo vu < xv < yu * y + x * v < x * y + u * v
Axiom. (mul_SNo_Le) We take the following as an axiom:
∀x y u v, SNo xSNo ySNo uSNo vu xv yu * y + x * v x * y + u * v
Axiom. (mul_SNo_SNoL_interpolate) We take the following as an axiom:
∀x y, SNo xSNo yuSNoL (x * y), (vSNoL x, wSNoL y, u + v * w v * y + x * w) (vSNoR x, wSNoR y, u + v * w v * y + x * w)
Axiom. (mul_SNo_SNoL_interpolate_impred) We take the following as an axiom:
∀x y, SNo xSNo yuSNoL (x * y), ∀p : prop, (vSNoL x, wSNoL y, u + v * w v * y + x * wp)(vSNoR x, wSNoR y, u + v * w v * y + x * wp)p
Axiom. (mul_SNo_SNoR_interpolate) We take the following as an axiom:
∀x y, SNo xSNo yuSNoR (x * y), (vSNoL x, wSNoR y, v * y + x * w u + v * w) (vSNoR x, wSNoL y, v * y + x * w u + v * w)
Axiom. (mul_SNo_SNoR_interpolate_impred) We take the following as an axiom:
∀x y, SNo xSNo yuSNoR (x * y), ∀p : prop, (vSNoL x, wSNoR y, v * y + x * w u + v * wp)(vSNoR x, wSNoL y, v * y + x * w u + v * wp)p
Axiom. (mul_SNo_Subq_lem) We take the following as an axiom:
∀x y X Y Z W, ∀U U', (∀u, u U(∀q : prop, (w0X, w1Y, u = w0 * y + x * w1 + - w0 * w1q)(z0Z, z1W, u = z0 * y + x * z1 + - z0 * z1q)q))(w0X, w1Y, w0 * y + x * w1 + - w0 * w1 U')(w0Z, w1W, w0 * y + x * w1 + - w0 * w1 U')U U'
Axiom. (mul_SNo_zeroR) We take the following as an axiom:
∀x, SNo xx * 0 = 0
Axiom. (mul_SNo_oneR) We take the following as an axiom:
∀x, SNo xx * 1 = x
Axiom. (mul_SNo_com) We take the following as an axiom:
∀x y, SNo xSNo yx * y = y * x
Axiom. (mul_SNo_minus_distrL) We take the following as an axiom:
∀x y, SNo xSNo y(- x) * y = - x * y
Axiom. (mul_SNo_minus_distrR) We take the following as an axiom:
∀x y, SNo xSNo yx * (- y) = - (x * y)
Axiom. (mul_SNo_distrR) We take the following as an axiom:
∀x y z, SNo xSNo ySNo z(x + y) * z = x * z + y * z
Axiom. (mul_SNo_distrL) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx * (y + z) = x * y + x * z
Beginning of Section mul_SNo_assoc_lems
Variable M : setsetset
Hypothesis DL : ∀x y z, SNo xSNo ySNo zx * (y + z) = x * y + x * z
Hypothesis DR : ∀x y z, SNo xSNo ySNo z(x + y) * z = x * z + y * z
Hypothesis IL : ∀x y, SNo xSNo yuSNoL (x * y), ∀p : prop, (vSNoL x, wSNoL y, u + v * w v * y + x * wp)(vSNoR x, wSNoR y, u + v * w v * y + x * wp)p
Hypothesis IR : ∀x y, SNo xSNo yuSNoR (x * y), ∀p : prop, (vSNoL x, wSNoR y, v * y + x * w u + v * wp)(vSNoR x, wSNoL y, v * y + x * w u + v * wp)p
Hypothesis M_Lt : ∀x y u v, SNo xSNo ySNo uSNo vu < xv < yu * y + x * v < x * y + u * v
Hypothesis M_Le : ∀x y u v, SNo xSNo ySNo uSNo vu xv yu * y + x * v x * y + u * v
Axiom. (mul_SNo_assoc_lem1) We take the following as an axiom:
∀x y z, SNo xSNo ySNo z(uSNoS_ (SNoLev x), u * (y * z) = (u * y) * z)(vSNoS_ (SNoLev y), x * (v * z) = (x * v) * z)(wSNoS_ (SNoLev z), x * (y * w) = (x * y) * w)(uSNoS_ (SNoLev x), vSNoS_ (SNoLev y), u * (v * z) = (u * v) * z)(uSNoS_ (SNoLev x), wSNoS_ (SNoLev z), u * (y * w) = (u * y) * w)(vSNoS_ (SNoLev y), wSNoS_ (SNoLev z), x * (v * w) = (x * v) * w)(uSNoS_ (SNoLev x), vSNoS_ (SNoLev y), wSNoS_ (SNoLev z), u * (v * w) = (u * v) * w)∀L, (uL, ∀q : prop, (vSNoL x, wSNoL (y * z), u = v * (y * z) + x * w + - v * wq)(vSNoR x, wSNoR (y * z), u = v * (y * z) + x * w + - v * wq)q)uL, u < (x * y) * z
Axiom. (mul_SNo_assoc_lem2) We take the following as an axiom:
∀x y z, SNo xSNo ySNo z(uSNoS_ (SNoLev x), u * (y * z) = (u * y) * z)(vSNoS_ (SNoLev y), x * (v * z) = (x * v) * z)(wSNoS_ (SNoLev z), x * (y * w) = (x * y) * w)(uSNoS_ (SNoLev x), vSNoS_ (SNoLev y), u * (v * z) = (u * v) * z)(uSNoS_ (SNoLev x), wSNoS_ (SNoLev z), u * (y * w) = (u * y) * w)(vSNoS_ (SNoLev y), wSNoS_ (SNoLev z), x * (v * w) = (x * v) * w)(uSNoS_ (SNoLev x), vSNoS_ (SNoLev y), wSNoS_ (SNoLev z), u * (v * w) = (u * v) * w)∀R, (uR, ∀q : prop, (vSNoL x, wSNoR (y * z), u = v * (y * z) + x * w + - v * wq)(vSNoR x, wSNoL (y * z), u = v * (y * z) + x * w + - v * wq)q)uR, (x * y) * z < u
End of Section mul_SNo_assoc_lems
Axiom. (mul_SNo_assoc) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx * (y * z) = (x * y) * z
Axiom. (mul_nat_mul_SNo) We take the following as an axiom:
Axiom. (mul_SNo_In_omega) We take the following as an axiom:
Axiom. (mul_SNo_zeroL) We take the following as an axiom:
∀x, SNo x0 * x = 0
Axiom. (mul_SNo_oneL) We take the following as an axiom:
∀x, SNo x1 * x = x
Axiom. (pos_mul_SNo_Lt) We take the following as an axiom:
∀x y z, SNo x0 < xSNo ySNo zy < zx * y < x * z
Axiom. (nonneg_mul_SNo_Le) We take the following as an axiom:
∀x y z, SNo x0 xSNo ySNo zy zx * y x * z
Axiom. (neg_mul_SNo_Lt) We take the following as an axiom:
∀x y z, SNo xx < 0SNo ySNo zz < yx * y < x * z
Axiom. (pos_mul_SNo_Lt') We take the following as an axiom:
∀x y z, SNo xSNo ySNo z0 < zx < yx * z < y * z
Axiom. (mul_SNo_Lt1_pos_Lt) We take the following as an axiom:
∀x y, SNo xSNo yx < 10 < yx * y < y
Axiom. (nonneg_mul_SNo_Le') We take the following as an axiom:
∀x y z, SNo xSNo ySNo z0 zx yx * z y * z
Axiom. (mul_SNo_Le1_nonneg_Le) We take the following as an axiom:
∀x y, SNo xSNo yx 10 yx * y y
Axiom. (pos_mul_SNo_Lt2) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo w0 < x0 < yx < zy < wx * y < z * w
Axiom. (nonneg_mul_SNo_Le2) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo w0 x0 yx zy wx * y z * w
Axiom. (mul_SNo_pos_pos) We take the following as an axiom:
∀x y, SNo xSNo y0 < x0 < y0 < x * y
Axiom. (mul_SNo_pos_neg) We take the following as an axiom:
∀x y, SNo xSNo y0 < xy < 0x * y < 0
Axiom. (mul_SNo_neg_pos) We take the following as an axiom:
∀x y, SNo xSNo yx < 00 < yx * y < 0
Axiom. (mul_SNo_neg_neg) We take the following as an axiom:
∀x y, SNo xSNo yx < 0y < 00 < x * y
Axiom. (SNo_sqr_nonneg) We take the following as an axiom:
∀x, SNo x0 x * x
Axiom. (SNo_zero_or_sqr_pos) We take the following as an axiom:
∀x, SNo xx = 0 0 < x * x
Axiom. (SNo_foil) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo w(x + y) * (z + w) = x * z + x * w + y * z + y * w
Axiom. (mul_SNo_minus_minus) We take the following as an axiom:
∀x y, SNo xSNo y(- x) * (- y) = x * y
Axiom. (mul_SNo_com_3_0_1) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx * y * z = y * x * z
Axiom. (mul_SNo_com_3b_1_2) We take the following as an axiom:
∀x y z, SNo xSNo ySNo z(x * y) * z = (x * z) * y
Axiom. (mul_SNo_com_4_inner_mid) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo w(x * y) * (z * w) = (x * z) * (y * w)
Axiom. (mul_SNo_rotate_3_1) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx * y * z = z * x * y
Axiom. (mul_SNo_rotate_4_1) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo wx * y * z * w = w * x * y * z
Axiom. (SNo_foil_mm) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo w(x + - y) * (z + - w) = x * z + - x * w + - y * z + y * w
Axiom. (mul_SNo_nonzero_cancel) We take the following as an axiom:
∀x y z, SNo xx 0SNo ySNo zx * y = x * zy = z
End of Section SurrealMul
Beginning of Section SurrealExp
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.
Definition. We define exp_SNo_nat to be λn m : setnat_primrec 1 (λ_ r ⇒ n * r) m of type setsetset.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
Axiom. (exp_SNo_nat_0) We take the following as an axiom:
∀x, SNo xx ^ 0 = 1
Axiom. (exp_SNo_nat_S) We take the following as an axiom:
∀x, SNo x∀n, nat_p nx ^ (ordsucc n) = x * x ^ n
Axiom. (SNo_exp_SNo_nat) We take the following as an axiom:
∀x, SNo x∀n, nat_p nSNo (x ^ n)
Axiom. (nat_exp_SNo_nat) We take the following as an axiom:
∀x, nat_p x∀n, nat_p nnat_p (x ^ n)
Axiom. (eps_ordsucc_half_add) We take the following as an axiom:
∀n, nat_p neps_ (ordsucc n) + eps_ (ordsucc n) = eps_ n
Axiom. (eps_1_half_eq1) We take the following as an axiom:
Axiom. (eps_1_half_eq2) We take the following as an axiom:
Axiom. (double_eps_1) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx + x = y + zx = eps_ 1 * (y + z)
Axiom. (exp_SNo_1_bd) We take the following as an axiom:
∀x, SNo x1 x∀n, nat_p n1 x ^ n
Axiom. (exp_SNo_2_bd) We take the following as an axiom:
∀n, nat_p nn < 2 ^ n
Axiom. (mul_SNo_eps_power_2) We take the following as an axiom:
∀n, nat_p neps_ n * 2 ^ n = 1
Axiom. (eps_bd_1) We take the following as an axiom:
Axiom. (mul_SNo_eps_power_2') We take the following as an axiom:
∀n, nat_p n2 ^ n * eps_ n = 1
Axiom. (exp_SNo_nat_mul_add) We take the following as an axiom:
∀x, SNo x∀m, nat_p m∀n, nat_p nx ^ m * x ^ n = x ^ (m + n)
Axiom. (exp_SNo_nat_mul_add') We take the following as an axiom:
∀x, SNo xm nω, x ^ m * x ^ n = x ^ (m + n)
Axiom. (exp_SNo_nat_pos) We take the following as an axiom:
∀x, SNo x0 < x∀n, nat_p n0 < x ^ n
Axiom. (mul_SNo_eps_eps_add_SNo) We take the following as an axiom:
m nω, eps_ m * eps_ n = eps_ (m + n)
Axiom. (SNoS_omega_Lev_equip) We take the following as an axiom:
∀n, nat_p nequip {xSNoS_ ω|SNoLev x = n} (2 ^ n)
Axiom. (SNoS_finite) We take the following as an axiom:
Axiom. (SNoS_omega_SNoL_finite) We take the following as an axiom:
Axiom. (SNoS_omega_SNoR_finite) We take the following as an axiom:
End of Section SurrealExp
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.
Axiom. (int_SNo_cases) We take the following as an axiom:
∀p : setprop, (nω, p n)(nω, p (- n))xint, p x
Axiom. (int_3_cases) We take the following as an axiom:
nint, ∀p : prop, (mω, n = - ordsucc mp)(n = 0p)(mω, n = ordsucc mp)p
Axiom. (int_SNo) We take the following as an axiom:
Axiom. (Subq_omega_int) We take the following as an axiom:
Axiom. (int_minus_SNo_omega) We take the following as an axiom:
Axiom. (int_add_SNo_lem) We take the following as an axiom:
nω, ∀m, nat_p m- n + m int
Axiom. (int_add_SNo) We take the following as an axiom:
Axiom. (int_minus_SNo) We take the following as an axiom:
Axiom. (int_mul_SNo) We take the following as an axiom:
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.
Definition. We define abs_SNo to be λx ⇒ if 0 x then x else - x of type setset.
Axiom. (nonneg_abs_SNo) We take the following as an axiom:
∀x, 0 xabs_SNo x = x
Axiom. (not_nonneg_abs_SNo) We take the following as an axiom:
∀x, ¬ (0 x)abs_SNo x = - x
Axiom. (abs_SNo_0) We take the following as an axiom:
Axiom. (pos_abs_SNo) We take the following as an axiom:
∀x, 0 < xabs_SNo x = x
Axiom. (neg_abs_SNo) We take the following as an axiom:
∀x, SNo xx < 0abs_SNo x = - x
Axiom. (SNo_abs_SNo) We take the following as an axiom:
∀x, SNo xSNo (abs_SNo x)
Axiom. (abs_SNo_Lev) We take the following as an axiom:
∀x, SNo xSNoLev (abs_SNo x) = SNoLev x
Axiom. (abs_SNo_minus) We take the following as an axiom:
∀x, SNo xabs_SNo (- x) = abs_SNo x
Axiom. (abs_SNo_dist_swap) We take the following as an axiom:
∀x y, SNo xSNo yabs_SNo (x + - y) = abs_SNo (y + - x)
Axiom. (SNo_triangle) We take the following as an axiom:
∀x y, SNo xSNo yabs_SNo (x + y) abs_SNo x + abs_SNo y
Axiom. (SNo_triangle2) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zabs_SNo (x + - z) abs_SNo (x + - y) + abs_SNo (y + - z)
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.
Definition. We define SNo_max_of to be λX x ⇒ x X SNo x yX, SNo yy x of type setsetprop.
Definition. We define SNo_min_of to be λX x ⇒ x X SNo x yX, SNo yx y of type setsetprop.
Axiom. (minus_SNo_max_min) We take the following as an axiom:
∀X y, (xX, SNo x)SNo_max_of X ySNo_min_of {- x|xX} (- y)
Axiom. (minus_SNo_max_min') We take the following as an axiom:
∀X y, (xX, SNo x)SNo_max_of {- x|xX} ySNo_min_of X (- y)
Axiom. (minus_SNo_min_max) We take the following as an axiom:
∀X y, (xX, SNo x)SNo_min_of X ySNo_max_of {- x|xX} (- y)
Axiom. (double_SNo_max_1) We take the following as an axiom:
∀x y, SNo xSNo_max_of (SNoL x) y∀z, SNo zx < zy + z < x + xwSNoR z, y + w = x + x
Axiom. (double_SNo_min_1) We take the following as an axiom:
∀x y, SNo xSNo_min_of (SNoR x) y∀z, SNo zz < xx + x < y + zwSNoL z, y + w = x + x
Axiom. (finite_max_exists) We take the following as an axiom:
∀X, (xX, SNo x)finite XX 0x, SNo_max_of X x
Axiom. (finite_min_exists) We take the following as an axiom:
∀X, (xX, SNo x)finite XX 0x, SNo_min_of X x
Axiom. (SNoS_omega_SNoL_max_exists) We take the following as an axiom:
Axiom. (SNoS_omega_SNoR_min_exists) We take the following as an axiom:
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.
Axiom. (nonneg_diadic_rational_p_SNoS_omega) We take the following as an axiom:
kω, ∀n, nat_p neps_ k * n SNoS_ ω
Definition. We define diadic_rational_p to be λx ⇒ kω, mint, x = eps_ k * m of type setprop.
Axiom. (diadic_rational_p_SNoS_omega) We take the following as an axiom:
Axiom. (int_diadic_rational_p) We take the following as an axiom:
Axiom. (omega_diadic_rational_p) We take the following as an axiom:
Axiom. (eps_diadic_rational_p) We take the following as an axiom:
Axiom. (minus_SNo_diadic_rational_p) We take the following as an axiom:
Axiom. (mul_SNo_diadic_rational_p) We take the following as an axiom:
Axiom. (add_SNo_diadic_rational_p) We take the following as an axiom:
Axiom. (SNoS_omega_diadic_rational_p_lem) We take the following as an axiom:
∀n, nat_p n∀x, SNo xSNoLev x = ndiadic_rational_p x
Axiom. (SNoS_omega_diadic_rational_p) We take the following as an axiom:
Axiom. (mul_SNo_SNoS_omega) We take the following as an axiom:
End of Section DiadicRationals
Beginning of Section SurrealDiv
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.
Definition. We define SNoL_pos to be λx ⇒ {wSNoL x|0 < w} of type setset.
Axiom. (SNo_recip_pos_pos) We take the following as an axiom:
∀x xi, SNo xSNo xi0 < xx * xi = 10 < xi
Axiom. (SNo_recip_lem1) We take the following as an axiom:
∀x x' x'i y y', SNo x0 < xx' SNoL_pos xSNo x'ix' * x'i = 1SNo yx * y < 1SNo y'1 + - x * y' = (1 + - x * y) * (x' + - x) * x'i1 < x * y'
Axiom. (SNo_recip_lem2) We take the following as an axiom:
∀x x' x'i y y', SNo x0 < xx' SNoL_pos xSNo x'ix' * x'i = 1SNo y1 < x * ySNo y'1 + - x * y' = (1 + - x * y) * (x' + - x) * x'ix * y' < 1
Axiom. (SNo_recip_lem3) We take the following as an axiom:
∀x x' x'i y y', SNo x0 < xx' SNoR xSNo x'ix' * x'i = 1SNo yx * y < 1SNo y'1 + - x * y' = (1 + - x * y) * (x' + - x) * x'ix * y' < 1
Axiom. (SNo_recip_lem4) We take the following as an axiom:
∀x x' x'i y y', SNo x0 < xx' SNoR xSNo x'ix' * x'i = 1SNo y1 < x * ySNo y'1 + - x * y' = (1 + - x * y) * (x' + - x) * x'i1 < x * y'
Definition. We define SNo_recipauxset to be λY x X g ⇒ yY{(1 + (x' + - x) * y) * g x'|x'X} of type setsetset(setset)set.
Axiom. (SNo_recipauxset_I) We take the following as an axiom:
∀Y x X, ∀g : setset, yY, x'X, (1 + (x' + - x) * y) * g x' SNo_recipauxset Y x X g
Axiom. (SNo_recipauxset_E) We take the following as an axiom:
∀Y x X, ∀g : setset, zSNo_recipauxset Y x X g, ∀p : prop, (yY, x'X, z = (1 + (x' + - x) * y) * g x'p)p
Axiom. (SNo_recipauxset_ext) We take the following as an axiom:
∀Y x X, ∀g h : setset, (x'X, g x' = h x')SNo_recipauxset Y x X g = SNo_recipauxset Y x X h
Definition. We define SNo_recipaux to be λx g ⇒ nat_primrec ({0},0) (λk p ⇒ (p 0 SNo_recipauxset (p 0) x (SNoR x) g SNo_recipauxset (p 1) x (SNoL_pos x) g,p 1 SNo_recipauxset (p 0) x (SNoL_pos x) g SNo_recipauxset (p 1) x (SNoR x) g)) of type set(setset)setset.
Axiom. (SNo_recipaux_0) We take the following as an axiom:
∀x, ∀g : setset, SNo_recipaux x g 0 = ({0},0)
Axiom. (SNo_recipaux_S) We take the following as an axiom:
∀x, ∀g : setset, ∀n, nat_p nSNo_recipaux x g (ordsucc n) = (SNo_recipaux x g n 0 SNo_recipauxset (SNo_recipaux x g n 0) x (SNoR x) g SNo_recipauxset (SNo_recipaux x g n 1) x (SNoL_pos x) g,SNo_recipaux x g n 1 SNo_recipauxset (SNo_recipaux x g n 0) x (SNoL_pos x) g SNo_recipauxset (SNo_recipaux x g n 1) x (SNoR x) g)
Axiom. (SNo_recipaux_lem1) We take the following as an axiom:
∀x, SNo x0 < x∀g : setset, (x'SNoS_ (SNoLev x), 0 < x'SNo (g x') x' * g x' = 1)∀k, nat_p k(ySNo_recipaux x g k 0, SNo y x * y < 1) (ySNo_recipaux x g k 1, SNo y 1 < x * y)
Axiom. (SNo_recipaux_lem2) We take the following as an axiom:
∀x, SNo x0 < x∀g : setset, (x'SNoS_ (SNoLev x), 0 < x'SNo (g x') x' * g x' = 1)SNoCutP (kωSNo_recipaux x g k 0) (kωSNo_recipaux x g k 1)
Axiom. (SNo_recipaux_ext) We take the following as an axiom:
∀x, SNo x∀g h : setset, (x'SNoS_ (SNoLev x), g x' = h x')∀k, nat_p kSNo_recipaux x g k = SNo_recipaux x h k
Beginning of Section recip_SNo_pos
Let G : set(setset)setλx g ⇒ SNoCut (kωSNo_recipaux x g k 0) (kωSNo_recipaux x g k 1)
Definition. We define recip_SNo_pos to be SNo_rec_i G of type setset.
Axiom. (recip_SNo_pos_eq) We take the following as an axiom:
∀x, SNo xrecip_SNo_pos x = G x recip_SNo_pos
Axiom. (recip_SNo_pos_prop1) We take the following as an axiom:
∀x, SNo x0 < xSNo (recip_SNo_pos x) x * recip_SNo_pos x = 1
Axiom. (SNo_recip_SNo_pos) We take the following as an axiom:
∀x, SNo x0 < xSNo (recip_SNo_pos x)
Axiom. (recip_SNo_pos_invR) We take the following as an axiom:
∀x, SNo x0 < xx * recip_SNo_pos x = 1
Axiom. (recip_SNo_pos_1) We take the following as an axiom:
Axiom. (recip_SNo_pos_is_pos) We take the following as an axiom:
∀x, SNo x0 < x0 < recip_SNo_pos x
Axiom. (recip_SNo_pos_invol) We take the following as an axiom:
∀x, SNo x0 < xrecip_SNo_pos (recip_SNo_pos x) = x
Axiom. (recip_SNo_pos_eps_) We take the following as an axiom:
∀n, nat_p nrecip_SNo_pos (eps_ n) = 2 ^ n
Axiom. (recip_SNo_pos_pow_2) We take the following as an axiom:
∀n, nat_p nrecip_SNo_pos (2 ^ n) = eps_ n
Axiom. (exp_SNo_nat_1) We take the following as an axiom:
∀x, SNo xx ^ 1 = x
Axiom. (recip_SNo_pos_2) We take the following as an axiom:
End of Section recip_SNo_pos
Definition. We define recip_SNo to be λx ⇒ if 0 < x then recip_SNo_pos x else if x < 0 then - recip_SNo_pos (- x) else 0 of type setset.
Axiom. (recip_SNo_poscase) We take the following as an axiom:
∀x, 0 < xrecip_SNo x = recip_SNo_pos x
Axiom. (recip_SNo_negcase) We take the following as an axiom:
∀x, SNo xx < 0recip_SNo x = - recip_SNo_pos (- x)
Axiom. (recip_SNo_0) We take the following as an axiom:
Axiom. (recip_SNo_1) We take the following as an axiom:
Axiom. (SNo_recip_SNo) We take the following as an axiom:
∀x, SNo xSNo (recip_SNo x)
Axiom. (recip_SNo_invR) We take the following as an axiom:
∀x, SNo xx 0x * recip_SNo x = 1
Axiom. (recip_SNo_invL) We take the following as an axiom:
∀x, SNo xx 0recip_SNo x * x = 1
Axiom. (recip_SNo_eps_) We take the following as an axiom:
∀n, nat_p nrecip_SNo (eps_ n) = 2 ^ n
Axiom. (recip_SNo_pow_2) We take the following as an axiom:
∀n, nat_p nrecip_SNo (2 ^ n) = eps_ n
Axiom. (recip_SNo_2) We take the following as an axiom:
Axiom. (recip_SNo_invol) We take the following as an axiom:
∀x, SNo xrecip_SNo (recip_SNo x) = x
Axiom. (recip_SNo_of_pos_is_pos) We take the following as an axiom:
∀x, SNo x0 < x0 < recip_SNo x
Axiom. (recip_SNo_neg') We take the following as an axiom:
∀x, SNo xx < 0recip_SNo x < 0
Definition. We define div_SNo to be λx y ⇒ x * recip_SNo y of type setsetset.
Notation. We use :/: as an infix operator with priority 353 and no associativity corresponding to applying term div_SNo.
Axiom. (SNo_div_SNo) We take the following as an axiom:
∀x y, SNo xSNo ySNo (x :/: y)
Axiom. (div_SNo_0_num) We take the following as an axiom:
∀x, SNo x0 :/: x = 0
Axiom. (div_SNo_0_denum) We take the following as an axiom:
∀x, SNo xx :/: 0 = 0
Axiom. (mul_div_SNo_invL) We take the following as an axiom:
∀x y, SNo xSNo yy 0(x :/: y) * y = x
Axiom. (mul_div_SNo_invR) We take the following as an axiom:
∀x y, SNo xSNo yy 0y * (x :/: y) = x
Axiom. (mul_div_SNo_R) We take the following as an axiom:
∀x y z, SNo xSNo ySNo z(x :/: y) * z = (x * z) :/: y
Axiom. (mul_div_SNo_L) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zz * (x :/: y) = (z * x) :/: y
Axiom. (div_mul_SNo_invL) We take the following as an axiom:
∀x y, SNo xSNo yy 0(x * y) :/: y = x
Axiom. (div_div_SNo) We take the following as an axiom:
∀x y z, SNo xSNo ySNo z(x :/: y) :/: z = x :/: (y * z)
Axiom. (mul_div_SNo_both) We take the following as an axiom:
∀x y z w, SNo xSNo ySNo zSNo w(x :/: y) * (z :/: w) = (x * z) :/: (y * w)
Axiom. (recip_SNo_pos_pos) We take the following as an axiom:
∀x, SNo x0 < x0 < recip_SNo_pos x
Axiom. (recip_SNo_of_neg_is_neg) We take the following as an axiom:
∀x, SNo xx < 0recip_SNo x < 0
Axiom. (div_SNo_pos_pos) We take the following as an axiom:
∀x y, SNo xSNo y0 < x0 < y0 < x :/: y
Axiom. (div_SNo_neg_neg) We take the following as an axiom:
∀x y, SNo xSNo yx < 0y < 00 < x :/: y
Axiom. (div_SNo_pos_neg) We take the following as an axiom:
∀x y, SNo xSNo y0 < xy < 0x :/: y < 0
Axiom. (div_SNo_neg_pos) We take the following as an axiom:
∀x y, SNo xSNo yx < 00 < yx :/: y < 0
Axiom. (div_SNo_pos_LtL) We take the following as an axiom:
∀x y z, SNo xSNo ySNo z0 < yx < z * yx :/: y < z
Axiom. (div_SNo_pos_LtR) We take the following as an axiom:
∀x y z, SNo xSNo ySNo z0 < yz * y < xz < x :/: y
Axiom. (div_SNo_pos_LtL') We take the following as an axiom:
∀x y z, SNo xSNo ySNo z0 < yx :/: y < zx < z * y
Axiom. (div_SNo_pos_LtR') We take the following as an axiom:
∀x y z, SNo xSNo ySNo z0 < yz < x :/: yz * y < x
Axiom. (mul_div_SNo_nonzero_eq) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zy 0x = y * zx :/: y = z
End of Section SurrealDiv
Beginning of Section SurrealSqrt
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 353 and no associativity corresponding to applying term div_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.
Definition. We define SNoL_nonneg to be λx ⇒ {wSNoL x|0 w} of type setset.
Axiom. (SNoL_nonneg_0) We take the following as an axiom:
Axiom. (SNoL_nonneg_1) We take the following as an axiom:
Definition. We define SNo_sqrtauxset to be λY Z x ⇒ yY{(x + y * z) :/: (y + z)|zZ, 0 < y + z} of type setsetsetset.
Axiom. (SNo_sqrtauxset_I) We take the following as an axiom:
∀Y Z x, yY, zZ, 0 < y + z(x + y * z) :/: (y + z) SNo_sqrtauxset Y Z x
Axiom. (SNo_sqrtauxset_E) We take the following as an axiom:
∀Y Z x, uSNo_sqrtauxset Y Z x, ∀p : prop, (yY, zZ, 0 < y + zu = (x + y * z) :/: (y + z)p)p
Axiom. (SNo_sqrtauxset_0) We take the following as an axiom:
∀Z x, SNo_sqrtauxset 0 Z x = 0
Axiom. (SNo_sqrtauxset_0') We take the following as an axiom:
∀Y x, SNo_sqrtauxset Y 0 x = 0
Definition. We define SNo_sqrtaux to be λx g ⇒ nat_primrec ({g w|wSNoL_nonneg x},{g z|zSNoR x}) (λk p ⇒ (p 0 SNo_sqrtauxset (p 0) (p 1) x,p 1 SNo_sqrtauxset (p 0) (p 0) x SNo_sqrtauxset (p 1) (p 1) x)) of type set(setset)setset.
Axiom. (SNo_sqrtaux_0) We take the following as an axiom:
∀x, ∀g : setset, SNo_sqrtaux x g 0 = ({g w|wSNoL_nonneg x},{g z|zSNoR x})
Axiom. (SNo_sqrtaux_S) We take the following as an axiom:
∀x, ∀g : setset, ∀n, nat_p nSNo_sqrtaux x g (ordsucc n) = (SNo_sqrtaux x g n 0 SNo_sqrtauxset (SNo_sqrtaux x g n 0) (SNo_sqrtaux x g n 1) x,SNo_sqrtaux x g n 1 SNo_sqrtauxset (SNo_sqrtaux x g n 0) (SNo_sqrtaux x g n 0) x SNo_sqrtauxset (SNo_sqrtaux x g n 1) (SNo_sqrtaux x g n 1) x)
Axiom. (SNo_sqrtaux_mon_lem) We take the following as an axiom:
∀x, ∀g : setset, ∀m, nat_p m∀n, nat_p nSNo_sqrtaux x g m 0 SNo_sqrtaux x g (add_nat m n) 0 SNo_sqrtaux x g m 1 SNo_sqrtaux x g (add_nat m n) 1
Axiom. (SNo_sqrtaux_mon) We take the following as an axiom:
∀x, ∀g : setset, ∀m, nat_p m∀n, nat_p nm nSNo_sqrtaux x g m 0 SNo_sqrtaux x g n 0 SNo_sqrtaux x g m 1 SNo_sqrtaux x g n 1
Axiom. (SNo_sqrtaux_ext) We take the following as an axiom:
∀x, SNo x∀g h : setset, (x'SNoS_ (SNoLev x), g x' = h x')∀k, nat_p kSNo_sqrtaux x g k = SNo_sqrtaux x h k
Beginning of Section sqrt_SNo_nonneg
Let G : set(setset)setλx g ⇒ SNoCut (kωSNo_sqrtaux x g k 0) (kωSNo_sqrtaux x g k 1)
Axiom. (sqrt_SNo_nonneg_eq) We take the following as an axiom:
Axiom. (sqrt_SNo_nonneg_prop1a) We take the following as an axiom:
Axiom. (sqrt_SNo_nonneg_prop1c) We take the following as an axiom:
∀x, SNo x0 xSNoCutP (kωSNo_sqrtaux x sqrt_SNo_nonneg k 0) (kωSNo_sqrtaux x sqrt_SNo_nonneg k 1)(z(kωSNo_sqrtaux x sqrt_SNo_nonneg k 1), ∀p : prop, (SNo z0 zx < z * zp)p)0 G x sqrt_SNo_nonneg
Axiom. (sqrt_SNo_nonneg_prop1) We take the following as an axiom:
End of Section sqrt_SNo_nonneg
Axiom. (SNo_sqrtaux_0_1_prop) We take the following as an axiom:
∀x, SNo x0 x∀k, nat_p k(ySNo_sqrtaux x sqrt_SNo_nonneg k 0, SNo y 0 y y * y < x) (ySNo_sqrtaux x sqrt_SNo_nonneg k 1, SNo y 0 y x < y * y)
Axiom. (SNo_sqrtaux_0_prop) We take the following as an axiom:
∀x, SNo x0 x∀k, nat_p kySNo_sqrtaux x sqrt_SNo_nonneg k 0, SNo y 0 y y * y < x
Axiom. (SNo_sqrtaux_1_prop) We take the following as an axiom:
∀x, SNo x0 x∀k, nat_p kySNo_sqrtaux x sqrt_SNo_nonneg k 1, SNo y 0 y x < y * y
Axiom. (SNo_sqrt_SNo_SNoCutP) We take the following as an axiom:
Axiom. (SNo_sqrt_SNo_nonneg) We take the following as an axiom:
∀x, SNo x0 xSNo (sqrt_SNo_nonneg x)
Axiom. (sqrt_SNo_nonneg_nonneg) We take the following as an axiom:
∀x, SNo x0 x0 sqrt_SNo_nonneg x
Axiom. (sqrt_SNo_nonneg_sqr) We take the following as an axiom:
∀x, SNo x0 xsqrt_SNo_nonneg x * sqrt_SNo_nonneg x = x
Axiom. (sqrt_SNo_nonneg_0) We take the following as an axiom:
Axiom. (sqrt_SNo_nonneg_1) We take the following as an axiom:
End of Section SurrealSqrt
Beginning of Section Reals
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 353 and no associativity corresponding to applying term div_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.
Axiom. (SNoS_omega_drat_intvl) We take the following as an axiom:
Axiom. (SNoS_ordsucc_omega_bdd_above) We take the following as an axiom:
Axiom. (SNoS_ordsucc_omega_bdd_below) We take the following as an axiom:
Axiom. (SNoS_ordsucc_omega_bdd_drat_intvl) We take the following as an axiom:
Primitive. The name real is a term of type set.
Definition. We define rational to be {xreal|mint, nω {0}, x = m :/: n} of type set.
Axiom. (real_I) We take the following as an axiom:
xSNoS_ (ordsucc ω), x ωx - ω(qSNoS_ ω, (kω, abs_SNo (q + - x) < eps_ k)q = x)x real
Axiom. (real_E) We take the following as an axiom:
xreal, ∀p : prop, (SNo xSNoLev x ordsucc ωx SNoS_ (ordsucc ω)- ω < xx < ω(qSNoS_ ω, (kω, abs_SNo (q + - x) < eps_ k)q = x)(kω, qSNoS_ ω, q < x x < q + eps_ k)p)p
Axiom. (real_SNo) We take the following as an axiom:
Axiom. (real_SNoS_omega_prop) We take the following as an axiom:
Axiom. (SNoS_omega_real) We take the following as an axiom:
Axiom. (real_0) We take the following as an axiom:
Axiom. (real_1) We take the following as an axiom:
Axiom. (SNoLev_In_real_SNoS_omega) We take the following as an axiom:
xreal, ∀w, SNo wSNoLev w SNoLev xw SNoS_ ω
Axiom. (real_SNoCut_SNoS_omega) We take the following as an axiom:
L RSNoS_ ω, SNoCutP L RL 0R 0(wL, w'L, w < w')(zR, z'R, z' < z)SNoCut L R real
Axiom. (real_SNoCut) We take the following as an axiom:
L Rreal, SNoCutP L RL 0R 0(wL, w'L, w < w')(zR, z'R, z' < z)SNoCut L R real
Axiom. (minus_SNo_prereal_1) We take the following as an axiom:
∀x, SNo x(qSNoS_ ω, (kω, abs_SNo (q + - x) < eps_ k)q = x)(qSNoS_ ω, (kω, abs_SNo (q + - - x) < eps_ k)q = - x)
Axiom. (minus_SNo_prereal_2) We take the following as an axiom:
∀x, SNo x(kω, qSNoS_ ω, q < x x < q + eps_ k)(kω, qSNoS_ ω, q < - x - x < q + eps_ k)
Axiom. (SNo_prereal_incr_lower_pos) We take the following as an axiom:
∀x, SNo x0 < x(qSNoS_ ω, (kω, abs_SNo (q + - x) < eps_ k)q = x)(kω, qSNoS_ ω, q < x x < q + eps_ k)kω, ∀p : prop, (qSNoS_ ω, 0 < qq < xx < q + eps_ kp)p
Axiom. (real_minus_SNo) We take the following as an axiom:
Axiom. (SNo_prereal_incr_lower_approx) We take the following as an axiom:
∀x, SNo x(qSNoS_ ω, (kω, abs_SNo (q + - x) < eps_ k)q = x)(kω, qSNoS_ ω, q < x x < q + eps_ k)fSNoS_ ωω, nω, f n < x x < f n + eps_ n in, f i < f n
Axiom. (SNo_prereal_decr_upper_approx) We take the following as an axiom:
∀x, SNo x(qSNoS_ ω, (kω, abs_SNo (q + - x) < eps_ k)q = x)(kω, qSNoS_ ω, q < x x < q + eps_ k)gSNoS_ ωω, nω, g n + - eps_ n < x x < g n in, g n < g i
Axiom. (SNoCutP_SNoCut_lim) We take the following as an axiom:
∀lambda, ordinal lambda(alphalambda, ordsucc alpha lambda)L RSNoS_ lambda, SNoCutP L RSNoLev (SNoCut L R) ordsucc lambda
Axiom. (SNoCutP_SNoCut_omega) We take the following as an axiom:
Axiom. (SNo_approx_real_lem) We take the following as an axiom:
Axiom. (SNo_approx_real) We take the following as an axiom:
∀x, SNo xf gSNoS_ ωω, (nω, f n < x)(nω, x < f n + eps_ n)(nω, in, f i < f n)(nω, x < g n)(nω, in, g n < g i)x = SNoCut {f n|nω} {g n|nω}x real
Axiom. (SNo_approx_real_rep) We take the following as an axiom:
xreal, ∀p : prop, (f gSNoS_ ωω, (nω, f n < x)(nω, x < f n + eps_ n)(nω, in, f i < f n)(nω, g n + - eps_ n < x)(nω, x < g n)(nω, in, g n < g i)SNoCutP {f n|nω} {g n|nω}x = SNoCut {f n|nω} {g n|nω}p)p
Axiom. (real_add_SNo) We take the following as an axiom:
Axiom. (SNoS_ordsucc_omega_bdd_eps_pos) We take the following as an axiom:
Axiom. (real_mul_SNo_pos) We take the following as an axiom:
x yreal, 0 < x0 < yx * y real
Axiom. (real_mul_SNo) We take the following as an axiom:
Axiom. (abs_SNo_intvl_bd) We take the following as an axiom:
∀x y z, SNo xSNo ySNo zx yy < x + zabs_SNo (y + - x) < z
Axiom. (nonneg_real_nat_interval) We take the following as an axiom:
Axiom. (pos_real_left_approx_double) We take the following as an axiom:
Axiom. (real_recip_SNo_lem1) We take the following as an axiom:
Axiom. (real_recip_SNo_pos) We take the following as an axiom:
Axiom. (real_recip_SNo) We take the following as an axiom:
Axiom. (real_div_SNo) We take the following as an axiom:
Axiom. (sqrt_SNo_nonneg_0inL0) We take the following as an axiom:
∀x, SNo x0 x0 SNoLev x0 SNo_sqrtaux x sqrt_SNo_nonneg 0 0
Axiom. (sqrt_SNo_nonneg_Lnonempty) We take the following as an axiom:
∀x, SNo x0 x0 SNoLev x(kωSNo_sqrtaux x sqrt_SNo_nonneg k 0) 0
Axiom. (sqrt_SNo_nonneg_Rnonempty) We take the following as an axiom:
∀x, SNo x0 x1 SNoLev x(kωSNo_sqrtaux x sqrt_SNo_nonneg k 1) 0
Axiom. (SNo_sqrtauxset_real) We take the following as an axiom:
∀Y Z x, Y realZ realx realSNo_sqrtauxset Y Z x real
Axiom. (SNo_sqrtauxset_real_nonneg) We take the following as an axiom:
∀Y Z x, Y {wreal|0 w}Z {zreal|0 z}x real0 xSNo_sqrtauxset Y Z x {wreal|0 w}
Axiom. (sqrt_SNo_nonneg_SNoS_omega) We take the following as an axiom:
Axiom. (sqrt_SNo_nonneg_real) We take the following as an axiom:
Axiom. (real_Archimedean) We take the following as an axiom:
x yreal, 0 < x0 ynω, y n * x
Axiom. (real_complete1) We take the following as an axiom:
Axiom. (real_complete2) We take the following as an axiom:
a brealω, (nω, a n b n a n a (n + 1) b (n + 1) b n)xreal, nω, a n x x b n
End of Section Reals
Theorem. (mul_nat_1R) The following is provable:
∀x0, mul_nat x0 1 = x0
Proof:
Let m be given.
rewrite the current goal using mul_nat_SR m 0 nat_0 (from left to right).
We will prove add_nat m (mul_nat m 0) = m.
rewrite the current goal using mul_nat_0R m (from left to right).
Apply add_nat_0R to the current goal.
Theorem. (mul_nat_asso) The following is provable:
(∀x0, nat_p x0(∀x1, nat_p x1(∀x2, nat_p x2mul_nat (mul_nat x0 x1) x2 = mul_nat x0 (mul_nat x1 x2))))
Proof:
Let k be given.
Assume Hk.
Let m be given.
Assume Hm.
Let n be given.
Assume Hn.
rewrite the current goal using mul_nat_mul_SNo (mul_nat k m) (nat_p_omega (mul_nat k m) (mul_nat_p k Hk m Hm)) n (nat_p_omega n Hn) (from left to right).
rewrite the current goal using mul_nat_mul_SNo k (nat_p_omega k Hk) (mul_nat m n) (nat_p_omega (mul_nat m n) (mul_nat_p m Hm n Hn)) (from left to right).
rewrite the current goal using mul_nat_mul_SNo k (nat_p_omega k Hk) m (nat_p_omega m Hm) (from left to right).
rewrite the current goal using mul_nat_mul_SNo m (nat_p_omega m Hm) n (nat_p_omega n Hn) (from left to right).
Use symmetry.
An exact proof term for the current goal is mul_SNo_assoc k m n (nat_p_SNo k Hk) (nat_p_SNo m Hm) (nat_p_SNo n Hn).
Theorem. (mul_nat_com) The following is provable:
(∀x0, nat_p x0(∀x1, nat_p x1mul_nat x0 x1 = mul_nat x1 x0))
Proof:
Let m be given.
Assume Hm.
Let n be given.
Assume Hn.
rewrite the current goal using mul_nat_mul_SNo m (nat_p_omega m Hm) n (nat_p_omega n Hn) (from left to right).
rewrite the current goal using mul_nat_mul_SNo n (nat_p_omega n Hn) m (nat_p_omega m Hm) (from left to right).
An exact proof term for the current goal is mul_SNo_com m n (nat_p_SNo m Hm) (nat_p_SNo n Hn).
Theorem. (mul_nat_SL) The following is provable:
(∀x0, nat_p x0(∀x1, nat_p x1mul_nat (ordsucc x0) x1 = add_nat (mul_nat x0 x1) x1))
Proof:
Let m be given.
Assume Hm.
Let n be given.
Assume Hn.
rewrite the current goal using mul_nat_com (ordsucc m) (nat_ordsucc m Hm) n Hn (from left to right).
rewrite the current goal using mul_nat_SR n m Hm (from left to right).
We will prove add_nat n (mul_nat n m) = add_nat (mul_nat m n) n.
rewrite the current goal using mul_nat_com n Hn m Hm (from left to right).
We will prove add_nat n (mul_nat m n) = add_nat (mul_nat m n) n.
An exact proof term for the current goal is add_nat_com n Hn (mul_nat m n) (mul_nat_p m Hm n Hn).
Theorem. (eps_1_half_eq3) The following is provable:
Proof:
rewrite the current goal using mul_SNo_com (eps_ 1) 2 SNo_eps_1 SNo_2 (from left to right).
An exact proof term for the current goal is eps_1_half_eq2.
Theorem. (double_nat_cancel) The following is provable:
(∀x0, nat_p x0(∀x1, nat_p x1mul_nat 2 x0 = mul_nat 2 x1x0 = x1))
Proof:
Let x0 of type set be given.
Assume H0: nat_p x0.
Let x1 of type set be given.
Assume H1: nat_p x1.
An exact proof term for the current goal is (mul_nat_mul_SNo 2 (nat_p_omega 2 nat_2) x0 (nat_p_omega x0 H0) (λx2 x3 : setx3 = mul_nat 2 x1x0 = x1) (mul_nat_mul_SNo 2 (nat_p_omega 2 nat_2) x1 (nat_p_omega x1 H1) (λx2 x3 : setmul_SNo 2 x0 = x3x0 = x1) (λH2 : mul_SNo 2 x0 = mul_SNo 2 x1(mul_SNo_oneL x0 (nat_p_SNo x0 H0) (λx2 x3 : setx2 = x1) (mul_SNo_oneL x1 (nat_p_SNo x1 H1) (λx2 x3 : setmul_SNo 1 x0 = x2) (eps_1_half_eq3 (λx2 x3 : setmul_SNo x2 x0 = mul_SNo x2 x1) (mul_SNo_assoc (eps_ 1) 2 x0 (SNo_eps_ 1 (nat_p_omega 1 nat_1)) (nat_p_SNo 2 nat_2) (nat_p_SNo x0 H0) (λx2 x3 : setx2 = mul_SNo (mul_SNo (eps_ 1) 2) x1) (mul_SNo_assoc (eps_ 1) 2 x1 (SNo_eps_ 1 (nat_p_omega 1 nat_1)) (nat_p_SNo 2 nat_2) (nat_p_SNo x1 H1) (λx2 x3 : setmul_SNo (eps_ 1) (mul_SNo 2 x0) = x2) (H2 (λx2 x3 : setmul_SNo (eps_ 1) x3 = mul_SNo (eps_ 1) (mul_SNo 2 x1)) (λx2 : setsetprop(λH3 : x2 (mul_SNo (eps_ 1) (mul_SNo 2 x1)) (mul_SNo (eps_ 1) (mul_SNo 2 x1))H3))))))))))).
Theorem. (add_nat_Subq_L) The following is provable:
(∀x0, nat_p x0(∀x1, nat_p x1x0 add_nat x0 x1))
Proof:
Let x0 of type set be given.
Assume H0: nat_p x0.
An exact proof term for the current goal is (nat_ind (λx1 : setx0 add_nat x0 x1) (add_nat_0R x0 (λx1 x2 : setx0 x2) (Subq_ref x0)) (λx1 : set(λH1 : nat_p x1(λH2 : x0 add_nat x0 x1(add_nat_SR x0 x1 H1 (λx2 x3 : setx0 x3) (Subq_tra x0 (add_nat x0 x1) (ordsucc (add_nat x0 x1)) H2 (ordsuccI1 (add_nat x0 x1)))))))).
Theorem. (square_nat_Subq) The following is provable:
(∀x0, nat_p x0(∀x1, nat_p x1x0 x1mul_nat x0 x0 mul_nat x1 x1))
Proof:
Let x0 of type set be given.
Assume H0: nat_p x0.
An exact proof term for the current goal is (nat_ind (λx1 : setx0 x1mul_nat x0 x0 mul_nat x1 x1) (λH1 : x0 0(Empty_Subq_eq x0 H1 (λx1 x2 : setmul_nat x2 x2 mul_nat 0 0) (Subq_ref (mul_nat 0 0)))) (λx1 : set(λH1 : nat_p x1(λH2 : x0 x1mul_nat x0 x0 mul_nat x1 x1(λH3 : x0 ordsucc x1(ordinal_In_Or_Subq x1 x0 (nat_p_ordinal x1 H1) (nat_p_ordinal x0 H0) (mul_nat x0 x0 mul_nat (ordsucc x1) (ordsucc x1)) (λH4 : x1 x0((λH5 : x0 = ordsucc x1(H5 (λx2 x3 : setmul_nat x0 x0 mul_nat x2 x2) (Subq_ref (mul_nat x0 x0)))) (set_ext x0 (ordsucc x1) H3 (λx2 : set(λH5 : x2 ordsucc x1(ordsuccE x1 x2 H5 (x2 x0) (λH6 : x2 x1(nat_trans x0 H0 x1 H4 x2 H6)) (λH6 : x2 = x1(H6 (λx3 x4 : setx4 x0) H4)))))))) (λH4 : x0 x1((λH5 : mul_nat x0 x0 mul_nat x1 x1(mul_nat_SR (ordsucc x1) x1 H1 (λx2 x3 : setmul_nat x0 x0 x3) (mul_nat_SL x1 H1 x1 H1 (λx2 x3 : setmul_nat x0 x0 add_nat (ordsucc x1) x3) (Subq_tra (mul_nat x0 x0) (mul_nat x1 x1) (add_nat (ordsucc x1) (add_nat (mul_nat x1 x1) x1)) H5 ((λH6 : nat_p (add_nat (mul_nat x1 x1) x1)(add_nat_SL x1 H1 (add_nat (mul_nat x1 x1) x1) H6 (λx2 x3 : setmul_nat x1 x1 x3) (Subq_tra (mul_nat x1 x1) (add_nat x1 (add_nat (mul_nat x1 x1) x1)) (ordsucc (add_nat x1 (add_nat (mul_nat x1 x1) x1))) (Subq_tra (mul_nat x1 x1) (add_nat (mul_nat x1 x1) x1) (add_nat x1 (add_nat (mul_nat x1 x1) x1)) (add_nat_Subq_L (mul_nat x1 x1) (mul_nat_p x1 H1 x1 H1) x1 H1) (add_nat_com x1 H1 (add_nat (mul_nat x1 x1) x1) (add_nat_p (mul_nat x1 x1) (mul_nat_p x1 H1 x1 H1) x1 H1) (λx2 x3 : setadd_nat (mul_nat x1 x1) x1 x3) (add_nat_Subq_L (add_nat (mul_nat x1 x1) x1) (add_nat_p (mul_nat x1 x1) (mul_nat_p x1 H1 x1 H1) x1 H1) x1 H1))) (ordsuccI1 (add_nat x1 (add_nat (mul_nat x1 x1) x1)))))) (add_nat_p (mul_nat x1 x1) (mul_nat_p x1 H1 x1 H1) x1 H1)))))) (H2 H4))))))))).
Theorem. (ordsucc_in_double_nat_ordsucc) The following is provable:
(∀x0, nat_p x0ordsucc x0 mul_nat 2 (ordsucc x0))
Proof:
An exact proof term for the current goal is (nat_ind (λx0 : setordsucc x0 mul_nat 2 (ordsucc x0)) (mul_nat_1R 2 (λx0 x1 : set1 x1) In_1_2) (λx0 : set(λH0 : nat_p x0(λH1 : ordsucc x0 mul_nat 2 (ordsucc x0)(mul_nat_SR 2 (ordsucc x0) (nat_ordsucc x0 H0) (λx1 x2 : setordsucc (ordsucc x0) x2) ((λH2 : nat_p (mul_nat 2 (ordsucc x0))(add_nat_SL 1 nat_1 (mul_nat 2 (ordsucc x0)) H2 (λx1 x2 : setordsucc (ordsucc x0) x2) (add_nat_SL 0 nat_0 (mul_nat 2 (ordsucc x0)) H2 (λx1 x2 : setordsucc (ordsucc x0) ordsucc x2) (add_nat_0L (mul_nat 2 (ordsucc x0)) H2 (λx1 x2 : setordsucc (ordsucc x0) ordsucc (ordsucc x2)) (ordinal_ordsucc_In (ordsucc (mul_nat 2 (ordsucc x0))) (nat_p_ordinal (ordsucc (mul_nat 2 (ordsucc x0))) (nat_ordsucc (mul_nat 2 (ordsucc x0)) H2)) (ordsucc x0) (ordsuccI1 (mul_nat 2 (ordsucc x0)) (ordsucc x0) H1)))))) (mul_nat_p 2 nat_2 (ordsucc x0) (nat_ordsucc x0 H0)))))))).
Theorem. (double_nat_Subq_0) The following is provable:
(∀x0, nat_p x0mul_nat 2 x0 x0x0 = 0)
Proof:
Let x0 of type set be given.
Assume H0: nat_p x0.
An exact proof term for the current goal is (nat_inv x0 H0 (mul_nat 2 x0 x0x0 = 0) (λH1 : x0 = 0(λH2 : mul_nat 2 x0 x0H1)) (λH1 : (x1, and (nat_p x1) (x0 = ordsucc x1))(H1 (mul_nat 2 x0 x0x0 = 0) (λx1 : set(λH2 : (λx2 : setand (nat_p x2) (x0 = ordsucc x2)) x1(H2 (mul_nat 2 x0 x0x0 = 0) (λH3 : nat_p x1(λH4 : x0 = ordsucc x1(H4 (λx2 x3 : setmul_nat 2 x3 x3x3 = 0) (λH5 : mul_nat 2 (ordsucc x1) ordsucc x1(FalseE (In_irref (ordsucc x1) (H5 (ordsucc x1) (ordsucc_in_double_nat_ordsucc x1 H3))) (ordsucc x1 = 0)))))))))))).
Definition. We define even_nat to be (λx0 : setand (x0 ω) (∀x1 : prop, (∀x2, and (x2 ω) (x0 = mul_nat 2 x2)x1)x1)) of type setprop.
Definition. We define odd_nat to be (λx0 : setand (x0 ω) (∀x1, x1 ωx0 = mul_nat 2 x1(∀x2 : prop, x2))) of type setprop.
Theorem. (even_nat_0) The following is provable:
Proof:
An exact proof term for the current goal is (andI (0 ω) (x0, and (x0 ω) (0 = mul_nat 2 x0)) (nat_p_omega 0 nat_0) (λx0 : prop(λH0 : (∀x1, and (x1 ω) (0 = mul_nat 2 x1)x0)(H0 0 (andI (0 ω) (0 = mul_nat 2 0) (nat_p_omega 0 nat_0) (λx1 : setsetprop(mul_nat_0R 2 (λx2 x3 : setx1 x3 x2)))))))).
Theorem. (even_nat_not_odd_nat) The following is provable:
(∀x0, even_nat x0not (odd_nat x0))
Proof:
Let x0 of type set be given.
Assume H0: even_nat x0.
An exact proof term for the current goal is (H0 (not (odd_nat x0)) (λH1 : x0 ω(λH2 : (x1, and (x1 ω) (x0 = mul_nat 2 x1))(H2 (not (odd_nat x0)) (λx1 : set(λH3 : (λx2 : setand (x2 ω) (x0 = mul_nat 2 x2)) x1(H3 (not (odd_nat x0)) (λH4 : x1 ω(λH5 : x0 = mul_nat 2 x1(λH6 : odd_nat x0(H6 False (λH7 : x0 ω(λH8 : (∀x2, x2 ωx0 = mul_nat 2 x2(∀x3 : prop, x3))(H8 x1 H4 H5)))))))))))))).
Theorem. (odd_nat_1) The following is provable:
Proof:
An exact proof term for the current goal is (andI (1 ω) (∀x0, x0 ω1 = mul_nat 2 x0(∀x1 : prop, x1)) (nat_p_omega 1 nat_1) (λx0 : set(λH0 : x0 ω(λH1 : 1 = mul_nat 2 x0(nat_inv x0 (omega_nat_p x0 H0) False (λH2 : x0 = 0(neq_1_0 ((λx1 x2 : set(λH3 : (∀x3 : setprop, x3 x2x3 x1)(λx3 : setsetprop(H3 (λx4 : setx3 x4 x2x3 x2 x4) (λH4 : x3 x2 x2H4))))) 1 0 (λx1 : setprop(λH3 : x1 0(H1 (λx2 : setx1) (H2 (λx2 x3 : setmul_nat 2 x3 = 0) (mul_nat_0R 2) (λx2 : setx1) H3))))))) (λH2 : (x1, and (nat_p x1) (x0 = ordsucc x1))(H2 False (λx1 : set(λH3 : (λx2 : setand (nat_p x2) (x0 = ordsucc x2)) x1(H3 False (λH4 : nat_p x1(λH5 : x0 = ordsucc x1(In_irref 1 (H1 (λx2 x3 : set1 x3) (H5 (λx2 x3 : set1 mul_nat 2 x3) (mul_nat_SR 2 x1 H4 (λx2 x3 : set1 x3) ((λH6 : nat_p (mul_nat 2 x1)(add_nat_SL 1 nat_1 (mul_nat 2 x1) H6 (λx2 x3 : set1 x3) (add_nat_SL 0 nat_0 (mul_nat 2 x1) H6 (λx2 x3 : set1 ordsucc x3) (add_nat_0L (mul_nat 2 x1) H6 (λx2 x3 : set1 ordsucc (ordsucc x3)) (nat_ordsucc_in_ordsucc (ordsucc (mul_nat 2 x1)) (nat_ordsucc (mul_nat 2 x1) H6) 0 (nat_0_in_ordsucc (mul_nat 2 x1) H6)))))) (mul_nat_p 2 nat_2 x1 H4)))))))))))))))))).
Theorem. (even_nat_double) The following is provable:
(∀x0, nat_p x0even_nat (mul_nat 2 x0))
Proof:
Let x0 of type set be given.
Assume H0: nat_p x0.
An exact proof term for the current goal is (andI (mul_nat 2 x0 ω) (x1, and (x1 ω) (mul_nat 2 x0 = mul_nat 2 x1)) (nat_p_omega (mul_nat 2 x0) (mul_nat_p 2 nat_2 x0 H0)) (λx1 : prop(λH1 : (∀x2, and (x2 ω) (mul_nat 2 x0 = mul_nat 2 x2)x1)(H1 x0 (andI (x0 ω) (mul_nat 2 x0 = mul_nat 2 x0) (nat_p_omega x0 H0) (λx2 : setsetprop(λH2 : x2 (mul_nat 2 x0) (mul_nat 2 x0)H2))))))).
Theorem. (even_nat_S_S) The following is provable:
(∀x0, even_nat x0even_nat (ordsucc (ordsucc x0)))
Proof:
Let x0 of type set be given.
Assume H0: even_nat x0.
An exact proof term for the current goal is (H0 (even_nat (ordsucc (ordsucc x0))) (λH1 : x0 ω(λH2 : (x1, and (x1 ω) (x0 = mul_nat 2 x1))(H2 (even_nat (ordsucc (ordsucc x0))) (λx1 : set(λH3 : (λx2 : setand (x2 ω) (x0 = mul_nat 2 x2)) x1(H3 (even_nat (ordsucc (ordsucc x0))) (λH4 : x1 ω(λH5 : x0 = mul_nat 2 x1(andI (ordsucc (ordsucc x0) ω) (x2, and (x2 ω) (ordsucc (ordsucc x0) = mul_nat 2 x2)) (omega_ordsucc (ordsucc x0) (omega_ordsucc x0 H1)) (λx2 : prop(λH6 : (∀x3, and (x3 ω) (ordsucc (ordsucc x0) = mul_nat 2 x3)x2)(H6 (ordsucc x1) (andI (ordsucc x1 ω) (ordsucc (ordsucc x0) = mul_nat 2 (ordsucc x1)) (omega_ordsucc x1 H4) (mul_nat_SR 2 x1 (omega_nat_p x1 H4) (λx3 x4 : setordsucc (ordsucc x0) = x4) (H5 (λx3 x4 : setordsucc (ordsucc x0) = add_nat 2 x3) (add_nat_SL 1 nat_1 x0 (omega_nat_p x0 H1) (λx3 x4 : setordsucc (ordsucc x0) = x4) ((λx3 x4 : set(λH7 : (∀x5 : setprop, x5 x4x5 x3)(λx5 : setsetprop(H7 (λx6 : setx5 x6 x4x5 x4 x6) (λH8 : x5 x4 x4H8))))) (ordsucc (ordsucc x0)) (ordsucc (add_nat 1 x0)) (λx3 : setprop(λH7 : x3 (ordsucc (add_nat 1 x0))((λx4 : setsetprop(add_nat_SL 0 nat_0 x0 (omega_nat_p x0 H1) (λx5 x6 : setordsucc x0 = x6) ((λx5 x6 : set(λH8 : (∀x7 : setprop, x7 x6x7 x5)(λx7 : setsetprop(H8 (λx8 : setx7 x8 x6x7 x6 x8) (λH9 : x7 x6 x6H9))))) (ordsucc x0) (ordsucc (add_nat 0 x0)) (λx5 : setprop(λH8 : x5 (ordsucc (add_nat 0 x0))((λx6 : setsetprop((λx7 : setsetprop(add_nat_0L x0 (omega_nat_p x0 H1) (λx8 x9 : setx7 x9 x8))) (λx7 x8 : setx6 (ordsucc x7) (ordsucc x8)))) (λx6 : setx5) H8)))) (λx5 x6 : setx4 (ordsucc x5) (ordsucc x6)))) (λx4 : setx3) H7))))))))))))))))))))).
Theorem. (even_nat_S_S_inv) The following is provable:
(∀x0, nat_p x0even_nat (ordsucc (ordsucc x0))even_nat x0)
Proof:
Let x0 of type set be given.
Assume H0: nat_p x0.
Assume H1: even_nat (ordsucc (ordsucc x0)).
An exact proof term for the current goal is (H1 (even_nat x0) (λH2 : ordsucc (ordsucc x0) ω(λH3 : (x1, and (x1 ω) (ordsucc (ordsucc x0) = mul_nat 2 x1))(andI (x0 ω) (x1, and (x1 ω) (x0 = mul_nat 2 x1)) (nat_p_omega x0 H0) (H3 (x1, and (x1 ω) (x0 = mul_nat 2 x1)) (λx1 : set(λH4 : (λx2 : setand (x2 ω) (ordsucc (ordsucc x0) = mul_nat 2 x2)) x1(H4 (x2, and (x2 ω) (x0 = mul_nat 2 x2)) (λH5 : x1 ω(λH6 : ordsucc (ordsucc x0) = mul_nat 2 x1(nat_inv x1 (omega_nat_p x1 H5) (x2, and (x2 ω) (x0 = mul_nat 2 x2)) (λH7 : x1 = 0(neq_ordsucc_0 (ordsucc x0) ((λx2 x3 : set(λH8 : (∀x4 : setprop, x4 x3x4 x2)(λx4 : setsetprop(H8 (λx5 : setx4 x5 x3x4 x3 x5) (λH9 : x4 x3 x3H9))))) (ordsucc (ordsucc x0)) 0 (λx2 : setprop(λH8 : x2 0(H6 (λx3 : setx2) (H7 (λx3 x4 : setmul_nat 2 x4 = 0) (mul_nat_0R 2) (λx3 : setx2) H8))))) (x2, and (x2 ω) (x0 = mul_nat 2 x2)))) (λH7 : (x2, and (nat_p x2) (x1 = ordsucc x2))(H7 (x2, and (x2 ω) (x0 = mul_nat 2 x2)) (λx2 : set(λH8 : (λx3 : setand (nat_p x3) (x1 = ordsucc x3)) x2(H8 (x3, and (x3 ω) (x0 = mul_nat 2 x3)) (λH9 : nat_p x2(λH10 : x1 = ordsucc x2(λx3 : prop(λH11 : (∀x4, and (x4 ω) (x0 = mul_nat 2 x4)x3)(H11 x2 (andI (x2 ω) (x0 = mul_nat 2 x2) (nat_p_omega x2 H9) (ordsucc_inj x0 (mul_nat 2 x2) (ordsucc_inj (ordsucc x0) (ordsucc (mul_nat 2 x2)) (H6 (λx4 x5 : setx5 = ordsucc (ordsucc (mul_nat 2 x2))) (H10 (λx4 x5 : setmul_nat 2 x5 = ordsucc (ordsucc (mul_nat 2 x2))) (mul_nat_SR 2 x2 H9 (λx4 x5 : setx5 = ordsucc (ordsucc (mul_nat 2 x2))) ((λH12 : nat_p (mul_nat 2 x2)(add_nat_SL 1 nat_1 (mul_nat 2 x2) H12 (λx4 x5 : setx5 = ordsucc (ordsucc (mul_nat 2 x2))) ((λx4 x5 : set(λH13 : (∀x6 : setprop, x6 x5x6 x4)(λx6 : setsetprop(H13 (λx7 : setx6 x7 x5x6 x5 x7) (λH14 : x6 x5 x5H14))))) (ordsucc (add_nat 1 (mul_nat 2 x2))) (ordsucc (ordsucc (mul_nat 2 x2))) (λx4 : setprop(λH13 : x4 (ordsucc (ordsucc (mul_nat 2 x2)))((λx5 : setsetprop(add_nat_SL 0 nat_0 (mul_nat 2 x2) H12 (λx6 x7 : setx7 = ordsucc (mul_nat 2 x2)) ((λx6 x7 : set(λH14 : (∀x8 : setprop, x8 x7x8 x6)(λx8 : setsetprop(H14 (λx9 : setx8 x9 x7x8 x7 x9) (λH15 : x8 x7 x7H15))))) (ordsucc (add_nat 0 (mul_nat 2 x2))) (ordsucc (mul_nat 2 x2)) (λx6 : setprop(λH14 : x6 (ordsucc (mul_nat 2 x2))((λx7 : setsetprop(add_nat_0L (mul_nat 2 x2) H12 (λx8 x9 : setx7 (ordsucc x8) (ordsucc x9)))) (λx7 : setx6) H14)))) (λx6 x7 : setx5 (ordsucc x6) (ordsucc x7)))) (λx5 : setx4) H13)))))) (mul_nat_p 2 nat_2 x2 H9))))))))))))))))))))))))))))).
Theorem. (even_nat_xor_S) The following is provable:
(∀x0, nat_p x0exactly1of2 (even_nat x0) (even_nat (ordsucc x0)))
Proof:
An exact proof term for the current goal is (nat_ind (λx0 : setexactly1of2 (even_nat x0) (even_nat (ordsucc x0))) (exactly1of2_I1 (even_nat 0) (even_nat 1) (andI (0 ω) (x0, and (x0 ω) (0 = mul_nat 2 x0)) (nat_p_omega 0 nat_0) (λx0 : prop(λH0 : (∀x1, and (x1 ω) (0 = mul_nat 2 x1)x0)(H0 0 (andI (0 ω) (0 = mul_nat 2 0) (nat_p_omega 0 nat_0) (λx1 : setsetprop(mul_nat_0R 2 (λx2 x3 : setx1 x3 x2)))))))) (λH0 : even_nat 1(even_nat_not_odd_nat 1 H0 odd_nat_1))) (λx0 : set(λH0 : nat_p x0(λH1 : exactly1of2 (even_nat x0) (even_nat (ordsucc x0))(exactly1of2_E (even_nat x0) (even_nat (ordsucc x0)) H1 (exactly1of2 (even_nat (ordsucc x0)) (even_nat (ordsucc (ordsucc x0)))) (λH2 : even_nat x0(λH3 : not (even_nat (ordsucc x0))(exactly1of2_I2 (even_nat (ordsucc x0)) (even_nat (ordsucc (ordsucc x0))) H3 (even_nat_S_S x0 H2)))) (λH2 : not (even_nat x0)(λH3 : even_nat (ordsucc x0)(exactly1of2_I1 (even_nat (ordsucc x0)) (even_nat (ordsucc (ordsucc x0))) H3 (λH4 : even_nat (ordsucc (ordsucc x0))(H2 (even_nat_S_S_inv x0 H0 H4))))))))))).
Theorem. (even_nat_or_odd_nat) The following is provable:
(∀x0, nat_p x0or (even_nat x0) (odd_nat x0))
Proof:
An exact proof term for the current goal is (nat_ind (λx0 : setor (even_nat x0) (odd_nat x0)) (orIL (even_nat 0) (odd_nat 0) even_nat_0) (λx0 : set(λH0 : nat_p x0(λH1 : or (even_nat x0) (odd_nat x0)(H1 (or (even_nat (ordsucc x0)) (odd_nat (ordsucc x0))) (λH2 : even_nat x0(orIR (even_nat (ordsucc x0)) (odd_nat (ordsucc x0)) (exactly1of2_E (even_nat x0) (even_nat (ordsucc x0)) (even_nat_xor_S x0 H0) (odd_nat (ordsucc x0)) (λH3 : even_nat x0(λH4 : not (even_nat (ordsucc x0))(andI (ordsucc x0 ω) (∀x1, x1 ωordsucc x0 = mul_nat 2 x1(∀x2 : prop, x2)) (omega_ordsucc x0 (nat_p_omega x0 H0)) (λx1 : set(λH5 : x1 ω(λH6 : ordsucc x0 = mul_nat 2 x1(H4 (andI (ordsucc x0 ω) (x2, and (x2 ω) (ordsucc x0 = mul_nat 2 x2)) (omega_ordsucc x0 (nat_p_omega x0 H0)) (λx2 : prop(λH7 : (∀x3, and (x3 ω) (ordsucc x0 = mul_nat 2 x3)x2)(H7 x1 (andI (x1 ω) (ordsucc x0 = mul_nat 2 x1) H5 H6)))))))))))) (λH3 : not (even_nat x0)(FalseE (H3 H2) (even_nat (ordsucc x0)odd_nat (ordsucc x0))))))) (λH2 : odd_nat x0(orIL (even_nat (ordsucc x0)) (odd_nat (ordsucc x0)) (exactly1of2_E (even_nat x0) (even_nat (ordsucc x0)) (even_nat_xor_S x0 H0) (even_nat (ordsucc x0)) (λH3 : even_nat x0(FalseE (even_nat_not_odd_nat x0 H3 H2) (not (even_nat (ordsucc x0))even_nat (ordsucc x0)))) (λH3 : not (even_nat x0)(λH4 : even_nat (ordsucc x0)H4)))))))))).
Theorem. (not_odd_nat_0) The following is provable:
Proof:
Assume H0: odd_nat 0.
An exact proof term for the current goal is (even_nat_not_odd_nat 0 even_nat_0 H0).
Theorem. (even_nat_odd_nat_S) The following is provable:
(∀x0, even_nat x0odd_nat (ordsucc x0))
Proof:
Let x0 of type set be given.
Assume H0: even_nat x0.
An exact proof term for the current goal is (H0 (odd_nat (ordsucc x0)) (λH1 : x0 ω(λH2 : (x1, and (x1 ω) (x0 = mul_nat 2 x1))(exactly1of2_E (even_nat x0) (even_nat (ordsucc x0)) (even_nat_xor_S x0 (omega_nat_p x0 H1)) (odd_nat (ordsucc x0)) (λH3 : even_nat x0(λH4 : not (even_nat (ordsucc x0))(even_nat_or_odd_nat (ordsucc x0) (nat_ordsucc x0 (omega_nat_p x0 H1)) (odd_nat (ordsucc x0)) (λH5 : even_nat (ordsucc x0)(FalseE (H4 H5) (odd_nat (ordsucc x0)))) (λH5 : odd_nat (ordsucc x0)H5)))) (λH3 : not (even_nat x0)(FalseE (H3 H0) (even_nat (ordsucc x0)odd_nat (ordsucc x0)))))))).
Theorem. (odd_nat_even_nat_S) The following is provable:
(∀x0, odd_nat x0even_nat (ordsucc x0))
Proof:
Let x0 of type set be given.
Assume H0: odd_nat x0.
An exact proof term for the current goal is (H0 (even_nat (ordsucc x0)) (λH1 : x0 ω(λH2 : (∀x1, x1 ωx0 = mul_nat 2 x1(∀x2 : prop, x2))(exactly1of2_E (even_nat x0) (even_nat (ordsucc x0)) (even_nat_xor_S x0 (omega_nat_p x0 H1)) (even_nat (ordsucc x0)) (λH3 : even_nat x0(FalseE (even_nat_not_odd_nat x0 H3 H0) (not (even_nat (ordsucc x0))even_nat (ordsucc x0)))) (λH3 : not (even_nat x0)(λH4 : even_nat (ordsucc x0)H4)))))).
Theorem. (odd_nat_xor_odd_sum) The following is provable:
(∀x0, odd_nat x0(∀x1, nat_p x1exactly1of2 (odd_nat x1) (odd_nat (add_nat x0 x1))))
Proof:
Let x0 of type set be given.
Assume H0: odd_nat x0.
An exact proof term for the current goal is (H0 (∀x1, nat_p x1exactly1of2 (odd_nat x1) (odd_nat (add_nat x0 x1))) (λH1 : x0 ω(λH2 : (∀x1, x1 ωx0 = mul_nat 2 x1(∀x2 : prop, x2))(nat_ind (λx1 : setexactly1of2 (odd_nat x1) (odd_nat (add_nat x0 x1))) (add_nat_0R x0 (λx1 x2 : setexactly1of2 (odd_nat 0) (odd_nat x2)) (exactly1of2_I2 (odd_nat 0) (odd_nat x0) not_odd_nat_0 H0)) (λx1 : set(λH3 : nat_p x1(λH4 : exactly1of2 (odd_nat x1) (odd_nat (add_nat x0 x1))(add_nat_SR x0 x1 H3 (λx2 x3 : setexactly1of2 (odd_nat (ordsucc x1)) (odd_nat x3)) (exactly1of2_E (odd_nat x1) (odd_nat (add_nat x0 x1)) H4 (exactly1of2 (odd_nat (ordsucc x1)) (odd_nat (ordsucc (add_nat x0 x1)))) (λH5 : odd_nat x1(λH6 : not (odd_nat (add_nat x0 x1))(exactly1of2_I2 (odd_nat (ordsucc x1)) (odd_nat (ordsucc (add_nat x0 x1))) (even_nat_not_odd_nat (ordsucc x1) (odd_nat_even_nat_S x1 H5)) (even_nat_odd_nat_S (add_nat x0 x1) (even_nat_or_odd_nat (add_nat x0 x1) (add_nat_p x0 (omega_nat_p x0 H1) x1 H3) (even_nat (add_nat x0 x1)) (λH7 : even_nat (add_nat x0 x1)H7) (λH7 : odd_nat (add_nat x0 x1)(FalseE (H6 H7) (even_nat (add_nat x0 x1))))))))) (λH5 : not (odd_nat x1)(λH6 : odd_nat (add_nat x0 x1)(exactly1of2_I1 (odd_nat (ordsucc x1)) (odd_nat (ordsucc (add_nat x0 x1))) (even_nat_odd_nat_S x1 (even_nat_or_odd_nat x1 H3 (even_nat x1) (λH7 : even_nat x1H7) (λH7 : odd_nat x1(FalseE (H5 H7) (even_nat x1))))) (even_nat_not_odd_nat (ordsucc (add_nat x0 x1)) (odd_nat_even_nat_S (add_nat x0 x1) H6)))))))))))))).
Theorem. (odd_nat_iff_odd_mul_nat) The following is provable:
(∀x0, odd_nat x0(∀x1, nat_p x1iff (odd_nat x1) (odd_nat (mul_nat x0 x1))))
Proof:
Let x0 of type set be given.
Assume H0: odd_nat x0.
An exact proof term for the current goal is (H0 (∀x1, nat_p x1iff (odd_nat x1) (odd_nat (mul_nat x0 x1))) (λH1 : x0 ω(λH2 : (∀x1, x1 ωx0 = mul_nat 2 x1(∀x2 : prop, x2))(nat_ind (λx1 : setiff (odd_nat x1) (odd_nat (mul_nat x0 x1))) (mul_nat_0R x0 (λx1 x2 : setiff (odd_nat 0) (odd_nat x2)) (iff_refl (odd_nat 0))) (λx1 : set(λH3 : nat_p x1(λH4 : iff (odd_nat x1) (odd_nat (mul_nat x0 x1))(mul_nat_SR x0 x1 H3 (λx2 x3 : setiff (odd_nat (ordsucc x1)) (odd_nat x3)) (iffI (odd_nat (ordsucc x1)) (odd_nat (add_nat x0 (mul_nat x0 x1))) (λH5 : odd_nat (ordsucc x1)(exactly1of2_E (odd_nat (mul_nat x0 x1)) (odd_nat (add_nat x0 (mul_nat x0 x1))) (odd_nat_xor_odd_sum x0 H0 (mul_nat x0 x1) (mul_nat_p x0 (omega_nat_p x0 H1) x1 H3)) (odd_nat (add_nat x0 (mul_nat x0 x1))) (λH6 : odd_nat (mul_nat x0 x1)(λH7 : not (odd_nat (add_nat x0 (mul_nat x0 x1)))((λH8 : odd_nat x1(FalseE (even_nat_not_odd_nat (ordsucc x1) (odd_nat_even_nat_S x1 H8) H5) (odd_nat (add_nat x0 (mul_nat x0 x1))))) (iffER (odd_nat x1) (odd_nat (mul_nat x0 x1)) H4 H6)))) (λH6 : not (odd_nat (mul_nat x0 x1))(λH7 : odd_nat (add_nat x0 (mul_nat x0 x1))H7)))) (λH5 : odd_nat (add_nat x0 (mul_nat x0 x1))(even_nat_odd_nat_S x1 (exactly1of2_E (odd_nat (mul_nat x0 x1)) (odd_nat (add_nat x0 (mul_nat x0 x1))) (odd_nat_xor_odd_sum x0 H0 (mul_nat x0 x1) (mul_nat_p x0 (omega_nat_p x0 H1) x1 H3)) (even_nat x1) (λH6 : odd_nat (mul_nat x0 x1)(λH7 : not (odd_nat (add_nat x0 (mul_nat x0 x1)))(FalseE (H7 H5) (even_nat x1)))) (λH6 : not (odd_nat (mul_nat x0 x1))(λH7 : odd_nat (add_nat x0 (mul_nat x0 x1))(even_nat_or_odd_nat x1 H3 (even_nat x1) (λH8 : even_nat x1H8) (λH8 : odd_nat x1(FalseE (H6 (iffEL (odd_nat x1) (odd_nat (mul_nat x0 x1)) H4 H8)) (even_nat x1)))))))))))))))))).
Theorem. (odd_nat_mul_nat) The following is provable:
(∀x0 x1, odd_nat x0odd_nat x1odd_nat (mul_nat x0 x1))
Proof:
Let x0 and x1 of type set be given.
Assume H0: odd_nat x0.
Assume H1: odd_nat x1.
An exact proof term for the current goal is (H1 (odd_nat (mul_nat x0 x1)) (λH2 : x1 ω(λH3 : (∀x2, x2 ωx1 = mul_nat 2 x2(∀x3 : prop, x3))(iffEL (odd_nat x1) (odd_nat (mul_nat x0 x1)) (odd_nat_iff_odd_mul_nat x0 H0 x1 (omega_nat_p x1 H2)) H1)))).
Theorem. (add_nat_0_inv) The following is provable:
(∀x0, x0 ω(∀x1, x1 ωadd_nat x0 x1 = 0and (x0 = 0) (x1 = 0)))
Proof:
Let x0 of type set be given.
Assume H0: x0 ω.
Let x1 of type set be given.
Assume H1: x1 ω.
An exact proof term for the current goal is (nat_inv x0 (omega_nat_p x0 H0) (add_nat x0 x1 = 0and (x0 = 0) (x1 = 0)) (λH2 : x0 = 0(nat_inv x1 (omega_nat_p x1 H1) (add_nat x0 x1 = 0and (x0 = 0) (x1 = 0)) (λH3 : x1 = 0(λH4 : add_nat x0 x1 = 0(andI (x0 = 0) (x1 = 0) H2 H3))) (λH3 : (x2, and (nat_p x2) (x1 = ordsucc x2))(H3 (add_nat x0 x1 = 0and (x0 = 0) (x1 = 0)) (λx2 : set(λH4 : (λx3 : setand (nat_p x3) (x1 = ordsucc x3)) x2(H4 (add_nat x0 x1 = 0and (x0 = 0) (x1 = 0)) (λH5 : nat_p x2(λH6 : x1 = ordsucc x2(H6 (λx3 x4 : setadd_nat x0 x4 = 0and (x0 = 0) (x4 = 0)) (add_nat_SR x0 x2 H5 (λx3 x4 : setx4 = 0and (x0 = 0) (ordsucc x2 = 0)) (λH7 : ordsucc (add_nat x0 x2) = 0(FalseE (neq_ordsucc_0 (add_nat x0 x2) H7) (and (x0 = 0) (ordsucc x2 = 0))))))))))))))) (λH2 : (x2, and (nat_p x2) (x0 = ordsucc x2))(H2 (add_nat x0 x1 = 0and (x0 = 0) (x1 = 0)) (λx2 : set(λH3 : (λx3 : setand (nat_p x3) (x0 = ordsucc x3)) x2(H3 (add_nat x0 x1 = 0and (x0 = 0) (x1 = 0)) (λH4 : nat_p x2(λH5 : x0 = ordsucc x2(H5 (λx3 x4 : setadd_nat x4 x1 = 0and (x4 = 0) (x1 = 0)) (add_nat_SL x2 H4 x1 (omega_nat_p x1 H1) (λx3 x4 : setx4 = 0and (ordsucc x2 = 0) (x1 = 0)) (λH6 : ordsucc (add_nat x2 x1) = 0(FalseE (neq_ordsucc_0 (add_nat x2 x1) H6) (and (ordsucc x2 = 0) (x1 = 0)))))))))))))).
Theorem. (mul_nat_0_inv) The following is provable:
(∀x0, x0 ω(∀x1, x1 ωmul_nat x0 x1 = 0or (x0 = 0) (x1 = 0)))
Proof:
Let x0 of type set be given.
Assume H0: x0 ω.
Let x1 of type set be given.
Assume H1: x1 ω.
An exact proof term for the current goal is (nat_inv x1 (omega_nat_p x1 H1) (mul_nat x0 x1 = 0or (x0 = 0) (x1 = 0)) (λH2 : x1 = 0(λH3 : mul_nat x0 x1 = 0(orIR (x0 = 0) (x1 = 0) H2))) (λH2 : (x2, and (nat_p x2) (x1 = ordsucc x2))(H2 (mul_nat x0 x1 = 0or (x0 = 0) (x1 = 0)) (λx2 : set(λH3 : (λx3 : setand (nat_p x3) (x1 = ordsucc x3)) x2(H3 (mul_nat x0 x1 = 0or (x0 = 0) (x1 = 0)) (λH4 : nat_p x2(λH5 : x1 = ordsucc x2(H5 (λx3 x4 : setmul_nat x0 x4 = 0or (x0 = 0) (x4 = 0)) (mul_nat_SR x0 x2 H4 (λx3 x4 : setx4 = 0or (x0 = 0) (ordsucc x2 = 0)) (λH6 : add_nat x0 (mul_nat x0 x2) = 0(add_nat_0_inv x0 H0 (mul_nat x0 x2) (nat_p_omega (mul_nat x0 x2) (mul_nat_p x0 (omega_nat_p x0 H0) x2 H4)) H6 (or (x0 = 0) (ordsucc x2 = 0)) (λH7 : x0 = 0(λH8 : mul_nat x0 x2 = 0(orIL (x0 = 0) (ordsucc x2 = 0) H7))))))))))))))).
Theorem. (form100_1_v1_lem) The following is provable:
(∀x0, nat_p x0(∀x1, nat_p x1mul_nat x0 x0 = mul_nat 2 (mul_nat x1 x1)x1 = 0))
Proof:
An exact proof term for the current goal is (nat_complete_ind (λx0 : set∀x1, nat_p x1mul_nat x0 x0 = mul_nat 2 (mul_nat x1 x1)x1 = 0) (λx0 : set(λH0 : nat_p x0(λH1 : (∀x1, x1 x0(∀x2, nat_p x2mul_nat x1 x1 = mul_nat 2 (mul_nat x2 x2)x2 = 0))(λx1 : set(λH2 : nat_p x1(λH3 : mul_nat x0 x0 = mul_nat 2 (mul_nat x1 x1)((λH4 : nat_p (mul_nat x1 x1)((λH5 : even_nat (mul_nat x0 x0)((λH6 : even_nat x0(H6 (x1 = 0) (λH7 : x0 ω(λH8 : (x2, and (x2 ω) (x0 = mul_nat 2 x2))(H8 (x1 = 0) (λx2 : set(λH9 : (λx3 : setand (x3 ω) (x0 = mul_nat 2 x3)) x2(H9 (x1 = 0) (λH10 : x2 ω(λH11 : x0 = mul_nat 2 x2(dneg (x1 = 0) (λH12 : x1 = 0(∀x3 : prop, x3)((λH13 : nat_p x2((λH14 : nat_p (mul_nat 2 x2)((λH15 : mul_nat x1 x1 = mul_nat 2 (mul_nat x2 x2)((λH16 : x1 x0((λH17 : x2 = 0((λH18 : mul_nat x1 x1 = 0(H12 (mul_nat_0_inv x1 (nat_p_omega x1 H2) x1 (nat_p_omega x1 H2) H18 (x1 = 0) (λH19 : x1 = 0H19) (λH19 : x1 = 0H19)))) (H15 (λx3 x4 : setx4 = 0) (H17 (λx3 x4 : setmul_nat 2 (mul_nat x4 x4) = 0) (mul_nat_0R 0 (λx3 x4 : setmul_nat 2 x4 = 0) (mul_nat_0R 2)))))) (H1 x1 H16 x2 (omega_nat_p x2 H10) H15))) (ordinal_In_Or_Subq x1 x0 (nat_p_ordinal x1 H2) (nat_p_ordinal x0 H0) (x1 x0) (λH16 : x1 x0H16) (λH16 : x0 x1(FalseE (H12 ((λH17 : mul_nat x1 x1 = 0(mul_nat_0_inv x1 (nat_p_omega x1 H2) x1 (nat_p_omega x1 H2) H17 (x1 = 0) (λH18 : x1 = 0H18) (λH18 : x1 = 0H18))) (double_nat_Subq_0 (mul_nat x1 x1) H4 (H3 (λx3 x4 : setx3 mul_nat x1 x1) (square_nat_Subq x0 H0 x1 H2 H16))))) (x1 x0)))))) (double_nat_cancel (mul_nat x1 x1) H4 (mul_nat 2 (mul_nat x2 x2)) (mul_nat_p 2 nat_2 (mul_nat x2 x2) (mul_nat_p x2 H13 x2 H13)) (H3 (λx3 x4 : setx3 = mul_nat 2 (mul_nat 2 (mul_nat x2 x2))) (H11 (λx3 x4 : setmul_nat x4 x4 = mul_nat 2 (mul_nat 2 (mul_nat x2 x2))) (mul_nat_asso (mul_nat 2 x2) H14 2 nat_2 x2 H13 (λx3 x4 : setx3 = mul_nat 2 (mul_nat 2 (mul_nat x2 x2))) (mul_nat_com (mul_nat 2 x2) H14 2 nat_2 (λx3 x4 : setmul_nat x4 x2 = mul_nat 2 (mul_nat 2 (mul_nat x2 x2))) (mul_nat_asso 2 nat_2 (mul_nat 2 x2) H14 x2 H13 (λx3 x4 : setx4 = mul_nat 2 (mul_nat 2 (mul_nat x2 x2))) ((λx3 x4 : set(λH15 : (∀x5 : setprop, x5 x4x5 x3)(λx5 : setsetprop(H15 (λx6 : setx5 x6 x4x5 x4 x6) (λH16 : x5 x4 x4H16))))) (mul_nat 2 (mul_nat (mul_nat 2 x2) x2)) (mul_nat 2 (mul_nat 2 (mul_nat x2 x2))) (λx3 : setprop(λH15 : x3 (mul_nat 2 (mul_nat 2 (mul_nat x2 x2)))((λx4 : setsetprop(mul_nat_asso 2 nat_2 x2 H13 x2 H13 (λx5 x6 : setx4 (mul_nat 2 x5) (mul_nat 2 x6)))) (λx4 : setx3) H15)))))))))))) (H11 (λx3 x4 : setnat_p x3) H0))) (omega_nat_p x2 H10)))))))))))))) (even_nat_or_odd_nat x0 H0 (even_nat x0) (λH6 : even_nat x0H6) (λH6 : odd_nat x0(FalseE (even_nat_not_odd_nat (mul_nat x0 x0) H5 (odd_nat_mul_nat x0 x0 H6 H6)) (even_nat x0)))))) (H3 (λx2 x3 : seteven_nat x3) (even_nat_double (mul_nat x1 x1) H4)))) (mul_nat_p x1 H2 x1 H2))))))))).
Theorem. (form100_1_v1) The following is provable:
(∀x0, x0 setminus ω 1(∀x1, x1 setminus ω 1mul_nat x0 x0 = mul_nat 2 (mul_nat x1 x1)(∀x2 : prop, x2)))
Proof:
Let x0 of type set be given.
Assume H0: x0 setminus ω 1.
Let x1 of type set be given.
Assume H1: x1 setminus ω 1.
An exact proof term for the current goal is (setminusE ω 1 x0 H0 (mul_nat x0 x0 = mul_nat 2 (mul_nat x1 x1)(∀x2 : prop, x2)) (λH2 : x0 ω(λH3 : nIn x0 1(setminusE ω 1 x1 H1 (mul_nat x0 x0 = mul_nat 2 (mul_nat x1 x1)(∀x2 : prop, x2)) (λH4 : x1 ω(λH5 : nIn x1 1(λH6 : mul_nat x0 x0 = mul_nat 2 (mul_nat x1 x1)((λH7 : x1 = 0(H5 (H7 (λx2 x3 : setx3 1) In_0_1))) (form100_1_v1_lem x0 (omega_nat_p x0 H2) x1 (omega_nat_p x1 H4) H6))))))))).
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 353 and no associativity corresponding to applying term div_SNo.
Theorem. (sqrt_2_irrational) The following is provable:
Proof:
Apply setminusI to the current goal.
We will prove sqrt_SNo_nonneg 2 real.
Apply sqrt_SNo_nonneg_real 2 to the current goal.
We will prove 2 real.
Apply SNoS_omega_real to the current goal.
We will prove 2 SNoS_ ω.
Apply omega_SNoS_omega to the current goal.
We will prove 2 ω.
An exact proof term for the current goal is nat_p_omega 2 nat_2.
We will prove 0 2.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNoLt_0_2.
Apply SepE real (λx ⇒ mint, nω {0}, x = m :/: n) (sqrt_SNo_nonneg 2) H1 to the current goal.
Apply H3 to the current goal.
Let m be given.
Assume H.
Apply H to the current goal.
Assume Hm: m int.
Assume H.
Apply H to the current goal.
Let n be given.
Assume H.
Apply H to the current goal.
Assume Hn: n ω {0}.
Assume H4: sqrt_SNo_nonneg 2 = m :/: n.
We prove the intermediate claim LmS: SNo m.
An exact proof term for the current goal is int_SNo m Hm.
We prove the intermediate claim Ln: n ω.
An exact proof term for the current goal is setminusE1 ω {0} n Hn.
We prove the intermediate claim LnS: SNo n.
An exact proof term for the current goal is omega_SNo n Ln.
We prove the intermediate claim LS2: SNo (sqrt_SNo_nonneg 2).
Apply SNo_sqrt_SNo_nonneg to the current goal.
An exact proof term for the current goal is SNo_2.
We will prove 0 2.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNoLt_0_2.
We prove the intermediate claim L1: sqrt_SNo_nonneg 2 * n = m.
rewrite the current goal using H4 (from left to right).
We will prove (m :/: n) * n = m.
Apply mul_div_SNo_invL to the current goal.
We will prove SNo m.
An exact proof term for the current goal is LmS.
We will prove SNo n.
An exact proof term for the current goal is LnS.
We will prove n 0.
Assume Hn0: n = 0.
Apply setminusE2 ω {0} n Hn to the current goal.
We will prove n {0}.
rewrite the current goal using Hn0 (from left to right).
Apply SingI to the current goal.
We prove the intermediate claim L2: 0 sqrt_SNo_nonneg 2.
Apply sqrt_SNo_nonneg_nonneg to the current goal.
An exact proof term for the current goal is SNo_2.
We will prove 0 2.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNoLt_0_2.
We prove the intermediate claim L3: 0 < n.
Apply SNoLeE 0 n SNo_0 LnS (omega_nonneg n Ln) to the current goal.
Assume H5: 0 < n.
An exact proof term for the current goal is H5.
Assume H5: 0 = n.
Apply setminusE2 ω {0} n Hn to the current goal.
We will prove n {0}.
rewrite the current goal using H5 (from right to left).
Apply SingI to the current goal.
We prove the intermediate claim L4: (sqrt_SNo_nonneg 2 * n) * (sqrt_SNo_nonneg 2 * n) = 2 * (n * n).
rewrite the current goal using mul_SNo_com_4_inner_mid (sqrt_SNo_nonneg 2) n (sqrt_SNo_nonneg 2) n LS2 LnS LS2 LnS (from left to right).
We will prove (sqrt_SNo_nonneg 2 * sqrt_SNo_nonneg 2) * (n * n) = 2 * (n * n).
Use f_equal.
Apply sqrt_SNo_nonneg_sqr to the current goal.
We will prove SNo 2.
An exact proof term for the current goal is SNo_2.
We will prove 0 2.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNoLt_0_2.
Apply int_3_cases m Hm to the current goal.
Let k be given.
Assume Hk: k ω.
Assume HmSk: m = - ordsucc k.
Apply SNoLt_irref 0 to the current goal.
We will prove 0 < 0.
Apply SNoLeLt_tra 0 (sqrt_SNo_nonneg 2) 0 SNo_0 LS2 SNo_0 L2 to the current goal.
We will prove sqrt_SNo_nonneg 2 < 0.
rewrite the current goal using H4 (from left to right).
We will prove m :/: n < 0.
We prove the intermediate claim LkS: SNo k.
An exact proof term for the current goal is omega_SNo k Hk.
We prove the intermediate claim LSkS: SNo (ordsucc k).
An exact proof term for the current goal is omega_SNo (ordsucc k) (omega_ordsucc k Hk).
Apply div_SNo_neg_pos m n LmS LnS to the current goal.
We will prove m < 0.
rewrite the current goal using HmSk (from left to right).
We will prove - ordsucc k < 0.
Apply minus_SNo_Lt_contra1 0 (ordsucc k) SNo_0 LSkS to the current goal.
We will prove - 0 < ordsucc k.
rewrite the current goal using minus_SNo_0 (from left to right).
We will prove 0 < ordsucc k.
rewrite the current goal using ordinal_ordsucc_SNo_eq k (nat_p_ordinal k (omega_nat_p k Hk)) (from left to right).
We will prove 0 < 1 + k.
Apply SNoLtLe_tra 0 1 (1 + k) SNo_0 SNo_1 (SNo_add_SNo 1 k SNo_1 LkS) SNoLt_0_1 to the current goal.
We will prove 1 1 + k.
rewrite the current goal using add_SNo_0R 1 SNo_1 (from right to left) at position 1.
We will prove 1 + 0 1 + k.
Apply add_SNo_Le2 1 0 k SNo_1 SNo_0 LkS to the current goal.
We will prove 0 k.
An exact proof term for the current goal is omega_nonneg k Hk.
An exact proof term for the current goal is L3.
Assume Hm0: m = 0.
We prove the intermediate claim L5: sqrt_SNo_nonneg 2 * n = 0.
rewrite the current goal using Hm0 (from right to left) at position 2.
An exact proof term for the current goal is L1.
We prove the intermediate claim L6: 2 * (n * n) = 0.
rewrite the current goal using L4 (from right to left).
rewrite the current goal using L5 (from left to right).
We will prove 0 * 0 = 0.
An exact proof term for the current goal is mul_SNo_zeroR 0 SNo_0.
Apply SNoLt_irref 0 to the current goal.
rewrite the current goal using L6 (from right to left) at position 2.
We will prove 0 < 2 * (n * n).
Apply mul_SNo_pos_pos 2 (n * n) SNo_2 (SNo_mul_SNo n n LnS LnS) SNoLt_0_2 to the current goal.
We will prove 0 < n * n.
An exact proof term for the current goal is mul_SNo_pos_pos n n LnS LnS L3 L3.
Let k be given.
Assume Hk: k ω.
Assume HmSk: m = ordsucc k.
We prove the intermediate claim Lm: m ω.
rewrite the current goal using HmSk (from left to right).
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is Hk.
We prove the intermediate claim Lm1: m ω 1.
Apply setminusI to the current goal.
An exact proof term for the current goal is Lm.
Assume H5: m 1.
Apply neq_ordsucc_0 k to the current goal.
We will prove ordsucc k = 0.
rewrite the current goal using HmSk (from right to left).
An exact proof term for the current goal is cases_1 m H5 (λi ⇒ i = 0) (λq H ⇒ H).
We prove the intermediate claim Ln1: n ω 1.
rewrite the current goal using eq_1_Sing0 (from left to right).
An exact proof term for the current goal is Hn.
Apply form100_1_v1 m Lm1 n Ln1 to the current goal.
We will prove mul_nat m m = mul_nat 2 (mul_nat n n).
rewrite the current goal using mul_nat_mul_SNo m Lm m Lm (from left to right).
rewrite the current goal using mul_nat_mul_SNo 2 (nat_p_omega 2 nat_2) (mul_nat n n) (nat_p_omega (mul_nat n n) (mul_nat_p n (omega_nat_p n Ln) n (omega_nat_p n Ln))) (from left to right).
rewrite the current goal using mul_nat_mul_SNo n Ln n Ln (from left to right).
We will prove m * m = 2 * (n * n).
rewrite the current goal using L1 (from right to left).
An exact proof term for the current goal is L4.