Addition on Surreal Numbers
From Parts 1 - 4
Object . 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
Object . 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 .
Object . The name
Empty is a term of type
set .
Axiom. (
EmptyAx ) We take the following as an axiom:
Object . The name
⋃ is a term of type
set → set .
Axiom. (
UnionEq ) We take the following as an axiom:
∀X x, x ∈ ⋃ X ↔ ∃Y, x ∈ Y ∧ Y ∈ X
Object . 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
Object . 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 .
Object . 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:
∀A B : prop , A ∧ B → A
Axiom. (
andER ) We take the following as an axiom:
∀A B : prop , A ∧ B → B
Axiom. (
orIL ) We take the following as an axiom:
∀A B : prop , A → A ∨ B
Axiom. (
orIR ) We take the following as an axiom:
∀A B : prop , B → A ∨ B
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:
P1 → P1 ∨ P2 ∨ P3
Axiom. (
or3I2 ) We take the following as an axiom:
P2 → P1 ∨ P2 ∨ P3
Axiom. (
or3I3 ) We take the following as an axiom:
P3 → P1 ∨ P2 ∨ P3
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. (
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 : set → prop , (¬ ∃x, P x ) → ∀x, ¬ P x
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:
∀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 = 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:
∀x y, x ≠ y → y ≠ x
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:
∀X : set , X ⊆ X
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:
∀X : set , (∀x, x ∉ X ) → X = Empty
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:
∀P : prop , P ∨ ¬ P
Axiom. (
dneg ) We take the following as an axiom:
∀P : prop , ¬ ¬ P → P
Axiom. (
not_all_ex_demorgan_i ) We take the following as an axiom:
∀P : set → prop , ¬ (∀x, P x ) → ∃x, ¬ P x
Axiom. (
eq_or_nand ) We take the following as an axiom:
or = (λx y : prop ⇒ ¬ (¬ x ∧ ¬ y ) )
Object . 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_sub ) 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. (
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
Object . 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_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
Object . 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:
∀y z : set , y ∈ {y ,z }
Axiom. (
UPairI2 ) We take the following as an axiom:
∀y z : set , z ∈ {y ,z }
Object . 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:
∀x : set , x ∈ {x }
Axiom. (
SingE ) We take the following as an axiom:
∀x y : set , y ∈ {x } → y = x
Object . 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_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_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 ⊆ Z → Y ⊆ Z → X ∪ 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
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.
Object . 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 )
Let F : set → set ≝ λx ⇒ if P x then x else z
Object . 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_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
Object . 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
Object . 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
Axiom. (
binintersectE1 ) We take the following as an axiom:
∀X Y z, z ∈ X ∩ Y → z ∈ X
Axiom. (
binintersectE2 ) We take the following as an axiom:
∀X Y z, z ∈ X ∩ Y → z ∈ Y
Axiom. (
binintersect_Subq_max ) We take the following as an axiom:
∀X Y Z : set , Z ⊆ X → Z ⊆ Y → Z ⊆ X ∩ Y
Axiom. (
binintersect_com ) We take the following as an axiom:
∀X Y : set , X ∩ Y = Y ∩ X
Object . 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. (
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 ⊆ Y → X ∖ Y ⊆ X ∖ Z
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 ∈ y → y ∈ x → False
Object . 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:
∀x y : set , y ∈ ordsucc x → y ∈ 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. (
ordsucc_inj ) We take the following as an axiom:
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 : 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_complete_ind ) We take the following as an axiom:
∀p : set → prop , (∀n, nat_p n → (∀m ∈ n , p m ) → p n ) → ∀n, nat_p n → p n
Axiom. (
nat_p_trans ) We take the following as an axiom:
Axiom. (
nat_trans ) We take the following as an axiom:
∀n, nat_p n → ∀m ∈ n , m ⊆ n
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:
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:
Axiom. (
ZF_Repl_closed ) We take the following as an axiom:
∀U, ZF_closed U → ∀X ∈ U , ∀F : set → set , (∀x ∈ X , F x ∈ U ) → {F x |x ∈ X } ∈ U
Object . 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:
Definition. We define
ordinal to be
λalpha : set ⇒ TransSet alpha ∧ ∀beta ∈ alpha , TransSet beta of type
set → prop .
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
Axiom. (
least_ordinal_ex ) We take the following as an axiom:
∀p : set → prop , (∃alpha, ordinal alpha ∧ p alpha ) → ∃alpha, ordinal alpha ∧ p alpha ∧ ∀beta ∈ alpha , ¬ p beta
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
Object . The name
inv is a term of type
set → (set → set ) → set → set .
Axiom. (
surj_rinv ) We take the following as an axiom:
∀X Y, ∀f : set → set , (∀w ∈ Y , ∃u ∈ X , f u = w ) → ∀y ∈ Y , inv X f y ∈ X ∧ f (inv X f y ) = y
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
Axiom. (
KnasterTarski_set ) We take the following as an axiom:
∀A, ∀F : set → set , (∀U ∈ 𝒫 A , F U ∈ 𝒫 A ) → (∀U V ∈ 𝒫 A , U ⊆ V → F U ⊆ F V ) → ∃Y ∈ 𝒫 A , F Y = Y
Axiom. (
image_In_Power ) We take the following as an axiom:
∀A B, ∀f : set → set , (∀x ∈ A , f x ∈ B ) → ∀U ∈ 𝒫 A , {f x |x ∈ U } ∈ 𝒫 B
Axiom. (
image_monotone ) We take the following as an axiom:
∀f : set → set , ∀U V, U ⊆ V → {f x |x ∈ U } ⊆ {f x |x ∈ V }
End of Section SchroederBernstein
Beginning of Section PigeonHole
Axiom. (
PigeonHole_nat_bij ) We take the following as an axiom:
∀n, nat_p n → ∀f : set → set , (∀i ∈ n , f i ∈ n ) → (∀i j ∈ n , f i = f j → i = j ) → bij n n f
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:
∀p : set → prop , p Empty → (∀X y, finite X → y ∉ X → p X → p (X ∪ {y } ) ) → ∀X, finite X → p X
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
Object . 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
Object . 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
Variable P : Vo 1 → prop
Object . 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
Object . 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
Object . 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
Object . 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 )
Object . 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 )
Object . 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:
∀n : set , n + 0 = n
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_1_1_2 ) We take the following as an axiom:
1 + 1 = 2
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:
∀n : set , n * 0 = 0
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
Definition. We define
Inj1 to be
In_rec_i (λX f ⇒ {0 } ∪ {f x |x ∈ X } ) of type
set → set .
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:
∀X y : set , y ∈ Inj1 X → y = 0 ∨ ∃x ∈ X , y = Inj1 x
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:
∀X y : set , y ∈ Inj0 X → ∃x : set , x ∈ X ∧ y = Inj1 x
Definition. We define
Unj to be
In_rec_i (λX f ⇒ {f x |x ∈ X ∖ {0 } } ) of type
set → set .
Axiom. (
Unj_eq ) We take the following as an axiom:
∀X : set , Unj X = {Unj x |x ∈ X ∖ {0 } }
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:
Definition. We define
setsum to be
λX Y ⇒ {Inj0 x |x ∈ X } ∪ {Inj1 y |y ∈ Y } of type
set → set → set .
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_Inj_inv ) We take the following as an axiom:
∀X Y z : set , z ∈ X + Y → (∃x ∈ X , z = Inj0 x ) ∨ (∃y ∈ Y , z = Inj1 y )
Axiom. (
Subq_1_Sing0 ) We take the following as an axiom:
1 ⊆ {0 }
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
Definition. We define
proj0 to be
λZ ⇒ {Unj z |z ∈ Z , ∃x : set , Inj0 x = z } of type
set → set .
Definition. We define
proj1 to be
λZ ⇒ {Unj z |z ∈ Z , ∃y : set , Inj1 y = z } of type
set → set .
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:
∀w u : set , pair 0 u ∈ w → u ∈ proj0 w
Axiom. (
proj0E ) We take the following as an axiom:
∀w u : set , u ∈ proj0 w → pair 0 u ∈ w
Axiom. (
proj1I ) We take the following as an axiom:
∀w u : set , pair 1 u ∈ w → u ∈ proj1 w
Axiom. (
proj1E ) We take the following as an axiom:
∀w u : set , u ∈ proj1 w → pair 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 ⇒ ⋃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. (
proj_Sigma_eta ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀z ∈ (∑x ∈ X , Y x ) , pair (proj0 z ) (proj1 z ) = z
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 ).
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. (
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 : set → set , ∀x ∈ X , ∀y ∈ F x , (x ,y ) ∈ λx ∈ X ⇒ 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 : set → set → set , (∀x ∈ X , ∀y ∈ Y , F x y = G x y ) → {F (w 0 ) (w 1 ) |w ∈ X ⨯ Y } = {G (w 0 ) (w 1 ) |w ∈ X ⨯ Y }
Axiom. (
tuple_2_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀x ∈ X , ∀y ∈ Y x , (x ,y ) ∈ ∑x ∈ X , Y x
Axiom. (
tuple_2_setprod ) We take the following as an axiom:
∀X : set , ∀Y : set , ∀x ∈ X , ∀y ∈ Y , (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 .
Object . The name
DescrR_i_io_1 is a term of type
(set → (set → prop ) → prop ) → set .
Object . The name
DescrR_i_io_2 is a term of type
(set → (set → prop ) → prop ) → set → prop .
Axiom. (
DescrR_i_io_12 ) We take the following as an axiom:
∀R : set → (set → prop ) → prop , (∃x, (∃y : set → prop , R x y ) ∧ (∀y z : set → prop , R x y → R x z → y = z ) ) → R (DescrR_i_io_1 R ) (DescrR_i_io_2 R )
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:
Definition. We define
PNoLt_ to be
λalpha p q ⇒ ∃beta ∈ alpha , PNoEq_ beta p q ∧ ¬ p beta ∧ q beta of type
set → (set → prop ) → (set → prop ) → prop .
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:
Object . 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:
∀alpha beta, ∀p q : set → prop , alpha ∈ beta → PNoEq_ alpha p q → q alpha → PNoLt alpha p beta q
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:
Definition. We define
PNo_downc to be
λL alpha p ⇒ ∃beta, ordinal beta ∧ ∃q : set → prop , L beta q ∧ PNoLe alpha p beta q of type
(set → (set → prop ) → prop ) → set → (set → prop ) → prop .
Definition. We define
PNo_upc to be
λR alpha p ⇒ ∃beta, ordinal beta ∧ ∃q : set → prop , R beta q ∧ PNoLe beta q alpha p of type
(set → (set → prop ) → prop ) → set → (set → prop ) → prop .
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 .
Object . The name
PNo_bd is a term of type
(set → (set → prop ) → prop ) → (set → (set → prop ) → prop ) → set .
Object . 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
Let tag : set → set ≝ λalpha ⇒ SetAdjoin alpha {1 }
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:
Definition. We define
PSNo to be
λalpha p ⇒ {beta ∈ alpha |p beta } ∪ {beta ' |beta ∈ alpha , ¬ p beta } of type
set → (set → prop ) → set .
Axiom. (
PNoEq_PSNo ) We take the following as an axiom:
Axiom. (
SNo_PSNo ) We take the following as an axiom:
Object . The name
SNo is a term of type
set → prop .
Axiom. (
SNo_SNo ) We take the following as an axiom:
Object . 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:
∀x y, x < y → x ≤ y
Axiom. (
SNoLeE ) We take the following as an axiom:
∀x y, SNo x → SNo y → x ≤ y → x < y ∨ x = y
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:
∀x y z, SNo x → SNo y → SNo z → x < y → y < z → x < z
Axiom. (
SNoLe_ref ) We take the following as an axiom:
Axiom. (
SNoLe_antisym ) We take the following as an axiom:
∀x y, SNo x → SNo y → x ≤ y → y ≤ x → x = y
Axiom. (
SNoLtLe_tra ) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x < y → y ≤ z → x < z
Axiom. (
SNoLeLt_tra ) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x ≤ y → y < z → x < z
Axiom. (
SNoLe_tra ) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x ≤ y → y ≤ z → x ≤ z
Axiom. (
SNoLtLe_or ) We take the following as an axiom:
∀x y, SNo x → SNo y → x < y ∨ y ≤ x
Definition. We define
SNoCutP to be
λL R ⇒ (∀x ∈ L , SNo x ) ∧ (∀y ∈ R , SNo y ) ∧ (∀x ∈ L , ∀y ∈ R , x < y ) of type
set → set → prop .
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:
Definition. We define
SNoS_ to be
λalpha ⇒ {x ∈ 𝒫 (SNoElts_ alpha ) |∃beta ∈ alpha , SNo_ beta x } of type
set → set .
Axiom. (
SNoS_E ) We take the following as an axiom:
Beginning of Section TaggedSets2
Let tag : set → set ≝ λ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:
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:
Definition. We define
SNoL to be
λz ⇒ {x ∈ SNoS_ (SNoLev z ) |x < z } of type
set → set .
Definition. We define
SNoR to be
λz ⇒ {y ∈ SNoS_ (SNoLev z ) |z < y } of type
set → set .
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:
Definition. We define
eps_ to be
λn ⇒ {0 } ∪ {(ordsucc m ) ' |m ∈ n } of type
set → set .
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:
∀P : set → prop , (∀L R, SNoCutP L R → (∀x ∈ L , P x ) → (∀y ∈ R , P y ) → P (SNoCut L R ) ) → ∀z, SNo z → P z
Beginning of Section SurrealRecI
Variable F : set → (set → set ) → set
Let G : set → (set → set → set ) → set → set ≝ λalpha g ⇒ If_ii (ordinal alpha ) (λz : set ⇒ if z ∈ SNoS_ (ordsucc alpha ) then F z (λw ⇒ g (SNoLev w ) w ) else default ) (λz : set ⇒ default )
Object . 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 )
Object . 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 )
Let H : set → (set → set → set ) → set → set ≝ λw f z ⇒ if SNo z then SNo_rec_i (G w f ) z else Empty
Object . The name
SNo_rec2 is a term of type
set → set → set .
Hypothesis Fr : ∀w, SNo w → ∀z, SNo z → ∀g h : set → set → set , (∀x ∈ SNoS_ (SNoLev w ) , ∀y, SNo y → g x y = h x y ) → (∀y ∈ SNoS_ (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 : set → set → set , (∀x ∈ SNoS_ (SNoLev w ) , f x = k x ) → ∀z, SNo z → ∀g h : set → set , (∀u ∈ SNoS_ (SNoLev z ) , g u = h u ) → G w f z g = G w k z h
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:
∀P : set → prop , (∀x, SNo x → (∀w ∈ SNoS_ (SNoLev x ) , P w ) → P x ) → (∀x, SNo x → P x )
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:
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:
Axiom. (
restr_SNo ) We take the following as an axiom:
Axiom. (
restr_SNoEq ) We take the following as an axiom:
Beginning of Section SurrealMinus
Object . 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
Part 5
Beginning of Section SurrealAdd
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 .
Proof: Set F to be the term
λx y a ⇒ SNoCut ({a w y |w ∈ SNoL x } ∪ {a x w |w ∈ SNoL y } ) ({a z y |z ∈ SNoR x } ∪ {a x z |z ∈ SNoR y } ) of type
set → set → (set → set → set ) → set .
We prove the intermediate
claim L1 :
∀x, SNo x → ∀y, SNo y → ∀g h : set → set → set , (∀w ∈ SNoS_ (SNoLev x ) , ∀z, SNo z → g w z = h w z ) → (∀z ∈ SNoS_ (SNoLev y ) , g x z = h x z ) → F x y g = F x y h .
Let x be given.
Let y be given.
Let g and h be given.
We will prove F x y g = F x y h .
We prove the intermediate
claim L1a :
{g w y |w ∈ SNoL x } = {h w y |w ∈ SNoL x } .
Let w be given.
We will prove g w y = h w y .
Apply Hgh1 to the current goal.
An
exact proof term for the current goal is
SNoL_SNoS x Hx w Hw .
An exact proof term for the current goal is Hy .
We prove the intermediate
claim L1b :
{g x w |w ∈ SNoL y } = {h x w |w ∈ SNoL y } .
Let w be given.
We will prove g x w = h x w .
Apply Hgh2 to the current goal.
An
exact proof term for the current goal is
SNoL_SNoS y Hy w Hw .
We prove the intermediate
claim L1c :
{g z y |z ∈ SNoR x } = {h z y |z ∈ SNoR x } .
Let z be given.
We will prove g z y = h z y .
Apply Hgh1 to the current goal.
An
exact proof term for the current goal is
SNoR_SNoS x Hx z Hz .
An exact proof term for the current goal is Hy .
We prove the intermediate
claim L1d :
{g x z |z ∈ SNoR y } = {h x z |z ∈ SNoR y } .
Let z be given.
We will prove g x z = h x z .
Apply Hgh2 to the current goal.
An
exact proof term for the current goal is
SNoR_SNoS y Hy z Hz .
rewrite the current goal using L1a (from left to right).
rewrite the current goal using L1b (from left to right).
rewrite the current goal using L1c (from left to right).
rewrite the current goal using L1d (from left to right).
Use reflexivity.
An
exact proof term for the current goal is
SNo_rec2_eq F L1 .
∎
Proof: Set P to be the term
λx y ⇒ SNo (x + y ) ∧ (∀u ∈ SNoL x , u + y < x + y ) ∧ (∀u ∈ SNoR x , x + y < u + y ) ∧ (∀u ∈ SNoL y , x + u < x + y ) ∧ (∀u ∈ SNoR y , x + y < x + u ) ∧ SNoCutP ({w + y |w ∈ SNoL x } ∪ {x + w |w ∈ SNoL y } ) ({z + y |z ∈ SNoR x } ∪ {x + z |z ∈ SNoR y } ) of type
set → set → prop .
We prove the intermediate
claim LPE :
∀x y, P x y → ∀p : prop , (SNo (x + y ) → (∀u ∈ SNoL x , u + y < x + y ) → (∀u ∈ SNoR x , x + y < u + y ) → (∀u ∈ SNoL y , x + u < x + y ) → (∀u ∈ SNoR y , x + y < x + u ) → p ) → p .
Let x and y be given.
Assume Hxy .
Let p be given.
Assume Hp .
Apply Hxy to the current goal.
Assume H .
Apply H to the current goal.
Assume H .
Apply H to the current goal.
Assume H .
Apply H to the current goal.
Assume H .
Apply H to the current goal.
Assume H1 H2 H3 H4 H5 _ .
An exact proof term for the current goal is Hp H1 H2 H3 H4 H5 .
We will
prove ∀x y, SNo x → SNo y → P x y .
Let x and y be given.
Set L1 to be the term
{w + y |w ∈ SNoL x } .
Set L2 to be the term
{x + w |w ∈ SNoL y } .
Set L to be the term L1 ∪ L2 .
Set R1 to be the term
{z + y |z ∈ SNoR x } .
Set R2 to be the term
{x + z |z ∈ SNoR y } .
Set R to be the term R1 ∪ R2 .
We prove the intermediate
claim IHLx :
∀w ∈ SNoL x , P w y .
Let w be given.
Apply SNoL_E x Hx w Hw to the current goal.
Assume Hw3 : w < x .
We prove the intermediate
claim Lw :
w ∈ SNoS_ (SNoLev x ) .
An
exact proof term for the current goal is
SNoS_I2 w x Hw1 Hx Hw2 .
An exact proof term for the current goal is IHx w Lw .
We prove the intermediate
claim IHRx :
∀w ∈ SNoR x , P w y .
Let w be given.
Apply SNoR_E x Hx w Hw to the current goal.
Assume Hw3 : x < w .
We prove the intermediate
claim Lw :
w ∈ SNoS_ (SNoLev x ) .
An
exact proof term for the current goal is
SNoS_I2 w x Hw1 Hx Hw2 .
An exact proof term for the current goal is IHx w Lw .
We prove the intermediate
claim IHLy :
∀w ∈ SNoL y , P x w .
Let w be given.
Apply SNoL_E y Hy w Hw to the current goal.
Assume Hw3 : w < y .
We prove the intermediate
claim Lw :
w ∈ SNoS_ (SNoLev y ) .
An
exact proof term for the current goal is
SNoS_I2 w y Hw1 Hy Hw2 .
An exact proof term for the current goal is IHy w Lw .
We prove the intermediate
claim IHRy :
∀w ∈ SNoR y , P x w .
Let w be given.
Apply SNoR_E y Hy w Hw to the current goal.
Assume Hw3 : y < w .
We prove the intermediate
claim Lw :
w ∈ SNoS_ (SNoLev y ) .
An
exact proof term for the current goal is
SNoS_I2 w y Hw1 Hy Hw2 .
An exact proof term for the current goal is IHy w Lw .
We prove the intermediate
claim LLR :
SNoCutP L R .
We will
prove (∀w ∈ L , SNo w ) ∧ (∀z ∈ R , SNo z ) ∧ (∀w ∈ L , ∀z ∈ R , w < z ) .
Apply and3I to the current goal.
Let w be given.
Assume Hw : w ∈ L1 ∪ L2 .
Apply binunionE L1 L2 w Hw to the current goal.
Let z be given.
Assume Hwz : w = z + y .
Apply LPE z y (IHLx z Hz ) to the current goal.
Assume _ _ _ _ .
rewrite the current goal using Hwz (from left to right).
An exact proof term for the current goal is H2 .
Let z be given.
Assume Hwz : w = x + z .
Apply LPE x z (IHLy z Hz ) to the current goal.
Assume _ _ _ _ .
rewrite the current goal using Hwz (from left to right).
An exact proof term for the current goal is H2 .
Let w be given.
Assume Hw : w ∈ R1 ∪ R2 .
Apply binunionE R1 R2 w Hw to the current goal.
Let z be given.
Assume Hwz : w = z + y .
Apply LPE z y (IHRx z Hz ) to the current goal.
Assume _ _ _ _ .
rewrite the current goal using Hwz (from left to right).
An exact proof term for the current goal is H2 .
Let z be given.
Assume Hwz : w = x + z .
Apply LPE x z (IHRy z Hz ) to the current goal.
Assume _ _ _ _ .
rewrite the current goal using Hwz (from left to right).
An exact proof term for the current goal is H2 .
Let w be given.
Assume Hw : w ∈ L .
Let z be given.
Assume Hz : z ∈ R .
We will prove w < z .
Apply binunionE L1 L2 w Hw to the current goal.
Let u be given.
Assume Hwu : w = u + y .
Apply SNoL_E x Hx u Hu to the current goal.
Assume Hu3 : u < x .
We prove the intermediate
claim Lux :
u ∈ SNoS_ (SNoLev x ) .
An
exact proof term for the current goal is
SNoS_I2 u x Hu1 Hx Hu2 .
Apply LPE u y (IHLx u Hu ) to the current goal.
We will prove w < z .
rewrite the current goal using Hwu (from left to right).
We will prove u + y < z .
Apply binunionE R1 R2 z Hz to the current goal.
Let v be given.
Assume Hzv : z = v + y .
Apply SNoR_E x Hx v Hv to the current goal.
Assume Hv3 : x < v .
Apply LPE v y (IHRx v Hv ) to the current goal.
rewrite the current goal using Hzv (from left to right).
We will prove u + y < v + y .
We prove the intermediate claim Luv : u < v .
An
exact proof term for the current goal is
SNoLt_tra u x v Hu1 Hx Hv1 Hu3 Hv3 .
Apply SNoLtE u v Hu1 Hv1 Luv to the current goal.
Let q be given.
Assume _ _ .
Assume Hq5 : u < q .
Assume Hq6 : q < v .
Assume _ _ .
Assume Hq2u Hq2v .
An
exact proof term for the current goal is
LLxa (SNoLev u ) Hu2 (SNoLev q ) Hq2u .
We prove the intermediate
claim Lqx2 :
q ∈ SNoS_ (SNoLev x ) .
An
exact proof term for the current goal is
SNoS_I2 q x Hq1 Hx Lqx .
We prove the intermediate
claim Lqy :
SNo (q + y ) .
Apply LPE q y (IHx q Lqx2 ) to the current goal.
Assume IHq1 _ _ _ _ .
An exact proof term for the current goal is IHq1 .
Apply SNoLt_tra (u + y ) (q + y ) (v + y ) IHu1 Lqy IHv1 to the current goal.
We will prove u + y < q + y .
Apply IHu3 to the current goal.
We will
prove q ∈ SNoR u .
An
exact proof term for the current goal is
SNoR_I u Hu1 q Hq1 Hq2u Hq5 .
We will prove q + y < v + y .
Apply IHv2 to the current goal.
We will
prove q ∈ SNoL v .
An
exact proof term for the current goal is
SNoL_I v Hv1 q Hq1 Hq2v Hq6 .
Assume _ _ .
We will prove u + y < v + y .
Apply IHv2 to the current goal.
We will
prove u ∈ SNoL v .
An
exact proof term for the current goal is
SNoL_I v Hv1 u Hu1 Huv Luv .
Assume _ _ .
We will prove u + y < v + y .
Apply IHu3 to the current goal.
We will
prove v ∈ SNoR u .
An
exact proof term for the current goal is
SNoR_I u Hu1 v Hv1 Hvu Luv .
Let v be given.
Assume Hzv : z = x + v .
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hv3 : y < v .
We prove the intermediate
claim Lvy :
v ∈ SNoS_ (SNoLev y ) .
An
exact proof term for the current goal is
SNoS_I2 v y Hv1 Hy Hv2 .
Apply LPE x v (IHRy v Hv ) to the current goal.
rewrite the current goal using Hzv (from left to right).
We will prove u + y < x + v .
Apply LPE u v (IHxy u Lux v Lvy ) to the current goal.
Assume _ _ _ _ .
We will prove u + y < x + v .
Apply SNoLt_tra (u + y ) (u + v ) (x + v ) IHu1 IHuv1 IHv1 to the current goal.
We will prove u + y < u + v .
Apply IHu5 to the current goal.
We will
prove v ∈ SNoR y .
An
exact proof term for the current goal is
SNoR_I y Hy v Hv1 Hv2 Hv3 .
We will prove u + v < x + v .
Apply IHv2 to the current goal.
We will
prove u ∈ SNoL x .
An
exact proof term for the current goal is
SNoL_I x Hx u Hu1 Hu2 Hu3 .
Let u be given.
Assume Hwu : w = x + u .
Apply SNoL_E y Hy u Hu to the current goal.
Assume Hu3 : u < y .
We prove the intermediate
claim Luy :
u ∈ SNoS_ (SNoLev y ) .
An
exact proof term for the current goal is
SNoS_I2 u y Hu1 Hy Hu2 .
Apply LPE x u (IHLy u Hu ) to the current goal.
We will prove w < z .
rewrite the current goal using Hwu (from left to right).
We will prove x + u < z .
Apply binunionE R1 R2 z Hz to the current goal.
Let v be given.
Assume Hzv : z = v + y .
Apply SNoR_E x Hx v Hv to the current goal.
Assume Hv3 : x < v .
We prove the intermediate
claim Lvx :
v ∈ SNoS_ (SNoLev x ) .
An
exact proof term for the current goal is
SNoS_I2 v x Hv1 Hx Hv2 .
Apply LPE v y (IHRx v Hv ) to the current goal.
rewrite the current goal using Hzv (from left to right).
We will prove x + u < v + y .
Apply LPE v u (IHxy v Lvx u Luy ) to the current goal.
Assume _ _ _ _ .
We will prove x + u < v + y .
Apply SNoLt_tra (x + u ) (v + u ) (v + y ) IHu1 IHvu1 IHv1 to the current goal.
We will prove x + u < v + u .
Apply IHu3 to the current goal.
We will
prove v ∈ SNoR x .
An
exact proof term for the current goal is
SNoR_I x Hx v Hv1 Hv2 Hv3 .
We will prove v + u < v + y .
Apply IHv4 to the current goal.
We will
prove u ∈ SNoL y .
An
exact proof term for the current goal is
SNoL_I y Hy u Hu1 Hu2 Hu3 .
Let v be given.
Assume Hzv : z = x + v .
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hv3 : y < v .
Apply LPE x v (IHRy v Hv ) to the current goal.
rewrite the current goal using Hzv (from left to right).
We will prove x + u < x + v .
We prove the intermediate claim Luv : u < v .
An
exact proof term for the current goal is
SNoLt_tra u y v Hu1 Hy Hv1 Hu3 Hv3 .
Apply SNoLtE u v Hu1 Hv1 Luv to the current goal.
Let q be given.
Assume _ _ .
Assume Hq5 : u < q .
Assume Hq6 : q < v .
Assume _ _ .
Assume Hq2u Hq2v .
An
exact proof term for the current goal is
LLya (SNoLev v ) Hv2 (SNoLev q ) Hq2v .
We prove the intermediate
claim Lqy2 :
q ∈ SNoS_ (SNoLev y ) .
An
exact proof term for the current goal is
SNoS_I2 q y Hq1 Hy Lqy .
We prove the intermediate
claim Lxq :
SNo (x + q ) .
Apply LPE x q (IHy q Lqy2 ) to the current goal.
Assume IHq1 _ _ _ _ .
An exact proof term for the current goal is IHq1 .
We will prove x + u < x + v .
Apply SNoLt_tra (x + u ) (x + q ) (x + v ) IHu1 Lxq IHv1 to the current goal.
We will prove x + u < x + q .
Apply IHu5 to the current goal.
We will
prove q ∈ SNoR u .
An
exact proof term for the current goal is
SNoR_I u Hu1 q Hq1 Hq2u Hq5 .
We will prove x + q < x + v .
Apply IHv4 to the current goal.
We will
prove q ∈ SNoL v .
An
exact proof term for the current goal is
SNoL_I v Hv1 q Hq1 Hq2v Hq6 .
Assume _ _ .
We will prove x + u < x + v .
Apply IHv4 to the current goal.
We will
prove u ∈ SNoL v .
An
exact proof term for the current goal is
SNoL_I v Hv1 u Hu1 Huv Luv .
Assume _ _ .
We will prove x + u < x + v .
Apply IHu5 to the current goal.
We will
prove v ∈ SNoR u .
An
exact proof term for the current goal is
SNoR_I u Hu1 v Hv1 Hvu Luv .
We will prove P x y .
We will
prove SNo (x + y ) ∧ (∀u ∈ SNoL x , u + y < x + y ) ∧ (∀u ∈ SNoR x , x + y < u + y ) ∧ (∀u ∈ SNoL y , x + u < x + y ) ∧ (∀u ∈ SNoR y , x + y < x + u ) ∧ SNoCutP L R .
We prove the intermediate
claim LNLR :
SNo (SNoCut L R ) .
Apply andI to the current goal.
rewrite the current goal using
add_SNo_eq x Hx y Hy (from left to right).
Apply and5I to the current goal.
An exact proof term for the current goal is LNLR .
Let u be given.
We will
prove u + y < SNoCut L R .
Apply SNoL_E x Hx u Hu to the current goal.
Assume Hu3 : u < x .
We prove the intermediate claim LuyL : u + y ∈ L .
We will prove u + y ∈ L1 ∪ L2 .
We will
prove u + y ∈ {w + y |w ∈ SNoL x } .
Apply ReplI (SNoL x ) (λw ⇒ w + y ) u to the current goal.
We will
prove u ∈ SNoL x .
An exact proof term for the current goal is Hu .
We will
prove u + y < SNoCut L R .
An
exact proof term for the current goal is
SNoCutP_SNoCut_L L R LLR (u + y ) LuyL .
Let u be given.
We will
prove SNoCut L R < u + y .
Apply SNoR_E x Hx u Hu to the current goal.
Assume Hu3 : x < u .
We prove the intermediate claim LuyR : u + y ∈ R .
We will prove u + y ∈ R1 ∪ R2 .
We will
prove u + y ∈ {z + y |z ∈ SNoR x } .
Apply ReplI (SNoR x ) (λw ⇒ w + y ) u to the current goal.
We will
prove u ∈ SNoR x .
An exact proof term for the current goal is Hu .
We will
prove SNoCut L R < u + y .
An
exact proof term for the current goal is
SNoCutP_SNoCut_R L R LLR (u + y ) LuyR .
Let u be given.
We will
prove x + u < SNoCut L R .
Apply SNoL_E y Hy u Hu to the current goal.
Assume Hu3 : u < y .
We prove the intermediate claim LxuL : x + u ∈ L .
We will prove x + u ∈ L1 ∪ L2 .
We will
prove x + u ∈ {x + w |w ∈ SNoL y } .
Apply ReplI (SNoL y ) (λw ⇒ x + w ) u to the current goal.
We will
prove u ∈ SNoL y .
An exact proof term for the current goal is Hu .
We will
prove x + u < SNoCut L R .
An
exact proof term for the current goal is
SNoCutP_SNoCut_L L R LLR (x + u ) LxuL .
Let u be given.
We will
prove SNoCut L R < x + u .
Apply SNoR_E y Hy u Hu to the current goal.
Assume Hu3 : y < u .
We prove the intermediate claim LxuR : x + u ∈ R .
We will prove x + u ∈ R1 ∪ R2 .
We will
prove x + u ∈ {x + z |z ∈ SNoR y } .
Apply ReplI (SNoR y ) (λz ⇒ x + z ) u to the current goal.
We will
prove u ∈ SNoR y .
An exact proof term for the current goal is Hu .
We will
prove SNoCut L R < x + u .
An
exact proof term for the current goal is
SNoCutP_SNoCut_R L R LLR (x + u ) LxuR .
An exact proof term for the current goal is LLR .
∎
Proof: Let x and y be given.
Assume H .
Apply H to the current goal.
Assume H .
Apply H to the current goal.
Assume H .
Apply H to the current goal.
Assume H .
Apply H to the current goal.
Assume H _ _ _ _ _ .
An exact proof term for the current goal is H .
∎
Proof: Let x, y and z be given.
Assume Hx Hy Hz .
An exact proof term for the current goal is Hx .
An exact proof term for the current goal is Hy .
An exact proof term for the current goal is Hz .
∎
Proof: Let x, y and z be given.
Assume Hx Hy Hz .
An exact proof term for the current goal is Hx .
An exact proof term for the current goal is Hy .
An exact proof term for the current goal is Hz .
∎
Proof: Let x, y, z and w be given.
Assume Hx Hy Hz Hw .
∎
Theorem. (
add_SNo_Lt1 ) The following is provable:
∀x y z, SNo x → SNo y → SNo z → x < z → x + y < z + y
Proof: Let x, y and z be given.
Assume Hxz : x < z .
Assume H .
Apply H to the current goal.
Assume H .
Apply H to the current goal.
Assume H .
Apply H to the current goal.
Assume H .
Apply H to the current goal.
Assume _ .
Assume _ _ _ .
Assume H .
Apply H to the current goal.
Assume H .
Apply H to the current goal.
Assume H .
Apply H to the current goal.
Assume H .
Apply H to the current goal.
Assume _ _ _ _ .
Apply SNoLtE x z Hx Hz Hxz to the current goal.
Let w be given.
Assume _ _ .
Assume Hw5 : x < w .
Assume Hw6 : w < z .
Assume _ _ .
Assume Hw2x Hw2z .
We will prove x + y < z + y .
We will prove x + y < w + y .
Apply H2 to the current goal.
We will
prove w ∈ SNoR x .
Apply SNoR_I x Hx w Hw1 to the current goal.
An exact proof term for the current goal is Hw2x .
We will prove x < w .
An exact proof term for the current goal is Hw5 .
We will prove w + y < z + y .
Apply H4 to the current goal.
We will
prove w ∈ SNoL z .
Apply SNoL_I z Hz w Hw1 to the current goal.
An exact proof term for the current goal is Hw2z .
We will prove w < z .
An exact proof term for the current goal is Hw6 .
Assume _ _ .
We will prove x + y < z + y .
Apply H4 to the current goal.
We will
prove x ∈ SNoL z .
Apply SNoL_I z Hz x Hx to the current goal.
An exact proof term for the current goal is Hxz1 .
We will prove x < z .
An exact proof term for the current goal is Hxz .
Assume _ _ .
We will prove x + y < z + y .
Apply H2 to the current goal.
We will
prove z ∈ SNoR x .
Apply SNoR_I x Hx z Hz to the current goal.
An exact proof term for the current goal is Hzx .
We will prove x < z .
An exact proof term for the current goal is Hxz .
∎
Theorem. (
add_SNo_Le1 ) The following is provable:
∀x y z, SNo x → SNo y → SNo z → x ≤ z → x + y ≤ z + y
Proof: Let x, y and z be given.
Assume Hxz : x ≤ z .
We will prove x + y ≤ z + y .
Apply SNoLeE x z Hx Hz Hxz to the current goal.
Assume H1 : x < z .
An
exact proof term for the current goal is
add_SNo_Lt1 x y z Hx Hy Hz H1 .
Assume H1 : x = z .
rewrite the current goal using H1 (from left to right).
∎
Theorem. (
add_SNo_Lt2 ) The following is provable:
∀x y z, SNo x → SNo y → SNo z → y < z → x + y < x + z
Proof: Let x, y and z be given.
Assume Hyz : y < z .
Assume H .
Apply H to the current goal.
Assume H .
Apply H to the current goal.
Assume H .
Apply H to the current goal.
Assume H .
Apply H to the current goal.
Assume _ _ _ .
Assume _ .
Assume H .
Apply H to the current goal.
Assume H .
Apply H to the current goal.
Assume H .
Apply H to the current goal.
Assume H .
Apply H to the current goal.
Assume _ _ .
Assume _ _ .
Apply SNoLtE y z Hy Hz Hyz to the current goal.
Let w be given.
Assume _ _ .
Assume Hw5 : y < w .
Assume Hw6 : w < z .
Assume _ _ .
Assume Hw2y Hw2z .
We will prove x + y < x + z .
We will prove x + y < x + w .
Apply H2 to the current goal.
We will
prove w ∈ SNoR y .
Apply SNoR_I y Hy w Hw1 to the current goal.
An exact proof term for the current goal is Hw2y .
We will prove y < w .
An exact proof term for the current goal is Hw5 .
We will prove x + w < x + z .
Apply H4 to the current goal.
We will
prove w ∈ SNoL z .
Apply SNoL_I z Hz w Hw1 to the current goal.
An exact proof term for the current goal is Hw2z .
We will prove w < z .
An exact proof term for the current goal is Hw6 .
Assume _ _ .
We will prove x + y < x + z .
Apply H4 to the current goal.
We will
prove y ∈ SNoL z .
Apply SNoL_I z Hz y Hy to the current goal.
An exact proof term for the current goal is Hyz1 .
We will prove y < z .
An exact proof term for the current goal is Hyz .
Assume _ _ .
We will prove x + y < x + z .
Apply H2 to the current goal.
We will
prove z ∈ SNoR y .
Apply SNoR_I y Hy z Hz to the current goal.
An exact proof term for the current goal is Hzy .
We will prove y < z .
An exact proof term for the current goal is Hyz .
∎
Theorem. (
add_SNo_Le2 ) The following is provable:
∀x y z, SNo x → SNo y → SNo z → y ≤ z → x + y ≤ x + z
Proof: Let x, y and z be given.
Assume Hyz : y ≤ z .
We will prove x + y ≤ x + z .
Apply SNoLeE y z Hy Hz Hyz to the current goal.
Assume H1 : y < z .
An
exact proof term for the current goal is
add_SNo_Lt2 x y z Hx Hy Hz H1 .
Assume H1 : y = z .
rewrite the current goal using H1 (from left to right).
∎
Theorem. (
add_SNo_Lt3a ) The following is provable:
∀x y z w, SNo x → SNo y → SNo z → SNo w → x < z → y ≤ w → x + y < z + w
Proof: Let x, y, z and w be given.
Assume Hxz : x < z .
Assume Hyw : y ≤ w .
We will prove x + y < z + y .
An
exact proof term for the current goal is
add_SNo_Lt1 x y z Hx Hy Hz Hxz .
We will prove z + y ≤ z + w .
An
exact proof term for the current goal is
add_SNo_Le2 z y w Hz Hy Hw Hyw .
∎
Theorem. (
add_SNo_Lt3b ) The following is provable:
∀x y z w, SNo x → SNo y → SNo z → SNo w → x ≤ z → y < w → x + y < z + w
Proof: Let x, y, z and w be given.
Assume Hxz : x ≤ z .
Assume Hyw : y < w .
We will prove x + y ≤ z + y .
An
exact proof term for the current goal is
add_SNo_Le1 x y z Hx Hy Hz Hxz .
We will prove z + y < z + w .
An
exact proof term for the current goal is
add_SNo_Lt2 z y w Hz Hy Hw Hyw .
∎
Theorem. (
add_SNo_Lt3 ) The following is provable:
∀x y z w, SNo x → SNo y → SNo z → SNo w → x < z → y < w → x + y < z + w
Proof: Let x, y, z and w be given.
Assume Hxz : x < z .
Assume Hyw : y < w .
Apply add_SNo_Lt3a x y z w Hx Hy Hz Hw Hxz to the current goal.
We will prove y ≤ w .
We will prove y < w .
An exact proof term for the current goal is Hyw .
∎
Theorem. (
add_SNo_Le3 ) The following is provable:
∀x y z w, SNo x → SNo y → SNo z → SNo w → x ≤ z → y ≤ w → x + y ≤ z + w
Proof: Let x, y, z and w be given.
Assume Hxz : x ≤ z .
Assume Hyw : y ≤ w .
We will prove x + y ≤ z + y .
An
exact proof term for the current goal is
add_SNo_Le1 x y z Hx Hy Hz Hxz .
We will prove z + y ≤ z + w .
An
exact proof term for the current goal is
add_SNo_Le2 z y w Hz Hy Hw Hyw .
∎
Proof: Let x and y be given.
Assume _ H .
An exact proof term for the current goal is H .
∎
Theorem. (
add_SNo_com ) The following is provable:
∀x y, SNo x → SNo y → x + y = y + x
Proof:
Let x and y be given.
We prove the intermediate
claim IHLx :
∀w ∈ SNoL x , w + y = y + w .
Let w be given.
Apply SNoL_E x Hx w Hw to the current goal.
Assume Hw3 : w < x .
We prove the intermediate
claim Lw :
w ∈ SNoS_ (SNoLev x ) .
An
exact proof term for the current goal is
SNoS_I2 w x Hw1 Hx Hw2 .
An exact proof term for the current goal is IHx w Lw .
We prove the intermediate
claim IHRx :
∀w ∈ SNoR x , w + y = y + w .
Let w be given.
Apply SNoR_E x Hx w Hw to the current goal.
Assume Hw3 : x < w .
We prove the intermediate
claim Lw :
w ∈ SNoS_ (SNoLev x ) .
An
exact proof term for the current goal is
SNoS_I2 w x Hw1 Hx Hw2 .
An exact proof term for the current goal is IHx w Lw .
We prove the intermediate
claim IHLy :
∀w ∈ SNoL y , x + w = w + x .
Let w be given.
Apply SNoL_E y Hy w Hw to the current goal.
Assume Hw3 : w < y .
We prove the intermediate
claim Lw :
w ∈ SNoS_ (SNoLev y ) .
An
exact proof term for the current goal is
SNoS_I2 w y Hw1 Hy Hw2 .
An exact proof term for the current goal is IHy w Lw .
We prove the intermediate
claim IHRy :
∀w ∈ SNoR y , x + w = w + x .
Let w be given.
Apply SNoR_E y Hy w Hw to the current goal.
Assume Hw3 : y < w .
We prove the intermediate
claim Lw :
w ∈ SNoS_ (SNoLev y ) .
An
exact proof term for the current goal is
SNoS_I2 w y Hw1 Hy Hw2 .
An exact proof term for the current goal is IHy w Lw .
We will prove x + y = y + x .
Set Lxy1 to be the term
{w + y |w ∈ SNoL x } .
Set Lxy2 to be the term
{x + w |w ∈ SNoL y } .
Set Rxy1 to be the term
{z + y |z ∈ SNoR x } .
Set Rxy2 to be the term
{x + z |z ∈ SNoR y } .
rewrite the current goal using
add_SNo_eq x Hx y Hy (from left to right).
We will
prove (SNoCut (Lxy1 ∪ Lxy2 ) (Rxy1 ∪ Rxy2 ) ) = y + x .
Set Lyx1 to be the term
{w + x |w ∈ SNoL y } .
Set Lyx2 to be the term
{y + w |w ∈ SNoL x } .
Set Ryx1 to be the term
{z + x |z ∈ SNoR y } .
Set Ryx2 to be the term
{y + z |z ∈ SNoR x } .
rewrite the current goal using
add_SNo_eq y Hy x Hx (from left to right).
We will
prove (SNoCut (Lxy1 ∪ Lxy2 ) (Rxy1 ∪ Rxy2 ) ) = (SNoCut (Lyx1 ∪ Lyx2 ) (Ryx1 ∪ Ryx2 ) ) .
We prove the intermediate claim Lxy1yx2 : Lxy1 = Lyx2 .
We will
prove {w + y |w ∈ SNoL x } = {y + w |w ∈ SNoL x } .
Apply ReplEq_ext (SNoL x ) (λw ⇒ w + y ) (λw ⇒ y + w ) to the current goal.
Let w be given.
We will prove w + y = y + w .
An exact proof term for the current goal is IHLx w Hw .
We prove the intermediate claim Lxy2yx1 : Lxy2 = Lyx1 .
We will
prove {x + w |w ∈ SNoL y } = {w + x |w ∈ SNoL y } .
Apply ReplEq_ext (SNoL y ) (λw ⇒ x + w ) (λw ⇒ w + x ) to the current goal.
Let w be given.
We will prove x + w = w + x .
An exact proof term for the current goal is IHLy w Hw .
We prove the intermediate claim Rxy1yx2 : Rxy1 = Ryx2 .
We will
prove {w + y |w ∈ SNoR x } = {y + w |w ∈ SNoR x } .
Apply ReplEq_ext (SNoR x ) (λw ⇒ w + y ) (λw ⇒ y + w ) to the current goal.
Let w be given.
We will prove w + y = y + w .
An exact proof term for the current goal is IHRx w Hw .
We prove the intermediate claim Rxy2yx1 : Rxy2 = Ryx1 .
We will
prove {x + w |w ∈ SNoR y } = {w + x |w ∈ SNoR y } .
Apply ReplEq_ext (SNoR y ) (λw ⇒ x + w ) (λw ⇒ w + x ) to the current goal.
Let w be given.
We will prove x + w = w + x .
An exact proof term for the current goal is IHRy w Hw .
rewrite the current goal using Lxy1yx2 (from left to right).
rewrite the current goal using Lxy2yx1 (from left to right).
rewrite the current goal using Rxy1yx2 (from left to right).
rewrite the current goal using Rxy2yx1 (from left to right).
We will
prove (SNoCut (Lyx2 ∪ Lyx1 ) (Ryx2 ∪ Ryx1 ) ) = (SNoCut (Lyx1 ∪ Lyx2 ) (Ryx1 ∪ Ryx2 ) ) .
rewrite the current goal using
binunion_com Lyx2 Lyx1 (from left to right).
rewrite the current goal using
binunion_com Ryx2 Ryx1 (from left to right).
Use reflexivity.
∎
Proof:
Let x be given.
We will prove 0 + x = x .
rewrite the current goal using
add_SNo_eq 0 SNo_0 x Hx (from left to right).
We prove the intermediate
claim L1 :
{w + x |w ∈ SNoL 0 } ∪ {0 + w |w ∈ SNoL x } = SNoL x .
rewrite the current goal using
SNoL_0 (from left to right).
rewrite the current goal using
Repl_Empty (λw ⇒ w + x ) (from left to right).
rewrite the current goal using
binunion_idl (from left to right).
We will
prove {0 + w |w ∈ SNoL x } = SNoL x .
Let u be given.
Let w be given.
Assume H1 : u = 0 + w .
We will
prove u ∈ SNoL x .
rewrite the current goal using H1 (from left to right).
We will
prove 0 + w ∈ SNoL x .
rewrite the current goal using
IH w (SNoL_SNoS_ x w Hw ) (from left to right).
We will
prove w ∈ SNoL x .
An exact proof term for the current goal is Hw .
Let u be given.
We will
prove u ∈ {0 + w |w ∈ SNoL x } .
rewrite the current goal using
IH u (SNoL_SNoS_ x u Hu ) (from right to left).
We will
prove 0 + u ∈ {0 + w |w ∈ SNoL x } .
An
exact proof term for the current goal is
ReplI (SNoL x ) (λw ⇒ 0 + w ) u Hu .
We prove the intermediate
claim L2 :
{w + x |w ∈ SNoR 0 } ∪ {0 + w |w ∈ SNoR x } = SNoR x .
rewrite the current goal using
SNoR_0 (from left to right).
rewrite the current goal using
Repl_Empty (λw ⇒ w + x ) (from left to right).
rewrite the current goal using
binunion_idl (from left to right).
We will
prove {0 + w |w ∈ SNoR x } = SNoR x .
Let u be given.
Let w be given.
Assume H1 : u = 0 + w .
We will
prove u ∈ SNoR x .
rewrite the current goal using H1 (from left to right).
We will
prove 0 + w ∈ SNoR x .
rewrite the current goal using
IH w (SNoR_SNoS_ x w Hw ) (from left to right).
We will
prove w ∈ SNoR x .
An exact proof term for the current goal is Hw .
Let u be given.
We will
prove u ∈ {0 + w |w ∈ SNoR x } .
rewrite the current goal using
IH u (SNoR_SNoS_ x u Hu ) (from right to left).
We will
prove 0 + u ∈ {0 + w |w ∈ SNoR x } .
An
exact proof term for the current goal is
ReplI (SNoR x ) (λw ⇒ 0 + w ) u Hu .
rewrite the current goal using L1 (from left to right).
rewrite the current goal using L2 (from left to right).
Use symmetry.
An
exact proof term for the current goal is
SNo_eta x Hx .
∎
Proof: Let x be given.
An
exact proof term for the current goal is
add_SNo_0L x Hx .
∎
Proof:
Let x be given.
We will prove - x + x = 0 .
We prove the intermediate
claim Lmx :
SNo (- x ) .
Set L1 to be the term
{w + x |w ∈ SNoL (- x ) } .
Set L2 to be the term
{- x + w |w ∈ SNoL x } .
Set R1 to be the term
{z + x |z ∈ SNoR (- x ) } .
Set R2 to be the term
{- x + z |z ∈ SNoR x } .
Set L to be the term L1 ∪ L2 .
Set R to be the term R1 ∪ R2 .
rewrite the current goal using
add_SNo_eq (- x ) Lmx x Hx (from left to right).
We prove the intermediate
claim LLR :
SNoCutP L R .
An
exact proof term for the current goal is
add_SNo_SNoCutP (- x ) x Lmx Hx .
We prove the intermediate
claim LNLR :
SNo (SNoCut L R ) .
We will prove ∀w ∈ L , w < 0 .
Let w be given.
Assume Hw : w ∈ L .
Apply binunionE L1 L2 w Hw to the current goal.
Let u be given.
Assume Hwu : w = u + x .
Apply SNoL_E (- x ) Lmx u Hu to the current goal.
Assume Hu3 : u < - x .
We prove the intermediate
claim Lmu :
SNo (- u ) .
An exact proof term for the current goal is Hu1 .
We prove the intermediate claim Lmuu : - u + u = 0 .
Apply IH to the current goal.
Apply SNoS_I2 u x Hu1 Hx to the current goal.
rewrite the current goal using
minus_SNo_Lev x Hx (from right to left).
An exact proof term for the current goal is Hu2 .
We prove the intermediate claim Lxmu : x < - u .
We will prove - - x < - u .
We will prove u < - x .
An exact proof term for the current goal is Hu3 .
We will prove w < 0 .
rewrite the current goal using Hwu (from left to right).
We will prove u + x < 0 .
rewrite the current goal using
add_SNo_com u x Hu1 Hx (from left to right).
We will prove x + u < 0 .
rewrite the current goal using Lmuu (from right to left).
We will prove x + u < - u + u .
Apply add_SNo_Lt1 x u (- u ) Hx Hu1 Lmu to the current goal.
We will prove x < - u .
An exact proof term for the current goal is Lxmu .
Let u be given.
Assume Hwu : w = - x + u .
Apply SNoL_E x Hx u Hu to the current goal.
Assume Hu3 : u < x .
We prove the intermediate
claim Lmu :
SNo (- u ) .
An exact proof term for the current goal is Hu1 .
We prove the intermediate claim Lmuu : - u + u = 0 .
Apply IH to the current goal.
Apply SNoS_I2 u x Hu1 Hx to the current goal.
An exact proof term for the current goal is Hu2 .
We prove the intermediate claim Lmxmu : - x < - u .
We will prove u < x .
An exact proof term for the current goal is Hu3 .
We will prove w < 0 .
rewrite the current goal using Hwu (from left to right).
We will prove - x + u < 0 .
rewrite the current goal using Lmuu (from right to left).
We will prove - x + u < - u + u .
Apply add_SNo_Lt1 (- x ) u (- u ) Lmx Hu1 Lmu to the current goal.
We will prove - x < - u .
An exact proof term for the current goal is Lmxmu .
We will prove ∀z ∈ R , 0 < z .
Let z be given.
Assume Hz : z ∈ R .
Apply binunionE R1 R2 z Hz to the current goal.
Let v be given.
Assume Hzv : z = v + x .
Apply SNoR_E (- x ) Lmx v Hv to the current goal.
Assume Hv3 : - x < v .
We prove the intermediate
claim Lmv :
SNo (- v ) .
An exact proof term for the current goal is Hv1 .
We prove the intermediate claim Lmvv : - v + v = 0 .
Apply IH to the current goal.
Apply SNoS_I2 v x Hv1 Hx to the current goal.
rewrite the current goal using
minus_SNo_Lev x Hx (from right to left).
An exact proof term for the current goal is Hv2 .
We prove the intermediate claim Lmvx : - v < x .
We will prove - v < - - x .
We will prove - x < v .
An exact proof term for the current goal is Hv3 .
We will prove 0 < z .
rewrite the current goal using Hzv (from left to right).
We will prove 0 < v + x .
rewrite the current goal using
add_SNo_com v x Hv1 Hx (from left to right).
We will prove 0 < x + v .
rewrite the current goal using Lmvv (from right to left).
We will prove - v + v < x + v .
Apply add_SNo_Lt1 (- v ) v x Lmv Hv1 Hx to the current goal.
We will prove - v < x .
An exact proof term for the current goal is Lmvx .
Let v be given.
Assume Hzv : z = - x + v .
Apply SNoR_E x Hx v Hv to the current goal.
Assume Hv3 : x < v .
We prove the intermediate
claim Lmv :
SNo (- v ) .
An exact proof term for the current goal is Hv1 .
We prove the intermediate claim Lmvv : - v + v = 0 .
Apply IH to the current goal.
Apply SNoS_I2 v x Hv1 Hx to the current goal.
An exact proof term for the current goal is Hv2 .
We prove the intermediate claim Lmvmx : - v < - x .
We will prove x < v .
An exact proof term for the current goal is Hv3 .
We will prove 0 < z .
rewrite the current goal using Hzv (from left to right).
We will prove 0 < - x + v .
rewrite the current goal using Lmvv (from right to left).
We will prove - v + v < - x + v .
Apply add_SNo_Lt1 (- v ) v (- x ) Lmv Hv1 Lmx to the current goal.
We will prove - v < - x .
An exact proof term for the current goal is Lmvmx .
Apply Lfst to the current goal.
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is H2 .
∎
Proof: Let x be given.
We prove the intermediate
claim Lmx :
SNo (- x ) .
We will prove x + - x = 0 .
rewrite the current goal using
add_SNo_com x (- x ) Hx Lmx (from left to right).
We will prove - x + x = 0 .
∎
Proof: Let alpha be given.
Let beta be given.
Set Lo1 to be the term
{x + beta |x ∈ SNoS_ alpha } .
Set Lo2 to be the term
{alpha + x |x ∈ SNoS_ beta } .
We will
prove (∀x ∈ Lo1 ∪ Lo2 , SNo x ) ∧ (∀y ∈ Empty , SNo y ) ∧ (∀x ∈ Lo1 ∪ Lo2 , ∀y ∈ Empty , x < y ) .
Apply and3I to the current goal.
Let w be given.
Assume Hw : w ∈ Lo1 ∪ Lo2 .
Apply binunionE Lo1 Lo2 w Hw to the current goal.
Assume H1 : w ∈ Lo1 .
Let x be given.
Apply SNoS_E2 alpha Ha x Hx to the current goal.
Assume _ _ .
Assume _ .
rewrite the current goal using H2 (from left to right).
Assume H1 : w ∈ Lo2 .
Let x be given.
Assume H2 : w = alpha + x .
Assume _ _ .
Assume _ .
rewrite the current goal using H2 (from left to right).
We will
prove SNo (alpha + x ) .
Let y be given.
An
exact proof term for the current goal is
EmptyE y Hy .
Let x be given.
Assume _ .
Let y be given.
An
exact proof term for the current goal is
EmptyE y Hy .
∎
Proof: Let alpha be given.
Let beta be given.
Set Lo1 to be the term
{x + beta |x ∈ SNoS_ alpha } .
Set Lo2 to be the term
{alpha + x |x ∈ SNoS_ beta } .
We prove the intermediate
claim La :
SNo alpha .
An
exact proof term for the current goal is
ordinal_SNo alpha Ha .
We prove the intermediate
claim Lb :
SNo beta .
rewrite the current goal using
add_SNo_eq alpha La beta Lb (from left to right).
rewrite the current goal using
ordinal_SNoL alpha Ha (from left to right).
rewrite the current goal using
ordinal_SNoR alpha Ha (from left to right).
rewrite the current goal using
Repl_Empty (from left to right).
rewrite the current goal using
Repl_Empty (from left to right).
rewrite the current goal using
binunion_idl (from left to right).
Use reflexivity.
∎
Proof: Let alpha be given.
Let beta be given.
We prove the intermediate
claim La :
SNo alpha .
An
exact proof term for the current goal is
ordinal_SNo alpha Ha .
We prove the intermediate
claim Lb :
SNo beta .
We prove the intermediate
claim Lab1 :
SNo (alpha + beta ) .
Let y be given.
Set Lo1 to be the term
{x + beta |x ∈ SNoS_ alpha } .
Set Lo2 to be the term
{alpha + x |x ∈ SNoS_ beta } .
Assume H1 .
Apply H1 to the current goal.
An exact proof term for the current goal is H1 .
rewrite the current goal using H1 (from left to right) at position 2.
An exact proof term for the current goal is Hy1 .
Assume H2 .
Apply H2 to the current goal.
Assume _ _ .
Assume H3 .
Apply H3 to the current goal.
Assume H3 .
Apply H3 to the current goal.
Assume _ .
Assume _ .
Apply H4 y Hy3 to the current goal.
Let w be given.
Assume Hw : w ∈ Lo1 ∪ Lo2 .
We will prove w < y .
Apply SNoLt_tra w (alpha + beta ) y (H2 w Hw ) Lab1 Hy3 to the current goal.
We will
prove w < alpha + beta .
An exact proof term for the current goal is H3 w Hw .
We will
prove alpha + beta < y .
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 .
Apply L1 to the current goal.
Assume _ .
Apply H5 to the current goal.
An exact proof term for the current goal is Hy1 .
∎
Proof: Let alpha be given.
Let beta be given.
We prove the intermediate
claim La :
SNo alpha .
An
exact proof term for the current goal is
ordinal_SNo alpha Ha .
We prove the intermediate
claim Lb :
SNo beta .
We prove the intermediate
claim Lab :
ordinal (alpha + beta ) .
An exact proof term for the current goal is Ha .
We prove the intermediate
claim LSa2 :
SNo (ordsucc alpha ) .
An exact proof term for the current goal is LSa .
Assume H1 .
Apply H1 to the current goal.
Assume H1 .
Apply H1 to the current goal.
Assume _ .
Assume _ .
Apply H1 to the current goal.
We will
prove alpha + beta ∈ Lo1 ∪ Lo2 .
We will
prove SNo_ alpha alpha .
An
exact proof term for the current goal is
ordinal_SNo_ alpha Ha .
We prove the intermediate
claim Lz :
ordinal z .
We prove the intermediate
claim Lz1 :
TransSet z .
We prove the intermediate
claim Lz2 :
SNo z .
An exact proof term for the current goal is Lz .
Let w be given.
Assume Hw : w ∈ Lo1 ∪ Lo2 .
We will prove w < z .
Apply binunionE Lo1 Lo2 w Hw to the current goal.
Assume H4 : w ∈ Lo1 .
Let x be given.
We will prove w < z .
rewrite the current goal using Hwx (from left to right).
We will
prove x + beta < z .
An exact proof term for the current goal is LLxb .
We will
prove SNoLev x ≤ alpha .
We will
prove SNoLev x ⊆ alpha .
Apply Ha to the current goal.
Assume Ha1 _ .
An
exact proof term for the current goal is
Ha1 (SNoLev x ) H5 .
rewrite the current goal using H5 (from left to right).
We will
prove alpha + beta < z .
Assume H4 : w ∈ Lo2 .
Let x be given.
We will prove w < z .
rewrite the current goal using Hwx (from left to right).
We will
prove ordsucc alpha + x < z .
An
exact proof term for the current goal is
IH (SNoLev x ) Hx1 .
We prove the intermediate
claim LSax :
SNo (ordsucc alpha + x ) .
We prove the intermediate
claim LaLx :
ordinal (alpha + SNoLev x ) .
An exact proof term for the current goal is LSaLx .
rewrite the current goal using IHLx (from left to right).
An exact proof term for the current goal is Hx1 .
Let w be given.
An
exact proof term for the current goal is
EmptyE w Hw .
Apply L2 to the current goal.
rewrite the current goal using
ordinal_SNoLev z Lz (from left to right).
Assume _ .
Apply H4 to the current goal.
An exact proof term for the current goal is H3 .
An exact proof term for the current goal is H3 .
∎
Proof: Let alpha be given.
Let beta be given.
We prove the intermediate
claim La :
SNo alpha .
An
exact proof term for the current goal is
ordinal_SNo alpha Ha .
We prove the intermediate
claim Lb :
SNo beta .
We prove the intermediate
claim La :
SNo alpha .
An
exact proof term for the current goal is
ordinal_SNo alpha Ha .
An exact proof term for the current goal is Hb .
rewrite the current goal using
add_SNo_com beta alpha Lb La (from left to right).
Use reflexivity.
∎
Proof: Let alpha be given.
Assume Ha .
Let beta be given.
Assume Hb .
Let gamma be given.
Assume Hc .
We prove the intermediate
claim Lc :
ordinal gamma .
An
exact proof term for the current goal is
ordinal_Hered alpha Ha gamma Hc .
We prove the intermediate
claim Lab :
ordinal (alpha + beta ) .
An exact proof term for the current goal is Ha .
An exact proof term for the current goal is Hb .
We prove the intermediate
claim Lcb :
ordinal (gamma + beta ) .
An exact proof term for the current goal is Lc .
An exact proof term for the current goal is Hb .
We will
prove gamma + beta ∈ alpha + beta .
We will
prove gamma + beta < alpha + beta .
An exact proof term for the current goal is Lc .
An exact proof term for the current goal is Hb .
An exact proof term for the current goal is Ha .
∎
Proof: Let alpha be given.
Let beta be given.
Let gamma be given.
We prove the intermediate
claim La :
SNo alpha .
An
exact proof term for the current goal is
ordinal_SNo alpha Ha .
We prove the intermediate
claim Lb :
SNo beta .
We prove the intermediate
claim Lc :
ordinal gamma .
We prove the intermediate
claim Lc2 :
SNo gamma .
An
exact proof term for the current goal is
ordinal_SNo gamma Lc .
rewrite the current goal using
add_SNo_com alpha gamma La Lc2 (from left to right).
rewrite the current goal using
add_SNo_com alpha beta La Lb (from left to right).
∎
Proof: Let n be given.
We prove the intermediate
claim Ln1 :
nat_p n .
An
exact proof term for the current goal is
omega_nat_p n Hn .
We prove the intermediate
claim Ln2 :
ordinal n .
We prove the intermediate
claim Ln3 :
SNo n .
An
exact proof term for the current goal is
ordinal_SNo n Ln2 .
We prove the intermediate
claim L1 :
∀m, nat_p m → add_nat n m = n + m .
rewrite the current goal using
add_SNo_0R n Ln3 (from left to right).
An
exact proof term for the current goal is
add_nat_0R n .
Let m be given.
rewrite the current goal using IH (from right to left).
An
exact proof term for the current goal is
add_nat_SR n m Hm .
Let m be given.
An
exact proof term for the current goal is
L1 m (omega_nat_p m Hm ) .
∎
Proof: Let n be given.
Assume Hn .
Let m be given.
Assume Hm .
rewrite the current goal using
add_nat_add_SNo n Hn m Hm (from right to left).
An exact proof term for the current goal is Hn .
An exact proof term for the current goal is Hm .
∎
Proof: Let x and y be given.
We prove the intermediate
claim Lxy :
SNo (x + y ) .
An
exact proof term for the current goal is
SNo_add_SNo x y Hx Hy .
We prove the intermediate
claim LI :
∀u, SNo u → SNoLev u ∈ SNoLev (x + y ) → u < x + y → (∃v ∈ SNoL x , u ≤ v + y ) ∨ (∃v ∈ SNoL y , u ≤ x + v ) .
Let u be given.
Assume Hu3 : u < x + y .
Apply dneg to the current goal.
We will prove u < u .
Apply SNoLtLe_tra u (x + y ) u Hu1 Lxy Hu1 Hu3 to the current goal.
We will prove x + y ≤ u .
Set Lxy1 to be the term
{w + y |w ∈ SNoL x } .
Set Lxy2 to be the term
{x + w |w ∈ SNoL y } .
Set Rxy1 to be the term
{z + y |z ∈ SNoR x } .
Set Rxy2 to be the term
{x + z |z ∈ SNoR y } .
rewrite the current goal using
add_SNo_eq x Hx y Hy (from left to right).
We will
prove SNoCut (Lxy1 ∪ Lxy2 ) (Rxy1 ∪ Rxy2 ) ≤ u .
rewrite the current goal using
SNo_eta u Hu1 (from left to right).
rewrite the current goal using
SNo_eta u Hu1 (from right to left).
We will prove ∀w ∈ Lxy1 ∪ Lxy2 , w < u .
Let w be given.
Assume Hw : w ∈ Lxy1 ∪ Lxy2 .
Apply binunionE Lxy1 Lxy2 w Hw to the current goal.
Assume Hw2 : w ∈ Lxy1 .
We will prove w < u .
Let v be given.
Assume Hwv : w = v + y .
Apply SNoL_E x Hx v Hv to the current goal.
Assume Hv3 : v < x .
rewrite the current goal using Hwv (from left to right).
We will prove v + y < u .
We prove the intermediate
claim Lvy :
SNo (v + y ) .
An
exact proof term for the current goal is
SNo_add_SNo v y Hv1 Hy .
Apply SNoLtLe_or (v + y ) u Lvy Hu1 to the current goal.
Assume H1 : v + y < u .
An exact proof term for the current goal is H1 .
Assume H1 : u ≤ v + y .
Apply HNC to the current goal.
Apply orIL to the current goal.
We use v to witness the existential quantifier.
Apply andI to the current goal.
We will
prove v ∈ SNoL x .
An exact proof term for the current goal is Hv .
We will prove u ≤ v + y .
An exact proof term for the current goal is H1 .
Assume Hw2 : w ∈ Lxy2 .
We will prove w < u .
Let v be given.
Assume Hwv : w = x + v .
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hv3 : v < y .
rewrite the current goal using Hwv (from left to right).
We will prove x + v < u .
We prove the intermediate
claim Lxv :
SNo (x + v ) .
An
exact proof term for the current goal is
SNo_add_SNo x v Hx Hv1 .
Apply SNoLtLe_or (x + v ) u Lxv Hu1 to the current goal.
Assume H1 : x + v < u .
An exact proof term for the current goal is H1 .
Assume H1 : u ≤ x + v .
Apply HNC to the current goal.
Apply orIR to the current goal.
We use v to witness the existential quantifier.
Apply andI to the current goal.
We will
prove v ∈ SNoL y .
An exact proof term for the current goal is Hv .
We will prove u ≤ x + v .
An exact proof term for the current goal is H1 .
rewrite the current goal using
add_SNo_eq x Hx y Hy (from right to left).
We will
prove ∀z ∈ SNoR u , x + y < z .
Let z be given.
Apply SNoR_E u Hu1 z Hz to the current goal.
Assume Hz3 : u < z .
Assume H1 .
Apply H1 to the current goal.
Assume H1 : x + y < z .
An exact proof term for the current goal is H1 .
Assume H1 : x + y = z .
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hu2 .
Assume H1 : z < x + y .
We prove the intermediate
claim Lz1 :
z ∈ SNoS_ (SNoLev u ) .
An
exact proof term for the current goal is
SNoR_SNoS_ u z Hz .
We prove the intermediate
claim Lz2 :
SNoLev z ∈ SNoLev (x + y ) .
Assume Hxy1 _ .
An
exact proof term for the current goal is
Hxy1 (SNoLev u ) Hu2 (SNoLev z ) Hz2 .
Apply IH z Lz1 Lz2 H1 to the current goal.
Apply H2 to the current goal.
Let v be given.
Assume H3 .
Apply H3 to the current goal.
Assume H3 : z ≤ v + y .
Apply SNoL_E x Hx v Hv to the current goal.
Assume Hv3 : v < x .
Apply HNC to the current goal.
Apply orIL to the current goal.
We use v to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv .
We will prove u ≤ v + y .
We will prove u ≤ z .
An exact proof term for the current goal is Hz3 .
We will prove z ≤ v + y .
An exact proof term for the current goal is H3 .
Apply H2 to the current goal.
Let v be given.
Assume H3 .
Apply H3 to the current goal.
Assume H3 : z ≤ x + v .
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hv3 : v < y .
Apply HNC to the current goal.
Apply orIR to the current goal.
We use v to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv .
We will prove u ≤ x + v .
We will prove u ≤ z .
An exact proof term for the current goal is Hz3 .
We will prove z ≤ x + v .
An exact proof term for the current goal is H3 .
Let u be given.
Apply SNoL_E (x + y ) Lxy u Hu to the current goal.
Assume Hu3 : u < x + y .
An exact proof term for the current goal is LI u Hu1 Hu2 Hu3 .
∎
Proof: Let x and y be given.
We prove the intermediate
claim Lxy :
SNo (x + y ) .
An
exact proof term for the current goal is
SNo_add_SNo x y Hx Hy .
We prove the intermediate
claim LI :
∀u, SNo u → SNoLev u ∈ SNoLev (x + y ) → x + y < u → (∃v ∈ SNoR x , v + y ≤ u ) ∨ (∃v ∈ SNoR y , x + v ≤ u ) .
Let u be given.
Assume Hu3 : x + y < u .
Apply dneg to the current goal.
We will prove u < u .
Apply (λH : u ≤ x + y ⇒ SNoLeLt_tra u (x + y ) u Hu1 Lxy Hu1 H Hu3 ) to the current goal.
We will prove u ≤ x + y .
Set Lxy1 to be the term
{w + y |w ∈ SNoL x } .
Set Lxy2 to be the term
{x + w |w ∈ SNoL y } .
Set Rxy1 to be the term
{z + y |z ∈ SNoR x } .
Set Rxy2 to be the term
{x + z |z ∈ SNoR y } .
rewrite the current goal using
add_SNo_eq x Hx y Hy (from left to right).
We will
prove u ≤ SNoCut (Lxy1 ∪ Lxy2 ) (Rxy1 ∪ Rxy2 ) .
rewrite the current goal using
SNo_eta u Hu1 (from left to right).
rewrite the current goal using
add_SNo_eq x Hx y Hy (from right to left).
We will
prove ∀z ∈ SNoL u , z < x + y .
Let z be given.
Apply SNoL_E u Hu1 z Hz to the current goal.
Assume Hz3 : z < u .
Assume H1 .
Apply H1 to the current goal.
Assume H1 : z < x + y .
An exact proof term for the current goal is H1 .
Assume H1 : z = x + y .
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hu2 .
Assume H1 : x + y < z .
We prove the intermediate
claim Lz1 :
z ∈ SNoS_ (SNoLev u ) .
An
exact proof term for the current goal is
SNoL_SNoS_ u z Hz .
We prove the intermediate
claim Lz2 :
SNoLev z ∈ SNoLev (x + y ) .
Assume Hxy1 _ .
An
exact proof term for the current goal is
Hxy1 (SNoLev u ) Hu2 (SNoLev z ) Hz2 .
Apply IH z Lz1 Lz2 H1 to the current goal.
Apply H2 to the current goal.
Let v be given.
Assume H3 .
Apply H3 to the current goal.
Assume H3 : v + y ≤ z .
Apply SNoR_E x Hx v Hv to the current goal.
Assume Hv3 : x < v .
Apply HNC to the current goal.
Apply orIL to the current goal.
We use v to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv .
We will prove v + y ≤ u .
We will prove v + y ≤ z .
An exact proof term for the current goal is H3 .
We will prove z ≤ u .
An exact proof term for the current goal is Hz3 .
Apply H2 to the current goal.
Let v be given.
Assume H3 .
Apply H3 to the current goal.
Assume H3 : x + v ≤ z .
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hv3 : y < v .
Apply HNC to the current goal.
Apply orIR to the current goal.
We use v to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv .
We will prove x + v ≤ u .
We will prove x + v ≤ z .
An exact proof term for the current goal is H3 .
We will prove z ≤ u .
An exact proof term for the current goal is Hz3 .
rewrite the current goal using
SNo_eta u Hu1 (from right to left).
We will prove ∀w ∈ Rxy1 ∪ Rxy2 , u < w .
Let w be given.
Assume Hw : w ∈ Rxy1 ∪ Rxy2 .
Apply binunionE Rxy1 Rxy2 w Hw to the current goal.
Assume Hw2 : w ∈ Rxy1 .
We will prove u < w .
Let v be given.
Assume Hwv : w = v + y .
Apply SNoR_E x Hx v Hv to the current goal.
Assume Hv3 : x < v .
rewrite the current goal using Hwv (from left to right).
We will prove u < v + y .
We prove the intermediate
claim Lvy :
SNo (v + y ) .
An
exact proof term for the current goal is
SNo_add_SNo v y Hv1 Hy .
Apply SNoLtLe_or u (v + y ) Hu1 Lvy to the current goal.
Assume H1 : u < v + y .
An exact proof term for the current goal is H1 .
Assume H1 : v + y ≤ u .
Apply HNC to the current goal.
Apply orIL to the current goal.
We use v to witness the existential quantifier.
Apply andI to the current goal.
We will
prove v ∈ SNoR x .
An exact proof term for the current goal is Hv .
We will prove v + y ≤ u .
An exact proof term for the current goal is H1 .
Assume Hw2 : w ∈ Rxy2 .
We will prove u < w .
Let v be given.
Assume Hwv : w = x + v .
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hv3 : y < v .
rewrite the current goal using Hwv (from left to right).
We will prove u < x + v .
We prove the intermediate
claim Lxv :
SNo (x + v ) .
An
exact proof term for the current goal is
SNo_add_SNo x v Hx Hv1 .
Apply SNoLtLe_or u (x + v ) Hu1 Lxv to the current goal.
Assume H1 : u < x + v .
An exact proof term for the current goal is H1 .
Assume H1 : x + v ≤ u .
Apply HNC to the current goal.
Apply orIR to the current goal.
We use v to witness the existential quantifier.
Apply andI to the current goal.
We will
prove v ∈ SNoR y .
An exact proof term for the current goal is Hv .
We will prove x + v ≤ u .
An exact proof term for the current goal is H1 .
Let u be given.
Apply SNoR_E (x + y ) Lxy u Hu to the current goal.
Assume Hu3 : x + y < u .
An exact proof term for the current goal is LI u Hu1 Hu2 Hu3 .
∎
Proof: Set P to be the term λx y z ⇒ x + (y + z ) = (x + y ) + z of type set → set → set → prop .
Let x, y and z be given.
We will prove x + (y + z ) = (x + y ) + z .
We prove the intermediate
claim Lxy :
SNo (x + y ) .
An
exact proof term for the current goal is
SNo_add_SNo x y Hx Hy .
We prove the intermediate
claim Lyz :
SNo (y + z ) .
An
exact proof term for the current goal is
SNo_add_SNo y z Hy Hz .
Set Lxyz1 to be the term
{w + (y + z ) |w ∈ SNoL x } .
Set Lxyz2 to be the term
{x + w |w ∈ SNoL (y + z ) } .
Set Rxyz1 to be the term
{w + (y + z ) |w ∈ SNoR x } .
Set Rxyz2 to be the term
{x + w |w ∈ SNoR (y + z ) } .
Set Lxyz3 to be the term
{w + z |w ∈ SNoL (x + y ) } .
Set Lxyz4 to be the term
{(x + y ) + w |w ∈ SNoL z } .
Set Rxyz3 to be the term
{w + z |w ∈ SNoR (x + y ) } .
Set Rxyz4 to be the term
{(x + y ) + w |w ∈ SNoR z } .
rewrite the current goal using
add_SNo_eq x Hx (y + z ) Lyz (from left to right).
rewrite the current goal using
add_SNo_eq (x + y ) Lxy z Hz (from left to right).
We will
prove (SNoCut (Lxyz1 ∪ Lxyz2 ) (Rxyz1 ∪ Rxyz2 ) ) = (SNoCut (Lxyz3 ∪ Lxyz4 ) (Rxyz3 ∪ Rxyz4 ) ) .
We prove the intermediate
claim Lxyz12 :
SNoCutP (Lxyz1 ∪ Lxyz2 ) (Rxyz1 ∪ Rxyz2 ) .
An
exact proof term for the current goal is
add_SNo_SNoCutP x (y + z ) Hx Lyz .
We prove the intermediate
claim Lxyz34 :
SNoCutP (Lxyz3 ∪ Lxyz4 ) (Rxyz3 ∪ Rxyz4 ) .
An
exact proof term for the current goal is
add_SNo_SNoCutP (x + y ) z Lxy Hz .
An exact proof term for the current goal is Lxyz12 .
An exact proof term for the current goal is Lxyz34 .
We will
prove ∀w ∈ Lxyz1 ∪ Lxyz2 , w < SNoCut (Lxyz3 ∪ Lxyz4 ) (Rxyz3 ∪ Rxyz4 ) .
rewrite the current goal using
add_SNo_eq (x + y ) Lxy z Hz (from right to left).
We will prove ∀w ∈ Lxyz1 ∪ Lxyz2 , w < (x + y ) + z .
Let w be given.
Assume Hw : w ∈ Lxyz1 ∪ Lxyz2 .
Apply binunionE Lxyz1 Lxyz2 w Hw to the current goal.
Assume Hw : w ∈ Lxyz1 .
Let u be given.
Assume Hwu : w = u + (y + z ) .
Apply SNoL_E x Hx u Hu to the current goal.
Assume Hu3 : u < x .
We will prove w < (x + y ) + z .
rewrite the current goal using Hwu (from left to right).
We will prove u + (y + z ) < (x + y ) + z .
We prove the intermediate claim IH1u : u + (y + z ) = (u + y ) + z .
An
exact proof term for the current goal is
IH1 u (SNoL_SNoS_ x u Hu ) .
rewrite the current goal using IH1u (from left to right).
We will prove (u + y ) + z < (x + y ) + z .
We will prove u + y < x + y .
We will prove u < x .
An exact proof term for the current goal is Hu3 .
Assume Hw : w ∈ Lxyz2 .
Let u be given.
Assume Hwu : w = x + u .
Apply SNoL_E (y + z ) Lyz u Hu to the current goal.
Assume Hu3 : u < y + z .
rewrite the current goal using Hwu (from left to right).
We will prove x + u < (x + y ) + z .
Apply H1 to the current goal.
Let v be given.
Assume H2 .
Apply H2 to the current goal.
Assume H2 : u ≤ v + z .
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hv3 : v < y .
We prove the intermediate claim IH2v : x + (v + z ) = (x + v ) + z .
An
exact proof term for the current goal is
IH2 v (SNoL_SNoS_ y v Hv ) .
We will prove x + u < (x + y ) + z .
We will prove x + u ≤ x + (v + z ) .
We will prove u ≤ v + z .
An exact proof term for the current goal is H2 .
We will prove x + (v + z ) < (x + y ) + z .
rewrite the current goal using IH2v (from left to right).
We will prove (x + v ) + z < (x + y ) + z .
We will prove x + v < x + y .
We will prove v < y .
An exact proof term for the current goal is Hv3 .
Apply H1 to the current goal.
Let v be given.
Assume H2 .
Apply H2 to the current goal.
Assume H2 : u ≤ y + v .
Apply SNoL_E z Hz v Hv to the current goal.
Assume Hv3 : v < z .
We prove the intermediate claim IH3v : x + (y + v ) = (x + y ) + v .
An
exact proof term for the current goal is
IH3 v (SNoL_SNoS_ z v Hv ) .
We will prove x + u < (x + y ) + z .
We will prove x + u ≤ x + (y + v ) .
We will prove u ≤ y + v .
An exact proof term for the current goal is H2 .
We will prove x + (y + v ) < (x + y ) + z .
rewrite the current goal using IH3v (from left to right).
We will prove (x + y ) + v < (x + y ) + z .
Apply add_SNo_Lt2 (x + y ) v z Lxy Hv1 Hz to the current goal.
We will prove v < z .
An exact proof term for the current goal is Hv3 .
We will
prove ∀v ∈ Rxyz1 ∪ Rxyz2 , SNoCut (Lxyz3 ∪ Lxyz4 ) (Rxyz3 ∪ Rxyz4 ) < v .
rewrite the current goal using
add_SNo_eq (x + y ) Lxy z Hz (from right to left).
We will prove ∀v ∈ Rxyz1 ∪ Rxyz2 , (x + y ) + z < v .
Let v be given.
Assume Hv : v ∈ Rxyz1 ∪ Rxyz2 .
Apply binunionE Rxyz1 Rxyz2 v Hv to the current goal.
Assume Hv : v ∈ Rxyz1 .
Let u be given.
Assume Hvu : v = u + (y + z ) .
Apply SNoR_E x Hx u Hu to the current goal.
Assume Hu3 : x < u .
We will prove (x + y ) + z < v .
rewrite the current goal using Hvu (from left to right).
We will prove (x + y ) + z < u + (y + z ) .
We prove the intermediate claim IH1u : u + (y + z ) = (u + y ) + z .
An
exact proof term for the current goal is
IH1 u (SNoR_SNoS_ x u Hu ) .
rewrite the current goal using IH1u (from left to right).
We will prove (x + y ) + z < (u + y ) + z .
We will prove x + y < u + y .
We will prove x < u .
An exact proof term for the current goal is Hu3 .
Assume Hv : v ∈ Rxyz2 .
Let u be given.
Assume Hvu : v = x + u .
Apply SNoR_E (y + z ) Lyz u Hu to the current goal.
Assume Hu3 : y + z < u .
rewrite the current goal using Hvu (from left to right).
We will prove (x + y ) + z < x + u .
Apply H1 to the current goal.
Let v be given.
Assume H2 .
Apply H2 to the current goal.
Assume H2 : v + z ≤ u .
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hv3 : y < v .
We prove the intermediate claim IH2v : x + (v + z ) = (x + v ) + z .
An
exact proof term for the current goal is
IH2 v (SNoR_SNoS_ y v Hv ) .
We will prove (x + y ) + z < x + u .
We will prove (x + y ) + z < x + (v + z ) .
rewrite the current goal using IH2v (from left to right).
We will prove (x + y ) + z < (x + v ) + z .
We will prove x + y < x + v .
We will prove y < v .
An exact proof term for the current goal is Hv3 .
We will prove x + (v + z ) ≤ x + u .
We will prove v + z ≤ u .
An exact proof term for the current goal is H2 .
Apply H1 to the current goal.
Let v be given.
Assume H2 .
Apply H2 to the current goal.
Assume H2 : y + v ≤ u .
Apply SNoR_E z Hz v Hv to the current goal.
Assume Hv3 : z < v .
We prove the intermediate claim IH3v : x + (y + v ) = (x + y ) + v .
An
exact proof term for the current goal is
IH3 v (SNoR_SNoS_ z v Hv ) .
We will prove (x + y ) + z < x + u .
We will prove (x + y ) + z < x + (y + v ) .
rewrite the current goal using IH3v (from left to right).
We will prove (x + y ) + z < (x + y ) + v .
Apply add_SNo_Lt2 (x + y ) z v Lxy Hz Hv1 to the current goal.
We will prove z < v .
An exact proof term for the current goal is Hv3 .
We will prove x + (y + v ) ≤ x + u .
We will prove y + v ≤ u .
An exact proof term for the current goal is H2 .
We will
prove ∀w ∈ Lxyz3 ∪ Lxyz4 , w < SNoCut (Lxyz1 ∪ Lxyz2 ) (Rxyz1 ∪ Rxyz2 ) .
rewrite the current goal using
add_SNo_eq x Hx (y + z ) Lyz (from right to left).
We will prove ∀w ∈ Lxyz3 ∪ Lxyz4 , w < x + (y + z ) .
Let w be given.
Assume Hw : w ∈ Lxyz3 ∪ Lxyz4 .
Apply binunionE Lxyz3 Lxyz4 w Hw to the current goal.
Assume Hw : w ∈ Lxyz3 .
Let u be given.
Assume Hwu : w = u + z .
Apply SNoL_E (x + y ) Lxy u Hu to the current goal.
Assume Hu3 : u < x + y .
rewrite the current goal using Hwu (from left to right).
We will prove u + z < x + (y + z ) .
Apply H1 to the current goal.
Let v be given.
Assume H2 .
Apply H2 to the current goal.
Assume H2 : u ≤ v + y .
Apply SNoL_E x Hx v Hv to the current goal.
Assume Hv3 : v < x .
We prove the intermediate claim IH1v : v + (y + z ) = (v + y ) + z .
An
exact proof term for the current goal is
IH1 v (SNoL_SNoS_ x v Hv ) .
We will prove u + z < x + (y + z ) .
We will prove u + z ≤ (v + y ) + z .
We will prove u ≤ v + y .
An exact proof term for the current goal is H2 .
We will prove (v + y ) + z < x + (y + z ) .
rewrite the current goal using IH1v (from right to left).
We will prove v + (y + z ) < x + (y + z ) .
Apply add_SNo_Lt1 v (y + z ) x Hv1 Lyz Hx to the current goal.
We will prove v < x .
An exact proof term for the current goal is Hv3 .
Apply H1 to the current goal.
Let v be given.
Assume H2 .
Apply H2 to the current goal.
Assume H2 : u ≤ x + v .
Apply SNoL_E y Hy v Hv to the current goal.
Assume Hv3 : v < y .
We prove the intermediate claim IH2v : x + (v + z ) = (x + v ) + z .
An
exact proof term for the current goal is
IH2 v (SNoL_SNoS_ y v Hv ) .
We will prove u + z < x + (y + z ) .
We will prove u + z ≤ (x + v ) + z .
We will prove u ≤ x + v .
An exact proof term for the current goal is H2 .
We will prove (x + v ) + z < x + (y + z ) .
rewrite the current goal using IH2v (from right to left).
We will prove x + (v + z ) < x + (y + z ) .
We will prove v + z < y + z .
We will prove v < y .
An exact proof term for the current goal is Hv3 .
Assume Hw : w ∈ Lxyz4 .
Let u be given.
Assume Hwu : w = (x + y ) + u .
Apply SNoL_E z Hz u Hu to the current goal.
Assume Hu3 : u < z .
We will prove w < x + (y + z ) .
rewrite the current goal using Hwu (from left to right).
We will prove (x + y ) + u < x + (y + z ) .
We prove the intermediate claim IH3u : x + (y + u ) = (x + y ) + u .
An
exact proof term for the current goal is
IH3 u (SNoL_SNoS_ z u Hu ) .
rewrite the current goal using IH3u (from right to left).
We will prove x + (y + u ) < x + (y + z ) .
We will prove y + u < y + z .
We will prove u < z .
An exact proof term for the current goal is Hu3 .
We will
prove ∀v ∈ Rxyz3 ∪ Rxyz4 , SNoCut (Lxyz1 ∪ Lxyz2 ) (Rxyz1 ∪ Rxyz2 ) < v .
rewrite the current goal using
add_SNo_eq x Hx (y + z ) Lyz (from right to left).
We will prove ∀v ∈ Rxyz3 ∪ Rxyz4 , x + (y + z ) < v .
Let v be given.
Assume Hv : v ∈ Rxyz3 ∪ Rxyz4 .
Apply binunionE Rxyz3 Rxyz4 v Hv to the current goal.
Assume Hv : v ∈ Rxyz3 .
Let u be given.
Assume Hvu : v = u + z .
Apply SNoR_E (x + y ) Lxy u Hu to the current goal.
Assume Hu3 : x + y < u .
rewrite the current goal using Hvu (from left to right).
We will prove x + (y + z ) < u + z .
Apply H1 to the current goal.
Let v be given.
Assume H2 .
Apply H2 to the current goal.
Assume H2 : v + y ≤ u .
Apply SNoR_E x Hx v Hv to the current goal.
Assume Hv3 : x < v .
We prove the intermediate claim IH1v : v + (y + z ) = (v + y ) + z .
An
exact proof term for the current goal is
IH1 v (SNoR_SNoS_ x v Hv ) .
We will prove x + (y + z ) < u + z .
We will prove x + (y + z ) < (v + y ) + z .
rewrite the current goal using IH1v (from right to left).
We will prove x + (y + z ) < v + (y + z ) .
Apply add_SNo_Lt1 x (y + z ) v Hx Lyz Hv1 to the current goal.
We will prove x < v .
An exact proof term for the current goal is Hv3 .
We will prove (v + y ) + z ≤ u + z .
We will prove v + y ≤ u .
An exact proof term for the current goal is H2 .
Apply H1 to the current goal.
Let v be given.
Assume H2 .
Apply H2 to the current goal.
Assume H2 : x + v ≤ u .
Apply SNoR_E y Hy v Hv to the current goal.
Assume Hv3 : y < v .
We prove the intermediate claim IH2v : x + (v + z ) = (x + v ) + z .
An
exact proof term for the current goal is
IH2 v (SNoR_SNoS_ y v Hv ) .
We will prove x + (y + z ) < u + z .
We will prove x + (y + z ) < (x + v ) + z .
rewrite the current goal using IH2v (from right to left).
We will prove x + (y + z ) < x + (v + z ) .
We will prove y + z < v + z .
We will prove y < v .
An exact proof term for the current goal is Hv3 .
We will prove (x + v ) + z ≤ u + z .
We will prove x + v ≤ u .
An exact proof term for the current goal is H2 .
Assume Hv : v ∈ Rxyz4 .
Let u be given.
Assume Hvu : v = (x + y ) + u .
Apply SNoR_E z Hz u Hu to the current goal.
Assume Hu3 : z < u .
We will prove x + (y + z ) < v .
rewrite the current goal using Hvu (from left to right).
We will prove x + (y + z ) < (x + y ) + u .
We prove the intermediate claim IH3u : x + (y + u ) = (x + y ) + u .
An
exact proof term for the current goal is
IH3 u (SNoR_SNoS_ z u Hu ) .
rewrite the current goal using IH3u (from right to left).
We will prove x + (y + z ) < x + (y + u ) .
We will prove y + z < y + u .
We will prove z < u .
An exact proof term for the current goal is Hu3 .
∎
Proof: Let x, y and z be given.
Assume Hxyz : x + y = x + z .
We prove the intermediate
claim Lmx :
SNo (- x ) .
We prove the intermediate claim L1 : - x + (x + y ) = y .
rewrite the current goal using
add_SNo_assoc (- x ) x y Lmx Hx Hy (from left to right).
We will prove (- x + x ) + y = y .
We will prove 0 + y = y .
An
exact proof term for the current goal is
add_SNo_0L y Hy .
We prove the intermediate claim L2 : - x + (x + z ) = z .
rewrite the current goal using
add_SNo_assoc (- x ) x z Lmx Hx Hz (from left to right).
We will prove (- x + x ) + z = z .
We will prove 0 + z = z .
An
exact proof term for the current goal is
add_SNo_0L z Hz .
rewrite the current goal using L1 (from right to left).
rewrite the current goal using Hxyz (from left to right).
An exact proof term for the current goal is L2 .
∎
Theorem. (
minus_SNo_0 ) The following is provable:
- 0 = 0
Proof:
We will prove 0 + - 0 = 0 + 0 .
Use transitivity with and 0 .
∎
Proof: Let x and y be given.
We prove the intermediate
claim Lmx :
SNo (- x ) .
We prove the intermediate
claim Lmy :
SNo (- y ) .
We prove the intermediate
claim Lxy :
SNo (x + y ) .
An
exact proof term for the current goal is
SNo_add_SNo x y Hx Hy .
We prove the intermediate claim L1 : (x + y ) + - (x + y ) = (x + y ) + ((- x ) + (- y ) ) .
We will prove 0 = (x + y ) + ((- x ) + (- y ) ) .
rewrite the current goal using
add_SNo_assoc (x + y ) (- x ) (- y ) Lxy Lmx Lmy (from left to right).
We will prove 0 = ((x + y ) + (- x ) ) + (- y ) .
rewrite the current goal using
add_SNo_com x y Hx Hy (from left to right).
We will prove 0 = ((y + x ) + - x ) + - y .
rewrite the current goal using
add_SNo_assoc y x (- x ) Hy Hx Lmx (from right to left).
We will prove 0 = (y + (x + - x ) ) + - y .
We will prove 0 = (y + 0 ) + - y .
rewrite the current goal using
add_SNo_0R y Hy (from left to right).
We will prove 0 = y + - y .
We will prove 0 = 0 .
Use reflexivity.
∎
Proof: Let x, y and z be given.
Assume Hx Hy Hz .
Use transitivity with and - x + - (y + z ) .
Use f_equal.
We will prove - (y + z ) = - y + - z .
∎
Proof: Set P to be the term
λx y ⇒ SNoLev (x + y ) ⊆ SNoLev x + SNoLev y of type
set → set → prop .
Let x and y be given.
We prove the intermediate
claim Lxy :
SNo (x + y ) .
An
exact proof term for the current goal is
SNo_add_SNo x y Hx Hy .
An exact proof term for the current goal is Hx .
An exact proof term for the current goal is Hy .
Set Lxy1 to be the term
{w + y |w ∈ SNoL x } .
Set Lxy2 to be the term
{x + w |w ∈ SNoL y } .
Set Rxy1 to be the term
{z + y |z ∈ SNoR x } .
Set Rxy2 to be the term
{x + z |z ∈ SNoR y } .
rewrite the current goal using
add_SNo_eq x Hx y Hy (from left to right).
We prove the intermediate
claim L1 :
SNoCutP (Lxy1 ∪ Lxy2 ) (Rxy1 ∪ Rxy2 ) .
Assume _ _ _ .
We prove the intermediate
claim Lxy1E :
∀u ∈ Lxy1 , ∀p : set → prop , (∀w ∈ SNoS_ (SNoLev x ) , u = w + y → SNo w → SNoLev w ∈ SNoLev x → w < x → p (w + y ) ) → p u .
Let u be given.
Assume Hu .
Let p be given.
Assume Hp .
Let w be given.
Assume Huw : u = w + y .
rewrite the current goal using Huw (from left to right).
Apply SNoL_E x Hx w Hw to the current goal.
We prove the intermediate
claim Lw :
w ∈ SNoS_ (SNoLev x ) .
An
exact proof term for the current goal is
SNoL_SNoS_ x w Hw .
An exact proof term for the current goal is Hp w Lw Huw .
We prove the intermediate
claim Lxy2E :
∀u ∈ Lxy2 , ∀p : set → prop , (∀w ∈ SNoS_ (SNoLev y ) , u = x + w → SNo w → SNoLev w ∈ SNoLev y → w < y → p (x + w ) ) → p u .
Let u be given.
Assume Hu .
Let p be given.
Assume Hp .
Let w be given.
Assume Huw : u = x + w .
rewrite the current goal using Huw (from left to right).
Apply SNoL_E y Hy w Hw to the current goal.
We prove the intermediate
claim Lw :
w ∈ SNoS_ (SNoLev y ) .
An
exact proof term for the current goal is
SNoL_SNoS_ y w Hw .
An exact proof term for the current goal is Hp w Lw Huw .
We prove the intermediate
claim Rxy1E :
∀u ∈ Rxy1 , ∀p : set → prop , (∀w ∈ SNoS_ (SNoLev x ) , u = w + y → SNo w → SNoLev w ∈ SNoLev x → x < w → p (w + y ) ) → p u .
Let u be given.
Assume Hu .
Let p be given.
Assume Hp .
Let w be given.
Assume Huw : u = w + y .
rewrite the current goal using Huw (from left to right).
Apply SNoR_E x Hx w Hw to the current goal.
We prove the intermediate
claim Lw :
w ∈ SNoS_ (SNoLev x ) .
An
exact proof term for the current goal is
SNoR_SNoS_ x w Hw .
An exact proof term for the current goal is Hp w Lw Huw .
We prove the intermediate
claim Rxy2E :
∀u ∈ Rxy2 , ∀p : set → prop , (∀w ∈ SNoS_ (SNoLev y ) , u = x + w → SNo w → SNoLev w ∈ SNoLev y → y < w → p (x + w ) ) → p u .
Let u be given.
Assume Hu .
Let p be given.
Assume Hp .
Let w be given.
Assume Huw : u = x + w .
rewrite the current goal using Huw (from left to right).
Apply SNoR_E y Hy w Hw to the current goal.
We prove the intermediate
claim Lw :
w ∈ SNoS_ (SNoLev y ) .
An
exact proof term for the current goal is
SNoR_SNoS_ y w Hw .
An exact proof term for the current goal is Hp w Lw Huw .
We prove the intermediate
claim Lxy1E2 :
∀u ∈ Lxy1 , SNo u .
Let u be given.
Assume Hu .
Apply Lxy1E u Hu to the current goal.
Let w be given.
Assume Hw1 Hw2 Hw3 Hw4 Hw5 .
We will
prove SNo (w + y ) .
An exact proof term for the current goal is Hw3 .
An exact proof term for the current goal is Hy .
We prove the intermediate
claim Lxy2E2 :
∀u ∈ Lxy2 , SNo u .
Let u be given.
Assume Hu .
Apply Lxy2E u Hu to the current goal.
Let w be given.
Assume Hw1 Hw2 Hw3 Hw4 Hw5 .
We will
prove SNo (x + w ) .
An exact proof term for the current goal is Hx .
An exact proof term for the current goal is Hw3 .
We prove the intermediate
claim Rxy1E2 :
∀u ∈ Rxy1 , SNo u .
Let u be given.
Assume Hu .
Apply Rxy1E u Hu to the current goal.
Let w be given.
Assume Hw1 Hw2 Hw3 Hw4 Hw5 .
We will
prove SNo (w + y ) .
An exact proof term for the current goal is Hw3 .
An exact proof term for the current goal is Hy .
We prove the intermediate
claim Rxy2E2 :
∀u ∈ Rxy2 , SNo u .
Let u be given.
Assume Hu .
Apply Rxy2E u Hu to the current goal.
Let w be given.
Assume Hw1 Hw2 Hw3 Hw4 Hw5 .
We will
prove SNo (x + w ) .
An exact proof term for the current goal is Hx .
An exact proof term for the current goal is Hw3 .
Let u be given.
Assume Hu : u ∈ Lxy1 ∪ Lxy2 .
Apply binunionE Lxy1 Lxy2 u Hu to the current goal.
Assume Hu .
An exact proof term for the current goal is Lxy1E2 u Hu .
Assume Hu .
An exact proof term for the current goal is Lxy2E2 u Hu .
Let u be given.
Assume Hu : u ∈ Rxy1 ∪ Rxy2 .
Apply binunionE Rxy1 Rxy2 u Hu to the current goal.
Assume Hu .
An exact proof term for the current goal is Rxy1E2 u Hu .
Assume Hu .
An exact proof term for the current goal is Rxy2E2 u Hu .
Apply L2 to the current goal.
Assume H _ .
An exact proof term for the current goal is H .
An exact proof term for the current goal is H2 .
Let v be given.
Let u be given.
Assume Hu : u ∈ Lxy1 ∪ Lxy2 .
Apply binunionE Lxy1 Lxy2 u Hu to the current goal.
Assume Hu : u ∈ Lxy1 .
Apply Lxy1E u Hu to the current goal.
Let w be given.
Assume Hw2 : u = w + y .
Assume Hw5 : w < x .
We prove the intermediate
claim Lv :
ordinal v .
An exact proof term for the current goal is Hw3 .
An exact proof term for the current goal is Hy .
An exact proof term for the current goal is Hw6 .
An exact proof term for the current goal is H1 .
Apply IH1 to the current goal.
An exact proof term for the current goal is Hw1 .
An exact proof term for the current goal is Hx .
An exact proof term for the current goal is Hy .
An exact proof term for the current goal is Hw4 .
Apply LLxLy to the current goal.
Assume H _ .
An
exact proof term for the current goal is
H (SNoLev w + SNoLev y ) L4a .
We prove the intermediate
claim L4c :
v ⊆ SNoLev (w + y ) .
rewrite the current goal using H3 (from left to right) at position 1.
An exact proof term for the current goal is H2 .
An exact proof term for the current goal is H2 .
Apply LIHw to the current goal.
Apply L4c to the current goal.
Apply H1 to the current goal.
An exact proof term for the current goal is L4a .
Assume Hu : u ∈ Lxy2 .
Apply Lxy2E u Hu to the current goal.
Let w be given.
Assume Hw2 : u = x + w .
Assume Hw5 : w < y .
We prove the intermediate
claim Lv :
ordinal v .
An exact proof term for the current goal is Hx .
An exact proof term for the current goal is Hw3 .
An exact proof term for the current goal is Hw6 .
An exact proof term for the current goal is H1 .
Apply IH2 to the current goal.
An exact proof term for the current goal is Hw1 .
An exact proof term for the current goal is Hx .
An exact proof term for the current goal is Hy .
An exact proof term for the current goal is Hw4 .
Apply LLxLy to the current goal.
Assume H _ .
An
exact proof term for the current goal is
H (SNoLev x + SNoLev w ) L4a .
We prove the intermediate
claim L4c :
v ⊆ SNoLev (x + w ) .
rewrite the current goal using H3 (from left to right) at position 1.
An exact proof term for the current goal is H2 .
An exact proof term for the current goal is H2 .
Apply LIHw to the current goal.
Apply L4c to the current goal.
Apply H1 to the current goal.
An exact proof term for the current goal is L4a .
Let v be given.
Let u be given.
Assume Hu : u ∈ Rxy1 ∪ Rxy2 .
Apply binunionE Rxy1 Rxy2 u Hu to the current goal.
Assume Hu : u ∈ Rxy1 .
Apply Rxy1E u Hu to the current goal.
Let w be given.
Assume Hw2 : u = w + y .
Assume Hw5 : x < w .
We prove the intermediate
claim Lv :
ordinal v .
An exact proof term for the current goal is Hw3 .
An exact proof term for the current goal is Hy .
An exact proof term for the current goal is Hw6 .
An exact proof term for the current goal is H1 .
Apply IH1 to the current goal.
An exact proof term for the current goal is Hw1 .
An exact proof term for the current goal is Hx .
An exact proof term for the current goal is Hy .
An exact proof term for the current goal is Hw4 .
Apply LLxLy to the current goal.
Assume H _ .
An
exact proof term for the current goal is
H (SNoLev w + SNoLev y ) L4a .
We prove the intermediate
claim L4c :
v ⊆ SNoLev (w + y ) .
rewrite the current goal using H3 (from left to right) at position 1.
An exact proof term for the current goal is H2 .
An exact proof term for the current goal is H2 .
Apply LIHw to the current goal.
Apply L4c to the current goal.
Apply H1 to the current goal.
An exact proof term for the current goal is L4a .
Assume Hu : u ∈ Rxy2 .
Apply Rxy2E u Hu to the current goal.
Let w be given.
Assume Hw2 : u = x + w .
Assume Hw5 : y < w .
We prove the intermediate
claim Lv :
ordinal v .
An exact proof term for the current goal is Hx .
An exact proof term for the current goal is Hw3 .
An exact proof term for the current goal is Hw6 .
An exact proof term for the current goal is H1 .
Apply IH2 to the current goal.
An exact proof term for the current goal is Hw1 .
An exact proof term for the current goal is Hx .
An exact proof term for the current goal is Hy .
An exact proof term for the current goal is Hw4 .
Apply LLxLy to the current goal.
Assume H _ .
An
exact proof term for the current goal is
H (SNoLev x + SNoLev w ) L4a .
We prove the intermediate
claim L4c :
v ⊆ SNoLev (x + w ) .
rewrite the current goal using H3 (from left to right) at position 1.
An exact proof term for the current goal is H2 .
An exact proof term for the current goal is H2 .
Apply LIHw to the current goal.
Apply L4c to the current goal.
Apply H1 to the current goal.
An exact proof term for the current goal is L4a .
∎
Proof: Let x be given.
Assume Hx .
Let y be given.
Assume Hy .
An
exact proof term for the current goal is
SNo_add_SNo x y Hx3 Hy3 .
Assume H1 .
An exact proof term for the current goal is H1 .
Apply H1 to the current goal.
An
exact proof term for the current goal is
SNo_add_SNo x y Hx3 Hy3 .
∎
Proof: Let x and y be given.
Assume Hx Hy .
Use transitivity with x + (y + - y ) , and x + 0 .
An
exact proof term for the current goal is
add_SNo_0R x Hx .
∎
Proof: Let x and y be given.
Assume Hx Hy .
rewrite the current goal using
minus_SNo_invol y Hy (from right to left) at position 2.
∎
Proof: Let x and y be given.
Assume Hx Hy .
We will prove (x + y ) + - x = y .
rewrite the current goal using
add_SNo_com x y Hx Hy (from left to right).
We will prove (y + x ) + - x = y .
∎
Proof: Let x and y be given.
Assume Hx Hy .
rewrite the current goal using
minus_SNo_invol x Hx (from right to left) at position 1.
∎
Proof: Let x, y and z be given.
Assume Hx Hy Hz H1 .
We will prove x < z .
We prove the intermediate claim L1 : (x + y ) + - y = x .
We prove the intermediate claim L2 : (z + y ) + - y = z .
rewrite the current goal using L1 (from right to left).
rewrite the current goal using L2 (from right to left).
We will prove (x + y ) + - y < (z + y ) + - y .
∎
Proof: Let x, y and z be given.
Assume Hx Hy Hz .
rewrite the current goal using
add_SNo_com x y Hx Hy (from left to right).
rewrite the current goal using
add_SNo_com x z Hx Hz (from left to right).
∎
Proof: Let x, y, z and w be given.
Assume Hx Hy Hz Hw .
Use transitivity with (x + y ) + z + w , and ((x + y ) + z ) + w .
Use f_equal.
Use symmetry.
An
exact proof term for the current goal is
add_SNo_assoc x y z Hx Hy Hz .
∎
Proof: Let x, y and z be given.
Assume Hx Hy Hz .
rewrite the current goal using
add_SNo_assoc x y z Hx Hy Hz (from left to right).
rewrite the current goal using
add_SNo_assoc y x z Hy Hx Hz (from left to right).
Use f_equal.
An
exact proof term for the current goal is
add_SNo_com x y Hx Hy .
∎
Proof: Let x, y and z be given.
Assume Hx Hy Hz .
rewrite the current goal using
add_SNo_assoc x y z Hx Hy Hz (from right to left).
rewrite the current goal using
add_SNo_assoc x z y Hx Hz Hy (from right to left).
Use f_equal.
An
exact proof term for the current goal is
add_SNo_com y z Hy Hz .
∎
Proof: Let x, y, z and w be given.
Assume Hx Hy Hz Hw .
We will prove ((x + y ) + z ) + w = (x + z ) + (y + w ) .
We will prove ((x + z ) + y ) + w = (x + z ) + (y + w ) .
Use symmetry.
∎
Proof: Let x, y and z be given.
Assume Hx Hy Hz .
We will prove x + (y + z ) = z + (x + y ) .
Use transitivity with x + (z + y ) , (x + z ) + y , and (z + x ) + y .
Use f_equal.
An
exact proof term for the current goal is
add_SNo_com y z Hy Hz .
An
exact proof term for the current goal is
add_SNo_assoc x z y Hx Hz Hy .
Use f_equal.
An
exact proof term for the current goal is
add_SNo_com x z Hx Hz .
Use symmetry.
An
exact proof term for the current goal is
add_SNo_assoc z x y Hz Hx Hy .
∎
Proof: Let x, y, z and w be given.
Assume Hx Hy Hz Hw .
We will prove x + w + y + z = w + x + y + z .
∎
Proof: Let x, y, z, w and v be given.
Assume Hx Hy Hz Hw Hv .
rewrite the current goal using
add_SNo_rotate_4_1 y z w v Hy Hz Hw Hv (from left to right).
We will prove x + v + y + z + w = v + x + y + z + w .
∎
Proof: Let x, y, z, w and v be given.
Assume Hx Hy Hz Hw Hv .
Use transitivity with and (v + x + y + z + w ) .
∎
Proof: Let x, y, z and w be given.
Assume Hx Hy Hz Hw .
rewrite the current goal using
add_SNo_assoc x y z Hx Hy Hz (from left to right).
We will prove ((x + y ) + z ) + (- z + w ) = x + y + w .
We will prove (x + y ) + (z + - z + w ) = x + y + w .
We will prove (x + y ) + w = x + y + w .
Use symmetry.
An
exact proof term for the current goal is
add_SNo_assoc x y w Hx Hy Hw .
∎
Proof: Let x, y, z and w be given.
Assume Hx Hy Hz Hw .
We will prove (x + y + z ) + (- z + w ) = x + y + w .
∎
Proof: Let x, y, z and w be given.
Assume Hx Hy Hz Hw .
We will prove (x + y + - z ) + (z + w ) = x + y + w .
rewrite the current goal using
minus_SNo_invol z Hz (from right to left) at position 2.
We will prove (x + y + - z ) + (- - z + w ) = x + y + w .
∎
Proof: Let x, y and z be given.
Assume Hx Hy Hz H1 .
We will prove x + - y < (z + y ) + - y .
rewrite the current goal using
add_SNo_0R z Hz (from left to right).
An exact proof term for the current goal is H1 .
∎
Proof: Let x, y and z be given.
Assume Hx Hy Hz H1 .
We will prove (z + y ) + - y < x + - y .
We will prove z + y + - y < x + - y .
rewrite the current goal using
add_SNo_0R z Hz (from left to right).
An exact proof term for the current goal is H1 .
∎
Proof: Let x, y and z be given.
Assume Hx Hy Hz H1 .
We will prove (x + - y ) + y < z + y .
rewrite the current goal using
add_SNo_0R x Hx (from left to right).
An exact proof term for the current goal is H1 .
∎
Proof: Let x, y and z be given.
Assume Hx Hy Hz H1 .
We will prove z + y < (x + - y ) + y .
rewrite the current goal using
add_SNo_0R x Hx (from left to right).
An exact proof term for the current goal is H1 .
∎
Proof: Let x, y, z and w be given.
Assume Hx Hy Hz Hw H1 .
We will prove x + y + - z < w .
We will prove (x + y ) + - z < w .
An exact proof term for the current goal is H1 .
∎
Proof: Let x, y, z and w be given.
Assume Hx Hy Hz Hw H1 .
We will prove w < x + y + - z .
We will prove w < (x + y ) + - z .
An exact proof term for the current goal is H1 .
∎
Proof: Let x, y, z, u, v and w be given.
Assume Hx Hy Hz Hu Hv Hw H1 .
We prove the intermediate
claim Lmz :
SNo (- z ) .
We prove the intermediate
claim Lmw :
SNo (- w ) .
We prove the intermediate
claim Lxy :
SNo (x + y ) .
An
exact proof term for the current goal is
SNo_add_SNo x y Hx Hy .
We prove the intermediate
claim Luv :
SNo (u + v ) .
An
exact proof term for the current goal is
SNo_add_SNo u v Hu Hv .
rewrite the current goal using
add_SNo_assoc x y (- z ) Hx Hy Lmz (from left to right).
rewrite the current goal using
add_SNo_assoc u v (- w ) Hu Hv Lmw (from left to right).
We will prove (x + y ) + - z < (u + v ) + - w .
We will prove ((x + y ) + - z ) + w < u + v .
rewrite the current goal using
add_SNo_assoc (x + y ) (- z ) w Lxy Lmz Hw (from right to left).
We will prove (x + y ) + - z + w < u + v .
rewrite the current goal using
add_SNo_com (- z ) w Lmz Hw (from left to right).
We will prove (x + y ) + w + - z < u + v .
rewrite the current goal using
add_SNo_assoc (x + y ) w (- z ) Lxy Hw Lmz (from left to right).
We will prove ((x + y ) + w ) + - z < u + v .
We will prove (x + y ) + w < (u + v ) + z .
rewrite the current goal using
add_SNo_assoc x y w Hx Hy Hw (from right to left).
rewrite the current goal using
add_SNo_assoc u v z Hu Hv Hz (from right to left).
An exact proof term for the current goal is H1 .
∎
Proof: Let x, y and z be given.
Assume Hx Hy Hz H1 .
Assume H2 : z = x + - y .
We will prove z + y ≤ x .
rewrite the current goal using H2 (from left to right).
We will prove (x + - y ) + y ≤ x .
∎
Proof: Let x, y and z be given.
Assume Hx Hy Hz H1 .
Assume H2 : z + y = x .
We will prove z ≤ x + - y .
rewrite the current goal using H2 (from right to left).
We will prove z ≤ (z + y ) + - y .
∎
Proof: Let x, y, z, w, u and v be given.
Assume Hx Hy Hz Hw Hu Hv H1 H2 .
We will prove (x + y ) + (u + v ) < (z + w ) + (u + v ) .
We will prove (x + u ) + (y + v ) < (z + w ) + (u + v ) .
We prove the intermediate claim L1 : (z + w ) + (u + v ) = (z + v ) + (w + u ) .
We will prove z + (w + (u + v ) ) = z + (v + (w + u ) ) .
Use f_equal.
We will prove w + u + v = v + w + u .
rewrite the current goal using L1 (from left to right).
We will prove (x + u ) + (y + v ) < (z + v ) + (w + u ) .
∎
Proof: Let x, y, z, w, u and a be given.
Assume Hx Hy Hz Hw Hu Ha H1 H2 .
We will prove x + y + z < y + w + a .
rewrite the current goal using
add_SNo_com_3_0_1 x y z Hx Hy Hz (from left to right).
We will prove y + x + z < y + w + a .
An exact proof term for the current goal is H1 .
We will prove y + w + a < w + u .
We will prove w + a + y < w + u .
We will prove a + y < u .
rewrite the current goal using
add_SNo_com a y Ha Hy (from left to right).
An exact proof term for the current goal is H2 .
∎
Proof: Let x, y, w, u, v and a be given.
Assume Hx Hy Hw Hu Hv Ha H1 H2 .
rewrite the current goal using
add_SNo_com x y Hx Hy (from left to right).
We will prove y + x < w + u + v .
We will prove y + x < u + v + w .
rewrite the current goal using
add_SNo_0R x Hx (from right to left).
We will prove y + x + 0 < u + v + w .
We will prove y + 0 < u + a .
rewrite the current goal using
add_SNo_0R y Hy (from left to right).
rewrite the current goal using
add_SNo_com u a Hu Ha (from left to right).
An exact proof term for the current goal is H2 .
We will prove x + a < v + w .
rewrite the current goal using
add_SNo_com v w Hv Hw (from left to right).
An exact proof term for the current goal is H1 .
∎
Proof: Let x, y, z, w, u, a, b and c be given.
Assume Hx Hy Hz Hw Hu Ha Hb Hc H1 H2 H3 .
We prove the intermediate claim L1 : x + z < c + w .
We will prove x + a < c + b .
rewrite the current goal using
add_SNo_com c b Hc Hb (from left to right).
An exact proof term for the current goal is H1 .
We will prove z + b < w + a .
rewrite the current goal using
add_SNo_com z b Hz Hb (from left to right).
An exact proof term for the current goal is H3 .
We prove the intermediate
claim Lxz :
SNo (x + z ) .
An
exact proof term for the current goal is
SNo_add_SNo x z Hx Hz .
We prove the intermediate
claim Lcw :
SNo (c + w ) .
An
exact proof term for the current goal is
SNo_add_SNo c w Hc Hw .
Apply SNoLt_tra (x + y + z ) (c + w + y ) (w + u ) to the current goal.
An
exact proof term for the current goal is
SNo_add_SNo w u Hw Hu .
We will prove x + y + z < c + w + y .
rewrite the current goal using
add_SNo_com y z Hy Hz (from left to right).
We will prove x + z + y < c + w + y .
rewrite the current goal using
add_SNo_assoc x z y Hx Hz Hy (from left to right).
rewrite the current goal using
add_SNo_assoc c w y Hc Hw Hy (from left to right).
An
exact proof term for the current goal is
add_SNo_Lt1 (x + z ) y (c + w ) Lxz Hy Lcw L1 .
We will prove c + w + y < w + u .
We will prove w + y + c < w + u .
We will prove y + c < u .
An exact proof term for the current goal is H2 .
∎
Proof: Let x, y, w, u, v, a, b and c be given.
Assume Hx Hy Hw Hu Hv Ha Hb Hc H1 H2 H3 .
We prove the intermediate claim L1 : b + y < w + u + a .
An
exact proof term for the current goal is
add_SNo_Lt_subprop3b b y w u a c Hb Hy Hw Hu Ha Hc H3 H2 .
We prove the intermediate
claim Lxy :
SNo (x + y ) .
An
exact proof term for the current goal is
SNo_add_SNo x y Hx Hy .
We prove the intermediate
claim Lwuv :
SNo (w + u + v ) .
We prove the intermediate
claim Lwua :
SNo (w + u + a ) .
We prove the intermediate
claim Lby :
SNo (b + y ) .
An
exact proof term for the current goal is
SNo_add_SNo b y Hb Hy .
We will prove (x + y ) + b < (w + u + v ) + b .
We will prove (x + y ) + b < x + w + u + a .
rewrite the current goal using
add_SNo_assoc x y b Hx Hy Hb (from right to left).
We will prove x + y + b < x + w + u + a .
rewrite the current goal using
add_SNo_com y b Hy Hb (from left to right).
We will prove x + b + y < x + w + u + a .
Apply add_SNo_Lt2 x (b + y ) (w + u + a ) Hx Lby Lwua to the current goal.
We will prove b + y < w + u + a .
An exact proof term for the current goal is L1 .
We will prove x + w + u + a < (w + u + v ) + b .
We prove the intermediate claim L2 : x + w + u + a = (w + u ) + (x + a ) .
Use transitivity with (x + w + u ) + a , (w + u + x ) + a , and w + u + x + a .
An
exact proof term for the current goal is
add_SNo_assoc_4 x w u a Hx Hw Hu Ha .
Use f_equal.
Use symmetry.
Use symmetry.
An
exact proof term for the current goal is
add_SNo_assoc_4 w u x a Hw Hu Hx Ha .
We will prove w + u + x + a = (w + u ) + (x + a ) .
We prove the intermediate claim L3 : (w + u + v ) + b = (w + u ) + b + v .
Use transitivity with ((w + u ) + v ) + b , and (w + u ) + (v + b ) .
Use f_equal.
An
exact proof term for the current goal is
add_SNo_assoc w u v Hw Hu Hv .
Use f_equal.
An
exact proof term for the current goal is
add_SNo_com v b Hv Hb .
rewrite the current goal using L2 (from left to right).
rewrite the current goal using L3 (from left to right).
We will prove (w + u ) + (x + a ) < (w + u ) + (b + v ) .
An exact proof term for the current goal is H1 .
∎
Proof: Let alpha be given.
Assume Ha .
rewrite the current goal using
add_SNo_0L alpha (ordinal_SNo alpha Ha ) (from right to left) at position 1.
We will
prove ordsucc (0 + alpha ) = 1 + alpha .
Use symmetry.
∎
Theorem. (
add_SNo_3a_2b ) The following is provable:
∀x y z w u, SNo x → SNo y → SNo z → SNo w → SNo u → (x + y + z ) + (w + u ) = (u + y + z ) + (w + x )
Proof: Let x, y, z, w and u be given.
Assume Hx Hy Hz Hw Hu .
We will prove (w + u ) + (x + y + z ) = (u + y + z ) + (w + x ) .
We will prove (w + x ) + (u + y + z ) = (u + y + z ) + (w + x ) .
∎
Proof: Let n be given.
Assume Hn .
rewrite the current goal using
add_nat_0R (from left to right).
Use reflexivity.
∎
Proof: Let x be given.
Assume Hx .
Let n be given.
Assume Hn .
rewrite the current goal using
add_SNo_0R x Hx (from right to left) at position 1.
We will
prove x + 0 < x + eps_ n .
An
exact proof term for the current goal is
SNo_eps_pos n Hn .
∎
Proof: Let x and y be given.
Assume Hx Hy .
Let n be given.
Assume Hn .
Assume Hxy .
We will
prove y < y + eps_ n .
∎
Proof: Let x and y be given.
Assume Hx Hy Hxy .
We will prove 0 + x < y .
rewrite the current goal using
add_SNo_0L x Hx (from left to right).
An exact proof term for the current goal is Hxy .
∎
Proof: Let m and n be given.
Assume Hn .
We prove the intermediate
claim Ln :
SNo n .
An exact proof term for the current goal is Hn .
We will prove m ∈ n + 0 → m ∈ n ∨ m + - n ∈ 0 .
rewrite the current goal using
add_SNo_0R n Ln (from left to right).
Assume H1 .
Apply orIL to the current goal.
An exact proof term for the current goal is H1 .
Let k be given.
Assume Hk .
Assume IHk : m ∈ n + k → m ∈ n ∨ m + - n ∈ k .
Apply ordsuccE (n + k ) m H1 to the current goal.
Assume H2 : m ∈ n + k .
Apply IHk H2 to the current goal.
Assume H3 : m ∈ n .
Apply orIL to the current goal.
An exact proof term for the current goal is H3 .
Assume H3 : m + - n ∈ k .
Apply orIR to the current goal.
An exact proof term for the current goal is H3 .
Assume H2 : m = n + k .
Apply orIR to the current goal.
rewrite the current goal using H2 (from left to right).
We will
prove (n + k ) + - n ∈ ordsucc k .
∎
Theorem. (
add_SNo_Lt4 ) The following is provable:
∀x y z w u v, SNo x → SNo y → SNo z → SNo w → SNo u → SNo v → x < w → y < u → z < v → x + y + z < w + u + v
Proof: Let x, y, z, w, u and v be given.
Assume Hx Hy Hz Hw Hu Hv Hxw Hyu Hzv .
We will prove x + y + z < w + u + v .
We will prove y + z < u + v .
An
exact proof term for the current goal is
add_SNo_Lt3 y z u v Hy Hz Hu Hv Hyu Hzv .
∎
Proof: Let x, y, z, w and u be given.
Assume Hx Hy Hz Hw Hu H1 .
rewrite the current goal using
add_SNo_assoc x y u Hx Hy Hu (from left to right).
rewrite the current goal using
add_SNo_assoc z w u Hz Hw Hu (from left to right).
We will prove (x + y ) + u < (z + w ) + u .
∎
Proof: Let x, y, z, w and u be given.
Assume Hx Hy Hz Hw Hu H1 .
We will prove y + x + u < z + w + u .
An
exact proof term for the current goal is
add_SNo_3_3_3_Lt1 y x z w u Hy Hx Hz Hw Hu H1 .
∎
End of Section SurrealAdd