proposition: Lemma no_copy_succ_decreases : relation_decreases legal_config no_copy_succ no_copy_measure.
proof: Proof. unfold relation_decreases in |- *. intro. elim x. intro. intro. elim p. intro; intro; intro. elim y. intro; intro. elim p0. intro; intro. unfold no_copy_succ in |- *. unfold get_c in |- *. intro. unfold no_copy_measure in |- *. elim H. intros. decompose [and] H0. generalize (termination_measure_decreases c0 x2 l0 H2). rewrite <- H1. intro. apply Z_nat_axiom. apply termination_measure_positive. apply termination_measure_positive. auto. Qed.
imports: List DistributedReferenceCounting.machine2.invariant8