proposition: Lemma message_clock_ge_one: forall p h s m, (step_star (init p) h s /\ In m (messages s)) -> msg_clock m >= 1.
proof: Proof. intros. destruct H as [H1 H2]. remember (init p) as s0 eqn: Hs. induction H1. subst s. simpl in H2. contradiction. inversion H. rewrite <- H5 in H2. simpl in H2. apply in_app_iff in H2. destruct H2 as [H2 | H2]. apply IHstep_star. assumption. rewrite <- H3. simpl. assumption. apply in_map_iff in H2. destruct H2 as [rn [H21 H22]]. rewrite <- H21. simpl. assert (A1 := Nat.le_0_l c). assert (A2 := proj1 (Nat.add_le_mono_r 0 c 1)). depremise A2. assumption. simpl in A2. assumption. apply IHstep_star. assumption. rewrite <- H5 in H2. simpl in H2. rewrite <- H3. simpl. assumption. apply IHstep_star. assumption. rewrite <- H6 in H2. simpl in H2. rewrite <- H4. simpl. apply in_app_iff in H2. destruct H2. apply in_app_iff. left. assumption. apply in_app_iff. right. apply in_cons. assumption. apply IHstep_star. assumption. rewrite <- H5 in H2. simpl in H2. rewrite <- H3. simpl. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)