Search for blocks/addresses/...
Proofgold Term Root Disambiguation
∀ x0 x1 x2 x3 x4 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
∀ x5 x6 x7 x8 x9 :
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
(
ι → ι
)
→
ι → ι
)
→
(
ι → ι
)
→
ι → ι
.
ChurchNum_3ary_proj_p
x0
⟶
ChurchNum_3ary_proj_p
x1
⟶
ChurchNum_3ary_proj_p
x2
⟶
ChurchNum_3ary_proj_p
x3
⟶
ChurchNum_3ary_proj_p
x4
⟶
ChurchNum_8ary_proj_p
x5
⟶
ChurchNum_8ary_proj_p
x6
⟶
ChurchNum_8ary_proj_p
x7
⟶
ChurchNum_8ary_proj_p
x8
⟶
ChurchNum_8ary_proj_p
x9
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x0
x5
x1
x6
=
λ x11 x12 .
x12
)
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x0
x5
x2
x7
=
λ x11 x12 .
x12
)
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x0
x5
x3
x8
=
λ x11 x12 .
x12
)
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x0
x5
x4
x9
=
λ x11 x12 .
x12
)
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x1
x6
x2
x7
=
λ x11 x12 .
x12
)
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x1
x6
x3
x8
=
λ x11 x12 .
x12
)
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x1
x6
x4
x9
=
λ x11 x12 .
x12
)
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x2
x7
x3
x8
=
λ x11 x12 .
x12
)
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x2
x7
x4
x9
=
λ x11 x12 .
x12
)
⟶
(
TwoRamseyGraph_4_5_24_ChurchNums_3x8
x3
x8
x4
x9
=
λ x11 x12 .
x12
)
⟶
∀ x10 .
(
∀ x11 .
x11
∈
u5
⟶
∀ x12 .
x12
∈
u5
⟶
ap
(
ap
x10
x11
)
x12
∈
24
)
⟶
(
∀ x11 .
x11
∈
u5
⟶
∀ x12 .
x12
∈
u5
⟶
∀ x13 .
x13
∈
u5
⟶
ap
(
ap
x10
x11
)
x12
=
ap
(
ap
x10
x11
)
x13
⟶
x12
=
x13
)
⟶
(
∀ x11 .
x11
∈
u5
⟶
∀ x12 .
x12
∈
u5
⟶
(
x11
=
x12
⟶
∀ x13 : ο .
x13
)
⟶
∀ x13 .
x13
∈
u5
⟶
∀ x14 .
x14
∈
u5
⟶
ap
(
ap
x10
x11
)
x13
=
ap
(
ap
x10
x12
)
x14
⟶
∀ x15 : ο .
x15
)
⟶
False
as obj
-
as prop
cd8d1..
theory
HotG
stx
55a67..
address
TMb33..