Search for blocks/addresses/...

Proofgold Asset

asset id
97e2fda7e170720968710e7c84da407b827d16d8ff0fc19a1526cc3c3845aa4d
asset hash
7c6d16e2ae93622ee4638e7c5592cc365e3d0fd727932956393174d2d7f0ddb5
bday / block
18750
tx
0ee1b..
preasset
doc published by Pr4zB..
Param ordsuccordsucc : ιι
Definition ChurchNums_3x8_to_u24 := λ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . x0 (x1 (λ x2 : ι → ι . λ x3 . x3) (λ x2 : ι → ι . x2) (λ x2 : ι → ι . λ x3 . x2 (x2 x3)) (λ x2 : ι → ι . λ x3 . x2 (x2 (x2 x3))) (λ x2 : ι → ι . λ x3 . x2 (x2 (x2 (x2 x3)))) (λ x2 : ι → ι . λ x3 . x2 (x2 (x2 (x2 (x2 x3))))) (λ x2 : ι → ι . λ x3 . x2 (x2 (x2 (x2 (x2 (x2 x3)))))) (λ x2 : ι → ι . λ x3 . x2 (x2 (x2 (x2 (x2 (x2 (x2 x3)))))))) (λ x2 : ι → ι . λ x3 . x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x1 (λ x4 : ι → ι . λ x5 . x5) (λ x4 : ι → ι . x4) (λ x4 : ι → ι . λ x5 . x4 (x4 x5)) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 x5))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 x5)))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 (x4 x5))))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 (x4 (x4 x5)))))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 (x4 (x4 (x4 x5))))))) x2 x3))))))))) (λ x2 : ι → ι . λ x3 . x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x1 (λ x4 : ι → ι . λ x5 . x5) (λ x4 : ι → ι . x4) (λ x4 : ι → ι . λ x5 . x4 (x4 x5)) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 x5))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 x5)))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 (x4 x5))))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 (x4 (x4 x5)))))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 (x4 (x4 (x4 x5))))))) x2 x3))))))))))))))))) ordsucc 0
Definition ChurchNum_3ary_proj_p := λ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : (((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι) → ο . x1 (λ x2 x3 x4 : (ι → ι)ι → ι . x2)x1 (λ x2 x3 x4 : (ι → ι)ι → ι . x3)x1 (λ x2 x3 x4 : (ι → ι)ι → ι . x4)x1 x0
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
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
Definition u5 := ordsucc u4
Definition u6 := ordsucc u5
Definition u7 := ordsucc u6
Definition u8 := ordsucc u7
Definition u9 := ordsucc u8
Definition u10 := ordsucc u9
Definition u11 := ordsucc u10
Definition u12 := ordsucc u11
Definition u13 := ordsucc u12
Definition u14 := ordsucc u13
Definition u15 := ordsucc u14
Definition u16 := ordsucc u15
Definition u17 := ordsucc u16
Definition u18 := ordsucc u17
Definition u19 := ordsucc u18
Definition u20 := ordsucc u19
Definition u21 := ordsucc u20
Definition u22 := ordsucc u21
Definition u23 := ordsucc u22
Definition u24 := ordsucc u23
Known 4c607.. : 0u24
Known 610bf.. : u1u24
Known 30da6.. : u2u24
Known 3cb84.. : u3u24
Known 43f74.. : u4u24
Known 8f227.. : u5u24
Known 469db.. : u6u24
Known bb94c.. : u7u24
Known d2f24.. : u8u24
Known fd0d9.. : u9u24
Known df5ed.. : u10u24
Known 05672.. : u11u24
Known 15af9.. : u12u24
Known e6799.. : u13u24
Known 9522d.. : u14u24
Known fc764.. : u15u24
Known 2d7ca.. : u16u24
Known e4fb5.. : u17u24
Known f0252.. : u18u24
Known a4364.. : u19u24
Known 9da85.. : u20u24
Known 3ee80.. : u21u24
Known 9ec16.. : u22u24
Known d7b2c.. : u23u24
Theorem 16d18.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_8ary_proj_p x1ChurchNums_3x8_to_u24 x0 x1u24 (proof)
Definition ChurchNums_8x3_to_3_lt7_id_ge7_rot2 := λ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x2 x3 x4 : (ι → ι)ι → ι . x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x3 x4 x2)
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
Known neq_1_0neq_1_0 : u1 = 0∀ x0 : ο . x0
Known neq_2_1neq_2_1 : u2 = u1∀ x0 : ο . x0
Known neq_3_2neq_3_2 : u3 = u2∀ x0 : ο . x0
Known neq_4_3neq_4_3 : u4 = u3∀ x0 : ο . x0
Known neq_5_4neq_5_4 : u5 = u4∀ x0 : ο . x0
Known neq_6_5neq_6_5 : u6 = u5∀ x0 : ο . x0
Known neq_7_6neq_7_6 : u7 = u6∀ x0 : ο . x0
Known neq_8_7neq_8_7 : u8 = u7∀ x0 : ο . x0
Known neq_9_8neq_9_8 : u9 = u8∀ x0 : ο . x0
Known 4fc31.. : u10 = u9∀ x0 : ο . x0
Known ebfb7.. : u11 = u10∀ x0 : ο . x0
Known ab306.. : u12 = u11∀ x0 : ο . x0
Known ad02f.. : u13 = u12∀ x0 : ο . x0
Known e1947.. : u14 = u13∀ x0 : ο . x0
Known b8e82.. : u15 = u14∀ x0 : ο . x0
Known 41073.. : u16 = u15∀ x0 : ο . x0
Known 7fbc8.. : u17 = u16∀ x0 : ο . x0
Known 82c6a.. : u18 = u17∀ x0 : ο . x0
Known 97eb4.. : u19 = u18∀ x0 : ο . x0
Known 2615b.. : u20 = u19∀ x0 : ο . x0
Known 32e25.. : u21 = u20∀ x0 : ο . x0
Known 41315.. : u22 = u21∀ x0 : ο . x0
Known 3105f.. : u23 = u22∀ x0 : ο . x0
Known neq_i_symneq_i_sym : ∀ x0 x1 . (x0 = x1∀ x2 : ο . x2)x1 = x0∀ x2 : ο . x2
Known c432c.. : u23 = 0∀ x0 : ο . x0
Theorem 8f0b2.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_8ary_proj_p x1ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x1 x0) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x1) = ChurchNums_3x8_to_u24 x0 x1∀ x2 : ο . x2 (proof)
Definition ChurchNums_8x3_to_3_lt6_id_ge6_rot2 := λ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x2 x3 x4 : (ι → ι)ι → ι . x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x3 x4 x2) (x1 x3 x4 x2)
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
Known neq_2_0neq_2_0 : u2 = 0∀ x0 : ο . x0
Known neq_3_1neq_3_1 : u3 = u1∀ x0 : ο . x0
Known neq_4_2neq_4_2 : u4 = u2∀ x0 : ο . x0
Known neq_5_3neq_5_3 : u5 = u3∀ x0 : ο . x0
Known neq_6_4neq_6_4 : u6 = u4∀ x0 : ο . x0
Known neq_7_5neq_7_5 : u7 = u5∀ x0 : ο . x0
Known neq_8_6neq_8_6 : u8 = u6∀ x0 : ο . x0
Known neq_9_7neq_9_7 : u9 = u7∀ x0 : ο . x0
Known 96175.. : u10 = u8∀ x0 : ο . x0
Known 4f03f.. : u11 = u9∀ x0 : ο . x0
Known 6c583.. : u12 = u10∀ x0 : ο . x0
Known bf497.. : u13 = u11∀ x0 : ο . x0
Known ef4da.. : u14 = u12∀ x0 : ο . x0
Known 4d8d4.. : u15 = u13∀ x0 : ο . x0
Known 71c5e.. : u16 = u14∀ x0 : ο . x0
Known ac12b.. : u17 = u15∀ x0 : ο . x0
Known 0eaf4.. : u18 = u16∀ x0 : ο . x0
Known 3c054.. : u19 = u17∀ x0 : ο . x0
Known 75fad.. : u20 = u18∀ x0 : ο . x0
Known 44711.. : u21 = u19∀ x0 : ο . x0
Known c8ac0.. : u22 = u20∀ x0 : ο . x0
Known 1a616.. : u23 = u21∀ x0 : ο . x0
Known e8714.. : u22 = 0∀ x0 : ο . x0
Known 13d86.. : u23 = u1∀ x0 : ο . x0
Theorem 7bf94.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_8ary_proj_p x1ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x1 x0) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x1) = ChurchNums_3x8_to_u24 x0 x1∀ x2 : ο . x2 (proof)
Definition ChurchNums_8x3_to_3_lt5_id_ge5_rot2 := λ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x2 x3 x4 : (ι → ι)ι → ι . x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2)
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
Known neq_3_0neq_3_0 : u3 = 0∀ x0 : ο . x0
Known neq_4_1neq_4_1 : u4 = u1∀ x0 : ο . x0
Known neq_5_2neq_5_2 : u5 = u2∀ x0 : ο . x0
Known neq_6_3neq_6_3 : u6 = u3∀ x0 : ο . x0
Known neq_7_4neq_7_4 : u7 = u4∀ x0 : ο . x0
Known neq_8_5neq_8_5 : u8 = u5∀ x0 : ο . x0
Known neq_9_6neq_9_6 : u9 = u6∀ x0 : ο . x0
Known 7d7a8.. : u10 = u7∀ x0 : ο . x0
Known b3a20.. : u11 = u8∀ x0 : ο . x0
Known 22885.. : u12 = u9∀ x0 : ο . x0
Known 78358.. : u13 = u10∀ x0 : ο . x0
Known 4e1aa.. : u14 = u11∀ x0 : ο . x0
Known 72647.. : u15 = u12∀ x0 : ο . x0
Known 4326e.. : u16 = u13∀ x0 : ο . x0
Known 82608.. : u17 = u14∀ x0 : ο . x0
Known dfba1.. : u18 = u15∀ x0 : ο . x0
Known 0384c.. : u19 = u16∀ x0 : ο . x0
Known 9ce5b.. : u20 = u17∀ x0 : ο . x0
Known 80a82.. : u21 = u18∀ x0 : ο . x0
Known b0147.. : u22 = u19∀ x0 : ο . x0
Known 94779.. : u23 = u20∀ x0 : ο . x0
Known 1158c.. : u21 = 0∀ x0 : ο . x0
Known 9e7b1.. : u22 = u1∀ x0 : ο . x0
Known 60a3a.. : u23 = u2∀ x0 : ο . x0
Theorem a9b55.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_8ary_proj_p x1ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x1 x0) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x1) = ChurchNums_3x8_to_u24 x0 x1∀ x2 : ο . x2 (proof)
Definition ChurchNums_8x3_to_3_lt4_id_ge4_rot2 := λ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . λ x2 x3 x4 : (ι → ι)ι → ι . x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2)
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
Known neq_4_0neq_4_0 : u4 = 0∀ x0 : ο . x0
Known neq_5_1neq_5_1 : u5 = u1∀ x0 : ο . x0
Known neq_6_2neq_6_2 : u6 = u2∀ x0 : ο . x0
Known neq_7_3neq_7_3 : u7 = u3∀ x0 : ο . x0
Known neq_8_4neq_8_4 : u8 = u4∀ x0 : ο . x0
Known neq_9_5neq_9_5 : u9 = u5∀ x0 : ο . x0
Known d0401.. : u10 = u6∀ x0 : ο . x0
Known 4abfa.. : u11 = u7∀ x0 : ο . x0
Known a6a6c.. : u12 = u8∀ x0 : ο . x0
Known 3f24c.. : u13 = u9∀ x0 : ο . x0
Known f5ab5.. : u14 = u10∀ x0 : ο . x0
Known 9c5db.. : u15 = u11∀ x0 : ο . x0
Known fa664.. : u16 = u12∀ x0 : ο . x0
Known 30174.. : u17 = u13∀ x0 : ο . x0
Known d92fd.. : u18 = u14∀ x0 : ο . x0
Known 38ccc.. : u19 = u15∀ x0 : ο . x0
Known 996e8.. : u20 = u16∀ x0 : ο . x0
Known b821e.. : u21 = u17∀ x0 : ο . x0
Known 7957c.. : u22 = u18∀ x0 : ο . x0
Known ad532.. : u23 = u19∀ x0 : ο . x0
Known 4552b.. : u20 = 0∀ x0 : ο . x0
Known db0cd.. : u21 = u1∀ x0 : ο . x0
Known af720.. : u22 = u2∀ x0 : ο . x0
Known 3d5c1.. : u23 = u3∀ x0 : ο . x0
Theorem d6534.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_8ary_proj_p x1ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x1 x0) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x1) = ChurchNums_3x8_to_u24 x0 x1∀ x2 : ο . x2 (proof)
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 4ac5f.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0ChurchNum_8ary_proj_p (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x0)
Theorem 471b2.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_8ary_proj_p x1ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x1 x0) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x1) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x1 x0) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x1)∀ x2 : ο . x2 (proof)
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 c5de4.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0ChurchNum_8ary_proj_p (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x0)
Theorem 373fc.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_8ary_proj_p x1ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x1 x0) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x1) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x1 x0) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x1)∀ x2 : ο . x2 (proof)
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 eaaf4.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_8ary_proj_p x0ChurchNum_8ary_proj_p (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x0)
Theorem 987aa.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_8ary_proj_p x1ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x1 x0) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x1) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x1 x0) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x1)∀ x2 : ο . x2 (proof)
Theorem 08b75.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_8ary_proj_p x1ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x1 x0) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x1) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x1 x0) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x1)∀ x2 : ο . x2 (proof)
Theorem 290ad.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_8ary_proj_p x1ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x1 x0) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x1) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x1 x0) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x1)∀ x2 : ο . x2 (proof)
Theorem 83ebc.. : ∀ x0 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ∀ x1 : ((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)((ι → ι)ι → ι)(ι → ι)ι → ι . ChurchNum_3ary_proj_p x0ChurchNum_8ary_proj_p x1ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x1 x0) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x1) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x1 x0) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x1)∀ x2 : ο . x2 (proof)
Param nat_pnat_p : ιο
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Definition injinj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3x0x2 x3x1) (∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)
Definition atleastpatleastp := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . inj x0 x1 x3x2)x2
Known PigeonHole_natPigeonHole_nat : ∀ x0 . nat_p x0∀ x1 : ι → ι . (∀ x2 . x2ordsucc x0x1 x2x0)not (∀ x2 . x2ordsucc x0∀ x3 . x3ordsucc x0x1 x2 = x1 x3x2 = x3)
Theorem 4fb58..Pigeonhole_not_atleastp_ordsucc : ∀ x0 . nat_p x0not (atleastp (ordsucc x0) x0) (proof)
Definition bijbij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . x3x0x2 x3x1) (∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)) (∀ x3 . x3x1∀ x4 : ο . (∀ x5 . and (x5x0) (x2 x5 = x3)x4)x4)
Definition equipequip := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3x2)x2
Param mul_natmul_nat : ιιι
Param lamSigma : ι(ιι) → ι
Definition setprodsetprod := λ x0 x1 . lam x0 (λ x2 . x1)
Known nat_indnat_ind : ∀ x0 : ι → ο . x0 0(∀ x1 . nat_p x1x0 x1x0 (ordsucc x1))∀ x1 . nat_p x1x0 x1
Known mul_nat_0Rmul_nat_0R : ∀ x0 . mul_nat x0 0 = 0
Known equip_refequip_ref : ∀ x0 . equip x0 x0
Definition nInnIn := λ x0 x1 . not (x0x1)
Known Empty_eqEmpty_eq : ∀ x0 . (∀ x1 . nIn x1 x0)x0 = 0
Param apap : ιιι
Known EmptyEEmptyE : ∀ x0 . nIn x0 0
Known ap1_Sigmaap1_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2lam x0 x1ap x2 1x1 (ap x2 0)
Param add_natadd_nat : ιιι
Known mul_nat_SRmul_nat_SR : ∀ x0 x1 . nat_p x1mul_nat x0 (ordsucc x1) = add_nat x0 (mul_nat x0 x1)
Param setsumsetsum : ιιι
Known equip_traequip_tra : ∀ x0 x1 x2 . equip x0 x1equip x1 x2equip x0 x2
Known c88e0.. : ∀ x0 x1 x2 x3 . nat_p x0nat_p x1equip x0 x2equip x1 x3equip (add_nat x0 x1) (setsum x2 x3)
Known mul_nat_pmul_nat_p : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (mul_nat x0 x1)
Param combine_funcscombine_funcs : ιι(ιι) → (ιι) → ιι
Param If_iIf_i : οιιι
Param Inj0Inj0 : ιι
Param Inj1Inj1 : ιι
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Known and3Iand3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Known f4c7c.. : ∀ x0 x1 . ∀ x2 : ι → ο . (∀ x3 . x3x0x2 (Inj0 x3))(∀ x3 . x3x1x2 (Inj1 x3))∀ x3 . x3setsum x0 x1x2 x3
Known tuple_2_setprodtuple_2_setprod : ∀ x0 x1 x2 . x2x0∀ x3 . x3x1lam 2 (λ x4 . If_i (x4 = 0) x2 x3)setprod x0 x1
Known ordsuccI2ordsuccI2 : ∀ x0 . x0ordsucc x0
Known tuple_2_0_eqtuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0
Known FalseEFalseE : False∀ x0 : ο . x0
Known In_irrefIn_irref : ∀ x0 . nIn x0 x0
Known tuple_2_1_eqtuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known ordsuccEordsuccE : ∀ x0 x1 . x1ordsucc x0or (x1x0) (x1 = x0)
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known Inj1_setsumInj1_setsum : ∀ x0 x1 x2 . x2x1Inj1 x2setsum x0 x1
Known tuple_Sigma_etatuple_Sigma_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2lam x0 x1lam 2 (λ x4 . If_i (x4 = 0) (ap x2 0) (ap x2 1)) = x2
Known Inj0_setsumInj0_setsum : ∀ x0 x1 x2 . x2x0Inj0 x2setsum x0 x1
Known ap0_Sigmaap0_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2lam x0 x1ap x2 0x0
Known setprod_monsetprod_mon : ∀ x0 x1 . x0x1∀ x2 x3 . x2x3setprod x0 x2setprod x1 x3
Known Subq_refSubq_ref : ∀ x0 . x0x0
Known ordsuccI1ordsuccI1 : ∀ x0 . x0ordsucc x0
Known combine_funcs_eq2combine_funcs_eq2 : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj1 x4) = x3 x4
Known combine_funcs_eq1combine_funcs_eq1 : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj0 x4) = x2 x4
Theorem a57cb.. : ∀ x0 . nat_p x0∀ x1 . nat_p x1equip (mul_nat x0 x1) (setprod x0 x1) (proof)
Definition u25 := ordsucc u24
Known nat_4nat_4 : nat_p 4
Known nat_3nat_3 : nat_p 3
Known nat_2nat_2 : nat_p 2
Known nat_1nat_1 : nat_p 1
Known mul_nat_1Rmul_nat_1R : ∀ x0 . mul_nat x0 1 = x0
Param ChurchNum_p : ((ιι) → ιι) → ο
Known 39d66.. : ∀ x0 : (ι → ι)ι → ι . ChurchNum_p x0∀ x1 : (ι → ι)ι → ι . ChurchNum_p x1x0 ordsucc (x1 ordsucc 0) = add_nat (x0 ordsucc 0) (x1 ordsucc 0)
Known c9952.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 x1)))))
Known 0a45b.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1))))))))))
Known 466b2.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1)))))))))))))))
Known 4e557.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1))))))))))))))))))))
Theorem c12f7.. : mul_nat u5 u5 = u25 (proof)