proposition: Lemma entry_clock_leq_dep: forall (p: ICExec.Syntax.PProg)(h: list Label)(s: State)(n n': NId)(k: Key), let as2 := alg_state ((node_states s) n) in (step_star (init p) h s /\ entry_node (store as2 k) = n') -> entry_clock (store as2 k) <= dep as2 n'.
proof: Proof. intros. remember (init p) as s0 eqn: Hs. open_conjs. induction H. subst as2. subst s. simpl. apply Nat.le_refl. rename as2 into as3. pose (as2 := alg_state (node_states s2 n)). simpl in IHstep_star. depremise IHstep_star. assumption. subst as3. inversion H1; simpl in *. rewrite <- H3 in IHstep_star. simpl in IHstep_star. destruct (eq_nat_dec n n0). subst n. destruct (eq_nat_dec n' n0). subst n'. simpl_override. simpl. simpl_override. simpl. destruct (eq_nat_dec k0 k). simpl_override. simpl. simpl_override. reflexivity. simpl_override. rewrite <- H5 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. depremise IHstep_star. reflexivity. assert (A := dep_leq_rec p ls s2 n0). simpl in A. depremise A. subst s1. assumption. specialize (A n0). depremise A. assumption. rewrite <- H3 in A. simpl in A. simpl_override_in A. simpl in A. rewrite <- H5 in e0. simpl in e0. simpl_override_in e0. simpl in e0. simpl_override_in e0. rewrite e0 in IHstep_star. rewrite Nat.add_comm. simpl. apply le_S. eapply Nat.le_trans; eassumption. simpl_override. simpl. simpl_override. simpl. simpl_override_in IHstep_star. simpl in IHstep_star. rewrite <- H5 in H0. simpl in H0. simpl_override_in H0. simpl in H0. simpl_override_in H0. simpl in H0. destruct (eq_nat_dec k k0). subst k. simpl_override_in H0. simpl in H0. symmetry in H0. contradiction. simpl_override. simpl_override. simpl_override_in H0. depremise IHstep_star. assumption. assumption. simpl_override. simpl_override_in IHstep_star. simpl in IHstep_star. rewrite <- H5 in H0. simpl in H0. simpl_override_in H0. depremise IHstep_star. assumption. assumption. destruct (eq_nat_dec n n0). subst n. simpl_override. simpl. destruct (eq_nat_dec (entry_node (store s k0)) n'). subst n'. simpl_override. simpl. rewrite <- H3 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. rewrite <- H5 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. rewrite <- H5 in e0. simpl in e0. simpl_override_in e0. simpl in e0. depremise IHstep_star. reflexivity. apply PeanoNat.Nat.max_le_iff. left. rewrite e0. assumption. simpl_override. rewrite <- H3 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. rewrite <- H5 in H0. simpl in H0. simpl_override_in H0. simpl in H0. depremise IHstep_star. assumption. assumption. simpl_override. rewrite <- H3 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. rewrite <- H5 in H0. simpl in H0. simpl_override_in H0. simpl in H0. depremise IHstep_star. assumption. assumption. destruct (eq_nat_dec n n0). subst n. simpl_override. simpl. destruct (eq_nat_dec k k0). simpl_override. simpl. rewrite <- H6 in H0. simpl in H0. simpl_override_in H0. simpl in H0. rewrite e0 in H0. simpl_override_in H0. simpl in H0. rewrite H0. apply Nat.le_max_r. simpl_override. simpl. rewrite <- H4 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. depremise IHstep_star. rewrite <- H6 in H0. simpl in H0. simpl_override_in H0. simpl in H0. simpl_override_in H0. assumption. eapply Nat.le_trans. eassumption. apply Nat.le_max_l. simpl_override. rewrite <- H4 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. depremise IHstep_star. rewrite <- H6 in H0. simpl in H0. simpl_override_in H0. assumption. assumption. subv_in s2 IHstep_star. destruct (eq_nat_dec n n0). subst n. simpl_override. simpl_override_in IHstep_star. depremise IHstep_star. subv_in s3 H0. simpl_override_in H0. assumption. assumption. simpl_override. simpl_override_in IHstep_star. depremise IHstep_star. subv_in s3 H0. simpl_override_in H0. assumption. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool Program.Basics) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs extralib KVStore)