Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrCit..
/
430d9..
PUgaN..
/
d18da..
vout
PrCit..
/
312d9..
5.63 bars
TMG9T..
/
c319d..
ownership of
d74be..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMdKK..
/
c7c5c..
ownership of
c8f4c..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
PUbiS..
/
b6946..
doc published by
Pr4zB..
Definition
Church17_p
:=
λ x0 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
∀ x1 :
(
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→ ο
.
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x2
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x3
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x4
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x5
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x6
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x7
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x8
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x9
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x10
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x11
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x12
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x13
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x14
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x15
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x16
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x17
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x18
)
⟶
x1
x0
Param
u1
:
ι
Param
u2
:
ι
Param
u3
:
ι
Param
u4
:
ι
Param
u5
:
ι
Param
u6
:
ι
Param
u7
:
ι
Param
u8
:
ι
Param
u9
:
ι
Param
u10
:
ι
Param
u11
:
ι
Param
u12
:
ι
Param
u13
:
ι
Param
u14
:
ι
Param
u15
:
ι
Param
u16
:
ι
Definition
False
False
:=
∀ x0 : ο .
x0
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Known
neq_9_0
neq_9_0
:
u9
=
0
⟶
∀ x0 : ο .
x0
Known
neq_9_1
neq_9_1
:
u9
=
u1
⟶
∀ x0 : ο .
x0
Known
neq_9_2
neq_9_2
:
u9
=
u2
⟶
∀ x0 : ο .
x0
Known
neq_9_3
neq_9_3
:
u9
=
u3
⟶
∀ x0 : ο .
x0
Known
neq_9_4
neq_9_4
:
u9
=
u4
⟶
∀ x0 : ο .
x0
Known
neq_9_5
neq_9_5
:
u9
=
u5
⟶
∀ x0 : ο .
x0
Known
neq_9_6
neq_9_6
:
u9
=
u6
⟶
∀ x0 : ο .
x0
Known
neq_9_7
neq_9_7
:
u9
=
u7
⟶
∀ x0 : ο .
x0
Known
neq_9_8
neq_9_8
:
u9
=
u8
⟶
∀ x0 : ο .
x0
Known
4fc31..
:
u10
=
u9
⟶
∀ x0 : ο .
x0
Known
4f03f..
:
u11
=
u9
⟶
∀ x0 : ο .
x0
Known
22885..
:
u12
=
u9
⟶
∀ x0 : ο .
x0
Known
3f24c..
:
u13
=
u9
⟶
∀ x0 : ο .
x0
Known
d7730..
:
u14
=
u9
⟶
∀ x0 : ο .
x0
Known
3a7bc..
:
u15
=
u9
⟶
∀ x0 : ο .
x0
Known
78b49..
:
u16
=
u9
⟶
∀ x0 : ο .
x0
Known
0e10e..
:
u10
=
0
⟶
∀ x0 : ο .
x0
Known
d183f..
:
u10
=
u1
⟶
∀ x0 : ο .
x0
Known
e02d9..
:
u10
=
u2
⟶
∀ x0 : ο .
x0
Known
68152..
:
u10
=
u3
⟶
∀ x0 : ο .
x0
Known
33d16..
:
u10
=
u4
⟶
∀ x0 : ο .
x0
Known
a7d50..
:
u10
=
u5
⟶
∀ x0 : ο .
x0
Known
d0401..
:
u10
=
u6
⟶
∀ x0 : ο .
x0
Known
7d7a8..
:
u10
=
u7
⟶
∀ x0 : ο .
x0
Known
96175..
:
u10
=
u8
⟶
∀ x0 : ο .
x0
Known
ebfb7..
:
u11
=
u10
⟶
∀ x0 : ο .
x0
Known
6c583..
:
u12
=
u10
⟶
∀ x0 : ο .
x0
Known
78358..
:
u13
=
u10
⟶
∀ x0 : ο .
x0
Known
f5ab5..
:
u14
=
u10
⟶
∀ x0 : ο .
x0
Known
b7f53..
:
u15
=
u10
⟶
∀ x0 : ο .
x0
Known
6879f..
:
u16
=
u10
⟶
∀ x0 : ο .
x0
Known
19f75..
:
u11
=
0
⟶
∀ x0 : ο .
x0
Known
618f7..
:
u11
=
u1
⟶
∀ x0 : ο .
x0
Known
2c42c..
:
u11
=
u2
⟶
∀ x0 : ο .
x0
Known
b06e1..
:
u11
=
u3
⟶
∀ x0 : ο .
x0
Known
6a6f1..
:
u11
=
u4
⟶
∀ x0 : ο .
x0
Known
1b659..
:
u11
=
u5
⟶
∀ x0 : ο .
x0
Known
949f2..
:
u11
=
u6
⟶
∀ x0 : ο .
x0
Known
4abfa..
:
u11
=
u7
⟶
∀ x0 : ο .
x0
Known
b3a20..
:
u11
=
u8
⟶
∀ x0 : ο .
x0
Known
ab306..
:
u12
=
u11
⟶
∀ x0 : ο .
x0
Known
bf497..
:
u13
=
u11
⟶
∀ x0 : ο .
x0
Known
4e1aa..
:
u14
=
u11
⟶
∀ x0 : ο .
x0
Known
9c5db..
:
u15
=
u11
⟶
∀ x0 : ο .
x0
Known
22184..
:
u16
=
u11
⟶
∀ x0 : ο .
x0
Known
efdfc..
:
u12
=
0
⟶
∀ x0 : ο .
x0
Known
ce0cd..
:
u12
=
u1
⟶
∀ x0 : ο .
x0
Known
8158b..
:
u12
=
u2
⟶
∀ x0 : ο .
x0
Known
e015c..
:
u12
=
u3
⟶
∀ x0 : ο .
x0
Known
7aa79..
:
u12
=
u4
⟶
∀ x0 : ο .
x0
Known
07eba..
:
u12
=
u5
⟶
∀ x0 : ο .
x0
Known
0bd83..
:
u12
=
u6
⟶
∀ x0 : ο .
x0
Known
6a15f..
:
u12
=
u7
⟶
∀ x0 : ο .
x0
Known
a6a6c..
:
u12
=
u8
⟶
∀ x0 : ο .
x0
Known
ad02f..
:
u13
=
u12
⟶
∀ x0 : ο .
x0
Known
ef4da..
:
u14
=
u12
⟶
∀ x0 : ο .
x0
Known
72647..
:
u15
=
u12
⟶
∀ x0 : ο .
x0
Known
fa664..
:
u16
=
u12
⟶
∀ x0 : ο .
x0
Known
733b2..
:
u13
=
0
⟶
∀ x0 : ο .
x0
Known
16246..
:
u13
=
u1
⟶
∀ x0 : ο .
x0
Known
40d25..
:
u13
=
u2
⟶
∀ x0 : ο .
x0
Known
19222..
:
u13
=
u3
⟶
∀ x0 : ο .
x0
Known
4d850..
:
u13
=
u4
⟶
∀ x0 : ο .
x0
Known
29333..
:
u13
=
u5
⟶
∀ x0 : ο .
x0
Known
02f5c..
:
u13
=
u6
⟶
∀ x0 : ο .
x0
Known
d9b35..
:
u13
=
u7
⟶
∀ x0 : ο .
x0
Known
0b225..
:
u13
=
u8
⟶
∀ x0 : ο .
x0
Known
e1947..
:
u14
=
u13
⟶
∀ x0 : ο .
x0
Known
4d8d4..
:
u15
=
u13
⟶
∀ x0 : ο .
x0
Known
4326e..
:
u16
=
u13
⟶
∀ x0 : ο .
x0
Known
fc551..
:
u14
=
0
⟶
∀ x0 : ο .
x0
Known
ac679..
:
u14
=
u1
⟶
∀ x0 : ο .
x0
Known
0bb18..
:
u14
=
u2
⟶
∀ x0 : ο .
x0
Known
d0fe4..
:
u14
=
u3
⟶
∀ x0 : ο .
x0
Known
ffd62..
:
u14
=
u4
⟶
∀ x0 : ο .
x0
Known
d6c57..
:
u14
=
u5
⟶
∀ x0 : ο .
x0
Known
62d80..
:
u14
=
u6
⟶
∀ x0 : ο .
x0
Known
01bf6..
:
u14
=
u7
⟶
∀ x0 : ο .
x0
Known
4f6ad..
:
u14
=
u8
⟶
∀ x0 : ο .
x0
Known
b8e82..
:
u15
=
u14
⟶
∀ x0 : ο .
x0
Known
71c5e..
:
u16
=
u14
⟶
∀ x0 : ο .
x0
Known
160ad..
:
u15
=
0
⟶
∀ x0 : ο .
x0
Known
174d1..
:
u15
=
u1
⟶
∀ x0 : ο .
x0
Known
4d715..
:
u15
=
u2
⟶
∀ x0 : ο .
x0
Known
70124..
:
u15
=
u3
⟶
∀ x0 : ο .
x0
Known
4b742..
:
u15
=
u4
⟶
∀ x0 : ο .
x0
Known
24fad..
:
u15
=
u5
⟶
∀ x0 : ο .
x0
Known
f5ac7..
:
u15
=
u6
⟶
∀ x0 : ο .
x0
Known
008b1..
:
u15
=
u7
⟶
∀ x0 : ο .
x0
Known
c0d75..
:
u15
=
u8
⟶
∀ x0 : ο .
x0
Known
41073..
:
u16
=
u15
⟶
∀ x0 : ο .
x0
Known
86ae3..
:
u16
=
0
⟶
∀ x0 : ο .
x0
Known
ab690..
:
u16
=
u1
⟶
∀ x0 : ο .
x0
Known
296ac..
:
u16
=
u2
⟶
∀ x0 : ο .
x0
Known
ca5c3..
:
u16
=
u3
⟶
∀ x0 : ο .
x0
Known
7b2eb..
:
u16
=
u4
⟶
∀ x0 : ο .
x0
Known
35bff..
:
u16
=
u5
⟶
∀ x0 : ο .
x0
Known
3bd28..
:
u16
=
u6
⟶
∀ x0 : ο .
x0
Known
d3a2f..
:
u16
=
u7
⟶
∀ x0 : ο .
x0
Known
6c306..
:
u16
=
u8
⟶
∀ x0 : ο .
x0
Known
768c1..
:
(
(
λ x1 x2 .
x2
)
=
λ x1 x2 .
x1
)
⟶
∀ x0 : ο .
x0
Theorem
d74be..
:
∀ x0 x1 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church17_p
x0
⟶
Church17_p
x1
⟶
(
(
λ x3 x4 .
x0
x4
x4
x4
x4
x4
x4
x4
x4
x4
x3
x3
x3
x3
x3
x3
x3
x3
)
=
λ x3 x4 .
x3
)
⟶
x0
0
u1
u2
u3
u4
u5
u6
u7
u8
u9
u10
u11
u12
u13
u14
u15
u16
=
x1
0
u1
u2
u3
u4
u5
u6
u7
u8
u9
u10
u11
u12
u13
u14
u15
u16
⟶
x0
=
x1
(proof)