proposition: Theorem ds_sn : forall i l l', ds i l = Some l' -> exec l i l'.
proof: Proof. induction i. intros l l'; simpl; unfold bind. generalize (af_eval l a). case' (af l a). intros v He. generalize (uf_s l s v). intros Hu Heq. rewrite Heq in Hu. eauto. simpl; unfold comp_right; intros l l'. generalize (IHi1 l); case' (ds i1 l). intros l1 Hi1; generalize (IHi2 l1). simpl; intros IHi2' Heq; rewrite Heq in IHi2'. eauto. simpl; intros l l' Heq. pose (f:= F_phi (list(string*Z)) (fun l => bf l b)(ds i)). assert (Hn: exists n:nat, iter _ f n (fun _ : list(string*Z) => None) l = Some l'). apply (phi_terminates_n _ (fun l => bf l b)(ds i)). assumption. case Hn; intros n; generalize l; clear Heq Hn l. induction n; intros l. simpl; intros; discriminate. simpl. unfold f at 1, F_phi, ifthenelse at 1. generalize (bf_eval l b); case' (bf l b). intros [|] Hevalb. unfold bind at 1. generalize (IHi l); case' (ds i l). intros l1 Hds_i Hds_w. apply SN4 with l1. auto. auto. apply IHn. auto. intros Hres; injection Hres; intros; subst l'. apply SN5; auto. simpl; intros l l' Heq; injection Heq; intros; subst; apply SN1. Qed.
imports: Relations ClassicalEpsilon function_cpo constructs syntax little