Commit eb552e9d authored by MARCHE Claude's avatar MARCHE Claude

LCP continued

parent c6ede020
......@@ -190,6 +190,10 @@ let test1 () =
forall a:array int, x :int.
0 <= x < a.length -> le a x x
lemma le_asym :
forall a:array int, x y:int.
0 <= x < a.length /\ 0 <= y < a.length /\ not (le a x y) -> le a y x
lemma le_trans :
forall a:array int, x y z:int.
0 <= x < a.length /\ 0 <= y < a.length /\
......
This source diff could not be displayed because it is too large. You can view the blob instead.
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