proposition: Lemma put_inc_clock: forall (h: list Label)(s s': State)(l l': Label), (step_star s ((l :: h) ++ [l']) s' /\ label_is_put l /\ label_is_put l' /\ label_node l = label_node l') -> label_clock l < label_clock l'.
proof: Proof. intros. open_conjs. apply step_star_app_one in H. destruct H as [s2 [M1 M3]]. apply step_star_end in M1. destruct M1 as [s1 [M1 M2]]. assert (L := clock_inc h s1 s2 M2 (label_node l)). simpl in L. assert (N1 := label_poststate_clock s s1 l (conj M1 H0)). assert (N2 := label_poststate_clock s2 s' l' (conj M3 H1)). rewrite N1; clear N1. rewrite N2; clear N2. rewrite <- H2 in *. assert (M : clock_state (node_states s2 (label_node l)) < clock_state (node_states s' (label_node l))). inversion M3. simpl. rewrite <- H4 in H2. simpl in H2. rewrite H2. simpl_override. simpl_override. simpl. rewrite Nat.add_comm. simpl. apply Nat.lt_succ_diag_r. rewrite <- H4 in H1. unfold label_is_put in H1. contradiction. rewrite <- H5 in H1. unfold label_is_put in H1. contradiction. rewrite <- H4 in H1. unfold label_is_put in H1. contradiction. eapply Nat.le_lt_trans; eassumption. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)