proposition: Lemma algrec_step: forall p h s l s', (ICExec.StepStar.step_star (ICExec.init p) h s /\ ICExec.step s l s') -> (((ICExec.label_is_get l -> let n := ICExec.label_node l in forall n', algrec (ICExec.alg_state (ICExec.node_states s n)) n' = algrec (ICExec.alg_state (ICExec.node_states s' n)) n')) /\ (ICExec.label_is_put l -> let n := ICExec.label_node l in algrec (ICExec.alg_state (ICExec.node_states s' n)) n = S (algrec (ICExec.alg_state (ICExec.node_states s n)) n) /\ forall n', (not (n' = n) -> algrec (ICExec.alg_state (ICExec.node_states s n)) n' = algrec (ICExec.alg_state (ICExec.node_states s' n)) n')) /\ (ICExec.label_is_update l -> (let n := ICExec.label_node l in let n' := ICExec.label_orig_node l in let c' := ICExec.label_clock l in S (algrec (ICExec.alg_state (ICExec.node_states s n)) n') = c' /\ algrec (ICExec.alg_state (ICExec.node_states s' n)) n' = c' /\ (forall n'', not (n'' = label_orig_node l) -> algrec (ICExec.alg_state (ICExec.node_states s n)) n'' = algrec (ICExec.alg_state (ICExec.node_states s' n)) n'')))).
proof: Proof. intros. destruct H as [H0 H1]. split_all. intros. unfold algrec. destruct l; try contradiction. simpl in *. clear H. subst n. inversion H1. simpl. simpl_override. simpl_override. subst a. reflexivity. intros. unfold algrec. destruct l; try contradiction. simpl in *. clear H. subst n. inversion H1. simpl. simpl_override. simpl_override. split. subst a. rewrite Nat.add_comm. simpl. f_equal. assert (A := rec_eq_clock). specex A. simpl in A. depremise A. eassumption. instantiate (1 := n1) in A. subv_in s A. subv_in n A. simpl_override_in A. symmetry. assumption. intros. subst a. rewrite <- H4 in *. simpl_override. reflexivity. intros. unfold algrec. destruct l; try contradiction. simpl in *. clear H. subst n. subst n'. subst c'. inversion H1. simpl. simpl_override. simpl_override. subst a. subst c. split_all. assert (A := received_plus_one_eq_message_clock). specex_deprem A. split_all. eassumption. eassumption. simpl. apply I. simpl in A. subv_in s A. subv_in m A. subv_in n2 A. simpl_override_in A. rewrite Nat.add_comm in A. simpl in A. assumption. assert (A := message_update_node_clock_eq). specex A. simpl in A. depremise A. split_all. eassumption. subv s. apply in_app_iff. right. apply in_eq. simpl in A. destruct A as [A1 A2]. rewrite <- A1. rewrite <- A2. subv n1. simpl_override. reflexivity. intros. assert (A := message_update_node_clock_eq). specex A. simpl in A. depremise A. split_all. eassumption. subv s. apply in_app_iff. right. apply in_eq. simpl in A. destruct A as [A1 A2]. rewrite <- A1. rewrite <- A2. subst n2. rewrite <- H2 in H5. simpl_override. reflexivity. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)