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. (
setminusE2 ) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y → z ∉ Y 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. (
eq_1_Sing0 ) We take the following as an axiom:
Axiom. (
setsum_0_0 ) We take the following as an axiom:
Beginning of Section pair_setsum
Axiom. (
pairI0 ) We take the following as an axiom:
∀X Y x, x ∈ X pair 0 x ∈ pair X Y Axiom. (
pairI1 ) We take the following as an axiom:
∀X Y y, y ∈ Y pair 1 y ∈ pair X Y Axiom. (
pairE ) We take the following as an axiom:
∀X Y z, z ∈ pair X Y (∃ x ∈ X , z = pair 0 x ∨ (∃ y ∈ Y , z = pair 1 y Axiom. (
pairE0 ) We take the following as an axiom:
∀X Y x, pair 0 x ∈ pair X Y x ∈ X Axiom. (
pairE1 ) We take the following as an axiom:
∀X Y y, pair 1 y ∈ pair X Y y ∈ Y Axiom. (
proj0I ) We take the following as an axiom:
Axiom. (
proj0E ) We take the following as an axiom:
Axiom. (
proj1I ) We take the following as an axiom:
Axiom. (
proj1E ) We take the following as an axiom:
Definition. We define
Sigma to be
λX Y ⇒ ⋃ x ∈ X { pair x y | y ∈ Y x } of type
set → (set → set → set .
Notation . We use
∑ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Sigma .
Axiom. (
pair_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀ x ∈ X , ∀ y ∈ Y x , pair x y ∈ ∑ x ∈ X , Y x Axiom. (
proj0_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀z : set , z ∈ (∑ x ∈ X , Y x proj0 z ∈ X Axiom. (
proj1_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀z : set , z ∈ (∑ x ∈ X , Y x proj1 z ∈ Y (proj0 z Axiom. (
pair_Sigma_E1 ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀x y : set , pair x y ∈ (∑ x ∈ X , Y x y ∈ Y x Axiom. (
Sigma_E ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀z : set , z ∈ (∑ x ∈ X , Y x ∃ x ∈ X , ∃ y ∈ Y x , z = pair x y Definition. We define
setprod to be
λX Y : set ⇒ ∑ x ∈ X , Y of type
set → set → set .
Notation . We use
⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term
setprod .
Let lam : set → (set → set → set Sigma Definition. We define
ap to be
λf x ⇒ { proj1 z | z ∈ f , ∃ y : set , z = pair x y } of type
set → set → set .
Notation . When
x is a set, a term
x y is notation for
ap x y .
Notation .
λ x ∈ A ⇒ B is notation for the set
Sigma A (λ x : set ⇒ B ).
Notation . We now use n-tuple notation (
a0 ,...,
an-1 ) for n ≥ 2 for λ i ∈
n .
if i = 0
then a0 else ... if i =
n-2 then an-2 else an-1 .
Axiom. (
lamI ) We take the following as an axiom:
∀X : set , ∀F : set → set ∀ x ∈ X , ∀ y ∈ F x , pair x y ∈ λ x ∈ X ⇒ F x Axiom. (
lamE ) We take the following as an axiom:
∀X : set , ∀F : set → set ∀z : set , z ∈ (λ x ∈ X ⇒ F x ∃ x ∈ X , ∃ y ∈ F x , z = pair x y Axiom. (
apI ) We take the following as an axiom:
∀f x y, pair x y ∈ f y ∈ f x Axiom. (
apE ) We take the following as an axiom:
∀f x y, y ∈ f x pair x y ∈ f Axiom. (
beta ) We take the following as an axiom:
∀X : set , ∀F : set → set ∀x : set , x ∈ X (λ x ∈ X ⇒ F x x = F x Axiom. (
proj0_ap_0 ) We take the following as an axiom:
Axiom. (
proj1_ap_1 ) We take the following as an axiom:
Axiom. (
pair_ap_0 ) We take the following as an axiom:
∀x y : set , (pair x y 0 = x Axiom. (
pair_ap_1 ) We take the following as an axiom:
∀x y : set , (pair x y 1 = y Axiom. (
ap0_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀z : set , z ∈ (∑ x ∈ X , Y x (z 0 ∈ X Axiom. (
ap1_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀z : set , z ∈ (∑ x ∈ X , Y x (z 1 ∈ (Y (z 0 Definition. We define
pair_p to be
λu : set ⇒ pair (u 0 (u 1 = u of type
set → prop .
Axiom. (
pair_p_I ) We take the following as an axiom:
Axiom. (
tuple_pair ) We take the following as an axiom:
∀x y : set , pair x y = ( x , y ) Definition. We define
Pi to be
λX Y ⇒ { f ∈ 𝒫 (∑ x ∈ X , ⋃ (Y x | ∀ x ∈ X , f x ∈ Y x } of type
set → (set → set → set .
Notation . We use
∏ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Pi .
Axiom. (
PiI ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀f : set , (∀ u ∈ f , pair_p u ∧ u 0 ∈ X → (∀ x ∈ X , f x ∈ Y x → f ∈ ∏ x ∈ X , Y x Axiom. (
lam_Pi ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀F : set → set (∀ x ∈ X , F x ∈ Y x → (λ x ∈ X ⇒ F x ∈ (∏ x ∈ X , Y x Axiom. (
ap_Pi ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀f : set , ∀x : set , f ∈ (∏ x ∈ X , Y x x ∈ X f x ∈ Y x Definition. We define
setexp to be
λX Y : set ⇒ ∏ y ∈ Y , X of type
set → set → set .
Notation . We use
:^: as an infix operator with priority 430 and which associates to the left corresponding to applying term
setexp .
Axiom. (
lamI2 ) We take the following as an axiom:
Beginning of Section Tuples
Variable x0 x1 : set
End of Section Tuples
End of Section pair_setsum
Notation . We use
∑ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Sigma .
Notation . We use
⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term
setprod .
Notation . We use
∏ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Pi .
Notation . We use
:^: as an infix operator with priority 430 and which associates to the left corresponding to applying term
setexp .
Primitive . The name
DescrR_i_io_1 is a term of type
(set → (set → prop → prop → set .
Primitive . The name
DescrR_i_io_2 is a term of type
(set → (set → prop → prop → set → prop .
Definition. We define
PNoEq_ to be
λalpha p q ⇒ ∀ beta ∈ alpha , p beta ↔ q beta of type
set → (set → prop → (set → prop → prop .
Axiom. (
PNoEq_ref_ ) We take the following as an axiom:
∀alpha, ∀p : set → prop PNoEq_ alpha p p Axiom. (
PNoEq_sym_ ) We take the following as an axiom:
∀alpha, ∀p q : set → prop PNoEq_ alpha p q PNoEq_ alpha q p Axiom. (
PNoEq_tra_ ) We take the following as an axiom:
Axiom. (
PNoLt_E_ ) We take the following as an axiom:
Axiom. (
PNoLt_irref_ ) We take the following as an axiom:
∀alpha, ∀p : set → prop ¬ PNoLt_ alpha p p Axiom. (
PNoLt_mon_ ) We take the following as an axiom:
Axiom. (
PNoLt_tra_ ) We take the following as an axiom:
Primitive . The name
PNoLt is a term of type
set → (set → prop → set → (set → prop → prop .
Axiom. (
PNoLtI1 ) We take the following as an axiom:
Axiom. (
PNoLtI2 ) We take the following as an axiom:
Axiom. (
PNoLtI3 ) We take the following as an axiom:
Axiom. (
PNoLtE ) We take the following as an axiom:
Axiom. (
PNoLt_irref ) We take the following as an axiom:
∀alpha, ∀p : set → prop ¬ PNoLt alpha p alpha p Axiom. (
PNoLtEq_tra ) We take the following as an axiom:
Axiom. (
PNoEqLt_tra ) We take the following as an axiom:
Axiom. (
PNoLt_tra ) We take the following as an axiom:
Definition. We define
PNoLe to be
λalpha p beta q ⇒ PNoLt alpha p beta q ∨ alpha = beta ∧ PNoEq_ alpha p q of type
set → (set → prop → set → (set → prop → prop .
Axiom. (
PNoLeI1 ) We take the following as an axiom:
Axiom. (
PNoLeI2 ) We take the following as an axiom:
∀alpha, ∀p q : set → prop PNoEq_ alpha p q PNoLe alpha p alpha q Axiom. (
PNoLe_ref ) We take the following as an axiom:
∀alpha, ∀p : set → prop PNoLe alpha p alpha p Axiom. (
PNoLtLe_tra ) We take the following as an axiom:
Axiom. (
PNoLeLt_tra ) We take the following as an axiom:
Axiom. (
PNoEqLe_tra ) We take the following as an axiom:
Axiom. (
PNoLe_tra ) We take the following as an axiom:
Axiom. (
PNoLe_downc ) We take the following as an axiom:
Axiom. (
PNo_downc_ref ) We take the following as an axiom:
∀L : set → (set → prop → prop ∀alpha, ordinal alpha ∀p : set → prop L alpha p PNo_downc L alpha p Axiom. (
PNo_upc_ref ) We take the following as an axiom:
∀R : set → (set → prop → prop ∀alpha, ordinal alpha ∀p : set → prop R alpha p PNo_upc R alpha p Axiom. (
PNoLe_upc ) We take the following as an axiom:
Definition. We define
PNoLt_pwise to be
λL R ⇒ ∀gamma, ordinal gamma ∀p : set → prop L gamma p ∀delta, ordinal delta ∀q : set → prop R delta q PNoLt gamma p delta q of type
(set → (set → prop → prop → (set → (set → prop → prop → prop .
Axiom. (
PNo_extend0_eq ) We take the following as an axiom:
∀alpha, ∀p : set → prop PNoEq_ alpha p (λdelta ⇒ p delta ∧ delta ≠ alpha ) Axiom. (
PNo_extend1_eq ) We take the following as an axiom:
∀alpha, ∀p : set → prop PNoEq_ alpha p (λdelta ⇒ p delta ∨ delta = alpha ) Definition. We define
PNo_lenbdd to be
λalpha L ⇒ ∀beta, ∀p : set → prop L beta p beta ∈ alpha of type
set → (set → (set → prop → prop → prop .
Definition. We define
PNo_least_rep2 to be
λL R beta p ⇒ PNo_least_rep L R beta p ∧ ∀x, x ∉ beta ¬ p x of type
(set → (set → prop → prop → (set → (set → prop → prop → set → (set → prop → prop .
Primitive . The name
PNo_bd is a term of type
(set → (set → prop → prop → (set → (set → prop → prop → set .
Primitive . The name
PNo_pred is a term of type
(set → (set → prop → prop → (set → (set → prop → prop → set → prop .
Axiom. (
PNo_bd_pred ) We take the following as an axiom:
Axiom. (
PNo_bd_In ) We take the following as an axiom:
Beginning of Section TaggedSets
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
tag .
Definition. We define
SNoElts_ to be
λalpha ⇒ alpha ∪ { beta ' | beta ∈ alpha } of type
set → set .
Axiom. (
SNoElts_mon ) We take the following as an axiom:
Axiom. (
PNoEq_PSNo ) We take the following as an axiom:
Axiom. (
SNo_PSNo ) We take the following as an axiom:
Primitive . The name
SNo is a term of type
set → prop .
Axiom. (
SNo_SNo ) We take the following as an axiom:
Primitive . The name
SNoLev is a term of type
set → set .
Axiom. (
SNoLev_uniq ) We take the following as an axiom:
Axiom. (
SNoLev_prop ) We take the following as an axiom:
Axiom. (
SNoLev_ ) We take the following as an axiom:
Axiom. (
SNoLev_PSNo ) We take the following as an axiom:
Axiom. (
SNo_Subq ) We take the following as an axiom:
Definition. We define
SNoEq_ to be
λalpha x y ⇒ PNoEq_ alpha (λbeta ⇒ beta ∈ x ) (λbeta ⇒ beta ∈ y ) of type
set → set → set → prop .
Axiom. (
SNoEq_I ) We take the following as an axiom:
Axiom. (
SNo_eq ) We take the following as an axiom:
End of Section TaggedSets
Notation . We use
< as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLt .
Notation . We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLe .
Axiom. (
SNoLtLe ) We take the following as an axiom:
Axiom. (
SNoLeE ) We take the following as an axiom:
Axiom. (
SNoEq_sym_ ) We take the following as an axiom:
Axiom. (
SNoEq_tra_ ) We take the following as an axiom:
Axiom. (
SNoLtE ) We take the following as an axiom:
Axiom. (
SNoLtI2 ) We take the following as an axiom:
Axiom. (
SNoLtI3 ) We take the following as an axiom:
Axiom. (
SNoLt_irref ) We take the following as an axiom:
Axiom. (
SNoLt_tra ) We take the following as an axiom:
Axiom. (
SNoLe_ref ) We take the following as an axiom:
Axiom. (
SNoLtLe_tra ) We take the following as an axiom:
Axiom. (
SNoLeLt_tra ) We take the following as an axiom:
Axiom. (
SNoLe_tra ) We take the following as an axiom:
Axiom. (
SNoLtLe_or ) We take the following as an axiom:
Axiom. (
SNoCutP_L_0 ) We take the following as an axiom:
Axiom. (
SNoCutP_0_R ) We take the following as an axiom:
Axiom. (
SNoCutP_0_0 ) We take the following as an axiom:
Axiom. (
SNoS_E ) We take the following as an axiom:
Beginning of Section TaggedSets2
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
tag .
Axiom. (
SNoS_I ) We take the following as an axiom:
Axiom. (
SNoS_I2 ) We take the following as an axiom:
Axiom. (
SNoS_Subq ) We take the following as an axiom:
Axiom. (
SNoS_E2 ) We take the following as an axiom:
Axiom. (
SNoS_In_neq ) We take the following as an axiom:
Axiom. (
SNoS_SNoLev ) We take the following as an axiom:
Axiom. (
SNoL_E ) We take the following as an axiom:
Axiom. (
SNoR_E ) We take the following as an axiom:
Axiom. (
SNoL_SNoS_ ) We take the following as an axiom:
Axiom. (
SNoR_SNoS_ ) We take the following as an axiom:
Axiom. (
SNoL_SNoS ) We take the following as an axiom:
Axiom. (
SNoR_SNoS ) We take the following as an axiom:
Axiom. (
SNoL_I ) We take the following as an axiom:
Axiom. (
SNoR_I ) We take the following as an axiom:
Axiom. (
SNo_eta ) We take the following as an axiom:
Axiom. (
SNoCut_Le ) We take the following as an axiom:
Axiom. (
SNoCut_ext ) We take the following as an axiom:
Axiom. (
ordinal_SNo ) We take the following as an axiom:
Axiom. (
nat_p_SNo ) We take the following as an axiom:
Axiom. (
omega_SNo ) We take the following as an axiom:
Axiom. (
SNo_0 ) We take the following as an axiom:
Axiom. (
SNo_1 ) We take the following as an axiom:
Axiom. (
SNo_2 ) We take the following as an axiom:
Axiom. (
SNoLev_0 ) We take the following as an axiom:
Axiom. (
SNoCut_0_0 ) We take the following as an axiom:
Axiom. (
SNoL_0 ) We take the following as an axiom:
Axiom. (
SNoR_0 ) We take the following as an axiom:
Axiom. (
SNoL_1 ) We take the following as an axiom:
Axiom. (
SNoR_1 ) We take the following as an axiom:
Axiom. (
eps_0_1 ) We take the following as an axiom:
Axiom. (
SNo__eps_ ) We take the following as an axiom:
Axiom. (
SNo_eps_ ) We take the following as an axiom:
Axiom. (
SNo_eps_1 ) We take the following as an axiom:
Axiom. (
SNoLev_eps_ ) We take the following as an axiom:
Axiom. (
SNo_eps_pos ) We take the following as an axiom:
Axiom. (
eps_SNo_eq ) We take the following as an axiom:
Axiom. (
eps_SNoCutP ) We take the following as an axiom:
Axiom. (
eps_SNoCut ) We take the following as an axiom:
End of Section TaggedSets2
Axiom. (
SNo_etaE ) We take the following as an axiom:
Axiom. (
SNo_ind ) We take the following as an axiom:
Beginning of Section SurrealRecI
Variable F : set → (set → set → set
Primitive . The name
SNo_rec_i is a term of type
set → set .
Hypothesis Fr : ∀z, SNo z ∀g h : set → set (∀ w ∈ SNoS_ (SNoLev z , g w = h w → F z g = F z h End of Section SurrealRecI
Beginning of Section SurrealRecII
Variable F : set → (set → (set → set → (set → set
Let G : set → (set → set → (set → set → set → (set → set λalpha g ⇒ If_iii (ordinal alpha (λz : set ⇒ If_ii (z ∈ SNoS_ (ordsucc alpha (F z (λw ⇒ g (SNoLev w w ) default ) (λz : set ⇒ default ) Primitive . The name
SNo_rec_ii is a term of type
set → (set → set .
Hypothesis Fr : ∀z, SNo z ∀g h : set → (set → set (∀ w ∈ SNoS_ (SNoLev z , g w = h w → F z g = F z h End of Section SurrealRecII
Beginning of Section SurrealRec2
Variable F : set → set → (set → set → set → set
Let G : set → (set → set → set → set → (set → set → set λw f z g ⇒ F w z (λx y ⇒ if x = w then g y else f x y ) Primitive . The name
SNo_rec2 is a term of type
set → set → set .
Axiom. (
SNo_rec2_eq ) We take the following as an axiom:
End of Section SurrealRec2
Axiom. (
SNoLev_ind ) We take the following as an axiom:
Axiom. (
SNoLev_ind2 ) We take the following as an axiom:
Axiom. (
SNoLev_ind3 ) We take the following as an axiom:
∀P : set → set → set → prop (∀x y z, SNo x SNo y SNo z (∀ u ∈ SNoS_ (SNoLev x , P u y z → (∀ v ∈ SNoS_ (SNoLev y , P x v z → (∀ w ∈ SNoS_ (SNoLev z , P x y w → (∀ u ∈ SNoS_ (SNoLev x , ∀ v ∈ SNoS_ (SNoLev y , P u v z → (∀ u ∈ SNoS_ (SNoLev x , ∀ w ∈ SNoS_ (SNoLev z , P u y w → (∀ v ∈ SNoS_ (SNoLev y , ∀ w ∈ SNoS_ (SNoLev z , P x v w → (∀ u ∈ SNoS_ (SNoLev x , ∀ v ∈ SNoS_ (SNoLev y , ∀ w ∈ SNoS_ (SNoLev z , P u v w → P x y z ) → ∀x y z, SNo x SNo y SNo z P x y z Axiom. (
SNo_omega ) We take the following as an axiom:
Axiom. (
SNoLt_0_1 ) We take the following as an axiom:
Axiom. (
SNoLt_0_2 ) We take the following as an axiom:
Axiom. (
SNoLt_1_2 ) We take the following as an axiom:
Axiom. (
restr_SNo_ ) We take the following as an axiom:
Axiom. (
restr_SNo ) We take the following as an axiom:
Axiom. (
restr_SNoEq ) We take the following as an axiom:
Beginning of Section SurrealMinus
Primitive . The name
minus_SNo is a term of type
set → set .
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo .
Notation . We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLe .
End of Section SurrealMinus
Beginning of Section SurrealAdd
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo .
Primitive . The name
add_SNo is a term of type
set → set → set .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo .
Axiom. (
add_SNo_eq ) We take the following as an axiom:
Axiom. (
SNo_add_SNo ) We take the following as an axiom:
Axiom. (
add_SNo_Lt1 ) We take the following as an axiom:
Axiom. (
add_SNo_Le1 ) We take the following as an axiom:
Axiom. (
add_SNo_Lt2 ) We take the following as an axiom:
Axiom. (
add_SNo_Le2 ) We take the following as an axiom:
Axiom. (
add_SNo_Lt3 ) We take the following as an axiom:
Axiom. (
add_SNo_Le3 ) We take the following as an axiom:
Axiom. (
add_SNo_com ) We take the following as an axiom:
Axiom. (
add_SNo_0L ) We take the following as an axiom:
Axiom. (
add_SNo_0R ) We take the following as an axiom:
Axiom. (
minus_SNo_0 ) We take the following as an axiom:
Axiom. (
add_SNo_Lt4 ) We take the following as an axiom:
End of Section SurrealAdd
Beginning of Section SurrealMul
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo .
Axiom. (
mul_SNo_eq ) We take the following as an axiom:
Axiom. (
mul_SNo_eq_2 ) We take the following as an axiom:
∀x y, SNo x SNo y ∀p : prop , (∀L R, (∀u, u ∈ L (∀q : prop , (∀ w0 ∈ SNoL x , ∀ w1 ∈ SNoL y , u = w0 * y + x * w1 + - w0 * w1 q → (∀ z0 ∈ SNoR x , ∀ z1 ∈ SNoR y , u = z0 * y + x * z1 + - z0 * z1 q → q ) ) → (∀ w0 ∈ SNoL x , ∀ w1 ∈ SNoL y , w0 * y + x * w1 + - w0 * w1 ∈ L → (∀ z0 ∈ SNoR x , ∀ z1 ∈ SNoR y , z0 * y + x * z1 + - z0 * z1 ∈ L → (∀u, u ∈ R (∀q : prop , (∀ w0 ∈ SNoL x , ∀ z1 ∈ SNoR y , u = w0 * y + x * z1 + - w0 * z1 q → (∀ z0 ∈ SNoR x , ∀ w1 ∈ SNoL y , u = z0 * y + x * w1 + - z0 * w1 q → q ) ) → (∀ w0 ∈ SNoL x , ∀ z1 ∈ SNoR y , w0 * y + x * z1 + - w0 * z1 ∈ R → (∀ z0 ∈ SNoR x , ∀ w1 ∈ SNoL y , z0 * y + x * w1 + - z0 * w1 ∈ R → x * y = SNoCut L R p ) → p Axiom. (
mul_SNo_prop_1 ) We take the following as an axiom:
∀x, SNo x ∀y, SNo y ∀p : prop , (SNo (x * y (∀ u ∈ SNoL x , ∀ v ∈ SNoL y , u * y + x * v < x * y + u * v → (∀ u ∈ SNoR x , ∀ v ∈ SNoR y , u * y + x * v < x * y + u * v → (∀ u ∈ SNoL x , ∀ v ∈ SNoR y , x * y + u * v < u * y + x * v → (∀ u ∈ SNoR x , ∀ v ∈ SNoL y , x * y + u * v < u * y + x * v → p → p Axiom. (
SNo_mul_SNo ) We take the following as an axiom:
Axiom. (
mul_SNo_eq_3 ) We take the following as an axiom:
∀x y, SNo x SNo y ∀p : prop , (∀L R, SNoCutP L R (∀u, u ∈ L (∀q : prop , (∀ w0 ∈ SNoL x , ∀ w1 ∈ SNoL y , u = w0 * y + x * w1 + - w0 * w1 q → (∀ z0 ∈ SNoR x , ∀ z1 ∈ SNoR y , u = z0 * y + x * z1 + - z0 * z1 q → q ) ) → (∀ w0 ∈ SNoL x , ∀ w1 ∈ SNoL y , w0 * y + x * w1 + - w0 * w1 ∈ L → (∀ z0 ∈ SNoR x , ∀ z1 ∈ SNoR y , z0 * y + x * z1 + - z0 * z1 ∈ L → (∀u, u ∈ R (∀q : prop , (∀ w0 ∈ SNoL x , ∀ z1 ∈ SNoR y , u = w0 * y + x * z1 + - w0 * z1 q → (∀ z0 ∈ SNoR x , ∀ w1 ∈ SNoL y , u = z0 * y + x * w1 + - z0 * w1 q → q ) ) → (∀ w0 ∈ SNoL x , ∀ z1 ∈ SNoR y , w0 * y + x * z1 + - w0 * z1 ∈ R → (∀ z0 ∈ SNoR x , ∀ w1 ∈ SNoL y , z0 * y + x * w1 + - z0 * w1 ∈ R → x * y = SNoCut L R p ) → p Axiom. (
mul_SNo_Lt ) We take the following as an axiom:
Axiom. (
mul_SNo_Le ) We take the following as an axiom:
Axiom. (
mul_SNo_Subq_lem ) We take the following as an axiom:
∀x y X Y Z W, ∀U U', (∀u, u ∈ U (∀q : prop , (∀ w0 ∈ X , ∀ w1 ∈ Y , u = w0 * y + x * w1 + - w0 * w1 q → (∀ z0 ∈ Z , ∀ z1 ∈ W , u = z0 * y + x * z1 + - z0 * z1 q → q ) ) → (∀ w0 ∈ X , ∀ w1 ∈ Y , w0 * y + x * w1 + - w0 * w1 ∈ U' → (∀ w0 ∈ Z , ∀ w1 ∈ W , w0 * y + x * w1 + - w0 * w1 ∈ U' → U ⊆ U' Axiom. (
mul_SNo_com ) We take the following as an axiom:
Beginning of Section mul_SNo_assoc_lems
Variable M : set → set → set
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
M .
Hypothesis SNo_M : ∀x y, SNo x SNo y SNo (x * y Hypothesis DL : ∀x y z, SNo x SNo y SNo z x * (y + z = x * y + x * z Hypothesis DR : ∀x y z, SNo x SNo y SNo z (x + y * z = x * z + y * z Hypothesis M_Lt : ∀x y u v, SNo x SNo y SNo u SNo v u < x v < y u * y + x * v < x * y + u * v Hypothesis M_Le : ∀x y u v, SNo x SNo y SNo u SNo v u ≤ x v ≤ y u * y + x * v ≤ x * y + u * v Axiom. (
mul_SNo_assoc_lem1 ) We take the following as an axiom:
∀x y z, SNo x SNo y SNo z (∀ u ∈ SNoS_ (SNoLev x , u * (y * z = (u * y * z → (∀ v ∈ SNoS_ (SNoLev y , x * (v * z = (x * v * z → (∀ w ∈ SNoS_ (SNoLev z , x * (y * w = (x * y * w → (∀ u ∈ SNoS_ (SNoLev x , ∀ v ∈ SNoS_ (SNoLev y , u * (v * z = (u * v * z → (∀ u ∈ SNoS_ (SNoLev x , ∀ w ∈ SNoS_ (SNoLev z , u * (y * w = (u * y * w → (∀ v ∈ SNoS_ (SNoLev y , ∀ w ∈ SNoS_ (SNoLev z , x * (v * w = (x * v * w → (∀ u ∈ SNoS_ (SNoLev x , ∀ v ∈ SNoS_ (SNoLev y , ∀ w ∈ SNoS_ (SNoLev z , u * (v * w = (u * v * w → ∀L, (∀ u ∈ L , ∀q : prop , (∀ v ∈ SNoL x , ∀ w ∈ SNoL (y * z , u = v * (y * z + x * w + - v * w q → (∀ v ∈ SNoR x , ∀ w ∈ SNoR (y * z , u = v * (y * z + x * w + - v * w q → q → ∀ u ∈ L , u < (x * y * z Axiom. (
mul_SNo_assoc_lem2 ) We take the following as an axiom:
∀x y z, SNo x SNo y SNo z (∀ u ∈ SNoS_ (SNoLev x , u * (y * z = (u * y * z → (∀ v ∈ SNoS_ (SNoLev y , x * (v * z = (x * v * z → (∀ w ∈ SNoS_ (SNoLev z , x * (y * w = (x * y * w → (∀ u ∈ SNoS_ (SNoLev x , ∀ v ∈ SNoS_ (SNoLev y , u * (v * z = (u * v * z → (∀ u ∈ SNoS_ (SNoLev x , ∀ w ∈ SNoS_ (SNoLev z , u * (y * w = (u * y * w → (∀ v ∈ SNoS_ (SNoLev y , ∀ w ∈ SNoS_ (SNoLev z , x * (v * w = (x * v * w → (∀ u ∈ SNoS_ (SNoLev x , ∀ v ∈ SNoS_ (SNoLev y , ∀ w ∈ SNoS_ (SNoLev z , u * (v * w = (u * v * w → ∀R, (∀ u ∈ R , ∀q : prop , (∀ v ∈ SNoL x , ∀ w ∈ SNoR (y * z , u = v * (y * z + x * w + - v * w q → (∀ v ∈ SNoR x , ∀ w ∈ SNoL (y * z , u = v * (y * z + x * w + - v * w q → q → ∀ u ∈ R , (x * y * z < u End of Section mul_SNo_assoc_lems
Axiom. (
SNo_foil ) We take the following as an axiom:
Axiom. (
SNo_foil_mm ) We take the following as an axiom:
End of Section SurrealMul
Beginning of Section SurrealExp
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo .
Notation . We use
^ as an infix operator with priority 342 and which associates to the right corresponding to applying term
exp_SNo_nat .
Axiom. (
eps_bd_1 ) We take the following as an axiom:
Axiom. (
SNoS_finite ) We take the following as an axiom:
End of Section SurrealExp
Beginning of Section Int
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo .
Primitive . The name
int is a term of type
set .
Axiom. (
int_3_cases ) We take the following as an axiom:
Axiom. (
int_SNo ) We take the following as an axiom:
Axiom. (
int_add_SNo ) We take the following as an axiom:
Axiom. (
int_mul_SNo ) We take the following as an axiom:
End of Section Int
Beginning of Section SurrealAbs
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo .
Axiom. (
abs_SNo_0 ) We take the following as an axiom:
Axiom. (
pos_abs_SNo ) We take the following as an axiom:
Axiom. (
neg_abs_SNo ) We take the following as an axiom:
Axiom. (
SNo_abs_SNo ) We take the following as an axiom:
Axiom. (
abs_SNo_Lev ) We take the following as an axiom:
End of Section SurrealAbs
Beginning of Section SNoMaxMin
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo .
Notation . We use
^ as an infix operator with priority 342 and which associates to the right corresponding to applying term
exp_SNo_nat .
Notation . We use
< as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLt .
Notation . We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLe .
End of Section SNoMaxMin
Beginning of Section DiadicRationals
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo .
Notation . We use
< as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLt .
Notation . We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLe .
Notation . We use
^ as an infix operator with priority 342 and which associates to the right corresponding to applying term
exp_SNo_nat .
End of Section DiadicRationals
Beginning of Section SurrealDiv
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo .
Notation . We use
< as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLt .
Notation . We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLe .
Notation . We use
^ as an infix operator with priority 342 and which associates to the right corresponding to applying term
exp_SNo_nat .
Definition. We define
SNo_recipauxset to be
λY x X g ⇒ ⋃ y ∈ Y { (1 + (x' + - x * y * g x' | x' ∈ X } of type
set → set → set → (set → set → set .
Beginning of Section recip_SNo_pos
End of Section recip_SNo_pos
Axiom. (
recip_SNo_0 ) We take the following as an axiom:
Axiom. (
recip_SNo_1 ) We take the following as an axiom:
Axiom. (
recip_SNo_2 ) We take the following as an axiom:
Notation . We use
:/: as an infix operator with priority 353 and no associativity corresponding to applying term
div_SNo .
Axiom. (
SNo_div_SNo ) We take the following as an axiom:
Axiom. (
div_div_SNo ) We take the following as an axiom:
End of Section SurrealDiv
Beginning of Section SurrealSqrt
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo .
Notation . We use
:/: as an infix operator with priority 353 and no associativity corresponding to applying term
div_SNo .
Notation . We use
< as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLt .
Notation . We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLe .
Notation . We use
^ as an infix operator with priority 342 and which associates to the right corresponding to applying term
exp_SNo_nat .
Beginning of Section sqrt_SNo_nonneg
End of Section sqrt_SNo_nonneg
End of Section SurrealSqrt
Beginning of Section Reals
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo .
Notation . We use
:/: as an infix operator with priority 353 and no associativity corresponding to applying term
div_SNo .
Notation . We use
< as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLt .
Notation . We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLe .
Notation . We use
^ as an infix operator with priority 342 and which associates to the right corresponding to applying term
exp_SNo_nat .
Proof: Let x be given.
Assume Hx .
Assume Hx1 Hx2 Hx3 Hx4 .
Let k be given.
Assume Hk .
We use
x + - eps_ (ordsucc k to
witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
∎
Proof: Let x be given.
Assume Hx1 Hx2 .
Assume Hx1a Hx1b Hx1c Hx1d .
Let z be given.
An exact proof term for the current goal is Hz1
We prove the intermediate
claim Lz2 :
SNo (SNoLev z .
An exact proof term for the current goal is Lz1
We use
(SNoLev z to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz8
An exact proof term for the current goal is Hx1c
An exact proof term for the current goal is Lx1
We use
(ordsucc (SNoLev x to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H3
rewrite the current goal using H2
An exact proof term for the current goal is H1
∎
Proof: Let x be given.
Assume Hx1 Hx2 .
Assume Hx1a Hx1b Hx1c Hx1d .
We prove the intermediate
claim Lx2 :
- x < ω .
An exact proof term for the current goal is Hx2
Let N be given.
Assume HN .
Apply HN
We use N witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN1
An exact proof term for the current goal is HN2
∎
Proof: Let x be given.
Assume Hx1 Hx2 Hx3 .
Assume Hx1a Hx1b Hx1c Hx1d .
Apply dneg to the current goal.
We prove the intermediate
claim L1 :
x ∉ SNoS_ ω .
Apply HC
rewrite the current goal using
eps_0_1 (from left to right).
rewrite the current goal using
minus_SNo_0 (from left to right).
An
exact proof term for the current goal is
SNoLt_tra x 0 x Hx1c SNo_0 Hx1c H2 H1 .
Let N be given.
Assume HN .
We prove the intermediate
claim LN1 :
SNo N .
An
exact proof term for the current goal is
nat_p_SNo N HN .
We prove the intermediate
claim LN2 :
SNo (- N .
We prove the intermediate
claim LN3 :
N ∈ SNoS_ ω .
An
exact proof term for the current goal is
nat_p_omega N HN .
We use
(- ordsucc N to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN
Apply andI to the current goal.
An exact proof term for the current goal is H1
We will
prove x < - (N + 1 + 1 .
An exact proof term for the current goal is H4
Apply L1
rewrite the current goal using H4
An exact proof term for the current goal is LN3
An exact proof term for the current goal is IHN H4 H3
Apply L1
rewrite the current goal using H3
An exact proof term for the current goal is LN3
We use N witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is LN3
Apply andI to the current goal.
An exact proof term for the current goal is H3
An exact proof term for the current goal is H2
Let N be given.
Assume HN .
Apply HN
Let N' be given.
Assume HN' .
Apply HN'
Apply L1a N' (omega_nat_p N' HN'1 HN'2 to the current goal.
Apply L1a N' (omega_nat_p N' HN'1 HN'2 to the current goal.
rewrite the current goal using H1
An exact proof term for the current goal is HN2
We will
prove - N < - N' .
An exact proof term for the current goal is H1
An exact proof term for the current goal is HN'2
An exact proof term for the current goal is HN2
Let k be given.
Assume Hk .
Assume IHk .
Apply IHk
Let q be given.
Assume H .
Apply H
Assume H .
Apply H
Assume Hq1a Hq1b Hq1c Hq1d .
We use q witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hq1
Apply andI to the current goal.
An exact proof term for the current goal is Hq2
An exact proof term for the current goal is H1
Apply L1
rewrite the current goal using H1
We use
(q + eps_ (ordsucc k to
witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is H1
An exact proof term for the current goal is Hq3
Apply HC
Let k be given.
Assume Hk .
An
exact proof term for the current goal is
L2 k (omega_nat_p k Hk .
∎
Theorem. (
real_I ) The following is provable:
Proof: Let x be given.
Assume Hx H1 H2 H3 .
Apply SepI to the current goal.
An exact proof term for the current goal is Hx
Apply and3I to the current goal.
An exact proof term for the current goal is H1
An exact proof term for the current goal is H2
An exact proof term for the current goal is H3
∎
Theorem. (
real_E ) The following is provable:
Proof: Let x be given.
Assume Hx .
Let p be given.
Assume Hp .
Assume H1 H2 .
Apply H2
Assume H2 .
Apply H2
Assume H4 .
Assume H1a H1b H1c H1d .
We prove the intermediate
claim L1 :
x < ω .
We prove the intermediate
claim L1a :
x ≤ ω .
An exact proof term for the current goal is H1a
Assume H .
An exact proof term for the current goal is H
An exact proof term for the current goal is H2 H
We prove the intermediate
claim L2 :
- ω < x .
We prove the intermediate
claim L2a :
- ω ≤ x .
An exact proof term for the current goal is H1a
Assume H .
An exact proof term for the current goal is H
Apply H3
Use symmetry.
An exact proof term for the current goal is H
An exact proof term for the current goal is Hp H1c H1a H1 L2 L1 H4 L3
∎
Theorem. (
real_SNo ) The following is provable:
Proof: Let x be given.
Assume Hx .
Apply real_E x Hx to the current goal.
Assume Hx1 _ _ _ _ _ _ .
An exact proof term for the current goal is Hx1
∎
Proof: Let x be given.
Assume Hx .
Apply real_E x Hx to the current goal.
Assume _ _ _ _ _ Hx6 _ .
An exact proof term for the current goal is Hx6
∎
Proof: Let x be given.
Assume Hx1 Hx2 Hx3 Hx4 .
Apply real_I to the current goal.
An exact proof term for the current goal is Hx
rewrite the current goal using H1
An exact proof term for the current goal is Hx1
rewrite the current goal using H1
An exact proof term for the current goal is Hx1
Let q be given.
Assume Hq1 Hq2 Hq3 Hq4 .
We prove the intermediate
claim L1 :
0 < x + - q .
An exact proof term for the current goal is Hqx
We prove the intermediate
claim L2 :
x + - q ∈ SNoS_ ω .
We prove the intermediate
claim L3 :
abs_SNo (q + - x = x + - q .
An
exact proof term for the current goal is
pos_abs_SNo (x + - q L1 .
rewrite the current goal using L3
An
exact proof term for the current goal is
H1 (SNoLev (x + - q H2 .
An exact proof term for the current goal is H5
An exact proof term for the current goal is L1
An exact proof term for the current goal is Hqx
We prove the intermediate
claim L4 :
0 < q + - x .
An exact proof term for the current goal is Hxq
We prove the intermediate
claim L5 :
q + - x ∈ SNoS_ ω .
We prove the intermediate
claim L6 :
abs_SNo (q + - x = q + - x .
An
exact proof term for the current goal is
pos_abs_SNo (q + - x L4 .
rewrite the current goal using L6
An
exact proof term for the current goal is
H1 (SNoLev (q + - x H2 .
An exact proof term for the current goal is H5
An exact proof term for the current goal is L4
∎
Theorem. (
real_0 ) The following is provable:
Theorem. (
real_1 ) The following is provable:
Proof: Let x be given.
Assume Hx .
Let w be given.
Assume Hw1 Hw2 .
Apply real_E x Hx to the current goal.
Assume _ _ _ _ _ .
We prove the intermediate
claim L1 :
SNoLev w ∈ ω .
rewrite the current goal using H1
An exact proof term for the current goal is Hw2
An exact proof term for the current goal is Hw1
∎
Proof: Let L be given.
Assume HL .
Let R be given.
Assume HR .
Assume HLR .
Apply HLR
Assume H .
Apply H
Set x to be the term
SNoCut L R .
Let w be given.
Assume Hw .
An exact proof term for the current goal is HLR1 w Hw
Let z be given.
Assume Hz .
An exact proof term for the current goal is HLR2 z Hz
Assume H6 .
An exact proof term for the current goal is H6
Let w be given.
rewrite the current goal using H9
An exact proof term for the current goal is Hw1
Let z be given.
rewrite the current goal using H9
An exact proof term for the current goal is Hz1
An exact proof term for the current goal is H1
Apply real_I to the current goal.
rewrite the current goal using H6
An exact proof term for the current goal is H1
Apply HR0
Let z be given.
Apply SNoLt_tra z x z (HLR2 z Hz H1 (HLR2 z Hz to the current goal.
rewrite the current goal using H7
Assume _ _ _ .
An exact proof term for the current goal is Hz1
Apply H4
An exact proof term for the current goal is Hz
Apply HL0
Let w be given.
Apply SNoLt_tra w x w (HLR1 w Hw H1 (HLR1 w Hw to the current goal.
Apply H3
An exact proof term for the current goal is Hw
rewrite the current goal using H7
rewrite the current goal using
minus_SNo_Lev w (HLR1 w Hw (from left to right).
Assume _ _ _ .
An exact proof term for the current goal is Hw1
Let q be given.
We prove the intermediate
claim LqL :
∀ w ∈ L , w < q .
Let w be given.
Apply SNoLtLe_or w q (HLR1 w Hw Hq3 to the current goal.
An exact proof term for the current goal is H8
Apply HL1 w Hw
Let w' be given.
Assume H .
Apply H
We prove the intermediate
claim LqL1 :
w' + - q ∈ SNoS_ ω .
An exact proof term for the current goal is HL w' H9
An exact proof term for the current goal is Hq
We prove the intermediate
claim LqL2 :
0 < w' + - q .
An
exact proof term for the current goal is
SNoLeLt_tra q w w' Hq3 (HLR1 w Hw (HLR1 w' H9 H8 H10 .
We prove the intermediate
claim Lek :
SNo (eps_ k .
An
exact proof term for the current goal is
SNo_eps_ k Hw'q1 .
We prove the intermediate
claim LqL4 :
eps_ k < w' + - q .
We prove the intermediate
claim Lxq :
SNo (x + - q .
We will
prove w' + - q < x + - q .
Apply H3
An exact proof term for the current goal is H9
rewrite the current goal using
nonneg_abs_SNo (x + - q H11 (from right to left).
An exact proof term for the current goal is H7 k Hw'q1
We prove the intermediate
claim LqR :
∀ z ∈ R , q < z .
Let z be given.
Apply SNoLtLe_or q z Hq3 (HLR2 z Hz to the current goal.
An exact proof term for the current goal is H8
Apply HR1 z Hz
Let z' be given.
Assume H .
Apply H
We prove the intermediate
claim LqR1 :
q + - z' ∈ SNoS_ ω .
An exact proof term for the current goal is Hq
An exact proof term for the current goal is HR z' H9
We prove the intermediate
claim LqR2 :
0 < q + - z' .
An
exact proof term for the current goal is
SNoLtLe_tra z' z q (HLR2 z' H9 (HLR2 z Hz Hq3 H10 H8 .
We prove the intermediate
claim Lek :
SNo (eps_ k .
An
exact proof term for the current goal is
SNo_eps_ k Hz'q1 .
We prove the intermediate
claim LqR4 :
eps_ k < q + - z' .
We prove the intermediate
claim Lxq :
SNo (q + - x .
We will
prove q + - z' < q + - x .
We will
prove - z' < - x .
Apply H4
An exact proof term for the current goal is H9
rewrite the current goal using
nonneg_abs_SNo (q + - x H11 (from right to left).
An exact proof term for the current goal is H7 k Hz'q1
Apply H5 q Hq3 LqL LqR
Apply H10
rewrite the current goal using H6
An exact proof term for the current goal is Hq1
∎
Proof: Let L be given.
Assume HL .
Let R be given.
Assume HR .
Assume HLR .
Apply HLR
Assume H .
Apply H
Set x to be the term
SNoCut L R .
Set L_ to be the term
λn ⇒ { w' ∈ SNoS_ n | ∃ w ∈ L , w' ≤ w } of type
set → set .
Set R_ to be the term
λn ⇒ { z' ∈ SNoS_ n | ∃ z ∈ R , z ≤ z' } of type
set → set .
Set L' to be the term
⋃ n ∈ ω L_ n .
Set R' to be the term
⋃ n ∈ ω R_ n .
Set x' to be the term
SNoCut L' R' .
We prove the intermediate
claim LL'L :
∀ w' ∈ L' , ∃ w ∈ L , w' ≤ w .
Let w' be given.
Assume Hw' .
Let n be given.
An
exact proof term for the current goal is
SepE2 (SNoS_ n (λw' ⇒ ∃ w ∈ L , w' ≤ w ) w' Hw'2 .
We prove the intermediate
claim LR'R :
∀ z' ∈ R' , ∃ z ∈ R , z ≤ z' .
Let z' be given.
Assume Hz' .
Let n be given.
An
exact proof term for the current goal is
SepE2 (SNoS_ n (λz' ⇒ ∃ z ∈ R , z ≤ z' ) z' Hz'2 .
We prove the intermediate
claim LL'o :
L' ⊆ SNoS_ ω .
Let w' be given.
Assume Hw' .
Let n be given.
An exact proof term for the current goal is Hw'6
We prove the intermediate
claim LR'o :
R' ⊆ SNoS_ ω .
Let z' be given.
Assume Hz' .
Let n be given.
An exact proof term for the current goal is Hz'6
We prove the intermediate
claim LL' :
∀ w' ∈ L' , SNo w' .
Let w' be given.
Assume Hw' .
Assume _ _ H _ .
An exact proof term for the current goal is H
We prove the intermediate
claim LR' :
∀ z ∈ R' , SNo z .
Let z' be given.
Assume Hz' .
Assume _ _ H _ .
An exact proof term for the current goal is H
We prove the intermediate
claim LLR' :
SNoCutP L' R' .
Apply and3I to the current goal.
An exact proof term for the current goal is LL'
An exact proof term for the current goal is LR'
Let w' be given.
Assume Hw' .
Let z' be given.
Assume Hz' .
Apply LL'L w' Hw'
Let w be given.
Assume H .
Apply H
Apply LR'R z' Hz'
Let z be given.
Assume H .
Apply H
Apply SNoLeLt_tra w' w z' (LL' w' Hw' (HLR1 w Hw (LR' z' Hz' Hw'w to the current goal.
Apply SNoLtLe_tra w z z' (HLR1 w Hw (HLR2 z Hz (LR' z' Hz' to the current goal.
Apply HLR3
An exact proof term for the current goal is Hw
An exact proof term for the current goal is Hz
An exact proof term for the current goal is Hzz'
We prove the intermediate
claim L1 :
∀ w ∈ L , ∃ w' ∈ L' , w ≤ w' .
Let w be given.
Assume Hw .
Apply real_E w (HL w Hw to the current goal.
Assume _ _ _ _ _ .
We use w witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H6
Apply SepI to the current goal.
An exact proof term for the current goal is Hw1
We will
prove ∃ u ∈ L , w ≤ u .
We use w witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw
Apply HL1 w Hw
Let w' be given.
Assume H .
Apply H
Apply real_E w' (HL w' Hw' to the current goal.
Assume _ _ _ _ _ .
We use w' witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H7
Apply SepI to the current goal.
An exact proof term for the current goal is Hw'1
We will
prove ∃ u ∈ L , w' ≤ u .
We use w' witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw'
An exact proof term for the current goal is Hww'
Apply SNoLtE w w' Hw1 Hw'1 Hww' to the current goal.
Let w'' be given.
rewrite the current goal using H6
Assume _ _ .
Assume _ _ .
We use w'' witness the existential quantifier.
Apply andI to the current goal.
Apply SepI to the current goal.
An exact proof term for the current goal is Hw''1
We will
prove ∃ u ∈ L , w'' ≤ u .
We use w' witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw'
An exact proof term for the current goal is Hw''4
An exact proof term for the current goal is Hw''3
rewrite the current goal using H6
rewrite the current goal using H7
An
exact proof term for the current goal is
In_irref ω H8 .
rewrite the current goal using H6
rewrite the current goal using H7
An
exact proof term for the current goal is
In_irref ω H8 .
We prove the intermediate
claim L2 :
∀ z ∈ R , ∃ z' ∈ R' , z' ≤ z .
Let z be given.
Assume Hz .
Apply real_E z (HR z Hz to the current goal.
Assume _ _ _ _ _ .
We use z witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H6
Apply SepI to the current goal.
An exact proof term for the current goal is Hz1
We will
prove ∃ u ∈ R , u ≤ z .
We use z witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz
Apply HR1 z Hz
Let z' be given.
Assume H .
Apply H
Apply real_E z' (HR z' Hz' to the current goal.
Assume _ _ _ _ _ .
We use z' witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H7
Apply SepI to the current goal.
An exact proof term for the current goal is Hz'1
We will
prove ∃ u ∈ R , u ≤ z' .
We use z' witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz'
An exact proof term for the current goal is Hz'z
Apply SNoLtE z' z Hz'1 Hz1 Hz'z to the current goal.
Let z'' be given.
rewrite the current goal using H7
Assume _ _ .
Assume _ _ .
We use z'' witness the existential quantifier.
Apply andI to the current goal.
Apply SepI to the current goal.
An exact proof term for the current goal is Hz''1
We will
prove ∃ u ∈ R , u ≤ z'' .
We use z' witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz'
An exact proof term for the current goal is Hz''3
An exact proof term for the current goal is Hz''4
rewrite the current goal using H6
rewrite the current goal using H7
An
exact proof term for the current goal is
In_irref ω H8 .
rewrite the current goal using H6
rewrite the current goal using H7
An
exact proof term for the current goal is
In_irref ω H8 .
We prove the intermediate
claim L3 :
L' ≠ 0 .
Apply HL0
Let w be given.
Apply L1 w Hw
Let w' be given.
Assume H .
Apply H
Apply EmptyE w' to the current goal.
rewrite the current goal using H6
An exact proof term for the current goal is Hw'
We prove the intermediate
claim L4 :
R' ≠ 0 .
Apply HR0
Let z be given.
Apply L2 z Hz
Let z' be given.
Assume H .
Apply H
Apply EmptyE z' to the current goal.
rewrite the current goal using H6
An exact proof term for the current goal is Hz'
We prove the intermediate
claim L5 :
∀ w ∈ L' , ∃ w' ∈ L' , w < w' .
Let w be given.
Assume Hw .
Apply LL'L w Hw
Let u be given.
Assume H .
Apply H
Apply HL1 u Hu
Let v be given.
Assume H .
Apply H
Apply L1 v Hv
Let w' be given.
Assume H .
Apply H
We use w' witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw'
Apply SNoLeLt_tra w u w' (LL' w Hw (HLR1 u Hu (LL' w' Hw' Hwu to the current goal.
An
exact proof term for the current goal is
SNoLtLe_tra u v w' (HLR1 u Hu (HLR1 v Hv (LL' w' Hw' Huv Hvw' .
We prove the intermediate
claim L6 :
∀ z ∈ R' , ∃ z' ∈ R' , z' < z .
Let z be given.
Assume Hz .
Apply LR'R z Hz
Let u be given.
Assume H .
Apply H
Apply HR1 u Hu
Let v be given.
Assume H .
Apply H
Apply L2 v Hv
Let z' be given.
Assume H .
Apply H
We use z' witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz'
Apply SNoLeLt_tra z' v z (LR' z' Hz' (HLR2 v Hv (LR' z Hz Hz'v to the current goal.
An
exact proof term for the current goal is
SNoLtLe_tra v u z (HLR2 v Hv (HLR2 u Hu (LR' z Hz Hvu Huz .
We prove the intermediate
claim Lxx' :
x = x' .
An exact proof term for the current goal is HLR
An exact proof term for the current goal is LLR'
Let w be given.
Apply L1 w Hw
Let w' be given.
Assume H .
Apply H
An exact proof term for the current goal is HLR1 w Hw
An exact proof term for the current goal is LL' w' Hw'
An exact proof term for the current goal is H1'
An exact proof term for the current goal is Hww'
Apply H3'
An exact proof term for the current goal is Hw'
Let z be given.
Apply L2 z Hz
Let z' be given.
Assume H .
Apply H
An
exact proof term for the current goal is
SNoLtLe_tra x' z' z H1' (LR' z' Hz' (HLR2 z Hz (H4' z' Hz' Hz'z .
Let w be given.
Apply LL'L w Hw
Let u be given.
Assume H .
Apply H
An
exact proof term for the current goal is
SNoLeLt_tra w u x (LL' w Hw (HLR1 u Hu H1 Hwu (H3 u Hu .
Let z be given.
Apply LR'R z Hz
Let u be given.
Assume H .
Apply H
An
exact proof term for the current goal is
SNoLtLe_tra x u z H1 (HLR2 u Hu (LR' z Hz (H4 u Hu Huz .
rewrite the current goal using Lxx'
∎
Proof: Let x be given.
Assume Hx H1 .
Let q be given.
Assume Hq1a Hq1b Hq1c Hq1d .
rewrite the current goal using
minus_SNo_invol q Hq1c (from right to left).
We will
prove - - q = - x .
Use f_equal.
Let k be given.
Assume Hk .
rewrite the current goal using
minus_SNo_invol q Hq1c (from left to right).
rewrite the current goal using
add_SNo_com x q Hx Hq1c (from left to right).
An exact proof term for the current goal is Hq2 k Hk
∎
Proof: Let x be given.
Assume Hx H1 .
Let k be given.
Assume Hk .
Apply H1 k Hk
Let q be given.
Assume Hq .
Apply Hq
Assume Hq .
Apply Hq
Assume Hq1a Hq1b Hq1c Hq1d .
We prove the intermediate
claim Lqk :
SNo (q + eps_ k .
We use
(- (q + eps_ k to
witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hq3
An exact proof term for the current goal is Hq2
∎
Proof: Let x be given.
Assume Hx Hx0 Hx2 Hx3 .
Let k be given.
Assume Hk .
Let p be given.
Assume Hp .
Apply Hx3 k Hk
Let q be given.
Assume H .
Apply H
Assume H .
Apply H
Assume Hq1a Hq1b Hq1c Hq1d .
An exact proof term for the current goal is Hp q Hq1 H1 Hq2 Hq3
We prove the intermediate
claim L1 :
0 = x .
Let k' be given.
rewrite the current goal using
abs_SNo_minus x Hx (from left to right).
rewrite the current goal using
pos_abs_SNo x Hx0 (from left to right).
An exact proof term for the current goal is H2 k' Hk'
rewrite the current goal using L1
An exact proof term for the current goal is Hx0
Apply dneg to the current goal.
Apply H2
Let k' be given.
An exact proof term for the current goal is H4
We prove the intermediate
claim Lek' :
SNo (eps_ k' .
An exact proof term for the current goal is Hk'
An exact proof term for the current goal is Hk'
An exact proof term for the current goal is Hk'
Apply H3
An exact proof term for the current goal is Hk'
An exact proof term for the current goal is LeSk'pos
We will
prove eps_ k' ≤ x .
An exact proof term for the current goal is H4
An exact proof term for the current goal is H1
An exact proof term for the current goal is LeSk'pos
An exact proof term for the current goal is Hq3
An exact proof term for the current goal is L2
∎
Proof: Let x be given.
Assume Hx .
Apply real_E x Hx to the current goal.
Assume Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 .
Apply real_I to the current goal.
rewrite the current goal using
minus_SNo_invol x Hx1 (from right to left) at position 1.
rewrite the current goal using H1
An exact proof term for the current goal is Hx4
rewrite the current goal using
minus_SNo_invol x Hx1 (from right to left) at position 2.
rewrite the current goal using H1
An exact proof term for the current goal is Hx5
∎
Proof: Let x be given.
Assume H1 H2 H3 .
Set f to be the term
λn ∈ ω f' n .
rewrite the current goal using Lf'0
Let q be given.
Assume Hq .
Apply Hq
Assume Hq1 Hq .
Apply Hq
Assume Hq2 Hq3 .
We use q witness the existential quantifier.
Apply and3I to the current goal.
An exact proof term for the current goal is Hq1
An exact proof term for the current goal is Hq2
An exact proof term for the current goal is Hq3
Apply Lf'0b
Assume H H6 .
Apply H
Assume H4 H5 .
Apply and4I to the current goal.
An exact proof term for the current goal is H4
An exact proof term for the current goal is H5
An exact proof term for the current goal is H6
Let i be given.
Assume Hi .
An
exact proof term for the current goal is
EmptyE i Hi .
Let n be given.
Assume Hn .
Apply IHn
Assume IHn123 IHn4 .
Apply IHn123
Assume IHn12 IHn3 .
Apply IHn12
Assume IHn1 IHn2 .
Assume _ _ .
Assume _ .
Let q be given.
Assume Hq .
Apply Hq
Assume Hq1 Hq .
Apply Hq
Assume Hq2 Hq3 .
Assume Hq1a Hq1b Hq1c Hq1d .
Apply SNoLtLe_or (f' n q IHn1c Hq1c to the current goal.
We use q witness the existential quantifier.
Apply and4I to the current goal.
An exact proof term for the current goal is Hq1
An exact proof term for the current goal is Hq2
An exact proof term for the current goal is Hq3
An exact proof term for the current goal is H4
We prove the intermediate
claim L1ba :
SNo (- f' n .
An
exact proof term for the current goal is
SNo_minus_SNo (f' n IHn1c .
We prove the intermediate
claim L1bb :
SNo (x + - f' n .
An
exact proof term for the current goal is
SNo_add_SNo x (- f' n H1 L1ba .
Assume H5 .
Apply H5
Let k be given.
Assume H5 .
Apply H5
We use
(f' n + eps_ (ordsucc k to
witness the existential quantifier.
We prove the intermediate
claim Lk1 :
ordsucc k ∈ ω .
Assume _ _ .
Assume _ .
Apply and4I to the current goal.
An exact proof term for the current goal is Lk3
An exact proof term for the current goal is H6
An exact proof term for the current goal is H1
An exact proof term for the current goal is Lk1
We will
prove f' n + eps_ k ≤ x .
We will
prove f' n + eps_ k ≤ f' n + (- f' n + x .
rewrite the current goal using
add_SNo_com (- f' n x L1ba H1 (from left to right).
We will
prove f' n + eps_ k ≤ f' n + (x + - f' n .
An exact proof term for the current goal is H1
An exact proof term for the current goal is Hq3
We prove the intermediate
claim L1bd :
0 < x + - f' n .
We will
prove 0 + f' n < (x + - f' n + f' n .
rewrite the current goal using
add_SNo_0L (f' n IHn1c (from left to right).
rewrite the current goal using
add_SNo_minus_R2' x (f' n H1 IHn1c (from left to right).
An exact proof term for the current goal is IHn2
We prove the intermediate
claim L1be :
f' n = x .
Apply H2 (f' n IHn1
Let k be given.
Assume Hk .
rewrite the current goal using
abs_SNo_dist_swap (f' n x IHn1c H1 (from left to right).
rewrite the current goal using
pos_abs_SNo (x + - f' n L1bd (from left to right).
An exact proof term for the current goal is H6
Apply H5
We use k witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk
An exact proof term for the current goal is H6
rewrite the current goal using L1be
An exact proof term for the current goal is IHn2
rewrite the current goal using Lf'S n Hn
Apply L1c
Assume H H7 .
Apply H
Assume H H6 .
Apply H
Assume H4 H5 .
Apply and4I to the current goal.
An exact proof term for the current goal is H4
An exact proof term for the current goal is H5
An exact proof term for the current goal is H6
Let i be given.
Apply ordsuccE n i Hi to the current goal.
An exact proof term for the current goal is Hfi
An exact proof term for the current goal is IHn1c
Assume _ _ H9 _ .
An exact proof term for the current goal is H9
Apply IHn
Assume _ .
An exact proof term for the current goal is IHn4 i H8 Hfi
An exact proof term for the current goal is H7
rewrite the current goal using H8
rewrite the current goal using
beta ω f' n (nat_p_omega n Hn (from left to right).
An exact proof term for the current goal is H7
Let n be given.
Assume Hn .
We use f witness the existential quantifier.
Apply andI to the current goal.
Apply lam_Pi to the current goal.
Let n be given.
Assume Hn .
Apply L2 n Hn
Assume H _ .
Apply H
Assume H _ .
Apply H
Assume H _ .
An exact proof term for the current goal is H
Let n be given.
Assume Hn .
Apply L2 n Hn
Assume H H7 .
Apply H
Assume H H6 .
Apply H
Assume H4 H5 .
Apply and3I to the current goal.
An exact proof term for the current goal is H5
An exact proof term for the current goal is H6
Let i be given.
Apply H7 i Hi
We prove the intermediate
claim Li :
i ∈ ω .
rewrite the current goal using
beta ω f' i Li (from left to right).
We will
prove SNo (f' i .
Apply L2 i Li
Assume H _ .
Apply H
Assume H _ .
Apply H
Assume _ .
Assume _ _ H9 _ .
We will
prove SNo (f' i .
An exact proof term for the current goal is H9
∎
Proof: Let x be given.
Assume H1 H2 H3 .
We prove the intermediate
claim L1 :
SNo (- x .
Let f be given.
Assume Hf .
Apply Hf
We prove the intermediate
claim Lf :
∀ n ∈ ω , SNo (f n .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H
Set g to be the term
λn ∈ ω - f n .
We use g witness the existential quantifier.
Apply andI to the current goal.
Apply lam_Pi to the current goal.
Let n be given.
Assume Hn .
An
exact proof term for the current goal is
ap_Pi ω (λ_ ⇒ SNoS_ ω ) f n Hf1 Hn .
Let n be given.
Assume Hn .
We prove the intermediate
claim L1 :
- f n + - eps_ n < x ∧ x < - f n ∧ ∀ i ∈ n , - f n < g i .
Apply Hf2 n Hn
Assume H .
Apply H
Apply and3I to the current goal.
We will
prove - (f n + eps_ n < x .
An exact proof term for the current goal is Hf2b
An exact proof term for the current goal is Hf2a
Let i be given.
Assume Hi .
We prove the intermediate
claim Li :
i ∈ ω .
rewrite the current goal using
beta ω (λn ⇒ - f n ) i Li (from left to right).
We will
prove - f n < - f i .
An exact proof term for the current goal is Hf2c i Hi
We prove the intermediate
claim L2 :
g n = - f n .
An
exact proof term for the current goal is
beta ω (λn ⇒ - f n ) n Hn .
An
exact proof term for the current goal is
L2 (λu v ⇒ v + - eps_ n < x ∧ x < v ∧ ∀ i ∈ n , v < g i ) L1 .
∎
Proof: Let lambda be given.
Assume Hl1 Hl2 .
Let L be given.
Assume HL .
Let R be given.
Assume HR HLR .
We prove the intermediate
claim L1 :
∀ x ∈ L , SNoLev x ∈ lambda .
Let x be given.
Assume Hx .
Apply SNoS_E2 lambda Hl1 x (HL x Hx to the current goal.
Assume H _ _ _ .
An exact proof term for the current goal is H
We prove the intermediate
claim L2 :
∀ y ∈ R , SNoLev y ∈ lambda .
Let y be given.
Assume Hy .
Apply SNoS_E2 lambda Hl1 y (HR y Hy to the current goal.
Assume H _ _ _ .
An exact proof term for the current goal is H
Let x be given.
Assume Hx .
Apply SNoS_E2 lambda Hl1 x (HL x Hx to the current goal.
Assume _ H _ _ .
An exact proof term for the current goal is H
Let y be given.
Assume Hy .
Apply SNoS_E2 lambda Hl1 y (HR y Hy to the current goal.
Assume _ H _ _ .
An exact proof term for the current goal is H
An exact proof term for the current goal is Hl1
An exact proof term for the current goal is L4
Assume H1 .
An exact proof term for the current goal is H1
Let x be given.
Apply Hl2
An exact proof term for the current goal is L1 x Hx
Let y be given.
Apply Hl2
An exact proof term for the current goal is L2 y Hy
Assume _ _ _ .
An
exact proof term for the current goal is
L5 (SNoLev (SNoCut L R H2 .
∎
Proof: Let f be given.
Assume Hf1 .
Let g be given.
Assume Hg1 Hfg .
Let p be given.
Assume Hp .
Set L to be the term
{ f n | n ∈ ω } .
Set R to be the term
{ g n | n ∈ ω } .
Set x to be the term
SNoCut L R .
We prove the intermediate
claim Lf :
∀ n ∈ ω , SNo (f n .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H
We prove the intermediate
claim Lg :
∀ n ∈ ω , SNo (g n .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H
We prove the intermediate
claim L1 :
SNoCutP L R .
Apply and3I to the current goal.
Let w be given.
Let n be given.
Assume Hn .
rewrite the current goal using Hwn
An exact proof term for the current goal is Lf n Hn
Let z be given.
Let m be given.
Assume Hm .
rewrite the current goal using Hzm
An exact proof term for the current goal is Lg m Hm
Let w be given.
Let z be given.
Let n be given.
Assume Hn .
rewrite the current goal using Hwn
Let m be given.
Assume Hm .
rewrite the current goal using Hzm
An exact proof term for the current goal is Hfg n Hn m Hm
We prove the intermediate
claim L2 :
L ⊆ SNoS_ ω .
Let w be given.
Assume Hw .
Let n be given.
Assume Hn .
rewrite the current goal using Hwn
An
exact proof term for the current goal is
ap_Pi ω (λ_ ⇒ SNoS_ ω ) f n Hf1 Hn .
We prove the intermediate
claim L3 :
R ⊆ SNoS_ ω .
Let z be given.
Let m be given.
Assume Hm .
rewrite the current goal using Hzm
An
exact proof term for the current goal is
(ap_Pi ω (λ_ ⇒ SNoS_ ω ) g m Hg1 Hm .
An exact proof term for the current goal is L4
An exact proof term for the current goal is HLR1
Apply Hp L1 HLR1 L4 L5
Let n be given.
Assume Hn .
Apply HLR3
An
exact proof term for the current goal is
ReplI ω (λn ⇒ f n ) n Hn .
Let n be given.
Assume Hn .
Apply HLR4
An
exact proof term for the current goal is
ReplI ω (λn ⇒ g n ) n Hn .
∎
Proof: Let x be given.
Assume Hx .
Let f be given.
Assume Hf1 .
Let g be given.
Assume Hg1 Hf2 Hf3 Hf4 Hg3 Hg4 .
Set L to be the term
{ f n | n ∈ ω } .
Set R to be the term
{ g n | n ∈ ω } .
We prove the intermediate
claim Lmx :
SNo (- x .
We prove the intermediate
claim Lf :
∀ n ∈ ω , SNo (f n .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H
We prove the intermediate
claim Lg :
∀ n ∈ ω , SNo (g n .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H
We prove the intermediate
claim Lfg :
∀ n m ∈ ω , f n < g m .
Let n be given.
Assume Hn .
Let m be given.
Assume Hm .
Apply SNoLt_tra (f n x (g m (Lf n Hn Hx (Lg m Hm to the current goal.
An exact proof term for the current goal is Hf2 n Hn
An exact proof term for the current goal is Hg3 m Hm
rewrite the current goal using Hxfg
rewrite the current goal using Hxfg
rewrite the current goal using Hxfg
rewrite the current goal using Hxfg
rewrite the current goal using Hxfg
Assume _ _ _ _ .
An
exact proof term for the current goal is
SNoLev_ x Hx .
Apply real_I to the current goal.
An exact proof term for the current goal is H4
We prove the intermediate
claim Lbd1 :
x < g 0 .
Assume _ _ _ .
Assume _ _ .
Apply SNoLt_tra x (g 0 x Hx Hg0a Hx Lbd1 to the current goal.
rewrite the current goal using H9
An exact proof term for the current goal is Hg0b
We prove the intermediate
claim Lbd2 :
f 0 < x .
Assume _ _ .
Assume _ _ _ .
Apply SNoLt_tra x (f 0 x Hx Hf0a Hx to the current goal.
rewrite the current goal using H9
An exact proof term for the current goal is Hf0b
An exact proof term for the current goal is Lbd2
Let q be given.
Assume Hq1 Hq2 .
Assume Hq1a Hq1b Hq1c Hq1d .
We prove the intermediate
claim Lmq :
SNo (- q .
An
exact proof term for the current goal is
SNo_minus_SNo q Hq1c .
We prove the intermediate
claim Lxmq :
SNo (x + - q .
An
exact proof term for the current goal is
SNo_add_SNo x (- q Hx Lmq .
We prove the intermediate
claim Lqmx :
SNo (q + - x .
An
exact proof term for the current goal is
SNo_add_SNo q (- x Hq1c Lmx .
We prove the intermediate
claim L5 :
∀ w ∈ L , w < q .
Let w be given.
Assume Hw .
Let n be given.
Assume Hn .
rewrite the current goal using Hwn
Apply SNoLtLe_or (f n q (Lf n Hn Hq1c to the current goal.
An exact proof term for the current goal is H9
Assume _ _ _ _ _ .
Assume _ .
We prove the intermediate
claim L5a :
SNo (f (ordsucc n .
We prove the intermediate
claim L5b :
q < f (ordsucc n .
We prove the intermediate
claim L5c :
0 < f (ordsucc n + - q .
We prove the intermediate
claim L5d :
SNo (f (ordsucc n + - q .
We prove the intermediate
claim L5e :
f (ordsucc n < x .
We prove the intermediate
claim L5f :
q < x .
An
exact proof term for the current goal is
SNoLt_tra q (f (ordsucc n x Hq1c L5a Hx L5b L5e .
We prove the intermediate
claim L5g :
0 < x + - q .
An
exact proof term for the current goal is
SNoLt_minus_pos q x Hq1c Hx L5f .
We prove the intermediate
claim L5h :
abs_SNo (q + - x = x + - q .
An
exact proof term for the current goal is
pos_abs_SNo (x + - q L5g .
We prove the intermediate
claim L5i :
q = f (ordsucc n .
Apply Hfn2 q Hq1
Let k be given.
An exact proof term for the current goal is L5e
rewrite the current goal using L5h
An exact proof term for the current goal is Hq2 k Hk
rewrite the current goal using L5i
An exact proof term for the current goal is L5b
We prove the intermediate
claim L6 :
∀ z ∈ R , q < z .
Let z be given.
Let m be given.
Assume Hm .
rewrite the current goal using Hzm
Apply SNoLtLe_or q (g m Hq1c (Lg m Hm to the current goal.
An exact proof term for the current goal is H9
Assume _ _ _ _ _ .
Assume _ .
We prove the intermediate
claim L6a :
SNo (g (ordsucc m .
We prove the intermediate
claim L6b :
g (ordsucc m < q .
An exact proof term for the current goal is H9
We prove the intermediate
claim L6c :
0 < q + - g (ordsucc m .
We prove the intermediate
claim L6d :
SNo (q + - g (ordsucc m .
We prove the intermediate
claim L6e :
x < g (ordsucc m .
We prove the intermediate
claim L6f :
x < q .
An
exact proof term for the current goal is
SNoLt_tra x (g (ordsucc m q Hx L6a Hq1c L6e L6b .
We prove the intermediate
claim L6g :
0 < q + - x .
An
exact proof term for the current goal is
SNoLt_minus_pos x q Hx Hq1c L6f .
We prove the intermediate
claim L6h :
abs_SNo (q + - x = q + - x .
An
exact proof term for the current goal is
pos_abs_SNo (q + - x L6g .
We prove the intermediate
claim L6i :
q = g (ordsucc m .
Apply Hgm2 q Hq1
Let k be given.
An exact proof term for the current goal is L6e
rewrite the current goal using L6h
An exact proof term for the current goal is Hq2 k Hk
rewrite the current goal using L6i
An exact proof term for the current goal is L6b
Apply H7 q Hq1c L5 L6
rewrite the current goal using Hxfg
rewrite the current goal using H8
Apply H9
An exact proof term for the current goal is Hq1a
∎
Theorem. (
SNo_approx_real_rep ) The following is provable:
∀ x ∈ real , ∀p : prop , (∀ f g ∈ SNoS_ ω ω , (∀ n ∈ ω , f n < x → (∀ n ∈ ω , x < f n + eps_ n → (∀ n ∈ ω , ∀ i ∈ n , f i < f n → (∀ n ∈ ω , g n + - eps_ n < x → (∀ n ∈ ω , x < g n → (∀ n ∈ ω , ∀ i ∈ n , g n < g i → SNoCutP { f n | n ∈ ω } { g n | n ∈ ω } x = SNoCut { f n | n ∈ ω } { g n | n ∈ ω } p → p Proof: Let x be given.
Assume Hx .
Let p be given.
Assume Hp .
Apply real_E x Hx to the current goal.
Assume Hx1 Hx2 Hx3 _ _ Hx4 Hx5 .
Let f be given.
Assume Hf .
Apply Hf
Assume Hf1 Hf2 .
Let g be given.
Assume Hg .
Apply Hg
Assume Hg1 Hg2 .
We prove the intermediate
claim Lf :
∀ n ∈ ω , SNo (f n .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H
We prove the intermediate
claim Lg :
∀ n ∈ ω , SNo (g n .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H
We prove the intermediate
claim Lf1 :
∀ n ∈ ω , f n < x .
Let n be given.
Assume Hn .
Apply Hf2 n Hn
Assume H _ .
Apply H
Assume H _ .
An exact proof term for the current goal is H
We prove the intermediate
claim Lf2 :
∀ n ∈ ω , x < f n + eps_ n .
Let n be given.
Assume Hn .
Apply Hf2 n Hn
Assume H _ .
Apply H
Assume _ H .
An exact proof term for the current goal is H
We prove the intermediate
claim Lf3 :
∀ n ∈ ω , ∀ i ∈ n , f i < f n .
Let n be given.
Assume Hn .
Apply Hf2 n Hn
Assume _ H .
An exact proof term for the current goal is H
We prove the intermediate
claim Lg1 :
∀ n ∈ ω , g n + - eps_ n < x .
Let n be given.
Assume Hn .
Apply Hg2 n Hn
Assume H _ .
Apply H
Assume H _ .
An exact proof term for the current goal is H
We prove the intermediate
claim Lg2 :
∀ n ∈ ω , x < g n .
Let n be given.
Assume Hn .
Apply Hg2 n Hn
Assume H _ .
Apply H
Assume _ H .
An exact proof term for the current goal is H
We prove the intermediate
claim Lg3 :
∀ n ∈ ω , ∀ i ∈ n , g n < g i .
Let n be given.
Assume Hn .
Apply Hg2 n Hn
Assume _ H .
An exact proof term for the current goal is H
We prove the intermediate
claim Lfg :
∀ n m ∈ ω , f n < g m .
Let n be given.
Assume Hn .
Let m be given.
Assume Hm .
Apply SNoLt_tra (f n x (g m (Lf n Hn Hx1 (Lg m Hm to the current goal.
An exact proof term for the current goal is Lf1 n Hn
An exact proof term for the current goal is Lg2 m Hm
Set L to be the term
{ f n | n ∈ ω } .
Set R to be the term
{ g n | n ∈ ω } .
We prove the intermediate
claim Lxfg :
x = SNoCut L R .
rewrite the current goal using
SNo_eta x Hx1 (from left to right).
Let w be given.
Apply SNoL_E x Hx1 w Hw to the current goal.
We prove the intermediate
claim Lw1 :
w ∈ SNoS_ ω .
We prove the intermediate
claim Lw2 :
0 < x + - w .
An
exact proof term for the current goal is
SNoLt_minus_pos w x Hw1 Hx1 Hw3 .
We prove the intermediate
claim Lw3 :
∃ k ∈ ω , w + eps_ k ≤ x .
Apply dneg to the current goal.
We prove the intermediate
claim Lw3a :
w = x .
Apply Hx4 w Lw1
Let k be given.
rewrite the current goal using
pos_abs_SNo (x + - w Lw2 (from left to right).
An exact proof term for the current goal is H8
Apply H7
We use k witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk
rewrite the current goal using Lw3a
An exact proof term for the current goal is Hw3
Apply Lw3
Let k be given.
Assume Hk .
Apply Hk
Apply SNoLt_tra w (f k (SNoCut L R Hw1 (Lf k Hk1 H2 to the current goal.
We will
prove x < f k + eps_ k .
Apply Hf2 k Hk1
Assume H _ .
Apply H
Assume _ H .
An exact proof term for the current goal is H
An exact proof term for the current goal is H5 k Hk1
Let z be given.
Apply SNoR_E x Hx1 z Hz to the current goal.
We prove the intermediate
claim Lz1 :
z ∈ SNoS_ ω .
We prove the intermediate
claim Lz2 :
0 < z + - x .
An
exact proof term for the current goal is
SNoLt_minus_pos x z Hx1 Hz1 Hz3 .
We prove the intermediate
claim Lz3 :
∃ k ∈ ω , x + eps_ k ≤ z .
Apply dneg to the current goal.
We prove the intermediate
claim Lz3a :
z = x .
Apply Hx4 z Lz1
Let k be given.
rewrite the current goal using
pos_abs_SNo (z + - x Lz2 (from left to right).
An exact proof term for the current goal is H8
Apply H7
We use k witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk
rewrite the current goal using Lz3a
An exact proof term for the current goal is Hz3
Apply Lz3
Let k be given.
Assume Hk .
Apply Hk
Apply SNoLt_tra (SNoCut L R (g k z H2 (Lg k Hk1 Hz1 to the current goal.
An exact proof term for the current goal is H6 k Hk1
We will
prove g k < x + eps_ k .
An exact proof term for the current goal is Lg1 k Hk1
An exact proof term for the current goal is Hk2
Let w be given.
rewrite the current goal using
SNo_eta x Hx1 (from right to left).
Let n be given.
Assume Hn .
rewrite the current goal using Hwn
An exact proof term for the current goal is Lf1 n Hn
Let z be given.
rewrite the current goal using
SNo_eta x Hx1 (from right to left).
Let m be given.
Assume Hm .
rewrite the current goal using Hzm
An exact proof term for the current goal is Lg2 m Hm
An exact proof term for the current goal is Hp f Hf1 g Hg1 Lf1 Lf2 Lf3 Lg1 Lg2 Lg3 H1 Lxfg
∎
Proof: Let x be given.
Assume Hx .
Let y be given.
Assume Hy .
Let fL be given.
Assume HfL .
Let fR be given.
Assume HfR HfL1 HfL2 HfL3 HfR1 HfR2 HfR3 HfLR HxfLR .
Let gL be given.
Assume HgL .
Let gR be given.
Assume HgR HgL1 HgL2 HgL3 HgR1 HgR2 HgR3 HgLR HygLR .
Set L to be the term
{ hL n | n ∈ ω } .
Set R to be the term
{ hR n | n ∈ ω } .
We prove the intermediate
claim Lx :
SNo x .
An
exact proof term for the current goal is
real_SNo x Hx .
We prove the intermediate
claim Ly :
SNo y .
An
exact proof term for the current goal is
real_SNo y Hy .
We prove the intermediate
claim Lxy :
SNo (x + y .
An
exact proof term for the current goal is
SNo_add_SNo x y Lx Ly .
Let n be given.
Assume Hn .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H
Let n be given.
Assume Hn .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H
Let n be given.
Assume Hn .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H
Let n be given.
Assume Hn .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H
Let n be given.
Assume Hn .
Let n be given.
Assume Hn .
We prove the intermediate
claim LhLb :
∀ n ∈ ω , SNo (hL n .
Let n be given.
Assume Hn .
rewrite the current goal using LhL n Hn
We prove the intermediate
claim LhRb :
∀ n ∈ ω , SNo (hR n .
Let n be given.
Assume Hn .
rewrite the current goal using LhR n Hn
We prove the intermediate
claim L1 :
hL ∈ SNoS_ ω ω .
Apply lam_Pi to the current goal.
Let n be given.
Assume Hn .
An exact proof term for the current goal is LfLa n Hn
An exact proof term for the current goal is LgLa n Hn
We prove the intermediate
claim L2 :
hR ∈ SNoS_ ω ω .
Apply lam_Pi to the current goal.
Let n be given.
Assume Hn .
An exact proof term for the current goal is LfRa n Hn
An exact proof term for the current goal is LgRa n Hn
We prove the intermediate
claim L3 :
∀ n ∈ ω , hL n < x + y .
Let n be given.
Assume Hn .
rewrite the current goal using LhL n Hn
We prove the intermediate
claim L4 :
∀ n ∈ ω , x + y < hL n + eps_ n .
Let n be given.
Assume Hn .
rewrite the current goal using LhL n Hn
We prove the intermediate
claim L5 :
∀ n ∈ ω , ∀ i ∈ n , hL i < hL n .
Let n be given.
Assume Hn .
Let i be given.
Assume Hi .
rewrite the current goal using LhL n Hn
We prove the intermediate
claim Li :
i ∈ ω .
rewrite the current goal using LhL i Li
We prove the intermediate
claim L6 :
∀ n ∈ ω , hR n + - eps_ n < x + y .
Let n be given.
Assume Hn .
rewrite the current goal using LhR n Hn
We prove the intermediate
claim L7 :
∀ n ∈ ω , x + y < hR n .
Let n be given.
Assume Hn .
rewrite the current goal using LhR n Hn
We prove the intermediate
claim L8 :
∀ n ∈ ω , ∀ i ∈ n , hR n < hR i .
Let n be given.
Assume Hn .
Let i be given.
Assume Hi .
rewrite the current goal using LhR n Hn
We prove the intermediate
claim Li :
i ∈ ω .
rewrite the current goal using LhR i Li
We prove the intermediate
claim LLR :
SNoCutP L R .
Apply and3I to the current goal.
Let w be given.
Assume Hw .
Let n be given.
rewrite the current goal using Hwn
We will
prove SNo (hL n .
An exact proof term for the current goal is LhLb n Hn
Let z be given.
Assume Hz .
Let m be given.
rewrite the current goal using Hzm
We will
prove SNo (hR m .
An exact proof term for the current goal is LhRb m Hm
Let w be given.
Assume Hw .
Let z be given.
Assume Hz .
Let n be given.
rewrite the current goal using Hwn
Let m be given.
rewrite the current goal using Hzm
We will
prove hL n < hR m .
Apply SNoLt_tra (hL n (x + y (hR m (LhLb n Hn (SNo_add_SNo x y Lx Ly (LhRb m Hm to the current goal.
We will
prove hL n < x + y .
An exact proof term for the current goal is L3 n Hn
We will
prove x + y < hR m .
An exact proof term for the current goal is L7 m Hm
Assume HLR1 HLR2 HLR3 HLR4 HLR5 .
We prove the intermediate
claim L9 :
x + y = SNoCut L R .
rewrite the current goal using
add_SNo_eq x Lx y Ly (from left to right).
Let w be given.
Assume Hw .
Let w' be given.
Assume Hww' .
rewrite the current goal using Hww'
Apply SNoL_E x Lx w' Hw' to the current goal.
Assume Hw'1 Hw'2 Hw'3 .
We prove the intermediate
claim Lw'1 :
w' ∈ SNoS_ ω .
We prove the intermediate
claim Lw'2 :
∃ n ∈ ω , w' + y ≤ hL n .
Apply dneg to the current goal.
We prove the intermediate
claim Lw'2a :
0 < x + - w' .
We prove the intermediate
claim Lw'2b :
w' = x .
Apply Lx2 w' Lw'1
Let k be given.
Assume Hk .
rewrite the current goal using
pos_abs_SNo (x + - w' Lw'2a (from left to right).
We will
prove x < eps_ k + w' .
Assume H2 .
An exact proof term for the current goal is H2
Apply HC
We use k witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk
We will
prove w' + y ≤ hL k .
We will
prove w' + y < hL k .
We will
prove (w' + y + eps_ k ≤ x + y .
We will
prove (w' + eps_ k + y ≤ x + y .
We will
prove w' + eps_ k ≤ x .
We will
prove eps_ k + w' ≤ x .
An exact proof term for the current goal is H2
We will
prove x + y < hL k + eps_ k .
An exact proof term for the current goal is L4 k Hk
rewrite the current goal using Lw'2b
An exact proof term for the current goal is Hw'3
Apply Lw'2
Let n be given.
Assume Hn .
Apply Hn
Assume Hn1 Hn2 .
We will
prove w' + y ≤ hL n .
An exact proof term for the current goal is Hn2
Apply HLR3
Apply ReplI to the current goal.
An exact proof term for the current goal is Hn1
Let w' be given.
Assume Hww' .
rewrite the current goal using Hww'
Apply SNoL_E y Ly w' Hw' to the current goal.
Assume Hw'1 Hw'2 Hw'3 .
We prove the intermediate
claim Lw'1 :
w' ∈ SNoS_ ω .
We prove the intermediate
claim Lw'2 :
∃ n ∈ ω , x + w' ≤ hL n .
Apply dneg to the current goal.
We prove the intermediate
claim Lw'2a :
0 < y + - w' .
We prove the intermediate
claim Lw'2b :
w' = y .
Apply Ly2 w' Lw'1
Let k be given.
Assume Hk .
rewrite the current goal using
pos_abs_SNo (y + - w' Lw'2a (from left to right).
We will
prove y < eps_ k + w' .
Assume H2 .
An exact proof term for the current goal is H2
Apply HC
We use k witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk
We will
prove x + w' ≤ hL k .
We will
prove x + w' < hL k .
We will
prove (x + w' + eps_ k ≤ x + y .
We will
prove x + (w' + eps_ k ≤ x + y .
We will
prove w' + eps_ k ≤ y .
We will
prove eps_ k + w' ≤ y .
An exact proof term for the current goal is H2
We will
prove x + y < hL k + eps_ k .
An exact proof term for the current goal is L4 k Hk
rewrite the current goal using Lw'2b
An exact proof term for the current goal is Hw'3
Apply Lw'2
Let n be given.
Assume Hn .
Apply Hn
Assume Hn1 Hn2 .
We will
prove x + w' ≤ hL n .
An exact proof term for the current goal is Hn2
Apply HLR3
Apply ReplI to the current goal.
An exact proof term for the current goal is Hn1
Let z be given.
Assume Hz .
Let z' be given.
Assume Hzz' .
rewrite the current goal using Hzz'
Apply SNoR_E x Lx z' Hz' to the current goal.
Assume Hz'1 Hz'2 Hz'3 .
We prove the intermediate
claim Lz'1 :
z' ∈ SNoS_ ω .
We prove the intermediate
claim Lz'2 :
∃ n ∈ ω , hR n ≤ z' + y .
Apply dneg to the current goal.
We prove the intermediate
claim Lz'2a :
0 < z' + - x .
We prove the intermediate
claim Lz'2b :
z' = x .
Apply Lx2 z' Lz'1
Let k be given.
Assume Hk .
rewrite the current goal using
pos_abs_SNo (z' + - x Lz'2a (from left to right).
We will
prove z' < eps_ k + x .
Assume H2 .
An exact proof term for the current goal is H2
Apply HC
We use k witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk
We will
prove hR k ≤ z' + y .
An exact proof term for the current goal is L6 k Hk
We will
prove (x + y + eps_ k ≤ z' + y .
We will
prove (x + eps_ k + y ≤ z' + y .
We will
prove x + eps_ k ≤ z' .
An exact proof term for the current goal is H2
rewrite the current goal using Lz'2b
An exact proof term for the current goal is Hz'3
Apply Lz'2
Let n be given.
Assume Hn .
Apply Hn
Assume Hn1 Hn2 .
Apply HLR4
Apply ReplI to the current goal.
An exact proof term for the current goal is Hn1
We will
prove hR n ≤ z' + y .
An exact proof term for the current goal is Hn2
Let z' be given.
Assume Hzz' .
rewrite the current goal using Hzz'
Apply SNoR_E y Ly z' Hz' to the current goal.
Assume Hz'1 Hz'2 Hz'3 .
We prove the intermediate
claim Lz'1 :
z' ∈ SNoS_ ω .
We prove the intermediate
claim Lz'2 :
∃ n ∈ ω , hR n ≤ x + z' .
Apply dneg to the current goal.
We prove the intermediate
claim Lz'2a :
0 < z' + - y .
We prove the intermediate
claim Lz'2b :
z' = y .
Apply Ly2 z' Lz'1
Let k be given.
Assume Hk .
rewrite the current goal using
pos_abs_SNo (z' + - y Lz'2a (from left to right).
We will
prove z' < eps_ k + y .
Assume H2 .
An exact proof term for the current goal is H2
Apply HC
We use k witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk
We will
prove hR k ≤ x + z' .
An exact proof term for the current goal is L6 k Hk
We will
prove (x + y + eps_ k ≤ x + z' .
We will
prove x + (y + eps_ k ≤ x + z' .
We will
prove y + eps_ k ≤ z' .
An exact proof term for the current goal is H2
rewrite the current goal using Lz'2b
An exact proof term for the current goal is Hz'3
Apply Lz'2
Let n be given.
Assume Hn .
Apply Hn
Assume Hn1 Hn2 .
Apply HLR4
Apply ReplI to the current goal.
An exact proof term for the current goal is Hn1
We will
prove hR n ≤ x + z' .
An exact proof term for the current goal is Hn2
Let w be given.
rewrite the current goal using
add_SNo_eq x Lx y Ly (from right to left).
Let n be given.
rewrite the current goal using Hwn
We will
prove hL n < x + y .
An exact proof term for the current goal is L3 n Hn
Let z be given.
rewrite the current goal using
add_SNo_eq x Lx y Ly (from right to left).
Let n be given.
rewrite the current goal using Hzn
We will
prove x + y < hR n .
An exact proof term for the current goal is L7 n Hn
∎
Proof: Let x be given.
Assume Hx1 Hx2 Hx3 .
Assume Hx1a Hx1b Hx1c Hx1d .
Let N be given.
Assume HN .
Apply HN
We prove the intermediate
claim LN :
SNo N .
An
exact proof term for the current goal is
omega_SNo N HN1 .
We use N witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN1
An exact proof term for the current goal is HN2
An exact proof term for the current goal is H1
We prove the intermediate
claim L2N :
SNo (2 ^ N .
We prove the intermediate
claim L1 :
2 ^ N ≤ 2 ^ N * eps_ N * N .
rewrite the current goal using
mul_SNo_oneR (2 ^ N L2N (from right to left) at position 1.
An
exact proof term for the current goal is
SNo_1 .
An exact proof term for the current goal is H1
We will
prove 2 ^ N < 2 ^ N .
rewrite the current goal using
mul_SNo_oneL N LN (from right to left) at position 2.
We will
prove 2 ^ N ≤ 1 * N .
An exact proof term for the current goal is L1
∎
Proof: Let x be given.
Assume Hx .
Let y be given.
Assume Hy Hx0 Hy0 .
Apply dneg to the current goal.
Apply real_E x Hx to the current goal.
Assume Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 .
Apply real_E y Hy to the current goal.
Assume Hy1 Hy2 Hy3 Hy4 Hy5 Hy6 Hy7 .
We prove the intermediate
claim Lx7 :
∀ k ∈ ω , ∀p : prop , (∀ q ∈ SNoS_ ω , 0 < q q < x x < q + eps_ k p → p .
We prove the intermediate
claim Ly7 :
∀ k ∈ ω , ∀p : prop , (∀ q ∈ SNoS_ ω , 0 < q q < y y < q + eps_ k p → p .
We prove the intermediate
claim Lxy :
SNo (x * y .
An
exact proof term for the current goal is
SNo_mul_SNo x y Hx1 Hy1 .
We prove the intermediate
claim Lmxy :
SNo (- x * y .
An
exact proof term for the current goal is
SNo_minus_SNo (x * y Lxy .
We prove the intermediate
claim Lxy2 :
SNoLev (x * y ∉ ω .
Apply HC
An exact proof term for the current goal is Lxy
Let q be given.
Assume Hq1 Hq2 .
Assume H1 .
An exact proof term for the current goal is H1
Apply Lxy2
rewrite the current goal using H1
An exact proof term for the current goal is Hq2
Apply Lxy2
Let v be given.
Assume Hv .
Apply SNoL_E x Hx1 v Hv to the current goal.
Assume Hv3 .
rewrite the current goal using H1
An exact proof term for the current goal is Hv2
An exact proof term for the current goal is Hv1
Let v be given.
Assume Hv .
Apply SNoR_E x Hx1 v Hv to the current goal.
Assume Hv3 .
rewrite the current goal using H1
An exact proof term for the current goal is Hv2
An exact proof term for the current goal is Hv1
Let v be given.
Assume Hv .
Apply SNoL_E y Hy1 v Hv to the current goal.
Assume Hv3 .
rewrite the current goal using H1
An exact proof term for the current goal is Hv2
An exact proof term for the current goal is Hv1
Let v be given.
Assume Hv .
Apply SNoR_E y Hy1 v Hv to the current goal.
Assume Hv3 .
rewrite the current goal using H1
An exact proof term for the current goal is Hv2
An exact proof term for the current goal is Hv1
We prove the intermediate
claim LLx2 :
∀ v ∈ SNoL x , ∀p : prop , (∀k, k ∈ ω eps_ k ≤ x + - v p ) → p .
Let v be given.
Assume Hv .
Let p be given.
Assume Hp .
Apply SNoL_E x Hx1 v Hv to the current goal.
Assume H1 .
rewrite the current goal using Hx6 v (LLx v Hv H1
An exact proof term for the current goal is Hv3
Apply dneg to the current goal.
Apply H1
Let k be given.
An exact proof term for the current goal is H3
Apply H2
Apply Hp k Hk
An exact proof term for the current goal is H3
We prove the intermediate
claim LRx2 :
∀ v ∈ SNoR x , ∀p : prop , (∀k, k ∈ ω eps_ k ≤ v + - x p ) → p .
Let v be given.
Assume Hv .
Let p be given.
Assume Hp .
Apply SNoR_E x Hx1 v Hv to the current goal.
Assume H1 .
rewrite the current goal using Hx6 v (LRx v Hv H1
An exact proof term for the current goal is Hv3
Apply dneg to the current goal.
Apply H1
Let k be given.
An exact proof term for the current goal is H3
Apply H2
Apply Hp k Hk
An exact proof term for the current goal is H3
We prove the intermediate
claim LLy2 :
∀ v ∈ SNoL y , ∀p : prop , (∀k, k ∈ ω eps_ k ≤ y + - v p ) → p .
Let v be given.
Assume Hv .
Let p be given.
Assume Hp .
Apply SNoL_E y Hy1 v Hv to the current goal.
Assume H1 .
rewrite the current goal using Hy6 v (LLy v Hv H1
An exact proof term for the current goal is Hv3
Apply dneg to the current goal.
Apply H1
Let k be given.
An exact proof term for the current goal is H3
Apply H2
Apply Hp k Hk
An exact proof term for the current goal is H3
We prove the intermediate
claim LRy2 :
∀ v ∈ SNoR y , ∀p : prop , (∀k, k ∈ ω eps_ k ≤ v + - y p ) → p .
Let v be given.
Assume Hv .
Let p be given.
Assume Hp .
Apply SNoR_E y Hy1 v Hv to the current goal.
Assume H1 .
rewrite the current goal using Hy6 v (LRy v Hv H1
An exact proof term for the current goal is Hv3
Apply dneg to the current goal.
Apply H1
Let k be given.
An exact proof term for the current goal is H3
Apply H2
Apply Hp k Hk
An exact proof term for the current goal is H3
Let L and R be given.
Let q be given.
Assume Hq1 Hq2 .
Assume Hq1a Hq1b Hq1c Hq1d .
We prove the intermediate
claim Lq1 :
q ∈ SNoL (x * y .
Apply SNoL_I to the current goal.
An exact proof term for the current goal is Lxy
An exact proof term for the current goal is Hq1c
An exact proof term for the current goal is Lxy3 q Hq1c Hq1a
An exact proof term for the current goal is H1
Let v be given.
Let w be given.
Apply SNoL_E x Hx1 v Hv to the current goal.
Assume Hv1 _ _ .
Apply SNoL_E y Hy1 w Hw to the current goal.
Assume Hw1 _ _ .
We prove the intermediate
claim Lvw :
SNo (v * w .
An
exact proof term for the current goal is
SNo_mul_SNo v w Hv1 Hw1 .
We prove the intermediate
claim Lxw :
SNo (x * w .
An
exact proof term for the current goal is
SNo_mul_SNo x w ?? Hw1 .
We prove the intermediate
claim Lmxw :
SNo (- x * w .
An
exact proof term for the current goal is
SNo_minus_SNo (x * w Lxw .
We prove the intermediate
claim Lvy :
SNo (v * y .
An
exact proof term for the current goal is
SNo_mul_SNo v y Hv1 ?? .
We prove the intermediate
claim Lmvy :
SNo (- v * y .
An
exact proof term for the current goal is
SNo_minus_SNo (v * y Lvy .
We prove the intermediate
claim Lxmv :
SNo (x + - v .
We prove the intermediate
claim Lymw :
SNo (y + - w .
Apply LLx2 v Hv
Let k be given.
Apply LLy2 w Hw
Let k' be given.
We prove the intermediate
claim Lek :
SNo (eps_ k .
An
exact proof term for the current goal is
SNo_eps_ k Hk1 .
We prove the intermediate
claim Lek' :
SNo (eps_ k' .
An
exact proof term for the current goal is
SNo_eps_ k' Hk'1 .
We prove the intermediate
claim Lkk' :
k + k' ∈ ω .
We prove the intermediate
claim Lekk' :
SNo (eps_ (k + k' .
An
exact proof term for the current goal is
SNo_eps_ (k + k' Lkk' .
We prove the intermediate
claim Lekek' :
SNo (eps_ k * eps_ k' .
An
exact proof term for the current goal is
Hq2 (k + k' (add_SNo_In_omega k Hk1 k' Hk'1 .
We will
prove eps_ (k + k' + q ≤ x * y .
An
exact proof term for the current goal is
SNo_eps_pos k Hk1 .
An
exact proof term for the current goal is
SNo_eps_pos k' Hk'1 .
An exact proof term for the current goal is Hk2
An exact proof term for the current goal is Hk'2
We will
prove (x + - v * (y + - w + q ≤ x * y .
rewrite the current goal using
SNo_foil_mm x v y w Hx1 Hv1 Hy1 Hw1 (from left to right).
We will
prove (x * y + - x * w + - v * y + v * w + q ≤ x * y .
rewrite the current goal using
add_SNo_assoc_4 (x * y (- x * w (- v * y (v * w ?? ?? ?? ?? (from left to right).
We will
prove ((x * y + - x * w + - v * y + v * w + q ≤ x * y .
We will
prove (x * y + - x * w + - v * y + (v * w + q ≤ x * y .
rewrite the current goal using
add_SNo_com (v * w q ?? Hq1c (from left to right).
We will
prove (x * y + - x * w + - v * y + (q + v * w ≤ x * y .
We will
prove (x * y + - x * w + - v * y + (v * y + x * w ≤ x * y .
We will
prove x * y + - x * w + x * w ≤ x * y .
We will
prove x * y + 0 ≤ x * y .
rewrite the current goal using
add_SNo_0R (x * y ?? (from left to right).
We will
prove x * y ≤ x * y .
Let v be given.
Let w be given.
Apply SNoR_E x Hx1 v Hv to the current goal.
Assume Hv1 _ _ .
Apply SNoR_E y Hy1 w Hw to the current goal.
Assume Hw1 _ _ .
We prove the intermediate
claim Lvw :
SNo (v * w .
An
exact proof term for the current goal is
SNo_mul_SNo v w Hv1 Hw1 .
We prove the intermediate
claim Lxw :
SNo (x * w .
An
exact proof term for the current goal is
SNo_mul_SNo x w ?? Hw1 .
We prove the intermediate
claim Lmxw :
SNo (- x * w .
An
exact proof term for the current goal is
SNo_minus_SNo (x * w Lxw .
We prove the intermediate
claim Lvy :
SNo (v * y .
An
exact proof term for the current goal is
SNo_mul_SNo v y Hv1 ?? .
We prove the intermediate
claim Lmvy :
SNo (- v * y .
An
exact proof term for the current goal is
SNo_minus_SNo (v * y Lvy .
We prove the intermediate
claim Lvmx :
SNo (v + - x .
We prove the intermediate
claim Lwmy :
SNo (w + - y .
Apply LRx2 v Hv
Let k be given.
Apply LRy2 w Hw
Let k' be given.
We prove the intermediate
claim Lek :
SNo (eps_ k .
An
exact proof term for the current goal is
SNo_eps_ k Hk1 .
We prove the intermediate
claim Lek' :
SNo (eps_ k' .
An
exact proof term for the current goal is
SNo_eps_ k' Hk'1 .
We prove the intermediate
claim Lkk' :
k + k' ∈ ω .
We prove the intermediate
claim Lekk' :
SNo (eps_ (k + k' .
An
exact proof term for the current goal is
SNo_eps_ (k + k' Lkk' .
We prove the intermediate
claim Lekek' :
SNo (eps_ k * eps_ k' .
An
exact proof term for the current goal is
Hq2 (k + k' (add_SNo_In_omega k Hk1 k' Hk'1 .
We will
prove eps_ (k + k' + q ≤ x * y .
An
exact proof term for the current goal is
SNo_eps_pos k Hk1 .
An
exact proof term for the current goal is
SNo_eps_pos k' Hk'1 .
An exact proof term for the current goal is Hk2
An exact proof term for the current goal is Hk'2
We will
prove (v + - x * (w + - y + q ≤ x * y .
rewrite the current goal using
SNo_foil_mm v x w y Hv1 Hx1 Hw1 Hy1 (from left to right).
We will
prove (v * w + - v * y + - x * w + x * y + q ≤ x * y .
rewrite the current goal using
add_SNo_assoc_4 (v * w (- v * y (- x * w (x * y ?? ?? ?? ?? (from left to right).
We will
prove ((v * w + - v * y + - x * w + x * y + q ≤ x * y .
We will
prove (v * w + - v * y + - x * w + (x * y + q ≤ x * y .
rewrite the current goal using
add_SNo_com (x * y q ?? Hq1c (from left to right).
We will
prove (v * w + - v * y + - x * w + (q + x * y ≤ x * y .
rewrite the current goal using
add_SNo_3a_2b (v * w (- v * y (- x * w q (x * y ?? ?? ?? ?? ?? (from left to right).
We will
prove (x * y + - v * y + - x * w + (q + v * w ≤ x * y .
We will
prove q + v * w ≤ v * y + x * w .
An exact proof term for the current goal is H2
We will
prove (x * y + - v * y + - x * w + (v * y + x * w ≤ x * y .
rewrite the current goal using
add_SNo_com (v * y (x * w ?? ?? (from left to right).
We will
prove (x * y + - v * y + - x * w + (x * w + v * y ≤ x * y .
We will
prove x * y + - v * y + v * y ≤ x * y .
We will
prove x * y + 0 ≤ x * y .
rewrite the current goal using
add_SNo_0R (x * y ?? (from left to right).
An exact proof term for the current goal is H1
We prove the intermediate
claim Lq2 :
q ∈ SNoR (x * y .
Apply SNoR_I to the current goal.
An exact proof term for the current goal is Lxy
An exact proof term for the current goal is Hq1c
An exact proof term for the current goal is Lxy3 q Hq1c Hq1a
An exact proof term for the current goal is H1
Let v be given.
Let w be given.
Apply SNoL_E x Hx1 v Hv to the current goal.
Assume Hv1 _ _ .
Apply SNoR_E y Hy1 w Hw to the current goal.
Assume Hw1 _ _ .
We prove the intermediate
claim Lvy :
SNo (v * y .
An
exact proof term for the current goal is
SNo_mul_SNo v y Hv1 Hy1 .
We prove the intermediate
claim Lxw :
SNo (x * w .
An
exact proof term for the current goal is
SNo_mul_SNo x w ?? Hw1 .
We prove the intermediate
claim Lmxw :
SNo (- x * w .
An
exact proof term for the current goal is
SNo_minus_SNo (x * w Lxw .
We prove the intermediate
claim Lvw :
SNo (v * w .
An
exact proof term for the current goal is
SNo_mul_SNo v w Hv1 ?? .
We prove the intermediate
claim Lmvw :
SNo (- v * w .
An
exact proof term for the current goal is
SNo_minus_SNo (v * w Lvw .
We prove the intermediate
claim Lxmv :
SNo (x + - v .
We prove the intermediate
claim Lwmy :
SNo (w + - y .
Apply LLx2 v Hv
Let k be given.
Apply LRy2 w Hw
Let k' be given.
We prove the intermediate
claim Lek :
SNo (eps_ k .
An
exact proof term for the current goal is
SNo_eps_ k Hk1 .
We prove the intermediate
claim Lek' :
SNo (eps_ k' .
An
exact proof term for the current goal is
SNo_eps_ k' Hk'1 .
We prove the intermediate
claim Lkk' :
k + k' ∈ ω .
We prove the intermediate
claim Lekk' :
SNo (eps_ (k + k' .
An
exact proof term for the current goal is
SNo_eps_ (k + k' Lkk' .
We prove the intermediate
claim Lekek' :
SNo (eps_ k * eps_ k' .
An
exact proof term for the current goal is
Hq2 (k + k' (add_SNo_In_omega k Hk1 k' Hk'1 .
We will
prove eps_ (k + k' + x * y ≤ q .
An
exact proof term for the current goal is
SNo_eps_pos k Hk1 .
An
exact proof term for the current goal is
SNo_eps_pos k' Hk'1 .
An exact proof term for the current goal is Hk2
An exact proof term for the current goal is Hk'2
We will
prove (x + - v * (w + - y + x * y ≤ q .
rewrite the current goal using
SNo_foil_mm x v w y Hx1 Hv1 Hw1 Hy1 (from left to right).
We will
prove (x * w + - x * y + - v * w + v * y + x * y ≤ q .
We will
prove (- x * y + - v * w + v * y + x * w + x * y ≤ q .
We will
prove - v * w + v * y + x * w ≤ q .
We will
prove - v * w + v * y + x * w ≤ - v * w + q + v * w .
We will
prove - v * w + q + v * w ≤ q .
rewrite the current goal using
add_SNo_com q (v * w ?? ?? (from left to right).
rewrite the current goal using
add_SNo_minus_L2 (v * w q ?? ?? (from left to right).
Let v be given.
Let w be given.
Apply SNoR_E x Hx1 v Hv to the current goal.
Assume Hv1 _ _ .
Apply SNoL_E y Hy1 w Hw to the current goal.
Assume Hw1 _ _ .
We prove the intermediate
claim Lvy :
SNo (v * y .
An
exact proof term for the current goal is
SNo_mul_SNo v y Hv1 Hy1 .
We prove the intermediate
claim Lxw :
SNo (x * w .
An
exact proof term for the current goal is
SNo_mul_SNo x w ?? Hw1 .
We prove the intermediate
claim Lvw :
SNo (v * w .
An
exact proof term for the current goal is
SNo_mul_SNo v w Hv1 ?? .
We prove the intermediate
claim Lmvw :
SNo (- v * w .
An
exact proof term for the current goal is
SNo_minus_SNo (v * w Lvw .
We prove the intermediate
claim Lvmx :
SNo (v + - x .
We prove the intermediate
claim Lymw :
SNo (y + - w .
Apply LRx2 v Hv
Let k be given.
Apply LLy2 w Hw
Let k' be given.
We prove the intermediate
claim Lek :
SNo (eps_ k .
An
exact proof term for the current goal is
SNo_eps_ k Hk1 .
We prove the intermediate
claim Lek' :
SNo (eps_ k' .
An
exact proof term for the current goal is
SNo_eps_ k' Hk'1 .
We prove the intermediate
claim Lkk' :
k + k' ∈ ω .
We prove the intermediate
claim Lekk' :
SNo (eps_ (k + k' .
An
exact proof term for the current goal is
SNo_eps_ (k + k' Lkk' .
We prove the intermediate
claim Lekek' :
SNo (eps_ k * eps_ k' .
An
exact proof term for the current goal is
Hq2 (k + k' (add_SNo_In_omega k Hk1 k' Hk'1 .
We will
prove eps_ (k + k' + x * y ≤ q .
An
exact proof term for the current goal is
SNo_eps_pos k Hk1 .
An
exact proof term for the current goal is
SNo_eps_pos k' Hk'1 .
An exact proof term for the current goal is Hk2
An exact proof term for the current goal is Hk'2
We will
prove (v + - x * (y + - w + x * y ≤ q .
rewrite the current goal using
SNo_foil_mm v x y w Hv1 Hx1 Hy1 Hw1 (from left to right).
We will
prove (v * y + - v * w + - x * y + x * w + x * y ≤ q .
We will
prove (- x * y + x * w + v * y + - v * w + x * y ≤ q .
We will
prove x * y + - x * y + x * w + v * y + - v * w ≤ q .
We will
prove x * w + v * y + - v * w ≤ q .
We will
prove - v * w + x * w + v * y ≤ q .
We will
prove - v * w + x * w + v * y ≤ - v * w + q + v * w .
We will
prove x * w + v * y ≤ q + v * w .
rewrite the current goal using
add_SNo_com (x * w (v * y ?? ?? (from left to right).
An exact proof term for the current goal is H2
We will
prove - v * w + q + v * w ≤ q .
rewrite the current goal using
add_SNo_com q (v * w ?? ?? (from left to right).
We will
prove - v * w + v * w + q ≤ q .
rewrite the current goal using
add_SNo_minus_L2 (v * w q ?? ?? (from left to right).
Let N be given.
Assume HN .
Apply HN
Let N' be given.
Assume HN' .
Apply HN'
We use N' witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN'1
Apply andI to the current goal.
An
exact proof term for the current goal is
SNo_eps_decr N' HN'1 N H1 .
An exact proof term for the current goal is HN2
An exact proof term for the current goal is HN'2
We use N witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN1
Apply andI to the current goal.
An exact proof term for the current goal is HN2
rewrite the current goal using H1
An exact proof term for the current goal is HN'2
We use N witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN1
Apply andI to the current goal.
An exact proof term for the current goal is HN2
An
exact proof term for the current goal is
SNo_eps_decr N HN1 N' H1 .
An exact proof term for the current goal is HN'2
Apply LNex
Let N be given.
Assume HN .
Apply HN
Assume HN .
Apply HN
Let k be given.
Assume Hk .
We prove the intermediate
claim Lek :
SNo (eps_ k .
An
exact proof term for the current goal is
SNo_eps_ k Hk .
We prove the intermediate
claim Lk1 :
k + 1 ∈ ω .
We prove the intermediate
claim Lk2 :
k + 2 ∈ ω .
Set k' to be the term
N + k + 2 .
We prove the intermediate
claim Lk' :
k' ∈ ω .
We prove the intermediate
claim Lek' :
SNo (eps_ k' .
An
exact proof term for the current goal is
SNo_eps_ k' Lk' .
Apply Lx7 k' Lk'
Let q be given.
Assume Hq1a Hq1b Hq1c Hq1d .
Apply Ly7 k' Lk'
Let q' be given.
Assume Hq'1a Hq'1b Hq'1c Hq'1d .
We prove the intermediate
claim Lqq' :
SNo (q * q' .
An
exact proof term for the current goal is
SNo_mul_SNo q q' Hq1c Hq'1c .
We use
(q * q' to
witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
We will
prove q * q' < x * y .
An
exact proof term for the current goal is
pos_mul_SNo_Lt2 q q' x y Hq1c Hq'1c Hx1 Hy1 Hqpos Hq'pos Hq2 Hq'2 .
rewrite the current goal using
SNo_foil q (eps_ k' q' (eps_ k' Hq1c Lek' Hq'1c Lek' (from left to right).
rewrite the current goal using
add_SNo_1_1_2 (from left to right).
We prove the intermediate
claim LeN :
SNo (eps_ N .
An
exact proof term for the current goal is
SNo_eps_ N HN1 .
We prove the intermediate
claim Lek1 :
SNo (eps_ (k + 1 .
An
exact proof term for the current goal is
SNo_eps_ (k + 1 Lk1 .
We prove the intermediate
claim Lek2 :
SNo (eps_ (k + 2 .
An
exact proof term for the current goal is
SNo_eps_ (k + 2 Lk2 .
An
exact proof term for the current goal is
SNo_eps_pos N HN1 .
An exact proof term for the current goal is Hq2
rewrite the current goal using
mul_SNo_com x (eps_ N Hx1 LeN (from left to right).
An exact proof term for the current goal is HN2
An
exact proof term for the current goal is
SNo_eps_pos (k + 2 Lk2 .
An
exact proof term for the current goal is
SNo_eps_pos N HN1 .
An exact proof term for the current goal is Hq'2
rewrite the current goal using
mul_SNo_com y (eps_ N Hy1 LeN (from left to right).
An exact proof term for the current goal is HN3
An
exact proof term for the current goal is
SNo_eps_pos (k + 2 Lk2 .
An
exact proof term for the current goal is
SNo_eps_pos N HN1 .
An
exact proof term for the current goal is
SNo_eps_pos (k + 2 Lk2 .
An exact proof term for the current goal is HN1
An exact proof term for the current goal is Lk2
An
exact proof term for the current goal is
SNo_eps_pos N HN1 .
An
exact proof term for the current goal is
SNo_eps_pos (k + 2 Lk2 .
An exact proof term for the current goal is HN1
An
exact proof term for the current goal is
SNo_eps_pos (k + 2 Lk2 .
We will
prove k + 1 ∈ k + 2 .
We will
prove k + 1 < k + 2 .
An
exact proof term for the current goal is
SNoLt_1_2 .
Let hL be given.
Assume HhL .
Apply HhL
Let hR be given.
Assume HhR .
Apply HhR
We prove the intermediate
claim LhL :
∀ n ∈ ω , SNo (hL n .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H
We prove the intermediate
claim LhR :
∀ n ∈ ω , SNo (hR n .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H
We prove the intermediate
claim L3 :
∀ n ∈ ω , hL n < x * y .
Let n be given.
Assume Hn .
Apply HhL2 n Hn
Assume H _ .
Apply H
Assume H _ .
An exact proof term for the current goal is H
We prove the intermediate
claim L4 :
∀ n ∈ ω , x * y < hR n .
Let n be given.
Assume Hn .
Apply HhR2 n Hn
Assume H _ .
Apply H
Assume _ H .
An exact proof term for the current goal is H
We prove the intermediate
claim L5 :
∀ n m ∈ ω , hL n < hR m .
Let n be given.
Assume Hn .
Let m be given.
Assume Hm .
Apply SNoLt_tra (hL n (x * y (hR m (LhL n Hn Lxy (LhR m Hm to the current goal.
We will
prove hL n < x * y .
An exact proof term for the current goal is L3 n Hn
We will
prove x * y < hR m .
An exact proof term for the current goal is L4 m Hm
Assume _ _ .
We prove the intermediate
claim L6 :
∀ n ∈ ω , x * y < hL n + eps_ n .
Let n be given.
Assume Hn .
Apply HhL2 n Hn
Assume H _ .
Apply H
Assume _ H .
An exact proof term for the current goal is H
We prove the intermediate
claim L7 :
∀ n ∈ ω , ∀ i ∈ n , hL i < hL n .
Let n be given.
Assume Hn .
Apply HhL2 n Hn
Assume _ H .
An exact proof term for the current goal is H
We prove the intermediate
claim L8 :
∀ n ∈ ω , hR n + - eps_ n < x * y .
Let n be given.
Assume Hn .
Apply HhR2 n Hn
Assume H _ .
Apply H
Assume H _ .
An exact proof term for the current goal is H
We prove the intermediate
claim L9 :
∀ n ∈ ω , ∀ i ∈ n , hR n < hR i .
Let n be given.
Assume Hn .
Apply HhR2 n Hn
Assume _ H .
An exact proof term for the current goal is H
rewrite the current goal using HxyLR
Let w be given.
Apply HLE w Hw
Let w0 be given.
Let w1 be given.
Apply LLx2 w0 Hw0
Let k0 be given.
Apply LLy2 w1 Hw1
Let k1 be given.
Apply SNoL_E x Hx1 w0 Hw0 to the current goal.
Apply SNoL_E y Hy1 w1 Hw1 to the current goal.
We prove the intermediate
claim Lek0 :
SNo (eps_ k0 .
An
exact proof term for the current goal is
SNo_eps_ k0 Hk0 .
We prove the intermediate
claim Lek1 :
SNo (eps_ k1 .
An
exact proof term for the current goal is
SNo_eps_ k1 Hk1 .
We prove the intermediate
claim Lk0k1 :
k0 + k1 ∈ ω .
We prove the intermediate
claim Lek0k1 :
SNo (eps_ (k0 + k1 .
An
exact proof term for the current goal is
SNo_eps_ (k0 + k1 Lk0k1 .
We prove the intermediate
claim LhLk0k1 :
SNo (hL (k0 + k1 .
An
exact proof term for the current goal is
LhL (k0 + k1 Lk0k1 .
We prove the intermediate
claim Lw0y :
SNo (w0 * y .
An
exact proof term for the current goal is
SNo_mul_SNo w0 y Hw01 Hy1 .
We prove the intermediate
claim Lxw1 :
SNo (x * w1 .
An
exact proof term for the current goal is
SNo_mul_SNo x w1 Hx1 Hw11 .
We prove the intermediate
claim Lw0w1 :
SNo (w0 * w1 .
An
exact proof term for the current goal is
SNo_mul_SNo w0 w1 Hw01 Hw11 .
We prove the intermediate
claim Lmw0w1 :
SNo (- w0 * w1 .
An
exact proof term for the current goal is
SNo_minus_SNo (w0 * w1 Lw0w1 .
We prove the intermediate
claim Lw0yxw1mw0w1 :
SNo (w0 * y + x * w1 + - w0 * w1 .
An
exact proof term for the current goal is
SNo_add_SNo_3 (w0 * y (x * w1 (- w0 * w1 Lw0y Lxw1 Lmw0w1 .
rewrite the current goal using Hwe
We will
prove w0 * y + x * w1 + - w0 * w1 ≤ hL (k0 + k1 .
Apply SNoLtLe_or (hL (k0 + k1 (w0 * y + x * w1 + - w0 * w1 LhLk0k1 Lw0yxw1mw0w1 to the current goal.
We will
prove x * y < x * y .
We will
prove hL (k0 + k1 + eps_ (k0 + k1 < x * y .
Apply add_SNo_Lt1 (hL (k0 + k1 (eps_ (k0 + k1 (w0 * y + x * w1 + - w0 * w1 LhLk0k1 Lek0k1 Lw0yxw1mw0w1 to the current goal.
An exact proof term for the current goal is H1
rewrite the current goal using
add_SNo_com (w0 * y + x * w1 + - w0 * w1 (eps_ (k0 + k1 Lw0yxw1mw0w1 Lek0k1 (from left to right).
rewrite the current goal using
add_SNo_com_3_0_1 (w0 * y (x * w1 (- w0 * w1 Lw0y Lxw1 Lmw0w1 (from left to right).
We will
prove eps_ (k0 + k1 ≤ (x + - w0 * (y + - w1 .
An
exact proof term for the current goal is
SNo_eps_pos k0 Hk0 .
An
exact proof term for the current goal is
SNo_eps_pos k1 Hk1 .
An exact proof term for the current goal is Hk0b
An exact proof term for the current goal is Hk1b
An exact proof term for the current goal is H1
An
exact proof term for the current goal is
HhLR5 (k0 + k1 Lk0k1 .
Let z0 be given.
Let z1 be given.
Apply LRx2 z0 Hz0
Let k0 be given.
Apply LRy2 z1 Hz1
Let k1 be given.
Apply SNoR_E x Hx1 z0 Hz0 to the current goal.
Apply SNoR_E y Hy1 z1 Hz1 to the current goal.
We prove the intermediate
claim Lek0 :
SNo (eps_ k0 .
An
exact proof term for the current goal is
SNo_eps_ k0 Hk0 .
We prove the intermediate
claim Lek1 :
SNo (eps_ k1 .
An
exact proof term for the current goal is
SNo_eps_ k1 Hk1 .
We prove the intermediate
claim Lk0k1 :
k0 + k1 ∈ ω .
We prove the intermediate
claim Lek0k1 :
SNo (eps_ (k0 + k1 .
An
exact proof term for the current goal is
SNo_eps_ (k0 + k1 Lk0k1 .
We prove the intermediate
claim LhLk0k1 :
SNo (hL (k0 + k1 .
An
exact proof term for the current goal is
LhL (k0 + k1 Lk0k1 .
We prove the intermediate
claim Lz0y :
SNo (z0 * y .
An
exact proof term for the current goal is
SNo_mul_SNo z0 y Hz01 Hy1 .
We prove the intermediate
claim Lxz1 :
SNo (x * z1 .
An
exact proof term for the current goal is
SNo_mul_SNo x z1 Hx1 Hz11 .
We prove the intermediate
claim Lz0z1 :
SNo (z0 * z1 .
An
exact proof term for the current goal is
SNo_mul_SNo z0 z1 Hz01 Hz11 .
We prove the intermediate
claim Lmz0z1 :
SNo (- z0 * z1 .
An
exact proof term for the current goal is
SNo_minus_SNo (z0 * z1 Lz0z1 .
We prove the intermediate
claim Lz0yxz1mz0z1 :
SNo (z0 * y + x * z1 + - z0 * z1 .
An
exact proof term for the current goal is
SNo_add_SNo_3 (z0 * y (x * z1 (- z0 * z1 Lz0y Lxz1 Lmz0z1 .
rewrite the current goal using Hwe
We will
prove z0 * y + x * z1 + - z0 * z1 ≤ hL (k0 + k1 .
Apply SNoLtLe_or (hL (k0 + k1 (z0 * y + x * z1 + - z0 * z1 LhLk0k1 Lz0yxz1mz0z1 to the current goal.
We will
prove x * y < x * y .
We will
prove hL (k0 + k1 + eps_ (k0 + k1 < x * y .
Apply add_SNo_Lt1 (hL (k0 + k1 (eps_ (k0 + k1 (z0 * y + x * z1 + - z0 * z1 LhLk0k1 Lek0k1 Lz0yxz1mz0z1 to the current goal.
An exact proof term for the current goal is H1
rewrite the current goal using
add_SNo_com (z0 * y + x * z1 + - z0 * z1 (eps_ (k0 + k1 Lz0yxz1mz0z1 Lek0k1 (from left to right).
rewrite the current goal using
add_SNo_rotate_3_1 (z0 * y (x * z1 (- z0 * z1 Lz0y Lxz1 Lmz0z1 (from left to right).
rewrite the current goal using
minus_SNo_invol (z0 * z1 Lz0z1 (from left to right).
We will
prove eps_ (k0 + k1 ≤ (z0 + - x * (z1 + - y .
An
exact proof term for the current goal is
SNo_eps_pos k0 Hk0 .
An
exact proof term for the current goal is
SNo_eps_pos k1 Hk1 .
An exact proof term for the current goal is Hk0b
An exact proof term for the current goal is Hk1b
An exact proof term for the current goal is H1
An
exact proof term for the current goal is
HhLR5 (k0 + k1 Lk0k1 .
Let z be given.
Apply HRE z Hz
Let w0 be given.
Let z1 be given.
Apply LLx2 w0 Hw0
Let k0 be given.
Apply LRy2 z1 Hz1
Let k1 be given.
Apply SNoL_E x Hx1 w0 Hw0 to the current goal.
Apply SNoR_E y Hy1 z1 Hz1 to the current goal.
We prove the intermediate
claim Lek0 :
SNo (eps_ k0 .
An
exact proof term for the current goal is
SNo_eps_ k0 Hk0 .
We prove the intermediate
claim Lek1 :
SNo (eps_ k1 .
An
exact proof term for the current goal is
SNo_eps_ k1 Hk1 .
We prove the intermediate
claim Lk0k1 :
k0 + k1 ∈ ω .
We prove the intermediate
claim Lek0k1 :
SNo (eps_ (k0 + k1 .
An
exact proof term for the current goal is
SNo_eps_ (k0 + k1 Lk0k1 .
We prove the intermediate
claim Lmek0k1 :
SNo (- eps_ (k0 + k1 .
We prove the intermediate
claim LhRk0k1 :
SNo (hR (k0 + k1 .
An
exact proof term for the current goal is
LhR (k0 + k1 Lk0k1 .
We prove the intermediate
claim Lw0y :
SNo (w0 * y .
An
exact proof term for the current goal is
SNo_mul_SNo w0 y Hw01 Hy1 .
We prove the intermediate
claim Lxz1 :
SNo (x * z1 .
An
exact proof term for the current goal is
SNo_mul_SNo x z1 Hx1 Hz11 .
We prove the intermediate
claim Lw0z1 :
SNo (w0 * z1 .
An
exact proof term for the current goal is
SNo_mul_SNo w0 z1 Hw01 Hz11 .
We prove the intermediate
claim Lmw0z1 :
SNo (- w0 * z1 .
An
exact proof term for the current goal is
SNo_minus_SNo (w0 * z1 Lw0z1 .
We prove the intermediate
claim Lw0yxz1mw0z1 :
SNo (w0 * y + x * z1 + - w0 * z1 .
An
exact proof term for the current goal is
SNo_add_SNo_3 (w0 * y (x * z1 (- w0 * z1 Lw0y Lxz1 Lmw0z1 .
rewrite the current goal using Hze
An
exact proof term for the current goal is
HhLR6 (k0 + k1 Lk0k1 .
We will
prove hR (k0 + k1 ≤ w0 * y + x * z1 + - w0 * z1 .
Apply SNoLtLe_or (w0 * y + x * z1 + - w0 * z1 (hR (k0 + k1 Lw0yxz1mw0z1 LhRk0k1 to the current goal.
We will
prove x * y < x * y .
We will
prove x * y < hR (k0 + k1 + - eps_ (k0 + k1 .
rewrite the current goal using
add_SNo_com (x * y (eps_ (k0 + k1 Lxy Lek0k1 (from left to right).
rewrite the current goal using
add_SNo_rotate_3_1 (w0 * y (x * z1 (- w0 * z1 Lw0y Lxz1 Lmw0z1 (from left to right).
rewrite the current goal using
add_SNo_assoc_4 (- w0 * z1 (w0 * y (x * z1 (- x * y Lmw0z1 Lw0y Lxz1 Lmxy (from right to left).
rewrite the current goal using
add_SNo_rotate_4_1 (- w0 * z1 (w0 * y (x * z1 (- x * y Lmw0z1 Lw0y Lxz1 Lmxy (from left to right).
rewrite the current goal using
add_SNo_rotate_4_1 (- x * y (- w0 * z1 (w0 * y (x * z1 Lmxy Lmw0z1 Lw0y Lxz1 (from left to right).
An
exact proof term for the current goal is
SNo_eps_pos k0 Hk0 .
An
exact proof term for the current goal is
SNo_eps_pos k1 Hk1 .
An exact proof term for the current goal is Hk0b
An exact proof term for the current goal is Hk1b
Apply add_SNo_Lt1 (w0 * y + x * z1 + - w0 * z1 (- eps_ (k0 + k1 (hR (k0 + k1 Lw0yxz1mw0z1 Lmek0k1 LhRk0k1 to the current goal.
An exact proof term for the current goal is H1
An
exact proof term for the current goal is
L8 (k0 + k1 Lk0k1 .
An exact proof term for the current goal is H1
Let z0 be given.
Let w1 be given.
Apply LRx2 z0 Hz0
Let k0 be given.
Apply LLy2 w1 Hw1
Let k1 be given.
Apply SNoR_E x Hx1 z0 Hz0 to the current goal.
Apply SNoL_E y Hy1 w1 Hw1 to the current goal.
We prove the intermediate
claim Lek0 :
SNo (eps_ k0 .
An
exact proof term for the current goal is
SNo_eps_ k0 Hk0 .
We prove the intermediate
claim Lek1 :
SNo (eps_ k1 .
An
exact proof term for the current goal is
SNo_eps_ k1 Hk1 .
We prove the intermediate
claim Lk0k1 :
k0 + k1 ∈ ω .
We prove the intermediate
claim Lek0k1 :
SNo (eps_ (k0 + k1 .
An
exact proof term for the current goal is
SNo_eps_ (k0 + k1 Lk0k1 .
We prove the intermediate
claim Lmek0k1 :
SNo (- eps_ (k0 + k1 .
We prove the intermediate
claim LhRk0k1 :
SNo (hR (k0 + k1 .
An
exact proof term for the current goal is
LhR (k0 + k1 Lk0k1 .
We prove the intermediate
claim Lz0y :
SNo (z0 * y .
An
exact proof term for the current goal is
SNo_mul_SNo z0 y Hz01 Hy1 .
We prove the intermediate
claim Lxw1 :
SNo (x * w1 .
An
exact proof term for the current goal is
SNo_mul_SNo x w1 Hx1 Hw11 .
We prove the intermediate
claim Lz0w1 :
SNo (z0 * w1 .
An
exact proof term for the current goal is
SNo_mul_SNo z0 w1 Hz01 Hw11 .
We prove the intermediate
claim Lmz0w1 :
SNo (- z0 * w1 .
An
exact proof term for the current goal is
SNo_minus_SNo (z0 * w1 Lz0w1 .
We prove the intermediate
claim Lz0yxw1mz0w1 :
SNo (z0 * y + x * w1 + - z0 * w1 .
An
exact proof term for the current goal is
SNo_add_SNo_3 (z0 * y (x * w1 (- z0 * w1 Lz0y Lxw1 Lmz0w1 .
rewrite the current goal using Hze
An
exact proof term for the current goal is
HhLR6 (k0 + k1 Lk0k1 .
We will
prove hR (k0 + k1 ≤ z0 * y + x * w1 + - z0 * w1 .
Apply SNoLtLe_or (z0 * y + x * w1 + - z0 * w1 (hR (k0 + k1 Lz0yxw1mz0w1 LhRk0k1 to the current goal.
We will
prove x * y < x * y .
We will
prove x * y < hR (k0 + k1 + - eps_ (k0 + k1 .
rewrite the current goal using
add_SNo_com (x * y (eps_ (k0 + k1 Lxy Lek0k1 (from left to right).
rewrite the current goal using
add_SNo_assoc_4 (z0 * y (x * w1 (- z0 * w1 (- x * y Lz0y Lxw1 Lmz0w1 Lmxy (from right to left).
rewrite the current goal using
add_SNo_rotate_3_1 (- z0 * w1 (- x * y (x * w1 Lmz0w1 Lmxy Lxw1 (from right to left).
An
exact proof term for the current goal is
SNo_eps_pos k0 Hk0 .
An
exact proof term for the current goal is
SNo_eps_pos k1 Hk1 .
An exact proof term for the current goal is Hk0b
An exact proof term for the current goal is Hk1b
Apply add_SNo_Lt1 (z0 * y + x * w1 + - z0 * w1 (- eps_ (k0 + k1 (hR (k0 + k1 Lz0yxw1mz0w1 Lmek0k1 LhRk0k1 to the current goal.
An exact proof term for the current goal is H1
An
exact proof term for the current goal is
L8 (k0 + k1 Lk0k1 .
An exact proof term for the current goal is H1
Let w be given.
rewrite the current goal using HxyLR
Let n be given.
Assume Hn Hwn .
rewrite the current goal using Hwn
We will
prove hL n < x * y .
An exact proof term for the current goal is L3 n Hn
Let z be given.
rewrite the current goal using HxyLR
Let n be given.
Assume Hn Hzn .
rewrite the current goal using Hzn
We will
prove x * y < hR n .
An exact proof term for the current goal is L4 n Hn
Apply HC
An
exact proof term for the current goal is
SNo_approx_real (x * y Lxy hL HhL1 hR HhR1 L3 L6 L7 L4 L9 L10 .
∎
Proof: Let x be given.
Assume Hx .
Let y be given.
Assume Hy .
We prove the intermediate
claim Lx :
SNo x .
An
exact proof term for the current goal is
real_SNo x Hx .
We prove the intermediate
claim Ly :
SNo y .
An
exact proof term for the current goal is
real_SNo y Hy .
We prove the intermediate
claim Lxy :
SNo (x * y .
An
exact proof term for the current goal is
SNo_mul_SNo x y Lx Ly .
We prove the intermediate
claim Lmx :
0 < - x .
rewrite the current goal using
minus_SNo_0 (from left to right).
An exact proof term for the current goal is H1
rewrite the current goal using
minus_SNo_0 (from left to right).
An exact proof term for the current goal is H2
rewrite the current goal using H2
rewrite the current goal using
mul_SNo_zeroR x Lx (from left to right).
An
exact proof term for the current goal is
real_0 .
rewrite the current goal using
minus_SNo_invol (x * y Lxy (from right to left).
rewrite the current goal using H1
rewrite the current goal using
mul_SNo_zeroL y Ly (from left to right).
An
exact proof term for the current goal is
real_0 .
rewrite the current goal using
minus_SNo_invol (x * y Lxy (from right to left).
rewrite the current goal using
minus_SNo_0 (from left to right).
An exact proof term for the current goal is H2
rewrite the current goal using H2
rewrite the current goal using
mul_SNo_zeroR x Lx (from left to right).
An
exact proof term for the current goal is
real_0 .
∎
Proof: Let x, y and z be given.
Assume Hx Hy Hz Hxy Hyxz .
We prove the intermediate
claim L1 :
0 ≤ y + - x .
We will
prove x + - x ≤ y + - x .
We prove the intermediate
claim L2 :
abs_SNo (y + - x = y + - x .
rewrite the current goal using L2
We will
prove y + - x < z .
rewrite the current goal using
add_SNo_com z x Hz Hx (from left to right).
An exact proof term for the current goal is Hyxz
∎
Proof: Let x be given.
Assume HxR Hxnn .
Apply real_E x HxR to the current goal.
Let m be given.
Assume Hm .
Apply IHm
An exact proof term for the current goal is H3
We use m witness the existential quantifier.
Apply andI to the current goal.
An
exact proof term for the current goal is
nat_p_omega m Hm .
Apply andI to the current goal.
An exact proof term for the current goal is H3
An exact proof term for the current goal is H2
Let q be given.
Assume H .
Apply H
Assume H .
Apply H
rewrite the current goal using
eps_0_1 (from left to right).
Let m be given.
Assume H .
Apply H
We prove the intermediate
claim Lq :
SNo q .
Apply L1 (ordsucc m to the current goal.
An exact proof term for the current goal is Hm
We prove the intermediate
claim Lq1 :
SNo (q + 1 .
An exact proof term for the current goal is Lq
An
exact proof term for the current goal is
SNo_1 .
We will
prove SNo (q + 1 .
An exact proof term for the current goal is Lq1
An exact proof term for the current goal is H2
An exact proof term for the current goal is Lq
An
exact proof term for the current goal is
SNo_1 .
An exact proof term for the current goal is L2
An exact proof term for the current goal is H2
rewrite the current goal using L3
∎
Proof: Let x be given.
Assume HxR Hxpos Hxn2 Hxne .
Apply real_E x HxR to the current goal.
rewrite the current goal using
eps_0_1 (from left to right).
We use
1 to
witness the existential quantifier.
Apply andI to the current goal.
Apply SepI to the current goal.
An exact proof term for the current goal is H3
rewrite the current goal using
eps_0_1 (from left to right).
An
exact proof term for the current goal is
pos_low_eq_one x Hx1 Hxpos H3 .
An exact proof term for the current goal is H1
An
exact proof term for the current goal is
SNoLt_0_1 .
An exact proof term for the current goal is H2
Apply Hxn2
An exact proof term for the current goal is H2
Let m be given.
Assume H .
Apply H
Assume H .
Apply H
We prove the intermediate
claim Lm :
nat_p m .
An
exact proof term for the current goal is
omega_nat_p m Hm .
Apply nat_inv m Lm to the current goal.
rewrite the current goal using Hm0
An exact proof term for the current goal is Hxm1
An exact proof term for the current goal is H1
Assume H .
Apply H
Let m' be given.
Assume H .
Apply H
Apply nat_inv m' Hm' to the current goal.
rewrite the current goal using Hm'0
rewrite the current goal using Hmm'
An exact proof term for the current goal is Hxm1
An exact proof term for the current goal is H2
Assume H .
Apply H
Let m'' be given.
Assume H .
Apply H
We use m witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hm
Apply and3I to the current goal.
We prove the intermediate
claim L1aa :
m ∈ 2 .
An exact proof term for the current goal is H5
Apply cases_2 m L1aa (λi ⇒ m ≠ i ) to the current goal.
rewrite the current goal using Hmm'
rewrite the current goal using Hmm'
rewrite the current goal using Hm'm''
An exact proof term for the current goal is H5
An exact proof term for the current goal is H4
An exact proof term for the current goal is Hxm1
Apply nat_inv m'' Hm'' to the current goal.
Apply Hxn2
rewrite the current goal using H4
rewrite the current goal using Hmm'
rewrite the current goal using Hm'm''
rewrite the current goal using Hm''0
Use reflexivity.
Assume H .
Apply H
Let m''' be given.
Assume H .
Apply H
We use m' witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hm'
Apply and3I to the current goal.
rewrite the current goal using Hm'm''
We will
prove 2 ≤ 1 + m'' .
rewrite the current goal using Hm''m'''
We will
prove 2 ≤ 1 + 1 + m''' .
We will
prove 2 ≤ (1 + 1 + m''' .
rewrite the current goal using
add_SNo_1_1_2 (from left to right).
We will
prove 2 ≤ 2 + m''' .
rewrite the current goal using
add_SNo_0R 2 SNo_2 (from right to left) at position 1.
We will
prove 2 + 0 ≤ 2 + m''' .
rewrite the current goal using H4
rewrite the current goal using Hmm'
rewrite the current goal using H4
rewrite the current goal using Hmm'
Apply L1a
Let k be given.
Assume H .
Apply H
Assume H .
Apply H
Assume H .
Apply H
We prove the intermediate
claim Lk :
nat_p k .
An
exact proof term for the current goal is
omega_nat_p k Hk .
We prove the intermediate
claim LkS :
SNo k .
An
exact proof term for the current goal is
nat_p_SNo k Lk .
We use k witness the existential quantifier.
Apply andI to the current goal.
Apply SepI to the current goal.
We will
prove k ∈ SNoL x .
Apply SNoL_I to the current goal.
An exact proof term for the current goal is Hx1
An exact proof term for the current goal is LkS
An exact proof term for the current goal is H4
Apply SNoLtLe_tra k x k LkS Hx1 LkS Hkx to the current goal.
rewrite the current goal using H4
Apply SNoLt_tra k x k LkS Hx1 LkS Hkx to the current goal.
An exact proof term for the current goal is Hkx
An exact proof term for the current goal is H2k
rewrite the current goal using
add_SNo_1_1_2 (from right to left).
rewrite the current goal using
mul_SNo_oneL k LkS (from left to right).
We will
prove 1 + k < k + k .
An exact proof term for the current goal is H2k
Let m be given.
Assume Hm .
We prove the intermediate
claim Lm :
m ∈ ω .
An
exact proof term for the current goal is
nat_p_omega m Hm .
We prove the intermediate
claim Lem :
SNo (eps_ m .
An
exact proof term for the current goal is
SNo_eps_ m Lm .
We prove the intermediate
claim LSm :
ordsucc m ∈ ω .
We use
(eps_ (ordsucc m to
witness the existential quantifier.
Apply andI to the current goal.
Apply SepI to the current goal.
Apply SNoLtE x (eps_ m Hx1 Lem H2 to the current goal.
Let z be given.
We prove the intermediate
claim Lz0 :
z = 0 .
An exact proof term for the current goal is Hz8
Apply SNoLt_tra x z x Hx1 Hz1 Hx1 Hz5 to the current goal.
rewrite the current goal using Lz0
An exact proof term for the current goal is Hxpos
We prove the intermediate
claim Lx0 :
x = 0 .
An exact proof term for the current goal is H5
rewrite the current goal using Lx0
An exact proof term for the current goal is Hxpos
rewrite the current goal using
SNoLev_eps_ m Lm (from left to right).
Let z be given.
We prove the intermediate
claim Lz0 :
z = 0 .
Apply H4 (SNoLev z H6 to the current goal.
Assume H7 _ .
Apply H7
An exact proof term for the current goal is Hz8
rewrite the current goal using Lz0
Apply H5
rewrite the current goal using H6
An exact proof term for the current goal is Hz8
An exact proof term for the current goal is H6
rewrite the current goal using H9
An exact proof term for the current goal is H3
An exact proof term for the current goal is H1
rewrite the current goal using
add_SNo_1_1_2 (from right to left).
An exact proof term for the current goal is H2
An
exact proof term for the current goal is
Hxne m (nat_p_omega m Hm H2 .
An exact proof term for the current goal is IHm H2
We prove the intermediate
claim L2 :
∃ k ∈ ω , eps_ k < x .
Apply dneg to the current goal.
We prove the intermediate
claim Lx0 :
0 = x .
Apply Hx6 0 to the current goal.
An
exact proof term for the current goal is
nat_0 .
Let k be given.
Assume Hk .
rewrite the current goal using
abs_SNo_minus x Hx1 (from left to right).
rewrite the current goal using
pos_abs_SNo x Hxpos (from left to right).
We will
prove x < eps_ k .
An exact proof term for the current goal is H2
An exact proof term for the current goal is Hxne k Hk H2
Apply H1
We use k witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk
An exact proof term for the current goal is H2
rewrite the current goal using Lx0
An exact proof term for the current goal is Hxpos
Apply L2
Let k be given.
Assume H .
Apply H
An
exact proof term for the current goal is
L1 k (omega_nat_p k Hk H1 .
∎
Proof:
Let x be given.
Apply real_E x HxR to the current goal.
Assume _ .
Assume _ _ _ _ _ .
We prove the intermediate
claim Lmx :
SNo (- x .
Let y be given.
Assume Hy .
Let z be given.
Assume Hz Hzpos .
We prove the intermediate
claim LzR :
z ∈ real .
rewrite the current goal using H1
An exact proof term for the current goal is Hz1
An exact proof term for the current goal is Hz4
Apply IHx z Hz LzR Hzpos
Assume _ .
An
exact proof term for the current goal is
real_1 .
An exact proof term for the current goal is LzR
An exact proof term for the current goal is HxR
An exact proof term for the current goal is Hy
An exact proof term for the current goal is IH1
Apply andI to the current goal.
rewrite the current goal using
tuple_2_0_eq (from left to right).
Let y be given.
rewrite the current goal using
SingE 0 y Hy (from left to right).
An
exact proof term for the current goal is
real_0 .
rewrite the current goal using
tuple_2_1_eq (from left to right).
Let y be given.
An
exact proof term for the current goal is
EmptyE y Hy .
Let k be given.
Apply IHk
Assume IHk0 IHk1 .
Apply andI to the current goal.
rewrite the current goal using
tuple_2_0_eq (from left to right).
Let y be given.
An exact proof term for the current goal is IHk0 y
Let u be given.
Let z be given.
Apply SNoR_E x Hx z Hz to the current goal.
rewrite the current goal using Hye
Apply L1
An exact proof term for the current goal is IHk0 u Hu
An
exact proof term for the current goal is
SNoS_I2 z x Hz1 Hx Hz2 .
An
exact proof term for the current goal is
SNoLt_tra 0 x z SNo_0 Hx Hz1 Hxpos Hz3 .
Let u be given.
Let w be given.
Apply SepE (SNoL x (λw ⇒ 0 < w ) w Hw to the current goal.
Apply SNoL_E x Hx w Hw0 to the current goal.
rewrite the current goal using Hye
Apply L1
An exact proof term for the current goal is IHk1 u Hu
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 Hwpos
rewrite the current goal using
tuple_2_1_eq (from left to right).
Let y be given.
An exact proof term for the current goal is IHk1 y
Let u be given.
Let w be given.
Apply SepE (SNoL x (λw ⇒ 0 < w ) w Hw to the current goal.
Apply SNoL_E x Hx w Hw0 to the current goal.
rewrite the current goal using Hye
Apply L1
An exact proof term for the current goal is IHk0 u Hu
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 Hwpos
Let u be given.
Let z be given.
Apply SNoR_E x Hx z Hz to the current goal.
rewrite the current goal using Hye
Apply L1
An exact proof term for the current goal is IHk1 u Hu
An
exact proof term for the current goal is
SNoS_I2 z x Hz1 Hx Hz2 .
An
exact proof term for the current goal is
SNoLt_tra 0 x z SNo_0 Hx Hz1 Hxpos Hz3 .
Apply andI to the current goal.
Let u be given.
Assume Hu Hupos .
Assume _ _ .
Assume _ .
We prove the intermediate
claim LLR :
SNoCutP L R .
Set y to be the term
SNoCut L R .
Let k be given.
Assume Hk .
Let w be given.
Assume Hw .
Let k be given.
Assume Hk .
Let z be given.
Assume Hz .
Let w be given.
Let p be given.
Assume Hp .
Let k be given.
An exact proof term for the current goal is Hp k Hk Hwk
Let z be given.
Let p be given.
Assume Hp .
Let k be given.
An exact proof term for the current goal is Hp k Hk Hzk
We prove the intermediate
claim LLreal :
L ⊆ real .
Let w be given.
Apply LLE w Hw
Let k be given.
Assume _ .
An exact proof term for the current goal is H2 w Hwk
We prove the intermediate
claim LRreal :
R ⊆ real .
Let z be given.
Apply LRE z Hz
Let k be given.
Assume _ .
An exact proof term for the current goal is H2 z Hzk
We prove the intermediate
claim LL0 :
L ≠ 0 .
Apply EmptyE 0 to the current goal.
rewrite the current goal using H1
rewrite the current goal using
tuple_2_0_eq (from left to right).
Apply SingI to the current goal.
Assume H .
Apply H
Let m be given.
Assume H .
Apply H
rewrite the current goal using H1
Apply xm (x = 2 to the current goal.
rewrite the current goal using H2
An
exact proof term for the current goal is
nat_1 .
We prove the intermediate
claim L4 :
∀ m ∈ ω , x ≠ eps_ m .
Let m be given.
Assume Hm H3 .
Apply H1
We use m witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hm
An exact proof term for the current goal is H3
Let u be given.
Assume H .
Apply H
Apply SepE (SNoL x (λw ⇒ 0 < w ) u Hu to the current goal.
Apply SNoL_E x Hx u Hua to the current goal.
We prove the intermediate
claim Lumx :
SNo (u + - x .
An exact proof term for the current goal is Hua1
An exact proof term for the current goal is Lmx
We prove the intermediate
claim L5 :
∀ w ∈ L , f w ∈ R .
Let w be given.
Assume Hw .
Apply LLE w Hw
Let k be given.
rewrite the current goal using
tuple_2_1_eq (from left to right).
An exact proof term for the current goal is Hwk
An exact proof term for the current goal is Hu
We prove the intermediate
claim L6 :
∀ z ∈ R , f z ∈ L .
Let z be given.
Assume Hz .
Apply LRE z Hz
Let k be given.
rewrite the current goal using
tuple_2_0_eq (from left to right).
An exact proof term for the current goal is Hzk
An exact proof term for the current goal is Hu
We prove the intermediate
claim Luu :
SNo (u * u .
An
exact proof term for the current goal is
SNo_mul_SNo u u Hua1 Hua1 .
We prove the intermediate
claim Luupos :
0 < u * u .
An
exact proof term for the current goal is
mul_SNo_pos_pos u u Hua1 Hua1 Hub Hub .
We prove the intermediate
claim Luun0 :
u * u ≠ 0 .
Assume H .
rewrite the current goal using H
An exact proof term for the current goal is Luupos
We prove the intermediate
claim L2u :
SNo (2 * u .
We prove the intermediate
claim Lf :
∀v, SNo v ∀p : prop , (SNo ((u + - x * v SNo (1 + ((u + - x * v SNo (f v p → p .
Let v be given.
Assume Hv .
Let p be given.
Assume Hp .
We prove the intermediate
claim Lf1 :
SNo ((u + - x * v .
An exact proof term for the current goal is Lumx
An exact proof term for the current goal is Hv
We prove the intermediate
claim Lf2 :
SNo (1 + (u + - x * v .
An
exact proof term for the current goal is
SNo_1 .
An exact proof term for the current goal is Lf1
An exact proof term for the current goal is Lf2
An exact proof term for the current goal is Lru
An exact proof term for the current goal is Hp Lf1 Lf2 Lf3
We prove the intermediate
claim Luf :
∀v, SNo v u * f v = 1 + (u + - x * v .
Let v be given.
Assume Hv .
Apply Lf v Hv
We prove the intermediate
claim L7 :
∀v, SNo v f (f v = (v * u * u + x * x * v + 2 * u + - ((2 * u * x * v + x :/: (u * u .
Let v be given.
Assume Hv .
Set v' to be the term f v
Apply Lf v Hv
Apply Lf v' Hv'
We prove the intermediate
claim Lxv :
SNo (x * v .
An
exact proof term for the current goal is
SNo_mul_SNo x v Hx Hv .
We prove the intermediate
claim Lxxv :
SNo (x * x * v .
An
exact proof term for the current goal is
SNo_mul_SNo x (x * v Hx Lxv .
We prove the intermediate
claim L2uxv :
SNo ((2 * u * x * v .
An
exact proof term for the current goal is
SNo_mul_SNo (2 * u (x * v L2u Lxv .
We prove the intermediate
claim Lvuu :
SNo (v * u * u .
An
exact proof term for the current goal is
SNo_mul_SNo v (u * u Hv Luu .
We prove the intermediate
claim Luxv :
SNo (u * x * v .
An
exact proof term for the current goal is
SNo_mul_SNo u (x * v Hua1 Lxv .
We prove the intermediate
claim Luv :
SNo (u * v .
An
exact proof term for the current goal is
SNo_mul_SNo u v Hua1 Hv .
We prove the intermediate
claim Lxuv :
SNo (x * u * v .
An
exact proof term for the current goal is
SNo_mul_SNo x (u * v Hx Luv .
We prove the intermediate
claim Lmuxv :
SNo (- u * x * v .
An
exact proof term for the current goal is
SNo_minus_SNo (u * x * v Luxv .
We prove the intermediate
claim Lmxuv :
SNo (- x * u * v .
An
exact proof term for the current goal is
SNo_minus_SNo (x * u * v Lxuv .
We prove the intermediate
claim Lmxmxuv :
SNo (- x + - x * u * v .
An exact proof term for the current goal is Lmx
An exact proof term for the current goal is Lmxuv
We prove the intermediate
claim Lmxmxuvxxv :
SNo (- x + - x * u * v + x * x * v .
An exact proof term for the current goal is Lmx
An exact proof term for the current goal is Lmxuv
An exact proof term for the current goal is Lxxv
Use symmetry.
Use transitivity with
u + u * (1 + (u + - x * v + - x * (1 + (u + - x * v ,
u + u * u * v' + - x * u * v' ,
u * (1 + (u + - x * v' , and
u * (u * f v' .
Use f_equal.
rewrite the current goal using
add_SNo_1_1_2 (from right to left) at position 1.
rewrite the current goal using
mul_SNo_oneL u Hua1 (from left to right).
Use transitivity with and
u + u + x * x * v + - ((2 * u * x * v + x .
Use symmetry.
An exact proof term for the current goal is Lxxv
An exact proof term for the current goal is L2uxv
An exact proof term for the current goal is Hx
Use f_equal.
Use f_equal.
Use transitivity with and
x * x * v + - u * x * v + - x + - x * u * v .
Use f_equal.
We will
prove - ((2 * u * x * v + x = - (u * x * v + x + x * u * v .
Use f_equal.
We will
prove (2 * u * x * v + x = u * x * v + x + x * u * v .
rewrite the current goal using
mul_SNo_com_3_0_1 x u v Hx Hua1 Hv (from left to right).
We will
prove (2 * u * x * v + x = u * x * v + x + u * x * v .
rewrite the current goal using
add_SNo_com x (u * x * v Hx Luxv (from left to right).
rewrite the current goal using
add_SNo_assoc (u * x * v (u * x * v x Luxv Luxv Hx (from left to right).
Use f_equal.
We will
prove (2 * u * x * v = u * x * v + u * x * v .
rewrite the current goal using
add_SNo_1_1_2 (from right to left) at position 1.
rewrite the current goal using
mul_SNo_oneL u Hua1 (from left to right).
We will
prove (u + u * x * v = u * x * v + u * x * v .
An
exact proof term for the current goal is
mul_SNo_distrR u u (x * v Hua1 Hua1 Lxv .
rewrite the current goal using
add_SNo_com_3_0_1 (x * x * v (- u * x * v (- x + - x * u * v Lxxv Lmuxv Lmxmxuv (from left to right).
Use f_equal.
rewrite the current goal using
add_SNo_com_3_0_1 (x * x * v (- x (- x * u * v Lxxv Lmx Lmxuv (from left to right).
Use f_equal.
An
exact proof term for the current goal is
add_SNo_com (x * x * v (- x * u * v Lxxv Lmxuv .
Use f_equal.
An exact proof term for the current goal is Lvuu
An exact proof term for the current goal is Hua1
An exact proof term for the current goal is Lmuxv
An exact proof term for the current goal is Lmxmxuvxxv
An exact proof term for the current goal is Hua1
An exact proof term for the current goal is Lmuxv
An exact proof term for the current goal is Lmxmxuvxxv
Use f_equal.
Use f_equal.
rewrite the current goal using
mul_SNo_oneR u Hua1 (from left to right).
We will
prove v * u * u + u + - u * x * v = u + u * (u + - x * v .
We will
prove u + v * u * u + - u * x * v = u + u * (u + - x * v .
Use f_equal.
We will
prove v * u * u + - u * x * v = u * (u + - x * v .
rewrite the current goal using
mul_SNo_distrR u (- x v Hua1 Lmx Hv (from left to right).
We will
prove v * u * u + - u * x * v = u * (u * v + (- x * v .
We will
prove v * u * u + - u * x * v = u * u * v + u * (- x * v .
Use f_equal.
We will
prove v * u * u = u * u * v .
rewrite the current goal using
mul_SNo_com u v Hua1 Hv (from left to right).
We will
prove - u * x * v = u * (- x * v .
Use symmetry.
rewrite the current goal using
mul_SNo_oneR (- x Lmx (from left to right).
Use f_equal.
We will
prove - x * u * v + x * x * v = (- x * (u + - x * v .
rewrite the current goal using
mul_SNo_distrR u (- x v Hua1 Lmx Hv (from left to right).
Use f_equal.
We will
prove x * x * v = (- x * (- x * v .
rewrite the current goal using
mul_SNo_assoc (- x (- x v Lmx Lmx Hv (from left to right).
An
exact proof term for the current goal is
mul_SNo_assoc x x v Hx Hx Hv .
An
exact proof term for the current goal is
Luf v Hv (λw z ⇒ u + u * w + - x * w = u + u * u * v' + - x * u * v' ) (λq H ⇒ H ) .
We will
prove u + u * u * v' + - x * u * v' = u * (1 + (u + - x * v' .
rewrite the current goal using
mul_SNo_oneR u Hua1 (from left to right).
Use f_equal.
We will
prove u * u * v' + - x * u * v' = u * (u + - x * v' .
We will
prove u * u * v' + - x * u * v' = u * (u * v' + (- x * v' .
We will
prove u * u * v' + - x * u * v' = u * u * v' + u * (- x * v' .
Use f_equal.
We will
prove - x * u * v' = u * (- x * v' .
We will
prove - x * u * v' = (- x * u * v' .
Use symmetry.
Use f_equal.
Use symmetry.
An exact proof term for the current goal is Luf v' Hv'
An
exact proof term for the current goal is
mul_SNo_assoc u u (f v' Hua1 Hua1 Hfv' .
We prove the intermediate
claim L8 :
∀ w ∈ L , ∃ w' ∈ L , w < w' .
Let w be given.
Assume Hw .
We prove the intermediate
claim Lw :
SNo w .
An exact proof term for the current goal is LLreal w Hw
We prove the intermediate
claim Lxw :
SNo (x * w .
An
exact proof term for the current goal is
SNo_mul_SNo x w Hx Lw .
We prove the intermediate
claim Lxxw :
SNo (x * x * w .
An
exact proof term for the current goal is
SNo_mul_SNo x (x * w Hx Lxw .
We prove the intermediate
claim L2uxw :
SNo ((2 * u * x * w .
An
exact proof term for the current goal is
SNo_mul_SNo (2 * u (x * w L2u Lxw .
We prove the intermediate
claim Lwuu :
SNo (w * u * u .
An
exact proof term for the current goal is
SNo_mul_SNo w (u * u Lw Luu .
We use f (f w witness the existential quantifier.
Apply andI to the current goal.
Apply L6
Apply L5
An exact proof term for the current goal is Hw
We will
prove w < f (f w .
We prove the intermediate
claim L8a :
w < (w * u * u + x * x * w + 2 * u + - ((2 * u * x * w + x :/: (u * u .
An exact proof term for the current goal is Luu
An exact proof term for the current goal is Lw
An exact proof term for the current goal is Luupos
rewrite the current goal using
add_SNo_0R (w * u * u (from right to left) at position 1.
An exact proof term for the current goal is Lwuu
An
exact proof term for the current goal is
SNo_0 .
An exact proof term for the current goal is Lxxw
An exact proof term for the current goal is L2u
An
exact proof term for the current goal is
SNo_add_SNo ((2 * u * x * w x L2uxw Hx .
An
exact proof term for the current goal is
SNo_0 .
rewrite the current goal using
add_SNo_0L (from left to right).
rewrite the current goal using
add_SNo_com (x * x * w (2 * u Lxxw L2u (from left to right).
rewrite the current goal using
mul_SNo_oneR x Hx (from right to left) at position 1.
rewrite the current goal using
mul_SNo_oneR (2 * u L2u (from right to left) at position 2.
An exact proof term for the current goal is L2u
An
exact proof term for the current goal is
SNo_1 .
An exact proof term for the current goal is Hx
An exact proof term for the current goal is Lxw
An exact proof term for the current goal is H3
rewrite the current goal using
mul_SNo_com x w Hx Lw (from left to right).
An
exact proof term for the current goal is
SNo_1 .
An exact proof term for the current goal is Hx
An exact proof term for the current goal is Lw
An exact proof term for the current goal is Hxpos
We will
prove w < 1 :/: x .
rewrite the current goal using LrxLR
Apply HLR3
An exact proof term for the current goal is Hw
An exact proof term for the current goal is Lwuu
An
exact proof term for the current goal is
L7 w Lw (λu v ⇒ w < v ) L8a .
We prove the intermediate
claim L9 :
∀ z ∈ R , ∃ z' ∈ R , z' < z .
Let z be given.
Assume Hz .
We prove the intermediate
claim Lz :
SNo z .
An exact proof term for the current goal is LRreal z Hz
We prove the intermediate
claim Lxz :
SNo (x * z .
An
exact proof term for the current goal is
SNo_mul_SNo x z Hx Lz .
We prove the intermediate
claim Lxxz :
SNo (x * x * z .
An
exact proof term for the current goal is
SNo_mul_SNo x (x * z Hx Lxz .
We prove the intermediate
claim L2uxz :
SNo ((2 * u * x * z .
An
exact proof term for the current goal is
SNo_mul_SNo (2 * u (x * z L2u Lxz .
We prove the intermediate
claim Lzuu :
SNo (z * u * u .
An
exact proof term for the current goal is
SNo_mul_SNo z (u * u Lz Luu .
We use f (f z witness the existential quantifier.
Apply andI to the current goal.
Apply L5
Apply L6
An exact proof term for the current goal is Hz
We will
prove f (f z < z .
We prove the intermediate
claim L9a :
(z * u * u + x * x * z + 2 * u + - ((2 * u * x * z + x :/: (u * u < z .
An exact proof term for the current goal is Luu
An exact proof term for the current goal is Lz
An exact proof term for the current goal is Luupos
rewrite the current goal using
add_SNo_0R (z * u * u (from right to left) at position 2.
An exact proof term for the current goal is Lzuu
An
exact proof term for the current goal is
SNo_0 .
An exact proof term for the current goal is Lxxz
An exact proof term for the current goal is L2u
An
exact proof term for the current goal is
SNo_add_SNo ((2 * u * x * z x L2uxz Hx .
An
exact proof term for the current goal is
SNo_0 .
rewrite the current goal using
add_SNo_0L (from left to right).
rewrite the current goal using
mul_SNo_oneR x Hx (from right to left) at position 4.
rewrite the current goal using
mul_SNo_oneR (2 * u L2u (from right to left) at position 1.
An exact proof term for the current goal is L2u
An exact proof term for the current goal is Lxz
An exact proof term for the current goal is Hx
An
exact proof term for the current goal is
SNo_1 .
An exact proof term for the current goal is H3
rewrite the current goal using
mul_SNo_com x z Hx Lz (from left to right).
An
exact proof term for the current goal is
SNo_1 .
An exact proof term for the current goal is Hx
An exact proof term for the current goal is Lz
An exact proof term for the current goal is Hxpos
We will
prove 1 :/: x < z .
rewrite the current goal using LrxLR
Apply HLR4
An exact proof term for the current goal is Hz
An exact proof term for the current goal is Lzuu
An
exact proof term for the current goal is
L7 z Lz (λu v ⇒ v < z ) L9a .
An exact proof term for the current goal is LLreal
An exact proof term for the current goal is LRreal
An exact proof term for the current goal is LLR
An exact proof term for the current goal is LL0
rewrite the current goal using H4
Apply L5 0 to the current goal.
rewrite the current goal using
tuple_2_0_eq (from left to right).
Apply SingI to the current goal.
We will
prove ∀ w ∈ L , ∃ w' ∈ L , w < w' .
An exact proof term for the current goal is L8
We will
prove ∀ z ∈ R , ∃ z' ∈ R , z' < z .
An exact proof term for the current goal is L9
An exact proof term for the current goal is L2
∎
Proof: Let x be given.
Assume Hx Hxpos .
Assume H _ .
An exact proof term for the current goal is H
∎
Proof: Let x be given.
Assume Hx .
We prove the intermediate
claim Lx :
SNo x .
An
exact proof term for the current goal is
real_SNo x Hx .
rewrite the current goal using
minus_SNo_0 (from left to right).
An exact proof term for the current goal is H1
rewrite the current goal using H1
rewrite the current goal using
recip_SNo_0 (from left to right).
An
exact proof term for the current goal is
real_0 .
∎
Proof: Let x be given.
Assume Hx .
Let y be given.
Assume Hy .
An exact proof term for the current goal is Hx
An exact proof term for the current goal is Hy
∎
Proof: Let x be given.
Assume Hx Hxnn H1 .
rewrite the current goal using
tuple_2_0_eq (from left to right).
Apply ReplI to the current goal.
Apply SepI to the current goal.
rewrite the current goal using
SNoLev_0 (from left to right).
An exact proof term for the current goal is H1
An exact proof term for the current goal is H3
Apply EmptyE 0 to the current goal.
rewrite the current goal using
SNoLev_0 (from right to left) at position 2.
rewrite the current goal using H3
An exact proof term for the current goal is H1
∎
Proof: Let x be given.
Assume Hx Hxnn H1 .
Set L to be the term
⋃ k ∈ ω L_ k .
Set R to be the term
⋃ k ∈ ω R_ k .
rewrite the current goal using H2
∎
Proof: Let x be given.
Assume Hx Hxnn H1 .
Set L to be the term
⋃ k ∈ ω L_ k .
Set R to be the term
⋃ k ∈ ω R_ k .
We prove the intermediate
claim L1 :
1 ∈ SNoR x .
An exact proof term for the current goal is H1
An exact proof term for the current goal is H3
rewrite the current goal using
tuple_2_1_eq (from left to right).
Apply ReplI to the current goal.
An exact proof term for the current goal is L1
rewrite the current goal using H2
rewrite the current goal using H3
An exact proof term for the current goal is H1
Apply SepI to the current goal.
An exact proof term for the current goal is H1
An exact proof term for the current goal is H3
An
exact proof term for the current goal is
SNoLt_0_1 .
We prove the intermediate
claim L4 :
(x + 1 * 0 :/: (1 + 0 ∈ R_ 1 .
rewrite the current goal using
tuple_2_1_eq (from left to right).
rewrite the current goal using
SNo_sqrtaux_0 (from left to right).
rewrite the current goal using
tuple_2_0_eq (from left to right).
Apply ReplI to the current goal.
An exact proof term for the current goal is L3
An
exact proof term for the current goal is
SNoLt_0_1 .
rewrite the current goal using H2
∎
Proof: Let Y, Z and x be given.
Assume HY HZ Hx .
Let w be given.
Assume Hw .
Let y be given.
Let z be given.
rewrite the current goal using Hw3
An exact proof term for the current goal is Hx
An exact proof term for the current goal is HY y Hy
An exact proof term for the current goal is HZ z Hz
An exact proof term for the current goal is HY y Hy
An exact proof term for the current goal is HZ z Hz
∎
Proof: Let Y, Z and x be given.
Assume HY HZ Hx Hxnneg .
We prove the intermediate
claim LY :
Y ⊆ real .
Let y be given.
Assume Hy .
An
exact proof term for the current goal is
SepE1 real (λw ⇒ 0 ≤ w ) y (HY y Hy .
We prove the intermediate
claim LZ :
Z ⊆ real .
Let z be given.
Assume Hz .
An
exact proof term for the current goal is
SepE1 real (λw ⇒ 0 ≤ w ) z (HZ z Hz .
We prove the intermediate
claim LxS :
SNo x .
An
exact proof term for the current goal is
real_SNo x Hx .
Let w be given.
Assume Hw .
Apply SepI to the current goal.
Let y be given.
Let z be given.
Apply SepE real (λw ⇒ 0 ≤ w ) y (HY y Hy to the current goal.
We prove the intermediate
claim LyS :
SNo y .
An
exact proof term for the current goal is
real_SNo y HyR .
Apply SepE real (λz ⇒ 0 ≤ z ) z (HZ z Hz to the current goal.
We prove the intermediate
claim LzS :
SNo z .
An
exact proof term for the current goal is
real_SNo z HzR .
rewrite the current goal using Hw3
We will
prove 0 ≤ (x + y * z :/: (y + z .
We prove the intermediate
claim L1 :
0 ≤ x + y * z .
An exact proof term for the current goal is Hxnneg
An
exact proof term for the current goal is
mul_SNo_pos_pos y z LyS LzS H1 H2 .
rewrite the current goal using H2
rewrite the current goal using
mul_SNo_zeroR y LyS (from left to right).
rewrite the current goal using H1
rewrite the current goal using
mul_SNo_zeroL z LzS (from left to right).
We will
prove 0 ≤ (x + y * z :/: (y + z .
We will
prove 0 < (x + y * z :/: (y + z .
rewrite the current goal using H1
∎
Proof:
Let x be given.
We prove the intermediate
claim Lx :
x ∈ real .
An
exact proof term for the current goal is
SNoLev_ x Hx .
Set L to be the term
⋃ k ∈ ω L_ k .
Set R to be the term
⋃ k ∈ ω R_ k .
We prove the intermediate
claim L_L_R_real :
∀k, nat_p k L_ k ⊆ real ∧ R_ k ⊆ real .
rewrite the current goal using
SNo_sqrtaux_0 (from left to right).
rewrite the current goal using
tuple_2_0_eq (from left to right).
rewrite the current goal using
tuple_2_1_eq (from left to right).
Apply andI to the current goal.
Let w' be given.
Assume Hw' .
Let w be given.
rewrite the current goal using Hw'w
Apply SepE (SNoL x (λw ⇒ 0 ≤ w ) w Hw to the current goal.
Apply SNoL_E x Hx w Hw1 to the current goal.
Assume Hw1a Hw1b Hw1c .
Apply IH
An
exact proof term for the current goal is
SNoS_I2 w x Hw1a Hx Hw1b .
An exact proof term for the current goal is Hwnneg
Let z' be given.
Assume Hz' .
Let z be given.
rewrite the current goal using Hz'z
Apply SNoR_E x Hx z Hz to the current goal.
Assume Hz1 Hz2 Hz3 .
Apply IH
An
exact proof term for the current goal is
SNoS_I2 z x Hz1 Hx Hz2 .
An exact proof term for the current goal is Hz3
Let k be given.
Assume Hk .
Assume IHk .
Apply IHk
rewrite the current goal using
tuple_2_0_eq (from left to right).
rewrite the current goal using
tuple_2_1_eq (from left to right).
Apply andI to the current goal.
An exact proof term for the current goal is IHk0
An exact proof term for the current goal is IHk0
An exact proof term for the current goal is IHk1
An exact proof term for the current goal is Lx
An exact proof term for the current goal is IHk1
An exact proof term for the current goal is IHk0
An exact proof term for the current goal is IHk0
An exact proof term for the current goal is Lx
An exact proof term for the current goal is IHk1
An exact proof term for the current goal is IHk1
An exact proof term for the current goal is Lx
We prove the intermediate
claim L1L :
∀ w ∈ L , ∀p : prop , (SNo w 0 ≤ w w * w < x p → p .
Let w be given.
Assume Hw .
Let p be given.
Assume Hp .
Let k be given.
Assume H2 .
Apply H2
An exact proof term for the current goal is Hp
We prove the intermediate
claim L1R :
∀ z ∈ R , ∀p : prop , (SNo z 0 ≤ z x < z * z p → p .
Let z be given.
Assume Hz .
Let p be given.
Assume Hp .
Let k be given.
Assume H3 .
Apply H3
An exact proof term for the current goal is Hp
We prove the intermediate
claim LLR :
SNoCutP L R .
Apply LLR
Assume HLHR .
Apply HLHR
Let w be given.
Let k be given.
Apply L_L_R_real k (omega_nat_p k Hk to the current goal.
Assume H2 _ .
An exact proof term for the current goal is H2 w H1
Let z be given.
Let k be given.
Apply L_L_R_real k (omega_nat_p k Hk to the current goal.
Assume _ H2 .
An exact proof term for the current goal is H2 z H1
An exact proof term for the current goal is LLR
We will
prove ∀ w ∈ L , ∃ w' ∈ L , w < w' .
Let w be given.
Assume Hw .
Let k be given.
Apply L1L w Hw
We prove the intermediate
claim Lwmw :
SNo (w * w .
An
exact proof term for the current goal is
SNo_mul_SNo w w Hw1 Hw1 .
We prove the intermediate
claim Lwpw :
SNo (w + w .
An
exact proof term for the current goal is
SNo_add_SNo w w Hw1 Hw1 .
We prove the intermediate
claim L1a :
∃ z, z ∈ R_ (ordsucc k .
We use
1 to
witness the existential quantifier.
Assume _ .
Apply H5
rewrite the current goal using
SNo_sqrtaux_0 (from left to right).
rewrite the current goal using
tuple_2_1_eq (from left to right).
Apply ReplI to the current goal.
Apply SepI to the current goal.
An exact proof term for the current goal is H2
An exact proof term for the current goal is H4
rewrite the current goal using H4
An exact proof term for the current goal is H2
We prove the intermediate
claim L1a1 :
1 ∈ L_ k .
Assume _ .
Apply H5
rewrite the current goal using
SNo_sqrtaux_0 (from left to right).
rewrite the current goal using
tuple_2_0_eq (from left to right).
Apply ReplI to the current goal.
Apply SepI to the current goal.
Apply SepI to the current goal.
An exact proof term for the current goal is H2
An exact proof term for the current goal is H4
An
exact proof term for the current goal is
SNoLt_0_1 .
We prove the intermediate
claim L1a2 :
0 < 1 + 1 .
rewrite the current goal using
add_SNo_1_1_2 (from left to right).
An
exact proof term for the current goal is
SNoLt_0_2 .
We use z witness the existential quantifier.
rewrite the current goal using
tuple_2_1_eq (from left to right).
An
exact proof term for the current goal is
SNo_sqrtauxset_I (L_ k (L_ k x 1 L1a1 1 L1a1 L1a2 .
Apply L1a
Let z be given.
We prove the intermediate
claim Lz :
z ∈ R .
Apply L1R z Lz
We prove the intermediate
claim Lwmz :
SNo (w * z .
An
exact proof term for the current goal is
SNo_mul_SNo w z Hw1 Hz1 .
We prove the intermediate
claim Lwpz :
SNo (w + z .
An
exact proof term for the current goal is
SNo_add_SNo w z Hw1 Hz1 .
We prove the intermediate
claim Lzpos :
0 < z .
An exact proof term for the current goal is H4
rewrite the current goal using H4
An exact proof term for the current goal is Hz3
We prove the intermediate
claim Lwpzpos :
0 < w + z .
rewrite the current goal using
add_SNo_0L z Hz1 (from right to left) at position 1.
We will
prove 0 + z ≤ w + z .
We prove the intermediate
claim Lwpzn0 :
w + z ≠ 0 .
rewrite the current goal using H4
An exact proof term for the current goal is Lwpzpos
Set w' to be the term
(x + w * z :/: (w + z .
rewrite the current goal using
tuple_2_0_eq (from left to right).
We prove the intermediate
claim LwLk :
w ∈ L_ (ordsucc k .
Assume _ .
Apply H5
An exact proof term for the current goal is H3
We use w' witness the existential quantifier.
Apply andI to the current goal.
rewrite the current goal using
div_mul_SNo_invL w (w + z Hw1 Lwpz Lwpzn0 (from right to left) at position 1.
We will
prove (w * (w + z :/: (w + z < w' .
We will
prove w * (w + z < x + w * z .
rewrite the current goal using
mul_SNo_distrL w w z Hw1 Hw1 Hz1 (from left to right).
We will
prove w * w + w * z < x + w * z .
Apply add_SNo_Lt1 (w * w (w * z x Lwmw Lwmz Hx to the current goal.
An exact proof term for the current goal is Hw3
We will
prove ∀ z ∈ R , ∃ z' ∈ R , z' < z .
Let z be given.
Assume Hz .
Let k be given.
Apply L1R z Hz
We prove the intermediate
claim Lzmz :
SNo (z * z .
An
exact proof term for the current goal is
SNo_mul_SNo z z Hz1 Hz1 .
We prove the intermediate
claim Lzpz :
SNo (z + z .
An
exact proof term for the current goal is
SNo_add_SNo z z Hz1 Hz1 .
We prove the intermediate
claim Lzpos :
0 < z .
An exact proof term for the current goal is H4
rewrite the current goal using H4
An exact proof term for the current goal is Hz3
We prove the intermediate
claim Lzpzpos :
0 < z + z .
We prove the intermediate
claim Lzpzn0 :
z + z ≠ 0 .
rewrite the current goal using H4
An exact proof term for the current goal is Lzpzpos
Set z' to be the term
(x + z * z :/: (z + z .
We prove the intermediate
claim Lz' :
z' ∈ R_ (ordsucc k .
rewrite the current goal using
tuple_2_1_eq (from left to right).
An exact proof term for the current goal is H3
An exact proof term for the current goal is H3
An exact proof term for the current goal is Lzpzpos
We use z' witness the existential quantifier.
Apply andI to the current goal.
rewrite the current goal using
div_mul_SNo_invL z (z + z Hz1 Lzpz Lzpzn0 (from right to left) at position 5.
We will
prove z' < (z * (z + z :/: (z + z .
We will
prove x + z * z < z * (z + z .
rewrite the current goal using
mul_SNo_distrL z z z Hz1 Hz1 Hz1 (from left to right).
We will
prove x + z * z < z * z + z * z .
Apply add_SNo_Lt1 x (z * z (z * z Hx Lzmz Lzmz to the current goal.
An exact proof term for the current goal is Hz3
We prove the intermediate
claim L1_1 :
x = 1 .
Use symmetry.
Let u be given.
Apply cases_1 u Hu to the current goal.
An exact proof term for the current goal is H1
An exact proof term for the current goal is H2
Let u be given.
We will
prove u ∈ 1 ↔ u ∈ x .
Apply iffI to the current goal.
Assume _ .
Apply cases_1 u Hu to the current goal.
Apply dneg to the current goal.
rewrite the current goal using
SNoLev_0 (from left to right).
An exact proof term for the current goal is H1
rewrite the current goal using
SNoLev_0 (from left to right).
Let u be given.
An
exact proof term for the current goal is
EmptyE u Hu .
rewrite the current goal using
SNoLev_0 (from left to right).
An exact proof term for the current goal is H3
Assume _ .
An exact proof term for the current goal is Hu
rewrite the current goal using L1_1
An
exact proof term for the current goal is
real_1 .
We prove the intermediate
claim L1_0 :
x = 0 .
An exact proof term for the current goal is H1
rewrite the current goal using L1_0
An
exact proof term for the current goal is
real_0 .
Let x be given.
Assume Hx .
An exact proof term for the current goal is L1 x Hx3 Hx1
∎
Proof: Let x be given.
Assume Hx Hxnn .
Apply real_E x Hx to the current goal.
Assume H .
Apply H
An exact proof term for the current goal is Hx1
An exact proof term for the current goal is Hxnn
Set L to be the term
⋃ k ∈ ω L_ k .
Set R to be the term
⋃ k ∈ ω R_ k .
Let k be given.
Assume Hk .
Let w be given.
Assume Hw .
Let k be given.
Assume Hk .
Let z be given.
Assume Hz .
Let w be given.
Let p be given.
Assume Hp .
Let k be given.
An exact proof term for the current goal is Hp k Hk Hwk
Let z be given.
Let p be given.
Assume Hp .
Let k be given.
An exact proof term for the current goal is Hp k Hk Hzk
We prove the intermediate
claim L_L_Subq :
∀k, nat_p k L_ k ⊆ L_ (ordsucc k .
Let k be given.
Assume Hk .
Let w be given.
rewrite the current goal using
tuple_2_0_eq (from left to right).
An exact proof term for the current goal is Hw
We prove the intermediate
claim L_R_Subq :
∀k, nat_p k R_ k ⊆ R_ (ordsucc k .
Let k be given.
Assume Hk .
Let w be given.
rewrite the current goal using
tuple_2_1_eq (from left to right).
An exact proof term for the current goal is Hw
We prove the intermediate
claim L_L_R_Subq :
∀k, nat_p k ∀ k' ∈ k , L_ k' ⊆ L_ k ∧ R_ k' ⊆ R_ k .
Let k' be given.
An
exact proof term for the current goal is
EmptyE k' Hk' .
Let k be given.
Assume Hk .
Let k' be given.
Apply ordsuccE k k' Hk' to the current goal.
Apply IHk k' Hk'2
Assume IHkL IHkR .
Apply andI to the current goal.
An exact proof term for the current goal is L_L_Subq k Hk
An exact proof term for the current goal is L_R_Subq k Hk
rewrite the current goal using Hk'2
Apply andI to the current goal.
An exact proof term for the current goal is L_L_Subq k Hk
An exact proof term for the current goal is L_R_Subq k Hk
rewrite the current goal using
SNo_sqrtaux_0 (from left to right).
rewrite the current goal using
tuple_2_0_eq (from left to right).
rewrite the current goal using
tuple_2_1_eq (from left to right).
Apply andI to the current goal.
Let w' be given.
Assume Hw' .
Let w be given.
rewrite the current goal using Hw'w
Apply SepE (SNoL x (λw ⇒ 0 ≤ w ) w Hw to the current goal.
Apply SNoL_E x Hx1 w Hw1 to the current goal.
Assume Hw1a Hw1b Hw1c .
Apply SepI to the current goal.
rewrite the current goal using H4
An exact proof term for the current goal is Hw1b
An exact proof term for the current goal is Hw1a
An exact proof term for the current goal is Hwnneg
Let z' be given.
Assume Hz' .
Let z be given.
rewrite the current goal using Hz'z
Apply SNoR_E x Hx1 z Hz to the current goal.
Assume Hz1 Hz2 Hz3 .
Apply SepI to the current goal.
rewrite the current goal using H4
An exact proof term for the current goal is Hz2
An exact proof term for the current goal is Hz1
An
exact proof term for the current goal is
SNoLeLt_tra 0 x z SNo_0 Hx1 Hz1 Hxnn Hz3 .
An
exact proof term for the current goal is
SNoLeLt_tra 0 x z SNo_0 Hx1 Hz1 Hxnn Hz3 .
Let k be given.
Assume Hk .
Assume IHk .
Apply IHk
rewrite the current goal using
tuple_2_0_eq (from left to right).
rewrite the current goal using
tuple_2_1_eq (from left to right).
Apply andI to the current goal.
An exact proof term for the current goal is IHk0
An exact proof term for the current goal is IHk0
An exact proof term for the current goal is IHk1
An exact proof term for the current goal is Hx
An exact proof term for the current goal is Hxnn
An exact proof term for the current goal is IHk1
An exact proof term for the current goal is IHk0
An exact proof term for the current goal is IHk0
An exact proof term for the current goal is Hx
An exact proof term for the current goal is Hxnn
An exact proof term for the current goal is IHk1
An exact proof term for the current goal is IHk1
An exact proof term for the current goal is Hx
An exact proof term for the current goal is Hxnn
We prove the intermediate
claim LLsR :
L ⊆ real .
Let w be given.
Assume Hw .
Apply LLE w Hw
Let k be given.
Apply L_L_R_real k (omega_nat_p k Hk to the current goal.
Assume H _ .
An
exact proof term for the current goal is
SepE1 real (λw ⇒ 0 ≤ w ) w (H w Hwk .
We prove the intermediate
claim LRsR :
R ⊆ real .
Let z be given.
Assume Hz .
Apply LRE z Hz
Let k be given.
Apply L_L_R_real k (omega_nat_p k Hk to the current goal.
Assume _ H .
An
exact proof term for the current goal is
SepE1 real (λw ⇒ 0 ≤ w ) z (H z Hzk .
We prove the intermediate
claim LLR :
SNoCutP L R .
Assume HLR1 HLR2 .
Assume HLR5 .
We prove the intermediate
claim L0Lx :
0 ∈ SNoLev x .
rewrite the current goal using H4
We prove the intermediate
claim L1Lx :
1 ∈ SNoLev x .
rewrite the current goal using H4
We prove the intermediate
claim LLne :
L ≠ 0 .
We prove the intermediate
claim LRne :
R ≠ 0 .
We prove the intermediate
claim LRE' :
∀ z ∈ R , SNo z ∧ 0 < z .
Let z be given.
Assume Hz .
We prove the intermediate
claim LzS :
SNo z .
An
exact proof term for the current goal is
real_SNo z (LRsR z Hz .
Apply andI to the current goal.
An exact proof term for the current goal is LzS
An exact proof term for the current goal is H2
An exact proof term for the current goal is HLR4 z Hz
We prove the intermediate
claim LLnomax :
∀ w ∈ L , ∃ w' ∈ L , w < w' .
Let w be given.
Assume Hw .
Apply LLE w Hw
Let k be given.
Assume Hk .
Apply L_L_R_real k (omega_nat_p k Hk to the current goal.
Assume H _ .
Apply SepE real (λw ⇒ 0 ≤ w ) w (H w Hwk to the current goal.
We prove the intermediate
claim Lw :
SNo w .
An
exact proof term for the current goal is
real_SNo w HwR .
Apply xm (∃ z, z ∈ R to the current goal.
Assume H5 .
Apply H5
Let z be given.
Apply LRE z Hz
Let k' be given.
Assume Hk' .
Apply LRE' z Hz
Apply L_L_R_real k' (omega_nat_p k' Hk' to the current goal.
Assume _ H .
We prove the intermediate
claim LzR :
z ∈ real .
An
exact proof term for the current goal is
SepE1 real (λw ⇒ 0 ≤ w ) z (H z Hzk' .
We prove the intermediate
claim Lz :
SNo z .
An
exact proof term for the current goal is
real_SNo z LzR .
We prove the intermediate
claim Lzpos :
0 < z .
An exact proof term for the current goal is H2
An exact proof term for the current goal is HLR4 z Hz
We prove the intermediate
claim Lwz :
SNo (w + z .
An
exact proof term for the current goal is
SNo_add_SNo w z Lw Lz .
We prove the intermediate
claim Lwmz :
SNo (w * z .
An
exact proof term for the current goal is
SNo_mul_SNo w z Lw Lz .
We prove the intermediate
claim Lwzpos :
0 < w + z .
An exact proof term for the current goal is Lzpos
Set w' to be the term
(x + w * z :/: (w + z .
We use w' witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate
claim Lwzk'' :
∃ k'' ∈ ω , w ∈ L_ k'' ∧ z ∈ R_ k'' .
We use k' witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk'
Apply andI to the current goal.
Apply L_L_R_Subq k' (omega_nat_p k' Hk' k H6 to the current goal.
Assume H _ .
An exact proof term for the current goal is H w Hwk
An exact proof term for the current goal is Hzk'
We use k witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk
Apply andI to the current goal.
An exact proof term for the current goal is Hwk
rewrite the current goal using H6
An exact proof term for the current goal is Hzk'
We use k witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk
Apply andI to the current goal.
An exact proof term for the current goal is Hwk
Apply L_L_R_Subq k (omega_nat_p k Hk k' H6 to the current goal.
Assume _ H .
An exact proof term for the current goal is H z Hzk'
Apply Lwzk''
Let k'' be given.
Assume H .
Apply H
Assume H .
Apply H
We prove the intermediate
claim Lw'LSk'' :
w' ∈ L_ (ordsucc k'' .
rewrite the current goal using
tuple_2_0_eq (from left to right).
An exact proof term for the current goal is Hwk''
An exact proof term for the current goal is Hzk''
An exact proof term for the current goal is Lwzpos
We will
prove w < (x + w * z :/: (w + z .
We will
prove w * (w + z < x + w * z .
rewrite the current goal using
mul_SNo_distrL w w z Lw Lw HzS (from left to right).
We will
prove w * w + w * z < x + w * z .
rewrite the current goal using H3
An exact proof term for the current goal is HLR3 w Hw
rewrite the current goal using H6
rewrite the current goal using H6
An exact proof term for the current goal is Lwsx
Apply LRne
Let z be given.
Assume Hz .
Apply H5
We use z witness the existential quantifier.
An exact proof term for the current goal is Hz
We prove the intermediate
claim LRnomin :
∀ z ∈ R , ∃ z' ∈ R , z' < z .
Let z be given.
Assume Hz .
Apply LRE z Hz
Let k be given.
Assume Hk .
Apply LRE' z Hz
We prove the intermediate
claim Lzz :
SNo (z + z .
An
exact proof term for the current goal is
SNo_add_SNo z z HzS HzS .
We prove the intermediate
claim Lzzpos :
0 < z + z .
We will
prove 0 + 0 < z + z .
We prove the intermediate
claim Lzzn0 :
z + z ≠ 0 .
Assume H5 .
rewrite the current goal using H5
An exact proof term for the current goal is Lzzpos
We prove the intermediate
claim Lzmz :
SNo (z * z .
An
exact proof term for the current goal is
SNo_mul_SNo z z HzS HzS .
Set z' to be the term
(x + z * z :/: (z + z .
We prove the intermediate
claim Lz' :
z' ∈ R_ (ordsucc k .
rewrite the current goal using
tuple_2_1_eq (from left to right).
An exact proof term for the current goal is Hzk
An exact proof term for the current goal is Hzk
An exact proof term for the current goal is Lzzpos
We prove the intermediate
claim Lz'R :
z' ∈ R .
We prove the intermediate
claim Lz'S :
SNo z' .
An
exact proof term for the current goal is
real_SNo z' (LRsR z' Lz'R .
We use z' witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Lz'R
We will
prove (x + z * z :/: (z + z < z .
We will
prove x + z * z < z * (z + z .
rewrite the current goal using
mul_SNo_distrL z z z HzS HzS HzS (from left to right).
We will
prove x + z * z < z * z + z * z .
Apply add_SNo_Lt1 x (z * z (z * z Hx1 Lzmz Lzmz to the current goal.
rewrite the current goal using H3
rewrite the current goal using Hsx0
An
exact proof term for the current goal is
mul_SNo_pos_pos z z HzS HzS Hzpos Hzpos .
An
exact proof term for the current goal is
real_SNoCut L LLsR R LRsR LLR LLne LRne LLnomax LRnomin .
∎
Proof: Let x be given.
Assume Hx .
Let y be given.
Assume Hy .
Assume Hxpos Hynneg .
Apply real_E x Hx to the current goal.
Assume Hx1 Hx2 Hx3 Hx4 Hx5 .
Assume Hx7 .
We prove the intermediate
claim L1 :
∃ n ∈ ω , eps_ n ≤ x .
Apply dneg to the current goal.
We prove the intermediate
claim L1a :
0 = x .
Let k be given.
rewrite the current goal using
abs_SNo_minus x Hx1 (from left to right).
rewrite the current goal using
pos_abs_SNo x Hxpos (from left to right).
We will
prove x < eps_ k .
Assume H1 .
An exact proof term for the current goal is H1
Apply HC
We use k witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk
An exact proof term for the current goal is H1
rewrite the current goal using L1a
An exact proof term for the current goal is Hxpos
Apply L1
Let n be given.
Assume Hn .
Apply Hn
We prove the intermediate
claim L2n :
nat_p (2 ^ n .
An
exact proof term for the current goal is
nat_2 .
An
exact proof term for the current goal is
omega_nat_p n Hn1 .
We prove the intermediate
claim L2nb :
SNo (2 ^ n .
We prove the intermediate
claim L2nc :
0 ≤ 2 ^ n .
An exact proof term for the current goal is L2n
An
exact proof term for the current goal is
SNo_0 .
rewrite the current goal using
SNoLev_0 (from left to right).
An exact proof term for the current goal is L2n
We prove the intermediate
claim L2 :
1 ≤ 2 ^ n * x .
We will
prove eps_ n ≤ x .
An exact proof term for the current goal is Hn2
Apply real_E y Hy to the current goal.
Assume Hy1 Hy2 .
Assume Hy4 .
Assume Hy6 Hy7 .
Let N be given.
Assume HN .
Apply HN
We use
(N * 2 ^ n to
witness the existential quantifier.
Apply andI to the current goal.
We will
prove N * 2 ^ n ∈ ω .
We will
prove N * 2 ^ n ∈ ω .
An
exact proof term for the current goal is
omega_nat_p N HN1 .
An exact proof term for the current goal is L2n
We will
prove y ≤ (N * 2 ^ n * x .
We prove the intermediate
claim LN1 :
SNo N .
An
exact proof term for the current goal is
omega_SNo N HN1 .
We prove the intermediate
claim LN2n :
SNo (N * 2 ^ n .
An exact proof term for the current goal is LN1
An exact proof term for the current goal is L2nb
An exact proof term for the current goal is HN2
We will
prove N ≤ (N * 2 ^ n * x .
rewrite the current goal using
mul_SNo_oneR N LN1 (from right to left) at position 1.
We will
prove N * 1 ≤ (N * 2 ^ n * x .
rewrite the current goal using
mul_SNo_assoc N (2 ^ n x LN1 L2nb Hx1 (from right to left).
We will
prove N * 1 ≤ N * (2 ^ n * x .
We prove the intermediate
claim LN2 :
0 ≤ N .
An
exact proof term for the current goal is
omega_nat_p N HN1 .
An
exact proof term for the current goal is
SNo_0 .
rewrite the current goal using
SNoLev_0 (from left to right).
An
exact proof term for the current goal is
omega_nat_p N HN1 .
We will
prove SNo (2 ^ n * x .
An
exact proof term for the current goal is
SNo_mul_SNo (2 ^ n x L2nb Hx1 .
We will
prove 1 ≤ 2 ^ n * x .
An exact proof term for the current goal is L2
∎
Proof: Let a be given.
Assume Ha .
Let b be given.
Assume Hb H1 .
Apply dneg to the current goal.
We prove the intermediate
claim La1 :
∀ n ∈ ω , SNo (a n .
Let n be given.
Assume Hn .
Assume H _ _ _ _ _ _ .
An exact proof term for the current goal is H
We prove the intermediate
claim Lb1 :
∀ n ∈ ω , SNo (b n .
Let n be given.
Assume Hn .
Assume H _ _ _ _ _ _ .
An exact proof term for the current goal is H
We prove the intermediate
claim La2 :
∀n, nat_p n ∀ m ∈ n , a m ≤ a n .
Let m be given.
An
exact proof term for the current goal is
EmptyE m Hm .
Let n be given.
Assume Hn .
Let m be given.
We prove the intermediate
claim Ln :
n ∈ ω .
An
exact proof term for the current goal is
nat_p_omega n Hn .
We prove the intermediate
claim LSn :
ordsucc n ∈ ω .
We prove the intermediate
claim Lm :
m ∈ ω .
We prove the intermediate
claim LanSn :
a n ≤ a (ordsucc n .
Apply H1 n Ln
Assume H _ .
Apply H
Assume _ H .
An exact proof term for the current goal is H
Apply ordsuccE n m Hm to the current goal.
An exact proof term for the current goal is IHn m H2
An exact proof term for the current goal is LanSn
rewrite the current goal using H2
An exact proof term for the current goal is LanSn
We prove the intermediate
claim Lb2 :
∀n, nat_p n ∀ m ∈ n , b n ≤ b m .
Let m be given.
An
exact proof term for the current goal is
EmptyE m Hm .
Let n be given.
Assume Hn .
Let m be given.
We prove the intermediate
claim Ln :
n ∈ ω .
An
exact proof term for the current goal is
nat_p_omega n Hn .
We prove the intermediate
claim LSn :
ordsucc n ∈ ω .
We prove the intermediate
claim Lm :
m ∈ ω .
We prove the intermediate
claim LbSnn :
b (ordsucc n ≤ b n .
Apply H1 n Ln
Assume _ H .
An exact proof term for the current goal is H
Apply ordsuccE n m Hm to the current goal.
An exact proof term for the current goal is LbSnn
An exact proof term for the current goal is IHn m H2
rewrite the current goal using H2
An exact proof term for the current goal is LbSnn
We prove the intermediate
claim Lab :
∀ n m ∈ ω , a n ≤ b m .
Let n be given.
Assume Hn .
Let m be given.
Assume Hm .
We prove the intermediate
claim Ln :
nat_p n .
An
exact proof term for the current goal is
omega_nat_p n Hn .
We prove the intermediate
claim Lm :
nat_p m .
An
exact proof term for the current goal is
omega_nat_p m Hm .
We prove the intermediate
claim Labn :
a n ≤ b n .
Apply H1 n Hn
Assume H _ .
Apply H
Assume H _ .
An exact proof term for the current goal is H
Apply SNoLe_tra (a n (a m (b m (La1 n Hn (La1 m Hm (Lb1 m Hm to the current goal.
An exact proof term for the current goal is La2 m Lm n H2
Apply H1 m Hm
Assume H _ .
Apply H
Assume H _ .
An exact proof term for the current goal is H
rewrite the current goal using H2
An exact proof term for the current goal is Labn
Apply SNoLe_tra (a n (b n (b m (La1 n Hn (Lb1 n Hn (Lb1 m Hm to the current goal.
An exact proof term for the current goal is Labn
An exact proof term for the current goal is Lb2 n Ln m H2
Set x to be the term
SNoCut L R .
We prove the intermediate
claim LL :
L ⊆ SNoS_ ω .
We prove the intermediate
claim LR :
R ⊆ SNoS_ ω .
We prove the intermediate
claim LLR :
SNoCutP L R .
Apply and3I to the current goal.
Let w be given.
Assume H3 .
Apply H3
Let n be given.
Assume H3 .
Apply H3
Assume Hw1 Hw2 Hw3 Hw4 .
An exact proof term for the current goal is Hw3
Let z be given.
Assume H3 .
Apply H3
Let m be given.
Assume H3 .
Apply H3
Assume Hz1 Hz2 Hz3 Hz4 .
An exact proof term for the current goal is Hz3
Let w be given.
Let z be given.
Assume H3 .
Apply H3
Let n be given.
Assume H3 .
Apply H3
Assume Hw1 Hw2 Hw3 Hw4 .
Assume H5 .
Apply H5
Let m be given.
Assume H5 .
Apply H5
Assume Hz1 Hz2 Hz3 Hz4 .
Apply SNoLt_tra w (a n z Hw3 (La1 n Hn Hz3 H3 to the current goal.
Apply SNoLeLt_tra (a n (b m z (La1 n Hn (Lb1 m Hm Hz3 to the current goal.
An exact proof term for the current goal is Lab n Hn m Hm
An exact proof term for the current goal is H5
We prove the intermediate
claim Lax :
∀ n ∈ ω , a n ≤ x .
Let n be given.
Assume Hn .
Let f be given.
Assume Hf .
Let g be given.
Assume Hg Hf1 Hf2 Hf3 Hg1 Hg2 Hg3 Hfg Hanfg .
rewrite the current goal using Hanfg
An exact proof term for the current goal is Hfg
An exact proof term for the current goal is LLR
Let w be given.
Let m be given.
rewrite the current goal using Hwm
Apply HLR3
Apply SepI to the current goal.
An
exact proof term for the current goal is
ap_Pi ω (λ_ ⇒ SNoS_ ω ) f m Hf Hm .
We will
prove ∃ n ∈ ω , f m < a n .
We use n witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn
An exact proof term for the current goal is Hf1 m Hm
Let z be given.
rewrite the current goal using Hanfg
Assume H3 .
Apply H3
Let m be given.
Assume H3 .
Apply H3
Assume Hz1 Hz2 Hz3 Hz4 .
Apply SNoLeLt_tra (a n (b m z (La1 n Hn (Lb1 m Hm Hz3 to the current goal.
An exact proof term for the current goal is Lab n Hn m Hm
An exact proof term for the current goal is H3
We prove the intermediate
claim Lxb :
∀ n ∈ ω , x ≤ b n .
Let n be given.
Assume Hn .
Let f be given.
Assume Hf .
Let g be given.
Assume Hg Hf1 Hf2 Hf3 Hg1 Hg2 Hg3 Hfg Hbnfg .
rewrite the current goal using Hbnfg
An exact proof term for the current goal is LLR
An exact proof term for the current goal is Hfg
Let w be given.
rewrite the current goal using Hbnfg
Assume H3 .
Apply H3
Let m be given.
Assume H3 .
Apply H3
Assume Hw1 Hw2 Hw3 Hw4 .
Apply SNoLtLe_tra w (a m (b n Hw3 (La1 m Hm (Lb1 n Hn to the current goal.
An exact proof term for the current goal is H3
An exact proof term for the current goal is Lab m Hm n Hn
Let z be given.
Let m be given.
rewrite the current goal using Hzm
Apply HLR4
Apply SepI to the current goal.
An
exact proof term for the current goal is
ap_Pi ω (λ_ ⇒ SNoS_ ω ) g m Hg Hm .
We will
prove ∃ n ∈ ω , b n < g m .
We use n witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn
An exact proof term for the current goal is Hg2 m Hm
We prove the intermediate
claim Laxb :
∀ n ∈ ω , a n ≤ x ∧ x ≤ b n .
Let n be given.
Assume Hn .
Apply andI to the current goal.
An exact proof term for the current goal is Lax n Hn
An exact proof term for the current goal is Lxb n Hn
We prove the intermediate
claim L1 :
∀ q ∈ SNoS_ ω , q ∈ L ∨ q ∈ R .
Let q be given.
Assume Hq .
Apply dneg to the current goal.
Assume Hq1 Hq2 Hq3 Hq4 .
We prove the intermediate
claim L1a :
∀ w ∈ L , w < q .
Let w be given.
Assume H3 .
Apply H3
Let n be given.
Assume H3 .
Apply H3
Assume Hw1 Hw2 Hw3 Hw4 .
An exact proof term for the current goal is H4
Apply HCq
Apply orIL to the current goal.
Apply SepI to the current goal.
An exact proof term for the current goal is Hq
We will
prove ∃ n ∈ ω , q < a n .
We use n witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn
An
exact proof term for the current goal is
SNoLeLt_tra q w (a n Hq3 Hw3 (La1 n Hn H4 H3 .
We prove the intermediate
claim L1b :
∀ z ∈ R , q < z .
Let z be given.
Assume H3 .
Apply H3
Let n be given.
Assume H3 .
Apply H3
Assume Hz1 Hz2 Hz3 Hz4 .
An exact proof term for the current goal is H4
Apply HCq
Apply orIR to the current goal.
Apply SepI to the current goal.
An exact proof term for the current goal is Hq
We will
prove ∃ n ∈ ω , b n < q .
We use n witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn
An
exact proof term for the current goal is
SNoLtLe_tra (b n z q (Lb1 n Hn Hz3 Hq3 H3 H4 .
Apply HLR5 q Hq3 L1a L1b
Assume _ .
Apply HC
We use x witness the existential quantifier.
Apply andI to the current goal.
Assume H3 .
An exact proof term for the current goal is H3
Apply H2
Apply H3
An exact proof term for the current goal is HLR1
An exact proof term for the current goal is Laxb
Apply HC
We use x witness the existential quantifier.
Apply andI to the current goal.
Apply real_I to the current goal.
An exact proof term for the current goal is HLR1
We prove the intermediate
claim Lbd1 :
x ≤ b 0 .
Assume _ _ _ .
Assume _ _ .
Apply SNoLeLt_tra x (b 0 x HLR1 Hb0a HLR1 Lbd1 to the current goal.
rewrite the current goal using H2
An exact proof term for the current goal is Hb0b
We prove the intermediate
claim Lbd2 :
a 0 ≤ x .
Assume _ _ .
Assume _ _ _ .
Apply SNoLtLe_tra x (a 0 x HLR1 Ha0a HLR1 to the current goal.
rewrite the current goal using H2
An exact proof term for the current goal is Ha0b
An exact proof term for the current goal is Lbd2
Let q be given.
Assume Hq1a Hq1b Hq1c Hq1d .
Apply L1 q Hq1
Assume _ H3 .
Apply H3
Let n be given.
Assume H3 .
Apply H3
Assume _ _ _ _ _ .
Assume _ .
We prove the intermediate
claim L2 :
q = a n .
Apply H4 q Hq1
Let k be given.
We prove the intermediate
claim L2a :
0 < a n + - q .
An
exact proof term for the current goal is
SNoLt_minus_pos q (a n Hq1c (La1 n Hn H3 .
We prove the intermediate
claim L2b :
a n ≤ x .
An exact proof term for the current goal is Lax n Hn
We prove the intermediate
claim L2c :
0 < x + - q .
An
exact proof term for the current goal is
SNoLtLe_tra q (a n x Hq1c (La1 n Hn HLR1 H3 L2b .
rewrite the current goal using
abs_SNo_dist_swap q (a n Hq1c (La1 n Hn (from left to right).
rewrite the current goal using
pos_abs_SNo (a n + - q L2a (from left to right).
We will
prove a n + - q ≤ x + - q .
An exact proof term for the current goal is L2b
rewrite the current goal using
pos_abs_SNo (x + - q L2c (from right to left).
An exact proof term for the current goal is Hq2 k Hk
rewrite the current goal using L2
An exact proof term for the current goal is H3
Assume _ H3 .
Apply H3
Let n be given.
Assume H3 .
Apply H3
Assume _ _ _ _ _ .
Assume _ .
We prove the intermediate
claim L3 :
q = b n .
Apply H4 q Hq1
Let k be given.
We prove the intermediate
claim L3a :
0 < q + - b n .
An
exact proof term for the current goal is
SNoLt_minus_pos (b n q (Lb1 n Hn Hq1c H3 .
We prove the intermediate
claim L3b :
x ≤ b n .
An exact proof term for the current goal is Lxb n Hn
We prove the intermediate
claim L3c :
0 < q + - x .
An
exact proof term for the current goal is
SNoLeLt_tra x (b n q HLR1 (Lb1 n Hn Hq1c L3b H3 .
rewrite the current goal using
pos_abs_SNo (q + - b n L3a (from left to right).
We will
prove q + - b n ≤ q + - x .
We will
prove - b n ≤ - x .
rewrite the current goal using
pos_abs_SNo (q + - x L3c (from right to left).
An exact proof term for the current goal is Hq2 k Hk
rewrite the current goal using L3
An exact proof term for the current goal is H3
An exact proof term for the current goal is Laxb
∎
Proof: Let a be given.
Assume Ha .
Let b be given.
Assume Hb .
Assume H1 .
Let n be given.
Assume Hn .
We prove the intermediate
claim L1 :
ordsucc n = n + 1 .
rewrite the current goal using
add_nat_0R (from left to right).
Use reflexivity.
rewrite the current goal using L1
An exact proof term for the current goal is H1 n Hn
∎
End of Section Reals