proposition: Lemma dep_leq_rec: forall (p: ICExec.Syntax.PProg)(h: list Label)(s: State)(n: NId), let as2 := alg_state ((node_states s) n) in step_star (init p) h s -> forall n', In n' nids -> dep as2 n' <= rec as2 n'.
proof: Proof. intros p h s n as2 H n' Hi. remember (init p) as s0 eqn: Hs. 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 H0; clear H0; simpl in *. rewrite <- H2 in IHstep_star. simpl in IHstep_star. destruct (eq_nat_dec n n0). simpl_override. simpl. destruct (eq_nat_dec n' n0). simpl_override. simpl. simpl_override. subst n'. apply Nat.le_refl. simpl_override. simpl. simpl_override. subst n. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. simpl_override. simpl_override_in IHstep_star. assumption. unfold override. destruct (eq_nat_dec n n0). simpl. subst n. destruct (eq_nat_dec (entry_node (store s k)) n'). subst n'. simpl_override. apply Nat.max_lub. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. assert (A := inst_clock_leq_rec p ls s2 n0). simpl in A. depremise A. subst s1. assumption. specialize (A k). rewrite <- H2 in A. simpl in A. simpl_override_in A. simpl in A. assumption. simpl_override. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. assumption. destruct (n =_? n0). subst n. simpl_override. simpl. destruct (sender_node u =_? n'). rewrite e0 in *. simpl_override. rewrite <- H3 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. unfold guard_method in H2. bool_to_prop_in H2. destruct H2. bool_to_prop_in H2. rewrite e0 in H2. rewrite H2. apply Nat.max_lub. rewrite Nat.add_comm. simpl. apply le_S. assumption. apply Nat.le_refl. simpl_override. rewrite <- H3 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. apply Nat.max_lub. assumption. unfold guard_method in H2. bool_to_prop_in H2. destruct H2. assert (A:= fold_left_and NId nids n' (fun n => sender_dep u n <=? rec s n)). depremise A. split. assumption. assumption. simpl in A. bool_to_prop_in A. 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). subst n. simpl_override. subv_in s2 IHstep_star. simpl_override_in IHstep_star. assumption. simpl_override. subv_in s2 IHstep_star. simpl_override_in IHstep_star. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool Program.Basics) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs extralib KVStore)