Commit a1cb7615 authored by MARCHE Claude's avatar MARCHE Claude

example prover: porting proofs in progress

parent a7d76365
......@@ -488,6 +488,7 @@ module Impl
requires { bound_depth_of_symbol_in_fo_formula_list t <= i + 1 }
requires { correct_indexes_symbol x }
requires { bound_depth_of_symbol_in_symbol x = 0 }
variant { nlsize_fo_formula_list t }
ensures { correct_indexes_fo_formula_list result }
ensures { bound_depth_of_symbol_in_fo_formula_list result <= i }
ensures { bound_depth_of_fo_term_in_fo_formula_list result =
......@@ -563,6 +564,7 @@ module Impl
requires { correct_indexes_fo_term x }
requires { bound_depth_of_symbol_in_fo_term x = 0 }
requires { bound_depth_of_fo_term_in_fo_term x = 0 }
variant { nlsize_fo_formula_list t }
ensures { correct_indexes_fo_formula_list result }
ensures { bound_depth_of_fo_term_in_fo_formula_list result <= i }
ensures { bound_depth_of_symbol_in_fo_formula_list result =
......@@ -657,6 +659,7 @@ module Impl
requires { correct_indexes_fo_formula_list t }
requires { correct_indexes_symbol u }
requires { bound_depth_of_symbol_in_symbol u = 0 }
variant { nlsize_fo_formula_list t }
ensures { correct_indexes_fo_formula_list result }
ensures { bound_depth_of_symbol_in_fo_formula_list result =
bound_depth_of_symbol_in_fo_formula_list t }
......@@ -732,6 +735,7 @@ module Impl
requires { correct_indexes_fo_term u }
requires { bound_depth_of_symbol_in_fo_term u = 0 }
requires { bound_depth_of_fo_term_in_fo_term u = 0 }
variant { nlsize_fo_formula_list t }
ensures { correct_indexes_fo_formula_list result }
ensures { bound_depth_of_symbol_in_fo_formula_list result =
bound_depth_of_symbol_in_fo_formula_list t }
......@@ -1192,8 +1196,8 @@ module Impl
(const (Var_fo_term (-1)) : int -> (fo_term int int))
identity identity))
(identity) (identity)) ;
let mrv0 = rename_fo_formula mv0 identity identity in
let mrv1 = rename_fo_formula_list mv1 identity identity in
let ghost mrv0 = rename_fo_formula mv0 identity identity in
let ghost mrv1 = rename_fo_formula_list mv1 identity identity in
let resv0 =
{ nlrepr_fo_formula_field = v0 ;
nlfree_var_symbol_set_abstraction_fo_formula_field = fv0 ;
......
......@@ -227,10 +227,10 @@
<proof prover="7"><result status="valid" time="0.10" steps="14"/></proof>
</goal>
<goal name="VC rename_free_var_constructive_inversion_fo_term_fo_formula" expl="VC for rename_free_var_constructive_inversion_fo_term_fo_formula" proved="true">
<proof prover="7"><result status="valid" time="0.33" steps="1221"/></proof>
<proof prover="0"><result status="valid" time="0.26" steps="2163"/></proof>
</goal>
<goal name="VC rename_free_var_inversion_fo_term_fo_formula" expl="VC for rename_free_var_inversion_fo_term_fo_formula" proved="true">
<proof prover="7"><result status="valid" time="0.09" steps="14"/></proof>
<proof prover="3"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="VC rename_free_var_propagation_symbol_fo_formula" expl="VC for rename_free_var_propagation_symbol_fo_formula" proved="true">
<transf name="split_goal_right" proved="true" >
......
......@@ -6,13 +6,15 @@
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../Firstorder_symbol_spec.mlw" proved="true">
<theory name="Spec" proved="true">
<file name="../Firstorder_symbol_spec.mlw">
<theory name="Spec">
<goal name="VC size_positive_lemma_symbol" expl="VC for size_positive_lemma_symbol" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="4"/></proof>
</goal>
<goal name="VC rename_symbol" expl="VC for rename_symbol">
</goal>
<goal name="VC renaming_composition_lemma_symbol" expl="VC for renaming_composition_lemma_symbol" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="1"><result status="valid" time="0.07"/></proof>
......
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
This diff is collapsed.
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