proposition: Lemma step_star_rec_nondec: forall (p: ICExec.Syntax.PProg)(h0 h: list Label)(s s': State)(n: NId), let sc := rec (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', sc n' <= sc' n'.
proof: Proof. intros. destruct H as [HI H]. induction H. apply Nat.le_refl. rename sc' into sc''. pose (sc' := rec (alg_state (node_states s2 n))). assert (sc' n' <= sc'' n'). clear IHstep_star. inversion H0; clear H0; subst sc; subst sc'; subst sc''; simpl in *. rewrite <- H2. rewrite <- H4. simpl. destruct (eq_nat_dec n n0). simpl_override. destruct (eq_nat_dec n' n0). simpl_override. simpl. simpl_override. subst n'. rewrite Nat.add_comm. simpl. apply le_S. apply Nat.le_refl. simpl_override. simpl. simpl_override. apply Nat.le_refl. simpl_override. simpl_override. apply Nat.le_refl. rewrite <- H2. rewrite <- H4. simpl. destruct (eq_nat_dec n n0). subst n. simpl_override. simpl_override. simpl. apply Nat.le_refl. simpl_override. simpl_override. apply Nat.le_refl. rewrite <- H3. rewrite <- H5. simpl. destruct (eq_nat_dec n n0). subst n. simpl_override. simpl_override. simpl. destruct (eq_nat_dec (sender_node u) n'). simpl_override. unfold guard_method in H2. bool_to_prop_in H2. destruct H2. bool_to_prop_in H2. rewrite e0 in *. rewrite H2. rewrite Nat.add_comm. simpl. apply le_S. apply Nat.le_refl. simpl_override. apply Nat.le_refl. simpl_override. simpl_override. apply Nat.le_refl. subv s2. subv s3. destruct (eq_nat_dec n n0). subst n. simpl_override. simpl_override. apply Nat.le_refl. simpl_override. simpl_override. apply Nat.le_refl. simpl in IHstep_star. depremise IHstep_star. assumption. subst sc'. subst sc''. 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)