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: Church17_p x0.
Assume H2: Church17_p x1.
Assume H3: Church17_p x2.
Apply H1 with λ x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . ((λ x4 x5 . x3 x4 x4 x4 x4 x4 x4 x4 x4 x4 x5 x5 x5 x5 x5 x5 x5 x5) = λ x4 x5 . x4) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x3 ⟶ ∀ x4 : ο . x4) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x1 ⟶ ∀ x4 : ο . x4) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x2 ⟶ ∀ x4 : ο . x4) ⟶ (x3 = x1 ⟶ ∀ x4 : ο . x4) ⟶ (x3 = x2 ⟶ ∀ x4 : ο . x4) ⟶ (x1 = x2 ⟶ ∀ x4 : ο . x4) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x3 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x1 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x2 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 x3 x1 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 x3 x2 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 x1 x2 = λ x4 x5 . x4) ⟶ False leaving 17 subgoals.
Assume H4: (λ x3 x4 . (λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 . x5) x3 x3 x3 x3 x3 x3 x3 x3 x3 x4 x4 x4 x4 x4 x4 x4 x4) = λ x3 x4 . x3.
Assume H5: ((λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x3) = λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x3) ⟶ ∀ x3 : ο . x3.
Apply FalseE with ((λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x3) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x3) = x2 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x3) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x3) = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x3) = λ x3 x4 . x3) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x3) x1 = λ x3 x4 . x3) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x3) x2 = λ x3 x4 . x3) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x3) x1 = λ x3 x4 . x3) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x3) x2 = λ x3 x4 . x3) ⟶ (TwoRamseyGraph_4_4_Church17 x1 x2 = λ x3 x4 . x3) ⟶ False.
Apply H5.
Let x3 of type (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο be given.
Assume H6: x3 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4).
The subproof is completed by applying H6.
Assume H4: (λ x3 x4 . (λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 . x6) x3 x3 x3 x3 x3 x3 x3 x3 x3 x4 x4 x4 x4 x4 x4 x4 x4) = λ x3 x4 . x3.
Apply H2 with λ x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) ... = ... ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x5) x3 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x5) x2 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 x3 x2 = λ x4 x5 . x4) ⟶ False leaving 17 subgoals.
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
■