CommonLogic/TestData/partitioning.clf

	partitioning.clf revision dd2cdefff2e823963cde6ec1fb9c28af1b137865
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc(cl-module partitioning.clif
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc(cl-imports weak-tripartite.clif)
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc(cl-comment 'A line is incident with a unique plane.')
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc(forall (x y z)
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc    (if (and    (line x)
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc            (plane y)
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc            (plane z)
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc            (in x y)
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc            (in x z))
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc        (= y z)))
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc(cl-comment 'A line is incident with at most two points.')
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc(forall (x y z w)
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc    (if (and    (line x)
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc            (point y)
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc            (point z)
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc            (point w)
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc            (in y x)
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc            (in z x)
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc            (in w x))
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc        (or (= w z)
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc            (= w y))))
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc(forall (x)
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc    (if (line x)
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc        (exists (y z)
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc            (and    (point y)
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc                (point z)
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc                (in y x)
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc                (in z x)))))
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc
dd2cdefff2e823963cde6ec1fb9c28af1b137865Karl Luc)