Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Assume H0: ChurchNum_8ary_proj_p x0.
Apply H0 with λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8x3_lt6_id_ge6_rot1 x1 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x1 x2) = x2 leaving 8 subgoals.
Let x1 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x2 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H1: x2 (ChurchNums_8x3_lt6_id_ge6_rot1 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x3) (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x3) x1)) x1.
The subproof is completed by applying H1.
Let x1 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x2 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H1: x2 (ChurchNums_8x3_lt6_id_ge6_rot1 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x4) (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x4) x1)) x1.
The subproof is completed by applying H1.
Let x1 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x2 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H1: x2 (ChurchNums_8x3_lt6_id_ge6_rot1 (λ 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 : (ι → ι) → ι → ι . x5) x1)) x1.
The subproof is completed by applying H1.
Let x1 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x2 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H1: x2 (ChurchNums_8x3_lt6_id_ge6_rot1 (λ 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 : (ι → ι) → ι → ι . x6) x1)) x1.
The subproof is completed by applying H1.
Let x1 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x2 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H1: x2 (ChurchNums_8x3_lt6_id_ge6_rot1 (λ 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 : (ι → ι) → ι → ι . x7) x1)) x1.
The subproof is completed by applying H1.
Let x1 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x2 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H1: x2 (ChurchNums_8x3_lt6_id_ge6_rot1 (λ 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 : (ι → ι) → ι → ι . x8) x1)) x1.
The subproof is completed by applying H1.
Let x1 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Apply functional extensionality with ChurchNums_8x3_lt6_id_ge6_rot1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x8) (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x8) x1), x1.
Let x2 of type (ι → ι) → ι → ι be given.
Apply functional extensionality with ChurchNums_8x3_lt6_id_ge6_rot1 (λ 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 : (ι → ι) → ι → ι . x9) x1) x2, x1 x2.
Let x3 of type (ι → ι) → ι → ι be given.
Apply functional extensionality with ChurchNums_8x3_lt6_id_ge6_rot1 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x10) (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x10) x1) x2 x3, x1 x2 x3.
Let x4 of type (ι → ι) → ι → ι be given.
Let x5 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ο be given.
Assume H1: x5 (ChurchNums_8x3_lt6_id_ge6_rot1 (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x12) (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x12) x1) x2 x3 x4) (x1 x2 x3 x4).
The subproof is completed by applying H1.
Let x1 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Apply functional extensionality with ChurchNums_8x3_lt6_id_ge6_rot1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x9) (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x9) x1), x1.
Let x2 of type (ι → ι) → ι → ι be given.
Apply functional extensionality with ChurchNums_8x3_lt6_id_ge6_rot1 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x10) (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x10) x1) x2, x1 x2.
Let x3 of type (ι → ι) → ι → ι be given.
Apply functional extensionality with ChurchNums_8x3_lt6_id_ge6_rot1 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x11) (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x11) x1) x2 x3, x1 x2 x3.
Let x4 of type (ι → ι) → ι → ι be given.
Let x5 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ο be given.
Assume H1: x5 (ChurchNums_8x3_lt6_id_ge6_rot1 (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x13) (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x13) x1) x2 x3 x4) (x1 x2 x3 x4).
The subproof is completed by applying H1.
■