Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x1 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Assume H0: ChurchNum_3ary_proj_p x0.
Assume H1: ChurchNum_8ary_proj_p x1.
Assume H2: ChurchNums_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).
Apply unknownprop_9795ab363028b42b10ed8fae6a2d02d5bd364e2a93799ce790703318b440d176 with ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x1 x0, ChurchNums_8_perm_3_4_5_6_7_0_1_2 x1 leaving 3 subgoals.
Apply unknownprop_ba84a7f1e1da990c89c7b4a20e0c8ea3784f3072fd4d4532a9187e6eebf57222 with x1, x0 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
Apply unknownprop_7755de1b07fa829360026c1a038955e26e3aa4728904dec248e0cd71e05130fb with x1.
The subproof is completed by applying H1.
Claim L3: ChurchNums_8x3_to_3_lt7_id_ge7_rot2 (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x1) (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x1 x0) = ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x1 x0
Apply H1 with λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8x3_to_3_lt7_id_ge7_rot2 (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x2) (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x2 x0) = ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x2 x0 leaving 8 subgoals.
Claim L3: ChurchNums_8_perm_3_4_5_6_7_0_1_2 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x2) = λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x5
Let x2 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H3: x2 (ChurchNums_8_perm_3_4_5_6_7_0_1_2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x3)) (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x6).
The subproof is completed by applying H3.
Apply L3 with λ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x3 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) x0) = ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) x0.
Let x2 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H4: x2 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x6) (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x3) x0)) (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x3) x0).
The subproof is completed by applying H4.
Claim L3: ChurchNums_8_perm_3_4_5_6_7_0_1_2 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x3) = λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x6
Let x2 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H3: x2 (ChurchNums_8_perm_3_4_5_6_7_0_1_2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x4)) (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x7).
The subproof is completed by applying H3.
Apply L3 with λ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x3 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x5) x0) = ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x5) x0.
Let x2 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H4: x2 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x7) (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x4) x0)) (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x4) x0).
The subproof is completed by applying H4.
Claim L3: ChurchNums_8_perm_3_4_5_6_7_0_1_2 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x4) = λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x7
Let x2 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H3: x2 (ChurchNums_8_perm_3_4_5_6_7_0_1_2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x5)) (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x8).
The subproof is completed by applying H3.
Apply L3 with λ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x3 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x6) x0) = ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x6) x0.
Let x2 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H4: x2 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x8) (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x5) x0)) (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x5) x0).
The subproof is completed by applying H4.
Claim L3: ChurchNums_8_perm_3_4_5_6_7_0_1_2 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x5) = λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x8
Let x2 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H3: x2 (ChurchNums_8_perm_3_4_5_6_7_0_1_2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x6)) (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x9).
The subproof is completed by applying H3.
Apply L3 with λ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x3 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x7) x0) = ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x7) x0.
Let x2 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H4: x2 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x9) (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x6) x0)) (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x6) x0).
The subproof is completed by applying H4.
Let x2 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H3: x2 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 (ChurchNums_8_perm_3_4_5_6_7_0_1_2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x7)) (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x7) x0)) (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x7) x0).
The subproof is completed by applying H3.
Let x2 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H3: x2 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 (ChurchNums_8_perm_3_4_5_6_7_0_1_2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x8)) (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x8) x0)) ....
...
...
...
Apply L3 with λ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_3x8_to_u24 x3 (ChurchNums_8_perm_1_2_3_4_5_6_7_0 (ChurchNums_8_perm_3_4_5_6_7_0_1_2 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).
The subproof is completed by applying H2.
■