x_by_xyProgCompScript.sml

(*
  Auto-generated by Daisy (https://gitlab.mpi-sws.org/AVA/daisy
  *)
(* INCLUDES, do not change those *)
open exampleLib;

val _ = new_theory "x_by_xyProgComp";

val _ = translation_extends "cfSupport";

Definition theAST_pre_def:
  theAST_pre = \ (x:(string, string) id).
  if x = Short "x" then (((1)/(1), (4)/(1)):real#real)
  else if x = Short "y" then (((1)/(1), (4)/(1)):real#real)
  else (0,0)
End

Definition theAST_def:
  theAST =
  [ Dlet unknown_loc (Pvar "x_by_xy")
    (Fun "x"(Fun "y"
      (FpOptimise Opt
(App (FP_bop FP_Div)
        [
          Var (Short  "x");
          (App (FP_bop FP_Add)
          [
            Var (Short  "x");
            Var (Short  "y")
          ])
        ]))))]
End

Definition theErrBound_def:
  theErrBound = inv (2 pow (5))
End

val x = define_benchmark theAST_def theAST_pre_def true;

val _ = export_theory()