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: x0 = x2 ⟶ x1 = x3 ⟶ False.
Assume H7: TwoRamseyGraph_4_6_35_a x0 x1 x2 x3.
Assume H8: x0 ∈ u6.
Assume H9: x1 ∈ u6.
Assume H10: x2 ∈ u6.
Assume H11: x3 ∈ u6.
Apply unknownprop_b05801314deaedecaebb1d40a9af6cda4e149b7ce95d89db7b4c6e7e6d64e5d6 with nth_6_tuple x0, nth_6_tuple x1, nth_6_tuple x2, nth_6_tuple x3 leaving 8 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 H12: nth_6_tuple x0 = nth_6_tuple u5.
Assume H13: 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 H12.
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 H13.
Apply unknownprop_d1ab6c05d827ab2f0497648eeb2e74b0b0260f4e004a74cbc06a5c0a175e4a2a with λ x4 x5 : ι → ι → ι → ι → ι → ι → ι . nth_6_tuple x2 = x4 ⟶ nth_6_tuple x3 = x4 ⟶ False.
Assume H12: nth_6_tuple x2 = nth_6_tuple u5.
Assume H13: 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 H12.
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 H13.
Assume H12: nth_6_tuple x0 = nth_6_tuple x2.
Assume H13: nth_6_tuple x1 = nth_6_tuple x3.
Apply H6 leaving 2 subgoals.
Apply unknownprop_c75cff31880a89a656c47e80c0af1903547ace73a8cd84857ca0750f4ef54c4b with x0, x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H12.
Apply unknownprop_c75cff31880a89a656c47e80c0af1903547ace73a8cd84857ca0750f4ef54c4b with x1, x3 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H13.
The subproof is completed by applying H7.
■