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