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_lt5_id_ge5_rot2 x1 x2) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x1) = ChurchNums_3x8_to_u24 x2 x1 ⟶ ∀ x3 : ο . x3 leaving 3 subgoals.
Apply H1 with λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x2 (λ x3 x4 x5 : (ι → ι) → ι → ι . x3)) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x2) = ChurchNums_3x8_to_u24 (λ x3 x4 x5 : (ι → ι) → ι → ι . x3) x2 ⟶ ∀ x3 : ο . x3 leaving 8 subgoals.
The subproof is completed by applying neq_3_0.
The subproof is completed by applying neq_4_1.
The subproof is completed by applying neq_5_2.
The subproof is completed by applying neq_6_3.
The subproof is completed by applying neq_7_4.
The subproof is completed by applying neq_8_5.
The subproof is completed by applying neq_9_6.
The subproof is completed by applying unknownprop_f90d6a14135c76785343d196a602714aaebc8f848035cb3fc7d99e4a8069fa52.
Apply H1 with λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x2 (λ x3 x4 x5 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x2) = ChurchNums_3x8_to_u24 (λ x3 x4 x5 : (ι → ι) → ι → ι . x4) x2 ⟶ ∀ x3 : ο . x3 leaving 8 subgoals.
The subproof is completed by applying unknownprop_e3e7876f64d57e7b4aae114d87715d9a64fc4129a1a28df53f278ae0d8499348.
The subproof is completed by applying unknownprop_e9452875caa538a193e13eb1accc0d1d2221ffa1eb64478ef4b831d0c7fb8587.
The subproof is completed by applying unknownprop_611c167b8d8d5c2c171ede951fd79aafcb1fd16fb816a3f0e5c0edff9bd7addf.
The subproof is completed by applying unknownprop_00afc3423aeef527fa52daa0e685caaf0adcec70a4145f09454ed0ecaf166b37.
The subproof is completed by applying unknownprop_b71ad64ae5ee6739b72b7cf6202281008bcc9edc7ad98b81f40c22a64711fdc6.
The subproof is completed by applying unknownprop_4e5614ee6c60ca75b34344cfddfbe4840c89f999d594b201761970f40f5f2255.
The subproof is completed by applying unknownprop_4867b3ce4fe1d0a1c8ff8d2e2bc0717758c4ccc013cbbaaf26121557137d2316.
The subproof is completed by applying unknownprop_fc69b4f24fa74882a934d6a846b06596684e5849597d21231c600ed2d7a43c70.
Apply H1 with λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x2 (λ x3 x4 x5 : (ι → ι) → ι → ι . x5)) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x2) = ChurchNums_3x8_to_u24 (λ x3 x4 x5 : (ι → ι) → ι → ι . x5) x2 ⟶ ∀ x3 : ο . x3 leaving 8 subgoals.
The subproof is completed by applying unknownprop_f4eab5da6a90e1d04224584391affbc6b18c42542dd60d5730fe3dc72ad0cd62.
The subproof is completed by applying unknownprop_e875d4259eccd00196f9a81452eacf721af588c7e9269dc84035cecf04073b0a.
The subproof is completed by applying unknownprop_116e7cbd999186ad5cfa2811a7b1efe9808f1d43fddc92f1fecc1f6d9298b665.
The subproof is completed by applying unknownprop_1a53f970fcf4ee84e2f9d30498e0319f427d029bd6cae83309f9f5e645439192.
The subproof is completed by applying unknownprop_e046300dbabcb6879d5ee7b7a3484aad1e616228ce77872869131b66bd674d3c.
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_lt5_id_ge5_rot2 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x7) (λ x2 x3 x4 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x7)).
The subproof is completed by applying unknownprop_172f2affd770fc4865199fceeb6667b9418cbfb12988961b0522b9fcaefa561f.
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_lt5_id_ge5_rot2 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x8) (λ x2 x3 x4 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x8)).
The subproof is completed by applying unknownprop_45a64368e1c57028abfd9fa6ed583fc783c2b40be93475c6caa3fd23bbae3d49.
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_lt5_id_ge5_rot2 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x9) (λ x2 x3 x4 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x9)).
The subproof is completed by applying unknownprop_ddac1988a2199344800a986643397dbf7b977152e2795c780f668d66763c7142.
■