proposition: Lemma reduces_wf: forall cond p, well_founded (reduces cond p).
proof: Proof. unfold well_founded. intros cond p e0; apply Acc_intro. intros e1 H; unfold reduces in H. decompose [ex and] H; clear H. clear H2 H0 e0. case (exec_execn H1). intros n. generalize cond p e1 x; clear cond p e1 x H1. elim n. intros cond p e0 e1 H; inversion_clear H. clear n; intros n HR cond p e0 e1 H. inversion_clear H. inversion_clear H0. set (b:=E.eval cond e0) in * |-. cut (E.eval cond e0=b); auto. generalize H; clear H; case b; simpl. intros H; inversion_clear H. intros; apply Acc_intro. intros e2 H3; unfold reduces in H3. intuition. rewrite (exec_deterministic H3 H0); eauto. intros H H0; apply Acc_intro. unfold reduces; rewrite H0. intuition. discriminate. Qed.
imports: hoarelogicsemantics