proposition: Lemma step_star_dep_rec_nondec: forall (p: ICExec.Syntax.PProg)(h0 h: list Label)(s s': State)(n: NId), let sc := dep (alg_state ((node_states s) n)) in let sc' := rec (alg_state ((node_states s') n)) in (step_star (init p) h0 s /\ step_star s h s') -> forall n', In n' nids -> sc n' <= sc' n'.
proof: Proof. intros. subst sc. subst sc'. assert (A1 := step_star_clock_nondec p h0 h s s' n H n'). open_conjs. assert (A2 := dep_leq_rec p (h0 ++ h) s' n). simpl in A2. depremise A2. apply step_star_app. exists s. split; assumption. specialize (A2 n'). depremise A2. assumption. eapply Nat.le_trans; eassumption. Qed.
imports: Coq(FunctionalExtensionality List Bool Program.Basics) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs extralib KVStore)