Changeset 99 in CGBLisp

Timestamp:

Feb 2, 2009, 9:00:58 PM (15 years ago)

Author:

Marek Rychlik

Message:

* empty log message *

File:

• trunk/examples/prover-apollonius.lisp (modified) (1 diff)

trunk/examples/prover-apollonius.lisp

@@ -1 +1 @@
 ;;
-;; Prove Apollonius circle theorem
+;; Prove Apollonius Circle Theorem:
+;;----------------------------------------------------------------
+;; If ABC is a right triangle with hypotenuse BC,
+;; and
 ;;
+;; 1) M is the midpoint of BC;
+;; 2) M1 is the midpoint of AB;
+;; 3) M2 is the midpoint of AC;
+;; 4) is the foot of the altitude dropped from A;
+;;
+;; then A, H, M1, M2 and M lie on the same circle.
+;;----------------------------------------------------------------
+;;
+
 (prove-theorem
- ((perpendicular A B A C)
+
+ ;; If
+ (
+  ;; AB _|_ AC
+  (perpendicular A B A C)
+
+  ;; M is the midpoint of BC
   (midpoint B C M)
+
+  ;; O is the midpoint of AM
   (midpoint A M O)
+
+  ;; H lies on BC
   (collinear B H C)
-  (perpendicular A H B C))
- ((equidistant M O H O)
+
+  ;; AH _|_ BC
+  (perpendicular A H B C)
+
+  )
+
+ ;; Then
+
+ (
+  ;; MO = HO
+  (equidistant M O H O)
+
+  ;; or
+
+  ;; B = C
   (identical-points B C)
-  ))
+
+  )
+ )