Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ u6.
Let x1 of type ι be given.
Assume H1: x1 ∈ u6.
Let x2 of type ι be given.
Assume H2: x2 ∈ u6.
Let x3 of type ι be given.
Assume H3: x3 ∈ u6.
Assume H4: x0 = u5 ⟶ x1 = u5 ⟶ False.
Assume H5: x2 = u5 ⟶ x3 = u5 ⟶ False.
Assume H6: TwoRamseyGraph_4_6_35_b x0 x1 x2 x3.
Apply unknownprop_f2d48ee9534d86444c35e60a86dde436b9e38736c69ef2e4a50b6b67dd56fe3d with nth_6_tuple x0, nth_6_tuple x1, nth_6_tuple x2, nth_6_tuple x3 leaving 7 subgoals.
Apply unknownprop_90460311f4fb47844a8dd0d64a1306416f6a25ac4d465fc1811061f42791aace with x0.
The subproof is completed by applying H0.
Apply unknownprop_90460311f4fb47844a8dd0d64a1306416f6a25ac4d465fc1811061f42791aace with x1.
The subproof is completed by applying H1.
Apply unknownprop_90460311f4fb47844a8dd0d64a1306416f6a25ac4d465fc1811061f42791aace with x2.
The subproof is completed by applying H2.
Apply unknownprop_90460311f4fb47844a8dd0d64a1306416f6a25ac4d465fc1811061f42791aace with x3.
The subproof is completed by applying H3.
Apply unknownprop_d1ab6c05d827ab2f0497648eeb2e74b0b0260f4e004a74cbc06a5c0a175e4a2a with λ x4 x5 : ι → ι → ι → ι → ι → ι → ι . nth_6_tuple x0 = x4 ⟶ nth_6_tuple x1 = x4 ⟶ False.
Assume H7: nth_6_tuple x0 = nth_6_tuple u5.
Assume H8: nth_6_tuple x1 = nth_6_tuple u5.
Apply H4 leaving 2 subgoals.
Apply unknownprop_c75cff31880a89a656c47e80c0af1903547ace73a8cd84857ca0750f4ef54c4b with x0, u5 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying In_5_6.
The subproof is completed by applying H7.
Apply unknownprop_c75cff31880a89a656c47e80c0af1903547ace73a8cd84857ca0750f4ef54c4b with x1, u5 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying In_5_6.
The subproof is completed by applying H8.
Apply unknownprop_d1ab6c05d827ab2f0497648eeb2e74b0b0260f4e004a74cbc06a5c0a175e4a2a with λ x4 x5 : ι → ι → ι → ι → ι → ι → ι . nth_6_tuple x2 = x4 ⟶ nth_6_tuple x3 = x4 ⟶ False.
Assume H7: nth_6_tuple x2 = nth_6_tuple u5.
Assume H8: nth_6_tuple x3 = nth_6_tuple u5.
Apply H5 leaving 2 subgoals.
Apply unknownprop_c75cff31880a89a656c47e80c0af1903547ace73a8cd84857ca0750f4ef54c4b with x2, u5 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying In_5_6.
The subproof is completed by applying H7.
Apply unknownprop_c75cff31880a89a656c47e80c0af1903547ace73a8cd84857ca0750f4ef54c4b with x3, u5 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying In_5_6.
The subproof is completed by applying H8.
Apply H6 leaving 4 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 H3.
■