Primitive . The name
Eps_i is a term of type
(set → prop → set .
Axiom. (
Eps_i_ax ) We take the following as an axiom:
∀P : set → prop ∀x : set , P x P (Eps_i P Definition. We define
True to be
∀p : prop , p → p of type
prop .
Definition. We define
False to be
∀p : prop , p of type
prop .
Definition. We define
not to be
λA : prop ⇒ A → False of type
prop → prop .
Notation . We use
¬ as a prefix operator with priority 700 corresponding to applying term
not .
Definition. We define
and to be
λA B : prop ⇒ ∀p : prop , (A → B → p → p of type
prop → prop → prop .
Notation . We use
∧ as an infix operator with priority 780 and which associates to the left corresponding to applying term
and .
Definition. We define
or to be
λA B : prop ⇒ ∀p : prop , (A → p → (B → p → p of type
prop → prop → prop .
Notation . We use
∨ as an infix operator with priority 785 and which associates to the left corresponding to applying term
or .
Definition. We define
iff to be
λA B : prop ⇒ and (A → B (B → A of type
prop → prop → prop .
Notation . We use
↔ as an infix operator with priority 805 and no associativity corresponding to applying term
iff .
Beginning of Section Eq
Variable A : SType
Definition. We define
eq to be
λx y : A ⇒ ∀Q : A → A → prop Q x y Q y x of type
A → A → prop .
Definition. We define
neq to be
λx y : A ⇒ ¬ eq x y of type
A → A → prop .
End of Section Eq
Notation . We use
= as an infix operator with priority 502 and no associativity corresponding to applying term
eq .
Notation . We use
≠ as an infix operator with priority 502 and no associativity corresponding to applying term
neq .
Beginning of Section FE
Variable A B : SType
Axiom. (
func_ext ) We take the following as an axiom:
∀f g : A → B (∀x : A , f x = g x ) → f = g End of Section FE
Beginning of Section Ex
Variable A : SType
Definition. We define
ex to be
λQ : A → prop ∀P : prop , (∀x : A , Q x P ) → P of type
(A → prop → prop .
End of Section Ex
Notation . We use
∃ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
ex .
Axiom. (
prop_ext ) We take the following as an axiom:
∀p q : prop , iff p q p = q Primitive . The name
In is a term of type
set → set → prop .
Notation . We use
∈ as an infix operator with priority 500 and no associativity corresponding to applying term
In . Furthermore, we may write
∀ x ∈ A , B to mean
∀ x : set, x ∈ A → B .
Definition. We define
Subq to be
λA B ⇒ ∀ x ∈ A , x ∈ B of type
set → set → prop .
Notation . We use
⊆ as an infix operator with priority 500 and no associativity corresponding to applying term
Subq . Furthermore, we may write
∀ x ⊆ A , B to mean
∀ x : set, x ⊆ A → B .
Axiom. (
set_ext ) We take the following as an axiom:
∀X Y : set , X ⊆ Y Y ⊆ X X = Y Axiom. (
In_ind ) We take the following as an axiom:
∀P : set → prop (∀X : set , (∀ x ∈ X , P x → P X ) → ∀X : set , P X Notation . We use
∃ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
ex and handling ∈ or ⊆ ascriptions using
and .
Primitive . The name
Empty is a term of type
set .
Axiom. (
EmptyAx ) We take the following as an axiom:
Primitive . The name
⋃ is a term of type
set → set .
Axiom. (
UnionEq ) We take the following as an axiom:
Primitive . The name
𝒫 is a term of type
set → set .
Axiom. (
PowerEq ) We take the following as an axiom:
∀X Y : set , Y ∈ 𝒫 X ↔ Y ⊆ X Primitive . The name
Repl is a term of type
set → (set → set → set .
Notation .
{B | x ∈ A } is notation for
Repl A (λ x . B ).
Axiom. (
ReplEq ) We take the following as an axiom:
∀A : set , ∀F : set → set ∀y : set , y ∈ { F x | x ∈ A } ↔ ∃ x ∈ A , y = F x Definition. We define
TransSet to be
λU : set ⇒ ∀ x ∈ U , x ⊆ U of type
set → prop .
Definition. We define
Union_closed to be
λU : set ⇒ ∀X : set , X ∈ U ⋃ X ∈ U of type
set → prop .
Definition. We define
Power_closed to be
λU : set ⇒ ∀X : set , X ∈ U 𝒫 X ∈ U of type
set → prop .
Definition. We define
Repl_closed to be
λU : set ⇒ ∀X : set , X ∈ U ∀F : set → set (∀x : set , x ∈ X F x ∈ U ) → { F x | x ∈ X } ∈ U of type
set → prop .
Primitive . The name
UnivOf is a term of type
set → set .
Axiom. (
UnivOf_In ) We take the following as an axiom:
Axiom. (
UnivOf_Min ) We take the following as an axiom:
Axiom. (
FalseE ) We take the following as an axiom:
Axiom. (
TrueI ) We take the following as an axiom:
Axiom. (
andI ) We take the following as an axiom:
∀A B : prop , A → B → A ∧ B Axiom. (
andEL ) We take the following as an axiom:
Axiom. (
andER ) We take the following as an axiom:
Axiom. (
orIL ) We take the following as an axiom:
Axiom. (
orIR ) We take the following as an axiom:
Beginning of Section PropN
Variable P1 P2 P3 : prop
Axiom. (
and3I ) We take the following as an axiom:
P1 → P2 → P3 → P1 ∧ P2 ∧ P3 Axiom. (
and3E ) We take the following as an axiom:
P1 ∧ P2 ∧ P3 (∀p : prop , (P1 → P2 → P3 → p → p ) Axiom. (
or3I1 ) We take the following as an axiom:
Axiom. (
or3I2 ) We take the following as an axiom:
Axiom. (
or3I3 ) We take the following as an axiom:
Axiom. (
or3E ) We take the following as an axiom:
P1 ∨ P2 ∨ P3 (∀p : prop , (P1 → p → (P2 → p → (P3 → p → p ) Variable P4 : prop
Axiom. (
and4I ) We take the following as an axiom:
P1 → P2 → P3 → P4 → P1 ∧ P2 ∧ P3 ∧ P4 Variable P5 : prop
Axiom. (
and5I ) We take the following as an axiom:
P1 → P2 → P3 → P4 → P5 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 End of Section PropN
Axiom. (
iffI ) We take the following as an axiom:
∀A B : prop , (A → B → (B → A → (A ↔ B Axiom. (
iffEL ) We take the following as an axiom:
∀A B : prop , (A ↔ B → A → B Axiom. (
iffER ) We take the following as an axiom:
∀A B : prop , (A ↔ B → B → A Axiom. (
iff_refl ) We take the following as an axiom:
Axiom. (
iff_sym ) We take the following as an axiom:
∀A B : prop , (A ↔ B → (B ↔ A Axiom. (
iff_trans ) We take the following as an axiom:
∀A B C : prop , (A ↔ B → (B ↔ C → (A ↔ C Axiom. (
eq_i_tra ) We take the following as an axiom:
∀x y z, x = y y = z x = z Axiom. (
f_eq_i ) We take the following as an axiom:
∀f : set → set ∀x y, x = y f x = f y Axiom. (
neq_i_sym ) We take the following as an axiom:
Definition. We define
nIn to be
λx X ⇒ ¬ In x X of type
set → set → prop .
Notation . We use
∉ as an infix operator with priority 502 and no associativity corresponding to applying term
nIn .
Axiom. (
Eps_i_ex ) We take the following as an axiom:
∀P : set → prop (∃ x, P x → P (Eps_i P Axiom. (
pred_ext ) We take the following as an axiom:
∀P Q : set → prop (∀x, P x ↔ Q x ) → P = Q Axiom. (
prop_ext_2 ) We take the following as an axiom:
∀p q : prop , (p → q → (q → p → p = q Axiom. (
Subq_ref ) We take the following as an axiom:
Axiom. (
Subq_tra ) We take the following as an axiom:
∀X Y Z : set , X ⊆ Y Y ⊆ Z X ⊆ Z Axiom. (
Subq_contra ) We take the following as an axiom:
∀X Y z : set , X ⊆ Y z ∉ Y z ∉ X Axiom. (
EmptyE ) We take the following as an axiom:
Axiom. (
Subq_Empty ) We take the following as an axiom:
Axiom. (
Empty_eq ) We take the following as an axiom:
Axiom. (
UnionI ) We take the following as an axiom:
∀X x Y : set , x ∈ Y Y ∈ X x ∈ ⋃ X Axiom. (
UnionE ) We take the following as an axiom:
∀X x : set , x ∈ ⋃ X ∃ Y : set , x ∈ Y ∧ Y ∈ X Axiom. (
UnionE_impred ) We take the following as an axiom:
∀X x : set , x ∈ ⋃ X ∀p : prop , (∀Y : set , x ∈ Y Y ∈ X p ) → p Axiom. (
PowerI ) We take the following as an axiom:
∀X Y : set , Y ⊆ X Y ∈ 𝒫 X Axiom. (
PowerE ) We take the following as an axiom:
∀X Y : set , Y ∈ 𝒫 X Y ⊆ X Axiom. (
xm ) We take the following as an axiom:
Axiom. (
dneg ) We take the following as an axiom:
Axiom. (
eq_or_nand ) We take the following as an axiom:
Primitive . The name
exactly1of2 is a term of type
prop → prop → prop .
Axiom. (
exactly1of2_E ) We take the following as an axiom:
∀A B : prop , exactly1of2 A B ∀p : prop , (A → ¬ B p → (¬ A B → p → p Axiom. (
ReplI ) We take the following as an axiom:
∀A : set , ∀F : set → set ∀x : set , x ∈ A F x ∈ { F x | x ∈ A } Axiom. (
ReplE ) We take the following as an axiom:
∀A : set , ∀F : set → set ∀y : set , y ∈ { F x | x ∈ A } ∃ x ∈ A , y = F x Axiom. (
ReplE_impred ) We take the following as an axiom:
∀A : set , ∀F : set → set ∀y : set , y ∈ { F x | x ∈ A } ∀p : prop , (∀x : set , x ∈ A y = F x p ) → p Axiom. (
ReplE' ) We take the following as an axiom:
∀X, ∀f : set → set ∀p : set → prop (∀ x ∈ X , p (f x → ∀ y ∈ { f x | x ∈ X } , p y Axiom. (
Repl_Empty ) We take the following as an axiom:
Axiom. (
ReplEq_ext ) We take the following as an axiom:
∀X, ∀F G : set → set (∀ x ∈ X , F x = G x → { F x | x ∈ X } = { G x | x ∈ X } Axiom. (
Repl_inv_eq ) We take the following as an axiom:
∀P : set → prop ∀f g : set → set (∀x, P x g (f x = x ) → ∀X, (∀ x ∈ X , P x → { g y | y ∈ { f x | x ∈ X } } = X Axiom. (
Repl_invol_eq ) We take the following as an axiom:
∀P : set → prop ∀f : set → set (∀x, P x f (f x = x ) → ∀X, (∀ x ∈ X , P x → { f y | y ∈ { f x | x ∈ X } } = X Primitive . The name
If_i is a term of type
prop → set → set → set .
Notation .
if cond then T else E is notation corresponding to
If_i type cond T E where
type is the inferred type of
T .
Axiom. (
If_i_0 ) We take the following as an axiom:
Axiom. (
If_i_1 ) We take the following as an axiom:
Axiom. (
If_i_or ) We take the following as an axiom:
Primitive . The name
UPair is a term of type
set → set → set .
Notation .
{x ,y } is notation for
UPair x y .
Axiom. (
UPairE ) We take the following as an axiom:
∀x y z : set , x ∈ { y , z } x = y ∨ x = z Axiom. (
UPairI1 ) We take the following as an axiom:
Axiom. (
UPairI2 ) We take the following as an axiom:
Primitive . The name
Sing is a term of type
set → set .
Notation .
{x } is notation for
Sing x .
Axiom. (
SingI ) We take the following as an axiom:
Axiom. (
SingE ) We take the following as an axiom:
∀x y : set , y ∈ { x } y = x 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:
∀X Y z : set , z ∈ X ∪ Y z ∈ X ∨ z ∈ Y Axiom. (
binunionE' ) We take the following as an axiom:
∀X Y z, ∀p : prop , (z ∈ X p → (z ∈ Y p → (z ∈ X ∪ Y p Axiom. (
binunion_asso ) We take the following as an axiom:
∀X Y Z : set , X ∪ (Y ∪ Z = (X ∪ Y ∪ Z Axiom. (
binunion_com ) We take the following as an axiom:
∀X Y : set , X ∪ Y = Y ∪ X Definition. We define
SetAdjoin to be
λX y ⇒ X ∪ { y } of type
set → set → set .
Notation . We now use the set enumeration notation
{...,...,...} in general. If 0 elements are given, then
Empty is used to form the corresponding term. If 1 element is given, then
Sing is used to form the corresponding term. If 2 elements are given, then
UPair is used to form the corresponding term. If more than elements are given, then
SetAdjoin is used to reduce to the case with one fewer elements.
Primitive . The name
famunion is a term of type
set → (set → set → set .
Notation . We use
⋃ x [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
famunion .
Axiom. (
famunionI ) We take the following as an axiom:
∀X : set , ∀F : (set → set , ∀x y : set , x ∈ X y ∈ F x y ∈ ⋃ x ∈ X F x Axiom. (
famunionE ) We take the following as an axiom:
∀X : set , ∀F : (set → set , ∀y : set , y ∈ (⋃ x ∈ X F x ∃ x ∈ X , y ∈ F x Axiom. (
famunionE_impred ) We take the following as an axiom:
∀X : set , ∀F : (set → set , ∀y : set , y ∈ (⋃ x ∈ X F x ∀p : prop , (∀x, x ∈ X y ∈ F x p ) → p
Beginning of Section SepSec
Variable X : set
Variable P : set → prop
Let z : set ≝ Eps_i (λz ⇒ z ∈ X ∧ P z ) Primitive . The name
Sep is a term of type
set .
End of Section SepSec
Notation .
{x ∈ A | B } is notation for
Sep A (λ x . B ).
Axiom. (
SepI ) We take the following as an axiom:
∀X : set , ∀P : (set → prop , ∀x : set , x ∈ X P x x ∈ { x ∈ X | P x } Axiom. (
SepE ) We take the following as an axiom:
∀X : set , ∀P : (set → prop , ∀x : set , x ∈ { x ∈ X | P x } x ∈ X ∧ P x Axiom. (
SepE1 ) We take the following as an axiom:
∀X : set , ∀P : (set → prop , ∀x : set , x ∈ { x ∈ X | P x } x ∈ X Axiom. (
SepE2 ) We take the following as an axiom:
∀X : set , ∀P : (set → prop , ∀x : set , x ∈ { x ∈ X | P x } P x Axiom. (
Sep_Subq ) We take the following as an axiom:
∀X : set , ∀P : set → prop { x ∈ X | P x } ⊆ X Axiom. (
Sep_In_Power ) We take the following as an axiom:
∀X : set , ∀P : set → prop { x ∈ X | P x } ∈ 𝒫 X Primitive . The name
ReplSep is a term of type
set → (set → prop → (set → set → set .
Notation .
{B | x ∈ A , C } is notation for
ReplSep A (λ x . C ) (λ x . B ).
Axiom. (
ReplSepI ) We take the following as an axiom:
∀X : set , ∀P : set → prop ∀F : set → set ∀x : set , x ∈ X P x F x ∈ { F x | x ∈ X , P x } Axiom. (
ReplSepE ) We take the following as an axiom:
∀X : set , ∀P : set → prop ∀F : set → set ∀y : set , y ∈ { F x | x ∈ X , P x } ∃ x : set , x ∈ X ∧ P x ∧ y = F x Axiom. (
ReplSepE_impred ) We take the following as an axiom:
∀X : set , ∀P : set → prop ∀F : set → set ∀y : set , y ∈ { F x | x ∈ X , P x } ∀p : prop , (∀ x ∈ X , P x y = F x p → p Primitive . The name
binintersect is a term of type
set → set → set .
Notation . We use
∩ as an infix operator with priority 340 and which associates to the left corresponding to applying term
binintersect .
Axiom. (
binintersectI ) We take the following as an axiom:
∀X Y z, z ∈ X z ∈ Y z ∈ X ∩ Y Axiom. (
binintersectE ) We take the following as an axiom:
∀X Y z, z ∈ X ∩ Y z ∈ X ∧ z ∈ Y Primitive . The name
setminus is a term of type
set → set → set .
Notation . We use
∖ as an infix operator with priority 350 and no associativity corresponding to applying term
setminus .
Axiom. (
setminusI ) We take the following as an axiom:
∀X Y z, (z ∈ X → (z ∉ Y → z ∈ X ∖ Y Axiom. (
setminusE ) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y → z ∈ X ∧ z ∉ Y Axiom. (
setminusE1 ) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y → z ∈ X Axiom. (
In_irref ) We take the following as an axiom:
Axiom. (
In_no2cycle ) We take the following as an axiom:
Primitive . The name
ordsucc is a term of type
set → set .
Axiom. (
ordsuccI1 ) We take the following as an axiom:
Axiom. (
ordsuccI2 ) We take the following as an axiom:
Axiom. (
ordsuccE ) We take the following as an axiom:
Notation . Natural numbers 0,1,2,... are notation for the terms formed using
Empty as 0 and forming successors with
ordsucc .
Axiom. (
ordsucc_inj ) We take the following as an axiom:
Axiom. (
In_0_1 ) We take the following as an axiom:
Axiom. (
In_0_2 ) We take the following as an axiom:
Axiom. (
In_1_2 ) We take the following as an axiom:
Definition. We define
nat_p to be
λn : set ⇒ ∀p : set → prop p 0 (∀x : set , p x p (ordsucc x ) → p n of type
set → prop .
Axiom. (
nat_0 ) We take the following as an axiom:
Axiom. (
nat_ordsucc ) We take the following as an axiom:
Axiom. (
nat_1 ) We take the following as an axiom:
Axiom. (
nat_2 ) We take the following as an axiom:
Axiom. (
nat_3 ) We take the following as an axiom:
Axiom. (
nat_4 ) 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. (
nat_ind ) We take the following as an axiom:
Axiom. (
nat_inv ) We take the following as an axiom:
Axiom. (
nat_p_trans ) We take the following as an axiom:
Axiom. (
nat_trans ) We take the following as an axiom:
Axiom. (
cases_1 ) We take the following as an axiom:
∀ i ∈ 1 , ∀p : set → prop p 0 p i Axiom. (
cases_2 ) We take the following as an axiom:
∀ i ∈ 2 , ∀p : set → prop p 0 p 1 p i Axiom. (
cases_3 ) We take the following as an axiom:
∀ i ∈ 3 , ∀p : set → prop p 0 p 1 p 2 p i Axiom. (
neq_0_1 ) We take the following as an axiom:
Axiom. (
neq_1_0 ) We take the following as an axiom:
Axiom. (
neq_0_2 ) We take the following as an axiom:
Axiom. (
neq_2_0 ) We take the following as an axiom:
Axiom. (
neq_1_2 ) We take the following as an axiom:
Axiom. (
ZF_closed_E ) We take the following as an axiom:
Primitive . The name
ω is a term of type
set .
Axiom. (
omega_nat_p ) We take the following as an axiom:
Axiom. (
nat_p_omega ) We take the following as an axiom:
Axiom. (
ordinal_1 ) We take the following as an axiom:
Axiom. (
ordinal_2 ) We take the following as an axiom:
Axiom. (
ordinal_ind ) We take the following as an axiom:
∀p : set → prop (∀alpha, ordinal alpha (∀ beta ∈ alpha , p beta → p alpha ) → ∀alpha, ordinal alpha p alpha Definition. We define
inj to be
λX Y f ⇒ (∀ u ∈ X , f u ∈ Y ∧ (∀ u v ∈ X , f u = f v u = v of type
set → set → (set → set → prop .
Definition. We define
bij to be
λX Y f ⇒ (∀ u ∈ X , f u ∈ Y ∧ (∀ u v ∈ X , f u = f v u = v ∧ (∀ w ∈ Y , ∃ u ∈ X , f u = w of type
set → set → (set → set → prop .
Axiom. (
bijI ) We take the following as an axiom:
∀X Y, ∀f : set → set (∀ u ∈ X , f u ∈ Y → (∀ u v ∈ X , f u = f v u = v → (∀ w ∈ Y , ∃ u ∈ X , f u = w → bij X Y f Axiom. (
bijE ) We take the following as an axiom:
∀X Y, ∀f : set → set bij X Y f ∀p : prop , ((∀ u ∈ X , f u ∈ Y → (∀ u v ∈ X , f u = f v u = v → (∀ w ∈ Y , ∃ u ∈ X , f u = w → p → p Primitive . The name
inv is a term of type
set → (set → set → set → set .
Axiom. (
surj_rinv ) We take the following as an axiom:
Axiom. (
inj_linv ) We take the following as an axiom:
∀X, ∀f : set → set (∀ u v ∈ X , f u = f v u = v → ∀ x ∈ X , inv X f (f x = x Axiom. (
bij_inv ) We take the following as an axiom:
∀X Y, ∀f : set → set bij X Y f bij Y X (inv X f Axiom. (
bij_id ) We take the following as an axiom:
Axiom. (
bij_comp ) We take the following as an axiom:
∀X Y Z : set , ∀f g : set → set bij X Y f bij Y Z g bij X Z (λx ⇒ g (f x ) Definition. We define
equip to be
λX Y : set ⇒ ∃ f : set → set , bij X Y f of type
set → set → prop .
Axiom. (
equip_ref ) We take the following as an axiom:
Axiom. (
equip_sym ) We take the following as an axiom:
Axiom. (
equip_tra ) We take the following as an axiom:
Beginning of Section SchroederBernstein
End of Section SchroederBernstein
Beginning of Section PigeonHole
End of Section PigeonHole
Definition. We define
finite to be
λX ⇒ ∃ n ∈ ω , equip X n of type
set → prop .
Axiom. (
finite_ind ) We take the following as an axiom:
Axiom. (
Subq_finite ) We take the following as an axiom:
Axiom. (
exandE_i ) We take the following as an axiom:
∀P Q : set → prop (∃ x, P x ∧ Q x → ∀r : prop , (∀x, P x Q x r ) → r Axiom. (
exandE_ii ) We take the following as an axiom:
∀P Q : (set → set → prop (∃ x : set → set , P x ∧ Q x → ∀p : prop , (∀x : set → set P x Q x p ) → p Axiom. (
exandE_iii ) We take the following as an axiom:
∀P Q : (set → set → set → prop (∃ x : set → set → set , P x ∧ Q x → ∀p : prop , (∀x : set → set → set P x Q x p ) → p Axiom. (
exandE_iiii ) We take the following as an axiom:
∀P Q : (set → set → set → set → prop (∃ x : set → set → set → set , P x ∧ Q x → ∀p : prop , (∀x : set → set → set → set P x Q x p ) → p
Beginning of Section Descr_ii
Variable P : (set → set → prop
Primitive . The name
Descr_ii is a term of type
set → set .
Hypothesis Pex : ∃ f : set → set , P f Hypothesis Puniq : ∀f g : set → set P f P g f = g End of Section Descr_ii
Beginning of Section Descr_iii
Variable P : (set → set → set → prop
Primitive . The name
Descr_iii is a term of type
set → set → set .
Hypothesis Pex : ∃ f : set → set → set , P f Hypothesis Puniq : ∀f g : set → set → set P f P g f = g End of Section Descr_iii
Beginning of Section Descr_Vo1
Primitive . The name
Descr_Vo1 is a term of type
Vo 1 .
Hypothesis Pex : ∃ f : Vo 1 , P f Hypothesis Puniq : ∀f g : Vo 1 P f P g f = g End of Section Descr_Vo1
Beginning of Section If_ii
Variable p : prop
Variable f g : set → set
Primitive . The name
If_ii is a term of type
set → set .
Axiom. (
If_ii_1 ) We take the following as an axiom:
Axiom. (
If_ii_0 ) We take the following as an axiom:
End of Section If_ii
Beginning of Section If_iii
Variable p : prop
Variable f g : set → set → set
Primitive . The name
If_iii is a term of type
set → set → set .
Axiom. (
If_iii_1 ) We take the following as an axiom:
Axiom. (
If_iii_0 ) We take the following as an axiom:
End of Section If_iii
Beginning of Section EpsilonRec_i
Variable F : set → (set → set → set
Primitive . The name
In_rec_i is a term of type
set → set .
Hypothesis Fr : ∀X : set , ∀g h : set → set (∀ x ∈ X , g x = h x → F X g = F X h Axiom. (
In_rec_i_eq ) We take the following as an axiom:
End of Section EpsilonRec_i
Beginning of Section EpsilonRec_ii
Variable F : set → (set → (set → set → (set → set
Primitive . The name
In_rec_ii is a term of type
set → (set → set .
Hypothesis Fr : ∀X : set , ∀g h : set → (set → set (∀ x ∈ X , g x = h x → F X g = F X h End of Section EpsilonRec_ii
Beginning of Section EpsilonRec_iii
Variable F : set → (set → (set → set → set → (set → set → set
Primitive . The name
In_rec_iii is a term of type
set → (set → set → set .
Hypothesis Fr : ∀X : set , ∀g h : set → (set → set → set (∀ x ∈ X , g x = h x → F X g = F X h End of Section EpsilonRec_iii
Beginning of Section NatRec
Variable z : set
Variable f : set → set → set
Let F : set → (set → set → set λn g ⇒ if ⋃ n ∈ n then f (⋃ n (g (⋃ n else z Axiom. (
nat_primrec_r ) We take the following as an axiom:
∀X : set , ∀g h : set → set (∀ x ∈ X , g x = h x → F X g = F X h End of Section NatRec
Beginning of Section NatArith
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_nat .
Axiom. (
add_nat_0R ) We take the following as an axiom:
Axiom. (
add_nat_SR ) We take the following as an axiom:
Axiom. (
add_nat_p ) We take the following as an axiom:
Definition. We define
mul_nat to be
λn m : set ⇒ nat_primrec 0 (λ_ r ⇒ n + r ) m of type
set → set → set .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_nat .
Axiom. (
mul_nat_0R ) We take the following as an axiom:
Axiom. (
mul_nat_SR ) We take the following as an axiom:
Axiom. (
mul_nat_p ) We take the following as an axiom:
End of Section NatArith
Axiom. (
Inj1_eq ) We take the following as an axiom:
Axiom. (
Inj1I1 ) We take the following as an axiom:
Axiom. (
Inj1I2 ) We take the following as an axiom:
Axiom. (
Inj1E ) We take the following as an axiom:
Axiom. (
Inj1NE1 ) We take the following as an axiom:
Axiom. (
Inj1NE2 ) We take the following as an axiom:
Definition. We define
Inj0 to be
λX ⇒ { Inj1 x | x ∈ X } of type
set → set .
Axiom. (
Inj0I ) We take the following as an axiom:
Axiom. (
Inj0E ) We take the following as an axiom:
Axiom. (
Unj_eq ) We take the following as an axiom:
Axiom. (
Unj_Inj1_eq ) We take the following as an axiom:
Axiom. (
Inj1_inj ) We take the following as an axiom:
Axiom. (
Unj_Inj0_eq ) We take the following as an axiom:
Axiom. (
Inj0_inj ) We take the following as an axiom:
Axiom. (
Inj0_0 ) We take the following as an axiom:
Notation . We use
+ as an infix operator with priority 450 and which associates to the left corresponding to applying term
setsum .
Axiom. (
Inj0_setsum ) We take the following as an axiom:
∀X Y x : set , x ∈ X Inj0 x ∈ X + Y Axiom. (
Inj1_setsum ) We take the following as an axiom:
∀X Y y : set , y ∈ Y Inj1 y ∈ X + Y Axiom. (
setsum_0_0 ) We take the following as an axiom:
Beginning of Section pair_setsum
Axiom. (
pairI0 ) We take the following as an axiom:
∀X Y x, x ∈ X pair 0 x ∈ pair X Y Axiom. (
pairI1 ) We take the following as an axiom:
∀X Y y, y ∈ Y pair 1 y ∈ pair X Y Axiom. (
pairE ) We take the following as an axiom:
∀X Y z, z ∈ pair X Y (∃ x ∈ X , z = pair 0 x ∨ (∃ y ∈ Y , z = pair 1 y Axiom. (
pairE0 ) We take the following as an axiom:
∀X Y x, pair 0 x ∈ pair X Y x ∈ X Axiom. (
pairE1 ) We take the following as an axiom:
∀X Y y, pair 1 y ∈ pair X Y y ∈ Y Axiom. (
proj0I ) We take the following as an axiom:
Axiom. (
proj0E ) We take the following as an axiom:
Axiom. (
proj1I ) We take the following as an axiom:
Axiom. (
proj1E ) We take the following as an axiom:
Definition. We define
Sigma to be
λX Y ⇒ ⋃ x ∈ X { pair x y | y ∈ Y x } of type
set → (set → set → set .
Notation . We use
∑ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Sigma .
Axiom. (
pair_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀ x ∈ X , ∀ y ∈ Y x , pair x y ∈ ∑ x ∈ X , Y x Axiom. (
proj0_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀z : set , z ∈ (∑ x ∈ X , Y x proj0 z ∈ X Axiom. (
proj1_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀z : set , z ∈ (∑ x ∈ X , Y x proj1 z ∈ Y (proj0 z Axiom. (
pair_Sigma_E1 ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀x y : set , pair x y ∈ (∑ x ∈ X , Y x y ∈ Y x Axiom. (
Sigma_E ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀z : set , z ∈ (∑ x ∈ X , Y x ∃ x ∈ X , ∃ y ∈ Y x , z = pair x y Definition. We define
setprod to be
λX Y : set ⇒ ∑ x ∈ X , Y of type
set → set → set .
Notation . We use
⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term
setprod .
Let lam : set → (set → set → set Sigma Definition. We define
ap to be
λf x ⇒ { proj1 z | z ∈ f , ∃ y : set , z = pair x y } of type
set → set → set .
Notation . When
x is a set, a term
x y is notation for
ap x y .
Notation .
λ x ∈ A ⇒ B is notation for the set
Sigma A (λ x : set ⇒ B ).
Notation . We now use n-tuple notation (
a0 ,...,
an-1 ) for n ≥ 2 for λ i ∈
n .
if i = 0
then a0 else ... if i =
n-2 then an-2 else an-1 .
Axiom. (
lamI ) We take the following as an axiom:
∀X : set , ∀F : set → set ∀ x ∈ X , ∀ y ∈ F x , pair x y ∈ λ x ∈ X ⇒ F x Axiom. (
lamE ) We take the following as an axiom:
∀X : set , ∀F : set → set ∀z : set , z ∈ (λ x ∈ X ⇒ F x ∃ x ∈ X , ∃ y ∈ F x , z = pair x y Axiom. (
apI ) We take the following as an axiom:
∀f x y, pair x y ∈ f y ∈ f x Axiom. (
apE ) We take the following as an axiom:
∀f x y, y ∈ f x pair x y ∈ f Axiom. (
beta ) We take the following as an axiom:
∀X : set , ∀F : set → set ∀x : set , x ∈ X (λ x ∈ X ⇒ F x x = F x Axiom. (
proj0_ap_0 ) We take the following as an axiom:
Axiom. (
proj1_ap_1 ) We take the following as an axiom:
Axiom. (
pair_ap_0 ) We take the following as an axiom:
∀x y : set , (pair x y 0 = x Axiom. (
pair_ap_1 ) We take the following as an axiom:
∀x y : set , (pair x y 1 = y Axiom. (
ap0_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀z : set , z ∈ (∑ x ∈ X , Y x (z 0 ∈ X Axiom. (
ap1_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀z : set , z ∈ (∑ x ∈ X , Y x (z 1 ∈ (Y (z 0 Definition. We define
pair_p to be
λu : set ⇒ pair (u 0 (u 1 = u of type
set → prop .
Axiom. (
pair_p_I ) We take the following as an axiom:
Axiom. (
tuple_pair ) We take the following as an axiom:
∀x y : set , pair x y = ( x , y ) Definition. We define
Pi to be
λX Y ⇒ { f ∈ 𝒫 (∑ x ∈ X , ⋃ (Y x | ∀ x ∈ X , f x ∈ Y x } of type
set → (set → set → set .
Notation . We use
∏ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Pi .
Axiom. (
PiI ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀f : set , (∀ u ∈ f , pair_p u ∧ u 0 ∈ X → (∀ x ∈ X , f x ∈ Y x → f ∈ ∏ x ∈ X , Y x Axiom. (
lam_Pi ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀F : set → set (∀ x ∈ X , F x ∈ Y x → (λ x ∈ X ⇒ F x ∈ (∏ x ∈ X , Y x Axiom. (
ap_Pi ) We take the following as an axiom:
∀X : set , ∀Y : set → set ∀f : set , ∀x : set , f ∈ (∏ x ∈ X , Y x x ∈ X f x ∈ Y x Definition. We define
setexp to be
λX Y : set ⇒ ∏ y ∈ Y , X of type
set → set → set .
Notation . We use
:^: as an infix operator with priority 430 and which associates to the left corresponding to applying term
setexp .
Axiom. (
lamI2 ) We take the following as an axiom:
Beginning of Section Tuples
Variable x0 x1 : set
End of Section Tuples
End of Section pair_setsum
Notation . We use
∑ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Sigma .
Notation . We use
⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term
setprod .
Notation . We use
∏ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Pi .
Notation . We use
:^: as an infix operator with priority 430 and which associates to the left corresponding to applying term
setexp .
Primitive . The name
DescrR_i_io_1 is a term of type
(set → (set → prop → prop → set .
Primitive . The name
DescrR_i_io_2 is a term of type
(set → (set → prop → prop → set → prop .
Definition. We define
PNoEq_ to be
λalpha p q ⇒ ∀ beta ∈ alpha , p beta ↔ q beta of type
set → (set → prop → (set → prop → prop .
Axiom. (
PNoEq_ref_ ) We take the following as an axiom:
∀alpha, ∀p : set → prop PNoEq_ alpha p p Axiom. (
PNoEq_sym_ ) We take the following as an axiom:
∀alpha, ∀p q : set → prop PNoEq_ alpha p q PNoEq_ alpha q p Axiom. (
PNoEq_tra_ ) We take the following as an axiom:
Axiom. (
PNoLt_E_ ) We take the following as an axiom:
Axiom. (
PNoLt_irref_ ) We take the following as an axiom:
∀alpha, ∀p : set → prop ¬ PNoLt_ alpha p p Axiom. (
PNoLt_mon_ ) We take the following as an axiom:
Axiom. (
PNoLt_tra_ ) We take the following as an axiom:
Primitive . The name
PNoLt is a term of type
set → (set → prop → set → (set → prop → prop .
Axiom. (
PNoLtI1 ) We take the following as an axiom:
Axiom. (
PNoLtI2 ) We take the following as an axiom:
Axiom. (
PNoLtI3 ) We take the following as an axiom:
Axiom. (
PNoLtE ) We take the following as an axiom:
Axiom. (
PNoLt_irref ) We take the following as an axiom:
∀alpha, ∀p : set → prop ¬ PNoLt alpha p alpha p Axiom. (
PNoLtEq_tra ) We take the following as an axiom:
Axiom. (
PNoEqLt_tra ) We take the following as an axiom:
Axiom. (
PNoLt_tra ) We take the following as an axiom:
Definition. We define
PNoLe to be
λalpha p beta q ⇒ PNoLt alpha p beta q ∨ alpha = beta ∧ PNoEq_ alpha p q of type
set → (set → prop → set → (set → prop → prop .
Axiom. (
PNoLeI1 ) We take the following as an axiom:
Axiom. (
PNoLeI2 ) We take the following as an axiom:
∀alpha, ∀p q : set → prop PNoEq_ alpha p q PNoLe alpha p alpha q Axiom. (
PNoLe_ref ) We take the following as an axiom:
∀alpha, ∀p : set → prop PNoLe alpha p alpha p Axiom. (
PNoLtLe_tra ) We take the following as an axiom:
Axiom. (
PNoLeLt_tra ) We take the following as an axiom:
Axiom. (
PNoEqLe_tra ) We take the following as an axiom:
Axiom. (
PNoLe_tra ) We take the following as an axiom:
Axiom. (
PNoLe_downc ) We take the following as an axiom:
Axiom. (
PNo_downc_ref ) We take the following as an axiom:
∀L : set → (set → prop → prop ∀alpha, ordinal alpha ∀p : set → prop L alpha p PNo_downc L alpha p Axiom. (
PNo_upc_ref ) We take the following as an axiom:
∀R : set → (set → prop → prop ∀alpha, ordinal alpha ∀p : set → prop R alpha p PNo_upc R alpha p Axiom. (
PNoLe_upc ) We take the following as an axiom:
Definition. We define
PNoLt_pwise to be
λL R ⇒ ∀gamma, ordinal gamma ∀p : set → prop L gamma p ∀delta, ordinal delta ∀q : set → prop R delta q PNoLt gamma p delta q of type
(set → (set → prop → prop → (set → (set → prop → prop → prop .
Axiom. (
PNo_extend0_eq ) We take the following as an axiom:
∀alpha, ∀p : set → prop PNoEq_ alpha p (λdelta ⇒ p delta ∧ delta ≠ alpha ) Axiom. (
PNo_extend1_eq ) We take the following as an axiom:
∀alpha, ∀p : set → prop PNoEq_ alpha p (λdelta ⇒ p delta ∨ delta = alpha ) Definition. We define
PNo_lenbdd to be
λalpha L ⇒ ∀beta, ∀p : set → prop L beta p beta ∈ alpha of type
set → (set → (set → prop → prop → prop .
Definition. We define
PNo_least_rep2 to be
λL R beta p ⇒ PNo_least_rep L R beta p ∧ ∀x, x ∉ beta ¬ p x of type
(set → (set → prop → prop → (set → (set → prop → prop → set → (set → prop → prop .
Primitive . The name
PNo_bd is a term of type
(set → (set → prop → prop → (set → (set → prop → prop → set .
Primitive . The name
PNo_pred is a term of type
(set → (set → prop → prop → (set → (set → prop → prop → set → prop .
Axiom. (
PNo_bd_pred ) We take the following as an axiom:
Axiom. (
PNo_bd_In ) We take the following as an axiom:
Beginning of Section TaggedSets
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
tag .
Definition. We define
SNoElts_ to be
λalpha ⇒ alpha ∪ { beta ' | beta ∈ alpha } of type
set → set .
Axiom. (
SNoElts_mon ) We take the following as an axiom:
Axiom. (
PNoEq_PSNo ) We take the following as an axiom:
Axiom. (
SNo_PSNo ) We take the following as an axiom:
Primitive . The name
SNo is a term of type
set → prop .
Axiom. (
SNo_SNo ) We take the following as an axiom:
Primitive . The name
SNoLev is a term of type
set → set .
Axiom. (
SNoLev_uniq ) We take the following as an axiom:
Axiom. (
SNoLev_prop ) We take the following as an axiom:
Axiom. (
SNoLev_ ) We take the following as an axiom:
Axiom. (
SNoLev_PSNo ) We take the following as an axiom:
Axiom. (
SNo_Subq ) We take the following as an axiom:
Definition. We define
SNoEq_ to be
λalpha x y ⇒ PNoEq_ alpha (λbeta ⇒ beta ∈ x ) (λbeta ⇒ beta ∈ y ) of type
set → set → set → prop .
Axiom. (
SNoEq_I ) We take the following as an axiom:
Axiom. (
SNo_eq ) We take the following as an axiom:
End of Section TaggedSets
Notation . We use
< as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLt .
Notation . We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLe .
Axiom. (
SNoLtLe ) We take the following as an axiom:
Axiom. (
SNoLeE ) We take the following as an axiom:
Axiom. (
SNoEq_sym_ ) We take the following as an axiom:
Axiom. (
SNoEq_tra_ ) We take the following as an axiom:
Axiom. (
SNoLtE ) We take the following as an axiom:
Axiom. (
SNoLtI2 ) We take the following as an axiom:
Axiom. (
SNoLtI3 ) We take the following as an axiom:
Axiom. (
SNoLt_irref ) We take the following as an axiom:
Axiom. (
SNoLt_tra ) We take the following as an axiom:
Axiom. (
SNoLe_ref ) We take the following as an axiom:
Axiom. (
SNoLtLe_tra ) We take the following as an axiom:
Axiom. (
SNoLeLt_tra ) We take the following as an axiom:
Axiom. (
SNoLe_tra ) We take the following as an axiom:
Axiom. (
SNoLtLe_or ) We take the following as an axiom:
Axiom. (
SNoCutP_L_0 ) We take the following as an axiom:
Axiom. (
SNoCutP_0_R ) We take the following as an axiom:
Axiom. (
SNoCutP_0_0 ) We take the following as an axiom:
Axiom. (
SNoS_E ) We take the following as an axiom:
Beginning of Section TaggedSets2
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
tag .
Axiom. (
SNoS_I ) We take the following as an axiom:
Axiom. (
SNoS_I2 ) We take the following as an axiom:
Axiom. (
SNoS_Subq ) We take the following as an axiom:
Axiom. (
SNoS_E2 ) We take the following as an axiom:
Axiom. (
SNoS_In_neq ) We take the following as an axiom:
Axiom. (
SNoS_SNoLev ) We take the following as an axiom:
Axiom. (
SNoL_E ) We take the following as an axiom:
Axiom. (
SNoR_E ) We take the following as an axiom:
Axiom. (
SNoL_SNoS_ ) We take the following as an axiom:
Axiom. (
SNoR_SNoS_ ) We take the following as an axiom:
Axiom. (
SNoL_SNoS ) We take the following as an axiom:
Axiom. (
SNoR_SNoS ) We take the following as an axiom:
Axiom. (
SNoL_I ) We take the following as an axiom:
Axiom. (
SNoR_I ) We take the following as an axiom:
Axiom. (
SNo_eta ) We take the following as an axiom:
Axiom. (
SNoCut_Le ) We take the following as an axiom:
Axiom. (
SNoCut_ext ) We take the following as an axiom:
Axiom. (
ordinal_SNo ) We take the following as an axiom:
Axiom. (
nat_p_SNo ) We take the following as an axiom:
Axiom. (
omega_SNo ) We take the following as an axiom:
Axiom. (
SNo_0 ) We take the following as an axiom:
Axiom. (
SNo_1 ) We take the following as an axiom:
Axiom. (
SNo_2 ) We take the following as an axiom:
Axiom. (
SNoLev_0 ) We take the following as an axiom:
Axiom. (
SNoCut_0_0 ) We take the following as an axiom:
Axiom. (
SNoL_0 ) We take the following as an axiom:
Axiom. (
SNoR_0 ) We take the following as an axiom:
Axiom. (
SNoL_1 ) We take the following as an axiom:
Axiom. (
SNoR_1 ) We take the following as an axiom:
Axiom. (
eps_0_1 ) We take the following as an axiom:
Axiom. (
SNo__eps_ ) We take the following as an axiom:
Axiom. (
SNo_eps_ ) We take the following as an axiom:
Axiom. (
SNo_eps_1 ) We take the following as an axiom:
Axiom. (
SNoLev_eps_ ) We take the following as an axiom:
Axiom. (
SNo_eps_pos ) We take the following as an axiom:
Axiom. (
eps_SNo_eq ) We take the following as an axiom:
Axiom. (
eps_SNoCutP ) We take the following as an axiom:
Axiom. (
eps_SNoCut ) We take the following as an axiom:
End of Section TaggedSets2
Axiom. (
SNo_etaE ) We take the following as an axiom:
Axiom. (
SNo_ind ) We take the following as an axiom:
Beginning of Section SurrealRecI
Variable F : set → (set → set → set
Primitive . The name
SNo_rec_i is a term of type
set → set .
Hypothesis Fr : ∀z, SNo z ∀g h : set → set (∀ w ∈ SNoS_ (SNoLev z , g w = h w → F z g = F z h End of Section SurrealRecI
Beginning of Section SurrealRecII
Variable F : set → (set → (set → set → (set → set
Let G : set → (set → set → (set → set → set → (set → set λalpha g ⇒ If_iii (ordinal alpha (λz : set ⇒ If_ii (z ∈ SNoS_ (ordsucc alpha (F z (λw ⇒ g (SNoLev w w ) default ) (λz : set ⇒ default ) Primitive . The name
SNo_rec_ii is a term of type
set → (set → set .
Hypothesis Fr : ∀z, SNo z ∀g h : set → (set → set (∀ w ∈ SNoS_ (SNoLev z , g w = h w → F z g = F z h End of Section SurrealRecII
Beginning of Section SurrealRec2
Variable F : set → set → (set → set → set → set
Let G : set → (set → set → set → set → (set → set → set λw f z g ⇒ F w z (λx y ⇒ if x = w then g y else f x y ) Primitive . The name
SNo_rec2 is a term of type
set → set → set .
Axiom. (
SNo_rec2_eq ) We take the following as an axiom:
End of Section SurrealRec2
Axiom. (
SNoLev_ind ) We take the following as an axiom:
Axiom. (
SNoLev_ind2 ) We take the following as an axiom:
Axiom. (
SNoLev_ind3 ) We take the following as an axiom:
∀P : set → set → set → prop (∀x y z, SNo x SNo y SNo z (∀ u ∈ SNoS_ (SNoLev x , P u y z → (∀ v ∈ SNoS_ (SNoLev y , P x v z → (∀ w ∈ SNoS_ (SNoLev z , P x y w → (∀ u ∈ SNoS_ (SNoLev x , ∀ v ∈ SNoS_ (SNoLev y , P u v z → (∀ u ∈ SNoS_ (SNoLev x , ∀ w ∈ SNoS_ (SNoLev z , P u y w → (∀ v ∈ SNoS_ (SNoLev y , ∀ w ∈ SNoS_ (SNoLev z , P x v w → (∀ u ∈ SNoS_ (SNoLev x , ∀ v ∈ SNoS_ (SNoLev y , ∀ w ∈ SNoS_ (SNoLev z , P u v w → P x y z ) → ∀x y z, SNo x SNo y SNo z P x y z Axiom. (
SNo_omega ) We take the following as an axiom:
Axiom. (
SNoLt_0_1 ) We take the following as an axiom:
Axiom. (
SNoLt_0_2 ) We take the following as an axiom:
Axiom. (
SNoLt_1_2 ) We take the following as an axiom:
Axiom. (
restr_SNo_ ) We take the following as an axiom:
Axiom. (
restr_SNo ) We take the following as an axiom:
Axiom. (
restr_SNoEq ) We take the following as an axiom:
Beginning of Section SurrealMinus
Primitive . The name
minus_SNo is a term of type
set → set .
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo .
Notation . We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLe .
End of Section SurrealMinus
Beginning of Section SurrealAdd
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo .
Primitive . The name
add_SNo is a term of type
set → set → set .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo .
Axiom. (
add_SNo_eq ) We take the following as an axiom:
Axiom. (
SNo_add_SNo ) We take the following as an axiom:
Axiom. (
add_SNo_Lt1 ) We take the following as an axiom:
Axiom. (
add_SNo_Le1 ) We take the following as an axiom:
Axiom. (
add_SNo_Lt2 ) We take the following as an axiom:
Axiom. (
add_SNo_Le2 ) We take the following as an axiom:
Axiom. (
add_SNo_Lt3 ) We take the following as an axiom:
Axiom. (
add_SNo_Le3 ) We take the following as an axiom:
Axiom. (
add_SNo_com ) We take the following as an axiom:
Axiom. (
add_SNo_0L ) We take the following as an axiom:
Axiom. (
add_SNo_0R ) We take the following as an axiom:
Axiom. (
minus_SNo_0 ) We take the following as an axiom:
Axiom. (
add_SNo_Lt4 ) We take the following as an axiom:
End of Section SurrealAdd
Beginning of Section SurrealMul
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo .
Axiom. (
mul_SNo_eq ) We take the following as an axiom:
Axiom. (
mul_SNo_eq_2 ) We take the following as an axiom:
∀x y, SNo x SNo y ∀p : prop , (∀L R, (∀u, u ∈ L (∀q : prop , (∀ w0 ∈ SNoL x , ∀ w1 ∈ SNoL y , u = w0 * y + x * w1 + - w0 * w1 q → (∀ z0 ∈ SNoR x , ∀ z1 ∈ SNoR y , u = z0 * y + x * z1 + - z0 * z1 q → q ) ) → (∀ w0 ∈ SNoL x , ∀ w1 ∈ SNoL y , w0 * y + x * w1 + - w0 * w1 ∈ L → (∀ z0 ∈ SNoR x , ∀ z1 ∈ SNoR y , z0 * y + x * z1 + - z0 * z1 ∈ L → (∀u, u ∈ R (∀q : prop , (∀ w0 ∈ SNoL x , ∀ z1 ∈ SNoR y , u = w0 * y + x * z1 + - w0 * z1 q → (∀ z0 ∈ SNoR x , ∀ w1 ∈ SNoL y , u = z0 * y + x * w1 + - z0 * w1 q → q ) ) → (∀ w0 ∈ SNoL x , ∀ z1 ∈ SNoR y , w0 * y + x * z1 + - w0 * z1 ∈ R → (∀ z0 ∈ SNoR x , ∀ w1 ∈ SNoL y , z0 * y + x * w1 + - z0 * w1 ∈ R → x * y = SNoCut L R p ) → p Axiom. (
mul_SNo_prop_1 ) We take the following as an axiom:
∀x, SNo x ∀y, SNo y ∀p : prop , (SNo (x * y (∀ u ∈ SNoL x , ∀ v ∈ SNoL y , u * y + x * v < x * y + u * v → (∀ u ∈ SNoR x , ∀ v ∈ SNoR y , u * y + x * v < x * y + u * v → (∀ u ∈ SNoL x , ∀ v ∈ SNoR y , x * y + u * v < u * y + x * v → (∀ u ∈ SNoR x , ∀ v ∈ SNoL y , x * y + u * v < u * y + x * v → p → p Axiom. (
SNo_mul_SNo ) We take the following as an axiom:
Axiom. (
mul_SNo_eq_3 ) We take the following as an axiom:
∀x y, SNo x SNo y ∀p : prop , (∀L R, SNoCutP L R (∀u, u ∈ L (∀q : prop , (∀ w0 ∈ SNoL x , ∀ w1 ∈ SNoL y , u = w0 * y + x * w1 + - w0 * w1 q → (∀ z0 ∈ SNoR x , ∀ z1 ∈ SNoR y , u = z0 * y + x * z1 + - z0 * z1 q → q ) ) → (∀ w0 ∈ SNoL x , ∀ w1 ∈ SNoL y , w0 * y + x * w1 + - w0 * w1 ∈ L → (∀ z0 ∈ SNoR x , ∀ z1 ∈ SNoR y , z0 * y + x * z1 + - z0 * z1 ∈ L → (∀u, u ∈ R (∀q : prop , (∀ w0 ∈ SNoL x , ∀ z1 ∈ SNoR y , u = w0 * y + x * z1 + - w0 * z1 q → (∀ z0 ∈ SNoR x , ∀ w1 ∈ SNoL y , u = z0 * y + x * w1 + - z0 * w1 q → q ) ) → (∀ w0 ∈ SNoL x , ∀ z1 ∈ SNoR y , w0 * y + x * z1 + - w0 * z1 ∈ R → (∀ z0 ∈ SNoR x , ∀ w1 ∈ SNoL y , z0 * y + x * w1 + - z0 * w1 ∈ R → x * y = SNoCut L R p ) → p Axiom. (
mul_SNo_Lt ) We take the following as an axiom:
Axiom. (
mul_SNo_Le ) We take the following as an axiom:
Axiom. (
mul_SNo_Subq_lem ) We take the following as an axiom:
∀x y X Y Z W, ∀U U', (∀u, u ∈ U (∀q : prop , (∀ w0 ∈ X , ∀ w1 ∈ Y , u = w0 * y + x * w1 + - w0 * w1 q → (∀ z0 ∈ Z , ∀ z1 ∈ W , u = z0 * y + x * z1 + - z0 * z1 q → q ) ) → (∀ w0 ∈ X , ∀ w1 ∈ Y , w0 * y + x * w1 + - w0 * w1 ∈ U' → (∀ w0 ∈ Z , ∀ w1 ∈ W , w0 * y + x * w1 + - w0 * w1 ∈ U' → U ⊆ U' Axiom. (
mul_SNo_com ) We take the following as an axiom:
Beginning of Section mul_SNo_assoc_lems
Variable M : set → set → set
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
M .
Hypothesis SNo_M : ∀x y, SNo x SNo y SNo (x * y Hypothesis DL : ∀x y z, SNo x SNo y SNo z x * (y + z = x * y + x * z Hypothesis DR : ∀x y z, SNo x SNo y SNo z (x + y * z = x * z + y * z Hypothesis M_Lt : ∀x y u v, SNo x SNo y SNo u SNo v u < x v < y u * y + x * v < x * y + u * v Hypothesis M_Le : ∀x y u v, SNo x SNo y SNo u SNo v u ≤ x v ≤ y u * y + x * v ≤ x * y + u * v Axiom. (
mul_SNo_assoc_lem1 ) We take the following as an axiom:
∀x y z, SNo x SNo y SNo z (∀ u ∈ SNoS_ (SNoLev x , u * (y * z = (u * y * z → (∀ v ∈ SNoS_ (SNoLev y , x * (v * z = (x * v * z → (∀ w ∈ SNoS_ (SNoLev z , x * (y * w = (x * y * w → (∀ u ∈ SNoS_ (SNoLev x , ∀ v ∈ SNoS_ (SNoLev y , u * (v * z = (u * v * z → (∀ u ∈ SNoS_ (SNoLev x , ∀ w ∈ SNoS_ (SNoLev z , u * (y * w = (u * y * w → (∀ v ∈ SNoS_ (SNoLev y , ∀ w ∈ SNoS_ (SNoLev z , x * (v * w = (x * v * w → (∀ u ∈ SNoS_ (SNoLev x , ∀ v ∈ SNoS_ (SNoLev y , ∀ w ∈ SNoS_ (SNoLev z , u * (v * w = (u * v * w → ∀L, (∀ u ∈ L , ∀q : prop , (∀ v ∈ SNoL x , ∀ w ∈ SNoL (y * z , u = v * (y * z + x * w + - v * w q → (∀ v ∈ SNoR x , ∀ w ∈ SNoR (y * z , u = v * (y * z + x * w + - v * w q → q → ∀ u ∈ L , u < (x * y * z Axiom. (
mul_SNo_assoc_lem2 ) We take the following as an axiom:
∀x y z, SNo x SNo y SNo z (∀ u ∈ SNoS_ (SNoLev x , u * (y * z = (u * y * z → (∀ v ∈ SNoS_ (SNoLev y , x * (v * z = (x * v * z → (∀ w ∈ SNoS_ (SNoLev z , x * (y * w = (x * y * w → (∀ u ∈ SNoS_ (SNoLev x , ∀ v ∈ SNoS_ (SNoLev y , u * (v * z = (u * v * z → (∀ u ∈ SNoS_ (SNoLev x , ∀ w ∈ SNoS_ (SNoLev z , u * (y * w = (u * y * w → (∀ v ∈ SNoS_ (SNoLev y , ∀ w ∈ SNoS_ (SNoLev z , x * (v * w = (x * v * w → (∀ u ∈ SNoS_ (SNoLev x , ∀ v ∈ SNoS_ (SNoLev y , ∀ w ∈ SNoS_ (SNoLev z , u * (v * w = (u * v * w → ∀R, (∀ u ∈ R , ∀q : prop , (∀ v ∈ SNoL x , ∀ w ∈ SNoR (y * z , u = v * (y * z + x * w + - v * w q → (∀ v ∈ SNoR x , ∀ w ∈ SNoL (y * z , u = v * (y * z + x * w + - v * w q → q → ∀ u ∈ R , (x * y * z < u End of Section mul_SNo_assoc_lems
Axiom. (
SNo_foil ) We take the following as an axiom:
Axiom. (
SNo_foil_mm ) We take the following as an axiom:
End of Section SurrealMul
Beginning of Section SurrealExp
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo .
Notation . We use
^ as an infix operator with priority 342 and which associates to the right corresponding to applying term
exp_SNo_nat .
Axiom. (
eps_bd_1 ) We take the following as an axiom:
Axiom. (
SNoS_finite ) We take the following as an axiom:
End of Section SurrealExp
Beginning of Section Int
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo .
Primitive . The name
int is a term of type
set .
Axiom. (
int_SNo ) We take the following as an axiom:
Axiom. (
int_add_SNo ) We take the following as an axiom:
Axiom. (
int_mul_SNo ) We take the following as an axiom:
End of Section Int
Beginning of Section SurrealAbs
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo .
Axiom. (
abs_SNo_0 ) We take the following as an axiom:
Axiom. (
pos_abs_SNo ) We take the following as an axiom:
Axiom. (
neg_abs_SNo ) We take the following as an axiom:
Axiom. (
SNo_abs_SNo ) We take the following as an axiom:
Axiom. (
abs_SNo_Lev ) We take the following as an axiom:
End of Section SurrealAbs
Beginning of Section SNoMaxMin
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo .
Notation . We use
^ as an infix operator with priority 342 and which associates to the right corresponding to applying term
exp_SNo_nat .
Notation . We use
< as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLt .
Notation . We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLe .
End of Section SNoMaxMin
Beginning of Section DiadicRationals
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo .
Notation . We use
< as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLt .
Notation . We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLe .
Notation . We use
^ as an infix operator with priority 342 and which associates to the right corresponding to applying term
exp_SNo_nat .
End of Section DiadicRationals
Beginning of Section SurrealDiv
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo .
Notation . We use
< as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLt .
Notation . We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLe .
Notation . We use
^ as an infix operator with priority 342 and which associates to the right corresponding to applying term
exp_SNo_nat .
Definition. We define
SNo_recipauxset to be
λY x X g ⇒ ⋃ y ∈ Y { (1 + (x' + - x * y * g x' | x' ∈ X } of type
set → set → set → (set → set → set .
Beginning of Section recip_SNo_pos
End of Section recip_SNo_pos
Axiom. (
recip_SNo_0 ) We take the following as an axiom:
Axiom. (
recip_SNo_1 ) We take the following as an axiom:
Axiom. (
recip_SNo_2 ) We take the following as an axiom:
Notation . We use
:/: as an infix operator with priority 353 and no associativity corresponding to applying term
div_SNo .
Axiom. (
SNo_div_SNo ) We take the following as an axiom:
Axiom. (
div_div_SNo ) We take the following as an axiom:
End of Section SurrealDiv
Beginning of Section SurrealSqrt
Notation . We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo .
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo .
Notation . We use
:/: as an infix operator with priority 353 and no associativity corresponding to applying term
div_SNo .
Notation . We use
< as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLt .
Notation . We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLe .
Notation . We use
^ as an infix operator with priority 342 and which associates to the right corresponding to applying term
exp_SNo_nat .
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 .
Primitive . The name
real is a term of type
set .
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_ ω ω , (∀ n ∈ ω , f n < x → (∀ n ∈ ω , x < f n + eps_ n → (∀ n ∈ ω , ∀ i ∈ n , f i < f n → (∀ n ∈ ω , g n + - eps_ n < x → (∀ n ∈ ω , x < g n → (∀ n ∈ ω , ∀ i ∈ n , g n < g i → SNoCutP { f n | n ∈ ω } { g n | n ∈ ω } x = SNoCut { f n | n ∈ ω } { g n | n ∈ ω } p → p End of Section Reals
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 .
Definition. We define
pair_tag to be
λx y ⇒ x ∪ { u '' | u ∈ y } of type
set → set → set .
Variable F : set → prop
Hypothesis extension_tag_fresh : ∀x, F x ∀ u ∈ x , extension_tag ∉ u
Proof: Let x and y be given.
Assume Hx : F x
Apply extension_tag_fresh x Hx (y '' H1 to the current goal.
We will
prove extension_tag ∈ y '' .
We will
prove extension_tag ∈ y ∪ { extension_tag } .
Apply SingI to the current goal.
∎
Proof: Let x and y be given.
Assume Hx .
Let u be given.
Assume Hu .
Let v be given.
Assume Huv .
Let w be given.
We prove the intermediate
claim L1 :
w ∈ v '' .
rewrite the current goal using Huv
We will
prove w ∈ u ∪ { extension_tag } .
An exact proof term for the current goal is Hw
Apply binunionE v { extension_tag } w L1 to the current goal.
An exact proof term for the current goal is H1
We prove the intermediate
claim L2 :
w = extension_tag .
An
exact proof term for the current goal is
SingE extension_tag w H1 .
Apply extension_tag_fresh x Hx u Hu
We will
prove extension_tag ∈ u .
rewrite the current goal using L2
An exact proof term for the current goal is Hw
∎
Proof: Let x and y be given.
Assume Hx Hy .
Let u be given.
Assume Hu .
Let v be given.
Assume Hv Huv .
Use symmetry.
An exact proof term for the current goal is Huv
∎
Proof: Let x1, y1, x2 and y2 be given.
Assume Hx1 .
Let v be given.
We prove the intermediate
claim L1 :
v ∈ pair_tag x2 y2 .
rewrite the current goal using H1
An exact proof term for the current goal is Hv
An exact proof term for the current goal is H2
Let u be given.
rewrite the current goal using Hvu
An exact proof term for the current goal is Hv
∎
Proof: Let x1, y1, x2 and y2 be given.
Assume Hx1 Hx2 .
Use symmetry.
An exact proof term for the current goal is H1
∎
Proof: Let x1, y1, x2 and y2 be given.
Assume Hy1 Hx2 Hy2 .
Let v be given.
We prove the intermediate
claim L1 :
v '' ∈ pair_tag x2 y2 .
rewrite the current goal using H1
An
exact proof term for the current goal is
ReplI y1 (λu ⇒ u '' ) v Hv .
Let u be given.
We prove the intermediate
claim L2 :
v = u .
An
exact proof term for the current goal is
ctagged_eqE_eq y1 y2 Hy1 Hy2 v Hv u Hu Hvu .
rewrite the current goal using L2
An exact proof term for the current goal is Hu
∎
Proof: Let x1, y1, x2 and y2 be given.
Assume Hx1 Hy1 Hx2 Hy2 .
Use symmetry.
An exact proof term for the current goal is H1
∎
Proof: Let x be given.
rewrite the current goal using
Repl_Empty (λu ⇒ u '' ) (from left to right).
∎
Theorem. (
CD_carr_I ) The following is provable:
Proof: Let x and y be given.
Assume Hx Hy .
We use x witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hx
We use y witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hy
∎
Theorem. (
CD_carr_E ) The following is provable:
Proof: Let z be given.
Assume Hz .
Let p be given.
Assume Hp .
Apply Hz
Let x be given.
Assume H1 .
Apply H1
Assume Hx .
Assume H1 .
Apply H1
Let y be given.
Assume H1 .
Apply H1
Assume Hy Hzxy .
rewrite the current goal using Hzxy
An exact proof term for the current goal is Hp x y Hx Hy Hzxy
∎
Proof: Assume H0 .
Let x be given.
Assume Hx .
We use x witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hx
We use
0 to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H0
Use symmetry.
An
exact proof term for the current goal is
pair_tag_0 x .
∎
Proof: Let z be given.
Assume Hz .
Apply Eps_i_ex (λx ⇒ F x ∧ ∃ y, F y ∧ z = pa x y ) to the current goal.
We will
prove ∃ x, F x ∧ ∃ y, F y ∧ z = pa x y .
An exact proof term for the current goal is Hz
∎
Theorem. (
CD_proj0_2 ) The following is provable:
∀x y, F x F y proj0 (pa x y = x Proof: Let x and y be given.
Assume Hx Hy .
Apply H2
Let y' be given.
Assume H3 .
Apply H3
Assume Hy' : F y'
Use symmetry.
∎
Proof: Let z be given.
Assume Hz .
Let x and y be given.
Assume Hx Hy .
We use y witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hy
We will
prove pa x y = pa (proj0 (pa x y y .
Apply CD_proj0_2 x y Hx Hy (λu v ⇒ pa x y = pa v y ) to the current goal.
We will
prove pa x y = pa x y .
Use reflexivity.
∎
Theorem. (
CD_proj1_2 ) The following is provable:
∀x y, F x F y proj1 (pa x y = y Proof: Let x and y be given.
Assume Hx Hy .
Use symmetry.
∎
Theorem. (
CD_proj0R ) The following is provable:
Proof: Let z be given.
Assume Hz .
An exact proof term for the current goal is (λH _ ⇒ H )
∎
Theorem. (
CD_proj1R ) The following is provable:
Proof: Let z be given.
Assume Hz .
An exact proof term for the current goal is (λH _ ⇒ H )
∎
Proof: Let z be given.
Assume Hz .
An exact proof term for the current goal is (λ_ H ⇒ H )
∎
Proof: Let z and w be given.
Assume Hz Hw .
Assume H1 H2 .
Use transitivity with and
(pa (proj0 z (proj1 z .
Use transitivity with and
(pa (proj0 w (proj1 w .
rewrite the current goal using H1
rewrite the current goal using H2
Use reflexivity.
∎
Proof: Assume H0 .
Let x be given.
Assume Hx .
rewrite the current goal using
pair_tag_0 x (from right to left) at position 1.
An
exact proof term for the current goal is
CD_proj0_2 x 0 Hx H0 .
∎
Proof: Assume H0 .
Let x be given.
Assume Hx .
rewrite the current goal using
pair_tag_0 x (from right to left) at position 1.
An
exact proof term for the current goal is
CD_proj1_2 x 0 Hx H0 .
∎
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
Proof: Let z be given.
Assume Hz .
Apply F_minus
An exact proof term for the current goal is Hz
Apply F_minus
An exact proof term for the current goal is Hz
∎
Proof: Let z be given.
Assume Hz .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
We prove the intermediate
claim Lmp0z :
F (- proj0 z .
Apply F_minus
An exact proof term for the current goal is Lp0z
We prove the intermediate
claim Lmp1z :
F (- proj1 z .
Apply F_minus
An exact proof term for the current goal is Lp1z
∎
Proof: Let z be given.
Assume Hz .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
We prove the intermediate
claim Lmp0z :
F (- proj0 z .
Apply F_minus
An exact proof term for the current goal is Lp0z
We prove the intermediate
claim Lmp1z :
F (- proj1 z .
Apply F_minus
An exact proof term for the current goal is Lp1z
∎
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
Proof: Let z be given.
Assume Hz .
Apply F_conj
An exact proof term for the current goal is Hz
Apply F_minus
An exact proof term for the current goal is Hz
∎
Proof: Let z be given.
Assume Hz .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
We prove the intermediate
claim Lcp0z :
F (conj (proj0 z .
Apply F_conj
An exact proof term for the current goal is Lp0z
We prove the intermediate
claim Lmp1z :
F (- proj1 z .
Apply F_minus
An exact proof term for the current goal is Lp1z
∎
Proof: Let z be given.
Assume Hz .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
We prove the intermediate
claim Lcp0z :
F (conj (proj0 z .
Apply F_conj
An exact proof term for the current goal is Lp0z
We prove the intermediate
claim Lmp1z :
F (- proj1 z .
Apply F_minus
An exact proof term for the current goal is Lp1z
∎
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 Theorem. (
CD_add_CD ) The following is provable:
Proof: Let z and w be given.
Assume Hz Hw .
Apply F_add
An exact proof term for the current goal is Hz
An exact proof term for the current goal is Hw
Apply F_add
An exact proof term for the current goal is Hz
An exact proof term for the current goal is Hw
∎
Proof: Let z and w be given.
Assume Hz Hw .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
We prove the intermediate
claim Lp0w :
F (proj0 w .
An
exact proof term for the current goal is
CD_proj0R w Hw .
We prove the intermediate
claim Lp1w :
F (proj1 w .
An
exact proof term for the current goal is
CD_proj1R w Hw .
We prove the intermediate
claim Lp0zw :
F (proj0 z + proj0 w .
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1zw :
F (proj1 z + proj1 w .
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
∎
Proof: Let z and w be given.
Assume Hz Hw .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
We prove the intermediate
claim Lp0w :
F (proj0 w .
An
exact proof term for the current goal is
CD_proj0R w Hw .
We prove the intermediate
claim Lp1w :
F (proj1 w .
An
exact proof term for the current goal is
CD_proj1R w Hw .
We prove the intermediate
claim Lp0zw :
F (proj0 z + proj0 w .
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1zw :
F (proj1 z + proj1 w .
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
∎
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 Theorem. (
CD_mul_CD ) The following is provable:
Proof: Let z and w be given.
Assume Hz Hw .
Apply F_add
Apply F_mul
An exact proof term for the current goal is Hz
An exact proof term for the current goal is Hw
Apply F_minus
Apply F_mul
Apply F_conj
An exact proof term for the current goal is Hw
An exact proof term for the current goal is Hz
Apply F_add
Apply F_mul
An exact proof term for the current goal is Hw
An exact proof term for the current goal is Hz
Apply F_mul
An exact proof term for the current goal is Hz
Apply F_conj
An exact proof term for the current goal is Hw
∎
Proof: Let z and w be given.
Assume Hz Hw .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
We prove the intermediate
claim Lp0w :
F (proj0 w .
An
exact proof term for the current goal is
CD_proj0R w Hw .
We prove the intermediate
claim Lp1w :
F (proj1 w .
An
exact proof term for the current goal is
CD_proj1R w Hw .
We prove the intermediate
claim Lcp0w :
F (conj (proj0 w .
Apply F_conj
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1w :
F (conj (proj1 w .
Apply F_conj
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp0zp0w :
F (proj0 z * proj0 w .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1wp1z :
F (conj (proj1 w * proj1 z .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1wp1z :
F (- conj (proj1 w * proj1 z .
Apply F_minus
An exact proof term for the current goal is ??
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1wp0z :
F (proj1 w * proj0 z .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1zcp0w :
F (proj1 z * conj (proj0 w .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
∎
Proof: Let z and w be given.
Assume Hz Hw .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
We prove the intermediate
claim Lp0w :
F (proj0 w .
An
exact proof term for the current goal is
CD_proj0R w Hw .
We prove the intermediate
claim Lp1w :
F (proj1 w .
An
exact proof term for the current goal is
CD_proj1R w Hw .
We prove the intermediate
claim Lcp0w :
F (conj (proj0 w .
Apply F_conj
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1w :
F (conj (proj1 w .
Apply F_conj
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp0zp0w :
F (proj0 z * proj0 w .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1wp1z :
F (conj (proj1 w * proj1 z .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1wp1z :
F (- conj (proj1 w * proj1 z .
Apply F_minus
An exact proof term for the current goal is ??
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1wp0z :
F (proj1 w * proj0 z .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1zcp0w :
F (proj1 z * conj (proj0 w .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
∎
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
Proof: Let x be given.
Assume Hx .
rewrite the current goal using
CD_proj0_F F_0 x Hx (from left to right).
rewrite the current goal using
CD_proj1_F F_0 x Hx (from left to right).
rewrite the current goal using F_minus_0
We will
prove pa (- x 0 = - x .
An
exact proof term for the current goal is
pair_tag_0 (- x .
∎
Variable conj : set → set
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj .
Proof: Let x be given.
Assume Hx .
rewrite the current goal using
CD_proj0_F F_0 x Hx (from left to right).
rewrite the current goal using
CD_proj1_F F_0 x Hx (from left to right).
rewrite the current goal using F_minus_0
We will
prove pa (conj x 0 = conj x .
An
exact proof term for the current goal is
pair_tag_0 (conj x .
∎
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 Theorem. (
CD_add_F_eq ) The following is provable:
∀x y, F x F y x + y = x + y Proof: Let x and y be given.
Assume Hx Hy .
rewrite the current goal using
CD_proj0_F F_0 x Hx (from left to right).
rewrite the current goal using
CD_proj1_F F_0 x Hx (from left to right).
rewrite the current goal using
CD_proj0_F F_0 y Hy (from left to right).
rewrite the current goal using
CD_proj1_F F_0 y Hy (from left to right).
rewrite the current goal using F_add_0_0
We will
prove pa (x + y 0 = x + y .
An
exact proof term for the current goal is
pair_tag_0 (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 Theorem. (
CD_mul_F_eq ) The following is provable:
∀x y, F x F y x ⨯ y = x * y Proof: Let x and y be given.
Assume Hx Hy .
rewrite the current goal using
CD_proj0_F F_0 x Hx (from left to right).
rewrite the current goal using
CD_proj1_F F_0 x Hx (from left to right).
rewrite the current goal using
CD_proj0_F F_0 y Hy (from left to right).
rewrite the current goal using
CD_proj1_F F_0 y Hy (from left to right).
We will
prove pa (x * y + - conj 0 * 0 (0 * x + 0 * conj y = x * y .
rewrite the current goal using
F_mul_0R (conj 0 (F_conj 0 F_0 (from left to right).
rewrite the current goal using F_mul_0L x Hx
rewrite the current goal using F_mul_0L (conj y (F_conj y Hy
rewrite the current goal using F_minus_0
rewrite the current goal using
F_add_0R 0 F_0 (from left to right).
rewrite the current goal using
F_add_0R (x * y (F_mul x y Hx Hy (from left to right).
We will
prove pa (x * y 0 = x * y .
An
exact proof term for the current goal is
pair_tag_0 (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
Proof: Let z be given.
Assume Hz .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
We prove the intermediate
claim Lmp0z :
F (- proj0 z .
Apply F_minus
An exact proof term for the current goal is Lp0z
We prove the intermediate
claim Lmp1z :
F (- proj1 z .
Apply F_minus
An exact proof term for the current goal is Lp1z
rewrite the current goal using
F_minus_invol (proj0 z Lp0z (from left to right).
rewrite the current goal using
F_minus_invol (proj1 z Lp1z (from left to right).
Use symmetry.
∎
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
Proof: Let z be given.
Assume Hz .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
We prove the intermediate
claim Lcp0z :
F (conj (proj0 z .
Apply F_conj
An exact proof term for the current goal is Lp0z
We prove the intermediate
claim Lmp1z :
F (- proj1 z .
Apply F_minus
An exact proof term for the current goal is Lp1z
rewrite the current goal using
F_conj_invol (proj0 z Lp0z (from left to right).
rewrite the current goal using
F_minus_invol (proj1 z Lp1z (from left to right).
Use symmetry.
∎
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
Proof: Let z be given.
Assume Hz .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
We prove the intermediate
claim Lmp0z :
F (- proj0 z .
Apply F_minus
An exact proof term for the current goal is Lp0z
We prove the intermediate
claim Lmp1z :
F (- proj1 z .
Apply F_minus
An exact proof term for the current goal is Lp1z
We prove the intermediate
claim Lcp0z :
F (conj (proj0 z .
Apply F_conj
An exact proof term for the current goal is Lp0z
We prove the intermediate
claim Lcmp0z :
F (conj (- proj0 z .
Apply F_conj
An exact proof term for the current goal is Lmp0z
Use f_equal.
An
exact proof term for the current goal is
F_conj_minus (proj0 z ?? .
∎
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
Proof: Let z and w be given.
Assume Hz Hw .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
We prove the intermediate
claim Lmp0z :
F (- proj0 z .
Apply F_minus
An exact proof term for the current goal is Lp0z
We prove the intermediate
claim Lmp1z :
F (- proj1 z .
Apply F_minus
An exact proof term for the current goal is Lp1z
We prove the intermediate
claim Lp0w :
F (proj0 w .
An
exact proof term for the current goal is
CD_proj0R w Hw .
We prove the intermediate
claim Lp1w :
F (proj1 w .
An
exact proof term for the current goal is
CD_proj1R w Hw .
We prove the intermediate
claim Lmp0w :
F (- proj0 w .
Apply F_minus
An exact proof term for the current goal is Lp0w
We prove the intermediate
claim Lmp1w :
F (- proj1 w .
Apply F_minus
An exact proof term for the current goal is Lp1w
We prove the intermediate
claim Lp0zw :
F (proj0 z + proj0 w .
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1zw :
F (proj1 z + proj1 w .
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
Use f_equal.
Apply F_minus_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
Apply F_minus_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
∎
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
Proof: Let z and w be given.
Assume Hz Hw .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
We prove the intermediate
claim Lcp0z :
F (conj (proj0 z .
Apply F_conj
An exact proof term for the current goal is Lp0z
We prove the intermediate
claim Lmp1z :
F (- proj1 z .
Apply F_minus
An exact proof term for the current goal is Lp1z
We prove the intermediate
claim Lp0w :
F (proj0 w .
An
exact proof term for the current goal is
CD_proj0R w Hw .
We prove the intermediate
claim Lp1w :
F (proj1 w .
An
exact proof term for the current goal is
CD_proj1R w Hw .
We prove the intermediate
claim Lcp0w :
F (conj (proj0 w .
Apply F_conj
An exact proof term for the current goal is Lp0w
We prove the intermediate
claim Lmp1w :
F (- proj1 w .
Apply F_minus
An exact proof term for the current goal is Lp1w
We prove the intermediate
claim Lp0zw :
F (proj0 z + proj0 w .
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1zw :
F (proj1 z + proj1 w .
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
Use f_equal.
Apply F_conj_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
Apply F_minus_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
∎
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
Proof: Let z and w be given.
Assume Hz Hw .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
We prove the intermediate
claim Lp0w :
F (proj0 w .
An
exact proof term for the current goal is
CD_proj0R w Hw .
We prove the intermediate
claim Lp1w :
F (proj1 w .
An
exact proof term for the current goal is
CD_proj1R w Hw .
Use f_equal.
Apply F_add_com
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
Apply F_add_com
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
∎
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
Proof: Let z, w and u be given.
Assume Hz Hw Hu .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
We prove the intermediate
claim Lp0w :
F (proj0 w .
An
exact proof term for the current goal is
CD_proj0R w Hw .
We prove the intermediate
claim Lp1w :
F (proj1 w .
An
exact proof term for the current goal is
CD_proj1R w Hw .
We prove the intermediate
claim Lp0u :
F (proj0 u .
An
exact proof term for the current goal is
CD_proj0R u Hu .
We prove the intermediate
claim Lp1u :
F (proj1 u .
An
exact proof term for the current goal is
CD_proj1R u Hu .
We prove the intermediate
claim Lp0zw :
F (proj0 z + proj0 w .
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1zw :
F (proj1 z + proj1 w .
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp0wu :
F (proj0 w + proj0 u .
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1wu :
F (proj1 w + proj1 u .
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
Use f_equal.
Apply F_add_assoc
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 ??
Apply F_add_assoc
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 ??
∎
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 Theorem. (
CD_add_0R ) The following is provable:
Proof: Let z be given.
Assume Hz .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
rewrite the current goal using
CD_proj0_F F_0 0 F_0 (from left to right).
rewrite the current goal using
CD_proj1_F F_0 0 F_0 (from left to right).
rewrite the current goal using
F_add_0R (proj0 z ?? (from left to right).
rewrite the current goal using
F_add_0R (proj1 z ?? (from left to right).
Use symmetry.
∎
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 Theorem. (
CD_add_0L ) The following is provable:
Proof: Let z be given.
Assume Hz .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
rewrite the current goal using
CD_proj0_F F_0 0 F_0 (from left to right).
rewrite the current goal using
CD_proj1_F F_0 0 F_0 (from left to right).
rewrite the current goal using
F_add_0L (proj0 z ?? (from left to right).
rewrite the current goal using
F_add_0L (proj1 z ?? (from left to right).
Use symmetry.
∎
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
Proof: Let z be given.
Assume Hz .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
We prove the intermediate
claim Lmp0z :
F (- proj0 z .
Apply F_minus
An exact proof term for the current goal is Lp0z
We prove the intermediate
claim Lmp1z :
F (- proj1 z .
Apply F_minus
An exact proof term for the current goal is Lp1z
rewrite the current goal using
F_add_minus_linv (proj0 z Lp0z (from left to right).
rewrite the current goal using
F_add_minus_linv (proj1 z Lp1z (from left to right).
We will
prove pa 0 0 = 0 .
An
exact proof term for the current goal is
pair_tag_0 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
Proof: Let z be given.
Assume Hz .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
We prove the intermediate
claim Lmp0z :
F (- proj0 z .
Apply F_minus
An exact proof term for the current goal is Lp0z
We prove the intermediate
claim Lmp1z :
F (- proj1 z .
Apply F_minus
An exact proof term for the current goal is Lp1z
rewrite the current goal using
F_add_minus_rinv (proj0 z Lp0z (from left to right).
rewrite the current goal using
F_add_minus_rinv (proj1 z Lp1z (from left to right).
We will
prove pa 0 0 = 0 .
An
exact proof term for the current goal is
pair_tag_0 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 Theorem. (
CD_mul_0R ) The following is provable:
Proof: Let z be given.
Assume Hz .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
rewrite the current goal using
CD_proj0_F F_0 0 F_0 (from left to right).
rewrite the current goal using
CD_proj1_F F_0 0 F_0 (from left to right).
rewrite the current goal using F_conj_0
rewrite the current goal using
F_mul_0L (proj0 z ?? (from left to right).
rewrite the current goal using
F_mul_0L (proj1 z ?? (from left to right).
rewrite the current goal using
F_mul_0R (proj0 z ?? (from left to right).
rewrite the current goal using
F_mul_0R (proj1 z ?? (from left to right).
rewrite the current goal using F_minus_0
rewrite the current goal using F_add_0_0
We will
prove pa 0 0 = 0 .
An
exact proof term for the current goal is
pair_tag_0 0 .
∎
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 Theorem. (
CD_mul_0L ) The following is provable:
Proof: Let z be given.
Assume Hz .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
We prove the intermediate
claim Lcp0z :
F (conj (proj0 z .
Apply F_conj
An exact proof term for the current goal is Lp0z
We prove the intermediate
claim Lcp1z :
F (conj (proj1 z .
Apply F_conj
An exact proof term for the current goal is Lp1z
rewrite the current goal using
CD_proj0_F F_0 0 F_0 (from left to right).
rewrite the current goal using
CD_proj1_F F_0 0 F_0 (from left to right).
rewrite the current goal using
F_mul_0L (proj0 z ?? (from left to right).
rewrite the current goal using
F_mul_0L (conj (proj0 z ?? (from left to right).
rewrite the current goal using
F_mul_0R (conj (proj1 z ?? (from left to right).
rewrite the current goal using
F_mul_0R (proj1 z ?? (from left to right).
rewrite the current goal using F_minus_0
rewrite the current goal using F_add_0_0
We will
prove pa 0 0 = 0 .
An
exact proof term for the current goal is
pair_tag_0 0 .
∎
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 Theorem. (
CD_mul_1R ) The following is provable:
Proof: Let z be given.
Assume Hz .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
rewrite the current goal using
CD_proj0_F F_0 1 F_1 (from left to right).
rewrite the current goal using
CD_proj1_F F_0 1 F_1 (from left to right).
rewrite the current goal using F_conj_0
rewrite the current goal using F_conj_1
rewrite the current goal using
F_mul_1R (proj0 z ?? (from left to right).
rewrite the current goal using
F_mul_1R (proj1 z ?? (from left to right).
rewrite the current goal using
F_mul_0L (proj0 z ?? (from left to right).
rewrite the current goal using
F_mul_0L (proj1 z ?? (from left to right).
rewrite the current goal using F_minus_0
rewrite the current goal using
F_add_0L (proj1 z ?? (from left to right).
rewrite the current goal using
F_add_0R (proj0 z ?? (from left to right).
Use symmetry.
∎
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 Theorem. (
CD_mul_1L ) The following is provable:
Proof: Let z be given.
Assume Hz .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
We prove the intermediate
claim Lcp0z :
F (conj (proj0 z .
Apply F_conj
An exact proof term for the current goal is Lp0z
We prove the intermediate
claim Lcp1z :
F (conj (proj1 z .
Apply F_conj
An exact proof term for the current goal is Lp1z
rewrite the current goal using
CD_proj0_F F_0 1 F_1 (from left to right).
rewrite the current goal using
CD_proj1_F F_0 1 F_1 (from left to right).
rewrite the current goal using
F_mul_1L (proj0 z ?? (from left to right).
rewrite the current goal using
F_mul_1R (proj1 z ?? (from left to right).
rewrite the current goal using
F_mul_0L (conj (proj0 z ?? (from left to right).
rewrite the current goal using
F_mul_0R (conj (proj1 z ?? (from left to right).
rewrite the current goal using F_minus_0
rewrite the current goal using
F_add_0R (proj0 z ?? (from left to right).
rewrite the current goal using
F_add_0R (proj1 z ?? (from left to right).
Use symmetry.
∎
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
Proof: Let z and w be given.
Assume Hz Hw .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
We prove the intermediate
claim Lcp0z :
F (conj (proj0 z .
Apply F_conj
An exact proof term for the current goal is Lp0z
We prove the intermediate
claim Lcp1z :
F (conj (proj1 z .
Apply F_conj
An exact proof term for the current goal is Lp1z
We prove the intermediate
claim Lmcp1z :
F (- conj (proj1 z .
Apply F_minus
An exact proof term for the current goal is Lcp1z
We prove the intermediate
claim Lmp1z :
F (- proj1 z .
Apply F_minus
An exact proof term for the current goal is Lp1z
We prove the intermediate
claim Lp0w :
F (proj0 w .
An
exact proof term for the current goal is
CD_proj0R w Hw .
We prove the intermediate
claim Lp1w :
F (proj1 w .
An
exact proof term for the current goal is
CD_proj1R w Hw .
We prove the intermediate
claim Lcp0w :
F (conj (proj0 w .
Apply F_conj
An exact proof term for the current goal is Lp0w
We prove the intermediate
claim Lcp1w :
F (conj (proj1 w .
Apply F_conj
An exact proof term for the current goal is Lp1w
We prove the intermediate
claim Lmp1w :
F (- proj1 w .
Apply F_minus
An exact proof term for the current goal is Lp1w
We prove the intermediate
claim Lp0zp0w :
F (proj0 z * proj0 w .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1wp1z :
F (conj (proj1 w * proj1 z .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1wp1z :
F (- conj (proj1 w * proj1 z .
Apply F_minus
An exact proof term for the current goal is ??
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1wp0z :
F (proj1 w * proj0 z .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1zcp0w :
F (proj1 z * conj (proj0 w .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp0w' :
F (proj0 w' .
We prove the intermediate
claim Lp1w' :
F (proj1 w' .
We prove the intermediate
claim Lp0z' :
F (proj0 z' .
We prove the intermediate
claim Lp1z' :
F (proj1 z' .
We prove the intermediate
claim Lcp0z' :
F (conj (proj0 z' .
Apply F_conj
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1z' :
F (conj (proj1 z' .
Apply F_conj
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp0w'p0z' :
F (proj0 w' * proj0 z' .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1z'p1w' :
F (conj (proj1 z' * proj1 w' .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1z'p1w' :
F (- conj (proj1 z' * proj1 w' .
Apply F_minus
An exact proof term for the current goal is ??
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1z'p0w' :
F (proj1 z' * proj0 w' .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1w'cp0z' :
F (proj1 w' * conj (proj0 z' .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1zp1w :
F (conj (proj1 z * proj1 w .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lmp1zcp0w :
F ((- proj1 z * (conj (proj0 w .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lmp1wp0z :
F ((- proj1 w * proj0 z .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
Use f_equal.
rewrite the current goal using
F_conj_add (proj0 z * proj0 w (- conj (proj1 w * proj1 z ?? ?? (from left to right).
Use f_equal.
An
exact proof term for the current goal is
F_conj_mul (proj0 z (proj0 w ?? ?? .
rewrite the current goal using
F_conj_minus (conj (proj1 w * proj1 z ?? (from left to right).
Use f_equal.
rewrite the current goal using
F_conj_mul (conj (proj1 w (proj1 z ?? ?? (from left to right).
rewrite the current goal using
F_conj_invol (proj1 w ?? (from left to right).
rewrite the current goal using
F_conj_minus (proj1 z ?? (from left to right).
rewrite the current goal using
F_minus_mul_distrR (- conj (proj1 z (proj1 w ?? ?? (from left to right).
rewrite the current goal using
F_minus_mul_distrL (conj (proj1 z (proj1 w ?? ?? (from left to right).
Use symmetry.
Apply F_minus_invol (conj (proj1 z * proj1 w ?? to the current goal.
rewrite the current goal using
F_conj_invol (proj0 z ?? (from left to right).
rewrite the current goal using
F_minus_add (proj1 w * proj0 z (proj1 z * conj (proj0 w ?? ?? (from left to right).
rewrite the current goal using
F_add_com ((- proj1 z * (conj (proj0 w ((- proj1 w * proj0 z ?? ?? (from left to right).
Use f_equal.
Use symmetry.
An
exact proof term for the current goal is
F_minus_mul_distrL (proj1 w (proj0 z ?? ?? .
Use symmetry.
An
exact proof term for the current goal is
F_minus_mul_distrL (proj1 z (conj (proj0 w ?? ?? .
∎
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
Proof: We prove the intermediate
claim L_add_4_inner_mid :
∀x y z w, F x F y F z F w (x + y + (z + w = (x + z + (y + w .
Let x, y, z and w be given.
Assume Hx Hy Hz Hw .
rewrite the current goal using
F_add_assoc (x + y z w (F_add x y Hx Hy Hz Hw (from right to left).
We will
prove ((x + y + z + w = (x + z + (y + w .
rewrite the current goal using F_add_assoc x y z Hx Hy Hz
We will
prove (x + (y + z + w = (x + z + (y + w .
rewrite the current goal using F_add_com y z Hy Hz
We will
prove (x + (z + y + w = (x + z + (y + w .
rewrite the current goal using F_add_assoc x z y Hx Hz Hy
We will
prove ((x + z + y + w = (x + z + (y + w .
An
exact proof term for the current goal is
F_add_assoc (x + z y w (F_add x z Hx Hz Hy Hw .
Let z, w and u be given.
Assume Hz Hw Hu .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
We prove the intermediate
claim Lp0w :
F (proj0 w .
An
exact proof term for the current goal is
CD_proj0R w Hw .
We prove the intermediate
claim Lp1w :
F (proj1 w .
An
exact proof term for the current goal is
CD_proj1R w Hw .
We prove the intermediate
claim Lp0u :
F (proj0 u .
An
exact proof term for the current goal is
CD_proj0R u Hu .
We prove the intermediate
claim Lp1u :
F (proj1 u .
An
exact proof term for the current goal is
CD_proj1R u Hu .
We prove the intermediate
claim Lp0zw :
F (proj0 z + proj0 w .
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1zw :
F (proj1 z + proj1 w .
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp0u :
F (conj (proj0 u .
Apply F_conj
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1u :
F (conj (proj1 u .
Apply F_conj
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp0zp0u :
F (proj0 z * proj0 u .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1up1z :
F (conj (proj1 u * proj1 z .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1up1z :
F (- conj (proj1 u * proj1 z .
Apply F_minus
An exact proof term for the current goal is ??
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1up0z :
F (proj1 u * proj0 z .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1zcp0u :
F (proj1 z * conj (proj0 u .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp0wp0u :
F (proj0 w * proj0 u .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1up1w :
F (conj (proj1 u * proj1 w .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1up1w :
F (- conj (proj1 u * proj1 w .
Apply F_minus
An exact proof term for the current goal is ??
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1up0w :
F (proj1 u * proj0 w .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1wcp0u :
F (proj1 w * conj (proj0 u .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
Use f_equal.
Use f_equal.
Apply F_add_mul_distrR
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
F_minus_add (conj (proj1 u * proj1 z (conj (proj1 u * proj1 w ?? ?? (from right to left).
Use f_equal.
Apply F_add_mul_distrL
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.
Apply F_add_mul_distrL
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 ??
Apply F_add_mul_distrR
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 ??
∎
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
Proof: We prove the intermediate
claim L_add_4_inner_mid :
∀x y z w, F x F y F z F w (x + y + (z + w = (x + z + (y + w .
Let x, y, z and w be given.
Assume Hx Hy Hz Hw .
rewrite the current goal using
F_add_assoc (x + y z w (F_add x y Hx Hy Hz Hw (from right to left).
We will
prove ((x + y + z + w = (x + z + (y + w .
rewrite the current goal using F_add_assoc x y z Hx Hy Hz
We will
prove (x + (y + z + w = (x + z + (y + w .
rewrite the current goal using F_add_com y z Hy Hz
We will
prove (x + (z + y + w = (x + z + (y + w .
rewrite the current goal using F_add_assoc x z y Hx Hz Hy
We will
prove ((x + z + y + w = (x + z + (y + w .
An
exact proof term for the current goal is
F_add_assoc (x + z y w (F_add x z Hx Hz Hy Hw .
Let z, w and u be given.
Assume Hz Hw Hu .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
We prove the intermediate
claim Lp0w :
F (proj0 w .
An
exact proof term for the current goal is
CD_proj0R w Hw .
We prove the intermediate
claim Lp1w :
F (proj1 w .
An
exact proof term for the current goal is
CD_proj1R w Hw .
We prove the intermediate
claim Lp0u :
F (proj0 u .
An
exact proof term for the current goal is
CD_proj0R u Hu .
We prove the intermediate
claim Lp1u :
F (proj1 u .
An
exact proof term for the current goal is
CD_proj1R u Hu .
We prove the intermediate
claim Lp0wu :
F (proj0 w + proj0 u .
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1wu :
F (proj1 w + proj1 u .
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp0w :
F (conj (proj0 w .
Apply F_conj
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1w :
F (conj (proj1 w .
Apply F_conj
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp0u :
F (conj (proj0 u .
Apply F_conj
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1u :
F (conj (proj1 u .
Apply F_conj
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp0zp0w :
F (proj0 z * proj0 w .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1wp1z :
F (conj (proj1 w * proj1 z .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1wp1z :
F (- conj (proj1 w * proj1 z .
Apply F_minus
An exact proof term for the current goal is ??
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1wp0z :
F (proj1 w * proj0 z .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1zcp0w :
F (proj1 z * conj (proj0 w .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp0zp0u :
F (proj0 z * proj0 u .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1up1z :
F (conj (proj1 u * proj1 z .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1up1z :
F (- conj (proj1 u * proj1 z .
Apply F_minus
An exact proof term for the current goal is ??
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1up0z :
F (proj1 u * proj0 z .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1zcp0u :
F (proj1 z * conj (proj0 u .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
Use f_equal.
Use f_equal.
Apply F_add_mul_distrL
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
F_conj_add (proj1 w (proj1 u ?? ?? (from left to right).
rewrite the current goal using
F_add_mul_distrR (conj (proj1 w (conj (proj1 u (proj1 z ?? ?? ?? (from left to right).
Apply F_minus_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
Use f_equal.
Apply F_add_mul_distrR
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
F_conj_add (proj0 w (proj0 u ?? ?? (from left to right).
Apply F_add_mul_distrL
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 ??
∎
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
Proof: Let z and w be given.
Assume Hz Hw .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
We prove the intermediate
claim Lp0w :
F (proj0 w .
An
exact proof term for the current goal is
CD_proj0R w Hw .
We prove the intermediate
claim Lp1w :
F (proj1 w .
An
exact proof term for the current goal is
CD_proj1R w Hw .
We prove the intermediate
claim Lmp0w :
F (- proj0 w .
Apply F_minus
An exact proof term for the current goal is ??
We prove the intermediate
claim Lmp1w :
F (- proj1 w .
Apply F_minus
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp0w :
F (conj (proj0 w .
Apply F_conj
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1w :
F (conj (proj1 w .
Apply F_conj
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1wp1z :
F (conj (proj1 w * proj1 z .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lmcp1wp1z :
F (- conj (proj1 w * proj1 z .
Apply F_minus
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp0zp0w :
F (proj0 z * proj0 w .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1wp0z :
F (proj1 w * proj0 z .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1zcp0w :
F (proj1 z * conj (proj0 w .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
Use f_equal.
rewrite the current goal using
F_minus_add (proj0 z * proj0 w (- conj (proj1 w * proj1 z ?? ?? (from left to right).
Use f_equal.
An
exact proof term for the current goal is
F_minus_mul_distrR (proj0 z (proj0 w ?? ?? .
Use f_equal.
rewrite the current goal using
F_conj_minus (proj1 w ?? (from left to right).
An
exact proof term for the current goal is
F_minus_mul_distrL (conj (proj1 w (proj1 z ?? ?? .
rewrite the current goal using
F_minus_add (proj1 w * proj0 z (proj1 z * conj (proj0 w ?? ?? (from left to right).
Use f_equal.
An
exact proof term for the current goal is
F_minus_mul_distrL (proj1 w (proj0 z ?? ?? .
rewrite the current goal using
F_conj_minus (proj0 w ?? (from left to right).
An
exact proof term for the current goal is
F_minus_mul_distrR (proj1 z (conj (proj0 w ?? ?? .
∎
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
Proof: Let z and w be given.
Assume Hz Hw .
We prove the intermediate
claim Lp0z :
F (proj0 z .
An
exact proof term for the current goal is
CD_proj0R z Hz .
We prove the intermediate
claim Lp1z :
F (proj1 z .
An
exact proof term for the current goal is
CD_proj1R z Hz .
We prove the intermediate
claim Lp0w :
F (proj0 w .
An
exact proof term for the current goal is
CD_proj0R w Hw .
We prove the intermediate
claim Lp1w :
F (proj1 w .
An
exact proof term for the current goal is
CD_proj1R w Hw .
We prove the intermediate
claim Lmp0z :
F (- proj0 z .
Apply F_minus
An exact proof term for the current goal is ??
We prove the intermediate
claim Lmp1z :
F (- proj1 z .
Apply F_minus
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp0w :
F (conj (proj0 w .
Apply F_conj
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1w :
F (conj (proj1 w .
Apply F_conj
An exact proof term for the current goal is ??
We prove the intermediate
claim Lcp1wp1z :
F (conj (proj1 w * proj1 z .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lmcp1wp1z :
F (- conj (proj1 w * proj1 z .
Apply F_minus
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp0zp0w :
F (proj0 z * proj0 w .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1wp0z :
F (proj1 w * proj0 z .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
We prove the intermediate
claim Lp1zcp0w :
F (proj1 z * conj (proj0 w .
Apply F_mul
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
Apply F_add
An exact proof term for the current goal is ??
An exact proof term for the current goal is ??
Use f_equal.
rewrite the current goal using
F_minus_add (proj0 z * proj0 w (- conj (proj1 w * proj1 z ?? ?? (from left to right).
Use f_equal.
An
exact proof term for the current goal is
F_minus_mul_distrL (proj0 z (proj0 w ?? ?? .
Use f_equal.
An
exact proof term for the current goal is
F_minus_mul_distrR (conj (proj1 w (proj1 z ?? ?? .
rewrite the current goal using
F_minus_add (proj1 w * proj0 z (proj1 z * conj (proj0 w ?? ?? (from left to right).
Use f_equal.
An
exact proof term for the current goal is
F_minus_mul_distrR (proj1 w (proj0 z ?? ?? .
An
exact proof term for the current goal is
F_minus_mul_distrL (proj1 z (conj (proj0 w ?? ?? .
∎
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 .
Proof: Let z be given.
An
exact proof term for the current goal is
nat_primrec_0 1 (λ_ r ⇒ z ⨯ r ) .
∎
Proof: Let z and n be given.
Assume Hn .
An
exact proof term for the current goal is
nat_primrec_S 1 (λ_ r ⇒ z ⨯ r ) n Hn .
∎
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
Proof: Let z be given.
Assume Hz .
We will
prove z ⨯ z ^ 0 = z .
rewrite the current goal using
CD_exp_nat_0 z (from left to right).
An
exact proof term for the current goal is
CD_mul_1R minus conj add mul F_0 F_1 F_minus_0 F_conj_0 F_conj_1 F_add_0L F_add_0R F_mul_0L F_mul_1R z Hz .
∎
Proof: Let z be given.
Assume Hz .
We will
prove z ⨯ z ^ 1 = z ⨯ z .
Use f_equal.
An
exact proof term for the current goal is
CD_exp_nat_1 z Hz .
∎
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
Proof: Let z be given.
Assume Hz .
rewrite the current goal using
CD_exp_nat_0 (from left to right).
An
exact proof term for the current goal is
CD_carr_0ext F_0 1 F_1 .
Let n be given.
Assume Hn .
rewrite the current goal using
CD_exp_nat_S z n Hn (from left to right).
Apply CD_mul_CD minus conj add mul F_minus F_conj F_add F_mul to the current goal.
An exact proof term for the current goal is Hz
An exact proof term for the current goal is IHn
∎
End of Section CD_exp_nat
End of Section Alg