Search for blocks/addresses/...

Proofgold Signed Transaction

vin
Pr3fd../7e5d8..
PUaM9../9e6a6..
vout
Pr3fd../4d14e.. 2,549.88 bars
TMLRo../72de7.. ownership of 9fe18.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMUNZ../f2221.. ownership of 2f9b7.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMbU5../761b6.. ownership of 59f06.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMcu9../2d696.. ownership of 24314.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
Pr4zB../15473.. 800.00 bars
PUeWV../21ee9.. doc published by Pr4zB..
Param ChurchNum_3ary_proj_p : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο
Param ChurchNum_8ary_proj_p : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο
Definition TwoRamseyGraph_4_5_24_ChurchNums_3x8 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x4 . x0 (x1 (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5))) (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5))) (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5))) (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)))) (x1 (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5))) (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5))) (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)))) (x1 (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5))) (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5))) (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5))) (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)))) (λ x5 . x4)
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Param ChurchNums_3x8_eq : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο
Definition ChurchNums_3x8_neq := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . not (ChurchNums_3x8_eq x0 x1 x2 x3)
Known fc1b4.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x1 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x3 x4 x5 : (ι → ι) → ι → ι . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x3) x0 x1 = λ x3 x4 . x3) ⟶ ∀ x2 : ο . ((x0 = λ x4 x5 x6 : (ι → ι) → ι → ι . x4) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) ⟶ x2) ⟶ ((x0 = λ x4 x5 x6 : (ι → ι) → ι → ι . x4) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x5) ⟶ x2) ⟶ ((x0 = λ x4 x5 x6 : (ι → ι) → ι → ι . x4) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x6) ⟶ x2) ⟶ ((x0 = λ x4 x5 x6 : (ι → ι) → ι → ι . x4) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x8) ⟶ x2) ⟶ ((x0 = λ x4 x5 x6 : (ι → ι) → ι → ι . x5) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) ⟶ x2) ⟶ ((x0 = λ x4 x5 x6 : (ι → ι) → ι → ι . x5) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x5) ⟶ x2) ⟶ ((x0 = λ x4 x5 x6 : (ι → ι) → ι → ι . x5) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x11) ⟶ x2) ⟶ ((x0 = λ x4 x5 x6 : (ι → ι) → ι → ι . x6) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) ⟶ x2) ⟶ ((x0 = λ x4 x5 x6 : (ι → ι) → ι → ι . x6) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x8) ⟶ x2) ⟶ ((x0 = λ x4 x5 x6 : (ι → ι) → ι → ι . x6) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x10) ⟶ x2) ⟶ ((x0 = λ x4 x5 x6 : (ι → ι) → ι → ι . x6) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x11) ⟶ x2) ⟶ x2
Known f6916.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x0 = x1 ⟶ x2 = x3 ⟶ ChurchNums_3x8_eq x0 x2 x1 x3
Known fa458.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_8ary_proj_p x3 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5) x0 x2 = λ x5 x6 . x5) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5) x1 x3 = λ x5 x6 . x5) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x6) x0 x2 = λ x5 x6 . x5) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x6) x1 x3 = λ x5 x6 . x5) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = λ x5 x6 . x5) ⟶ ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) x0 x2 ⟶ ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x5) x0 x2 ⟶ ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) x1 x3 ⟶ ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x5) x1 x3 ⟶ ChurchNums_3x8_neq x0 x2 x1 x3 ⟶ False
Known 639c7.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_8ary_proj_p x3 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5) x0 x2 = λ x5 x6 . x5) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5) x1 x3 = λ x5 x6 . x5) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x7) x0 x2 = λ x5 x6 . x5) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x7) x1 x3 = λ x5 x6 . x5) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = λ x5 x6 . x5) ⟶ ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) x0 x2 ⟶ ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x6) x0 x2 ⟶ ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) x1 x3 ⟶ ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x6) x1 x3 ⟶ ChurchNums_3x8_neq x0 x2 x1 x3 ⟶ False
Known FalseEFalseE : False ⟶ ∀ x0 : ο . x0
Known 99ba2.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_8ary_proj_p x3 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5) x0 x2 = λ x5 x6 . x5) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5) x1 x3 = λ x5 x6 . x5) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x5 x6 x7 : (ι → ι) → ι → ι . x6) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5) x0 x2 = λ x5 x6 . x5) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x5 x6 x7 : (ι → ι) → ι → ι . x6) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5) x1 x3 = λ x5 x6 . x5) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = λ x5 x6 . x5) ⟶ ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) x0 x2 ⟶ ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι) → ι → ι . x5) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) x0 x2 ⟶ ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) x1 x3 ⟶ ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι) → ι → ι . x5) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) x1 x3 ⟶ ChurchNums_3x8_neq x0 x2 x1 x3 ⟶ False
Definition ChurchNums_8_perm_0_7_6_5_4_3_2_1 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι) → ι → ι . x0 x1 x8 x7 x6 x5 x4 x3 x2
Definition ChurchNums_3x8_3_lt1_swap_1_2_ge1_rot2 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x2 x3 x4 : (ι → ι) → ι → ι . x0 (x1 x2 x4 x4 x4 x4 x4 x4 x4) (x1 x4 x3 x3 x3 x3 x3 x3 x3) (x1 x3 x2 x2 x2 x2 x2 x2 x2)
Known 424ab.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p (ChurchNums_3x8_3_lt1_swap_1_2_ge1_rot2 x0 x1)
Known 6bdd9.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p (ChurchNums_8_perm_0_7_6_5_4_3_2_1 x0)
Known 33bbb.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_8ary_proj_p x3 ⟶ TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = TwoRamseyGraph_4_5_24_ChurchNums_3x8 (ChurchNums_3x8_3_lt1_swap_1_2_ge1_rot2 x0 x2) (ChurchNums_8_perm_0_7_6_5_4_3_2_1 x2) (ChurchNums_3x8_3_lt1_swap_1_2_ge1_rot2 x1 x3) (ChurchNums_8_perm_0_7_6_5_4_3_2_1 x3)
Known cef55.. : ChurchNum_3ary_proj_p (λ x0 x1 x2 : (ι → ι) → ι → ι . x0)
Known 208f3.. : ChurchNum_8ary_proj_p (λ x0 x1 x2 x3 x4 x5 x6 x7 : (ι → ι) → ι → ι . x0)
Known a5963.. : ChurchNum_3ary_proj_p (λ x0 x1 x2 : (ι → ι) → ι → ι . x2)
Known 080b7.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_8ary_proj_p x3 ⟶ ChurchNums_3x8_eq (ChurchNums_3x8_3_lt1_swap_1_2_ge1_rot2 x0 x2) (ChurchNums_8_perm_0_7_6_5_4_3_2_1 x2) (ChurchNums_3x8_3_lt1_swap_1_2_ge1_rot2 x1 x3) (ChurchNums_8_perm_0_7_6_5_4_3_2_1 x3) ⟶ ChurchNums_3x8_eq x0 x2 x1 x3
Known 94187.. : ChurchNum_8ary_proj_p (λ x0 x1 x2 x3 x4 x5 x6 x7 : (ι → ι) → ι → ι . x6)
Known 7734d.. : ChurchNum_8ary_proj_p (λ x0 x1 x2 x3 x4 x5 x6 x7 : (ι → ι) → ι → ι . x7)
Theorem 59f06.. : ∀ x0 x1 x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x3 x4 x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p x2 ⟶ ChurchNum_8ary_proj_p x3 ⟶ ChurchNum_8ary_proj_p x4 ⟶ ChurchNum_8ary_proj_p x5 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x7 x8 x9 : (ι → ι) → ι → ι . x7) (λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x7) x0 x3 = λ x7 x8 . x7) ⟶ not (∀ x6 : ο . ((x0 = λ x8 x9 x10 : (ι → ι) → ι → ι . x8) ⟶ (x3 = λ x8 x9 x10 x11 x12 x13 x14 x15 : (ι → ι) → ι → ι . x12) ⟶ x6) ⟶ ((x0 = λ x8 x9 x10 : (ι → ι) → ι → ι . x9) ⟶ (x3 = λ x8 x9 x10 x11 x12 x13 x14 x15 : (ι → ι) → ι → ι . x9) ⟶ x6) ⟶ ((x0 = λ x8 x9 x10 : (ι → ι) → ι → ι . x9) ⟶ (x3 = λ x8 x9 x10 x11 x12 x13 x14 x15 : (ι → ι) → ι → ι . x15) ⟶ x6) ⟶ ((x0 = λ x8 x9 x10 : (ι → ι) → ι → ι . x10) ⟶ (x3 = λ x8 x9 x10 x11 x12 x13 x14 x15 : (ι → ι) → ι → ι . x12) ⟶ x6) ⟶ x6) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x7 x8 x9 : (ι → ι) → ι → ι . x7) (λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x7) x1 x4 = λ x7 x8 . x7) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x7 x8 x9 : (ι → ι) → ι → ι . x7) (λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x7) x2 x5 = λ x7 x8 . x7) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x3 x1 x4 = λ x7 x8 . x7) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x3 x2 x5 = λ x7 x8 . x7) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x4 x2 x5 = λ x7 x8 . x7) ⟶ ChurchNums_3x8_neq (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x0 x3 ⟶ ChurchNums_3x8_neq (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x1 x4 ⟶ ChurchNums_3x8_neq (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x2 x5 ⟶ ChurchNums_3x8_neq x0 x3 x1 x4 ⟶ ChurchNums_3x8_neq x0 x3 x2 x5 ⟶ ChurchNums_3x8_neq x1 x4 x2 x5 ⟶ False (proof)
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Known a5d1b.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (∀ x4 : ο . ((x0 = λ x6 x7 x8 : (ι → ι) → ι → ι . x6) ⟶ (x2 = λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x10) ⟶ x4) ⟶ ((x0 = λ x6 x7 x8 : (ι → ι) → ι → ι . x7) ⟶ (x2 = λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x7) ⟶ x4) ⟶ ((x0 = λ x6 x7 x8 : (ι → ι) → ι → ι . x7) ⟶ (x2 = λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x13) ⟶ x4) ⟶ ((x0 = λ x6 x7 x8 : (ι → ι) → ι → ι . x8) ⟶ (x2 = λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x10) ⟶ x4) ⟶ x4) ⟶ (∀ x4 : ο . ((x1 = λ x6 x7 x8 : (ι → ι) → ι → ι . x6) ⟶ (x3 = λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x10) ⟶ x4) ⟶ ((x1 = λ x6 x7 x8 : (ι → ι) → ι → ι . x7) ⟶ (x3 = λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x7) ⟶ x4) ⟶ ((x1 = λ x6 x7 x8 : (ι → ι) → ι → ι . x7) ⟶ (x3 = λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x13) ⟶ x4) ⟶ ((x1 = λ x6 x7 x8 : (ι → ι) → ι → ι . x8) ⟶ (x3 = λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x10) ⟶ x4) ⟶ x4) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x9) x0 x2 = λ x5 x6 . x5) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x9) x1 x3 = λ x5 x6 . x5) ⟶ ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x8) x0 x2 ⟶ ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x8) x1 x3 ⟶ ChurchNums_3x8_neq x0 x2 x1 x3 ⟶ False
Known bfc1e.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_3x8_neq x0 x2 x1 x3 ⟶ ChurchNums_3x8_neq x1 x3 x0 x2
Known f60cd.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_8ary_proj_p x3 ⟶ TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x3 x0 x2
Known 3a83b.. : ChurchNum_8ary_proj_p (λ x0 x1 x2 x3 x4 x5 x6 x7 : (ι → ι) → ι → ι . x4)
Known 768c1.. : ((λ x1 x2 . x2) = λ x1 x2 . x1) ⟶ ∀ x0 : ο . x0
Theorem 9fe18.. : ∀ x0 x1 x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x3 x4 x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p x2 ⟶ ChurchNum_8ary_proj_p x3 ⟶ ChurchNum_8ary_proj_p x4 ⟶ ChurchNum_8ary_proj_p x5 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x7 x8 x9 : (ι → ι) → ι → ι . x7) (λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x7) x0 x3 = λ x7 x8 . x7) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x7 x8 x9 : (ι → ι) → ι → ι . x7) (λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x7) x1 x4 = λ x7 x8 . x7) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x7 x8 x9 : (ι → ι) → ι → ι . x7) (λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x7) x2 x5 = λ x7 x8 . x7) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x3 x1 x4 = λ x7 x8 . x7) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x3 x2 x5 = λ x7 x8 . x7) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x4 x2 x5 = λ x7 x8 . x7) ⟶ ChurchNums_3x8_neq (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x0 x3 ⟶ ChurchNums_3x8_neq (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x1 x4 ⟶ ChurchNums_3x8_neq (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x2 x5 ⟶ ChurchNums_3x8_neq x0 x3 x1 x4 ⟶ ChurchNums_3x8_neq x0 x3 x2 x5 ⟶ ChurchNums_3x8_neq x1 x4 x2 x5 ⟶ False (proof)