Primitive . The name
Eps_i is a term of type
(set → prop → set .
Axiom. (
Eps_i_ax ) We take the following as an axiom:
∀P : set → prop ∀x : set , P x P (Eps_i P Definition. We define
True to be
∀p : prop , p → p of type
prop .
Definition. We define
False to be
∀p : prop , p of type
prop .
Definition. We define
not to be
λA : prop ⇒ A → False of type
prop → prop .
Notation . We use
¬ as a prefix operator with priority 700 corresponding to applying term
not .
Definition. We define
and to be
λA B : prop ⇒ ∀p : prop , (A → B → p → p of type
prop → prop → prop .
Notation . We use
∧ as an infix operator with priority 780 and which associates to the left corresponding to applying term
and .
Definition. We define
or to be
λA B : prop ⇒ ∀p : prop , (A → p → (B → p → p of type
prop → prop → prop .
Notation . We use
∨ as an infix operator with priority 785 and which associates to the left corresponding to applying term
or .
Definition. We define
iff to be
λA B : prop ⇒ and (A → B (B → A of type
prop → prop → prop .
Notation . We use
↔ as an infix operator with priority 805 and no associativity corresponding to applying term
iff .
Beginning of Section Eq
Variable A : SType
Definition. We define
eq to be
λx y : A ⇒ ∀Q : A → A → prop Q x y Q y x of type
A → A → prop .
Definition. We define
neq to be
λx y : A ⇒ ¬ eq x y of type
A → A → prop .
End of Section Eq
Notation . We use
= as an infix operator with priority 502 and no associativity corresponding to applying term
eq .
Notation . We use
≠ as an infix operator with priority 502 and no associativity corresponding to applying term
neq .
Beginning of Section FE
Variable A B : SType
Axiom. (
func_ext ) We take the following as an axiom:
∀f g : A → B (∀x : A , f x = g x ) → f = g End of Section FE
Beginning of Section Ex
Variable A : SType
Definition. We define
ex to be
λQ : A → prop ∀P : prop , (∀x : A , Q x P ) → P of type
(A → prop → prop .
End of Section Ex
Notation . We use
∃ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
ex .
Axiom. (
prop_ext ) We take the following as an axiom:
∀p q : prop , iff p q p = q Primitive . The name
In is a term of type
set → set → prop .
Notation . We use
∈ as an infix operator with priority 500 and no associativity corresponding to applying term
In . Furthermore, we may write
∀ x ∈ A , B to mean
∀ x : set, x ∈ A → B .
Definition. We define
Subq to be
λA B ⇒ ∀ x ∈ A , x ∈ B of type
set → set → prop .
Notation . We use
⊆ as an infix operator with priority 500 and no associativity corresponding to applying term
Subq . Furthermore, we may write
∀ x ⊆ A , B to mean
∀ x : set, x ⊆ A → B .
Axiom. (
set_ext ) We take the following as an axiom:
∀X Y : set , X ⊆ Y Y ⊆ X X = Y Axiom. (
In_ind ) We take the following as an axiom:
∀P : set → prop (∀X : set , (∀ x ∈ X , P x → P X ) → ∀X : set , P X Notation . We use
∃ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
ex and handling ∈ or ⊆ ascriptions using
and .
Primitive . The name
Empty is a term of type
set .
Axiom. (
EmptyAx ) We take the following as an axiom:
Primitive . The name
⋃ is a term of type
set → set .
Axiom. (
UnionEq ) We take the following as an axiom:
Primitive . The name
𝒫 is a term of type
set → set .
Axiom. (
PowerEq ) We take the following as an axiom:
∀X Y : set , Y ∈ 𝒫 X ↔ Y ⊆ X Primitive . The name
Repl is a term of type
set → (set → set → set .
Notation .
{B | x ∈ A } is notation for
Repl A (λ x . B ).
Axiom. (
ReplEq ) We take the following as an axiom:
∀A : set , ∀F : set → set ∀y : set , y ∈ { F x | x ∈ A } ↔ ∃ x ∈ A , y = F x Definition. We define
TransSet to be
λU : set ⇒ ∀ x ∈ U , x ⊆ U of type
set → prop .
Definition. We define
Union_closed to be
λU : set ⇒ ∀X : set , X ∈ U ⋃ X ∈ U of type
set → prop .
Definition. We define
Power_closed to be
λU : set ⇒ ∀X : set , X ∈ U 𝒫 X ∈ U of type
set → prop .
Definition. We define
Repl_closed to be
λU : set ⇒ ∀X : set , X ∈ U ∀F : set → set (∀x : set , x ∈ X F x ∈ U ) → { F x | x ∈ X } ∈ U of type
set → prop .
Primitive . The name
UnivOf is a term of type
set → set .
Axiom. (
UnivOf_In ) We take the following as an axiom:
Axiom. (
UnivOf_Min ) We take the following as an axiom:
Axiom. (
FalseE ) We take the following as an axiom:
Axiom. (
TrueI ) We take the following as an axiom:
Axiom. (
andI ) We take the following as an axiom:
∀A B : prop , A → B → A ∧ B Axiom. (
andEL ) We take the following as an axiom:
Axiom. (
andER ) We take the following as an axiom:
Axiom. (
orIL ) We take the following as an axiom:
Axiom. (
orIR ) We take the following as an axiom:
Beginning of Section PropN
Variable P1 P2 P3 : prop
Axiom. (
and3I ) We take the following as an axiom:
P1 → P2 → P3 → P1 ∧ P2 ∧ P3 Axiom. (
and3E ) We take the following as an axiom:
P1 ∧ P2 ∧ P3 (∀p : prop , (P1 → P2 → P3 → p → p ) Axiom. (
or3I1 ) We take the following as an axiom:
Axiom. (
or3I2 ) We take the following as an axiom:
Axiom. (
or3I3 ) We take the following as an axiom:
Axiom. (
or3E ) We take the following as an axiom:
P1 ∨ P2 ∨ P3 (∀p : prop , (P1 → p → (P2 → p → (P3 → p → p ) Variable P4 : prop
Axiom. (
and4I ) We take the following as an axiom:
P1 → P2 → P3 → P4 → P1 ∧ P2 ∧ P3 ∧ P4 Variable P5 : prop
Axiom. (
and5I ) We take the following as an axiom:
P1 → P2 → P3 → P4 → P5 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 End of Section PropN
Axiom. (
iffI ) We take the following as an axiom:
∀A B : prop , (A → B → (B → A → (A ↔ B Axiom. (
iffEL ) We take the following as an axiom:
∀A B : prop , (A ↔ B → A → B Axiom. (
iffER ) We take the following as an axiom:
∀A B : prop , (A ↔ B → B → A Axiom. (
iff_refl ) We take the following as an axiom:
Axiom. (
iff_sym ) We take the following as an axiom:
∀A B : prop , (A ↔ B → (B ↔ A Axiom. (
iff_trans ) We take the following as an axiom:
∀A B C : prop , (A ↔ B → (B ↔ C → (A ↔ C Axiom. (
eq_i_tra ) We take the following as an axiom:
∀x y z, x = y y = z x = z Axiom. (
f_eq_i ) We take the following as an axiom:
∀f : set → set ∀x y, x = y f x = f y Axiom. (
neq_i_sym ) We take the following as an axiom:
Definition. We define
nIn to be
λx X ⇒ ¬ In x X of type
set → set → prop .
Notation . We use
∉ as an infix operator with priority 502 and no associativity corresponding to applying term
nIn .
Axiom. (
Eps_i_ex ) We take the following as an axiom:
∀P : set → prop (∃ x, P x → P (Eps_i P Axiom. (
pred_ext ) We take the following as an axiom:
∀P Q : set → prop (∀x, P x ↔ Q x ) → P = Q Axiom. (
prop_ext_2 ) We take the following as an axiom:
∀p q : prop , (p → q → (q → p → p = q Axiom. (
Subq_ref ) We take the following as an axiom:
Axiom. (
Subq_tra ) We take the following as an axiom:
∀X Y Z : set , X ⊆ Y Y ⊆ Z X ⊆ Z Axiom. (
Subq_contra ) We take the following as an axiom:
∀X Y z : set , X ⊆ Y z ∉ Y z ∉ X Axiom. (
EmptyE ) We take the following as an axiom:
Axiom. (
Subq_Empty ) We take the following as an axiom:
Axiom. (
Empty_eq ) We take the following as an axiom:
Axiom. (
UnionI ) We take the following as an axiom:
∀X x Y : set , x ∈ Y Y ∈ X x ∈ ⋃ X Axiom. (
UnionE ) We take the following as an axiom:
∀X x : set , x ∈ ⋃ X ∃ Y : set , x ∈ Y ∧ Y ∈ X Axiom. (
UnionE_impred ) We take the following as an axiom:
∀X x : set , x ∈ ⋃ X ∀p : prop , (∀Y : set , x ∈ Y Y ∈ X p ) → p Axiom. (
PowerI ) We take the following as an axiom:
∀X Y : set , Y ⊆ X Y ∈ 𝒫 X Axiom. (
PowerE ) We take the following as an axiom:
∀X Y : set , Y ∈ 𝒫 X Y ⊆ X Axiom. (
xm ) We take the following as an axiom:
Axiom. (
dneg ) We take the following as an axiom:
Axiom. (
eq_or_nand ) We take the following as an axiom:
Primitive . The name
exactly1of2 is a term of type
prop → prop → prop .
Axiom. (
exactly1of2_E ) We take the following as an axiom:
∀A B : prop , exactly1of2 A B ∀p : prop , (A → ¬ B p → (¬ A B → p → p Axiom. (
ReplI ) We take the following as an axiom:
∀A : set , ∀F : set → set ∀x : set , x ∈ A F x ∈ { F x | x ∈ A } Axiom. (
ReplE ) We take the following as an axiom:
∀A : set , ∀F : set → set ∀y : set , y ∈ { F x | x ∈ A } ∃ x ∈ A , y = F x Axiom. (
ReplE_impred ) We take the following as an axiom:
∀A : set , ∀F : set → set ∀y : set , y ∈ { F x | x ∈ A } ∀p : prop , (∀x : set , x ∈ A y = F x p ) → p Axiom. (
ReplE' ) We take the following as an axiom:
∀X, ∀f : set → set ∀p : set → prop (∀ x ∈ X , p (f x → ∀ y ∈ { f x | x ∈ X } , p y Axiom. (
Repl_Empty ) We take the following as an axiom:
Axiom. (
ReplEq_ext ) We take the following as an axiom:
∀X, ∀F G : set → set (∀ x ∈ X , F x = G x → { F x | x ∈ X } = { G x | x ∈ X } Axiom. (
Repl_inv_eq ) We take the following as an axiom:
∀P : set → prop ∀f g : set → set (∀x, P x g (f x = x ) → ∀X, (∀ x ∈ X , P x → { g y | y ∈ { f x | x ∈ X } } = X Axiom. (
Repl_invol_eq ) We take the following as an axiom:
∀P : set → prop ∀f : set → set (∀x, P x f (f x = x ) → ∀X, (∀ x ∈ X , P x → { f y | y ∈ { f x | x ∈ X } } = X Primitive . The name
If_i is a term of type
prop → set → set → set .
Notation .
if cond then T else E is notation corresponding to
If_i type cond T E where
type is the inferred type of
T .
Axiom. (
If_i_0 ) We take the following as an axiom:
Axiom. (
If_i_1 ) We take the following as an axiom:
Axiom. (
If_i_or ) We take the following as an axiom:
Primitive . The name
UPair is a term of type
set → set → set .
Notation .
{x ,y } is notation for
UPair x y .
Axiom. (
UPairE ) We take the following as an axiom:
∀x y z : set , x ∈ { y , z } x = y ∨ x = z Axiom. (
UPairI1 ) We take the following as an axiom:
Axiom. (
UPairI2 ) We take the following as an axiom:
Primitive . The name
Sing is a term of type
set → set .
Notation .
{x } is notation for
Sing x .
Axiom. (
SingI ) We take the following as an axiom:
Axiom. (
SingE ) We take the following as an axiom:
∀x y : set , y ∈ { x } y = x Primitive . The name
binunion is a term of type
set → set → set .
Notation . We use
∪ as an infix operator with priority 345 and which associates to the left corresponding to applying term
binunion .
Axiom. (
binunionI1 ) We take the following as an axiom:
∀X Y z : set , z ∈ X z ∈ X ∪ Y Axiom. (
binunionI2 ) We take the following as an axiom:
∀X Y z : set , z ∈ Y z ∈ X ∪ Y Axiom. (
binunionE ) We take the following as an axiom:
∀X Y z : set , z ∈ X ∪ Y z ∈ X ∨ z ∈ Y Axiom. (
binunionE' ) We take the following as an axiom:
∀X Y z, ∀p : prop , (z ∈ X p → (z ∈ Y p → (z ∈ X ∪ Y p Axiom. (
binunion_asso ) We take the following as an axiom:
∀X Y Z : set , X ∪ (Y ∪ Z = (X ∪ Y ∪ Z Axiom. (
binunion_com ) We take the following as an axiom:
∀X Y : set , X ∪ Y = Y ∪ X Definition. We define
SetAdjoin to be
λX y ⇒ X ∪ { y } of type
set → set → set .
Notation . We now use the set enumeration notation
{...,...,...} in general. If 0 elements are given, then
Empty is used to form the corresponding term. If 1 element is given, then
Sing is used to form the corresponding term. If 2 elements are given, then
UPair is used to form the corresponding term. If more than elements are given, then
SetAdjoin is used to reduce to the case with one fewer elements.
Primitive . The name
famunion is a term of type
set → (set → set → set .
Notation . We use
⋃ x [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
famunion .
Axiom. (
famunionI ) We take the following as an axiom:
∀X : set , ∀F : (set → set , ∀x y : set , x ∈ X y ∈ F x y ∈ ⋃ x ∈ X F x Axiom. (
famunionE ) We take the following as an axiom:
∀X : set , ∀F : (set → set , ∀y : set , y ∈ (⋃ x ∈ X F x ∃ x ∈ X , y ∈ F x Axiom. (
famunionE_impred ) We take the following as an axiom:
∀X : set , ∀F : (set → set , ∀y : set , y ∈ (⋃ x ∈ X F x ∀p : prop , (∀x, x ∈ X y ∈ F x p ) → p
Beginning of Section SepSec
Variable X : set
Variable P : set → prop
Let z : set ≝ Eps_i (λz ⇒ z ∈ X ∧ P z ) Primitive . The name
Sep is a term of type
set .
End of Section SepSec
Notation .
{x ∈ A | B } is notation for
Sep A (λ x . B ).
Axiom. (
SepI ) We take the following as an axiom:
∀X : set , ∀P : (set → prop , ∀x : set , x ∈ X P x x ∈ { x ∈ X | P x } Axiom. (
SepE ) We take the following as an axiom:
∀X : set , ∀P : (set → prop , ∀x : set , x ∈ { x ∈ X | P x } x ∈ X ∧ P x Axiom. (
SepE1 ) We take the following as an axiom:
∀X : set , ∀P : (set → prop , ∀x : set , x ∈ { x ∈ X | P x } x ∈ X Axiom. (
SepE2 ) We take the following as an axiom:
∀X : set , ∀P : (set → prop , ∀x : set , x ∈ { x ∈ X | P x } P x Axiom. (
Sep_Subq ) We take the following as an axiom:
∀X : set , ∀P : set → prop { x ∈ X | P x } ⊆ X Axiom. (
Sep_In_Power ) We take the following as an axiom:
∀X : set , ∀P : set → prop { x ∈ X | P x } ∈ 𝒫 X Primitive . The name
ReplSep is a term of type
set → (set → prop → (set → set → set .
Notation .
{B | x ∈ A , C } is notation for
ReplSep A (λ x . C ) (λ x . B ).
Axiom. (
ReplSepI ) We take the following as an axiom:
∀X : set , ∀P : set → prop ∀F : set → set ∀x : set , x ∈ X P x F x ∈ { F x | x ∈ X , P x } Axiom. (
ReplSepE ) We take the following as an axiom:
∀X : set , ∀P : set → prop ∀F : set → set ∀y : set , y ∈ { F x | x ∈ X , P x } ∃ x : set , x ∈ X ∧ P x ∧ y = F x Axiom. (
ReplSepE_impred ) We take the following as an axiom:
∀X : set , ∀P : set → prop ∀F : set → set ∀y : set , y ∈ { F x | x ∈ X , P x } ∀p : prop , (∀ x ∈ X , P x y = F x p → p Primitive . The name
binintersect is a term of type
set → set → set .
Notation . We use
∩ as an infix operator with priority 340 and which associates to the left corresponding to applying term
binintersect .
Axiom. (
binintersectI ) We take the following as an axiom:
∀X Y z, z ∈ X z ∈ Y z ∈ X ∩ Y Axiom. (
binintersectE ) We take the following as an axiom:
∀X Y z, z ∈ X ∩ Y z ∈ X ∧ z ∈ Y Primitive . The name
setminus is a term of type
set → set → set .
Notation . We use
∖ as an infix operator with priority 350 and no associativity corresponding to applying term
setminus .
Axiom. (
setminusI ) We take the following as an axiom:
∀X Y z, (z ∈ X → (z ∉ Y → z ∈ X ∖ Y Axiom. (
setminusE ) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y → z ∈ X ∧ z ∉ Y Axiom. (
setminusE1 ) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y → z ∈ X Axiom. (
In_irref ) We take the following as an axiom:
Axiom. (
In_no2cycle ) We take the following as an axiom:
Primitive . The name
ordsucc is a term of type
set → set .
Axiom. (
ordsuccI1 ) We take the following as an axiom:
Axiom. (
ordsuccI2 ) We take the following as an axiom:
Axiom. (
ordsuccE ) We take the following as an axiom:
Notation . Natural numbers 0,1,2,... are notation for the terms formed using
Empty as 0 and forming successors with
ordsucc .
Axiom. (
ordsucc_inj ) We take the following as an axiom:
Axiom. (
In_0_1 ) We take the following as an axiom:
Axiom. (
In_0_2 ) We take the following as an axiom:
Axiom. (
In_1_2 ) We take the following as an axiom:
Definition. We define
nat_p to be
λn : set ⇒ ∀p : set → prop p 0 (∀x : set , p x p (ordsucc x ) → p n of type
set → prop .
Axiom. (
nat_0 ) We take the following as an axiom:
Axiom. (
nat_ordsucc ) We take the following as an axiom:
Axiom. (
nat_1 ) We take the following as an axiom:
Axiom. (
nat_2 ) We take the following as an axiom:
Axiom. (
nat_ind ) We take the following as an axiom:
Axiom. (
nat_inv ) We take the following as an axiom:
Axiom. (
nat_p_trans ) We take the following as an axiom:
Axiom. (
nat_trans ) We take the following as an axiom:
Axiom. (
cases_1 ) We take the following as an axiom:
∀ i ∈ 1 , ∀p : set → prop p 0 p i Axiom. (
cases_2 ) We take the following as an axiom:
∀ i ∈ 2 , ∀p : set → prop p 0 p 1 p i Axiom. (
cases_3 ) We take the following as an axiom:
∀ i ∈ 3 , ∀p : set → prop p 0 p 1 p 2 p i Axiom. (
neq_0_1 ) We take the following as an axiom:
Axiom. (
neq_1_0 ) We take the following as an axiom:
Axiom. (
neq_0_2 ) We take the following as an axiom:
Axiom. (
neq_2_0 ) We take the following as an axiom:
Axiom. (
neq_1_2 ) We take the following as an axiom:
Axiom. (
ZF_closed_E ) We take the following as an axiom:
Primitive . The name
ω is a term of type
set .
Axiom. (
omega_nat_p ) We take the following as an axiom:
Axiom. (
nat_p_omega ) We take the following as an axiom:
Axiom. (
ordinal_1 ) We take the following as an axiom:
Axiom. (
ordinal_2 ) We take the following as an axiom:
Axiom. (
ordinal_ind ) We take the following as an axiom:
∀p : set → prop (∀alpha, ordinal alpha (∀ beta ∈ alpha , p beta → p alpha ) → ∀alpha, ordinal alpha p alpha Definition. We define
inj to be
λX Y f ⇒ (∀ u ∈ X , f u ∈ Y ∧ (∀ u v ∈ X , f u = f v u = v of type
set → set → (set → set → prop .
Definition. We define
bij to be
λX Y f ⇒ (∀ u ∈ X , f u ∈ Y ∧ (∀ u v ∈ X , f u = f v u = v ∧ (∀ w ∈ Y , ∃ u ∈ X , f u = w of type
set → set → (set → set → prop .
Axiom. (
bijI ) We take the following as an axiom:
∀X Y, ∀f : set → set (∀ u ∈ X , f u ∈ Y → (∀ u v ∈ X , f u = f v u = v → (∀ w ∈ Y , ∃ u ∈ X , f u = w → bij X Y f Axiom. (
bijE ) We take the following as an axiom:
∀X Y, ∀f : set → set bij X Y f ∀p : prop , ((∀ u ∈ X , f u ∈ Y → (∀ u v ∈ X , f u = f v u = v → (∀ w ∈ Y , ∃ u ∈ X , f u = w → p → p Primitive . The name
inv is a term of type
set → (set → set → set → set .
Axiom. (
surj_rinv ) We take the following as an axiom:
Axiom. (
inj_linv ) We take the following as an axiom:
∀X, ∀f : set → set (∀ u v ∈ X , f u = f v u = v → ∀ x ∈ X , inv X f (f x = x Axiom. (
bij_inv ) We take the following as an axiom:
∀X Y, ∀f : set → set bij X Y f bij Y X (inv X f Axiom. (
bij_id ) We take the following as an axiom:
Axiom. (
bij_comp ) We take the following as an axiom:
∀X Y Z : set , ∀f g : set → set bij X Y f bij Y Z g bij X Z (λx ⇒ g (f x ) Definition. We define
equip to be
λX Y : set ⇒ ∃ f : set → set , bij X Y f of type
set → set → prop .
Axiom. (
equip_ref ) We take the following as an axiom:
Axiom. (
equip_sym ) We take the following as an axiom:
Axiom. (
equip_tra ) We take the following as an axiom:
Beginning of Section SchroederBernstein
End of Section SchroederBernstein
Beginning of Section PigeonHole
End of Section PigeonHole
Definition. We define
finite to be
λX ⇒ ∃ n ∈ ω , equip X n of type
set → prop .
Axiom. (
finite_ind ) We take the following as an axiom:
Axiom. (
Subq_finite ) We take the following as an axiom:
Axiom. (
exandE_i ) We take the following as an axiom:
∀P Q : set → prop (∃ x, P x ∧ Q x → ∀r : prop , (∀x, P x Q x r ) → r Axiom. (
exandE_ii ) We take the following as an axiom:
∀P Q : (set → set → prop (∃ x : set → set , P x ∧ Q x → ∀p : prop , (∀x : set → set P x Q x p ) → p Axiom. (
exandE_iii ) We take the following as an axiom:
∀P Q : (set → set → set → prop (∃ x : set → set → set , P x ∧ Q x → ∀p : prop , (∀x : set → set → set P x Q x p ) → p Axiom. (
exandE_iiii ) We take the following as an axiom:
∀P Q : (set → set → set → set → prop (∃ x : set → set → set → set , P x ∧ Q x → ∀p : prop , (∀x : set → set → set → set P x Q x p ) → p
Beginning of Section Descr_ii
Variable P : (set → set → prop
Primitive . The name
Descr_ii is a term of type
set → set .
Hypothesis Pex : ∃ f : set → set , P f Hypothesis Puniq : ∀f g : set → set P f P g f = g End of Section Descr_ii
Beginning of Section Descr_iii
Variable P : (set → set → set → prop
Primitive . The name
Descr_iii is a term of type
set → set → set .
Hypothesis Pex : ∃ f : set → set → set , P f Hypothesis Puniq : ∀f g : set → set → set P f P g f = g End of Section Descr_iii
Beginning of Section Descr_Vo1
Primitive . The name
Descr_Vo1 is a term of type
Vo 1 .
Hypothesis Pex : ∃ f : Vo 1 , P f Hypothesis Puniq : ∀f g : Vo 1 P f P g f = g End of Section Descr_Vo1
Beginning of Section If_ii
Variable p : prop
Variable f g : set → set
Primitive . The name
If_ii is a term of type
set → set .
Axiom. (
If_ii_1 ) We take the following as an axiom:
Axiom. (
If_ii_0 ) We take the following as an axiom:
End of Section If_ii
Beginning of Section If_iii
Variable p : prop
Variable f g : set → set → set
Primitive . The name
If_iii is a term of type
set → set → set .
Axiom. (
If_iii_1 ) We take the following as an axiom:
Axiom. (
If_iii_0 ) We take the following as an axiom:
End of Section If_iii
Beginning of Section EpsilonRec_i
Variable F : set → (set → set → set
Primitive . The name
In_rec_i is a term of type
set → set .
Hypothesis Fr : ∀X : set , ∀g h : set → set (∀ x ∈ X , g x = h x → F X g = F X h Axiom. (
In_rec_i_eq ) We take the following as an axiom:
End of Section EpsilonRec_i
Beginning of Section EpsilonRec_ii
Variable F : set → (set → (set → set → (set → set
Primitive . The name
In_rec_ii is a term of type
set → (set → set .
Hypothesis Fr : ∀X : set , ∀g h : set → (set → set (∀ x ∈ X , g x = h x → F X g = F X h End of Section EpsilonRec_ii
Beginning of Section EpsilonRec_iii
Variable F : set → (set → (set → set → set → (set → set → set
Primitive . The name
In_rec_iii is a term of type
set → (set → set → set .
Hypothesis Fr : ∀X : set , ∀g h : set → (set → set → set (∀ x ∈ X , g x = h x → F X g = F X h End of Section EpsilonRec_iii
Beginning of Section NatRec
Variable z : set
Variable f : set → set → set
Let F : set → (set → set → set λn g ⇒ if ⋃ n ∈ n then f (⋃ n (g (⋃ n else z Axiom. (
nat_primrec_r ) We take the following as an axiom:
∀X : set , ∀g h : set → set (∀ x ∈ X , g x = h x → F X g = F X h End of Section NatRec
Beginning of Section NatArith
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_nat .
Axiom. (
add_nat_0R ) We take the following as an axiom:
Axiom. (
add_nat_SR ) We take the following as an axiom:
Axiom. (
add_nat_p ) We take the following as an axiom:
Definition. We define
mul_nat to be
λn m : set ⇒ nat_primrec 0 (λ_ r ⇒ n + r ) m of type
set → set → set .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_nat .
Axiom. (
mul_nat_0R ) We take the following as an axiom:
Axiom. (
mul_nat_SR ) We take the following as an axiom:
Axiom. (
mul_nat_p ) We take the following as an axiom:
End of Section NatArith
Axiom. (
Inj1_eq ) We take the following as an axiom:
Axiom. (
Inj1I1 ) We take the following as an axiom:
Axiom. (
Inj1I2 ) We take the following as an axiom:
Axiom. (
Inj1E ) We take the following as an axiom:
Axiom. (
Inj1NE1 ) We take the following as an axiom:
Axiom. (
Inj1NE2 ) We take the following as an axiom:
Definition. We define
Inj0 to be
λX ⇒ { Inj1 x | x ∈ X } of type
set → set .
Axiom. (
Inj0I ) We take the following as an axiom:
Axiom. (
Inj0E ) We take the following as an axiom:
Axiom. (
Unj_eq ) We take the following as an axiom:
Axiom. (
Unj_Inj1_eq ) We take the following as an axiom:
Axiom. (
Inj1_inj ) We take the following as an axiom:
Axiom. (
Unj_Inj0_eq ) We take the following as an axiom:
Axiom. (
Inj0_inj ) We take the following as an axiom:
Axiom. (
Inj0_0 ) We take the following as an axiom:
Notation . We use
+ as an infix operator with priority 450 and which associates to the left corresponding to applying term
setsum .
Axiom. (
Inj0_setsum ) We take the following as an axiom:
∀X Y x : set , x ∈ X Inj0 x ∈ X + Y Axiom. (
Inj1_setsum ) We take the following as an axiom:
∀X Y y : set , y ∈ Y Inj1 y ∈ X + Y Axiom. (
setsum_0_0 ) We take the following as an axiom:
Beginning of Section pair_setsum
Axiom. (
pairI0 ) We take the following as an axiom:
∀X Y x, x ∈ X pair 0 x ∈ pair X Y Axiom. (
pairI1 ) We take the following as an axiom:
∀X Y y, y ∈ Y pair 1 y ∈ pair X Y Axiom. (
pairE ) We take the following as an axiom:
∀X Y z, z ∈ pair X Y (∃ x ∈ X , z = pair 0 x ∨ (∃ y ∈ Y , z = pair 1 y Axiom. (
pairE0 ) We take the following as an axiom:
∀X Y x, pair 0 x ∈ pair X Y x ∈ X Axiom. (
pairE1 ) We take the following as an axiom:
∀X Y y, pair 1 y ∈ pair X Y y ∈ Y Axiom. (
proj0I ) We take the following as an axiom:
Axiom. (
proj0E ) We take the following as an axiom:
Axiom. (
proj1I ) We take the following as an axiom:
Axiom. (
proj1E ) We take the following as an axiom:
Definition. We define
Sigma to be
λX Y ⇒ ⋃ x ∈ X { pair x y | y ∈ Y x } of type
set → (set → set → set .
Notation . We use
∑ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Sigma .
Axiom. (
pair_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀ x ∈ X , ∀ y ∈ Y x , pair x y ∈ ∑ x ∈ X , Y x Axiom. (
proj0_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀z : set , z ∈ (∑ x ∈ X , Y x proj0 z ∈ X Axiom. (
proj1_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀z : set , z ∈ (∑ x ∈ X , Y x proj1 z ∈ Y (proj0 z Axiom. (
pair_Sigma_E1 ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀x y : set , pair x y ∈ (∑ x ∈ X , Y x y ∈ Y x Axiom. (
Sigma_E ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀z : set , z ∈ (∑ x ∈ X , Y x ∃ x ∈ X , ∃ y ∈ Y x , z = pair x y Definition. We define
setprod to be
λX Y : set ⇒ ∑ x ∈ X , Y of type
set → set → set .
Notation . We use
⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term
setprod .
Let lam : set → (set → set → set Sigma Definition. We define
ap to be
λf x ⇒ { proj1 z | z ∈ f , ∃ y : set , z = pair x y } of type
set → set → set .
Notation . When
x is a set, a term
x y is notation for
ap x y .
Notation .
λ x ∈ A ⇒ B is notation for the set
Sigma A (λ x : set ⇒ B ).
Notation . We now use n-tuple notation (
a0 ,...,
an-1 ) for n ≥ 2 for λ i ∈
n .
if i = 0
then a0 else ... if i =
n-2 then an-2 else an-1 .
Axiom. (
lamI ) We take the following as an axiom:
∀X : set , ∀F : set → set ∀ x ∈ X , ∀ y ∈ F x , pair x y ∈ λ x ∈ X ⇒ F x Axiom. (
lamE ) We take the following as an axiom:
∀X : set , ∀F : set → set ∀z : set , z ∈ (λ x ∈ X ⇒ F x ∃ x ∈ X , ∃ y ∈ F x , z = pair x y Axiom. (
apI ) We take the following as an axiom:
∀f x y, pair x y ∈ f y ∈ f x Axiom. (
apE ) We take the following as an axiom:
∀f x y, y ∈ f x pair x y ∈ f Axiom. (
beta ) We take the following as an axiom:
∀X : set , ∀F : set → set ∀x : set , x ∈ X (λ x ∈ X ⇒ F x x = F x Axiom. (
proj0_ap_0 ) We take the following as an axiom:
Axiom. (
proj1_ap_1 ) We take the following as an axiom:
Axiom. (
pair_ap_0 ) We take the following as an axiom:
∀x y : set , (pair x y 0 = x Axiom. (
pair_ap_1 ) We take the following as an axiom:
∀x y : set , (pair x y 1 = y Axiom. (
ap0_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀z : set , z ∈ (∑ x ∈ X , Y x (z 0 ∈ X Axiom. (
ap1_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀z : set , z ∈ (∑ x ∈ X , Y x (z 1 ∈ (Y (z 0 Definition. We define
pair_p to be
λu : set ⇒ pair (u 0 (u 1 = u of type
set → prop .
Axiom. (
pair_p_I ) We take the following as an axiom:
Axiom. (
tuple_pair ) We take the following as an axiom:
∀x y : set , pair x y = ( x , y ) Definition. We define
Pi to be
λX Y ⇒ { f ∈ 𝒫 (∑ x ∈ X , ⋃ (Y x | ∀ x ∈ X , f x ∈ Y x } of type
set → (set → set → set .
Notation . We use
∏ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Pi .
Axiom. (
PiI ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀f : set , (∀ u ∈ f , pair_p u ∧ u 0 ∈ X → (∀ x ∈ X , f x ∈ Y x → f ∈ ∏ x ∈ X , Y x Axiom. (
lam_Pi ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀F : set → set (∀ x ∈ X , F x ∈ Y x → (λ x ∈ X ⇒ F x ∈ (∏ x ∈ X , Y x Axiom. (
ap_Pi ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀f : set , ∀x : set , f ∈ (∏ x ∈ X , Y x x ∈ X f x ∈ Y x Definition. We define
setexp to be
λX Y : set ⇒ ∏ y ∈ Y , X of type
set → set → set .
Notation . We use
:^: as an infix operator with priority 430 and which associates to the left corresponding to applying term
setexp .
Axiom. (
lamI2 ) We take the following as an axiom:
Beginning of Section Tuples
Variable x0 x1 : set
End of Section Tuples
End of Section pair_setsum
Notation . We use
∑ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Sigma .
Notation . We use
⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term
setprod .
Notation . We use
∏ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Pi .
Notation . We use
:^: as an infix operator with priority 430 and which associates to the left corresponding to applying term
setexp .
Primitive . The name
DescrR_i_io_1 is a term of type
(set → (set → prop → prop → set .
Primitive . The name
DescrR_i_io_2 is a term of type
(set → (set → prop → prop → set → prop .
Definition. We define
PNoEq_ to be
λalpha p q ⇒ ∀ beta ∈ alpha , p beta ↔ q beta of type
set → (set → prop → (set → prop → prop .
Axiom. (
PNoEq_ref_ ) We take the following as an axiom:
∀alpha, ∀p : set → prop PNoEq_ alpha p p Axiom. (
PNoEq_sym_ ) We take the following as an axiom:
∀alpha, ∀p q : set → prop PNoEq_ alpha p q PNoEq_ alpha q p Axiom. (
PNoEq_tra_ ) We take the following as an axiom:
Axiom. (
PNoLt_E_ ) We take the following as an axiom:
Axiom. (
PNoLt_irref_ ) We take the following as an axiom:
∀alpha, ∀p : set → prop ¬ PNoLt_ alpha p p Axiom. (
PNoLt_mon_ ) We take the following as an axiom:
Axiom. (
PNoLt_tra_ ) We take the following as an axiom:
Primitive . The name
PNoLt is a term of type
set → (set → prop → set → (set → prop → prop .
Axiom. (
PNoLtI1 ) We take the following as an axiom:
Axiom. (
PNoLtI2 ) We take the following as an axiom:
Axiom. (
PNoLtI3 ) We take the following as an axiom:
Axiom. (
PNoLtE ) We take the following as an axiom:
Axiom. (
PNoLt_irref ) We take the following as an axiom:
∀alpha, ∀p : set → prop ¬ PNoLt alpha p alpha p Axiom. (
PNoLtEq_tra ) We take the following as an axiom:
Axiom. (
PNoEqLt_tra ) We take the following as an axiom:
Axiom. (
PNoLt_tra ) We take the following as an axiom:
Definition. We define
PNoLe to be
λalpha p beta q ⇒ PNoLt alpha p beta q ∨ alpha = beta ∧ PNoEq_ alpha p q of type
set → (set → prop → set → (set → prop → prop .
Axiom. (
PNoLeI1 ) We take the following as an axiom:
Axiom. (
PNoLeI2 ) We take the following as an axiom:
∀alpha, ∀p q : set → prop PNoEq_ alpha p q PNoLe alpha p alpha q Axiom. (
PNoLe_ref ) We take the following as an axiom:
∀alpha, ∀p : set → prop PNoLe alpha p alpha p Axiom. (
PNoLtLe_tra ) We take the following as an axiom:
Axiom. (
PNoLeLt_tra ) We take the following as an axiom:
Axiom. (
PNoEqLe_tra ) We take the following as an axiom:
Axiom. (
PNoLe_tra ) We take the following as an axiom:
Axiom. (
PNoLe_downc ) We take the following as an axiom:
Axiom. (
PNo_downc_ref ) We take the following as an axiom:
∀L : set → (set → prop → prop ∀alpha, ordinal alpha ∀p : set → prop L alpha p PNo_downc L alpha p Axiom. (
PNo_upc_ref ) We take the following as an axiom:
∀R : set → (set → prop → prop ∀alpha, ordinal alpha ∀p : set → prop R alpha p PNo_upc R alpha p Axiom. (
PNoLe_upc ) We take the following as an axiom:
Definition. We define
PNoLt_pwise to be
λL R ⇒ ∀gamma, ordinal gamma ∀p : set → prop L gamma p ∀delta, ordinal delta ∀q : set → prop R delta q PNoLt gamma p delta q of type
(set → (set → prop → prop → (set → (set → prop → prop → prop .
Axiom. (
PNo_extend0_eq ) We take the following as an axiom:
∀alpha, ∀p : set → prop PNoEq_ alpha p (λdelta ⇒ p delta ∧ delta ≠ alpha ) Axiom. (
PNo_extend1_eq ) We take the following as an axiom:
∀alpha, ∀p : set → prop PNoEq_ alpha p (λdelta ⇒ p delta ∨ delta = alpha ) Definition. We define
PNo_lenbdd to be
λalpha L ⇒ ∀beta, ∀p : set → prop L beta p beta ∈ alpha of type
set → (set → (set → prop → prop → prop .
Definition. We define
PNo_least_rep2 to be
λL R beta p ⇒ PNo_least_rep L R beta p ∧ ∀x, x ∉ beta ¬ p x of type
(set → (set → prop → prop → (set → (set → prop → prop → set → (set → prop → prop .
Primitive . The name
PNo_bd is a term of type
(set → (set → prop → prop → (set → (set → prop → prop → set .
Primitive . The name
PNo_pred is a term of type
(set → (set → prop → prop → (set → (set → prop → prop → set → prop .
Axiom. (
PNo_bd_pred ) We take the following as an axiom:
Axiom. (
PNo_bd_In ) We take the following as an axiom:
Beginning of Section TaggedSets
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
tag .
Definition. We define
SNoElts_ to be
λalpha ⇒ alpha ∪ { beta ' | beta ∈ alpha } of type
set → set .
Axiom. (
SNoElts_mon ) We take the following as an axiom:
Axiom. (
PNoEq_PSNo ) We take the following as an axiom:
Axiom. (
SNo_PSNo ) We take the following as an axiom:
Primitive . The name
SNo is a term of type
set → prop .
Axiom. (
SNo_SNo ) We take the following as an axiom:
Primitive . The name
SNoLev is a term of type
set → set .
Axiom. (
SNoLev_uniq ) We take the following as an axiom:
Axiom. (
SNoLev_prop ) We take the following as an axiom:
Axiom. (
SNoLev_ ) We take the following as an axiom:
Axiom. (
SNoLev_PSNo ) We take the following as an axiom:
Axiom. (
SNo_Subq ) We take the following as an axiom:
Definition. We define
SNoEq_ to be
λalpha x y ⇒ PNoEq_ alpha (λbeta ⇒ beta ∈ x ) (λbeta ⇒ beta ∈ y ) of type
set → set → set → prop .
Axiom. (
SNoEq_I ) We take the following as an axiom:
Axiom. (
SNo_eq ) We take the following as an axiom:
End of Section TaggedSets
Notation . We use
< as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLt .
Notation . We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLe .
Axiom. (
SNoLtLe ) We take the following as an axiom:
Axiom. (
SNoLeE ) We take the following as an axiom:
Axiom. (
SNoEq_sym_ ) We take the following as an axiom:
Axiom. (
SNoEq_tra_ ) We take the following as an axiom:
Axiom. (
SNoLtE ) We take the following as an axiom:
Axiom. (
SNoLtI2 ) We take the following as an axiom:
Axiom. (
SNoLtI3 ) We take the following as an axiom:
Axiom. (
SNoLt_irref ) We take the following as an axiom:
Axiom. (
SNoLt_tra ) We take the following as an axiom:
Axiom. (
SNoLe_ref ) We take the following as an axiom:
Axiom. (
SNoLtLe_tra ) We take the following as an axiom:
Axiom. (
SNoLeLt_tra ) We take the following as an axiom:
Axiom. (
SNoLe_tra ) We take the following as an axiom:
Axiom. (
SNoLtLe_or ) We take the following as an axiom:
Axiom. (
SNoCutP_L_0 ) We take the following as an axiom:
Axiom. (
SNoCutP_0_R ) We take the following as an axiom:
Axiom. (
SNoCutP_0_0 ) We take the following as an axiom:
Axiom. (
SNoS_E ) We take the following as an axiom:
Beginning of Section TaggedSets2
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
tag .
Axiom. (
SNoS_I ) We take the following as an axiom:
Axiom. (
SNoS_I2 ) We take the following as an axiom:
Axiom. (
SNoS_Subq ) We take the following as an axiom:
Axiom. (
SNoS_E2 ) We take the following as an axiom:
Axiom. (
SNoS_In_neq ) We take the following as an axiom:
Axiom. (
SNoS_SNoLev ) We take the following as an axiom:
Axiom. (
SNoL_E ) We take the following as an axiom:
Axiom. (
SNoR_E ) We take the following as an axiom:
Axiom. (
SNoL_SNoS_ ) We take the following as an axiom:
Axiom. (
SNoR_SNoS_ ) We take the following as an axiom:
Axiom. (
SNoL_SNoS ) We take the following as an axiom:
Axiom. (
SNoR_SNoS ) We take the following as an axiom:
Axiom. (
SNoL_I ) We take the following as an axiom:
Axiom. (
SNoR_I ) We take the following as an axiom:
Axiom. (
SNo_eta ) We take the following as an axiom:
Axiom. (
SNoCut_Le ) We take the following as an axiom:
Axiom. (
SNoCut_ext ) We take the following as an axiom:
Axiom. (
ordinal_SNo ) We take the following as an axiom:
Axiom. (
nat_p_SNo ) We take the following as an axiom:
Axiom. (
omega_SNo ) We take the following as an axiom:
Axiom. (
SNo_0 ) We take the following as an axiom:
Axiom. (
SNo_1 ) We take the following as an axiom:
Axiom. (
SNo_2 ) We take the following as an axiom:
Axiom. (
SNoLev_0 ) We take the following as an axiom:
Axiom. (
SNoCut_0_0 ) We take the following as an axiom:
Axiom. (
SNoL_0 ) We take the following as an axiom:
Axiom. (
SNoR_0 ) We take the following as an axiom:
Axiom. (
SNoL_1 ) We take the following as an axiom:
Axiom. (
SNoR_1 ) We take the following as an axiom:
Axiom. (
eps_0_1 ) We take the following as an axiom:
Axiom. (
SNo__eps_ ) We take the following as an axiom:
Axiom. (
SNo_eps_ ) We take the following as an axiom:
Axiom. (
SNo_eps_1 ) We take the following as an axiom:
Axiom. (
SNoLev_eps_ ) We take the following as an axiom:
Axiom. (
SNo_eps_pos ) We take the following as an axiom:
Axiom. (
eps_SNo_eq ) We take the following as an axiom:
Axiom. (
eps_SNoCutP ) We take the following as an axiom:
Axiom. (
eps_SNoCut ) We take the following as an axiom:
End of Section TaggedSets2
Axiom. (
SNo_etaE ) We take the following as an axiom:
Axiom. (
SNo_ind ) We take the following as an axiom:
Beginning of Section SurrealRecI
Variable F : set → (set → set → set
Primitive . The name
SNo_rec_i is a term of type
set → set .
Hypothesis Fr : ∀z, SNo z ∀g h : set → set (∀ w ∈ SNoS_ (SNoLev z , g w = h w → F z g = F z h End of Section SurrealRecI
Beginning of Section SurrealRecII
Variable F : set → (set → (set → set → (set → set
Let G : set → (set → set → (set → set → set → (set → set λalpha g ⇒ If_iii (ordinal alpha (λz : set ⇒ If_ii (z ∈ SNoS_ (ordsucc alpha (F z (λw ⇒ g (SNoLev w w ) default ) (λz : set ⇒ default ) Primitive . The name
SNo_rec_ii is a term of type
set → (set → set .
Hypothesis Fr : ∀z, SNo z ∀g h : set → (set → set (∀ w ∈ SNoS_ (SNoLev z , g w = h w → F z g = F z h End of Section SurrealRecII
Beginning of Section SurrealRec2
Variable F : set → set → (set → set → set → set
Let G : set → (set → set → set → set → (set → set → set λw f z g ⇒ F w z (λx y ⇒ if x = w then g y else f x y ) Primitive . The name
SNo_rec2 is a term of type
set → set → set .
Axiom. (
SNo_rec2_eq ) We take the following as an axiom:
End of Section SurrealRec2
Axiom. (
SNoLev_ind ) We take the following as an axiom:
Axiom. (
SNoLev_ind2 ) We take the following as an axiom:
Axiom. (
SNoLev_ind3 ) We take the following as an axiom:
∀P : set → set → set → prop (∀x y z, SNo x SNo y SNo z (∀ u ∈ SNoS_ (SNoLev x , P u y z → (∀ v ∈ SNoS_ (SNoLev y , P x v z → (∀ w ∈ SNoS_ (SNoLev z , P x y w → (∀ u ∈ SNoS_ (SNoLev x , ∀ v ∈ SNoS_ (SNoLev y , P u v z → (∀ u ∈ SNoS_ (SNoLev x , ∀ w ∈ SNoS_ (SNoLev z , P u y w → (∀ v ∈ SNoS_ (SNoLev y , ∀ w ∈ SNoS_ (SNoLev z , P x v w → (∀ u ∈ SNoS_ (SNoLev x , ∀ v ∈ SNoS_ (SNoLev y , ∀ w ∈ SNoS_ (SNoLev z , P u v w → P x y z ) → ∀x y z, SNo x SNo y SNo z P x y z Axiom. (
SNo_omega ) We take the following as an axiom:
Axiom. (
SNoLt_0_1 ) We take the following as an axiom:
Axiom. (
SNoLt_0_2 ) We take the following as an axiom:
Axiom. (
SNoLt_1_2 ) We take the following as an axiom:
Axiom. (
restr_SNo_ ) We take the following as an axiom:
Axiom. (
restr_SNo ) We take the following as an axiom:
Axiom. (
restr_SNoEq ) We take the following as an axiom:
Beginning of Section SurrealMinus
Primitive . The name
minus_SNo is a term of type
set → set .
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo .
Notation . We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLe .
End of Section SurrealMinus
Beginning of Section SurrealAdd
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo .
Proof:
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 .
Let w be given.
We will
prove g w y = h w y .
Apply Hgh1
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
Let w be given.
We will
prove g x w = h x w .
Apply Hgh2
An
exact proof term for the current goal is
SNoL_SNoS y Hy w Hw .
Let z be given.
We will
prove g z y = h z y .
Apply Hgh1
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
Let z be given.
We will
prove g x z = h x z .
Apply Hgh2
An
exact proof term for the current goal is
SNoR_SNoS y Hy z Hz .
rewrite the current goal using L1a
rewrite the current goal using L1b
rewrite the current goal using L1c
rewrite the current goal using L1d
Use reflexivity.
An
exact proof term for the current goal is
SNo_rec2_eq F L1 .
∎
Proof:
Let x and y be given.
Assume Hxy .
Let p be given.
Assume Hp .
Apply Hxy
Assume H .
Apply H
Assume H .
Apply H
Assume H .
Apply H
Assume H .
Apply H
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 L to be the term
L1 ∪ L2 .
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.
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.
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.
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.
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 .
Apply and3I to the current goal.
Let w be given.
Apply binunionE L1 L2 w Hw to the current goal.
Let z be given.
Apply LPE z y (IHLx z Hz
Assume _ _ _ _ .
rewrite the current goal using Hwz
An exact proof term for the current goal is H2
Let z be given.
Apply LPE x z (IHLy z Hz
Assume _ _ _ _ .
rewrite the current goal using Hwz
An exact proof term for the current goal is H2
Let w be given.
Apply binunionE R1 R2 w Hw to the current goal.
Let z be given.
Apply LPE z y (IHRx z Hz
Assume _ _ _ _ .
rewrite the current goal using Hwz
An exact proof term for the current goal is H2
Let z be given.
Apply LPE x z (IHRy z Hz
Assume _ _ _ _ .
rewrite the current goal using Hwz
An exact proof term for the current goal is H2
Let w be given.
Let z be given.
Apply binunionE L1 L2 w Hw to the current goal.
Let u be given.
Apply SNoL_E x Hx u Hu to the current goal.
An
exact proof term for the current goal is
SNoS_I2 u x Hu1 Hx Hu2 .
Apply LPE u y (IHLx u Hu
rewrite the current goal using Hwu
Apply binunionE R1 R2 z Hz to the current goal.
Let v be given.
Apply SNoR_E x Hx v Hv to the current goal.
Apply LPE v y (IHRx v Hv
rewrite the current goal using Hzv
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 _ _ .
Assume Hq2u Hq2v .
An
exact proof term for the current goal is
LLxa (SNoLev u Hu2 (SNoLev q Hq2u .
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
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
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
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
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
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.
Apply SNoR_E y Hy v Hv to the current goal.
An
exact proof term for the current goal is
SNoS_I2 v y Hv1 Hy Hv2 .
Apply LPE x v (IHRy v Hv
rewrite the current goal using Hzv
We will
prove u + y < x + v .
Apply LPE u v (IHxy u Lux v Lvy
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
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
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.
Apply SNoL_E y Hy u Hu to the current goal.
An
exact proof term for the current goal is
SNoS_I2 u y Hu1 Hy Hu2 .
Apply LPE x u (IHLy u Hu
rewrite the current goal using Hwu
Apply binunionE R1 R2 z Hz to the current goal.
Let v be given.
Apply SNoR_E x Hx v Hv to the current goal.
An
exact proof term for the current goal is
SNoS_I2 v x Hv1 Hx Hv2 .
Apply LPE v y (IHRx v Hv
rewrite the current goal using Hzv
We will
prove x + u < v + y .
Apply LPE v u (IHxy v Lvx u Luy
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
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
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.
Apply SNoR_E y Hy v Hv to the current goal.
Apply LPE x v (IHRy v Hv
rewrite the current goal using Hzv
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 _ _ .
Assume Hq2u Hq2v .
An
exact proof term for the current goal is
LLya (SNoLev v Hv2 (SNoLev q Hq2v .
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
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
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
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
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
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 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.
Apply SNoL_E x Hx u Hu to the current goal.
We prove the intermediate
claim LuyL :
u + y ∈ L .
We will
prove u + y ∈ L1 ∪ L2 .
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
Let u be given.
Apply SNoR_E x Hx u Hu to the current goal.
We prove the intermediate
claim LuyR :
u + y ∈ R .
We will
prove u + y ∈ R1 ∪ R2 .
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
Let u be given.
Apply SNoL_E y Hy u Hu to the current goal.
We prove the intermediate
claim LxuL :
x + u ∈ L .
We will
prove x + u ∈ L1 ∪ L2 .
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
Let u be given.
Apply SNoR_E y Hy u Hu to the current goal.
We prove the intermediate
claim LxuR :
x + u ∈ R .
We will
prove x + u ∈ R1 ∪ R2 .
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
An exact proof term for the current goal is LLR
∎
Proof: Let x and y be given.
Assume H .
Apply H
Assume H .
Apply H
Assume H .
Apply H
Assume H .
Apply H
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 .
∎
Proof: Let x, y and z be given.
Assume H .
Apply H
Assume H .
Apply H
Assume H .
Apply H
Assume H .
Apply H
Assume _ .
Assume _ _ _ .
Assume H .
Apply H
Assume H .
Apply H
Assume H .
Apply H
Assume H .
Apply H
Assume _ _ _ _ .
Apply SNoLtE x z Hx Hz Hxz to the current goal.
Let w be given.
Assume _ _ .
Assume _ _ .
Assume Hw2x Hw2z .
We will
prove x + y < z + y .
We will
prove x + y < w + y .
Apply H2
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
An exact proof term for the current goal is Hw5
We will
prove w + y < z + y .
Apply H4
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
An exact proof term for the current goal is Hw6
Assume _ _ .
We will
prove x + y < z + y .
Apply H4
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
An exact proof term for the current goal is Hxz
Assume _ _ .
We will
prove x + y < z + y .
Apply H2
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
An exact proof term for the current goal is Hxz
∎
Proof: Let x, y and z be given.
We will
prove x + y ≤ z + y .
Apply SNoLeE x z Hx Hz Hxz to the current goal.
An
exact proof term for the current goal is
add_SNo_Lt1 x y z Hx Hy Hz H1 .
rewrite the current goal using H1
∎
Proof: Let x, y and z be given.
Assume H .
Apply H
Assume H .
Apply H
Assume H .
Apply H
Assume H .
Apply H
Assume _ _ _ .
Assume _ .
Assume H .
Apply H
Assume H .
Apply H
Assume H .
Apply H
Assume H .
Apply H
Assume _ _ .
Assume _ _ .
Apply SNoLtE y z Hy Hz Hyz to the current goal.
Let w be given.
Assume _ _ .
Assume _ _ .
Assume Hw2y Hw2z .
We will
prove x + y < x + z .
We will
prove x + y < x + w .
Apply H2
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
An exact proof term for the current goal is Hw5
We will
prove x + w < x + z .
Apply H4
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
An exact proof term for the current goal is Hw6
Assume _ _ .
We will
prove x + y < x + z .
Apply H4
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
An exact proof term for the current goal is Hyz
Assume _ _ .
We will
prove x + y < x + z .
Apply H2
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
An exact proof term for the current goal is Hyz
∎
Proof: Let x, y and z be given.
We will
prove x + y ≤ x + z .
Apply SNoLeE y z Hy Hz Hyz to the current goal.
An
exact proof term for the current goal is
add_SNo_Lt2 x y z Hx Hy Hz H1 .
rewrite the current goal using H1
∎
Proof: Let x, y, z and w be given.
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 .
∎
Proof: Let x, y, z and w be given.
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 .
∎
Proof: Let x, y, z and w be given.
Apply add_SNo_Lt3a x y z w Hx Hy Hz Hw Hxz to the current goal.
An exact proof term for the current goal is Hyw
∎
Proof: Let x, y, z and w be given.
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
∎
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.
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.
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.
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.
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 .
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 .
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 .
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 .
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 .
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 .
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
rewrite the current goal using Lxy2yx1
rewrite the current goal using Rxy1yx2
rewrite the current goal using Rxy2yx1
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.
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).
Let u be given.
Let w be given.
We will
prove u ∈ SNoL x .
rewrite the current goal using H1
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.
rewrite the current goal using
IH u (SNoL_SNoS_ x u Hu (from right to left).
An
exact proof term for the current goal is
ReplI (SNoL x (λw ⇒ 0 + w ) u Hu .
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).
Let u be given.
Let w be given.
We will
prove u ∈ SNoR x .
rewrite the current goal using H1
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.
rewrite the current goal using
IH u (SNoR_SNoS_ x u Hu (from right to left).
An
exact proof term for the current goal is
ReplI (SNoR x (λw ⇒ 0 + w ) u Hu .
rewrite the current goal using L1
rewrite the current goal using L2
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 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 .
We prove the intermediate
claim LNLR :
SNo (SNoCut L R .
We will
prove ∀ w ∈ L , w < 0 .
Let w be given.
Apply binunionE L1 L2 w Hw to the current goal.
Let u be given.
Apply SNoL_E (- x Lmx u Hu to the current goal.
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
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 .
An exact proof term for the current goal is Hu3
rewrite the current goal using Hwu
rewrite the current goal using
add_SNo_com u x Hu1 Hx (from left to right).
rewrite the current goal using Lmuu
We will
prove x + u < - u + u .
An exact proof term for the current goal is Lxmu
Let u be given.
Apply SNoL_E x Hx u Hu to the current goal.
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
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 .
An exact proof term for the current goal is Hu3
rewrite the current goal using Hwu
We will
prove - x + u < 0 .
rewrite the current goal using Lmuu
We will
prove - x + u < - u + u .
An exact proof term for the current goal is Lmxmu
We will
prove ∀ z ∈ R , 0 < z .
Let z be given.
Apply binunionE R1 R2 z Hz to the current goal.
Let v be given.
Apply SNoR_E (- x Lmx v Hv to the current goal.
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
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 .
An exact proof term for the current goal is Hv3
rewrite the current goal using Hzv
rewrite the current goal using
add_SNo_com v x Hv1 Hx (from left to right).
rewrite the current goal using Lmvv
We will
prove - v + v < x + v .
An exact proof term for the current goal is Lmvx
Let v be given.
Apply SNoR_E x Hx v Hv to the current goal.
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
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 .
An exact proof term for the current goal is Hv3
rewrite the current goal using Hzv
We will
prove 0 < - x + v .
rewrite the current goal using Lmvv
We will
prove - v + v < - x + v .
An exact proof term for the current goal is Lmvmx
Apply Lfst
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.
Apply and3I to the current goal.
Let w be given.
Apply binunionE Lo1 Lo2 w Hw to the current goal.
Let x be given.
Apply SNoS_E2 alpha Ha x Hx to the current goal.
Assume _ _ .
Assume _ .
rewrite the current goal using H2
Let x be given.
Assume _ _ .
Assume _ .
rewrite the current goal using H2
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.
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.
Assume H1 .
Apply H1
An exact proof term for the current goal is H1
rewrite the current goal using H1
An exact proof term for the current goal is Hy1
Assume H2 .
Apply H2
Assume _ _ .
Assume H3 .
Apply H3
Assume H3 .
Apply H3
Assume _ .
Assume _ .
Apply H4 y Hy3
Let w be given.
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
Assume _ .
Apply H5
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
Assume H1 .
Apply H1
Assume _ .
Assume _ .
Apply H1
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.
Apply binunionE Lo1 Lo2 w Hw to the current goal.
Let x be given.
rewrite the current goal using Hwx
An exact proof term for the current goal is LLxb
Apply Ha
Assume Ha1 _ .
An
exact proof term for the current goal is
Ha1 (SNoLev x H5 .
rewrite the current goal using H5
We will
prove alpha + beta < z .
Let x be given.
rewrite the current goal using Hwx
An
exact proof term for the current goal is
IH (SNoLev x Hx1 .
We prove the intermediate
claim LSax :
SNo (ordsucc alpha + x .
An exact proof term for the current goal is LSaLx
rewrite the current goal using IHLx
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
rewrite the current goal using
ordinal_SNoLev z Lz (from left to right).
Assume _ .
Apply H4
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
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
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 .
Let u be given.
Apply dneg to the current goal.
Apply SNoLtLe_tra u (x + y u Hu1 Lxy Hu1 Hu3 to the current goal.
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.
Apply binunionE Lxy1 Lxy2 w Hw to the current goal.
Let v be given.
Apply SNoL_E x Hx v Hv to the current goal.
rewrite the current goal using Hwv
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.
An exact proof term for the current goal is H1
Apply HNC
Apply orIL to the current goal.
We use v 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
An exact proof term for the current goal is H1
Let v be given.
Apply SNoL_E y Hy v Hv to the current goal.
rewrite the current goal using Hwv
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.
An exact proof term for the current goal is H1
Apply HNC
Apply orIR to the current goal.
We use v 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
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).
Let z be given.
Apply SNoR_E u Hu1 z Hz to the current goal.
Assume H1 .
Apply H1
An exact proof term for the current goal is H1
rewrite the current goal using H1
An exact proof term for the current goal is Hu2
An
exact proof term for the current goal is
SNoR_SNoS_ u z Hz .
Assume Hxy1 _ .
An
exact proof term for the current goal is
Hxy1 (SNoLev u Hu2 (SNoLev z Hz2 .
Apply IH z Lz1 Lz2 H1
Apply H2
Let v be given.
Assume H3 .
Apply H3
Apply SNoL_E x Hx v Hv to the current goal.
Apply HNC
Apply orIL to the current goal.
We use v witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv
An exact proof term for the current goal is Hz3
An exact proof term for the current goal is H3
Apply H2
Let v be given.
Assume H3 .
Apply H3
Apply SNoL_E y Hy v Hv to the current goal.
Apply HNC
Apply orIR to the current goal.
We use v witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv
An exact proof term for the current goal is Hz3
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.
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 .
Let u be given.
Apply dneg to the current goal.
Apply (λH : u ≤ x + y SNoLeLt_tra u (x + y u Hu1 Lxy Hu1 H Hu3 ) to the current goal.
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).
Let z be given.
Apply SNoL_E u Hu1 z Hz to the current goal.
Assume H1 .
Apply H1
An exact proof term for the current goal is H1
rewrite the current goal using H1
An exact proof term for the current goal is Hu2
An
exact proof term for the current goal is
SNoL_SNoS_ u z Hz .
Assume Hxy1 _ .
An
exact proof term for the current goal is
Hxy1 (SNoLev u Hu2 (SNoLev z Hz2 .
Apply IH z Lz1 Lz2 H1
Apply H2
Let v be given.
Assume H3 .
Apply H3
Apply SNoR_E x Hx v Hv to the current goal.
Apply HNC
Apply orIL to the current goal.
We use v witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv
An exact proof term for the current goal is H3
An exact proof term for the current goal is Hz3
Apply H2
Let v be given.
Assume H3 .
Apply H3
Apply SNoR_E y Hy v Hv to the current goal.
Apply HNC
Apply orIR to the current goal.
We use v witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv
An exact proof term for the current goal is H3
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.
Apply binunionE Rxy1 Rxy2 w Hw to the current goal.
Let v be given.
Apply SNoR_E x Hx v Hv to the current goal.
rewrite the current goal using Hwv
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.
An exact proof term for the current goal is H1
Apply HNC
Apply orIL to the current goal.
We use v 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
An exact proof term for the current goal is H1
Let v be given.
Apply SNoR_E y Hy v Hv to the current goal.
rewrite the current goal using Hwv
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.
An exact proof term for the current goal is H1
Apply HNC
Apply orIR to the current goal.
We use v 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
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.
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 .
We prove the intermediate
claim Lxyz34 :
SNoCutP (Lxyz3 ∪ Lxyz4 (Rxyz3 ∪ Rxyz4 .
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.
Apply binunionE Lxyz1 Lxyz2 w Hw to the current goal.
Let u be given.
Apply SNoL_E x Hx u Hu to the current goal.
We will
prove w < (x + y + z .
rewrite the current goal using Hwu
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
We will
prove (u + y + z < (x + y + z .
We will
prove u + y < x + y .
An exact proof term for the current goal is Hu3
Let u be given.
Apply SNoL_E (y + z Lyz u Hu to the current goal.
rewrite the current goal using Hwu
We will
prove x + u < (x + y + z .
Apply H1
Let v be given.
Assume H2 .
Apply H2
Apply SNoL_E y Hy v Hv to the current goal.
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 .
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
We will
prove (x + v + z < (x + y + z .
We will
prove x + v < x + y .
An exact proof term for the current goal is Hv3
Apply H1
Let v be given.
Assume H2 .
Apply H2
Apply SNoL_E z Hz v Hv to the current goal.
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 .
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
We will
prove (x + y + v < (x + y + z .
Apply add_SNo_Lt2 (x + y v z Lxy Hv1 Hz to the current goal.
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.
Apply binunionE Rxyz1 Rxyz2 v Hv to the current goal.
Let u be given.
Apply SNoR_E x Hx u Hu to the current goal.
We will
prove (x + y + z < v .
rewrite the current goal using Hvu
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
We will
prove (x + y + z < (u + y + z .
We will
prove x + y < u + y .
An exact proof term for the current goal is Hu3
Let u be given.
Apply SNoR_E (y + z Lyz u Hu to the current goal.
rewrite the current goal using Hvu
We will
prove (x + y + z < x + u .
Apply H1
Let v be given.
Assume H2 .
Apply H2
Apply SNoR_E y Hy v Hv to the current goal.
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
We will
prove (x + y + z < (x + v + z .
We will
prove x + y < x + v .
An exact proof term for the current goal is Hv3
We will
prove x + (v + z ≤ x + u .
An exact proof term for the current goal is H2
Apply H1
Let v be given.
Assume H2 .
Apply H2
Apply SNoR_E z Hz v Hv to the current goal.
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
We will
prove (x + y + z < (x + y + v .
Apply add_SNo_Lt2 (x + y z v Lxy Hz Hv1 to the current goal.
An exact proof term for the current goal is Hv3
We will
prove x + (y + v ≤ x + 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.
Apply binunionE Lxyz3 Lxyz4 w Hw to the current goal.
Let u be given.
Apply SNoL_E (x + y Lxy u Hu to the current goal.
rewrite the current goal using Hwu
We will
prove u + z < x + (y + z .
Apply H1
Let v be given.
Assume H2 .
Apply H2
Apply SNoL_E x Hx v Hv to the current goal.
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 .
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
We will
prove v + (y + z < x + (y + z .
Apply add_SNo_Lt1 v (y + z x Hv1 Lyz Hx to the current goal.
An exact proof term for the current goal is Hv3
Apply H1
Let v be given.
Assume H2 .
Apply H2
Apply SNoL_E y Hy v Hv to the current goal.
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 .
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
We will
prove x + (v + z < x + (y + z .
We will
prove v + z < y + z .
An exact proof term for the current goal is Hv3
Let u be given.
Apply SNoL_E z Hz u Hu to the current goal.
We will
prove w < x + (y + z .
rewrite the current goal using Hwu
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
We will
prove x + (y + u < x + (y + z .
We will
prove y + u < y + 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.
Apply binunionE Rxyz3 Rxyz4 v Hv to the current goal.
Let u be given.
Apply SNoR_E (x + y Lxy u Hu to the current goal.
rewrite the current goal using Hvu
We will
prove x + (y + z < u + z .
Apply H1
Let v be given.
Assume H2 .
Apply H2
Apply SNoR_E x Hx v Hv to the current goal.
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
We will
prove x + (y + z < v + (y + z .
Apply add_SNo_Lt1 x (y + z v Hx Lyz Hv1 to the current goal.
An exact proof term for the current goal is Hv3
We will
prove (v + y + z ≤ u + z .
An exact proof term for the current goal is H2
Apply H1
Let v be given.
Assume H2 .
Apply H2
Apply SNoR_E y Hy v Hv to the current goal.
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
We will
prove x + (y + z < x + (v + z .
We will
prove y + z < v + z .
An exact proof term for the current goal is Hv3
We will
prove (x + v + z ≤ u + z .
An exact proof term for the current goal is H2
Let u be given.
Apply SNoR_E z Hz u Hu to the current goal.
We will
prove x + (y + z < v .
rewrite the current goal using Hvu
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
We will
prove x + (y + z < x + (y + u .
We will
prove y + z < y + u .
An exact proof term for the current goal is Hu3
∎
Proof: Let x, y and z be given.
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 .
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 .
An
exact proof term for the current goal is
add_SNo_0L z Hz .
rewrite the current goal using L1
rewrite the current goal using Hxyz
An exact proof term for the current goal is L2
∎
Proof:
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 .
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:
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
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 _ _ _ .
Let u be given.
Assume Hu .
Let p be given.
Assume Hp .
Let w be given.
rewrite the current goal using Huw
Apply SNoL_E x Hx w Hw to the current goal.
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
Let u be given.
Assume Hu .
Let p be given.
Assume Hp .
Let w be given.
rewrite the current goal using Huw
Apply SNoL_E y Hy w Hw to the current goal.
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
Let u be given.
Assume Hu .
Let p be given.
Assume Hp .
Let w be given.
rewrite the current goal using Huw
Apply SNoR_E x Hx w Hw to the current goal.
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
Let u be given.
Assume Hu .
Let p be given.
Assume Hp .
Let w be given.
rewrite the current goal using Huw
Apply SNoR_E y Hy w Hw to the current goal.
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
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
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
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
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.
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.
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
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.
Apply binunionE Lxy1 Lxy2 u Hu to the current goal.
Apply Lxy1E u Hu
Let w be given.
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
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
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
An exact proof term for the current goal is H2
An exact proof term for the current goal is H2
Apply LIHw
Apply L4c
Apply H1
An exact proof term for the current goal is L4a
Apply Lxy2E u Hu
Let w be given.
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
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
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
An exact proof term for the current goal is H2
An exact proof term for the current goal is H2
Apply LIHw
Apply L4c
Apply H1
An exact proof term for the current goal is L4a
Let v be given.
Let u be given.
Apply binunionE Rxy1 Rxy2 u Hu to the current goal.
Apply Rxy1E u Hu
Let w be given.
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
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
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
An exact proof term for the current goal is H2
An exact proof term for the current goal is H2
Apply LIHw
Apply L4c
Apply H1
An exact proof term for the current goal is L4a
Apply Rxy2E u Hu
Let w be given.
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
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
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
An exact proof term for the current goal is H2
An exact proof term for the current goal is H2
Apply LIHw
Apply L4c
Apply H1
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
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 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
rewrite the current goal using L2
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 and y be given.
Assume Hx Hy .
We will
prove (x + - x + y = y .
An
exact proof term for the current goal is
add_SNo_0L y Hy .
∎
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 .
rewrite the current goal using H2
We will
prove (x + - y + y ≤ x .
∎
Proof: Let x, y and z be given.
Assume Hx Hy Hz H1 .
We will
prove z ≤ x + - y .
rewrite the current goal using H2
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
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 .
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 .
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 .
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
rewrite the current goal using L3
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.
Use symmetry.
∎
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.
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 .
∎
Proof: Let x and y be given.
Assume Hx Hy Hxy .
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 .
Apply ordsuccE (n + k m H1 to the current goal.
Apply IHk H2
Apply orIL to the current goal.
An exact proof term for the current goal is H3
Apply orIR to the current goal.
An exact proof term for the current goal is H3
Apply orIR to the current goal.
rewrite the current goal using H2
∎
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 .
∎
Proof: Let Lx, Rx, Ly, Ry, x and y be given.
Assume HLRx HLRy Hxe Hye .
Apply HLRx
Assume H .
Apply H
Apply HLRy
Assume H .
Apply H
Set Lx' to be the term
{ w + y | w ∈ Lx } .
Set Ly' to be the term
{ x + w | w ∈ Ly } .
Set Rx' to be the term
{ z + y | z ∈ Rx } .
Set Ry' to be the term
{ x + z | z ∈ Ry } .
rewrite the current goal using Hxe
rewrite the current goal using Hye
We prove the intermediate
claim L1 :
SNoCutP (Lx' ∪ Ly' (Rx' ∪ Ry' .
Apply and3I to the current goal.
Let w be given.
Let w' be given.
rewrite the current goal using Hwe
An
exact proof term for the current goal is
SNo_add_SNo w' y (HLRx1 w' Hw' Hy1 .
Let w' be given.
rewrite the current goal using Hwe
An
exact proof term for the current goal is
SNo_add_SNo x w' Hx1 (HLRy1 w' Hw' .
Let z be given.
Let z' be given.
rewrite the current goal using Hze
An
exact proof term for the current goal is
SNo_add_SNo z' y (HLRx2 z' Hz' Hy1 .
Let z' be given.
rewrite the current goal using Hze
An
exact proof term for the current goal is
SNo_add_SNo x z' Hx1 (HLRy2 z' Hz' .
Let w be given.
Let w' be given.
We prove the intermediate
claim Lw' :
SNo w' .
An exact proof term for the current goal is HLRx1 w' Hw'
rewrite the current goal using Hwe
Let z be given.
Let z' be given.
We prove the intermediate
claim Lz' :
SNo z' .
An exact proof term for the current goal is HLRx2 z' Hz'
rewrite the current goal using Hze
We will
prove w' + y < z' + y .
Apply add_SNo_Lt1 w' y z' Lw' Hy1 Lz' to the current goal.
An
exact proof term for the current goal is
SNoLt_tra w' x z' Lw' Hx1 Lz' (Hx3 w' Hw' (Hx4 z' Hz' .
Let z' be given.
We prove the intermediate
claim Lz' :
SNo z' .
An exact proof term for the current goal is HLRy2 z' Hz'
rewrite the current goal using Hze
We will
prove w' + y < x + z' .
Apply add_SNo_Lt3 w' y x z' Lw' Hy1 Hx1 Lz' to the current goal.
An exact proof term for the current goal is Hx3 w' Hw'
An exact proof term for the current goal is Hy4 z' Hz'
Let w' be given.
We prove the intermediate
claim Lw' :
SNo w' .
An exact proof term for the current goal is HLRy1 w' Hw'
rewrite the current goal using Hwe
Let z be given.
Let z' be given.
We prove the intermediate
claim Lz' :
SNo z' .
An exact proof term for the current goal is HLRx2 z' Hz'
rewrite the current goal using Hze
We will
prove x + w' < z' + y .
Apply add_SNo_Lt3 x w' z' y Hx1 Lw' Lz' Hy1 to the current goal.
An exact proof term for the current goal is Hx4 z' Hz'
An exact proof term for the current goal is Hy3 w' Hw'
Let z' be given.
We prove the intermediate
claim Lz' :
SNo z' .
An exact proof term for the current goal is HLRy2 z' Hz'
rewrite the current goal using Hze
We will
prove x + w' < x + z' .
Apply add_SNo_Lt2 x w' z' Hx1 Lw' Lz' to the current goal.
An
exact proof term for the current goal is
SNoLt_tra w' y z' Lw' Hy1 Lz' (Hy3 w' Hw' (Hy4 z' Hz' .
We will
prove x + y = SNoCut (Lx' ∪ Ly' (Rx' ∪ Ry' .
rewrite the current goal using
add_SNo_eq x Hx1 y Hy1 (from left to right).
Set v to be the term
SNoCut (Lx' ∪ Ly' (Rx' ∪ Ry' .
An exact proof term for the current goal is L1
Let w be given.
Assume Hw .
Let w' be given.
Apply SNoL_E x Hx1 w' Hw' to the current goal.
We prove the intermediate
claim L2 :
∃ w'' ∈ Lx , w' ≤ w'' .
Apply dneg to the current goal.
Assume HC .
Apply Hx5 w' Hw'1
We will
prove ∀ w'' ∈ Lx , w'' < w' .
Let w'' be given.
Assume Hw''1 .
Apply SNoLtLe_or w'' w' (HLRx1 w'' Hw''1 Hw'1 to the current goal.
Assume H .
An exact proof term for the current goal is H
Apply HC
We use w'' witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw''1
An exact proof term for the current goal is Hw''2
We will
prove ∀ z ∈ Rx , w' < z .
Let z be given.
Assume Hz .
Apply SNoLt_tra w' x z Hw'1 Hx1 (HLRx2 z Hz to the current goal.
An exact proof term for the current goal is Hw'3
An exact proof term for the current goal is Hx4 z Hz
Apply L2a
Assume _ .
Apply Hxw'
An exact proof term for the current goal is Hw'2
Apply L2
Let w'' be given.
Assume H .
Apply H
rewrite the current goal using Hwe
We will
prove w' + y < v .
We will
prove w' + y ≤ w'' + y .
Apply add_SNo_Le1 w' y w'' Hw'1 Hy1 (HLRx1 w'' Hw''1 to the current goal.
An exact proof term for the current goal is Hw''2
We will
prove w'' + y < v .
Apply Hv3
We will
prove w'' + y ∈ Lx' ∪ Ly' .
We will
prove w'' + y ∈ Lx' .
An
exact proof term for the current goal is
ReplI Lx (λw ⇒ w + y ) w'' Hw''1 .
Assume Hw .
Let w' be given.
Apply SNoL_E y Hy1 w' Hw' to the current goal.
We prove the intermediate
claim L3 :
∃ w'' ∈ Ly , w' ≤ w'' .
Apply dneg to the current goal.
Assume HC .
Apply Hy5 w' Hw'1
We will
prove ∀ w'' ∈ Ly , w'' < w' .
Let w'' be given.
Assume Hw''1 .
Apply SNoLtLe_or w'' w' (HLRy1 w'' Hw''1 Hw'1 to the current goal.
Assume H .
An exact proof term for the current goal is H
Apply HC
We use w'' witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw''1
An exact proof term for the current goal is Hw''2
We will
prove ∀ z ∈ Ry , w' < z .
Let z be given.
Assume Hz .
Apply SNoLt_tra w' y z Hw'1 Hy1 (HLRy2 z Hz to the current goal.
An exact proof term for the current goal is Hw'3
An exact proof term for the current goal is Hy4 z Hz
Apply L3a
Assume _ .
Apply Hyw'
An exact proof term for the current goal is Hw'2
Apply L3
Let w'' be given.
Assume H .
Apply H
rewrite the current goal using Hwe
We will
prove x + w' < v .
We will
prove x + w' ≤ x + w'' .
Apply add_SNo_Le2 x w' w'' Hx1 Hw'1 (HLRy1 w'' Hw''1 to the current goal.
An exact proof term for the current goal is Hw''2
We will
prove x + w'' < v .
Apply Hv3
We will
prove x + w'' ∈ Lx' ∪ Ly' .
We will
prove x + w'' ∈ Ly' .
An
exact proof term for the current goal is
ReplI Ly (λw ⇒ x + w ) w'' Hw''1 .
Let z be given.
Assume Hz .
Let z' be given.
Apply SNoR_E x Hx1 z' Hz' to the current goal.
We prove the intermediate
claim L4 :
∃ z'' ∈ Rx , z'' ≤ z' .
Apply dneg to the current goal.
Assume HC .
Apply Hx5 z' Hz'1
We will
prove ∀ w ∈ Lx , w < z' .
Let w be given.
Assume Hw .
Apply SNoLt_tra w x z' (HLRx1 w Hw Hx1 Hz'1 to the current goal.
An exact proof term for the current goal is Hx3 w Hw
An exact proof term for the current goal is Hz'3
We will
prove ∀ z'' ∈ Rx , z' < z'' .
Let z'' be given.
Assume Hz''1 .
Apply SNoLtLe_or z' z'' Hz'1 (HLRx2 z'' Hz''1 to the current goal.
Assume H .
An exact proof term for the current goal is H
Apply HC
We use z'' witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz''1
An exact proof term for the current goal is Hz''2
Apply L4a
Assume _ .
Apply Hxz'
An exact proof term for the current goal is Hz'2
Apply L4
Let z'' be given.
Assume H .
Apply H
rewrite the current goal using Hze
We will
prove v < z' + y .
We will
prove v < z'' + y .
Apply Hv4
We will
prove z'' + y ∈ Rx' ∪ Ry' .
We will
prove z'' + y ∈ Rx' .
An
exact proof term for the current goal is
ReplI Rx (λz ⇒ z + y ) z'' Hz''1 .
We will
prove z'' + y ≤ z' + y .
Apply add_SNo_Le1 z'' y z' (HLRx2 z'' Hz''1 Hy1 Hz'1 to the current goal.
An exact proof term for the current goal is Hz''2
Assume Hz .
Let z' be given.
Apply SNoR_E y Hy1 z' Hz' to the current goal.
We prove the intermediate
claim L5 :
∃ z'' ∈ Ry , z'' ≤ z' .
Apply dneg to the current goal.
Assume HC .
Apply Hy5 z' Hz'1
We will
prove ∀ w ∈ Ly , w < z' .
Let w be given.
Assume Hw .
Apply SNoLt_tra w y z' (HLRy1 w Hw Hy1 Hz'1 to the current goal.
An exact proof term for the current goal is Hy3 w Hw
An exact proof term for the current goal is Hz'3
We will
prove ∀ z'' ∈ Ry , z' < z'' .
Let z'' be given.
Assume Hz''1 .
Apply SNoLtLe_or z' z'' Hz'1 (HLRy2 z'' Hz''1 to the current goal.
Assume H .
An exact proof term for the current goal is H
Apply HC
We use z'' witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz''1
An exact proof term for the current goal is Hz''2
Apply L5a
Assume _ .
Apply Hyz'
An exact proof term for the current goal is Hz'2
Apply L5
Let z'' be given.
Assume H .
Apply H
rewrite the current goal using Hze
We will
prove v < x + z' .
We will
prove v < x + z'' .
Apply Hv4
We will
prove x + z'' ∈ Rx' ∪ Ry' .
We will
prove x + z'' ∈ Ry' .
An
exact proof term for the current goal is
ReplI Ry (λz ⇒ x + z ) z'' Hz''1 .
We will
prove x + z'' ≤ x + z' .
Apply add_SNo_Le2 x z'' z' Hx1 (HLRy2 z'' Hz''1 Hz'1 to the current goal.
An exact proof term for the current goal is Hz''2
rewrite the current goal using
add_SNo_eq x Hx1 y Hy1 (from right to left).
We will
prove ∀ w ∈ Lx' ∪ Ly' , w < x + y .
Let w be given.
Let w' be given.
rewrite the current goal using Hwe
We will
prove w' + y < x + y .
Apply add_SNo_Lt1 w' y x (HLRx1 w' Hw' Hy1 Hx1 to the current goal.
An exact proof term for the current goal is Hx3 w' Hw'
Let w' be given.
rewrite the current goal using Hwe
We will
prove x + w' < x + y .
Apply add_SNo_Lt2 x w' y Hx1 (HLRy1 w' Hw' Hy1 to the current goal.
An exact proof term for the current goal is Hy3 w' Hw'
rewrite the current goal using
add_SNo_eq x Hx1 y Hy1 (from right to left).
We will
prove ∀ z ∈ Rx' ∪ Ry' , x + y < z .
Let z be given.
Let z' be given.
rewrite the current goal using Hze
We will
prove x + y < z' + y .
Apply add_SNo_Lt1 x y z' Hx1 Hy1 (HLRx2 z' Hz' to the current goal.
An exact proof term for the current goal is Hx4 z' Hz'
Let z' be given.
rewrite the current goal using Hze
We will
prove x + y < x + z' .
Apply add_SNo_Lt2 x y z' Hx1 Hy1 (HLRy2 z' Hz' to the current goal.
An exact proof term for the current goal is Hy4 z' Hz'
∎
Proof: Let Lx, Rx, Ly, Ry, x and y be given.
Assume HLRx HLRy Hxe Hye .
Apply add_SNoCutP_lem Lx Rx Ly Ry x y HLRx HLRy Hxe Hye to the current goal.
Assume H _ .
An exact proof term for the current goal is H
∎
Proof: Let Lx, Rx, Ly, Ry, x and y be given.
Assume HLRx HLRy Hxe Hye .
Apply add_SNoCutP_lem Lx Rx Ly Ry x y HLRx HLRy Hxe Hye to the current goal.
Assume _ H .
An exact proof term for the current goal is H
∎
Proof: Let Lx, Rx, Ly, Ry, x and y be given.
Assume HLRx HLRy Hxe Hye .
Apply HLRx
Assume H .
Apply H
Apply HLRy
Assume H .
Apply H
rewrite the current goal using Hxe
rewrite the current goal using Hye
We prove the intermediate
claim Lxy :
SNo (x + y .
An
exact proof term for the current goal is
SNo_add_SNo x y Hx1 Hy1 .
Let u be given.
Apply dneg to the current goal.
Apply SNoLtLe_tra u (x + y u Hu1 Lxy Hu1 Hu3 to the current goal.
Set Lxy1 to be the term
{ w + y | w ∈ Lx } .
Set Lxy2 to be the term
{ x + w | w ∈ Ly } .
Set Rxy1 to be the term
{ z + y | z ∈ Rx } .
Set Rxy2 to be the term
{ x + z | z ∈ Ry } .
rewrite the current goal using
add_SNoCut_eq Lx Rx Ly Ry x y HLRx HLRy Hxe Hye (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).
An
exact proof term for the current goal is
add_SNoCutP_gen Lx Rx Ly Ry x y HLRx HLRy Hxe Hye .
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.
Apply binunionE Lxy1 Lxy2 w Hw to the current goal.
Let v be given.
rewrite the current goal using Hwv
We prove the intermediate
claim Lvy :
SNo (v + y .
An
exact proof term for the current goal is
SNo_add_SNo v y (HLRx1 v Hv Hy1 .
Apply SNoLtLe_or (v + y u Lvy Hu1 to the current goal.
An exact proof term for the current goal is H1
Apply HNC
Apply orIL to the current goal.
We use v witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv
An exact proof term for the current goal is H1
Let v be given.
rewrite the current goal using Hwv
We prove the intermediate
claim Lxv :
SNo (x + v .
An
exact proof term for the current goal is
SNo_add_SNo x v Hx1 (HLRy1 v Hv .
Apply SNoLtLe_or (x + v u Lxv Hu1 to the current goal.
An exact proof term for the current goal is H1
Apply HNC
Apply orIR to the current goal.
We use v witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv
An exact proof term for the current goal is H1
rewrite the current goal using
add_SNoCut_eq Lx Rx Ly Ry x y HLRx HLRy Hxe Hye (from right to left).
Let z be given.
Apply SNoR_E u Hu1 z Hz to the current goal.
Assume H1 .
Apply H1
An exact proof term for the current goal is H1
rewrite the current goal using H1
An exact proof term for the current goal is Hu2
An
exact proof term for the current goal is
SNoR_SNoS_ u z Hz .
Assume Hxy1 _ .
An
exact proof term for the current goal is
Hxy1 (SNoLev u Hu2 (SNoLev z Hz2 .
Apply IH z Lz1 Lz2 H1
Apply H2
Let v be given.
Assume H3 .
Apply H3
Apply HNC
Apply orIL to the current goal.
We use v witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv
An exact proof term for the current goal is Hz3
An exact proof term for the current goal is H3
Apply H2
Let v be given.
Assume H3 .
Apply H3
Apply HNC
Apply orIR to the current goal.
We use v witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv
An exact proof term for the current goal is Hz3
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.
An exact proof term for the current goal is LI u Hu1 Hu2 Hu3
∎
Proof: Let Lx, Rx, Ly, Ry, x and y be given.
Assume HLRx HLRy Hxe Hye .
Apply HLRx
Assume H .
Apply H
Apply HLRy
Assume H .
Apply H
rewrite the current goal using Hxe
rewrite the current goal using Hye
We prove the intermediate
claim Lxy :
SNo (x + y .
An
exact proof term for the current goal is
SNo_add_SNo x y Hx1 Hy1 .
Let u be given.
Apply dneg to the current goal.
Apply (λH : u ≤ x + y SNoLeLt_tra u (x + y u Hu1 Lxy Hu1 H Hu3 ) to the current goal.
Set Lxy1 to be the term
{ w + y | w ∈ Lx } .
Set Lxy2 to be the term
{ x + w | w ∈ Ly } .
Set Rxy1 to be the term
{ z + y | z ∈ Rx } .
Set Rxy2 to be the term
{ x + z | z ∈ Ry } .
rewrite the current goal using
add_SNoCut_eq Lx Rx Ly Ry x y HLRx HLRy Hxe Hye (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).
An
exact proof term for the current goal is
add_SNoCutP_gen Lx Rx Ly Ry x y HLRx HLRy Hxe Hye .
rewrite the current goal using
add_SNoCut_eq Lx Rx Ly Ry x y HLRx HLRy Hxe Hye (from right to left).
Let z be given.
Apply SNoL_E u Hu1 z Hz to the current goal.
Assume H1 .
Apply H1
An exact proof term for the current goal is H1
rewrite the current goal using H1
An exact proof term for the current goal is Hu2
An
exact proof term for the current goal is
SNoL_SNoS_ u z Hz .
Assume Hxy1 _ .
An
exact proof term for the current goal is
Hxy1 (SNoLev u Hu2 (SNoLev z Hz2 .
Apply IH z Lz1 Lz2 H1
Apply H2
Let v be given.
Assume H3 .
Apply H3
Apply HNC
Apply orIL to the current goal.
We use v witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv
An exact proof term for the current goal is H3
An exact proof term for the current goal is Hz3
Apply H2
Let v be given.
Assume H3 .
Apply H3
Apply HNC
Apply orIR to the current goal.
We use v witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv
An exact proof term for the current goal is H3
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.
Apply binunionE Rxy1 Rxy2 w Hw to the current goal.
Let v be given.
rewrite the current goal using Hwv
We prove the intermediate
claim Lvy :
SNo (v + y .
An
exact proof term for the current goal is
SNo_add_SNo v y (HLRx2 v Hv Hy1 .
Apply SNoLtLe_or u (v + y Hu1 Lvy to the current goal.
An exact proof term for the current goal is H1
Apply HNC
Apply orIL to the current goal.
We use v witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv
An exact proof term for the current goal is H1
Let v be given.
rewrite the current goal using Hwv
We prove the intermediate
claim Lxv :
SNo (x + v .
An
exact proof term for the current goal is
SNo_add_SNo x v Hx1 (HLRy2 v Hv .
Apply SNoLtLe_or u (x + v Hu1 Lxv to the current goal.
An exact proof term for the current goal is H1
Apply HNC
Apply orIR to the current goal.
We use v witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv
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.
An exact proof term for the current goal is LI u Hu1 Hu2 Hu3
∎
Proof: Let x, y, z, w, u and v be given.
Assume Hx Hy Hz Hw Hu Hv .
We will
prove x + y + - z < w + u + - v .
We prove the intermediate
claim Lmv :
SNo (- v .
We will
prove x + y < (w + u + - v + z .
rewrite the current goal using
add_SNo_assoc w u (- v Hw Hu Lmv (from left to right).
We will
prove x + y < ((w + u + - v + z .
We will
prove x + y < ((w + u + z + - v .
We will
prove (x + y + v < (w + u + z .
rewrite the current goal using
add_SNo_assoc x y v Hx Hy Hv (from right to left).
rewrite the current goal using
add_SNo_assoc w u z Hw Hu 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 .
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
rewrite the current goal using L2
We will
prove (x + y + - y ≤ (z + y + - y .
∎
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, 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, w, u and v be given.
Assume Hx Hy Hz Hw Hu Hv .
We will
prove x + y + - z ≤ w + u + - v .
We prove the intermediate
claim Lmv :
SNo (- v .
We will
prove x + y ≤ (w + u + - v + z .
rewrite the current goal using
add_SNo_assoc w u (- v Hw Hu Lmv (from left to right).
We will
prove x + y ≤ ((w + u + - v + z .
We will
prove x + y ≤ ((w + u + z + - v .
We will
prove (x + y + v ≤ (w + u + z .
rewrite the current goal using
add_SNo_assoc x y v Hx Hy Hv (from right to left).
rewrite the current goal using
add_SNo_assoc w u z Hw Hu Hz (from right to left).
An exact proof term for the current goal is H1
∎
End of Section SurrealAdd