Search for blocks/addresses/...
Proofgold Proposition
(
∀ x0 :
(
ι → ι
)
→
ι → ο
.
∀ x1 x2 :
(
(
ι → ι
)
→ ι
)
→
ι →
ι → ο
.
∀ x3 :
(
ι →
(
(
ι → ι
)
→ ι
)
→ ι
)
→
ι →
(
(
(
ι → ι
)
→ ι
)
→
ι → ι
)
→ ο
.
(
∀ x4 x5 x6 x7 .
In
(
setsum
(
setsum
(
setsum
(
Inj1
0
)
0
)
(
Inj0
(
Inj0
0
)
)
)
(
setsum
(
setsum
0
0
)
(
Inj0
(
setsum
0
0
)
)
)
)
(
setsum
(
setsum
(
setsum
(
setsum
0
0
)
x4
)
x7
)
0
)
⟶
x1
(
λ x8 :
ι → ι
.
setsum
(
setsum
(
Inj0
x5
)
(
Inj0
0
)
)
0
)
(
Inj0
(
setsum
(
setsum
(
setsum
0
0
)
(
setsum
0
0
)
)
(
Inj0
(
Inj0
0
)
)
)
)
(
setsum
(
Inj0
(
setsum
0
(
Inj1
0
)
)
)
0
)
⟶
x3
(
λ x8 .
λ x9 :
(
ι → ι
)
→ ι
.
x9
(
λ x10 .
x8
)
)
x5
(
λ x8 :
(
ι → ι
)
→ ι
.
λ x9 .
Inj0
0
)
)
⟶
(
∀ x4 :
ι →
ι → ι
.
∀ x5 .
∀ x6 :
ι →
ι → ι
.
∀ x7 :
ι →
(
ι →
ι → ι
)
→ ι
.
x3
(
λ x8 .
λ x9 :
(
ι → ι
)
→ ι
.
setsum
(
x9
(
λ x10 .
setsum
(
setsum
0
0
)
x8
)
)
0
)
0
(
λ x8 :
(
ι → ι
)
→ ι
.
λ x9 .
setsum
(
x8
(
λ x10 .
x8
(
λ x11 .
setsum
0
0
)
)
)
0
)
⟶
False
)
⟶
(
∀ x4 .
∀ x5 :
ι →
(
ι → ι
)
→ ι
.
∀ x6 :
ι → ι
.
∀ x7 :
(
ι → ι
)
→
(
ι →
ι → ι
)
→
ι → ι
.
x0
(
λ x8 .
0
)
(
x6
(
Inj0
(
setsum
(
setsum
0
0
)
(
setsum
0
0
)
)
)
)
⟶
x2
(
λ x8 :
ι → ι
.
setsum
(
setsum
(
x8
0
)
0
)
(
x7
(
λ x9 .
0
)
(
λ x9 x10 .
setsum
(
Inj0
0
)
0
)
(
x6
(
Inj0
0
)
)
)
)
0
(
x7
(
λ x8 .
Inj1
(
x5
0
(
λ x9 .
0
)
)
)
(
λ x8 x9 .
x8
)
0
)
)
⟶
(
∀ x4 .
∀ x5 :
ι →
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→ ι
.
∀ x6 x7 .
x2
(
λ x8 :
ι → ι
.
x6
)
(
setsum
(
setsum
x4
x7
)
(
setsum
0
0
)
)
(
Inj0
0
)
⟶
x0
(
λ x8 .
Inj0
(
x5
0
(
λ x9 :
ι → ι
.
λ x10 .
Inj1
(
Inj0
0
)
)
(
λ x9 .
0
)
)
)
(
setsum
x6
(
Inj0
(
Inj0
(
Inj1
0
)
)
)
)
)
⟶
(
∀ x4 .
∀ x5 :
ι → ι
.
∀ x6 :
(
ι → ι
)
→
ι → ι
.
∀ x7 .
x0
(
λ x8 .
0
)
(
Inj1
x4
)
⟶
x1
(
λ x8 :
ι → ι
.
setsum
0
(
Inj0
(
Inj1
(
Inj1
0
)
)
)
)
x4
(
setsum
0
0
)
)
⟶
(
∀ x4 :
ι → ι
.
∀ x5 .
∀ x6 :
ι →
(
ι → ι
)
→ ι
.
∀ x7 :
(
(
(
ι → ι
)
→ ι
)
→ ι
)
→
ι →
ι →
ι → ι
.
x1
(
λ x8 :
ι → ι
.
setsum
0
x5
)
(
setsum
(
Inj1
0
)
(
setsum
(
Inj0
(
setsum
0
0
)
)
0
)
)
(
Inj1
(
x7
(
λ x8 :
(
ι → ι
)
→ ι
.
x6
(
Inj0
0
)
(
λ x9 .
Inj1
0
)
)
(
Inj1
(
Inj0
0
)
)
(
Inj0
(
setsum
0
0
)
)
0
)
)
⟶
In
(
Inj0
(
Inj0
(
x7
(
λ x8 :
(
ι → ι
)
→ ι
.
x8
(
λ x9 .
0
)
)
x5
(
Inj1
0
)
(
Inj0
0
)
)
)
)
(
x4
x5
)
)
⟶
(
∀ x4 x5 .
∀ x6 :
ι →
ι → ι
.
∀ x7 .
In
(
setsum
x7
(
setsum
0
0
)
)
(
Inj0
x7
)
⟶
x0
(
λ x8 .
x8
)
(
Inj1
0
)
⟶
x0
(
λ x8 .
x6
0
(
setsum
0
(
Inj0
0
)
)
)
(
setsum
(
setsum
(
Inj1
x5
)
0
)
(
setsum
(
x6
0
x4
)
(
setsum
(
Inj1
0
)
(
x6
0
0
)
)
)
)
)
⟶
(
∀ x4 x5 .
∀ x6 :
(
ι → ι
)
→ ι
.
∀ x7 :
(
(
(
ι → ι
)
→ ι
)
→
(
ι → ι
)
→
ι → ι
)
→
(
ι →
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
x0
(
λ x8 .
x6
(
λ x9 .
Inj1
0
)
)
(
Inj1
(
setsum
0
(
Inj1
(
setsum
0
0
)
)
)
)
⟶
False
)
⟶
False
)
⟶
∀ x0 : ο .
x0
type
prop
theory
HF
name
-
proof
PUPLh..
Megalodon
-
proofgold address
TMUEd..
creator
11899
PrGVS..
/
eec2a..
owner
11899
PrGVS..
/
eec2a..
term root
277ae..