Commit 632c0484 authored by MARCHE Claude's avatar MARCHE Claude

why3doc for defunctionalization example

parent 83f4dee5
......@@ -21,7 +21,7 @@ all: $(MAIN).opt
doc:
why3doc ../defunctionalization.mlw
why3session html ../defunctionalization.mlw
firefox defunctionalization.mlw.html defunctionalization.html
firefox defunctionalization.mlw.html defunctionalization.html &
$(MAIN).byte: $(CMO) $(MAIN).cmo
ocamlc -g $(ZARITH) $(WHY3) $(NUMLIB).cma why3extract.cma -o $@ $^
......
theory T
use import int.Int
use import int.Power
goal g: power 2 3321941 < power 10 (power 10 6 + 4) < power 2 3321942
end
(* This file is generated by Why3's Coq 8.4 driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Power.
Require Import Interval_tactic.
(* Why3 goal *)
Theorem g : ((int.Power.power 2%Z 3321941%Z) < (int.Power.power 10%Z
((int.Power.power 10%Z 6%Z) + 4%Z)%Z))%Z /\ ((int.Power.power 10%Z
((int.Power.power 10%Z 6%Z) + 4%Z)%Z) < (int.Power.power 2%Z 3321942%Z))%Z.
interval.
Qed.
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover
id="0"
name="Alt-Ergo"
version="0.95.2"/>
<prover
id="1"
name="CVC3"
version="2.4.1"/>
<prover
id="2"
name="CVC4"
version="1.3"/>
<prover
id="3"
name="Coq"
version="8.4pl2"/>
<prover
id="4"
name="Z3"
version="3.2"/>
<prover
id="5"
name="Z3"
version="4.3.1"/>
<file
name="../computation.why"
verified="false"
expanded="true">
<theory
name="T"
locfile="../computation.why"
loclnum="2" loccnumb="7" loccnume="8"
verified="false"
expanded="true">
<goal
name="g"
locfile="../computation.why"
loclnum="7" loccnumb="5" loccnume="6"
sum="d360b93003fb60f5e122e2f5936933a3"
proved="false"
expanded="true"
shape="ainfix &lt;apowerc10ainfix +apowerc10c6c4apowerc2c3321942Aainfix &lt;apowerc2c3321941apowerc10ainfix +apowerc10c6c4">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="4.99"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.00"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="4.93"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
edited="computation_T_g_1.v"
obsolete="true"
archived="false">
<undone/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.20"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
</proof>
</goal>
</theory>
</file>
</why3session>
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