Search for blocks/addresses/...
Proofgold Address
address
PUSKj5wYwuKi1BSD8mBfEdE2hcegbcSRTgS
total
0
mg
-
conjpub
-
current assets
25382..
/
35a27..
bday:
18210
doc published by
Pr4zB..
Definition
Church13_p
:=
λ x0 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
∀ x1 :
(
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→ ο
.
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x2
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x3
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x4
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x5
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x6
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x7
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x8
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x9
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x10
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x11
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x12
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x13
)
⟶
x1
(
λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x14
)
⟶
x1
x0
Definition
TwoRamseyGraph_3_5_Church13
:=
λ x0 x1 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
λ x2 x3 .
x0
(
x1
x3
x2
x3
x3
x3
x2
x3
x3
x2
x3
x3
x3
x2
)
(
x1
x2
x3
x2
x3
x3
x3
x2
x3
x3
x2
x3
x3
x3
)
(
x1
x3
x2
x3
x2
x3
x3
x3
x2
x3
x3
x2
x3
x3
)
(
x1
x3
x3
x2
x3
x2
x3
x3
x3
x2
x3
x3
x2
x3
)
(
x1
x3
x3
x3
x2
x3
x2
x3
x3
x3
x2
x3
x3
x2
)
(
x1
x2
x3
x3
x3
x2
x3
x2
x3
x3
x3
x2
x3
x3
)
(
x1
x3
x2
x3
x3
x3
x2
x3
x2
x3
x3
x3
x2
x3
)
(
x1
x3
x3
x2
x3
x3
x3
x2
x3
x2
x3
x3
x3
x2
)
(
x1
x2
x3
x3
x2
x3
x3
x3
x2
x3
x2
x3
x3
x3
)
(
x1
x3
x2
x3
x3
x2
x3
x3
x3
x2
x3
x2
x3
x3
)
(
x1
x3
x3
x2
x3
x3
x2
x3
x3
x3
x2
x3
x2
x3
)
(
x1
x3
x3
x3
x2
x3
x3
x2
x3
x3
x3
x2
x3
x2
)
(
x1
x2
x3
x3
x3
x2
x3
x3
x2
x3
x3
x3
x2
x3
)
Definition
False
False
:=
∀ x0 : ο .
x0
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Known
691d6..
:
∀ x0 x1 x2 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church13_p
x0
⟶
Church13_p
x1
⟶
Church13_p
x2
⟶
(
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x6
)
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
x0
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x6
)
=
x0
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x6
)
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x6
)
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
x0
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
x0
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
x1
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x6
)
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
x0
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
x1
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
x2
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x6
)
x0
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x6
)
x1
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x6
)
x2
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
x0
x1
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
x0
x2
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
x1
x2
=
λ x4 x5 .
x5
)
⟶
False
Known
167fd..
:
∀ x0 x1 x2 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church13_p
x0
⟶
Church13_p
x1
⟶
Church13_p
x2
⟶
(
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x7
)
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
x0
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x7
)
=
x0
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x7
)
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x7
)
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
x0
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
x0
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
x1
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x7
)
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
x0
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
x1
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
x2
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x7
)
x0
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x7
)
x1
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x7
)
x2
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
x0
x1
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
x0
x2
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
x1
x2
=
λ x4 x5 .
x5
)
⟶
False
Known
8e1ba..
:
∀ x0 x1 x2 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church13_p
x0
⟶
Church13_p
x1
⟶
Church13_p
x2
⟶
(
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x8
)
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
x0
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x8
)
=
x0
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x8
)
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x8
)
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
x0
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
x0
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
x1
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x8
)
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
x0
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
x1
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
x2
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x8
)
x0
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x8
)
x1
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x8
)
x2
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
x0
x1
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
x0
x2
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
x1
x2
=
λ x4 x5 .
x5
)
⟶
False
Known
e781d..
:
∀ x0 x1 x2 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church13_p
x0
⟶
Church13_p
x1
⟶
Church13_p
x2
⟶
(
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x10
)
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
x0
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x10
)
=
x0
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x10
)
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x10
)
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
x0
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
x0
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
x1
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x10
)
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
x0
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
x1
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
x2
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x10
)
x0
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x10
)
x1
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x10
)
x2
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
x0
x1
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
x0
x2
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
x1
x2
=
λ x4 x5 .
x5
)
⟶
False
Known
27109..
:
∀ x0 x1 x2 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church13_p
x0
⟶
Church13_p
x1
⟶
Church13_p
x2
⟶
(
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x11
)
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
x0
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x11
)
=
x0
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x11
)
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x11
)
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
x0
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
x0
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
x1
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x11
)
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
x0
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
x1
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
x2
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x11
)
x0
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x11
)
x1
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x11
)
x2
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
x0
x1
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
x0
x2
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
x1
x2
=
λ x4 x5 .
x5
)
⟶
False
Known
43ae5..
:
∀ x0 x1 x2 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church13_p
x0
⟶
Church13_p
x1
⟶
Church13_p
x2
⟶
(
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x13
)
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
x0
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x13
)
=
x0
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x13
)
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x13
)
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
x0
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
x0
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
x1
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x13
)
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
x0
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
x1
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
x2
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x13
)
x0
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x13
)
x1
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x13
)
x2
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
x0
x1
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
x0
x2
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
x1
x2
=
λ x4 x5 .
x5
)
⟶
False
Known
1af1a..
:
∀ x0 x1 x2 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church13_p
x0
⟶
Church13_p
x1
⟶
Church13_p
x2
⟶
(
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x14
)
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
x0
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x14
)
=
x0
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x14
)
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x14
)
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
x0
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
x0
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
x1
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x14
)
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
x0
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
x1
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
x2
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x14
)
x0
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x14
)
x1
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x14
)
x2
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
x0
x1
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
x0
x2
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
x1
x2
=
λ x4 x5 .
x5
)
⟶
False
Known
cc732..
:
∀ x0 x1 x2 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church13_p
x0
⟶
Church13_p
x1
⟶
Church13_p
x2
⟶
(
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x15
)
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
x0
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x15
)
=
x0
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x15
)
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x15
)
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
x0
=
x1
⟶
∀ x3 : ο .
x3
)
⟶
(
x0
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
x1
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x15
)
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
x0
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
x1
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x4
)
x2
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x15
)
x0
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x15
)
x1
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x15
)
x2
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
x0
x1
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
x0
x2
=
λ x4 x5 .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
x1
x2
=
λ x4 x5 .
x5
)
⟶
False
Known
768c1..
:
(
(
λ x1 x2 .
x2
)
=
λ x1 x2 .
x1
)
⟶
∀ x0 : ο .
x0
Theorem
f57a7..
:
∀ x0 x1 x2 x3 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church13_p
x0
⟶
Church13_p
x1
⟶
Church13_p
x2
⟶
Church13_p
x3
⟶
(
(
λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x5
)
=
x0
⟶
∀ x4 : ο .
x4
)
⟶
(
(
λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x5
)
=
x1
⟶
∀ x4 : ο .
x4
)
⟶
(
(
λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x5
)
=
x2
⟶
∀ x4 : ο .
x4
)
⟶
(
(
λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x5
)
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
(
x0
=
x1
⟶
∀ x4 : ο .
x4
)
⟶
(
x0
=
x2
⟶
∀ x4 : ο .
x4
)
⟶
(
x0
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
(
x1
=
x2
⟶
∀ x4 : ο .
x4
)
⟶
(
x1
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
(
x2
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x5
)
x0
=
λ x5 x6 .
x6
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x5
)
x1
=
λ x5 x6 .
x6
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x5
)
x2
=
λ x5 x6 .
x6
)
⟶
(
TwoRamseyGraph_3_5_Church13
(
λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x5
)
x3
=
λ x5 x6 .
x6
)
⟶
(
TwoRamseyGraph_3_5_Church13
x0
x1
=
λ x5 x6 .
x6
)
⟶
(
TwoRamseyGraph_3_5_Church13
x0
x2
=
λ x5 x6 .
x6
)
⟶
(
TwoRamseyGraph_3_5_Church13
x0
x3
=
λ x5 x6 .
x6
)
⟶
(
TwoRamseyGraph_3_5_Church13
x1
x2
=
λ x5 x6 .
x6
)
⟶
(
TwoRamseyGraph_3_5_Church13
x1
x3
=
λ x5 x6 .
x6
)
⟶
(
TwoRamseyGraph_3_5_Church13
x2
x3
=
λ x5 x6 .
x6
)
⟶
False
(proof)
Known
b9bfd..
:
∀ x0 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church13_p
x0
⟶
∀ x1 : ο .
(
∀ x2 x3 :
(
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
(
∀ x4 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church13_p
x4
⟶
Church13_p
(
x2
x4
)
)
⟶
(
∀ x4 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church13_p
x4
⟶
Church13_p
(
x3
x4
)
)
⟶
(
∀ x4 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
x2
(
x3
x4
)
=
x4
)
⟶
(
∀ x4 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
x3
(
x2
x4
)
=
x4
)
⟶
(
∀ x4 x5 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church13_p
x4
⟶
Church13_p
x5
⟶
TwoRamseyGraph_3_5_Church13
x4
x5
=
TwoRamseyGraph_3_5_Church13
(
x2
x4
)
(
x2
x5
)
)
⟶
(
x2
x0
=
λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x5
)
⟶
x1
)
⟶
x1
Theorem
4a8a6..
:
∀ x0 x1 x2 x3 x4 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church13_p
x0
⟶
Church13_p
x1
⟶
Church13_p
x2
⟶
Church13_p
x3
⟶
Church13_p
x4
⟶
(
x0
=
x1
⟶
∀ x5 : ο .
x5
)
⟶
(
x0
=
x2
⟶
∀ x5 : ο .
x5
)
⟶
(
x0
=
x3
⟶
∀ x5 : ο .
x5
)
⟶
(
x0
=
x4
⟶
∀ x5 : ο .
x5
)
⟶
(
x1
=
x2
⟶
∀ x5 : ο .
x5
)
⟶
(
x1
=
x3
⟶
∀ x5 : ο .
x5
)
⟶
(
x1
=
x4
⟶
∀ x5 : ο .
x5
)
⟶
(
x2
=
x3
⟶
∀ x5 : ο .
x5
)
⟶
(
x2
=
x4
⟶
∀ x5 : ο .
x5
)
⟶
(
x3
=
x4
⟶
∀ x5 : ο .
x5
)
⟶
(
TwoRamseyGraph_3_5_Church13
x0
x1
=
λ x6 x7 .
x7
)
⟶
(
TwoRamseyGraph_3_5_Church13
x0
x2
=
λ x6 x7 .
x7
)
⟶
(
TwoRamseyGraph_3_5_Church13
x0
x3
=
λ x6 x7 .
x7
)
⟶
(
TwoRamseyGraph_3_5_Church13
x0
x4
=
λ x6 x7 .
x7
)
⟶
(
TwoRamseyGraph_3_5_Church13
x1
x2
=
λ x6 x7 .
x7
)
⟶
(
TwoRamseyGraph_3_5_Church13
x1
x3
=
λ x6 x7 .
x7
)
⟶
(
TwoRamseyGraph_3_5_Church13
x1
x4
=
λ x6 x7 .
x7
)
⟶
(
TwoRamseyGraph_3_5_Church13
x2
x3
=
λ x6 x7 .
x7
)
⟶
(
TwoRamseyGraph_3_5_Church13
x2
x4
=
λ x6 x7 .
x7
)
⟶
(
TwoRamseyGraph_3_5_Church13
x3
x4
=
λ x6 x7 .
x7
)
⟶
False
(proof)
Param
or
or
:
ο
→
ο
→
ο
Known
orIR
orIR
:
∀ x0 x1 : ο .
x1
⟶
or
x0
x1
Known
orIL
orIL
:
∀ x0 x1 : ο .
x0
⟶
or
x0
x1
Theorem
cd49f..
:
∀ x0 x1 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church13_p
x0
⟶
Church13_p
x1
⟶
or
(
TwoRamseyGraph_3_5_Church13
x0
x1
=
λ x3 x4 .
x3
)
(
TwoRamseyGraph_3_5_Church13
x0
x1
=
λ x3 x4 .
x4
)
(proof)
Param
u1
:
ι
Param
u2
:
ι
Param
u3
:
ι
Param
u4
:
ι
Param
u5
:
ι
Param
u6
:
ι
Param
u7
:
ι
Param
u8
:
ι
Param
u9
:
ι
Param
u10
:
ι
Param
u11
:
ι
Param
u12
:
ι
Known
neq_1_0
neq_1_0
:
u1
=
0
⟶
∀ x0 : ο .
x0
Known
neq_2_0
neq_2_0
:
u2
=
0
⟶
∀ x0 : ο .
x0
Known
neq_3_0
neq_3_0
:
u3
=
0
⟶
∀ x0 : ο .
x0
Known
neq_4_0
neq_4_0
:
u4
=
0
⟶
∀ x0 : ο .
x0
Known
neq_5_0
neq_5_0
:
u5
=
0
⟶
∀ x0 : ο .
x0
Known
neq_6_0
neq_6_0
:
u6
=
0
⟶
∀ x0 : ο .
x0
Known
neq_7_0
neq_7_0
:
u7
=
0
⟶
∀ x0 : ο .
x0
Known
neq_8_0
neq_8_0
:
u8
=
0
⟶
∀ x0 : ο .
x0
Known
neq_9_0
neq_9_0
:
u9
=
0
⟶
∀ x0 : ο .
x0
Known
0e10e..
:
u10
=
0
⟶
∀ x0 : ο .
x0
Known
19f75..
:
u11
=
0
⟶
∀ x0 : ο .
x0
Known
efdfc..
:
u12
=
0
⟶
∀ x0 : ο .
x0
Known
neq_2_1
neq_2_1
:
u2
=
u1
⟶
∀ x0 : ο .
x0
Known
neq_3_1
neq_3_1
:
u3
=
u1
⟶
∀ x0 : ο .
x0
Known
neq_4_1
neq_4_1
:
u4
=
u1
⟶
∀ x0 : ο .
x0
Known
neq_5_1
neq_5_1
:
u5
=
u1
⟶
∀ x0 : ο .
x0
Known
neq_6_1
neq_6_1
:
u6
=
u1
⟶
∀ x0 : ο .
x0
Known
neq_7_1
neq_7_1
:
u7
=
u1
⟶
∀ x0 : ο .
x0
Known
neq_8_1
neq_8_1
:
u8
=
u1
⟶
∀ x0 : ο .
x0
Known
neq_9_1
neq_9_1
:
u9
=
u1
⟶
∀ x0 : ο .
x0
Known
d183f..
:
u10
=
u1
⟶
∀ x0 : ο .
x0
Known
618f7..
:
u11
=
u1
⟶
∀ x0 : ο .
x0
Known
ce0cd..
:
u12
=
u1
⟶
∀ x0 : ο .
x0
Known
neq_3_2
neq_3_2
:
u3
=
u2
⟶
∀ x0 : ο .
x0
Known
neq_4_2
neq_4_2
:
u4
=
u2
⟶
∀ x0 : ο .
x0
Known
neq_5_2
neq_5_2
:
u5
=
u2
⟶
∀ x0 : ο .
x0
Known
neq_6_2
neq_6_2
:
u6
=
u2
⟶
∀ x0 : ο .
x0
Known
neq_7_2
neq_7_2
:
u7
=
u2
⟶
∀ x0 : ο .
x0
Known
neq_8_2
neq_8_2
:
u8
=
u2
⟶
∀ x0 : ο .
x0
Known
neq_9_2
neq_9_2
:
u9
=
u2
⟶
∀ x0 : ο .
x0
Known
e02d9..
:
u10
=
u2
⟶
∀ x0 : ο .
x0
Known
2c42c..
:
u11
=
u2
⟶
∀ x0 : ο .
x0
Known
8158b..
:
u12
=
u2
⟶
∀ x0 : ο .
x0
Known
neq_4_3
neq_4_3
:
u4
=
u3
⟶
∀ x0 : ο .
x0
Known
neq_5_3
neq_5_3
:
u5
=
u3
⟶
∀ x0 : ο .
x0
Known
neq_6_3
neq_6_3
:
u6
=
u3
⟶
∀ x0 : ο .
x0
Known
neq_7_3
neq_7_3
:
u7
=
u3
⟶
∀ x0 : ο .
x0
Known
neq_8_3
neq_8_3
:
u8
=
u3
⟶
∀ x0 : ο .
x0
Known
neq_9_3
neq_9_3
:
u9
=
u3
⟶
∀ x0 : ο .
x0
Known
68152..
:
u10
=
u3
⟶
∀ x0 : ο .
x0
Known
b06e1..
:
u11
=
u3
⟶
∀ x0 : ο .
x0
Known
e015c..
:
u12
=
u3
⟶
∀ x0 : ο .
x0
Known
neq_5_4
neq_5_4
:
u5
=
u4
⟶
∀ x0 : ο .
x0
Known
neq_6_4
neq_6_4
:
u6
=
u4
⟶
∀ x0 : ο .
x0
Known
neq_7_4
neq_7_4
:
u7
=
u4
⟶
∀ x0 : ο .
x0
Known
neq_8_4
neq_8_4
:
u8
=
u4
⟶
∀ x0 : ο .
x0
Known
neq_9_4
neq_9_4
:
u9
=
u4
⟶
∀ x0 : ο .
x0
Known
33d16..
:
u10
=
u4
⟶
∀ x0 : ο .
x0
Known
6a6f1..
:
u11
=
u4
⟶
∀ x0 : ο .
x0
Known
7aa79..
:
u12
=
u4
⟶
∀ x0 : ο .
x0
Known
neq_6_5
neq_6_5
:
u6
=
u5
⟶
∀ x0 : ο .
x0
Known
neq_7_5
neq_7_5
:
u7
=
u5
⟶
∀ x0 : ο .
x0
Known
neq_8_5
neq_8_5
:
u8
=
u5
⟶
∀ x0 : ο .
x0
Known
neq_9_5
neq_9_5
:
u9
=
u5
⟶
∀ x0 : ο .
x0
Known
a7d50..
:
u10
=
u5
⟶
∀ x0 : ο .
x0
Known
1b659..
:
u11
=
u5
⟶
∀ x0 : ο .
x0
Known
07eba..
:
u12
=
u5
⟶
∀ x0 : ο .
x0
Known
neq_7_6
neq_7_6
:
u7
=
u6
⟶
∀ x0 : ο .
x0
Known
neq_8_6
neq_8_6
:
u8
=
u6
⟶
∀ x0 : ο .
x0
Known
neq_9_6
neq_9_6
:
u9
=
u6
⟶
∀ x0 : ο .
x0
Known
d0401..
:
u10
=
u6
⟶
∀ x0 : ο .
x0
Known
949f2..
:
u11
=
u6
⟶
∀ x0 : ο .
x0
Known
0bd83..
:
u12
=
u6
⟶
∀ x0 : ο .
x0
Known
neq_8_7
neq_8_7
:
u8
=
u7
⟶
∀ x0 : ο .
x0
Known
neq_9_7
neq_9_7
:
u9
=
u7
⟶
∀ x0 : ο .
x0
Known
7d7a8..
:
u10
=
u7
⟶
∀ x0 : ο .
x0
Known
4abfa..
:
u11
=
u7
⟶
∀ x0 : ο .
x0
Known
6a15f..
:
u12
=
u7
⟶
∀ x0 : ο .
x0
Known
neq_9_8
neq_9_8
:
u9
=
u8
⟶
∀ x0 : ο .
x0
Known
96175..
:
u10
=
u8
⟶
∀ x0 : ο .
x0
Known
b3a20..
:
u11
=
u8
⟶
∀ x0 : ο .
x0
Known
a6a6c..
:
u12
=
u8
⟶
∀ x0 : ο .
x0
Known
4fc31..
:
u10
=
u9
⟶
∀ x0 : ο .
x0
Known
4f03f..
:
u11
=
u9
⟶
∀ x0 : ο .
x0
Known
22885..
:
u12
=
u9
⟶
∀ x0 : ο .
x0
Known
ebfb7..
:
u11
=
u10
⟶
∀ x0 : ο .
x0
Known
6c583..
:
u12
=
u10
⟶
∀ x0 : ο .
x0
Known
ab306..
:
u12
=
u11
⟶
∀ x0 : ο .
x0
Theorem
d7c49..
:
∀ x0 x1 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
Church13_p
x0
⟶
Church13_p
x1
⟶
x0
0
u1
u2
u3
u4
u5
u6
u7
u8
u9
u10
u11
u12
=
x1
0
u1
u2
u3
u4
u5
u6
u7
u8
u9
u10
u11
u12
⟶
x0
=
x1
(proof)
previous assets