proposition: Lemma inst_clock_leq_rec: forall (p: ICExec.Syntax.PProg)(h: list Label)(s: State)(n: NId), let as1 := alg_state ((node_states (init p)) n) in let as2 := alg_state ((node_states s) n) in step_star (init p) h s -> forall k, entry_clock (store as2 k) <= rec as2 (entry_node (store as2 k)).
proof: Proof. intros. remember (init p) as s0 eqn: Hs. induction H. subst as1. subst as2. subst s. simpl. apply Nat.le_refl. rename as2 into as3. pose (as2 := alg_state (node_states s2 n)). depremise IHstep_star. assumption. subst as3. inversion H0; clear H0; simpl in *. destruct (eq_nat_dec n n0). simpl_override. simpl. simpl_override. simpl. destruct (eq_nat_dec k0 k). simpl_override. simpl. simpl_override. simpl. apply Nat.le_refl. simpl_override. rewrite <- H2 in IHstep_star. simpl in IHstep_star. subst n. simpl_override_in IHstep_star. simpl in IHstep_star. destruct (eq_nat_dec n0 (entry_node (store s k))). simpl_override. rewrite e0. rewrite Nat.add_comm. simpl. apply le_S. assumption. simpl_override. assumption. simpl_override. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. assumption. destruct (eq_nat_dec n n0). simpl_override. simpl. rewrite <- H2 in IHstep_star. simpl in IHstep_star. subst n. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. simpl_override. simpl. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. destruct (eq_nat_dec n n0). simpl_override. simpl. simpl_override. simpl. destruct (eq_nat_dec k0 k). simpl_override. simpl. simpl_override. simpl. apply Nat.le_refl. simpl_override. rewrite <- H3 in IHstep_star. simpl in IHstep_star. subst n. simpl_override_in IHstep_star. simpl in IHstep_star. destruct (eq_nat_dec (sender_node u) (entry_node (store s k))). simpl_override. rewrite <- e0 in *. unfold guard_method in H2. bool_to_prop_in H2. destruct H2. bool_to_prop_in H2. rewrite H2. rewrite Nat.add_comm. simpl. apply le_S. assumption. simpl_override. assumption. simpl_override. rewrite <- H3 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. destruct (eq_nat_dec n n0). simpl_override. simpl. rewrite <- H2 in IHstep_star. simpl in IHstep_star. subst n. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. simpl_override. simpl. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool Program.Basics) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs extralib KVStore)