Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ⊆ u12.
Assume H1: atleastp u5 x0.
Assume H2: ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_3_6_17 x1 x2).
Assume H3: atleastp u2 (setminus x0 u8).
Let x1 of type ο be given.
Assume H4: ∀ x2 . x2 ⊆ u12 ⟶ atleastp u5 x2 ⟶ (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ not (TwoRamseyGraph_3_6_17 x3 x4)) ⟶ u8 ∈ x2 ⟶ u9 ∈ x2 ⟶ x1.
Assume H5: ∀ x2 . x2 ⊆ u12 ⟶ atleastp u5 x2 ⟶ (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ not (TwoRamseyGraph_3_6_17 x3 x4)) ⟶ u8 ∈ x2 ⟶ u10 ∈ x2 ⟶ x1.
Claim L6: ...
...
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Apply unknownprop_6d92d1f1dc2442370b11e307d2507ca4f85754f5689757e7fe022101bb36e82e with λ x2 x3 . and (TwoRamseyGraph_3_6_17 x2 x3) (x2 = x3 ⟶ ∀ x4 : ο . x4), u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12, x0, x1 leaving 14 subgoals.
The subproof is completed by applying unknownprop_b12bb4463d091b1cd992428972a90829208a78c99e502cb179137d8ffeb2e9ed.
The subproof is completed by applying unknownprop_0c825f2c7c09729d7ce0ddc2bcc1c1164def77499abc770e53acff066a542f42.
The subproof is completed by applying L7.
The subproof is completed by applying unknownprop_4e46240fa21fb39b84708f415e3b21cc616773a08b926976627048ab8fc29078.
The subproof is completed by applying unknownprop_29ccb5c4e7950928d647b0941425c5e64d69ebaaed74cba3c055174a14ae4c5b.
The subproof is completed by applying unknownprop_9b334a439f93d75505077dcc1fe4c60157a3105589338dee138085e931431815.
The subproof is completed by applying L8.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying L9.
The subproof is completed by applying H3.
Let x2 of type ι be given.
Assume H10: x2 ⊆ u12.
Assume H11: atleastp u5 x2.
Assume H12: ∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ not (and (TwoRamseyGraph_3_6_17 x3 x4) (x3 = x4 ⟶ ∀ x5 : ο . x5)).
Assume H13: u8 ∈ x2.
Assume H14: u9 ∈ x2.
Apply H4 with x2 leaving 5 subgoals.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
Let x3 of type ι be given.
Assume H15: x3 ∈ x2.
Let x4 of type ι be given.
Assume H16: x4 ∈ x2.
Assume H17: x3 = x4 ⟶ ∀ x5 : ο . x5.
Assume H18: TwoRamseyGraph_3_6_17 x3 x4.
Apply H12 with x3, x4 leaving 3 subgoals.
The subproof is completed by applying H15.
The subproof is completed by applying H16.
Apply andI with TwoRamseyGraph_3_6_17 x3 x4, x3 = x4 ⟶ ∀ x5 : ο . x5 leaving 2 subgoals.
The subproof is completed by applying H18.
The subproof is completed by applying H17.
The subproof is completed by applying H13.
The subproof is completed by applying H14.
Let x2 of type ι be given.
Assume H10: x2 ⊆ u12.
Assume H11: atleastp u5 x2.
Assume H12: ∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ not (and (TwoRamseyGraph_3_6_17 x3 x4) (x3 = x4 ⟶ ∀ x5 : ο . x5)).
Assume H13: u8 ∈ x2.
Assume H14: u10 ∈ x2.
Apply H5 with x2 leaving 5 subgoals.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
Let x3 of type ι be given.
Assume H15: x3 ∈ x2.
Let x4 of type ι be given.
Assume H16: x4 ∈ x2.
Assume H17: x3 = x4 ⟶ ∀ x5 : ο . x5.
Assume H18: TwoRamseyGraph_3_6_17 x3 x4.
Apply H12 with x3, x4 leaving 3 subgoals.
The subproof is completed by applying H15.
The subproof is completed by applying H16.
Apply andI with TwoRamseyGraph_3_6_17 x3 x4, x3 = x4 ⟶ ∀ x5 : ο . x5 leaving 2 subgoals.
The subproof is completed by applying H18.
The subproof is completed by applying H17.
The subproof is completed by applying H13.
The subproof is completed by applying H14.
Let x2 of type ι be given.
Assume H10: x2 ⊆ u12.
Assume H11: atleastp u5 x2.
Assume H12: ∀ x3 . ... ⟶ ∀ x4 . ... ⟶ not (and (TwoRamseyGraph_3_6_17 x3 x4) (x3 = x4 ⟶ ∀ x5 : ο . x5)).
...
■