cl2casl_compact.clif revision 7cf538c8e2119b185da357ec8dc6457341b3302b
e808b8824ca1091c8efb5669db9129e68e5e1c14Satyen Desai(cl-text prop
e808b8824ca1091c8efb5669db9129e68e5e1c14Satyen Desai (thisMustBeTrue)
e808b8824ca1091c8efb5669db9129e68e5e1c14Satyen Desai (and (a) (b) (not (c)))
e808b8824ca1091c8efb5669db9129e68e5e1c14Satyen Desai (or (d) (e) (not (f)))
e808b8824ca1091c8efb5669db9129e68e5e1c14Satyen Desai(cl-text pred
e808b8824ca1091c8efb5669db9129e68e5e1c14Satyen Desai(cl-text quant
e808b8824ca1091c8efb5669db9129e68e5e1c14Satyen Desai (forall (x y z) (and (P x) (P y) (not (P z))))
e808b8824ca1091c8efb5669db9129e68e5e1c14Satyen Desai (exists (x) (P x))
e808b8824ca1091c8efb5669db9129e68e5e1c14Satyen Desai(cl-text compact
e808b8824ca1091c8efb5669db9129e68e5e1c14Satyen Desai (forall (P) (P h))
e808b8824ca1091c8efb5669db9129e68e5e1c14Satyen Desai(cl-text func
e808b8824ca1091c8efb5669db9129e68e5e1c14Satyen Desai (= g (G h i j))
e808b8824ca1091c8efb5669db9129e68e5e1c14Satyen Desai (forall (H I) (= (H g) (I h i)))
e808b8824ca1091c8efb5669db9129e68e5e1c14Satyen Desai (= ((J ((K g) h) i) j) k)