test metitarski

examples/tests-provers/metitarski.why

+theory P
+
+  use import real.Real
+
+  goal x_mul_x_pos :
+    forall x:real. x * x >= 0.0
+
+  function sqr (x:real) : real = x * x
+
+  goal sqr_pos :
+    forall x:real. sqr x >= 0.0
+
+end
\ No newline at end of file

examples/tests-provers/metitarski/why3session.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="3">
+ <prover
+  id="0"
+  name="MetiTarski"
+  version="2.2"/>
+ <file
+  name="../metitarski.why"
+  verified="false"
+  expanded="true">
+  <theory
+   name="P"
+   locfile="../metitarski.why"
+   loclnum="1" loccnumb="7" loccnume="8"
+   verified="false"
+   expanded="true">
+   <goal
+    name="x_mul_x_pos"
+    locfile="../metitarski.why"
+    loclnum="5" loccnumb="7" loccnume="18"
+    sum="a72dfdff8d757085e294ef63fb5e8c71"
+    proved="true"
+    expanded="true"
+    shape="ainfix &gt;=ainfix *V0V0c0.0F">
+    <proof
+     prover="0"
+     timelimit="5"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.02"/>
+    </proof>
+   </goal>
+   <goal
+    name="sqr_pos"
+    locfile="../metitarski.why"
+    loclnum="10" loccnumb="7" loccnume="14"
+    sum="14c5e18ceaa4ec73959d4db9a1295376"
+    proved="false"
+    expanded="true"
+    shape="ainfix &gt;=asqrV0c0.0F">
+    <proof
+     prover="0"
+     timelimit="5"
+     memlimit="1000"
+     edited="metitarski-P-sqr_pos_1.tptp"
+     obsolete="false"
+     archived="false">
+     <result status="unknown" time="0.24"/>
+    </proof>
+   </goal>
+  </theory>
+ </file>
+</why3session>