fact: Definition no_copy_succ (lc2 lc1 : legal_config) := exists t : class_trans (get_c lc1), get_c lc2 = transition (get_c lc1) t /\ ~ copy_p (get_c lc1) t.
imports: List DistributedReferenceCounting.machine2.invariant8