Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x1 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x2 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x3 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Assume H0: ChurchNums_3x8_eq x0 x2 x1 x3.
Apply H0 with ChurchNums_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).
Assume H1: x0 = x1.
Assume H2: x2 = x3.
Apply H1 with λ x4 x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_3x8_eq (ChurchNums_3x8_3_lt1_swap_1_2_ge1_rot2 x5 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).
Apply H2 with λ x4 x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_3x8_eq (ChurchNums_3x8_3_lt1_swap_1_2_ge1_rot2 x1 x5) (ChurchNums_8_perm_0_7_6_5_4_3_2_1 x5) (ChurchNums_3x8_3_lt1_swap_1_2_ge1_rot2 x1 x3) (ChurchNums_8_perm_0_7_6_5_4_3_2_1 x3).
Apply unknownprop_489a19599530946830ae79502aec6ef7b2f064765691a3ca83405abd2ab867f4 with ChurchNums_3x8_3_lt1_swap_1_2_ge1_rot2 x1 x3, ChurchNums_3x8_3_lt1_swap_1_2_ge1_rot2 x1 x3, ChurchNums_8_perm_0_7_6_5_4_3_2_1 x3, ChurchNums_8_perm_0_7_6_5_4_3_2_1 x3 leaving 2 subgoals.
Let x4 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H3: x4 (ChurchNums_3x8_3_lt1_swap_1_2_ge1_rot2 x1 x3) (ChurchNums_3x8_3_lt1_swap_1_2_ge1_rot2 x1 x3).
The subproof is completed by applying H3.
Let x4 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H3: x4 (ChurchNums_8_perm_0_7_6_5_4_3_2_1 x3) (ChurchNums_8_perm_0_7_6_5_4_3_2_1 x3).
The subproof is completed by applying H3.
■