Search for blocks/addresses/...

Proofgold Proof

pf
Assume H0: TwoRamseyProp_atleastp 4 5 24.
Apply H0 with TwoRamseyGraph_4_5_24, False leaving 3 subgoals.
The subproof is completed by applying unknownprop_214df808d911cebbf3429c39ac7b14dcaba95c0948647fcb9a7514b4cc53fec3.
Assume H1: ∃ x0 . and (x0 ⊆ u24) (and (atleastp u4 x0) (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ TwoRamseyGraph_4_5_24 x1 x2)).
Apply H1 with False.
Let x0 of type ι be given.
Assume H2: (λ x1 . and (x1 ⊆ u24) (and (atleastp u4 x1) (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ TwoRamseyGraph_4_5_24 x2 x3))) x0.
Apply H2 with False.
Assume H3: x0 ⊆ u24.
Assume H4: and (atleastp u4 x0) (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ TwoRamseyGraph_4_5_24 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_5_24 x1 x2.
Apply unknownprop_04e88456fa9b12269b649b664ba7c6f7b828569f8b71bac74f04b5637be6dc8b 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 ⊆ u24) (and (atleastp u5 x0) (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_4_5_24 x1 x2))).
Apply H1 with False.
Let x0 of type ι be given.
Assume H2: (λ x1 . and (x1 ⊆ u24) (and (atleastp u5 x1) (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (TwoRamseyGraph_4_5_24 x2 x3)))) x0.
Apply H2 with False.
Assume H3: x0 ⊆ u24.
Assume H4: and (atleastp u5 x0) (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_4_5_24 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_4_5_24 x1 x2).
Apply unknownprop_c75cac62cf8ee24606f428093063bda6b2ace7a38b571566d2d0f84db5257101 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.
■