Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: ...
...
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 H1: ChurchNum_3ary_proj_p x0.
Assume H2: ChurchNum_8ary_proj_p x2.
Assume H3: ChurchNum_3ary_proj_p x1.
Assume H4: ChurchNum_8ary_proj_p x3.
Apply L0 with ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x2 x0) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x2) = ChurchNums_3x8_to_u24 x1 x3 ⟶ and (x1 = ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x2 x0) (x3 = ChurchNums_8_perm_3_4_5_6_7_0_1_2 x2).
Let x4 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H5: ∀ x5 x6 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x7 x8 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x4 x5 x6 x7 x8 ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x7 x5) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x7) = ChurchNums_3x8_to_u24 x6 x8 ⟶ and (x6 = ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x7 x5) (x8 = ChurchNums_8_perm_3_4_5_6_7_0_1_2 x7).
Assume H6: ∀ x5 x6 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x7 x8 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x7 x5) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x7) = ChurchNums_3x8_to_u24 x6 x8 ⟶ ∀ x9 : ο . x9) ⟶ x4 x5 x6 x7 x8.
Assume H7: ∀ x5 x6 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x7 x8 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x6 = ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x7 x5 ⟶ x8 = ChurchNums_8_perm_3_4_5_6_7_0_1_2 x7 ⟶ x4 x5 x6 x7 x8.
Apply H5 with x0, x1, x2, x3.
Apply H1 with λ x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x4 x5 x1 x2 x3 leaving 3 subgoals.
Apply H2 with λ x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x4 (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) x1 x5 x3 leaving 8 subgoals.
Apply H3 with λ x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x4 (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) x5 (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x3 leaving 3 subgoals.
Apply H4 with λ x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x4 (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x5 leaving 8 subgoals.
Apply H6 with λ x5 x6 x7 : (ι → ι) → ι → ι . x5, λ x5 x6 x7 : (ι → ι) → ι → ι . x5, λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5, λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5.
Assume H8: ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 : (ι → ι) → ι → ι . x5)) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5)) = ChurchNums_3x8_to_u24 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5).
Apply neq_3_0.
The subproof is completed by applying H8.
Apply H6 with λ x5 x6 x7 : (ι → ι) → ι → ι . x5, λ x5 x6 x7 : (ι → ι) → ι → ι . x5, λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5, λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x6.
Assume H8: ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 : (ι → ι) → ι → ι . x5)) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5)) = ChurchNums_3x8_to_u24 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x6).
Apply neq_3_1.
The subproof is completed by applying H8.
Apply H6 with λ x5 x6 x7 : (ι → ι) → ι → ι . x5, λ x5 x6 x7 : (ι → ι) → ι → ι . x5, λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5, λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x7.
Assume H8: ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 : (ι → ι) → ι → ι . x5)) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5)) = ChurchNums_3x8_to_u24 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x7).
Apply neq_3_2.
The subproof is completed by applying H8.
Apply H7 with λ x5 x6 x7 : (ι → ι) → ι → ι . x5, λ x5 x6 x7 : (ι → ι) → ι → ι . x5, λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5, λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x8 leaving 2 subgoals.
Let x5 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H8: x5 (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 : (ι → ι) → ι → ι . x6)).
The subproof is completed by applying H8.
Let x5 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H8: x5 (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x9) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6)).
The subproof is completed by applying H8.
Apply H6 with λ x5 x6 x7 : (ι → ι) → ι → ι . x5, λ x5 x6 x7 : (ι → ι) → ι → ι . x5, λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5, λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x9.
Assume H8: ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 : (ι → ι) → ι → ι . x5)) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5)) = ChurchNums_3x8_to_u24 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x9).
Apply neq_4_3.
Let x5 of type ι → ι → ο be given.
The subproof is completed by applying H8 with λ x6 x7 . x5 x7 x6.
Apply H6 with λ x5 x6 x7 : (ι → ι) → ι → ι . x5, λ x5 x6 x7 : (ι → ι) → ι → ι . x5, λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . ..., ....
...
...
...
...
...
...
...
...
...
...
...
...
...
...
■