proposition: Lemma clock_in_dep: forall p h s n, let ns := alg_state (node_states s n) in let c := clock ns in let d := dep ns in step_star (init p) h s -> c > 0 -> In (n, c) d.
proof: Proof. intros. remember (init p) as s0 eqn: Hs. induction H. subst c. subst ns. subst d. subst s. simpl in H0. inversion H0. simpl in IHstep_star. depremise IHstep_star. assumption. inversion H1. subst d. subst ns. rewrite <- H5. simpl. destruct (eq_nat_dec n0 n). rewrite e0 in *. simpl_override. simpl. left. rewrite e0 in *. apply f2_equal. split. reflexivity. subst c. rewrite <- H5. simpl. simpl_override. simpl. reflexivity. simpl_override. subst c. rewrite <- H5. simpl. simpl_override. depremise IHstep_star. rewrite <- H3. simpl. simpl_override. rewrite <- H5 in H0. simpl in H0. simpl_override_in H0. assumption. rewrite <- H3 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. assumption. subst c. subst d. subst ns. rewrite <- H5. simpl. destruct (eq_nat_dec n0 n). subst n. simpl_override. simpl. depremise IHstep_star. rewrite <- H3. simpl. simpl_override. simpl. rewrite <- H5 in H0. simpl in H0. simpl_override_in H0. simpl in H0. assumption. rewrite <- H3 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. destruct (entry_node (store s k) <>? init_nid). apply in_cons. assumption. assumption. simpl_override. depremise IHstep_star. rewrite <- H3. simpl. simpl_override. simpl. rewrite <- H5 in H0. simpl in H0. simpl_override_in H0. assumption. rewrite <- H3 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. assumption. subst c. subst d. subst ns. rewrite <- H6. simpl. destruct (eq_nat_dec n0 n). subst n. simpl_override. simpl. depremise IHstep_star. rewrite <- H4. simpl. simpl_override. simpl. rewrite <- H6 in H0. simpl in H0. simpl_override_in H0. simpl in H0. assumption. rewrite <- H4 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. simpl_override. depremise IHstep_star. rewrite <- H4. simpl. simpl_override. simpl. rewrite <- H6 in H0. simpl in H0. simpl_override_in H0. assumption. rewrite <- H4 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. assumption. subst c. subst d. subst ns. rewrite <- H5. simpl. destruct (eq_nat_dec n0 n). subst n. simpl_override. depremise IHstep_star. rewrite <- H3. simpl. simpl_override. rewrite <- H5 in H0. simpl in H0. simpl_override_in H0. simpl in H0. assumption. rewrite <- H3 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. assumption. simpl_override. depremise IHstep_star. rewrite <- H3. simpl. simpl_override. rewrite <- H5 in H0. simpl in H0. simpl_override_in H0. assumption. rewrite <- H3 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)