bp_dense.clif

(cl-text http://colore.oor.net/timepoints/bp_dense.clif

(cl-imports http://colore.oor.net/timepoints/bp_ordering.clif)

(forall (x y)
	(if	(and	(timepoint x) 
			(timepoint y)
			(before x y))
		(exists (z)
			(and 	(timepoint z) 
				(before x z)
				(before z y)))))
)