Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrRL5..
/
9fd18..
PUUiC..
/
d3124..
vout
PrRL5..
/
89357..
6.96 bars
TMLkw..
/
d2d44..
ownership of
edc75..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMEsC..
/
276d8..
ownership of
63c3e..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMbw3..
/
d29c4..
ownership of
88e0a..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMMax..
/
5fce5..
ownership of
9e623..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMKKy..
/
5e81d..
ownership of
f80eb..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMT5x..
/
a6e4a..
ownership of
53a99..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMLAs..
/
7acd6..
ownership of
75cbc..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMdT3..
/
876b0..
ownership of
be3c0..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMXkS..
/
7ac8c..
ownership of
7223d..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMFpz..
/
a72f5..
ownership of
bb0dd..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMZVZ..
/
dd1e6..
ownership of
182e5..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMaKi..
/
71e92..
ownership of
d46ed..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMKUi..
/
22ac2..
ownership of
d5791..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMN4V..
/
14276..
ownership of
b0f58..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMR5s..
/
e8c37..
ownership of
db93f..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMU82..
/
7506c..
ownership of
2d39c..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMQeZ..
/
73ff7..
ownership of
b7810..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMPWj..
/
1003b..
ownership of
0bec9..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMJxC..
/
17601..
ownership of
c09ca..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMRWG..
/
a4f9e..
ownership of
4b16a..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMMZ1..
/
94cfc..
ownership of
e3fc2..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMYud..
/
92e82..
ownership of
74d4e..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMWv2..
/
4c3ff..
ownership of
67aa5..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMVhx..
/
65aae..
ownership of
ab6dc..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMZXH..
/
aa63d..
ownership of
e3473..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMWHY..
/
740ca..
ownership of
f3694..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMJSV..
/
010e1..
ownership of
ebab7..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMX3p..
/
0460e..
ownership of
2e3e0..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMXPY..
/
3dc5d..
ownership of
e7b02..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMVsr..
/
4a2e0..
ownership of
b2de4..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMQQU..
/
21830..
ownership of
c6f6d..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMZp1..
/
45649..
ownership of
38996..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMR6o..
/
a2d6e..
ownership of
7c330..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMLKs..
/
49dec..
ownership of
af615..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMM8o..
/
aa3fd..
ownership of
55b10..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMSsj..
/
7108d..
ownership of
35af7..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMUbG..
/
d40bd..
ownership of
a9fc4..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMYSg..
/
d831e..
ownership of
1a110..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMZtm..
/
ae8d9..
ownership of
a033a..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMKzb..
/
da90c..
ownership of
7eb20..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMYBi..
/
3e63b..
ownership of
9c174..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMQA4..
/
a4b95..
ownership of
ea0c3..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMUCP..
/
825f2..
ownership of
3cd34..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMWJ5..
/
77752..
ownership of
fb23e..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMTXz..
/
12cb3..
ownership of
b572b..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMTV5..
/
f074e..
ownership of
41730..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMPAa..
/
268a8..
ownership of
22668..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMVNU..
/
27191..
ownership of
b6e63..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMPnN..
/
2d1ef..
ownership of
1a06f..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMKBz..
/
7e1be..
ownership of
42315..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMRN9..
/
eb5d0..
ownership of
b197c..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMbZW..
/
c4703..
ownership of
76115..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMMPZ..
/
6385d..
ownership of
5b48d..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMU1P..
/
7193d..
ownership of
8f006..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMHSp..
/
c4d38..
ownership of
90612..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMUBg..
/
623f9..
ownership of
54e1f..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMU8p..
/
56ca6..
ownership of
fcd53..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMaFB..
/
c62aa..
ownership of
c597e..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMLBT..
/
9adc0..
ownership of
db40a..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMbE2..
/
ae996..
ownership of
7c84e..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMMkf..
/
b99c5..
ownership of
bb0b5..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMTFa..
/
4850f..
ownership of
ca7be..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMJ2L..
/
568e3..
ownership of
6d8af..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMaKq..
/
048a4..
ownership of
3b469..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMa5b..
/
705fa..
ownership of
d45b7..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMYCN..
/
9f703..
ownership of
68d62..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMQ3F..
/
7a8f2..
ownership of
31cc9..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMLxM..
/
d717b..
ownership of
f4183..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMYgM..
/
63c36..
ownership of
2c7fa..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMYx5..
/
e7ba6..
ownership of
a1e40..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMUzV..
/
da5d1..
ownership of
5bc23..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMSrr..
/
4a2f3..
ownership of
8dc4c..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMHbb..
/
f7428..
ownership of
b1b15..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMN9B..
/
6a945..
ownership of
5f0b7..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMF4Z..
/
86ac6..
ownership of
20211..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMUwP..
/
bad70..
ownership of
71d15..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMS1S..
/
27f8b..
ownership of
2ebc8..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMcdA..
/
b1556..
ownership of
e233d..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMHDv..
/
8eaff..
ownership of
3fc62..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMYnp..
/
ff1e2..
ownership of
211c6..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMGLo..
/
a14e9..
ownership of
1ec1d..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMRA5..
/
e0f57..
ownership of
426e3..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMcTq..
/
ec5b5..
ownership of
8b12f..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMHoW..
/
440d7..
ownership of
a77cc..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMLXx..
/
6a366..
ownership of
0d39b..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMdJF..
/
ee013..
ownership of
aa96a..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMVss..
/
7c22b..
ownership of
2f4ee..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMNiA..
/
8a796..
ownership of
88641..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMMVt..
/
a9f8c..
ownership of
6fc28..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMSPx..
/
8c9a6..
ownership of
8cdbe..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMRv6..
/
9f92b..
ownership of
d4094..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMa2B..
/
75e82..
ownership of
f6355..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMRRM..
/
d1f34..
ownership of
65d5a..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMSe4..
/
775ba..
ownership of
399f0..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
PUewm..
/
603c5..
doc published by
PrQUS..
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
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
famunionI
famunionI
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 x3 .
x2
∈
x0
⟶
x3
∈
x1
x2
⟶
x3
∈
famunion
x0
x1
Theorem
famunion_Subq
famunion_Subq
:
∀ x0 .
∀ x1 x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
x1
x3
⊆
x2
x3
)
⟶
famunion
x0
x1
⊆
famunion
x0
x2
(proof)
Known
set_ext
set_ext
:
∀ x0 x1 .
x0
⊆
x1
⟶
x1
⊆
x0
⟶
x0
=
x1
Known
Subq_ref
Subq_ref
:
∀ x0 .
x0
⊆
x0
Theorem
famunion_ext
famunion_ext
:
∀ x0 .
∀ x1 x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
x1
x3
=
x2
x3
)
⟶
famunion
x0
x1
=
famunion
x0
x2
(proof)
Param
nat_p
nat_p
:
ι
→
ο
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Param
add_nat
add_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
andI
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Known
add_nat_0R
add_nat_0R
:
∀ x0 .
add_nat
x0
0
=
x0
Known
nat_inv_impred
nat_inv_impred
:
∀ x0 :
ι → ο
.
x0
0
⟶
(
∀ x1 .
nat_p
x1
⟶
x0
(
ordsucc
x1
)
)
⟶
∀ x1 .
nat_p
x1
⟶
x0
x1
Definition
False
False
:=
∀ x0 : ο .
x0
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Definition
nIn
nIn
:=
λ x0 x1 .
not
(
x0
∈
x1
)
Known
EmptyE
EmptyE
:
∀ x0 .
nIn
x0
0
Known
ordsuccI2
ordsuccI2
:
∀ x0 .
x0
∈
ordsucc
x0
Param
ordinal
ordinal
:
ι
→
ο
Definition
or
or
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x2
)
⟶
(
x1
⟶
x2
)
⟶
x2
Known
ordinal_In_Or_Subq
ordinal_In_Or_Subq
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
or
(
x0
∈
x1
)
(
x1
⊆
x0
)
Known
nat_p_ordinal
nat_p_ordinal
:
∀ x0 .
nat_p
x0
⟶
ordinal
x0
Known
In_irref
In_irref
:
∀ x0 .
nIn
x0
x0
Known
nat_ordsucc_in_ordsucc
nat_ordsucc_in_ordsucc
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
x1
∈
x0
⟶
ordsucc
x1
∈
ordsucc
x0
Known
add_nat_SR
add_nat_SR
:
∀ x0 x1 .
nat_p
x1
⟶
add_nat
x0
(
ordsucc
x1
)
=
ordsucc
(
add_nat
x0
x1
)
Theorem
nat_Subq_add_ex
nat_Subq_add_ex
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
x0
⊆
x1
⟶
∀ x2 : ο .
(
∀ x3 .
and
(
nat_p
x3
)
(
x1
=
add_nat
x3
x0
)
⟶
x2
)
⟶
x2
(proof)
Param
SNo
SNo
:
ι
→
ο
Param
SNoLe
SNoLe
:
ι
→
ι
→
ο
Param
SNoLt
SNoLt
:
ι
→
ι
→
ο
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
orIL
orIL
:
∀ x0 x1 : ο .
x0
⟶
or
x0
x1
Known
orIR
orIR
:
∀ x0 x1 : ο .
x1
⟶
or
x0
x1
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
SNoLeE
SNoLeE
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLe
x0
x1
⟶
or
(
SNoLt
x0
x1
)
(
x0
=
x1
)
(proof)
Param
mul_SNo
mul_SNo
:
ι
→
ι
→
ι
Known
SNo_0
SNo_0
:
SNo
0
Known
SNoLtLe
SNoLtLe
:
∀ x0 x1 .
SNoLt
x0
x1
⟶
SNoLe
x0
x1
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
)
Known
mul_SNo_zeroR
mul_SNo_zeroR
:
∀ x0 .
SNo
x0
⟶
mul_SNo
x0
0
=
0
Known
SNoLe_ref
SNoLe_ref
:
∀ x0 .
SNoLe
x0
x0
Known
mul_SNo_zeroL
mul_SNo_zeroL
:
∀ x0 .
SNo
x0
⟶
mul_SNo
0
x0
=
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)
Known
pos_mul_SNo_Lt2
pos_mul_SNo_Lt2
:
∀ x0 x1 x2 x3 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNo
x3
⟶
SNoLt
0
x0
⟶
SNoLt
0
x1
⟶
SNoLt
x0
x2
⟶
SNoLt
x1
x3
⟶
SNoLt
(
mul_SNo
x0
x1
)
(
mul_SNo
x2
x3
)
Theorem
SNo_pos_sqr_uniq
SNo_pos_sqr_uniq
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLt
0
x0
⟶
SNoLt
0
x1
⟶
mul_SNo
x0
x0
=
mul_SNo
x1
x1
⟶
x0
=
x1
(proof)
Known
SNo_zero_or_sqr_pos
SNo_zero_or_sqr_pos
:
∀ x0 .
SNo
x0
⟶
or
(
x0
=
0
)
(
SNoLt
0
(
mul_SNo
x0
x0
)
)
Theorem
SNo_nonneg_sqr_uniq
SNo_nonneg_sqr_uniq
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLe
0
x0
⟶
SNoLe
0
x1
⟶
mul_SNo
x0
x0
=
mul_SNo
x1
x1
⟶
x0
=
x1
(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
SNoL
SNoL
:
ι
→
ι
Param
SNoCut
SNoCut
:
ι
→
ι
→
ι
Known
dneg
dneg
:
∀ x0 : ο .
not
(
not
x0
)
⟶
x0
Param
SNoLev
SNoLev
:
ι
→
ι
Param
binunion
binunion
:
ι
→
ι
→
ι
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
SNoCutP_SNoCut_impred
SNoCutP_SNoCut_impred
:
∀ x0 x1 .
SNoCutP
x0
x1
⟶
∀ x2 : ο .
(
SNo
(
SNoCut
x0
x1
)
⟶
SNoLev
(
SNoCut
x0
x1
)
∈
ordsucc
(
binunion
(
famunion
x0
(
λ x3 .
ordsucc
(
SNoLev
x3
)
)
)
(
famunion
x1
(
λ x3 .
ordsucc
(
SNoLev
x3
)
)
)
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
SNoLt
x3
(
SNoCut
x0
x1
)
)
⟶
(
∀ x3 .
x3
∈
x1
⟶
SNoLt
(
SNoCut
x0
x1
)
x3
)
⟶
(
∀ x3 .
SNo
x3
⟶
(
∀ x4 .
x4
∈
x0
⟶
SNoLt
x4
x3
)
⟶
(
∀ x4 .
x4
∈
x1
⟶
SNoLt
x3
x4
)
⟶
and
(
SNoLev
(
SNoCut
x0
x1
)
⊆
SNoLev
x3
)
(
SNoEq_
(
SNoLev
(
SNoCut
x0
x1
)
)
(
SNoCut
x0
x1
)
x3
)
)
⟶
x2
)
⟶
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
andEL
andEL
:
∀ x0 x1 : ο .
and
x0
x1
⟶
x0
Known
SNoLtLe_or
SNoLtLe_or
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
or
(
SNoLt
x0
x1
)
(
SNoLe
x1
x0
)
Known
SNoLt_tra
SNoLt_tra
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
x0
x1
⟶
SNoLt
x1
x2
⟶
SNoLt
x0
x2
Theorem
SNoL_SNoCutP_ex
SNoL_SNoCutP_ex
:
∀ x0 x1 .
SNoCutP
x0
x1
⟶
∀ x2 .
x2
∈
SNoL
(
SNoCut
x0
x1
)
⟶
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
x0
)
(
SNoLe
x2
x4
)
⟶
x3
)
⟶
x3
(proof)
Param
SNoR
SNoR
:
ι
→
ι
Known
SNoR_E
SNoR_E
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
x1
∈
SNoR
x0
⟶
∀ x2 : ο .
(
SNo
x1
⟶
SNoLev
x1
∈
SNoLev
x0
⟶
SNoLt
x0
x1
⟶
x2
)
⟶
x2
Theorem
SNoR_SNoCutP_ex
SNoR_SNoCutP_ex
:
∀ x0 x1 .
SNoCutP
x0
x1
⟶
∀ x2 .
x2
∈
SNoR
(
SNoCut
x0
x1
)
⟶
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
x1
)
(
SNoLe
x4
x2
)
⟶
x3
)
⟶
x3
(proof)
Param
binintersect
binintersect
:
ι
→
ι
→
ι
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
ordinal_SNoLev
ordinal_SNoLev
:
∀ x0 .
ordinal
x0
⟶
SNoLev
x0
=
x0
Known
ordinal_Empty
ordinal_Empty
:
ordinal
0
Known
binintersectE1
binintersectE1
:
∀ x0 x1 x2 .
x2
∈
binintersect
x0
x1
⟶
x2
∈
x0
Known
SNo_eq
SNo_eq
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLev
x0
=
SNoLev
x1
⟶
SNoEq_
(
SNoLev
x0
)
x0
x1
⟶
x0
=
x1
Known
SNo_1
SNo_1
:
SNo
1
Known
nat_1
nat_1
:
nat_p
1
Known
cases_1
cases_1
:
∀ x0 .
x0
∈
1
⟶
∀ x1 :
ι → ο
.
x1
0
⟶
x1
x0
Known
iffI
iffI
:
∀ x0 x1 : ο .
(
x0
⟶
x1
)
⟶
(
x1
⟶
x0
)
⟶
iff
x0
x1
Known
In_0_1
In_0_1
:
0
∈
1
Theorem
pos_low_eq_one
pos_low_eq_one
:
∀ x0 .
SNo
x0
⟶
SNoLt
0
x0
⟶
SNoLev
x0
⊆
1
⟶
x0
=
1
(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
Known
SNoLe_antisym
SNoLe_antisym
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLe
x0
x1
⟶
SNoLe
x1
x0
⟶
x0
=
x1
Theorem
mul_SNo_nonpos_pos
mul_SNo_nonpos_pos
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLe
x0
0
⟶
SNoLt
0
x1
⟶
SNoLe
(
mul_SNo
x0
x1
)
0
(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
mul_SNo_nonpos_neg
mul_SNo_nonpos_neg
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLe
x0
0
⟶
SNoLt
x1
0
⟶
SNoLe
0
(
mul_SNo
x0
x1
)
(proof)
Known
neg_mul_SNo_Lt
neg_mul_SNo_Lt
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNoLt
x0
0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
x2
x1
⟶
SNoLt
(
mul_SNo
x0
x1
)
(
mul_SNo
x0
x2
)
Theorem
nonpos_mul_SNo_Le
nonpos_mul_SNo_Le
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNoLe
x0
0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLe
x2
x1
⟶
SNoLe
(
mul_SNo
x0
x1
)
(
mul_SNo
x0
x2
)
(proof)
Param
Sep
Sep
:
ι
→
(
ι
→
ο
) →
ι
Definition
SNoL_pos
SNoL_pos
:=
λ x0 .
Sep
(
SNoL
x0
)
(
SNoLt
0
)
Known
neq_0_1
neq_0_1
:
0
=
1
⟶
∀ x0 : ο .
x0
Known
SNoLt_0_1
SNoLt_0_1
:
SNoLt
0
1
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
Theorem
SNo_recip_pos_pos
SNo_recip_pos_pos
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLt
0
x0
⟶
mul_SNo
x0
x1
=
1
⟶
SNoLt
0
x1
(proof)
Param
add_SNo
add_SNo
:
ι
→
ι
→
ι
Param
minus_SNo
minus_SNo
:
ι
→
ι
Known
SepE
SepE
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
Sep
x0
x1
⟶
and
(
x2
∈
x0
)
(
x1
x2
)
Known
add_SNo_0L
add_SNo_0L
:
∀ x0 .
SNo
x0
⟶
add_SNo
0
x0
=
x0
Known
SNo_mul_SNo
SNo_mul_SNo
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNo
(
mul_SNo
x0
x1
)
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
SNo_add_SNo
SNo_add_SNo
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNo
(
add_SNo
x0
x1
)
Known
SNo_minus_SNo
SNo_minus_SNo
:
∀ x0 .
SNo
x0
⟶
SNo
(
minus_SNo
x0
)
Known
add_SNo_minus_Lt2b
add_SNo_minus_Lt2b
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
(
add_SNo
x2
x1
)
x0
⟶
SNoLt
x2
(
add_SNo
x0
(
minus_SNo
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
SNo_recip_lem1
SNo_recip_lem1
:
∀ x0 x1 x2 x3 x4 .
SNo
x0
⟶
SNoLt
0
x0
⟶
x1
∈
SNoL_pos
x0
⟶
SNo
x2
⟶
mul_SNo
x1
x2
=
1
⟶
SNo
x3
⟶
SNoLt
(
mul_SNo
x0
x3
)
1
⟶
SNo
x4
⟶
add_SNo
1
(
minus_SNo
(
mul_SNo
x0
x4
)
)
=
mul_SNo
(
add_SNo
1
(
minus_SNo
(
mul_SNo
x0
x3
)
)
)
(
mul_SNo
(
add_SNo
x1
(
minus_SNo
x0
)
)
x2
)
⟶
SNoLt
1
(
mul_SNo
x0
x4
)
(proof)
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
Theorem
SNo_recip_lem2
SNo_recip_lem2
:
∀ x0 x1 x2 x3 x4 .
SNo
x0
⟶
SNoLt
0
x0
⟶
x1
∈
SNoL_pos
x0
⟶
SNo
x2
⟶
mul_SNo
x1
x2
=
1
⟶
SNo
x3
⟶
SNoLt
1
(
mul_SNo
x0
x3
)
⟶
SNo
x4
⟶
add_SNo
1
(
minus_SNo
(
mul_SNo
x0
x4
)
)
=
mul_SNo
(
add_SNo
1
(
minus_SNo
(
mul_SNo
x0
x3
)
)
)
(
mul_SNo
(
add_SNo
x1
(
minus_SNo
x0
)
)
x2
)
⟶
SNoLt
(
mul_SNo
x0
x4
)
1
(proof)
Theorem
SNo_recip_lem3
SNo_recip_lem3
:
∀ x0 x1 x2 x3 x4 .
SNo
x0
⟶
SNoLt
0
x0
⟶
x1
∈
SNoR
x0
⟶
SNo
x2
⟶
mul_SNo
x1
x2
=
1
⟶
SNo
x3
⟶
SNoLt
(
mul_SNo
x0
x3
)
1
⟶
SNo
x4
⟶
add_SNo
1
(
minus_SNo
(
mul_SNo
x0
x4
)
)
=
mul_SNo
(
add_SNo
1
(
minus_SNo
(
mul_SNo
x0
x3
)
)
)
(
mul_SNo
(
add_SNo
x1
(
minus_SNo
x0
)
)
x2
)
⟶
SNoLt
(
mul_SNo
x0
x4
)
1
(proof)
Theorem
SNo_recip_lem4
SNo_recip_lem4
:
∀ x0 x1 x2 x3 x4 .
SNo
x0
⟶
SNoLt
0
x0
⟶
x1
∈
SNoR
x0
⟶
SNo
x2
⟶
mul_SNo
x1
x2
=
1
⟶
SNo
x3
⟶
SNoLt
1
(
mul_SNo
x0
x3
)
⟶
SNo
x4
⟶
add_SNo
1
(
minus_SNo
(
mul_SNo
x0
x4
)
)
=
mul_SNo
(
add_SNo
1
(
minus_SNo
(
mul_SNo
x0
x3
)
)
)
(
mul_SNo
(
add_SNo
x1
(
minus_SNo
x0
)
)
x2
)
⟶
SNoLt
1
(
mul_SNo
x0
x4
)
(proof)
Definition
SNo_recipauxset
SNo_recipauxset
:=
λ x0 x1 x2 .
λ x3 :
ι → ι
.
famunion
x0
(
λ x4 .
{
mul_SNo
(
add_SNo
1
(
mul_SNo
(
add_SNo
x5
(
minus_SNo
x1
)
)
x4
)
)
(
x3
x5
)
|x5 ∈
x2
}
)
Known
ReplI
ReplI
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
x0
⟶
x1
x2
∈
prim5
x0
x1
Theorem
SNo_recipauxset_I
SNo_recipauxset_I
:
∀ x0 x1 x2 .
∀ x3 :
ι → ι
.
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x2
⟶
mul_SNo
(
add_SNo
1
(
mul_SNo
(
add_SNo
x5
(
minus_SNo
x1
)
)
x4
)
)
(
x3
x5
)
∈
SNo_recipauxset
x0
x1
x2
x3
(proof)
Known
ReplE_impred
ReplE_impred
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
prim5
x0
x1
⟶
∀ x3 : ο .
(
∀ x4 .
x4
∈
x0
⟶
x2
=
x1
x4
⟶
x3
)
⟶
x3
Theorem
SNo_recipauxset_E
SNo_recipauxset_E
:
∀ x0 x1 x2 .
∀ x3 :
ι → ι
.
∀ x4 .
x4
∈
SNo_recipauxset
x0
x1
x2
x3
⟶
∀ x5 : ο .
(
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x2
⟶
x4
=
mul_SNo
(
add_SNo
1
(
mul_SNo
(
add_SNo
x7
(
minus_SNo
x1
)
)
x6
)
)
(
x3
x7
)
⟶
x5
)
⟶
x5
(proof)
Known
ReplEq_ext
ReplEq_ext
:
∀ x0 .
∀ x1 x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
x1
x3
=
x2
x3
)
⟶
prim5
x0
x1
=
prim5
x0
x2
Theorem
SNo_recipauxset_ext
SNo_recipauxset_ext
:
∀ x0 x1 x2 .
∀ x3 x4 :
ι → ι
.
(
∀ x5 .
x5
∈
x2
⟶
x3
x5
=
x4
x5
)
⟶
SNo_recipauxset
x0
x1
x2
x3
=
SNo_recipauxset
x0
x1
x2
x4
(proof)
Param
nat_primrec
nat_primrec
:
ι
→
(
ι
→
ι
→
ι
) →
ι
→
ι
Param
lam
Sigma
:
ι
→
(
ι
→
ι
) →
ι
Param
If_i
If_i
:
ο
→
ι
→
ι
→
ι
Param
Sing
Sing
:
ι
→
ι
Param
ap
ap
:
ι
→
ι
→
ι
Definition
SNo_recipaux
SNo_recipaux
:=
λ x0 .
λ x1 :
ι → ι
.
nat_primrec
(
lam
2
(
λ x2 .
If_i
(
x2
=
0
)
(
Sing
0
)
0
)
)
(
λ x2 x3 .
lam
2
(
λ x4 .
If_i
(
x4
=
0
)
(
binunion
(
binunion
(
ap
x3
0
)
(
SNo_recipauxset
(
ap
x3
0
)
x0
(
SNoR
x0
)
x1
)
)
(
SNo_recipauxset
(
ap
x3
1
)
x0
(
SNoL_pos
x0
)
x1
)
)
(
binunion
(
binunion
(
ap
x3
1
)
(
SNo_recipauxset
(
ap
x3
0
)
x0
(
SNoL_pos
x0
)
x1
)
)
(
SNo_recipauxset
(
ap
x3
1
)
x0
(
SNoR
x0
)
x1
)
)
)
)
Known
nat_primrec_0
nat_primrec_0
:
∀ x0 .
∀ x1 :
ι →
ι → ι
.
nat_primrec
x0
x1
0
=
x0
Theorem
SNo_recipaux_0
SNo_recipaux_0
:
∀ x0 .
∀ x1 :
ι → ι
.
SNo_recipaux
x0
x1
0
=
lam
2
(
λ x3 .
If_i
(
x3
=
0
)
(
Sing
0
)
0
)
(proof)
Known
nat_primrec_S
nat_primrec_S
:
∀ x0 .
∀ x1 :
ι →
ι → ι
.
∀ x2 .
nat_p
x2
⟶
nat_primrec
x0
x1
(
ordsucc
x2
)
=
x1
x2
(
nat_primrec
x0
x1
x2
)
Theorem
SNo_recipaux_S
SNo_recipaux_S
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
nat_p
x2
⟶
SNo_recipaux
x0
x1
(
ordsucc
x2
)
=
lam
2
(
λ x4 .
If_i
(
x4
=
0
)
(
binunion
(
binunion
(
ap
(
SNo_recipaux
x0
x1
x2
)
0
)
(
SNo_recipauxset
(
ap
(
SNo_recipaux
x0
x1
x2
)
0
)
x0
(
SNoR
x0
)
x1
)
)
(
SNo_recipauxset
(
ap
(
SNo_recipaux
x0
x1
x2
)
1
)
x0
(
SNoL_pos
x0
)
x1
)
)
(
binunion
(
binunion
(
ap
(
SNo_recipaux
x0
x1
x2
)
1
)
(
SNo_recipauxset
(
ap
(
SNo_recipaux
x0
x1
x2
)
0
)
x0
(
SNoL_pos
x0
)
x1
)
)
(
SNo_recipauxset
(
ap
(
SNo_recipaux
x0
x1
x2
)
1
)
x0
(
SNoR
x0
)
x1
)
)
)
(proof)
Param
SNoS_
SNoS_
:
ι
→
ι
Known
tuple_2_0_eq
tuple_2_0_eq
:
∀ x0 x1 .
ap
(
lam
2
(
λ x3 .
If_i
(
x3
=
0
)
x0
x1
)
)
0
=
x0
Known
SingE
SingE
:
∀ x0 x1 .
x1
∈
Sing
x0
⟶
x1
=
x0
Known
tuple_2_1_eq
tuple_2_1_eq
:
∀ x0 x1 .
ap
(
lam
2
(
λ x3 .
If_i
(
x3
=
0
)
x0
x1
)
)
1
=
x1
Known
binunionE
binunionE
:
∀ x0 x1 x2 .
x2
∈
binunion
x0
x1
⟶
or
(
x2
∈
x0
)
(
x2
∈
x1
)
Known
SNoS_I2
SNoS_I2
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLev
x0
∈
SNoLev
x1
⟶
x0
∈
SNoS_
(
SNoLev
x1
)
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
SNoLev_ordinal
SNoLev_ordinal
:
∀ x0 .
SNo
x0
⟶
ordinal
(
SNoLev
x0
)
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
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
mul_SNo_oneL
mul_SNo_oneL
:
∀ x0 .
SNo
x0
⟶
mul_SNo
1
x0
=
x0
Known
mul_SNo_oneR
mul_SNo_oneR
:
∀ x0 .
SNo
x0
⟶
mul_SNo
x0
1
=
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
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_com
mul_SNo_com
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
mul_SNo
x0
x1
=
mul_SNo
x1
x0
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
SNo_recipaux_lem1
SNo_recipaux_lem1
:
∀ x0 .
SNo
x0
⟶
SNoLt
0
x0
⟶
∀ x1 :
ι → ι
.
(
∀ x2 .
x2
∈
SNoS_
(
SNoLev
x0
)
⟶
SNoLt
0
x2
⟶
and
(
SNo
(
x1
x2
)
)
(
mul_SNo
x2
(
x1
x2
)
=
1
)
)
⟶
∀ x2 .
nat_p
x2
⟶
and
(
∀ x3 .
x3
∈
ap
(
SNo_recipaux
x0
x1
x2
)
0
⟶
and
(
SNo
x3
)
(
SNoLt
(
mul_SNo
x0
x3
)
1
)
)
(
∀ x3 .
x3
∈
ap
(
SNo_recipaux
x0
x1
x2
)
1
⟶
and
(
SNo
x3
)
(
SNoLt
1
(
mul_SNo
x0
x3
)
)
)
(proof)
Param
omega
omega
:
ι
Known
and3I
and3I
:
∀ x0 x1 x2 : ο .
x0
⟶
x1
⟶
x2
⟶
and
(
and
x0
x1
)
x2
Known
omega_nat_p
omega_nat_p
:
∀ x0 .
x0
∈
omega
⟶
nat_p
x0
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
)
Theorem
SNo_recipaux_lem2
SNo_recipaux_lem2
:
∀ x0 .
SNo
x0
⟶
SNoLt
0
x0
⟶
∀ x1 :
ι → ι
.
(
∀ x2 .
x2
∈
SNoS_
(
SNoLev
x0
)
⟶
SNoLt
0
x2
⟶
and
(
SNo
(
x1
x2
)
)
(
mul_SNo
x2
(
x1
x2
)
=
1
)
)
⟶
SNoCutP
(
famunion
omega
(
λ x2 .
ap
(
SNo_recipaux
x0
x1
x2
)
0
)
)
(
famunion
omega
(
λ x2 .
ap
(
SNo_recipaux
x0
x1
x2
)
1
)
)
(proof)
Known
SepE1
SepE1
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
Sep
x0
x1
⟶
x2
∈
x0
Theorem
SNo_recipaux_ext
SNo_recipaux_ext
:
∀ x0 .
SNo
x0
⟶
∀ x1 x2 :
ι → ι
.
(
∀ x3 .
x3
∈
SNoS_
(
SNoLev
x0
)
⟶
x1
x3
=
x2
x3
)
⟶
∀ x3 .
nat_p
x3
⟶
SNo_recipaux
x0
x1
x3
=
SNo_recipaux
x0
x2
x3
(proof)
Param
SNo_rec_i
SNo_rec_i
:
(
ι
→
(
ι
→
ι
) →
ι
) →
ι
→
ι
Definition
recip_SNo_pos
recip_SNo_pos
:=
SNo_rec_i
(
λ x0 .
λ x1 :
ι → ι
.
SNoCut
(
famunion
omega
(
λ x2 .
ap
(
SNo_recipaux
x0
x1
x2
)
0
)
)
(
famunion
omega
(
λ x2 .
ap
(
SNo_recipaux
x0
x1
x2
)
1
)
)
)
Known
SNo_rec_i_eq
SNo_rec_i_eq
:
∀ x0 :
ι →
(
ι → ι
)
→ ι
.
(
∀ x1 .
SNo
x1
⟶
∀ x2 x3 :
ι → ι
.
(
∀ x4 .
x4
∈
SNoS_
(
SNoLev
x1
)
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
SNo
x1
⟶
SNo_rec_i
x0
x1
=
x0
x1
(
SNo_rec_i
x0
)
Theorem
recip_SNo_pos_eq
recip_SNo_pos_eq
:
∀ x0 .
SNo
x0
⟶
recip_SNo_pos
x0
=
SNoCut
(
famunion
omega
(
λ x2 .
ap
(
SNo_recipaux
x0
recip_SNo_pos
x2
)
0
)
)
(
famunion
omega
(
λ x2 .
ap
(
SNo_recipaux
x0
recip_SNo_pos
x2
)
1
)
)
(proof)
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
)
Definition
div_SNo
div_SNo
:=
λ x0 x1 .
mul_SNo
x0
(
recip_SNo
x1
)
Definition
SNoL_nonneg
SNoL_nonneg
:=
λ x0 .
Sep
(
SNoL
x0
)
(
SNoLe
0
)
Known
Empty_eq
Empty_eq
:
∀ x0 .
(
∀ x1 .
nIn
x1
x0
)
⟶
x0
=
0
Theorem
Sep_Empty
Sep_Empty
:
∀ x0 :
ι → ο
.
Sep
0
x0
=
0
(proof)
Known
SNoL_0
SNoL_0
:
SNoL
0
=
0
Theorem
SNoL_nonneg_0
SNoL_nonneg_0
:
SNoL_nonneg
0
=
0
(proof)
Known
SNoL_1
SNoL_1
:
SNoL
1
=
1
Known
Sep_Subq
Sep_Subq
:
∀ x0 .
∀ x1 :
ι → ο
.
Sep
x0
x1
⊆
x0
Known
SepI
SepI
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
x0
⟶
x1
x2
⟶
x2
∈
Sep
x0
x1
Theorem
SNoL_nonneg_1
SNoL_nonneg_1
:
SNoL_nonneg
1
=
1
(proof)
Param
ReplSep
ReplSep
:
ι
→
(
ι
→
ο
) →
(
ι
→
ι
) →
ι
Definition
SNo_sqrtauxset
SNo_sqrtauxset
:=
λ x0 x1 x2 .
famunion
x0
(
λ x3 .
{
div_SNo
(
add_SNo
x2
(
mul_SNo
x3
x4
)
)
(
add_SNo
x3
x4
)
|x4 ∈
x1
,
SNoLt
0
(
add_SNo
x3
x4
)
}
)
Known
ReplSepI
ReplSepI
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 :
ι → ι
.
∀ x3 .
x3
∈
x0
⟶
x1
x3
⟶
x2
x3
∈
ReplSep
x0
x1
x2
Theorem
SNo_sqrtauxset_I
SNo_sqrtauxset_I
:
∀ x0 x1 x2 x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x1
⟶
SNoLt
0
(
add_SNo
x3
x4
)
⟶
div_SNo
(
add_SNo
x2
(
mul_SNo
x3
x4
)
)
(
add_SNo
x3
x4
)
∈
SNo_sqrtauxset
x0
x1
x2
(proof)
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
Theorem
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
(proof)
Theorem
SNo_sqrtauxset_0
SNo_sqrtauxset_0
:
∀ x0 x1 .
SNo_sqrtauxset
0
x0
x1
=
0
(proof)
Theorem
SNo_sqrtauxset_0'
SNo_sqrtauxset_0
:
∀ x0 x1 .
SNo_sqrtauxset
x0
0
x1
=
0
(proof)
Definition
SNo_sqrtaux
SNo_sqrtaux
:=
λ x0 .
λ x1 :
ι → ι
.
nat_primrec
(
lam
2
(
λ x2 .
If_i
(
x2
=
0
)
(
prim5
(
SNoL_nonneg
x0
)
x1
)
(
prim5
(
SNoR
x0
)
x1
)
)
)
(
λ x2 x3 .
lam
2
(
λ x4 .
If_i
(
x4
=
0
)
(
binunion
(
ap
x3
0
)
(
SNo_sqrtauxset
(
ap
x3
0
)
(
ap
x3
1
)
x0
)
)
(
binunion
(
binunion
(
ap
x3
1
)
(
SNo_sqrtauxset
(
ap
x3
0
)
(
ap
x3
0
)
x0
)
)
(
SNo_sqrtauxset
(
ap
x3
1
)
(
ap
x3
1
)
x0
)
)
)
)
Theorem
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
)
)
(proof)
Theorem
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
)
)
)
(proof)
Known
add_nat_p
add_nat_p
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
nat_p
(
add_nat
x0
x1
)
Known
Subq_tra
Subq_tra
:
∀ x0 x1 x2 .
x0
⊆
x1
⟶
x1
⊆
x2
⟶
x0
⊆
x2
Known
binunion_Subq_1
binunion_Subq_1
:
∀ x0 x1 .
x0
⊆
binunion
x0
x1
Theorem
SNo_sqrtaux_mon_lem
SNo_sqrtaux_mon_lem
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
nat_p
x2
⟶
∀ x3 .
nat_p
x3
⟶
and
(
ap
(
SNo_sqrtaux
x0
x1
x2
)
0
⊆
ap
(
SNo_sqrtaux
x0
x1
(
add_nat
x2
x3
)
)
0
)
(
ap
(
SNo_sqrtaux
x0
x1
x2
)
1
⊆
ap
(
SNo_sqrtaux
x0
x1
(
add_nat
x2
x3
)
)
1
)
(proof)
Known
add_nat_com
add_nat_com
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
add_nat
x0
x1
=
add_nat
x1
x0
Theorem
SNo_sqrtaux_mon
SNo_sqrtaux_mon
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
nat_p
x2
⟶
∀ x3 .
nat_p
x3
⟶
x2
⊆
x3
⟶
and
(
ap
(
SNo_sqrtaux
x0
x1
x2
)
0
⊆
ap
(
SNo_sqrtaux
x0
x1
x3
)
0
)
(
ap
(
SNo_sqrtaux
x0
x1
x2
)
1
⊆
ap
(
SNo_sqrtaux
x0
x1
x3
)
1
)
(proof)
Theorem
SNo_sqrtaux_ext
SNo_sqrtaux_ext
:
∀ x0 .
SNo
x0
⟶
∀ x1 x2 :
ι → ι
.
(
∀ x3 .
x3
∈
SNoS_
(
SNoLev
x0
)
⟶
x1
x3
=
x2
x3
)
⟶
∀ x3 .
nat_p
x3
⟶
SNo_sqrtaux
x0
x1
x3
=
SNo_sqrtaux
x0
x2
x3
(proof)
Definition
sqrt_SNo_nonneg
sqrt_SNo_nonneg
:=
SNo_rec_i
(
λ x0 .
λ x1 :
ι → ι
.
SNoCut
(
famunion
omega
(
λ x2 .
ap
(
SNo_sqrtaux
x0
x1
x2
)
0
)
)
(
famunion
omega
(
λ x2 .
ap
(
SNo_sqrtaux
x0
x1
x2
)
1
)
)
)
Theorem
sqrt_SNo_nonneg_eq
sqrt_SNo_nonneg_eq
:
∀ x0 .
SNo
x0
⟶
sqrt_SNo_nonneg
x0
=
SNoCut
(
famunion
omega
(
λ x2 .
ap
(
SNo_sqrtaux
x0
sqrt_SNo_nonneg
x2
)
0
)
)
(
famunion
omega
(
λ x2 .
ap
(
SNo_sqrtaux
x0
sqrt_SNo_nonneg
x2
)
1
)
)
(proof)