Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrAa9..
/
aae8c..
PUSnY..
/
46451..
vout
PrAa9..
/
a9310..
5.46 bars
TMYTq..
/
54ace..
negprop ownership controlledby
Pr5Zc..
upto 0
TMHE1..
/
2d82b..
negprop ownership controlledby
Pr5Zc..
upto 0
TMcbJ..
/
2cf96..
ownership of
426ae..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMTHZ..
/
d5bc2..
ownership of
044a9..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMXhq..
/
0d879..
ownership of
ea079..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMYUv..
/
cd4b5..
ownership of
9008f..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMXBu..
/
5adc3..
ownership of
8ceb9..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMGYH..
/
c950b..
ownership of
30527..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMKKw..
/
12ada..
ownership of
4a201..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMaYm..
/
327a6..
ownership of
4c98b..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMEkS..
/
fc638..
ownership of
2ec25..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMFAb..
/
b9ab9..
ownership of
65e94..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMFWu..
/
eb4ff..
ownership of
8fb40..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMd5r..
/
6bc25..
ownership of
17925..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMRo5..
/
843d5..
ownership of
855eb..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMNPf..
/
1b2be..
ownership of
65d1d..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMGMd..
/
f4320..
ownership of
fc765..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMVe8..
/
32498..
ownership of
53d61..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMKUC..
/
43351..
ownership of
6b9fe..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMZVw..
/
4b1b7..
ownership of
fe405..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMMVm..
/
dc0f2..
ownership of
6996b..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMM8s..
/
a910e..
ownership of
011a0..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMa9U..
/
8c0af..
ownership of
8946c..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMXt6..
/
f7a14..
ownership of
df3ed..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMMFv..
/
12291..
ownership of
3b135..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMJdC..
/
1ee8a..
ownership of
3c6b5..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMcRe..
/
ab46e..
ownership of
506d4..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMG3Z..
/
60c52..
ownership of
3b0d7..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMTj7..
/
77a06..
ownership of
54e36..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMFFa..
/
170e9..
ownership of
6aedd..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMVLk..
/
d5cfb..
ownership of
a4bb2..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMZPy..
/
85cfb..
ownership of
d5ca4..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMJi9..
/
d41e5..
ownership of
d438a..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMYkc..
/
39d52..
ownership of
670a2..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMEgT..
/
b198d..
ownership of
d35ef..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMNKm..
/
1ff09..
ownership of
114cc..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMPrS..
/
2dd76..
ownership of
b2df3..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMZcF..
/
e8cb2..
ownership of
9b52c..
as prop with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMZD3..
/
9c5fe..
ownership of
c3146..
as obj with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
TMKqg..
/
c1384..
ownership of
22d50..
as obj with payaddr
Pr5Zc..
rights free controlledby
Pr5Zc..
upto 0
PUaSr..
/
4232e..
doc published by
Pr5Zc..
Param
nat_p
nat_p
:
ι
→
ο
Param
mul_nat
mul_nat
:
ι
→
ι
→
ι
Param
ordsucc
ordsucc
:
ι
→
ι
Known
nat_ind
nat_ind
:
∀ x0 :
ι → ο
.
x0
0
⟶
(
∀ x1 .
nat_p
x1
⟶
x0
x1
⟶
x0
(
ordsucc
x1
)
)
⟶
∀ x1 .
nat_p
x1
⟶
x0
x1
Known
mul_nat_1R
mul_nat_1R
:
∀ x0 .
mul_nat
x0
1
=
x0
Known
In_0_2
In_0_2
:
0
∈
2
Param
add_nat
add_nat
:
ι
→
ι
→
ι
Known
mul_nat_SR
mul_nat_SR
:
∀ x0 x1 .
nat_p
x1
⟶
mul_nat
x0
(
ordsucc
x1
)
=
add_nat
x0
(
mul_nat
x0
x1
)
Known
nat_ordsucc
nat_ordsucc
:
∀ x0 .
nat_p
x0
⟶
nat_p
(
ordsucc
x0
)
Known
add_nat_SL
add_nat_SL
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
add_nat
(
ordsucc
x0
)
x1
=
ordsucc
(
add_nat
x0
x1
)
Known
nat_1
nat_1
:
nat_p
1
Known
nat_0
nat_0
:
nat_p
0
Known
add_nat_0L
add_nat_0L
:
∀ x0 .
nat_p
x0
⟶
add_nat
0
x0
=
x0
Known
nat_ordsucc_in_ordsucc
nat_ordsucc_in_ordsucc
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
x1
∈
x0
⟶
ordsucc
x1
∈
ordsucc
x0
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Known
ordsuccI1
ordsuccI1
:
∀ x0 .
x0
⊆
ordsucc
x0
Known
mul_nat_p
mul_nat_p
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
nat_p
(
mul_nat
x0
x1
)
Known
nat_2
nat_2
:
nat_p
2
Theorem
nat_In_double_S
:
∀ x0 .
nat_p
x0
⟶
x0
∈
mul_nat
2
(
ordsucc
x0
)
(proof)
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Param
omega
omega
:
ι
Definition
odd_nat
odd_nat
:=
λ x0 .
and
(
x0
∈
omega
)
(
∀ x1 .
x1
∈
omega
⟶
x0
=
mul_nat
2
x1
⟶
∀ x2 : ο .
x2
)
Known
andI
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Known
nat_p_omega
nat_p_omega
:
∀ x0 .
nat_p
x0
⟶
x0
∈
omega
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
or
or
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x2
)
⟶
(
x1
⟶
x2
)
⟶
x2
Known
nat_inv
nat_inv
:
∀ x0 .
nat_p
x0
⟶
or
(
x0
=
0
)
(
∀ x1 : ο .
(
∀ x2 .
and
(
nat_p
x2
)
(
x0
=
ordsucc
x2
)
⟶
x1
)
⟶
x1
)
Known
omega_nat_p
omega_nat_p
:
∀ x0 .
x0
∈
omega
⟶
nat_p
x0
Known
neq_1_0
neq_1_0
:
1
=
0
⟶
∀ x0 : ο .
x0
Known
mul_nat_0R
mul_nat_0R
:
∀ x0 .
mul_nat
x0
0
=
0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Definition
nIn
nIn
:=
λ x0 x1 .
not
(
x0
∈
x1
)
Known
In_irref
In_irref
:
∀ x0 .
nIn
x0
x0
Known
nat_0_in_ordsucc
nat_0_in_ordsucc
:
∀ x0 .
nat_p
x0
⟶
0
∈
ordsucc
x0
Theorem
odd_nat_1
odd_nat_1
:
odd_nat
1
(proof)
Definition
even_nat
even_nat
:=
λ x0 .
and
(
x0
∈
omega
)
(
∀ x1 : ο .
(
∀ x2 .
and
(
x2
∈
omega
)
(
x0
=
mul_nat
2
x2
)
⟶
x1
)
⟶
x1
)
Theorem
even_nat_not_odd_nat
even_nat_not_odd_nat
:
∀ x0 .
even_nat
x0
⟶
not
(
odd_nat
x0
)
(proof)
Known
omega_ordsucc
omega_ordsucc
:
∀ x0 .
x0
∈
omega
⟶
ordsucc
x0
∈
omega
Theorem
even_nat_S_S
even_nat_S_S
:
∀ x0 .
even_nat
x0
⟶
even_nat
(
ordsucc
(
ordsucc
x0
)
)
(proof)
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
Theorem
even_nat_S_S_inv
even_nat_S_S_inv
:
∀ x0 .
nat_p
x0
⟶
even_nat
(
ordsucc
(
ordsucc
x0
)
)
⟶
even_nat
x0
(proof)
Theorem
even_nat_double
even_nat_double
:
∀ x0 .
nat_p
x0
⟶
even_nat
(
mul_nat
2
x0
)
(proof)
Param
exactly1of2
exactly1of2
:
ο
→
ο
→
ο
Known
exactly1of2_I1
exactly1of2_I1
:
∀ x0 x1 : ο .
x0
⟶
not
x1
⟶
exactly1of2
x0
x1
Known
exactly1of2_E
exactly1of2_E
:
∀ x0 x1 : ο .
exactly1of2
x0
x1
⟶
∀ x2 : ο .
(
x0
⟶
not
x1
⟶
x2
)
⟶
(
not
x0
⟶
x1
⟶
x2
)
⟶
x2
Known
exactly1of2_I2
exactly1of2_I2
:
∀ x0 x1 : ο .
not
x0
⟶
x1
⟶
exactly1of2
x0
x1
Theorem
even_nat_xor_S
even_nat_xor_S
:
∀ x0 .
nat_p
x0
⟶
exactly1of2
(
even_nat
x0
)
(
even_nat
(
ordsucc
x0
)
)
(proof)
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Theorem
not_even_nat_S_double
:
∀ x0 .
nat_p
x0
⟶
not
(
even_nat
(
ordsucc
(
mul_nat
2
x0
)
)
)
(proof)
Definition
inj
inj
:=
λ x0 x1 .
λ x2 :
ι → ι
.
and
(
∀ x3 .
x3
∈
x0
⟶
x2
x3
∈
x1
)
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
x2
x3
=
x2
x4
⟶
x3
=
x4
)
Definition
atleastp
atleastp
:=
λ x0 x1 .
∀ x2 : ο .
(
∀ x3 :
ι → ι
.
inj
x0
x1
x3
⟶
x2
)
⟶
x2
Known
form100_63_Cantor
form100_63_injCantor
:
∀ x0 .
∀ x1 :
ι → ι
.
not
(
inj
(
prim4
x0
)
x0
x1
)
Theorem
Cantor_atleastp
:
∀ x0 .
not
(
atleastp
(
prim4
x0
)
x0
)
(proof)
Param
SNo
SNo
:
ι
→
ο
Param
mul_SNo
mul_SNo
:
ι
→
ι
→
ι
Known
mul_SNo_oneL
mul_SNo_oneL
:
∀ x0 .
SNo
x0
⟶
mul_SNo
1
x0
=
x0
Param
eps_
eps_
:
ι
→
ι
Known
eps_1_half_eq3
eps_1_half_eq3
:
mul_SNo
(
eps_
1
)
2
=
1
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
Known
SNo_eps_1
SNo_eps_1
:
SNo
(
eps_
1
)
Known
SNo_2
SNo_2
:
SNo
2
Known
mul_nat_mul_SNo
mul_nat_mul_SNo
:
∀ x0 .
x0
∈
omega
⟶
∀ x1 .
x1
∈
omega
⟶
mul_nat
x0
x1
=
mul_SNo
x0
x1
Known
omega_SNo
omega_SNo
:
∀ x0 .
x0
∈
omega
⟶
SNo
x0
Theorem
double_omega_cancel
:
∀ x0 .
x0
∈
omega
⟶
∀ x1 .
x1
∈
omega
⟶
mul_nat
2
x0
=
mul_nat
2
x1
⟶
x0
=
x1
(proof)
Param
SNoLe
SNoLe
:
ι
→
ι
→
ο
Known
mul_SNo_zeroR
mul_SNo_zeroR
:
∀ x0 .
SNo
x0
⟶
mul_SNo
x0
0
=
0
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
SNo_0
SNo_0
:
SNo
0
Theorem
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
)
(proof)
Param
binunion
binunion
:
ι
→
ι
→
ι
Param
minus_SNo
minus_SNo
:
ι
→
ι
Definition
int
int
:=
binunion
omega
(
prim5
omega
minus_SNo
)
Definition
diadic_rational_p
diadic_rational_p
:=
λ x0 .
∀ x1 : ο .
(
∀ x2 .
and
(
x2
∈
omega
)
(
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
int
)
(
x0
=
mul_SNo
(
eps_
x2
)
x4
)
⟶
x3
)
⟶
x3
)
⟶
x1
)
⟶
x1
Param
SNoLt
SNoLt
:
ι
→
ι
→
ο
Param
ordinal
ordinal
:
ι
→
ο
Param
SNoS_
SNoS_
:
ι
→
ι
Param
SNoLev
SNoLev
:
ι
→
ι
Param
SNo_
SNo_
:
ι
→
ι
→
ο
Known
SNoS_E2
SNoS_E2
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
x1
∈
SNoS_
x0
⟶
∀ x2 : ο .
(
SNoLev
x1
∈
x0
⟶
ordinal
(
SNoLev
x1
)
⟶
SNo
x1
⟶
SNo_
(
SNoLev
x1
)
x1
⟶
x2
)
⟶
x2
Known
omega_ordinal
omega_ordinal
:
ordinal
omega
Known
diadic_rational_p_SNoS_omega
diadic_rational_p_SNoS_omega
:
∀ x0 .
diadic_rational_p
x0
⟶
x0
∈
SNoS_
omega
Known
binunionE
binunionE
:
∀ x0 x1 x2 .
x2
∈
binunion
x0
x1
⟶
or
(
x2
∈
x0
)
(
x2
∈
x1
)
Known
SNo_eps_
SNo_eps_
:
∀ x0 .
x0
∈
omega
⟶
SNo
(
eps_
x0
)
Known
SNoLe_ref
SNoLe_ref
:
∀ x0 .
SNoLe
x0
x0
Param
add_SNo
add_SNo
:
ι
→
ι
→
ι
Known
ordinal_ordsucc_SNo_eq
ordinal_ordsucc_SNo_eq
:
∀ x0 .
ordinal
x0
⟶
ordsucc
x0
=
add_SNo
1
x0
Known
nat_p_ordinal
nat_p_ordinal
:
∀ x0 .
nat_p
x0
⟶
ordinal
x0
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_1
SNo_1
:
SNo
1
Known
nat_p_SNo
nat_p_SNo
:
∀ x0 .
nat_p
x0
⟶
SNo
x0
Known
mul_SNo_oneR
mul_SNo_oneR
:
∀ x0 .
SNo
x0
⟶
mul_SNo
x0
1
=
x0
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
SNo_mul_SNo
SNo_mul_SNo
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNo
(
mul_SNo
x0
x1
)
Known
SNoLtLe
SNoLtLe
:
∀ x0 x1 .
SNoLt
x0
x1
⟶
SNoLe
x0
x1
Known
SNo_eps_pos
SNo_eps_pos
:
∀ x0 .
x0
∈
omega
⟶
SNoLt
0
(
eps_
x0
)
Known
ordinal_Subq_SNoLe
ordinal_Subq_SNoLe
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
x0
⊆
x1
⟶
SNoLe
x0
x1
Known
ordinal_Empty
ordinal_Empty
:
ordinal
0
Known
Subq_Empty
Subq_Empty
:
∀ x0 .
0
⊆
x0
Known
ReplE_impred
ReplE_impred
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
prim5
x0
x1
⟶
∀ x3 : ο .
(
∀ x4 .
x4
∈
x0
⟶
x2
=
x1
x4
⟶
x3
)
⟶
x3
Known
minus_SNo_0
minus_SNo_0
:
minus_SNo
0
=
0
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
minus_SNo_Le_contra
minus_SNo_Le_contra
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLe
x0
x1
⟶
SNoLe
(
minus_SNo
x1
)
(
minus_SNo
x0
)
Known
SNoLt_irref
SNoLt_irref
:
∀ x0 .
not
(
SNoLt
x0
x0
)
Known
SNoLeLt_tra
SNoLeLt_tra
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLe
x0
x1
⟶
SNoLt
x1
x2
⟶
SNoLt
x0
x2
Theorem
diadic_rational_p_pos_eps_between
:
∀ x0 .
diadic_rational_p
x0
⟶
SNoLt
0
x0
⟶
∀ x1 : ο .
(
∀ x2 .
and
(
x2
∈
omega
)
(
SNoLe
(
eps_
x2
)
x0
)
⟶
x1
)
⟶
x1
(proof)
Param
abs_SNo
abs_SNo
:
ι
→
ι
Param
binintersect
binintersect
:
ι
→
ι
→
ι
Param
SetAdjoin
SetAdjoin
:
ι
→
ι
→
ι
Param
Sing
Sing
:
ι
→
ι
Definition
SNoElts_
SNoElts_
:=
λ x0 .
binunion
x0
{
SetAdjoin
x1
(
Sing
1
)
|x1 ∈
x0
}
Param
iff
iff
:
ο
→
ο
→
ο
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
)
Known
xm
xm
:
∀ x0 : ο .
or
x0
(
not
x0
)
Known
orIR
orIR
:
∀ x0 x1 : ο .
x1
⟶
or
x0
x1
Known
SNoLt_tra
SNoLt_tra
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
x0
x1
⟶
SNoLt
x1
x2
⟶
SNoLt
x0
x2
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
SNo_minus_SNo
SNo_minus_SNo
:
∀ x0 .
SNo
x0
⟶
SNo
(
minus_SNo
x0
)
Known
SNoLtI2
SNoLtI2
:
∀ x0 x1 .
SNoLev
x0
∈
SNoLev
x1
⟶
SNoEq_
(
SNoLev
x0
)
x0
x1
⟶
SNoLev
x0
∈
x1
⟶
SNoLt
x0
x1
Known
restr_SNoLev
restr_SNoLev
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
x1
∈
SNoLev
x0
⟶
SNoLev
(
binintersect
x0
(
SNoElts_
x1
)
)
=
x1
Known
SNoEq_tra_
SNoEq_tra_
:
∀ x0 x1 x2 x3 .
SNoEq_
x0
x1
x2
⟶
SNoEq_
x0
x2
x3
⟶
SNoEq_
x0
x1
x3
Known
iffI
iffI
:
∀ x0 x1 : ο .
(
x0
⟶
x1
)
⟶
(
x1
⟶
x0
)
⟶
iff
x0
x1
Known
binintersectI
binintersectI
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
x2
∈
x1
⟶
x2
∈
binintersect
x0
x1
Known
binunionI1
binunionI1
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
x2
∈
binunion
x0
x1
Known
nat_trans
nat_trans
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
x1
∈
x0
⟶
x1
⊆
x0
Known
binintersectE1
binintersectE1
:
∀ x0 x1 x2 .
x2
∈
binintersect
x0
x1
⟶
x2
∈
x0
Known
orIL
orIL
:
∀ x0 x1 : ο .
x0
⟶
or
x0
x1
Known
dneg
dneg
:
∀ x0 : ο .
not
(
not
x0
)
⟶
x0
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
)
Known
minus_SNo_Lt_contra
minus_SNo_Lt_contra
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLt
x0
x1
⟶
SNoLt
(
minus_SNo
x1
)
(
minus_SNo
x0
)
Known
SNoLtI3
SNoLtI3
:
∀ x0 x1 .
SNoLev
x1
∈
SNoLev
x0
⟶
SNoEq_
(
SNoLev
x1
)
x0
x1
⟶
nIn
(
SNoLev
x1
)
x0
⟶
SNoLt
x0
x1
Known
SNoEq_sym_
SNoEq_sym_
:
∀ x0 x1 x2 .
SNoEq_
x0
x1
x2
⟶
SNoEq_
x0
x2
x1
Known
Subq_ref
Subq_ref
:
∀ x0 .
x0
⊆
x0
Known
EmptyE
EmptyE
:
∀ x0 .
nIn
x0
0
Known
ordsuccE
ordsuccE
:
∀ x0 x1 .
x1
∈
ordsucc
x0
⟶
or
(
x1
∈
x0
)
(
x1
=
x0
)
Known
ordsuccI2
ordsuccI2
:
∀ x0 .
x0
∈
ordsucc
x0
Known
Subq_tra
Subq_tra
:
∀ x0 x1 x2 .
x0
⊆
x1
⟶
x1
⊆
x2
⟶
x0
⊆
x2
Known
restr_SNoEq
restr_SNoEq
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
x1
∈
SNoLev
x0
⟶
SNoEq_
x1
(
binintersect
x0
(
SNoElts_
x1
)
)
x0
Known
SNoS_omega_diadic_rational_p
SNoS_omega_diadic_rational_p
:
∀ x0 .
x0
∈
SNoS_
omega
⟶
diadic_rational_p
x0
Known
add_SNo_Lt1_cancel
add_SNo_Lt1_cancel
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
(
add_SNo
x0
x1
)
(
add_SNo
x2
x1
)
⟶
SNoLt
x0
x2
Known
add_SNo_0L
add_SNo_0L
:
∀ x0 .
SNo
x0
⟶
add_SNo
0
x0
=
x0
Known
add_SNo_minus_R2'
add_SNo_minus_R2
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
add_SNo
(
add_SNo
x0
(
minus_SNo
x1
)
)
x1
=
x0
Known
add_SNo_SNoS_omega
add_SNo_SNoS_omega
:
∀ x0 .
x0
∈
SNoS_
omega
⟶
∀ x1 .
x1
∈
SNoS_
omega
⟶
add_SNo
x0
x1
∈
SNoS_
omega
Known
minus_SNo_SNoS_omega
minus_SNo_SNoS_omega
:
∀ x0 .
x0
∈
SNoS_
omega
⟶
minus_SNo
x0
∈
SNoS_
omega
Known
SNoS_I
SNoS_I
:
∀ x0 .
ordinal
x0
⟶
∀ x1 x2 .
x2
∈
x0
⟶
SNo_
x2
x1
⟶
x1
∈
SNoS_
x0
Known
restr_SNo_
restr_SNo_
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
x1
∈
SNoLev
x0
⟶
SNo_
x1
(
binintersect
x0
(
SNoElts_
x1
)
)
Known
abs_SNo_dist_swap
abs_SNo_dist_swap
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
abs_SNo
(
add_SNo
x0
(
minus_SNo
x1
)
)
=
abs_SNo
(
add_SNo
x1
(
minus_SNo
x0
)
)
Known
nonneg_abs_SNo
nonneg_abs_SNo
:
∀ x0 .
SNoLe
0
x0
⟶
abs_SNo
x0
=
x0
Known
SNo_add_SNo
SNo_add_SNo
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNo
(
add_SNo
x0
x1
)
Known
SNoLev_uniq
SNoLev_uniq
:
∀ x0 x1 x2 .
ordinal
x1
⟶
ordinal
x2
⟶
SNo_
x1
x0
⟶
SNo_
x2
x0
⟶
x1
=
x2
Known
SNoLev_ordinal
SNoLev_ordinal
:
∀ x0 .
SNo
x0
⟶
ordinal
(
SNoLev
x0
)
Known
SNoLev_
SNoLev_
:
∀ x0 .
SNo
x0
⟶
SNo_
(
SNoLev
x0
)
x0
Known
SNo_SNo
SNo_SNo
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
SNo_
x0
x1
⟶
SNo
x1
Theorem
8fb40..
:
∀ x0 .
SNo_
omega
x0
⟶
∀ x1 .
x1
∈
SNoS_
omega
⟶
(
∀ x2 .
x2
∈
omega
⟶
SNoLt
(
abs_SNo
(
add_SNo
x1
(
minus_SNo
x0
)
)
)
(
eps_
x2
)
)
⟶
or
(
and
(
nIn
(
SNoLev
x1
)
x0
)
(
∀ x2 .
x2
∈
omega
⟶
SNoLev
x1
∈
x2
⟶
x2
∈
x0
)
)
(
and
(
SNoLev
x1
∈
x0
)
(
∀ x2 .
x2
∈
omega
⟶
SNoLev
x1
∈
x2
⟶
nIn
x2
x0
)
)
(proof)
Known
minus_SNo_In
minus_SNo_In
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
x1
∈
SNoLev
x0
⟶
x1
∈
x0
⟶
nIn
x1
(
minus_SNo
x0
)
Known
SNo_omega
SNo_omega
:
SNo
omega
Known
ordinal_SNoLev
ordinal_SNoLev
:
∀ x0 .
ordinal
x0
⟶
SNoLev
x0
=
x0
Theorem
nat_nIn_minus_SNo_omega
:
∀ x0 .
x0
∈
omega
⟶
nIn
x0
(
minus_SNo
omega
)
(proof)
Param
real
real
:
ι
Param
Sep
Sep
:
ι
→
(
ι
→
ο
) →
ι
Param
ReplSep
ReplSep
:
ι
→
(
ι
→
ο
) →
(
ι
→
ι
) →
ι
Definition
PSNo
PSNo
:=
λ x0 .
λ x1 :
ι → ο
.
binunion
(
Sep
x0
x1
)
{
SetAdjoin
x2
(
Sing
1
)
|x2 ∈
x0
,
not
(
x1
x2
)
}
Known
real_I
real_I
:
∀ x0 .
x0
∈
SNoS_
(
ordsucc
omega
)
⟶
(
x0
=
omega
⟶
∀ x1 : ο .
x1
)
⟶
(
x0
=
minus_SNo
omega
⟶
∀ x1 : ο .
x1
)
⟶
(
∀ x1 .
x1
∈
SNoS_
omega
⟶
(
∀ x2 .
x2
∈
omega
⟶
SNoLt
(
abs_SNo
(
add_SNo
x1
(
minus_SNo
x0
)
)
)
(
eps_
x2
)
)
⟶
x1
=
x0
)
⟶
x0
∈
real
Known
ordsucc_omega_ordinal
ordsucc_omega_ordinal
:
ordinal
(
ordsucc
omega
)
Known
nat_3
nat_3
:
nat_p
3
Known
SNoLev_uniq2
SNoLev_uniq2
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
SNo_
x0
x1
⟶
SNoLev
x1
=
x0
Known
SNo_PSNo
SNo_PSNo
:
∀ x0 .
ordinal
x0
⟶
∀ x1 :
ι → ο
.
SNo_
x0
(
PSNo
x0
x1
)
Known
PowerE
PowerE
:
∀ x0 x1 .
x1
∈
prim4
x0
⟶
x1
⊆
x0
Known
set_ext
set_ext
:
∀ x0 x1 .
x0
⊆
x1
⟶
x1
⊆
x0
⟶
x0
=
x1
Known
SepI
SepI
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
x0
⟶
x1
x2
⟶
x2
∈
Sep
x0
x1
Known
ReplSepI
ReplSepI
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 :
ι → ι
.
∀ x3 .
x3
∈
x0
⟶
x1
x3
⟶
x2
x3
∈
ReplSep
x0
x1
x2
Known
SepE2
SepE2
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
Sep
x0
x1
⟶
x1
x2
Known
ReplSepE_impred
ReplSepE_impred
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 :
ι → ι
.
∀ x3 .
x3
∈
ReplSep
x0
x1
x2
⟶
∀ x4 : ο .
(
∀ x5 .
x5
∈
x0
⟶
x1
x5
⟶
x3
=
x2
x5
⟶
x4
)
⟶
x4
Known
tagged_not_ordinal
tagged_not_ordinal
:
∀ x0 .
not
(
ordinal
(
SetAdjoin
x0
(
Sing
1
)
)
)
Known
ReplI
ReplI
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
x0
⟶
x1
x2
∈
prim5
x0
x1
Theorem
atleastp_Power_omega_real
:
atleastp
(
prim4
omega
)
real
(proof)
Param
equip
equip
:
ι
→
ι
→
ο
Known
atleastp_tra
atleastp_tra
:
∀ x0 x1 x2 .
atleastp
x0
x1
⟶
atleastp
x1
x2
⟶
atleastp
x0
x2
Known
equip_atleastp
equip_atleastp
:
∀ x0 x1 .
equip
x0
x1
⟶
atleastp
x0
x1
Known
equip_sym
equip_sym
:
∀ x0 x1 .
equip
x0
x1
⟶
equip
x1
x0
Theorem
real_uncountable
:
not
(
equip
omega
real
)
(proof)
Param
explicit_Field
explicit_Field
:
ι
→
ι
→
ι
→
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
ο
Known
explicit_Field_I
explicit_Field_I
:
∀ x0 x1 x2 .
∀ x3 x4 :
ι →
ι → ι
.
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
x3
x5
x6
∈
x0
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x3
x5
(
x3
x6
x7
)
=
x3
(
x3
x5
x6
)
x7
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
x3
x5
x6
=
x3
x6
x5
)
⟶
x1
∈
x0
⟶
(
∀ x5 .
x5
∈
x0
⟶
x3
x1
x5
=
x5
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 : ο .
(
∀ x7 .
and
(
x7
∈
x0
)
(
x3
x5
x7
=
x1
)
⟶
x6
)
⟶
x6
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
x4
x5
x6
∈
x0
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x4
x5
(
x4
x6
x7
)
=
x4
(
x4
x5
x6
)
x7
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
x4
x5
x6
=
x4
x6
x5
)
⟶
x2
∈
x0
⟶
(
x2
=
x1
⟶
∀ x5 : ο .
x5
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
x4
x2
x5
=
x5
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
(
x5
=
x1
⟶
∀ x6 : ο .
x6
)
⟶
∀ x6 : ο .
(
∀ x7 .
and
(
x7
∈
x0
)
(
x4
x5
x7
=
x2
)
⟶
x6
)
⟶
x6
)
⟶
(
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x4
x5
(
x3
x6
x7
)
=
x3
(
x4
x5
x6
)
(
x4
x5
x7
)
)
⟶
explicit_Field
x0
x1
x2
x3
x4
Known
real_add_SNo
real_add_SNo
:
∀ x0 .
x0
∈
real
⟶
∀ x1 .
x1
∈
real
⟶
add_SNo
x0
x1
∈
real
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
real_SNo
real_SNo
:
∀ x0 .
x0
∈
real
⟶
SNo
x0
Known
add_SNo_com
add_SNo_com
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
add_SNo
x0
x1
=
add_SNo
x1
x0
Known
real_0
real_0
:
0
∈
real
Known
real_minus_SNo
real_minus_SNo
:
∀ x0 .
x0
∈
real
⟶
minus_SNo
x0
∈
real
Known
add_SNo_minus_SNo_rinv
add_SNo_minus_SNo_rinv
:
∀ x0 .
SNo
x0
⟶
add_SNo
x0
(
minus_SNo
x0
)
=
0
Known
real_mul_SNo
real_mul_SNo
:
∀ x0 .
x0
∈
real
⟶
∀ x1 .
x1
∈
real
⟶
mul_SNo
x0
x1
∈
real
Known
mul_SNo_com
mul_SNo_com
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
mul_SNo
x0
x1
=
mul_SNo
x1
x0
Known
real_1
real_1
:
1
∈
real
Known
nonzero_real_recip_ex
nonzero_real_recip_ex
:
∀ x0 .
x0
∈
real
⟶
(
x0
=
0
⟶
∀ x1 : ο .
x1
)
⟶
∀ x1 : ο .
(
∀ x2 .
and
(
x2
∈
real
)
(
mul_SNo
x0
x2
=
1
)
⟶
x1
)
⟶
x1
Theorem
explicit_Field_real
:
explicit_Field
real
0
1
add_SNo
mul_SNo
(proof)
Param
explicit_OrderedField
explicit_OrderedField
:
ι
→
ι
→
ι
→
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ο
) →
ο
Known
explicit_OrderedField_I
explicit_OrderedField_I
:
∀ x0 x1 x2 .
∀ x3 x4 :
ι →
ι → ι
.
∀ x5 :
ι →
ι → ο
.
explicit_Field
x0
x1
x2
x3
x4
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
x5
x6
x7
⟶
x5
x7
x8
⟶
x5
x6
x8
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
iff
(
and
(
x5
x6
x7
)
(
x5
x7
x6
)
)
(
x6
=
x7
)
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
or
(
x5
x6
x7
)
(
x5
x7
x6
)
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
x5
x6
x7
⟶
x5
(
x3
x6
x8
)
(
x3
x7
x8
)
)
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
x5
x1
x6
⟶
x5
x1
x7
⟶
x5
x1
(
x4
x6
x7
)
)
⟶
explicit_OrderedField
x0
x1
x2
x3
x4
x5
Known
SNoLe_tra
SNoLe_tra
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLe
x0
x1
⟶
SNoLe
x1
x2
⟶
SNoLe
x0
x2
Known
SNoLe_antisym
SNoLe_antisym
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLe
x0
x1
⟶
SNoLe
x1
x0
⟶
x0
=
x1
Known
SNoLtLe_or
SNoLtLe_or
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
or
(
SNoLt
x0
x1
)
(
SNoLe
x1
x0
)
Known
add_SNo_Le1
add_SNo_Le1
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLe
x0
x2
⟶
SNoLe
(
add_SNo
x0
x1
)
(
add_SNo
x2
x1
)
Theorem
explicit_OrderedField_real
:
explicit_OrderedField
real
0
1
add_SNo
mul_SNo
SNoLe
(proof)
Param
explicit_Reals
explicit_Reals
:
ι
→
ι
→
ι
→
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ο
) →
ο
Param
natOfOrderedField_p
natOfOrderedField_p
:
ι
→
ι
→
ι
→
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ο
) →
ι
→
ο
Param
explicit_Nats
explicit_Nats
:
ι
→
ι
→
(
ι
→
ι
) →
ο
Known
explicit_Nats_E
explicit_Nats_E
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
∀ x3 : ο .
(
explicit_Nats
x0
x1
x2
⟶
x1
∈
x0
⟶
(
∀ x4 .
x4
∈
x0
⟶
x2
x4
∈
x0
)
⟶
(
∀ x4 .
x4
∈
x0
⟶
x2
x4
=
x1
⟶
∀ x5 : ο .
x5
)
⟶
(
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
x2
x4
=
x2
x5
⟶
x4
=
x5
)
⟶
(
∀ x4 :
ι → ο
.
x4
x1
⟶
(
∀ x5 .
x4
x5
⟶
x4
(
x2
x5
)
)
⟶
∀ x5 .
x5
∈
x0
⟶
x4
x5
)
⟶
x3
)
⟶
explicit_Nats
x0
x1
x2
⟶
x3
Definition
lt
lt
:=
λ x0 x1 x2 .
λ x3 x4 :
ι →
ι → ι
.
λ x5 :
ι →
ι → ο
.
λ x6 x7 .
and
(
x5
x6
x7
)
(
x6
=
x7
⟶
∀ x8 : ο .
x8
)
Param
setexp
setexp
:
ι
→
ι
→
ι
Param
ap
ap
:
ι
→
ι
→
ι
Known
explicit_Reals_I
explicit_Reals_I
:
∀ x0 x1 x2 .
∀ x3 x4 :
ι →
ι → ι
.
∀ x5 :
ι →
ι → ο
.
explicit_OrderedField
x0
x1
x2
x3
x4
x5
⟶
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
lt
x0
x1
x2
x3
x4
x5
x1
x6
⟶
x5
x1
x7
⟶
∀ x8 : ο .
(
∀ x9 .
and
(
x9
∈
Sep
x0
(
natOfOrderedField_p
x0
x1
x2
x3
x4
x5
)
)
(
x5
x7
(
x4
x9
x6
)
)
⟶
x8
)
⟶
x8
)
⟶
(
∀ x6 .
x6
∈
setexp
x0
(
Sep
x0
(
natOfOrderedField_p
x0
x1
x2
x3
x4
x5
)
)
⟶
∀ x7 .
x7
∈
setexp
x0
(
Sep
x0
(
natOfOrderedField_p
x0
x1
x2
x3
x4
x5
)
)
⟶
(
∀ x8 .
x8
∈
Sep
x0
(
natOfOrderedField_p
x0
x1
x2
x3
x4
x5
)
⟶
and
(
and
(
x5
(
ap
x6
x8
)
(
ap
x7
x8
)
)
(
x5
(
ap
x6
x8
)
(
ap
x6
(
x3
x8
x2
)
)
)
)
(
x5
(
ap
x7
(
x3
x8
x2
)
)
(
ap
x7
x8
)
)
)
⟶
∀ x8 : ο .
(
∀ x9 .
and
(
x9
∈
x0
)
(
∀ x10 .
x10
∈
Sep
x0
(
natOfOrderedField_p
x0
x1
x2
x3
x4
x5
)
⟶
and
(
x5
(
ap
x6
x10
)
x9
)
(
x5
x9
(
ap
x7
x10
)
)
)
⟶
x8
)
⟶
x8
)
⟶
explicit_Reals
x0
x1
x2
x3
x4
x5
Known
real_Archimedean
real_Archimedean
:
∀ x0 .
x0
∈
real
⟶
∀ x1 .
x1
∈
real
⟶
SNoLt
0
x0
⟶
SNoLe
0
x1
⟶
∀ x2 : ο .
(
∀ x3 .
and
(
x3
∈
omega
)
(
SNoLe
x1
(
mul_SNo
x3
x0
)
)
⟶
x2
)
⟶
x2
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
SNoLtLe_tra
SNoLtLe_tra
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
x0
x1
⟶
SNoLe
x1
x2
⟶
SNoLt
x0
x2
Known
real_complete2
real_complete2
:
∀ x0 .
x0
∈
setexp
real
omega
⟶
∀ x1 .
x1
∈
setexp
real
omega
⟶
(
∀ x2 .
x2
∈
omega
⟶
and
(
and
(
SNoLe
(
ap
x0
x2
)
(
ap
x1
x2
)
)
(
SNoLe
(
ap
x0
x2
)
(
ap
x0
(
add_SNo
x2
1
)
)
)
)
(
SNoLe
(
ap
x1
(
add_SNo
x2
1
)
)
(
ap
x1
x2
)
)
)
⟶
∀ x2 : ο .
(
∀ x3 .
and
(
x3
∈
real
)
(
∀ x4 .
x4
∈
omega
⟶
and
(
SNoLe
(
ap
x0
x4
)
x3
)
(
SNoLe
x3
(
ap
x1
x4
)
)
)
⟶
x2
)
⟶
x2
Known
add_nat_add_SNo
add_nat_add_SNo
:
∀ x0 .
x0
∈
omega
⟶
∀ x1 .
x1
∈
omega
⟶
add_nat
x0
x1
=
add_SNo
x0
x1
Known
add_nat_p
add_nat_p
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
nat_p
(
add_nat
x0
x1
)
Known
ordinal_Hered
ordinal_Hered
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
x1
∈
x0
⟶
ordinal
x1
Known
explicit_Nats_natOfOrderedField
explicit_Nats_natOfOrderedField
:
∀ x0 x1 x2 .
∀ x3 x4 :
ι →
ι → ι
.
∀ x5 :
ι →
ι → ο
.
explicit_OrderedField
x0
x1
x2
x3
x4
x5
⟶
explicit_Nats
(
Sep
x0
(
natOfOrderedField_p
x0
x1
x2
x3
x4
x5
)
)
x1
(
λ x6 .
x3
x6
x2
)
Theorem
explicit_Reals_real
:
explicit_Reals
real
0
1
add_SNo
mul_SNo
SNoLe
(proof)
Definition
c3146..
:=
λ x0 x1 x2 .
λ x3 x4 :
ι →
ι → ι
.
λ x5 :
ι →
ι → ο
.
λ x6 .
∀ x7 : ο .
(
∀ x8 .
(
∀ x9 : ο .
(
∀ x10 .
and
(
and
(
natOfOrderedField_p
x0
x1
x2
x3
x4
x5
x8
)
(
natOfOrderedField_p
x0
x1
x2
x3
x4
x5
x10
)
)
(
x4
x10
x6
=
x8
)
⟶
x9
)
⟶
x9
)
⟶
x7
)
⟶
x7
Known
Sep_Subq
Sep_Subq
:
∀ x0 .
∀ x1 :
ι → ο
.
Sep
x0
x1
⊆
x0
Known
and3I
and3I
:
∀ x0 x1 x2 : ο .
x0
⟶
x1
⟶
x2
⟶
and
(
and
x0
x1
)
x2
Known
explicit_Field_zero_multL
explicit_Field_zero_multL
:
∀ x0 x1 x2 .
∀ x3 x4 :
ι →
ι → ι
.
explicit_Field
x0
x1
x2
x3
x4
⟶
∀ x5 .
x5
∈
x0
⟶
x4
x1
x5
=
x1
Known
explicit_OrderedField_E
explicit_OrderedField_E
:
∀ x0 x1 x2 .
∀ x3 x4 :
ι →
ι → ι
.
∀ x5 :
ι →
ι → ο
.
∀ x6 : ο .
(
explicit_OrderedField
x0
x1
x2
x3
x4
x5
⟶
explicit_Field
x0
x1
x2
x3
x4
⟶
(
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
x5
x7
x8
⟶
x5
x8
x9
⟶
x5
x7
x9
)
⟶
(
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
iff
(
and
(
x5
x7
x8
)
(
x5
x8
x7
)
)
(
x7
=
x8
)
)
⟶
(
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
or
(
x5
x7
x8
)
(
x5
x8
x7
)
)
⟶
(
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
x5
x7
x8
⟶
x5
(
x3
x7
x9
)
(
x3
x8
x9
)
)
⟶
(
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
x5
x1
x7
⟶
x5
x1
x8
⟶
x5
x1
(
x4
x7
x8
)
)
⟶
x6
)
⟶
explicit_OrderedField
x0
x1
x2
x3
x4
x5
⟶
x6
Theorem
ea079..
:
∀ x0 x1 x2 .
∀ x3 x4 :
ι →
ι → ι
.
∀ x5 :
ι →
ι → ο
.
explicit_OrderedField
x0
x1
x2
x3
x4
x5
⟶
Sep
x0
(
c3146..
x0
x1
x2
x3
x4
x5
)
=
x0
(proof)
Theorem
426ae..
:
(
∀ x0 x1 x2 .
∀ x3 x4 :
ι →
ι → ι
.
∀ x5 :
ι →
ι → ο
.
explicit_Reals
x0
x1
x2
x3
x4
x5
⟶
equip
omega
(
Sep
x0
(
c3146..
x0
x1
x2
x3
x4
x5
)
)
)
⟶
∀ x0 : ο .
x0
(proof)