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