proposition: Theorem sn_ds : forall l i l', exec l i l' -> ds i l = Some l'.
proof: Proof. induction 1. auto. simpl; unfold bind; match goal with id : _ |- _ => rewrite aeval_f with (1:=id); apply s_update_f; auto end. simpl; unfold comp_right; match goal with id : _ |- _ => rewrite id; assumption end. pose (f:= F_phi _ (fun l' => bf l' b)(ds i)). simpl in IHexec2 |- *. rewrite <- fix_phi. unfold F_phi at 1. assert (Ht : bf r b = Some true) by (apply beval_f; auto). rewrite Ht; simpl. rewrite IHexec1; simpl. assumption. pose (f:= F_phi _ (fun l' => bf l' b)(ds i)). simpl. rewrite <- fix_phi. assert (Ht : bf r b = Some false) by (apply beval_f; auto). simpl; unfold f, F_phi; rewrite Ht; auto. Qed.
imports: Relations ClassicalEpsilon function_cpo constructs syntax little