proposition: Lemma put_clock_gtz: forall (p: PProg)(h: list Label)(s: State)(l: Label), (step_star (init p) h s /\ In l h /\ label_is_put l) -> label_clock l > 0.
proof: Proof. intros. open_conjs. induction H. inversion H0. apply in_app_iff in H0. destruct H0. apply IHstep_star in H0. assumption. clear H IHstep_star. unfold In in H0. destruct H0; try contradiction. subst l0. inversion H2. simpl. rewrite Nat.add_comm. simpl. apply Nat.lt_0_succ. rewrite <- H3 in H1. unfold label_is_put in H1. contradiction. rewrite <- H4 in H1. unfold label_is_update in H1. contradiction. rewrite <- H3 in H1. unfold label_is_update in H1. contradiction. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)