Commit 082ea344 authored by MARCHE Claude's avatar MARCHE Claude

Update sessions

parent 81c3a9ef
......@@ -63,11 +63,11 @@ echo "=== Standard Library ==="
run_dir ../lib/why3
echo ""
echo "=== Tests ==="
# there's no session there...
# echo "=== Tests ==="
# run_dir tests
# run_dir tests-provers
# echo ""
run_dir tests-provers
echo ""
echo "=== Check Builtin translation ==="
run_dir check-builtin
......
......@@ -20,7 +20,7 @@
locfile="../alt-ergo-models.mlw"
loclnum="16" loccnumb="6" loccnume="7"
expl="VC for f"
sum="43b5cd89c4a52dac700602cc0d4dc0e6"
sum="8cc242702e67821a4b9cf0e7042df2d3"
proved="false"
expanded="true"
shape="ainfix <=ic0ainfix +V0c3ainfix >=V0c42c50F">
......@@ -40,7 +40,7 @@
locfile="../alt-ergo-models.mlw"
loclnum="20" loccnumb="6" loccnume="14"
expl="VC for f_no_lab"
sum="43b5cd89c4a52dac700602cc0d4dc0e6"
sum="8cc242702e67821a4b9cf0e7042df2d3"
proved="false"
expanded="true"
shape="ainfix <=ic0ainfix +V0c3ainfix >=V0c42c50F">
......@@ -60,7 +60,7 @@
locfile="../alt-ergo-models.mlw"
loclnum="26" loccnumb="6" loccnume="7"
expl="VC for g"
sum="e15ca0e9cafe57beb29d464140427eeb"
sum="618aa543d0727345b8225c89dc0690b9"
proved="false"
expanded="true"
shape="iainfix <=c0c50ainfix <=ainfix +V1c3c50ainfix >=V1c42Iainfix =V1ainfix +V0c1FF">
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import Rfunctions.
Require Import BuiltIn.
Require Reals.Rfunctions.
Require BuiltIn.
Require real.Real.
Require real.RealInfix.
Require int.Int.
Axiom Power_s : forall (x:R) (n:Z), (0%Z <= n)%Z ->
((powerRZ x (n + 1%Z)%Z) = (x * (powerRZ x n))%R).
Axiom Power_sum : forall (x:R) (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) ->
((powerRZ x (n + m)%Z) = ((powerRZ x n) * (powerRZ x m))%R).
Axiom Power_mult : forall (x:R) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
((powerRZ x (n * m)%Z) = (powerRZ (powerRZ x n) m))).
Require real.PowerInt.
Require Import Interval_tactic.
(* Why3 goal *)
Theorem pow_eps2_max_int : ((powerRZ (1%R + ((7 / 1125899906842624)%R + (3 / 9007199254740992)%R)%R)%R 2147483647%Z) <= 2%R)%R.
Strategy 1000 [powerRZ].
Theorem pow_eps2_max_int : ((Reals.Rfunctions.powerRZ (1%R + ((7 / 1125899906842624)%R + (3 / 9007199254740992)%R)%R)%R 2147483647%Z) <= 2%R)%R.
Strategy 1000 [Rfunctions.powerRZ].
interval with (i_prec 34).
Qed.
......@@ -30,7 +30,7 @@
edited="coqmninterval_P_pow_eps2_max_int_1.v"
obsolete="false"
archived="false">
<result status="valid" time="2.97"/>
<result status="valid" time="2.90"/>
</proof>
</goal>
</theory>
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment