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