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
exists 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
exists 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
Union is a term of type
set → set .
Axiom. (
UnionEq ) We take the following as an axiom:
Primitive . The name
Power is a term of type
set → set .
Axiom. (
PowerEq ) We take the following as an axiom:
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:
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 Union X ∈ U of type
set → prop .
Definition. We define
Power_closed to be
λU : set ⇒ ∀X : set , X ∈ U Power 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
/:e 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:
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 /:e Y z /:e 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 ∈ Union X Axiom. (
UnionE ) We take the following as an axiom:
Axiom. (
UnionE_impred ) We take the following as an axiom:
∀X x : set , x ∈ Union X ∀p : prop , (∀Y : set , x ∈ Y Y ∈ X p ) → p Axiom. (
PowerI ) We take the following as an axiom:
Axiom. (
PowerE ) We take the following as an axiom:
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 } exists 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 Axiom. (
Sing_inj ) We take the following as an axiom:
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:
Axiom. (
binunionE' ) We take the following as an axiom:
∀X Y z, ∀p : prop , (z ∈ X p → (z ∈ Y p → (z ∈ X :\/: Y p 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 exists 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
Primitive . The name
Sep is a term of type
set .
End of Section SepSec
Notation .
{x ∈ A | B } is notation for
Sep A (λ x . B ).
Axiom. (
SepI ) We take the following as an axiom:
∀X : set , ∀P : (set → prop , ∀x : set , x ∈ X P x x ∈ { x ∈ X | P x } Axiom. (
SepE ) We take the following as an axiom:
∀X : set , ∀P : (set → prop , ∀x : set , x ∈ { x ∈ X | P x } x ∈ X /\ P x Axiom. (
SepE1 ) We take the following as an axiom:
∀X : set , ∀P : (set → prop , ∀x : set , x ∈ { x ∈ X | P x } x ∈ X Axiom. (
SepE2 ) We take the following as an axiom:
∀X : set , ∀P : (set → prop , ∀x : set , x ∈ { x ∈ X | P x } P x Axiom. (
Sep_Empty ) We take the following as an axiom:
Axiom. (
Sep_Subq ) We take the following as an axiom:
∀X : set , ∀P : set → prop { x ∈ X | P x } ⊆ X 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 } exists 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 .
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 /:e Y → z ∈ X :\: Y Axiom. (
setminusE ) We take the following as an axiom:
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:
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:
Axiom. (
In_1_3 ) We take the following as an axiom:
Axiom. (
In_2_3 ) We take the following as an axiom:
Axiom. (
In_1_4 ) We take the following as an axiom:
Axiom. (
In_2_4 ) We take the following as an axiom:
Axiom. (
In_3_4 ) We take the following as an axiom:
Axiom. (
In_1_5 ) We take the following as an axiom:
Axiom. (
In_2_5 ) We take the following as an axiom:
Axiom. (
In_3_5 ) We take the following as an axiom:
Axiom. (
In_4_5 ) We take the following as an axiom:
Axiom. (
In_1_6 ) We take the following as an axiom:
Axiom. (
In_1_7 ) We take the following as an axiom:
Axiom. (
In_1_8 ) 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_3 ) We take the following as an axiom:
Axiom. (
nat_4 ) We take the following as an axiom:
Axiom. (
nat_5 ) We take the following as an axiom:
Axiom. (
nat_6 ) We take the following as an axiom:
Axiom. (
nat_7 ) We take the following as an axiom:
Axiom. (
nat_8 ) 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. (
neq_1_3 ) We take the following as an axiom:
Axiom. (
neq_2_3 ) We take the following as an axiom:
Axiom. (
neq_2_4 ) We take the following as an axiom:
Axiom. (
neq_3_4 ) We take the following as an axiom:
Axiom. (
ZF_closed_E ) We take the following as an axiom:
Primitive . The name
omega 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 , exists u ∈ X , f u = w of type
set → set → (set → set → prop .
Axiom. (
bijI ) We take the following as an axiom:
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 , exists 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 ⇒ exists 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
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 (exists 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 (exists 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 (exists 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 (exists 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 : exists 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 : exists 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 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
Definition. We define
In_rec_i_G to be
λX Y ⇒ ∀R : set → set → prop (∀X : set , ∀f : set → set (∀ x ∈ X , R x (f x → R X (F X f ) → R X Y of type
set → set → prop .
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
Definition. We define
In_rec_G_ii to be
λX Y ⇒ ∀R : set → (set → set → prop (∀X : set , ∀f : set → (set → set (∀ x ∈ X , R x (f x → R X (F X f ) → R X Y of type
set → (set → set → prop .
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
Definition. We define
In_rec_G_iii to be
λX Y ⇒ ∀R : set → (set → set → set → prop (∀X : set , ∀f : set → (set → set → set (∀ x ∈ X , R x (f x → R X (F X f ) → R X Y of type
set → (set → set → set → prop .
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
Axiom. (
nat_primrec_r ) We take the following as an axiom:
∀X : set , ∀g h : set → set (∀ x ∈ X , g x = h x → F X g = F X h End of Section NatRec
Beginning of Section NatArith
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_nat .
Axiom. (
add_nat_0R ) We take the following as an axiom:
Axiom. (
add_nat_SR ) We take the following as an axiom:
Axiom. (
add_nat_p ) We take the following as an axiom:
Axiom. (
add_nat_0L ) We take the following as an axiom:
Axiom. (
add_nat_SL ) We take the following as an axiom:
Axiom. (
add_nat_com ) We take the following as an axiom:
Definition. We define
mul_nat to be
λn m : set ⇒ nat_primrec 0 (λ_ r ⇒ n + r ) m of type
set → set → set .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_nat .
Axiom. (
mul_nat_0R ) We take the following as an axiom:
Axiom. (
mul_nat_SR ) We take the following as an axiom:
Axiom. (
mul_nat_p ) We take the following as an axiom:
End of Section NatArith
Axiom. (
Inj1_eq ) We take the following as an axiom:
Axiom. (
Inj1I1 ) We take the following as an axiom:
Axiom. (
Inj1I2 ) We take the following as an axiom:
Axiom. (
Inj1E ) We take the following as an axiom:
Axiom. (
Inj1NE1 ) We take the following as an axiom:
Axiom. (
Inj1NE2 ) We take the following as an axiom:
Definition. We define
Inj0 to be
λX ⇒ { Inj1 x | x ∈ X } of type
set → set .
Axiom. (
Inj0I ) We take the following as an axiom:
Axiom. (
Inj0E ) We take the following as an axiom:
Axiom. (
Unj_eq ) We take the following as an axiom:
Axiom. (
Unj_Inj1_eq ) We take the following as an axiom:
Axiom. (
Inj1_inj ) We take the following as an axiom:
Axiom. (
Unj_Inj0_eq ) We take the following as an axiom:
Axiom. (
Inj0_inj ) We take the following as an axiom:
Axiom. (
Inj0_0 ) We take the following as an axiom:
Notation . We use
:+: as an infix operator with priority 450 and which associates to the left corresponding to applying term
setsum .
Axiom. (
Inj0_setsum ) We take the following as an axiom:
Axiom. (
Inj1_setsum ) We take the following as an axiom:
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:
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
Sigma_ 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:
Axiom. (
proj0_Sigma ) We take the following as an axiom:
Axiom. (
proj1_Sigma ) We take the following as an axiom:
Axiom. (
pair_Sigma_E1 ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀x y : set , pair x y ∈ (Sigma_ x ∈ X , Y x y ∈ Y x Axiom. (
Sigma_E ) We take the following as an axiom:
Definition. We define
setprod to be
λX Y : set ⇒ Sigma_ 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 , exists 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:
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 ∈ (Sigma_ 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 ∈ (Sigma_ 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 ) Notation . We use
Pi_ 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:
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 ∈ (Pi_ x ∈ X , Y x Axiom. (
ap_Pi ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀f : set , ∀x : set , f ∈ (Pi_ x ∈ X , Y x x ∈ X f x ∈ Y x Definition. We define
setexp to be
λX Y : set ⇒ Pi_ 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
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 .
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 .
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. (
SNo_0_eq_0 ) 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
Notation . We use
:*: as an infix operator with priority 440 and which associates to the left corresponding to applying term
setprod .
Notation . We use
:^: as an infix operator with priority 430 and which associates to the left corresponding to applying term
setexp .
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 .
Primitive . The name
mul_SNo is a term 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_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 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:
Axiom. (
mul_SNoCutP_lem ) We take the following as an axiom:
∀Lx Rx Ly Ry x y, SNoCutP Lx Rx SNoCutP Ly Ry x = SNoCut Lx Rx y = SNoCut Ly Ry SNoCutP ({ w 0 * y + x * w 1 + - w 0 * w 1 | w ∈ Lx :*: Ly } :\/: { z 0 * y + x * z 1 + - z 0 * z 1 | z ∈ Rx :*: Ry } ({ w 0 * y + x * w 1 + - w 0 * w 1 | w ∈ Lx :*: Ry } :\/: { z 0 * y + x * z 1 + - z 0 * z 1 | z ∈ Rx :*: Ly } /\ x * y = SNoCut ({ w 0 * y + x * w 1 + - w 0 * w 1 | w ∈ Lx :*: Ly } :\/: { z 0 * y + x * z 1 + - z 0 * z 1 | z ∈ Rx :*: Ry } ({ w 0 * y + x * w 1 + - w 0 * w 1 | w ∈ Lx :*: Ry } :\/: { z 0 * y + x * z 1 + - z 0 * z 1 | z ∈ Rx :*: Ly } /\ ∀q : prop , (∀LxLy' RxRy' LxRy' RxLy', (∀ u ∈ LxLy' , ∀p : prop , (∀ w ∈ Lx , ∀ w' ∈ Ly , SNo w SNo w' w < x w' < y u = w * y + x * w' + - w * w' p → p → (∀ w ∈ Lx , ∀ w' ∈ Ly , w * y + x * w' + - w * w' ∈ LxLy' → (∀ u ∈ RxRy' , ∀p : prop , (∀ z ∈ Rx , ∀ z' ∈ Ry , SNo z SNo z' x < z y < z' u = z * y + x * z' + - z * z' p → p → (∀ z ∈ Rx , ∀ z' ∈ Ry , z * y + x * z' + - z * z' ∈ RxRy' → (∀ u ∈ LxRy' , ∀p : prop , (∀ w ∈ Lx , ∀ z ∈ Ry , SNo w SNo z w < x y < z u = w * y + x * z + - w * z p → p → (∀ w ∈ Lx , ∀ z ∈ Ry , w * y + x * z + - w * z ∈ LxRy' → (∀ u ∈ RxLy' , ∀p : prop , (∀ z ∈ Rx , ∀ w ∈ Ly , SNo z SNo w x < z w < y u = z * y + x * w + - z * w p → p → (∀ z ∈ Rx , ∀ w ∈ Ly , z * y + x * w + - z * w ∈ RxLy' → SNoCutP (LxLy' :\/: RxRy' (LxRy' :\/: RxLy' x * y = SNoCut (LxLy' :\/: RxRy' (LxRy' :\/: RxLy' q ) → q Axiom. (
mul_SNoCut_abs ) We take the following as an axiom:
∀Lx Rx Ly Ry x y, SNoCutP Lx Rx SNoCutP Ly Ry x = SNoCut Lx Rx y = SNoCut Ly Ry ∀q : prop , (∀LxLy' RxRy' LxRy' RxLy', (∀ u ∈ LxLy' , ∀p : prop , (∀ w ∈ Lx , ∀ w' ∈ Ly , SNo w SNo w' w < x w' < y u = w * y + x * w' + - w * w' p → p → (∀ w ∈ Lx , ∀ w' ∈ Ly , w * y + x * w' + - w * w' ∈ LxLy' → (∀ u ∈ RxRy' , ∀p : prop , (∀ z ∈ Rx , ∀ z' ∈ Ry , SNo z SNo z' x < z y < z' u = z * y + x * z' + - z * z' p → p → (∀ z ∈ Rx , ∀ z' ∈ Ry , z * y + x * z' + - z * z' ∈ RxRy' → (∀ u ∈ LxRy' , ∀p : prop , (∀ w ∈ Lx , ∀ z ∈ Ry , SNo w SNo z w < x y < z u = w * y + x * z + - w * z p → p → (∀ w ∈ Lx , ∀ z ∈ Ry , w * y + x * z + - w * z ∈ LxRy' → (∀ u ∈ RxLy' , ∀p : prop , (∀ z ∈ Rx , ∀ w ∈ Ly , SNo z SNo w x < z w < y u = z * y + x * w + - z * w p → p → (∀ z ∈ Rx , ∀ w ∈ Ly , z * y + x * w + - z * w ∈ RxLy' → SNoCutP (LxLy' :\/: RxRy' (LxRy' :\/: RxLy' x * y = SNoCut (LxLy' :\/: RxRy' (LxRy' :\/: RxLy' q ) → q 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 .
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 .
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 .
Axiom. (
real_I ) We take the following as an axiom:
Axiom. (
real_E ) We take the following as an axiom:
Axiom. (
real_SNo ) We take the following as an axiom:
Axiom. (
real_0 ) We take the following as an axiom:
Axiom. (
real_1 ) We take the following as an axiom:
Axiom. (
real_SNoCut ) We take the following as an axiom:
Axiom. (
SNo_approx_real_rep ) We take the following as an axiom:
∀ x ∈ real , ∀p : prop , (∀ f g ∈ SNoS_ omega :^: omega , (∀ n ∈ omega , f n < x → (∀ n ∈ omega , x < f n + eps_ n → (∀ n ∈ omega , ∀ i ∈ n , f i < f n → (∀ n ∈ omega , g n + - eps_ n < x → (∀ n ∈ omega , x < g n → (∀ n ∈ omega , ∀ i ∈ n , g n < g i → SNoCutP { f n | n ∈ omega } { g n | n ∈ omega } x = SNoCut { f n | n ∈ omega } { g n | n ∈ omega } p → p End of Section Reals
Axiom. (
mul_nat_1R ) We take the following as an axiom:
Axiom. (
mul_nat_com ) We take the following as an axiom:
Axiom. (
mul_nat_SL ) We take the following as an axiom:
Axiom. (
even_nat_0 ) We take the following as an axiom:
Axiom. (
odd_nat_1 ) We take the following as an axiom:
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 .
Beginning of Section Alg
Variable extension_tag : set
Let ctag : set → set λalpha ⇒ SetAdjoin alpha extension_tag Notation . We use
'' as a postfix operator with priority 100 corresponding to applying term
ctag .
Variable F : set → prop
Hypothesis extension_tag_fresh : ∀x, F x ∀ u ∈ x , extension_tag /:e u Axiom. (
pair_tag_0 ) We take the following as an axiom:
Axiom. (
CD_carr_I ) We take the following as an axiom:
Axiom. (
CD_carr_E ) We take the following as an axiom:
Axiom. (
CD_proj0_1 ) We take the following as an axiom:
Axiom. (
CD_proj0_2 ) We take the following as an axiom:
∀x y, F x F y proj0 (pa x y = x Axiom. (
CD_proj1_1 ) We take the following as an axiom:
Axiom. (
CD_proj1_2 ) We take the following as an axiom:
∀x y, F x F y proj1 (pa x y = y Axiom. (
CD_proj0R ) We take the following as an axiom:
Axiom. (
CD_proj1R ) We take the following as an axiom:
Axiom. (
CD_proj0_F ) We take the following as an axiom:
Axiom. (
CD_proj1_F ) We take the following as an axiom:
Beginning of Section CD_minus_conj
Variable minus : set → set
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus .
Notation . We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus .
Variable conj : set → set
Definition. We define
CD_conj to be
λz ⇒ pa (conj (proj0 z (- proj1 z of type
set → set .
End of Section CD_minus_conj
Beginning of Section CD_add
Variable add : set → set → set
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add .
End of Section CD_add
Beginning of Section CD_mul
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul .
Notation . We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul .
End of Section CD_mul
Beginning of Section CD_minus_conj_clos
Variable minus : set → set
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus .
Notation . We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus .
Hypothesis F_minus : ∀x, F x F (- x Axiom. (
CD_minus_CD ) We take the following as an axiom:
Variable conj : set → set
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj .
Hypothesis F_conj : ∀x, F x F (conj x
Axiom. (
CD_conj_CD ) We take the following as an axiom:
End of Section CD_minus_conj_clos
Beginning of Section CD_add_clos
Variable add : set → set → set
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add .
Notation . We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add .
Hypothesis F_add : ∀x y, F x F y F (x + y Axiom. (
CD_add_CD ) We take the following as an axiom:
End of Section CD_add_clos
Beginning of Section CD_mul_clos
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul .
Notation . We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus .
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj .
Notation . We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add .
Notation . We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul .
Hypothesis F_minus : ∀x, F x F (- x Hypothesis F_conj : ∀x, F x F (conj x
Hypothesis F_add : ∀x y, F x F y F (x + y Hypothesis F_mul : ∀x y, F x F y F (x * y Axiom. (
CD_mul_CD ) We take the following as an axiom:
End of Section CD_mul_clos
Beginning of Section CD_minus_conj_F
Variable minus : set → set
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus .
Notation . We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus .
Hypothesis F_minus_0 : - 0 = 0 Variable conj : set → set
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj .
End of Section CD_minus_conj_F
Beginning of Section CD_add_F
Variable add : set → set → set
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add .
Notation . We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add .
Hypothesis F_add_0_0 : 0 + 0 = 0 Axiom. (
CD_add_F_eq ) We take the following as an axiom:
∀x y, F x F y x :+: y = x + y End of Section CD_add_F
Beginning of Section CD_mul_F
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul .
Notation . We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus .
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj .
Notation . We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add .
Notation . We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul .
Hypothesis F_conj : ∀x, F x F (conj x
Hypothesis F_mul : ∀x y, F x F y F (x * y Hypothesis F_minus_0 : - 0 = 0 Hypothesis F_add_0R : ∀x, F x x + 0 = x Hypothesis F_mul_0L : ∀x, F x 0 * x = 0 Hypothesis F_mul_0R : ∀x, F x x * 0 = 0 Axiom. (
CD_mul_F_eq ) We take the following as an axiom:
∀x y, F x F y x :*: y = x * y End of Section CD_mul_F
Beginning of Section CD_minus_invol
Variable minus : set → set
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus .
Notation . We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus .
Hypothesis F_minus : ∀x, F x F (- x Hypothesis F_minus_invol : ∀x, F x - - x = x End of Section CD_minus_invol
Beginning of Section CD_conj_invol
Variable minus : set → set
Variable conj : set → set
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus .
Notation . We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus .
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj .
Hypothesis F_minus : ∀x, F x F (- x Hypothesis F_conj : ∀x, F x F (conj x
Hypothesis F_minus_invol : ∀x, F x - - x = x Hypothesis F_conj_invol : ∀x, F x conj (conj x = x End of Section CD_conj_invol
Beginning of Section CD_conj_minus
Variable minus : set → set
Variable conj : set → set
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus .
Notation . We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus .
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj .
Hypothesis F_minus : ∀x, F x F (- x Hypothesis F_conj : ∀x, F x F (conj x
Hypothesis F_conj_minus : ∀x, F x conj (- x = - conj x End of Section CD_conj_minus
Beginning of Section CD_minus_add
Variable minus : set → set
Variable add : set → set → set
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add .
Notation . We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus .
Notation . We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add .
Hypothesis F_minus : ∀x, F x F (- x Hypothesis F_add : ∀x y, F x F y F (x + y Hypothesis F_minus_add : ∀x y, F x F y - (x + y = - x + - y End of Section CD_minus_add
Beginning of Section CD_conj_add
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add .
Notation . We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus .
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj .
Notation . We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add .
Hypothesis F_minus : ∀x, F x F (- x Hypothesis F_conj : ∀x, F x F (conj x
Hypothesis F_add : ∀x y, F x F y F (x + y Hypothesis F_minus_add : ∀x y, F x F y - (x + y = - x + - y Hypothesis F_conj_add : ∀x y, F x F y conj (x + y = conj x + conj y Axiom. (
CD_conj_add ) We take the following as an axiom:
End of Section CD_conj_add
Beginning of Section CD_add_com
Variable add : set → set → set
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add .
Notation . We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add .
Hypothesis F_add_com : ∀x y, F x F y x + y = y + x Axiom. (
CD_add_com ) We take the following as an axiom:
End of Section CD_add_com
Beginning of Section CD_add_assoc
Variable add : set → set → set
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add .
Notation . We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add .
Hypothesis F_add : ∀x y, F x F y F (x + y Hypothesis F_add_assoc : ∀x y z, F x F y F z (x + y + z = x + (y + z End of Section CD_add_assoc
Beginning of Section CD_add_0R
Variable add : set → set → set
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add .
Notation . We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add .
Hypothesis F_add_0R : ∀x, F x x + 0 = x Axiom. (
CD_add_0R ) We take the following as an axiom:
End of Section CD_add_0R
Beginning of Section CD_add_0L
Variable add : set → set → set
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add .
Notation . We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add .
Hypothesis F_add_0L : ∀x, F x 0 + x = x Axiom. (
CD_add_0L ) We take the following as an axiom:
End of Section CD_add_0L
Beginning of Section CD_add_minus_linv
Variable minus : set → set
Variable add : set → set → set
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add .
Notation . We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus .
Notation . We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add .
Hypothesis F_minus : ∀x, F x F (- x Hypothesis F_add_minus_linv : ∀x, F x - x + x = 0 End of Section CD_add_minus_linv
Beginning of Section CD_add_minus_rinv
Variable minus : set → set
Variable add : set → set → set
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add .
Notation . We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus .
Notation . We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add .
Hypothesis F_minus : ∀x, F x F (- x Hypothesis F_add_minus_rinv : ∀x, F x x + - x = 0 End of Section CD_add_minus_rinv
Beginning of Section CD_mul_0R
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul .
Notation . We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus .
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj .
Notation . We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add .
Notation . We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul .
Hypothesis F_minus_0 : - 0 = 0 Hypothesis F_conj_0 : conj 0 = 0 Hypothesis F_add_0_0 : 0 + 0 = 0 Hypothesis F_mul_0L : ∀x, F x 0 * x = 0 Hypothesis F_mul_0R : ∀x, F x x * 0 = 0 Axiom. (
CD_mul_0R ) We take the following as an axiom:
End of Section CD_mul_0R
Beginning of Section CD_mul_0L
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul .
Notation . We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus .
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj .
Notation . We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add .
Notation . We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul .
Hypothesis F_conj : ∀x, F x F (conj x
Hypothesis F_minus_0 : - 0 = 0 Hypothesis F_add_0_0 : 0 + 0 = 0 Hypothesis F_mul_0L : ∀x, F x 0 * x = 0 Hypothesis F_mul_0R : ∀x, F x x * 0 = 0 Axiom. (
CD_mul_0L ) We take the following as an axiom:
End of Section CD_mul_0L
Beginning of Section CD_mul_1R
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul .
Notation . We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus .
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj .
Notation . We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add .
Notation . We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul .
Hypothesis F_minus_0 : - 0 = 0 Hypothesis F_conj_0 : conj 0 = 0 Hypothesis F_conj_1 : conj 1 = 1 Hypothesis F_add_0L : ∀x, F x 0 + x = x Hypothesis F_add_0R : ∀x, F x x + 0 = x Hypothesis F_mul_0L : ∀x, F x 0 * x = 0 Hypothesis F_mul_1R : ∀x, F x x * 1 = x Axiom. (
CD_mul_1R ) We take the following as an axiom:
End of Section CD_mul_1R
Beginning of Section CD_mul_1L
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul .
Notation . We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus .
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj .
Notation . We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add .
Notation . We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul .
Hypothesis F_conj : ∀x, F x F (conj x
Hypothesis F_minus_0 : - 0 = 0 Hypothesis F_add_0R : ∀x, F x x + 0 = x Hypothesis F_mul_0L : ∀x, F x 0 * x = 0 Hypothesis F_mul_0R : ∀x, F x x * 0 = 0 Hypothesis F_mul_1L : ∀x, F x 1 * x = x Hypothesis F_mul_1R : ∀x, F x x * 1 = x Axiom. (
CD_mul_1L ) We take the following as an axiom:
End of Section CD_mul_1L
Beginning of Section CD_conj_mul
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul .
Notation . We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus .
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj .
Notation . We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add .
Notation . We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul .
Hypothesis F_minus : ∀x, F x F (- x Hypothesis F_conj : ∀x, F x F (conj x
Hypothesis F_add : ∀x y, F x F y F (x + y Hypothesis F_mul : ∀x y, F x F y F (x * y Hypothesis F_minus_invol : ∀x, F x - - x = x Hypothesis F_conj_invol : ∀x, F x conj (conj x = x Hypothesis F_conj_minus : ∀x, F x conj (- x = - conj x Hypothesis F_conj_add : ∀x y, F x F y conj (x + y = conj x + conj y Hypothesis F_minus_add : ∀x y, F x F y - (x + y = - x + - y Hypothesis F_add_com : ∀x y, F x F y x + y = y + x Hypothesis F_conj_mul : ∀x y, F x F y conj (x * y = conj y * conj x Hypothesis F_minus_mul_distrR : ∀x y, F x F y x * (- y = - (x * y Hypothesis F_minus_mul_distrL : ∀x y, F x F y (- x * y = - (x * y Axiom. (
CD_conj_mul ) We take the following as an axiom:
End of Section CD_conj_mul
Beginning of Section CD_add_mul_distrR
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul .
Notation . We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus .
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj .
Notation . We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add .
Notation . We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul .
Hypothesis F_minus : ∀x, F x F (- x Hypothesis F_conj : ∀x, F x F (conj x
Hypothesis F_add : ∀x y, F x F y F (x + y Hypothesis F_mul : ∀x y, F x F y F (x * y Hypothesis F_minus_add : ∀x y, F x F y - (x + y = - x + - y Hypothesis F_add_assoc : ∀x y z, F x F y F z (x + y + z = x + (y + z Hypothesis F_add_com : ∀x y, F x F y x + y = y + x Hypothesis F_add_mul_distrL : ∀x y z, F x F y F z x * (y + z = x * y + x * z Hypothesis F_add_mul_distrR : ∀x y z, F x F y F z (x + y * z = x * z + y * z End of Section CD_add_mul_distrR
Beginning of Section CD_add_mul_distrL
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul .
Notation . We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus .
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj .
Notation . We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add .
Notation . We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul .
Hypothesis F_minus : ∀x, F x F (- x Hypothesis F_conj : ∀x, F x F (conj x
Hypothesis F_add : ∀x y, F x F y F (x + y Hypothesis F_mul : ∀x y, F x F y F (x * y Hypothesis F_minus_add : ∀x y, F x F y - (x + y = - x + - y Hypothesis F_conj_add : ∀x y, F x F y conj (x + y = conj x + conj y Hypothesis F_add_assoc : ∀x y z, F x F y F z (x + y + z = x + (y + z Hypothesis F_add_com : ∀x y, F x F y x + y = y + x Hypothesis F_add_mul_distrL : ∀x y z, F x F y F z x * (y + z = x * y + x * z Hypothesis F_add_mul_distrR : ∀x y z, F x F y F z (x + y * z = x * z + y * z End of Section CD_add_mul_distrL
Beginning of Section CD_minus_mul_distrR
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul .
Notation . We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus .
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj .
Notation . We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add .
Notation . We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul .
Hypothesis F_minus : ∀x, F x F (- x Hypothesis F_conj : ∀x, F x F (conj x
Hypothesis F_add : ∀x y, F x F y F (x + y Hypothesis F_mul : ∀x y, F x F y F (x * y Hypothesis F_conj_minus : ∀x, F x conj (- x = - conj x Hypothesis F_minus_add : ∀x y, F x F y - (x + y = - x + - y Hypothesis F_minus_mul_distrR : ∀x y, F x F y x * (- y = - (x * y Hypothesis F_minus_mul_distrL : ∀x y, F x F y (- x * y = - (x * y End of Section CD_minus_mul_distrR
Beginning of Section CD_minus_mul_distrL
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul .
Notation . We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus .
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj .
Notation . We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add .
Notation . We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul .
Hypothesis F_minus : ∀x, F x F (- x Hypothesis F_conj : ∀x, F x F (conj x
Hypothesis F_add : ∀x y, F x F y F (x + y Hypothesis F_mul : ∀x y, F x F y F (x * y Hypothesis F_minus_add : ∀x y, F x F y - (x + y = - x + - y Hypothesis F_minus_mul_distrR : ∀x y, F x F y x * (- y = - (x * y Hypothesis F_minus_mul_distrL : ∀x y, F x F y (- x * y = - (x * y End of Section CD_minus_mul_distrL
Beginning of Section CD_exp_nat
Variable minus : set → set
Variable conj : set → set
Variable add : set → set → set
Variable mul : set → set → set
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus .
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
conj .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul .
Notation . We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus .
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj .
Notation . We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add .
Notation . We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul .
Notation . We use
^ as an infix operator with priority 342 and no associativity corresponding to applying term
CD_exp_nat minus conj add mul .
Beginning of Section CD_exp_nat_1_2
Hypothesis F_minus_0 : - 0 = 0 Hypothesis F_conj_0 : conj 0 = 0 Hypothesis F_conj_1 : conj 1 = 1 Hypothesis F_add_0L : ∀x, F x 0 + x = x Hypothesis F_add_0R : ∀x, F x x + 0 = x Hypothesis F_mul_0L : ∀x, F x 0 * x = 0 Hypothesis F_mul_1R : ∀x, F x x * 1 = x End of Section CD_exp_nat_1_2
Hypothesis F_minus : ∀x, F x F (- x Hypothesis F_conj : ∀x, F x F (conj x
Hypothesis F_add : ∀x y, F x F y F (x + y Hypothesis F_mul : ∀x y, F x F y F (x * y End of Section CD_exp_nat
End of Section Alg
Beginning of Section Tags
Variable tagn : set
Hypothesis tagn_nat : nat_p tagn Hypothesis tagn_1 : 1 ∈ tagn
Proof:
We prove the intermediate
claim L1 :
0 ∈ { tagn } .
Apply H1 tagn (SingI tagn to the current goal.
An
exact proof term for the current goal is
nat_trans tagn tagn_nat 1 tagn_1 0 In_0_1 .
rewrite the current goal using
SingE tagn 0 L1 (from left to right) at position 2.
An exact proof term for the current goal is tagn_1
∎
Proof: Assume H1 .
Apply H1
Assume H2 _ .
∎
End of Section Tags
Beginning of Section ExtendedSNo
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
tag .
Proof: Let M and N be given.
Assume HMN .
Let x be given.
Assume Hx .
Let v be given.
Assume Hv .
Apply Hx v Hv
Apply orIL to the current goal.
An exact proof term for the current goal is H1
Assume H .
Apply H
Let i be given.
Assume H .
Apply H
Apply orIR to the current goal.
We use i witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HMN i Hi
An exact proof term for the current goal is H1
∎
Proof: Let n be given.
Assume Hn .
Let x be given.
Assume Hx .
Let u be given.
Assume Hu .
We prove the intermediate
claim L1 :
{ n } ∈ Union x .
An
exact proof term for the current goal is
UnionI x { n } u H1 Hu .
Apply Hx { n } L1 to the current goal.
Assume H .
Apply H
Let i be given.
Assume H .
Apply H
rewrite the current goal using
Sing_inj n i H2 (from right to left) at position 2.
An exact proof term for the current goal is Hi
∎
Proof: Let x be given.
Assume Hx .
Let v be given.
Assume Hv .
Let u be given.
Apply SNoLev_ x Hx to the current goal.
Assume _ .
We prove the intermediate
claim Luo :
ordinal u .
Apply orIL to the current goal.
An
exact proof term for the current goal is
ordinal_Hered u Luo v H1 .
Let beta be given.
We prove the intermediate
claim Lv :
v ∈ beta ' .
rewrite the current goal using Hub
An exact proof term for the current goal is H1
Apply orIL to the current goal.
Apply orIR to the current goal.
We use
1 to
witness the existential quantifier.
Apply andI to the current goal.
An
exact proof term for the current goal is
In_1_2 .
An
exact proof term for the current goal is
SingE { 1 } v H5 .
∎
End of Section ExtendedSNo
Beginning of Section SurComplex
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
tag .
Proof: Let x be given.
Assume Hx .
∎
Theorem. (
CSNo_I ) The following is provable:
Theorem. (
CSNo_E ) The following is provable:
Theorem. (
SNo_CSNo ) The following is provable:
Theorem. (
CSNo_0 ) The following is provable:
Proof:
An
exact proof term for the current goal is
SNo_0 .
∎
Theorem. (
CSNo_1 ) The following is provable:
Proof:
An
exact proof term for the current goal is
SNo_1 .
∎
Notation . We use
'' as a postfix operator with priority 100 corresponding to applying term
ctag .
Proof: Let z be given.
Assume Hz .
Apply CSNo_E z Hz to the current goal.
Let x and y be given.
Let v be given.
Let u be given.
We prove the intermediate
claim L1 :
v ∈ Union x .
An
exact proof term for the current goal is
UnionI x v u H1 H3 .
Let w be given.
We prove the intermediate
claim L2 :
v ∈ w '' .
rewrite the current goal using H4
An exact proof term for the current goal is H1
We prove the intermediate
claim L3 :
v ∈ Union y .
An
exact proof term for the current goal is
UnionI y v w H5 Hw .
Apply orIR to the current goal.
We use
2 to
witness the existential quantifier.
Apply andI to the current goal.
An
exact proof term for the current goal is
In_2_3 .
An
exact proof term for the current goal is
SingE { 2 } v H5 .
∎
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 342 and which associates to the right corresponding to applying term
exp_SNo_nat .
Theorem. (
CSNo_Re1 ) The following is provable:
Theorem. (
CSNo_Re2 ) The following is provable:
∀x y, SNo x SNo y Re (pa x y = x Theorem. (
CSNo_Im1 ) The following is provable:
Theorem. (
CSNo_Im2 ) The following is provable:
∀x y, SNo x SNo y Im (pa x y = y Theorem. (
CSNo_ReR ) The following is provable:
Theorem. (
CSNo_ImR ) The following is provable:
Theorem. (
CSNo_ReIm ) The following is provable:
∀z, CSNo z z = pa (Re z (Im z
Proof: Let z be given.
Assume Hz .
Apply CSNo_E z Hz to the current goal.
Let x and y be given.
Assume Hx Hy .
rewrite the current goal using
CSNo_Re2 x y Hx Hy (from left to right).
rewrite the current goal using
CSNo_Im2 x y Hx Hy (from left to right).
∎
Let conj : set → set λx ⇒ x
Notation . We use
:-: as a prefix operator with priority 358 corresponding to applying term
minus_CSNo .
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
conj_CSNo .
Notation . We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_CSNo .
Notation . We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_CSNo .
Notation . We use
:^: as an infix operator with priority 355 and which associates to the right corresponding to applying term
exp_CSNo_nat .
Proof:
Apply CSNo_I to the current goal.
An
exact proof term for the current goal is
SNo_0 .
An
exact proof term for the current goal is
SNo_1 .
∎
Proof: Let z, w and v be given.
Assume Hz Hw Hv .
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
∎
Proof: Let z, w and v be given.
Assume Hz Hw Hv .
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
∎
Theorem. (
SNo_Re ) The following is provable:
Theorem. (
SNo_Im ) The following is provable:
Theorem. (
Re_0 ) The following is provable:
Theorem. (
Im_0 ) The following is provable:
Theorem. (
Re_1 ) The following is provable:
Theorem. (
Im_1 ) The following is provable:
Theorem. (
Re_i ) The following is provable:
Theorem. (
Im_i ) The following is provable:
Proof:
We will
prove Re (i ' = Re (:-: i .
We will
prove Re i = - Re i .
rewrite the current goal using
Re_i (from left to right).
Use symmetry.
An
exact proof term for the current goal is
minus_SNo_0 .
We will
prove Im (i ' = Im (:-: i .
∎
Proof:
An
exact proof term for the current goal is
minus_SNo_0 .
∎
Proof: We prove the intermediate
claim L1 :
∀x y z, SNo x SNo y SNo z (x + y + z = x + (y + z .
Let x, y and z be given.
Assume Hx Hy Hz .
Use symmetry.
An
exact proof term for the current goal is
add_SNo_assoc x y z Hx Hy Hz .
∎
Proof: We prove the intermediate
claim L1 :
∀x y z, SNo x SNo y SNo z (x + y + z = x + (y + z .
Let x, y and z be given.
Assume Hx Hy Hz .
Use symmetry.
An
exact proof term for the current goal is
add_SNo_assoc x y z Hx Hy Hz .
∎
Proof: We prove the intermediate
claim L1 :
∀x y z, SNo x SNo y SNo z (x + y + z = x + (y + z .
Let x, y and z be given.
Assume Hx Hy Hz .
Use symmetry.
An
exact proof term for the current goal is
add_SNo_assoc x y z Hx Hy Hz .
∎
Proof: Let x, y, z and w be given.
Assume Hx Hy Hz Hw .
rewrite the current goal using
add_SNo_com z w Hz Hw (from left to right).
We will
prove (x + y + (w + z = (x + w + (y + z .
∎
Proof: Let z and w be given.
Assume Hz Hw .
We prove the intermediate
claim Lzw :
CSNo (mult' z w .
An
exact proof term for the current goal is
CSNo_mul_CSNo z w Hz Hw .
We prove the intermediate
claim Lwz :
CSNo (mult' w z .
An
exact proof term for the current goal is
CSNo_mul_CSNo w z Hw Hz .
We prove the intermediate
claim LRezR :
SNo (Re z .
An
exact proof term for the current goal is
CSNo_ReR z Hz .
We prove the intermediate
claim LRewR :
SNo (Re w .
An
exact proof term for the current goal is
CSNo_ReR w Hw .
We prove the intermediate
claim LImzR :
SNo (Im z .
An
exact proof term for the current goal is
CSNo_ImR z Hz .
We prove the intermediate
claim LImwR :
SNo (Im w .
An
exact proof term for the current goal is
CSNo_ImR w Hw .
We will
prove Re (mult' z w = Re (mult' w z .
Use transitivity with
Re z * Re w + - (Im w * Im z , and
Re w * Re z + - (Im z * Im w .
An
exact proof term for the current goal is
mul_CSNo_CRe z w Hz Hw .
Use f_equal.
An
exact proof term for the current goal is
mul_SNo_com (Re z (Re w LRezR LRewR .
Use f_equal.
An
exact proof term for the current goal is
mul_SNo_com (Im w (Im z LImwR LImzR .
Use symmetry.
An
exact proof term for the current goal is
mul_CSNo_CRe w z Hw Hz .
We will
prove Im (mult' z w = Im (mult' w z .
Use transitivity with
Im w * Re z + Im z * Re w , and
Im z * Re w + Im w * Re z .
An
exact proof term for the current goal is
mul_CSNo_CIm z w Hz Hw .
Use symmetry.
An
exact proof term for the current goal is
mul_CSNo_CIm w z Hw Hz .
∎
Proof: Let z, w and v be given.
Assume Hz Hw Hv .
We prove the intermediate
claim Lwv :
CSNo (mult' w v .
An
exact proof term for the current goal is
CSNo_mul_CSNo w v Hw Hv .
We prove the intermediate
claim Lzw :
CSNo (mult' z w .
An
exact proof term for the current goal is
CSNo_mul_CSNo z w Hz Hw .
We prove the intermediate
claim Lzwv1 :
CSNo (mult' z (mult' w v .
An
exact proof term for the current goal is
CSNo_mul_CSNo z (mult' w v Hz Lwv .
We prove the intermediate
claim Lzwv2 :
CSNo (mult' (mult' z w v .
An
exact proof term for the current goal is
CSNo_mul_CSNo (mult' z w v Lzw Hv .
We prove the intermediate
claim LRezR :
SNo (Re z .
An
exact proof term for the current goal is
CSNo_ReR z Hz .
We prove the intermediate
claim LRewR :
SNo (Re w .
An
exact proof term for the current goal is
CSNo_ReR w Hw .
We prove the intermediate
claim LRevR :
SNo (Re v .
An
exact proof term for the current goal is
CSNo_ReR v Hv .
We prove the intermediate
claim LImzR :
SNo (Im z .
An
exact proof term for the current goal is
CSNo_ImR z Hz .
We prove the intermediate
claim LImwR :
SNo (Im w .
An
exact proof term for the current goal is
CSNo_ImR w Hw .
We prove the intermediate
claim LImvR :
SNo (Im v .
An
exact proof term for the current goal is
CSNo_ImR v Hv .
Apply CSNo_ReIm_split (mult' z (mult' w v (mult' (mult' z w v Lzwv1 Lzwv2 to the current goal.
We will
prove Re (mult' z (mult' w v = Re (mult' (mult' z w v .
Use transitivity with
Re z * Re (mult' w v + - (Im (mult' w v * Im z ,
(Re z * Re w * Re v + - (Re z * Im v * Im w + (- Im v * Re w * Im z + - Im w * Re v * Im z ,
(Re z * Re w * Re v + - Im w * Re v * Im z + (- (Re z * Im v * Im w + - Im v * Re w * Im z , and
Re (mult' z w * Re v + - (Im v * Im (mult' z w .
An
exact proof term for the current goal is
mul_CSNo_CRe z (mult' w v Hz Lwv .
Use f_equal.
We will
prove Re z * Re (mult' w v = Re z * Re w * Re v + - (Re z * Im v * Im w .
Use transitivity with
Re z * (Re w * Re v + - (Im v * Im w , and
Re z * Re w * Re v + Re z * (- (Im v * Im w .
Use f_equal.
An
exact proof term for the current goal is
mul_CSNo_CRe w v Hw Hv .
An
exact proof term for the current goal is
SNo_mul_SNo (Im v (Im w LImvR LImwR .
Use f_equal.
We will
prove Re z * (- (Im v * Im w = - (Re z * Im v * Im w .
We will
prove - (Im (mult' w v * Im z = - Im v * Re w * Im z + - Im w * Re v * Im z .
Use transitivity with and
- (Im v * Re w * Im z + Im w * Re v * Im z .
Use f_equal.
We will
prove Im (mult' w v * Im z = Im v * Re w * Im z + Im w * Re v * Im z .
Use transitivity with
(Im v * Re w + Im w * Re v * Im z , and
(Im v * Re w * Im z + (Im w * Re v * Im z .
Use f_equal.
An
exact proof term for the current goal is
mul_CSNo_CIm w v Hw Hv .
We will
prove (Im v * Re w + Im w * Re v * Im z = (Im v * Re w * Im z + (Im w * Re v * Im z .
Use f_equal.
Use symmetry.
An
exact proof term for the current goal is
mul_SNo_assoc (Im v (Re w (Im z ?? ?? ?? .
Use symmetry.
An
exact proof term for the current goal is
mul_SNo_assoc (Im w (Re v (Im z ?? ?? ?? .
We will
prove - (Im v * Re w * Im z + Im w * Re v * Im z = - Im v * Re w * Im z + - Im w * Re v * Im z .
An
exact proof term for the current goal is
SNo_mul_SNo_3 (Im v (Re w (Im z LImvR LRewR LImzR .
An
exact proof term for the current goal is
SNo_mul_SNo_3 (Im w (Re v (Im z LImwR LRevR LImzR .
An
exact proof term for the current goal is
SNo_mul_SNo_3 (Re z (Re w (Re v LRezR LRewR LRevR .
An
exact proof term for the current goal is
SNo_mul_SNo_3 (Re z (Im v (Im w LRezR LImvR LImwR .
An
exact proof term for the current goal is
SNo_mul_SNo_3 (Im v (Re w (Im z LImvR LRewR LImzR .
An
exact proof term for the current goal is
SNo_mul_SNo_3 (Im w (Re v (Im z LImwR LRevR LImzR .
We will
prove (Re z * Re w * Re v + - Im w * Re v * Im z + (- (Re z * Im v * Im w + - Im v * Re w * Im z = (Re (mult' z w * Re v + - (Im v * Im (mult' z w .
Use f_equal.
We will
prove Re z * Re w * Re v + - Im w * Re v * Im z = Re (mult' z w * Re v .
Use transitivity with
(Re z * Re w * Re v + (- (Im w * Im z * Re v , and
(Re z * Re w + - (Im w * Im z * Re v .
Use f_equal.
We will
prove Re z * Re w * Re v = (Re z * Re w * Re v .
An
exact proof term for the current goal is
mul_SNo_assoc (Re z (Re w (Re v LRezR LRewR LRevR .
We will
prove - (Im w * Re v * Im z = (- (Im w * Im z * Re v .
Use transitivity with and
- ((Im w * Im z * Re v .
Use f_equal.
Use transitivity with and
(Im w * Im z * Re v .
Use f_equal.
An
exact proof term for the current goal is
mul_SNo_com (Re v (Im z ?? ?? .
An
exact proof term for the current goal is
mul_SNo_assoc (Im w (Im z (Re v ?? ?? ?? .
Use symmetry.
We will
prove (- (Im w * Im z * Re v = - ((Im w * Im z * Re v .
Use f_equal.
Use symmetry.
An
exact proof term for the current goal is
mul_CSNo_CRe z w Hz Hw .
We will
prove - (Re z * Im v * Im w + - Im v * Re w * Im z = - (Im v * Im (mult' z w .
Use transitivity with and
- (Re z * Im v * Im w + Im v * Re w * Im z .
Use symmetry.
An
exact proof term for the current goal is
SNo_mul_SNo_3 (Re z (Im v (Im w ?? ?? ?? .
An
exact proof term for the current goal is
SNo_mul_SNo_3 (Im v (Re w (Im z ?? ?? ?? .
Use f_equal.
We will
prove Re z * Im v * Im w + Im v * Re w * Im z = Im v * Im (mult' z w .
rewrite the current goal using
mul_SNo_com_3_0_1 (Re z (Im v (Im w ?? ?? ?? (from left to right).
Use transitivity with and
Im v * (Re z * Im w + Re w * Im z .
We will
prove Im v * (Re z * Im w + Re w * Im z = Im v * Im (mult' z w .
Use f_equal.
Use symmetry.
We will
prove Im (mult' z w = Re z * Im w + Re w * Im z .
rewrite the current goal using
mul_SNo_com (Re z (Im w ?? ?? (from left to right).
rewrite the current goal using
mul_SNo_com (Re w (Im z ?? ?? (from left to right).
An
exact proof term for the current goal is
mul_CSNo_CIm z w Hz Hw .
We will
prove (Re (mult' z w * Re v + - (Im v * Im (mult' z w = Re (mult' (mult' z w v .
Use symmetry.
An
exact proof term for the current goal is
mul_CSNo_CRe (mult' z w v Lzw Hv .
We will
prove Im (mult' z (mult' w v = Im (mult' (mult' z w v .
Use transitivity with
Im (mult' w v * Re z + Im z * Re (mult' w v ,
(Im v * Re w + Im w * Re v * Re z + Im z * (Re w * Re v + - (Im v * Im w ,
(Im v * Re w * Re z + Im w * Re v * Re z + (Im z * Re w * Re v + - (Im z * Im v * Im w ,
(Im v * Re w * Re z + - (Im z * Im v * Im w + (Im w * Re v * Re z + Im z * Re w * Re v ,
Im v * (Re z * Re w + - (Im w * Im z + (Im w * Re z + Im z * Re w * Re v , and
Im v * Re (mult' z w + Im (mult' z w * Re v .
We will
prove Im (mult' z (mult' w v = Im (mult' w v * Re z + Im z * Re (mult' w v .
An
exact proof term for the current goal is
mul_CSNo_CIm z (mult' w v Hz Lwv .
We will
prove Im (mult' w v * Re z + Im z * Re (mult' w v = (Im v * Re w + Im w * Re v * Re z + Im z * (Re w * Re v + - (Im v * Im w .
Use f_equal.
Use f_equal.
An
exact proof term for the current goal is
mul_CSNo_CIm w v ?? ?? .
Use f_equal.
An
exact proof term for the current goal is
mul_CSNo_CRe w v ?? ?? .
We will
prove (Im v * Re w + Im w * Re v * Re z + Im z * (Re w * Re v + - (Im v * Im w = (Im v * Re w * Re z + Im w * Re v * Re z + (Im z * Re w * Re v + - (Im z * Im v * Im w .
Use f_equal.
Use transitivity with and
(Im v * Re w * Re z + (Im w * Re v * Re z .
Use f_equal.
Use symmetry.
An
exact proof term for the current goal is
mul_SNo_assoc (Im v (Re w (Re z ?? ?? ?? .
Use symmetry.
An
exact proof term for the current goal is
mul_SNo_assoc (Im w (Re v (Re z ?? ?? ?? .
Use transitivity with and
Im z * Re w * Re v + Im z * (- (Im v * Im w .
An
exact proof term for the current goal is
SNo_mul_SNo (Im v (Im w ?? ?? .
Use f_equal.
We will
prove Im z * (- (Im v * Im w = - Im z * Im v * Im w .
We will
prove (Im v * Re w * Re z + Im w * Re v * Re z + (Im z * Re w * Re v + - (Im z * Im v * Im w = (Im v * Re w * Re z + - (Im z * Im v * Im w + (Im w * Re v * Re z + Im z * Re w * Re v .
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
Use f_equal.
We will
prove Im v * Re w * Re z + - (Im z * Im v * Im w = Im v * (Re z * Re w + - (Im w * Im z .
rewrite the current goal using
mul_SNo_com (Re w (Re z ?? ?? (from left to right).
rewrite the current goal using
mul_SNo_com (Im w (Im z ?? ?? (from left to right).
rewrite the current goal using
mul_SNo_com_3_0_1 (Im z (Im v (Im w ?? ?? ?? (from left to right).
We will
prove Im v * Re z * Re w + - (Im v * Im z * Im w = Im v * (Re z * Re w + - (Im z * Im w .
Use symmetry.
We will
prove Im v * (Re z * Re w + - (Im z * Im w = Im v * Re z * Re w + Im v * (- Im z * Im w .
We will
prove Im w * Re v * Re z + Im z * Re w * Re v = (Im w * Re z + Im z * Re w * Re v .
rewrite the current goal using
mul_SNo_com (Re v (Re z ?? ?? (from left to right).
rewrite the current goal using
mul_SNo_assoc (Im w (Re z (Re v ?? ?? ?? (from left to right).
rewrite the current goal using
mul_SNo_assoc (Im z (Re w (Re v ?? ?? ?? (from left to right).
Use symmetry.
We will
prove Im v * (Re z * Re w + - (Im w * Im z + (Im w * Re z + Im z * Re w * Re v = Im v * Re (mult' z w + Im (mult' z w * Re v .
Use f_equal.
Use f_equal.
Use symmetry.
An
exact proof term for the current goal is
mul_CSNo_CRe z w Hz Hw .
Use f_equal.
Use symmetry.
An
exact proof term for the current goal is
mul_CSNo_CIm z w Hz Hw .
We will
prove Im v * Re (mult' z w + Im (mult' z w * Re v = Im (mult' (mult' z w v .
Use symmetry.
An
exact proof term for the current goal is
mul_CSNo_CIm (mult' z w v Lzw Hv .
∎
Proof: We prove the intermediate
claim Lii :
CSNo (i :*: i .
We prove the intermediate
claim Lm1 :
CSNo (:-: 1 .
We will
prove Re (i :*: i = Re (:-: 1 .
We will
prove Re i * Re i + - Im i * Im i = - Re 1 .
rewrite the current goal using
Re_i (from left to right).
rewrite the current goal using
Im_i (from left to right).
rewrite the current goal using
Re_1 (from left to right).
We will
prove Im (i :*: i = Im (:-: 1 .
We will
prove Im i * Re i + Im i * Re i = - Im 1 .
rewrite the current goal using
Re_i (from left to right).
rewrite the current goal using
Im_i (from left to right).
rewrite the current goal using
Im_1 (from left to right).
rewrite the current goal using
minus_SNo_0 (from left to right).
∎
Proof: Let z be given.
Assume Hz .
We will
prove SNo (Re z ^ 2 + Im z ^ 2 .
An
exact proof term for the current goal is
CSNo_ReR z Hz .
An
exact proof term for the current goal is
nat_2 .
An
exact proof term for the current goal is
CSNo_ImR z Hz .
An
exact proof term for the current goal is
nat_2 .
∎
Proof: Let z be given.
Assume Hz .
Set x to be the term Re z
Set y to be the term Im z
We prove the intermediate
claim Lx :
SNo x .
An
exact proof term for the current goal is
CSNo_ReR z Hz .
We prove the intermediate
claim Ly :
SNo y .
An
exact proof term for the current goal is
CSNo_ImR z Hz .
We prove the intermediate
claim Lxx :
SNo (x ^ 2 .
We prove the intermediate
claim Lyy :
SNo (y ^ 2 .
rewrite the current goal using
add_SNo_0L 0 SNo_0 (from right to left) at position 1.
rewrite the current goal using
exp_SNo_nat_2 x Lx (from left to right).
rewrite the current goal using
exp_SNo_nat_2 y Ly (from left to right).
∎
Proof: Let z be given.
Assume Hz .
Set x to be the term Re z
Set y to be the term Im z
Set s to be the term
x ^ 2 + y ^ 2 .
We prove the intermediate
claim Lx :
SNo x .
An
exact proof term for the current goal is
CSNo_ReR z Hz .
We prove the intermediate
claim Ly :
SNo y .
An
exact proof term for the current goal is
CSNo_ImR z Hz .
We prove the intermediate
claim Lxx :
SNo (x ^ 2 .
We prove the intermediate
claim Lyy :
SNo (y ^ 2 .
We prove the intermediate
claim Ls :
SNo s .
An
exact proof term for the current goal is
SNo_add_SNo (x ^ 2 (y ^ 2 Lxx Lyy .
We will
prove Re z = Re 0 .
rewrite the current goal using
Re_0 (from left to right).
An exact proof term for the current goal is H2
rewrite the current goal using H1
We will
prove x ^ 2 <= s .
rewrite the current goal using
add_SNo_0R (x ^ 2 ?? (from right to left) at position 1.
We will
prove 0 <= y ^ 2 .
We will
prove Im z = Im 0 .
rewrite the current goal using
Im_0 (from left to right).
An exact proof term for the current goal is H2
rewrite the current goal using H1
We will
prove y ^ 2 <= s .
rewrite the current goal using
add_SNo_0L (y ^ 2 ?? (from right to left) at position 1.
We will
prove 0 <= x ^ 2 .
∎
Proof: Let z be given.
Assume Hz .
Set s to be the term
Re z ^ 2 + Im z ^ 2 .
We prove the intermediate
claim LRezR :
SNo (Re z .
An
exact proof term for the current goal is
CSNo_ReR z Hz .
We prove the intermediate
claim LImzR :
SNo (Im z .
An
exact proof term for the current goal is
CSNo_ImR z Hz .
We prove the intermediate
claim Ls :
SNo s .
Apply CSNo_I to the current goal.
We will
prove SNo (Re z :/: s .
An exact proof term for the current goal is LRezR
An exact proof term for the current goal is Ls
We will
prove SNo (- (Im z :/: s .
An exact proof term for the current goal is LImzR
An exact proof term for the current goal is Ls
∎
Proof: Let z be given.
Assume Hz .
Let u be given.
Assume Hu .
We prove the intermediate
claim LRezR :
SNo (Re z .
An
exact proof term for the current goal is
CSNo_ReR z Hz .
We prove the intermediate
claim LImzR :
SNo (Im z .
An
exact proof term for the current goal is
CSNo_ImR z Hz .
rewrite the current goal using
mul_CSNo_mul_SNo u (Re z Hu LRezR (from left to right).
rewrite the current goal using
mul_CSNo_mul_SNo u (Im z Hu LImzR (from left to right).
We prove the intermediate
claim LuRez :
SNo (u * Re z .
An
exact proof term for the current goal is
SNo_mul_SNo u (Re z ?? ?? .
We prove the intermediate
claim LuRez' :
CSNo (u * Re z .
An exact proof term for the current goal is LuRez
We prove the intermediate
claim LuImz :
SNo (u * Im z .
An
exact proof term for the current goal is
SNo_mul_SNo u (Im z ?? ?? .
We prove the intermediate
claim LuImz' :
CSNo (u * Im z .
An exact proof term for the current goal is LuImz
We prove the intermediate
claim LiuImz :
CSNo (i :*: u * Im z .
An exact proof term for the current goal is LuImz'
We prove the intermediate
claim LmiuImz :
CSNo (:-: i :*: u * Im z .
An exact proof term for the current goal is LiuImz
We prove the intermediate
claim L1 :
CSNo (u * Re z :+: :-: i :*: u * Im z .
We will
prove CSNo (u * Re z .
An exact proof term for the current goal is LuRez'
An exact proof term for the current goal is LmiuImz
We prove the intermediate
claim LRezRez :
SNo (Re z * Re z .
An
exact proof term for the current goal is
SNo_mul_SNo (Re z (Re z ?? ?? .
We prove the intermediate
claim LImzImz :
SNo (Im z * Im z .
An
exact proof term for the current goal is
SNo_mul_SNo (Im z (Im z ?? ?? .
rewrite the current goal using
Re_1 (from left to right).
rewrite the current goal using
add_CSNo_CRe (u * Re z (:-: i :*: u * Im z LuRez' LmiuImz (from left to right).
rewrite the current goal using
add_CSNo_CIm (u * Re z (:-: i :*: u * Im z LuRez' LmiuImz (from left to right).
We will
prove Re z * (Re (u * Re z + Re (:-: i :*: u * Im z + - (Im (u * Re z + Im (:-: i :*: u * Im z * Im z = 1 .
rewrite the current goal using
minus_CSNo_CRe (i :*: u * Im z LiuImz (from left to right).
rewrite the current goal using
minus_CSNo_CIm (i :*: u * Im z LiuImz (from left to right).
rewrite the current goal using
SNo_Re (u * Re z LuRez (from left to right).
rewrite the current goal using
SNo_Im (u * Re z LuRez (from left to right).
We will
prove Re z * (u * Re z + - (Re i * Re (u * Im z + - Im (u * Im z * Im i + - (0 + - Im (i :*: u * Im z * Im z = 1 .
We will
prove Re z * (u * Re z + - (Re i * Re (u * Im z + - Im (u * Im z * Im i + - (0 + - (Im (u * Im z * Re i + Im i * Re (u * Im z * Im z = 1 .
rewrite the current goal using
Re_i (from left to right).
rewrite the current goal using
Im_i (from left to right).
We will
prove Re z * (u * Re z + - (0 * Re (u * Im z + - Im (u * Im z * 1 + - (0 + - (Im (u * Im z * 0 + 1 * Re (u * Im z * Im z = 1 .
rewrite the current goal using
SNo_Re (u * Im z LuImz (from left to right).
rewrite the current goal using
SNo_Im (u * Im z LuImz (from left to right).
rewrite the current goal using
mul_SNo_zeroL (u * Im z LuImz (from left to right).
rewrite the current goal using
minus_SNo_0 (from left to right).
rewrite the current goal using
minus_SNo_0 (from left to right).
rewrite the current goal using
add_SNo_0R (u * Re z LuRez (from left to right).
We will
prove Re z * (u * Re z + - (0 + - (0 + 1 * (u * Im z * Im z = 1 .
rewrite the current goal using
mul_SNo_oneL (u * Im z LuImz (from left to right).
We will
prove Re z * (u * Re z + - (0 + - (0 + (u * Im z * Im z = 1 .
rewrite the current goal using
add_SNo_0L (u * Im z LuImz (from left to right).
We will
prove Re z * (u * Re z + - (- (u * Im z * Im z = 1 .
rewrite the current goal using
minus_SNo_invol (u * Im z LuImz (from left to right).
We will
prove Re z * (u * Re z + (u * Im z * Im z = 1 .
rewrite the current goal using
mul_SNo_com_3_0_1 (Re z u (Re z ?? ?? ?? (from left to right).
rewrite the current goal using
mul_SNo_assoc u (Im z (Im z ?? ?? ?? (from right to left).
We will
prove u * (Re z * Re z + u * (Im z * Im z = 1 .
rewrite the current goal using
mul_SNo_com u (Re z * Re z ?? ?? (from left to right).
rewrite the current goal using
mul_SNo_com u (Im z * Im z ?? ?? (from left to right).
rewrite the current goal using
mul_SNo_distrR (Re z * Re z (Im z * Im z u ?? ?? ?? (from right to left).
rewrite the current goal using
exp_SNo_nat_2 (Re z ?? (from right to left).
rewrite the current goal using
exp_SNo_nat_2 (Im z ?? (from right to left).
An exact proof term for the current goal is Hur
rewrite the current goal using
Im_1 (from left to right).
rewrite the current goal using
add_CSNo_CRe (u * Re z (:-: i :*: u * Im z LuRez' LmiuImz (from left to right).
rewrite the current goal using
add_CSNo_CIm (u * Re z (:-: i :*: u * Im z LuRez' LmiuImz (from left to right).
We will
prove (Im (u * Re z + Im (:-: i :*: u * Im z * Re z + Im z * (Re (u * Re z + Re (:-: i :*: u * Im z = 0 .
rewrite the current goal using
minus_CSNo_CRe (i :*: u * Im z LiuImz (from left to right).
rewrite the current goal using
minus_CSNo_CIm (i :*: u * Im z LiuImz (from left to right).
We will
prove (Im (u * Re z + - Im (i :*: u * Im z * Re z + Im z * (Re (u * Re z + - Re (i :*: u * Im z = 0 .
rewrite the current goal using
SNo_Re (u * Re z LuRez (from left to right).
rewrite the current goal using
SNo_Im (u * Re z LuRez (from left to right).
We will
prove (0 + - Im (i :*: u * Im z * Re z + Im z * ((u * Re z + - Re (i :*: u * Im z = 0 .
We will
prove (0 + - Im (i :*: u * Im z * Re z + Im z * ((u * Re z + - (Re i * Re (u * Im z + - Im (u * Im z * Im i = 0 .
We will
prove (0 + - (Im (u * Im z * Re i + Im i * Re (u * Im z * Re z + Im z * ((u * Re z + - (Re i * Re (u * Im z + - Im (u * Im z * Im i = 0 .
rewrite the current goal using
Re_i (from left to right).
rewrite the current goal using
Im_i (from left to right).
We will
prove (0 + - (Im (u * Im z * 0 + 1 * Re (u * Im z * Re z + Im z * ((u * Re z + - (0 * Re (u * Im z + - Im (u * Im z * 1 = 0 .
rewrite the current goal using
SNo_Re (u * Im z LuImz (from left to right).
rewrite the current goal using
SNo_Im (u * Im z LuImz (from left to right).
rewrite the current goal using
mul_SNo_zeroL (u * Im z ?? (from left to right).
rewrite the current goal using
mul_SNo_oneL (u * Im z ?? (from left to right).
rewrite the current goal using
minus_SNo_0 (from left to right).
rewrite the current goal using
minus_SNo_0 (from left to right).
rewrite the current goal using
add_SNo_0R (u * Re z ?? (from left to right).
rewrite the current goal using
add_SNo_0L (u * Im z ?? (from left to right).
We will
prove (0 + - (u * Im z * Re z + Im z * (u * Re z = 0 .
We will
prove (- (u * Im z * Re z + Im z * (u * Re z = 0 .
We will
prove - (u * Im z * Re z + Im z * u * Re z = 0 .
rewrite the current goal using
mul_SNo_assoc u (Im z (Re z ?? ?? ?? (from right to left).
rewrite the current goal using
mul_SNo_com (Im z (Re z ?? ?? (from left to right).
rewrite the current goal using
mul_SNo_com_3_0_1 (Im z u (Re z ?? ?? ?? (from left to right).
We will
prove - u * Re z * Im z + u * Im z * Re z = 0 .
rewrite the current goal using
mul_SNo_com (Re z (Im z ?? ?? (from left to right).
We will
prove - u * Im z * Re z + u * Im z * Re z = 0 .
∎
Proof: Let z be given.
Assume Hz Hznz .
Set x to be the term Re z
Set y to be the term Im z
Set s to be the term
x ^ 2 + y ^ 2 .
We prove the intermediate
claim Lx :
SNo x .
An
exact proof term for the current goal is
CSNo_ReR z Hz .
We prove the intermediate
claim Ly :
SNo y .
An
exact proof term for the current goal is
CSNo_ImR z Hz .
We prove the intermediate
claim Ls :
SNo s .
We prove the intermediate
claim LsC :
CSNo s .
An
exact proof term for the current goal is
SNo_CSNo s Ls .
We prove the intermediate
claim Lu :
SNo u .
We prove the intermediate
claim LuC :
CSNo u .
An
exact proof term for the current goal is
SNo_CSNo u Lu .
We prove the intermediate
claim LReuS :
SNo (Re u .
An
exact proof term for the current goal is
CSNo_ReR u LuC .
We prove the intermediate
claim LImuS :
SNo (Im u .
An
exact proof term for the current goal is
CSNo_ImR u LuC .
We prove the intermediate
claim Luy :
CSNo (u :*: y .
An exact proof term for the current goal is LuC
An exact proof term for the current goal is Ly
We prove the intermediate
claim Lsnz :
s <> 0 .
Apply Hznz
We prove the intermediate
claim L1 :
Re (i :*: u :*: y = 0 .
We will
prove Re i * Re (u :*: y + - (Im (u :*: y * Im i = 0 .
rewrite the current goal using
Re_i (from left to right).
rewrite the current goal using
Im_i (from left to right).
We will
prove 0 + - (Im y * Re u + Im u * Re y = 0 .
rewrite the current goal using
SNo_Im y Ly (from left to right).
rewrite the current goal using
SNo_Im u Lu (from left to right).
rewrite the current goal using
mul_SNo_zeroL (Re u LReuS (from left to right).
rewrite the current goal using
minus_SNo_0 (from left to right).
We prove the intermediate
claim L2 :
Im (i :*: u :*: y = u * y .
We will
prove Im (u :*: y * Re i + Im i * Re (u :*: y = u * y .
rewrite the current goal using
Re_i (from left to right).
rewrite the current goal using
Im_i (from left to right).
We will
prove 0 + Re (u :*: y = u * y .
rewrite the current goal using
SNo_Re (u * y (SNo_mul_SNo u y ?? ?? (from left to right).
We will
prove 0 + u * y = u * y .
Use f_equal.
Apply CSNo_I to the current goal.
An
exact proof term for the current goal is
SNo_div_SNo x s ?? ?? .
An
exact proof term for the current goal is
SNo_div_SNo y s ?? ?? .
rewrite the current goal using
SNo_Re (u * x (SNo_mul_SNo u x ?? ?? (from left to right).
rewrite the current goal using L1
rewrite the current goal using
minus_SNo_0 (from left to right).
We will
prove x * u = u * x .
An
exact proof term for the current goal is
mul_SNo_com x u ?? ?? .
rewrite the current goal using
SNo_Im (u * x (SNo_mul_SNo u x ?? ?? (from left to right).
rewrite the current goal using L2
We will
prove - (y * u = 0 + - (u * y .
Use f_equal.
An
exact proof term for the current goal is
mul_SNo_com y u ?? ?? .
∎
Proof: Let z be given.
Assume Hz Hznz .
∎
Proof: Let z and w be given.
Assume Hz Hw .
∎
Proof: Let z and w be given.
Assume Hz Hw Hw0 .
rewrite the current goal using
recip_CSNo_invL w Hw Hw0 (from left to right).
We will
prove z :*: 1 = z .
An
exact proof term for the current goal is
mul_CSNo_1R z Hz .
∎
Proof: Let z and w be given.
Assume Hz Hw Hw0 .
∎
Proof: Let x be given.
Assume Hx Hxnn .
We prove the intermediate
claim Lx2S :
SNo (x ^ 2 .
We prove the intermediate
claim Lx2nn :
0 <= x ^ 2 .
rewrite the current goal using
exp_SNo_nat_2 x Hx (from left to right).
rewrite the current goal using
exp_SNo_nat_2 x Hx (from right to left).
An exact proof term for the current goal is H2
rewrite the current goal using H2
rewrite the current goal using Lsx22xx
An
exact proof term for the current goal is
mul_SNo_pos_pos x x ?? ?? ?? ?? .
We will
prove x * x < x * x .
rewrite the current goal using Lsx22xx
An exact proof term for the current goal is H2
We will
prove x * x < x * x .
rewrite the current goal using Lsx22xx
rewrite the current goal using
exp_SNo_nat_2 x Hx (from left to right).
rewrite the current goal using H1
∎
Proof: Let x and y be given.
Assume Hx Hy Hxnn Hxy .
We prove the intermediate
claim Lynn :
0 <= y .
An exact proof term for the current goal is Hxy
Assume H2 .
An exact proof term for the current goal is H2
Apply SNoLtLe_tra x y x Hx Hy Hx Hxy to the current goal.
∎
Proof: Let x and y be given.
Assume Hx Hy Hxnn Hxy .
Apply SNoLeE x y Hx Hy Hxy to the current goal.
rewrite the current goal using H1
∎
Proof: Let x and y be given.
Assume Hx Hy Hxnn Hynn .
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
rewrite the current goal using L1
An exact proof term for the current goal is LsxsyS
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
∎
Proof: Let z be given.
Assume Hz .
∎
Proof: Let z be given.
Assume Hz .
∎
Proof: Let z be given.
Assume Hz .
Set x to be the term Re z
Set y to be the term Im z
We prove the intermediate
claim Lx :
SNo x .
An
exact proof term for the current goal is
CSNo_ReR z Hz .
We prove the intermediate
claim Ly :
SNo y .
An
exact proof term for the current goal is
CSNo_ImR z Hz .
We prove the intermediate
claim Lmx :
SNo (- x .
An exact proof term for the current goal is Lx
We prove the intermediate
claim Lmy :
SNo (- y .
An exact proof term for the current goal is Ly
We prove the intermediate
claim Lx2S :
SNo (x ^ 2 .
We prove the intermediate
claim Ly2S :
SNo (y ^ 2 .
We prove the intermediate
claim Lx2nn :
0 <= x ^ 2 .
rewrite the current goal using
exp_SNo_nat_2 x Lx (from left to right).
We prove the intermediate
claim Ly2nn :
0 <= y ^ 2 .
rewrite the current goal using
exp_SNo_nat_2 y Ly (from left to right).
We prove the intermediate
claim Lx2mx2 :
x ^ 2 = (- x ^ 2 .
rewrite the current goal using
exp_SNo_nat_2 x Lx (from left to right).
rewrite the current goal using
exp_SNo_nat_2 (- x Lmx (from left to right).
We will
prove x * x = (- x * (- x .
Use symmetry.
An exact proof term for the current goal is H1
An exact proof term for the current goal is Lsx2nn
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
rewrite the current goal using
add_SNo_0R (x ^ 2 ?? (from right to left) at position 1.
An exact proof term for the current goal is ??
An
exact proof term for the current goal is
SNo_0 .
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is H1
An exact proof term for the current goal is Lsx2nn
rewrite the current goal using Lx2mx2
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
rewrite the current goal using
add_SNo_0R (x ^ 2 ?? (from right to left) at position 1.
An exact proof term for the current goal is ??
An
exact proof term for the current goal is
SNo_0 .
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Le1S :
SNo (eps_ 1 .
We prove the intermediate
claim Le1nn :
0 <= eps_ 1 .
We prove the intermediate
claim Le12S :
SNo (eps_ 1 ^ 2 .
An exact proof term for the current goal is ??
An
exact proof term for the current goal is
nat_2 .
We prove the intermediate
claim Le12nn :
0 <= eps_ 1 ^ 2 .
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
rewrite the current goal using
add_SNo_0L (- x Lmx (from left to right).
An exact proof term for the current goal is Lmgtnx
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
rewrite the current goal using
add_SNo_0L x Lx (from left to right).
An exact proof term for the current goal is Lmgtx
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim LgammaS :
SNo gamma .
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lgammann :
0 <= gamma .
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim LdeltaS :
SNo delta .
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Ldeltann :
0 <= delta .
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim LmdeltaS :
SNo (- delta .
An exact proof term for the current goal is ??
We prove the intermediate
claim LdeltagammaS :
SNo (delta * gamma .
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lpa1 :
CSNo (pa gamma (- delta .
Apply CSNo_I to the current goal.
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lpa2 :
CSNo (pa gamma delta .
Apply CSNo_I to the current goal.
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lpa1s :
CSNo (pa gamma (- delta :^: 2 .
An exact proof term for the current goal is ??
An
exact proof term for the current goal is
nat_2 .
We prove the intermediate
claim Lpa2s :
CSNo (pa gamma delta :^: 2 .
An exact proof term for the current goal is ??
An
exact proof term for the current goal is
nat_2 .
Use f_equal.
Use f_equal.
rewrite the current goal using
exp_SNo_nat_2 x ?? (from right to left).
We prove the intermediate
claim Lgamma2mdelta2 :
gamma * gamma + - (delta * delta = x .
rewrite the current goal using Lgamma2eq
rewrite the current goal using Ldelta2eq
An
exact proof term for the current goal is
mul_SNo_oneL x ?? .
We prove the intermediate
claim Lcase1cond :
y < 0 \/ y = 0 /\ x < 0 .
Apply orIL to the current goal.
An exact proof term for the current goal is H1
rewrite the current goal using
If_i_1 (y < 0 \/ y = 0 /\ x < 0 (pa gamma (- delta (pa gamma delta Lcase1cond (from left to right).
We will
prove pa gamma (- delta :^: 2 = z .
rewrite the current goal using
exp_CSNo_nat_2 (pa gamma (- delta ?? (from left to right).
We will
prove Re (pa gamma (- delta :*: pa gamma (- delta = x .
rewrite the current goal using
mul_CSNo_CRe (pa gamma (- delta (pa gamma (- delta ?? ?? (from left to right).
rewrite the current goal using
CSNo_Re2 gamma (- delta ?? ?? (from left to right).
rewrite the current goal using
CSNo_Im2 gamma (- delta ?? ?? (from left to right).
We will
prove gamma * gamma + - ((- delta * (- delta = x .
We will
prove gamma * gamma + - (delta * delta = x .
An exact proof term for the current goal is Lgamma2mdelta2
rewrite the current goal using
exp_CSNo_nat_2 (pa gamma (- delta ?? (from left to right).
We will
prove Im (pa gamma (- delta :*: pa gamma (- delta = y .
rewrite the current goal using
mul_CSNo_CIm (pa gamma (- delta (pa gamma (- delta ?? ?? (from left to right).
rewrite the current goal using
CSNo_Re2 gamma (- delta ?? ?? (from left to right).
rewrite the current goal using
CSNo_Im2 gamma (- delta ?? ?? (from left to right).
We will
prove (- delta * gamma + (- delta * gamma = y .
We will
prove - delta * gamma + - delta * gamma = y .
rewrite the current goal using
minus_add_SNo_distr (delta * gamma (delta * gamma ?? ?? (from right to left).
We will
prove - (delta * gamma + delta * gamma = y .
rewrite the current goal using Ldeltagamma
rewrite the current goal using
exp_SNo_nat_2 y ?? (from left to right).
rewrite the current goal using
exp_SNo_nat_2 (- y ?? (from right to left).
We prove the intermediate
claim L1 :
0 <= - y .
rewrite the current goal using
minus_SNo_0 (from left to right).
An exact proof term for the current goal is H1
We prove the intermediate
claim Lcase1cond :
y < 0 \/ y = 0 /\ x < 0 .
Apply orIR 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 H2
rewrite the current goal using
If_i_1 (y < 0 \/ y = 0 /\ x < 0 (pa gamma (- delta (pa gamma delta Lcase1cond (from left to right).
We will
prove pa gamma (- delta :^: 2 = z .
rewrite the current goal using
exp_CSNo_nat_2 (pa gamma (- delta ?? (from left to right).
We will
prove Re (pa gamma (- delta :*: pa gamma (- delta = x .
rewrite the current goal using
mul_CSNo_CRe (pa gamma (- delta (pa gamma (- delta ?? ?? (from left to right).
rewrite the current goal using
CSNo_Re2 gamma (- delta ?? ?? (from left to right).
rewrite the current goal using
CSNo_Im2 gamma (- delta ?? ?? (from left to right).
We will
prove gamma * gamma + - ((- delta * (- delta = x .
We will
prove gamma * gamma + - (delta * delta = x .
An exact proof term for the current goal is Lgamma2mdelta2
rewrite the current goal using
exp_CSNo_nat_2 (pa gamma (- delta ?? (from left to right).
We will
prove Im (pa gamma (- delta :*: pa gamma (- delta = y .
rewrite the current goal using
mul_CSNo_CIm (pa gamma (- delta (pa gamma (- delta ?? ?? (from left to right).
rewrite the current goal using
CSNo_Re2 gamma (- delta ?? ?? (from left to right).
rewrite the current goal using
CSNo_Im2 gamma (- delta ?? ?? (from left to right).
We will
prove (- delta * gamma + (- delta * gamma = y .
We will
prove - delta * gamma + - delta * gamma = y .
rewrite the current goal using Ldeltagamma
rewrite the current goal using
exp_SNo_nat_2 y ?? (from left to right).
rewrite the current goal using H1
rewrite the current goal using
minus_SNo_0 (from left to right).
We prove the intermediate
claim Lcase2cond :
~ (y < 0 \/ y = 0 /\ x < 0 .
Assume H .
Apply H
rewrite the current goal using H1
An exact proof term for the current goal is H3
Assume H .
Apply H
rewrite the current goal using
If_i_0 (y < 0 \/ y = 0 /\ x < 0 (pa gamma (- delta (pa gamma delta Lcase2cond (from left to right).
We will
prove pa gamma delta :^: 2 = z .
rewrite the current goal using
exp_CSNo_nat_2 (pa gamma delta ?? (from left to right).
We will
prove Re (pa gamma delta :*: pa gamma delta = x .
rewrite the current goal using
mul_CSNo_CRe (pa gamma delta (pa gamma delta ?? ?? (from left to right).
rewrite the current goal using
CSNo_Re2 gamma delta ?? ?? (from left to right).
rewrite the current goal using
CSNo_Im2 gamma delta ?? ?? (from left to right).
We will
prove gamma * gamma + - (delta * delta = x .
An exact proof term for the current goal is Lgamma2mdelta2
rewrite the current goal using
exp_CSNo_nat_2 (pa gamma delta ?? (from left to right).
We will
prove Im (pa gamma delta :*: pa gamma delta = y .
rewrite the current goal using
mul_CSNo_CIm (pa gamma delta (pa gamma delta ?? ?? (from left to right).
rewrite the current goal using
CSNo_Re2 gamma delta ?? ?? (from left to right).
rewrite the current goal using
CSNo_Im2 gamma delta ?? ?? (from left to right).
We will
prove delta * gamma + delta * gamma = y .
rewrite the current goal using Ldeltagamma
rewrite the current goal using
exp_SNo_nat_2 y ?? (from left to right).
rewrite the current goal using H1
We prove the intermediate
claim Lcase2cond :
~ (y < 0 \/ y = 0 /\ x < 0 .
Assume H .
Apply H
An
exact proof term for the current goal is
SNoLt_tra y 0 y ?? SNo_0 ?? H2 H1 .
Assume H .
Apply H
rewrite the current goal using H2
An exact proof term for the current goal is H1
rewrite the current goal using
If_i_0 (y < 0 \/ y = 0 /\ x < 0 (pa gamma (- delta (pa gamma delta Lcase2cond (from left to right).
We will
prove pa gamma delta :^: 2 = z .
rewrite the current goal using
exp_CSNo_nat_2 (pa gamma delta ?? (from left to right).
We will
prove Re (pa gamma delta :*: pa gamma delta = x .
rewrite the current goal using
mul_CSNo_CRe (pa gamma delta (pa gamma delta ?? ?? (from left to right).
rewrite the current goal using
CSNo_Re2 gamma delta ?? ?? (from left to right).
rewrite the current goal using
CSNo_Im2 gamma delta ?? ?? (from left to right).
We will
prove gamma * gamma + - (delta * delta = x .
An exact proof term for the current goal is Lgamma2mdelta2
rewrite the current goal using
exp_CSNo_nat_2 (pa gamma delta ?? (from left to right).
We will
prove Im (pa gamma delta :*: pa gamma delta = y .
rewrite the current goal using
mul_CSNo_CIm (pa gamma delta (pa gamma delta ?? ?? (from left to right).
rewrite the current goal using
CSNo_Re2 gamma delta ?? ?? (from left to right).
rewrite the current goal using
CSNo_Im2 gamma delta ?? ?? (from left to right).
We will
prove delta * gamma + delta * gamma = y .
rewrite the current goal using Ldeltagamma
An exact proof term for the current goal is H1
∎
End of Section SurComplex
Beginning of Section Complex
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus_CSNo .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_CSNo .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_CSNo .
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 .
Theorem. (
complex_I ) The following is provable:
Proof: Let x be given.
Assume Hx .
Let y be given.
Assume Hy .
rewrite the current goal using
tuple_2_0_eq x y (from right to left).
rewrite the current goal using
tuple_2_1_eq x y (from right to left) at position 2.
∎
Theorem. (
complex_E ) The following is provable:
Proof: Let z be given.
Assume Hz .
Let p be given.
Assume Hp .
Let u be given.
∎
Proof: Let z be given.
Assume Hz .
Let x be given.
Assume Hx .
Let y be given.
Assume Hy .
rewrite the current goal using Hzxy
Apply CSNo_I to the current goal.
An
exact proof term for the current goal is
real_SNo x Hx .
An
exact proof term for the current goal is
real_SNo y Hy .
∎
Proof: Let x be given.
rewrite the current goal using
SNo_pair_0 x (from right to left).
An exact proof term for the current goal is Hx
An
exact proof term for the current goal is
real_0 .
∎
Theorem. (
complex_0 ) The following is provable:
Theorem. (
complex_1 ) The following is provable:
Theorem. (
complex_i ) The following is provable:
Proof:
An
exact proof term for the current goal is
real_0 .
An
exact proof term for the current goal is
real_1 .
∎
Proof: Let x be given.
Assume Hx .
Let y be given.
Assume Hy .
∎
Proof: Let x be given.
Assume Hx .
Let y be given.
Assume Hy .
∎
Proof: Let z be given.
Assume Hz .
Let x be given.
Assume Hx .
Let y be given.
Assume Hy Hzxy .
rewrite the current goal using Hzxy
We will
prove Re (pa x y ∈ real .
rewrite the current goal using
complex_Re_eq x Hx y Hy (from left to right).
An exact proof term for the current goal is Hx
∎
Proof: Let z be given.
Assume Hz .
Let x be given.
Assume Hx .
Let y be given.
Assume Hy Hzxy .
rewrite the current goal using Hzxy
We will
prove Im (pa x y ∈ real .
rewrite the current goal using
complex_Im_eq x Hx y Hy (from left to right).
An exact proof term for the current goal is Hy
∎
Proof: Let z be given.
Assume Hz .
Let w be given.
Assume Hw .
∎
Proof: Let z be given.
Assume Hz .
∎
Proof: Let z be given.
Assume Hz .
∎
Proof: Let z be given.
Assume Hz .
Let w be given.
Assume Hw .
∎
Proof: Let z be given.
Assume Hz .
Let w be given.
Assume Hw .
We prove the intermediate
claim Lz0 :
Re z ∈ real .
We prove the intermediate
claim Lz1 :
Im z ∈ real .
We prove the intermediate
claim Lw0 :
Re w ∈ real .
We prove the intermediate
claim Lw1 :
Im w ∈ real .
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
∎
Proof: Let x be given.
Assume Hx .
rewrite the current goal using
SNo_pair_0 x (from right to left) at position 1.
∎
Proof: Let x be given.
Assume Hx .
rewrite the current goal using
SNo_pair_0 x (from right to left).
∎
Proof: Let x be given.
Assume Hx .
rewrite the current goal using
real_Re_eq x Hx (from left to right).
rewrite the current goal using
real_Im_eq x Hx (from left to right).
rewrite the current goal using
minus_SNo_0 (from left to right).
Use reflexivity.
∎
Proof: Let x be given.
Assume Hx .
rewrite the current goal using
mul_i_real_eq x Hx (from left to right).
We will
prove Re (pa 0 x = 0 .
∎
Proof: Let x be given.
Assume Hx .
rewrite the current goal using
mul_i_real_eq x Hx (from left to right).
We will
prove Im (pa 0 x = x .
∎
Proof: Let z be given.
Assume Hz .
Let x be given.
Assume Hx .
Let y be given.
Assume Hy Hzxy .
rewrite the current goal using Hzxy
rewrite the current goal using
complex_Re_eq x Hx y Hy (from left to right).
rewrite the current goal using
complex_Im_eq x Hx y Hy (from left to right).
We will
prove pa x y = x + i * y .
We will
prove pa x y = pa (add_SNo (Re x (Re (i * y (add_SNo (Im x (Im (i * y .
rewrite the current goal using
real_Re_eq x Hx (from left to right).
rewrite the current goal using
real_Im_eq x Hx (from left to right).
rewrite the current goal using
real_Re_i_eq y Hy (from left to right).
rewrite the current goal using
real_Im_i_eq y Hy (from left to right).
Use reflexivity.
∎
Beginning of Section ComplexDiv
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 342 and which associates to the right corresponding to applying term
exp_SNo_nat .
Proof: Let z be given.
Assume Hz .
We prove the intermediate
claim Lz :
CSNo z .
An
exact proof term for the current goal is
complex_CSNo z Hz .
Let x be given.
Assume Hx .
Let y be given.
Assume Hy .
We prove the intermediate
claim LRez :
Re z ∈ real .
rewrite the current goal using Hzxy
rewrite the current goal using
complex_Re_eq x Hx y Hy (from left to right).
An exact proof term for the current goal is Hx
We prove the intermediate
claim LImz :
Im z ∈ real .
rewrite the current goal using Hzxy
rewrite the current goal using
complex_Im_eq x Hx y Hy (from left to right).
An exact proof term for the current goal is Hy
We prove the intermediate
claim LRez2 :
Re z ^ 2 ∈ real .
An
exact proof term for the current goal is
real_mul_SNo (Re z ?? (Re z ?? .
We prove the intermediate
claim LImz2 :
Im z ^ 2 ∈ real .
An
exact proof term for the current goal is
real_mul_SNo (Im z ?? (Im z ?? .
We prove the intermediate
claim LRez2Imz2 :
Re z ^ 2 + Im z ^ 2 ∈ real .
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
An exact proof term for the current goal is LRez
An exact proof term for the current goal is LRez2Imz2
An exact proof term for the current goal is LImz
An exact proof term for the current goal is LRez2Imz2
∎
Proof: Let z be given.
Assume Hz .
Let w be given.
Assume Hw .
∎
End of Section ComplexDiv
Proof:
Let x be given.
Apply SepI to the current goal.
An
exact proof term for the current goal is
real_complex x Hx .
An
exact proof term for the current goal is
real_Re_eq x Hx .
Let z be given.
Apply SepE complex (λz ⇒ Re z = z ) z Hz to the current goal.
rewrite the current goal using Hz2
∎
End of Section Complex