Search for blocks/addresses/...
Proofgold Signed Transaction
vin
Pr314..
/
54b13..
PULd2..
/
d8344..
vout
Pr314..
/
94b3d..
44.19 bars
TMRNh..
/
a6af7..
ownership of
3a96a..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMZ9b..
/
f062f..
ownership of
79d32..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMJQ8..
/
b1532..
ownership of
44bfa..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMbk8..
/
6b30b..
ownership of
111bf..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMUA8..
/
0aaf6..
ownership of
b8001..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMNrv..
/
856b3..
ownership of
721fe..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TML6t..
/
65850..
ownership of
a6e1f..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMG38..
/
33ceb..
ownership of
00f33..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMUDX..
/
fc595..
ownership of
73cdc..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMW2V..
/
0cdfa..
ownership of
c9027..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMQr2..
/
28f24..
ownership of
7bd75..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMcYq..
/
1a96e..
ownership of
72efa..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMXcb..
/
d57c4..
ownership of
bea16..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMFCk..
/
a01fc..
ownership of
4c4da..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMV6s..
/
ce15e..
ownership of
a7e3d..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMdqU..
/
684d8..
ownership of
0c5a4..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMaBG..
/
030ad..
ownership of
de638..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMQmm..
/
e52fb..
ownership of
6d81e..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMSLg..
/
83820..
ownership of
c36da..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMasN..
/
5226a..
ownership of
caaa9..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMEui..
/
cacf7..
ownership of
87c1a..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMLkj..
/
64f77..
ownership of
6ffbf..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMY6n..
/
0ea82..
ownership of
df8e4..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMTTn..
/
bc391..
ownership of
ff8d4..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMTf6..
/
9e347..
ownership of
d188d..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMYk3..
/
9a652..
ownership of
8b3bd..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMRWf..
/
915ba..
ownership of
7268e..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMc8Y..
/
3abc6..
ownership of
92b21..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMRsP..
/
e9028..
ownership of
9935d..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMTkE..
/
898ef..
ownership of
acf73..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMJzg..
/
f0780..
ownership of
49b9e..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMSxV..
/
d5187..
ownership of
eceae..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMZ5Y..
/
94cde..
ownership of
30d6a..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMX6Y..
/
f0904..
ownership of
c9574..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMH3U..
/
50ae8..
ownership of
e61f1..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMXU7..
/
c7808..
ownership of
06b28..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMFD2..
/
a83bc..
ownership of
de036..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMVF4..
/
33032..
ownership of
3e982..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMN5m..
/
c7878..
ownership of
b99cd..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMZg2..
/
a92be..
ownership of
c7497..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMQYT..
/
e6f6b..
ownership of
c10e5..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMVZq..
/
20a3a..
ownership of
95a4c..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMcTC..
/
93336..
ownership of
daa8e..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMRuG..
/
fb606..
ownership of
a7853..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMFm4..
/
af090..
ownership of
df334..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMRoC..
/
49f47..
ownership of
9b260..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMN8s..
/
17cce..
ownership of
07d80..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMYeW..
/
6dff6..
ownership of
2484b..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMYof..
/
46991..
ownership of
46b3d..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMMNC..
/
56a41..
ownership of
d6eb4..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMKNj..
/
7e3b9..
ownership of
ec5f7..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMR5u..
/
c2867..
ownership of
28c3d..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMZNd..
/
bdaf0..
ownership of
c761b..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMP63..
/
7214a..
ownership of
cebe7..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMcC5..
/
2bb9f..
ownership of
1015d..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMRaW..
/
22e09..
ownership of
8f569..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMGzc..
/
6be3f..
ownership of
f0af4..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMF6S..
/
bfa75..
ownership of
d2c4c..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMKNy..
/
48919..
ownership of
c21d2..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMLvp..
/
e35b1..
ownership of
1a754..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMauk..
/
6a95f..
ownership of
80f32..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMNhc..
/
72845..
ownership of
761b6..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMbxP..
/
e798a..
ownership of
811e5..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMWso..
/
aaa11..
ownership of
bbfae..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMbQ7..
/
6e3e5..
ownership of
e80fd..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMUBi..
/
99d3b..
ownership of
85d43..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMRSb..
/
dbcaa..
ownership of
446f1..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMYp4..
/
2048d..
ownership of
33c26..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMamt..
/
2f095..
ownership of
9f036..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMR4r..
/
ed302..
ownership of
67557..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMYV5..
/
da6a8..
ownership of
75c88..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMYQW..
/
46a31..
ownership of
cb7d7..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMcx5..
/
ec15a..
ownership of
466da..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMHh9..
/
a8d7b..
ownership of
bda1b..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMVZ6..
/
29f5b..
ownership of
126cc..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMU41..
/
b51f1..
ownership of
c9618..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMUGd..
/
7682e..
ownership of
2f43f..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMHDQ..
/
beaeb..
ownership of
15268..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMcYr..
/
92a61..
ownership of
4addd..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMMk2..
/
a8d5f..
ownership of
1953c..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMHoq..
/
9329b..
ownership of
d52b5..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMFmf..
/
52db0..
ownership of
9a610..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMMdc..
/
27eb4..
ownership of
9ca0e..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMK6s..
/
3c600..
ownership of
e4f02..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMP57..
/
301a0..
ownership of
3c721..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMaFq..
/
19730..
ownership of
ce7e5..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMFLQ..
/
dcb2c..
ownership of
a3c6c..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMR7W..
/
1da5a..
ownership of
5e740..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMc1P..
/
18ace..
ownership of
bf827..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMZos..
/
f3d99..
ownership of
df53e..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMYV2..
/
f5558..
ownership of
a4f83..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMZrp..
/
75483..
ownership of
12c41..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMXpG..
/
06954..
ownership of
6b929..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMdCs..
/
2eae5..
ownership of
90e6e..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
PUSRj..
/
c61fe..
doc published by
PrQUS..
Param
SNo
SNo
:
ι
→
ο
Param
SNoLt
SNoLt
:
ι
→
ι
→
ο
Param
recip_SNo_pos
recip_SNo_pos
:
ι
→
ι
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Param
mul_SNo
mul_SNo
:
ι
→
ι
→
ι
Param
ordsucc
ordsucc
:
ι
→
ι
Known
recip_SNo_pos_prop1
recip_SNo_pos_prop1
:
∀ x0 .
SNo
x0
⟶
SNoLt
0
x0
⟶
and
(
SNo
(
recip_SNo_pos
x0
)
)
(
mul_SNo
x0
(
recip_SNo_pos
x0
)
=
1
)
Theorem
SNo_recip_SNo_pos
SNo_recip_SNo_pos
:
∀ x0 .
SNo
x0
⟶
SNoLt
0
x0
⟶
SNo
(
recip_SNo_pos
x0
)
(proof)
Theorem
recip_SNo_pos_invR
recip_SNo_pos_invR
:
∀ x0 .
SNo
x0
⟶
SNoLt
0
x0
⟶
mul_SNo
x0
(
recip_SNo_pos
x0
)
=
1
(proof)
Known
mul_SNo_nonzero_cancel
mul_SNo_nonzero_cancel_L
:
∀ x0 x1 x2 .
SNo
x0
⟶
(
x0
=
0
⟶
∀ x3 : ο .
x3
)
⟶
SNo
x1
⟶
SNo
x2
⟶
mul_SNo
x0
x1
=
mul_SNo
x0
x2
⟶
x1
=
x2
Known
SNo_1
SNo_1
:
SNo
1
Known
neq_1_0
neq_1_0
:
1
=
0
⟶
∀ x0 : ο .
x0
Known
SNoLt_0_1
SNoLt_0_1
:
SNoLt
0
1
Known
mul_SNo_oneL
mul_SNo_oneL
:
∀ x0 .
SNo
x0
⟶
mul_SNo
1
x0
=
x0
Theorem
recip_SNo_pos_1
recip_SNo_pos_1
:
recip_SNo_pos
1
=
1
(proof)
Known
SNoLt_trichotomy_or_impred
SNoLt_trichotomy_or_impred
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
∀ x2 : ο .
(
SNoLt
x0
x1
⟶
x2
)
⟶
(
x0
=
x1
⟶
x2
)
⟶
(
SNoLt
x1
x0
⟶
x2
)
⟶
x2
Known
SNo_0
SNo_0
:
SNo
0
Definition
False
False
:=
∀ x0 : ο .
x0
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Known
SNoLt_irref
SNoLt_irref
:
∀ x0 .
not
(
SNoLt
x0
x0
)
Known
SNoLt_tra
SNoLt_tra
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
x0
x1
⟶
SNoLt
x1
x2
⟶
SNoLt
x0
x2
Known
mul_SNo_pos_neg
mul_SNo_pos_neg
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLt
0
x0
⟶
SNoLt
x1
0
⟶
SNoLt
(
mul_SNo
x0
x1
)
0
Known
mul_SNo_zeroR
mul_SNo_zeroR
:
∀ x0 .
SNo
x0
⟶
mul_SNo
x0
0
=
0
Theorem
recip_SNo_pos_pos
recip_SNo_pos_pos
:
∀ x0 .
SNo
x0
⟶
SNoLt
0
x0
⟶
SNoLt
0
(
recip_SNo_pos
x0
)
(proof)
Known
mul_SNo_com
mul_SNo_com
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
mul_SNo
x0
x1
=
mul_SNo
x1
x0
Theorem
recip_SNo_pos_invol
recip_SNo_pos_invol
:
∀ x0 .
SNo
x0
⟶
SNoLt
0
x0
⟶
recip_SNo_pos
(
recip_SNo_pos
x0
)
=
x0
(proof)
Param
nat_p
nat_p
:
ι
→
ο
Param
eps_
eps_
:
ι
→
ι
Param
exp_SNo_nat
exp_SNo_nat
:
ι
→
ι
→
ι
Known
SNo_exp_SNo_nat
SNo_exp_SNo_nat
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
nat_p
x1
⟶
SNo
(
exp_SNo_nat
x0
x1
)
Known
SNo_2
SNo_2
:
SNo
2
Known
mul_SNo_eps_power_2
mul_SNo_eps_power_2
:
∀ x0 .
nat_p
x0
⟶
mul_SNo
(
eps_
x0
)
(
exp_SNo_nat
2
x0
)
=
1
Param
omega
omega
:
ι
Known
SNo_eps_pos
SNo_eps_pos
:
∀ x0 .
x0
∈
omega
⟶
SNoLt
0
(
eps_
x0
)
Known
nat_p_omega
nat_p_omega
:
∀ x0 .
nat_p
x0
⟶
x0
∈
omega
Known
SNo_eps_
SNo_eps_
:
∀ x0 .
x0
∈
omega
⟶
SNo
(
eps_
x0
)
Theorem
recip_SNo_pos_eps_
recip_SNo_pos_eps_
:
∀ x0 .
nat_p
x0
⟶
recip_SNo_pos
(
eps_
x0
)
=
exp_SNo_nat
2
x0
(proof)
Theorem
recip_SNo_pos_pow_2
recip_SNo_pos_pow_2
:
∀ x0 .
nat_p
x0
⟶
recip_SNo_pos
(
exp_SNo_nat
2
x0
)
=
eps_
x0
(proof)
Known
exp_SNo_nat_S
exp_SNo_nat_S
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
nat_p
x1
⟶
exp_SNo_nat
x0
(
ordsucc
x1
)
=
mul_SNo
x0
(
exp_SNo_nat
x0
x1
)
Known
nat_0
nat_0
:
nat_p
0
Known
exp_SNo_nat_0
exp_SNo_nat_0
:
∀ x0 .
SNo
x0
⟶
exp_SNo_nat
x0
0
=
1
Known
mul_SNo_oneR
mul_SNo_oneR
:
∀ x0 .
SNo
x0
⟶
mul_SNo
x0
1
=
x0
Theorem
exp_SNo_nat_1
exp_SNo_nat_1
:
∀ x0 .
SNo
x0
⟶
exp_SNo_nat
x0
1
=
x0
(proof)
Known
nat_1
nat_1
:
nat_p
1
Theorem
recip_SNo_pos_2
recip_SNo_pos_2
:
recip_SNo_pos
2
=
eps_
1
(proof)
Param
If_i
If_i
:
ο
→
ι
→
ι
→
ι
Param
minus_SNo
minus_SNo
:
ι
→
ι
Definition
recip_SNo
recip_SNo
:=
λ x0 .
If_i
(
SNoLt
0
x0
)
(
recip_SNo_pos
x0
)
(
If_i
(
SNoLt
x0
0
)
(
minus_SNo
(
recip_SNo_pos
(
minus_SNo
x0
)
)
)
0
)
Known
If_i_1
If_i_1
:
∀ x0 : ο .
∀ x1 x2 .
x0
⟶
If_i
x0
x1
x2
=
x1
Theorem
recip_SNo_poscase
recip_SNo_poscase
:
∀ x0 .
SNoLt
0
x0
⟶
recip_SNo
x0
=
recip_SNo_pos
x0
(proof)
Known
If_i_0
If_i_0
:
∀ x0 : ο .
∀ x1 x2 .
not
x0
⟶
If_i
x0
x1
x2
=
x2
Theorem
recip_SNo_negcase
recip_SNo_negcase
:
∀ x0 .
SNo
x0
⟶
SNoLt
x0
0
⟶
recip_SNo
x0
=
minus_SNo
(
recip_SNo_pos
(
minus_SNo
x0
)
)
(proof)
Theorem
recip_SNo_0
recip_SNo_0
:
recip_SNo
0
=
0
(proof)
Theorem
recip_SNo_1
recip_SNo_1
:
recip_SNo
1
=
1
(proof)
Known
SNo_minus_SNo
SNo_minus_SNo
:
∀ x0 .
SNo
x0
⟶
SNo
(
minus_SNo
x0
)
Known
minus_SNo_Lt_contra2
minus_SNo_Lt_contra2
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLt
x0
(
minus_SNo
x1
)
⟶
SNoLt
x1
(
minus_SNo
x0
)
Known
minus_SNo_0
minus_SNo_0
:
minus_SNo
0
=
0
Theorem
SNo_recip_SNo
SNo_recip_SNo
:
∀ x0 .
SNo
x0
⟶
SNo
(
recip_SNo
x0
)
(proof)
Known
mul_SNo_minus_distrR
mul_minus_SNo_distrR
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
mul_SNo
x0
(
minus_SNo
x1
)
=
minus_SNo
(
mul_SNo
x0
x1
)
Known
mul_SNo_minus_distrL
mul_SNo_minus_distrL
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
mul_SNo
(
minus_SNo
x0
)
x1
=
minus_SNo
(
mul_SNo
x0
x1
)
Theorem
recip_SNo_invR
recip_SNo_invR
:
∀ x0 .
SNo
x0
⟶
(
x0
=
0
⟶
∀ x1 : ο .
x1
)
⟶
mul_SNo
x0
(
recip_SNo
x0
)
=
1
(proof)
Theorem
recip_SNo_invL
recip_SNo_invL
:
∀ x0 .
SNo
x0
⟶
(
x0
=
0
⟶
∀ x1 : ο .
x1
)
⟶
mul_SNo
(
recip_SNo
x0
)
x0
=
1
(proof)
Theorem
recip_SNo_eps_
recip_SNo_eps_
:
∀ x0 .
nat_p
x0
⟶
recip_SNo
(
eps_
x0
)
=
exp_SNo_nat
2
x0
(proof)
Known
exp_SNo_nat_pos
exp_SNo_nat_pos
:
∀ x0 .
SNo
x0
⟶
SNoLt
0
x0
⟶
∀ x1 .
nat_p
x1
⟶
SNoLt
0
(
exp_SNo_nat
x0
x1
)
Known
SNoLt_0_2
SNoLt_0_2
:
SNoLt
0
2
Theorem
recip_SNo_pow_2
recip_SNo_pow_2
:
∀ x0 .
nat_p
x0
⟶
recip_SNo
(
exp_SNo_nat
2
x0
)
=
eps_
x0
(proof)
Theorem
recip_SNo_2
recip_SNo_2
:
recip_SNo
2
=
eps_
1
(proof)
Known
minus_SNo_Lt_contra1
minus_SNo_Lt_contra1
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLt
(
minus_SNo
x0
)
x1
⟶
SNoLt
(
minus_SNo
x1
)
x0
Known
minus_SNo_invol
minus_SNo_invol
:
∀ x0 .
SNo
x0
⟶
minus_SNo
(
minus_SNo
x0
)
=
x0
Theorem
recip_SNo_invol
recip_SNo_invol
:
∀ x0 .
SNo
x0
⟶
recip_SNo
(
recip_SNo
x0
)
=
x0
(proof)
Theorem
recip_SNo_of_pos_is_pos
recip_SNo_of_pos_is_pos
:
∀ x0 .
SNo
x0
⟶
SNoLt
0
x0
⟶
SNoLt
0
(
recip_SNo
x0
)
(proof)
Theorem
recip_SNo_of_neg_is_neg
recip_SNo_of_neg_is_neg
:
∀ x0 .
SNo
x0
⟶
SNoLt
x0
0
⟶
SNoLt
(
recip_SNo
x0
)
0
(proof)
Definition
div_SNo
div_SNo
:=
λ x0 x1 .
mul_SNo
x0
(
recip_SNo
x1
)
Known
SNo_mul_SNo
SNo_mul_SNo
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNo
(
mul_SNo
x0
x1
)
Theorem
SNo_div_SNo
SNo_div_SNo
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNo
(
div_SNo
x0
x1
)
(proof)
Known
mul_SNo_zeroL
mul_SNo_zeroL
:
∀ x0 .
SNo
x0
⟶
mul_SNo
0
x0
=
0
Theorem
div_SNo_0_num
div_SNo_0_num
:
∀ x0 .
SNo
x0
⟶
div_SNo
0
x0
=
0
(proof)
Theorem
div_SNo_0_denum
div_SNo_0_denum
:
∀ x0 .
SNo
x0
⟶
div_SNo
x0
0
=
0
(proof)
Known
mul_SNo_assoc
mul_SNo_assoc
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
mul_SNo
x0
(
mul_SNo
x1
x2
)
=
mul_SNo
(
mul_SNo
x0
x1
)
x2
Theorem
mul_div_SNo_invL
mul_div_SNo_invL
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
(
x1
=
0
⟶
∀ x2 : ο .
x2
)
⟶
mul_SNo
(
div_SNo
x0
x1
)
x1
=
x0
(proof)
Theorem
mul_div_SNo_invR
mul_div_SNo_invR
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
(
x1
=
0
⟶
∀ x2 : ο .
x2
)
⟶
mul_SNo
x1
(
div_SNo
x0
x1
)
=
x0
(proof)
Definition
or
or
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x2
)
⟶
(
x1
⟶
x2
)
⟶
x2
Known
xm
xm
:
∀ x0 : ο .
or
x0
(
not
x0
)
Theorem
mul_div_SNo_R
mul_div_SNo_R
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
mul_SNo
(
div_SNo
x0
x1
)
x2
=
div_SNo
(
mul_SNo
x0
x2
)
x1
(proof)
Theorem
mul_div_SNo_L
mul_div_SNo_L
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
mul_SNo
x2
(
div_SNo
x0
x1
)
=
div_SNo
(
mul_SNo
x2
x0
)
x1
(proof)
Theorem
div_mul_SNo_invL
div_mul_SNo_invL
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
(
x1
=
0
⟶
∀ x2 : ο .
x2
)
⟶
div_SNo
(
mul_SNo
x0
x1
)
x1
=
x0
(proof)
Theorem
div_div_SNo
div_div_SNo
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
div_SNo
(
div_SNo
x0
x1
)
x2
=
div_SNo
x0
(
mul_SNo
x1
x2
)
(proof)
Theorem
mul_div_SNo_both
mul_div_SNo_both
:
∀ x0 x1 x2 x3 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNo
x3
⟶
mul_SNo
(
div_SNo
x0
x1
)
(
div_SNo
x2
x3
)
=
div_SNo
(
mul_SNo
x0
x2
)
(
mul_SNo
x1
x3
)
(proof)
Param
SNoLe
SNoLe
:
ι
→
ι
→
ο
Known
SNoLtLe_or
SNoLtLe_or
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
or
(
SNoLt
x0
x1
)
(
SNoLe
x1
x0
)
Known
SNoLtLe_tra
SNoLtLe_tra
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
x0
x1
⟶
SNoLe
x1
x2
⟶
SNoLt
x0
x2
Known
nonneg_mul_SNo_Le
nonneg_mul_SNo_Le
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNoLe
0
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLe
x1
x2
⟶
SNoLe
(
mul_SNo
x0
x1
)
(
mul_SNo
x0
x2
)
Known
SNoLtLe
SNoLtLe
:
∀ x0 x1 .
SNoLt
x0
x1
⟶
SNoLe
x0
x1
Theorem
recip_SNo_pos_pos
recip_SNo_pos_pos
:
∀ x0 .
SNo
x0
⟶
SNoLt
0
x0
⟶
SNoLt
0
(
recip_SNo_pos
x0
)
(proof)
Theorem
recip_SNo_of_neg_is_neg
recip_SNo_of_neg_is_neg
:
∀ x0 .
SNo
x0
⟶
SNoLt
x0
0
⟶
SNoLt
(
recip_SNo
x0
)
0
(proof)
Known
mul_SNo_pos_pos
mul_SNo_pos_pos
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLt
0
x0
⟶
SNoLt
0
x1
⟶
SNoLt
0
(
mul_SNo
x0
x1
)
Theorem
div_SNo_pos_pos
div_SNo_pos_pos
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLt
0
x0
⟶
SNoLt
0
x1
⟶
SNoLt
0
(
div_SNo
x0
x1
)
(proof)
Known
mul_SNo_neg_neg
mul_SNo_neg_neg
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLt
x0
0
⟶
SNoLt
x1
0
⟶
SNoLt
0
(
mul_SNo
x0
x1
)
Theorem
div_SNo_neg_neg
div_SNo_neg_neg
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLt
x0
0
⟶
SNoLt
x1
0
⟶
SNoLt
0
(
div_SNo
x0
x1
)
(proof)
Theorem
div_SNo_pos_neg
div_SNo_pos_neg
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLt
0
x0
⟶
SNoLt
x1
0
⟶
SNoLt
(
div_SNo
x0
x1
)
0
(proof)
Known
mul_SNo_neg_pos
mul_SNo_neg_pos
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLt
x0
0
⟶
SNoLt
0
x1
⟶
SNoLt
(
mul_SNo
x0
x1
)
0
Theorem
div_SNo_neg_pos
div_SNo_neg_pos
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLt
x0
0
⟶
SNoLt
0
x1
⟶
SNoLt
(
div_SNo
x0
x1
)
0
(proof)
Known
pos_mul_SNo_Lt'
pos_mul_SNo_Lt
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
0
x2
⟶
SNoLt
x0
x1
⟶
SNoLt
(
mul_SNo
x0
x2
)
(
mul_SNo
x1
x2
)
Theorem
div_SNo_pos_LtL
div_SNo_pos_LtL
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
0
x1
⟶
SNoLt
x0
(
mul_SNo
x2
x1
)
⟶
SNoLt
(
div_SNo
x0
x1
)
x2
(proof)
Theorem
div_SNo_pos_LtR
div_SNo_pos_LtR
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
0
x1
⟶
SNoLt
(
mul_SNo
x2
x1
)
x0
⟶
SNoLt
x2
(
div_SNo
x0
x1
)
(proof)
Theorem
div_SNo_pos_LtL'
div_SNo_pos_LtL
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
0
x1
⟶
SNoLt
(
div_SNo
x0
x1
)
x2
⟶
SNoLt
x0
(
mul_SNo
x2
x1
)
(proof)
Theorem
div_SNo_pos_LtR'
div_SNo_pos_LtR
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
0
x1
⟶
SNoLt
x2
(
div_SNo
x0
x1
)
⟶
SNoLt
(
mul_SNo
x2
x1
)
x0
(proof)
Theorem
mul_div_SNo_nonzero_eq
mul_div_SNo_nonzero_eq
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
(
x1
=
0
⟶
∀ x3 : ο .
x3
)
⟶
x0
=
mul_SNo
x1
x2
⟶
div_SNo
x0
x1
=
x2
(proof)
Param
SNo_
SNo_
:
ι
→
ι
→
ο
Param
SNoLev
SNoLev
:
ι
→
ι
Known
SNoLev_0_eq_0
SNoLev_0_eq_0
:
∀ x0 .
SNo
x0
⟶
SNoLev
x0
=
0
⟶
x0
=
0
Param
ordinal
ordinal
:
ι
→
ο
Known
SNo_SNo
SNo_SNo
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
SNo_
x0
x1
⟶
SNo
x1
Known
ordinal_Empty
ordinal_Empty
:
ordinal
0
Known
SNoLev_uniq2
SNoLev_uniq2
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
SNo_
x0
x1
⟶
SNoLev
x1
=
x0
Theorem
SNo_0_eq_0
SNo_0_eq_0
:
∀ x0 .
SNo_
0
x0
⟶
x0
=
0
(proof)
Param
add_SNo
add_SNo
:
ι
→
ι
→
ι
Known
add_SNo_1_1_2
add_SNo_1_1_2
:
add_SNo
1
1
=
2
Known
mul_SNo_distrR
mul_SNo_distrR
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
mul_SNo
(
add_SNo
x0
x1
)
x2
=
add_SNo
(
mul_SNo
x0
x2
)
(
mul_SNo
x1
x2
)
Known
add_SNo_Lt2
add_SNo_Lt2
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
x1
x2
⟶
SNoLt
(
add_SNo
x0
x1
)
(
add_SNo
x0
x2
)
Theorem
SNo_gt2_double_ltS
SNo_gt2_double_ltS
:
∀ x0 .
SNo
x0
⟶
SNoLt
1
x0
⟶
SNoLt
(
add_SNo
x0
1
)
(
mul_SNo
2
x0
)
(proof)
Param
real
real
:
ι
Param
SNoS_
SNoS_
:
ι
→
ι
Param
abs_SNo
abs_SNo
:
ι
→
ι
Known
real_E
real_E
:
∀ x0 .
x0
∈
real
⟶
∀ x1 : ο .
(
SNo
x0
⟶
SNoLev
x0
∈
ordsucc
omega
⟶
x0
∈
SNoS_
(
ordsucc
omega
)
⟶
SNoLt
(
minus_SNo
omega
)
x0
⟶
SNoLt
x0
omega
⟶
(
∀ x2 .
x2
∈
SNoS_
omega
⟶
(
∀ x3 .
x3
∈
omega
⟶
SNoLt
(
abs_SNo
(
add_SNo
x2
(
minus_SNo
x0
)
)
)
(
eps_
x3
)
)
⟶
x2
=
x0
)
⟶
(
∀ x2 .
x2
∈
omega
⟶
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
SNoS_
omega
)
(
and
(
SNoLt
x4
x0
)
(
SNoLt
x0
(
add_SNo
x4
(
eps_
x2
)
)
)
)
⟶
x3
)
⟶
x3
)
⟶
x1
)
⟶
x1
Known
eps_0_1
eps_0_1
:
eps_
0
=
1
Known
SNoS_E
SNoS_E
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
x1
∈
SNoS_
x0
⟶
∀ x2 : ο .
(
∀ x3 .
and
(
x3
∈
x0
)
(
SNo_
x3
x1
)
⟶
x2
)
⟶
x2
Known
omega_ordinal
omega_ordinal
:
ordinal
omega
Known
nat_ind
nat_ind
:
∀ x0 :
ι → ο
.
x0
0
⟶
(
∀ x1 .
nat_p
x1
⟶
x0
x1
⟶
x0
(
ordsucc
x1
)
)
⟶
∀ x1 .
nat_p
x1
⟶
x0
x1
Known
SNoLeLt_tra
SNoLeLt_tra
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLe
x0
x1
⟶
SNoLt
x1
x2
⟶
SNoLt
x0
x2
Known
nat_p_SNo
nat_p_SNo
:
∀ x0 .
nat_p
x0
⟶
SNo
x0
Known
andI
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Known
nat_ordsucc
nat_ordsucc
:
∀ x0 .
nat_p
x0
⟶
nat_p
(
ordsucc
x0
)
Known
omega_nat_p
omega_nat_p
:
∀ x0 .
x0
∈
omega
⟶
nat_p
x0
Known
SNo_add_SNo
SNo_add_SNo
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNo
(
add_SNo
x0
x1
)
Known
ordinal_SNoLev_max_2
ordinal_SNoLev_max_2
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
SNo
x1
⟶
SNoLev
x1
∈
ordsucc
x0
⟶
SNoLe
x1
x0
Known
nat_p_ordinal
nat_p_ordinal
:
∀ x0 .
nat_p
x0
⟶
ordinal
x0
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Known
ordinal_In_Or_Subq
ordinal_In_Or_Subq
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
or
(
x0
∈
x1
)
(
x1
⊆
x0
)
Known
SNoLev_ordinal
SNoLev_ordinal
:
∀ x0 .
SNo
x0
⟶
ordinal
(
SNoLev
x0
)
Known
ordsuccI1
ordsuccI1
:
∀ x0 .
x0
⊆
ordsucc
x0
Known
set_ext
set_ext
:
∀ x0 x1 .
x0
⊆
x1
⟶
x1
⊆
x0
⟶
x0
=
x1
Known
Subq_tra
Subq_tra
:
∀ x0 x1 x2 .
x0
⊆
x1
⟶
x1
⊆
x2
⟶
x0
⊆
x2
Known
add_SNo_Lev_bd
add_SNo_Lev_bd
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLev
(
add_SNo
x0
x1
)
⊆
add_SNo
(
SNoLev
x0
)
(
SNoLev
x1
)
Known
ordinal_SNoLev
ordinal_SNoLev
:
∀ x0 .
ordinal
x0
⟶
SNoLev
x0
=
x0
Known
add_SNo_1_ordsucc
add_SNo_1_ordsucc
:
∀ x0 .
x0
∈
omega
⟶
add_SNo
x0
1
=
ordsucc
x0
Known
Subq_ref
Subq_ref
:
∀ x0 .
x0
⊆
x0
Known
ordsuccI2
ordsuccI2
:
∀ x0 .
x0
∈
ordsucc
x0
Theorem
nonneg_real_nat_interval
nonneg_real_nat_interval
:
∀ x0 .
x0
∈
real
⟶
SNoLe
0
x0
⟶
∀ x1 : ο .
(
∀ x2 .
and
(
x2
∈
omega
)
(
and
(
SNoLe
x2
x0
)
(
SNoLt
x0
(
ordsucc
x2
)
)
)
⟶
x1
)
⟶
x1
(proof)
Param
Sep
Sep
:
ι
→
(
ι
→
ο
) →
ι
Param
SNoL
SNoL
:
ι
→
ι
Definition
SNoL_pos
SNoL_pos
:=
λ x0 .
Sep
(
SNoL
x0
)
(
SNoLt
0
)
Known
dneg
dneg
:
∀ x0 : ο .
not
(
not
x0
)
⟶
x0
Known
SNoS_I
SNoS_I
:
∀ x0 .
ordinal
x0
⟶
∀ x1 x2 .
x2
∈
x0
⟶
SNo_
x2
x1
⟶
x1
∈
SNoS_
x0
Known
ordinal_SNo_
ordinal_SNo_
:
∀ x0 .
ordinal
x0
⟶
SNo_
x0
x0
Known
add_SNo_0L
add_SNo_0L
:
∀ x0 .
SNo
x0
⟶
add_SNo
0
x0
=
x0
Known
abs_SNo_minus
abs_SNo_minus
:
∀ x0 .
SNo
x0
⟶
abs_SNo
(
minus_SNo
x0
)
=
abs_SNo
x0
Known
pos_abs_SNo
pos_abs_SNo
:
∀ x0 .
SNoLt
0
x0
⟶
abs_SNo
x0
=
x0
Known
SepI
SepI
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
x0
⟶
x1
x2
⟶
x2
∈
Sep
x0
x1
Known
SNoL_I
SNoL_I
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
SNo
x1
⟶
SNoLev
x1
∈
SNoLev
x0
⟶
SNoLt
x1
x0
⟶
x1
∈
SNoL
x0
Known
pos_low_eq_one
pos_low_eq_one
:
∀ x0 .
SNo
x0
⟶
SNoLt
0
x0
⟶
SNoLev
x0
⊆
1
⟶
x0
=
1
Known
nat_inv
nat_inv
:
∀ x0 .
nat_p
x0
⟶
or
(
x0
=
0
)
(
∀ x1 : ο .
(
∀ x2 .
and
(
nat_p
x2
)
(
x0
=
ordsucc
x2
)
⟶
x1
)
⟶
x1
)
Known
SNoLeE
SNoLeE
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLe
x0
x1
⟶
or
(
SNoLt
x0
x1
)
(
x0
=
x1
)
Known
and3I
and3I
:
∀ x0 x1 x2 : ο .
x0
⟶
x1
⟶
x2
⟶
and
(
and
x0
x1
)
x2
Known
cases_2
cases_2
:
∀ x0 .
x0
∈
2
⟶
∀ x1 :
ι → ο
.
x1
0
⟶
x1
1
⟶
x1
x0
Known
ordinal_SNoLt_In
ordinal_SNoLt_In
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
SNoLt
x0
x1
⟶
x0
∈
x1
Known
nat_2
nat_2
:
nat_p
2
Known
neq_ordsucc_0
neq_ordsucc_0
:
∀ x0 .
ordsucc
x0
=
0
⟶
∀ x1 : ο .
x1
Known
ordsucc_inj
ordsucc_inj
:
∀ x0 x1 .
ordsucc
x0
=
ordsucc
x1
⟶
x0
=
x1
Known
ordinal_ordsucc_SNo_eq
ordinal_ordsucc_SNo_eq
:
∀ x0 .
ordinal
x0
⟶
ordsucc
x0
=
add_SNo
1
x0
Known
add_SNo_assoc
add_SNo_assoc
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
add_SNo
x0
(
add_SNo
x1
x2
)
=
add_SNo
(
add_SNo
x0
x1
)
x2
Known
add_SNo_0R
add_SNo_0R
:
∀ x0 .
SNo
x0
⟶
add_SNo
x0
0
=
x0
Known
add_SNo_Le2
add_SNo_Le2
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLe
x1
x2
⟶
SNoLe
(
add_SNo
x0
x1
)
(
add_SNo
x0
x2
)
Known
ordinal_Subq_SNoLe
ordinal_Subq_SNoLe
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
x0
⊆
x1
⟶
SNoLe
x0
x1
Known
Subq_Empty
Subq_Empty
:
∀ x0 .
0
⊆
x0
Known
ordinal_In_SNoLt
ordinal_In_SNoLt
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
x1
∈
x0
⟶
SNoLt
x1
x0
Known
SNoLe_ref
SNoLe_ref
:
∀ x0 .
SNoLe
x0
x0
Known
ordinal_trichotomy_or_impred
ordinal_trichotomy_or_impred
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
∀ x2 : ο .
(
x0
∈
x1
⟶
x2
)
⟶
(
x0
=
x1
⟶
x2
)
⟶
(
x1
∈
x0
⟶
x2
)
⟶
x2
Known
ordinal_SNoLev_max
ordinal_SNoLev_max
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
SNo
x1
⟶
SNoLev
x1
∈
x0
⟶
SNoLt
x1
x0
Known
add_SNo_Lt1
add_SNo_Lt1
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
x0
x2
⟶
SNoLt
(
add_SNo
x0
x1
)
(
add_SNo
x2
x1
)
Known
SNoLt_1_2
SNoLt_1_2
:
SNoLt
1
2
Param
binintersect
binintersect
:
ι
→
ι
→
ι
Definition
iff
iff
:=
λ x0 x1 : ο .
and
(
x0
⟶
x1
)
(
x1
⟶
x0
)
Definition
PNoEq_
PNoEq_
:=
λ x0 .
λ x1 x2 :
ι → ο
.
∀ x3 .
x3
∈
x0
⟶
iff
(
x1
x3
)
(
x2
x3
)
Definition
SNoEq_
SNoEq_
:=
λ x0 x1 x2 .
PNoEq_
x0
(
λ x3 .
x3
∈
x1
)
(
λ x3 .
x3
∈
x2
)
Definition
nIn
nIn
:=
λ x0 x1 .
not
(
x0
∈
x1
)
Known
SNoLtE
SNoLtE
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLt
x0
x1
⟶
∀ x2 : ο .
(
∀ x3 .
SNo
x3
⟶
SNoLev
x3
∈
binintersect
(
SNoLev
x0
)
(
SNoLev
x1
)
⟶
SNoEq_
(
SNoLev
x3
)
x3
x0
⟶
SNoEq_
(
SNoLev
x3
)
x3
x1
⟶
SNoLt
x0
x3
⟶
SNoLt
x3
x1
⟶
nIn
(
SNoLev
x3
)
x0
⟶
SNoLev
x3
∈
x1
⟶
x2
)
⟶
(
SNoLev
x0
∈
SNoLev
x1
⟶
SNoEq_
(
SNoLev
x0
)
x0
x1
⟶
SNoLev
x0
∈
x1
⟶
x2
)
⟶
(
SNoLev
x1
∈
SNoLev
x0
⟶
SNoEq_
(
SNoLev
x1
)
x0
x1
⟶
nIn
(
SNoLev
x1
)
x0
⟶
x2
)
⟶
x2
Known
eps_ordinal_In_eq_0
eps_ordinal_In_eq_0
:
∀ x0 x1 .
ordinal
x1
⟶
x1
∈
eps_
x0
⟶
x1
=
0
Known
SNoLev_eps_
SNoLev_eps_
:
∀ x0 .
x0
∈
omega
⟶
SNoLev
(
eps_
x0
)
=
ordsucc
x0
Known
ordsuccE
ordsuccE
:
∀ x0 x1 .
x1
∈
ordsucc
x0
⟶
or
(
x1
∈
x0
)
(
x1
=
x0
)
Known
binintersectE1
binintersectE1
:
∀ x0 x1 x2 .
x2
∈
binintersect
x0
x1
⟶
x2
∈
x0
Known
In_no2cycle
In_no2cycle
:
∀ x0 x1 .
x0
∈
x1
⟶
x1
∈
x0
⟶
False
Known
In_irref
In_irref
:
∀ x0 .
nIn
x0
x0
Known
eps_ordsucc_half_add
eps_ordsucc_half_add
:
∀ x0 .
nat_p
x0
⟶
add_SNo
(
eps_
(
ordsucc
x0
)
)
(
eps_
(
ordsucc
x0
)
)
=
eps_
x0
Known
omega_ordsucc
omega_ordsucc
:
∀ x0 .
x0
∈
omega
⟶
ordsucc
x0
∈
omega
Theorem
pos_real_left_approx_double
pos_real_left_approx_double
:
∀ x0 .
x0
∈
real
⟶
SNoLt
0
x0
⟶
(
x0
=
2
⟶
∀ x1 : ο .
x1
)
⟶
(
∀ x1 .
x1
∈
omega
⟶
x0
=
eps_
x1
⟶
∀ x2 : ο .
x2
)
⟶
∀ x1 : ο .
(
∀ x2 .
and
(
x2
∈
SNoL_pos
x0
)
(
SNoLt
x0
(
mul_SNo
2
x2
)
)
⟶
x1
)
⟶
x1
(proof)
Param
sqrt_SNo_nonneg
sqrt_SNo_nonneg
:
ι
→
ι
Param
ap
ap
:
ι
→
ι
→
ι
Param
SNo_sqrtaux
SNo_sqrtaux
:
ι
→
(
ι
→
ι
) →
ι
→
ι
Param
lam
Sigma
:
ι
→
(
ι
→
ι
) →
ι
Definition
SNoL_nonneg
SNoL_nonneg
:=
λ x0 .
Sep
(
SNoL
x0
)
(
SNoLe
0
)
Param
SNoR
SNoR
:
ι
→
ι
Known
SNo_sqrtaux_0
SNo_sqrtaux_0
:
∀ x0 .
∀ x1 :
ι → ι
.
SNo_sqrtaux
x0
x1
0
=
lam
2
(
λ x3 .
If_i
(
x3
=
0
)
(
prim5
(
SNoL_nonneg
x0
)
x1
)
(
prim5
(
SNoR
x0
)
x1
)
)
Known
tuple_2_0_eq
tuple_2_0_eq
:
∀ x0 x1 .
ap
(
lam
2
(
λ x3 .
If_i
(
x3
=
0
)
x0
x1
)
)
0
=
x0
Known
ReplE_impred
ReplE_impred
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
prim5
x0
x1
⟶
∀ x3 : ο .
(
∀ x4 .
x4
∈
x0
⟶
x2
=
x1
x4
⟶
x3
)
⟶
x3
Known
SepE
SepE
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
Sep
x0
x1
⟶
and
(
x2
∈
x0
)
(
x1
x2
)
Known
SNoL_E
SNoL_E
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
x1
∈
SNoL
x0
⟶
∀ x2 : ο .
(
SNo
x1
⟶
SNoLev
x1
∈
SNoLev
x0
⟶
SNoLt
x1
x0
⟶
x2
)
⟶
x2
Known
SNoS_I2
SNoS_I2
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLev
x0
∈
SNoLev
x1
⟶
x0
∈
SNoS_
(
SNoLev
x1
)
Known
tuple_2_1_eq
tuple_2_1_eq
:
∀ x0 x1 .
ap
(
lam
2
(
λ x3 .
If_i
(
x3
=
0
)
x0
x1
)
)
1
=
x1
Known
SNoR_E
SNoR_E
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
x1
∈
SNoR
x0
⟶
∀ x2 : ο .
(
SNo
x1
⟶
SNoLev
x1
∈
SNoLev
x0
⟶
SNoLt
x0
x1
⟶
x2
)
⟶
x2
Known
SNoLe_tra
SNoLe_tra
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLe
x0
x1
⟶
SNoLe
x1
x2
⟶
SNoLe
x0
x2
Param
binunion
binunion
:
ι
→
ι
→
ι
Param
SNo_sqrtauxset
SNo_sqrtauxset
:
ι
→
ι
→
ι
→
ι
Known
SNo_sqrtaux_S
SNo_sqrtaux_S
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
nat_p
x2
⟶
SNo_sqrtaux
x0
x1
(
ordsucc
x2
)
=
lam
2
(
λ x4 .
If_i
(
x4
=
0
)
(
binunion
(
ap
(
SNo_sqrtaux
x0
x1
x2
)
0
)
(
SNo_sqrtauxset
(
ap
(
SNo_sqrtaux
x0
x1
x2
)
0
)
(
ap
(
SNo_sqrtaux
x0
x1
x2
)
1
)
x0
)
)
(
binunion
(
binunion
(
ap
(
SNo_sqrtaux
x0
x1
x2
)
1
)
(
SNo_sqrtauxset
(
ap
(
SNo_sqrtaux
x0
x1
x2
)
0
)
(
ap
(
SNo_sqrtaux
x0
x1
x2
)
0
)
x0
)
)
(
SNo_sqrtauxset
(
ap
(
SNo_sqrtaux
x0
x1
x2
)
1
)
(
ap
(
SNo_sqrtaux
x0
x1
x2
)
1
)
x0
)
)
)
Known
binunionE'
binunionE
:
∀ x0 x1 x2 .
∀ x3 : ο .
(
x2
∈
x0
⟶
x3
)
⟶
(
x2
∈
x1
⟶
x3
)
⟶
x2
∈
binunion
x0
x1
⟶
x3
Known
SNo_sqrtauxset_E
SNo_sqrtauxset_E
:
∀ x0 x1 x2 x3 .
x3
∈
SNo_sqrtauxset
x0
x1
x2
⟶
∀ x4 : ο .
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x1
⟶
SNoLt
0
(
add_SNo
x5
x6
)
⟶
x3
=
div_SNo
(
add_SNo
x2
(
mul_SNo
x5
x6
)
)
(
add_SNo
x5
x6
)
⟶
x4
)
⟶
x4
Known
add_SNo_Le3
add_SNo_Le3
:
∀ x0 x1 x2 x3 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNo
x3
⟶
SNoLe
x0
x2
⟶
SNoLe
x1
x3
⟶
SNoLe
(
add_SNo
x0
x1
)
(
add_SNo
x2
x3
)
Known
mul_SNo_nonneg_nonneg
mul_SNo_nonneg_nonneg
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLe
0
x0
⟶
SNoLe
0
x1
⟶
SNoLe
0
(
mul_SNo
x0
x1
)
Known
SNo_foil
SNo_foil
:
∀ x0 x1 x2 x3 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNo
x3
⟶
mul_SNo
(
add_SNo
x0
x1
)
(
add_SNo
x2
x3
)
=
add_SNo
(
mul_SNo
x0
x2
)
(
add_SNo
(
mul_SNo
x0
x3
)
(
add_SNo
(
mul_SNo
x1
x2
)
(
mul_SNo
x1
x3
)
)
)
Known
add_SNo_rotate_4_1
add_SNo_rotate_4_1
:
∀ x0 x1 x2 x3 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNo
x3
⟶
add_SNo
x0
(
add_SNo
x1
(
add_SNo
x2
x3
)
)
=
add_SNo
x3
(
add_SNo
x0
(
add_SNo
x1
x2
)
)
Known
mul_SNo_distrL
mul_SNo_distrL
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
mul_SNo
x0
(
add_SNo
x1
x2
)
=
add_SNo
(
mul_SNo
x0
x1
)
(
mul_SNo
x0
x2
)
Known
SNo_add_SNo_3
SNo_add_SNo_3
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNo
(
add_SNo
x0
(
add_SNo
x1
x2
)
)
Known
add_SNo_minus_Lt2
add_SNo_minus_Lt2
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
x2
(
add_SNo
x0
(
minus_SNo
x1
)
)
⟶
SNoLt
(
add_SNo
x2
x1
)
x0
Known
minus_add_SNo_distr
minus_add_SNo_distr
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
minus_SNo
(
add_SNo
x0
x1
)
=
add_SNo
(
minus_SNo
x0
)
(
minus_SNo
x1
)
Known
add_SNo_rotate_3_1
add_SNo_rotate_3_1
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
add_SNo
x0
(
add_SNo
x1
x2
)
=
add_SNo
x2
(
add_SNo
x0
x1
)
Known
add_SNo_com
add_SNo_com
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
add_SNo
x0
x1
=
add_SNo
x1
x0
Known
mul_SNo_com_3_0_1
mul_SNo_com_3_0_1
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
mul_SNo
x0
(
mul_SNo
x1
x2
)
=
mul_SNo
x1
(
mul_SNo
x0
x2
)
Known
SNo_foil_mm
SNo_foil_mm
:
∀ x0 x1 x2 x3 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNo
x3
⟶
mul_SNo
(
add_SNo
x0
(
minus_SNo
x1
)
)
(
add_SNo
x2
(
minus_SNo
x3
)
)
=
add_SNo
(
mul_SNo
x0
x2
)
(
add_SNo
(
minus_SNo
(
mul_SNo
x0
x3
)
)
(
add_SNo
(
minus_SNo
(
mul_SNo
x1
x2
)
)
(
mul_SNo
x1
x3
)
)
)
Known
SNoLt_minus_pos
SNoLt_minus_pos
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLt
x0
x1
⟶
SNoLt
0
(
add_SNo
x1
(
minus_SNo
x0
)
)
Known
SNo_mul_SNo_3
SNo_mul_SNo_3
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNo
(
mul_SNo
x0
(
mul_SNo
x1
x2
)
)
Known
add_SNo_minus_Lt1
add_SNo_minus_Lt1
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
(
add_SNo
x0
(
minus_SNo
x1
)
)
x2
⟶
SNoLt
x0
(
add_SNo
x2
x1
)
Known
add_SNo_minus_Lt1b
add_SNo_minus_Lt1b
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
x0
(
add_SNo
x2
x1
)
⟶
SNoLt
(
add_SNo
x0
(
minus_SNo
x1
)
)
x2
Theorem
sqrt_SNo_nonneg_prop1a
sqrt_SNo_nonneg_prop1a
:
∀ x0 .
SNo
x0
⟶
SNoLe
0
x0
⟶
(
∀ x1 .
x1
∈
SNoS_
(
SNoLev
x0
)
⟶
SNoLe
0
x1
⟶
and
(
and
(
SNo
(
sqrt_SNo_nonneg
x1
)
)
(
SNoLe
0
(
sqrt_SNo_nonneg
x1
)
)
)
(
mul_SNo
(
sqrt_SNo_nonneg
x1
)
(
sqrt_SNo_nonneg
x1
)
=
x1
)
)
⟶
∀ x1 .
nat_p
x1
⟶
and
(
∀ x2 .
x2
∈
ap
(
SNo_sqrtaux
x0
sqrt_SNo_nonneg
x1
)
0
⟶
and
(
and
(
SNo
x2
)
(
SNoLe
0
x2
)
)
(
SNoLt
(
mul_SNo
x2
x2
)
x0
)
)
(
∀ x2 .
x2
∈
ap
(
SNo_sqrtaux
x0
sqrt_SNo_nonneg
x1
)
1
⟶
and
(
and
(
SNo
x2
)
(
SNoLe
0
x2
)
)
(
SNoLt
x0
(
mul_SNo
x2
x2
)
)
)
(proof)
Definition
SNoCutP
SNoCutP
:=
λ x0 x1 .
and
(
and
(
∀ x2 .
x2
∈
x0
⟶
SNo
x2
)
(
∀ x2 .
x2
∈
x1
⟶
SNo
x2
)
)
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x1
⟶
SNoLt
x2
x3
)
Param
famunion
famunion
:
ι
→
(
ι
→
ι
) →
ι
Known
famunionE_impred
famunionE_impred
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
famunion
x0
x1
⟶
∀ x3 : ο .
(
∀ x4 .
x4
∈
x0
⟶
x2
∈
x1
x4
⟶
x3
)
⟶
x3
Known
nonneg_mul_SNo_Le2
nonneg_mul_SNo_Le2
:
∀ x0 x1 x2 x3 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNo
x3
⟶
SNoLe
0
x0
⟶
SNoLe
0
x1
⟶
SNoLe
x0
x2
⟶
SNoLe
x1
x3
⟶
SNoLe
(
mul_SNo
x0
x1
)
(
mul_SNo
x2
x3
)
Theorem
sqrt_SNo_nonneg_prop1b
sqrt_SNo_nonneg_prop1b
:
∀ x0 .
SNo
x0
⟶
SNoLe
0
x0
⟶
(
∀ x1 .
nat_p
x1
⟶
and
(
∀ x2 .
x2
∈
ap
(
SNo_sqrtaux
x0
sqrt_SNo_nonneg
x1
)
0
⟶
and
(
and
(
SNo
x2
)
(
SNoLe
0
x2
)
)
(
SNoLt
(
mul_SNo
x2
x2
)
x0
)
)
(
∀ x2 .
x2
∈
ap
(
SNo_sqrtaux
x0
sqrt_SNo_nonneg
x1
)
1
⟶
and
(
and
(
SNo
x2
)
(
SNoLe
0
x2
)
)
(
SNoLt
x0
(
mul_SNo
x2
x2
)
)
)
)
⟶
SNoCutP
(
famunion
omega
(
λ x1 .
ap
(
SNo_sqrtaux
x0
sqrt_SNo_nonneg
x1
)
0
)
)
(
famunion
omega
(
λ x1 .
ap
(
SNo_sqrtaux
x0
sqrt_SNo_nonneg
x1
)
1
)
)
(proof)