new theory int.Lex2

parent 659ad0f2
......@@ -84,9 +84,7 @@ module KnuthMorrisPratt
lemma next_1_0:
forall p: array char. 1 <= length p -> is_next p 1 0
predicate lt_nat (x y: int) = 0 <= y /\ x < y
clone import relations.Lex with type t1 = int, type t2 = int,
predicate rel1 = lt_nat, predicate rel2 = lt_nat
use import int.Lex2
(* The pattern *)
......
This diff is collapsed.
......@@ -28,10 +28,7 @@ module McCarthy91
axiom iter_f_0: forall x: int. iter_f 0 x = x
axiom iter_f_s: forall k x: int. 0 < k -> iter_f k x = iter_f (k-1) (f x)
predicate lt_nat (x y: int) = 0 <= y /\ x < y
clone import relations.Lex with type t1 = int, type t2 = int,
predicate rel1 = lt_nat, predicate rel2 = lt_nat
use import int.Lex2
let f91_nonrec (n0: int) =
{ }
......
......@@ -17,12 +17,12 @@
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter f91_nonrec" expl="correctness of parameter f91_nonrec" sum="75f22cdba2f4a634d9942900b5b0c525" proved="true" expanded="true">
<goal name="WP_parameter f91_nonrec" expl="correctness of parameter f91_nonrec" sum="fbd734e7f0f402db73a779f18601e0e7" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.64"/>
<result status="valid" time="0.96"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.04"/>
</proof>
</goal>
</theory>
......
......@@ -30,6 +30,17 @@ theory MinMax
end
theory Lex2
use import Int
predicate lt_nat (x y: int) = 0 <= y /\ x < y
clone export relations.Lex with type t1 = int, type t2 = int,
predicate rel1 = lt_nat, predicate rel2 = lt_nat
end
theory EuclideanDivision
use import Int
......
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