[STATEMENT]
lemma pos_ord_acyclic:
  shows "acyclic (pos_ord C t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. acyclic (pos_ord C t)
[PROOF STEP]
by (simp add: acyclic_irrefl pos_ord_irrefl pos_ord_trans)