Theorems

1. Theorem([arbitrary(A,D,B), perpendicular(D,B,A,D), equidistance(C,B,C,D), midpoint(B,A,C)],[midpoint(B,A,C)])
   Warning: the coordinates of the points from {A, B, C, D} are reassigned
   
   
   Theorem: If the points A, D, and B are arbitrary, the line DB is perpendicular to the line AD, the distance between C and B is equal to the distance between C and D, and C is the midpoint of B and A, then C is the midpoint of B and A.
   
   Proof:
   
   char set produced: [2 x1 1] [2 y1 1]
   pseudo-remainder: [2 x1 1] = 2*x1 + ... (1 terms)
   pseudo-remainder: [2 y1 1] = 2*y1 + ... (1 terms)
   
   `The theorem is true.`
   
   QED.


2. Theorem([arbitrary(D,B,C), equidistance(C,B,C,D), midpoint(B,A,C), midpoint(B,A,C)],[perpendicular(D,B,A,D)])
   Warning: the coordinates of the points from {A, B, C, D} are reassigned
   
   
   Theorem: If the points D, B, and C are arbitrary, the distance between C and B is equal to the distance between C and D, C is the midpoint of B and A, and C is the midpoint of B and A, then the line DB is perpendicular to the line AD.
   
   Proof:
   
   char set produced: [2 u2 2] [2 x1 1] [2 y1 1]
   pseudo-remainder: [4 x1 1] = x1*u1 + ... (3 terms)
   pseudo-remainder: [2 u2 2] = -u2^2 + ... (1 terms)
   
   `The theorem is true.`
   
   QED.