Search for blocks/addresses/...
Proofgold Signed Transaction
vin
Pr7pr..
/
53b9d..
PUcyY..
/
d0c9c..
vout
Pr7pr..
/
0559e..
19.99 bars
TMGqV..
/
e0bf1..
ownership of
573f9..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMNSF..
/
1abbb..
ownership of
00e25..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMWa9..
/
078a9..
ownership of
2cb7a..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKKR..
/
66aa8..
ownership of
d8d0b..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMPFy..
/
f04eb..
ownership of
994ef..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJX5..
/
6ba9e..
ownership of
07e5d..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMUP4..
/
3f5b6..
ownership of
69f96..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMbZk..
/
c1011..
ownership of
722ac..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQQ2..
/
e48f3..
ownership of
2f624..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMRjX..
/
2885d..
ownership of
ebaf1..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMPDi..
/
c29eb..
ownership of
4d242..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMddu..
/
9f7aa..
ownership of
0d2cd..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMZyT..
/
11522..
ownership of
bff32..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMWGq..
/
48e66..
ownership of
67223..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMd2K..
/
c7d73..
ownership of
409d6..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMVFM..
/
7b1fc..
ownership of
41db9..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMWYH..
/
2c7b7..
ownership of
b0c8e..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMNe8..
/
ce466..
ownership of
6f12d..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMe1L..
/
eb559..
ownership of
a0709..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMUed..
/
dd361..
ownership of
c05f7..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQYo..
/
7ff8a..
ownership of
37f9a..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMYyG..
/
d565c..
ownership of
40978..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMRfr..
/
04529..
ownership of
f47da..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMFut..
/
348f5..
ownership of
a7d90..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMF2c..
/
12d12..
ownership of
7bb1e..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMGiS..
/
8e65e..
ownership of
f1207..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMHoR..
/
48299..
ownership of
2893f..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMWYH..
/
f7b59..
ownership of
a3826..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMM7U..
/
81157..
ownership of
b4a18..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMUBE..
/
ad967..
ownership of
49fbe..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMbKw..
/
dc03a..
ownership of
e8653..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMX1h..
/
959b8..
ownership of
5b92f..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMWKc..
/
0b525..
ownership of
dc235..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMUcK..
/
54fcc..
ownership of
02b4e..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQqG..
/
5c422..
ownership of
5cfac..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMZa9..
/
42e40..
ownership of
bc452..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMRyc..
/
3d4c1..
ownership of
49a8c..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMYAJ..
/
b5394..
ownership of
530c0..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMbk4..
/
d3f4f..
ownership of
09748..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMYBc..
/
0c66e..
ownership of
5c40c..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMFdP..
/
3bfcb..
ownership of
78529..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMFtd..
/
f746f..
ownership of
62b2b..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMG9g..
/
1fd45..
ownership of
d1120..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMP1N..
/
125eb..
ownership of
48bc1..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJAF..
/
b98a3..
ownership of
36418..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMc5k..
/
c7df0..
ownership of
342a1..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMaBE..
/
9a3b5..
ownership of
763c8..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMLLp..
/
1b0a7..
ownership of
2213e..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMK1B..
/
0d7ad..
ownership of
44dca..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMLfZ..
/
3535a..
ownership of
16042..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMdRU..
/
49af6..
ownership of
e705d..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQyq..
/
ec284..
ownership of
ad03b..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMZrs..
/
28bf5..
ownership of
9e40e..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMNR9..
/
737e2..
ownership of
d1536..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKrU..
/
df79b..
ownership of
80b3b..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJje..
/
e5821..
ownership of
ed9d6..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMF6o..
/
638b6..
ownership of
a78d0..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMNbs..
/
ba26d..
ownership of
258d1..
as prop with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMMQW..
/
da8ed..
ownership of
b67f4..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMGNS..
/
dfec4..
ownership of
2b1c2..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMRg5..
/
cc520..
ownership of
b1f6e..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJsK..
/
8edb0..
ownership of
f6068..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMLjG..
/
b4689..
ownership of
ebf7a..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMSTW..
/
81077..
ownership of
6b023..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMNNG..
/
17d54..
ownership of
65107..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQYf..
/
fb304..
ownership of
7a2f6..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMVfe..
/
bcf44..
ownership of
3841b..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMbhP..
/
68c3e..
ownership of
b31db..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMKBp..
/
5f223..
ownership of
93aac..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMSJV..
/
0299e..
ownership of
a81e1..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMZuq..
/
fbf67..
ownership of
f6760..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMVgQ..
/
d48f3..
ownership of
f0254..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMaRP..
/
242e5..
ownership of
c5705..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMXbi..
/
9e12c..
ownership of
dd7e2..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMPHW..
/
0acce..
ownership of
e2901..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMQQU..
/
fe419..
ownership of
546d6..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMJ6a..
/
154eb..
ownership of
0423e..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMUoa..
/
8d958..
ownership of
877e4..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
TMPXy..
/
bc9b5..
ownership of
3a4ad..
as obj with payaddr
Pr6Pc..
rights free controlledby
Pr6Pc..
upto 0
PUVNt..
/
079a5..
doc published by
Pr6Pc..
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Definition
nIn
nIn
:=
λ x0 x1 .
not
(
x0
∈
x1
)
Known
In_ind
In_ind
:
∀ x0 :
ι → ο
.
(
∀ x1 .
(
∀ x2 .
x2
∈
x1
⟶
x0
x2
)
⟶
x0
x1
)
⟶
∀ x1 .
x0
x1
Known
In_irref
In_irref
:
∀ x0 .
nIn
x0
x0
Theorem
258d1..
:
∀ x0 x1 x2 .
x0
∈
x1
⟶
x1
∈
x2
⟶
nIn
x2
x0
(proof)
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Known
Eps_i_ax
Eps_i_ax
:
∀ x0 :
ι → ο
.
∀ x1 .
x0
x1
⟶
x0
(
prim0
x0
)
Known
andI
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Theorem
Eps_i_set_R
Eps_i_set_R
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
x0
⟶
x1
x2
⟶
and
(
prim0
(
λ x3 .
and
(
x3
∈
x0
)
(
x1
x3
)
)
∈
x0
)
(
x1
(
prim0
(
λ x3 .
and
(
x3
∈
x0
)
(
x1
x3
)
)
)
)
(proof)
Definition
or
or
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x2
)
⟶
(
x1
⟶
x2
)
⟶
x2
Definition
If_i
If_i
:=
λ x0 : ο .
λ x1 x2 .
prim0
(
λ x3 .
or
(
and
x0
(
x3
=
x1
)
)
(
and
(
not
x0
)
(
x3
=
x2
)
)
)
Known
xm
xm
:
∀ x0 : ο .
or
x0
(
not
x0
)
Known
orIL
orIL
:
∀ x0 x1 : ο .
x0
⟶
or
x0
x1
Known
orIR
orIR
:
∀ x0 x1 : ο .
x1
⟶
or
x0
x1
Known
If_i_correct
If_i_correct
:
∀ x0 : ο .
∀ x1 x2 .
or
(
and
x0
(
If_i
x0
x1
x2
=
x1
)
)
(
and
(
not
x0
)
(
If_i
x0
x1
x2
=
x2
)
)
Known
andEL
andEL
:
∀ x0 x1 : ο .
and
x0
x1
⟶
x0
Known
andER
andER
:
∀ x0 x1 : ο .
and
x0
x1
⟶
x1
Known
If_i_0
If_i_0
:
∀ x0 : ο .
∀ x1 x2 .
not
x0
⟶
If_i
x0
x1
x2
=
x2
Known
If_i_1
If_i_1
:
∀ x0 : ο .
∀ x1 x2 .
x0
⟶
If_i
x0
x1
x2
=
x1
Known
If_i_or
If_i_or
:
∀ x0 : ο .
∀ x1 x2 .
or
(
If_i
x0
x1
x2
=
x1
)
(
If_i
x0
x1
x2
=
x2
)
Known
If_i_eta
If_i_eta
:
∀ x0 : ο .
∀ x1 .
If_i
x0
x1
x1
=
x1
Theorem
exandE_ii
exandE_ii
:
∀ x0 x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 : ο .
(
∀ x3 :
ι → ι
.
and
(
x0
x3
)
(
x1
x3
)
⟶
x2
)
⟶
x2
)
⟶
∀ x2 : ο .
(
∀ x3 :
ι → ι
.
x0
x3
⟶
x1
x3
⟶
x2
)
⟶
x2
(proof)
Theorem
exandE_iii
exandE_iii
:
∀ x0 x1 :
(
ι →
ι → ι
)
→ ο
.
(
∀ x2 : ο .
(
∀ x3 :
ι →
ι → ι
.
and
(
x0
x3
)
(
x1
x3
)
⟶
x2
)
⟶
x2
)
⟶
∀ x2 : ο .
(
∀ x3 :
ι →
ι → ι
.
x0
x3
⟶
x1
x3
⟶
x2
)
⟶
x2
(proof)
Theorem
exandE_iiii
exandE_iiii
:
∀ x0 x1 :
(
ι →
ι →
ι → ι
)
→ ο
.
(
∀ x2 : ο .
(
∀ x3 :
ι →
ι →
ι → ι
.
and
(
x0
x3
)
(
x1
x3
)
⟶
x2
)
⟶
x2
)
⟶
∀ x2 : ο .
(
∀ x3 :
ι →
ι →
ι → ι
.
x0
x3
⟶
x1
x3
⟶
x2
)
⟶
x2
(proof)
Theorem
exandE_iio
exandE_iio
:
∀ x0 x1 :
(
ι →
ι → ο
)
→ ο
.
(
∀ x2 : ο .
(
∀ x3 :
ι →
ι → ο
.
and
(
x0
x3
)
(
x1
x3
)
⟶
x2
)
⟶
x2
)
⟶
∀ x2 : ο .
(
∀ x3 :
ι →
ι → ο
.
x0
x3
⟶
x1
x3
⟶
x2
)
⟶
x2
(proof)
Theorem
exandE_iiio
exandE_iiio
:
∀ x0 x1 :
(
ι →
ι →
ι → ο
)
→ ο
.
(
∀ x2 : ο .
(
∀ x3 :
ι →
ι →
ι → ο
.
and
(
x0
x3
)
(
x1
x3
)
⟶
x2
)
⟶
x2
)
⟶
∀ x2 : ο .
(
∀ x3 :
ι →
ι →
ι → ο
.
x0
x3
⟶
x1
x3
⟶
x2
)
⟶
x2
(proof)
Definition
Descr_ii
Descr_ii
:=
λ x0 :
(
ι → ι
)
→ ο
.
λ x1 .
prim0
(
λ x2 .
∀ x3 :
ι → ι
.
x0
x3
⟶
x3
x1
=
x2
)
Theorem
Descr_ii_prop
Descr_ii_prop
:
∀ x0 :
(
ι → ι
)
→ ο
.
(
∀ x1 : ο .
(
∀ x2 :
ι → ι
.
x0
x2
⟶
x1
)
⟶
x1
)
⟶
(
∀ x1 x2 :
ι → ι
.
x0
x1
⟶
x0
x2
⟶
x1
=
x2
)
⟶
x0
(
Descr_ii
x0
)
(proof)
Definition
Descr_iii
Descr_iii
:=
λ x0 :
(
ι →
ι → ι
)
→ ο
.
λ x1 x2 .
prim0
(
λ x3 .
∀ x4 :
ι →
ι → ι
.
x0
x4
⟶
x4
x1
x2
=
x3
)
Theorem
Descr_iii_prop
Descr_iii_prop
:
∀ x0 :
(
ι →
ι → ι
)
→ ο
.
(
∀ x1 : ο .
(
∀ x2 :
ι →
ι → ι
.
x0
x2
⟶
x1
)
⟶
x1
)
⟶
(
∀ x1 x2 :
ι →
ι → ι
.
x0
x1
⟶
x0
x2
⟶
x1
=
x2
)
⟶
x0
(
Descr_iii
x0
)
(proof)
Definition
Descr_iio
Descr_iio
:=
λ x0 :
(
ι →
ι → ο
)
→ ο
.
λ x1 x2 .
∀ x3 :
ι →
ι → ο
.
x0
x3
⟶
x3
x1
x2
Known
prop_ext_2
prop_ext_2
:
∀ x0 x1 : ο .
(
x0
⟶
x1
)
⟶
(
x1
⟶
x0
)
⟶
x0
=
x1
Theorem
Descr_iio_prop
Descr_iio_prop
:
∀ x0 :
(
ι →
ι → ο
)
→ ο
.
(
∀ x1 : ο .
(
∀ x2 :
ι →
ι → ο
.
x0
x2
⟶
x1
)
⟶
x1
)
⟶
(
∀ x1 x2 :
ι →
ι → ο
.
x0
x1
⟶
x0
x2
⟶
x1
=
x2
)
⟶
x0
(
Descr_iio
x0
)
(proof)
Definition
Descr_Vo1
Descr_Vo1
:=
λ x0 :
(
ι → ο
)
→ ο
.
λ x1 .
∀ x2 :
ι → ο
.
x0
x2
⟶
x2
x1
Theorem
Descr_Vo1_prop
Descr_Vo1_prop
:
∀ x0 :
(
ι → ο
)
→ ο
.
(
∀ x1 : ο .
(
∀ x2 :
ι → ο
.
x0
x2
⟶
x1
)
⟶
x1
)
⟶
(
∀ x1 x2 :
ι → ο
.
x0
x1
⟶
x0
x2
⟶
x1
=
x2
)
⟶
x0
(
Descr_Vo1
x0
)
(proof)
Definition
Descr_Vo2
Descr_Vo2
:=
λ x0 :
(
(
ι → ο
)
→ ο
)
→ ο
.
λ x1 :
ι → ο
.
∀ x2 :
(
ι → ο
)
→ ο
.
x0
x2
⟶
x2
x1
Theorem
Descr_Vo2_prop
Descr_Vo2_prop
:
∀ x0 :
(
(
ι → ο
)
→ ο
)
→ ο
.
(
∀ x1 : ο .
(
∀ x2 :
(
ι → ο
)
→ ο
.
x0
x2
⟶
x1
)
⟶
x1
)
⟶
(
∀ x1 x2 :
(
ι → ο
)
→ ο
.
x0
x1
⟶
x0
x2
⟶
x1
=
x2
)
⟶
x0
(
Descr_Vo2
x0
)
(proof)
Definition
If_ii
If_ii
:=
λ x0 : ο .
λ x1 x2 :
ι → ι
.
λ x3 .
If_i
x0
(
x1
x3
)
(
x2
x3
)
Theorem
If_ii_1
If_ii_1
:
∀ x0 : ο .
∀ x1 x2 :
ι → ι
.
x0
⟶
If_ii
x0
x1
x2
=
x1
(proof)
Theorem
If_ii_0
If_ii_0
:
∀ x0 : ο .
∀ x1 x2 :
ι → ι
.
not
x0
⟶
If_ii
x0
x1
x2
=
x2
(proof)
Definition
If_iii
If_iii
:=
λ x0 : ο .
λ x1 x2 :
ι →
ι → ι
.
λ x3 x4 .
If_i
x0
(
x1
x3
x4
)
(
x2
x3
x4
)
Theorem
If_iii_1
If_iii_1
:
∀ x0 : ο .
∀ x1 x2 :
ι →
ι → ι
.
x0
⟶
If_iii
x0
x1
x2
=
x1
(proof)
Theorem
If_iii_0
If_iii_0
:
∀ x0 : ο .
∀ x1 x2 :
ι →
ι → ι
.
not
x0
⟶
If_iii
x0
x1
x2
=
x2
(proof)
Definition
If_Vo1
If_Vo1
:=
λ x0 : ο .
λ x1 x2 :
ι → ο
.
λ x3 .
and
(
x0
⟶
x1
x3
)
(
not
x0
⟶
x2
x3
)
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Known
notE
notE
:
∀ x0 : ο .
not
x0
⟶
x0
⟶
False
Theorem
If_Vo1_1
If_Vo1_1
:
∀ x0 : ο .
∀ x1 x2 :
ι → ο
.
x0
⟶
If_Vo1
x0
x1
x2
=
x1
(proof)
Theorem
If_Vo1_0
If_Vo1_0
:
∀ x0 : ο .
∀ x1 x2 :
ι → ο
.
not
x0
⟶
If_Vo1
x0
x1
x2
=
x2
(proof)
Definition
If_iio
If_iio
:=
λ x0 : ο .
λ x1 x2 :
ι →
ι → ο
.
λ x3 x4 .
and
(
x0
⟶
x1
x3
x4
)
(
not
x0
⟶
x2
x3
x4
)
Theorem
If_iio_1
If_iio_1
:
∀ x0 : ο .
∀ x1 x2 :
ι →
ι → ο
.
x0
⟶
If_iio
x0
x1
x2
=
x1
(proof)
Theorem
If_iio_0
If_iio_0
:
∀ x0 : ο .
∀ x1 x2 :
ι →
ι → ο
.
not
x0
⟶
If_iio
x0
x1
x2
=
x2
(proof)
Definition
If_Vo2
If_Vo2
:=
λ x0 : ο .
λ x1 x2 :
(
ι → ο
)
→ ο
.
λ x3 :
ι → ο
.
and
(
x0
⟶
x1
x3
)
(
not
x0
⟶
x2
x3
)
Theorem
If_Vo2_1
If_Vo2_1
:
∀ x0 : ο .
∀ x1 x2 :
(
ι → ο
)
→ ο
.
x0
⟶
If_Vo2
x0
x1
x2
=
x1
(proof)
Theorem
If_Vo2_0
If_Vo2_0
:
∀ x0 : ο .
∀ x1 x2 :
(
ι → ο
)
→ ο
.
not
x0
⟶
If_Vo2
x0
x1
x2
=
x2
(proof)
Definition
In_rec_i_G
In_rec_i_G
:=
λ x0 :
ι →
(
ι → ι
)
→ ι
.
λ x1 x2 .
∀ x3 :
ι →
ι → ο
.
(
∀ x4 .
∀ x5 :
ι → ι
.
(
∀ x6 .
x6
∈
x4
⟶
x3
x6
(
x5
x6
)
)
⟶
x3
x4
(
x0
x4
x5
)
)
⟶
x3
x1
x2
Definition
In_rec_i
In_rec_i
:=
λ x0 :
ι →
(
ι → ι
)
→ ι
.
λ x1 .
prim0
(
In_rec_i_G
x0
x1
)
Theorem
In_rec_i_G_c
In_rec_i_G_c
:
∀ x0 :
ι →
(
ι → ι
)
→ ι
.
∀ x1 .
∀ x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x1
⟶
In_rec_i_G
x0
x3
(
x2
x3
)
)
⟶
In_rec_i_G
x0
x1
(
x0
x1
x2
)
(proof)
Theorem
In_rec_i_G_inv
In_rec_i_G_inv
:
∀ x0 :
ι →
(
ι → ι
)
→ ι
.
∀ x1 x2 .
In_rec_i_G
x0
x1
x2
⟶
∀ x3 : ο .
(
∀ x4 :
ι → ι
.
and
(
∀ x5 .
x5
∈
x1
⟶
In_rec_i_G
x0
x5
(
x4
x5
)
)
(
x2
=
x0
x1
x4
)
⟶
x3
)
⟶
x3
(proof)
Theorem
In_rec_i_G_f
In_rec_i_G_f
:
∀ x0 :
ι →
(
ι → ι
)
→ ι
.
(
∀ x1 .
∀ x2 x3 :
ι → ι
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 x2 x3 .
In_rec_i_G
x0
x1
x2
⟶
In_rec_i_G
x0
x1
x3
⟶
x2
=
x3
(proof)
Theorem
In_rec_i_G_In_rec_i
In_rec_i_G_In_rec_i
:
∀ x0 :
ι →
(
ι → ι
)
→ ι
.
(
∀ x1 .
∀ x2 x3 :
ι → ι
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
In_rec_i_G
x0
x1
(
In_rec_i
x0
x1
)
(proof)
Theorem
In_rec_i_G_In_rec_i_d
In_rec_i_G_In_rec_i_d
:
∀ x0 :
ι →
(
ι → ι
)
→ ι
.
(
∀ x1 .
∀ x2 x3 :
ι → ι
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
In_rec_i_G
x0
x1
(
x0
x1
(
In_rec_i
x0
)
)
(proof)
Theorem
In_rec_i_eq
In_rec_i_eq
:
∀ x0 :
ι →
(
ι → ι
)
→ ι
.
(
∀ x1 .
∀ x2 x3 :
ι → ι
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
In_rec_i
x0
x1
=
x0
x1
(
In_rec_i
x0
)
(proof)
Definition
In_rec_G_ii
In_rec_G_ii
:=
λ x0 :
ι →
(
ι →
ι → ι
)
→
ι → ι
.
λ x1 .
λ x2 :
ι → ι
.
∀ x3 :
ι →
(
ι → ι
)
→ ο
.
(
∀ x4 .
∀ x5 :
ι →
ι → ι
.
(
∀ x6 .
x6
∈
x4
⟶
x3
x6
(
x5
x6
)
)
⟶
x3
x4
(
x0
x4
x5
)
)
⟶
x3
x1
x2
Definition
In_rec_ii
In_rec_ii
:=
λ x0 :
ι →
(
ι →
ι → ι
)
→
ι → ι
.
λ x1 .
Descr_ii
(
In_rec_G_ii
x0
x1
)
Theorem
In_rec_G_ii_c
In_rec_G_ii_c
:
∀ x0 :
ι →
(
ι →
ι → ι
)
→
ι → ι
.
∀ x1 .
∀ x2 :
ι →
ι → ι
.
(
∀ x3 .
x3
∈
x1
⟶
In_rec_G_ii
x0
x3
(
x2
x3
)
)
⟶
In_rec_G_ii
x0
x1
(
x0
x1
x2
)
(proof)
Theorem
In_rec_G_ii_inv
In_rec_G_ii_inv
:
∀ x0 :
ι →
(
ι →
ι → ι
)
→
ι → ι
.
∀ x1 .
∀ x2 :
ι → ι
.
In_rec_G_ii
x0
x1
x2
⟶
∀ x3 : ο .
(
∀ x4 :
ι →
ι → ι
.
and
(
∀ x5 .
x5
∈
x1
⟶
In_rec_G_ii
x0
x5
(
x4
x5
)
)
(
x2
=
x0
x1
x4
)
⟶
x3
)
⟶
x3
(proof)
Theorem
In_rec_G_ii_f
In_rec_G_ii_f
:
∀ x0 :
ι →
(
ι →
ι → ι
)
→
ι → ι
.
(
∀ x1 .
∀ x2 x3 :
ι →
ι → ι
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
∀ x2 x3 :
ι → ι
.
In_rec_G_ii
x0
x1
x2
⟶
In_rec_G_ii
x0
x1
x3
⟶
x2
=
x3
(proof)
Theorem
In_rec_G_ii_In_rec_ii
In_rec_G_ii_In_rec_ii
:
∀ x0 :
ι →
(
ι →
ι → ι
)
→
ι → ι
.
(
∀ x1 .
∀ x2 x3 :
ι →
ι → ι
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
In_rec_G_ii
x0
x1
(
In_rec_ii
x0
x1
)
(proof)
Theorem
In_rec_G_ii_In_rec_ii_d
In_rec_G_ii_In_rec_ii_d
:
∀ x0 :
ι →
(
ι →
ι → ι
)
→
ι → ι
.
(
∀ x1 .
∀ x2 x3 :
ι →
ι → ι
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
In_rec_G_ii
x0
x1
(
x0
x1
(
In_rec_ii
x0
)
)
(proof)
Theorem
In_rec_ii_eq
In_rec_ii_eq
:
∀ x0 :
ι →
(
ι →
ι → ι
)
→
ι → ι
.
(
∀ x1 .
∀ x2 x3 :
ι →
ι → ι
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
In_rec_ii
x0
x1
=
x0
x1
(
In_rec_ii
x0
)
(proof)
Definition
In_rec_G_iii
In_rec_G_iii
:=
λ x0 :
ι →
(
ι →
ι →
ι → ι
)
→
ι →
ι → ι
.
λ x1 .
λ x2 :
ι →
ι → ι
.
∀ x3 :
ι →
(
ι →
ι → ι
)
→ ο
.
(
∀ x4 .
∀ x5 :
ι →
ι →
ι → ι
.
(
∀ x6 .
x6
∈
x4
⟶
x3
x6
(
x5
x6
)
)
⟶
x3
x4
(
x0
x4
x5
)
)
⟶
x3
x1
x2
Definition
In_rec_iii
In_rec_iii
:=
λ x0 :
ι →
(
ι →
ι →
ι → ι
)
→
ι →
ι → ι
.
λ x1 .
Descr_iii
(
In_rec_G_iii
x0
x1
)
Theorem
In_rec_G_iii_c
In_rec_G_iii_c
:
∀ x0 :
ι →
(
ι →
ι →
ι → ι
)
→
ι →
ι → ι
.
∀ x1 .
∀ x2 :
ι →
ι →
ι → ι
.
(
∀ x3 .
x3
∈
x1
⟶
In_rec_G_iii
x0
x3
(
x2
x3
)
)
⟶
In_rec_G_iii
x0
x1
(
x0
x1
x2
)
(proof)
Theorem
In_rec_G_iii_inv
In_rec_G_iii_inv
:
∀ x0 :
ι →
(
ι →
ι →
ι → ι
)
→
ι →
ι → ι
.
∀ x1 .
∀ x2 :
ι →
ι → ι
.
In_rec_G_iii
x0
x1
x2
⟶
∀ x3 : ο .
(
∀ x4 :
ι →
ι →
ι → ι
.
and
(
∀ x5 .
x5
∈
x1
⟶
In_rec_G_iii
x0
x5
(
x4
x5
)
)
(
x2
=
x0
x1
x4
)
⟶
x3
)
⟶
x3
(proof)
Theorem
In_rec_G_iii_f
In_rec_G_iii_f
:
∀ x0 :
ι →
(
ι →
ι →
ι → ι
)
→
ι →
ι → ι
.
(
∀ x1 .
∀ x2 x3 :
ι →
ι →
ι → ι
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
∀ x2 x3 :
ι →
ι → ι
.
In_rec_G_iii
x0
x1
x2
⟶
In_rec_G_iii
x0
x1
x3
⟶
x2
=
x3
(proof)
Theorem
In_rec_G_iii_In_rec_iii
In_rec_G_iii_In_rec_iii
:
∀ x0 :
ι →
(
ι →
ι →
ι → ι
)
→
ι →
ι → ι
.
(
∀ x1 .
∀ x2 x3 :
ι →
ι →
ι → ι
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
In_rec_G_iii
x0
x1
(
In_rec_iii
x0
x1
)
(proof)
Theorem
In_rec_G_iii_In_rec_iii_d
In_rec_G_iii_In_rec_iii_d
:
∀ x0 :
ι →
(
ι →
ι →
ι → ι
)
→
ι →
ι → ι
.
(
∀ x1 .
∀ x2 x3 :
ι →
ι →
ι → ι
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
In_rec_G_iii
x0
x1
(
x0
x1
(
In_rec_iii
x0
)
)
(proof)
Theorem
In_rec_iii_eq
In_rec_iii_eq
:
∀ x0 :
ι →
(
ι →
ι →
ι → ι
)
→
ι →
ι → ι
.
(
∀ x1 .
∀ x2 x3 :
ι →
ι →
ι → ι
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
In_rec_iii
x0
x1
=
x0
x1
(
In_rec_iii
x0
)
(proof)
Definition
6b023..
:=
λ x0 :
ι →
(
ι →
ι →
ι → ο
)
→
ι →
ι → ο
.
λ x1 .
λ x2 :
ι →
ι → ο
.
∀ x3 :
ι →
(
ι →
ι → ο
)
→ ο
.
(
∀ x4 .
∀ x5 :
ι →
ι →
ι → ο
.
(
∀ x6 .
x6
∈
x4
⟶
x3
x6
(
x5
x6
)
)
⟶
x3
x4
(
x0
x4
x5
)
)
⟶
x3
x1
x2
Definition
In_rec_iio
In_rec_iio
:=
λ x0 :
ι →
(
ι →
ι →
ι → ο
)
→
ι →
ι → ο
.
λ x1 .
Descr_iio
(
6b023..
x0
x1
)
Theorem
6f12d..
:
∀ x0 :
ι →
(
ι →
ι →
ι → ο
)
→
ι →
ι → ο
.
∀ x1 .
∀ x2 :
ι →
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
6b023..
x0
x3
(
x2
x3
)
)
⟶
6b023..
x0
x1
(
x0
x1
x2
)
(proof)
Theorem
b0c8e..
:
∀ x0 :
ι →
(
ι →
ι →
ι → ο
)
→
ι →
ι → ο
.
∀ x1 .
∀ x2 :
ι →
ι → ο
.
6b023..
x0
x1
x2
⟶
∀ x3 : ο .
(
∀ x4 :
ι →
ι →
ι → ο
.
and
(
∀ x5 .
x5
∈
x1
⟶
6b023..
x0
x5
(
x4
x5
)
)
(
x2
=
x0
x1
x4
)
⟶
x3
)
⟶
x3
(proof)
Theorem
41db9..
:
∀ x0 :
ι →
(
ι →
ι →
ι → ο
)
→
ι →
ι → ο
.
(
∀ x1 .
∀ x2 x3 :
ι →
ι →
ι → ο
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
∀ x2 x3 :
ι →
ι → ο
.
6b023..
x0
x1
x2
⟶
6b023..
x0
x1
x3
⟶
x2
=
x3
(proof)
Theorem
409d6..
:
∀ x0 :
ι →
(
ι →
ι →
ι → ο
)
→
ι →
ι → ο
.
(
∀ x1 .
∀ x2 x3 :
ι →
ι →
ι → ο
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
6b023..
x0
x1
(
In_rec_iio
x0
x1
)
(proof)
Theorem
67223..
:
∀ x0 :
ι →
(
ι →
ι →
ι → ο
)
→
ι →
ι → ο
.
(
∀ x1 .
∀ x2 x3 :
ι →
ι →
ι → ο
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
6b023..
x0
x1
(
x0
x1
(
In_rec_iio
x0
)
)
(proof)
Theorem
In_rec_iio_eq
In_rec_iio_eq
:
∀ x0 :
ι →
(
ι →
ι →
ι → ο
)
→
ι →
ι → ο
.
(
∀ x1 .
∀ x2 x3 :
ι →
ι →
ι → ο
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
In_rec_iio
x0
x1
=
x0
x1
(
In_rec_iio
x0
)
(proof)
Definition
f6068..
:=
λ x0 :
ι →
(
ι →
ι → ο
)
→
ι → ο
.
λ x1 .
λ x2 :
ι → ο
.
∀ x3 :
ι →
(
ι → ο
)
→ ο
.
(
∀ x4 .
∀ x5 :
ι →
ι → ο
.
(
∀ x6 .
x6
∈
x4
⟶
x3
x6
(
x5
x6
)
)
⟶
x3
x4
(
x0
x4
x5
)
)
⟶
x3
x1
x2
Definition
In_rec_Vo1
In_rec_Vo1
:=
λ x0 :
ι →
(
ι →
ι → ο
)
→
ι → ο
.
λ x1 .
Descr_Vo1
(
f6068..
x0
x1
)
Theorem
0d2cd..
:
∀ x0 :
ι →
(
ι →
ι → ο
)
→
ι → ο
.
∀ x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
f6068..
x0
x3
(
x2
x3
)
)
⟶
f6068..
x0
x1
(
x0
x1
x2
)
(proof)
Theorem
4d242..
:
∀ x0 :
ι →
(
ι →
ι → ο
)
→
ι → ο
.
∀ x1 .
∀ x2 :
ι → ο
.
f6068..
x0
x1
x2
⟶
∀ x3 : ο .
(
∀ x4 :
ι →
ι → ο
.
and
(
∀ x5 .
x5
∈
x1
⟶
f6068..
x0
x5
(
x4
x5
)
)
(
x2
=
x0
x1
x4
)
⟶
x3
)
⟶
x3
(proof)
Theorem
ebaf1..
:
∀ x0 :
ι →
(
ι →
ι → ο
)
→
ι → ο
.
(
∀ x1 .
∀ x2 x3 :
ι →
ι → ο
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
∀ x2 x3 :
ι → ο
.
f6068..
x0
x1
x2
⟶
f6068..
x0
x1
x3
⟶
x2
=
x3
(proof)
Theorem
2f624..
:
∀ x0 :
ι →
(
ι →
ι → ο
)
→
ι → ο
.
(
∀ x1 .
∀ x2 x3 :
ι →
ι → ο
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
f6068..
x0
x1
(
In_rec_Vo1
x0
x1
)
(proof)
Theorem
722ac..
:
∀ x0 :
ι →
(
ι →
ι → ο
)
→
ι → ο
.
(
∀ x1 .
∀ x2 x3 :
ι →
ι → ο
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
f6068..
x0
x1
(
x0
x1
(
In_rec_Vo1
x0
)
)
(proof)
Theorem
In_rec_Vo1_eq
In_rec_Vo1_eq
:
∀ x0 :
ι →
(
ι →
ι → ο
)
→
ι → ο
.
(
∀ x1 .
∀ x2 x3 :
ι →
ι → ο
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
In_rec_Vo1
x0
x1
=
x0
x1
(
In_rec_Vo1
x0
)
(proof)
Definition
2b1c2..
:=
λ x0 :
ι →
(
ι →
(
ι → ο
)
→ ο
)
→
(
ι → ο
)
→ ο
.
λ x1 .
λ x2 :
(
ι → ο
)
→ ο
.
∀ x3 :
ι →
(
(
ι → ο
)
→ ο
)
→ ο
.
(
∀ x4 .
∀ x5 :
ι →
(
ι → ο
)
→ ο
.
(
∀ x6 .
x6
∈
x4
⟶
x3
x6
(
x5
x6
)
)
⟶
x3
x4
(
x0
x4
x5
)
)
⟶
x3
x1
x2
Definition
In_rec_Vo2
In_rec_Vo2
:=
λ x0 :
ι →
(
ι →
(
ι → ο
)
→ ο
)
→
(
ι → ο
)
→ ο
.
λ x1 .
Descr_Vo2
(
2b1c2..
x0
x1
)
Theorem
07e5d..
:
∀ x0 :
ι →
(
ι →
(
ι → ο
)
→ ο
)
→
(
ι → ο
)
→ ο
.
∀ x1 .
∀ x2 :
ι →
(
ι → ο
)
→ ο
.
(
∀ x3 .
x3
∈
x1
⟶
2b1c2..
x0
x3
(
x2
x3
)
)
⟶
2b1c2..
x0
x1
(
x0
x1
x2
)
(proof)
Theorem
994ef..
:
∀ x0 :
ι →
(
ι →
(
ι → ο
)
→ ο
)
→
(
ι → ο
)
→ ο
.
∀ x1 .
∀ x2 :
(
ι → ο
)
→ ο
.
2b1c2..
x0
x1
x2
⟶
∀ x3 : ο .
(
∀ x4 :
ι →
(
ι → ο
)
→ ο
.
and
(
∀ x5 .
x5
∈
x1
⟶
2b1c2..
x0
x5
(
x4
x5
)
)
(
x2
=
x0
x1
x4
)
⟶
x3
)
⟶
x3
(proof)
Theorem
d8d0b..
:
∀ x0 :
ι →
(
ι →
(
ι → ο
)
→ ο
)
→
(
ι → ο
)
→ ο
.
(
∀ x1 .
∀ x2 x3 :
ι →
(
ι → ο
)
→ ο
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
∀ x2 x3 :
(
ι → ο
)
→ ο
.
2b1c2..
x0
x1
x2
⟶
2b1c2..
x0
x1
x3
⟶
x2
=
x3
(proof)
Theorem
2cb7a..
:
∀ x0 :
ι →
(
ι →
(
ι → ο
)
→ ο
)
→
(
ι → ο
)
→ ο
.
(
∀ x1 .
∀ x2 x3 :
ι →
(
ι → ο
)
→ ο
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
2b1c2..
x0
x1
(
In_rec_Vo2
x0
x1
)
(proof)
Theorem
00e25..
:
∀ x0 :
ι →
(
ι →
(
ι → ο
)
→ ο
)
→
(
ι → ο
)
→ ο
.
(
∀ x1 .
∀ x2 x3 :
ι →
(
ι → ο
)
→ ο
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
2b1c2..
x0
x1
(
x0
x1
(
In_rec_Vo2
x0
)
)
(proof)
Theorem
In_rec_Vo2_eq
In_rec_Vo2_eq
:
∀ x0 :
ι →
(
ι →
(
ι → ο
)
→ ο
)
→
(
ι → ο
)
→ ο
.
(
∀ x1 .
∀ x2 x3 :
ι →
(
ι → ο
)
→ ο
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
In_rec_Vo2
x0
x1
=
x0
x1
(
In_rec_Vo2
x0
)
(proof)