This PR adds a subclass of downward finite partial orders, i.e. partial orders where each element has only a finite number of predecessors. The set of predecessors of an element is also called a principal ideal, so in other words is that partial order should have finite principal ideal. In Coq it is encoded as function pideal : E -> {fset E} together with axiom forall x y : T, x \in (pideal y) = (x <= y).
Moreover, this condition allows us to have upward closure operator up_clos which returns decidable predicate (as opposed to Prop predicate in the general case). In this PR we also prove that up_clos satisfies Kuratowsky closure axioms.
This PR adds a subclass of downward finite partial orders, i.e. partial orders where each element has only a finite number of predecessors. The set of predecessors of an element is also called a principal ideal, so in other words is that partial order should have finite principal ideal. In Coq it is encoded as function
pideal : E -> {fset E}together with axiomforall x y : T, x \in (pideal y) = (x <= y). Moreover, this condition allows us to have upward closure operatorup_closwhich returns decidable predicate (as opposed toProppredicate in the general case). In this PR we also prove thatup_clossatisfies Kuratowsky closure axioms.