proposition: Lemma Refinement': forall p h s, N.ICExec.StepStar.step_star (N.ICExec.init p) h s -> exists h' s', AExec.StepStar.step_star (AExec.init p) h' s' /\ h' = hist_map h /\ (forall n, N.ICExec.clock_state (N.ICExec.node_states s n) = length (AExec.ptrace (s' n))) /\ (forall n, N.ICExec.prog_state (N.ICExec.node_states s n) = AExec.prog (s' n)) /\ (forall m c, let n' := N.ICExec.msg_sender m in let c' := N.ICExec.msg_clock m in let k := N.ICExec.msg_key m in let v := N.ICExec.msg_val m in (In m (N.ICExec.messages s) /\ S c = c' -> let tp := nth c (AExec.ptrace (s' n')) AExec.dummy_t_put in (AExec.t_put_key tp = k /\ AExec.t_put_val tp = v))) /\ (forall n pid, let d := AExec.dep (s' n) in let n' := AExec.put_id_nid pid in let c' := AExec.put_id_clock pid in In pid d -> (exists l' l, N.ICExec.label_node l = n /\ N.ICExec.label_is_get l /\ N.ICExec.label_is_put l' /\ N.ICExec.label_node l' = n' /\ N.ICExec.label_clock l' = c' /\ N.ICExec.cause h l' l) \/ (exists l, N.ICExec.label_node l = n /\ N.ICExec.label_node l = n' /\ N.ICExec.label_clock l = c' /\ N.ICExec.label_is_put l /\ In l h)) /\ (forall l i n' c', let n := N.ICExec.label_node l in let c := N.ICExec.label_clock l in let d := AExec.t_put_dep (nth i (AExec.ptrace (s' n)) AExec.dummy_t_put) in (N.ICExec.label_is_put l /\ In l h /\ S i = c /\ i < length (AExec.ptrace (s' n)) /\ In (AExec.put_id n' c') d) -> exists l', (N.ICExec.label_is_put l' /\ N.ICExec.label_node l' = n' /\ N.ICExec.label_clock l' = c' /\ N.ICExec.cause h l' l)) /\ (forall n n', N.algrec (N.ICExec.alg_state (N.ICExec.node_states s n)) n' = AExec.rec (s' n) n') /\ (forall n k n' c', let n'' := AExec.entry_nid ((AExec.store (s' n)) k) in let c'' := AExec.entry_clock ((AExec.store (s' n)) k) in not (n'' = init_nid) -> exists l, N.ICExec.label_is_put l /\ N.ICExec.label_node l = n'' /\ N.ICExec.label_clock l = c'' /\ In l h /\ let d'' := AExec.entry_dep ((AExec.store (s' n)) k) in In (AExec.put_id n' c') d'' -> (exists l', N.ICExec.label_is_put l' /\ N.ICExec.label_node l' = n' /\ N.ICExec.label_clock l' = c' /\ N.ICExec.cause h l' l)).
proof: Proof. intros. remember (N.ICExec.init p) as s0 eqn: Hs. induction H as [s | s1 h s2 l s3]. exists nil. exists (AExec.init p). subst s. split_all. constructor. simpl. reflexivity. intros. reflexivity. intros. simpl. reflexivity. intros. simpl in H. open_conjs. contradiction. intros. subst d. simpl in *. contradiction. intros. open_conjs. subst d. assert (A := nth_in_or_default). specialize (A AExec.TPut i (AExec.ptrace (AExec.init p n)) AExec.dummy_t_put). destruct A as [A | A]. simpl in A. contradiction. eapply nth_In in H2. instantiate (1 := AExec.dummy_t_put) in H2. rewrite A in H2; clear A. exfalso. simpl in H2. assumption. intros. simpl. assert (A := N.algrec_init). specex A. instantiate (3 := p) in A. instantiate (2 := n) in A. instantiate (1 := n') in A. simpl in A. assumption. intros. exfalso. subst n''. simpl in H. apply H. reflexivity. depremise IHstep_star. assumption. destruct IHstep_star as [h' [s' [N1 [N2 [N3 [N4 [N5 [N6 [N7 [N8 N9]]]]]]]]]]. inversion H0. subst l0. pose (ptrace := AExec.ptrace (s' n)). pose (dep := AExec.dep (s' n)). pose (rec := AExec.rec (s' n)). pose (store := AExec.store (s' n)). pose (ptrace' := ptrace ++ [(AExec.t_put k v dep)]). pose (dep' := (AExec.put_id n (length ptrace')) :: dep). pose (rec' := override rec n (rec n + 1)). pose (store' := override store k (AExec.entry v n (length ptrace') nil)). exists (h' ++ [AExec.put_label n (length ptrace') k v]). exists (override s' n (AExec.node_state p0 ptrace' dep' rec' store')). split_all. clear N2 N3 N5 N6 N7 N8 N9. eapply AExec.StepStar.steps. eassumption. assert (A: s' = override s' n (AExec.node_state (AExec.Syntax.put k v p0) ptrace dep rec store)). apply functional_extensionality. intros. destruct (eq_nat_dec x n). subst x. simpl_override. specialize (N4 n). rewrite <- H2 in N4. simpl in N4. simpl_override_in N4. simpl in N4. destruct (s' n). simpl in N4. subst ptrace. subst dep. subst rec. subst store. subst prog. simpl. reflexivity. simpl_override. reflexivity. rewrite A at 1. clear A. econstructor. assumption. clear N1 N4 N5 N6 N7 N8 N9. rewrite N2. rewrite hist_map_app. simpl. f_equal. f_equal. f_equal. unfold ptrace'. unfold ptrace. rewrite app_length. simpl. f_equal. specex N3. instantiate (1 := n) in N3. subv_in s2 N3. simpl_override_in N3. symmetry. assumption. clear N1 N2 N4 N5 N6 N7 N8. intro. simpl. destruct (eq_nat_dec n0 n). simpl_override. simpl_override. specialize (N3 n). subv_in s2 N3. simpl_override_in N3. subv c. subv ptrace'. rewrite app_length. simpl. reflexivity. simpl_override. simpl_override. specialize (N3 n0). subv_in s2 N3. simpl_override_in N3. assumption. intros. simpl. destruct (eq_nat_dec n0 n). simpl_override. simpl_override. simpl. reflexivity. simpl_override. simpl_override. specialize (N4 n0). rewrite <- H2 in N4. simpl in N4. simpl_override_in N4. assumption. clear N1 N2 N4 N6 N7 N8. intros. simpl in H5. destruct H5 as [N1 N2]. apply in_app_iff in N1. destruct N1 as [N1 | N1]. specialize (N5 m c0). simpl in N5. depremise N5. split. subv s2. assumption. assumption. destruct N5 as [N51 N52]. subst n'. remember (N.ICExec.msg_sender m) as n'. subst c'. remember (N.ICExec.msg_clock m) as c'. subst k0. remember (N.ICExec.msg_key m) as k0. subst v0. remember (N.ICExec.msg_val m) as v0. subst tp. destruct (eq_nat_dec n n'). rewrite <- e0 in N51. rewrite <- e0 in N52. simpl_override. subst ptrace'. subst ptrace. specialize (N3 n). rewrite <- H2 in N3. simpl in N3. simpl_override_in N3. assert (A := N.ICExec.msg_clock_lte_state_clock p h s2 m). simpl in A. depremise A. split. subst s1. assumption. rewrite <- H2. simpl. assumption. rewrite <- H2 in A. simpl in A. subv_in n A. subv_in n' A. simpl_override_in A. subst c'. remember (N.ICExec.msg_clock m) as c'. rewrite <- N2 in A; clear N2. subv_in c A. split. rewrite <- N51. apply f_equal. eapply app_nth1. assumption. rewrite <- N52. apply f_equal. eapply app_nth1. assumption. simpl_override. split; assumption. apply in_map_iff in N1. destruct N1 as [tn [N11 N12]]. subst tp. subst n'. rewrite <- N11. simpl. simpl_override. subst ptrace'. subst ptrace. subst c'. subv_in m N2. rewrite Nat.add_comm in N2. simpl in N2. apply eq_add_S in N2. subst c0. specialize (N3 n). rewrite <- H2 in N3. simpl in N3. simpl_override_in N3. simpl in N3. split. rewrite app_nth2. rewrite N3. rewrite Nat.sub_diag. simpl. subv k0. subv m. reflexivity. subv c. apply Nat.le_refl. rewrite app_nth2. rewrite N3. rewrite Nat.sub_diag. simpl. subv v0. subv m. reflexivity. subv c. apply Nat.le_refl. clear N1 N2 N4 N5 N7 N8. intros. subst d. destruct (eq_nat_dec n0 n). subst n0. simpl_override_in H5. simpl in H5. destruct H5 as [H5 | H5]. right. exists l. split_all. subst l. simpl. reflexivity. subst l. simpl. subst n'. subst pid. simpl. reflexivity. subst l. simpl. subst c'. subst pid. simpl. subst rec. specialize (N3 n). rewrite <- H2 in N3. simpl in N3. simpl_override_in N3. simpl in N3. rewrite N3. unfold ptrace'. unfold ptrace. rewrite app_length. simpl. reflexivity. subst l. simpl. apply I. subst l. apply in_app_iff. right. apply in_eq. specialize (N6 n pid). simpl in N6. subst dep. apply N6 in H5. clear N6. destruct H5. destruct H5 as [l1 [l2 H5]]. open_conjs. left. exists l1. exists l2. subst n'. subst c'. split_all; try assumption. apply N.ICExec.cause_ext_cause. assumption. destruct H5 as [l1 H5]. open_conjs. right. exists l1. subst n'. subst c'. split_all; try assumption. apply in_app_iff. left. assumption. simpl_override_in H5. specialize (N6 n0 pid). simpl in N6. depremise N6. subst dep. assumption. destruct N6 as [N6 | N6]. destruct N6 as [l1 [l2 N6]]. open_conjs. left. exists l1. exists l2. subst n'. subst c'. split_all; try assumption. apply N.ICExec.cause_ext_cause. assumption. destruct N6 as [l1 N6]. open_conjs. right. exists l1. subst n'. subst c'. split_all; try assumption. apply in_app_iff. left. assumption. clear N1 N2 N4 N5 N8. intros l' i n' c'. intros. destruct H5 as [M1 [M2 [M3 [M4 M5]]]]. subst d. destruct (eq_nat_dec n n0). subst n0. rewrite <- e0 in M4. rewrite <- e0 in M5. simpl_override_in M4. simpl_override_in M5. subv_in ptrace' M4. rewrite app_length in M4. simpl in M4. rewrite Nat.add_comm in M4. simpl in M4. apply (proj1 (Nat.lt_succ_r _ _)) in M4. apply le_lt_eq_dec in M4. destruct M4 as [M4 | M4]. specialize (N7 l' i n' c'). simpl in N7. depremise N7. split_all. assumption. apply in_app_iff in M2. destruct M2 as [M2 | M2]. assumption. exfalso. simpl in M2. destruct M2 as [M2 | M2]; try contradiction. unfold c0 in M3. rewrite <- M2 in M3. simpl in M3. rewrite Nat.add_comm in M3. simpl in M3. apply eq_add_S in M3. subst i. subv_in ptrace M4. specex N3. instantiate (1 := n) in N3. subv_in s2 N3. simpl_override_in N3. rewrite N3 in M4. eapply Nat.lt_irrefl. eassumption. assumption. subv_in ptrace M4. subv_in n M4. assumption. subv_in ptrace' M5. rewrite app_nth1 in M5. subv_in ptrace M5. subv_in n M5. assumption. assumption. destruct N7 as [l'' N7]. open_conjs. exists l''. split_all; try assumption. apply N.ICExec.cause_ext_cause. assumption. rewrite H3 in M2. subv_in ptrace M4. specex N3. instantiate (1 := n) in N3. subv_in s2 N3. simpl_override_in N3. rewrite <- N3 in M4. subst i. assert (A := N.ICExec.put_unique). specex_deprem A. split_all. subst s1. instantiate (1 := s3). eapply N.ICExec.StepStar.step_star_app_one. eexists. split. eassumption. eassumption. apply in_app_iff. right. apply in_eq. eassumption. subv l. apply I. eassumption. subv l. eassumption. subv l. subst c0. rewrite PeanoNat.Nat.add_comm. simpl. eassumption. rewrite <- A in *. subv_in ptrace' M5. rewrite app_nth2 in M5. subv_in c M5. rewrite Nat.sub_diag in M5. simpl in M5. subv_in dep M5. specex N6. simpl in N6. depremise N6. eassumption. destruct N6 as [N6 | N6]. destruct N6 as [l_1 [l_2 N6]]. open_conjs. simpl in H8. simpl in H9. exists l_1. split_all. assumption. assumption. assumption. rewrite H3. assert (B: N.ICExec.cause (h++[l]) l_2 l). apply N.ICExec.cause_in in H10. destruct H10 as [_ H10]. constructor. unfold N.ICExec.cause_step. left. split_all. eapply N.ICExec.in_prec. assumption. rewrite H5. assumption. left. split; assumption. eapply N.ICExec.cause_ext_cause in H10. instantiate (1 := [l]) in H10. eapply N.ICExec.cause_cause_trans. split; eassumption. destruct N6 as [l_1 N6]. open_conjs. simpl in H6. simpl in H7. exists l_1. split_all; try assumption. rewrite H3. constructor. unfold N.ICExec.cause_step. left. split_all. eapply N.ICExec.in_prec. assumption. subst l. simpl. assumption. right. split; assumption. subv ptrace. subv c. apply Nat.le_refl. simpl_override_in M4. simpl_override_in M5. specialize (N7 l' i n' c'). simpl in N7. depremise N7. split_all. assumption. apply in_app_iff in M2. destruct M2 as [M2 | M2]. assumption. exfalso. simpl in M2. destruct M2 as [M2 | M2]; try contradiction. apply n1. subv n0. subv l'. reflexivity. assumption. assumption. subst n0. subst c0. assumption. destruct N7 as [l'' N7]. open_conjs. exists l''. split_all; try assumption. apply N.ICExec.cause_ext_cause. assumption. clear N1 N2 N4 N5 N6 N7. intros n1 n2. intros. simpl. destruct (eq_nat_dec n n1). subst n1. simpl_override. simpl_override. unfold rec. assert (A := N.algrec_step). specex_deprem A. subst s1. split; eassumption. destruct A as [_ [A _]]. depremise A. subst l. simpl. apply I. simpl in A. destruct A as [A1 A2]. specialize (A2 n2). subv_in l A1. subv_in l A2. subv_in s2 A1. subv_in s2 A2. subv_in s3 A1. subv_in s3 A2. simpl_override_in A1. simpl_override_in A1. simpl_override_in A2. simpl_override_in A2. specex N8. instantiate (2 := n) in N8. instantiate (1 := n2) in N8. subv_in s2 N8. simpl_override_in N8. unfold rec'. unfold rec. destruct (eq_nat_dec n n2). subst n2. simpl_override. rewrite Nat.add_comm. simpl. rewrite <- N8. rewrite <- A1. reflexivity. simpl_override. rewrite <- N8. symmetry. apply A2. apply not_eq_sym. assumption. simpl_override. simpl_override. specex N8. instantiate (2 := n1) in N8. instantiate (1 := n2) in N8. subv_in s2 N8. simpl_override_in N8. assumption. clear N1 N2 N4 N5 N6 N7 N8. rewrite H3 in *. intros. destruct (eq_nat_dec n0 n). destruct (eq_nat_dec k k0). exists l. split_all. subst l. simpl. apply I. subst l. simpl. subst n''. simpl_override. unfold store'. simpl_override. reflexivity. subst l. simpl. subv c''. simpl_override. unfold store'. simpl_override. unfold ptrace'. unfold ptrace. rewrite app_length. simpl. f_equal. specex N3. instantiate (2 := n0) in N3. subv_in s2 N3. rewrite e0 in N3. simpl_override_in N3. assumption. apply in_app_iff. right. apply in_eq. intros. subv_in d'' H6. exfalso. rewrite e0 in H6. simpl_override_in H6. unfold store' in H6. rewrite e1 in H6. simpl_override_in H6. assumption. specialize (N9 n k0 n' c'). simpl in N9. depremise N9. subv_in n'' H5. rewrite e0 in H5. simpl_override_in H5. unfold store' in H5. simpl_override_in H5. unfold store in H5. assumption. destruct N9 as [l1 N9]. open_conjs. exists l1. split_all; try assumption. subv n''. simpl_override. unfold store'. simpl_override. assumption. subv c''. simpl_override. unfold store'. simpl_override. assumption. apply in_app_iff. left. assumption. intros. depremise H10. subv_in d'' H11. rewrite e0 in H11. simpl_override_in H11. unfold store' in H11. simpl_override_in H11. unfold store in H11. assumption. destruct H10 as [l2 H10]. open_conjs. exists l2. split_all; try assumption. apply N.ICExec.cause_ext_cause. assumption. simpl_override_in H5. specialize (N9 n0 k0 n' c'). simpl in N9. depremise N9. subv_in n'' H5. simpl_override_in H5. assumption. destruct N9 as [l1 N9]. open_conjs. exists l1. split_all; try assumption. subv n''. simpl_override. unfold store'. simpl_override. assumption. subv c''. simpl_override. unfold store'. simpl_override. assumption. apply in_app_iff. left. assumption. intros. depremise H10. subv_in d'' H11. simpl_override_in H11. assumption. destruct H10 as [l2 H10]. open_conjs. exists l2. split_all; try assumption. apply N.ICExec.cause_ext_cause. assumption. pose (ptrace := AExec.ptrace (s' n)). pose (dep := AExec.dep (s' n)). pose (rec := AExec.rec (s' n)). pose (store := AExec.store (s' n)). pose (val := AExec.entry_val (store k)). pose (n'' := AExec.entry_nid (store k)). pose (c'' := AExec.entry_clock (store k)). pose (dep'' := AExec.entry_dep (store k)). pose (dep' := if eq_nat_dec n'' init_nid then dep else dep ++ [AExec.put_id n'' c''] ++ dep''). exists (h' ++ [AExec.get_label n'' c'' n k val]). exists (override s' n (AExec.node_state (p0 val) ptrace dep' rec store)). assert (P: val = v' /\ n'' = n' /\ c'' = c'). unfold val. unfold n''. unfold c''. unfold store. assert (A1 := InstExecToSeqExec). specex_deprem A1. apply N.ICExec.StepStar.step_star_app_one. eexists. split. subst s1. eassumption. eassumption. destruct A1 as [sh' [ss [A11 A12]]]. rewrite A12 in A11. clear A12. rewrite inst_exec_eff_app in A11. apply I.SExec.StepStar.step_star_app_one in A11. destruct A11 as [ssm [A11 A12]]. subv_in l A12. assert (A2 := AbsExecSeqExecStore). specex_deprem A2. split. eassumption. subv h'. rewrite eff_hist_map. eassumption. instantiate (2 := n) in A2. instantiate (2 := k) in A2. inversion A12. subst n0. subst k0. clear H6. subv_in ssm A2. simpl_override_in A2. rewrite H9 in A2. simpl in A2. destruct A2 as [A21 [A22 A23]]. split_all; try assumption. destruct P as [P1 [P2 P3]]. split_all. clear N2 N3 N5 N6 N7 N8 N9. eapply AExec.StepStar.steps. eassumption. assert (A: s' = override s' n (AExec.node_state (AExec.Syntax.get k p0) ptrace dep rec store)). apply functional_extensionality. intros. destruct (eq_nat_dec x n). subst x. simpl_override. specialize (N4 n). rewrite <- H2 in N4. simpl in N4. simpl_override_in N4. simpl in N4. destruct (s' n). simpl in N4. subst ptrace. subst dep. subst rec. subst store. rewrite <- N4. simpl. reflexivity. simpl_override. reflexivity. rewrite A at 1. clear A. econstructor. assumption. clear N3 N4 N5 N6 N7 N8 N9. rewrite N2. rewrite hist_map_app. simpl. f_equal. f_equal. f_equal. assumption. assumption. assumption. clear N1 N2 N4 N5 N6 N7 N8 N9. intro. simpl. destruct (eq_nat_dec n0 n). subst n0. simpl_override. simpl_override. unfold ptrace. specialize (N3 n). subv_in s2 N3. simpl_override_in N3. assumption. simpl_override. simpl_override. specialize (N3 n0). subv_in s2 N3. simpl_override_in N3. assumption. intros. simpl. destruct (eq_nat_dec n0 n). subst n0. simpl_override. simpl_override. subv val. reflexivity. simpl_override. simpl_override. specialize (N4 n0). subv_in s2 N4. simpl in N4. simpl_override_in N4. assumption. clear N1 N2 N4 N6 N7 N8 N9. intros. simpl in H5. destruct H5 as [M1 M2]. specialize (N5 m c0). simpl in N5. depremise N5. split. subv s2. assumption. assumption. destruct N5 as [N51 N52]. subst tp. subst n'0. remember (N.ICExec.msg_sender m) as n'0. subst k0. remember (N.ICExec.msg_key m) as k0. subst v. remember (N.ICExec.msg_val m) as v. destruct (eq_nat_dec n n'0). simpl_override. unfold ptrace. rewrite e0. split; assumption. simpl_override. split; assumption. clear N1 N2 N4 N5 N7 N8. rewrite H3. intros. subst d. destruct (eq_nat_dec n0 n). subst n0. simpl_override_in H5. unfold dep' in H5. destruct (n'' =_? init_nid). unfold dep in H5. specex N6. simpl in N6. depremise N6. eassumption. destruct N6 as [N6 | N6]. destruct N6 as [l1 [l2 N6]]. open_conjs. left. exists l1. exists l2. split_all; try assumption. apply N.ICExec.cause_ext_cause. assumption. destruct N6 as [l1 N6]. open_conjs. right. exists l1. split_all; try assumption. apply in_app_iff. left. assumption. apply in_app_iff in H5. rewrite in_app_iff in H5. simpl in H5. destruct H5. unfold dep in H5. specex N6. simpl in N6. depremise N6. eassumption. destruct N6 as [N6 | N6]. destruct N6 as [l1 [l2 N6]]. open_conjs. left. exists l1. exists l2. split_all; try assumption. apply N.ICExec.cause_ext_cause. assumption. destruct N6 as [l1 N6]. open_conjs. right. exists l1. split_all; try assumption. apply in_app_iff. left. assumption. unfold dep'' in H5. unfold store in H5. specex N9. simpl in N9. depremise N9. instantiate (2 := n). instantiate (1 := k). subst n''. unfold store in *. assumption. destruct N9 as [l' N9]. open_conjs. assert (A: N.ICExec.cause (h ++ [l]) l' l). constructor. unfold N.ICExec.cause_step. right. split_all. apply N.ICExec.in_prec. assumption. assumption. subst l. simpl. apply I. subst l. simpl. rewrite <- P2. subst n''. subst store. assumption. subst l. simpl. rewrite <- P3. subst c''. subst store. assumption. destruct H5 as [[H5 | H5] | H5]; try contradiction. left. exists l'. exists l. split_all. subst l. simpl. reflexivity. subst l. simpl. apply I. assumption. rewrite H7. subst n'0. subst pid. simpl. subst n''. unfold store. reflexivity. rewrite H8. subst c'0. subst pid. simpl. subst n''. unfold store. reflexivity. assumption. left. instantiate (2 := AExec.put_id_nid pid) in H10. instantiate (1 := AExec.put_id_clock pid) in H10. depremise H10. destruct pid. simpl. assumption. destruct H10 as [l'' H10]. open_conjs. exists l''. exists l. split_all. subst l. simpl. reflexivity. subst l. simpl. apply I. assumption. rewrite H11. subst n'0. reflexivity. rewrite H12. subst c'0. reflexivity. eapply N.ICExec.cause_cause_trans. split. eapply N.ICExec.cause_ext_cause. eassumption. assumption. simpl_override_in H5. specialize (N6 n0 pid). simpl in N6. depremise N6. assumption. destruct N6 as [N6 | N6]. destruct N6 as [l1 [l2 N6]]. open_conjs. left. exists l1. exists l2. split_all; try assumption. apply N.ICExec.cause_ext_cause. assumption. destruct N6 as [l1 N6]. open_conjs. right. exists l1. split_all; try assumption. apply in_app_iff. left. assumption. clear N1 N2 N3 N4 N5 N6 N8 N9. rewrite H3 in *. intros l' i n''' c'''. intros. destruct H5 as [M1 [M2 [M3 [M4 M5]]]]. subst d. assert (A2: i < length (AExec.ptrace (s' n0))). clear M5. destruct (eq_nat_dec n n0). rewrite e0 in M4. simpl_override_in M4. unfold ptrace in M4. rewrite e0 in M4. assumption. simpl_override_in M4. assumption. assert (A3: In (AExec.put_id n''' c''') (AExec.t_put_dep (nth i (AExec.ptrace (s' n0)) AExec.dummy_t_put))). clear A2. destruct (eq_nat_dec n n0). rewrite e0 in M5. simpl_override_in M5. unfold ptrace in M5. rewrite e0 in M5. assumption. simpl_override_in M5. assumption. clear M5. specialize (N7 l' i n''' c'''). simpl in N7. depremise N7. split_all. assumption. apply in_app_iff in M2. destruct M2 as [M2 | M2]. assumption. exfalso. simpl in M2. destruct M2 as [M2 | M2]; try contradiction. subv_in l' M1. rewrite <- H3 in M1. simpl in M1. contradiction. assumption. assumption. subst n0. subst c0. assumption. destruct N7 as [l'' N7]. open_conjs. exists l''. split_all; try assumption. apply N.ICExec.cause_ext_cause. assumption. clear N1 N2 N3 N4 N5 N6 N7 N9. intros n1 n2. simpl. specex N8. instantiate (2 := n1) in N8. instantiate (1 := n2) in N8. subv_in s2 N8. assert (A2 := N.algrec_step). specex A2. depremise A2. subst s1. split_all; eassumption. destruct A2 as [A2 _]. depremise A2. subv l. apply I. simpl in A2. subv_in l A2. subv_in s2 A2. subv_in s3 A2. simpl_override_in A2. simpl_override_in A2. destruct (eq_nat_dec n1 n). subst n1. simpl_override. simpl_override. simpl_override_in N8. specialize (A2 n2). eapply eq_trans. symmetry. eassumption. eassumption. simpl_override. simpl_override. simpl_override_in N8. assumption. clear N1 N2 N3 N4 N5 N6 N7 N8. rewrite H3 in *. intros. specialize (N9 n0 k0 n'0 c'0). simpl in N9. depremise N9. subst n''0. destruct (eq_nat_dec n n0). subst n0. simpl_override_in H5. unfold store in H5. assumption. simpl_override_in H5. assumption. destruct (eq_nat_dec n n0). rewrite e0 in *. destruct N9 as [l1 N9]. open_conjs. exists l1. split_all; try assumption. subv n''0. simpl_override. unfold store. rewrite e0. assumption. subv c''0. simpl_override. unfold store. rewrite e0. assumption. apply in_app_iff. left. assumption. intros. depremise H10. subv_in d'' H11. simpl_override_in H11. unfold store in H11. rewrite e0 in *. assumption. destruct H10 as [l2 H10]. open_conjs. exists l2. split_all; try assumption. apply N.ICExec.cause_ext_cause. assumption. destruct N9 as [l1 N9]. open_conjs. exists l1. split_all; try assumption. subv n''0. simpl_override. unfold store. assumption. subv c''0. simpl_override. unfold store. assumption. apply in_app_iff. left. assumption. intros. depremise H10. subv_in d'' H11. simpl_override_in H11. assumption. destruct H10 as [l2 H10]. open_conjs. exists l2. split_all; try assumption. apply N.ICExec.cause_ext_cause. assumption. pose (ptrace_1 := AExec.ptrace (s' n)). pose (dep_1 := AExec.dep (s' n)). pose (rec_1 := AExec.rec (s' n)). pose (store_1 := AExec.store (s' n)). pose (prog_2 := AExec.prog (s' n')). pose (ptrace_2 := AExec.ptrace (s' n')). pose (dep_2 := AExec.dep (s' n')). pose (rec_2 := AExec.rec (s' n')). pose (store_2 := AExec.store (s' n')). pose (ek := AExec.t_put_key (nth (rec_1 n') ptrace_2 AExec.dummy_t_put)). pose (ev := AExec.t_put_val (nth (rec_1 n') ptrace_2 AExec.dummy_t_put)). pose (ed := AExec.t_put_dep (nth (rec_1 n') ptrace_2 AExec.dummy_t_put)). pose (rec_1' := override rec_1 n' ((rec_1 n') + 1)). pose (store_1' := override store_1 ek (AExec.entry ev n' (rec_1' n') ed)). exists (h' ++ [AExec.update_label n' (rec_1' n') n ek ev]). exists (override (override s' n (AExec.node_state p0 ptrace_1 dep_1 rec_1' store_1')) n' (AExec.node_state prog_2 ptrace_2 dep_2 rec_2 store_2)). assert (A1 := N.ICExec.no_self_message). specex_deprem A1. split. subv_in s1 H. eassumption. instantiate (1 := N.ICExec.message n' c' k v u n lp). subv s2. apply in_app_iff. right. apply in_eq. simpl in A1. split_all. clear N2 N5 N6. eapply AExec.StepStar.steps. eassumption. assert (A2: s' = (override (override s' n (AExec.node_state p0 ptrace_1 dep_1 rec_1 store_1)) n' (AExec.node_state prog_2 ptrace_2 dep_2 rec_2 store_2))). apply functional_extensionality. intros. destruct (eq_nat_dec x n). subst x. simpl_override. simpl_override. specialize (N4 n). subv_in s2 N4. simpl_override_in N4. destruct (s' n). simpl in N4. subst ptrace_1. subst dep_1. subst rec_1. subst store_1. subst prog. simpl. reflexivity. destruct (eq_nat_dec x n'). subst x. simpl_override. specialize (N4 n'). subv_in s2 N4. simpl_override_in N4. destruct (s' n'). simpl in N4. subst prog_2. subst ptrace_2. subst dep_2. subst rec_2. subst store_2. simpl. reflexivity. simpl_override. simpl_override. reflexivity. rewrite A2 at 1. clear A2. assert (C: rec_1 n' < length ptrace_2). unfold rec_1. unfold ptrace_2. specialize (N8 n n'). subv_in s2 N8. simpl_override_in N8. assert (A2 := N.algrec_step). specex_deprem A2. subst s1. split_all; eassumption. destruct A2 as [_ [_ A2]]. depremise A2. subv l. apply I. simpl in A2. destruct A2 as [A2 _]. subv_in l A2. subv_in s2 A2. subv_in s3 A2. simpl_override_in A2. simpl_override_in A2. assert (A3 := N.ICExec.msg_clock_lte_state_clock). specex A3. simpl in A3. depremise A3. split. subst s1. eassumption. instantiate (1 := N.ICExec.message n' c' k v u n lp). subv s2. apply in_app_iff. right. apply in_eq. simpl in A3. subv_in s2 A3. simpl_override_in A3. specex N3. instantiate (1 := n') in N3. subv_in s2 N3. simpl_override_in N3. rewrite <- N8. clear N8. rewrite <- N3. clear N3. rewrite <- A2 in A3. clear A2. assumption. econstructor. assumption. apply not_eq_sym. assumption. assumption. apply Forall_forall. intros pid M. assert (A2 := N.ICExec.msg_label_eq_key_val). specex_deprem A2. split. subst s1. eassumption. instantiate (1 := N.ICExec.message n' c' k v u n lp). subv s2. apply in_app_iff. right. apply in_eq. simpl in A2. destruct A2 as [A21 [A22 [A23 [A24 [A25 A26]]]]]. specex N7. simpl in N7. depremise N7. split_all. instantiate (1 := lp). assumption. assumption. instantiate (1 := rec_1 n'). rewrite <- A25. unfold rec_1. subv_in s2 N8. simpl_override_in N8. rewrite <- N8. clear N8. assert (A3 := N.algrec_step). specex_deprem A3. subst s1. split_all; eassumption. destruct A3 as [_ [_ A3]]. depremise A3. subv l. apply I. simpl in A3. destruct A3 as [A3 _]. subv_in s2 A3. subv_in l A3. simpl_override_in A3. simpl_override. assumption. unfold ptrace_2 in C. rewrite <- A24. assumption. instantiate (2 := AExec.put_id_nid pid). instantiate (1 := AExec.put_id_clock pid). subv_in ptrace_2 M. rewrite <- A24. destruct pid. simpl. unfold AExec.put_id. assumption. destruct N7 as [l' [N71 [N72 [N73 N74]]]]. rewrite <- N72. rewrite <- N73. assert (A3 := N.cause_rec). specex A3. simpl in A3. depremise A3. split_all. subst s1. eassumption. eassumption. apply N71. subv l. apply I. subv l. assumption. subv_in l A3. subv_in s2 A3. simpl_override_in A3. unfold rec_1. specex N8. instantiate (1 := N.ICExec.label_node l') in N8. instantiate (1 := n) in N8. subv_in s2 N8. simpl_override_in N8. rewrite <- N8. clear N8. assumption. clear N1 N3 N4 N6 N7 N9. rewrite N2. rewrite hist_map_app. simpl. assert (A2: S (rec_1 n') = c'). unfold rec_1. specex N8. instantiate (2 := n) in N8. instantiate (1 := n') in N8. subv_in s2 N8. simpl_override_in N8. rewrite <- N8. clear N8. assert (A := N.algrec_step). specex_deprem A. subst s1. split_all; eassumption. destruct A as [_ [_ A]]. depremise A. subv l. apply I. simpl in A. destruct A as [A _]. subv_in s2 A. subv_in l A. simpl_override_in A. assumption. specex N5. simpl in N5. depremise N5. split. instantiate (1 := N.ICExec.message n' c' k v u n lp). subv s2. apply in_app_iff. right. apply in_eq. simpl. instantiate (1 := rec_1 n'). assumption. simpl in N5. destruct N5 as [N51 N52]. subv ek. subv ev. unfold ptrace_2. rewrite N51. rewrite N52. unfold rec_1'. simpl_override. rewrite PeanoNat.Nat.add_comm. simpl. rewrite A2. reflexivity. clear N1 N2 N4 N5 N6 N7 N8 N9. intro. simpl. destruct (eq_nat_dec n0 n). subst n0. simpl_override. simpl_override. unfold ptrace_1. specialize (N3 n). subv_in s2 N3. simpl_override_in N3. assumption. simpl_override. destruct (eq_nat_dec n0 n'). subst n0. simpl_override. unfold ptrace_2. specialize (N3 n'). subv_in s2 N3. simpl_override_in N3. assumption. simpl_override. simpl_override. unfold ptrace_2. specialize (N3 n0). subv_in s2 N3. simpl_override_in N3. assumption. clear N1 N2 N3 N5 N6 N7 N8 N9. intros. simpl. destruct (eq_nat_dec n0 n). subst n0. simpl_override. simpl_override. reflexivity. simpl_override. destruct (eq_nat_dec n' n0). subst n0. simpl_override. unfold prog_2. specialize (N4 n'). subv_in s2 N4. simpl in N4. simpl_override_in N4. assumption. simpl_override. simpl_override. specialize (N4 n0). subv_in s2 N4. simpl in N4. simpl_override_in N4. assumption. clear N1 N2 N4 N6 N7 N8 N9. intros. destruct H6 as [M1 M2]. simpl in M1. specialize (N5 m c0). simpl in N5. depremise N5. split. subv s2. apply in_app_iff in M1. destruct M1 as [M1 | M1]. apply in_app_iff. left. assumption. apply in_app_iff. right. apply in_cons. assumption. assumption. destruct N5 as [N51 N52]. subst n'0. remember (N.ICExec.msg_sender m) as n'0. subst c'0. remember (N.ICExec.msg_clock m) as c'0. subst k0. remember (N.ICExec.msg_key m) as k0. subst v0. remember (N.ICExec.msg_val m) as v0. subst tp. simpl. destruct (eq_nat_dec n'0 n'). simpl_override. unfold ptrace_2. rewrite <- e0. split; assumption. simpl_override. destruct (eq_nat_dec n'0 n). simpl_override. unfold ptrace_1. rewrite <- e0. split; assumption. simpl_override. split; assumption. clear N1 N2 N4 N5 N7 N8 N9. intros. subst d. assert (In pid (AExec.dep (s' n0))). destruct (eq_nat_dec n0 n'). subst n0. simpl_override_in H6. unfold dep_2 in H6. assumption. simpl_override_in H6. destruct (eq_nat_dec n n0). subst n0. simpl_override_in H6. unfold dep_1 in H6. assumption. simpl_override_in H6. assumption. clear H6. specialize (N6 n0 pid). simpl in N6. depremise N6. assumption. destruct N6 as [N6 | N6]. destruct N6 as [l1 [l2 N6]]. open_conjs. left. exists l1. exists l2. split_all; try assumption. apply N.ICExec.cause_ext_cause. assumption. destruct N6 as [l1 N6]. open_conjs. right. exists l1. split_all; try assumption. apply in_app_iff. left. assumption. clear N1 N2 N3 N4 N5 N6 N8 N9. intros l' i n'' c''. intros. destruct H6 as [M1 [M2 [M3 [M4 M5]]]]. rewrite H4 in *. subst d. assert (A2: i < length (AExec.ptrace (s' n0))). clear M5. destruct (eq_nat_dec n' n0). rewrite e0 in M4. simpl_override_in M4. unfold ptrace_2 in M4. rewrite e0 in M4. assumption. simpl_override_in M4. destruct (eq_nat_dec n n0). rewrite e0 in M4. simpl_override_in M4. unfold ptrace_1 in M4. rewrite e0 in M4. assumption. simpl_override_in M4. assumption. clear M4. assert (A3: In (AExec.put_id n'' c'') (AExec.t_put_dep (nth i (AExec.ptrace (s' n0)) AExec.dummy_t_put))). clear A2. destruct (eq_nat_dec n' n0). rewrite e0 in M5. simpl_override_in M5. unfold ptrace_2 in M5. rewrite e0 in M5. assumption. simpl_override_in M5. destruct (eq_nat_dec n n0). rewrite e0 in M5. simpl_override_in M5. unfold ptrace_1 in M5. rewrite e0 in M5. assumption. simpl_override_in M5. assumption. clear M5. specialize (N7 l' i n'' c''). simpl in N7. depremise N7. split_all. assumption. apply in_app_iff in M2. destruct M2 as [M2 | M2]. assumption. exfalso. simpl in M2. destruct M2 as [M2 | M2]; try contradiction. subv_in l' M1. rewrite <- H4 in M1. simpl in M1. contradiction. assumption. assumption. subst n0. subst c0. assumption. destruct N7 as [l'' N7]. open_conjs. exists l''. split_all; try assumption. apply N.ICExec.cause_ext_cause. assumption. clear N1 N2 N3 N4 N5 N6 N7 N9. intros n1 n2. simpl. specex N8. instantiate (2 := n1) in N8. instantiate (1 := n2) in N8. subv_in s2 N8. assert (A2 := N.algrec_step). specex A2. depremise A2. subst s1. split_all; eassumption. destruct A2 as [_ [_ A2]]. depremise A2. subv l. apply I. simpl in A2. subv_in l A2. subv_in s2 A2. subv_in s3 A2. simpl_override_in A2. destruct A2 as [A21 [A22 A23]]. rewrite <- A21 in A22. clear A21. destruct (eq_nat_dec n1 n). subst n1. simpl_override. simpl_override. simpl_override_in N8. simpl_override_in A22. simpl_override_in A23. unfold rec_1'. destruct (eq_nat_dec n' n2). subst n2. simpl_override. unfold rec_1. rewrite Nat.add_comm. simpl. rewrite <- N8. assumption. simpl_override. unfold rec_1. rewrite <- N8. symmetry. apply A23. apply not_eq_sym. assumption. simpl_override. simpl_override_in N8. simpl_override_in A22. simpl_override_in A23. destruct (eq_nat_dec n' n1). subst n1. simpl_override. unfold rec_2. assumption. simpl_override. simpl_override. assumption. clear N2 N4 N5 N6. rewrite H4 in *. intros. destruct (eq_nat_dec n n0). assert (A3: not (n0 = n')). intro. apply A1. eapply eq_trans. symmetry. eassumption. symmetry. assumption. destruct (eq_nat_dec ek k0). assert (A2 := N.ICExec.msg_label_eq_key_val). specex_deprem A2. split_all. subst s1. eassumption. subv s2. apply in_app_iff. right. apply in_eq. simpl in A2. destruct A2 as [A21 [A22 [A23 [A24 [A25 A26]]]]]. assert (A4: S (rec_1 n') = c'). unfold rec_1. specialize (N8 n n'). subv_in s2 N8. simpl_override_in N8. rewrite <- N8. clear N8. assert (A4 := N.algrec_step). specex_deprem A4. subst s1. split_all; eassumption. destruct A4 as [_ [_ A4]]. depremise A4. subv l. apply I. simpl in A4. destruct A4 as [A4 _]. subv_in l A4. subv_in s2 A4. subv_in s3 A4. simpl_override_in A4. simpl_override_in A4. assumption. exists lp. split_all; try assumption. subv n''. subv n. simpl_override. simpl_override. unfold store_1'. subv ek. simpl_override. symmetry. assumption. subv c''. subv n. simpl_override. simpl_override. unfold store_1'. subv ek. simpl_override. unfold rec_1'. simpl_override. rewrite PeanoNat.Nat.add_comm. simpl. rewrite A4. symmetry. assumption. apply in_app_iff. left. assumption. intros. subst d''. simpl_override_in H7. subv_in n H7. simpl_override_in H7. specialize (N7 lp (rec_1 n') n'0 c'0). simpl in N7. depremise N7. split_all; try assumption. rewrite A4. assumption. rewrite <- A24. unfold rec_1. specialize (N8 n n'). subv_in s2 N8. simpl_override_in N8. assert (A5 := N.algrec_step). specex_deprem A5. subst s1. split_all; eassumption. destruct A5 as [_ [_ A5]]. depremise A5. subv l. apply I. simpl in A5. destruct A5 as [A5 _]. subv_in l A5. subv_in s2 A5. subv_in s3 A5. simpl_override_in A5. simpl_override_in A5. assert (A6 := N.ICExec.msg_clock_lte_state_clock). specex A6. simpl in A6. depremise A6. split. subst s1. eassumption. instantiate (1 := N.ICExec.message n' c' k v u n lp). subv s2. apply in_app_iff. right. apply in_eq. simpl in A6. subv_in s2 A6. simpl_override_in A6. specex N3. instantiate (1 := n') in N3. subv_in s2 N3. simpl_override_in N3. rewrite <- N8. clear N8. rewrite <- N3. clear N3. rewrite <- A5 in A6. clear A5. assumption. rewrite <- A24. unfold store_1' in H7. subv_in ek H7. simpl_override_in H7. unfold ed in H7. unfold ptrace_2 in H7. assumption. destruct N7 as [l'' N7]. open_conjs. exists l''. split_all; try assumption. apply N.ICExec.cause_ext_cause. assumption. specialize (N9 n k0 n'0 c'0). simpl in N9. depremise N9. subst n''. subv_in n H6. simpl_override_in H6. simpl_override_in H6. unfold store_1' in H6. simpl_override_in H6. unfold store_1 in H6. assumption. destruct N9 as [l_2 N9]. open_conjs. exists l_2. split_all; try assumption. rewrite H8. subv n''. simpl_override. simpl_override. unfold store_1'. simpl_override. unfold store_1. reflexivity. rewrite H9. subv c''. simpl_override. simpl_override. unfold store_1'. simpl_override. unfold store_1. reflexivity. apply in_app_iff. left. assumption. simpl. simpl_override. simpl_override. intros. depremise H11. unfold store_1' in H12. simpl_override_in H12. unfold store_1 in H12. assumption. destruct H11 as [l_1 H11]. open_conjs. exists l_1. split_all; try assumption. apply N.ICExec.cause_ext_cause. assumption. destruct (eq_nat_dec n0 n'). specialize (N9 n' k0 n'0 c'0). simpl in N9. depremise N9. subst n''. subv_in n0 H6. simpl_override_in H6. unfold store_2 in H6. assumption. destruct N9 as [l_2 N9]. open_conjs. exists l_2. split_all; try assumption. rewrite H8. subv n''. simpl_override. unfold store_2. reflexivity. rewrite H9. subv c''. simpl_override. unfold store_2. reflexivity. apply in_app_iff. left. assumption. simpl. simpl_override. intros. depremise H11. unfold store_2 in H12. assumption. destruct H11 as [l_1 H11]. open_conjs. exists l_1. split_all; try assumption. apply N.ICExec.cause_ext_cause. assumption. specialize (N9 n0 k0 n'0 c'0). simpl in N9. depremise N9. subst n''. simpl_override_in H6. simpl_override_in H6. assumption. destruct N9 as [l_2 N9]. open_conjs. exists l_2. split_all; try assumption. rewrite H8. subv n''. simpl_override. simpl_override. reflexivity. rewrite H9. subv c''. simpl_override. simpl_override. reflexivity. apply in_app_iff. left. assumption. simpl. simpl_override. simpl_override. intros. depremise H11. assumption. destruct H11 as [l_1 H11]. open_conjs. exists l_1. split_all; try assumption. apply N.ICExec.cause_ext_cause. assumption. pose (ptrace := AExec.ptrace (s' n)). pose (dep := AExec.dep (s' n)). pose (rec := AExec.rec (s' n)). pose (store := AExec.store (s' n)). exists (h' ++ [AExec.fault_label n]). exists (override s' n (AExec.node_state (AExec.Syntax.skip) ptrace dep rec store)). split_all. clear N2 N3 N5 N6 N7 N8 N9. eapply AExec.StepStar.steps. eassumption. assert (A: s' = override s' n (AExec.node_state (AExec.Syntax.fault) ptrace dep rec store)). apply functional_extensionality. intros. destruct (eq_nat_dec x n). subst x. simpl_override. specialize (N4 n). rewrite <- H2 in N4. simpl in N4. simpl_override_in N4. simpl in N4. destruct (s' n). simpl in N4. subst ptrace. subst dep. subst rec. subst store. rewrite <- N4. simpl. reflexivity. simpl_override. reflexivity. rewrite A at 1. clear A. econstructor. assumption. clear N3 N4 N5 N6 N7 N8 N9. rewrite N2. rewrite hist_map_app. simpl. f_equal. clear N1 N2 N4 N5 N6 N7 N8 N9. intro. simpl. destruct (eq_nat_dec n0 n). subst n0. simpl_override. simpl_override. unfold ptrace. specialize (N3 n). subv_in s2 N3. simpl_override_in N3. assumption. simpl_override. simpl_override. specialize (N3 n0). subv_in s2 N3. simpl_override_in N3. assumption. intros. simpl. destruct (eq_nat_dec n0 n). subst n0. simpl_override. simpl_override. subv val. reflexivity. simpl_override. simpl_override. specialize (N4 n0). subv_in s2 N4. simpl in N4. simpl_override_in N4. assumption. clear N1 N2 N4 N6 N7 N8 N9. intros. simpl in H5. destruct H5 as [M1 M2]. specialize (N5 m c0). simpl in N5. depremise N5. split. subv s2. assumption. assumption. destruct N5 as [N51 N52]. subst tp. destruct (eq_nat_dec n n'). simpl_override. unfold ptrace. rewrite e0. split; assumption. simpl_override. split; assumption. clear N1 N2 N4 N5 N7 N8. rewrite H3. intros. subst d. destruct (eq_nat_dec n0 n). subst n0. simpl_override_in H5. specialize (N6 n pid). simpl in N6. depremise N6. assumption. destruct N6 as [N6 | N6]. destruct N6 as [l1 [l2 N6]]. open_conjs. left. exists l1. exists l2. split_all; try assumption. apply N.ICExec.cause_ext_cause. assumption. destruct N6 as [l1 N6]. open_conjs. right. exists l1. split_all; try assumption. apply in_app_iff. left. assumption. simpl_override_in H5. specialize (N6 n0 pid). simpl in N6. depremise N6. assumption. destruct N6 as [N6 | N6]. destruct N6 as [l1 [l2 N6]]. open_conjs. left. exists l1. exists l2. split_all; try assumption. apply N.ICExec.cause_ext_cause. assumption. destruct N6 as [l1 N6]. open_conjs. right. exists l1. split_all; try assumption. apply in_app_iff. left. assumption. clear N1 N2 N3 N4 N5 N6 N8 N9. rewrite H3 in *. intros l' i n''' c'''. intros. destruct H5 as [M1 [M2 [M3 [M4 M5]]]]. subst d. assert (A2: i < length (AExec.ptrace (s' n0))). clear M5. destruct (eq_nat_dec n n0). rewrite e0 in M4. simpl_override_in M4. unfold ptrace in M4. rewrite e0 in M4. assumption. simpl_override_in M4. assumption. assert (A3: In (AExec.put_id n''' c''') (AExec.t_put_dep (nth i (AExec.ptrace (s' n0)) AExec.dummy_t_put))). clear A2. destruct (eq_nat_dec n n0). rewrite e0 in M5. simpl_override_in M5. unfold ptrace in M5. rewrite e0 in M5. assumption. simpl_override_in M5. assumption. clear M5. specialize (N7 l' i n''' c'''). simpl in N7. depremise N7. split_all. assumption. apply in_app_iff in M2. destruct M2 as [M2 | M2]. assumption. exfalso. simpl in M2. destruct M2 as [M2 | M2]; try contradiction. subv_in l' M1. rewrite <- H3 in M1. simpl in M1. contradiction. assumption. assumption. subst n0. subst c0. assumption. destruct N7 as [l'' N7]. open_conjs. exists l''. split_all; try assumption. apply N.ICExec.cause_ext_cause. assumption. clear N1 N2 N3 N4 N5 N6 N7 N9. intros n1 n2. simpl. specex N8. instantiate (2 := n1) in N8. instantiate (1 := n2) in N8. subv_in s2 N8. subst l. inversion H0. subst. destruct (eq_nat_dec n1 n). subst n1. simpl_override. simpl_override. simpl_override_in N8. unfold rec. assumption. simpl_override. simpl_override. simpl_override_in N8. assumption. clear N1 N2 N3 N4 N5 N6 N7 N8. rewrite H3 in *. intros. specialize (N9 n0 k0 n' c'). simpl in N9. depremise N9. subst n''. destruct (eq_nat_dec n n0). subst n0. simpl_override_in H5. unfold store in H5. assumption. simpl_override_in H5. assumption. destruct (eq_nat_dec n n0). rewrite e0 in *. destruct N9 as [l1 N9]. open_conjs. exists l1. split_all; try assumption. subv n''. simpl_override. unfold store. rewrite e0. assumption. subv c''. simpl_override. unfold store. rewrite e0. assumption. apply in_app_iff. left. assumption. intros. depremise H10. subv_in d'' H11. simpl_override_in H11. subst store. rewrite e0 in *. assumption. destruct H10 as [l2 H10]. open_conjs. exists l2. split_all; try assumption. apply N.ICExec.cause_ext_cause. assumption. destruct N9 as [l1 N9]. open_conjs. exists l1. split_all; try assumption. subv n''. simpl_override. unfold store. assumption. subv c''. simpl_override. unfold store. assumption. apply in_app_iff. left. assumption. intros. depremise H10. subv_in d'' H11. simpl_override_in H11. subst store. assumption. destruct H10 as [l2 H10]. open_conjs. exists l2. split_all; try assumption. apply N.ICExec.cause_ext_cause. assumption. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)