Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: ...
...
Let x0 of type ι → ι → ι → ι → ι → ι → ι be given.
Let x1 of type ι → ι → ι → ι → ι → ι → ι be given.
Let x2 of type ι → ι → ι → ι → ι → ι → ι be given.
Assume H1: Church6_p x0.
Assume H2: Church6_p x1.
Assume H3: a4ee9.. x2.
Apply H1 with λ x3 : ι → ι → ι → ι → ι → ι → ι . ((x3 = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ False) ⟶ ((x3 = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ x1 = x2 ⟶ False) ⟶ (TwoRamseyGraph_4_6_Church6_squared_a x3 x1 (λ x4 x5 x6 x7 x8 x9 . x9) x2 = λ x4 x5 . x4) ⟶ TwoRamseyGraph_4_6_Church6_squared_b x3 x1 (λ x4 x5 x6 x7 x8 x9 . x9) x2 = λ x4 x5 . x4 leaving 6 subgoals.
Apply H2 with λ x3 : ι → ι → ι → ι → ι → ι → ι . (((λ x4 x5 x6 x7 x8 x9 . x4) = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ (x3 = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ False) ⟶ (((λ x4 x5 x6 x7 x8 x9 . x4) = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ x3 = x2 ⟶ False) ⟶ (TwoRamseyGraph_4_6_Church6_squared_a (λ x4 x5 x6 x7 x8 x9 . x4) x3 (λ x4 x5 x6 x7 x8 x9 . x9) x2 = λ x4 x5 . x4) ⟶ TwoRamseyGraph_4_6_Church6_squared_b (λ x4 x5 x6 x7 x8 x9 . x4) x3 (λ x4 x5 x6 x7 x8 x9 . x9) x2 = λ x4 x5 . x4 leaving 6 subgoals.
Apply H3 with λ x3 : ι → ι → ι → ι → ι → ι → ι . (((λ x4 x5 x6 x7 x8 x9 . x4) = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ ((λ x4 x5 x6 x7 x8 x9 . x4) = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ False) ⟶ (((λ x4 x5 x6 x7 x8 x9 . x4) = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ (λ x4 x5 x6 x7 x8 x9 . x4) = x3 ⟶ False) ⟶ (TwoRamseyGraph_4_6_Church6_squared_a (λ x4 x5 x6 x7 x8 x9 . x4) (λ x4 x5 x6 x7 x8 x9 . x4) (λ x4 x5 x6 x7 x8 x9 . x9) x3 = λ x4 x5 . x4) ⟶ TwoRamseyGraph_4_6_Church6_squared_b (λ x4 x5 x6 x7 x8 x9 . x4) (λ x4 x5 x6 x7 x8 x9 . x4) (λ x4 x5 x6 x7 x8 x9 . x9) x3 = λ x4 x5 . x4 leaving 5 subgoals.
Assume H4: ((λ x3 x4 x5 x6 x7 x8 . x3) = λ x3 x4 x5 x6 x7 x8 . x8) ⟶ ((λ x3 x4 x5 x6 x7 x8 . x3) = λ x3 x4 x5 x6 x7 x8 . x8) ⟶ False.
Assume H5: ((λ x3 x4 x5 x6 x7 x8 . x3) = λ x3 x4 x5 x6 x7 x8 . x8) ⟶ ((λ x3 x4 x5 x6 x7 x8 . x3) = λ x3 x4 x5 x6 x7 x8 . x3) ⟶ False.
Assume H6: TwoRamseyGraph_4_6_Church6_squared_a (λ x3 x4 x5 x6 x7 x8 . x3) (λ x3 x4 x5 x6 x7 x8 . x3) (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x3) = λ x3 x4 . x3.
Let x3 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H7: x3 (TwoRamseyGraph_4_6_Church6_squared_b (λ x4 x5 x6 x7 x8 x9 . x4) (λ x4 x5 x6 x7 x8 x9 . x4) (λ x4 x5 x6 x7 x8 x9 . x9) (λ x4 x5 x6 x7 x8 x9 . x4)) (λ x4 x5 . x4).
The subproof is completed by applying H7.
Assume H4: ((λ x3 x4 x5 x6 x7 x8 . x3) = λ x3 x4 x5 x6 x7 x8 . x8) ⟶ ((λ x3 x4 x5 x6 x7 x8 . x3) = λ x3 x4 x5 x6 x7 x8 . x8) ⟶ False.
Assume H5: ((λ x3 x4 x5 x6 x7 x8 . x3) = λ x3 x4 x5 x6 x7 x8 . x8) ⟶ ((λ x3 x4 x5 x6 x7 x8 . x3) = λ x3 x4 x5 x6 x7 x8 . x4) ⟶ False.
Assume H6: TwoRamseyGraph_4_6_Church6_squared_a (λ x3 x4 x5 x6 x7 x8 . x3) (λ x3 x4 x5 x6 x7 x8 . x3) (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x4) = λ x3 x4 . x3.
Apply FalseE with TwoRamseyGraph_4_6_Church6_squared_b (λ x3 x4 x5 x6 x7 x8 . x3) (λ x3 x4 x5 x6 x7 x8 . x3) (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x4) = λ x3 x4 . x3.
Apply L0.
The subproof is completed by applying H6.
Assume H4: ((λ x3 x4 x5 x6 x7 x8 . x3) = λ x3 x4 x5 x6 x7 x8 . x8) ⟶ ((λ x3 x4 x5 x6 x7 x8 . x3) = λ x3 x4 x5 x6 x7 x8 . x8) ⟶ False.
Assume H5: ((λ x3 x4 x5 x6 x7 x8 . x3) = λ x3 x4 x5 x6 x7 x8 . x8) ⟶ ((λ x3 x4 x5 x6 x7 x8 . x3) = λ x3 x4 x5 x6 x7 x8 . x5) ⟶ False.
Assume H6: TwoRamseyGraph_4_6_Church6_squared_a (λ x3 x4 x5 x6 x7 x8 . x3) (λ x3 x4 x5 x6 x7 x8 . x3) (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x5) = λ x3 x4 . x3.
Let x3 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H7: ....
...
...
...
...
...
...
...
...
...
...
...
...
...
■