Search for blocks/addresses/...

Proofgold Proof

pf
Assume H0: TwoRamseyProp_atleastp 4 4 17.
Apply H0 with TwoRamseyGraph_4_4_17, False leaving 3 subgoals.
The subproof is completed by applying unknownprop_bf922fbc15ef367e36095d6fe104c659782efdeb2f3c623c6ad8079831449813.
Assume H1: ∃ x0 . and (x0 ⊆ u17) (and (atleastp u4 x0) (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ TwoRamseyGraph_4_4_17 x1 x2)).
Apply H1 with False.
Let x0 of type ι be given.
Assume H2: (λ x1 . and (x1 ⊆ u17) (and (atleastp u4 x1) (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ TwoRamseyGraph_4_4_17 x2 x3))) x0.
Apply H2 with False.
Assume H3: x0 ⊆ u17.
Assume H4: and (atleastp u4 x0) (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ TwoRamseyGraph_4_4_17 x1 x2).
Apply H4 with False.
Assume H5: atleastp u4 x0.
Assume H6: ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ TwoRamseyGraph_4_4_17 x1 x2.
Apply unknownprop_1947e9bb22af44c2835c404efac3be226fcf1cde719d4bda48e06372ac44fe1d with x0 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
Assume H1: ∃ x0 . and (x0 ⊆ u17) (and (atleastp u4 x0) (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_4_4_17 x1 x2))).
Apply H1 with False.
Let x0 of type ι be given.
Assume H2: (λ x1 . and (x1 ⊆ u17) (and (atleastp u4 x1) (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (TwoRamseyGraph_4_4_17 x2 x3)))) x0.
Apply H2 with False.
Assume H3: x0 ⊆ u17.
Assume H4: and (atleastp u4 x0) (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_4_4_17 x1 x2)).
Apply H4 with False.
Assume H5: atleastp u4 x0.
Assume H6: ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_4_4_17 x1 x2).
Apply unknownprop_dadf5826f13a875cf09df22d9944f81bee726f8a1b299f608c97841ffb4cd64a with x0 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
■