proposition: Lemma decidable_no_copy_succ : decidable_relation legal_config no_copy_succ.
proof: Proof. unfold decidable_relation in |- *. intro. elim x. intros. elim p. intros. generalize (decide_no_copy_successor c l). intro. elim H. intro. elim H0. intros. left. decompose [and] H1. split with (existS legal_as_set (transition c x1) (intro_leg (transition c x1) H3)). unfold no_copy_succ in |- *. unfold get_c in |- *. split with x1. split; auto. intro. right. intro. unfold no_copy_succ in |- *. unfold get_c in |- *. unfold not in |- *; intro. elim H1. intros. decompose [and] H2. apply H4. auto. Qed.
imports: List DistributedReferenceCounting.machine2.invariant8