proposition: Lemma prec_in_dep: forall p h0 s1 h s2 l n, let as1 := alg_state (node_states s1 n) in let as2 := alg_state (node_states s2 n) in let lid := (label_node l, label_clock l) in (step_star (init p) h0 s1 /\ step_star s1 h s2 /\ label_is_put l /\ In l h0 /\ (In lid (dep as1) \/ (exists l', let lid' := (label_node l', label_clock l') in label_is_put l' /\ cause h0 l l' /\ In lid' (dep as1) /\ In l' h0))) -> (In lid (dep as2) \/ (exists l', let lid' := (label_node l', label_clock l') in label_is_put l' /\ cause (h0++h) l l' /\ In lid' (dep as2) /\ In l' (h0++h))).
proof: Proof. intros. destruct H as [N1 [N2 [N3 [N4 N5]]]]. induction N2 as [s1 | s1 h s2 lc s3 N21 N22 N23]. subst as1. subst as2. rewrite app_nil_r. destruct N5 as [N5 | N5]. left. assumption. right. destruct N5 as [l' [N51 [N52 [N53 N54]]]]. exists l'. simpl. split_all; assumption. subst as1. subst as2. simpl in N22. depremise N22. assumption. depremise N22. destruct N5 as [N5 | N5]. left. assumption. right. destruct N5 as [l' N5]. simpl in N5. destruct N5 as [N51 [N52 [N53 N54]]]. exists l'. split_all; assumption. clear N5. destruct (eq_nat_dec (label_node lc) n). inversion N23. subst l0. rewrite <- H1 in e. simpl in e. subst n. rewrite <- H0 in N22. simpl in *. simpl_override. simpl. simpl_override_in N22. simpl in N22. right. rewrite H1. exists lc. split_all. subst lc. simpl. apply I. destruct N22 as [N22 | N22]. assert (A1 := in_dep_get_or_put p (h0 ++ h) s2 (label_node lc)). simpl in A1. depremise A1. apply step_star_app. exists s1. split; assumption. specialize (A1 lid). rewrite <- H0 in A1. rewrite <- H1 in A1. simpl in A1. simpl_override_in A1. simpl in A1. depremise A1. assumption. destruct A1 as [A1 | A1]. destruct A1 as [l' [l'' [A11 [A12 [A13 [A14 [A15 A16]]]]]]]. assert (A2: l' = l). eapply put_unique. split_all. eapply step_star_app. exists s1. split. eassumption. eassumption. apply cause_in in A16. destruct A16. assumption. apply in_app_iff. left. assumption. assumption. assumption. assumption. assumption. subst l'. assert (A3: cause (h0 ++ h ++ [lc]) l'' lc). assert (B1 := cause_in (h0 ++ h) l l''). depremise B1. assumption. destruct B1 as [_ B1]. apply in_split in B1. destruct B1 as [l1 [l2 B1]]. apply cause_cause_step. unfold cause_step. left. split_all. unfold prec. rewrite app_assoc. rewrite B1. exists l1. exists l2. exists nil. rewrite app_assoc. reflexivity. subst lc. simpl. assumption. left. split. assumption. subst lc. simpl. apply I. eapply cause_cause_trans. split. rewrite app_assoc. apply cause_ext_cause. eassumption. assumption. destruct A1 as [l' [A11 [A12 [A13 [A14 A15]]]]]. assert (A2: l' = l). eapply put_unique. split_all. eapply step_star_app. exists s1. split. eassumption. eassumption. assumption. apply in_app_iff. left. assumption. assumption. assumption. assumption. assumption. subst l'. apply cause_cause_step. unfold cause_step. left. split_all. apply in_split in A15. destruct A15 as [l1 [l2 A15]]. rewrite app_assoc. rewrite A15. unfold prec. exists l1. exists l2. exists nil. rewrite app_assoc. reflexivity. subst lc. simpl. assumption. right. split. assumption. subst lc. simpl. apply I. destruct N22 as [lm [N221 [N222 [N223 N224]]]]. assert (A1 := in_dep_get_or_put p (h0 ++ h) s2 (label_node lc)). simpl in A1. depremise A1. apply step_star_app. exists s1. split; assumption. specialize (A1 (label_node lm, label_clock lm)). rewrite <- H0 in A1. rewrite <- H1 in A1. simpl in A1. simpl_override_in A1. simpl in A1. depremise A1. assumption. destruct A1 as [A1 | A1]. destruct A1 as [l' [l'' [A11 [A12 [A13 [A14 [A15 A16]]]]]]]. assert (A2: l' = lm). eapply put_unique. split_all. eapply step_star_app. exists s1. split. eassumption. eassumption. apply cause_in in A16. destruct A16. assumption. eapply prec_in. eapply cause_prec. split. apply step_star_app. exists s1. split; eassumption. eassumption. assumption. assumption. assumption. assumption. subst l'. assert (A3: cause (h0 ++ h ++ [lc]) l'' lc). assert (B1 := cause_in (h0 ++ h) lm l''). depremise B1. assumption. destruct B1 as [_ B1]. apply in_split in B1. destruct B1 as [l1 [l2 B1]]. apply cause_cause_step. unfold cause_step. left. split_all. unfold prec. rewrite app_assoc. rewrite B1. exists l1. exists l2. exists nil. rewrite app_assoc. reflexivity. subst lc. simpl. assumption. left. split. assumption. subst lc. simpl. apply I. eapply cause_cause_trans. split. rewrite app_assoc. apply cause_ext_cause. eassumption. eapply cause_cause_trans. split. rewrite app_assoc. apply cause_ext_cause. eassumption. eassumption. destruct A1 as [l' [A11 [A12 [A13 [A14 A15]]]]]. assert (A2: l' = lm). eapply put_unique. split_all. eapply step_star_app. exists s1. split. eassumption. eassumption. assumption. eapply cause_in. eassumption. assumption. assumption. assumption. assumption. subst l'. assert (A3: cause (h0 ++ h ++ [lc]) lm lc). apply cause_cause_step. unfold cause_step. left. split_all. apply in_split in A15. destruct A15 as [l1 [l2 A15]]. rewrite app_assoc. rewrite A15. unfold prec. exists l1. exists l2. exists nil. rewrite app_assoc. reflexivity. subst lc. simpl. assumption. right. split. assumption. subst lc. simpl. apply I. eapply cause_cause_trans. split. rewrite app_assoc. apply cause_ext_cause. eassumption. eassumption. left. rewrite <- H1. simpl. assert (A1 := sem_clock_alg_state_clock p (h0++h) s2 n0). depremise A1. apply step_star_app. exists s1. split; assumption. simpl in A1. rewrite <- H0 in A1. simpl in A1. simpl_override_in A1. simpl in A1. rewrite A1. reflexivity. rewrite app_assoc. apply in_app_iff. right. apply in_eq. simpl in *. rewrite <- H1 in e. simpl in e. subst n. simpl_override. simpl. rewrite <- H0 in N22. simpl in N22. simpl_override_in N22. simpl in N22. destruct N22 as [N22 | N22]. left. destruct (entry_node (store s k) <>? init_nid). apply in_cons. assumption. assumption. right. destruct N22 as [l' [N221 [N222 [N223 N224]]]]. exists l'. split_all. assumption. rewrite H1. rewrite app_assoc. apply cause_ext_cause. assumption. destruct (entry_node (store s k) <>? init_nid). apply in_cons. assumption. assumption. rewrite app_assoc. apply in_app_iff. left. assumption. simpl. rewrite <- H2 in e. simpl in e. subst n. simpl_override. simpl. rewrite <- H1 in N22. simpl in N22. simpl_override_in N22. simpl in N22. destruct N22 as [N22 | N22]. left. assumption. right. destruct N22 as [l' [N221 [N222 [N223 N224]]]]. exists l'. split_all. assumption. rewrite H2. rewrite app_assoc. eapply cause_ext_cause. assumption. assumption. rewrite app_assoc. apply in_app_iff. left. assumption. simpl in *. rewrite <- H1 in e. simpl in e. subst n. simpl_override. rewrite <- H0 in N22. simpl in N22. simpl_override_in N22. destruct N22 as [N22 | N22]. left. assumption. right. destruct N22 as [l' [N221 [N222 [N223 N224]]]]. exists l'. split_all. assumption. rewrite H1. rewrite app_assoc. apply cause_ext_cause. assumption. assumption. rewrite app_assoc. apply in_app_iff. left. assumption. inversion N23; simpl in *. assert (A: alg_state (node_states s2 n) = alg_state (node_states s3 n)). subst s2. subst s3. simpl. subst. subst. simpl in *. simpl_override. simpl_override. reflexivity. subst lc. simpl_override. rewrite <- H0 in N22. simpl in N22. simpl_override_in N22. destruct N22 as [N22 | N22]. left. assumption. right. destruct N22 as [l'' [N221 [N222 [N223 N224]]]]. exists l''. split_all. assumption. rewrite app_assoc. eapply cause_ext_cause. assumption. assumption. rewrite app_assoc. apply in_app_iff. left. assumption. assert (A: alg_state (node_states s2 n) = alg_state (node_states s3 n)). subst s2. subst s3. simpl. subst. simpl in *. simpl_override. simpl_override. reflexivity. subst lc. simpl_override. rewrite <- H0 in N22. simpl in N22. simpl_override_in N22. destruct N22 as [N22 | N22]. left. assumption. right. destruct N22 as [l'' [N221 [N222 [N223 N224]]]]. exists l''. split_all. assumption. rewrite app_assoc. eapply cause_ext_cause. assumption. assumption. rewrite app_assoc. apply in_app_iff. left. assumption. assert (A: alg_state (node_states s2 n) = alg_state (node_states s3 n)). subst s2. subst s3. simpl. subst. simpl in *. simpl_override. simpl_override. reflexivity. subst lc. simpl_override. rewrite <- H1 in N22. simpl in N22. simpl_override_in N22. destruct N22 as [N22 | N22]. left. assumption. right. destruct N22 as [l'' [N221 [N222 [N223 N224]]]]. exists l''. split_all. assumption. rewrite app_assoc. eapply cause_ext_cause. assumption. assumption. rewrite app_assoc. apply in_app_iff. left. assumption. assert (A: alg_state (node_states s2 n) = alg_state (node_states s3 n)). subst s2. subst s3. simpl. subst. simpl in *. simpl_override. simpl_override. reflexivity. subst lc. simpl_override. rewrite <- H0 in N22. simpl in N22. simpl_override_in N22. destruct N22 as [N22 | N22]. left. assumption. right. destruct N22 as [l'' [N221 [N222 [N223 N224]]]]. exists l''. split_all. assumption. rewrite app_assoc. eapply cause_ext_cause. assumption. assumption. rewrite app_assoc. apply in_app_iff. left. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)