Search for blocks/addresses/...

Proofgold Proof

pf
Assume H0: TwoRamseyProp_atleastp 3 5 13.
Apply H0 with TwoRamseyGraph_3_5_13, False leaving 3 subgoals.
The subproof is completed by applying unknownprop_6691451906f37677ba45db254ad43a055bbea9a71de659c8291ba833ff1f99a2.
Assume H1: ∃ x0 . and (x0 ⊆ u13) (and (atleastp u3 x0) (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ TwoRamseyGraph_3_5_13 x1 x2)).
Apply H1 with False.
Let x0 of type ι be given.
Assume H2: (λ x1 . and (x1 ⊆ u13) (and (atleastp u3 x1) (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ TwoRamseyGraph_3_5_13 x2 x3))) x0.
Apply H2 with False.
Assume H3: x0 ⊆ u13.
Assume H4: and (atleastp u3 x0) (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ TwoRamseyGraph_3_5_13 x1 x2).
Apply H4 with False.
Assume H5: atleastp u3 x0.
Assume H6: ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ TwoRamseyGraph_3_5_13 x1 x2.
Apply unknownprop_611e3f668a310864e980350cd8f2559c41b2ec84dbf2aad8dbbd2fc90ee63435 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 ⊆ u13) (and (atleastp u5 x0) (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_3_5_13 x1 x2))).
Apply H1 with False.
Let x0 of type ι be given.
Assume H2: (λ x1 . and (x1 ⊆ u13) (and (atleastp u5 x1) (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (TwoRamseyGraph_3_5_13 x2 x3)))) x0.
Apply H2 with False.
Assume H3: x0 ⊆ u13.
Assume H4: and (atleastp u5 x0) (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_3_5_13 x1 x2)).
Apply H4 with False.
Assume H5: atleastp u5 x0.
Assume H6: ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_3_5_13 x1 x2).
Apply unknownprop_849959d181c1dc78420c17f9296fa40544a13424ff126e0d46a89188d82f2316 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.
■