diff --git a/T/my_cosine-CosineSingle-MethodError.gappa b/T/my_cosine-CosineSingle-MethodError.gappa
new file mode 100644
index 0000000000000000000000000000000000000000..15515381984b941d0cdbabdc2452dbd20db55c90
--- /dev/null
+++ b/T/my_cosine-CosineSingle-MethodError.gappa
@@ -0,0 +1,494 @@
+# this is a prelude for Gappa
+# this is a prelude for Gappa real arithmetic
+# this is a prelude for Gappa integer arithmetic
+@rnd_ieee32_ne=float<ieee_32,ne>;
+theory Task
+  (* use BuiltIn *)
+  
+  logic infix_ls real real
+  
+  (* clone Assoc with type t = real, logic op = infix_pl,
+    prop Assoc = Assoc1 *)
+  
+  (* clone Group with type t1 = real, logic inv = prefix_mn,
+    logic op1 = infix_pl, logic unit = zero, prop Inv_def = Inv_def1,
+    prop Assoc2 = Assoc1, prop Unit_def = Unit_def1 *)
+  
+  (* clone Comm with type t2 = real, logic op2 = infix_pl,
+    prop Comm = Comm1 *)
+  
+  (* meta AC logic infix_pl *)
+  
+  (* clone CommutativeGroup with type t3 = real, logic inv1 = prefix_mn,
+    logic op3 = infix_pl, logic unit1 = zero, prop Comm2 = Comm1,
+    prop Inv_def2 = Inv_def1, prop Assoc3 = Assoc1,
+    prop Unit_def2 = Unit_def1 *)
+  
+  (* clone Assoc with type t = real, logic op = infix_as,
+    prop Assoc = Assoc4 *)
+  
+  (* clone Ring with type t4 = real, logic infix_mn = infix_mn1,
+    logic infix_as1 = infix_as, logic prefix_mn1 = prefix_mn,
+    logic infix_pl1 = infix_pl, logic zero1 = zero,
+    prop Mul_distr = Mul_distr1, prop Assoc5 = Assoc4, prop Comm3 = Comm1,
+    prop Inv_def3 = Inv_def1, prop Assoc6 = Assoc1,
+    prop Unit_def3 = Unit_def1 *)
+  
+  (* clone Comm with type t2 = real, logic op2 = infix_as,
+    prop Comm = Comm4 *)
+  
+  (* meta AC logic infix_as *)
+  
+  (* clone CommutativeRing with type t5 = real, logic infix_mn2 = infix_mn1,
+    logic infix_as2 = infix_as, logic prefix_mn2 = prefix_mn,
+    logic infix_pl2 = infix_pl, logic zero2 = zero, prop Comm5 = Comm4,
+    prop Mul_distr2 = Mul_distr1, prop Assoc7 = Assoc4, prop Comm6 = Comm1,
+    prop Inv_def4 = Inv_def1, prop Assoc8 = Assoc1,
+    prop Unit_def4 = Unit_def1 *)
+  
+  axiom NonTrivialRing : not (0.0 = 1.0)
+  
+  (* clone UnitaryCommutativeRing with type t6 = real, logic one = one1,
+    logic infix_mn3 = infix_mn1, logic infix_as3 = infix_as,
+    logic prefix_mn3 = prefix_mn, logic infix_pl3 = infix_pl,
+    logic zero3 = zero, prop NonTrivialRing1 = NonTrivialRing,
+    prop Unitary = Unitary1, prop Comm7 = Comm4,
+    prop Mul_distr3 = Mul_distr1, prop Assoc9 = Assoc4, prop Comm8 = Comm1,
+    prop Inv_def5 = Inv_def1, prop Assoc10 = Assoc1,
+    prop Unit_def5 = Unit_def1 *)
+  
+  (* clone Field with type t7 = real, logic infix_sl = infix_sl1,
+    logic inv2 = inv3, logic one2 = one1, logic infix_mn4 = infix_mn1,
+    logic infix_as4 = infix_as, logic prefix_mn4 = prefix_mn,
+    logic infix_pl4 = infix_pl, logic zero4 = zero, prop Inverse = Inverse1,
+    prop NonTrivialRing2 = NonTrivialRing, prop Unitary2 = Unitary1,
+    prop Comm9 = Comm4, prop Mul_distr4 = Mul_distr1, prop Assoc11 = Assoc4,
+    prop Comm10 = Comm1, prop Inv_def6 = Inv_def1, prop Assoc12 = Assoc1,
+    prop Unit_def6 = Unit_def1 *)
+  
+  (* clone EndoRelation with type t8 = real, logic rel = infix_lseq,  *)
+  
+  (* clone Reflexive with type t9 = real, logic rel1 = infix_lseq,
+    prop Refl = Refl1 *)
+  
+  (* clone EndoRelation with type t8 = real, logic rel = infix_lseq,  *)
+  
+  (* clone Transitive with type t10 = real, logic rel2 = infix_lseq,
+    prop Trans = Trans1 *)
+  
+  (* clone PreOrder with type t11 = real, logic rel3 = infix_lseq,
+    prop Trans2 = Trans1, prop Refl2 = Refl1 *)
+  
+  (* clone EndoRelation with type t8 = real, logic rel = infix_lseq,  *)
+  
+  (* clone Antisymmetric with type t12 = real, logic rel4 = infix_lseq,
+    prop Antisymm = Antisymm1 *)
+  
+  (* clone PartialOrder with type t13 = real, logic rel5 = infix_lseq,
+    prop Antisymm2 = Antisymm1, prop Trans3 = Trans1, prop Refl3 = Refl1 *)
+  
+  (* clone EndoRelation with type t8 = real, logic rel = infix_lseq,  *)
+  
+  (* clone Total with type t14 = real, logic rel6 = infix_lseq,
+    prop Total = Total1 *)
+  
+  (* clone TotalOrder with type t15 = real, logic rel7 = infix_lseq,
+    prop Total2 = Total1, prop Antisymm3 = Antisymm1, prop Trans4 = Trans1,
+    prop Refl4 = Refl1 *)
+  
+  axiom CompatOrderAdd : forall x:real, y:real, z:real. infix_ls x y or
+    (x = y) -> infix_ls (x + z) (y + z) or ((x + z) = (y + z))
+  
+  axiom CompatOrderMult : forall x:real, y:real, z:real. infix_ls x y or
+    (x = y) -> infix_ls 0.0 z or (0.0 = z) -> infix_ls (x * z) (y * z) or
+    ((x * z) = (y * z))
+  
+  (* clone OrderedField with type t16 = real, logic infix_gteq = infix_gteq1,
+    logic infix_lseq1 = infix_lseq, logic infix_sl2 = infix_sl1,
+    logic inv4 = inv3, logic one3 = one1, logic infix_mn5 = infix_mn1,
+    logic infix_as5 = infix_as, logic prefix_mn5 = prefix_mn,
+    logic infix_pl5 = infix_pl, logic zero5 = zero,
+    prop CompatOrderMult1 = CompatOrderMult,
+    prop CompatOrderAdd1 = CompatOrderAdd, prop Total3 = Total1,
+    prop Antisymm4 = Antisymm1, prop Trans5 = Trans1, prop Refl5 = Refl1,
+    prop Inverse2 = Inverse1, prop NonTrivialRing3 = NonTrivialRing,
+    prop Unitary3 = Unitary1, prop Comm11 = Comm4,
+    prop Mul_distr5 = Mul_distr1, prop Assoc13 = Assoc4, prop Comm12 = Comm1,
+    prop Inv_def7 = Inv_def1, prop Assoc14 = Assoc1,
+    prop Unit_def7 = Unit_def1 *)
+  
+  (* use Real *)
+  
+  axiom Abs_le : forall x:real, y:real. infix_ls | x | y or (| x | = y) <->
+    (infix_ls (-y) x or ((-y) = x)) and (infix_ls x y or (x = y))
+  
+  axiom Abs_pos : forall x:real. infix_ls 0.0 | x | or (0.0 = | x |)
+  
+  (* use Abs *)
+  
+  logic sqr (x:real) : real = (x * x)
+  
+  logic sqrt real : real
+  
+  axiom Sqrt_positive : forall x:real. infix_ls 0.0 x or (0.0 = x) ->
+    infix_ls 0.0 (sqrt x) or (0.0 = sqrt x)
+  
+  axiom Sqrt_square : forall x:real. infix_ls 0.0 x or (0.0 = x) -> (sqr
+    (sqrt x) = x)
+  
+  axiom Square_sqrt : forall x:real. infix_ls 0.0 x or (0.0 = x) -> (sqrt
+    (x * x) = x)
+  
+  (* use Square *)
+  
+  logic cos real : real
+  
+  logic sin real : real
+  
+  axiom Pythagorean_identity : forall x:real. ((sqr (cos x) + sqr (sin
+    x)) = 1.0)
+  
+  axiom Cos_le_one : forall x:real. infix_ls | cos x | 1.0 or (| cos
+    x | = 1.0)
+  
+  axiom Sin_le_one : forall x:real. infix_ls | sin x | 1.0 or (| sin
+    x | = 1.0)
+  
+  axiom Cos_0 : (cos 0.0 = 1.0)
+  
+  axiom Sin_0 : (sin 0.0 = 0.0)
+  
+  logic pi : real
+  
+  axiom Pi_interval : infix_ls
+    3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196
+    pi and infix_ls pi
+    3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197
+  
+  axiom Cos_pi : (cos pi = (-1.0))
+  
+  axiom Sin_pi : (sin pi = 0.0)
+  
+  axiom Cos_pi2 : (cos (0.5 * pi) = 0.0)
+  
+  axiom Sin_pi2 : (sin (0.5 * pi) = 1.0)
+  
+  axiom Cos_plus_pi : forall x:real. (cos (x + pi) = (-cos x))
+  
+  axiom Sin_plus_pi : forall x:real. (sin (x + pi) = (-sin x))
+  
+  axiom Cos_plus_pi2 : forall x:real. (cos (x + (0.5 * pi)) = (-sin x))
+  
+  axiom Sin_plus_pi2 : forall x:real. (sin (x + (0.5 * pi)) = cos x)
+  
+  axiom Cos_neg : forall x:real. (cos (-x) = cos x)
+  
+  axiom Sin_neg : forall x:real. (sin (-x) = (-sin x))
+  
+  axiom Cos_sum : forall x:real, y:real. (cos (x + y) = ((cos x * cos
+    y) - (sin x * sin y)))
+  
+  axiom Sin_sum : forall x:real, y:real. (sin (x + y) = ((sin x * cos
+    y) + (cos x * sin y)))
+  
+  logic tan (x:real) : real = (sin x / cos x)
+  
+  logic atan real : real
+  
+  axiom Tan_atan : forall x:real. (tan (atan x) = x)
+  
+  (* use Trigonometry *)
+  
+  type mode =
+    | NearestTiesToEven
+    | ToZero
+    | Up
+    | Down
+    | NearTiesToAway
+  
+  (* use Rounding *)
+  
+  type single
+  
+  logic max_single : real = 0x1.FFFFFEp127
+  
+  logic max_int : int = 16777216
+  
+  logic infix_ls1 int int
+  
+  (* clone Assoc with type t = int, logic op = infix_pl6,
+    prop Assoc = Assoc15 *)
+  
+  (* clone Group with type t1 = int, logic inv = prefix_mn6,
+    logic op1 = infix_pl6, logic unit = zero6, prop Inv_def = Inv_def8,
+    prop Assoc2 = Assoc15, prop Unit_def = Unit_def8 *)
+  
+  (* clone Comm with type t2 = int, logic op2 = infix_pl6,
+    prop Comm = Comm13 *)
+  
+  (* meta AC logic infix_pl6 *)
+  
+  (* clone CommutativeGroup with type t3 = int, logic inv1 = prefix_mn6,
+    logic op3 = infix_pl6, logic unit1 = zero6, prop Comm2 = Comm13,
+    prop Inv_def2 = Inv_def8, prop Assoc3 = Assoc15,
+    prop Unit_def2 = Unit_def8 *)
+  
+  (* clone Assoc with type t = int, logic op = infix_as6,
+    prop Assoc = Assoc16 *)
+  
+  (* clone Ring with type t4 = int, logic infix_mn = infix_mn6,
+    logic infix_as1 = infix_as6, logic prefix_mn1 = prefix_mn6,
+    logic infix_pl1 = infix_pl6, logic zero1 = zero6,
+    prop Mul_distr = Mul_distr6, prop Assoc5 = Assoc16, prop Comm3 = Comm13,
+    prop Inv_def3 = Inv_def8, prop Assoc6 = Assoc15,
+    prop Unit_def3 = Unit_def8 *)
+  
+  (* clone Comm with type t2 = int, logic op2 = infix_as6,
+    prop Comm = Comm14 *)
+  
+  (* meta AC logic infix_as6 *)
+  
+  (* clone CommutativeRing with type t5 = int, logic infix_mn2 = infix_mn6,
+    logic infix_as2 = infix_as6, logic prefix_mn2 = prefix_mn6,
+    logic infix_pl2 = infix_pl6, logic zero2 = zero6, prop Comm5 = Comm14,
+    prop Mul_distr2 = Mul_distr6, prop Assoc7 = Assoc16, prop Comm6 = Comm13,
+    prop Inv_def4 = Inv_def8, prop Assoc8 = Assoc15,
+    prop Unit_def4 = Unit_def8 *)
+  
+  axiom NonTrivialRing4 : not (0 = 1)
+  
+  (* clone UnitaryCommutativeRing with type t6 = int, logic one = one4,
+    logic infix_mn3 = infix_mn6, logic infix_as3 = infix_as6,
+    logic prefix_mn3 = prefix_mn6, logic infix_pl3 = infix_pl6,
+    logic zero3 = zero6, prop NonTrivialRing1 = NonTrivialRing4,
+    prop Unitary = Unitary4, prop Comm7 = Comm14,
+    prop Mul_distr3 = Mul_distr6, prop Assoc9 = Assoc16, prop Comm8 = Comm13,
+    prop Inv_def5 = Inv_def8, prop Assoc10 = Assoc15,
+    prop Unit_def5 = Unit_def8 *)
+  
+  (* clone EndoRelation with type t8 = int, logic rel = infix_lseq2,  *)
+  
+  (* clone Reflexive with type t9 = int, logic rel1 = infix_lseq2,
+    prop Refl = Refl6 *)
+  
+  (* clone EndoRelation with type t8 = int, logic rel = infix_lseq2,  *)
+  
+  (* clone Transitive with type t10 = int, logic rel2 = infix_lseq2,
+    prop Trans = Trans6 *)
+  
+  (* clone PreOrder with type t11 = int, logic rel3 = infix_lseq2,
+    prop Trans2 = Trans6, prop Refl2 = Refl6 *)
+  
+  (* clone EndoRelation with type t8 = int, logic rel = infix_lseq2,  *)
+  
+  (* clone Antisymmetric with type t12 = int, logic rel4 = infix_lseq2,
+    prop Antisymm = Antisymm5 *)
+  
+  (* clone PartialOrder with type t13 = int, logic rel5 = infix_lseq2,
+    prop Antisymm2 = Antisymm5, prop Trans3 = Trans6, prop Refl3 = Refl6 *)
+  
+  (* clone EndoRelation with type t8 = int, logic rel = infix_lseq2,  *)
+  
+  (* clone Total with type t14 = int, logic rel6 = infix_lseq2,
+    prop Total = Total4 *)
+  
+  (* clone TotalOrder with type t15 = int, logic rel7 = infix_lseq2,
+    prop Total2 = Total4, prop Antisymm3 = Antisymm5, prop Trans4 = Trans6,
+    prop Refl4 = Refl6 *)
+  
+  axiom CompatOrderAdd2 : forall x:int, y:int, z:int. infix_ls1 x y or
+    (x = y) -> infix_ls1 (x + z) (y + z) or ((x + z) = (y + z))
+  
+  axiom CompatOrderMult2 : forall x:int, y:int, z:int. infix_ls1 x y or
+    (x = y) -> infix_ls1 0 z or (0 = z) -> infix_ls1 (x * z) (y * z) or
+    ((x * z) = (y * z))
+  
+  (* clone OrderedUnitaryCommutativeRing with type t17 = int,
+    logic infix_gteq2 = infix_gteq3, logic infix_lseq3 = infix_lseq2,
+    logic one5 = one4, logic infix_mn7 = infix_mn6,
+    logic infix_as7 = infix_as6, logic prefix_mn7 = prefix_mn6,
+    logic infix_pl7 = infix_pl6, logic zero7 = zero6,
+    prop CompatOrderMult3 = CompatOrderMult2,
+    prop CompatOrderAdd3 = CompatOrderAdd2, prop Total5 = Total4,
+    prop Antisymm6 = Antisymm5, prop Trans7 = Trans6, prop Refl7 = Refl6,
+    prop NonTrivialRing5 = NonTrivialRing4, prop Unitary5 = Unitary4,
+    prop Comm15 = Comm14, prop Mul_distr7 = Mul_distr6,
+    prop Assoc17 = Assoc16, prop Comm16 = Comm13, prop Inv_def9 = Inv_def8,
+    prop Assoc18 = Assoc15, prop Unit_def9 = Unit_def8 *)
+  
+  (* use Int *)
+  
+  logic from_int int : real
+  
+  axiom Zero : (from_int 0 = 0.0)
+  
+  axiom One : (from_int 1 = 1.0)
+  
+  axiom Add : forall x:int, y:int. (from_int (x + y) = (from_int x + from_int
+    y))
+  
+  axiom Sub : forall x:int, y:int. (from_int (x - y) = (from_int x - from_int
+    y))
+  
+  axiom Mul : forall x:int, y:int. (from_int (x * y) = (from_int x * from_int
+    y))
+  
+  axiom Neg : forall x:int, y:int. (from_int (-x) = (-from_int x))
+  
+  (* use FromInt *)
+  
+  logic round mode real : real
+  
+  logic round_logic mode real : single
+  
+  logic value single : real
+  
+  logic exact single : real
+  
+  logic model single : real
+  
+  logic round_error (x:single) : real = | (value x - exact x) |
+  
+  logic total_error (x:single) : real = | (value x - model x) |
+  
+  logic no_overflow (m:mode) (x:real) = infix_ls | round m x | max_single or
+    (| round m x | = max_single)
+  
+  axiom Bounded_real_no_overflow : forall m:mode, x:real. infix_ls | x |
+    max_single or (| x | = max_single) -> no_overflow m x
+  
+  axiom Round_monotonic : forall m:mode, x:real, y:real. infix_ls x y or
+    (x = y) -> infix_ls (round m x) (round m y) or (round m x = round m y)
+  
+  axiom Exact_rounding_for_integers : forall m:mode, i:int. (infix_ls1
+    (-max_int) i or ((-max_int) = i)) and (infix_ls1 i max_int or
+    (i = max_int)) -> (round m (from_int i) = from_int i)
+  
+  axiom Round_down_le : forall x:real. infix_ls (round Down x) x or (round
+    Down x = x)
+  
+  axiom Round_up_ge : forall x:real. infix_ls x (round Up x) or (x = round Up
+    x)
+  
+  axiom Round_down_neg : forall x:real. (round Down (-x) = (-round Up x))
+  
+  axiom Round_up_neg : forall x:real. (round Up (-x) = (-round Down x))
+  
+  (* clone GenFloat with type t18 = single,
+    logic max_representable_integer = max_int,
+    logic no_overflow1 = no_overflow, logic max = max_single,
+    logic total_error1 = total_error, logic round_error1 = round_error,
+    logic model1 = model, logic exact1 = exact, logic value1 = value,
+    logic round_logic1 = round_logic, logic round1 = round,
+    prop Round_up_neg1 = Round_up_neg, prop Round_down_neg1 = Round_down_neg,
+    prop Round_up_ge1 = Round_up_ge, prop Round_down_le1 = Round_down_le,
+    prop Exact_rounding_for_integers1 = Exact_rounding_for_integers,
+    prop Round_monotonic1 = Round_monotonic,
+    prop Bounded_real_no_overflow1 = Bounded_real_no_overflow *)
+  
+  (* use Single *)
+  
+  (* meta syntax_type type int, "int" *)
+  
+  (* meta syntax_type type real, "real" *)
+  
+  (* meta syntax_logic logic infix_eq, "(%1 = %2)" *)
+  
+  (* meta syntax_logic logic zero6, "0" *)
+  
+  (* meta syntax_logic logic one4, "1" *)
+  
+  (* meta syntax_logic logic infix_pl6, "(%1 + %2)" *)
+  
+  (* meta syntax_logic logic infix_mn6, "(%1 - %2)" *)
+  
+  (* meta syntax_logic logic infix_as6, "(%1 * %2)" *)
+  
+  (* meta syntax_logic logic prefix_mn6, "(-%1)" *)
+  
+  (* meta inline : no logic infix_lseq2 *)
+  
+  (* meta inline : no logic infix_gteq3 *)
+  
+  (* meta inline : no logic infix_gt *)
+  
+  (* meta remove_prop prop Comm13 *)
+  
+  (* meta remove_prop prop Assoc15 *)
+  
+  (* meta remove_prop prop Unit_def8 *)
+  
+  (* meta remove_prop prop Inv_def8 *)
+  
+  (* meta remove_prop prop Assoc16 *)
+  
+  (* meta remove_prop prop Mul_distr6 *)
+  
+  (* meta remove_prop prop Comm14 *)
+  
+  (* meta remove_prop prop Unitary4 *)
+  
+  (* meta remove_prop prop Refl6 *)
+  
+  (* meta remove_prop prop Trans6 *)
+  
+  (* meta remove_prop prop Total4 *)
+  
+  (* meta remove_prop prop Antisymm5 *)
+  
+  (* meta syntax_logic logic zero, "0.0" *)
+  
+  (* meta syntax_logic logic one1, "1.0" *)
+  
+  (* meta syntax_logic logic infix_pl, "(%1 + %2)" *)
+  
+  (* meta syntax_logic logic infix_mn1, "(%1 - %2)" *)
+  
+  (* meta syntax_logic logic infix_as, "(%1 * %2)" *)
+  
+  (* meta syntax_logic logic infix_sl1, "(%1 / %2)" *)
+  
+  (* meta syntax_logic logic prefix_mn, "(-%1)" *)
+  
+  (* meta syntax_logic logic inv3, "(1.0 / %1)" *)
+  
+  (* meta inline : no logic infix_lseq *)
+  
+  (* meta inline : no logic infix_gteq1 *)
+  
+  (* meta inline : no logic infix_gt1 *)
+  
+  (* meta remove_prop prop Comm1 *)
+  
+  (* meta remove_prop prop Assoc1 *)
+  
+  (* meta remove_prop prop Unit_def1 *)
+  
+  (* meta remove_prop prop Inv_def1 *)
+  
+  (* meta remove_prop prop Assoc4 *)
+  
+  (* meta remove_prop prop Mul_distr1 *)
+  
+  (* meta remove_prop prop Comm4 *)
+  
+  (* meta remove_prop prop Unitary1 *)
+  
+  (* meta remove_prop prop Refl1 *)
+  
+  (* meta remove_prop prop Trans1 *)
+  
+  (* meta remove_prop prop Total1 *)
+  
+  (* meta remove_prop prop Antisymm1 *)
+  
+  (* meta remove_prop prop Inverse1 *)
+  
+  (* meta syntax_logic logic abs, "| %1 |" *)
+  
+  goal MethodError : forall x:real. infix_ls | x | 0x1.p-5 or
+    (| x | = 0x1.p-5) -> infix_ls | ((1.0 - ((x * x) * 0.5)) - cos x) |
+    0x1.p-24 or (| ((1.0 - ((x * x) * 0.5)) - cos x) | = 0x1.p-24)
+  
+  
+end
diff --git a/T/my_cosine-CosineSingle-MethodError.why b/T/my_cosine-CosineSingle-MethodError.why
new file mode 100644
index 0000000000000000000000000000000000000000..1b94d815496e626ba422c29bb41422e6476034af
--- /dev/null
+++ b/T/my_cosine-CosineSingle-MethodError.why
@@ -0,0 +1,500 @@
+theory Task
+  (* use BuiltIn *)
+  
+  logic zero : real = 0.0
+  
+  logic one : real = 1.0
+  
+  logic infix_ls real real
+  
+  logic infix_gt (x:real) (y:real) = infix_ls y x
+  
+  logic infix_lseq (x:real) (y:real) = infix_ls x y or (x = y)
+  
+  logic infix_pl real real : real
+  
+  logic prefix_mn real : real
+  
+  logic infix_as real real : real
+  
+  axiom Unit_def : forall x:real. (infix_pl x zero = x)
+  
+  axiom Assoc : forall x:real, y:real, z:real. (infix_pl (infix_pl x y)
+    z = infix_pl x (infix_pl y z))
+  
+  (* clone Assoc with type t = real, logic op = infix_pl,
+    prop Assoc1 = Assoc *)
+  
+  axiom Inv_def : forall x:real. (infix_pl x (prefix_mn x) = zero)
+  
+  (* clone Group with type t1 = real, logic inv = prefix_mn,
+    logic op1 = infix_pl, logic unit = zero, prop Inv_def1 = Inv_def,
+    prop Assoc2 = Assoc, prop Unit_def1 = Unit_def *)
+  
+  axiom Comm : forall x:real, y:real. (infix_pl x y = infix_pl y x)
+  
+  (* clone Comm with type t2 = real, logic op2 = infix_pl,
+    prop Comm1 = Comm *)
+  
+  (* meta AC logic infix_pl *)
+  
+  (* clone CommutativeGroup with type t3 = real, logic inv1 = prefix_mn,
+    logic op3 = infix_pl, logic unit1 = zero, prop Comm2 = Comm,
+    prop Inv_def2 = Inv_def, prop Assoc3 = Assoc,
+    prop Unit_def2 = Unit_def *)
+  
+  axiom Assoc4 : forall x:real, y:real, z:real. (infix_as (infix_as x y)
+    z = infix_as x (infix_as y z))
+  
+  (* clone Assoc with type t = real, logic op = infix_as,
+    prop Assoc1 = Assoc4 *)
+  
+  axiom Mul_distr : forall x:real, y:real, z:real. (infix_as x (infix_pl y
+    z) = infix_pl (infix_as x y) (infix_as x z))
+  
+  logic infix_mn (x:real) (y:real) : real = infix_pl x (prefix_mn y)
+  
+  (* clone Ring with type t4 = real, logic infix_mn1 = infix_mn,
+    logic infix_as1 = infix_as, logic prefix_mn1 = prefix_mn,
+    logic infix_pl1 = infix_pl, logic zero1 = zero,
+    prop Mul_distr1 = Mul_distr, prop Assoc5 = Assoc4, prop Comm3 = Comm,
+    prop Inv_def3 = Inv_def, prop Assoc6 = Assoc,
+    prop Unit_def3 = Unit_def *)
+  
+  axiom Comm4 : forall x:real, y:real. (infix_as x y = infix_as y x)
+  
+  (* clone Comm with type t2 = real, logic op2 = infix_as,
+    prop Comm1 = Comm4 *)
+  
+  (* meta AC logic infix_as *)
+  
+  (* clone CommutativeRing with type t5 = real, logic infix_mn2 = infix_mn,
+    logic infix_as2 = infix_as, logic prefix_mn2 = prefix_mn,
+    logic infix_pl2 = infix_pl, logic zero2 = zero, prop Comm5 = Comm4,
+    prop Mul_distr2 = Mul_distr, prop Assoc7 = Assoc4, prop Comm6 = Comm,
+    prop Inv_def4 = Inv_def, prop Assoc8 = Assoc,
+    prop Unit_def4 = Unit_def *)
+  
+  axiom Unitary : forall x:real. (infix_as one x = x)
+  
+  axiom NonTrivialRing : not (zero = one)
+  
+  (* clone UnitaryCommutativeRing with type t6 = real, logic one1 = one,
+    logic infix_mn3 = infix_mn, logic infix_as3 = infix_as,
+    logic prefix_mn3 = prefix_mn, logic infix_pl3 = infix_pl,
+    logic zero3 = zero, prop NonTrivialRing1 = NonTrivialRing,
+    prop Unitary1 = Unitary, prop Comm7 = Comm4, prop Mul_distr3 = Mul_distr,
+    prop Assoc9 = Assoc4, prop Comm8 = Comm, prop Inv_def5 = Inv_def,
+    prop Assoc10 = Assoc, prop Unit_def5 = Unit_def *)
+  
+  logic inv2 real : real
+  
+  axiom Inverse : forall x:real. not (x = zero) -> (infix_as x (inv2
+    x) = one)
+  
+  logic infix_sl (x:real) (y:real) : real = infix_as x (inv2 y)
+  
+  (* clone Field with type t7 = real, logic infix_sl1 = infix_sl,
+    logic inv3 = inv2, logic one2 = one, logic infix_mn4 = infix_mn,
+    logic infix_as4 = infix_as, logic prefix_mn4 = prefix_mn,
+    logic infix_pl4 = infix_pl, logic zero4 = zero, prop Inverse1 = Inverse,
+    prop NonTrivialRing2 = NonTrivialRing, prop Unitary2 = Unitary,
+    prop Comm9 = Comm4, prop Mul_distr4 = Mul_distr, prop Assoc11 = Assoc4,
+    prop Comm10 = Comm, prop Inv_def6 = Inv_def, prop Assoc12 = Assoc,
+    prop Unit_def6 = Unit_def *)
+  
+  logic infix_gteq (x:real) (y:real) = infix_lseq y x
+  
+  (* clone EndoRelation with type t8 = real, logic rel = infix_lseq,  *)
+  
+  axiom Refl : forall x:real. infix_lseq x x
+  
+  (* clone Reflexive with type t9 = real, logic rel1 = infix_lseq,
+    prop Refl1 = Refl *)
+  
+  (* clone EndoRelation with type t8 = real, logic rel = infix_lseq,  *)
+  
+  axiom Trans : forall x:real, y:real, z:real. infix_lseq x y -> infix_lseq y
+    z -> infix_lseq x z
+  
+  (* clone Transitive with type t10 = real, logic rel2 = infix_lseq,
+    prop Trans1 = Trans *)
+  
+  (* clone PreOrder with type t11 = real, logic rel3 = infix_lseq,
+    prop Trans2 = Trans, prop Refl2 = Refl *)
+  
+  (* clone EndoRelation with type t8 = real, logic rel = infix_lseq,  *)
+  
+  axiom Antisymm : forall x:real, y:real. infix_lseq x y -> infix_lseq y x ->
+    (x = y)
+  
+  (* clone Antisymmetric with type t12 = real, logic rel4 = infix_lseq,
+    prop Antisymm1 = Antisymm *)
+  
+  (* clone PartialOrder with type t13 = real, logic rel5 = infix_lseq,
+    prop Antisymm2 = Antisymm, prop Trans3 = Trans, prop Refl3 = Refl *)
+  
+  (* clone EndoRelation with type t8 = real, logic rel = infix_lseq,  *)
+  
+  axiom Total : forall x:real, y:real. infix_lseq x y or infix_lseq y x
+  
+  (* clone Total with type t14 = real, logic rel6 = infix_lseq,
+    prop Total1 = Total *)
+  
+  (* clone TotalOrder with type t15 = real, logic rel7 = infix_lseq,
+    prop Total2 = Total, prop Antisymm3 = Antisymm, prop Trans4 = Trans,
+    prop Refl4 = Refl *)
+  
+  axiom CompatOrderAdd : forall x:real, y:real, z:real. infix_lseq x y ->
+    infix_lseq (infix_pl x z) (infix_pl y z)
+  
+  axiom CompatOrderMult : forall x:real, y:real, z:real. infix_lseq x y ->
+    infix_lseq zero z -> infix_lseq (infix_as x z) (infix_as y z)
+  
+  (* clone OrderedField with type t16 = real, logic infix_gteq1 = infix_gteq,
+    logic infix_lseq1 = infix_lseq, logic infix_sl2 = infix_sl,
+    logic inv4 = inv2, logic one3 = one, logic infix_mn5 = infix_mn,
+    logic infix_as5 = infix_as, logic prefix_mn5 = prefix_mn,
+    logic infix_pl5 = infix_pl, logic zero5 = zero,
+    prop CompatOrderMult1 = CompatOrderMult,
+    prop CompatOrderAdd1 = CompatOrderAdd, prop Total3 = Total,
+    prop Antisymm4 = Antisymm, prop Trans5 = Trans, prop Refl5 = Refl,
+    prop Inverse2 = Inverse, prop NonTrivialRing3 = NonTrivialRing,
+    prop Unitary3 = Unitary, prop Comm11 = Comm4,
+    prop Mul_distr5 = Mul_distr, prop Assoc13 = Assoc4, prop Comm12 = Comm,
+    prop Inv_def7 = Inv_def, prop Assoc14 = Assoc,
+    prop Unit_def7 = Unit_def *)
+  
+  (* use Real *)
+  
+  logic abs (x:real) : real = if infix_gteq x 0.0 then x else prefix_mn x
+  
+  axiom Abs_le : forall x:real, y:real. infix_lseq (abs x) y <-> infix_lseq
+    (prefix_mn y) x and infix_lseq x y
+  
+  axiom Abs_pos : forall x:real. infix_gteq (abs x) 0.0
+  
+  (* use Abs *)
+  
+  logic sqr (x:real) : real = infix_as x x
+  
+  logic sqrt real : real
+  
+  axiom Sqrt_positive : forall x:real. infix_gteq x 0.0 -> infix_gteq (sqrt
+    x) 0.0
+  
+  axiom Sqrt_square : forall x:real. infix_gteq x 0.0 -> (sqr (sqrt x) = x)
+  
+  axiom Square_sqrt : forall x:real. infix_gteq x 0.0 -> (sqrt (infix_as x
+    x) = x)
+  
+  (* use Square *)
+  
+  logic cos real : real
+  
+  logic sin real : real
+  
+  axiom Pythagorean_identity : forall x:real. (infix_pl (sqr (cos x)) (sqr
+    (sin x)) = 1.0)
+  
+  axiom Cos_le_one : forall x:real. infix_lseq (abs (cos x)) 1.0
+  
+  axiom Sin_le_one : forall x:real. infix_lseq (abs (sin x)) 1.0
+  
+  axiom Cos_0 : (cos 0.0 = 1.0)
+  
+  axiom Sin_0 : (sin 0.0 = 0.0)
+  
+  logic pi : real
+  
+  axiom Pi_interval : infix_ls
+    3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196
+    pi and infix_ls pi
+    3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197
+  
+  axiom Cos_pi : (cos pi = prefix_mn 1.0)
+  
+  axiom Sin_pi : (sin pi = 0.0)
+  
+  axiom Cos_pi2 : (cos (infix_as 0.5 pi) = 0.0)
+  
+  axiom Sin_pi2 : (sin (infix_as 0.5 pi) = 1.0)
+  
+  axiom Cos_plus_pi : forall x:real. (cos (infix_pl x pi) = prefix_mn (cos
+    x))
+  
+  axiom Sin_plus_pi : forall x:real. (sin (infix_pl x pi) = prefix_mn (sin
+    x))
+  
+  axiom Cos_plus_pi2 : forall x:real. (cos (infix_pl x (infix_as 0.5
+    pi)) = prefix_mn (sin x))
+  
+  axiom Sin_plus_pi2 : forall x:real. (sin (infix_pl x (infix_as 0.5
+    pi)) = cos x)
+  
+  axiom Cos_neg : forall x:real. (cos (prefix_mn x) = cos x)
+  
+  axiom Sin_neg : forall x:real. (sin (prefix_mn x) = prefix_mn (sin x))
+  
+  axiom Cos_sum : forall x:real, y:real. (cos (infix_pl x y) = infix_mn
+    (infix_as (cos x) (cos y)) (infix_as (sin x) (sin y)))
+  
+  axiom Sin_sum : forall x:real, y:real. (sin (infix_pl x y) = infix_pl
+    (infix_as (sin x) (cos y)) (infix_as (cos x) (sin y)))
+  
+  logic tan (x:real) : real = infix_sl (sin x) (cos x)
+  
+  logic atan real : real
+  
+  axiom Tan_atan : forall x:real. (tan (atan x) = x)
+  
+  (* use Trigonometry *)
+  
+  type mode =
+    | NearestTiesToEven
+    | ToZero
+    | Up
+    | Down
+    | NearTiesToAway
+  
+  (* use Rounding *)
+  
+  type single
+  
+  logic max_single : real = 0x1.FFFFFEp127
+  
+  logic max_int : int = 16777216
+  
+  logic zero6 : int = 0
+  
+  logic one4 : int = 1
+  
+  logic infix_ls1 int int
+  
+  logic infix_gt1 (x:int) (y:int) = infix_ls1 y x
+  
+  logic infix_lseq2 (x:int) (y:int) = infix_ls1 x y or (x = y)
+  
+  logic infix_pl6 int int : int
+  
+  logic prefix_mn6 int : int
+  
+  logic infix_as6 int int : int
+  
+  axiom Unit_def8 : forall x:int. (infix_pl6 x zero6 = x)
+  
+  axiom Assoc15 : forall x:int, y:int, z:int. (infix_pl6 (infix_pl6 x y)
+    z = infix_pl6 x (infix_pl6 y z))
+  
+  (* clone Assoc with type t = int, logic op = infix_pl6,
+    prop Assoc1 = Assoc15 *)
+  
+  axiom Inv_def8 : forall x:int. (infix_pl6 x (prefix_mn6 x) = zero6)
+  
+  (* clone Group with type t1 = int, logic inv = prefix_mn6,
+    logic op1 = infix_pl6, logic unit = zero6, prop Inv_def1 = Inv_def8,
+    prop Assoc2 = Assoc15, prop Unit_def1 = Unit_def8 *)
+  
+  axiom Comm13 : forall x:int, y:int. (infix_pl6 x y = infix_pl6 y x)
+  
+  (* clone Comm with type t2 = int, logic op2 = infix_pl6,
+    prop Comm1 = Comm13 *)
+  
+  (* meta AC logic infix_pl6 *)
+  
+  (* clone CommutativeGroup with type t3 = int, logic inv1 = prefix_mn6,
+    logic op3 = infix_pl6, logic unit1 = zero6, prop Comm2 = Comm13,
+    prop Inv_def2 = Inv_def8, prop Assoc3 = Assoc15,
+    prop Unit_def2 = Unit_def8 *)
+  
+  axiom Assoc16 : forall x:int, y:int, z:int. (infix_as6 (infix_as6 x y)
+    z = infix_as6 x (infix_as6 y z))
+  
+  (* clone Assoc with type t = int, logic op = infix_as6,
+    prop Assoc1 = Assoc16 *)
+  
+  axiom Mul_distr6 : forall x:int, y:int, z:int. (infix_as6 x (infix_pl6 y
+    z) = infix_pl6 (infix_as6 x y) (infix_as6 x z))
+  
+  logic infix_mn6 (x:int) (y:int) : int = infix_pl6 x (prefix_mn6 y)
+  
+  (* clone Ring with type t4 = int, logic infix_mn1 = infix_mn6,
+    logic infix_as1 = infix_as6, logic prefix_mn1 = prefix_mn6,
+    logic infix_pl1 = infix_pl6, logic zero1 = zero6,
+    prop Mul_distr1 = Mul_distr6, prop Assoc5 = Assoc16, prop Comm3 = Comm13,
+    prop Inv_def3 = Inv_def8, prop Assoc6 = Assoc15,
+    prop Unit_def3 = Unit_def8 *)
+  
+  axiom Comm14 : forall x:int, y:int. (infix_as6 x y = infix_as6 y x)
+  
+  (* clone Comm with type t2 = int, logic op2 = infix_as6,
+    prop Comm1 = Comm14 *)
+  
+  (* meta AC logic infix_as6 *)
+  
+  (* clone CommutativeRing with type t5 = int, logic infix_mn2 = infix_mn6,
+    logic infix_as2 = infix_as6, logic prefix_mn2 = prefix_mn6,
+    logic infix_pl2 = infix_pl6, logic zero2 = zero6, prop Comm5 = Comm14,
+    prop Mul_distr2 = Mul_distr6, prop Assoc7 = Assoc16, prop Comm6 = Comm13,
+    prop Inv_def4 = Inv_def8, prop Assoc8 = Assoc15,
+    prop Unit_def4 = Unit_def8 *)
+  
+  axiom Unitary4 : forall x:int. (infix_as6 one4 x = x)
+  
+  axiom NonTrivialRing4 : not (zero6 = one4)
+  
+  (* clone UnitaryCommutativeRing with type t6 = int, logic one1 = one4,
+    logic infix_mn3 = infix_mn6, logic infix_as3 = infix_as6,
+    logic prefix_mn3 = prefix_mn6, logic infix_pl3 = infix_pl6,
+    logic zero3 = zero6, prop NonTrivialRing1 = NonTrivialRing4,
+    prop Unitary1 = Unitary4, prop Comm7 = Comm14,
+    prop Mul_distr3 = Mul_distr6, prop Assoc9 = Assoc16, prop Comm8 = Comm13,
+    prop Inv_def5 = Inv_def8, prop Assoc10 = Assoc15,
+    prop Unit_def5 = Unit_def8 *)
+  
+  logic infix_gteq2 (x:int) (y:int) = infix_lseq2 y x
+  
+  (* clone EndoRelation with type t8 = int, logic rel = infix_lseq2,  *)
+  
+  axiom Refl6 : forall x:int. infix_lseq2 x x
+  
+  (* clone Reflexive with type t9 = int, logic rel1 = infix_lseq2,
+    prop Refl1 = Refl6 *)
+  
+  (* clone EndoRelation with type t8 = int, logic rel = infix_lseq2,  *)
+  
+  axiom Trans6 : forall x:int, y:int, z:int. infix_lseq2 x y -> infix_lseq2 y
+    z -> infix_lseq2 x z
+  
+  (* clone Transitive with type t10 = int, logic rel2 = infix_lseq2,
+    prop Trans1 = Trans6 *)
+  
+  (* clone PreOrder with type t11 = int, logic rel3 = infix_lseq2,
+    prop Trans2 = Trans6, prop Refl2 = Refl6 *)
+  
+  (* clone EndoRelation with type t8 = int, logic rel = infix_lseq2,  *)
+  
+  axiom Antisymm5 : forall x:int, y:int. infix_lseq2 x y -> infix_lseq2 y
+    x -> (x = y)
+  
+  (* clone Antisymmetric with type t12 = int, logic rel4 = infix_lseq2,
+    prop Antisymm1 = Antisymm5 *)
+  
+  (* clone PartialOrder with type t13 = int, logic rel5 = infix_lseq2,
+    prop Antisymm2 = Antisymm5, prop Trans3 = Trans6, prop Refl3 = Refl6 *)
+  
+  (* clone EndoRelation with type t8 = int, logic rel = infix_lseq2,  *)
+  
+  axiom Total4 : forall x:int, y:int. infix_lseq2 x y or infix_lseq2 y x
+  
+  (* clone Total with type t14 = int, logic rel6 = infix_lseq2,
+    prop Total1 = Total4 *)
+  
+  (* clone TotalOrder with type t15 = int, logic rel7 = infix_lseq2,
+    prop Total2 = Total4, prop Antisymm3 = Antisymm5, prop Trans4 = Trans6,
+    prop Refl4 = Refl6 *)
+  
+  axiom CompatOrderAdd2 : forall x:int, y:int, z:int. infix_lseq2 x y ->
+    infix_lseq2 (infix_pl6 x z) (infix_pl6 y z)
+  
+  axiom CompatOrderMult2 : forall x:int, y:int, z:int. infix_lseq2 x y ->
+    infix_lseq2 zero6 z -> infix_lseq2 (infix_as6 x z) (infix_as6 y z)
+  
+  (* clone OrderedUnitaryCommutativeRing with type t17 = int,
+    logic infix_gteq3 = infix_gteq2, logic infix_lseq3 = infix_lseq2,
+    logic one5 = one4, logic infix_mn7 = infix_mn6,
+    logic infix_as7 = infix_as6, logic prefix_mn7 = prefix_mn6,
+    logic infix_pl7 = infix_pl6, logic zero7 = zero6,
+    prop CompatOrderMult3 = CompatOrderMult2,
+    prop CompatOrderAdd3 = CompatOrderAdd2, prop Total5 = Total4,
+    prop Antisymm6 = Antisymm5, prop Trans7 = Trans6, prop Refl7 = Refl6,
+    prop NonTrivialRing5 = NonTrivialRing4, prop Unitary5 = Unitary4,
+    prop Comm15 = Comm14, prop Mul_distr7 = Mul_distr6,
+    prop Assoc17 = Assoc16, prop Comm16 = Comm13, prop Inv_def9 = Inv_def8,
+    prop Assoc18 = Assoc15, prop Unit_def9 = Unit_def8 *)
+  
+  (* use Int *)
+  
+  logic from_int int : real
+  
+  axiom Zero : (from_int 0 = 0.0)
+  
+  axiom One : (from_int 1 = 1.0)
+  
+  axiom Add : forall x:int, y:int. (from_int (infix_pl6 x y) = infix_pl
+    (from_int x) (from_int y))
+  
+  axiom Sub : forall x:int, y:int. (from_int (infix_mn6 x y) = infix_mn
+    (from_int x) (from_int y))
+  
+  axiom Mul : forall x:int, y:int. (from_int (infix_as6 x y) = infix_as
+    (from_int x) (from_int y))
+  
+  axiom Neg : forall x:int, y:int. (from_int (prefix_mn6 x) = prefix_mn
+    (from_int x))
+  
+  (* use FromInt *)
+  
+  logic round mode real : real
+  
+  logic round_logic mode real : single
+  
+  logic value single : real
+  
+  logic exact single : real
+  
+  logic model single : real
+  
+  logic round_error (x:single) : real = abs (infix_mn (value x) (exact x))
+  
+  logic total_error (x:single) : real = abs (infix_mn (value x) (model x))
+  
+  logic no_overflow (m:mode) (x:real) = infix_lseq (abs (round m x))
+    max_single
+  
+  axiom Bounded_real_no_overflow : forall m:mode, x:real. infix_lseq (abs x)
+    max_single -> no_overflow m x
+  
+  axiom Round_monotonic : forall m:mode, x:real, y:real. infix_lseq x y ->
+    infix_lseq (round m x) (round m y)
+  
+  axiom Exact_rounding_for_integers : forall m:mode, i:int. infix_lseq2
+    (prefix_mn6 max_int) i and infix_lseq2 i max_int -> (round m (from_int
+    i) = from_int i)
+  
+  axiom Round_down_le : forall x:real. infix_lseq (round Down x) x
+  
+  axiom Round_up_ge : forall x:real. infix_gteq (round Up x) x
+  
+  axiom Round_down_neg : forall x:real. (round Down (prefix_mn x) = prefix_mn
+    (round Up x))
+  
+  axiom Round_up_neg : forall x:real. (round Up (prefix_mn x) = prefix_mn
+    (round Down x))
+  
+  (* clone GenFloat with type t18 = single,
+    logic max_representable_integer = max_int,
+    logic no_overflow1 = no_overflow, logic max = max_single,
+    logic total_error1 = total_error, logic round_error1 = round_error,
+    logic model1 = model, logic exact1 = exact, logic value1 = value,
+    logic round_logic1 = round_logic, logic round1 = round,
+    prop Round_up_neg1 = Round_up_neg, prop Round_down_neg1 = Round_down_neg,
+    prop Round_up_ge1 = Round_up_ge, prop Round_down_le1 = Round_down_le,
+    prop Exact_rounding_for_integers1 = Exact_rounding_for_integers,
+    prop Round_monotonic1 = Round_monotonic,
+    prop Bounded_real_no_overflow1 = Bounded_real_no_overflow *)
+  
+  (* use Single *)
+  
+  (* meta syntax_type type int, "int" *)
+  
+  (* meta syntax_type type real, "real" *)
+  
+  (* meta syntax_logic logic infix_eq, "(%1 = %2)" *)
+  
+  goal MethodError : forall x:real. infix_lseq (abs x) 0x1.p-5 -> infix_lseq
+    (abs (infix_mn (infix_mn 1.0 (infix_as (infix_as x x) 0.5)) (cos x)))
+    0x1.p-24
+  
+  
+end
diff --git a/T/my_cosine-CosineSingle-TotalError.gappa b/T/my_cosine-CosineSingle-TotalError.gappa
new file mode 100644
index 0000000000000000000000000000000000000000..104cc1be9f518d1b332036e24145f98f7988156e
--- /dev/null
+++ b/T/my_cosine-CosineSingle-TotalError.gappa
@@ -0,0 +1,509 @@
+# this is a prelude for Gappa
+# this is a prelude for Gappa real arithmetic
+# this is a prelude for Gappa integer arithmetic
+@rnd_ieee32_ne=float<ieee_32,ne>;
+theory Task
+  (* use BuiltIn *)
+  
+  logic infix_ls real real
+  
+  (* clone Assoc with type t = real, logic op = infix_pl,
+    prop Assoc = Assoc1 *)
+  
+  (* clone Group with type t1 = real, logic inv = prefix_mn,
+    logic op1 = infix_pl, logic unit = zero, prop Inv_def = Inv_def1,
+    prop Assoc2 = Assoc1, prop Unit_def = Unit_def1 *)
+  
+  (* clone Comm with type t2 = real, logic op2 = infix_pl,
+    prop Comm = Comm1 *)
+  
+  (* meta AC logic infix_pl *)
+  
+  (* clone CommutativeGroup with type t3 = real, logic inv1 = prefix_mn,
+    logic op3 = infix_pl, logic unit1 = zero, prop Comm2 = Comm1,
+    prop Inv_def2 = Inv_def1, prop Assoc3 = Assoc1,
+    prop Unit_def2 = Unit_def1 *)
+  
+  (* clone Assoc with type t = real, logic op = infix_as,
+    prop Assoc = Assoc4 *)
+  
+  (* clone Ring with type t4 = real, logic infix_mn = infix_mn1,
+    logic infix_as1 = infix_as, logic prefix_mn1 = prefix_mn,
+    logic infix_pl1 = infix_pl, logic zero1 = zero,
+    prop Mul_distr = Mul_distr1, prop Assoc5 = Assoc4, prop Comm3 = Comm1,
+    prop Inv_def3 = Inv_def1, prop Assoc6 = Assoc1,
+    prop Unit_def3 = Unit_def1 *)
+  
+  (* clone Comm with type t2 = real, logic op2 = infix_as,
+    prop Comm = Comm4 *)
+  
+  (* meta AC logic infix_as *)
+  
+  (* clone CommutativeRing with type t5 = real, logic infix_mn2 = infix_mn1,
+    logic infix_as2 = infix_as, logic prefix_mn2 = prefix_mn,
+    logic infix_pl2 = infix_pl, logic zero2 = zero, prop Comm5 = Comm4,
+    prop Mul_distr2 = Mul_distr1, prop Assoc7 = Assoc4, prop Comm6 = Comm1,
+    prop Inv_def4 = Inv_def1, prop Assoc8 = Assoc1,
+    prop Unit_def4 = Unit_def1 *)
+  
+  axiom NonTrivialRing : not (0.0 = 1.0)
+  
+  (* clone UnitaryCommutativeRing with type t6 = real, logic one = one1,
+    logic infix_mn3 = infix_mn1, logic infix_as3 = infix_as,
+    logic prefix_mn3 = prefix_mn, logic infix_pl3 = infix_pl,
+    logic zero3 = zero, prop NonTrivialRing1 = NonTrivialRing,
+    prop Unitary = Unitary1, prop Comm7 = Comm4,
+    prop Mul_distr3 = Mul_distr1, prop Assoc9 = Assoc4, prop Comm8 = Comm1,
+    prop Inv_def5 = Inv_def1, prop Assoc10 = Assoc1,
+    prop Unit_def5 = Unit_def1 *)
+  
+  (* clone Field with type t7 = real, logic infix_sl = infix_sl1,
+    logic inv2 = inv3, logic one2 = one1, logic infix_mn4 = infix_mn1,
+    logic infix_as4 = infix_as, logic prefix_mn4 = prefix_mn,
+    logic infix_pl4 = infix_pl, logic zero4 = zero, prop Inverse = Inverse1,
+    prop NonTrivialRing2 = NonTrivialRing, prop Unitary2 = Unitary1,
+    prop Comm9 = Comm4, prop Mul_distr4 = Mul_distr1, prop Assoc11 = Assoc4,
+    prop Comm10 = Comm1, prop Inv_def6 = Inv_def1, prop Assoc12 = Assoc1,
+    prop Unit_def6 = Unit_def1 *)
+  
+  (* clone EndoRelation with type t8 = real, logic rel = infix_lseq,  *)
+  
+  (* clone Reflexive with type t9 = real, logic rel1 = infix_lseq,
+    prop Refl = Refl1 *)
+  
+  (* clone EndoRelation with type t8 = real, logic rel = infix_lseq,  *)
+  
+  (* clone Transitive with type t10 = real, logic rel2 = infix_lseq,
+    prop Trans = Trans1 *)
+  
+  (* clone PreOrder with type t11 = real, logic rel3 = infix_lseq,
+    prop Trans2 = Trans1, prop Refl2 = Refl1 *)
+  
+  (* clone EndoRelation with type t8 = real, logic rel = infix_lseq,  *)
+  
+  (* clone Antisymmetric with type t12 = real, logic rel4 = infix_lseq,
+    prop Antisymm = Antisymm1 *)
+  
+  (* clone PartialOrder with type t13 = real, logic rel5 = infix_lseq,
+    prop Antisymm2 = Antisymm1, prop Trans3 = Trans1, prop Refl3 = Refl1 *)
+  
+  (* clone EndoRelation with type t8 = real, logic rel = infix_lseq,  *)
+  
+  (* clone Total with type t14 = real, logic rel6 = infix_lseq,
+    prop Total = Total1 *)
+  
+  (* clone TotalOrder with type t15 = real, logic rel7 = infix_lseq,
+    prop Total2 = Total1, prop Antisymm3 = Antisymm1, prop Trans4 = Trans1,
+    prop Refl4 = Refl1 *)
+  
+  axiom CompatOrderAdd : forall x:real, y:real, z:real. infix_ls x y or
+    (x = y) -> infix_ls (x + z) (y + z) or ((x + z) = (y + z))
+  
+  axiom CompatOrderMult : forall x:real, y:real, z:real. infix_ls x y or
+    (x = y) -> infix_ls 0.0 z or (0.0 = z) -> infix_ls (x * z) (y * z) or
+    ((x * z) = (y * z))
+  
+  (* clone OrderedField with type t16 = real, logic infix_gteq = infix_gteq1,
+    logic infix_lseq1 = infix_lseq, logic infix_sl2 = infix_sl1,
+    logic inv4 = inv3, logic one3 = one1, logic infix_mn5 = infix_mn1,
+    logic infix_as5 = infix_as, logic prefix_mn5 = prefix_mn,
+    logic infix_pl5 = infix_pl, logic zero5 = zero,
+    prop CompatOrderMult1 = CompatOrderMult,
+    prop CompatOrderAdd1 = CompatOrderAdd, prop Total3 = Total1,
+    prop Antisymm4 = Antisymm1, prop Trans5 = Trans1, prop Refl5 = Refl1,
+    prop Inverse2 = Inverse1, prop NonTrivialRing3 = NonTrivialRing,
+    prop Unitary3 = Unitary1, prop Comm11 = Comm4,
+    prop Mul_distr5 = Mul_distr1, prop Assoc13 = Assoc4, prop Comm12 = Comm1,
+    prop Inv_def7 = Inv_def1, prop Assoc14 = Assoc1,
+    prop Unit_def7 = Unit_def1 *)
+  
+  (* use Real *)
+  
+  axiom Abs_le : forall x:real, y:real. infix_ls | x | y or (| x | = y) <->
+    (infix_ls (-y) x or ((-y) = x)) and (infix_ls x y or (x = y))
+  
+  axiom Abs_pos : forall x:real. infix_ls 0.0 | x | or (0.0 = | x |)
+  
+  (* use Abs *)
+  
+  logic sqr (x:real) : real = (x * x)
+  
+  logic sqrt real : real
+  
+  axiom Sqrt_positive : forall x:real. infix_ls 0.0 x or (0.0 = x) ->
+    infix_ls 0.0 (sqrt x) or (0.0 = sqrt x)
+  
+  axiom Sqrt_square : forall x:real. infix_ls 0.0 x or (0.0 = x) -> (sqr
+    (sqrt x) = x)
+  
+  axiom Square_sqrt : forall x:real. infix_ls 0.0 x or (0.0 = x) -> (sqrt
+    (x * x) = x)
+  
+  (* use Square *)
+  
+  logic cos real : real
+  
+  logic sin real : real
+  
+  axiom Pythagorean_identity : forall x:real. ((sqr (cos x) + sqr (sin
+    x)) = 1.0)
+  
+  axiom Cos_le_one : forall x:real. infix_ls | cos x | 1.0 or (| cos
+    x | = 1.0)
+  
+  axiom Sin_le_one : forall x:real. infix_ls | sin x | 1.0 or (| sin
+    x | = 1.0)
+  
+  axiom Cos_0 : (cos 0.0 = 1.0)
+  
+  axiom Sin_0 : (sin 0.0 = 0.0)
+  
+  logic pi : real
+  
+  axiom Pi_interval : infix_ls
+    3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196
+    pi and infix_ls pi
+    3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197
+  
+  axiom Cos_pi : (cos pi = (-1.0))
+  
+  axiom Sin_pi : (sin pi = 0.0)
+  
+  axiom Cos_pi2 : (cos (0.5 * pi) = 0.0)
+  
+  axiom Sin_pi2 : (sin (0.5 * pi) = 1.0)
+  
+  axiom Cos_plus_pi : forall x:real. (cos (x + pi) = (-cos x))
+  
+  axiom Sin_plus_pi : forall x:real. (sin (x + pi) = (-sin x))
+  
+  axiom Cos_plus_pi2 : forall x:real. (cos (x + (0.5 * pi)) = (-sin x))
+  
+  axiom Sin_plus_pi2 : forall x:real. (sin (x + (0.5 * pi)) = cos x)
+  
+  axiom Cos_neg : forall x:real. (cos (-x) = cos x)
+  
+  axiom Sin_neg : forall x:real. (sin (-x) = (-sin x))
+  
+  axiom Cos_sum : forall x:real, y:real. (cos (x + y) = ((cos x * cos
+    y) - (sin x * sin y)))
+  
+  axiom Sin_sum : forall x:real, y:real. (sin (x + y) = ((sin x * cos
+    y) + (cos x * sin y)))
+  
+  logic tan (x:real) : real = (sin x / cos x)
+  
+  logic atan real : real
+  
+  axiom Tan_atan : forall x:real. (tan (atan x) = x)
+  
+  (* use Trigonometry *)
+  
+  type mode =
+    | NearestTiesToEven
+    | ToZero
+    | Up
+    | Down
+    | NearTiesToAway
+  
+  (* use Rounding *)
+  
+  type single
+  
+  logic max_single : real = 0x1.FFFFFEp127
+  
+  logic max_int : int = 16777216
+  
+  logic infix_ls1 int int
+  
+  (* clone Assoc with type t = int, logic op = infix_pl6,
+    prop Assoc = Assoc15 *)
+  
+  (* clone Group with type t1 = int, logic inv = prefix_mn6,
+    logic op1 = infix_pl6, logic unit = zero6, prop Inv_def = Inv_def8,
+    prop Assoc2 = Assoc15, prop Unit_def = Unit_def8 *)
+  
+  (* clone Comm with type t2 = int, logic op2 = infix_pl6,
+    prop Comm = Comm13 *)
+  
+  (* meta AC logic infix_pl6 *)
+  
+  (* clone CommutativeGroup with type t3 = int, logic inv1 = prefix_mn6,
+    logic op3 = infix_pl6, logic unit1 = zero6, prop Comm2 = Comm13,
+    prop Inv_def2 = Inv_def8, prop Assoc3 = Assoc15,
+    prop Unit_def2 = Unit_def8 *)
+  
+  (* clone Assoc with type t = int, logic op = infix_as6,
+    prop Assoc = Assoc16 *)
+  
+  (* clone Ring with type t4 = int, logic infix_mn = infix_mn6,
+    logic infix_as1 = infix_as6, logic prefix_mn1 = prefix_mn6,
+    logic infix_pl1 = infix_pl6, logic zero1 = zero6,
+    prop Mul_distr = Mul_distr6, prop Assoc5 = Assoc16, prop Comm3 = Comm13,
+    prop Inv_def3 = Inv_def8, prop Assoc6 = Assoc15,
+    prop Unit_def3 = Unit_def8 *)
+  
+  (* clone Comm with type t2 = int, logic op2 = infix_as6,
+    prop Comm = Comm14 *)
+  
+  (* meta AC logic infix_as6 *)
+  
+  (* clone CommutativeRing with type t5 = int, logic infix_mn2 = infix_mn6,
+    logic infix_as2 = infix_as6, logic prefix_mn2 = prefix_mn6,
+    logic infix_pl2 = infix_pl6, logic zero2 = zero6, prop Comm5 = Comm14,
+    prop Mul_distr2 = Mul_distr6, prop Assoc7 = Assoc16, prop Comm6 = Comm13,
+    prop Inv_def4 = Inv_def8, prop Assoc8 = Assoc15,
+    prop Unit_def4 = Unit_def8 *)
+  
+  axiom NonTrivialRing4 : not (0 = 1)
+  
+  (* clone UnitaryCommutativeRing with type t6 = int, logic one = one4,
+    logic infix_mn3 = infix_mn6, logic infix_as3 = infix_as6,
+    logic prefix_mn3 = prefix_mn6, logic infix_pl3 = infix_pl6,
+    logic zero3 = zero6, prop NonTrivialRing1 = NonTrivialRing4,
+    prop Unitary = Unitary4, prop Comm7 = Comm14,
+    prop Mul_distr3 = Mul_distr6, prop Assoc9 = Assoc16, prop Comm8 = Comm13,
+    prop Inv_def5 = Inv_def8, prop Assoc10 = Assoc15,
+    prop Unit_def5 = Unit_def8 *)
+  
+  (* clone EndoRelation with type t8 = int, logic rel = infix_lseq2,  *)
+  
+  (* clone Reflexive with type t9 = int, logic rel1 = infix_lseq2,
+    prop Refl = Refl6 *)
+  
+  (* clone EndoRelation with type t8 = int, logic rel = infix_lseq2,  *)
+  
+  (* clone Transitive with type t10 = int, logic rel2 = infix_lseq2,
+    prop Trans = Trans6 *)
+  
+  (* clone PreOrder with type t11 = int, logic rel3 = infix_lseq2,
+    prop Trans2 = Trans6, prop Refl2 = Refl6 *)
+  
+  (* clone EndoRelation with type t8 = int, logic rel = infix_lseq2,  *)
+  
+  (* clone Antisymmetric with type t12 = int, logic rel4 = infix_lseq2,
+    prop Antisymm = Antisymm5 *)
+  
+  (* clone PartialOrder with type t13 = int, logic rel5 = infix_lseq2,
+    prop Antisymm2 = Antisymm5, prop Trans3 = Trans6, prop Refl3 = Refl6 *)
+  
+  (* clone EndoRelation with type t8 = int, logic rel = infix_lseq2,  *)
+  
+  (* clone Total with type t14 = int, logic rel6 = infix_lseq2,
+    prop Total = Total4 *)
+  
+  (* clone TotalOrder with type t15 = int, logic rel7 = infix_lseq2,
+    prop Total2 = Total4, prop Antisymm3 = Antisymm5, prop Trans4 = Trans6,
+    prop Refl4 = Refl6 *)
+  
+  axiom CompatOrderAdd2 : forall x:int, y:int, z:int. infix_ls1 x y or
+    (x = y) -> infix_ls1 (x + z) (y + z) or ((x + z) = (y + z))
+  
+  axiom CompatOrderMult2 : forall x:int, y:int, z:int. infix_ls1 x y or
+    (x = y) -> infix_ls1 0 z or (0 = z) -> infix_ls1 (x * z) (y * z) or
+    ((x * z) = (y * z))
+  
+  (* clone OrderedUnitaryCommutativeRing with type t17 = int,
+    logic infix_gteq2 = infix_gteq3, logic infix_lseq3 = infix_lseq2,
+    logic one5 = one4, logic infix_mn7 = infix_mn6,
+    logic infix_as7 = infix_as6, logic prefix_mn7 = prefix_mn6,
+    logic infix_pl7 = infix_pl6, logic zero7 = zero6,
+    prop CompatOrderMult3 = CompatOrderMult2,
+    prop CompatOrderAdd3 = CompatOrderAdd2, prop Total5 = Total4,
+    prop Antisymm6 = Antisymm5, prop Trans7 = Trans6, prop Refl7 = Refl6,
+    prop NonTrivialRing5 = NonTrivialRing4, prop Unitary5 = Unitary4,
+    prop Comm15 = Comm14, prop Mul_distr7 = Mul_distr6,
+    prop Assoc17 = Assoc16, prop Comm16 = Comm13, prop Inv_def9 = Inv_def8,
+    prop Assoc18 = Assoc15, prop Unit_def9 = Unit_def8 *)
+  
+  (* use Int *)
+  
+  logic from_int int : real
+  
+  axiom Zero : (from_int 0 = 0.0)
+  
+  axiom One : (from_int 1 = 1.0)
+  
+  axiom Add : forall x:int, y:int. (from_int (x + y) = (from_int x + from_int
+    y))
+  
+  axiom Sub : forall x:int, y:int. (from_int (x - y) = (from_int x - from_int
+    y))
+  
+  axiom Mul : forall x:int, y:int. (from_int (x * y) = (from_int x * from_int
+    y))
+  
+  axiom Neg : forall x:int, y:int. (from_int (-x) = (-from_int x))
+  
+  (* use FromInt *)
+  
+  logic round mode real : real
+  
+  logic round_logic mode real : single
+  
+  logic value single : real
+  
+  logic exact single : real
+  
+  logic model single : real
+  
+  logic round_error (x:single) : real = | (value x - exact x) |
+  
+  logic total_error (x:single) : real = | (value x - model x) |
+  
+  logic no_overflow (m:mode) (x:real) = infix_ls | round m x | max_single or
+    (| round m x | = max_single)
+  
+  axiom Bounded_real_no_overflow : forall m:mode, x:real. infix_ls | x |
+    max_single or (| x | = max_single) -> no_overflow m x
+  
+  axiom Round_monotonic : forall m:mode, x:real, y:real. infix_ls x y or
+    (x = y) -> infix_ls (round m x) (round m y) or (round m x = round m y)
+  
+  axiom Exact_rounding_for_integers : forall m:mode, i:int. (infix_ls1
+    (-max_int) i or ((-max_int) = i)) and (infix_ls1 i max_int or
+    (i = max_int)) -> (round m (from_int i) = from_int i)
+  
+  axiom Round_down_le : forall x:real. infix_ls (round Down x) x or (round
+    Down x = x)
+  
+  axiom Round_up_ge : forall x:real. infix_ls x (round Up x) or (x = round Up
+    x)
+  
+  axiom Round_down_neg : forall x:real. (round Down (-x) = (-round Up x))
+  
+  axiom Round_up_neg : forall x:real. (round Up (-x) = (-round Down x))
+  
+  (* clone GenFloat with type t18 = single,
+    logic max_representable_integer = max_int,
+    logic no_overflow1 = no_overflow, logic max = max_single,
+    logic total_error1 = total_error, logic round_error1 = round_error,
+    logic model1 = model, logic exact1 = exact, logic value1 = value,
+    logic round_logic1 = round_logic, logic round1 = round,
+    prop Round_up_neg1 = Round_up_neg, prop Round_down_neg1 = Round_down_neg,
+    prop Round_up_ge1 = Round_up_ge, prop Round_down_le1 = Round_down_le,
+    prop Exact_rounding_for_integers1 = Exact_rounding_for_integers,
+    prop Round_monotonic1 = Round_monotonic,
+    prop Bounded_real_no_overflow1 = Bounded_real_no_overflow *)
+  
+  (* use Single *)
+  
+  axiom MethodError : forall x:real. infix_ls | x | 0x1.p-5 or
+    (| x | = 0x1.p-5) -> infix_ls | ((1.0 - ((x * x) * 0.5)) - cos x) |
+    0x1.p-24 or (| ((1.0 - ((x * x) * 0.5)) - cos x) | = 0x1.p-24)
+  
+  logic round_single mode real : single
+  
+  axiom RoundSingle : forall m:mode, x:real. (value (round_single m
+    x) = round m x)
+  
+  logic cos_single (x:single) : single =
+    let x2 = round_single NearestTiesToEven (value x * value x) in
+    let x2o2 = round_single NearestTiesToEven (0.5 * value x2) in
+    round_single NearestTiesToEven (1.0 - value x2o2)
+  
+  (* meta syntax_type type int, "int" *)
+  
+  (* meta syntax_type type real, "real" *)
+  
+  (* meta syntax_logic logic infix_eq, "(%1 = %2)" *)
+  
+  (* meta syntax_logic logic zero6, "0" *)
+  
+  (* meta syntax_logic logic one4, "1" *)
+  
+  (* meta syntax_logic logic infix_pl6, "(%1 + %2)" *)
+  
+  (* meta syntax_logic logic infix_mn6, "(%1 - %2)" *)
+  
+  (* meta syntax_logic logic infix_as6, "(%1 * %2)" *)
+  
+  (* meta syntax_logic logic prefix_mn6, "(-%1)" *)
+  
+  (* meta inline : no logic infix_lseq2 *)
+  
+  (* meta inline : no logic infix_gteq3 *)
+  
+  (* meta inline : no logic infix_gt *)
+  
+  (* meta remove_prop prop Comm13 *)
+  
+  (* meta remove_prop prop Assoc15 *)
+  
+  (* meta remove_prop prop Unit_def8 *)
+  
+  (* meta remove_prop prop Inv_def8 *)
+  
+  (* meta remove_prop prop Assoc16 *)
+  
+  (* meta remove_prop prop Mul_distr6 *)
+  
+  (* meta remove_prop prop Comm14 *)
+  
+  (* meta remove_prop prop Unitary4 *)
+  
+  (* meta remove_prop prop Refl6 *)
+  
+  (* meta remove_prop prop Trans6 *)
+  
+  (* meta remove_prop prop Total4 *)
+  
+  (* meta remove_prop prop Antisymm5 *)
+  
+  (* meta syntax_logic logic zero, "0.0" *)
+  
+  (* meta syntax_logic logic one1, "1.0" *)
+  
+  (* meta syntax_logic logic infix_pl, "(%1 + %2)" *)
+  
+  (* meta syntax_logic logic infix_mn1, "(%1 - %2)" *)
+  
+  (* meta syntax_logic logic infix_as, "(%1 * %2)" *)
+  
+  (* meta syntax_logic logic infix_sl1, "(%1 / %2)" *)
+  
+  (* meta syntax_logic logic prefix_mn, "(-%1)" *)
+  
+  (* meta syntax_logic logic inv3, "(1.0 / %1)" *)
+  
+  (* meta inline : no logic infix_lseq *)
+  
+  (* meta inline : no logic infix_gteq1 *)
+  
+  (* meta inline : no logic infix_gt1 *)
+  
+  (* meta remove_prop prop Comm1 *)
+  
+  (* meta remove_prop prop Assoc1 *)
+  
+  (* meta remove_prop prop Unit_def1 *)
+  
+  (* meta remove_prop prop Inv_def1 *)
+  
+  (* meta remove_prop prop Assoc4 *)
+  
+  (* meta remove_prop prop Mul_distr1 *)
+  
+  (* meta remove_prop prop Comm4 *)
+  
+  (* meta remove_prop prop Unitary1 *)
+  
+  (* meta remove_prop prop Refl1 *)
+  
+  (* meta remove_prop prop Trans1 *)
+  
+  (* meta remove_prop prop Total1 *)
+  
+  (* meta remove_prop prop Antisymm1 *)
+  
+  (* meta remove_prop prop Inverse1 *)
+  
+  (* meta syntax_logic logic abs, "| %1 |" *)
+  
+  goal TotalError : forall x:single. infix_ls | value x | 0x1.p-5 or (| value
+    x | = 0x1.p-5) -> (let cos_x = cos_single x in infix_ls | (value
+    cos_x - cos (value x)) | 0x1.p-24 or (| (value cos_x - cos (value
+    x)) | = 0x1.p-24))
+  
+  
+end
diff --git a/T/my_cosine-CosineSingle-TotalError.why b/T/my_cosine-CosineSingle-TotalError.why
new file mode 100644
index 0000000000000000000000000000000000000000..55221cba1deec232444527dabafca8ac2e414e61
--- /dev/null
+++ b/T/my_cosine-CosineSingle-TotalError.why
@@ -0,0 +1,514 @@
+theory Task
+  (* use BuiltIn *)
+  
+  logic zero : real = 0.0
+  
+  logic one : real = 1.0
+  
+  logic infix_ls real real
+  
+  logic infix_gt (x:real) (y:real) = infix_ls y x
+  
+  logic infix_lseq (x:real) (y:real) = infix_ls x y or (x = y)
+  
+  logic infix_pl real real : real
+  
+  logic prefix_mn real : real
+  
+  logic infix_as real real : real
+  
+  axiom Unit_def : forall x:real. (infix_pl x zero = x)
+  
+  axiom Assoc : forall x:real, y:real, z:real. (infix_pl (infix_pl x y)
+    z = infix_pl x (infix_pl y z))
+  
+  (* clone Assoc with type t = real, logic op = infix_pl,
+    prop Assoc1 = Assoc *)
+  
+  axiom Inv_def : forall x:real. (infix_pl x (prefix_mn x) = zero)
+  
+  (* clone Group with type t1 = real, logic inv = prefix_mn,
+    logic op1 = infix_pl, logic unit = zero, prop Inv_def1 = Inv_def,
+    prop Assoc2 = Assoc, prop Unit_def1 = Unit_def *)
+  
+  axiom Comm : forall x:real, y:real. (infix_pl x y = infix_pl y x)
+  
+  (* clone Comm with type t2 = real, logic op2 = infix_pl,
+    prop Comm1 = Comm *)
+  
+  (* meta AC logic infix_pl *)
+  
+  (* clone CommutativeGroup with type t3 = real, logic inv1 = prefix_mn,
+    logic op3 = infix_pl, logic unit1 = zero, prop Comm2 = Comm,
+    prop Inv_def2 = Inv_def, prop Assoc3 = Assoc,
+    prop Unit_def2 = Unit_def *)
+  
+  axiom Assoc4 : forall x:real, y:real, z:real. (infix_as (infix_as x y)
+    z = infix_as x (infix_as y z))
+  
+  (* clone Assoc with type t = real, logic op = infix_as,
+    prop Assoc1 = Assoc4 *)
+  
+  axiom Mul_distr : forall x:real, y:real, z:real. (infix_as x (infix_pl y
+    z) = infix_pl (infix_as x y) (infix_as x z))
+  
+  logic infix_mn (x:real) (y:real) : real = infix_pl x (prefix_mn y)
+  
+  (* clone Ring with type t4 = real, logic infix_mn1 = infix_mn,
+    logic infix_as1 = infix_as, logic prefix_mn1 = prefix_mn,
+    logic infix_pl1 = infix_pl, logic zero1 = zero,
+    prop Mul_distr1 = Mul_distr, prop Assoc5 = Assoc4, prop Comm3 = Comm,
+    prop Inv_def3 = Inv_def, prop Assoc6 = Assoc,
+    prop Unit_def3 = Unit_def *)
+  
+  axiom Comm4 : forall x:real, y:real. (infix_as x y = infix_as y x)
+  
+  (* clone Comm with type t2 = real, logic op2 = infix_as,
+    prop Comm1 = Comm4 *)
+  
+  (* meta AC logic infix_as *)
+  
+  (* clone CommutativeRing with type t5 = real, logic infix_mn2 = infix_mn,
+    logic infix_as2 = infix_as, logic prefix_mn2 = prefix_mn,
+    logic infix_pl2 = infix_pl, logic zero2 = zero, prop Comm5 = Comm4,
+    prop Mul_distr2 = Mul_distr, prop Assoc7 = Assoc4, prop Comm6 = Comm,
+    prop Inv_def4 = Inv_def, prop Assoc8 = Assoc,
+    prop Unit_def4 = Unit_def *)
+  
+  axiom Unitary : forall x:real. (infix_as one x = x)
+  
+  axiom NonTrivialRing : not (zero = one)
+  
+  (* clone UnitaryCommutativeRing with type t6 = real, logic one1 = one,
+    logic infix_mn3 = infix_mn, logic infix_as3 = infix_as,
+    logic prefix_mn3 = prefix_mn, logic infix_pl3 = infix_pl,
+    logic zero3 = zero, prop NonTrivialRing1 = NonTrivialRing,
+    prop Unitary1 = Unitary, prop Comm7 = Comm4, prop Mul_distr3 = Mul_distr,
+    prop Assoc9 = Assoc4, prop Comm8 = Comm, prop Inv_def5 = Inv_def,
+    prop Assoc10 = Assoc, prop Unit_def5 = Unit_def *)
+  
+  logic inv2 real : real
+  
+  axiom Inverse : forall x:real. not (x = zero) -> (infix_as x (inv2
+    x) = one)
+  
+  logic infix_sl (x:real) (y:real) : real = infix_as x (inv2 y)
+  
+  (* clone Field with type t7 = real, logic infix_sl1 = infix_sl,
+    logic inv3 = inv2, logic one2 = one, logic infix_mn4 = infix_mn,
+    logic infix_as4 = infix_as, logic prefix_mn4 = prefix_mn,
+    logic infix_pl4 = infix_pl, logic zero4 = zero, prop Inverse1 = Inverse,
+    prop NonTrivialRing2 = NonTrivialRing, prop Unitary2 = Unitary,
+    prop Comm9 = Comm4, prop Mul_distr4 = Mul_distr, prop Assoc11 = Assoc4,
+    prop Comm10 = Comm, prop Inv_def6 = Inv_def, prop Assoc12 = Assoc,
+    prop Unit_def6 = Unit_def *)
+  
+  logic infix_gteq (x:real) (y:real) = infix_lseq y x
+  
+  (* clone EndoRelation with type t8 = real, logic rel = infix_lseq,  *)
+  
+  axiom Refl : forall x:real. infix_lseq x x
+  
+  (* clone Reflexive with type t9 = real, logic rel1 = infix_lseq,
+    prop Refl1 = Refl *)
+  
+  (* clone EndoRelation with type t8 = real, logic rel = infix_lseq,  *)
+  
+  axiom Trans : forall x:real, y:real, z:real. infix_lseq x y -> infix_lseq y
+    z -> infix_lseq x z
+  
+  (* clone Transitive with type t10 = real, logic rel2 = infix_lseq,
+    prop Trans1 = Trans *)
+  
+  (* clone PreOrder with type t11 = real, logic rel3 = infix_lseq,
+    prop Trans2 = Trans, prop Refl2 = Refl *)
+  
+  (* clone EndoRelation with type t8 = real, logic rel = infix_lseq,  *)
+  
+  axiom Antisymm : forall x:real, y:real. infix_lseq x y -> infix_lseq y x ->
+    (x = y)
+  
+  (* clone Antisymmetric with type t12 = real, logic rel4 = infix_lseq,
+    prop Antisymm1 = Antisymm *)
+  
+  (* clone PartialOrder with type t13 = real, logic rel5 = infix_lseq,
+    prop Antisymm2 = Antisymm, prop Trans3 = Trans, prop Refl3 = Refl *)
+  
+  (* clone EndoRelation with type t8 = real, logic rel = infix_lseq,  *)
+  
+  axiom Total : forall x:real, y:real. infix_lseq x y or infix_lseq y x
+  
+  (* clone Total with type t14 = real, logic rel6 = infix_lseq,
+    prop Total1 = Total *)
+  
+  (* clone TotalOrder with type t15 = real, logic rel7 = infix_lseq,
+    prop Total2 = Total, prop Antisymm3 = Antisymm, prop Trans4 = Trans,
+    prop Refl4 = Refl *)
+  
+  axiom CompatOrderAdd : forall x:real, y:real, z:real. infix_lseq x y ->
+    infix_lseq (infix_pl x z) (infix_pl y z)
+  
+  axiom CompatOrderMult : forall x:real, y:real, z:real. infix_lseq x y ->
+    infix_lseq zero z -> infix_lseq (infix_as x z) (infix_as y z)
+  
+  (* clone OrderedField with type t16 = real, logic infix_gteq1 = infix_gteq,
+    logic infix_lseq1 = infix_lseq, logic infix_sl2 = infix_sl,
+    logic inv4 = inv2, logic one3 = one, logic infix_mn5 = infix_mn,
+    logic infix_as5 = infix_as, logic prefix_mn5 = prefix_mn,
+    logic infix_pl5 = infix_pl, logic zero5 = zero,
+    prop CompatOrderMult1 = CompatOrderMult,
+    prop CompatOrderAdd1 = CompatOrderAdd, prop Total3 = Total,
+    prop Antisymm4 = Antisymm, prop Trans5 = Trans, prop Refl5 = Refl,
+    prop Inverse2 = Inverse, prop NonTrivialRing3 = NonTrivialRing,
+    prop Unitary3 = Unitary, prop Comm11 = Comm4,
+    prop Mul_distr5 = Mul_distr, prop Assoc13 = Assoc4, prop Comm12 = Comm,
+    prop Inv_def7 = Inv_def, prop Assoc14 = Assoc,
+    prop Unit_def7 = Unit_def *)
+  
+  (* use Real *)
+  
+  logic abs (x:real) : real = if infix_gteq x 0.0 then x else prefix_mn x
+  
+  axiom Abs_le : forall x:real, y:real. infix_lseq (abs x) y <-> infix_lseq
+    (prefix_mn y) x and infix_lseq x y
+  
+  axiom Abs_pos : forall x:real. infix_gteq (abs x) 0.0
+  
+  (* use Abs *)
+  
+  logic sqr (x:real) : real = infix_as x x
+  
+  logic sqrt real : real
+  
+  axiom Sqrt_positive : forall x:real. infix_gteq x 0.0 -> infix_gteq (sqrt
+    x) 0.0
+  
+  axiom Sqrt_square : forall x:real. infix_gteq x 0.0 -> (sqr (sqrt x) = x)
+  
+  axiom Square_sqrt : forall x:real. infix_gteq x 0.0 -> (sqrt (infix_as x
+    x) = x)
+  
+  (* use Square *)
+  
+  logic cos real : real
+  
+  logic sin real : real
+  
+  axiom Pythagorean_identity : forall x:real. (infix_pl (sqr (cos x)) (sqr
+    (sin x)) = 1.0)
+  
+  axiom Cos_le_one : forall x:real. infix_lseq (abs (cos x)) 1.0
+  
+  axiom Sin_le_one : forall x:real. infix_lseq (abs (sin x)) 1.0
+  
+  axiom Cos_0 : (cos 0.0 = 1.0)
+  
+  axiom Sin_0 : (sin 0.0 = 0.0)
+  
+  logic pi : real
+  
+  axiom Pi_interval : infix_ls
+    3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196
+    pi and infix_ls pi
+    3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197
+  
+  axiom Cos_pi : (cos pi = prefix_mn 1.0)
+  
+  axiom Sin_pi : (sin pi = 0.0)
+  
+  axiom Cos_pi2 : (cos (infix_as 0.5 pi) = 0.0)
+  
+  axiom Sin_pi2 : (sin (infix_as 0.5 pi) = 1.0)
+  
+  axiom Cos_plus_pi : forall x:real. (cos (infix_pl x pi) = prefix_mn (cos
+    x))
+  
+  axiom Sin_plus_pi : forall x:real. (sin (infix_pl x pi) = prefix_mn (sin
+    x))
+  
+  axiom Cos_plus_pi2 : forall x:real. (cos (infix_pl x (infix_as 0.5
+    pi)) = prefix_mn (sin x))
+  
+  axiom Sin_plus_pi2 : forall x:real. (sin (infix_pl x (infix_as 0.5
+    pi)) = cos x)
+  
+  axiom Cos_neg : forall x:real. (cos (prefix_mn x) = cos x)
+  
+  axiom Sin_neg : forall x:real. (sin (prefix_mn x) = prefix_mn (sin x))
+  
+  axiom Cos_sum : forall x:real, y:real. (cos (infix_pl x y) = infix_mn
+    (infix_as (cos x) (cos y)) (infix_as (sin x) (sin y)))
+  
+  axiom Sin_sum : forall x:real, y:real. (sin (infix_pl x y) = infix_pl
+    (infix_as (sin x) (cos y)) (infix_as (cos x) (sin y)))
+  
+  logic tan (x:real) : real = infix_sl (sin x) (cos x)
+  
+  logic atan real : real
+  
+  axiom Tan_atan : forall x:real. (tan (atan x) = x)
+  
+  (* use Trigonometry *)
+  
+  type mode =
+    | NearestTiesToEven
+    | ToZero
+    | Up
+    | Down
+    | NearTiesToAway
+  
+  (* use Rounding *)
+  
+  type single
+  
+  logic max_single : real = 0x1.FFFFFEp127
+  
+  logic max_int : int = 16777216
+  
+  logic zero6 : int = 0
+  
+  logic one4 : int = 1
+  
+  logic infix_ls1 int int
+  
+  logic infix_gt1 (x:int) (y:int) = infix_ls1 y x
+  
+  logic infix_lseq2 (x:int) (y:int) = infix_ls1 x y or (x = y)
+  
+  logic infix_pl6 int int : int
+  
+  logic prefix_mn6 int : int
+  
+  logic infix_as6 int int : int
+  
+  axiom Unit_def8 : forall x:int. (infix_pl6 x zero6 = x)
+  
+  axiom Assoc15 : forall x:int, y:int, z:int. (infix_pl6 (infix_pl6 x y)
+    z = infix_pl6 x (infix_pl6 y z))
+  
+  (* clone Assoc with type t = int, logic op = infix_pl6,
+    prop Assoc1 = Assoc15 *)
+  
+  axiom Inv_def8 : forall x:int. (infix_pl6 x (prefix_mn6 x) = zero6)
+  
+  (* clone Group with type t1 = int, logic inv = prefix_mn6,
+    logic op1 = infix_pl6, logic unit = zero6, prop Inv_def1 = Inv_def8,
+    prop Assoc2 = Assoc15, prop Unit_def1 = Unit_def8 *)
+  
+  axiom Comm13 : forall x:int, y:int. (infix_pl6 x y = infix_pl6 y x)
+  
+  (* clone Comm with type t2 = int, logic op2 = infix_pl6,
+    prop Comm1 = Comm13 *)
+  
+  (* meta AC logic infix_pl6 *)
+  
+  (* clone CommutativeGroup with type t3 = int, logic inv1 = prefix_mn6,
+    logic op3 = infix_pl6, logic unit1 = zero6, prop Comm2 = Comm13,
+    prop Inv_def2 = Inv_def8, prop Assoc3 = Assoc15,
+    prop Unit_def2 = Unit_def8 *)
+  
+  axiom Assoc16 : forall x:int, y:int, z:int. (infix_as6 (infix_as6 x y)
+    z = infix_as6 x (infix_as6 y z))
+  
+  (* clone Assoc with type t = int, logic op = infix_as6,
+    prop Assoc1 = Assoc16 *)
+  
+  axiom Mul_distr6 : forall x:int, y:int, z:int. (infix_as6 x (infix_pl6 y
+    z) = infix_pl6 (infix_as6 x y) (infix_as6 x z))
+  
+  logic infix_mn6 (x:int) (y:int) : int = infix_pl6 x (prefix_mn6 y)
+  
+  (* clone Ring with type t4 = int, logic infix_mn1 = infix_mn6,
+    logic infix_as1 = infix_as6, logic prefix_mn1 = prefix_mn6,
+    logic infix_pl1 = infix_pl6, logic zero1 = zero6,
+    prop Mul_distr1 = Mul_distr6, prop Assoc5 = Assoc16, prop Comm3 = Comm13,
+    prop Inv_def3 = Inv_def8, prop Assoc6 = Assoc15,
+    prop Unit_def3 = Unit_def8 *)
+  
+  axiom Comm14 : forall x:int, y:int. (infix_as6 x y = infix_as6 y x)
+  
+  (* clone Comm with type t2 = int, logic op2 = infix_as6,
+    prop Comm1 = Comm14 *)
+  
+  (* meta AC logic infix_as6 *)
+  
+  (* clone CommutativeRing with type t5 = int, logic infix_mn2 = infix_mn6,
+    logic infix_as2 = infix_as6, logic prefix_mn2 = prefix_mn6,
+    logic infix_pl2 = infix_pl6, logic zero2 = zero6, prop Comm5 = Comm14,
+    prop Mul_distr2 = Mul_distr6, prop Assoc7 = Assoc16, prop Comm6 = Comm13,
+    prop Inv_def4 = Inv_def8, prop Assoc8 = Assoc15,
+    prop Unit_def4 = Unit_def8 *)
+  
+  axiom Unitary4 : forall x:int. (infix_as6 one4 x = x)
+  
+  axiom NonTrivialRing4 : not (zero6 = one4)
+  
+  (* clone UnitaryCommutativeRing with type t6 = int, logic one1 = one4,
+    logic infix_mn3 = infix_mn6, logic infix_as3 = infix_as6,
+    logic prefix_mn3 = prefix_mn6, logic infix_pl3 = infix_pl6,
+    logic zero3 = zero6, prop NonTrivialRing1 = NonTrivialRing4,
+    prop Unitary1 = Unitary4, prop Comm7 = Comm14,
+    prop Mul_distr3 = Mul_distr6, prop Assoc9 = Assoc16, prop Comm8 = Comm13,
+    prop Inv_def5 = Inv_def8, prop Assoc10 = Assoc15,
+    prop Unit_def5 = Unit_def8 *)
+  
+  logic infix_gteq2 (x:int) (y:int) = infix_lseq2 y x
+  
+  (* clone EndoRelation with type t8 = int, logic rel = infix_lseq2,  *)
+  
+  axiom Refl6 : forall x:int. infix_lseq2 x x
+  
+  (* clone Reflexive with type t9 = int, logic rel1 = infix_lseq2,
+    prop Refl1 = Refl6 *)
+  
+  (* clone EndoRelation with type t8 = int, logic rel = infix_lseq2,  *)
+  
+  axiom Trans6 : forall x:int, y:int, z:int. infix_lseq2 x y -> infix_lseq2 y
+    z -> infix_lseq2 x z
+  
+  (* clone Transitive with type t10 = int, logic rel2 = infix_lseq2,
+    prop Trans1 = Trans6 *)
+  
+  (* clone PreOrder with type t11 = int, logic rel3 = infix_lseq2,
+    prop Trans2 = Trans6, prop Refl2 = Refl6 *)
+  
+  (* clone EndoRelation with type t8 = int, logic rel = infix_lseq2,  *)
+  
+  axiom Antisymm5 : forall x:int, y:int. infix_lseq2 x y -> infix_lseq2 y
+    x -> (x = y)
+  
+  (* clone Antisymmetric with type t12 = int, logic rel4 = infix_lseq2,
+    prop Antisymm1 = Antisymm5 *)
+  
+  (* clone PartialOrder with type t13 = int, logic rel5 = infix_lseq2,
+    prop Antisymm2 = Antisymm5, prop Trans3 = Trans6, prop Refl3 = Refl6 *)
+  
+  (* clone EndoRelation with type t8 = int, logic rel = infix_lseq2,  *)
+  
+  axiom Total4 : forall x:int, y:int. infix_lseq2 x y or infix_lseq2 y x
+  
+  (* clone Total with type t14 = int, logic rel6 = infix_lseq2,
+    prop Total1 = Total4 *)
+  
+  (* clone TotalOrder with type t15 = int, logic rel7 = infix_lseq2,
+    prop Total2 = Total4, prop Antisymm3 = Antisymm5, prop Trans4 = Trans6,
+    prop Refl4 = Refl6 *)
+  
+  axiom CompatOrderAdd2 : forall x:int, y:int, z:int. infix_lseq2 x y ->
+    infix_lseq2 (infix_pl6 x z) (infix_pl6 y z)
+  
+  axiom CompatOrderMult2 : forall x:int, y:int, z:int. infix_lseq2 x y ->
+    infix_lseq2 zero6 z -> infix_lseq2 (infix_as6 x z) (infix_as6 y z)
+  
+  (* clone OrderedUnitaryCommutativeRing with type t17 = int,
+    logic infix_gteq3 = infix_gteq2, logic infix_lseq3 = infix_lseq2,
+    logic one5 = one4, logic infix_mn7 = infix_mn6,
+    logic infix_as7 = infix_as6, logic prefix_mn7 = prefix_mn6,
+    logic infix_pl7 = infix_pl6, logic zero7 = zero6,
+    prop CompatOrderMult3 = CompatOrderMult2,
+    prop CompatOrderAdd3 = CompatOrderAdd2, prop Total5 = Total4,
+    prop Antisymm6 = Antisymm5, prop Trans7 = Trans6, prop Refl7 = Refl6,
+    prop NonTrivialRing5 = NonTrivialRing4, prop Unitary5 = Unitary4,
+    prop Comm15 = Comm14, prop Mul_distr7 = Mul_distr6,
+    prop Assoc17 = Assoc16, prop Comm16 = Comm13, prop Inv_def9 = Inv_def8,
+    prop Assoc18 = Assoc15, prop Unit_def9 = Unit_def8 *)
+  
+  (* use Int *)
+  
+  logic from_int int : real
+  
+  axiom Zero : (from_int 0 = 0.0)
+  
+  axiom One : (from_int 1 = 1.0)
+  
+  axiom Add : forall x:int, y:int. (from_int (infix_pl6 x y) = infix_pl
+    (from_int x) (from_int y))
+  
+  axiom Sub : forall x:int, y:int. (from_int (infix_mn6 x y) = infix_mn
+    (from_int x) (from_int y))
+  
+  axiom Mul : forall x:int, y:int. (from_int (infix_as6 x y) = infix_as
+    (from_int x) (from_int y))
+  
+  axiom Neg : forall x:int, y:int. (from_int (prefix_mn6 x) = prefix_mn
+    (from_int x))
+  
+  (* use FromInt *)
+  
+  logic round mode real : real
+  
+  logic round_logic mode real : single
+  
+  logic value single : real
+  
+  logic exact single : real
+  
+  logic model single : real
+  
+  logic round_error (x:single) : real = abs (infix_mn (value x) (exact x))
+  
+  logic total_error (x:single) : real = abs (infix_mn (value x) (model x))
+  
+  logic no_overflow (m:mode) (x:real) = infix_lseq (abs (round m x))
+    max_single
+  
+  axiom Bounded_real_no_overflow : forall m:mode, x:real. infix_lseq (abs x)
+    max_single -> no_overflow m x
+  
+  axiom Round_monotonic : forall m:mode, x:real, y:real. infix_lseq x y ->
+    infix_lseq (round m x) (round m y)
+  
+  axiom Exact_rounding_for_integers : forall m:mode, i:int. infix_lseq2
+    (prefix_mn6 max_int) i and infix_lseq2 i max_int -> (round m (from_int
+    i) = from_int i)
+  
+  axiom Round_down_le : forall x:real. infix_lseq (round Down x) x
+  
+  axiom Round_up_ge : forall x:real. infix_gteq (round Up x) x
+  
+  axiom Round_down_neg : forall x:real. (round Down (prefix_mn x) = prefix_mn
+    (round Up x))
+  
+  axiom Round_up_neg : forall x:real. (round Up (prefix_mn x) = prefix_mn
+    (round Down x))
+  
+  (* clone GenFloat with type t18 = single,
+    logic max_representable_integer = max_int,
+    logic no_overflow1 = no_overflow, logic max = max_single,
+    logic total_error1 = total_error, logic round_error1 = round_error,
+    logic model1 = model, logic exact1 = exact, logic value1 = value,
+    logic round_logic1 = round_logic, logic round1 = round,
+    prop Round_up_neg1 = Round_up_neg, prop Round_down_neg1 = Round_down_neg,
+    prop Round_up_ge1 = Round_up_ge, prop Round_down_le1 = Round_down_le,
+    prop Exact_rounding_for_integers1 = Exact_rounding_for_integers,
+    prop Round_monotonic1 = Round_monotonic,
+    prop Bounded_real_no_overflow1 = Bounded_real_no_overflow *)
+  
+  (* use Single *)
+  
+  axiom MethodError : forall x:real. infix_lseq (abs x) 0x1.p-5 -> infix_lseq
+    (abs (infix_mn (infix_mn 1.0 (infix_as (infix_as x x) 0.5)) (cos x)))
+    0x1.p-24
+  
+  logic round_single mode real : single
+  
+  axiom RoundSingle : forall m:mode, x:real. (value (round_single m
+    x) = round m x)
+  
+  logic cos_single (x:single) : single =
+    let x2 = round_single NearestTiesToEven (infix_as (value x) (value x)) in
+    let x2o2 = round_single NearestTiesToEven (infix_as 0.5 (value x2)) in
+    round_single NearestTiesToEven (infix_mn 1.0 (value x2o2))
+  
+  (* meta syntax_type type int, "int" *)
+  
+  (* meta syntax_type type real, "real" *)
+  
+  (* meta syntax_logic logic infix_eq, "(%1 = %2)" *)
+  
+  goal TotalError : forall x:single. infix_lseq (abs (value x)) 0x1.p-5 ->
+    (let cos_x = cos_single x in infix_lseq (abs (infix_mn (value cos_x) (cos
+    (value x)))) 0x1.p-24)
+  
+  
+end
diff --git a/T/project.db b/T/project.db
new file mode 100644
index 0000000000000000000000000000000000000000..9ae97c8c67d87d8111a88d3432ce66ca0210ca8b
Binary files /dev/null and b/T/project.db differ
diff --git a/doc/starting.log b/doc/starting.log
new file mode 100644
index 0000000000000000000000000000000000000000..9b2ca3ccacbaa0161a7d22bf39be762844c11158
--- /dev/null
+++ b/doc/starting.log
@@ -0,0 +1,341 @@
+This is pdfTeX, Version 3.1415926-1.40.10 (TeX Live 2009/Debian) (format=pdflatex 2010.8.27)  14 DEC 2010 16:08
+entering extended mode
+ restricted \write18 enabled.
+ %&-line parsing enabled.
+**\input starting.tex
+(./starting.tex
+! Undefined control sequence.
+l.1 \chapter
+            {Getting Started}
+The control sequence at the end of the top line
+of your error message was never \def'ed. If you have
+misspelled it (e.g., `\hobx'), type `I' and the correct
+spelling (e.g., `I\hbox'). Otherwise just continue,
+and I'll forget about whatever was undefined.
+
+
+! LaTeX Error: Missing \begin{document}.
+
+See the LaTeX manual or LaTeX Companion for explanation.
+Type  H <return>  for immediate help.
+ ...                                              
+                                                  
+l.1 \chapter{G
+              etting Started}
+You're in trouble here.  Try typing  <return>  to proceed.
+If that doesn't work, type  X <return>  to quit.
+
+Missing character: There is no G in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no t in font nullfont!
+Missing character: There is no t in font nullfont!
+Missing character: There is no i in font nullfont!
+Missing character: There is no n in font nullfont!
+Missing character: There is no g in font nullfont!
+Missing character: There is no S in font nullfont!
+Missing character: There is no t in font nullfont!
+Missing character: There is no a in font nullfont!
+Missing character: There is no r in font nullfont!
+Missing character: There is no t in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no d in font nullfont!
+
+Overfull \hbox (20.0pt too wide) in paragraph at lines 1--3
+[]
+ []
+
+! Undefined control sequence.
+l.4 \section
+            {Hello Proof}
+The control sequence at the end of the top line
+of your error message was never \def'ed. If you have
+misspelled it (e.g., `\hobx'), type `I' and the correct
+spelling (e.g., `I\hbox'). Otherwise just continue,
+and I'll forget about whatever was undefined.
+
+
+! LaTeX Error: Missing \begin{document}.
+
+See the LaTeX manual or LaTeX Companion for explanation.
+Type  H <return>  for immediate help.
+ ...                                              
+                                                  
+l.4 \section{H
+              ello Proof}
+You're in trouble here.  Try typing  <return>  to proceed.
+If that doesn't work, type  X <return>  to quit.
+
+Missing character: There is no H in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no l in font nullfont!
+Missing character: There is no l in font nullfont!
+Missing character: There is no o in font nullfont!
+Missing character: There is no P in font nullfont!
+Missing character: There is no r in font nullfont!
+Missing character: There is no o in font nullfont!
+Missing character: There is no o in font nullfont!
+Missing character: There is no f in font nullfont!
+
+Overfull \hbox (20.0pt too wide) in paragraph at lines 4--5
+[]
+ []
+
+
+! LaTeX Error: Missing \begin{document}.
+
+See the LaTeX manual or LaTeX Companion for explanation.
+Type  H <return>  for immediate help.
+ ...                                              
+                                                  
+l.6 T
+     he graphical interface allows to browse into a file or a set of
+You're in trouble here.  Try typing  <return>  to proceed.
+If that doesn't work, type  X <return>  to quit.
+
+Missing character: There is no T in font nullfont!
+Missing character: There is no h in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no g in font nullfont!
+Missing character: There is no r in font nullfont!
+Missing character: There is no a in font nullfont!
+Missing character: There is no p in font nullfont!
+Missing character: There is no h in font nullfont!
+Missing character: There is no i in font nullfont!
+Missing character: There is no c in font nullfont!
+Missing character: There is no a in font nullfont!
+Missing character: There is no l in font nullfont!
+Missing character: There is no i in font nullfont!
+Missing character: There is no n in font nullfont!
+Missing character: There is no t in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no r in font nullfont!
+Missing character: There is no f in font nullfont!
+Missing character: There is no a in font nullfont!
+Missing character: There is no c in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no a in font nullfont!
+Missing character: There is no l in font nullfont!
+Missing character: There is no l in font nullfont!
+Missing character: There is no o in font nullfont!
+Missing character: There is no w in font nullfont!
+Missing character: There is no s in font nullfont!
+Missing character: There is no t in font nullfont!
+Missing character: There is no o in font nullfont!
+Missing character: There is no b in font nullfont!
+Missing character: There is no r in font nullfont!
+Missing character: There is no o in font nullfont!
+Missing character: There is no w in font nullfont!
+Missing character: There is no s in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no i in font nullfont!
+Missing character: There is no n in font nullfont!
+Missing character: There is no t in font nullfont!
+Missing character: There is no o in font nullfont!
+Missing character: There is no a in font nullfont!
+Missing character: There is no f in font nullfont!
+Missing character: There is no i in font nullfont!
+Missing character: There is no l in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no o in font nullfont!
+Missing character: There is no r in font nullfont!
+Missing character: There is no a in font nullfont!
+Missing character: There is no s in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no t in font nullfont!
+Missing character: There is no o in font nullfont!
+Missing character: There is no f in font nullfont!
+Missing character: There is no f in font nullfont!
+Missing character: There is no i in font nullfont!
+Missing character: There is no l in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no s in font nullfont!
+Missing character: There is no , in font nullfont!
+Missing character: There is no a in font nullfont!
+Missing character: There is no n in font nullfont!
+Missing character: There is no d in font nullfont!
+Missing character: There is no c in font nullfont!
+Missing character: There is no h in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no c in font nullfont!
+Missing character: There is no k in font nullfont!
+Missing character: There is no t in font nullfont!
+Missing character: There is no h in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no v in font nullfont!
+Missing character: There is no a in font nullfont!
+Missing character: There is no l in font nullfont!
+Missing character: There is no i in font nullfont!
+Missing character: There is no d in font nullfont!
+Missing character: There is no i in font nullfont!
+Missing character: There is no t in font nullfont!
+Missing character: There is no y in font nullfont!
+Missing character: There is no o in font nullfont!
+Missing character: There is no f in font nullfont!
+Missing character: There is no g in font nullfont!
+Missing character: There is no o in font nullfont!
+Missing character: There is no a in font nullfont!
+Missing character: There is no l in font nullfont!
+Missing character: There is no s in font nullfont!
+Missing character: There is no w in font nullfont!
+Missing character: There is no i in font nullfont!
+Missing character: There is no t in font nullfont!
+Missing character: There is no h in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no x in font nullfont!
+Missing character: There is no t in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no r in font nullfont!
+Missing character: There is no n in font nullfont!
+Missing character: There is no a in font nullfont!
+Missing character: There is no l in font nullfont!
+Missing character: There is no p in font nullfont!
+Missing character: There is no r in font nullfont!
+Missing character: There is no o in font nullfont!
+Missing character: There is no v in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no r in font nullfont!
+Missing character: There is no s in font nullfont!
+Missing character: There is no , in font nullfont!
+Missing character: There is no i in font nullfont!
+Missing character: There is no n in font nullfont!
+Missing character: There is no a in font nullfont!
+Missing character: There is no f in font nullfont!
+Missing character: There is no r in font nullfont!
+Missing character: There is no i in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no n in font nullfont!
+Missing character: There is no d in font nullfont!
+Missing character: There is no l in font nullfont!
+Missing character: There is no y in font nullfont!
+Missing character: There is no w in font nullfont!
+Missing character: There is no a in font nullfont!
+Missing character: There is no y in font nullfont!
+Missing character: There is no . in font nullfont!
+Missing character: There is no T in font nullfont!
+Missing character: There is no h in font nullfont!
+Missing character: There is no i in font nullfont!
+Missing character: There is no s in font nullfont!
+Missing character: There is no s in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no c in font nullfont!
+Missing character: There is no t in font nullfont!
+Missing character: There is no i in font nullfont!
+Missing character: There is no o in font nullfont!
+Missing character: There is no n in font nullfont!
+Missing character: There is no p in font nullfont!
+Missing character: There is no r in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no s in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no n in font nullfont!
+Missing character: There is no t in font nullfont!
+Missing character: There is no s in font nullfont!
+Missing character: There is no t in font nullfont!
+Missing character: There is no h in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no b in font nullfont!
+Missing character: There is no a in font nullfont!
+Missing character: There is no s in font nullfont!
+Missing character: There is no i in font nullfont!
+Missing character: There is no c in font nullfont!
+Missing character: There is no u in font nullfont!
+Missing character: There is no s in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no o in font nullfont!
+Missing character: There is no f in font nullfont!
+Missing character: There is no t in font nullfont!
+Missing character: There is no h in font nullfont!
+Missing character: There is no i in font nullfont!
+Missing character: There is no s in font nullfont!
+Missing character: There is no G in font nullfont!
+Missing character: There is no U in font nullfont!
+Missing character: There is no I in font nullfont!
+Missing character: There is no . in font nullfont!
+Missing character: There is no P in font nullfont!
+Missing character: There is no l in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no a in font nullfont!
+Missing character: There is no s in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no r in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no f in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no r in font nullfont!
+Missing character: There is no t in font nullfont!
+Missing character: There is no o in font nullfont!
+Missing character: There is no S in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no c in font nullfont!
+Missing character: There is no t in font nullfont!
+Missing character: There is no i in font nullfont!
+Missing character: There is no o in font nullfont!
+Missing character: There is no n in font nullfont!
+! Undefined control sequence.
+<write> ...eference `sec:ideref' on page \thepage 
+                                                  \space undefined\on@line .
+l.9 refer to Section~\ref{sec:ideref}
+                                      for a more complete description.
+The control sequence at the end of the top line
+of your error message was never \def'ed. If you have
+misspelled it (e.g., `\hobx'), type `I' and the correct
+spelling (e.g., `I\hbox'). Otherwise just continue,
+and I'll forget about whatever was undefined.
+
+
+LaTeX Warning: Reference `sec:ideref' on page  undefined on input line 9.
+
+Missing character: There is no f in font nullfont!
+Missing character: There is no o in font nullfont!
+Missing character: There is no r in font nullfont!
+Missing character: There is no a in font nullfont!
+Missing character: There is no m in font nullfont!
+Missing character: There is no o in font nullfont!
+Missing character: There is no r in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no c in font nullfont!
+Missing character: There is no o in font nullfont!
+Missing character: There is no m in font nullfont!
+Missing character: There is no p in font nullfont!
+Missing character: There is no l in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no t in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no d in font nullfont!
+Missing character: There is no e in font nullfont!
+Missing character: There is no s in font nullfont!
+Missing character: There is no c in font nullfont!
+Missing character: There is no r in font nullfont!
+Missing character: There is no i in font nullfont!
+Missing character: There is no p in font nullfont!
+Missing character: There is no t in font nullfont!
+Missing character: There is no i in font nullfont!
+Missing character: There is no o in font nullfont!
+Missing character: There is no n in font nullfont!
+Missing character: There is no . in font nullfont!
+
+Overfull \hbox (20.0pt too wide) in paragraph at lines 6--10
+[]
+ []
+
+
+Overfull \hbox (10.86105pt too wide) in paragraph at lines 6--10
+[]
+ []
+
+)
+! Emergency stop.
+<*> \input starting.tex
+                       
+*** (job aborted, no legal \end found)
+
+ 
+Here is how much of TeX's memory you used:
+ 9 strings out of 493857
+ 174 string characters out of 1153305
+ 47808 words of memory out of 3000000
+ 3383 multiletter control sequences out of 15000+50000
+ 3948 words of font info for 15 fonts, out of 3000000 for 9000
+ 714 hyphenation exceptions out of 8191
+ 19i,2n,19p,104b,89s stack positions out of 5000i,500n,10000p,200000b,50000s
+!  ==> Fatal error occurred, no output PDF file produced!
diff --git a/examples/programs/essai.mlw b/examples/programs/essai.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/examples/programs/essai/project.db b/examples/programs/essai/project.db
new file mode 100644
index 0000000000000000000000000000000000000000..fd67fab488f327a5044de66f60e76f26b7b59e02
Binary files /dev/null and b/examples/programs/essai/project.db differ
diff --git a/examples/programs/isqrt.why b/examples/programs/isqrt.why
new file mode 100644
index 0000000000000000000000000000000000000000..c6905582064b1c86d1d4e3262d8448b340e865a2
--- /dev/null
+++ b/examples/programs/isqrt.why
@@ -0,0 +1,17 @@
+
+theory T
+
+  use import int.Int
+
+  logic sqr (x:int) : int = x * x
+
+  goal WP :  forall x:int. x >= 0 ->
+     ( ( 0 >= 0) and ( ( x >= sqr 0) and ( 1 = sqr (0 + 1)))) and
+    (forall sum:int. forall count:int. ( ( count >= 0) and ( ( x >= sqr
+    count) and ( sum = sqr (count + 1)))) ->
+    (if sum <= x then
+     ( ( (count + 1) >= 0) and ( ( x >= sqr (count + 1)) and
+    ( ((sum + (2 * (count + 1))) + 1) = sqr ((count + 1) + 1)))) else  ( count >= 0) and
+    ( ( sqr count <= x) and ( x < sqr (count + 1)))))
+
+end
\ No newline at end of file
diff --git a/examples/programs/prgbench.avg b/examples/programs/prgbench.avg
new file mode 100644
index 0000000000000000000000000000000000000000..a56010b2f0a9c2d94e5dae696de2e4be55f64799
--- /dev/null
+++ b/examples/programs/prgbench.avg
@@ -0,0 +1,3 @@
+(v,t,u,f,i) - valid, unknown, timeout, invalid, failure
+(17 : 0.06, 0 : 0.00, 2 : 5.01, 0 : 0.00, 0 : 0.00) - fast.cvc3
+(16 : 0.29, 0 : 0.00, 3 : 5.01, 0 : 0.00, 0 : 0.00) - fast.alt-ergo
diff --git a/examples/programs/prgbench.csv b/examples/programs/prgbench.csv
new file mode 100644
index 0000000000000000000000000000000000000000..0fbced14751c9eef9efac2498fa78f19f81f9ece
--- /dev/null
+++ b/examples/programs/prgbench.csv
@@ -0,0 +1,3 @@
+prover ,funny.talk290.mlw.Pgm, , funny.talk290.mlw.Pgm, , funny.talk290.mlw.Pgm, , funny.talk290.mlw.Pgm, , funny.talk290.mlw.Pgm, , funny.talk290.mlw.Pgm, , funny.talk290.mlw.Pgm, , funny.talk290.mlw.Pgm, , funny.talk290.mlw.Pgm, , funny.talk290.mlw.Pgm, , funny.talk290.mlw.Pgm, , funny.talk290.mlw.Pgm, , funny.talk290.mlw.Pgm, , funny.talk290.mlw.Pgm, , funny.talk290.mlw.Pgm, , funny.talk290.mlw.Pgm, , funny.talk290.mlw.Pgm, , funny.talk290.mlw.Pgm, , funny.talk290.mlw.Pgm, 
+fast.cvc3 ,Valid, 0.045, Valid, 0.042, Timeout, 5.008, Valid, 0.054, Valid, 0.074, Timeout, 5.020, Valid, 0.025, Valid, 0.036, Valid, 0.038, Valid, 0.036, Valid, 0.032, Valid, 0.028, Valid, 0.033, Valid, 0.111, Valid, 0.066, Valid, 0.033, Valid, 0.382, Valid, 0.030, Valid, 0.027
+fast.alt-ergo ,Valid, 0.042, Valid, 0.069, Timeout, 4.995, Valid, 0.036, Valid, 0.033, Timeout, 5.015, Valid, 0.030, Valid, 0.031, Valid, 0.026, Valid, 0.023, Valid, 0.033, Valid, 0.023, Valid, 0.023, Timeout, 5.011, Valid, 2.704, Valid, 0.028, Valid, 1.529, Valid, 0.030, Valid, 0.018
\ No newline at end of file
diff --git a/examples/programs/prgbench.time b/examples/programs/prgbench.time
new file mode 100644
index 0000000000000000000000000000000000000000..169042e176a48ed5a3c594c31b4fb2036dc4fa4c
--- /dev/null
+++ b/examples/programs/prgbench.time
@@ -0,0 +1,3 @@
+0.00, 0.28, 0.56, 0.84, 1.12, 1.40, 1.68, 1.96, 2.24, 2.52
+   0,   16,   17,   17,   17,   17,   17,   17,   17,   17 - fast.cvc3
+   0,   14,   14,   14,   14,   14,   15,   15,   15,   15 - fast.alt-ergo
diff --git a/examples/tptp/agatha/agatha.why-Agatha-Diff1_1.why b/examples/tptp/agatha/agatha.why-Agatha-Diff1_1.why
new file mode 100644
index 0000000000000000000000000000000000000000..a1afac170d9271ba8e4527b0eec62dbf350d0233
--- /dev/null
+++ b/examples/tptp/agatha/agatha.why-Agatha-Diff1_1.why
@@ -0,0 +1,74 @@
+(* this is a prelude for Alt-Ergo*)
+type person
+
+logic Agatha : person
+
+
+logic Butler : person
+
+
+logic Charles : person
+
+
+logic match_person : person, 'a, 'a, 'a -> 'a
+
+
+axiom match_person_Agatha :
+  (forall z:'a. forall z1:'a. forall z2:'a [match_person(Agatha, z, z1, z2)].
+  (match_person(Agatha, z, z1, z2) = z))
+
+
+axiom match_person_Butler :
+  (forall z:'a. forall z1:'a. forall z2:'a [match_person(Butler, z, z1, z2)].
+  (match_person(Butler, z, z1, z2) = z1))
+
+
+axiom match_person_Charles :
+  (forall z:'a. forall z1:'a. forall z2:'a [match_person(Charles, z, z1,
+  z2)]. (match_person(Charles, z, z1, z2) = z2))
+
+
+axiom person_inversion :
+  (forall u:person. forall z:'a. forall z1:'a. forall z2:'a [match_person(u,
+  z2, z1, z)]. (((u = Agatha) or (u = Butler)) or (u = Charles)))
+
+
+logic hates : person, person -> prop
+
+
+logic richer : person, person -> prop
+
+
+logic lives : person -> prop
+
+
+logic killed : person, person -> prop
+
+
+axiom Lives1 : lives(Agatha)
+
+
+axiom Lives2 : lives(Charles)
+
+
+axiom Lives3 : lives(Butler)
+
+
+axiom NoOneLivesForever :
+  (forall x:person. (lives(x) -> ((x = Agatha) or ((x = Charles) or
+  (x = Butler)))))
+
+
+axiom MURDER : (exists x:person. (lives(x) and killed(x, Agatha)))
+
+
+axiom Hate_and_killed :
+  (forall p1:person. forall p2:person. (killed(p1, p2) -> hates(p1, p2)))
+
+
+axiom Killed_and_wealth :
+  (forall p1:person. forall p2:person. (killed(p1, p2) -> (not richer(p1,
+  p2))))
+
+
+goal Diff1 : (not (Agatha = Butler))
diff --git a/examples/tptp/agatha/agatha.why_Agatha_Enigma_1.v b/examples/tptp/agatha/agatha.why_Agatha_Enigma_1.v
new file mode 100644
index 0000000000000000000000000000000000000000..2c50007afff8e4d08b8fa1b32dbfbb7f66ffe55f
--- /dev/null
+++ b/examples/tptp/agatha/agatha.why_Agatha_Enigma_1.v
@@ -0,0 +1,59 @@
+(* Beware! Only edit allowed sections below    *)
+(* This file is generated by Why3's Coq driver *)
+Require Import ZArith.
+Require Import Rbase.
+Inductive person  :=
+  | agatha : person 
+  | butler : person 
+  | charles : person .
+
+Parameter hates: person -> person  -> Prop.
+
+Parameter richer: person -> person  -> Prop.
+
+Parameter lives: person  -> Prop.
+
+Parameter killed: person -> person  -> Prop.
+
+Axiom Lives1 : (lives (agatha )).
+
+Axiom Lives2 : (lives (charles )).
+
+Axiom Lives3 : (lives (butler )).
+
+Axiom NoOneLivesForever : forall (x:person), (lives x) -> ((x = (agatha )) \/
+  ((x = (charles )) \/ (x = (butler )))).
+
+Axiom MURDER : exists x:person, (lives x) /\ (killed x (agatha )).
+
+Axiom Hate_and_killed : forall (p1:person) (p2:person), (killed p1 p2) ->
+  (hates p1 p2).
+
+Axiom Killed_and_wealth : forall (p1:person) (p2:person), (killed p1 p2) ->
+  ~ (richer p1 p2).
+
+Axiom Diff1 : ~ ((agatha ) = (butler )).
+
+Axiom Diff2 : ~ ((agatha ) = (charles )).
+
+Axiom Diff3 : ~ ((charles ) = (butler )).
+
+Axiom H1 : forall (x:person), (hates (agatha ) x) -> ~ (hates (charles ) x).
+
+Axiom H2 : forall (x:person), (~ (x = (butler ))) -> (hates (agatha ) x).
+
+Axiom H3 : forall (x:person), (~ (richer x (agatha ))) -> (hates (butler )
+  x).
+
+Axiom H4 : forall (x:person), (hates (agatha ) x) -> (hates (butler ) x).
+
+Axiom H5 : forall (x:person), exists y:person, ~ (hates x y).
+
+Theorem Enigma : (killed (agatha ) (agatha )).
+(* YOU MAY EDIT THE PROOF BELOW *)
+
+
+Qed.
+(* DO NOT EDIT BELOW *)
+
+
diff --git a/examples/tptp/agatha/project.db b/examples/tptp/agatha/project.db
new file mode 100644
index 0000000000000000000000000000000000000000..5eabc703ef9658b91783a7d64b3bed2d0e3776d4
Binary files /dev/null and b/examples/tptp/agatha/project.db differ
diff --git a/theories/comparison/comparison.why_MinMax_Max_sym_1.v b/theories/comparison/comparison.why_MinMax_Max_sym_1.v
new file mode 100644
index 0000000000000000000000000000000000000000..cd89c3c8a03e4fbf2995ca52e368dbd86ce0c393
--- /dev/null
+++ b/theories/comparison/comparison.why_MinMax_Max_sym_1.v
@@ -0,0 +1,36 @@
+(* Beware! Only edit allowed sections below    *)
+(* This file is generated by Why3's Coq driver *)
+Require Import ZArith.
+Require Import Rbase.
+Parameter t : Type.
+
+Parameter ge: t -> t  -> Prop.
+
+Parameter min: t -> t  -> t.
+
+Parameter max: t -> t  -> t.
+
+Axiom Max_is_ge : forall (x:t) (y:t), (ge (max x y) x) /\ (ge (max x y) y).
+
+Axiom Max_is_some : forall (x:t) (y:t), ((max x y) = x) \/ ((max x y) = y).
+
+Axiom Min_is_le : forall (x:t) (y:t), (ge x (min x y)) /\ (ge y (min x y)).
+
+Axiom Min_is_some : forall (x:t) (y:t), ((min x y) = x) \/ ((min x y) = y).
+
+Axiom Max_x : forall (x:t) (y:t), (ge x y) -> ((max x y) = x).
+
+Axiom Max_y : forall (x:t) (y:t), (ge y x) -> ((max x y) = y).
+
+Axiom Min_x : forall (x:t) (y:t), (ge y x) -> ((min x y) = x).
+
+Axiom Min_y : forall (x:t) (y:t), (ge x y) -> ((min x y) = y).
+
+Theorem Max_sym : forall (x:t) (y:t), (ge x y) -> ((max x y) = (max y x)).
+(* YOU MAY EDIT THE PROOF BELOW *)
+intuition.
+
+Qed.
+(* DO NOT EDIT BELOW *)
+
+
diff --git a/theories/comparison/comparison.why_MinMax_Max_x_1.v b/theories/comparison/comparison.why_MinMax_Max_x_1.v
new file mode 100644
index 0000000000000000000000000000000000000000..33fc09520c9cc7c6340d20c548dc29fbe2b64cf7
--- /dev/null
+++ b/theories/comparison/comparison.why_MinMax_Max_x_1.v
@@ -0,0 +1,28 @@
+(* Beware! Only edit allowed sections below    *)
+(* This file is generated by Why3's Coq driver *)
+Require Import ZArith.
+Require Import Rbase.
+Parameter t : Type.
+
+Parameter ge: t -> t  -> Prop.
+
+Parameter min: t -> t  -> t.
+
+Parameter max: t -> t  -> t.
+
+Axiom Max_is_ge : forall (x:t) (y:t), (ge (max x y) x) /\ (ge (max x y) y).
+
+Axiom Max_is_some : forall (x:t) (y:t), ((max x y) = x) \/ ((max x y) = y).
+
+Axiom Min_is_le : forall (x:t) (y:t), (ge x (min x y)) /\ (ge y (min x y)).
+
+Axiom Min_is_some : forall (x:t) (y:t), ((min x y) = x) \/ ((min x y) = y).
+
+Theorem Max_x : forall (x:t) (y:t), (ge x y) -> ((max x y) = x).
+(* YOU MAY EDIT THE PROOF BELOW *)
+
+
+Qed.
+(* DO NOT EDIT BELOW *)
+
+
diff --git a/theories/comparison/project.db b/theories/comparison/project.db
new file mode 100644
index 0000000000000000000000000000000000000000..5ac792739b420e69044b80e4c29fc2423923e867
Binary files /dev/null and b/theories/comparison/project.db differ
diff --git a/tmp.why b/tmp.why
new file mode 100644
index 0000000000000000000000000000000000000000..e223b40f277d1727dc23c470130e46ef5fed3689
--- /dev/null
+++ b/tmp.why
@@ -0,0 +1,41 @@
+theory CosineSingle
+
+use import real.Real
+use import real.Abs
+use import real.Trigonometry
+use import floating_point.Rounding
+use import floating_point.Single
+
+(* approximation of cosine function by 1 - x^2 / 2 on interval [-1/32; 1/32] *)
+
+
+
+lemma MethodError: forall x:real. abs x <= 0x1p-5 ->
+  abs (1.0 - x * x * 0.5 - cos x) <= 0x1p-24 
+
+
+(* computation in single precision *)
+
+logic round_single (m:mode) (x:real) : single
+
+axiom RoundSingle: forall m:mode, x:real.
+  value (round_single m x) = round m x
+
+logic cos_single (x:single) : single =
+  let x2 = round_single NearestTiesToEven (value x * value x) in
+  let x2o2 = round_single NearestTiesToEven (0.5 * value x2) in
+  round_single NearestTiesToEven (1.0 - value x2o2) 
+
+lemma TotalError: forall x:single. abs (value x) <= 0x1p-5 ->
+  let cos_x = cos_single x in
+  abs (value cos_x - cos (value x)) <= 0x1p-24
+
+end
+
+(*
+Local Variables:
+compile-command: "../bin/whyide.byte my_cosine.why"
+End:
+*)
+
+