Commit 01f936d6 authored by MARCHE Claude's avatar MARCHE Claude

update sessions

parent c3af2d13
......@@ -46,7 +46,7 @@
name="nth_one1"
locfile="../double.why"
loclnum="73" loccnumb="8" loccnume="16"
sum="779313c3d425e95c0f0b6bc0a29d053c"
sum="d93706da8f80916a7cccd7f4adfcdb1f"
proved="true"
expanded="true"
shape="ainfix =anthaoneV0aFalseIainfix <=V0c51Aainfix <=c0V0F">
......@@ -63,7 +63,7 @@
name="nth_one2"
locfile="../double.why"
loclnum="74" loccnumb="8" loccnume="16"
sum="6c5ab56d5ca58c8563265ef1e76caaff"
sum="f9798dd9cc48af1e59ee6f9a1e25c01b"
proved="true"
expanded="true"
shape="ainfix =anthaoneV0aTrueIainfix <=V0c61Aainfix <=c52V0F">
......@@ -80,7 +80,7 @@
name="nth_one3"
locfile="../double.why"
loclnum="75" loccnumb="8" loccnume="16"
sum="9b7649e3d4b50c0652cca89ce17ffb16"
sum="53352cd7abc005bbbe493bc4cb6c9c7e"
proved="true"
expanded="false"
shape="ainfix =anthaoneV0aFalseIainfix <=V0c63Aainfix <=c62V0F">
......@@ -97,7 +97,7 @@
name="sign_one"
locfile="../double.why"
loclnum="77" loccnumb="8" loccnume="16"
sum="4d768e8050c8a290ad59f6fb9c3648f3"
sum="3ffab2a9db52af753f5eed5538b1db69"
proved="true"
expanded="false"
shape="ainfix =asignaoneaFalse">
......@@ -146,7 +146,7 @@
name="exp_one"
locfile="../double.why"
loclnum="78" loccnumb="8" loccnume="15"
sum="5cc0aeaf0df1030578dc94096e87e552"
sum="2dca867e9e8fcf82917bf2822f43935f"
proved="true"
expanded="false"
shape="ainfix =aexpaonec1023">
......@@ -172,7 +172,7 @@
name="mantissa_one"
locfile="../double.why"
loclnum="79" loccnumb="8" loccnume="20"
sum="911f111a48f29e043cd6271df6d92b7b"
sum="0feb145c042bb763a553aba0bb907944"
proved="true"
expanded="false"
shape="ainfix =amantissaaonec0">
......@@ -205,7 +205,7 @@
name="double_value_of_1"
locfile="../double.why"
loclnum="81" loccnumb="8" loccnume="25"
sum="3c554760bb4cb8554fc679a00a8da995"
sum="0b9b42fc43149dcbbe29549dd92564a1"
proved="true"
expanded="false"
shape="ainfix =adouble_of_bv64aonec1.0">
......
......@@ -35,13 +35,13 @@
version="3.2"/>
<file
name="../power2.why"
verified="false"
verified="true"
expanded="true">
<theory
name="Pow2int"
locfile="../power2.why"
loclnum="1" loccnumb="7" loccnume="14"
verified="false"
verified="true"
expanded="true">
<goal
name="Power_1"
......@@ -3354,7 +3354,7 @@
locfile="../power2.why"
loclnum="106" loccnumb="8" loccnume="20"
sum="9ec8d3a875e92f04087a08c99a61c4a2"
proved="false"
proved="true"
expanded="false"
shape="ainfix =amodadivainfix +V0apow2V1apow2V2c2amodadivV0apow2V2c2Iainfix &lt;V2V1Aainfix &lt;=c0V2F">
<proof
......@@ -3362,7 +3362,7 @@
timelimit="5"
memlimit="1000"
edited="power2_Pow2int_Mod_pow2_gen_1.v"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="1.80"/>
</proof>
......@@ -3372,7 +3372,7 @@
name="Pow2real"
locfile="../power2.why"
loclnum="113" loccnumb="7" loccnume="15"
verified="false"
verified="true"
expanded="true">
<goal
name="Power_s_all"
......@@ -3747,7 +3747,7 @@
locfile="../power2.why"
loclnum="149" loccnumb="8" loccnume="21"
sum="57627b08500c0a655d559ee4615414bf"
proved="false"
proved="true"
expanded="false"
shape="ainfix =apow2V0afrom_intapow2V0Iainfix &gt;=V0c0F">
<proof
......@@ -3755,7 +3755,7 @@
timelimit="5"
memlimit="1000"
edited="power2_Pow2real_Pow2_int_real_1.v"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="1.20"/>
</proof>
......
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