Theorem([arbitrary(E,A,B,C), equiangle(B,C,E,E,C,A), intersection(E,C,B,D,F), equidistance(E,C,B,D), equiangle(A,B,D,D,B,C), equidistance(C,A,B,A), equidistance(F,C,B,F), online(A,C,D), online(B,A,E)],[equidistance(E,F,F,D)]) Warning: the coordinates of the points from {A, B, C, D, E, F} are reassigned Theorem: If the points E, A, B, and C are arbitrary, the angle BCE is equal to the angle ECA, the two lines EC and BD intersect at F, the distance between E and C is equal to the distance between B and D, the angle ABD is equal to the angle DBC, the distance between C and A is equal to the distance between B and A, the distance between F and C is equal to the distance between B and F, the point D is on the line AC, and the point E is on the line BA, then the distance between E and F is equal to the distance between F and D. Proof: Status: used = 798, alloced = 3072, time = 4.336 char set produced: [14 u3 4] [1 v1 1] [13 v2 1] [34 x1 1] [4 y1 1] [11 x2 1] [4 y2 1] char set recomputed: [7 u3 3] [1 v1 1] [1 v2 1] [11 x1 2] [4 y1 1] [5 x2 1] [4 y2 1] pseudo-remainder: [6 y2 1] = 2*y2*y1 + ... (5 terms) pseudo-remainder: [12 x2 1] = 2*u1^2*x2 + ... (11 terms) pseudo-remainder: [21 y1 2] = u1^2*y1^2 + ... (20 terms) pseudo-remainder: [30 x1 2] = u1*u2^2*x1^2 + ... (29 terms) pseudo-remainder: [47 v2 2] = -u1^3*u2^2*v2^2 + ... (46 terms) pseudo-remainder: [21 v1 0] = 2*u1^3*u2^2*u3 + ... (20 terms) pseudo-remainder: [16 u3 3] = 2*u1^2*u3^3 + ... (15 terms) the thoerem is possibly false: further decomposition in progress pseudo-remainder: [6 y2 1] = 2*y2*y1 + ... (5 terms) pseudo-remainder: [12 x2 1] = 2*u1^2*x2 + ... (11 terms) pseudo-remainder: [13 y1 2] = u1^2*y1^2 + ... (12 terms) pseudo-remainder: [11 x1 2] = u1^2*u2^2*x1^2 + ... (10 terms) pseudo-remainder: [8 v2 2] = 4*u1^5*v2^2 + ... (7 terms) char set produced: [1 O 0] char set produced: [2 u3 1] [1 v1 1] [1 v2 1] [4 x1 2] [1 y1 1] [2 x2 1] [1 y2 1] pseudo-remainder: [6 y2 1] = 2*y2*y1 + ... (5 terms) pseudo-remainder: [5 x2 1] = -2*u1*x2 + ... (4 terms) pseudo-remainder: [5 y1 2] = y1^2 + ... (4 terms) pseudo-remainder: [4 x1 2] = x1^2 + ... (3 terms) pseudo-remainder: [3 v2 0] = 2*u2*u1 + ... (2 terms) pseudo-remainder: [3 v1 0] = 2*u2*u1 + ... (2 terms) pseudo-remainder: [3 u3 0] = 2*u2*u1 + ... (2 terms) further decomposition in progress 8 Status: used = 3434, alloced = 5506, time = 4.508 char set produced: [3 u2 2] [2 u3 1] [1 v1 1] [4 v2 2] [2 x1 1] [1 x2 1] pseudo-remainder: [6 x2 1] = -2*u1*x2 + ... (5 terms) pseudo-remainder: [4 x1 2] = -x1^2 + ... (3 terms) pseudo-remainder: [4 u2 2] = -u2^2 + ... (3 terms) further decomposition in progress 15 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: [1 O 0] char set produced: [1 O 0] char set produced: [3 u2 2] [2 u3 1] [1 v1 1] [4 v2 2] [2 x1 1] [1 x2 1] char set produced: [1 u3 1] [1 v1 1] [1 v2 1] [2 x1 2] [1 y1 1] [1 y2 1] pseudo-remainder: [6 y2 1] = 2*y2*y1 + ... (5 terms) pseudo-remainder: [5 y1 2] = -y1^2 + ... (4 terms) pseudo-remainder: [4 x1 2] = -x1^2 + ... (3 terms) pseudo-remainder: [2 v2 0] = 2*u1*x2 + ... (1 terms) pseudo-remainder: [2 v1 0] = 2*u1*x2 + ... (1 terms) pseudo-remainder: [2 u3 0] = 2*u1*x2 + ... (1 terms) further decomposition in progress 16 char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [2 u2 1] [2 u3 1] [1 v1 1] [1 v2 1] [2 x1 2] [1 y1 1] [2 x2 1] [1 y2 1] char set produced: [1 O 0] char set produced: [2 u3 1] [1 v1 1] [1 v2 1] [3 x1 1] [1 y1 1] [2 x2 1] [1 y2 1] pseudo-remainder: [6 y2 1] = 2*y2*y1 + ... (5 terms) pseudo-remainder: [5 x2 1] = -2*u1*x2 + ... (4 terms) pseudo-remainder: [5 y1 2] = y1^2 + ... (4 terms) pseudo-remainder: [4 x1 2] = x1^2 + ... (3 terms) pseudo-remainder: [2 v2 0] = -4*u2*u1 + ... (1 terms) pseudo-remainder: [2 v1 0] = -4*u2*u1 + ... (1 terms) pseudo-remainder: [2 u3 0] = -4*u2*u1 + ... (1 terms) further decomposition in progress 15 char set produced: [2 u3 1] [1 v1 1] [1 v2 1] [3 x1 1] [1 y1 1] [2 x2 1] [1 y2 1] pseudo-remainder: [6 y2 1] = 2*y2*y1 + ... (5 terms) pseudo-remainder: [5 x2 1] = -2*u1*x2 + ... (4 terms) pseudo-remainder: [5 y1 2] = y1^2 + ... (4 terms) pseudo-remainder: [4 x1 2] = x1^2 + ... (3 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: [1 O 0] 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: [1 O 0] 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: [1 O 0] 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: [1 O 0] `The theorem is true under the following subsidiary conditions:` . u1-2*u2 <> 0 . the line AE is non-isotropic . the line AE is not perpendicular to the line AB . the line AE is not perpendicular to the line AC . the line AE is not perpendicular to the line CB . the line AE is not perpendicular to the line CE . -2*u2+u1-x1 <> 0 . the line AE is not perpendicular to the line DB QED.
Theorem([arbitrary(A,E,C,B), equiangle(B,C,E,E,C,A), intersection(E,C,B,D,F), equidistance(E,C,B,D), equiangle(A,B,D,D,B,C), equidistance(C,A,B,A), equidistance(F,C,B,F), online(B,A,E), equidistance(E,F,F,D)],[online(A,C,D)]) Warning: the coordinates of the points from {A, B, C, D, E, F} are reassigned Theorem: If the points A, E, C, and B are arbitrary, the angle BCE is equal to the angle ECA, the two lines EC and BD intersect at F, the distance between E and C is equal to the distance between B and D, the angle ABD is equal to the angle DBC, the distance between C and A is equal to the distance between B and A, the distance between F and C is equal to the distance between B and F, the point E is on the line BA, and the distance between E and F is equal to the distance between F and D, then the point D is on the line AC. Proof: char set produced: [9 u3 5] [1 v1 1] [1 v2 1] [11 x1 1] [20 y1 1] [7 x2 1] [3 y2 1] pseudo-remainder: [3 y1 1] = -u1*y1 + ... (2 terms) pseudo-remainder: [22 x1 1] = -2*u1*u2*v1*x1*u3 + ... (21 terms) pseudo-remainder: [45 v2 5] = -v2^5*u2*u1 + ... (44 terms) pseudo-remainder: [6 v1 3] = u2*v1^3 + ... (5 terms) `The theorem is true under the following subsidiary conditions:` . the line AE is non-isotropic . the line CE is non-isotropic . the line AE is not perpendicular to the line CE . u3^2*u2+2*v1^2*u3+2*u2*v2*v1-u2*v1^2-u2*v2^2-2*v2*v1*u3 <> 0 . 2*u1^2*u3-6*u3*u2*u1+u2^2*u1+u1*u3^2+u3*u2^2+2*u3^2*u2-u3^3 <> 0 . the line BC is non-isotropic . the line BC is not perpendicular to the line CE QED.
Theorem([arbitrary(E,A,B,C), equiangle(B,C,E,E,C,A), intersection(E,C,B,D,F), equidistance(E,C,B,D), equiangle(A,B,D,D,B,C), equidistance(C,A,B,A), online(A,C,D), online(B,A,E), equidistance(E,F,F,D)],[equidistance(F,C,B,F)]) Warning: the coordinates of the points from {A, B, C, D, E, F} are reassigned Theorem: If the points E, A, B, and C are arbitrary, the angle BCE is equal to the angle ECA, the two lines EC and BD intersect at F, the distance between E and C is equal to the distance between B and D, the angle ABD is equal to the angle DBC, the distance between C and A is equal to the distance between B and A, the point D is on the line AC, the point E is on the line BA, and the distance between E and F is equal to the distance between F and D, then the distance between F and C is equal to the distance between B and F. Proof: char set produced: [14 u3 4] [1 v1 1] [13 v2 1] [43 x1 1] [4 y1 1] [8 x2 1] [4 y2 1] char set recomputed: [7 u3 3] [1 v1 1] [1 v2 1] [11 x1 2] [4 y1 1] [47 x2 1] [4 y2 1] pseudo-remainder: [6 y2 1] = 2*v1*y2 + ... (5 terms) pseudo-remainder: [11 x2 1] = 2*u1*x2*u3 + ... (10 terms) pseudo-remainder: [155 x1 1] = -2*u3^2*u1^5*u2^2*x1 + ... (154 terms) pseudo-remainder: [155 v2 2] = 2*u1^6*u2^2*v2^2 + ... (154 terms) pseudo-remainder: [84 v1 2] = 2*u1^6*u2^2*v1^2 + ... (83 terms) pseudo-remainder: [30 u3 4] = -2*u1^5*u3^4 + ... (29 terms) the thoerem is possibly false: further decomposition in progress pseudo-remainder: [6 y2 1] = 2*v1*y2 + ... (5 terms) pseudo-remainder: [9 x2 1] = 2*u1*x2*u3 + ... (8 terms) pseudo-remainder: [13 v2 2] = v2^2*u1^2 + ... (12 terms) pseudo-remainder: [26 v1 2] = -4*u1^5*v1^2 + ... (25 terms) pseudo-remainder: [14 u3 2] = 4*u1^5*u3^2 + ... (13 terms) char set produced: [1 O 0] char set produced: [2 u3 1] [1 v1 1] [1 v2 1] [4 x1 2] [1 y1 1] [3 x2 1] pseudo-remainder: [6 x2 1] = -2*x2*u3 + ... (5 terms) pseudo-remainder: [7 x1 1] = u3*x1 + ... (6 terms) pseudo-remainder: [7 v2 2] = -v2^2 + ... (6 terms) pseudo-remainder: [5 v1 2] = v1^2 + ... (4 terms) pseudo-remainder: [3 u3 2] = -u3^2 + ... (2 terms) further decomposition in progress 9 char set produced: [3 u2 2] [2 u3 1] [1 v1 1] [4 v2 2] [2 x1 1] [1 x2 1] pseudo-remainder: [6 x2 1] = -2*x2*u3 + ... (5 terms) pseudo-remainder: [5 v2 2] = v2^2 + ... (4 terms) pseudo-remainder: [10 v1 2] = 2*u1*v1^2 + ... (9 terms) pseudo-remainder: [6 u3 2] = -2*u1*u3^2 + ... (5 terms) pseudo-remainder: [6 u2 3] = 2*u2^3 + ... (5 terms) further decomposition in progress 17 char set produced: [1 O 0] char set produced: [3 u2 2] [4 u3 1] [1 v1 1] [7 v2 2] [12 x1 2] [9 y1 1] [10 x2 1] [13 y2 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: [1 O 0] char set produced: [3 u2 2] [2 u3 1] [1 v1 1] [4 v2 2] [2 x1 1] [1 x2 1] char set produced: [1 u3 1] [1 v1 1] [1 v2 1] [2 x1 2] [1 y1 1] [3 x2 1] pseudo-remainder: [6 x2 1] = -2*x2*u3 + ... (5 terms) pseudo-remainder: [7 x1 1] = u3*x1 + ... (6 terms) pseudo-remainder: [7 v2 2] = -v2^2 + ... (6 terms) pseudo-remainder: [5 v1 2] = v1^2 + ... (4 terms) pseudo-remainder: [3 u3 2] = -u3^2 + ... (2 terms) char set produced: [3 u2 2] [2 u3 1] [1 v1 1] [1 v2 1] [1 x1 1] [1 y1 1] [2 x2 1] [1 y2 1] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [2 u2 1] [2 u3 1] [1 v1 1] [1 v2 1] [2 x1 1] [1 y1 1] [3 x2 1] [1 y2 1] char set produced: [1 O 0] char set produced: [2 u3 1] [1 v1 1] [1 v2 1] [3 x1 1] [1 y1 1] [3 x2 1] [1 y2 1] pseudo-remainder: [6 y2 1] = 2*v1*y2 + ... (5 terms) pseudo-remainder: [4 x2 1] = -2*x2*u3 + ... (3 terms) pseudo-remainder: [5 v2 2] = -v2^2 + ... (4 terms) pseudo-remainder: [4 v1 2] = v1^2 + ... (3 terms) pseudo-remainder: [3 u3 2] = -u3^2 + ... (2 terms) further decomposition in progress 10 char set produced: [2 u3 1] [1 v1 1] [1 v2 1] [3 x1 1] [1 y1 1] [2 x2 1] [1 y2 1] pseudo-remainder: [6 y2 1] = 2*v1*y2 + ... (5 terms) pseudo-remainder: [4 x2 1] = -2*x2*u3 + ... (3 terms) pseudo-remainder: [4 v2 2] = -v2^2 + ... (3 terms) pseudo-remainder: [3 v1 2] = v1^2 + ... (2 terms) pseudo-remainder: [2 u3 2] = -u3^2 + ... (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: [1 O 0] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [3 u2 2] [4 u3 1] [1 v1 1] [2 v2 1] [4 x1 1] [4 x2 1] char set produced: [3 u2 2] [4 u3 1] [1 v1 1] [2 v2 1] [4 x1 1] [4 x2 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: [1 O 0] char set produced: [1 O 0] `The theorem is true under the following subsidiary conditions:` . u1-2*u2 <> 0 . u1^2+2*u2^2-4*u2*u1 <> 0 . the line AE is non-isotropic . the line AE is not perpendicular to the line AB . the line AE is not perpendicular to the line BE . the line AE is not perpendicular to the line AC . the line AE is not perpendicular to the line CB . the line AE is not perpendicular to the line CE . -2*u2+u1-x1 <> 0 . the line AE is not perpendicular to the line DB . the line AE is not perpendicular to the line DE . -u2+u1-x2 <> 0 QED.
Theorem([arbitrary(A,E,B,C), equiangle(B,C,E,E,C,A), intersection(E,C,B,D,F), equidistance(E,C,B,D), equiangle(A,B,D,D,B,C), equidistance(F,C,B,F), online(A,C,D), online(B,A,E), equidistance(E,F,F,D)],[equidistance(C,A,B,A)]) Warning: the coordinates of the points from {A, B, C, D, E, F} are reassigned Theorem: If the points A, E, B, and C are arbitrary, the angle BCE is equal to the angle ECA, the two lines EC and BD intersect at F, the distance between E and C is equal to the distance between B and D, the angle ABD is equal to the angle DBC, the distance between F and C is equal to the distance between B and F, the point D is on the line AC, the point E is on the line BA, and the distance between E and F is equal to the distance between F and D, then the distance between C and A is equal to the distance between B and A. Proof: char set produced: [1 v1 1] [1120 v2 1] [34 x1 1] [4 y1 1] [11 x2 1] [4 y2 1] Status: used = 1234567, alloced = 95305, time = 1031.8060000000003 char set recomputed: [1 v1 1] [1 v2 1] [4 y1 1] [2 x2 1] [4 y2 1] pseudo-remainder: [4 v2 2] = v2^2 + ... (3 terms) pseudo-remainder: [3 v1 2] = -v1^2 + ... (2 terms) the thoerem is possibly false: further decomposition in progress pseudo-remainder: [4 v2 2] = v2^2 + ... (3 terms) pseudo-remainder: [18 v1 2] = 4*v1^2*u1^4 + ... (17 terms) pseudo-remainder: [13 u3 2] = -4*u1^4*u3^2 + ... (12 terms) char set produced: [1 O 0] char set produced: [1 v1 1] [1 v2 1] [3 x1 1] [1 y1 1] [2 x2 1] pseudo-remainder: [4 v2 2] = v2^2 + ... (3 terms) pseudo-remainder: [3 v1 2] = -v1^2 + ... (2 terms) further decomposition in progress 15 pseudo-remainder: [4 v2 2] = v2^2 + ... (3 terms) pseudo-remainder: [3 v1 2] = -v1^2 + ... (2 terms) char set produced: [1 O 0] char set produced: [3 u2 2] [3 u3 2] [1 v1 1] [5 v2 2] [8 x1 1] [7 y1 1] [7 x2 1] [6 y2 1] char set produced: [1 u2 1] [2 u3 1] [1 v1 1] [2 v2 2] [2 x1 1] [2 y1 1] [2 x2 1] [2 y2 1] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [2 u2 1] [2 u3 1] [1 v1 1] [2 x1 1] [2 y1 1] [2 x2 1] [1 y2 1] char set produced: [1 O 0] char set produced: [2 u3 1] [1 v1 1] [5 v2 2] [2 x1 1] [1 y1 1] [2 x2 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: [1 O 0] char set produced: [1 O 0] char set produced: [1 u3 1] [1 v1 1] [1 v2 1] [2 x1 2] [1 y1 1] [3 x2 1] char set produced: [1 O 0] char set produced: [1 v1 1] [1 v2 1] [3 x1 1] [1 y1 1] [2 x2 1] [1 y2 1] char set produced: [1 O 0] char set produced: [2 u3 1] [1 v1 1] [1 v2 1] [3 x1 1] [1 y1 1] [2 x2 1] char set produced: [2 u2 1] [1 v1 1] [1 v2 1] [3 x1 1] [1 y1 1] [2 x2 1] [1 y2 1] char set produced: [1 O 0] `The theorem is true under the following subsidiary conditions:` . u1-2*u2 <> 0 . 2*u1-u2 <> 0 . the three points A, B and E are not collinear . the line AE is non-isotropic . the line AE is not perpendicular to the line AB . the three points A, C and E are not collinear . the line AE is not perpendicular to the line CB . the line AE is not perpendicular to the line CE . the three points A, D and E are not collinear . the line AE is not perpendicular to the line DB . the three points A, E and F are not collinear . x1-u3+u2 <> 0 . -2*x2+u3 <> 0 QED.
Theorem([arbitrary(A,B,E,C), equiangle(B,C,E,E,C,A), intersection(E,C,B,D,F), equidistance(E,C,B,D), equidistance(C,A,B,A), equidistance(F,C,B,F), online(A,C,D), online(B,A,E), equidistance(E,F,F,D)],[equiangle(A,B,D,D,B,C)]) Warning: the coordinates of the points from {A, B, C, D, E, F} are reassigned Theorem: If the points A, B, E, and C are arbitrary, the angle BCE is equal to the angle ECA, the two lines EC and BD intersect at F, the distance between E and C is equal to the distance between B and D, the distance between C and A is equal to the distance between B and A, the distance between F and C is equal to the distance between B and F, the point D is on the line AC, the point E is on the line BA, and the distance between E and F is equal to the distance between F and D, then the angle ABD is equal to the angle DBC. Proof: char set produced: [21 u3 4] [1 v1 1] [14 v2 1] [33 x1 1] [4 y1 1] [8 x2 1] [4 y2 1] char set recomputed: [10 u3 3] [1 v1 1] [1 v2 1] [23 x1 1] [4 y1 1] [3 x2 1] [4 y2 1] pseudo-remainder: [8 y1 2] = -y1^2*v2 + ... (7 terms) pseudo-remainder: [15 x1 2] = v2*x1^2*u1^2 + ... (14 terms) pseudo-remainder: [121 v2 3] = -64*u1^14*u2^2*v2^3 + ... (120 terms) `The theorem is true under the following subsidiary conditions:` . the line BA is non-isotropic . 2*u1-u2 <> 0 . the line AE is not perpendicular to the line AB . -2*u1^2*u3-u2^3+u2^2*u1+2*u1^2*u2 <> 0 . 4*u1^5*u2-4*u1^5*u3+2*u1^4*u2^2+2*u1^4*u2*u3-2*u1^3*u2^2*u3-u1^2*u2^4-u1^2*u2^3*u3-2*u1*u2^5+u2^6+u3*u2^5 <> 0 . the line AB is not perpendicular to the line BC . the line AB is not perpendicular to the line CE . the line AC is not perpendicular to the line AB QED.
Theorem([arbitrary(E,A,B,C), equiangle(B,C,E,E,C,A), intersection(E,C,B,D,F), equiangle(A,B,D,D,B,C), equidistance(C,A,B,A), equidistance(F,C,B,F), online(A,C,D), online(B,A,E), equidistance(E,F,F,D)],[equidistance(E,C,B,D)]) Warning: the coordinates of the points from {A, B, C, D, E, F} are reassigned Theorem: If the points E, A, B, and C are arbitrary, the angle BCE is equal to the angle ECA, the two lines EC and BD intersect at F, the angle ABD is equal to the angle DBC, the distance between C and A is equal to the distance between B and A, the distance between F and C is equal to the distance between B and F, the point D is on the line AC, the point E is on the line BA, and the distance between E and F is equal to the distance between F and D, then the distance between E and C is equal to the distance between B and D. Proof: char set produced: [14 u3 4] [1 v1 1] [13 v2 1] [34 x1 1] [4 y1 1] [11 x2 1] [4 y2 1] char set recomputed: [7 u3 3] [1 v1 1] [1 v2 1] [18 x1 2] [4 y1 1] [5 x2 1] [4 y2 1] pseudo-remainder: [8 y1 2] = -y1^2 + ... (7 terms) pseudo-remainder: [23 x1 2] = -u2^2*x1^2 + ... (22 terms) pseudo-remainder: [59 v2 2] = u1^3*u2^2*v2^2 + ... (58 terms) pseudo-remainder: [25 v1 2] = u2^3*u1*v1^2 + ... (24 terms) pseudo-remainder: [14 u3 3] = -2*u1^2*u3^3 + ... (13 terms) the thoerem is possibly false: further decomposition in progress pseudo-remainder: [8 y1 2] = -y1^2 + ... (7 terms) pseudo-remainder: [9 x1 2] = -u2^2*x1^2 + ... (8 terms) pseudo-remainder: [19 v2 2] = -4*u1^4*v2^2 + ... (18 terms) pseudo-remainder: [24 v1 2] = 4*u2^2*u1^4*v1^2 + ... (23 terms) pseudo-remainder: [13 u3 2] = -4*u1^4*u2*u3^2 + ... (12 terms) char set produced: [1 O 0] char set produced: [2 u3 1] [1 v1 1] [1 v2 1] [3 x1 1] [1 y1 1] [2 x2 1] pseudo-remainder: [8 y1 2] = -y1^2 + ... (7 terms) pseudo-remainder: [6 x1 2] = -x1^2 + ... (5 terms) pseudo-remainder: [6 v2 2] = v2^2 + ... (5 terms) pseudo-remainder: [5 v1 2] = -v1^2 + ... (4 terms) pseudo-remainder: [4 u3 2] = u3^2 + ... (3 terms) char set produced: [3 u2 2] [2 u3 1] [1 v1 1] [4 v2 2] [2 x1 1] [1 x2 1] pseudo-remainder: [8 x1 2] = -x1^2 + ... (7 terms) pseudo-remainder: [8 v2 2] = v2^2 + ... (7 terms) pseudo-remainder: [14 v1 2] = 2*u1*v1^2 + ... (13 terms) pseudo-remainder: [10 u3 2] = -2*u1*u3^2 + ... (9 terms) pseudo-remainder: [5 u2 2] = -4*u2^2*u1 + ... (4 terms) further decomposition in progress 7 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: [1 O 0] char set produced: [1 O 0] char set produced: [3 u2 2] [2 u3 1] [1 v1 1] [4 v2 2] [2 x1 1] [1 x2 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: [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 u2 2] [4 u3 1] [1 v1 1] [2 v2 1] [4 x1 1] [4 x2 1] char set produced: [3 u2 2] [4 u3 1] [1 v1 1] [2 v2 1] [4 x1 1] [4 x2 1] `The theorem is true under the following subsidiary conditions:` . u1-2*u2 <> 0 . the line AE is non-isotropic . the line AE is not perpendicular to the line AB QED.
Theorem([arbitrary(E,C,D,B), intersection(E,C,B,D,F), equidistance(E,C,B,D), equiangle(A,B,D,D,B,C), equidistance(C,A,B,A), equidistance(F,C,B,F), online(A,C,D), online(B,A,E), equidistance(E,F,F,D)],[equiangle(B,C,E,E,C,A)]) Warning: the coordinates of the points from {A, B, C, D, E, F} are reassigned Theorem: If the points E, C, D, and B are arbitrary, the two lines EC and BD intersect at F, the distance between E and C is equal to the distance between B and D, the angle ABD is equal to the angle DBC, the distance between C and A is equal to the distance between B and A, the distance between F and C is equal to the distance between B and F, the point D is on the line AC, the point E is on the line BA, and the distance between E and F is equal to the distance between F and D, then the angle BCE is equal to the angle ECA. Proof: char set produced: [31 u3 11] [6 v1 2] [5 v2 1] [3 x1 1] [1 y1 1] [6 x2 1] [3 y2 1] pseudo-remainder: [4 y2 1] = u2*y2 + ... (3 terms) pseudo-remainder: [6 x2 1] = u2*v1*x2 + ... (5 terms) pseudo-remainder: [6 v2 2] = v2^2*u2^2*u1 + ... (5 terms) pseudo-remainder: [11 v1 6] = 2*u2*v1^6 + ... (10 terms) pseudo-remainder: [10 u3 5] = 4*u1^5*u3^5 + ... (9 terms) the thoerem is possibly false: further decomposition in progress char set produced: [1 O 0] char set produced: [1 u2 1] [1 u3 1] [2 v1 2] [1 v2 1] [1 x1 1] [1 y1 1] [1 x2 1] [1 y2 1] char set produced: [2 u2 1] [2 u3 1] [4 v2 2] [5 x1 1] [7 y1 1] [2 x2 1] [1 y2 1] pseudo-remainder: [4 y2 1] = u2*y2 + ... (3 terms) pseudo-remainder: [2 x2 1] = -v2*x2 + ... (1 terms) pseudo-remainder: [2 v2 1] = v2*u1 + ... (1 terms) pseudo-remainder: [2 u3 0] = v2*u1 + ... (1 terms) pseudo-remainder: [2 u2 1] = -v2*u2 + ... (1 terms) char set produced: [4 u2 3] [2 u3 1] [3 v1 2] [4 v2 1] [2 x1 1] [1 y1 1] [3 x2 1] [3 y2 1] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [2 u2 1] [2 u3 1] [4 v2 2] [5 x1 1] [7 y1 1] [2 x2 1] [1 y2 1] char set produced: [1 O 0] char set produced: [1 O 0] `The theorem is true under the following subsidiary conditions:` . the line CE is not perpendicular to the line CD . the line CE is not perpendicular to the line DE . v1^2-v2*v1+u1^2 <> 0 QED.
