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_lt6_id_ge6_rot2 x1 x2) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x1) = ChurchNums_3x8_to_u24 x2 x1 ⟶ ∀ x3 : ο . x3 leaving 3 subgoals.
Apply H1 with λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x2 (λ x3 x4 x5 : (ι → ι) → ι → ι . x3)) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x2) = ChurchNums_3x8_to_u24 (λ x3 x4 x5 : (ι → ι) → ι → ι . x3) x2 ⟶ ∀ x3 : ο . x3 leaving 8 subgoals.
The subproof is completed by applying neq_2_0.
The subproof is completed by applying neq_3_1.
The subproof is completed by applying neq_4_2.
The subproof is completed by applying neq_5_3.
The subproof is completed by applying neq_6_4.
The subproof is completed by applying neq_7_5.
The subproof is completed by applying neq_8_6.
The subproof is completed by applying neq_9_7.
Apply H1 with λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x2 (λ x3 x4 x5 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x2) = ChurchNums_3x8_to_u24 (λ x3 x4 x5 : (ι → ι) → ι → ι . x4) x2 ⟶ ∀ x3 : ο . x3 leaving 8 subgoals.
The subproof is completed by applying unknownprop_00ce3e990e394696d648599b893a93cd3cb153c371b93008eddec6849fd2aaa9.
The subproof is completed by applying unknownprop_eee73695077ff6070731183421778635002a71c030b9e35e65d114074acaa597.
The subproof is completed by applying unknownprop_a52e53b541a40078b90241258be0a0067f5bc813eb10693b9b961df0bbb05001.
The subproof is completed by applying unknownprop_0a910a83fae7c1219e51ae6f441b8120dc6f2353f129945859e5867a1d5c1be3.
The subproof is completed by applying unknownprop_15d8fee75ef2fcef507dcd58e078d7224460844031194a35f38ebec160a6c36c.
The subproof is completed by applying unknownprop_c4ec81028536a24273f04958b27208043a8e72bdb9f95435ebeb3fd5cd7535fc.
The subproof is completed by applying unknownprop_44dd594ce330f92aa460a3bc4ae154c08d18da149afbcbc953cc12dc2b8e3572.
The subproof is completed by applying unknownprop_d1dffc1c336e15bfd52ffbb0cdea2a47c856c061ff9c118dd9e985b84e29dc83.
Apply H1 with λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x2 (λ x3 x4 x5 : (ι → ι) → ι → ι . x5)) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x2) = ChurchNums_3x8_to_u24 (λ x3 x4 x5 : (ι → ι) → ι → ι . x5) x2 ⟶ ∀ x3 : ο . x3 leaving 8 subgoals.
The subproof is completed by applying unknownprop_48199a2c576158ae82528e00e9bdbc57db7b153fd2b9b08b5d19a699f50aefe3.
The subproof is completed by applying unknownprop_89cc3d43552b98630e93adfaacb03e2574aff9c02b3aa2506638d17b6117ee62.
The subproof is completed by applying unknownprop_d94e53b115bb7c8ad97900540e455e96755fdc4d2af5fa1f16b225e4dd920138.
The subproof is completed by applying unknownprop_9e5c3630c6bde594a7482457e2f23c53ccb7bfb274cd4576ad1a676c48795b2e.
The subproof is completed by applying unknownprop_3e4ce6e92e08efa4fce1ccf5a1aaf4446405b517ccaaabd655218dc861e608f6.
The subproof is completed by applying unknownprop_68107b5958592b9f4c85905bf7dcf474b342acbe0c7e4ec024664ad44c39e21d.
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_lt6_id_ge6_rot2 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x8) (λ x2 x3 x4 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x8)).
The subproof is completed by applying unknownprop_32b5dfdfa4f5b3ac9a9a00b831e93c63f93d8af007743ee91fcda4129b5fa6a7.
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_lt6_id_ge6_rot2 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x9) (λ x2 x3 x4 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x9)).
The subproof is completed by applying unknownprop_445cbfbee89069914628dcbfc9698480d93297cc7c419597623522230f6064f3.
■