Commit ad518fe0 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

updated sessions

parent aa0b071b
......@@ -10,7 +10,7 @@
<file name="../defunctionalization.mlw" expanded="true">
<theory name="Expr" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="DirectSem" sum="af2552f4879203af23b438bd246b031f" expanded="true">
<theory name="DirectSem" sum="af2552f4879203af23b438bd246b031f">
<goal name="WP_parameter test" expl="VC for test">
<proof prover="0" memlimit="1000"><result status="valid" time="0.00"/></proof>
<proof prover="1" memlimit="1000"><result status="valid" time="0.00"/></proof>
......@@ -31,10 +31,7 @@
<transf name="induction_ty_lex">
<goal name="cps_correct_expr.1" expl="1.">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="timeout" time="5.02"/></proof>
<proof prover="2"><result status="timeout" time="5.01"/></proof>
<proof prover="3" timelimit="6" memlimit="1000"><result status="valid" time="0.01" steps="22"/></proof>
<proof prover="4"><result status="timeout" time="4.98"/></proof>
</goal>
</transf>
</goal>
......@@ -65,20 +62,20 @@
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.02" steps="134"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.02" steps="120"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter eval_2" expl="VC for eval_2">
<proof prover="0" memlimit="1000"><result status="valid" time="0.05"/></proof>
<proof prover="1" memlimit="1000"><result status="valid" time="0.02"/></proof>
<proof prover="2" memlimit="1000"><result status="valid" time="0.02"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.10" steps="161"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.10" steps="122"/></proof>
</goal>
<goal name="WP_parameter interpret_2" expl="VC for interpret_2">
<proof prover="0" memlimit="1000"><result status="valid" time="0.00"/></proof>
<proof prover="1" memlimit="1000"><result status="valid" time="0.00"/></proof>
<proof prover="2" memlimit="1000"><result status="valid" time="0.02"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.02" steps="25"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.02" steps="20"/></proof>
<proof prover="4" memlimit="1000"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter test" expl="VC for test">
......@@ -133,8 +130,6 @@
<transf name="split_goal_wp">
<goal name="WP_parameter eval_2.1" expl="1. variant decrease">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="timeout" time="4.99"/></proof>
<proof prover="2"><result status="timeout" time="4.96"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="9"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -147,17 +142,13 @@
</goal>
<goal name="WP_parameter eval_2.3" expl="3. variant decrease">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="timeout" time="4.98"/></proof>
<proof prover="2"><result status="timeout" time="4.97"/></proof>
<proof prover="3"><result status="unknown" time="0.33"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter eval_2.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.04" steps="77"/></proof>
<proof prover="4"><result status="timeout" time="4.99"/></proof>
<proof prover="3"><result status="valid" time="0.04" steps="58"/></proof>
</goal>
</transf>
</goal>
......@@ -165,7 +156,7 @@
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="21"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter test" expl="VC for test">
......@@ -216,7 +207,6 @@
</transf>
</goal>
<goal name="cps2_correct">
<proof prover="0" memlimit="1000"><result status="valid" time="0.02"/></proof>
<proof prover="1" memlimit="1000"><result status="valid" time="0.01"/></proof>
<proof prover="2" memlimit="1000"><result status="valid" time="0.03"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.02" steps="16"/></proof>
......@@ -225,7 +215,6 @@
<goal name="WP_parameter cps3_correct_expr" expl="VC for cps3_correct_expr">
<transf name="split_goal_wp">
<goal name="WP_parameter cps3_correct_expr.1" expl="1. postcondition">
<proof prover="0" memlimit="1000"><result status="valid" time="0.03"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.02" steps="45"/></proof>
<proof prover="4" memlimit="1000"><result status="valid" time="0.04"/></proof>
</goal>
......@@ -257,7 +246,6 @@
</transf>
</goal>
<goal name="cps3_correct">
<proof prover="0" memlimit="1000"><result status="valid" time="0.03"/></proof>
<proof prover="1" memlimit="1000"><result status="valid" time="0.01"/></proof>
<proof prover="2" memlimit="1000"><result status="valid" time="0.02"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.03" steps="7"/></proof>
......@@ -315,7 +303,6 @@
<proof prover="4" memlimit="1000"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter continue_4.6" expl="6. postcondition">
<proof prover="0" memlimit="1000"><result status="valid" time="0.03"/></proof>
<proof prover="1" memlimit="1000"><result status="valid" time="0.01"/></proof>
<proof prover="2" memlimit="1000"><result status="valid" time="0.02"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.02" steps="21"/></proof>
......@@ -333,13 +320,13 @@
<goal name="WP_parameter eval_4" expl="VC for eval_4">
<proof prover="0" memlimit="1000"><result status="valid" time="0.17"/></proof>
<proof prover="2" memlimit="1000"><result status="valid" time="0.10"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.83" steps="891"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.83" steps="856"/></proof>
</goal>
<goal name="WP_parameter interpret_4" expl="VC for interpret_4">
<proof prover="0" memlimit="1000"><result status="valid" time="0.02"/></proof>
<proof prover="1" memlimit="1000"><result status="valid" time="0.01"/></proof>
<proof prover="2" memlimit="1000"><result status="valid" time="0.03"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.02" steps="38"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.02" steps="37"/></proof>
<proof prover="4" memlimit="1000"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter test" expl="VC for test">
......@@ -404,7 +391,6 @@
<proof prover="1" memlimit="1000"><result status="valid" time="0.00"/></proof>
<proof prover="2" memlimit="1000"><result status="valid" time="0.01"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.03" steps="113"/></proof>
<proof prover="4" memlimit="1000"><result status="timeout" time="4.99"/></proof>
</goal>
<goal name="WP_parameter itere_opt" expl="VC for itere_opt">
<transf name="split_goal_wp">
......@@ -472,7 +458,6 @@
<goal name="WP_parameter recompose_values" expl="VC for recompose_values">
<transf name="split_goal_wp">
<goal name="WP_parameter recompose_values.1" expl="1. postcondition">
<proof prover="0" memlimit="1000"><result status="valid" time="0.06"/></proof>
<proof prover="1" memlimit="1000"><result status="valid" time="0.02"/></proof>
<proof prover="2" memlimit="1000"><result status="valid" time="0.01"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.02" steps="11"/></proof>
......@@ -517,7 +502,6 @@
</transf>
</goal>
<goal name="WP_parameter recompose_underflow" expl="VC for recompose_underflow">
<proof prover="0" memlimit="1000"><result status="valid" time="0.06"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.07" steps="235"/></proof>
<proof prover="4" memlimit="1000"><result status="valid" time="0.14"/></proof>
</goal>
......@@ -529,7 +513,6 @@
<goal name="WP_parameter eval_2" expl="VC for eval_2">
<transf name="split_goal_wp">
<goal name="WP_parameter eval_2.1" expl="1. postcondition">
<proof prover="0" memlimit="1000"><result status="valid" time="0.06"/></proof>
<proof prover="1" memlimit="1000"><result status="valid" time="0.02"/></proof>
<proof prover="2" memlimit="1000"><result status="valid" time="0.02"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.02" steps="23"/></proof>
......@@ -555,11 +538,11 @@
<proof prover="4" memlimit="1000"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter eval_2.5" expl="5. postcondition">
<proof prover="0" memlimit="1000"><result status="valid" time="1.43"/></proof>
<proof prover="0" memlimit="1000"><result status="valid" time="1.17"/></proof>
</goal>
<goal name="WP_parameter eval_2.6" expl="6. postcondition">
<proof prover="0" memlimit="1000"><result status="valid" time="0.10"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="2.66" steps="850"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="2.27" steps="842"/></proof>
<proof prover="4" memlimit="1000"><result status="valid" time="0.38"/></proof>
</goal>
</transf>
......
......@@ -6,7 +6,6 @@
<prover id="1" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="2" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="4" name="Z3" version="4.3.3" timelimit="70" memlimit="1000"/>
<file name="../hackers-delight.mlw" expanded="true">
<theory name="Utils" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
......@@ -66,9 +65,9 @@
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter hamming_spec" expl="VC for hamming_spec" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter hamming_spec.1" expl="1. assertion" expanded="true">
<goal name="WP_parameter hamming_spec" expl="VC for hamming_spec">
<transf name="split_goal_wp">
<goal name="WP_parameter hamming_spec.1" expl="1. assertion">
<proof prover="0"><result status="valid" time="2.43" steps="956"/></proof>
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
......@@ -90,13 +89,12 @@
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="WP_parameter triangleInequalityInt" expl="VC for triangleInequalityInt" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter triangleInequalityInt.1" expl="1. assertion" expanded="true">
<goal name="WP_parameter triangleInequalityInt" expl="VC for triangleInequalityInt">
<transf name="split_goal_wp">
<goal name="WP_parameter triangleInequalityInt.1" expl="1. assertion">
<proof prover="2" timelimit="70"><result status="valid" time="1.34"/></proof>
<proof prover="4"><result status="valid" time="1.31"/></proof>
</goal>
<goal name="WP_parameter triangleInequalityInt.2" expl="2. postcondition" expanded="true">
<goal name="WP_parameter triangleInequalityInt.2" expl="2. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="79"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.09"/></proof>
......
......@@ -6,15 +6,15 @@
<prover id="1" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="10" memlimit="1000"/>
<prover id="4" name="Z3" version="4.3.3" timelimit="10" memlimit="1000"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="10" memlimit="1000"/>
<file name="../linked_list_rev.mlw">
<prover id="6" name="Z3" version="4.4.0" timelimit="5" memlimit="1000"/>
<file name="../linked_list_rev.mlw" expanded="true">
<theory name="Disjoint" sum="d9538770c8f60c61e92f6baffbf62d5d">
<goal name="WP_parameter mem_decomp" expl="VC for mem_decomp">
<proof prover="2"><result status="valid" time="0.02" steps="54"/></proof>
</goal>
</theory>
<theory name="InPlaceRev" sum="b22837339323e806694c7579e14400db">
<theory name="InPlaceRev" sum="b22837339323e806694c7579e14400db" expanded="true">
<goal name="WP_parameter list_seg_frame_ext" expl="VC for list_seg_frame_ext">
<proof prover="2"><result status="valid" time="0.16" steps="276"/></proof>
</goal>
......@@ -95,7 +95,7 @@
</transf>
</goal>
</theory>
<theory name="InPlaceRevSeq" sum="38c0bab239afbeb1f1b0cc0a7d5c1f81">
<theory name="InPlaceRevSeq" sum="38c0bab239afbeb1f1b0cc0a7d5c1f81" expanded="true">
<goal name="WP_parameter mem_decomp" expl="VC for mem_decomp">
<transf name="split_goal_wp">
<goal name="WP_parameter mem_decomp.1" expl="1. postcondition">
......@@ -121,13 +121,13 @@
<ip_library name="HighOrd"/>
<ip_qualid name="pred"/>
</ts_pos>
<ts_pos name="&apos;mark" arity="0" id="64"
<ts_pos name="&apos;mark" arity="0" id="68"
ip_theory="Mark">
<ip_library name="why3"/>
<ip_library name="Mark"/>
<ip_qualid name="&apos;mark"/>
</ts_pos>
<ts_pos name="ref" arity="1" id="4569"
<ts_pos name="ref" arity="1" id="4572"
ip_theory="Ref">
<ip_library name="ref"/>
<ip_qualid name="ref"/>
......@@ -144,270 +144,270 @@
<ip_library name="HighOrd"/>
<ip_qualid name="infix @"/>
</ls_pos>
<ls_pos name="one" id="268"
<ls_pos name="one" id="272"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="one"/>
</ls_pos>
<ls_pos name="infix &lt;" id="269"
<ls_pos name="infix &lt;" id="273"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix &lt;"/>
</ls_pos>
<ls_pos name="infix &gt;" id="272"
<ls_pos name="infix &gt;" id="276"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix &gt;"/>
</ls_pos>
<ls_pos name="infix +" id="1438"
<ls_pos name="infix +" id="1442"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix +"/>
</ls_pos>
<ls_pos name="prefix -" id="1439"
<ls_pos name="prefix -" id="1443"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="prefix -"/>
</ls_pos>
<ls_pos name="infix *" id="1440"
<ls_pos name="infix *" id="1444"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix *"/>
</ls_pos>
<ls_pos name="infix &gt;=" id="1508"
<ls_pos name="infix &gt;=" id="1512"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="infix &gt;="/>
</ls_pos>
<ls_pos name="get" id="2968"
<ls_pos name="get" id="2971"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="get"/>
</ls_pos>
<ls_pos name="set" id="2971"
<ls_pos name="set" id="2974"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="set"/>
</ls_pos>
<ls_pos name="mixfix [&lt;-]" id="2991"
<ls_pos name="mixfix [&lt;-]" id="2994"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="mixfix [&lt;-]"/>
</ls_pos>
<ls_pos name="prefix !" id="4575"
<ls_pos name="prefix !" id="4578"
ip_theory="Ref">
<ip_library name="ref"/>
<ip_qualid name="prefix !"/>
</ls_pos>
<ls_pos name="length" id="6389"
<ls_pos name="length" id="6392"
ip_theory="Seq">
<ip_library name="seq"/>
<ip_qualid name="length"/>
</ls_pos>
<ls_pos name="empty" id="6394"
<ls_pos name="empty" id="6397"
ip_theory="Seq">
<ip_library name="seq"/>
<ip_qualid name="empty"/>
</ls_pos>
<ls_pos name="get" id="6396"
<ls_pos name="get" id="6399"
ip_theory="Seq">
<ip_library name="seq"/>
<ip_qualid name="get"/>
</ls_pos>
<ls_pos name="set" id="6408"
<ls_pos name="set" id="6411"
ip_theory="Seq">
<ip_library name="seq"/>
<ip_qualid name="set"/>
</ls_pos>
<ls_pos name="mixfix [&lt;-]" id="6435"
<ls_pos name="mixfix [&lt;-]" id="6438"
ip_theory="Seq">
<ip_library name="seq"/>
<ip_qualid name="mixfix [&lt;-]"/>
</ls_pos>
<ls_pos name="infix ==" id="6448"
<ls_pos name="infix ==" id="6451"
ip_theory="Seq">
<ip_library name="seq"/>
<ip_qualid name="infix =="/>
</ls_pos>
<ls_pos name="cons" id="6465"
<ls_pos name="cons" id="6468"
ip_theory="Seq">
<ip_library name="seq"/>
<ip_qualid name="cons"/>
</ls_pos>
<ls_pos name="snoc" id="6480"
<ls_pos name="snoc" id="6483"
ip_theory="Seq">
<ip_library name="seq"/>
<ip_qualid name="snoc"/>
</ls_pos>
<ls_pos name="create" id="6560"
<ls_pos name="create" id="6563"
ip_theory="Seq">
<ip_library name="seq"/>
<ip_qualid name="create"/>
</ls_pos>
<ls_pos name="disjoint" id="7000"
<ls_pos name="disjoint" id="7003"
ip_theory="InPlaceRevSeq">
<ip_qualid name="disjoint"/>
</ls_pos>
<pr_pos name="Assoc" id="1441"
<pr_pos name="Assoc" id="1445"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Assoc"/>
</pr_pos>
<pr_pos name="Unit_def_l" id="1448"
<pr_pos name="Unit_def_l" id="1452"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Unit_def_l"/>
</pr_pos>
<pr_pos name="Unit_def_r" id="1451"
<pr_pos name="Unit_def_r" id="1455"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Unit_def_r"/>
</pr_pos>
<pr_pos name="Inv_def_l" id="1454"
<pr_pos name="Inv_def_l" id="1458"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Inv_def_l"/>
</pr_pos>
<pr_pos name="Inv_def_r" id="1457"
<pr_pos name="Inv_def_r" id="1461"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Inv_def_r"/>
</pr_pos>
<pr_pos name="Comm" id="1460"
<pr_pos name="Comm" id="1464"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CommutativeGroup"/>
<ip_qualid name="Comm"/>
<ip_qualid name="Comm"/>
</pr_pos>
<pr_pos name="Assoc" id="1465"
<pr_pos name="Assoc" id="1469"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Assoc"/>
<ip_qualid name="Assoc"/>
</pr_pos>
<pr_pos name="Mul_distr_l" id="1472"
<pr_pos name="Mul_distr_l" id="1476"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Mul_distr_l"/>
</pr_pos>
<pr_pos name="Mul_distr_r" id="1479"
<pr_pos name="Mul_distr_r" id="1483"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Mul_distr_r"/>
</pr_pos>
<pr_pos name="Comm" id="1497"
<pr_pos name="Comm" id="1501"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Comm"/>
<ip_qualid name="Comm"/>
</pr_pos>
<pr_pos name="Unitary" id="1502"
<pr_pos name="Unitary" id="1506"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Unitary"/>
</pr_pos>
<pr_pos name="NonTrivialRing" id="1505"
<pr_pos name="NonTrivialRing" id="1509"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="NonTrivialRing"/>
</pr_pos>
<pr_pos name="Refl" id="1517"
<pr_pos name="Refl" id="1521"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Refl"/>
</pr_pos>
<pr_pos name="Trans" id="1520"
<pr_pos name="Trans" id="1524"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Trans"/>
</pr_pos>
<pr_pos name="Antisymm" id="1527"
<pr_pos name="Antisymm" id="1531"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Antisymm"/>
</pr_pos>
<pr_pos name="Total" id="1532"
<pr_pos name="Total" id="1536"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="Total"/>
</pr_pos>
<pr_pos name="ZeroLessOne" id="1537"
<pr_pos name="ZeroLessOne" id="1541"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="ZeroLessOne"/>
</pr_pos>
<pr_pos name="CompatOrderAdd" id="1538"
<pr_pos name="CompatOrderAdd" id="1542"
ip_theory="Int">
<ip_library name="int"/>
<ip_qualid name="CompatOrderAdd"/>
</pr_pos>
<pr_pos name="Select_eq" id="3004"
<pr_pos name="Select_eq" id="3007"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="Select_eq"/>
</pr_pos>
<pr_pos name="Select_neq" id="3013"
<pr_pos name="Select_neq" id="3016"
ip_theory="Map">
<ip_library name="map"/>
<ip_qualid name="Select_neq"/>
</pr_pos>
<pr_pos name="length_nonnegative" id="6391"
<pr_pos name="length_nonnegative" id="6394"
ip_theory="Seq">
<ip_library name="seq"/>
<ip_qualid name="length_nonnegative"/>
</pr_pos>
<pr_pos name="empty_length" id="6395"
<pr_pos name="empty_length" id="6398"
ip_theory="Seq">
<ip_library name="seq"/>
<ip_qualid name="empty_length"/>
</pr_pos>
<pr_pos name="set_def1" id="6412"
<pr_pos name="set_def1" id="6415"
ip_theory="Seq">
<ip_library name="seq"/>
<ip_qualid name="set_def1"/>
</pr_pos>
<pr_pos name="set_def2" id="6419"
<pr_pos name="set_def2" id="6422"
ip_theory="Seq">
<ip_library name="seq"/>
<ip_qualid name="set_def2"/>
</pr_pos>
<pr_pos name="set_def3" id="6426"
<pr_pos name="set_def3" id="6429"
ip_theory="Seq">
<ip_library name="seq"/>
<ip_qualid name="set_def3"/>
</pr_pos>
<pr_pos name="extensionality" id="6460"
<pr_pos name="extensionality" id="6463"
ip_theory="Seq">
<ip_library name="seq"/>
<ip_qualid name="extensionality"/>
</pr_pos>
<pr_pos name="cons_length" id="6468"
<pr_pos name="cons_length" id="6471"
ip_theory="Seq">
<ip_library name="seq"/>
<ip_qualid name="cons_length"/>
</pr_pos>
<pr_pos name="cons_get" id="6473"
<pr_pos name="cons_get" id="6476"
ip_theory="Seq">
<ip_library name="seq"/>
<ip_qualid name="cons_get"/>
</pr_pos>
<pr_pos name="snoc_length" id="6483"
<pr_pos name="snoc_length" id="6486"
ip_theory="Seq">
<ip_library name="seq"/>
<ip_qualid name="snoc_length"/>
</pr_pos>
<pr_pos name="create_length" id="6563"
<pr_pos name="create_length" id="6566"
ip_theory="Seq">
<ip_library name="seq"/>
<ip_qualid name="create_length"/>
</pr_pos>
<pr_pos name="create_get" id="6568"
<pr_pos name="create_get" id="6571"
ip_theory="Seq">
<ip_library name="seq"/>
<ip_qualid name="create_get"/>
......@@ -419,160 +419,160 @@
<meta_arg_ls id="15"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="268"/>
<meta_arg_ls id="272"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="269"/>
<meta_arg_ls id="273"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="272"/>
<meta_arg_ls id="276"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="1438"/>
<meta_arg_ls id="1442"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="1439"/>
<meta_arg_ls id="1443"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="1440"/>
<meta_arg_ls id="1444"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="1508"/></