Search for blocks/addresses/...
Proofgold Signed Transaction
vin
Pr48i..
/
d3472..
PUe1o..
/
665bf..
vout
Pr48i..
/
a66a1..
0.07 bars
TMK3B..
/
a7f76..
ownership of
963bd..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMXEU..
/
0e839..
ownership of
a9c76..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMJcf..
/
6b887..
ownership of
bf97d..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMFEt..
/
bdf21..
ownership of
85a5e..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMYwd..
/
774c5..
ownership of
4e625..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMJHN..
/
32b09..
ownership of
bd7ab..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMaaU..
/
dcb64..
ownership of
e4ff6..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMHyo..
/
c74e4..
ownership of
ed6a3..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMRtp..
/
2a764..
ownership of
bc482..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMYQu..
/
a138b..
ownership of
bb6f7..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMK2p..
/
2185a..
ownership of
cc109..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMGib..
/
afed8..
ownership of
d306d..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMUo7..
/
9e210..
ownership of
c250b..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMSbe..
/
eac01..
ownership of
40b04..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMbi4..
/
3994d..
ownership of
8a4cf..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMcXa..
/
0366b..
ownership of
88ce9..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMHvZ..
/
045ec..
ownership of
418cf..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMcsC..
/
355d5..
ownership of
6dafe..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMcxv..
/
f0855..
ownership of
3dea6..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMZS1..
/
1a8fc..
ownership of
b7e7a..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMGwn..
/
29cd1..
ownership of
f4056..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMNtL..
/
8e923..
ownership of
a7bc9..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMbTE..
/
b600b..
ownership of
b2c59..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMTPG..
/
fd386..
ownership of
00e71..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMF8o..
/
d82e1..
ownership of
1036d..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMUCt..
/
55de9..
ownership of
d6697..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMWod..
/
fc4c1..
ownership of
aab9d..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMYnN..
/
2918b..
ownership of
8f004..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMJXh..
/
17aef..
ownership of
3a259..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMJkS..
/
bf12d..
ownership of
86950..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMdSi..
/
bfbed..
ownership of
b1bb2..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMS2o..
/
2d351..
ownership of
405dd..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMJzr..
/
8eecf..
ownership of
6089e..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMFj4..
/
05649..
ownership of
19fdd..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMGYK..
/
c96ea..
ownership of
14278..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMGbS..
/
85aff..
ownership of
60107..
as prop with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMP68..
/
cd279..
ownership of
25bca..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMFaW..
/
d67cb..
ownership of
a02ca..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMVTd..
/
b9f6f..
ownership of
33166..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMXnk..
/
3f4bb..
ownership of
90ee8..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
PUMdw..
/
91191..
doc published by
PrGxv..
Param
omega
omega
:
ι
Param
mul_SNo
mul_SNo
:
ι
→
ι
→
ι
Param
eps_
eps_
:
ι
→
ι
Param
add_SNo
add_SNo
:
ι
→
ι
→
ι
Known
mul_SNo_eps_eps_add_SNo
mul_SNo_eps_eps_add_SNo
:
∀ x0 .
x0
∈
omega
⟶
∀ x1 .
x1
∈
omega
⟶
mul_SNo
(
eps_
x0
)
(
eps_
x1
)
=
eps_
(
add_SNo
x0
x1
)
Param
SNo
SNo
:
ι
→
ο
Known
mul_SNo_com_4_inner_mid
mul_SNo_com_4_inner_mid
:
∀ x0 x1 x2 x3 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNo
x3
⟶
mul_SNo
(
mul_SNo
x0
x1
)
(
mul_SNo
x2
x3
)
=
mul_SNo
(
mul_SNo
x0
x2
)
(
mul_SNo
x1
x3
)
Param
nat_p
nat_p
:
ι
→
ο
Param
exp_SNo_nat
exp_SNo_nat
:
ι
→
ι
→
ι
Known
nat_exp_SNo_nat
nat_exp_SNo_nat
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
nat_p
(
exp_SNo_nat
x0
x1
)
Param
ordsucc
ordsucc
:
ι
→
ι
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
binunion
binunion
:
ι
→
ι
→
ι
Param
minus_SNo
minus_SNo
:
ι
→
ι
Definition
int
int
:=
binunion
omega
(
prim5
omega
minus_SNo
)
Definition
or
or
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x2
)
⟶
(
x1
⟶
x2
)
⟶
x2
Known
binunionE
binunionE
:
∀ x0 x1 x2 .
x2
∈
binunion
x0
x1
⟶
or
(
x2
∈
x0
)
(
x2
∈
x1
)
Known
ReplE_impred
ReplE_impred
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
prim5
x0
x1
⟶
∀ x3 : ο .
(
∀ x4 .
x4
∈
x0
⟶
x2
=
x1
x4
⟶
x3
)
⟶
x3
Theorem
int_SNo_cases
int_SNo_cases
:
∀ x0 :
ι → ο
.
(
∀ x1 .
x1
∈
omega
⟶
x0
x1
)
⟶
(
∀ x1 .
x1
∈
omega
⟶
x0
(
minus_SNo
x1
)
)
⟶
∀ x1 .
x1
∈
int
⟶
x0
x1
(proof)
Known
omega_SNo
omega_SNo
:
∀ x0 .
x0
∈
omega
⟶
SNo
x0
Known
SNo_minus_SNo
SNo_minus_SNo
:
∀ x0 .
SNo
x0
⟶
SNo
(
minus_SNo
x0
)
Theorem
int_SNo
int_SNo
:
∀ x0 .
x0
∈
int
⟶
SNo
x0
(proof)
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Known
binunionI1
binunionI1
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
x2
∈
binunion
x0
x1
Theorem
Subq_omega_int
Subq_omega_int
:
omega
⊆
int
(proof)
Known
binunionI2
binunionI2
:
∀ x0 x1 x2 .
x2
∈
x1
⟶
x2
∈
binunion
x0
x1
Known
ReplI
ReplI
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
x0
⟶
x1
x2
∈
prim5
x0
x1
Theorem
int_minus_SNo_omega
int_minus_SNo_omega
:
∀ x0 .
x0
∈
omega
⟶
minus_SNo
x0
∈
int
(proof)
Known
nat_ind
nat_ind
:
∀ x0 :
ι → ο
.
x0
0
⟶
(
∀ x1 .
nat_p
x1
⟶
x0
x1
⟶
x0
(
ordsucc
x1
)
)
⟶
∀ x1 .
nat_p
x1
⟶
x0
x1
Known
add_SNo_0R
add_SNo_0R
:
∀ x0 .
SNo
x0
⟶
add_SNo
x0
0
=
x0
Param
ordinal
ordinal
:
ι
→
ο
Known
ordinal_SNo
ordinal_SNo
:
∀ x0 .
ordinal
x0
⟶
SNo
x0
Known
nat_p_ordinal
nat_p_ordinal
:
∀ x0 .
nat_p
x0
⟶
ordinal
x0
Known
omega_nat_p
omega_nat_p
:
∀ x0 .
x0
∈
omega
⟶
nat_p
x0
Known
ordinal_ordsucc_SNo_eq
ordinal_ordsucc_SNo_eq
:
∀ x0 .
ordinal
x0
⟶
ordsucc
x0
=
add_SNo
1
x0
Known
add_SNo_com_3_0_1
add_SNo_com_3_0_1
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
add_SNo
x0
(
add_SNo
x1
x2
)
=
add_SNo
x1
(
add_SNo
x0
x2
)
Known
SNo_1
SNo_1
:
SNo
1
Known
omega_ordsucc
omega_ordsucc
:
∀ x0 .
x0
∈
omega
⟶
ordsucc
x0
∈
omega
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
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
minus_SNo_0
minus_SNo_0
:
minus_SNo
0
=
0
Known
nat_p_omega
nat_p_omega
:
∀ x0 .
nat_p
x0
⟶
x0
∈
omega
Known
nat_1
nat_1
:
nat_p
1
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_minus_SNo_prop2
add_SNo_minus_SNo_prop2
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
add_SNo
x0
(
add_SNo
(
minus_SNo
x0
)
x1
)
=
x1
Theorem
int_add_SNo_lem
int_add_SNo_lem
:
∀ x0 .
x0
∈
omega
⟶
∀ x1 .
nat_p
x1
⟶
add_SNo
(
minus_SNo
x0
)
x1
∈
int
(proof)
Known
add_SNo_In_omega
add_SNo_In_omega
:
∀ x0 .
x0
∈
omega
⟶
∀ x1 .
x1
∈
omega
⟶
add_SNo
x0
x1
∈
omega
Known
add_SNo_com
add_SNo_com
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
add_SNo
x0
x1
=
add_SNo
x1
x0
Theorem
int_add_SNo
int_add_SNo
:
∀ x0 .
x0
∈
int
⟶
∀ x1 .
x1
∈
int
⟶
add_SNo
x0
x1
∈
int
(proof)
Known
minus_SNo_invol
minus_SNo_invol
:
∀ x0 .
SNo
x0
⟶
minus_SNo
(
minus_SNo
x0
)
=
x0
Theorem
int_minus_SNo
int_minus_SNo
:
∀ x0 .
x0
∈
int
⟶
minus_SNo
x0
∈
int
(proof)
Known
mul_SNo_In_omega
mul_SNo_In_omega
:
∀ x0 .
x0
∈
omega
⟶
∀ x1 .
x1
∈
omega
⟶
mul_SNo
x0
x1
∈
omega
Known
mul_SNo_com
mul_SNo_com
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
mul_SNo
x0
x1
=
mul_SNo
x1
x0
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
)
Known
SNo_mul_SNo
SNo_mul_SNo
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNo
(
mul_SNo
x0
x1
)
Theorem
int_mul_SNo
int_mul_SNo
:
∀ x0 .
x0
∈
int
⟶
∀ x1 .
x1
∈
int
⟶
mul_SNo
x0
x1
∈
int
(proof)
Param
SNoS_
SNoS_
:
ι
→
ι
Known
nonneg_diadic_rational_p_SNoS_omega
nonneg_diadic_rational_p_SNoS_omega
:
∀ x0 .
x0
∈
omega
⟶
∀ x1 .
nat_p
x1
⟶
mul_SNo
(
eps_
x0
)
x1
∈
SNoS_
omega
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
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
SNo_eps_
SNo_eps_
:
∀ x0 .
x0
∈
omega
⟶
SNo
(
eps_
x0
)
Known
minus_SNo_SNoS_omega
minus_SNo_SNoS_omega
:
∀ x0 .
x0
∈
SNoS_
omega
⟶
minus_SNo
x0
∈
SNoS_
omega
Theorem
diadic_rational_p_SNoS_omega
diadic_rational_p_SNoS_omega
:
∀ x0 .
diadic_rational_p
x0
⟶
x0
∈
SNoS_
omega
(proof)
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
Theorem
418cf..
:
∀ x0 .
diadic_rational_p
x0
⟶
SNo
x0
(proof)
Known
andI
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Known
nat_0
nat_0
:
nat_p
0
Known
eps_0_1
eps_0_1
:
eps_
0
=
1
Known
mul_SNo_oneL
mul_SNo_oneL
:
∀ x0 .
SNo
x0
⟶
mul_SNo
1
x0
=
x0
Theorem
int_diadic_rational_p
int_diadic_rational_p
:
∀ x0 .
x0
∈
int
⟶
diadic_rational_p
x0
(proof)
Theorem
omega_diadic_rational_p
omega_diadic_rational_p
:
∀ x0 .
x0
∈
omega
⟶
diadic_rational_p
x0
(proof)
Known
mul_SNo_oneR
mul_SNo_oneR
:
∀ x0 .
SNo
x0
⟶
mul_SNo
x0
1
=
x0
Theorem
eps_diadic_rational_p
eps_diadic_rational_p
:
∀ x0 .
x0
∈
omega
⟶
diadic_rational_p
(
eps_
x0
)
(proof)
Theorem
minus_SNo_diadic_rational_p
minus_SNo_diadic_rational_p
:
∀ x0 .
diadic_rational_p
x0
⟶
diadic_rational_p
(
minus_SNo
x0
)
(proof)
Theorem
mul_SNo_diadic_rational_p
mul_SNo_diadic_rational_p
:
∀ x0 x1 .
diadic_rational_p
x0
⟶
diadic_rational_p
x1
⟶
diadic_rational_p
(
mul_SNo
x0
x1
)
(proof)
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
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
nat_2
nat_2
:
nat_p
2
Theorem
add_SNo_diadic_rational_p
add_SNo_diadic_rational_p
:
∀ x0 x1 .
diadic_rational_p
x0
⟶
diadic_rational_p
x1
⟶
diadic_rational_p
(
add_SNo
x0
x1
)
(proof)
Param
SNoLe
SNoLe
:
ι
→
ι
→
ο
Definition
SNo_max_of
SNo_max_of
:=
λ x0 x1 .
and
(
and
(
x1
∈
x0
)
(
SNo
x1
)
)
(
∀ x2 .
x2
∈
x0
⟶
SNo
x2
⟶
SNoLe
x2
x1
)
Definition
SNo_min_of
SNo_min_of
:=
λ x0 x1 .
and
(
and
(
x1
∈
x0
)
(
SNo
x1
)
)
(
∀ x2 .
x2
∈
x0
⟶
SNo
x2
⟶
SNoLe
x1
x2
)
Param
SNoL
SNoL
:
ι
→
ι
Known
SNoS_omega_SNoL_max_exists
SNoS_omega_SNoL_max_exists
:
∀ x0 .
x0
∈
SNoS_
omega
⟶
or
(
SNoL
x0
=
0
)
(
∀ x1 : ο .
(
∀ x2 .
SNo_max_of
(
SNoL
x0
)
x2
⟶
x1
)
⟶
x1
)
Param
SNoR
SNoR
:
ι
→
ι
Known
SNoS_omega_SNoR_min_exists
SNoS_omega_SNoR_min_exists
:
∀ x0 .
x0
∈
SNoS_
omega
⟶
or
(
SNoR
x0
=
0
)
(
∀ x1 : ο .
(
∀ x2 .
SNo_min_of
(
SNoR
x0
)
x2
⟶
x1
)
⟶
x1
)
Param
SNoLt
SNoLt
:
ι
→
ι
→
ο
Known
double_SNo_min_1
double_SNo_min_1
:
∀ x0 x1 .
SNo
x0
⟶
SNo_min_of
(
SNoR
x0
)
x1
⟶
∀ x2 .
SNo
x2
⟶
SNoLt
x2
x0
⟶
SNoLt
(
add_SNo
x0
x0
)
(
add_SNo
x1
x2
)
⟶
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
SNoL
x2
)
(
add_SNo
x1
x4
=
add_SNo
x0
x0
)
⟶
x3
)
⟶
x3
Known
double_SNo_max_1
double_SNo_max_1
:
∀ x0 x1 .
SNo
x0
⟶
SNo_max_of
(
SNoL
x0
)
x1
⟶
∀ x2 .
SNo
x2
⟶
SNoLt
x0
x2
⟶
SNoLt
(
add_SNo
x1
x2
)
(
add_SNo
x0
x0
)
⟶
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
SNoR
x2
)
(
add_SNo
x1
x4
=
add_SNo
x0
x0
)
⟶
x3
)
⟶
x3
Known
double_eps_1
double_eps_1
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
add_SNo
x0
x0
=
add_SNo
x1
x2
⟶
x0
=
mul_SNo
(
eps_
1
)
(
add_SNo
x1
x2
)
Known
nat_complete_ind
nat_complete_ind
:
∀ x0 :
ι → ο
.
(
∀ x1 .
nat_p
x1
⟶
(
∀ x2 .
x2
∈
x1
⟶
x0
x2
)
⟶
x0
x1
)
⟶
∀ x1 .
nat_p
x1
⟶
x0
x1
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Known
dneg
dneg
:
∀ x0 : ο .
not
(
not
x0
)
⟶
x0
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Known
minus_SNo_Lev
minus_SNo_Lev
:
∀ x0 .
SNo
x0
⟶
SNoLev
(
minus_SNo
x0
)
=
SNoLev
x0
Known
ordinal_SNoLev
ordinal_SNoLev
:
∀ x0 .
ordinal
x0
⟶
SNoLev
x0
=
x0
Known
SNo_max_ordinal
SNo_max_ordinal
:
∀ x0 .
SNo
x0
⟶
(
∀ x1 .
x1
∈
SNoS_
(
SNoLev
x0
)
⟶
SNoLt
x1
x0
)
⟶
ordinal
x0
Known
SNoLev_ordinal
SNoLev_ordinal
:
∀ x0 .
SNo
x0
⟶
ordinal
(
SNoLev
x0
)
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
Definition
nIn
nIn
:=
λ x0 x1 .
not
(
x0
∈
x1
)
Known
In_irref
In_irref
:
∀ x0 .
nIn
x0
x0
Known
EmptyE
EmptyE
:
∀ x0 .
nIn
x0
0
Known
SNoL_I
SNoL_I
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
SNo
x1
⟶
SNoLev
x1
∈
SNoLev
x0
⟶
SNoLt
x1
x0
⟶
x1
∈
SNoL
x0
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
SNoL_E
SNoL_E
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
x1
∈
SNoL
x0
⟶
∀ x2 : ο .
(
SNo
x1
⟶
SNoLev
x1
∈
SNoLev
x0
⟶
SNoLt
x1
x0
⟶
x2
)
⟶
x2
Known
SNoR_I
SNoR_I
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
SNo
x1
⟶
SNoLev
x1
∈
SNoLev
x0
⟶
SNoLt
x0
x1
⟶
x1
∈
SNoR
x0
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
SNo_add_SNo
SNo_add_SNo
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNo
(
add_SNo
x0
x1
)
Definition
TransSet
TransSet
:=
λ x0 .
∀ x1 .
x1
∈
x0
⟶
x1
⊆
x0
Known
ordinal_TransSet
ordinal_TransSet
:
∀ x0 .
ordinal
x0
⟶
TransSet
x0
Known
SNoS_I
SNoS_I
:
∀ x0 .
ordinal
x0
⟶
∀ x1 x2 .
x2
∈
x0
⟶
SNo_
x2
x1
⟶
x1
∈
SNoS_
x0
Known
SNoLev_
SNoLev_
:
∀ x0 .
SNo
x0
⟶
SNo_
(
SNoLev
x0
)
x0
Theorem
SNoS_omega_diadic_rational_p_lem
SNoS_omega_diadic_rational_p_lem
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
SNo
x1
⟶
SNoLev
x1
=
x0
⟶
diadic_rational_p
x1
(proof)
Theorem
SNoS_omega_diadic_rational_p
SNoS_omega_diadic_rational_p
:
∀ x0 .
x0
∈
SNoS_
omega
⟶
diadic_rational_p
x0
(proof)