Search for blocks/addresses/...

Proofgold Proof

pf
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 H0: ChurchNum_3ary_proj_p x0.
Assume H1: ChurchNum_3ary_proj_p x1.
Assume H2: ChurchNum_8ary_proj_p x2.
Assume H3: ChurchNum_8ary_proj_p x3.
Apply H0 with λ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (λ x5 x6 : (ι → ι) → ι → ι . λ x7 : ι → ι . λ x8 . x5 x7 (x6 x7 x8)) (x4 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 x6)))))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 x6))))))))))))))))) (x2 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x5 (x5 x6)) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 x6))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 x6)))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 x6))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 x6)))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 x6)))))))) ordsucc 0 = (λ x5 x6 : (ι → ι) → ι → ι . λ x7 : ι → ι . λ x8 . x5 x7 (x6 x7 x8)) (x1 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 x6)))))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 x6))))))))))))))))) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x5 (x5 x6)) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 x6))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 x6)))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 x6))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 x6)))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 x6)))))))) ordsucc 0 ⟶ and (x4 = x1) (x2 = x3) leaving 3 subgoals.
Apply H1 with λ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (λ x5 x6 : (ι → ι) → ι → ι . λ x7 : ι → ι . λ x8 . x5 x7 (x6 x7 x8)) ((λ x5 x6 x7 : (ι → ι) → ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 x6)))))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 ...)))))))) ... ... 0 = ... ⟶ and ((λ x5 x6 x7 : (ι → ι) → ι → ι . x5) = x4) (x2 = x3) leaving 3 subgoals.
...
...
...
...
...
■