proposition: Lemma termination_measure_positive : forall c : Config, (0 <= termination_measure c)%Z.
proof: Proof. unfold termination_measure in |- *. unfold termination_rt_measure, termination_q_measure in |- *. intros. apply add_reduce23. unfold sigma_table in |- *. apply sigma_pos. intros. unfold Z_id in |- *. unfold termination_rt_count in |- *. case (rt c x_). omega. omega. unfold sigma2_table in |- *. unfold sigma_table in |- *. apply sigma_pos. intros. unfold Z_id in |- *. apply sigma_pos. intros. unfold termination_q_count in |- *. apply reduce_positive_or_null. intros. unfold termination_count in |- *. case a. omega. intro; omega. omega. Qed.
imports: List DistributedReferenceCounting.machine2.invariant8