# gruninger/colore

updated comments in Ordered Geometry Hierarchies with single quotes

carmenchui committed Jun 20, 2018
1 parent 0e638aa commit 3c7d314fe71a991bcb7c1c632505530db395903e
 @@ -2,17 +2,17 @@ (cl-imports http://colore.oor.net/bipartite_incidence/hilbert_incidence.clif) (cl-comment "If a point p2 is between points p1 and p3, then p2 is also between p3 and p1, and there exists a line containing the points.") (cl-comment 'If a point p2 is between points p1 and p3, then p2 is also between p3 and p1, and there exists a line containing the points.') (forall (p1 p2 p3) (if (and (point p1) (point p2) (point p3) (between p1 p2 p3)) (between p3 p2 p1))) (cl-comment "If a point p2 is between points p1 and p3, then there exists a line containing the points.") (cl-comment 'If a point p2 is between points p1 and p3, then there exists a line containing the points.') (forall (p1 p2 p3) (if (and (point p1) (point p2) @@ -24,8 +24,8 @@ there exists a line containing the points.") (in p2 l) (in p3 l))))) (cl-comment "If p1 and p3 are two points of a straight line, then there exists at least one point p2 lying between p1 and p3.") (cl-comment 'If p1 and p3 are two points of a straight line, then there exists at least one point p2 lying between p1 and p3.') (forall (p1 p3 l) (if (and (point p1) (point p3) @@ -36,8 +36,8 @@ then there exists at least one point p2 lying between p1 and p3.") (and (point p2) (between p1 p2 p3))))) (cl-comment "Of any three points situated on a straight line, there is always one which lies between the other two.") (cl-comment 'Of any three points situated on a straight line, there is always one which lies between the other two.') (forall (p1 p2 p3 l) (if (and (point p1) @@ -51,8 +51,8 @@ there is always one which lies between the other two.") (between p2 p1 p3) (between p1 p3 p2)))) (cl-comment "Of any three points situated on a straight line, there is only one which lies between the other two.") (cl-comment 'Of any three points situated on a straight line, there is only one which lies between the other two.') (forall (p1 p2 p3 l) (if (and (point p1) @@ -62,7 +62,7 @@ there is only one which lies between the other two.") (between p1 p2 p3)) (not (between p1 p3 p2)))) (cl-comment "Paschs Axiom:Let A, B, C be three points not lying in the same straight line and let a be a straight line lying in the plane ABC and not passing through any of the points A, B, C. Then, if the straight line a passes through a point of the segment AB, it will also pass through either a point of the segment BC or a point of the segment AC.") (cl-comment 'Paschs Axiom:Let A, B, C be three points not lying in the same straight line and let a be a straight line lying in the plane ABC and not passing through any of the points A, B, C. Then, if the straight line a passes through a point of the segment AB, it will also pass through either a point of the segment BC or a point of the segment AC.') (forall (p1 p2 p3 p4 l1) (if (and (point p1) (point p2)
 @@ -10,9 +10,9 @@ (cl-text http://colore.oor.net/ordered_incidence_geometry/b_2d (cl-comment "basic axioms of betweenness in 2D incidence geometry") (cl-comment 'basic axioms of betweenness in 2D incidence geometry') (cl-comment "incidence") (cl-comment 'incidence') (forall (x y) (if @@ -25,7 +25,7 @@ ) (cl-comment "B1: outer symmetry") (cl-comment 'B1: outer symmetry') (forall (a b c) (if @@ -35,7 +35,7 @@ ) (cl-comment "B2: strict, i.e. acyclic") (cl-comment 'B2: strict, i.e. acyclic') (forall (a b c) (if @@ -44,7 +44,7 @@ ) ) (cl-comment "B3: linear coherence") (cl-comment 'B3: linear coherence') (forall (a b c p) (iff @@ -69,7 +69,7 @@ ) (cl-comment "B4: Separation") (cl-comment 'B4: Separation') (forall (a b c p l) (if
 @@ -10,12 +10,12 @@ (cl-text http://colore.oor.net/ordered_incidence_geometry/b_3d (cl-comment "basic axioms of betweenness in 3D incidence geometry") (cl-comment 'basic axioms of betweenness in 3D incidence geometry') (cl-comment "sets of points, lines, and planes") (cl-comment 'sets of points, lines, and planes') (cl-comment "I.0b") (cl-comment 'I.0b') (forall (x) (if @@ -48,7 +48,7 @@ ) (cl-comment "I.0c") (cl-comment 'I.0c') (forall (x y) (if @@ -61,7 +61,7 @@ ) (cl-comment "O.1: outer symmetry") (cl-comment 'O.1: outer symmetry') (forall (a b c) (if @@ -71,7 +71,7 @@ ) (cl-comment "O.2: strict, i.e. acyclic") (cl-comment 'O.2: strict, i.e. acyclic') (forall (a b c) (if @@ -80,7 +80,7 @@ ) ) (cl-comment "O.3: linear coherence") (cl-comment 'O.3: linear coherence') (forall (a b c p) (iff @@ -106,7 +106,7 @@ ) (cl-comment "B4: Separation") (cl-comment 'B4: Separation') (forall (a b c p l) (if
 @@ -13,7 +13,7 @@ (cl-imports http://colore.oor.net/ordered_incidence_geometry/b_2d) (cl-comment "separation property") (cl-comment 'separation property') (forall (a b c x) (if @@ -26,7 +26,7 @@ ) (cl-comment "no more than one of three distinct elements is in the middle position") (cl-comment 'no more than one of three distinct elements is in the middle position') (forall (a b c) (if @@ -39,7 +39,7 @@ ) (cl-comment "4") (cl-comment '4') (forall (a b x y) (if @@ -56,7 +56,7 @@ ) (cl-comment "6") (cl-comment '6') (forall (a b x y) (if @@ -73,7 +73,7 @@ ) (cl-comment "outer transitivity") (cl-comment 'outer transitivity') (forall (a b x y) (if @@ -86,7 +86,7 @@ ) (cl-comment "inner transitivity") (cl-comment 'inner transitivity') (forall (a b x y) (if
 @@ -13,7 +13,7 @@ (cl-imports http://colore.oor.net/ordered_incidence_geometry/b_3d) (cl-comment "separation property") (cl-comment 'separation property') (forall (a b c x) (if @@ -26,7 +26,7 @@ ) (cl-comment "no more than one of three distinct elements is in the middle position") (cl-comment 'no more than one of three distinct elements is in the middle position') (forall (a b c) (if @@ -39,7 +39,7 @@ ) (cl-comment "4") (cl-comment '4') (forall (a b x y) (if @@ -56,7 +56,7 @@ ) (cl-comment "6") (cl-comment '6') (forall (a b x y) (if @@ -73,7 +73,7 @@ ) (cl-comment "outer transitivity") (cl-comment 'outer transitivity') (forall (a b x y) (if @@ -86,7 +86,7 @@ ) (cl-comment "inner transitivity") (cl-comment 'inner transitivity') (forall (a b x y) (if
 @@ -33,7 +33,7 @@ ) ) (cl-comment "separation property") (cl-comment 'separation property') (forall (a b c x) (if @@ -46,7 +46,7 @@ ) (cl-comment "no more than one of three distinct elements is in the middle position") (cl-comment 'no more than one of three distinct elements is in the middle position') (forall (a b c) (if @@ -59,7 +59,7 @@ ) (cl-comment "4") (cl-comment '4') (forall (a b x y) (if @@ -76,7 +76,7 @@ ) (cl-comment "6") (cl-comment '6') (forall (a b x y) (if @@ -93,7 +93,7 @@ ) (cl-comment "outer transitivity") (cl-comment 'outer transitivity') (forall (a b x y) (if @@ -106,7 +106,7 @@ ) (cl-comment "inner transitivity") (cl-comment 'inner transitivity') (forall (a b x y) (if
 @@ -13,7 +13,7 @@ (cl-imports http://colore.oor.net/ordered_incidence_geometry/woig) (cl-comment "O.7: outer transitivity") (cl-comment 'O.7: outer transitivity') (forall (a b x y l) (if @@ -31,7 +31,7 @@ ) (cl-comment "O.8: inner transitivity") (cl-comment 'O.8: inner transitivity') (forall (a b x y l) (if @@ -49,7 +49,7 @@ ) (cl-comment "separation property") (cl-comment 'separation property') (forall (a b c x l) (if @@ -67,7 +67,7 @@ ) (cl-comment "no more than one of three distinct elements is in the middle position") (cl-comment 'no more than one of three distinct elements is in the middle position') (forall (a b c) (if @@ -80,7 +80,7 @@ ) (cl-comment "4") (cl-comment '4') (forall (a b x y l) (if @@ -102,7 +102,7 @@ ) (cl-comment "6") (cl-comment '6') (forall (a b x y l) (if 