proof (prove): step 11 goal (theorem (DRA24_Composition1), 1 subgoal): 1. !!a b c. [| ~ (0 = 0 & 0 = 1); ~ (xc(sp(b)) = xc(ep(b)) & yc(sp(b)) = yc(ep(b))); ~ (xc(sp(c)) = xc(ep(c)) & yc(sp(c)) = yc(ep(c))); False | 0 = 0 & 0 = 0; 0 = 0 & 1 = 1 | 0 = 0 & 1 = 0; False | xc(sp(b)) = xc(sp(b)) & yc(sp(b)) = yc(sp(b)); xc(ep(b)) = xc(ep(b)) & yc(ep(b)) = yc(ep(b)) | xc(ep(b)) = xc(sp(b)) & yc(ep(b)) = yc(sp(b)); False | xc(sp(c)) = xc(sp(c)) & yc(sp(c)) = yc(sp(c)); xc(ep(c)) = xc(ep(c)) & yc(ep(c)) = yc(ep(c)) | xc(ep(c)) = xc(sp(c)) & yc(ep(c)) = yc(sp(c)); 0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c))) --> 0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (0 + - yc(sp(c))) --> 0 < (1 + - 0) * (xc(ep(c)) + - 0) + (0 + - 0) * (yc(ep(c)) + - 0) --> 0 < (1 + - 0) * (xc(sp(c)) + - 0) + (0 + - 0) * (yc(sp(c)) + - 0) --> 0 = xc(sp(c)) & 1 = yc(sp(c)) | 0 = xc(sp(c)) & 0 = yc(sp(c)) | 0 = xc(ep(c)) & 1 = yc(ep(c)) | 0 = xc(ep(c)) & 0 = yc(ep(c)) | xc(ep(c)) = 0 & yc(ep(c)) = 0 | xc(sp(c)) = 0 & yc(sp(c)) = 0 | xc(ep(c)) = 0 & yc(ep(c)) = 1 | xc(sp(c)) = 0 & yc(sp(c)) = 1; (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c))) < 0 --> 0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (0 + - yc(sp(c))) --> 0 < (1 + - 0) * (xc(ep(c)) + - 0) + (0 + - 0) * (yc(ep(c)) + - 0) --> 0 < (1 + - 0) * (xc(sp(c)) + - 0) + (0 + - 0) * (yc(sp(c)) + - 0) --> 0 = xc(sp(c)) & 1 = yc(sp(c)) | 0 = xc(sp(c)) & 0 = yc(sp(c)) | 0 = xc(ep(c)) & 1 = yc(ep(c)) | 0 = xc(ep(c)) & 0 = yc(ep(c)) | xc(ep(c)) = 0 & yc(ep(c)) = 0 | xc(sp(c)) = 0 & yc(sp(c)) = 0 | xc(ep(c)) = 0 & yc(ep(c)) = 1 | xc(sp(c)) = 0 & yc(sp(c)) = 1; 0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c))) --> (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (0 + - yc(sp(c))) < 0 --> 0 < (1 + - 0) * (xc(ep(c)) + - 0) + (0 + - 0) * (yc(ep(c)) + - 0) --> 0 < (1 + - 0) * (xc(sp(c)) + - 0) + (0 + - 0) * (yc(sp(c)) + - 0) --> 0 = xc(sp(c)) & 1 = yc(sp(c)) | 0 = xc(sp(c)) & 0 = yc(sp(c)) | 0 = xc(ep(c)) & 1 = yc(ep(c)) | 0 = xc(ep(c)) & 0 = yc(ep(c)) | xc(ep(c)) = 0 & yc(ep(c)) = 0 | xc(sp(c)) = 0 & yc(sp(c)) = 0 | xc(ep(c)) = 0 & yc(ep(c)) = 1 | xc(sp(c)) = 0 & yc(sp(c)) = 1; (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c))) < 0 --> (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (0 + - yc(sp(c))) < 0 --> 0 < (1 + - 0) * (xc(ep(c)) + - 0) + (0 + - 0) * (yc(ep(c)) + - 0) --> 0 < (1 + - 0) * (xc(sp(c)) + - 0) + (0 + - 0) * (yc(sp(c)) + - 0) --> 0 = xc(sp(c)) & 1 = yc(sp(c)) | 0 = xc(sp(c)) & 0 = yc(sp(c)) | 0 = xc(ep(c)) & 1 = yc(ep(c)) | 0 = xc(ep(c)) & 0 = yc(ep(c)) | xc(ep(c)) = 0 & yc(ep(c)) = 0 | xc(sp(c)) = 0 & yc(sp(c)) = 0 | xc(ep(c)) = 0 & yc(ep(c)) = 1 | xc(sp(c)) = 0 & yc(sp(c)) = 1; 0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c))) --> 0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (0 + - yc(sp(c))) --> (1 + - 0) * (xc(ep(c)) + - 0) + (0 + - 0) * (yc(ep(c)) + - 0) < 0 --> 0 < (1 + - 0) * (xc(sp(c)) + - 0) + (0 + - 0) * (yc(sp(c)) + - 0) --> 0 = xc(sp(c)) & 1 = yc(sp(c)) | 0 = xc(sp(c)) & 0 = yc(sp(c)) | 0 = xc(ep(c)) & 1 = yc(ep(c)) | 0 = xc(ep(c)) & 0 = yc(ep(c)) | xc(ep(c)) = 0 & yc(ep(c)) = 0 | xc(sp(c)) = 0 & yc(sp(c)) = 0 | xc(ep(c)) = 0 & yc(ep(c)) = 1 | xc(sp(c)) = 0 & yc(sp(c)) = 1; 0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c))) --> (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (0 + - yc(sp(c))) < 0 --> (1 + - 0) * (xc(ep(c)) + - 0) + (0 + - 0) * (yc(ep(c)) + - 0) < 0 --> 0 < (1 + - 0) * (xc(sp(c)) + - 0) + (0 + - 0) * (yc(sp(c)) + - 0) --> 0 = xc(sp(c)) & 1 = yc(sp(c)) | 0 = xc(sp(c)) & 0 = yc(sp(c)) | 0 = xc(ep(c)) & 1 = yc(ep(c)) | 0 = xc(ep(c)) & 0 = yc(ep(c)) | xc(ep(c)) = 0 & yc(ep(c)) = 0 | xc(sp(c)) = 0 & yc(sp(c)) = 0 | xc(ep(c)) = 0 & yc(ep(c)) = 1 | xc(sp(c)) = 0 & yc(sp(c)) = 1; (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c))) < 0 --> (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (0 + - yc(sp(c))) < 0 --> (1 + - 0) * (xc(ep(c)) + - 0) + (0 + - 0) * (yc(ep(c)) + - 0) < 0 --> 0 < (1 + - 0) * (xc(sp(c)) + - 0) + (0 + - 0) * (yc(sp(c)) + - 0) --> 0 = xc(sp(c)) & 1 = yc(sp(c)) | 0 = xc(sp(c)) & 0 = yc(sp(c)) | 0 = xc(ep(c)) & 1 = yc(ep(c)) | 0 = xc(ep(c)) & 0 = yc(ep(c)) | xc(ep(c)) = 0 & yc(ep(c)) = 0 | xc(sp(c)) = 0 & yc(sp(c)) = 0 | xc(ep(c)) = 0 & yc(ep(c)) = 1 | xc(sp(c)) = 0 & yc(sp(c)) = 1; 0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c))) --> 0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (0 + - yc(sp(c))) --> 0 < (1 + - 0) * (xc(ep(c)) + - 0) + (0 + - 0) * (yc(ep(c)) + - 0) --> (1 + - 0) * (xc(sp(c)) + - 0) + (0 + - 0) * (yc(sp(c)) + - 0) < 0 --> 0 = xc(sp(c)) & 1 = yc(sp(c)) | 0 = xc(sp(c)) & 0 = yc(sp(c)) | 0 = xc(ep(c)) & 1 = yc(ep(c)) | 0 = xc(ep(c)) & 0 = yc(ep(c)) | xc(ep(c)) = 0 & yc(ep(c)) = 0 | xc(sp(c)) = 0 & yc(sp(c)) = 0 | xc(ep(c)) = 0 & yc(ep(c)) = 1 | xc(sp(c)) = 0 & yc(sp(c)) = 1; (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c))) < 0 --> 0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (0 + - yc(sp(c))) --> 0 < (1 + - 0) * (xc(ep(c)) + - 0) + (0 + - 0) * (yc(ep(c)) + - 0) --> (1 + - 0) * (xc(sp(c)) + - 0) + (0 + - 0) * (yc(sp(c)) + - 0) < 0 --> 0 = xc(sp(c)) & 1 = yc(sp(c)) | 0 = xc(sp(c)) & 0 = yc(sp(c)) | 0 = xc(ep(c)) & 1 = yc(ep(c)) | 0 = xc(ep(c)) & 0 = yc(ep(c)) | xc(ep(c)) = 0 & yc(ep(c)) = 0 | xc(sp(c)) = 0 & yc(sp(c)) = 0 | xc(ep(c)) = 0 & yc(ep(c)) = 1 | xc(sp(c)) = 0 & yc(sp(c)) = 1; (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c))) < 0 --> (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (0 + - yc(sp(c))) < 0 --> 0 < (1 + - 0) * (xc(ep(c)) + - 0) + (0 + - 0) * (yc(ep(c)) + - 0) --> (1 + - 0) * (xc(sp(c)) + - 0) + (0 + - 0) * (yc(sp(c)) + - 0) < 0 --> 0 = xc(sp(c)) & 1 = yc(sp(c)) | 0 = xc(sp(c)) & 0 = yc(sp(c)) | 0 = xc(ep(c)) & 1 = yc(ep(c)) | 0 = xc(ep(c)) & 0 = yc(ep(c)) | xc(ep(c)) = 0 & yc(ep(c)) = 0 | xc(sp(c)) = 0 & yc(sp(c)) = 0 | xc(ep(c)) = 0 & yc(ep(c)) = 1 | xc(sp(c)) = 0 & yc(sp(c)) = 1; 0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c))) --> 0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (0 + - yc(sp(c))) --> (1 + - 0) * (xc(ep(c)) + - 0) + (0 + - 0) * (yc(ep(c)) + - 0) < 0 --> (1 + - 0) * (xc(sp(c)) + - 0) + (0 + - 0) * (yc(sp(c)) + - 0) < 0 --> 0 = xc(sp(c)) & 1 = yc(sp(c)) | 0 = xc(sp(c)) & 0 = yc(sp(c)) | 0 = xc(ep(c)) & 1 = yc(ep(c)) | 0 = xc(ep(c)) & 0 = yc(ep(c)) | xc(ep(c)) = 0 & yc(ep(c)) = 0 | xc(sp(c)) = 0 & yc(sp(c)) = 0 | xc(ep(c)) = 0 & yc(ep(c)) = 1 | xc(sp(c)) = 0 & yc(sp(c)) = 1; (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c))) < 0 --> 0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (0 + - yc(sp(c))) --> (1 + - 0) * (xc(ep(c)) + - 0) + (0 + - 0) * (yc(ep(c)) + - 0) < 0 --> (1 + - 0) * (xc(sp(c)) + - 0) + (0 + - 0) * (yc(sp(c)) + - 0) < 0 --> 0 = xc(sp(c)) & 1 = yc(sp(c)) | 0 = xc(sp(c)) & 0 = yc(sp(c)) | 0 = xc(ep(c)) & 1 = yc(ep(c)) | 0 = xc(ep(c)) & 0 = yc(ep(c)) | xc(ep(c)) = 0 & yc(ep(c)) = 0 | xc(sp(c)) = 0 & yc(sp(c)) = 0 | xc(ep(c)) = 0 & yc(ep(c)) = 1 | xc(sp(c)) = 0 & yc(sp(c)) = 1; 0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c))) --> (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (0 + - yc(sp(c))) < 0 --> (1 + - 0) * (xc(ep(c)) + - 0) + (0 + - 0) * (yc(ep(c)) + - 0) < 0 --> (1 + - 0) * (xc(sp(c)) + - 0) + (0 + - 0) * (yc(sp(c)) + - 0) < 0 --> 0 = xc(sp(c)) & 1 = yc(sp(c)) | 0 = xc(sp(c)) & 0 = yc(sp(c)) | 0 = xc(ep(c)) & 1 = yc(ep(c)) | 0 = xc(ep(c)) & 0 = yc(ep(c)) | xc(ep(c)) = 0 & yc(ep(c)) = 0 | xc(sp(c)) = 0 & yc(sp(c)) = 0 | xc(ep(c)) = 0 & yc(ep(c)) = 1 | xc(sp(c)) = 0 & yc(sp(c)) = 1; (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c))) < 0 --> (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (0 + - yc(sp(c))) < 0 --> (1 + - 0) * (xc(ep(c)) + - 0) + (0 + - 0) * (yc(ep(c)) + - 0) < 0 --> (1 + - 0) * (xc(sp(c)) + - 0) + (0 + - 0) * (yc(sp(c)) + - 0) < 0 --> 0 = xc(sp(c)) & 1 = yc(sp(c)) | 0 = xc(sp(c)) & 0 = yc(sp(c)) | 0 = xc(ep(c)) & 1 = yc(ep(c)) | 0 = xc(ep(c)) & 0 = yc(ep(c)) | xc(ep(c)) = 0 & yc(ep(c)) = 0 | xc(sp(c)) = 0 & yc(sp(c)) = 0 | xc(ep(c)) = 0 & yc(ep(c)) = 1 | xc(sp(c)) = 0 & yc(sp(c)) = 1; xc(sp(c)) = 0 & yc(sp(c)) = 1 --> (yc(ep(c)) + - 1) * (0 + - 0) + (0 + - xc(ep(c))) * (0 + - 1) < 0 --> (1 + - 0) * (xc(ep(c)) + - 0) + (0 + - 0) * (yc(ep(c)) + - 0) < 0 --> False | 0 = xc(ep(c)) & 1 = yc(ep(c)) | 0 = xc(ep(c)) & 0 = yc(ep(c)) | xc(ep(c)) = 0 & yc(ep(c)) = 0 | 0 = 0 & 1 = 0 | xc(ep(c)) = 0 & yc(ep(c)) = 1; xc(sp(c)) = 0 & yc(sp(c)) = 1 --> 0 < (yc(ep(c)) + - 1) * (0 + - 0) + (0 + - xc(ep(c))) * (0 + - 1) --> 0 < (1 + - 0) * (xc(ep(c)) + - 0) + (0 + - 0) * (yc(ep(c)) + - 0) --> False | 0 = xc(ep(c)) & 1 = yc(ep(c)) | 0 = xc(ep(c)) & 0 = yc(ep(c)) | xc(ep(c)) = 0 & yc(ep(c)) = 0 | 0 = 0 & 1 = 0 | xc(ep(c)) = 0 & yc(ep(c)) = 1; xc(ep(c)) = 0 & yc(ep(c)) = 1 --> 0 < (1 + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - 0) * (0 + - yc(sp(c))) --> (1 + - 0) * (xc(sp(c)) + - 0) + (0 + - 0) * (yc(sp(c)) + - 0) < 0 --> 0 = xc(sp(c)) & 1 = yc(sp(c)) | 0 = xc(sp(c)) & 0 = yc(sp(c)) | False | 0 = 0 & 1 = 0 | xc(sp(c)) = 0 & yc(sp(c)) = 0 | xc(sp(c)) = 0 & yc(sp(c)) = 1; xc(ep(c)) = 0 & yc(ep(c)) = 1 --> (1 + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - 0) * (0 + - yc(sp(c))) < 0 --> 0 < (1 + - 0) * (xc(sp(c)) + - 0) + (0 + - 0) * (yc(sp(c)) + - 0) --> 0 = xc(sp(c)) & 1 = yc(sp(c)) | 0 = xc(sp(c)) & 0 = yc(sp(c)) | False | 0 = 0 & 1 = 0 | xc(sp(c)) = 0 & yc(sp(c)) = 0 | xc(sp(c)) = 0 & yc(sp(c)) = 1; 0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c))) --> xc(sp(c)) = 0 & yc(sp(c)) = 0 --> (1 + - 0) * (xc(ep(c)) + - 0) + (0 + - 0) * (yc(ep(c)) + - 0) < 0 --> 0 = 0 & 1 = 0 | 0 = xc(ep(c)) & 1 = yc(ep(c)) | 0 = xc(ep(c)) & 0 = yc(ep(c)) | xc(ep(c)) = 0 & yc(ep(c)) = 0 | xc(ep(c)) = 0 & yc(ep(c)) = 1 | False; (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c))) < 0 --> xc(sp(c)) = 0 & yc(sp(c)) = 0 --> 0 < (1 + - 0) * (xc(ep(c)) + - 0) + (0 + - 0) * (yc(ep(c)) + - 0) --> 0 = 0 & 1 = 0 | 0 = xc(ep(c)) & 1 = yc(ep(c)) | 0 = xc(ep(c)) & 0 = yc(ep(c)) | xc(ep(c)) = 0 & yc(ep(c)) = 0 | xc(ep(c)) = 0 & yc(ep(c)) = 1 | False; (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c))) < 0 --> xc(ep(c)) = 0 & yc(ep(c)) = 0 --> (1 + - 0) * (xc(sp(c)) + - 0) + (0 + - 0) * (yc(sp(c)) + - 0) < 0 --> 0 = xc(sp(c)) & 1 = yc(sp(c)) | 0 = xc(sp(c)) & 0 = yc(sp(c)) | 0 = 0 & 1 = 0 | xc(sp(c)) = 0 & yc(sp(c)) = 0 | False | xc(sp(c)) = 0 & yc(sp(c)) = 1; xc(ep(c)) = 0 & yc(ep(c)) = 1 --> xc(sp(c)) = 0 & yc(sp(c)) = 0 --> 0 = 0 & 1 = 0 | False | 0 = 0 & 1 = 0 | False; xc(sp(a)) = 0; (1 + - 0) * (xc(sp(c)) + - 0) + (0 + - 0) * (yc(sp(c)) + - 0) = 0 --> 0 = xc(sp(c)) & 1 = yc(sp(c)) | 0 = xc(sp(c)) & 0 = yc(sp(c)); 0 < (1 + - 0) * (xc(sp(b)) + - 0) + (0 + - 0) * (yc(sp(b)) + - 0); 0 < (1 + - 0) * (xc(ep(b)) + - 0) + (0 + - 0) * (yc(ep(b)) + - 0); 0 < (yc(ep(b)) + - yc(sp(b))) * (0 + - xc(sp(b))) + (xc(sp(b)) + - xc(ep(b))) * (0 + - yc(sp(b))); 0 < (yc(ep(b)) + - yc(sp(b))) * (0 + - xc(sp(b))) + (xc(sp(b)) + - xc(ep(b))) * (1 + - yc(sp(b))); 0 < (yc(ep(b)) + - yc(sp(b))) * (xc(sp(c)) + - xc(sp(b))) + (xc(sp(b)) + - xc(ep(b))) * (yc(sp(c)) + - yc(sp(b))); 0 < (yc(ep(b)) + - yc(sp(b))) * (xc(ep(c)) + - xc(sp(b))) + (xc(sp(b)) + - xc(ep(b))) * (yc(ep(c)) + - yc(sp(b))); 0 < (yc(ep(c)) + - yc(sp(c))) * (xc(sp(b)) + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (yc(sp(b)) + - yc(sp(c))); 0 < (yc(ep(c)) + - yc(sp(c))) * (xc(ep(b)) + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (yc(ep(b)) + - yc(sp(c))); yc(sp(a)) = 0; (1 + - 0) * (xc(ep(c)) + - 0) + (0 + - 0) * (yc(ep(c)) + - 0) = 0 --> 0 = xc(ep(c)) & 1 = yc(ep(c)) | 0 = xc(ep(c)) & 0 = yc(ep(c)); ~ (0 = xc(sp(b)) & 1 = yc(sp(b))); ~ (0 = xc(sp(b)) & 0 = yc(sp(b))); ~ (0 = xc(ep(b)) & 1 = yc(ep(b))); ~ (0 = xc(ep(b)) & 0 = yc(ep(b))); ~ (xc(ep(b)) = 0 & yc(ep(b)) = 0); ~ (xc(sp(b)) = 0 & yc(sp(b)) = 0); ~ (xc(ep(b)) = 0 & yc(ep(b)) = 1); ~ (xc(sp(b)) = 0 & yc(sp(b)) = 1); ~ (xc(ep(b)) = xc(sp(c)) & yc(ep(b)) = yc(sp(c))); ~ (xc(sp(b)) = xc(sp(c)) & yc(sp(b)) = yc(sp(c))); ~ (xc(ep(b)) = xc(ep(c)) & yc(ep(b)) = yc(ep(c))); ~ (xc(sp(b)) = xc(ep(c)) & yc(sp(b)) = yc(ep(c))); ~ (xc(ep(c)) = xc(sp(b)) & yc(ep(c)) = yc(sp(b))); ~ (xc(sp(c)) = xc(sp(b)) & yc(sp(c)) = yc(sp(b))); ~ (xc(ep(c)) = xc(ep(b)) & yc(ep(c)) = yc(ep(b))); ~ (xc(sp(c)) = xc(ep(b)) & yc(sp(c)) = yc(ep(b))); xc(ep(a)) = 0; yc(ep(a)) = 1; (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (0 + - yc(sp(c))) = 0 --> xc(ep(c)) = 0 & yc(ep(c)) = 0 | xc(sp(c)) = 0 & yc(sp(c)) = 0; (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c))) = 0 --> xc(ep(c)) = 0 & yc(ep(c)) = 1 | xc(sp(c)) = 0 & yc(sp(c)) = 1 |] ==> 0 < (1 + - 0) * (xc(sp(c)) + - 0) + (0 + - 0) * (yc(sp(c)) + - 0) & ~ (0 = xc(sp(c)) & 1 = yc(sp(c))) & ~ (0 = xc(sp(c)) & 0 = yc(sp(c))) & (0 = xc(ep(c)) & 0 = yc(ep(c))) & ~ (0 = xc(ep(c)) & 1 = yc(ep(c))) & (xc(ep(c)) = 0 & yc(ep(c)) = 0) & ~ (xc(sp(c)) = 0 & yc(sp(c)) = 0) & 0 < (yc(ep(c)) + - yc(sp(c))) * (0 + - xc(sp(c))) + (xc(sp(c)) + - xc(ep(c))) * (1 + - yc(sp(c))) & ~ (xc(ep(c)) = 0 & yc(ep(c)) = 1) & ~ (xc(sp(c)) = 0 & yc(sp(c)) = 1)