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