Coq proofs for bag.Bag in theories/bag/

theories/bag/why3session.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session SYSTEM "/home/jcf/why3/share/why3session.dtd">
+<why3session
+ name="bag/why3session.xml">
+ <prover
+  id="0"
+  name="Alt-Ergo"
+  version="0.94"/>
+ <prover
+  id="1"
+  name="CVC3"
+  version="2.4.1"/>
+ <prover
+  id="2"
+  name="Coq"
+  version="8.3pl3"/>
+ <file
+  name="../bag.why"
+  verified="true"
+  expanded="true">
+  <theory
+   name="Bag"
+   locfile="bag/../bag.why"
+   loclnum="4" loccnumb="7" loccnume="10"
+   verified="true"
+   expanded="true">
+   <goal
+    name="is_empty"
+    locfile="bag/../bag.why"
+    loclnum="31" loccnumb="8" loccnume="16"
+    sum="d77095ea37831bcd3bbea60cae4fee05"
+    proved="true"
+    expanded="false"
+    shape="ainfix =V0aempty_bagIainfix =anb_occV1V0c0FF">
+    <proof
+     prover="1"
+     timelimit="60"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.01"/>
+    </proof>
+   </goal>
+   <goal
+    name="occ_singleton_eq"
+    locfile="bag/../bag.why"
+    loclnum="40" loccnumb="8" loccnume="24"
+    sum="a9825a1a35d41e7746fd3bac8cb19ecb"
+    proved="true"
+    expanded="false"
+    shape="ainfix =anb_occV1asingletonV0c1Iainfix =V0V1F">
+    <proof
+     prover="0"
+     timelimit="60"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.01"/>
+    </proof>
+   </goal>
+   <goal
+    name="occ_singleton_neq"
+    locfile="bag/../bag.why"
+    loclnum="42" loccnumb="8" loccnume="25"
+    sum="f68c91c87a6fe5d6c1b83f0777fa8a49"
+    proved="true"
+    expanded="false"
+    shape="ainfix =anb_occV1asingletonV0c0Iainfix =V0V1NF">
+    <proof
+     prover="0"
+     timelimit="60"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+   </goal>
+   <goal
+    name="Union_comm"
+    locfile="bag/../bag.why"
+    loclnum="53" loccnumb="8" loccnume="18"
+    sum="58fbae88bad3a455c60815dbaf53257a"
+    proved="true"
+    expanded="false"
+    shape="ainfix =aunionV0V1aunionV1V0F">
+    <proof
+     prover="2"
+     timelimit="60"
+     edited="bag_Bag_Union_comm_1.v"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.73"/>
+    </proof>
+   </goal>
+   <goal
+    name="Union_identity"
+    locfile="bag/../bag.why"
+    loclnum="55" loccnumb="8" loccnume="22"
+    sum="9c2ce352a14859e0baecfd7d320ff17b"
+    proved="true"
+    expanded="false"
+    shape="ainfix =aunionV0aempty_bagV0F">
+    <proof
+     prover="2"
+     timelimit="60"
+     edited="bag_Bag_Union_identity_1.v"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.75"/>
+    </proof>
+   </goal>
+   <goal
+    name="Union_assoc"
+    locfile="bag/../bag.why"
+    loclnum="57" loccnumb="8" loccnume="19"
+    sum="4d83b0ea8710f624c0952d8b1fd0bca7"
+    proved="true"
+    expanded="false"
+    shape="ainfix =aunionV0aunionV1V2aunionaunionV0V1V2F">
+    <proof
+     prover="2"
+     timelimit="60"
+     edited="bag_Bag_Union_assoc_1.v"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.74"/>
+    </proof>
+   </goal>
+   <goal
+    name="bag_simpl"
+    locfile="bag/../bag.why"
+    loclnum="60" loccnumb="8" loccnume="17"
+    sum="356f083e7eb5ae679731508085001539"
+    proved="true"
+    expanded="false"
+    shape="ainfix =V0V2Iainfix =aunionV0V1aunionV2V1F">
+    <proof
+     prover="2"
+     timelimit="60"
+     edited="bag_Bag_bag_simpl_1.v"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.76"/>
+    </proof>
+   </goal>
+   <goal
+    name="bag_simpl_left"
+    locfile="bag/../bag.why"
+    loclnum="63" loccnumb="8" loccnume="22"
+    sum="0a74029dc1ed387aab558a13434ae978"
+    proved="true"
+    expanded="false"
+    shape="ainfix =V1V2Iainfix =aunionV0V1aunionV0V2F">
+    <proof
+     prover="0"
+     timelimit="60"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.03"/>
+    </proof>
+   </goal>
+   <goal
+    name="occ_add_eq"
+    locfile="bag/../bag.why"
+    loclnum="70" loccnumb="8" loccnume="18"
+    sum="4e57e2136c73f216e76c3b7f2e9c083f"
+    proved="true"
+    expanded="false"
+    shape="ainfix =anb_occV1aaddV1V0ainfix +anb_occV1V0c1Iainfix =V1V2F">
+    <proof
+     prover="0"
+     timelimit="60"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.02"/>
+    </proof>
+   </goal>
+   <goal
+    name="occ_add_neq"
+    locfile="bag/../bag.why"
+    loclnum="74" loccnumb="8" loccnume="19"
+    sum="cbe9799ebc6ace0a7c885a612a789438"
+    proved="true"
+    expanded="false"
+    shape="ainfix =anb_occV2aaddV1V0anb_occV2V0Iainfix =V1V2NF">
+    <proof
+     prover="0"
+     timelimit="60"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+   </goal>
+   <goal
+    name="Card_add"
+    locfile="bag/../bag.why"
+    loclnum="86" loccnumb="8" loccnume="16"
+    sum="eedb761ba2e1b6bbff65644ec9ea984d"
+    proved="true"
+    expanded="false"
+    shape="ainfix =acardaaddV0V1ainfix +c1acardV1F">
+    <proof
+     prover="0"
+     timelimit="60"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.01"/>
+    </proof>
+   </goal>
+   <goal
+    name="Diff_empty_right"
+    locfile="bag/../bag.why"
+    loclnum="97" loccnumb="8" loccnume="24"
+    sum="3eeb720c4538804e913b6533ee839869"
+    proved="true"
+    expanded="false"
+    shape="ainfix =adiffV0aempty_bagV0F">
+    <proof
+     prover="2"
+     timelimit="60"
+     edited="bag_Bag_Diff_empty_right_1.v"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.78"/>
+    </proof>
+   </goal>
+   <goal
+    name="Diff_empty_left"
+    locfile="bag/../bag.why"
+    loclnum="98" loccnumb="8" loccnume="23"
+    sum="0c4a0deb6a063cef064e2614b35223d6"
+    proved="true"
+    expanded="false"
+    shape="ainfix =adiffaempty_bagV0aempty_bagF">
+    <proof
+     prover="2"
+     timelimit="60"
+     edited="bag_Bag_Diff_empty_left_1.v"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.76"/>
+    </proof>
+   </goal>
+   <goal
+    name="Diff_add"
+    locfile="bag/../bag.why"
+    loclnum="100" loccnumb="8" loccnume="16"
+    sum="ca1b0cda67984344863d7a8541f52005"
+    proved="true"
+    expanded="false"
+    shape="ainfix =adiffaaddV1V0asingletonV1V0F">
+    <proof
+     prover="2"
+     timelimit="60"
+     edited="bag_Bag_Diff_add_1.v"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.77"/>
+    </proof>
+   </goal>
+   <goal
+    name="Diff_comm"
+    locfile="bag/../bag.why"
+    loclnum="102" loccnumb="8" loccnume="17"
+    sum="4561b67ab6fe3f20c19fa8333de9c1eb"
+    proved="true"
+    expanded="false"
+    shape="ainfix =adiffadiffV0V1V2adiffadiffV0V2V1F">
+    <proof
+     prover="2"
+     timelimit="60"
+     edited="bag_Bag_Diff_comm_1.v"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="1.38"/>
+    </proof>
+   </goal>
+   <goal
+    name="Add_diff"
+    locfile="bag/../bag.why"
+    loclnum="105" loccnumb="8" loccnume="16"
+    sum="04361da122924d170e5143043cb472f3"
+    proved="true"
+    expanded="true"
+    shape="ainfix =aaddV1adiffV0asingletonV1V0IamemV1V0F">
+    <proof
+     prover="2"
+     timelimit="60"
+     edited="bag_Bag_Add_diff_1.v"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.80"/>
+    </proof>
+   </goal>
+  </theory>
+ </file>
+</why3session>