Primitive . The name
Eps_i is a term of type
(set → prop → set .
Axiom. (
Eps_i_ax ) We take the following as an axiom:
∀P : set → prop ∀x : set , P x P (Eps_i P Definition. We define
True to be
∀p : prop , p → p of type
prop .
Definition. We define
False to be
∀p : prop , p of type
prop .
Definition. We define
not to be
λA : prop ⇒ A → False of type
prop → prop .
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 , (A → B → p → p of type
prop → prop → prop .
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 , (A → p → (B → p → p of type
prop → prop → prop .
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 : prop ⇒ and (A → B (B → A of type
prop → prop → prop .
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 : A → A → prop Q x y Q y x of type
A → A → prop .
Definition. We define
neq to be
λx y : A ⇒ ¬ eq x y of type
A → A → prop .
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 : A → B (∀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 : A → prop ∀P : prop , (∀x : A , Q x P ) → P of type
(A → prop → 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 q p = q Primitive . The name
In is a term of type
set → set → prop .
Notation . We use
∈ as an infix operator with priority 500 and no associativity corresponding to applying term
In . Furthermore, we may write
∀ x ∈ A , B to mean
∀ x : set, x ∈ A → B .
Definition. We define
Subq to be
λA B ⇒ ∀ x ∈ A , x ∈ B of type
set → set → prop .
Notation . We use
⊆ as an infix operator with priority 500 and no associativity corresponding to applying term
Subq . Furthermore, we may write
∀ x ⊆ A , B to mean
∀ x : set, x ⊆ A → B .
Axiom. (
set_ext ) We take the following as an axiom:
∀X Y : set , X ⊆ Y Y ⊆ X X = Y Axiom. (
In_ind ) We take the following as an axiom:
∀P : set → prop (∀X : set , (∀ x ∈ X , 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:
Primitive . The name
⋃ is a term of type
set → set .
Axiom. (
UnionEq ) We take the following as an axiom:
Primitive . The name
𝒫 is a term of type
set → set .
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 → (set → set → set .
Notation .
{B | x ∈ A } is notation for
Repl A (λ x . B ).
Axiom. (
ReplEq ) We take the following as an axiom:
∀A : set , ∀F : set → set ∀y : set , y ∈ { F x | x ∈ A } ↔ ∃ x ∈ A , y = F x Definition. We define
TransSet to be
λU : set ⇒ ∀ x ∈ U , x ⊆ U of type
set → prop .
Definition. We define
Union_closed to be
λU : set ⇒ ∀X : set , X ∈ U ⋃ X ∈ U of type
set → prop .
Definition. We define
Power_closed to be
λU : set ⇒ ∀X : set , X ∈ U 𝒫 X ∈ U of type
set → prop .
Definition. We define
Repl_closed to be
λU : set ⇒ ∀X : set , X ∈ U ∀F : set → set (∀x : set , x ∈ X F x ∈ U ) → { F x | x ∈ X } ∈ U of type
set → prop .
Primitive . The name
UnivOf is a term of type
set → set .
Axiom. (
UnivOf_In ) We take the following as an axiom:
Axiom. (
UnivOf_Min ) We take the following as an axiom:
Axiom. (
FalseE ) We take the following as an axiom:
Axiom. (
TrueI ) We take the following as an axiom:
Axiom. (
andI ) We take the following as an axiom:
∀A B : prop , A → B → A ∧ B Axiom. (
andEL ) We take the following as an axiom:
Axiom. (
andER ) We take the following as an axiom:
Axiom. (
orIL ) We take the following as an axiom:
Axiom. (
orIR ) We take the following as an axiom:
Beginning of Section PropN
Variable P1 P2 P3 : prop
Axiom. (
and3I ) We take the following as an axiom:
P1 → P2 → P3 → P1 ∧ P2 ∧ P3 Axiom. (
and3E ) We take the following as an axiom:
P1 ∧ P2 ∧ P3 (∀p : prop , (P1 → P2 → P3 → p → p ) Axiom. (
or3I1 ) We take the following as an axiom:
Axiom. (
or3I2 ) We take the following as an axiom:
Axiom. (
or3I3 ) We take the following as an axiom:
Axiom. (
or3E ) We take the following as an axiom:
P1 ∨ P2 ∨ P3 (∀p : prop , (P1 → p → (P2 → p → (P3 → p → p ) Variable P4 : prop
Axiom. (
and4I ) We take the following as an axiom:
P1 → P2 → P3 → P4 → P1 ∧ P2 ∧ P3 ∧ P4 Variable P5 : prop
Axiom. (
and5I ) We take the following as an axiom:
P1 → P2 → P3 → P4 → P5 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 End of Section PropN
Axiom. (
iffI ) We take the following as an axiom:
∀A B : prop , (A → B → (B → A → (A ↔ B Axiom. (
iffEL ) We take the following as an axiom:
∀A B : prop , (A ↔ B → A → B Axiom. (
iffER ) We take the following as an axiom:
∀A B : prop , (A ↔ B → B → A Axiom. (
iff_refl ) We take the following as an axiom:
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 = y y = z x = z Axiom. (
f_eq_i ) We take the following as an axiom:
∀f : set → set ∀x y, x = y f x = f y Axiom. (
neq_i_sym ) We take the following as an axiom:
Definition. We define
nIn to be
λx X ⇒ ¬ In x X of type
set → set → prop .
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 : set → prop (∃ x, P x → P (Eps_i P Axiom. (
pred_ext ) We take the following as an axiom:
∀P Q : set → prop (∀x, P x ↔ Q x ) → P = Q Axiom. (
prop_ext_2 ) We take the following as an axiom:
∀p q : prop , (p → q → (q → p → p = q Axiom. (
Subq_ref ) We take the following as an axiom:
Axiom. (
Subq_tra ) We take the following as an axiom:
∀X Y Z : set , X ⊆ Y Y ⊆ Z X ⊆ Z Axiom. (
Subq_contra ) We take the following as an axiom:
∀X Y z : set , X ⊆ Y z ∉ Y z ∉ X Axiom. (
EmptyE ) We take the following as an axiom:
Axiom. (
Subq_Empty ) We take the following as an axiom:
Axiom. (
Empty_eq ) We take the following as an axiom:
Axiom. (
UnionI ) We take the following as an axiom:
∀X x Y : set , x ∈ Y Y ∈ X x ∈ ⋃ X Axiom. (
UnionE ) We take the following as an axiom:
∀X x : set , x ∈ ⋃ X ∃ Y : 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 ∈ Y Y ∈ X p ) → p Axiom. (
PowerI ) We take the following as an axiom:
∀X Y : set , Y ⊆ X Y ∈ 𝒫 X Axiom. (
PowerE ) We take the following as an axiom:
∀X Y : set , Y ∈ 𝒫 X Y ⊆ X Axiom. (
xm ) We take the following as an axiom:
Axiom. (
dneg ) We take the following as an axiom:
Axiom. (
eq_or_nand ) We take the following as an axiom:
Primitive . The name
exactly1of2 is a term of type
prop → prop → prop .
Axiom. (
exactly1of2_E ) We take the following as an axiom:
∀A B : prop , exactly1of2 A B ∀p : prop , (A → ¬ B p → (¬ A B → p → p Axiom. (
ReplI ) We take the following as an axiom:
∀A : set , ∀F : set → set ∀x : set , x ∈ A F x ∈ { F x | x ∈ A } Axiom. (
ReplE ) We take the following as an axiom:
∀A : set , ∀F : set → set ∀y : set , y ∈ { F x | x ∈ A } ∃ x ∈ A , y = F x Axiom. (
ReplE_impred ) We take the following as an axiom:
∀A : set , ∀F : set → set ∀y : set , y ∈ { F x | x ∈ A } ∀p : prop , (∀x : set , x ∈ A y = F x p ) → p Axiom. (
ReplE' ) We take the following as an axiom:
∀X, ∀f : set → set ∀p : set → prop (∀ x ∈ X , p (f x → ∀ y ∈ { f x | x ∈ X } , p y Axiom. (
Repl_Empty ) We take the following as an axiom:
Axiom. (
ReplEq_ext ) We take the following as an axiom:
∀X, ∀F G : set → set (∀ x ∈ X , F x = G x → { F x | x ∈ X } = { G x | x ∈ X } Axiom. (
Repl_inv_eq ) We take the following as an axiom:
∀P : set → prop ∀f g : set → set (∀x, P x g (f x = x ) → ∀X, (∀ x ∈ X , P x → { g y | y ∈ { f x | x ∈ X } } = X Axiom. (
Repl_invol_eq ) We take the following as an axiom:
∀P : set → prop ∀f : set → set (∀x, P x f (f x = x ) → ∀X, (∀ x ∈ X , P x → { f y | y ∈ { f x | x ∈ X } } = X Primitive . The name
If_i is a term of type
prop → set → set → set .
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_0 ) We take the following as an axiom:
Axiom. (
If_i_1 ) We take the following as an axiom:
Axiom. (
If_i_or ) We take the following as an axiom:
Primitive . The name
UPair is a term of type
set → set → set .
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:
Axiom. (
UPairI2 ) We take the following as an axiom:
Primitive . The name
Sing is a term of type
set → set .
Notation .
{x } is notation for
Sing x .
Axiom. (
SingI ) We take the following as an axiom:
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
set → set → set .
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 ∈ X z ∈ X ∪ Y Axiom. (
binunionI2 ) We take the following as an axiom:
∀X Y z : set , z ∈ Y z ∈ X ∪ Y Axiom. (
binunionE ) We take the following as an axiom:
∀X Y z : set , z ∈ X ∪ Y z ∈ X ∨ z ∈ Y Axiom. (
binunionE' ) We take the following as an axiom:
∀X Y z, ∀p : prop , (z ∈ X p → (z ∈ Y p → (z ∈ X ∪ Y p Axiom. (
binunion_asso ) We take the following as an axiom:
∀X Y Z : set , X ∪ (Y ∪ Z = (X ∪ Y ∪ Z Axiom. (
binunion_com ) We take the following as an axiom:
∀X Y : set , X ∪ Y = Y ∪ X Definition. We define
SetAdjoin to be
λX y ⇒ X ∪ { y } of type
set → set → set .
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 → (set → set → 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 : (set → set , ∀x y : set , x ∈ X y ∈ F x y ∈ ⋃ x ∈ X F x Axiom. (
famunionE ) We take the following as an axiom:
∀X : set , ∀F : (set → set , ∀y : set , y ∈ (⋃ x ∈ X F x ∃ x ∈ X , y ∈ F x Axiom. (
famunionE_impred ) We take the following as an axiom:
∀X : set , ∀F : (set → set , ∀y : set , y ∈ (⋃ x ∈ X F x ∀p : prop , (∀x, x ∈ X y ∈ F x p ) → p
Beginning of Section SepSec
Variable X : set
Variable P : set → prop
Let z : set ≝ Eps_i (λz ⇒ z ∈ X ∧ P z ) Primitive . The name
Sep is a term of type
set .
End of Section SepSec
Notation .
{x ∈ A | B } is notation for
Sep A (λ x . B ).
Axiom. (
SepI ) We take the following as an axiom:
∀X : set , ∀P : (set → prop , ∀x : set , x ∈ X P x x ∈ { x ∈ X | P x } Axiom. (
SepE ) We take the following as an axiom:
∀X : set , ∀P : (set → prop , ∀x : set , x ∈ { x ∈ X | P x } x ∈ X ∧ P x Axiom. (
SepE1 ) We take the following as an axiom:
∀X : set , ∀P : (set → prop , ∀x : set , x ∈ { x ∈ X | P x } x ∈ X Axiom. (
SepE2 ) We take the following as an axiom:
∀X : set , ∀P : (set → prop , ∀x : set , x ∈ { x ∈ X | P x } P x Axiom. (
Sep_Empty ) We take the following as an axiom:
Axiom. (
Sep_Subq ) We take the following as an axiom:
∀X : set , ∀P : set → prop { x ∈ X | P x } ⊆ X Axiom. (
Sep_In_Power ) We take the following as an axiom:
∀X : set , ∀P : set → prop { x ∈ X | P x } ∈ 𝒫 X Primitive . The name
ReplSep is a term of type
set → (set → prop → (set → set → set .
Notation .
{B | x ∈ A , C } is notation for
ReplSep A (λ x . C ) (λ x . B ).
Axiom. (
ReplSepI ) We take the following as an axiom:
∀X : set , ∀P : set → prop ∀F : set → set ∀x : set , x ∈ X P x F x ∈ { F x | x ∈ X , P x } Axiom. (
ReplSepE ) We take the following as an axiom:
∀X : set , ∀P : set → prop ∀F : set → set ∀y : set , y ∈ { F x | x ∈ X , P x } ∃ x : set , x ∈ X ∧ P x ∧ y = F x Axiom. (
ReplSepE_impred ) We take the following as an axiom:
∀X : set , ∀P : set → prop ∀F : set → set ∀y : set , y ∈ { F x | x ∈ X , P x } ∀p : prop , (∀ x ∈ X , P x y = F x p → p Primitive . The name
binintersect is a term of type
set → set → set .
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 ∈ X z ∈ Y z ∈ X ∩ Y Axiom. (
binintersectE ) We take the following as an axiom:
∀X Y z, z ∈ X ∩ Y z ∈ X ∧ z ∈ Y Primitive . The name
setminus is a term of type
set → set → set .
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. (
In_irref ) We take the following as an axiom:
Axiom. (
In_no2cycle ) We take the following as an axiom:
Primitive . The name
ordsucc is a term of type
set → set .
Axiom. (
ordsuccI1 ) We take the following as an axiom:
Axiom. (
ordsuccI2 ) We take the following as an axiom:
Axiom. (
ordsuccE ) We take the following as an axiom:
Notation . Natural numbers 0,1,2,... are notation for the terms formed using
Empty as 0 and forming successors with
ordsucc .
Axiom. (
ordsucc_inj ) We take the following as an axiom:
Axiom. (
In_0_1 ) We take the following as an axiom:
Axiom. (
In_0_2 ) We take the following as an axiom:
Axiom. (
In_1_2 ) We take the following as an axiom:
Definition. We define
nat_p to be
λn : set ⇒ ∀p : set → prop p 0 (∀x : set , p x p (ordsucc x ) → p n of type
set → prop .
Axiom. (
nat_0 ) We take the following as an axiom:
Axiom. (
nat_ordsucc ) We take the following as an axiom:
Axiom. (
nat_1 ) We take the following as an axiom:
Axiom. (
nat_2 ) We take the following as an axiom:
Axiom. (
nat_ind ) We take the following as an axiom:
Axiom. (
nat_inv ) We take the following as an axiom:
Axiom. (
nat_p_trans ) We take the following as an axiom:
Axiom. (
nat_trans ) We take the following as an axiom:
Axiom. (
cases_1 ) We take the following as an axiom:
∀ i ∈ 1 , ∀p : set → prop p 0 p i Axiom. (
cases_2 ) We take the following as an axiom:
∀ i ∈ 2 , ∀p : set → prop p 0 p 1 p i Axiom. (
cases_3 ) We take the following as an axiom:
∀ i ∈ 3 , ∀p : set → prop p 0 p 1 p 2 p i Axiom. (
neq_0_1 ) We take the following as an axiom:
Axiom. (
neq_1_0 ) We take the following as an axiom:
Axiom. (
neq_0_2 ) We take the following as an axiom:
Axiom. (
neq_2_0 ) We take the following as an axiom:
Axiom. (
neq_1_2 ) We take the following as an axiom:
Axiom. (
ZF_closed_E ) We take the following as an axiom:
Primitive . The name
ω is a term of type
set .
Axiom. (
omega_nat_p ) We take the following as an axiom:
Axiom. (
nat_p_omega ) We take the following as an axiom:
Axiom. (
ordinal_1 ) We take the following as an axiom:
Axiom. (
ordinal_2 ) We take the following as an axiom:
Axiom. (
ordinal_ind ) We take the following as an axiom:
∀p : set → prop (∀alpha, ordinal alpha (∀ beta ∈ alpha , p beta → p alpha ) → ∀alpha, ordinal alpha p alpha Definition. We define
inj to be
λX Y f ⇒ (∀ u ∈ X , f u ∈ Y ∧ (∀ u v ∈ X , f u = f v u = v of type
set → set → (set → set → prop .
Definition. We define
bij to be
λX Y f ⇒ (∀ u ∈ X , f u ∈ Y ∧ (∀ u v ∈ X , f u = f v u = v ∧ (∀ w ∈ Y , ∃ u ∈ X , f u = w of type
set → set → (set → set → prop .
Axiom. (
bijI ) We take the following as an axiom:
∀X Y, ∀f : set → set (∀ u ∈ X , f u ∈ Y → (∀ u v ∈ X , f u = f v u = v → (∀ w ∈ Y , ∃ u ∈ X , f u = w → bij X Y f Axiom. (
bijE ) We take the following as an axiom:
∀X Y, ∀f : set → set bij X Y f ∀p : prop , ((∀ u ∈ X , f u ∈ Y → (∀ u v ∈ X , f u = f v u = v → (∀ w ∈ Y , ∃ u ∈ X , f u = w → p → p Primitive . The name
inv is a term of type
set → (set → set → set → set .
Axiom. (
surj_rinv ) We take the following as an axiom:
Axiom. (
inj_linv ) We take the following as an axiom:
∀X, ∀f : set → set (∀ u v ∈ X , f u = f v u = v → ∀ x ∈ X , inv X f (f x = x Axiom. (
bij_inv ) We take the following as an axiom:
∀X Y, ∀f : set → set bij X Y f bij Y X (inv X f Axiom. (
bij_id ) We take the following as an axiom:
Axiom. (
bij_comp ) We take the following as an axiom:
∀X Y Z : set , ∀f g : set → set bij X Y f bij Y Z g bij X Z (λx ⇒ g (f x ) Definition. We define
equip to be
λX Y : set ⇒ ∃ f : set → set , bij X Y f of type
set → set → prop .
Axiom. (
equip_ref ) We take the following as an axiom:
Axiom. (
equip_sym ) We take the following as an axiom:
Axiom. (
equip_tra ) We take the following as an axiom:
Beginning of Section SchroederBernstein
End of Section SchroederBernstein
Beginning of Section PigeonHole
End of Section PigeonHole
Definition. We define
finite to be
λX ⇒ ∃ n ∈ ω , equip X n of type
set → prop .
Axiom. (
finite_ind ) We take the following as an axiom:
Axiom. (
Subq_finite ) We take the following as an axiom:
Axiom. (
exandE_i ) We take the following as an axiom:
∀P Q : set → prop (∃ x, P x ∧ Q x → ∀r : prop , (∀x, P x Q x r ) → r Axiom. (
exandE_ii ) We take the following as an axiom:
∀P Q : (set → set → prop (∃ x : set → set , P x ∧ Q x → ∀p : prop , (∀x : set → set P x Q x p ) → p Axiom. (
exandE_iii ) We take the following as an axiom:
∀P Q : (set → set → set → prop (∃ x : set → set → set , P x ∧ Q x → ∀p : prop , (∀x : set → set → set P x Q x p ) → p Axiom. (
exandE_iiii ) We take the following as an axiom:
∀P Q : (set → set → set → set → prop (∃ x : set → set → set → set , P x ∧ Q x → ∀p : prop , (∀x : set → set → set → set P x Q x p ) → p
Beginning of Section Descr_ii
Variable P : (set → set → prop
Primitive . The name
Descr_ii is a term of type
set → set .
Hypothesis Pex : ∃ f : set → set , P f Hypothesis Puniq : ∀f g : set → set P f P g f = g End of Section Descr_ii
Beginning of Section Descr_iii
Variable P : (set → set → set → prop
Primitive . The name
Descr_iii is a term of type
set → set → set .
Hypothesis Pex : ∃ f : set → set → set , P f Hypothesis Puniq : ∀f g : set → set → set P f P g f = g End of Section Descr_iii
Beginning of Section Descr_Vo1
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 f P g f = g End of Section Descr_Vo1
Beginning of Section If_ii
Variable p : prop
Variable f g : set → set
Primitive . The name
If_ii is a term of type
set → set .
Axiom. (
If_ii_1 ) We take the following as an axiom:
Axiom. (
If_ii_0 ) We take the following as an axiom:
End of Section If_ii
Beginning of Section If_iii
Variable p : prop
Variable f g : set → set → set
Primitive . The name
If_iii is a term of type
set → set → set .
Axiom. (
If_iii_1 ) We take the following as an axiom:
Axiom. (
If_iii_0 ) We take the following as an axiom:
End of Section If_iii
Beginning of Section EpsilonRec_i
Variable F : set → (set → set → set
Primitive . The name
In_rec_i is a term of type
set → set .
Hypothesis Fr : ∀X : set , ∀g h : set → set (∀ x ∈ X , g x = h x → F X g = F X h Axiom. (
In_rec_i_eq ) We take the following as an axiom:
End of Section EpsilonRec_i
Beginning of Section EpsilonRec_ii
Variable F : set → (set → (set → set → (set → set
Primitive . The name
In_rec_ii is a term of type
set → (set → set .
Hypothesis Fr : ∀X : set , ∀g h : set → (set → set (∀ x ∈ X , g x = h x → F X g = F X h End of Section EpsilonRec_ii
Beginning of Section EpsilonRec_iii
Variable F : set → (set → (set → set → set → (set → set → set
Primitive . The name
In_rec_iii is a term of type
set → (set → set → set .
Hypothesis Fr : ∀X : set , ∀g h : set → (set → set → set (∀ x ∈ X , g x = h x → F X g = F X h End of Section EpsilonRec_iii
Beginning of Section NatRec
Variable z : set
Variable f : set → set → set
Let F : set → (set → set → set λn g ⇒ if ⋃ n ∈ n then f (⋃ n (g (⋃ n else z Axiom. (
nat_primrec_r ) We take the following as an axiom:
∀X : set , ∀g h : set → set (∀ x ∈ X , g x = h x → F X g = F X h End of Section NatRec
Beginning of Section NatArith
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:
Axiom. (
add_nat_SR ) We take the following as an axiom:
Axiom. (
add_nat_p ) We take the following as an axiom:
Axiom. (
add_nat_com ) We take the following as an axiom:
Definition. We define
mul_nat to be
λn m : set ⇒ nat_primrec 0 (λ_ r ⇒ n + r ) m of type
set → set → set .
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:
Axiom. (
mul_nat_SR ) We take the following as an axiom:
Axiom. (
mul_nat_p ) We take the following as an axiom:
End of Section NatArith
Axiom. (
Inj1_eq ) We take the following as an axiom:
Axiom. (
Inj1I1 ) We take the following as an axiom:
Axiom. (
Inj1I2 ) We take the following as an axiom:
Axiom. (
Inj1E ) We take the following as an axiom:
Axiom. (
Inj1NE1 ) We take the following as an axiom:
Axiom. (
Inj1NE2 ) We take the following as an axiom:
Definition. We define
Inj0 to be
λX ⇒ { Inj1 x | x ∈ X } of type
set → set .
Axiom. (
Inj0I ) We take the following as an axiom:
Axiom. (
Inj0E ) We take the following as an axiom:
Axiom. (
Unj_eq ) We take the following as an axiom:
Axiom. (
Unj_Inj1_eq ) We take the following as an axiom:
Axiom. (
Inj1_inj ) We take the following as an axiom:
Axiom. (
Unj_Inj0_eq ) We take the following as an axiom:
Axiom. (
Inj0_inj ) We take the following as an axiom:
Axiom. (
Inj0_0 ) We take the following as an axiom:
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 ∈ X Inj0 x ∈ X + Y Axiom. (
Inj1_setsum ) We take the following as an axiom:
∀X Y y : set , y ∈ Y Inj1 y ∈ X + Y Axiom. (
setsum_0_0 ) We take the following as an axiom:
Beginning of Section pair_setsum
Axiom. (
pairI0 ) We take the following as an axiom:
∀X Y x, x ∈ X pair 0 x ∈ pair X Y Axiom. (
pairI1 ) We take the following as an axiom:
∀X Y y, y ∈ Y pair 1 y ∈ pair X Y Axiom. (
pairE ) We take the following as an axiom:
∀X Y z, z ∈ pair X Y (∃ x ∈ X , z = pair 0 x ∨ (∃ y ∈ Y , z = pair 1 y Axiom. (
pairE0 ) We take the following as an axiom:
∀X Y x, pair 0 x ∈ pair X Y x ∈ X Axiom. (
pairE1 ) We take the following as an axiom:
∀X Y y, pair 1 y ∈ pair X Y y ∈ Y Axiom. (
proj0I ) We take the following as an axiom:
Axiom. (
proj0E ) We take the following as an axiom:
Axiom. (
proj1I ) We take the following as an axiom:
Axiom. (
proj1E ) We take the following as an axiom:
Definition. We define
Sigma to be
λX Y ⇒ ⋃ x ∈ X { pair x y | y ∈ Y x } of type
set → (set → set → 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 : set → set ∀ x ∈ X , ∀ y ∈ Y x , pair x y ∈ ∑ x ∈ X , Y x Axiom. (
proj0_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀z : set , z ∈ (∑ x ∈ X , Y x proj0 z ∈ X Axiom. (
proj1_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀z : set , z ∈ (∑ x ∈ X , Y x proj1 z ∈ Y (proj0 z Axiom. (
pair_Sigma_E1 ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀x y : set , pair x y ∈ (∑ x ∈ X , Y x y ∈ Y x Axiom. (
Sigma_E ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀z : set , z ∈ (∑ x ∈ X , Y x ∃ x ∈ X , ∃ y ∈ Y x , z = pair x y Definition. We define
setprod to be
λX Y : set ⇒ ∑ x ∈ X , Y of type
set → set → set .
Notation . We use
⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term
setprod .
Let lam : set → (set → set → set Sigma Definition. We define
ap to be
λf x ⇒ { proj1 z | z ∈ f , ∃ y : set , z = pair x y } of type
set → set → set .
Notation . When
x is a set, a term
x y is notation for
ap x y .
Notation .
λ x ∈ A ⇒ B is notation for the set
Sigma A (λ x : 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 : set → set ∀ x ∈ X , ∀ y ∈ F x , pair x y ∈ λ x ∈ X ⇒ F x Axiom. (
lamE ) We take the following as an axiom:
∀X : set , ∀F : set → set ∀z : set , z ∈ (λ x ∈ X ⇒ F x ∃ x ∈ X , ∃ y ∈ F x , z = pair x y Axiom. (
apI ) We take the following as an axiom:
∀f x y, pair x y ∈ f y ∈ f x Axiom. (
apE ) We take the following as an axiom:
∀f x y, y ∈ f x pair x y ∈ f Axiom. (
beta ) We take the following as an axiom:
∀X : set , ∀F : set → set ∀x : set , x ∈ X (λ x ∈ X ⇒ F x x = F x Axiom. (
proj0_ap_0 ) We take the following as an axiom:
Axiom. (
proj1_ap_1 ) We take the following as an axiom:
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 : set → set ∀z : set , z ∈ (∑ x ∈ X , Y x (z 0 ∈ X Axiom. (
ap1_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀z : set , z ∈ (∑ x ∈ X , Y x (z 1 ∈ (Y (z 0 Definition. We define
pair_p to be
λu : set ⇒ pair (u 0 (u 1 = u of type
set → prop .
Axiom. (
pair_p_I ) 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 ∈ 𝒫 (∑ x ∈ X , ⋃ (Y x | ∀ x ∈ X , f x ∈ Y x } of type
set → (set → set → 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 : set → set ∀f : set , (∀ u ∈ f , pair_p u ∧ u 0 ∈ X → (∀ x ∈ X , f x ∈ Y x → f ∈ ∏ x ∈ X , Y x Axiom. (
lam_Pi ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀F : set → set (∀ x ∈ X , F x ∈ Y x → (λ x ∈ X ⇒ F x ∈ (∏ x ∈ X , Y x Axiom. (
ap_Pi ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀f : set , ∀x : set , f ∈ (∏ x ∈ X , Y x x ∈ X f x ∈ Y x Definition. We define
setexp to be
λX Y : set ⇒ ∏ y ∈ Y , X of type
set → set → set .
Notation . We use
:^: as an infix operator with priority 430 and which associates to the left corresponding to applying term
setexp .
Axiom. (
lamI2 ) We take the following as an axiom:
Beginning of Section Tuples
Variable x0 x1 : set
End of Section Tuples
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 → (set → prop → prop → set .
Primitive . The name
DescrR_i_io_2 is a term of type
(set → (set → prop → prop → set → prop .
Definition. We define
PNoEq_ to be
λalpha p q ⇒ ∀ beta ∈ alpha , p beta ↔ q beta of type
set → (set → prop → (set → prop → prop .
Axiom. (
PNoEq_ref_ ) We take the following as an axiom:
∀alpha, ∀p : set → prop PNoEq_ alpha p p Axiom. (
PNoEq_sym_ ) We take the following as an axiom:
∀alpha, ∀p q : set → prop PNoEq_ alpha p q PNoEq_ alpha q p Axiom. (
PNoEq_tra_ ) We take the following as an axiom:
Axiom. (
PNoLt_E_ ) We take the following as an axiom:
Axiom. (
PNoLt_irref_ ) We take the following as an axiom:
∀alpha, ∀p : set → prop ¬ PNoLt_ alpha p p Axiom. (
PNoLt_mon_ ) We take the following as an axiom:
Axiom. (
PNoLt_tra_ ) We take the following as an axiom:
Primitive . The name
PNoLt is a term of type
set → (set → prop → set → (set → prop → prop .
Axiom. (
PNoLtI1 ) We take the following as an axiom:
Axiom. (
PNoLtI2 ) We take the following as an axiom:
Axiom. (
PNoLtI3 ) We take the following as an axiom:
Axiom. (
PNoLtE ) We take the following as an axiom:
Axiom. (
PNoLt_irref ) We take the following as an axiom:
∀alpha, ∀p : set → prop ¬ PNoLt alpha p alpha p Axiom. (
PNoLtEq_tra ) We take the following as an axiom:
Axiom. (
PNoEqLt_tra ) We take the following as an axiom:
Axiom. (
PNoLt_tra ) We take the following as an axiom:
Definition. We define
PNoLe to be
λalpha p beta q ⇒ PNoLt alpha p beta q ∨ alpha = beta ∧ PNoEq_ alpha p q of type
set → (set → prop → set → (set → prop → prop .
Axiom. (
PNoLeI1 ) We take the following as an axiom:
Axiom. (
PNoLeI2 ) We take the following as an axiom:
∀alpha, ∀p q : set → prop PNoEq_ alpha p q PNoLe alpha p alpha q Axiom. (
PNoLe_ref ) We take the following as an axiom:
∀alpha, ∀p : set → prop PNoLe alpha p alpha p Axiom. (
PNoLtLe_tra ) We take the following as an axiom:
Axiom. (
PNoLeLt_tra ) We take the following as an axiom:
Axiom. (
PNoEqLe_tra ) We take the following as an axiom:
Axiom. (
PNoLe_tra ) We take the following as an axiom:
Axiom. (
PNoLe_downc ) We take the following as an axiom:
Axiom. (
PNo_downc_ref ) We take the following as an axiom:
∀L : set → (set → prop → prop ∀alpha, ordinal alpha ∀p : set → prop L alpha p PNo_downc L alpha p Axiom. (
PNo_upc_ref ) We take the following as an axiom:
∀R : set → (set → prop → prop ∀alpha, ordinal alpha ∀p : set → prop R alpha p PNo_upc R alpha p Axiom. (
PNoLe_upc ) We take the following as an axiom:
Definition. We define
PNoLt_pwise to be
λL R ⇒ ∀gamma, ordinal gamma ∀p : set → prop L gamma p ∀delta, ordinal delta ∀q : set → prop R delta q PNoLt gamma p delta q of type
(set → (set → prop → prop → (set → (set → prop → prop → prop .
Axiom. (
PNo_extend0_eq ) We take the following as an axiom:
∀alpha, ∀p : set → prop PNoEq_ alpha p (λdelta ⇒ p delta ∧ delta ≠ alpha ) Axiom. (
PNo_extend1_eq ) We take the following as an axiom:
∀alpha, ∀p : set → prop PNoEq_ alpha p (λdelta ⇒ p delta ∨ delta = alpha ) Definition. We define
PNo_lenbdd to be
λalpha L ⇒ ∀beta, ∀p : set → prop L beta p beta ∈ alpha of type
set → (set → (set → prop → prop → 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 → (set → prop → prop → (set → (set → prop → prop → set → (set → prop → prop .
Primitive . The name
PNo_bd is a term of type
(set → (set → prop → prop → (set → (set → prop → prop → set .
Primitive . The name
PNo_pred is a term of type
(set → (set → prop → prop → (set → (set → prop → prop → set → prop .
Axiom. (
PNo_bd_pred ) We take the following as an axiom:
Axiom. (
PNo_bd_In ) We take the following as an axiom:
Beginning of Section TaggedSets
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
tag .
Definition. We define
SNoElts_ to be
λalpha ⇒ alpha ∪ { beta ' | beta ∈ alpha } of type
set → set .
Axiom. (
SNoElts_mon ) We take the following as an axiom:
Axiom. (
PNoEq_PSNo ) We take the following as an axiom:
Axiom. (
SNo_PSNo ) We take the following as an axiom:
Primitive . The name
SNo is a term of type
set → prop .
Axiom. (
SNo_SNo ) We take the following as an axiom:
Primitive . The name
SNoLev is a term of type
set → set .
Axiom. (
SNoLev_uniq ) We take the following as an axiom:
Axiom. (
SNoLev_prop ) We take the following as an axiom:
Axiom. (
SNoLev_ ) We take the following as an axiom:
Axiom. (
SNoLev_PSNo ) We take the following as an axiom:
Axiom. (
SNo_Subq ) We take the following as an axiom:
Definition. We define
SNoEq_ to be
λalpha x y ⇒ PNoEq_ alpha (λbeta ⇒ beta ∈ x ) (λbeta ⇒ beta ∈ y ) of type
set → set → set → prop .
Axiom. (
SNoEq_I ) We take the following as an axiom:
Axiom. (
SNo_eq ) We take the following as an axiom:
End of Section TaggedSets
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 .
Axiom. (
SNoLtLe ) We take the following as an axiom:
Axiom. (
SNoLeE ) We take the following as an axiom:
Axiom. (
SNoEq_sym_ ) We take the following as an axiom:
Axiom. (
SNoEq_tra_ ) We take the following as an axiom:
Axiom. (
SNoLtE ) We take the following as an axiom:
Axiom. (
SNoLtI2 ) We take the following as an axiom:
Axiom. (
SNoLtI3 ) We take the following as an axiom:
Axiom. (
SNoLt_irref ) We take the following as an axiom:
Axiom. (
SNoLt_tra ) We take the following as an axiom:
Axiom. (
SNoLe_ref ) We take the following as an axiom:
Axiom. (
SNoLtLe_tra ) We take the following as an axiom:
Axiom. (
SNoLeLt_tra ) We take the following as an axiom:
Axiom. (
SNoLe_tra ) We take the following as an axiom:
Axiom. (
SNoLtLe_or ) We take the following as an axiom:
Axiom. (
SNoCutP_L_0 ) We take the following as an axiom:
Axiom. (
SNoCutP_0_R ) We take the following as an axiom:
Axiom. (
SNoCutP_0_0 ) We take the following as an axiom:
Axiom. (
SNoS_E ) We take the following as an axiom:
Beginning of Section TaggedSets2
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:
Axiom. (
SNoS_I2 ) We take the following as an axiom:
Axiom. (
SNoS_Subq ) We take the following as an axiom:
Axiom. (
SNoS_E2 ) We take the following as an axiom:
Axiom. (
SNoS_In_neq ) We take the following as an axiom:
Axiom. (
SNoS_SNoLev ) We take the following as an axiom:
Axiom. (
SNoL_E ) We take the following as an axiom:
Axiom. (
SNoR_E ) We take the following as an axiom:
Axiom. (
SNoL_SNoS_ ) We take the following as an axiom:
Axiom. (
SNoR_SNoS_ ) We take the following as an axiom:
Axiom. (
SNoL_SNoS ) We take the following as an axiom:
Axiom. (
SNoR_SNoS ) We take the following as an axiom:
Axiom. (
SNoL_I ) We take the following as an axiom:
Axiom. (
SNoR_I ) We take the following as an axiom:
Axiom. (
SNo_eta ) We take the following as an axiom:
Axiom. (
SNoCut_Le ) We take the following as an axiom:
Axiom. (
SNoCut_ext ) We take the following as an axiom:
Axiom. (
ordinal_SNo ) We take the following as an axiom:
Axiom. (
nat_p_SNo ) We take the following as an axiom:
Axiom. (
omega_SNo ) 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. (
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_pos ) We take the following as an axiom:
Axiom. (
eps_SNo_eq ) We take the following as an axiom:
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:
Axiom. (
SNo_ind ) We take the following as an axiom:
Beginning of Section SurrealRecI
Variable F : set → (set → set → set
Primitive . The name
SNo_rec_i is a term of type
set → set .
Hypothesis Fr : ∀z, SNo z ∀g h : set → set (∀ w ∈ SNoS_ (SNoLev z , g w = h w → F z g = F z h End of Section SurrealRecI
Beginning of Section SurrealRecII
Variable F : set → (set → (set → set → (set → set
Let G : set → (set → set → (set → set → set → (set → set λalpha g ⇒ If_iii (ordinal alpha (λz : set ⇒ If_ii (z ∈ SNoS_ (ordsucc alpha (F z (λw ⇒ g (SNoLev w w ) default ) (λz : set ⇒ default ) Primitive . The name
SNo_rec_ii is a term of type
set → (set → set .
Hypothesis Fr : ∀z, SNo z ∀g h : set → (set → set (∀ w ∈ SNoS_ (SNoLev z , g w = h w → F z g = F z h End of Section SurrealRecII
Beginning of Section SurrealRec2
Variable F : set → set → (set → set → set → set
Let G : set → (set → set → set → set → (set → set → set λw f z g ⇒ F w z (λx y ⇒ if x = w then g y else f x y ) Primitive . The name
SNo_rec2 is a term of type
set → set → set .
Axiom. (
SNo_rec2_eq ) We take the following as an axiom:
End of Section SurrealRec2
Axiom. (
SNoLev_ind ) We take the following as an axiom:
Axiom. (
SNoLev_ind2 ) We take the following as an axiom:
Axiom. (
SNoLev_ind3 ) We take the following as an axiom:
∀P : set → set → set → prop (∀x y z, SNo x SNo y SNo z (∀ u ∈ SNoS_ (SNoLev x , P u y z → (∀ v ∈ SNoS_ (SNoLev y , P x v z → (∀ w ∈ SNoS_ (SNoLev z , P x y w → (∀ u ∈ SNoS_ (SNoLev x , ∀ v ∈ SNoS_ (SNoLev y , P u v z → (∀ u ∈ SNoS_ (SNoLev x , ∀ w ∈ SNoS_ (SNoLev z , P u y w → (∀ v ∈ SNoS_ (SNoLev y , ∀ w ∈ SNoS_ (SNoLev z , P x v w → (∀ u ∈ SNoS_ (SNoLev x , ∀ v ∈ SNoS_ (SNoLev y , ∀ w ∈ SNoS_ (SNoLev z , P u v w → P x y z ) → ∀x y z, SNo x SNo y SNo z P x y z Axiom. (
SNo_omega ) We take the following as an axiom:
Axiom. (
SNoLt_0_1 ) We take the following as an axiom:
Axiom. (
SNoLt_0_2 ) We take the following as an axiom:
Axiom. (
SNoLt_1_2 ) We take the following as an axiom:
Axiom. (
restr_SNo_ ) We take the following as an axiom:
Axiom. (
restr_SNo ) We take the following as an axiom:
Axiom. (
restr_SNoEq ) We take the following as an axiom:
Beginning of Section SurrealMinus
Primitive . The name
minus_SNo is a term of type
set → set .
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 .
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
set → set → set .
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:
Axiom. (
SNo_add_SNo ) We take the following as an axiom:
Axiom. (
add_SNo_Lt1 ) We take the following as an axiom:
Axiom. (
add_SNo_Le1 ) We take the following as an axiom:
Axiom. (
add_SNo_Lt2 ) We take the following as an axiom:
Axiom. (
add_SNo_Le2 ) We take the following as an axiom:
Axiom. (
add_SNo_Lt3 ) We take the following as an axiom:
Axiom. (
add_SNo_Le3 ) We take the following as an axiom:
Axiom. (
add_SNo_com ) We take the following as an axiom:
Axiom. (
add_SNo_0L ) We take the following as an axiom:
Axiom. (
add_SNo_0R ) We take the following as an axiom:
Axiom. (
minus_SNo_0 ) We take the following as an axiom:
Axiom. (
add_SNo_Lt4 ) We take the following as an axiom:
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 .
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:
Axiom. (
mul_SNo_eq_2 ) We take the following as an axiom:
∀x y, SNo x SNo y ∀p : prop , (∀L R, (∀u, u ∈ L (∀q : prop , (∀ w0 ∈ SNoL x , ∀ w1 ∈ SNoL y , u = w0 * y + x * w1 + - w0 * w1 q → (∀ z0 ∈ SNoR x , ∀ z1 ∈ SNoR y , u = z0 * y + x * z1 + - z0 * z1 q → q ) ) → (∀ w0 ∈ SNoL x , ∀ w1 ∈ SNoL y , w0 * y + x * w1 + - w0 * w1 ∈ L → (∀ z0 ∈ SNoR x , ∀ z1 ∈ SNoR y , z0 * y + x * z1 + - z0 * z1 ∈ L → (∀u, u ∈ R (∀q : prop , (∀ w0 ∈ SNoL x , ∀ z1 ∈ SNoR y , u = w0 * y + x * z1 + - w0 * z1 q → (∀ z0 ∈ SNoR x , ∀ w1 ∈ SNoL y , u = z0 * y + x * w1 + - z0 * w1 q → q ) ) → (∀ w0 ∈ SNoL x , ∀ z1 ∈ SNoR y , w0 * y + x * z1 + - w0 * z1 ∈ R → (∀ z0 ∈ SNoR x , ∀ w1 ∈ SNoL y , z0 * y + x * w1 + - z0 * w1 ∈ R → x * y = SNoCut L R p ) → p Axiom. (
mul_SNo_prop_1 ) We take the following as an axiom:
∀x, SNo x ∀y, SNo y ∀p : prop , (SNo (x * y (∀ u ∈ SNoL x , ∀ v ∈ SNoL y , u * y + x * v < x * y + u * v → (∀ u ∈ SNoR x , ∀ v ∈ SNoR y , u * y + x * v < x * y + u * v → (∀ u ∈ SNoL x , ∀ v ∈ SNoR y , x * y + u * v < u * y + x * v → (∀ u ∈ SNoR x , ∀ v ∈ SNoL y , x * y + u * v < u * y + x * v → p → p Axiom. (
SNo_mul_SNo ) We take the following as an axiom:
Axiom. (
mul_SNo_eq_3 ) We take the following as an axiom:
∀x y, SNo x SNo y ∀p : prop , (∀L R, SNoCutP L R (∀u, u ∈ L (∀q : prop , (∀ w0 ∈ SNoL x , ∀ w1 ∈ SNoL y , u = w0 * y + x * w1 + - w0 * w1 q → (∀ z0 ∈ SNoR x , ∀ z1 ∈ SNoR y , u = z0 * y + x * z1 + - z0 * z1 q → q ) ) → (∀ w0 ∈ SNoL x , ∀ w1 ∈ SNoL y , w0 * y + x * w1 + - w0 * w1 ∈ L → (∀ z0 ∈ SNoR x , ∀ z1 ∈ SNoR y , z0 * y + x * z1 + - z0 * z1 ∈ L → (∀u, u ∈ R (∀q : prop , (∀ w0 ∈ SNoL x , ∀ z1 ∈ SNoR y , u = w0 * y + x * z1 + - w0 * z1 q → (∀ z0 ∈ SNoR x , ∀ w1 ∈ SNoL y , u = z0 * y + x * w1 + - z0 * w1 q → q ) ) → (∀ w0 ∈ SNoL x , ∀ z1 ∈ SNoR y , w0 * y + x * z1 + - w0 * z1 ∈ R → (∀ z0 ∈ SNoR x , ∀ w1 ∈ SNoL y , z0 * y + x * w1 + - z0 * w1 ∈ R → x * y = SNoCut L R p ) → p Axiom. (
mul_SNo_Lt ) We take the following as an axiom:
Axiom. (
mul_SNo_Le ) We take the following as an axiom:
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 , (∀ w0 ∈ X , ∀ w1 ∈ Y , u = w0 * y + x * w1 + - w0 * w1 q → (∀ z0 ∈ Z , ∀ z1 ∈ W , u = z0 * y + x * z1 + - z0 * z1 q → q ) ) → (∀ w0 ∈ X , ∀ w1 ∈ Y , w0 * y + x * w1 + - w0 * w1 ∈ U' → (∀ w0 ∈ Z , ∀ w1 ∈ W , w0 * y + x * w1 + - w0 * w1 ∈ U' → U ⊆ U' Axiom. (
mul_SNo_com ) We take the following as an axiom:
Beginning of Section mul_SNo_assoc_lems
Variable M : set → set → set
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
M .
Hypothesis SNo_M : ∀x y, SNo x SNo y SNo (x * y Hypothesis DL : ∀x y z, SNo x SNo y SNo z x * (y + z = x * y + x * z Hypothesis DR : ∀x y z, SNo x SNo y SNo z (x + y * z = x * z + y * z Hypothesis M_Lt : ∀x y u v, SNo x SNo y SNo u SNo v u < x v < y u * y + x * v < x * y + u * v Hypothesis M_Le : ∀x y u v, SNo x SNo y SNo u SNo v u ≤ x v ≤ y u * y + x * v ≤ x * y + u * v Axiom. (
mul_SNo_assoc_lem1 ) We take the following as an axiom:
∀x y z, SNo x SNo y SNo z (∀ u ∈ SNoS_ (SNoLev x , u * (y * z = (u * y * z → (∀ v ∈ SNoS_ (SNoLev y , x * (v * z = (x * v * z → (∀ w ∈ SNoS_ (SNoLev z , x * (y * w = (x * y * w → (∀ u ∈ SNoS_ (SNoLev x , ∀ v ∈ SNoS_ (SNoLev y , u * (v * z = (u * v * z → (∀ u ∈ SNoS_ (SNoLev x , ∀ w ∈ SNoS_ (SNoLev z , u * (y * w = (u * y * w → (∀ v ∈ SNoS_ (SNoLev y , ∀ w ∈ SNoS_ (SNoLev z , x * (v * w = (x * v * w → (∀ u ∈ SNoS_ (SNoLev x , ∀ v ∈ SNoS_ (SNoLev y , ∀ w ∈ SNoS_ (SNoLev z , u * (v * w = (u * v * w → ∀L, (∀ u ∈ L , ∀q : prop , (∀ v ∈ SNoL x , ∀ w ∈ SNoL (y * z , u = v * (y * z + x * w + - v * w q → (∀ v ∈ SNoR x , ∀ w ∈ SNoR (y * z , u = v * (y * z + x * w + - v * w q → q → ∀ u ∈ L , u < (x * y * z Axiom. (
mul_SNo_assoc_lem2 ) We take the following as an axiom:
∀x y z, SNo x SNo y SNo z (∀ u ∈ SNoS_ (SNoLev x , u * (y * z = (u * y * z → (∀ v ∈ SNoS_ (SNoLev y , x * (v * z = (x * v * z → (∀ w ∈ SNoS_ (SNoLev z , x * (y * w = (x * y * w → (∀ u ∈ SNoS_ (SNoLev x , ∀ v ∈ SNoS_ (SNoLev y , u * (v * z = (u * v * z → (∀ u ∈ SNoS_ (SNoLev x , ∀ w ∈ SNoS_ (SNoLev z , u * (y * w = (u * y * w → (∀ v ∈ SNoS_ (SNoLev y , ∀ w ∈ SNoS_ (SNoLev z , x * (v * w = (x * v * w → (∀ u ∈ SNoS_ (SNoLev x , ∀ v ∈ SNoS_ (SNoLev y , ∀ w ∈ SNoS_ (SNoLev z , u * (v * w = (u * v * w → ∀R, (∀ u ∈ R , ∀q : prop , (∀ v ∈ SNoL x , ∀ w ∈ SNoR (y * z , u = v * (y * z + x * w + - v * w q → (∀ v ∈ SNoR x , ∀ w ∈ SNoL (y * z , u = v * (y * z + x * w + - v * w q → q → ∀ u ∈ R , (x * y * z < u End of Section mul_SNo_assoc_lems
Axiom. (
SNo_foil ) We take the following as an axiom:
Axiom. (
SNo_foil_mm ) We take the following as an axiom:
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 .
Notation . We use
^ as an infix operator with priority 342 and which associates to the right corresponding to applying term
exp_SNo_nat .
Axiom. (
eps_bd_1 ) We take the following as an axiom:
Axiom. (
SNoS_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 ) We take the following as an axiom:
Axiom. (
int_add_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 .
Axiom. (
abs_SNo_0 ) We take the following as an axiom:
Axiom. (
pos_abs_SNo ) We take the following as an axiom:
Axiom. (
neg_abs_SNo ) We take the following as an axiom:
Axiom. (
SNo_abs_SNo ) We take the following as an axiom:
Axiom. (
abs_SNo_Lev ) We take the following as an axiom:
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 .
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 .
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
SNo_recipauxset to be
λY x X g ⇒ ⋃ y ∈ Y { (1 + (x' + - x * y * g x' | x' ∈ X } of type
set → set → set → (set → set → set .
Beginning of Section recip_SNo_pos
End of Section recip_SNo_pos
Axiom. (
recip_SNo_0 ) We take the following as an axiom:
Axiom. (
recip_SNo_1 ) We take the following as an axiom:
Axiom. (
recip_SNo_2 ) We take the following as an axiom:
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:
Axiom. (
div_div_SNo ) We take the following as an axiom:
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 .
Proof:
rewrite the current goal using
SNoL_0 (from left to right).
An
exact proof term for the current goal is
Sep_Empty (λw ⇒ 0 ≤ w ) .
∎
Proof:
rewrite the current goal using
SNoL_1 (from left to right).
An
exact proof term for the current goal is
Sep_Subq 1 (λw ⇒ 0 ≤ w ) .
Let w be given.
Apply cases_1 w Hw to the current goal.
Apply SepI to the current goal.
An
exact proof term for the current goal is
In_0_1 .
∎
Proof: Let Y, Z, x and y be given.
Assume Hy .
Let z be given.
Assume Hz .
Assume H1 .
An
exact proof term for the current goal is
ReplSepI Z (λz ⇒ 0 < y + z ) (λz ⇒ (x + y * z :/: (y + z ) z Hz H1 .
∎
Proof: Let Y, Z, x and u be given.
Assume Hu .
Let p be given.
Assume H1 .
Let y be given.
Assume Hu1 .
Let z be given.
An exact proof term for the current goal is H1 y Hy z Hz Hyz Hu2
∎
Proof: Let Z and x be given.
Let u be given.
Assume Hu .
Let y be given.
An
exact proof term for the current goal is
EmptyE y Hy .
∎
Proof: Let Y and x be given.
Let u be given.
Assume Hu .
Let y be given.
Let z be given.
An
exact proof term for the current goal is
EmptyE z Hz .
∎
Proof: Let x and g be given.
∎
Proof: Let x, g and n be given.
Assume Hn .
∎
Proof: Let x, g and m be given.
Assume Hm .
rewrite the current goal using
add_nat_0R m (from left to right).
Apply andI to the current goal.
Let n be given.
Assume Hn IH .
Apply IH
rewrite the current goal using
add_nat_SR m n Hn (from left to right).
rewrite the current goal using
tuple_2_0_eq (from left to right).
rewrite the current goal using
tuple_2_1_eq (from left to right).
Apply andI to the current goal.
∎
Proof: Let x, g and m be given.
Assume Hm .
Let n be given.
Assume Hn Hmn .
Let k be given.
Assume H .
Apply H
rewrite the current goal using
add_nat_com k Hk m Hm (from left to right).
rewrite the current goal using H1
∎
Proof: Let x be given.
Assume Hx .
Let g and h be given.
Assume Hgh .
rewrite the current goal using
SNo_sqrtaux_0 x g (from left to right).
rewrite the current goal using
SNo_sqrtaux_0 x h (from left to right).
Let w be given.
Assume Hw1 Hw2 Hw3 .
Apply Hgh
An
exact proof term for the current goal is
SNoS_I2 w x Hw1 Hx Hw2 .
Let w be given.
Apply SNoR_E x Hx w Hw to the current goal.
Assume Hw1 Hw2 Hw3 .
Apply Hgh
An
exact proof term for the current goal is
SNoS_I2 w x Hw1 Hx Hw2 .
rewrite the current goal using L1
rewrite the current goal using L2
Use reflexivity.
Let k be given.
rewrite the current goal using
SNo_sqrtaux_S x g k Hk (from left to right).
rewrite the current goal using
SNo_sqrtaux_S x h k Hk (from left to right).
rewrite the current goal using IH
Use reflexivity.
∎
Beginning of Section sqrt_SNo_nonneg
Proof:
Let x be given.
Assume Hx .
Let g and h be given.
Assume Hgh .
Use f_equal.
Let k be given.
Assume Hk .
Use f_equal.
An exact proof term for the current goal is Hgh
An
exact proof term for the current goal is
omega_nat_p k Hk .
Let k be given.
Assume Hk .
Use f_equal.
An exact proof term for the current goal is Hgh
An
exact proof term for the current goal is
omega_nat_p k Hk .
∎
Proof: Let x be given.
Assume Hx Hxnonneg IH .
Set L to be the term
⋃ k ∈ ω L_ k .
Set R to be the term
⋃ k ∈ ω R_ k .
Apply andI to the current goal.
Let y be given.
rewrite the current goal using
tuple_2_0_eq (from left to right).
Let w be given.
Apply SepE (SNoL x (λw ⇒ 0 ≤ w ) w Hw to the current goal.
Apply SNoL_E x Hx w Hw to the current goal.
Assume Hw1 Hw2 Hw3 .
An
exact proof term for the current goal is
SNoS_I2 w x Hw1 Hx Hw2 .
Apply IH w Lw Hwnonneg
Assume H .
Apply H
Apply and3I to the current goal.
rewrite the current goal using Hyw
An exact proof term for the current goal is IHa
rewrite the current goal using Hyw
An exact proof term for the current goal is IHb
rewrite the current goal using Hyw
rewrite the current goal using IHc
An exact proof term for the current goal is Hw3
Let y be given.
rewrite the current goal using
tuple_2_1_eq (from left to right).
Let z be given.
Apply SNoR_E x Hx z Hz to the current goal.
Assume Hz1 Hz2 Hz3 .
An
exact proof term for the current goal is
SNoS_I2 z x Hz1 Hx Hz2 .
We prove the intermediate
claim Lznonneg :
0 ≤ z .
Apply IH z Lz Lznonneg
Assume H .
Apply H
Apply and3I to the current goal.
rewrite the current goal using Hyz
An exact proof term for the current goal is IHa
rewrite the current goal using Hyz
An exact proof term for the current goal is IHb
rewrite the current goal using Hyz
rewrite the current goal using IHc
An exact proof term for the current goal is Hz3
Let k be given.
Apply IHk
Assume IHk0 IHk1 .
Apply andI to the current goal.
Let y be given.
rewrite the current goal using
tuple_2_0_eq (from left to right).
An exact proof term for the current goal is IHk0 y
Let w be given.
Let z be given.
Apply IHk0 w Hw
Assume H .
Apply H
Apply IHk1 z Hz
Assume H .
Apply H
We prove the intermediate
claim Lwz :
SNo (w * z .
An
exact proof term for the current goal is
SNo_mul_SNo w z Hw1 Hz1 .
We prove the intermediate
claim Lxpwz :
SNo (x + w * z .
An
exact proof term for the current goal is
SNo_add_SNo x (w * z Hx Lwz .
We prove the intermediate
claim Lwpz :
SNo (w + z .
An
exact proof term for the current goal is
SNo_add_SNo w z Hw1 Hz1 .
We prove the intermediate
claim Ly :
SNo y .
rewrite the current goal using Hywz
An
exact proof term for the current goal is
SNo_div_SNo (x + w * z (w + z Lxpwz Lwpz .
We prove the intermediate
claim Lxpwznonneg :
0 ≤ x + w * z .
We prove the intermediate
claim Lynonneg :
0 ≤ y .
rewrite the current goal using Hywz
We will
prove 0 ≤ (x + w * z :/: (w + z .
Apply SNoLeE 0 (x + w * z SNo_0 Lxpwz Lxpwznonneg to the current goal.
We will
prove 0 < x + w * z .
An exact proof term for the current goal is H1
An exact proof term for the current goal is Hwpzpos
rewrite the current goal using H1
rewrite the current goal using
div_SNo_0_num (w + z Lwpz (from left to right).
Apply and3I to the current goal.
An exact proof term for the current goal is Ly
An exact proof term for the current goal is Lynonneg
rewrite the current goal using Hywz
We will
prove ((x + w * z :/: (w + z * ((x + w * z :/: (w + z < x .
rewrite the current goal using
mul_div_SNo_both (x + w * z (w + z (x + w * z (w + z Lxpwz Lwpz Lxpwz Lwpz (from left to right).
We will
prove ((x + w * z * (x + w * z :/: ((w + z * (w + z < x .
We will
prove 0 < (w + z * (w + z .
An
exact proof term for the current goal is
mul_SNo_pos_pos (w + z (w + z Lwpz Lwpz Hwpzpos Hwpzpos .
We will
prove ((x + w * z * (x + w * z < x * ((w + z * (w + z .
rewrite the current goal using
SNo_foil x (w * z x (w * z Hx Lwz (from left to right).
rewrite the current goal using
SNo_foil w z w z Hw1 Hz1 Hw1 Hz1 (from left to right).
We will
prove x * x + x * w * z + (w * z * x + (w * z * w * z < x * (w * w + w * z + z * w + z * z .
rewrite the current goal using
mul_SNo_com z w Hz1 Hw1 (from left to right).
We will
prove x * x + x * w * z + (w * z * x + (w * z * w * z < x * (w * z + w * z + z * z + w * w .
rewrite the current goal using
mul_SNo_com (w * z x Lwz Hx (from left to right).
We will
prove x * x + x * w * z + x * w * z + (w * z * w * z < x * (w * z + w * z + z * z + w * w .
We prove the intermediate
claim Lxwz :
SNo (x * w * z .
An
exact proof term for the current goal is
SNo_mul_SNo x (w * z Hx Lwz .
We will
prove x * w * z + x * w * z + (w * z * w * z + x * x < x * (w * z + w * z + z * z + w * w .
We prove the intermediate
claim Lxwz :
SNo (x * w * z .
An
exact proof term for the current goal is
SNo_mul_SNo_3 x w z Hx Hw1 Hz1 .
We will
prove x * w * z + (w * z * w * z + x * x < x * w * z + x * (z * z + w * w .
We will
prove (w * z * w * z + x * x < x * (z * z + w * w .
We will
prove (w * z * w * z + x * x < x * z * z + x * w * w .
We will
prove (w * z * w * z + x * x < x * z * z + (w * w * x .
We will
prove 0 + (w * z * w * z + x * x < x * z * z + (w * w * x .
We will
prove 0 < (x * z * z + (w * w * x + - ((w * z * w * z + x * x .
rewrite the current goal using
mul_SNo_assoc w z (w * z Hw1 Hz1 Lwz (from right to left).
rewrite the current goal using
mul_SNo_com_3_0_1 z w z Hz1 Hw1 Hz1 (from left to right).
We will
prove 0 < (x + - w * w * (z * z + - x .
We will
prove 0 < x + - w * w .
We will
prove 0 < z * z + - x .
An exact proof term for the current goal is Hx
We will
prove SNo (w * z .
An exact proof term for the current goal is Lwz
Let y be given.
rewrite the current goal using
tuple_2_1_eq (from left to right).
An exact proof term for the current goal is IHk1 y
Let w be given.
Let w' be given.
Apply IHk0 w Hw
Assume H .
Apply H
Apply IHk0 w' Hw'
Assume H .
Apply H
We prove the intermediate
claim Lww' :
SNo (w * w' .
An
exact proof term for the current goal is
SNo_mul_SNo w w' Hw1 Hw'1 .
We prove the intermediate
claim Lxpww' :
SNo (x + w * w' .
An
exact proof term for the current goal is
SNo_add_SNo x (w * w' Hx Lww' .
We prove the intermediate
claim Lwpw' :
SNo (w + w' .
An
exact proof term for the current goal is
SNo_add_SNo w w' Hw1 Hw'1 .
We prove the intermediate
claim Ly :
SNo y .
rewrite the current goal using Hyww'
An
exact proof term for the current goal is
SNo_div_SNo (x + w * w' (w + w' Lxpww' Lwpw' .
We prove the intermediate
claim Lxpww'nonneg :
0 ≤ x + w * w' .
We will
prove 0 ≤ w * w' .
We prove the intermediate
claim Lynonneg :
0 ≤ y .
rewrite the current goal using Hyww'
We will
prove 0 ≤ (x + w * w' :/: (w + w' .
Apply SNoLeE 0 (x + w * w' SNo_0 Lxpww' Lxpww'nonneg to the current goal.
We will
prove 0 < x + w * w' .
An exact proof term for the current goal is H1
We will
prove 0 < w + w' .
An exact proof term for the current goal is Hww'pos
rewrite the current goal using H1
rewrite the current goal using
div_SNo_0_num (w + w' Lwpw' (from left to right).
Apply and3I to the current goal.
An exact proof term for the current goal is Ly
An exact proof term for the current goal is Lynonneg
rewrite the current goal using Hyww'
We will
prove x < ((x + w * w' :/: (w + w' * ((x + w * w' :/: (w + w' .
rewrite the current goal using
mul_div_SNo_both (x + w * w' (w + w' (x + w * w' (w + w' Lxpww' Lwpw' Lxpww' Lwpw' (from left to right).
We will
prove x < ((x + w * w' * (x + w * w' :/: ((w + w' * (w + w' .
We will
prove 0 < (w + w' * (w + w' .
An
exact proof term for the current goal is
mul_SNo_pos_pos (w + w' (w + w' Lwpw' Lwpw' Hww'pos Hww'pos .
We will
prove x * ((w + w' * (w + w' < ((x + w * w' * (x + w * w' .
rewrite the current goal using
SNo_foil x (w * w' x (w * w' Hx Lww' (from left to right).
rewrite the current goal using
SNo_foil w w' w w' Hw1 Hw'1 Hw1 Hw'1 (from left to right).
We will
prove x * (w * w + w * w' + w' * w + w' * w' < x * x + x * w * w' + (w * w' * x + (w * w' * w * w' .
rewrite the current goal using
mul_SNo_com w' w Hw'1 Hw1 (from left to right).
We will
prove x * (w * w' + w * w' + w' * w' + w * w < x * x + x * w * w' + (w * w' * x + (w * w' * w * w' .
rewrite the current goal using
mul_SNo_com (w * w' x Lww' Hx (from left to right).
We will
prove x * (w * w' + w * w' + w' * w' + w * w < x * x + x * w * w' + x * w * w' + (w * w' * w * w' .
We prove the intermediate
claim Lxww' :
SNo (x * w * w' .
An
exact proof term for the current goal is
SNo_mul_SNo x (w * w' Hx Lww' .
We will
prove x * (w * w' + w * w' + w' * w' + w * w < x * w * w' + x * w * w' + (w * w' * w * w' + x * x .
We will
prove x * w * w' + x * (w * w' + w' * w' + w * w < x * w * w' + x * w * w' + (w * w' * w * w' + x * x .
We will
prove x * w * w' + x * w * w' + x * (w' * w' + w * w < x * w * w' + x * w * w' + (w * w' * w * w' + x * x .
We prove the intermediate
claim Lxww' :
SNo (x * w * w' .
An
exact proof term for the current goal is
SNo_mul_SNo_3 x w w' Hx Hw1 Hw'1 .
We will
prove x * w * w' + x * (w' * w' + w * w < x * w * w' + (w * w' * w * w' + x * x .
We will
prove x * (w' * w' + w * w < (w * w' * w * w' + x * x .
We will
prove x * w' * w' + x * w * w < (w * w' * w * w' + x * x .
We will
prove x * w' * w' + (w * w * x < (w * w' * w * w' + x * x .
We will
prove x * w' * w' + (w * w * x < 0 + (w * w' * w * w' + x * x .
We will
prove (x * w' * w' + (w * w * x + - ((w * w' * w * w' + x * x < 0 .
We will
prove x * w' * w' + (w * w * x + - (w * w' * w * w' + - x * x < 0 .
We will
prove x * w' * w' + - x * x + (w * w * x + - (w * w' * w * w' < 0 .
We will
prove x * w' * w' + - x * x + - (w * w' * w * w' + (w * w * x < 0 .
rewrite the current goal using
mul_SNo_assoc w w' (w * w' Hw1 Hw'1 Lww' (from right to left).
rewrite the current goal using
mul_SNo_com_3_0_1 w' w w' Hw'1 Hw1 Hw'1 (from left to right).
We will
prove (x + - w * w * (w' * w' + - x < 0 .
We will
prove 0 < x + - w * w .
We will
prove w' * w' + - x < 0 .
We will
prove w' * w' < 0 + x .
rewrite the current goal using
add_SNo_0L x Hx (from left to right).
We will
prove w' * w' < x .
An exact proof term for the current goal is Hw'3
An exact proof term for the current goal is Hx
We will
prove SNo (w * w' .
An exact proof term for the current goal is Lww'
Let z be given.
Let z' be given.
Apply IHk1 z Hz
Assume H .
Apply H
Apply IHk1 z' Hz'
Assume H .
Apply H
We prove the intermediate
claim Lzz' :
SNo (z * z' .
An
exact proof term for the current goal is
SNo_mul_SNo z z' Hz1 Hz'1 .
We prove the intermediate
claim Lxpzz' :
SNo (x + z * z' .
An
exact proof term for the current goal is
SNo_add_SNo x (z * z' Hx Lzz' .
We prove the intermediate
claim Lzpz' :
SNo (z + z' .
An
exact proof term for the current goal is
SNo_add_SNo z z' Hz1 Hz'1 .
We prove the intermediate
claim Ly :
SNo y .
rewrite the current goal using Hyzz'
An
exact proof term for the current goal is
SNo_div_SNo (x + z * z' (z + z' Lxpzz' Lzpz' .
We prove the intermediate
claim Lxpzz'nonneg :
0 ≤ x + z * z' .
We will
prove 0 ≤ z * z' .
We prove the intermediate
claim Lynonneg :
0 ≤ y .
rewrite the current goal using Hyzz'
We will
prove 0 ≤ (x + z * z' :/: (z + z' .
Apply SNoLeE 0 (x + z * z' SNo_0 Lxpzz' Lxpzz'nonneg to the current goal.
We will
prove 0 < x + z * z' .
An exact proof term for the current goal is H1
We will
prove 0 < z + z' .
An exact proof term for the current goal is Hzz'pos
rewrite the current goal using H1
rewrite the current goal using
div_SNo_0_num (z + z' Lzpz' (from left to right).
Apply and3I to the current goal.
An exact proof term for the current goal is Ly
An exact proof term for the current goal is Lynonneg
rewrite the current goal using Hyzz'
We will
prove x < ((x + z * z' :/: (z + z' * ((x + z * z' :/: (z + z' .
rewrite the current goal using
mul_div_SNo_both (x + z * z' (z + z' (x + z * z' (z + z' Lxpzz' Lzpz' Lxpzz' Lzpz' (from left to right).
We will
prove x < ((x + z * z' * (x + z * z' :/: ((z + z' * (z + z' .
We will
prove 0 < (z + z' * (z + z' .
An
exact proof term for the current goal is
mul_SNo_pos_pos (z + z' (z + z' Lzpz' Lzpz' Hzz'pos Hzz'pos .
We will
prove x * ((z + z' * (z + z' < ((x + z * z' * (x + z * z' .
rewrite the current goal using
SNo_foil x (z * z' x (z * z' Hx Lzz' (from left to right).
rewrite the current goal using
SNo_foil z z' z z' Hz1 Hz'1 Hz1 Hz'1 (from left to right).
We will
prove x * (z * z + z * z' + z' * z + z' * z' < x * x + x * z * z' + (z * z' * x + (z * z' * z * z' .
rewrite the current goal using
mul_SNo_com z' z Hz'1 Hz1 (from left to right).
We will
prove x * (z * z' + z * z' + z' * z' + z * z < x * x + x * z * z' + (z * z' * x + (z * z' * z * z' .
rewrite the current goal using
mul_SNo_com (z * z' x Lzz' Hx (from left to right).
We will
prove x * (z * z' + z * z' + z' * z' + z * z < x * x + x * z * z' + x * z * z' + (z * z' * z * z' .
We prove the intermediate
claim Lxzz' :
SNo (x * z * z' .
An
exact proof term for the current goal is
SNo_mul_SNo x (z * z' Hx Lzz' .
We will
prove x * (z * z' + z * z' + z' * z' + z * z < x * z * z' + x * z * z' + (z * z' * z * z' + x * x .
We will
prove x * z * z' + x * (z * z' + z' * z' + z * z < x * z * z' + x * z * z' + (z * z' * z * z' + x * x .
We will
prove x * z * z' + x * z * z' + x * (z' * z' + z * z < x * z * z' + x * z * z' + (z * z' * z * z' + x * x .
We prove the intermediate
claim Lxzz' :
SNo (x * z * z' .
An
exact proof term for the current goal is
SNo_mul_SNo_3 x z z' Hx Hz1 Hz'1 .
We will
prove x * z * z' + x * (z' * z' + z * z < x * z * z' + (z * z' * z * z' + x * x .
We will
prove x * (z' * z' + z * z < (z * z' * z * z' + x * x .
We will
prove x * z' * z' + x * z * z < (z * z' * z * z' + x * x .
We will
prove x * z' * z' + (z * z * x < (z * z' * z * z' + x * x .
We will
prove x * z' * z' + (z * z * x < 0 + (z * z' * z * z' + x * x .
We will
prove (x * z' * z' + (z * z * x + - ((z * z' * z * z' + x * x < 0 .
We will
prove x * z' * z' + (z * z * x + - (z * z' * z * z' + - x * x < 0 .
We will
prove x * z' * z' + - x * x + (z * z * x + - (z * z' * z * z' < 0 .
We will
prove x * z' * z' + - x * x + - (z * z' * z * z' + (z * z * x < 0 .
rewrite the current goal using
mul_SNo_assoc z z' (z * z' Hz1 Hz'1 Lzz' (from right to left).
rewrite the current goal using
mul_SNo_com_3_0_1 z' z z' Hz'1 Hz1 Hz'1 (from left to right).
We will
prove (x + - z * z * (z' * z' + - x < 0 .
We will
prove x + - z * z < 0 .
We will
prove x < 0 + z * z .
An exact proof term for the current goal is Hz3
We will
prove 0 < z' * z' + - x .
An exact proof term for the current goal is Hx
We will
prove SNo (z * z' .
An exact proof term for the current goal is Lzz'
∎
Proof: Let x be given.
Assume Hx Hxnonneg .
Set L to be the term
⋃ k ∈ ω L_ k .
Set R to be the term
⋃ k ∈ ω R_ k .
Apply and3I to the current goal.
Let w be given.
Let k be given.
Assume H2 _ .
Apply H2 w H1
Assume H3 _ .
Apply H3
Assume H3 _ .
An exact proof term for the current goal is H3
Let z be given.
Let k be given.
Assume _ H2 .
Apply H2 z H1
Assume H3 _ .
Apply H3
Assume H3 _ .
An exact proof term for the current goal is H3
Let w be given.
Let z be given.
Let k be given.
Assume H2 _ .
Apply H2 w H1
Assume H .
Apply H
Let k' be given.
Assume _ H4 .
Apply H4 z H3
Assume H .
Apply H
An exact proof term for the current goal is H5
We will
prove z * z ≤ w * w .
An
exact proof term for the current goal is
nonneg_mul_SNo_Le2 z z w w Hz1 Hz1 Hw1 Hw1 Hz2 Hz2 H5 H5 .
An exact proof term for the current goal is Hw3
∎
Proof: Let x be given.
Assume Hx Hxnonneg H1 H1R .
rewrite the current goal using
SNoCut_0_0 (from right to left) at position 1.
Set L to be the term
⋃ k ∈ ω L_ k .
Set R to be the term
⋃ k ∈ ω R_ k .
An
exact proof term for the current goal is
SNoCutP_0_0 .
An exact proof term for the current goal is H1
Let w be given.
An
exact proof term for the current goal is
EmptyE w Hw .
Let z be given.
rewrite the current goal using
SNoCut_0_0 (from left to right).
Apply H1R z Hz
An exact proof term for the current goal is H6
rewrite the current goal using H6
An exact proof term for the current goal is Hz3
An exact proof term for the current goal is Hxnonneg
∎
Proof: Let x be given.
Assume Hx Hxnonneg IH HLR .
Set L to be the term
⋃ k ∈ ω L_ k .
Set R to be the term
⋃ k ∈ ω R_ k .
Set y to be the term
SNoCut L R .
Apply HLR
Assume HLHR .
Apply HLHR
We prove the intermediate
claim Lyy :
SNo (y * y .
An
exact proof term for the current goal is
SNo_mul_SNo y y H1 H1 .
We prove the intermediate
claim Lyynn :
0 ≤ y * y .
We prove the intermediate
claim LL_mon :
∀k k', nat_p k nat_p k' k ⊆ k' L_ k ⊆ L_ k' .
Let k and k' be given.
Assume Hk Hk' Hkk' .
Assume H _ .
An exact proof term for the current goal is H
We prove the intermediate
claim LR_mon :
∀k k', nat_p k nat_p k' k ⊆ k' R_ k ⊆ R_ k' .
Let k and k' be given.
Assume Hk Hk' Hkk' .
Assume _ H .
An exact proof term for the current goal is H
We prove the intermediate
claim L1L :
∀ w ∈ L , ∀p : prop , (SNo w 0 ≤ w w * w < x p → p .
Let w be given.
Assume Hw .
Let p be given.
Assume Hp .
Let k be given.
Assume H2 _ .
Apply H2 w H1
Assume H3 .
Apply H3
An exact proof term for the current goal is Hp
We prove the intermediate
claim L1R :
∀ z ∈ R , ∀p : prop , (SNo z 0 ≤ z x < z * z p → p .
Let z be given.
Assume Hz .
Let p be given.
Assume Hp .
Let k be given.
Assume _ H2 .
Apply H2 z H1
Assume H3 .
Apply H3
An exact proof term for the current goal is Hp
Apply SNoLtE (y * y x Lyy Hx H6 to the current goal.
Let u be given.
We prove the intermediate
claim Lunn :
0 ≤ u .
An
exact proof term for the current goal is
SNoLeLt_tra 0 (y * y u SNo_0 Lyy Hu1 Lyynn Hu5 .
Apply SNoS_I2 u x Hu1 Hx to the current goal.
Apply IH u LuSx Lunn
Assume H .
Apply H
Apply H3
rewrite the current goal using
SNo_sqrtaux_0 (from left to right).
rewrite the current goal using
tuple_2_0_eq (from left to right).
Apply ReplI to the current goal.
Apply SepI to the current goal.
Apply SNoL_I x Hx u Hu1 to the current goal.
An exact proof term for the current goal is Hu6
An exact proof term for the current goal is Lunn
We prove the intermediate
claim Luyy :
u ≤ y * y .
rewrite the current goal using H9
We will
prove y * y < y * y .
An
exact proof term for the current goal is
SNoLtLe_tra (y * y u (y * y Lyy Hu1 Lyy Hu5 Luyy .
Apply IH (y * y (SNoS_I2 (y * y x Lyy Hx H7 Lyynn to the current goal.
Assume H .
Apply H
rewrite the current goal using Lsryy
Apply H3
rewrite the current goal using
SNo_sqrtaux_0 (from left to right).
rewrite the current goal using
tuple_2_0_eq (from left to right).
Apply ReplI to the current goal.
Apply SepI to the current goal.
An
exact proof term for the current goal is
SNoL_I x Hx (y * y Lyy H7 H6 .
An exact proof term for the current goal is Lyynn
We prove the intermediate
claim L3 :
x ∈ SNoR (y * y .
An
exact proof term for the current goal is
SNoR_I (y * y Lyy x Hx H7 H6 .
We prove the intermediate
claim L4 :
∀p : prop , (∀ v ∈ L , ∀ w ∈ R , v * y + y * w ≤ x + v * w p → p .
Let p be given.
Assume Hp .
Let v be given.
Let w be given.
An exact proof term for the current goal is Hp v Hv w Hw H10
Let v be given.
Let w be given.
Apply Hp w Hw v Hv
We will
prove w * y + y * v ≤ x + w * v .
We prove the intermediate
claim Lv1 :
SNo v .
An exact proof term for the current goal is HR v Hv
We prove the intermediate
claim Lw1 :
SNo w .
An exact proof term for the current goal is HL w Hw
rewrite the current goal using
mul_SNo_com w v Lw1 Lv1 (from left to right).
We will
prove w * y + y * v ≤ x + v * w .
Apply mul_SNo_com w y Lw1 H1 (λ_ u ⇒ u + y * v ≤ x + v * w ) to the current goal.
We will
prove y * w + y * v ≤ x + v * w .
Apply mul_SNo_com y v H1 Lv1 (λ_ u ⇒ y * w + u ≤ x + v * w ) to the current goal.
We will
prove y * w + v * y ≤ x + v * w .
An exact proof term for the current goal is H10
Apply L4
Let v be given.
Let w be given.
Apply L1L v Hv
Apply L1R w Hw
We prove the intermediate
claim L5 :
∃ k, nat_p k ∧ v ∈ L_ k ∧ w ∈ R_ k .
Let k' be given.
Assume H .
Apply H
Let k'' be given.
Assume H .
Apply H
We use k'' witness the existential quantifier.
Apply and3I to the current goal.
An
exact proof term for the current goal is
omega_nat_p k'' Hk''1 .
We will
prove v ∈ L_ k'' .
An
exact proof term for the current goal is
LL_mon k' k'' (omega_nat_p k' Hk'1 (omega_nat_p k'' Hk''1 H1 v Hk'2 .
An exact proof term for the current goal is Hk''2
We use k' witness the existential quantifier.
Apply and3I to the current goal.
An
exact proof term for the current goal is
omega_nat_p k' Hk'1 .
An exact proof term for the current goal is Hk'2
An
exact proof term for the current goal is
LR_mon k'' k' (omega_nat_p k'' Hk''1 (omega_nat_p k' Hk'1 H1 w Hk''2 .
Apply L5
Let k be given.
Assume H .
Apply H
Assume H .
Apply H
We prove the intermediate
claim Lvwpos :
0 < v + w .
rewrite the current goal using
add_SNo_0R v Hv1 (from right to left) at position 1.
We will
prove v + 0 < v + w .
Apply H4
We prove the intermediate
claim Lvw0 :
v + w ≠ 0 .
Assume H .
rewrite the current goal using H
An exact proof term for the current goal is Lvwpos
We prove the intermediate
claim L6 :
(x + v * w :/: (v + w ∈ L_ (ordsucc k .
rewrite the current goal using
tuple_2_0_eq (from left to right).
An
exact proof term for the current goal is
SNo_sqrtauxset_I (L_ k (R_ k x v Hvk w Hwk Lvwpos .
We prove the intermediate
claim L7 :
(x + v * w :/: (v + w ∈ L .
We prove the intermediate
claim L8 :
(x + v * w :/: (v + w < y .
An
exact proof term for the current goal is
H3 ((x + v * w :/: (v + w L7 .
We prove the intermediate
claim L9 :
v * y + y * w = y * (v + w .
Use transitivity with and
y * v + y * w .
Use f_equal.
We will
prove v * y = y * v .
An
exact proof term for the current goal is
mul_SNo_com v y Hv1 H1 .
We will
prove y * v + y * w = y * (v + w .
Use symmetry.
An
exact proof term for the current goal is
mul_SNo_distrL y v w H1 Hv1 Hw1 .
We will
prove x + v * w < v * y + y * w .
rewrite the current goal using L9
We will
prove x + v * w < y * (v + w .
We will
prove ((x + v * w :/: (v + w * (v + w < y * (v + w .
∎
Proof: Let x be given.
Assume Hx Hxnonneg IH HLR .
Set L to be the term
⋃ k ∈ ω L_ k .
Set R to be the term
⋃ k ∈ ω R_ k .
Set y to be the term
SNoCut L R .
Apply HLR
Assume HLHR .
Apply HLHR
We prove the intermediate
claim Lyy :
SNo (y * y .
An
exact proof term for the current goal is
SNo_mul_SNo y y H1 H1 .
We prove the intermediate
claim Lyynn :
0 ≤ y * y .
We prove the intermediate
claim LL_mon :
∀k k', nat_p k nat_p k' k ⊆ k' L_ k ⊆ L_ k' .
Let k and k' be given.
Assume Hk Hk' Hkk' .
Assume H _ .
An exact proof term for the current goal is H
We prove the intermediate
claim LR_mon :
∀k k', nat_p k nat_p k' k ⊆ k' R_ k ⊆ R_ k' .
Let k and k' be given.
Assume Hk Hk' Hkk' .
Assume _ H .
An exact proof term for the current goal is H
We prove the intermediate
claim L1L :
∀ w ∈ L , ∀p : prop , (SNo w 0 ≤ w w * w < x p → p .
Let w be given.
Assume Hw .
Let p be given.
Assume Hp .
Let k be given.
Assume H2 _ .
Apply H2 w H1
Assume H3 .
Apply H3
An exact proof term for the current goal is Hp
We prove the intermediate
claim L1R :
∀ z ∈ R , ∀p : prop , (SNo z 0 ≤ z x < z * z p → p .
Let z be given.
Assume Hz .
Let p be given.
Assume Hp .
Let k be given.
Assume _ H2 .
Apply H2 z H1
Assume H3 .
Apply H3
An exact proof term for the current goal is Hp
Apply SNoLtE x (y * y Hx Lyy H6 to the current goal.
Let u be given.
We prove the intermediate
claim Lunn :
0 ≤ u .
An
exact proof term for the current goal is
SNoLeLt_tra 0 x u SNo_0 Hx Hu1 Hxnonneg Hu5 .
Apply SNoS_I2 u x Hu1 Hx to the current goal.
Apply IH u LuSx Lunn
Assume H .
Apply H
Apply H4
rewrite the current goal using
SNo_sqrtaux_0 (from left to right).
rewrite the current goal using
tuple_2_1_eq (from left to right).
Apply ReplI to the current goal.
Apply SNoR_I x Hx u Hu1 to the current goal.
An exact proof term for the current goal is Hu5
Apply SNoLtLe_tra u (y * y u Hu1 Lyy Hu1 Hu6 to the current goal.
rewrite the current goal using H9
We prove the intermediate
claim L10 :
x ∈ SNoL (y * y .
An
exact proof term for the current goal is
SNoL_I (y * y Lyy x Hx H7 H6 .
Let v be given.
Let w be given.
Apply L1L v Hv
Apply L1L w Hw
We prove the intermediate
claim L11 :
∃ k, nat_p k ∧ v ∈ L_ k ∧ w ∈ L_ k .
Let k' be given.
Assume H .
Apply H
Let k'' be given.
Assume H .
Apply H
We use k'' witness the existential quantifier.
Apply and3I to the current goal.
An
exact proof term for the current goal is
omega_nat_p k'' Hk''1 .
We will
prove v ∈ L_ k'' .
An
exact proof term for the current goal is
LL_mon k' k'' (omega_nat_p k' Hk'1 (omega_nat_p k'' Hk''1 H1 v Hk'2 .
An exact proof term for the current goal is Hk''2
We use k' witness the existential quantifier.
Apply and3I to the current goal.
An
exact proof term for the current goal is
omega_nat_p k' Hk'1 .
An exact proof term for the current goal is Hk'2
An
exact proof term for the current goal is
LL_mon k'' k' (omega_nat_p k'' Hk''1 (omega_nat_p k' Hk'1 H1 w Hk''2 .
Apply L11
Let k be given.
Assume H .
Apply H
Assume H .
Apply H
We prove the intermediate
claim Lvw0 :
v + w ≠ 0 .
Assume H .
rewrite the current goal using H
An exact proof term for the current goal is H11
We prove the intermediate
claim L12 :
(x + v * w :/: (v + w ∈ R_ (ordsucc k .
rewrite the current goal using
tuple_2_1_eq (from left to right).
An
exact proof term for the current goal is
SNo_sqrtauxset_I (L_ k (L_ k x v Hvk w Hwk H11 .
We prove the intermediate
claim L13 :
(x + v * w :/: (v + w ∈ R .
We prove the intermediate
claim L14 :
y < (x + v * w :/: (v + w .
An
exact proof term for the current goal is
H4 ((x + v * w :/: (v + w L13 .
We prove the intermediate
claim L15 :
v * y + y * w = y * (v + w .
Use transitivity with and
y * v + y * w .
Use f_equal.
We will
prove v * y = y * v .
An
exact proof term for the current goal is
mul_SNo_com v y Hv1 H1 .
We will
prove y * v + y * w = y * (v + w .
Use symmetry.
An
exact proof term for the current goal is
mul_SNo_distrL y v w H1 Hv1 Hw1 .
We will
prove v * y + y * w < x + v * w .
rewrite the current goal using L15
We will
prove y * (v + w < x + v * w .
We will
prove y * (v + w < ((x + v * w :/: (v + w * (v + w .
We prove the intermediate
claim L16 :
v = 0 ∧ w = 0 .
rewrite the current goal using
add_SNo_0R v Hv1 (from right to left) at position 1.
We will
prove v + 0 ≤ v + w .
An exact proof term for the current goal is H11
rewrite the current goal using
add_SNo_0L w Hw1 (from right to left) at position 1.
We will
prove 0 + w ≤ v + w .
An exact proof term for the current goal is H11
Apply andI to the current goal.
Apply L16
We prove the intermediate
claim L17 :
x + v * w = x .
rewrite the current goal using Hv0
rewrite the current goal using
mul_SNo_zeroL w Hw1 (from left to right).
An
exact proof term for the current goal is
add_SNo_0R x Hx .
We prove the intermediate
claim L18 :
v * y + y * w = 0 .
rewrite the current goal using Hv0
We will
prove 0 * y + y * w = 0 .
rewrite the current goal using Hw0
We prove the intermediate
claim L19 :
x ≤ 0 .
rewrite the current goal using L17
rewrite the current goal using L18
An exact proof term for the current goal is H10
We prove the intermediate
claim L20 :
x = 0 .
We will
prove v * v < v * v .
rewrite the current goal using Hv0
We will
prove v * v < 0 * v .
rewrite the current goal using
mul_SNo_zeroL v Hv1 (from left to right).
rewrite the current goal using L20
An exact proof term for the current goal is Hv3
Let v be given.
Let w be given.
Apply L1R v Hv
Apply L1R w Hw
We prove the intermediate
claim L21 :
∃ k, nat_p k ∧ v ∈ R_ k ∧ w ∈ R_ k .
Let k' be given.
Assume H .
Apply H
Let k'' be given.
Assume H .
Apply H
We use k'' witness the existential quantifier.
Apply and3I to the current goal.
An
exact proof term for the current goal is
omega_nat_p k'' Hk''1 .
We will
prove v ∈ R_ k'' .
An
exact proof term for the current goal is
LR_mon k' k'' (omega_nat_p k' Hk'1 (omega_nat_p k'' Hk''1 H1 v Hk'2 .
An exact proof term for the current goal is Hk''2
We use k' witness the existential quantifier.
Apply and3I to the current goal.
An
exact proof term for the current goal is
omega_nat_p k' Hk'1 .
An exact proof term for the current goal is Hk'2
An
exact proof term for the current goal is
LR_mon k'' k' (omega_nat_p k'' Hk''1 (omega_nat_p k' Hk'1 H1 w Hk''2 .
Apply L21
Let k be given.
Assume H .
Apply H
Assume H .
Apply H
We prove the intermediate
claim Lvwpos :
0 < v + w .
rewrite the current goal using
add_SNo_0R v Hv1 (from right to left) at position 1.
We will
prove v + 0 < v + w .
Apply H4
We prove the intermediate
claim Lvw0 :
v + w ≠ 0 .
Assume H .
rewrite the current goal using H
An exact proof term for the current goal is Lvwpos
We prove the intermediate
claim L22 :
(x + v * w :/: (v + w ∈ R_ (ordsucc k .
rewrite the current goal using
tuple_2_1_eq (from left to right).
An
exact proof term for the current goal is
SNo_sqrtauxset_I (R_ k (R_ k x v Hvk w Hwk Lvwpos .
We prove the intermediate
claim L23 :
(x + v * w :/: (v + w ∈ R .
We prove the intermediate
claim L24 :
y < (x + v * w :/: (v + w .
An
exact proof term for the current goal is
H4 ((x + v * w :/: (v + w L23 .
We prove the intermediate
claim L25 :
v * y + y * w = y * (v + w .
Use transitivity with and
y * v + y * w .
Use f_equal.
We will
prove v * y = y * v .
An
exact proof term for the current goal is
mul_SNo_com v y Hv1 H1 .
We will
prove y * v + y * w = y * (v + w .
Use symmetry.
An
exact proof term for the current goal is
mul_SNo_distrL y v w H1 Hv1 Hw1 .
We will
prove v * y + y * w < x + v * w .
rewrite the current goal using L25
We will
prove y * (v + w < x + v * w .
We will
prove y * (v + w < ((x + v * w :/: (v + w * (v + w .
Apply IH (y * y (SNoS_I2 (y * y x Lyy Hx H7 Lyynn to the current goal.
Assume H .
Apply H
rewrite the current goal using Lsryy
Apply H4
rewrite the current goal using
SNo_sqrtaux_0 (from left to right).
rewrite the current goal using
tuple_2_1_eq (from left to right).
Apply ReplI to the current goal.
An
exact proof term for the current goal is
SNoR_I x Hx (y * y Lyy H7 H6 .
∎
Proof:
Let x be given.
Set L to be the term
⋃ k ∈ ω L_ k .
Set R to be the term
⋃ k ∈ ω R_ k .
We prove the intermediate
claim LL_mon :
∀k k', nat_p k nat_p k' k ⊆ k' L_ k ⊆ L_ k' .
Let k and k' be given.
Assume Hk Hk' Hkk' .
Assume H _ .
An exact proof term for the current goal is H
We prove the intermediate
claim LR_mon :
∀k k', nat_p k nat_p k' k ⊆ k' R_ k ⊆ R_ k' .
Let k and k' be given.
Assume Hk Hk' Hkk' .
Assume _ H .
An exact proof term for the current goal is H
We prove the intermediate
claim L1L :
∀ w ∈ L , ∀p : prop , (SNo w 0 ≤ w w * w < x p → p .
Let w be given.
Assume Hw .
Let p be given.
Assume Hp .
Let k be given.
Assume H2 _ .
Apply H2 w H1
Assume H3 .
Apply H3
An exact proof term for the current goal is Hp
We prove the intermediate
claim L1R :
∀ z ∈ R , ∀p : prop , (SNo z 0 ≤ z x < z * z p → p .
Let z be given.
Assume Hz .
Let p be given.
Assume Hp .
Let k be given.
Assume _ H2 .
Apply H2 z H1
Assume H3 .
Apply H3
An exact proof term for the current goal is Hp
We prove the intermediate
claim L2 :
SNoCutP L R .
Apply L2
Assume HLHR .
Apply HLHR
Set y to be the term
SNoCut L R .
We prove the intermediate
claim Lynn :
0 ≤ y .
Apply and3I to the current goal.
An exact proof term for the current goal is H1
An exact proof term for the current goal is Lynn
We prove the intermediate
claim Lyy :
SNo (y * y .
An
exact proof term for the current goal is
SNo_mul_SNo y y H1 H1 .
We prove the intermediate
claim Lyynn :
0 ≤ y * y .
An exact proof term for the current goal is H6
∎
End of Section sqrt_SNo_nonneg
Proof: Let x be given.
Assume Hx Hxnonneg .
Let w be given.
Assume Hw Hwnonneg .
Assume Hw1 Hw2 Hw3 Hw4 .
∎
Proof: Let x be given.
Assume Hx Hxnonneg .
Let k be given.
Assume Hk .
Assume H _ .
An exact proof term for the current goal is H
∎
Proof: Let x be given.
Assume Hx Hxnonneg .
Let k be given.
Assume Hk .
Assume _ H .
An exact proof term for the current goal is H
∎
Proof: Let x be given.
Assume Hx Hxnonneg .
∎
Proof: Let x be given.
Assume Hx Hxnonneg .
Assume H _ .
Apply H
Assume H _ .
An exact proof term for the current goal is H
∎
Proof: Let x be given.
Assume Hx Hxnonneg .
Assume H _ .
Apply H
Assume _ H .
An exact proof term for the current goal is H
∎
Proof: Let x be given.
Assume Hx Hxnonneg .
Assume _ H .
An exact proof term for the current goal is H
∎
Proof:
Set L to be the term
⋃ k ∈ ω L_ k .
Set R to be the term
⋃ k ∈ ω R_ k .
We prove the intermediate
claim L1 :
∀k, nat_p k L_ k = 0 ∧ R_ k = 0 .
Apply andI to the current goal.
rewrite the current goal using
SNo_sqrtaux_0 (from left to right).
rewrite the current goal using
tuple_2_0_eq (from left to right).
rewrite the current goal using
SNoL_nonneg_0 (from left to right).
rewrite the current goal using
SNo_sqrtaux_0 (from left to right).
rewrite the current goal using
tuple_2_1_eq (from left to right).
rewrite the current goal using
SNoR_0 (from left to right).
Let k be given.
Assume Hk .
Assume IHk .
Apply IHk
Apply andI to the current goal.
rewrite the current goal using
tuple_2_0_eq (from left to right).
rewrite the current goal using IHLk
rewrite the current goal using
tuple_2_1_eq (from left to right).
rewrite the current goal using IHLk
rewrite the current goal using IHRk
rewrite the current goal using
binunion_idl 0 (from left to right).
We prove the intermediate
claim L2 :
L = 0 .
Let x be given.
Let k be given.
Assume _ .
rewrite the current goal using H1
An
exact proof term for the current goal is
EmptyE x .
We prove the intermediate
claim L3 :
R = 0 .
Let x be given.
Let k be given.
Assume _ .
rewrite the current goal using H1
An
exact proof term for the current goal is
EmptyE x .
rewrite the current goal using L2
rewrite the current goal using L3
An
exact proof term for the current goal is
SNoCut_0_0 .
∎
Proof:
Set L to be the term
⋃ k ∈ ω L_ k .
Set R to be the term
⋃ k ∈ ω R_ k .
We prove the intermediate
claim L1 :
∀k, nat_p k L_ k = 1 ∧ R_ k = 0 .
Apply andI to the current goal.
rewrite the current goal using
SNo_sqrtaux_0 (from left to right).
rewrite the current goal using
tuple_2_0_eq (from left to right).
rewrite the current goal using
SNoL_nonneg_1 (from left to right).
Let u be given.
Let w be given.
Apply cases_1 w Hw to the current goal.
rewrite the current goal using Hu0
An
exact proof term for the current goal is
In_0_1 .
Let u be given.
Apply cases_1 u Hu to the current goal.
Apply ReplI to the current goal.
An
exact proof term for the current goal is
In_0_1 .
rewrite the current goal using
SNo_sqrtaux_0 (from left to right).
rewrite the current goal using
tuple_2_1_eq (from left to right).
rewrite the current goal using
SNoR_1 (from left to right).
Let k be given.
Assume Hk .
Assume IHk .
Apply IHk
Apply andI to the current goal.
rewrite the current goal using
tuple_2_0_eq (from left to right).
rewrite the current goal using IHLk
rewrite the current goal using IHRk
rewrite the current goal using
tuple_2_1_eq (from left to right).
rewrite the current goal using IHLk
rewrite the current goal using IHRk
Let u be given.
Let w be given.
Let z be given.
Apply cases_1 w Hw to the current goal.
Apply cases_1 z Hz to the current goal.
An exact proof term for the current goal is H1
We prove the intermediate
claim L2 :
L = 1 .
Let x be given.
Let k be given.
Assume _ .
We will
prove x ∈ L_ k x ∈ 1 .
rewrite the current goal using H1
An exact proof term for the current goal is H2
Let x be given.
Apply cases_1 x Hx to the current goal.
We prove the intermediate
claim L2a :
0 ∈ L_ 0 .
Apply L1 0 nat_0 to the current goal.
Assume _ .
rewrite the current goal using H1
An
exact proof term for the current goal is
In_0_1 .
We will
prove 0 ∈ ⋃ k ∈ ω L_ k .
We prove the intermediate
claim L3 :
R = 0 .
Let x be given.
Let k be given.
Assume _ .
rewrite the current goal using H1
An
exact proof term for the current goal is
EmptyE x .
rewrite the current goal using L2
rewrite the current goal using L3
rewrite the current goal using
SNoL_1 (from right to left) at position 1.
rewrite the current goal using
SNoR_1 (from right to left) at position 2.
Use symmetry.
∎
End of Section SurrealSqrt