Search for blocks/addresses/...

Proofgold Proof

pf
Assume H0: ∀ x0 . x0 ∈ u17 ⟶ Church17_p (u17_to_Church17_buggy x0).
Assume H1: ∀ x0 . x0 ∈ u17 ⟶ ∀ x1 . x1 ∈ u17 ⟶ u17_to_Church17_buggy x0 = u17_to_Church17_buggy x1 ⟶ x0 = x1.
Assume H2: ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ Church17_p x2 ⟶ (x0 = x1 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (TwoRamseyGraph_3_6_Church17 x0 x1 = λ x3 x4 . x3) ⟶ (TwoRamseyGraph_3_6_Church17 x0 x2 = λ x3 x4 . x3) ⟶ (TwoRamseyGraph_3_6_Church17 x1 x2 = λ x3 x4 . x3) ⟶ False.
Assume H3: ∀ x0 x1 . TwoRamseyGraph_3_6_17_buggy x0 x1 ⟶ TwoRamseyGraph_3_6_17_buggy x1 x0.
Assume H4: ∀ x0 . x0 ⊆ u17 ⟶ atleastp u6 x0 ⟶ not (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_3_6_17_buggy x1 x2)).
Assume H5: TwoRamseyProp_atleastp u3 u6 u17.
Apply H5 with TwoRamseyGraph_3_6_17_buggy, False leaving 3 subgoals.
The subproof is completed by applying H3.
Assume H6: ∃ x0 . and (x0 ⊆ u17) (and (atleastp u3 x0) (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ TwoRamseyGraph_3_6_17_buggy x1 x2)).
Apply H6 with False.
Let x0 of type ι be given.
Assume H7: (λ x1 . and (x1 ⊆ u17) (and (atleastp u3 x1) (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ TwoRamseyGraph_3_6_17_buggy x2 x3))) x0.
Apply H7 with False.
Assume H8: x0 ⊆ u17.
Assume H9: and (atleastp u3 x0) (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ TwoRamseyGraph_3_6_17_buggy x1 x2).
Apply H9 with False.
Assume H10: atleastp u3 x0.
Assume H11: ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ TwoRamseyGraph_3_6_17_buggy x1 x2.
Apply unknownprop_770505912c32dda2498a8aaf85f0c77fe9f674b5bdbb481b51987aa8ab664128 with x0 leaving 6 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H8.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
Assume H6: ∃ x0 . and (x0 ⊆ u17) (and (atleastp u6 x0) (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_3_6_17_buggy x1 x2))).
Apply H6 with False.
Let x0 of type ι be given.
Assume H7: (λ x1 . and (x1 ⊆ u17) (and (atleastp u6 x1) (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (TwoRamseyGraph_3_6_17_buggy x2 x3)))) x0.
Apply H7 with False.
Assume H8: ....
...
■