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.
Apply H0 with λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x1 x2) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x1) = ChurchNums_3x8_to_u24 x2 x1 ⟶ ∀ x3 : ο . x3 leaving 3 subgoals.
Apply H1 with λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x2 (λ x3 x4 x5 : (ι → ι) → ι → ι . x3)) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x2) = ChurchNums_3x8_to_u24 (λ x3 x4 x5 : (ι → ι) → ι → ι . x3) x2 ⟶ ∀ x3 : ο . x3 leaving 8 subgoals.
The subproof is completed by applying neq_4_0.
The subproof is completed by applying neq_5_1.
The subproof is completed by applying neq_6_2.
The subproof is completed by applying neq_7_3.
The subproof is completed by applying neq_8_4.
The subproof is completed by applying neq_9_5.
The subproof is completed by applying unknownprop_1caafcfab421a8bbf73edb3267db1f6908bd5029c181663700c5c637b54bb883.
The subproof is completed by applying unknownprop_10a35d241244d98b266514a8fe38926cbcc9f4c51c46fbe5923bab64f9db063e.
Apply H1 with λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x2 (λ x3 x4 x5 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x2) = ChurchNums_3x8_to_u24 (λ x3 x4 x5 : (ι → ι) → ι → ι . x4) x2 ⟶ ∀ x3 : ο . x3 leaving 8 subgoals.
The subproof is completed by applying unknownprop_405ba169154d9d42445b73345355e3c1ff4a4c35ee248b0842bd8e1a26057bf4.
The subproof is completed by applying unknownprop_2f6e5b1338db3ff412e38a1ecfa4d466e2517777a8bbed02c867df317c357933.
The subproof is completed by applying unknownprop_3e7054688acb8ba4a0f18423b649f383cf90ecfc4f6200e2e049d580ebc2dc1f.
The subproof is completed by applying unknownprop_ee5d720135ac2a1e6675f04fc296d39836826d1754aace8d3d88db80c3a9bf7b.
The subproof is completed by applying unknownprop_0c2339ef07f9be63916ba4ed21f5ed3d1c0fc25d2883650f1a08db958e637e32.
The subproof is completed by applying unknownprop_ec9593399259670f4eff77c972d13de69785d35423977aacd7e0e7a77e866b61.
The subproof is completed by applying unknownprop_95a48bd166473dd69fbd1d6c212b33b8b186a59fa5f64873a57a406abcd861d7.
The subproof is completed by applying unknownprop_6d740d9c9b188e805405e2d34ec9986e71b10c02400c25af6128c2cd7b43204a.
Apply H1 with λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x2 (λ x3 x4 x5 : (ι → ι) → ι → ι . x5)) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x2) = ChurchNums_3x8_to_u24 (λ x3 x4 x5 : (ι → ι) → ι → ι . x5) x2 ⟶ ∀ x3 : ο . x3 leaving 8 subgoals.
The subproof is completed by applying unknownprop_e5a105866bd0ded6c3644380e06b833d4aba44e9391e3fab11d8053b9f135f2f.
The subproof is completed by applying unknownprop_5d7ae603d28081618c996edf9b87bde4055fc620b70ee849067dc72a1770788c.
The subproof is completed by applying unknownprop_4249317584a93eea4ea9a17155e60b737afb0c5091a7dcfe593f93235e696685.
The subproof is completed by applying unknownprop_9701b8a5483a090b78796eef708de261df3f2545c5ce3af5a81f0a4ee00037bd.
Apply neq_i_sym with ChurchNums_3x8_to_u24 (λ x2 x3 x4 : (ι → ι) → ι → ι . x4) (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x6), ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x6) (λ x2 x3 x4 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x6)).
The subproof is completed by applying unknownprop_961499f8542074f8c18d781755f9f77c78ed32eb1a4f15b1f06614982543eb0b.
Apply neq_i_sym with ChurchNums_3x8_to_u24 (λ x2 x3 x4 : (ι → ι) → ι → ι . x4) (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x7), ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x7) (λ x2 x3 x4 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x7)).
The subproof is completed by applying unknownprop_0a793590be20ff8e25a7a7b0c0297235ca4eaab6a5fd8d4f3d05cd6dc9695d58.
Apply neq_i_sym with ChurchNums_3x8_to_u24 (λ x2 x3 x4 : (ι → ι) → ι → ι . x4) (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x8), ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x8) (λ x2 x3 x4 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x8)).
The subproof is completed by applying unknownprop_28a93ac24d94b617505eb1b786cd962b918d2929cbc8be70154d9c3a16656a4b.
Apply neq_i_sym with ChurchNums_3x8_to_u24 (λ x2 x3 x4 : (ι → ι) → ι → ι . x4) (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x9), ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x9) (λ x2 x3 x4 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x9)).
The subproof is completed by applying unknownprop_30b4a643cd067cfd4a20b14b81dfdf6822c9b14e9e7bb4190f2b11f7f27ef255.
■