discrete_partial.clif

(cl-text http://colore.oor.net/orderings/discrete_partial.clif

(cl-imports http://colore.oor.net/orderings/partial_ordering.clif)

(cl-comment "Downwards discreteness")
(forall (x y)
	(if	(lt x y)
		(exists (z)
			(and	(covers y z)
				(leq x z)))))

(cl-comment "Upwards discreteness")
(forall (x y)
	(if	(lt x y)
		(exists (z)
			(and	(covers z x)
				(leq z y)))))

(forall (x y)
(iff	(covers y x)
	(and	(lt x y)
		(not (exists (z)
			(and	(lt x z)
				(lt z y)))))))

)