Quelle  dags.pvs

dags[T: TYPE+]: THEORY
BEGIN

   IMPORTING paths[T]

   acyclic_digraph: TYPE = {G: digraph | (FORALL (w: Walk(G)): path?(G,w))}

   dag: TYPE = acyclic_digraph

   DG: VAR dag
   dag_no_self_loops: LEMMA FORALL (e: edgetype): edges(DG)(e) IMPLIES
                                  LET (x,y) = e IN x /= y
END dags