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. subv n. reflexivity. 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. unfold guard_method in H13. bool_to_prop_in H13. destruct H13 as [_ N]. bool_to_prop_in N. assert (A1 := update_sender_eq_msg_sender). specex_deprem A1. split_all. eassumption. subv s. apply in_app_iff. right. apply in_eq. simpl in A1. assert (A2 := update_dep_eq_msg_clock). specex_deprem A2. split_all. eassumption. subv s. apply in_app_iff. right. apply in_eq. simpl in A2. rewrite A2 in N. rewrite A2. rewrite A1 in N. rewrite A1. rewrite Nat.add_comm in N. simpl in N. subst n'. clear A1 A2. split_all. symmetry. assumption. simpl_override. reflexivity. intros. simpl_override. reflexivity. Qed.
imports: Coq(FunctionalExtensionality List Bool Program.Basics) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs extralib KVStore)