Search for blocks/addresses/...

Proofgold Signed Transaction

vin
Pr5Hs../f1883..
PUfe3../aece0..
vout
Pr5Hs../2168a.. 9,370.74 bars
TMQUy../66e29.. ownership of 51a60.. as prop with payaddr PrDaH.. rightscost 800.00 controlledby Pr4zB.. upto 0
TMMJD../375c2.. ownership of 04e88.. as prop with payaddr PrDaH.. rightscost 800.00 controlledby Pr4zB.. upto 0
TML3k../361a3.. ownership of aa35a.. as prop with payaddr PrDaH.. rightscost 800.00 controlledby Pr4zB.. upto 0
TMcpr../42501.. ownership of fc1c5.. as prop with payaddr PrDaH.. rightscost 800.00 controlledby Pr4zB.. upto 0
TMGJ3../61ea6.. ownership of 3c996.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMZD6../2aeb8.. ownership of c8b48.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMPoc../5915a.. ownership of 6fa76.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMS62../e05bf.. ownership of fdd7f.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
Pr4zB../e672a.. 800.00 bars
PUKW4../07554.. doc published by Pr4zB..
Definition ChurchNum_8ary_proj_p := λ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : (((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι) → ο . x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι)ι → ι . x2)x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι)ι → ι . x3)x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι)ι → ι . x4)x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι)ι → ι . x5)x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι)ι → ι . x6)x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι)ι → ι . x7)x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι)ι → ι . x8)x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι)ι → ι . x9)x1 x0
Param ChurchNum_3ary_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 ChurchNums_8_perm_1_2_3_4_5_6_7_0 := λ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι)ι → ι . x0 x2 x3 x4 x5 x6 x7 x8 x1
Definition ChurchNums_8_perm_7_0_1_2_3_4_5_6 := λ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι)ι → ι . x0 x8 x1 x2 x3 x4 x5 x6 x7
Param ChurchNums_8x3_lt1_id_ge1_rot1 : (((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → (((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)
Param ChurchNums_8x3_lt1_id_ge1_rot2 : (((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → (((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)
Known b0f0d.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_3ary_proj_p (ChurchNums_8x3_lt1_id_ge1_rot2 x0 x1)
Known 0bfaf.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_3ary_proj_p (ChurchNums_8x3_lt1_id_ge1_rot1 x0 x1)
Known c2824.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNums_8x3_lt1_id_ge1_rot2 x0 (ChurchNums_8x3_lt1_id_ge1_rot1 x0 x1) = x1
Known b782a.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNums_8x3_lt1_id_ge1_rot1 x0 (ChurchNums_8x3_lt1_id_ge1_rot2 x0 x1) = x1
Known e1672.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0ChurchNum_8ary_proj_p (ChurchNums_8_perm_7_0_1_2_3_4_5_6 x0)
Known 4ac5f.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0ChurchNum_8ary_proj_p (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x0)
Known 06461.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNums_8_perm_7_0_1_2_3_4_5_6 (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x0) = x0
Known accc4.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNums_8_perm_1_2_3_4_5_6_7_0 (ChurchNums_8_perm_7_0_1_2_3_4_5_6 x0) = x0
Known 71c84.. : ∀ x0 x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x2 x3 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_8ary_proj_p x2ChurchNum_8ary_proj_p x3TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = TwoRamseyGraph_4_5_24_ChurchNums_3x8 (ChurchNums_8x3_lt1_id_ge1_rot2 x2 x0) (ChurchNums_8_perm_7_0_1_2_3_4_5_6 x2) (ChurchNums_8x3_lt1_id_ge1_rot2 x3 x1) (ChurchNums_8_perm_7_0_1_2_3_4_5_6 x3)
Definition ChurchNums_8_perm_2_3_4_5_6_7_0_1 := λ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι)ι → ι . x0 x3 x4 x5 x6 x7 x8 x1 x2
Definition ChurchNums_8_perm_6_7_0_1_2_3_4_5 := λ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι)ι → ι . x0 x7 x8 x1 x2 x3 x4 x5 x6
Param ChurchNums_8x3_lt2_id_ge2_rot1 : (((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → (((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)
Param ChurchNums_8x3_lt2_id_ge2_rot2 : (((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → (((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)
Known 16e4b.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_3ary_proj_p (ChurchNums_8x3_lt2_id_ge2_rot2 x0 x1)
Known 1d5ae.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_3ary_proj_p (ChurchNums_8x3_lt2_id_ge2_rot1 x0 x1)
Known 0e9d3.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNums_8x3_lt2_id_ge2_rot2 x0 (ChurchNums_8x3_lt2_id_ge2_rot1 x0 x1) = x1
Known 53c9b.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNums_8x3_lt2_id_ge2_rot1 x0 (ChurchNums_8x3_lt2_id_ge2_rot2 x0 x1) = x1
Known a5ec6.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0ChurchNum_8ary_proj_p (ChurchNums_8_perm_6_7_0_1_2_3_4_5 x0)
Known c5de4.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0ChurchNum_8ary_proj_p (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x0)
Known abce4.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNums_8_perm_6_7_0_1_2_3_4_5 (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x0) = x0
Known 13c67.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNums_8_perm_2_3_4_5_6_7_0_1 (ChurchNums_8_perm_6_7_0_1_2_3_4_5 x0) = x0
Known a486a.. : ∀ x0 x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x2 x3 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_8ary_proj_p x2ChurchNum_8ary_proj_p x3TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = TwoRamseyGraph_4_5_24_ChurchNums_3x8 (ChurchNums_8x3_lt2_id_ge2_rot2 x2 x0) (ChurchNums_8_perm_6_7_0_1_2_3_4_5 x2) (ChurchNums_8x3_lt2_id_ge2_rot2 x3 x1) (ChurchNums_8_perm_6_7_0_1_2_3_4_5 x3)
Definition ChurchNums_8_perm_3_4_5_6_7_0_1_2 := λ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι)ι → ι . x0 x4 x5 x6 x7 x8 x1 x2 x3
Definition ChurchNums_8_perm_5_6_7_0_1_2_3_4 := λ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι)ι → ι . x0 x6 x7 x8 x1 x2 x3 x4 x5
Param ChurchNums_8x3_lt3_id_ge3_rot1 : (((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → (((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)
Param ChurchNums_8x3_to_3_lt3_id_ge3_rot2 : (((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → (((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)
Known ec90a.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_3ary_proj_p (ChurchNums_8x3_to_3_lt3_id_ge3_rot2 x0 x1)
Known f7f04.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_3ary_proj_p (ChurchNums_8x3_lt3_id_ge3_rot1 x0 x1)
Known 92519.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNums_8x3_to_3_lt3_id_ge3_rot2 x0 (ChurchNums_8x3_lt3_id_ge3_rot1 x0 x1) = x1
Known 28253.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNums_8x3_lt3_id_ge3_rot1 x0 (ChurchNums_8x3_to_3_lt3_id_ge3_rot2 x0 x1) = x1
Known eed30.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0ChurchNum_8ary_proj_p (ChurchNums_8_perm_5_6_7_0_1_2_3_4 x0)
Known eaaf4.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0ChurchNum_8ary_proj_p (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x0)
Known 44285.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNums_8_perm_5_6_7_0_1_2_3_4 (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x0) = x0
Known d720a.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNums_8_perm_3_4_5_6_7_0_1_2 (ChurchNums_8_perm_5_6_7_0_1_2_3_4 x0) = x0
Known 693c5.. : ∀ x0 x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x2 x3 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_8ary_proj_p x2ChurchNum_8ary_proj_p x3TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = TwoRamseyGraph_4_5_24_ChurchNums_3x8 (ChurchNums_8x3_to_3_lt3_id_ge3_rot2 x2 x0) (ChurchNums_8_perm_5_6_7_0_1_2_3_4 x2) (ChurchNums_8x3_to_3_lt3_id_ge3_rot2 x3 x1) (ChurchNums_8_perm_5_6_7_0_1_2_3_4 x3)
Definition ChurchNums_8_perm_4_5_6_7_0_1_2_3 := λ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι)ι → ι . x0 x5 x6 x7 x8 x1 x2 x3 x4
Param ChurchNums_8x3_lt4_id_ge4_rot1 : (((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → (((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)
Param ChurchNums_8x3_to_3_lt4_id_ge4_rot2 : (((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → (((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)
Known 24233.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_3ary_proj_p (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x0 x1)
Known b68fb.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_3ary_proj_p (ChurchNums_8x3_lt4_id_ge4_rot1 x0 x1)
Known ad374.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x0 (ChurchNums_8x3_lt4_id_ge4_rot1 x0 x1) = x1
Known 49e33.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNums_8x3_lt4_id_ge4_rot1 x0 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x0 x1) = x1
Known dac10.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0ChurchNum_8ary_proj_p (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x0)
Known 5a925.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNums_8_perm_4_5_6_7_0_1_2_3 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x0) = x0
Known 1bd40.. : ∀ x0 x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x2 x3 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_8ary_proj_p x2ChurchNum_8ary_proj_p x3TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = TwoRamseyGraph_4_5_24_ChurchNums_3x8 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x2 x0) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x2) (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x3 x1) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x3)
Param ChurchNums_8x3_lt5_id_ge5_rot1 : (((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → (((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)
Param ChurchNums_8x3_to_3_lt5_id_ge5_rot2 : (((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → (((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)
Known 7b754.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_3ary_proj_p (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x0 x1)
Known a776d.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_3ary_proj_p (ChurchNums_8x3_lt5_id_ge5_rot1 x0 x1)
Known a48ad.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x0 (ChurchNums_8x3_lt5_id_ge5_rot1 x0 x1) = x1
Known b1cc9.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNums_8x3_lt5_id_ge5_rot1 x0 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x0 x1) = x1
Known 84d56.. : ∀ x0 x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x2 x3 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_8ary_proj_p x2ChurchNum_8ary_proj_p x3TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = TwoRamseyGraph_4_5_24_ChurchNums_3x8 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x2 x0) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x2) (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x3 x1) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x3)
Param ChurchNums_8x3_lt6_id_ge6_rot1 : (((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → (((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)
Param ChurchNums_8x3_to_3_lt6_id_ge6_rot2 : (((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → (((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)
Known 2f553.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_3ary_proj_p (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x0 x1)
Known 6c736.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_3ary_proj_p (ChurchNums_8x3_lt6_id_ge6_rot1 x0 x1)
Known fa851.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x0 (ChurchNums_8x3_lt6_id_ge6_rot1 x0 x1) = x1
Known 8922d.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNums_8x3_lt6_id_ge6_rot1 x0 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x0 x1) = x1
Known 1928f.. : ∀ x0 x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x2 x3 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_8ary_proj_p x2ChurchNum_8ary_proj_p x3TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = TwoRamseyGraph_4_5_24_ChurchNums_3x8 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x2 x0) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x2) (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x3 x1) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x3)
Param ChurchNums_8x3_lt7_id_ge7_rot1 : (((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → (((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)
Param ChurchNums_8x3_to_3_lt7_id_ge7_rot2 : (((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → (((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)) → ((ιι) → ιι) → ((ιι) → ιι) → CN (ιι)
Known 1aa1c.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_3ary_proj_p (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x0 x1)
Known f8e90.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_3ary_proj_p (ChurchNums_8x3_lt7_id_ge7_rot1 x0 x1)
Known dfbcd.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x0 (ChurchNums_8x3_lt7_id_ge7_rot1 x0 x1) = x1
Known e57bb.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNums_8x3_lt7_id_ge7_rot1 x0 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x0 x1) = x1
Known eb832.. : ∀ x0 x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x2 x3 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_8ary_proj_p x2ChurchNum_8ary_proj_p x3TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = TwoRamseyGraph_4_5_24_ChurchNums_3x8 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x2 x0) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x2) (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x3 x1) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x3)
Theorem 6fa76.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x1∀ x2 : ο . (∀ x3 x4 : (((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι)(((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x5 x6 : (((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . (∀ x7 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x8 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x7ChurchNum_8ary_proj_p x8ChurchNum_3ary_proj_p (x3 x8 x7))(∀ x7 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x8 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x7ChurchNum_8ary_proj_p x8ChurchNum_3ary_proj_p (x4 x8 x7))(∀ x7 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x8 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x8x3 x8 (x4 x8 x7) = x7)(∀ x7 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x8 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x8x4 x8 (x3 x8 x7) = x7)(∀ x7 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x7ChurchNum_8ary_proj_p (x5 x7))(∀ x7 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x7ChurchNum_8ary_proj_p (x6 x7))(∀ x7 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . x5 (x6 x7) = x7)(∀ x7 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . x6 (x5 x7) = x7)(∀ x7 x8 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x9 x10 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x7ChurchNum_3ary_proj_p x8ChurchNum_8ary_proj_p x9ChurchNum_8ary_proj_p x10TwoRamseyGraph_4_5_24_ChurchNums_3x8 x7 x9 x8 x10 = TwoRamseyGraph_4_5_24_ChurchNums_3x8 (x3 x9 x7) (x5 x9) (x3 x10 x8) (x5 x10))(x5 x1 = λ x8 x9 x10 x11 x12 x13 x14 x15 : (ι → ι)ι → ι . x8)x2)x2 (proof)
Known dca1b.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0∀ x1 : ο . (∀ x2 x3 : (((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . (∀ x4 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x4ChurchNum_3ary_proj_p (x2 x4))(∀ x4 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x4ChurchNum_3ary_proj_p (x3 x4))(∀ x4 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . x2 (x3 x4) = x4)(∀ x4 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . x3 (x2 x4) = x4)(∀ x4 x5 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x6 x7 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . TwoRamseyGraph_4_5_24_ChurchNums_3x8 x4 x6 x5 x7 = TwoRamseyGraph_4_5_24_ChurchNums_3x8 (x2 x4) x6 (x2 x5) x7)(x2 x0 = λ x5 x6 x7 : (ι → ι)ι → ι . x5)x1)x1
Theorem 3c996.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_8ary_proj_p x1∀ x2 : ο . (∀ x3 x4 : (((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι)(((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x5 x6 : (((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . (∀ x7 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x8 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x7ChurchNum_8ary_proj_p x8ChurchNum_3ary_proj_p (x3 x8 x7))(∀ x7 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x8 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x7ChurchNum_8ary_proj_p x8ChurchNum_3ary_proj_p (x4 x8 x7))(∀ x7 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x8 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x8x3 x8 (x4 x8 x7) = x7)(∀ x7 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x8 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x8x4 x8 (x3 x8 x7) = x7)(∀ x7 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x7ChurchNum_8ary_proj_p (x5 x7))(∀ x7 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x7ChurchNum_8ary_proj_p (x6 x7))(∀ x7 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . x5 (x6 x7) = x7)(∀ x7 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . x6 (x5 x7) = x7)(∀ x7 x8 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x9 x10 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x7ChurchNum_3ary_proj_p x8ChurchNum_8ary_proj_p x9ChurchNum_8ary_proj_p x10TwoRamseyGraph_4_5_24_ChurchNums_3x8 x7 x9 x8 x10 = TwoRamseyGraph_4_5_24_ChurchNums_3x8 (x3 x9 x7) (x5 x9) (x3 x10 x8) (x5 x10))(x3 x1 x0 = λ x8 x9 x10 : (ι → ι)ι → ι . x8)(x5 x1 = λ x8 x9 x10 x11 x12 x13 x14 x15 : (ι → ι)ι → ι . x8)x2)x2 (proof)
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Definition ChurchNums_3x8_eq := λ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x2 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x3 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . and (x0 = x2) (x1 = x3)
Definition ChurchNums_3x8_neq := λ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x2 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x3 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . not (ChurchNums_3x8_eq x0 x1 x2 x3)
Known fc1b4.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_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 = x1x2 = x3ChurchNums_3x8_eq x0 x2 x1 x3
Known fa458.. : ∀ x0 x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x2 x3 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_8ary_proj_p x2ChurchNum_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 x2ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι)ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x5) x0 x2ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι)ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x4) x1 x3ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι)ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x5) x1 x3ChurchNums_3x8_neq x0 x2 x1 x3False
Known 639c7.. : ∀ x0 x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x2 x3 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_8ary_proj_p x2ChurchNum_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 x2ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι)ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x6) x0 x2ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι)ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x4) x1 x3ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι)ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x6) x1 x3ChurchNums_3x8_neq x0 x2 x1 x3False
Known FalseEFalseE : False∀ x0 : ο . x0
Known 99ba2.. : ∀ x0 x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x2 x3 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_8ary_proj_p x2ChurchNum_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 x2ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι)ι → ι . x5) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x4) x0 x2ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι)ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x4) x1 x3ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι)ι → ι . x5) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x4) x1 x3ChurchNums_3x8_neq x0 x2 x1 x3False
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 x0ChurchNum_8ary_proj_p x1ChurchNum_3ary_proj_p (ChurchNums_3x8_3_lt1_swap_1_2_ge1_rot2 x0 x1)
Known 6bdd9.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0ChurchNum_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 x0ChurchNum_3ary_proj_p x1ChurchNum_8ary_proj_p x2ChurchNum_8ary_proj_p x3TwoRamseyGraph_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 x2ChurchNum_8ary_proj_p x3ChurchNums_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 x0ChurchNum_3ary_proj_p x1ChurchNum_3ary_proj_p x2ChurchNum_8ary_proj_p x3ChurchNum_8ary_proj_p x4ChurchNum_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 x3ChurchNums_3x8_neq (λ x6 x7 x8 : (ι → ι)ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι)ι → ι . x6) x1 x4ChurchNums_3x8_neq (λ x6 x7 x8 : (ι → ι)ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι)ι → ι . x6) x2 x5ChurchNums_3x8_neq x0 x3 x1 x4ChurchNums_3x8_neq x0 x3 x2 x5ChurchNums_3x8_neq x1 x4 x2 x5False (proof)
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)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 x2ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι)ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι)ι → ι . x8) x1 x3ChurchNums_3x8_neq x0 x2 x1 x3False
Known bfc1e.. : ∀ x0 x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x2 x3 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNums_3x8_neq x0 x2 x1 x3ChurchNums_3x8_neq x1 x3 x0 x2
Known f60cd.. : ∀ x0 x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x2 x3 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_8ary_proj_p x2ChurchNum_8ary_proj_p x3TwoRamseyGraph_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 x0ChurchNum_3ary_proj_p x1ChurchNum_3ary_proj_p x2ChurchNum_8ary_proj_p x3ChurchNum_8ary_proj_p x4ChurchNum_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 x3ChurchNums_3x8_neq (λ x6 x7 x8 : (ι → ι)ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι)ι → ι . x6) x1 x4ChurchNums_3x8_neq (λ x6 x7 x8 : (ι → ι)ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι)ι → ι . x6) x2 x5ChurchNums_3x8_neq x0 x3 x1 x4ChurchNums_3x8_neq x0 x3 x2 x5ChurchNums_3x8_neq x1 x4 x2 x5False (proof)
Theorem aa35a.. : ∀ x0 x1 x2 x3 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x4 x5 x6 x7 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_3ary_proj_p x1ChurchNum_3ary_proj_p x2ChurchNum_3ary_proj_p x3ChurchNum_8ary_proj_p x4ChurchNum_8ary_proj_p x5ChurchNum_8ary_proj_p x6ChurchNum_8ary_proj_p x7(TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x4 x1 x5 = λ x9 x10 . x9)(TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x4 x2 x6 = λ x9 x10 . x9)(TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x4 x3 x7 = λ x9 x10 . x9)(TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x5 x2 x6 = λ x9 x10 . x9)(TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x5 x3 x7 = λ x9 x10 . x9)(TwoRamseyGraph_4_5_24_ChurchNums_3x8 x2 x6 x3 x7 = λ x9 x10 . x9)ChurchNums_3x8_neq x0 x4 x1 x5ChurchNums_3x8_neq x0 x4 x2 x6ChurchNums_3x8_neq x0 x4 x3 x7ChurchNums_3x8_neq x1 x5 x2 x6ChurchNums_3x8_neq x1 x5 x3 x7ChurchNums_3x8_neq x2 x6 x3 x7False (proof)
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Param u24 : ι
Param atleastpatleastp : ιιο
Param u4 : ι
Param ordsuccordsucc : ιι
Definition TwoRamseyGraph_4_5_24 := λ x0 x1 . ∀ x2 x3 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x4 x5 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x2ChurchNum_3ary_proj_p x3ChurchNum_8ary_proj_p x4ChurchNum_8ary_proj_p x5x0 = x2 (λ x7 : ι → ι . λ x8 . x8) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 x8)))))))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 x8)))))))))))))))) ordsucc (x4 (λ x7 : ι → ι . λ x8 . x8) (λ x7 : ι → ι . x7) (λ x7 : ι → ι . λ x8 . x7 (x7 x8)) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 x8))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 x8)))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 x8))))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 x8)))))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 (x7 x8))))))) ordsucc 0)x1 = x3 (λ x7 : ι → ι . λ x8 . x8) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 x8)))))))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 x8)))))))))))))))) ordsucc (x5 (λ x7 : ι → ι . λ x8 . x8) (λ x7 : ι → ι . x7) (λ x7 : ι → ι . λ x8 . x7 (x7 x8)) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 x8))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 x8)))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 x8))))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 x8)))))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 (x7 x8))))))) ordsucc 0)TwoRamseyGraph_4_5_24_ChurchNums_3x8 x2 x4 x3 x5 = λ x7 x8 . x7
Known d03c6.. : ∀ x0 . atleastp u4 x0∀ x1 : ο . (∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0(x2 = x3∀ x6 : ο . x6)(x2 = x4∀ x6 : ο . x6)(x2 = x5∀ x6 : ο . x6)(x3 = x4∀ x6 : ο . x6)(x3 = x5∀ x6 : ο . x6)(x4 = x5∀ x6 : ο . x6)x1)x1
Known 4f390.. : ∀ x0 . x0u24∀ x1 : ο . (∀ x2 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x3 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x2ChurchNum_8ary_proj_p x3x0 = x2 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 x6)))))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 x6)))))))))))))))) ordsucc (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x5 (x5 x6)) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 x6))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 x6)))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 x6))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 x6)))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 x6))))))) ordsucc 0)x1)x1
Theorem 51a60.. : ∀ x0 . x0u24atleastp u4 x0not (∀ x1 . x1x0∀ x2 . x2x0(x1 = x2∀ x3 : ο . x3)TwoRamseyGraph_4_5_24 x1 x2) (proof)