proposition: Lemma step_star_clock_nondec: forall (h: list Label)(s s': State)(n: NId), let sc := clock (alg_state ((node_states s) n)) in let sc' := clock (alg_state ((node_states s') n)) in step_star s h s' -> forall n', sc n' <= sc' n'.
proof: Proof. intros. induction H. apply Nat.le_refl. rename sc' into sc''. pose (sc' := clock (alg_state (node_states s2 n))). assert (sc' n' <= sc'' n'). clear H IHstep_star. subst sc. subst sc'. subst sc''. inversion H0; clear H0; simpl in *. unfold override. unfold key_eq_dec. destruct (eq_nat_dec n n0). simpl. unfold SysPredefs.override. destruct (eq_nat_dec n' n0). subst. rewrite Nat.add_comm. simpl. apply Nat.le_succ_diag_r. apply Nat.le_refl. apply Nat.le_refl. unfold override. unfold key_eq_dec. destruct (eq_nat_dec n n0). simpl. apply Nat.le_refl. apply Nat.le_refl. unfold override. destruct (n =_? n0). simpl. unfold override. destruct (n' =_? (sender_node u)). subst. unfold guard_method in H1. bool_to_prop_in H1. destruct H1 as [H1 H2]. bool_to_prop_in H1. rewrite H1. rewrite Nat.add_comm. simpl. apply Nat.le_succ_diag_r. apply Nat.le_refl. apply Nat.le_refl. destruct (eq_nat_dec n n0). simpl_override. simpl_override. apply Nat.le_refl. simpl_override. simpl_override. apply Nat.le_refl. apply Nat.le_trans with (m := sc' n'); assumption. Qed.
imports: Coq(FunctionalExtensionality Arith List) Coq(Program.Equality ListSet Program.Basics Bool) Coq(Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs KVStore)