Theorem([arbitrary(C,B,A,D), intersection(C,B,A,D,H), intersection(F,B,E,D,I), online(A,B,E), online(C,D,F), intersection(C,E,A,F,G)],[online(I,H,G)]) Warning: the coordinates of the points from {I, A, B, C, D, E, F, G, H} are reassigned Theorem: If the points C, B, A, and D are arbitrary, the two lines CB and AD intersect at H, `the two lines FB and ED intersect at ` || (I) , the point E is on the line AB, the point F is on the line CD, and the two lines CE and AF intersect at G, then `the point G is on the line ` || (I) || H . Proof: char set produced: [3 x1 1] [1 y1 1] [4 y2 1] [3 y3 1] [12 x4 1] [4 y4 1] [8 x5 1] [4 y5 1] pseudo-remainder: [6 y5 1] = x1*y5 + ... (5 terms) pseudo-remainder: [10 x5 1] = -v1*x5*x1 + ... (9 terms) pseudo-remainder: [22 y4 1] = v1*u1*x2*x1*y4 + ... (21 terms) pseudo-remainder: [42 x4 1] = -u2*v1*u1*y1*x4 + ... (41 terms) pseudo-remainder: [177 y3 2] = u2^2*u3*y3^2*u1*v1 + ... (176 terms) pseudo-remainder: [4 y2 2] = -y2^2*y1 + ... (3 terms) pseudo-remainder: [8 y1 1] = v2*u1*v1*u3*y1 + ... (7 terms) pseudo-remainder: [8 y2 1] = -v1^2*x2*u1*y2*x1 + ... (7 terms) pseudo-remainder: [8 y1 1] = -v1^2*u1*x2*y1 + ... (7 terms) pseudo-remainder: [6 x1 1] = -v1^3*u1*x1 + ... (5 terms) pseudo-remainder: [12 y2 1] = v1^2*y2*u3*x2*u1 + ... (11 terms) pseudo-remainder: [22 y1 1] = -v1^2*u3*y1*u1^2 + ... (21 terms) pseudo-remainder: [16 x1 1] = -v1^3*u1^2*x1 + ... (15 terms) pseudo-remainder: [14 y2 1] = -v1^2*y2*u3*x2*u1 + ... (13 terms) pseudo-remainder: [23 y1 1] = v1^2*u3*y1*u1^2 + ... (22 terms) pseudo-remainder: [16 x1 1] = 2*v1^3*u1^2*x1 + ... (15 terms) pseudo-remainder: [16 y2 2] = v1*y2^2*u1 + ... (15 terms) pseudo-remainder: [35 y1 1] = -v1^2*u3*y1*u1^2 + ... (34 terms) pseudo-remainder: [19 x1 1] = v2*u1^2*v1^2*x1 + ... (18 terms) pseudo-remainder: [19 y2 2] = -v1*y2^2*u1 + ... (18 terms) pseudo-remainder: [36 y1 1] = v1^2*u3*y1*u1^2 + ... (35 terms) pseudo-remainder: [19 x1 1] = -v2*u1^2*v1^2*x1 + ... (18 terms) pseudo-remainder: [20 y2 2] = v1*y2^2*u3*u1 + ... (19 terms) pseudo-remainder: [53 y1 1] = -v1^2*u3*y1*u1^3 + ... (52 terms) pseudo-remainder: [38 x1 1] = -v1^3*u1^3*x1 + ... (37 terms) pseudo-remainder: [21 y2 2] = -v1*y2^2*u1*x1 + ... (20 terms) pseudo-remainder: [28 y1 1] = -v1^2*u1^2*x2*y1 + ... (27 terms) pseudo-remainder: [19 x1 1] = -v1^3*u1^2*x1 + ... (18 terms) pseudo-remainder: [28 y2 2] = -v1*y2^2*u3*u1 + ... (27 terms) pseudo-remainder: [59 y1 1] = v1^2*u3*y1*u1^3 + ... (58 terms) pseudo-remainder: [38 x1 1] = 2*v1^3*u1^3*x1 + ... (37 terms) `The theorem is true under the following subsidiary conditions:` . the line CB is not parallel to the line AD . the line CE is not parallel to the line AF . the line FB is not parallel to the line ED . the line AB is not perpendicular to the line BC . the line BC is not perpendicular to the line CD . the line AF is not perpendicular to the line CB . the line BF is not perpendicular to the line BC QED.
Theorem([arbitrary(C,D,B,A), intersection(C,B,A,D,H), intersection(F,B,E,D,I), online(A,B,E), intersection(C,E,A,F,G), online(I,H,G)],[online(C,D,F)]) Warning: the coordinates of the points from {I, A, B, C, D, E, F, G, H} are reassigned Theorem: If the points C, D, B, and A are arbitrary, the two lines CB and AD intersect at H, `the two lines FB and ED intersect at ` || (I) , the point E is on the line AB, the two lines CE and AF intersect at G, and `the point G is on the line ` || (I) || H , then the point F is on the line CD. Proof: char set produced: [6 x1 1] [3 y1 1] [66 x3 2] [4 y3 1] [8 x4 1] [4 y4 1] [12 x5 1] [6 y5 1] pseudo-remainder: [2 y1 0] = -y2*u1 + ... (1 terms) pseudo-remainder: [2 x1 0] = -y2*u1 + ... (1 terms) the thoerem is possibly false: further decomposition in progress pseudo-remainder: [2 y3 0] = -y2*u1 + ... (1 terms) pseudo-remainder: [2 x3 0] = -y2*u1 + ... (1 terms) pseudo-remainder: [2 y1 0] = -y2*u1 + ... (1 terms) pseudo-remainder: [2 x1 0] = -y2*u1 + ... (1 terms) char set produced: [1 u1 1] [1 x1 1] [3 y1 1] [2 x3 1] [2 y3 1] [8 x4 1] [8 y4 1] [2 x5 1] [2 y5 1] Status: used = 3370, alloced = 5506, time = 8.594999999999999 char set produced: [1 u3 1] [4 x1 1] [4 y1 1] [1 x3 1] [4 y3 2] [5 x4 1] [6 y4 1] [5 x5 1] [6 y5 1] char set produced: [6 x1 1] [5 y1 1] [1 x2 1] [2 x3 1] [2 y3 1] [1 x4 1] [3 y4 1] [2 x5 1] [2 y5 1] char set produced: [6 x1 1] [5 y1 1] [1 x3 1] [2 y3 1] [1 x4 1] [2 y4 1] [8 x5 1] [8 y5 1] pseudo-remainder: [2 y4 0] = -y2*u1 + ... (1 terms) pseudo-remainder: [2 x4 0] = -y2*u1 + ... (1 terms) pseudo-remainder: [2 y3 0] = -y2*u1 + ... (1 terms) pseudo-remainder: [2 x3 0] = -y2*u1 + ... (1 terms) pseudo-remainder: [2 y1 0] = -y2*u1 + ... (1 terms) pseudo-remainder: [2 x1 0] = -y2*u1 + ... (1 terms) the thoerem is possibly false: further decomposition in progress char set produced: [1 O 0] char set produced: [6 x1 1] [5 y1 1] [4 y2 2] [4 y3 1] [10 x4 1] [16 y4 1] [18 x5 1] [20 y5 1] pseudo-remainder: [2 y2 1] = -y2*u1 + ... (1 terms) pseudo-remainder: [2 y1 0] = -y2*u1 + ... (1 terms) pseudo-remainder: [2 x1 0] = -y2*u1 + ... (1 terms) the thoerem is possibly false: further decomposition in progress char set produced: [6 x1 1] [5 y1 1] [2 x2 1] [2 x3 1] [2 y3 1] [8 x4 1] [8 y4 1] [2 x5 1] [2 y5 1] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [6 x1 1] [5 y1 1] [2 x2 1] [1 x3 1] [2 y3 1] [1 x4 1] [2 y4 1] [2 x5 1] [3 y5 1] char set produced: [6 x1 1] [5 y1 1] [3 y2 1] [1 x3 1] [2 y3 1] [1 x4 1] [2 y4 1] [8 x5 1] [11 y5 1] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [6 x1 1] [5 y1 1] [1 y2 1] [4 y3 1] [8 x4 1] [11 y4 1] [14 x5 1] [12 y5 1] pseudo-remainder: [2 y2 1] = -y2*u1 + ... (1 terms) char set produced: [6 x1 1] [5 y1 1] [2 x2 1] [2 x3 1] [2 y3 1] [8 x4 1] [8 y4 1] [2 x5 1] [2 y5 1] char set produced: [6 x1 1] [5 y1 1] [4 y2 1] [4 y3 1] [2 x4 1] [4 y4 1] [2 x5 1] [4 y5 1] pseudo-remainder: [2 y2 1] = -y2*u1 + ... (1 terms) pseudo-remainder: [6 y1 0] = u1*u3*v1 + ... (5 terms) pseudo-remainder: [6 x1 0] = u1*u3*v1 + ... (5 terms) further decomposition in progress 0 char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [8 v2 2] [6 x1 1] [5 y1 1] [4 y2 1] [4 y3 1] [2 x4 1] [4 y4 1] [2 x5 1] [4 y5 1] char set produced: [1 O 0] char set produced: [3 v2 1] [1 x1 1] [2 y1 1] [3 y2 1] [3 y3 1] [3 y4 1] [2 x5 1] [3 y5 1] char set produced: [3 v2 1] [2 x1 1] [3 y1 1] [3 y2 1] [3 y3 1] [2 x4 1] [3 y4 1] [3 y5 1] `The theorem is true under the following subsidiary conditions:` . the line CB is not parallel to the line AD . x4 <> 0 . v1-y4 <> 0 . the line BC is not perpendicular to the line CD . the line AB is not perpendicular to the line CD . x3-x4 <> 0 . the line BE is not parallel to the line DC . the line BE is not perpendicular to the line DC . the line BF is not perpendicular to the line DC . -v1*x3-u3*y4+u3*v1+v2*x3 <> 0 . the line AE is not parallel to the line DC . the line AE is not perpendicular to the line DC . -u2*v1*x4+u2*y2*x4+v1*x4*u3-v1*u3*x2-y2*x4*u3+x2*u2*v1+x2*v2*x4-u2*v2*x2 <> 0 . -u2*v1*y4+u2*y2*y4+u3*v1*y4-y2*u3*y4-v1*v2*x2+x2*v2*y4-u2*v2*y2+u2*v1*v2 <> 0 . the three points A, B and F are not collinear . the three points A, C and F are not collinear . the line AD is not parallel to the line BF . the line AF is not parallel to the line CB . the line AF is not perpendicular to the line DC . the line AG is not parallel to the line DC . the line AG is not perpendicular to the line DC . the line CD is not perpendicular to the line EG . u2*u3*v1-u3*v1*x3-x2*v2*x3+x2*v1*x3-v1*u3*x2 <> 0 . u3^2*v1-x2*v2*x3+v2*u1*u3+x2*v1*x3-u3*v1*x3-v1*u3*x2 <> 0 . -u3*y5-v1*x3+u3*v1+v2*x3 <> 0 . u3*v1*y2-v1*u3*y5+y2*u1*y5-v2*u1*y5-v1*y2*u1+v2*u1*v1+x2*v1*y5-v1*v2*x2 <> 0 . y2*x5*u1-u3*y2*u1-v2*x5*u1+v2*x2*u1+v1*x2*x5-x2*v1*u1-u3*v1*x5+u1*u3*v1 <> 0 QED.
Theorem([arbitrary(B,A,C,D), intersection(C,B,A,D,H), intersection(F,B,E,D,I), online(C,D,F), intersection(C,E,A,F,G), online(I,H,G)],[online(A,B,E)]) Warning: the coordinates of the points from {I, A, B, C, D, E, F, G, H} are reassigned Theorem: If the points B, A, C, and D are arbitrary, the two lines CB and AD intersect at H, `the two lines FB and ED intersect at ` || (I) , the point F is on the line CD, the two lines CE and AF intersect at G, and `the point G is on the line ` || (I) || H , then the point E is on the line AB. Proof: char set produced: [6 x1 1] [3 y1 1] [4 y2 1] [88 y3 2] [12 x4 1] [4 y4 1] [8 x5 1] [4 y5 1] pseudo-remainder: [2 y3 1] = u1*y3 + ... (1 terms) pseudo-remainder: [2 y2 0] = u1*y3 + ... (1 terms) pseudo-remainder: [2 y1 0] = u1*y3 + ... (1 terms) pseudo-remainder: [2 x1 0] = u1*y3 + ... (1 terms) the thoerem is possibly false: further decomposition in progress pseudo-remainder: [2 y3 1] = u1*y3 + ... (1 terms) pseudo-remainder: [6 y2 0] = -u1*u3*v1 + ... (5 terms) pseudo-remainder: [6 y1 0] = -u1*u3*v1 + ... (5 terms) pseudo-remainder: [6 x1 0] = -u1*u3*v1 + ... (5 terms) char set produced: [1 u1 1] [1 x1 1] [3 y1 1] [4 y2 1] [4 y3 1] [2 x4 1] [4 y4 1] [2 x5 1] [4 y5 1] char set produced: [6 x1 1] [5 y1 1] [4 y2 1] [1 x3 1] [1 y3 1] [6 x4 1] [6 y4 1] [1 x5 1] [5 y5 1] char set produced: [6 x1 1] [5 y1 1] [4 y2 1] [1 y3 1] [14 x4 1] [12 y4 1] [8 x5 1] [11 y5 1] pseudo-remainder: [2 y3 1] = u1*y3 + ... (1 terms) char set produced: [1 O 0] char set produced: [6 x1 1] [5 y1 1] [4 y2 1] [2 x3 1] [18 x4 1] [14 y4 1] [10 x5 1] [14 y5 1] pseudo-remainder: [2 x3 0] = u1*y3 + ... (1 terms) pseudo-remainder: [2 y2 0] = u1*y3 + ... (1 terms) pseudo-remainder: [2 y1 0] = u1*y3 + ... (1 terms) pseudo-remainder: [2 x1 0] = u1*y3 + ... (1 terms) further decomposition in progress 2 Status: used = 14179, alloced = 13225, time = 9.391 char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [6 x1 1] [5 y1 1] [1 x2 1] [2 y2 1] [8 x4 1] [8 y4 1] [1 x5 1] [2 y5 1] pseudo-remainder: [2 y2 0] = u1*y3 + ... (1 terms) pseudo-remainder: [2 x2 0] = u1*y3 + ... (1 terms) pseudo-remainder: [2 y1 0] = u1*y3 + ... (1 terms) pseudo-remainder: [2 x1 0] = u1*y3 + ... (1 terms) further decomposition in progress 9 char set produced: [6 x1 1] [5 y1 1] [2 x2 2] [4 y2 1] [18 x4 1] [20 y4 1] [10 x5 1] [16 y5 1] pseudo-remainder: [2 y2 0] = u1*y3 + ... (1 terms) pseudo-remainder: [2 x2 0] = u1*y3 + ... (1 terms) pseudo-remainder: [2 y1 0] = u1*y3 + ... (1 terms) pseudo-remainder: [2 x1 0] = u1*y3 + ... (1 terms) further decomposition in progress 13 char set produced: [6 x1 1] [5 y1 1] [2 x2 1] [4 y2 1] [18 x4 1] [20 y4 1] [10 x5 1] [16 y5 1] pseudo-remainder: [2 y2 0] = u1*y3 + ... (1 terms) pseudo-remainder: [2 x2 0] = u1*y3 + ... (1 terms) pseudo-remainder: [2 y1 0] = u1*y3 + ... (1 terms) pseudo-remainder: [2 x1 0] = u1*y3 + ... (1 terms) further decomposition in progress 17 pseudo-remainder: [2 y2 0] = u1*y3 + ... (1 terms) pseudo-remainder: [2 x2 0] = u1*y3 + ... (1 terms) pseudo-remainder: [2 y1 0] = u1*y3 + ... (1 terms) pseudo-remainder: [2 x1 0] = u1*y3 + ... (1 terms) char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [3 v2 1] [1 x1 1] [2 y1 1] [2 x2 1] [3 y2 1] [2 x3 1] [3 y3 1] [2 x4 1] [1 x5 1] [2 y5 1] char set produced: [6 x1 1] [5 y1 1] [2 x2 1] [2 y2 1] [2 x4 1] [2 y4 1] [8 x5 1] [8 y5 1] char set produced: [6 x1 1] [5 y1 1] [3 x2 1] [1 y2 1] [2 x3 1] [9 y3 1] [2 x4 1] [6 x5 1] [1 y5 1] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [6 x1 1] [5 y1 1] [1 x2 1] [2 y2 1] [2 x3 1] [2 x4 1] [3 y4 1] [1 x5 1] [2 y5 1] char set produced: [6 x1 1] [5 y1 1] [1 x2 1] [2 y2 1] [3 y3 1] [8 x4 1] [11 y4 1] [1 x5 1] [2 y5 1] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [6 x1 1] [5 y1 1] [1 x2 1] [2 y2 1] [8 x4 1] [8 y4 1] [1 x5 1] [2 y5 1] further decomposition in progress 3 char set produced: [1 O 0] char set produced: [6 x1 1] [5 y1 1] [2 x2 1] [4 y2 1] [2 x3 1] [2 x4 1] [8 y4 1] [8 x5 1] [14 y5 1] char set produced: [6 x1 1] [5 y1 1] [2 x2 1] [2 y2 1] [2 x4 1] [2 y4 1] [8 x5 1] [8 y5 1] pseudo-remainder: [2 y4 0] = u1*y3 + ... (1 terms) pseudo-remainder: [2 x4 0] = u1*y3 + ... (1 terms) pseudo-remainder: [2 y2 0] = u1*y3 + ... (1 terms) pseudo-remainder: [2 x2 0] = u1*y3 + ... (1 terms) pseudo-remainder: [2 y1 0] = u1*y3 + ... (1 terms) pseudo-remainder: [2 x1 0] = u1*y3 + ... (1 terms) further decomposition in progress 5 char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [6 x1 1] [5 y1 1] [1 x2 1] [2 y2 1] [2 x3 1] [2 x4 1] [3 y4 1] [1 x5 1] [2 y5 1] char set produced: [6 x1 1] [5 y1 1] [1 x2 1] [2 y2 1] [3 y3 1] [8 x4 1] [11 y4 1] [1 x5 1] [2 y5 1] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [6 x1 1] [5 y1 1] [2 x2 1] [2 y2 1] [4 y3 1] [2 x4 1] [2 y4 1] [14 x5 1] [14 y5 1] `The theorem is true under the following subsidiary conditions:` . the line CB is not parallel to the line AD . the line AB is not perpendicular to the line BC . u3-x4 <> 0 . v2-y4 <> 0 . the three points A, C and D are not collinear . the line AB is not perpendicular to the line CD . the line AB is not perpendicular to the line CE . -x4+x2 <> 0 . the line AB is not parallel to the line CF . the line AB is not perpendicular to the line CF . the line AB is not parallel to the line CG . the line AB is not perpendicular to the line CG . u1*u3*v1+v1*x4*x3+u1*y3*x4-v1*x3*u1-u3*u1*y3+v2*x3*u1-u1*v2*x4-v1*x4*u3 <> 0 . -u3*v1*y4+u3*v1*y3+u1*y3*y4+v1*x3*y4-v1*u1*y3-v2*x3*v1-v2*u1*y4+v2*u1*v1 <> 0 . the three points B, D and E are not collinear . the three points C, D and E are not collinear . the line AD is not parallel to the line CE . the line BC is not parallel to the line DE . the line AB is not perpendicular to the line DE . u3*v1-u3*y4+v2*x2-x2*v1 <> 0 . the line AB is not parallel to the line DF . the line AB is not perpendicular to the line DF . the line AB is not perpendicular to the line FG . u2*u3*v1-u3*v1*x3-x2*v2*x3+x2*v1*x3-v1*u3*x2 <> 0 . u3^2*v1-x2*v2*x3+v2*u1*u3+x2*v1*x3-u3*v1*x3-v1*u3*x2 <> 0 . u2*y3*x5-v1*u2*x5-u3*y3*x5+u3*v1*x5-u3*v1*x3+u2*v1*x3+v2*x5*x3-u2*v2*x3 <> 0 . u2*y3*y5-u2*v1*y5+v1*u3*y5+v2*x3*y5-v2*x3*v1-u3*y3*y5+u2*v1*v2-u2*v2*y3 <> 0 . -x2*v1+u3*v1+v2*x2-u3*y5 <> 0 QED.
