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