Add ocaml run-time and updates to sail for ocaml backend

42 files changed, 6310 insertions, 0 deletions

diff --git a/lib/ocaml_rts/linksem/src_lem_library/bit.ml b/lib/ocaml_rts/linksem/src_lem_library/bit.ml
new file mode 100644
index 00000000..bd972008
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/bit.ml
@@ -0,0 +1,19 @@
+type bit = Zero | One
+
+let to_bool b = match b with | Zero -> false | _ -> true
+let bn b = match b with | Zero -> One | One -> Zero
+let bor b1 b2 = match (b1,b2) with
+  | Zero,Zero -> Zero
+  | _ -> One
+let xor b1 b2 = match (b1,b2) with
+  | Zero,Zero -> Zero
+  | Zero,One | One,Zero -> One
+  | _ -> Zero
+let band b1 b2 = match (b1,b2) with
+  | One,One -> One
+  | _ -> Zero
+
+let add b1 b2 = match (b1,b2) with
+  | Zero,Zero -> Zero, false
+  | Zero,One | One,Zero -> One, false
+  | One,One -> Zero, true
diff --git a/lib/ocaml_rts/linksem/src_lem_library/bit.mli b/lib/ocaml_rts/linksem/src_lem_library/bit.mli
new file mode 100644
index 00000000..a39c1a09
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/bit.mli
@@ -0,0 +1,8 @@
+type bit = Zero | One
+
+val to_bool : bit -> bool
+val bn : bit -> bit
+val bor : bit -> bit -> bit
+val xor : bit -> bit -> bit
+val band : bit -> bit -> bit
+val add : bit -> bit -> bit * bool
diff --git a/lib/ocaml_rts/linksem/src_lem_library/either.ml b/lib/ocaml_rts/linksem/src_lem_library/either.ml
new file mode 100644
index 00000000..ddf1b214
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/either.ml
@@ -0,0 +1,24 @@
+type ('a, 'b) either = 
+  | Left of 'a
+  | Right of 'b
+
+let either_case fa fb x = match x with
+  | (Left a) -> fa a
+  | (Right b) -> fb b
+
+let eitherEqualBy eql eqr (left: ('a, 'b) either) (right: ('a, 'b) either) =  
+  match (left, right) with
+    | ((Left l), (Left l')) -> eql l l'
+    | ((Right r), (Right r')) -> eqr r r'
+    | _ -> false
+  
+let rec either_partition l = ((match l with
+  | [] -> ([], [])
+  | x :: xs -> begin
+      let (ll, rl) = (either_partition xs) in
+      (match x with 
+        | (Left l) -> ((l::ll), rl)
+        | (Right r) -> (ll, (r::rl))
+      )
+    end
+))
diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem.ml b/lib/ocaml_rts/linksem/src_lem_library/lem.ml
new file mode 100644
index 00000000..2ff0090f
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/lem.ml
@@ -0,0 +1,103 @@
+(* ========================================================================== *)
+(* Tuples                                                                     *)
+(* ========================================================================== *)
+
+
+let pair_equal eq1 eq2 (a1, b1) (a2, b2) =
+  (eq1 a1 a2) && (eq2 b1 b2)
+
+let pair_swap (v1, v2) = (v2, v1)
+
+let curry f v1 v2 = f (v1, v2)
+
+let uncurry f (v1, v2) = f v1 v2
+
+(* ========================================================================== *)
+(* Orderings                                                                  *)
+(* ========================================================================== *)
+
+let orderingIsLess r = (r < 0)
+let orderingIsGreater r = (r > 0)
+let orderingIsEqual r = (r = 0)
+
+let ordering_cases (r : int) (lt : 'a) (eq : 'a) (gt : 'a) : 'a =  
+  (if (r < 0) then lt else
+   if (r = 0) then eq else gt)
+
+let orderingEqual r1 r2 = 
+  ordering_cases r1 (orderingIsLess r2) (orderingIsEqual r2) (orderingIsGreater r2)
+
+
+(* ========================================================================== *)
+(* Lists                                                                      *)
+(* ========================================================================== *)
+
+
+let list_null = function
+  | [] -> true
+  | _ -> false
+
+let rec lexicographic_compare cmp l1 l2 : int = (match (l1,l2) with
+  | ([], []) -> 0
+  | ([], _::_) -> -1
+  | (_::_, []) -> 1
+  | (x::xs, y::ys) -> begin  
+       ordering_cases (cmp x y) (-1) (lexicographic_compare cmp xs ys) (1)
+    end
+)
+
+let rec lexicographic_less less less_eq l1 l2 = ((match (l1,l2) with
+  | ([], []) -> false
+  | ([], _::_) -> true
+  | (_::_, []) -> false
+  | (x::xs, y::ys) -> ((less x y) || ((less_eq x y) && (lexicographic_less less less_eq xs ys)))
+))
+
+let rec lexicographic_less_eq less less_eq l1 l2 = ((match (l1,l2) with
+  | ([], []) -> true
+  | ([], _::_) -> true
+  | (_::_, []) -> false
+  | (x::xs, y::ys) -> (less x y || (less_eq x y && lexicographic_less_eq less less_eq xs ys))
+))
+
+let rec list_index l n = (match l with 
+  | []      -> None
+  | x :: xs -> if n = 0 then (Some x) else list_index xs (n - 1)
+)
+
+
+(* ========================================================================== *)
+(* Options                                                                    *)
+(* ========================================================================== *)
+
+let is_none = function
+  | None -> true
+  | Some _ -> false
+
+let is_some = function
+  | None -> false
+  | Some _ -> true
+
+let option_case d f mb = (match mb with 
+  | Some a -> f a
+  | None   -> d
+)
+
+let option_default d = function
+  | Some a -> a
+  | None   -> d
+
+let option_map f = function
+  | Some a -> Some (f a)
+  | None   -> None
+
+let option_bind m f =
+  match m with
+    | Some a -> f a
+    | None   -> None
+
+let option_equal eq o1 o2 = match (o1, o2) with
+  | (None, None)       -> true
+  | (None, Some _)     -> false
+  | (Some _,  None)    -> false
+  | (Some x1, Some x2) -> eq x1 x2
diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_assert_extra.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_assert_extra.ml
new file mode 100644
index 00000000..3b4a1548
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/lem_assert_extra.ml
@@ -0,0 +1,28 @@
+(*Generated by Lem from assert_extra.lem.*)
+
+open Xstring
+
+(* ------------------------------------ *)
+(* failing with a proper error message  *)
+(* ------------------------------------ *)
+
+(*val failwith: forall 'a. string -> 'a*)
+
+(* ------------------------------------ *)
+(* failing without an error message     *)
+(* ------------------------------------ *)
+
+(*val fail : forall 'a. 'a*)
+(*let fail = failwith "fail"*)
+
+(* ------------------------------------- *)
+(* assertions                            *)
+(* ------------------------------------- *)
+
+(*val ensure : bool -> string -> unit*)
+let ensure test msg =  
+(if test then
+    ()
+  else
+    failwith msg)
+;;
diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_basic_classes.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_basic_classes.ml
new file mode 100644
index 00000000..9f24e5fb
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/lem_basic_classes.ml
@@ -0,0 +1,323 @@
+(*Generated by Lem from basic_classes.lem.*)
+(******************************************************************************)
+(* Basic Type Classes                                                         *)
+(******************************************************************************)
+
+open Lem_bool
+
+(* ========================================================================== *)
+(* Equality                                                                   *)
+(* ========================================================================== *)
+
+(* Lem`s default equality (=) is defined by the following type-class Eq.
+   This typeclass should define equality on an abstract datatype 'a. It should
+   always coincide with the default equality of Coq, HOL and Isabelle.
+   For OCaml, it might be different, since abstract datatypes like sets
+   might have fancy equalities. *)
+
+type 'a eq_class= { 
+  isEqual_method : 'a -> 'a -> bool;
+  isInequal_method : 'a -> 'a -> bool
+}
+
+
+(* (=) should for all instances be an equivalence relation 
+   The isEquivalence predicate of relations could be used here.
+   However, this would lead to a cyclic dependency. *)
+
+(* TODO: add later, once lemmata can be assigned to classes 
+lemma eq_equiv: ((forall x. (x = x)) &&
+                 (forall x y. (x = y) <-> (y = x)) &&
+                 (forall x y z. ((x = y) && (y = z)) --> (x = z)))
+*)
+
+(* Structural equality *)
+
+(* Sometimes, it is also handy to be able to use structural equality.
+   This equality is mapped to the build-in equality of backends. This equality
+   differs significantly for each backend. For example, OCaml can`t check equality
+   of function types, whereas HOL can.  When using structural equality, one should 
+   know what one is doing. The only guarentee is that is behaves like 
+   the native backend equality.
+
+   A lengthy name for structural equality is used to discourage its direct use.
+   It also ensures that users realise it is unsafe (e.g. OCaml can`t check two functions
+   for equality *)
+(*val unsafe_structural_equality : forall 'a. 'a -> 'a -> bool*)
+
+(*val unsafe_structural_inequality : forall 'a. 'a -> 'a -> bool*)
+let unsafe_structural_inequality x y = (not (x = y))
+
+(* The default for equality is the unsafe structural one. It can 
+   (and should) be overriden for concrete types later. *)
+
+let instance_Basic_classes_Eq_var_dict =({
+
+  isEqual_method = (=);
+
+  isInequal_method = unsafe_structural_inequality})
+
+
+(* ========================================================================== *)
+(* Orderings                                                                  *)
+(* ========================================================================== *)
+
+(* The type-class Ord represents total orders (also called linear orders) *)
+(*type ordering = LT | EQ | GT*)
+
+(*let orderingIsLess r       = (match r with LT -> true | _ -> false end)*)
+(*let orderingIsGreater r    = (match r with GT -> true | _ -> false end)*)
+(*let orderingIsEqual r      = (match r with EQ -> true | _ -> false end)*)
+
+(*let ordering_cases r lt eq gt =
+  if orderingIsLess r then lt else
+  if orderingIsEqual r then eq else gt*)
+
+
+(*val orderingEqual : ordering -> ordering -> bool*)
+
+let instance_Basic_classes_Eq_Basic_classes_ordering_dict =({
+
+  isEqual_method = Lem.orderingEqual;
+
+  isInequal_method = (fun x y->not (Lem.orderingEqual x y))})
+
+type 'a ord_class= { 
+  compare_method                 : 'a -> 'a -> int;
+  isLess_method         : 'a -> 'a -> bool;
+  isLessEqual_method    : 'a -> 'a -> bool;
+  isGreater_method      : 'a -> 'a -> bool;
+  isGreaterEqual_method : 'a -> 'a -> bool 
+}
+
+
+(* Ocaml provides default, polymorphic compare functions. Let's use them
+   as the default. However, because used perhaps in a typeclass they must be 
+   defined for all targets. So, explicitly declare them as undefined for
+   all other targets. If explictly declare undefined, the type-checker won't complain and
+   an error will only be raised when trying to actually output the function for a certain
+   target. *)
+(*val defaultCompare   : forall 'a. 'a -> 'a -> ordering*)
+(*val defaultLess      : forall 'a. 'a -> 'a -> bool*)
+(*val defaultLessEq    : forall 'a. 'a -> 'a -> bool*)
+(*val defaultGreater   : forall 'a. 'a -> 'a -> bool*)
+(*val defaultGreaterEq : forall 'a. 'a -> 'a -> bool*) 
+;;
+
+let genericCompare (less: 'a -> 'a -> bool) (equal: 'a -> 'a -> bool) (x : 'a) (y : 'a) =  
+(if less x y then
+    (-1)
+  else if equal x y then
+    0
+  else
+    1)
+
+
+(*
+(* compare should really be a total order *)
+lemma ord_OK_1: (
+  (forall x y. (compare x y = EQ) <-> (compare y x = EQ)) &&
+  (forall x y. (compare x y = LT) <-> (compare y x = GT)))
+
+lemma ord_OK_2: (
+  (forall x y z. (x <= y) && (y <= z) --> (x <= z)) &&
+  (forall x y. (x <= y) || (y <= x))
+)
+*)
+
+(* let's derive a compare function from the Ord type-class *)
+(*val ordCompare : forall 'a. Eq 'a, Ord 'a => 'a -> 'a -> ordering*)
+let ordCompare dict_Basic_classes_Eq_a dict_Basic_classes_Ord_a x y =  
+(if ( dict_Basic_classes_Ord_a.isLess_method x y) then (-1) else
+  if ( dict_Basic_classes_Eq_a.isEqual_method x y) then 0 else 1)
+
+type 'a ordMaxMin_class= { 
+  max_method : 'a -> 'a -> 'a;
+  min_method : 'a -> 'a -> 'a
+}
+
+(*val minByLessEqual : forall 'a. ('a -> 'a -> bool) -> 'a -> 'a -> 'a*)
+let minByLessEqual le x y = (if (le x y) then x else y)
+
+(*val maxByLessEqual : forall 'a. ('a -> 'a -> bool) -> 'a -> 'a -> 'a*)
+let maxByLessEqual le x y = (if (le y x) then x else y)
+
+(*val defaultMax : forall 'a. Ord 'a => 'a -> 'a -> 'a*)
+
+(*val defaultMin : forall 'a. Ord 'a => 'a -> 'a -> 'a*)
+
+let instance_Basic_classes_OrdMaxMin_var_dict dict_Basic_classes_Ord_a =({
+
+  max_method = max;
+
+  min_method = min})
+
+
+(* ========================================================================== *)
+(* SetTypes                                                                   *)
+(* ========================================================================== *)
+
+(* Set implementations use often an order on the elements. This allows the OCaml implementation
+   to use trees for implementing them. At least, one needs to be able to check equality on sets.
+   One could use the Ord type-class for sets. However, defining a special typeclass is cleaner
+   and allows more flexibility. One can make e.g. sure, that this type-class is ignored for
+   backends like HOL or Isabelle, which don't need it. Moreover, one is not forced to also instantiate
+   the functions "<", "<=" ... *)
+
+type 'a setType_class= { 
+  setElemCompare_method : 'a -> 'a -> int
+}
+
+let instance_Basic_classes_SetType_var_dict =({
+
+  setElemCompare_method = compare})
+
+(* ========================================================================== *)
+(* Instantiations                                                             *)
+(* ========================================================================== *)
+
+let instance_Basic_classes_Eq_bool_dict =({
+
+  isEqual_method = (=);
+
+  isInequal_method = (fun x y->not ((=) x y))})
+
+let boolCompare b1 b2 = ((match (b1, b2) with
+  | (true, true) -> 0
+  | (true, false) -> 1
+  | (false, true) -> (-1)
+  | (false, false) -> 0
+))
+
+let instance_Basic_classes_SetType_bool_dict =({
+
+  setElemCompare_method = boolCompare})
+
+(* strings *)
+
+(*val charEqual : char -> char -> bool*)
+
+let instance_Basic_classes_Eq_char_dict =({
+
+  isEqual_method = (=);
+
+  isInequal_method = (fun left right->not (left = right))})
+
+(*val stringEquality : string -> string -> bool*)
+
+let instance_Basic_classes_Eq_string_dict =({
+
+  isEqual_method = (=);
+
+  isInequal_method = (fun l r->not (l = r))})
+
+(* pairs *)
+
+(*val pairEqual : forall 'a 'b. Eq 'a, Eq 'b => ('a * 'b) -> ('a * 'b) -> bool*)
+(*let pairEqual (a1, b1) (a2, b2) = ( 
+  dict_Basic_classes_Eq_a.isEqual_method a1 a2) && ( dict_Basic_classes_Eq_b.isEqual_method b1 b2)*)
+
+(*val pairEqualBy : forall 'a 'b. ('a -> 'a -> bool) -> ('b -> 'b -> bool) -> ('a * 'b) -> ('a * 'b) -> bool*)
+
+let instance_Basic_classes_Eq_tup2_dict dict_Basic_classes_Eq_a dict_Basic_classes_Eq_b =({
+
+  isEqual_method = (Lem.pair_equal  
+  dict_Basic_classes_Eq_a.isEqual_method  dict_Basic_classes_Eq_b.isEqual_method);
+
+  isInequal_method = (fun x y->not ((Lem.pair_equal  
+  dict_Basic_classes_Eq_a.isEqual_method  dict_Basic_classes_Eq_b.isEqual_method x y)))})
+
+(*val pairCompare : forall 'a 'b. ('a -> 'a -> ordering) -> ('b -> 'b -> ordering) -> ('a * 'b) -> ('a * 'b) -> ordering*)
+let pairCompare cmpa cmpb (a1, b1) (a2, b2) = 
+  (Lem.ordering_cases (cmpa a1 a2) (-1) (cmpb b1 b2) 1)
+
+let pairLess dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b (x1, x2) (y1, y2) = (( 
+  dict_Basic_classes_Ord_b.isLess_method x1 y1) || (( dict_Basic_classes_Ord_b.isLessEqual_method x1 y1) && ( dict_Basic_classes_Ord_a.isLess_method x2 y2)))
+let pairLessEq dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b (x1, x2) (y1, y2) = (( 
+  dict_Basic_classes_Ord_b.isLess_method x1 y1) || (( dict_Basic_classes_Ord_b.isLessEqual_method x1 y1) && ( dict_Basic_classes_Ord_a.isLessEqual_method x2 y2)))
+
+let pairGreater dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b x12 y12 = (pairLess 
+  dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y12 x12)
+let pairGreaterEq dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b x12 y12 = (pairLessEq 
+  dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y12 x12)
+
+let instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b =({
+
+  compare_method = (pairCompare  
+  dict_Basic_classes_Ord_a.compare_method  dict_Basic_classes_Ord_b.compare_method);
+
+  isLess_method = 
+  (pairLess dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a);
+
+  isLessEqual_method = 
+  (pairLessEq dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a);
+
+  isGreater_method = 
+  (pairGreater dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b);
+
+  isGreaterEqual_method = 
+  (pairGreaterEq dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b)})
+
+let instance_Basic_classes_SetType_tup2_dict dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b =({
+
+  setElemCompare_method = (pairCompare  
+  dict_Basic_classes_SetType_a.setElemCompare_method  dict_Basic_classes_SetType_b.setElemCompare_method)})
+
+
+(* triples *)
+
+(*val tripleEqual : forall 'a 'b 'c. Eq 'a, Eq 'b, Eq 'c => ('a * 'b * 'c) -> ('a * 'b * 'c) -> bool*)
+let tripleEqual dict_Basic_classes_Eq_a dict_Basic_classes_Eq_b dict_Basic_classes_Eq_c (x1, x2, x3) (y1, y2, y3) = ( (Lem.pair_equal  
+  dict_Basic_classes_Eq_a.isEqual_method (Lem.pair_equal  dict_Basic_classes_Eq_b.isEqual_method  dict_Basic_classes_Eq_c.isEqual_method)(x1, (x2, x3)) (y1, (y2, y3))))
+
+let instance_Basic_classes_Eq_tup3_dict dict_Basic_classes_Eq_a dict_Basic_classes_Eq_b dict_Basic_classes_Eq_c =({
+
+  isEqual_method = 
+  (tripleEqual dict_Basic_classes_Eq_a dict_Basic_classes_Eq_b
+     dict_Basic_classes_Eq_c);
+
+  isInequal_method = (fun x y->not (tripleEqual 
+  dict_Basic_classes_Eq_a dict_Basic_classes_Eq_b dict_Basic_classes_Eq_c x y))})
+
+(*val tripleCompare : forall 'a 'b 'c. ('a -> 'a -> ordering) -> ('b -> 'b -> ordering) -> ('c -> 'c -> ordering) -> ('a * 'b * 'c) -> ('a * 'b * 'c) -> ordering*)
+let tripleCompare cmpa cmpb cmpc (a1, b1, c1) (a2, b2, c2) =  
+(pairCompare cmpa (pairCompare cmpb cmpc) (a1, (b1, c1)) (a2, (b2, c2)))
+
+let tripleLess dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c (x1, x2, x3) (y1, y2, y3) = (pairLess 
+  (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_b
+     dict_Basic_classes_Ord_c) dict_Basic_classes_Ord_a (x1, (x2, x3)) (y1, (y2, y3)))
+let tripleLessEq dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c (x1, x2, x3) (y1, y2, y3) = (pairLessEq 
+  (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_b
+     dict_Basic_classes_Ord_c) dict_Basic_classes_Ord_a (x1, (x2, x3)) (y1, (y2, y3)))
+
+let tripleGreater dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c x123 y123 = (tripleLess 
+  dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y123 x123)
+let tripleGreaterEq dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c x123 y123 = (tripleLessEq 
+  dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y123 x123)
+
+let instance_Basic_classes_Ord_tup3_dict dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c =({
+
+  compare_method = (tripleCompare  
+  dict_Basic_classes_Ord_a.compare_method  dict_Basic_classes_Ord_b.compare_method  dict_Basic_classes_Ord_c.compare_method);
+
+  isLess_method = 
+  (tripleLess dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b
+     dict_Basic_classes_Ord_c);
+
+  isLessEqual_method = 
+  (tripleLessEq dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b
+     dict_Basic_classes_Ord_c);
+
+  isGreater_method = 
+  (tripleGreater dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b
+     dict_Basic_classes_Ord_a);
+
+  isGreaterEqual_method = 
+  (tripleGreaterEq dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b
+     dict_Basic_classes_Ord_a)})
+
+let instance_Basic_classes_SetType_tup3_dict dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b dict_Basic_classes_SetType_c =({
+
+  setElemCompare_method = (tripleCompare  
+  dict_Basic_classes_SetType_a.setElemCompare_method  dict_Basic_classes_SetType_b.setElemCompare_method  dict_Basic_classes_SetType_c.setElemCompare_method)})
+
diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_bool.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_bool.ml
new file mode 100644
index 00000000..9b6eb0f6
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/lem_bool.ml
@@ -0,0 +1,66 @@
+(*Generated by Lem from bool.lem.*)
+ 
+
+(* The type bool is hard-coded, so are true and false *)
+
+(* ----------------------- *)
+(* not                     *)
+(* ----------------------- *)
+
+(*val not : bool -> bool*)
+(*let not b = match b with
+  | true -> false
+  | false -> true
+end*)
+
+(* ----------------------- *)
+(* and                     *)
+(* ----------------------- *)
+
+(*val && [and] : bool -> bool -> bool*)
+(*let && b1 b2 = match (b1, b2) with
+  | (true, true) -> true
+  | _ -> false
+end*)
+
+
+(* ----------------------- *)
+(* or                      *)
+(* ----------------------- *)
+
+(*val || [or] : bool -> bool -> bool*)
+(*let || b1 b2 = match (b1, b2) with
+  | (false, false) -> false
+  | _ -> true
+end*)
+
+
+(* ----------------------- *)
+(* implication             *)
+(* ----------------------- *)
+
+(*val --> [imp] : bool -> bool -> bool*)
+(*let --> b1 b2 = match (b1, b2) with
+  | (true, false) -> false
+  | _ -> true
+end*)
+
+
+(* ----------------------- *)
+(* equivalence             *)
+(* ----------------------- *)
+
+(*val <-> [equiv] : bool -> bool -> bool*)
+(*let <-> b1 b2 = match (b1, b2) with
+  | (true, true) -> true
+  | (false, false) -> true
+  | _ -> false
+end*)
+
+
+(* ----------------------- *)
+(* xor                     *)
+(* ----------------------- *)
+
+(*val xor : bool -> bool -> bool*)
+
diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_either.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_either.ml
new file mode 100644
index 00000000..9f1b4ad8
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/lem_either.ml
@@ -0,0 +1,87 @@
+(*Generated by Lem from either.lem.*)
+ 
+
+open Lem_bool
+open Lem_basic_classes
+open Lem_list
+open Lem_tuple
+open Either
+
+(*type either 'a 'b
+  = Left  of 'a
+  | Right of 'b*)
+
+
+(* -------------------------------------------------------------------------- *)
+(* Equality.                                                                  *)
+(* -------------------------------------------------------------------------- *)
+
+(*val eitherEqual : forall 'a 'b. Eq 'a, Eq 'b => (either 'a 'b) -> (either 'a 'b) -> bool*)
+(*val eitherEqualBy : forall 'a 'b. ('a -> 'a -> bool) -> ('b -> 'b -> bool) -> (either 'a 'b) -> (either 'a 'b) -> bool*)
+
+(*let eitherEqualBy eql eqr (left: either 'a 'b) (right: either 'a 'b) =
+  match (left, right) with
+    | (Left l, Left l') -> eql l l'
+    | (Right r, Right r') -> eqr r r'
+    | _ -> false
+  end*)
+(*let eitherEqual = eitherEqualBy  
+  dict_Basic_classes_Eq_a.isEqual_method  dict_Basic_classes_Eq_b.isEqual_method*)
+
+let instance_Basic_classes_Eq_Either_either_dict dict_Basic_classes_Eq_a dict_Basic_classes_Eq_b =({
+
+  isEqual_method = (Either.eitherEqualBy  
+  dict_Basic_classes_Eq_a.isEqual_method  dict_Basic_classes_Eq_b.isEqual_method);
+
+  isInequal_method = (fun x y->not ((Either.eitherEqualBy  
+  dict_Basic_classes_Eq_a.isEqual_method  dict_Basic_classes_Eq_b.isEqual_method x y)))})
+
+let either_setElemCompare cmpa cmpb x y =  
+((match (x, y) with
+    | (Either.Left x', Either.Left y') -> cmpa x' y'
+    | (Either.Right x', Either.Right y') -> cmpb x' y'
+    | (Either.Left _, Either.Right _) -> (-1)
+    | (Either.Right _, Either.Left _) -> 1
+  ))
+
+let instance_Basic_classes_SetType_Either_either_dict dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b =({
+
+  setElemCompare_method = (fun x y->either_setElemCompare  
+  dict_Basic_classes_SetType_a.setElemCompare_method  dict_Basic_classes_SetType_b.setElemCompare_method x y)})
+                           
+
+(* -------------------------------------------------------------------------- *)
+(* Utility functions.                                                         *)
+(* -------------------------------------------------------------------------- *)
+
+(*val isLeft : forall 'a 'b. either 'a 'b -> bool*)
+
+(*val isRight : forall 'a 'b. either 'a 'b -> bool*)
+
+
+(*val either : forall 'a 'b 'c. ('a -> 'c) -> ('b -> 'c) -> either 'a 'b -> 'c*)
+(*let either fa fb x = match x with
+  | Left a -> fa a
+  | Right b -> fb b
+end*)
+
+
+(*val partitionEither : forall 'a 'b. list (either 'a 'b) -> (list 'a * list 'b)*)
+(*let rec partitionEither l = match l with
+  | [] -> ([], [])
+  | x :: xs -> begin
+      let (ll, rl) = partitionEither xs in
+      match x with 
+        | Left l -> (l::ll, rl)
+        | Right r -> (ll, r::rl)
+      end
+    end
+end*)
+
+
+(*val lefts : forall 'a 'b. list (either 'a 'b) -> list 'a*)
+
+
+(*val rights : forall 'a 'b. list (either 'a 'b) -> list 'b*)
+
+
diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_function.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_function.ml
new file mode 100644
index 00000000..677adc4c
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/lem_function.ml
@@ -0,0 +1,53 @@
+(*Generated by Lem from function.lem.*)
+(******************************************************************************)
+(* A library for common operations on functions                               *)
+(******************************************************************************)
+
+open Lem_bool
+open Lem_basic_classes
+
+(* ----------------------- *)
+(* identity function       *)
+(* ----------------------- *)
+
+(*val id : forall 'a. 'a -> 'a*)
+let id x = x
+
+
+(* ----------------------- *)
+(* constant function       *)
+(* ----------------------- *)
+
+(*val const : forall 'a 'b. 'a -> 'b -> 'a*)
+
+
+(* ----------------------- *)
+(* function composition    *)
+(* ----------------------- *)
+
+(*val comb : forall 'a 'b 'c. ('b -> 'c) -> ('a -> 'b) -> ('a -> 'c)*)
+let comb f g = (fun x -> f (g x))
+
+
+(* ----------------------- *)
+(* function application    *)
+(* ----------------------- *)
+
+(*val $ [apply] : forall 'a 'b. ('a -> 'b) -> ('a -> 'b)*)
+(*let $ f = (fun x -> f x)*)
+
+(* ----------------------- *)
+(* flipping argument order *)
+(* ----------------------- *)
+
+(*val flip : forall 'a 'b 'c. ('a -> 'b -> 'c) -> ('b -> 'a -> 'c)*)
+let flip f = (fun x y -> f y x)
+
+
+(* currying / uncurrying *)
+
+(*val curry : forall 'a 'b 'c. (('a * 'b) -> 'c) -> 'a -> 'b -> 'c*)
+let curry f = (fun a b -> f (a, b))
+
+(*val uncurry : forall 'a 'b 'c. ('a -> 'b -> 'c) -> ('a * 'b -> 'c)*)
+let uncurry f (a,b) = (f a b)
diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_function_extra.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_function_extra.ml
new file mode 100644
index 00000000..3c9e7854
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/lem_function_extra.ml
@@ -0,0 +1,15 @@
+(*Generated by Lem from function_extra.lem.*)
+
+
+open Lem_maybe
+open Lem_bool
+open Lem_basic_classes
+open Lem_num
+open Lem_function
+
+(* ----------------------- *)
+(* getting a unique value  *)
+(* ----------------------- *)
+
+(*val THE : forall 'a. ('a -> bool) -> maybe 'a*)
+
diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_list.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_list.ml
new file mode 100644
index 00000000..be308d6e
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/lem_list.ml
@@ -0,0 +1,722 @@
+(*Generated by Lem from list.lem.*)
+ 
+
+open Lem_bool
+open Lem_maybe
+open Lem_basic_classes
+open Lem_tuple
+open Lem_num
+
+(* ========================================================================== *)
+(* Basic list functions                                                       *)
+(* ========================================================================== *)
+
+(* The type of lists as well as list literals like [], [1;2], ... are hardcoded. 
+   Thus, we can directly dive into derived definitions. *)
+
+
+(* ----------------------- *)
+(* cons                    *)
+(* ----------------------- *)
+
+(*val :: : forall 'a. 'a -> list 'a -> list 'a*)
+
+
+(* ----------------------- *)
+(* Emptyness check         *)
+(* ----------------------- *)
+
+(*val null : forall 'a. list 'a -> bool*)
+let list_null l = ((match l with [] -> true | _ -> false ))
+
+(* ----------------------- *)
+(* Length                  *)
+(* ----------------------- *)
+
+(*val length : forall 'a. list 'a -> nat*)
+(*let rec length l =
+  match l with
+    | [] -> 0
+    | x :: xs -> (Instance_Num_NumAdd_nat.+) (length xs) 1
+  end*)
+
+(* ----------------------- *)
+(* Equality                *)
+(* ----------------------- *)
+
+(*val listEqual : forall 'a. Eq 'a => list 'a -> list 'a -> bool*)
+(*val listEqualBy : forall 'a. ('a -> 'a -> bool) -> list 'a -> list 'a -> bool*)
+
+let rec listEqualBy eq l1 l2 = ((match (l1,l2) with
+  | ([], []) -> true
+  | ([], (_::_)) -> false
+  | ((_::_), []) -> false
+  | (x::xs, y :: ys) -> (eq x y && listEqualBy eq xs ys)
+))
+
+let instance_Basic_classes_Eq_list_dict dict_Basic_classes_Eq_a =({
+
+  isEqual_method = (listEqualBy  
+  dict_Basic_classes_Eq_a.isEqual_method);
+
+  isInequal_method = (fun l1 l2->not ((listEqualBy  
+  dict_Basic_classes_Eq_a.isEqual_method l1 l2)))})
+
+
+(* ----------------------- *)
+(* compare                 *)
+(* ----------------------- *)
+
+(*val lexicographicCompare : forall 'a. Ord 'a => list 'a -> list 'a -> ordering*)
+(*val lexicographicCompareBy : forall 'a. ('a -> 'a -> ordering) -> list 'a -> list 'a -> ordering*)
+
+let rec lexicographic_compare cmp l1 l2 = ((match (l1,l2) with
+  | ([], []) -> 0
+  | ([], _::_) -> (-1)
+  | (_::_, []) -> 1
+  | (x::xs, y::ys) -> begin  
+  Lem.ordering_cases (cmp x y) (-1) (lexicographic_compare cmp xs ys) 1
+    end
+))
+
+(*val lexicographicLess : forall 'a. Ord 'a => list 'a -> list 'a -> bool*)
+(*val lexicographicLessBy : forall 'a. ('a -> 'a -> bool) -> ('a -> 'a -> bool) -> list 'a -> list 'a -> bool*)
+let rec lexicographic_less less less_eq l1 l2 = ((match (l1,l2) with
+  | ([], []) -> false
+  | ([], _::_) -> true
+  | (_::_, []) -> false
+  | (x::xs, y::ys) -> ((less x y) || ((less_eq x y) && (lexicographic_less less less_eq xs ys)))
+))
+
+(*val lexicographicLessEq : forall 'a. Ord 'a => list 'a -> list 'a -> bool*)
+(*val lexicographicLessEqBy : forall 'a. ('a -> 'a -> bool) -> ('a -> 'a -> bool) -> list 'a -> list 'a -> bool*)
+let rec lexicographic_less_eq less less_eq l1 l2 = ((match (l1,l2) with
+  | ([], []) -> true
+  | ([], _::_) -> true
+  | (_::_, []) -> false
+  | (x::xs, y::ys) -> (less x y || (less_eq x y && lexicographic_less_eq less less_eq xs ys))
+))
+
+
+let instance_Basic_classes_Ord_list_dict dict_Basic_classes_Ord_a =({
+
+  compare_method = (lexicographic_compare  
+  dict_Basic_classes_Ord_a.compare_method);
+
+  isLess_method = (lexicographic_less  
+  dict_Basic_classes_Ord_a.isLess_method  dict_Basic_classes_Ord_a.isLessEqual_method);
+
+  isLessEqual_method = (lexicographic_less_eq  
+  dict_Basic_classes_Ord_a.isLess_method  dict_Basic_classes_Ord_a.isLessEqual_method);
+
+  isGreater_method = (fun x y->(lexicographic_less  
+  dict_Basic_classes_Ord_a.isLess_method  dict_Basic_classes_Ord_a.isLessEqual_method y x));
+
+  isGreaterEqual_method = (fun x y->(lexicographic_less_eq  
+  dict_Basic_classes_Ord_a.isLess_method  dict_Basic_classes_Ord_a.isLessEqual_method y x))})
+
+
+(* ----------------------- *)
+(* Append                  *)
+(* ----------------------- *)
+
+(*val ++ : forall 'a. list 'a -> list 'a -> list 'a*) (* originally append *)
+(*let rec ++ xs ys = match xs with
+                     | [] -> ys
+                     | x :: xs' -> x :: (xs' ++ ys)
+                   end*)
+
+(* ----------------------- *)
+(* snoc                    *)
+(* ----------------------- *)
+
+(*val snoc : forall 'a. 'a -> list 'a -> list 'a*)
+let snoc e l =  (List.append l [e])
+
+
+(* ----------------------- *)
+(* Map                     *)
+(* ----------------------- *)
+
+(*val map : forall 'a 'b. ('a -> 'b) -> list 'a -> list 'b*)
+(*let rec map f l = match l with
+  | [] -> []
+  | x :: xs -> (f x) :: map f xs
+end*)
+
+(* ----------------------- *)
+(* Reverse                 *)
+(* ----------------------- *)
+
+(* First lets define the function [reverse_append], which is
+   closely related to reverse. [reverse_append l1 l2] appends the list [l2] to the reverse of [l1].
+   This can be implemented more efficienctly than appending and is
+   used to implement reverse. *)
+
+(*val reverseAppend : forall 'a. list 'a -> list 'a -> list 'a*) (* originally named rev_append *)
+(*let rec reverseAppend l1 l2 = match l1 with 
+                                | [] -> l2
+                                | x :: xs -> reverseAppend xs (x :: l2)
+                               end*)
+
+(* Reversing a list *)
+(*val reverse : forall 'a. list 'a -> list 'a*) (* originally named rev *)
+(*let reverse l = reverseAppend l []*)
+
+
+(* ----------------------- *)
+(* Reverse Map             *)
+(* ----------------------- *)
+
+(*val reverseMap : forall 'a 'b. ('a -> 'b) -> list 'a -> list 'b*)
+
+
+
+(* ========================================================================== *)
+(* Folding                                                                    *)
+(* ========================================================================== *)
+
+(* ----------------------- *)
+(* fold left               *)
+(* ----------------------- *)
+
+(*val foldl : forall 'a 'b. ('a -> 'b -> 'a) -> 'a -> list 'b -> 'a*) (* originally foldl *)
+
+(*let rec foldl f b l = match l with
+  | []      -> b
+  | x :: xs -> foldl f (f b x) xs
+end*)
+
+
+(* ----------------------- *)
+(* fold right              *)
+(* ----------------------- *)
+
+(*val foldr : forall 'a 'b. ('a -> 'b -> 'b) -> 'b -> list 'a -> 'b*) (* originally foldr with different argument order *)
+(*let rec foldr f b l = match l with
+  | []      -> b
+  | x :: xs -> f x (foldr f b xs)
+end*)
+
+
+(* ----------------------- *)
+(* concatenating lists     *)
+(* ----------------------- *)
+
+(*val concat : forall 'a. list (list 'a) -> list 'a*) (* before also called "flatten" *)
+(*let concat = foldr (++) []*)
+
+
+(* -------------------------- *)
+(* concatenating with mapping *)
+(* -------------------------- *)
+
+(*val concatMap : forall 'a 'b. ('a -> list 'b) -> list 'a -> list 'b*)
+
+
+(* ------------------------- *)
+(* universal qualification   *)
+(* ------------------------- *)
+
+(*val all : forall 'a. ('a -> bool) -> list 'a -> bool*) (* originally for_all *)
+(*let all P l = foldl (fun r e -> P e && r) true l*)
+
+
+
+(* ------------------------- *)
+(* existential qualification *)
+(* ------------------------- *)
+
+(*val any : forall 'a. ('a -> bool) -> list 'a -> bool*) (* originally exist *)
+(*let any P l = foldl (fun r e -> P e || r) false l*)
+
+
+(* ------------------------- *)
+(* dest_init                 *)
+(* ------------------------- *)
+
+(* get the initial part and the last element of the list in a safe way *)
+
+(*val dest_init : forall 'a. list 'a -> maybe (list 'a * 'a)*) 
+
+let rec dest_init_aux rev_init last_elem_seen to_process =  
+((match to_process with
+    | []    -> (List.rev rev_init, last_elem_seen)
+    | x::xs -> dest_init_aux (last_elem_seen::rev_init) x xs
+  ))
+
+let dest_init l = ((match l with
+  | [] -> None
+  | x::xs -> Some (dest_init_aux [] x xs)
+))
+
+
+(* ========================================================================== *)
+(* Indexing lists                                                             *)
+(* ========================================================================== *)
+
+(* ------------------------- *)
+(* index / nth with maybe   *)
+(* ------------------------- *)
+
+(*val index : forall 'a. list 'a -> nat -> maybe 'a*)
+
+let rec list_index l n = ((match l with 
+  | []      -> None
+  | x :: xs -> if n = 0 then Some x else list_index xs (Nat_num.nat_monus n( 1))
+))
+
+(* ------------------------- *)
+(* findIndices               *)
+(* ------------------------- *)
+
+(* [findIndices P l] returns the indices of all elements of list [l] that satisfy predicate [P]. 
+   Counting starts with 0, the result list is sorted ascendingly *)
+(*val findIndices : forall 'a. ('a -> bool) -> list 'a -> list nat*)
+
+let rec find_indices_aux (i:int) p0 l =  
+((match l with
+    | []      -> []
+    | x :: xs -> if p0 x then i :: find_indices_aux (i + 1) p0 xs else find_indices_aux (i + 1) p0 xs
+ ))
+let find_indices p0 l = (find_indices_aux( 0) p0 l)
+
+
+
+(* ------------------------- *)
+(* findIndex                 *)
+(* ------------------------- *)
+
+(* findIndex returns the first index of a list that satisfies a given predicate. *)
+(*val findIndex : forall 'a. ('a -> bool) -> list 'a -> maybe nat*)
+let find_index p0 l = ((match find_indices p0 l with
+  | [] -> None
+  | x :: _ -> Some x
+))
+
+(* ------------------------- *)
+(* elemIndices               *)
+(* ------------------------- *)
+
+(*val elemIndices : forall 'a. Eq 'a => 'a -> list 'a -> list nat*)
+
+(* ------------------------- *)
+(* elemIndex                 *)
+(* ------------------------- *)
+
+(*val elemIndex : forall 'a. Eq 'a => 'a -> list 'a -> maybe nat*)
+
+
+(* ========================================================================== *)
+(* Creating lists                                                             *)
+(* ========================================================================== *)
+
+(* ------------------------- *)
+(* genlist                   *)
+(* ------------------------- *)
+
+(* [genlist f n] generates the list [f 0; f 1; ... (f (n-1))] *)
+(*val genlist : forall 'a. (nat -> 'a) -> nat -> list 'a*)
+
+
+let rec genlist f n = 
+  (
+  if(n =  0) then ([]) else
+    (let n'0 =(Nat_num.nat_monus n ( 1)) in snoc (f n'0) (genlist f n'0)))
+
+
+(* ------------------------- *)
+(* replicate                 *)
+(* ------------------------- *)
+
+(*val replicate : forall 'a. nat -> 'a -> list 'a*)
+let rec replicate n x = 
+  (
+  if(n =  0) then ([]) else
+    (let n'0 =(Nat_num.nat_monus n ( 1)) in x :: replicate n'0 x))
+
+
+(* ========================================================================== *)
+(* Sublists                                                                   *)
+(* ========================================================================== *)
+
+(* ------------------------- *)
+(* splitAt                   *)
+(* ------------------------- *)
+
+(* [splitAt n xs] returns a tuple (xs1, xs2), with "append xs1 xs2 = xs" and 
+   "length xs1 = n". If there are not enough elements 
+   in [xs], the original list and the empty one are returned. *)
+(*val splitAt : forall 'a. nat -> list 'a -> (list 'a * list 'a)*)
+let rec split_at n l =  
+ ((match l with
+    | []    -> ([], [])
+    | x::xs -> 
+       if n <= 0 then ([], l) else
+       begin
+         let (l1, l2) = (split_at (Nat_num.nat_monus n( 1)) xs) in
+         ((x::l1), l2)
+       end    
+  ))
+
+
+(* ------------------------- *)
+(* take                      *)
+(* ------------------------- *)
+
+(* take n xs returns the prefix of xs of length n, or xs itself if n > length xs *)
+(*val take : forall 'a. nat -> list 'a -> list 'a*)
+let take n l = (fst (split_at n l))
+
+
+
+(* ------------------------- *)
+(* drop                      *)
+(* ------------------------- *)
+
+(* [drop n xs] drops the first [n] elements of [xs]. It returns the empty list, if [n] > [length xs]. *)
+(*val drop : forall 'a. nat -> list 'a -> list 'a*)
+let drop n l = (snd (split_at n l))
+
+(* ------------------------- *)
+(* dropWhile                 *)
+(* ------------------------- *)
+
+(* [dropWhile p xs] drops the first elements of [xs] that satisfy [p]. *)
+(*val dropWhile : forall 'a. ('a -> bool) -> list 'a -> list 'a*)
+let rec dropWhile p l = ((match l with 
+  | [] -> []
+  | x::xs -> if p x then dropWhile p xs else l
+))
+
+
+(* ------------------------- *)
+(* takeWhile                 *)
+(* ------------------------- *)
+
+(* [takeWhile p xs] takes the first elements of [xs] that satisfy [p]. *)
+(*val takeWhile : forall 'a. ('a -> bool) -> list 'a -> list 'a*)
+let rec takeWhile p l = ((match l with 
+  | [] -> []
+  | x::xs -> if p x then x::takeWhile p xs else []
+))
+
+
+(* ------------------------- *)
+(* isPrefixOf                *)
+(* ------------------------- *)
+
+(*val isPrefixOf : forall 'a. Eq 'a => list 'a -> list 'a -> bool*)
+let rec isPrefixOf dict_Basic_classes_Eq_a l1 l2 = ((match (l1, l2) with
+  | ([], _) -> true
+  | (_::_, []) -> false
+  | (x::xs, y::ys) -> ( 
+  dict_Basic_classes_Eq_a.isEqual_method x y) && isPrefixOf dict_Basic_classes_Eq_a xs ys
+))
+
+(* ------------------------- *)
+(* update                    *)
+(* ------------------------- *)
+(*val update : forall 'a. list 'a -> nat -> 'a -> list 'a*)
+let rec list_update l n e =  
+ ((match l with
+    | []      -> []
+    | x :: xs -> if n = 0 then e :: xs else x :: (list_update xs ( Nat_num.nat_monus n( 1)) e)
+))
+
+
+
+(* ========================================================================== *)
+(* Searching lists                                                            *)
+(* ========================================================================== *)
+
+(* ------------------------- *)
+(* Membership test           *)
+(* ------------------------- *)
+
+(* The membership test, one of the basic list functions, is actually tricky for
+   Lem, because it is tricky, which equality to use. From Lem`s point of 
+   perspective, we want to use the equality provided by the equality type - class.
+   This allows for example to check whether a set is in a list of sets.
+
+   However, in order to use the equality type class, elem essentially becomes
+   existential quantification over lists. For types, which implement semantic
+   equality (=) with syntactic equality, this is overly complicated. In
+   our theorem prover backend, we would end up with overly complicated, harder
+   to read definitions and some of the automation would be harder to apply.
+   Moreover, nearly all the old Lem generated code would change and require 
+   (hopefully minor) adaptions of proofs.
+
+   For now, we ignore this problem and just demand, that all instances of
+   the equality type class do the right thing for the theorem prover backends.   
+*)
+
+(*val elem : forall 'a. Eq 'a => 'a -> list 'a -> bool*)
+(*val elemBy : forall 'a. ('a -> 'a -> bool) -> 'a -> list 'a -> bool*)
+
+let elemBy eq e l = (List.exists (eq e) l)
+(*let elem = elemBy  dict_Basic_classes_Eq_a.isEqual_method*)
+
+(* ------------------------- *)
+(* Find                      *)
+(* ------------------------- *)
+(*val find : forall 'a. ('a -> bool) -> list 'a -> maybe 'a*) (* previously not of maybe type *)
+let rec list_find_opt p0 l = ((match l with 
+  | []      -> None
+  | x :: xs -> if p0 x then Some x else list_find_opt p0 xs
+))
+
+
+(* ----------------------------- *)
+(* Lookup in an associative list *)
+(* ----------------------------- *)
+(*val lookup   : forall 'a 'b. Eq 'a              => 'a -> list ('a * 'b) -> maybe 'b*)
+(*val lookupBy : forall 'a 'b. ('a -> 'a -> bool) -> 'a -> list ('a * 'b) -> maybe 'b*)
+
+(* DPM: eta-expansion for Coq backend type-inference. *)
+let lookupBy eq k m = (Lem.option_map (fun x -> snd x) (list_find_opt (fun (k', _) -> eq k k') m))
+
+(* ------------------------- *)
+(* filter                    *)
+(* ------------------------- *)
+(*val filter : forall 'a. ('a -> bool) -> list 'a -> list 'a*)
+(*let rec filter P l = match l with
+                       | [] -> []
+                       | x :: xs -> if (P x) then x :: (filter P xs) else filter P xs
+                     end*)
+
+
+(* ------------------------- *)
+(* partition                 *)
+(* ------------------------- *)
+(*val partition : forall 'a. ('a -> bool) -> list 'a -> list 'a * list 'a*)
+(*let partition P l = (filter P l, filter (fun x -> not (P x)) l)*)
+
+(*val reversePartition : forall 'a. ('a -> bool) -> list 'a -> list 'a * list 'a*)
+let reversePartition p0 l = (List.partition p0 (List.rev l))
+
+
+(* ------------------------- *)
+(* delete first element      *)
+(* with certain property     *)
+(* ------------------------- *)
+
+(*val deleteFirst : forall 'a. ('a -> bool) -> list 'a -> maybe (list 'a)*) 
+let rec list_delete_first p0 l = ((match l with
+                            | [] -> None
+                            | x :: xs -> if (p0 x) then Some xs else Lem.option_map (fun xs' -> x :: xs') (list_delete_first p0 xs)
+                          ))
+
+
+(*val delete : forall 'a. Eq 'a => 'a -> list 'a -> list 'a*)
+(*val deleteBy : forall 'a. ('a -> 'a -> bool) -> 'a -> list 'a -> list 'a*)
+
+let list_delete eq x l = (Lem.option_default l (list_delete_first (eq x) l))
+
+
+(* ========================================================================== *)
+(* Zipping and unzipping lists                                                *)
+(* ========================================================================== *)
+
+(* ------------------------- *)
+(* zip                       *)
+(* ------------------------- *)
+
+(* zip takes two lists and returns a list of corresponding pairs. If one input list is short, excess elements of the longer list are discarded. *)
+(*val zip : forall 'a 'b. list 'a -> list 'b -> list ('a * 'b)*) (* before combine *)
+let rec list_combine l1 l2 = ((match (l1, l2) with
+  | (x :: xs, y :: ys) -> (x, y) :: list_combine xs ys
+  | _ -> []
+))
+
+(* ------------------------- *)
+(* unzip                     *)
+(* ------------------------- *)
+
+(*val unzip: forall 'a 'b. list ('a * 'b) -> (list 'a * list 'b)*)
+(*let rec unzip l = match l with
+  | [] -> ([], [])
+  | (x, y) :: xys -> let (xs, ys) = unzip xys in (x :: xs, y :: ys)
+end*)
+
+
+let instance_Basic_classes_SetType_list_dict dict_Basic_classes_SetType_a =({
+
+  setElemCompare_method = (lexicographic_compare  
+  dict_Basic_classes_SetType_a.setElemCompare_method)})
+
+(* ------------------------- *)
+(* distinct elements         *)
+(* ------------------------- *)
+
+(*val allDistinct : forall 'a. Eq 'a => list 'a -> bool*)
+let rec allDistinct dict_Basic_classes_Eq_a l =  
+ ((match l with
+    | [] -> true
+    | (x::l') -> not (List.mem x l') && allDistinct 
+  dict_Basic_classes_Eq_a l'
+  ))
+
+(* some more useful functions *)
+(*val mapMaybe : forall 'a 'b. ('a -> maybe 'b) -> list 'a -> list 'b*)
+let rec mapMaybe f xs =  
+((match xs with
+  | [] -> []
+  | x::xs ->
+      (match f x with
+      | None -> mapMaybe f xs
+      | Some y -> y :: (mapMaybe f xs)
+      )
+  ))
+
+(*val mapi : forall 'a 'b. (nat -> 'a -> 'b) -> list 'a -> list 'b*)
+let rec mapiAux f (n : int) l = ((match l with
+  | [] -> []
+  | x :: xs -> (f n x) :: mapiAux f (n + 1) xs
+))
+let mapi f l = (mapiAux f( 0) l)
+
+(* ========================================================================== *)
+(* Comments (not clean yet, please ignore the rest of the file)               *)
+(* ========================================================================== *)
+
+(* ----------------------- *)
+(* skipped from Haskell Lib*)
+(* ----------------------- 
+
+intersperse :: a -> [a] -> [a]
+intercalate :: [a] -> [[a]] -> [a]
+transpose :: [[a]] -> [[a]]
+subsequences :: [a] -> [[a]]
+permutations :: [a] -> [[a]]
+foldl` :: (a -> b -> a) -> a -> [b] -> aSource
+foldl1` :: (a -> a -> a) -> [a] -> aSource
+
+and
+or
+sum
+product
+maximum
+minimum
+scanl
+scanr
+scanl1
+scanr1
+Accumulating maps
+
+mapAccumL :: (acc -> x -> (acc, y)) -> acc -> [x] -> (acc, [y])Source
+mapAccumR :: (acc -> x -> (acc, y)) -> acc -> [x] -> (acc, [y])Source
+
+iterate :: (a -> a) -> a -> [a]
+repeat :: a -> [a]
+cycle :: [a] -> [a]
+unfoldr
+
+
+takeWhile :: (a -> Bool) -> [a] -> [a]Source
+dropWhile :: (a -> Bool) -> [a] -> [a]Source
+dropWhileEnd :: (a -> Bool) -> [a] -> [a]Source
+span :: (a -> Bool) -> [a] -> ([a], [a])Source
+break :: (a -> Bool) -> [a] -> ([a], [a])Source
+break p is equivalent to span (not . p).
+stripPrefix :: Eq a => [a] -> [a] -> Maybe [a]Source
+group :: Eq a => [a] -> [[a]]Source
+inits :: [a] -> [[a]]Source
+tails :: [a] -> [[a]]Source
+
+
+isPrefixOf :: Eq a => [a] -> [a] -> BoolSource
+isSuffixOf :: Eq a => [a] -> [a] -> BoolSource
+isInfixOf :: Eq a => [a] -> [a] -> BoolSource
+
+
+
+notElem :: Eq a => a -> [a] -> BoolSource
+
+zip3 :: [a] -> [b] -> [c] -> [(a, b, c)]Source
+zip4 :: [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]Source
+zip5 :: [a] -> [b] -> [c] -> [d] -> [e] -> [(a, b, c, d, e)]Source
+zip6 :: [a] -> [b] -> [c] -> [d] -> [e] -> [f] -> [(a, b, c, d, e, f)]Source
+zip7 :: [a] -> [b] -> [c] -> [d] -> [e] -> [f] -> [g] -> [(a, b, c, d, e, f, g)]Source
+
+zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]Source
+zipWith3 :: (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]Source
+zipWith4 :: (a -> b -> c -> d -> e) -> [a] -> [b] -> [c] -> [d] -> [e]Source
+zipWith5 :: (a -> b -> c -> d -> e -> f) -> [a] -> [b] -> [c] -> [d] -> [e] -> [f]Source
+zipWith6 :: (a -> b -> c -> d -> e -> f -> g) -> [a] -> [b] -> [c] -> [d] -> [e] -> [f] -> [g]Source
+zipWith7 :: (a -> b -> c -> d -> e -> f -> g -> h) -> [a] -> [b] -> [c] -> [d] -> [e] -> [f] -> [g] -> [h]Source
+
+
+unzip3 :: [(a, b, c)] -> ([a], [b], [c])Source
+unzip4 :: [(a, b, c, d)] -> ([a], [b], [c], [d])Source
+unzip5 :: [(a, b, c, d, e)] -> ([a], [b], [c], [d], [e])Source
+unzip6 :: [(a, b, c, d, e, f)] -> ([a], [b], [c], [d], [e], [f])Source
+unzip7 :: [(a, b, c, d, e, f, g)] -> ([a], [b], [c], [d], [e], [f], [g])Source
+
+
+lines :: String -> [String]Source
+words :: String -> [String]Source
+unlines :: [String] -> StringSource
+unwords :: [String] -> StringSource
+nub :: Eq a => [a] -> [a]Source
+delete :: Eq a => a -> [a] -> [a]Source
+
+(\\) :: Eq a => [a] -> [a] -> [a]Source
+union :: Eq a => [a] -> [a] -> [a]Source
+intersect :: Eq a => [a] -> [a] -> [a]Source
+sort :: Ord a => [a] -> [a]Source
+insert :: Ord a => a -> [a] -> [a]Source
+
+
+nubBy :: (a -> a -> Bool) -> [a] -> [a]Source
+deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]Source
+deleteFirstsBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]Source
+unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]Source
+intersectBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]Source
+groupBy :: (a -> a -> Bool) -> [a] -> [[a]]Source
+sortBy :: (a -> a -> Ordering) -> [a] -> [a]Source
+insertBy :: (a -> a -> Ordering) -> a -> [a] -> [a]Source
+maximumBy :: (a -> a -> Ordering) -> [a] -> aSource
+minimumBy :: (a -> a -> Ordering) -> [a] -> aSource
+genericLength :: Num i => [b] -> iSource
+genericTake :: Integral i => i -> [a] -> [a]Source
+genericDrop :: Integral i => i -> [a] -> [a]Source
+genericSplitAt :: Integral i => i -> [b] -> ([b], [b])Source
+genericIndex :: Integral a => [b] -> a -> bSource
+genericReplicate :: Integral i => i -> a -> [a]Source
+
+
+*)
+
+
+(* ----------------------- *)
+(* skipped from Lem Lib    *)
+(* ----------------------- 
+
+
+val for_all2 : forall 'a 'b. ('a -> 'b -> bool) -> list 'a -> list 'b -> bool
+val exists2 : forall 'a 'b. ('a -> 'b -> bool) -> list 'a -> list 'b -> bool
+val map2 : forall 'a 'b 'c. ('a -> 'b -> 'c) -> list 'a -> list 'b -> list 'c 
+val rev_map2 : forall 'a 'b 'c. ('a -> 'b -> 'c) -> list 'a -> list 'b -> list 'c
+val fold_left2 : forall 'a 'b 'c. ('a -> 'b -> 'c -> 'a) -> 'a -> list 'b -> list 'c -> 'a
+val fold_right2 : forall 'a 'b 'c. ('a -> 'b -> 'c -> 'c) -> list 'a -> list 'b -> 'c -> 'c
+
+
+(* now maybe result and called lookup *)
+val assoc : forall 'a 'b. 'a -> list ('a * 'b) -> 'b
+let inline {ocaml} assoc = Ocaml.List.assoc
+
+
+val mem_assoc : forall 'a 'b. 'a -> list ('a * 'b) -> bool
+val remove_assoc : forall 'a 'b. 'a -> list ('a * 'b) -> list ('a * 'b)
+
+
+
+val stable_sort : forall 'a. ('a -> 'a -> num) -> list 'a -> list 'a
+val fast_sort : forall 'a. ('a -> 'a -> num) -> list 'a -> list 'a
+
+val merge : forall 'a. ('a -> 'a -> num) -> list 'a -> list 'a -> list 'a
+val intersect : forall 'a. list 'a -> list 'a -> list 'a
+
+
+*)
diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_list_extra.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_list_extra.ml
new file mode 100644
index 00000000..8769b232
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/lem_list_extra.ml
@@ -0,0 +1,85 @@
+(*Generated by Lem from list_extra.lem.*)
+
+
+open Lem_bool
+open Lem_maybe
+open Lem_basic_classes
+open Lem_tuple
+open Lem_num
+open Lem_list
+open Lem_assert_extra
+
+(* ------------------------- *)
+(* head of non-empty list    *)
+(* ------------------------- *)
+(*val head : forall 'a. list 'a -> 'a*)
+(*let head l = match l with | x::xs -> x | [] -> failwith "List_extra.head of empty list" end*)
+
+
+(* ------------------------- *)
+(* tail of non-empty list    *)
+(* ------------------------- *)
+(*val tail : forall 'a. list 'a -> list 'a*)
+(*let tail l = match l with | x::xs -> xs | [] -> failwith "List_extra.tail of empty list" end*)
+
+
+(* ------------------------- *)
+(* last                      *)
+(* ------------------------- *)
+(*val last : forall 'a. list 'a -> 'a*)
+let rec last l = ((match l with | [x] -> x | x1::x2::xs -> last (x2 :: xs) | [] -> failwith "List_extra.last of empty list" ))
+
+
+(* ------------------------- *)
+(* init                      *)
+(* ------------------------- *)
+
+(* All elements of a non-empty list except the last one. *)
+(*val init : forall 'a. list 'a -> list 'a*)
+let rec init l = ((match l with | [x] -> [] | x1::x2::xs -> x1::(init (x2::xs)) | [] -> failwith "List_extra.init of empty list" ))
+
+
+(* ------------------------- *)
+(* foldl1 / foldr1           *)
+(* ------------------------- *)
+
+(* folding functions for non-empty lists,
+    which don`t take the base case *)
+(*val foldl1 : forall 'a. ('a -> 'a -> 'a) -> list 'a -> 'a*)
+let foldl1 f x_xs = ((match x_xs with | (x :: xs) -> List.fold_left f x xs | [] -> failwith "List_extra.foldl1 of empty list" ))
+
+(*val foldr1 : forall 'a. ('a -> 'a -> 'a) -> list 'a -> 'a*)
+let foldr1 f x_xs = ((match x_xs with | (x :: xs) -> List.fold_right f xs x | [] -> failwith "List_extra.foldr1 of empty list" ))
+
+  
+(* ------------------------- *)
+(* nth element               *)
+(* ------------------------- *)
+
+(* get the nth element of a list *)
+(*val nth : forall 'a. list 'a -> nat -> 'a*)
+(*let nth l n = match index l n with Just e -> e | Nothing -> failwith "List_extra.nth" end*)
+
+
+(* ------------------------- *)
+(* Find_non_pure             *)
+(* ------------------------- *)
+(*val findNonPure : forall 'a. ('a -> bool) -> list 'a -> 'a*) 
+let findNonPure p0 l = ((match (list_find_opt p0 l) with 
+  | Some e      -> e
+  | None     -> failwith "List_extra.findNonPure"
+))
+
+
+(* ------------------------- *)
+(* zip same length           *)
+(* ------------------------- *)
+
+(*val zipSameLength : forall 'a 'b. list 'a -> list 'b -> list ('a * 'b)*) 
+(*let rec zipSameLength l1 l2 = match (l1, l2) with
+  | (x :: xs, y :: ys) -> (x, y) :: zipSameLength xs ys
+  | ([], []) -> []
+  | _ -> failwith "List_extra.zipSameLength of different length lists"
+
+end*)
+
diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_map.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_map.ml
new file mode 100644
index 00000000..a1aab076
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/lem_map.ml
@@ -0,0 +1,154 @@
+(*Generated by Lem from map.lem.*)
+
+
+open Lem_bool
+open Lem_basic_classes
+open Lem_function
+open Lem_maybe
+open Lem_list
+open Lem_tuple
+open Lem_set
+open Lem_num
+
+(*type map 'k 'v*)
+
+
+
+(* -------------------------------------------------------------------------- *)
+(* Map equality.                                                              *)
+(* -------------------------------------------------------------------------- *)
+
+(*val mapEqual : forall 'k 'v. Eq 'k, Eq 'v => map 'k 'v -> map 'k 'v -> bool*)
+(*val mapEqualBy : forall 'k 'v. ('k -> 'k -> bool) -> ('v -> 'v -> bool) -> map 'k 'v -> map 'k 'v -> bool*)
+
+let instance_Basic_classes_Eq_Map_map_dict dict_Basic_classes_Eq_k dict_Basic_classes_Eq_v =({
+
+  isEqual_method = (Pmap.equal dict_Basic_classes_Eq_v.isEqual_method);
+
+  isInequal_method = (fun m1 m2->not ((Pmap.equal dict_Basic_classes_Eq_v.isEqual_method m1 m2)))})
+
+
+(* -------------------------------------------------------------------------- *)
+(* Map type class                                                             *)
+(* -------------------------------------------------------------------------- *)
+
+type 'a mapKeyType_class= { 
+  mapKeyCompare_method : 'a -> 'a -> int
+}
+
+let instance_Map_MapKeyType_var_dict dict_Basic_classes_SetType_a =({
+
+  mapKeyCompare_method = dict_Basic_classes_SetType_a.setElemCompare_method})
+
+
+(* -------------------------------------------------------------------------- *)
+(* Empty maps                                                                 *)
+(* -------------------------------------------------------------------------- *)
+
+(*val empty : forall 'k 'v. MapKeyType 'k => map 'k 'v*)
+(*val emptyBy : forall 'k 'v. ('k -> 'k -> ordering) -> map 'k 'v*)
+
+
+(* -------------------------------------------------------------------------- *)
+(* Insertion                                                                  *)
+(* -------------------------------------------------------------------------- *)
+
+(*val insert    : forall 'k 'v. MapKeyType 'k => 'k -> 'v -> map 'k 'v -> map 'k 'v*)
+
+
+(* -------------------------------------------------------------------------- *)
+(* Singleton                                                                  *)
+(* -------------------------------------------------------------------------- *)
+
+(*val singleton : forall 'k 'v. MapKeyType 'k => 'k -> 'v -> map 'k 'v*)
+
+
+
+(* -------------------------------------------------------------------------- *)
+(* Emptyness check                                                            *)
+(* -------------------------------------------------------------------------- *)
+
+(*val null  : forall 'k 'v. MapKeyType 'k, Eq 'k, Eq 'v => map 'k 'v -> bool*)
+
+
+(* -------------------------------------------------------------------------- *)
+(* lookup                                                                     *)
+(* -------------------------------------------------------------------------- *)
+
+(*val lookupBy : forall 'k 'v. ('k -> 'k -> ordering) -> 'k -> map 'k 'v -> maybe 'v*)
+
+(*val lookup          : forall 'k 'v. MapKeyType 'k => 'k -> map 'k 'v -> maybe 'v*)
+
+(* -------------------------------------------------------------------------- *)
+(* findWithDefault                                                            *)
+(* -------------------------------------------------------------------------- *)
+
+(*val findWithDefault : forall 'k 'v. MapKeyType 'k => 'k -> 'v -> map 'k 'v -> 'v*)
+
+(* -------------------------------------------------------------------------- *)
+(* from lists                                                                 *)
+(* -------------------------------------------------------------------------- *)
+
+(*val fromList  : forall 'k 'v. MapKeyType 'k => list ('k * 'v) -> map 'k 'v*)
+let fromList dict_Map_MapKeyType_k l = (List.fold_left (fun m (k,v) -> Pmap.add k v m) (Pmap.empty  
+  dict_Map_MapKeyType_k.mapKeyCompare_method) l)
+
+
+(* -------------------------------------------------------------------------- *)
+(* to sets / domain / range                                                   *)
+(* -------------------------------------------------------------------------- *)
+
+(*val toSet : forall 'k 'v. MapKeyType 'k, SetType 'k, SetType 'v => map 'k 'v -> set ('k * 'v)*) 
+(*val toSetBy : forall 'k 'v. (('k * 'v) -> ('k * 'v) -> ordering) -> map 'k 'v -> set ('k * 'v)*)
+
+
+(*val domainBy : forall 'k 'v. ('k -> 'k -> ordering) -> map 'k 'v -> set 'k*)
+(*val domain : forall 'k 'v. MapKeyType 'k, SetType 'k => map 'k 'v -> set 'k*)
+
+
+(*val range : forall 'k 'v. MapKeyType 'k, SetType 'v => map 'k 'v -> set 'v*)
+(*val rangeBy : forall 'k 'v. ('v -> 'v -> ordering) -> map 'k 'v -> set 'v*)
+
+
+(* -------------------------------------------------------------------------- *)
+(* member                                                                     *)
+(* -------------------------------------------------------------------------- *)
+
+(*val member          : forall 'k 'v. MapKeyType 'k, SetType 'k, Eq 'k => 'k -> map 'k 'v -> bool*)
+
+(*val notMember       : forall 'k 'v. MapKeyType 'k, SetType 'k, Eq 'k => 'k -> map 'k 'v -> bool*)
+
+(* -------------------------------------------------------------------------- *)
+(* Quantification                                                             *)
+(* -------------------------------------------------------------------------- *)
+
+(*val any : forall 'k 'v. MapKeyType 'k, Eq 'v => ('k -> 'v -> bool) -> map 'k 'v -> bool*) 
+(*val all : forall 'k 'v. MapKeyType 'k, Eq 'v => ('k -> 'v -> bool) -> map 'k 'v -> bool*) 
+
+(*let all P m = (forall k v. (P k v && ((Instance_Basic_classes_Eq_Maybe_maybe.=) (lookup k m) (Just v))))*)
+
+
+(* -------------------------------------------------------------------------- *)
+(* Set-like operations.                                                       *)
+(* -------------------------------------------------------------------------- *)
+(*val deleteBy         : forall 'k 'v. ('k -> 'k -> ordering) -> 'k -> map 'k 'v -> map 'k 'v*)
+(*val delete           : forall 'k 'v. MapKeyType 'k => 'k -> map 'k 'v -> map 'k 'v*)
+(*val deleteSwap      : forall 'k 'v. MapKeyType 'k => map 'k 'v -> 'k -> map 'k 'v*)
+
+(*val union          : forall 'k 'v. MapKeyType 'k => map 'k 'v -> map 'k 'v -> map 'k 'v*)
+
+(*val unions           : forall 'k 'v. MapKeyType 'k => list (map 'k 'v) -> map 'k 'v*)
+
+
+(* -------------------------------------------------------------------------- *)
+(* Maps (in the functor sense).                                               *)
+(* -------------------------------------------------------------------------- *)
+
+(*val map             : forall 'k 'v 'w. MapKeyType 'k => ('v -> 'w) -> map 'k 'v -> map 'k 'w*)
+
+(*val mapi : forall 'k 'v 'w. MapKeyType 'k => ('k -> 'v -> 'w) -> map 'k 'v -> map 'k 'w*)
+
+(* -------------------------------------------------------------------------- *)
+(* Cardinality                                                                *)
+(* -------------------------------------------------------------------------- *)
+(*val size  : forall 'k 'v. MapKeyType 'k, SetType 'k => map 'k 'v -> nat*)
diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_map_extra.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_map_extra.ml
new file mode 100644
index 00000000..c27f6b73
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/lem_map_extra.ml
@@ -0,0 +1,41 @@
+(*Generated by Lem from map_extra.lem.*)
+
+
+open Lem_bool
+open Lem_basic_classes
+open Lem_function
+open Lem_assert_extra
+open Lem_maybe
+open Lem_list
+open Lem_num
+open Lem_set
+open Lem_map
+
+(* -------------------------------------------------------------------------- *)
+(* find                                                                       *)
+(* -------------------------------------------------------------------------- *)
+
+(*val find : forall 'k 'v. MapKeyType 'k => 'k -> map 'k 'v -> 'v*)
+(*let find k m = match (lookup k m) with Just x -> x | Nothing -> failwith "Map_extra.find" end*)
+
+
+
+(* -------------------------------------------------------------------------- *)
+(* from sets / domain / range                                                 *)
+(* -------------------------------------------------------------------------- *)
+
+
+(*val fromSet : forall 'k 'v. MapKeyType 'k => ('k -> 'v) -> set 'k -> map 'k 'v*)
+(*let fromSet f s = Set_helpers.fold (fun k m -> Map.insert k (f k) m) s Map.empty*)
+
+
+(* -------------------------------------------------------------------------- *)
+(* fold                                                                       *)
+(* -------------------------------------------------------------------------- *)
+
+(*val fold : forall 'k 'v 'r. MapKeyType 'k, SetType 'k, SetType 'v => ('k -> 'v -> 'r -> 'r) -> map 'k 'v -> 'r -> 'r*)
+(*let fold f m v = Set_helpers.fold (fun (k, v) r -> f k v r) (Map.toSet m) v*)
+
+
+(*val toList: forall 'k 'v. MapKeyType 'k => map 'k 'v -> list ('k * 'v)*)
+
diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_maybe.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_maybe.ml
new file mode 100644
index 00000000..8f35b88f
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/lem_maybe.ml
@@ -0,0 +1,98 @@
+(*Generated by Lem from maybe.lem.*)
+ 
+
+open Lem_bool
+open Lem_basic_classes
+open Lem_function
+
+(* ========================================================================== *)
+(* Basic stuff                                                                *)
+(* ========================================================================== *)
+
+(*type maybe 'a = 
+  | Nothing
+  | Just of 'a*)
+
+
+(*val maybeEqual : forall 'a. Eq 'a => maybe 'a -> maybe 'a -> bool*)
+(*val maybeEqualBy : forall 'a. ('a -> 'a -> bool) -> maybe 'a -> maybe 'a -> bool*)
+
+(*let maybeEqualBy eq x y = match (x,y) with
+  | (Nothing, Nothing) -> true
+  | (Nothing, Just _) -> false
+  | (Just _, Nothing) -> false
+  | (Just x', Just y') -> (eq x' y')
+end*)
+
+let instance_Basic_classes_Eq_Maybe_maybe_dict dict_Basic_classes_Eq_a =({
+
+  isEqual_method = (Lem.option_equal  
+  dict_Basic_classes_Eq_a.isEqual_method);
+
+  isInequal_method = (fun x y->not ((Lem.option_equal  
+  dict_Basic_classes_Eq_a.isEqual_method x y)))})  
+
+
+let maybeCompare cmp x y = ((match (x,y) with
+  | (None, None) -> 0
+  | (None, Some _) -> (-1)
+  | (Some _, None) -> 1
+  | (Some x', Some y') -> cmp x' y'
+))
+
+let instance_Basic_classes_SetType_Maybe_maybe_dict dict_Basic_classes_SetType_a =({
+
+  setElemCompare_method = (maybeCompare  
+  dict_Basic_classes_SetType_a.setElemCompare_method)})
+
+
+(* ----------------------- *)
+(* maybe                   *)
+(* ----------------------- *)
+
+(*val maybe : forall 'a 'b. 'b -> ('a -> 'b) -> maybe 'a -> 'b*)
+(*let maybe d f mb = match mb with 
+  | Just a -> f a
+  | Nothing -> d
+end*)
+
+(* ----------------------- *)
+(* isJust / isNothing      *)
+(* ----------------------- *)
+
+(*val isJust : forall 'a. maybe 'a -> bool*)
+(*let isJust mb = match mb with 
+  | Just _ -> true
+  | Nothing -> false
+end*)
+
+(*val isNothing : forall 'a. maybe 'a -> bool*)
+(*let isNothing mb = match mb with 
+  | Just _ -> false
+  | Nothing -> true
+end*)
+
+(* ----------------------- *)
+(* fromMaybe               *)
+(* ----------------------- *)
+
+(*val fromMaybe : forall 'a. 'a -> maybe 'a -> 'a*)
+(*let fromMaybe d mb = match mb with
+   | Just v  -> v
+   | Nothing -> d
+end*)
+
+(* ----------------------- *)
+(* map                     *)
+(* ----------------------- *)
+
+(*val map : forall 'a 'b. ('a -> 'b) -> maybe 'a -> maybe 'b*) 
+(*let map f = maybe Nothing (fun v -> Just (f v))*)
+
+
+(* ----------------------- *)
+(* bind                    *)
+(* ----------------------- *)
+
+(*val bind : forall 'a 'b. maybe 'a -> ('a -> maybe 'b) -> maybe 'b*) 
+(*let bind mb f = maybe Nothing f mb*)
diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_maybe_extra.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_maybe_extra.ml
new file mode 100644
index 00000000..7260b642
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/lem_maybe_extra.ml
@@ -0,0 +1,14 @@
+(*Generated by Lem from maybe_extra.lem.*)
+ 
+
+open Lem_basic_classes
+open Lem_maybe
+open Lem_assert_extra
+
+(* ----------------------- *)
+(* fromJust                *)
+(* ----------------------- *)
+
+(*val fromJust : forall 'a. maybe 'a -> 'a*)
+let fromJust op = ((match op with | Some v -> v | None -> failwith "fromJust of Nothing" ))
+
diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_num.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_num.ml
new file mode 100644
index 00000000..f2e10846
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/lem_num.ml
@@ -0,0 +1,901 @@
+(*Generated by Lem from num.lem.*)
+
+
+open Lem_bool
+open Lem_basic_classes 
+
+(*class inline ( Numeral 'a ) 
+  val fromNumeral : numeral -> 'a 
+end*)
+
+(* ========================================================================== *)
+(* Syntactic type-classes for common operations                               *)
+(* ========================================================================== *)
+
+(* Typeclasses can be used as a mean to overload constants like "+", "-", etc *)
+
+type 'a numNegate_class= { 
+  numNegate_method : 'a -> 'a 
+}
+
+type 'a numAbs_class= { 
+  abs_method : 'a -> 'a 
+}
+
+type 'a numAdd_class= { 
+  numAdd_method : 'a -> 'a -> 'a
+}
+
+type 'a numMinus_class= { 
+  numMinus_method : 'a -> 'a -> 'a
+}
+
+type 'a numMult_class= { 
+  numMult_method : 'a -> 'a -> 'a
+}
+
+type 'a numPow_class= { 
+  numPow_method : 'a -> int -> 'a
+}
+
+type 'a numDivision_class= { 
+  numDivision_method : 'a -> 'a -> 'a
+}
+
+type 'a numIntegerDivision_class= { 
+  div_method : 'a -> 'a -> 'a
+}
+
+
+type 'a numRemainder_class= { 
+  mod_method : 'a -> 'a -> 'a
+}
+
+type 'a numSucc_class= { 
+  succ_method : 'a -> 'a
+}
+
+type 'a numPred_class= { 
+  pred_method : 'a -> 'a
+} 
+
+
+(* ----------------------- *)
+(* natural                 *)
+(* ----------------------- *)
+
+(* unbounded size natural numbers *)
+(*type natural*)
+
+
+(* ----------------------- *)
+(* int                     *)
+(* ----------------------- *)
+
+(* bounded size integers with uncertain length *)
+
+(*type int*)
+
+
+(* ----------------------- *)
+(* integer                 *)
+(* ----------------------- *)
+
+(* unbounded size integers *)
+
+(*type integer*)
+
+(* ----------------------- *)
+(* bint                    *)
+(* ----------------------- *)
+
+(* TODO the bounded ints are only partially implemented, use with care. *)
+
+(* 32 bit integers *)
+(*type int32*) 
+
+(* 64 bit integers *)
+(*type int64*) 
+
+
+(* ----------------------- *)
+(* rational                *)
+(* ----------------------- *)
+
+(* unbounded size and precision rational numbers *)
+
+(*type rational*) (* ???: better type for this in HOL? *)
+
+
+(* ----------------------- *)
+(* double                  *)
+(* ----------------------- *)
+
+(* double precision floating point (64 bits) *)
+
+(*type float64*) (* ???: better type for this in HOL? *)
+
+(*type float32*) (* ???: better type for this in HOL? *)
+
+
+(* ========================================================================== *)
+(* Binding the standard operations for the number types                       *)
+(* ========================================================================== *)
+
+
+(* ----------------------- *)
+(* nat                     *)
+(* ----------------------- *)
+
+(*val natFromNumeral : numeral -> nat*)
+
+(*val natEq : nat -> nat -> bool*)
+let instance_Basic_classes_Eq_nat_dict =({
+
+  isEqual_method = (=);
+
+  isInequal_method = (fun n1 n2->not (n1 = n2))})
+
+(*val natLess : nat -> nat -> bool*)
+(*val natLessEqual : nat -> nat -> bool*)
+(*val natGreater : nat -> nat -> bool*)
+(*val natGreaterEqual : nat -> nat -> bool*)
+
+(*val natCompare : nat -> nat -> ordering*)
+
+let instance_Basic_classes_Ord_nat_dict =({
+
+  compare_method = compare;
+
+  isLess_method = (<);
+
+  isLessEqual_method = (<=);
+
+  isGreater_method = (>);
+
+  isGreaterEqual_method = (>=)})
+
+let instance_Basic_classes_SetType_nat_dict =({
+
+  setElemCompare_method = compare})
+
+(*val natAdd : nat -> nat -> nat*)
+
+let instance_Num_NumAdd_nat_dict =({
+
+  numAdd_method = (+)})
+
+(*val natMinus : nat -> nat -> nat*)
+
+let instance_Num_NumMinus_nat_dict =({
+
+  numMinus_method = Nat_num.nat_monus})
+
+(*val natSucc : nat -> nat*)
+(*let natSucc n = (Instance_Num_NumAdd_nat.+) n 1*)
+let instance_Num_NumSucc_nat_dict =({
+
+  succ_method = succ})
+
+(*val natPred : nat -> nat*)
+let instance_Num_NumPred_nat_dict =({
+
+  pred_method = Nat_num.nat_pred})
+
+(*val natMult : nat -> nat -> nat*)
+
+let instance_Num_NumMult_nat_dict =({
+
+  numMult_method = ( * )})
+
+(*val natDiv : nat -> nat -> nat*)
+
+let instance_Num_NumIntegerDivision_nat_dict =({
+
+  div_method = (/)})
+
+let instance_Num_NumDivision_nat_dict =({
+
+  numDivision_method = (/)})
+
+(*val natMod : nat -> nat -> nat*)
+
+let instance_Num_NumRemainder_nat_dict =({
+
+  mod_method = (mod)})
+
+
+(*val gen_pow_aux : forall 'a. ('a -> 'a -> 'a) -> 'a -> 'a -> nat -> 'a*)
+let rec gen_pow_aux (mul : 'a -> 'a -> 'a) (a : 'a) (b : 'a) (e : int) = 
+  ( (* cannot happen, call discipline guarentees e >= 1 *) if(e =  0) then 
+    a else
+      (
+      if(e =  1) then (mul a b) else
+        (let e'' = (e /  2) in
+         let a' = (if (e mod  2) =  0 then a else mul a b) in
+         gen_pow_aux mul a' (mul b b) e'')))
+       
+let gen_pow (one : 'a) (mul : 'a -> 'a -> 'a) (b : 'a) (e : int) : 'a =  
+ (if e < 0 then one else 
+  if (e = 0) then one else gen_pow_aux mul one b e)
+
+(*val natPow : nat -> nat -> nat*)
+let natPow = (gen_pow( 1) ( * ))
+
+let instance_Num_NumPow_nat_dict =({
+
+  numPow_method = natPow})
+
+(*val natMin : nat -> nat -> nat*)
+
+(*val natMax : nat -> nat -> nat*)
+
+let instance_Basic_classes_OrdMaxMin_nat_dict =({
+
+  max_method = max;
+
+  min_method = min})
+
+
+(* ----------------------- *)
+(* natural                 *)
+(* ----------------------- *)
+
+(*val naturalFromNumeral : numeral -> natural*)
+
+(*val naturalEq : natural -> natural -> bool*)
+let instance_Basic_classes_Eq_Num_natural_dict =({
+
+  isEqual_method = Big_int.eq_big_int;
+
+  isInequal_method = (fun n1 n2->not (Big_int.eq_big_int n1 n2))})
+
+(*val naturalLess : natural -> natural -> bool*)
+(*val naturalLessEqual : natural -> natural -> bool*)
+(*val naturalGreater : natural -> natural -> bool*)
+(*val naturalGreaterEqual : natural -> natural -> bool*)
+
+(*val naturalCompare : natural -> natural -> ordering*)
+
+let instance_Basic_classes_Ord_Num_natural_dict =({
+
+  compare_method = Big_int.compare_big_int;
+
+  isLess_method = Big_int.lt_big_int;
+
+  isLessEqual_method = Big_int.le_big_int;
+
+  isGreater_method = Big_int.gt_big_int;
+
+  isGreaterEqual_method = Big_int.ge_big_int})
+
+let instance_Basic_classes_SetType_Num_natural_dict =({
+
+  setElemCompare_method = Big_int.compare_big_int})
+
+(*val naturalAdd : natural -> natural -> natural*)
+
+let instance_Num_NumAdd_Num_natural_dict =({
+
+  numAdd_method = Big_int.add_big_int})
+
+(*val naturalMinus : natural -> natural -> natural*)
+
+let instance_Num_NumMinus_Num_natural_dict =({
+
+  numMinus_method = Nat_num.natural_monus})
+
+(*val naturalSucc : natural -> natural*)
+(*let naturalSucc n = (Instance_Num_NumAdd_Num_natural.+) n 1*)
+let instance_Num_NumSucc_Num_natural_dict =({
+
+  succ_method = Big_int.succ_big_int})
+
+(*val naturalPred : natural -> natural*)
+let instance_Num_NumPred_Num_natural_dict =({
+
+  pred_method = Nat_num.natural_pred})
+
+(*val naturalMult : natural -> natural -> natural*)
+
+let instance_Num_NumMult_Num_natural_dict =({
+
+  numMult_method = Big_int.mult_big_int})
+
+
+(*val naturalPow : natural -> nat -> natural*)
+
+let instance_Num_NumPow_Num_natural_dict =({
+
+  numPow_method = Big_int.power_big_int_positive_int})
+
+(*val naturalDiv : natural -> natural -> natural*)
+
+let instance_Num_NumIntegerDivision_Num_natural_dict =({
+
+  div_method = Big_int.div_big_int})
+
+let instance_Num_NumDivision_Num_natural_dict =({
+
+  numDivision_method = Big_int.div_big_int})
+
+(*val naturalMod : natural -> natural -> natural*)
+
+let instance_Num_NumRemainder_Num_natural_dict =({
+
+  mod_method = Big_int.mod_big_int})
+
+(*val naturalMin : natural -> natural -> natural*)
+
+(*val naturalMax : natural -> natural -> natural*)
+
+let instance_Basic_classes_OrdMaxMin_Num_natural_dict =({
+
+  max_method = Big_int.max_big_int;
+
+  min_method = Big_int.min_big_int})
+
+
+(* ----------------------- *)
+(* int                     *)
+(* ----------------------- *)
+
+(*val intFromNumeral : numeral -> int*)
+
+(*val intEq : int -> int -> bool*)
+let instance_Basic_classes_Eq_Num_int_dict =({
+
+  isEqual_method = (=);
+
+  isInequal_method = (fun n1 n2->not (n1 = n2))})
+
+(*val intLess : int -> int -> bool*)
+(*val intLessEqual : int -> int -> bool*)
+(*val intGreater : int -> int -> bool*)
+(*val intGreaterEqual : int -> int -> bool*)
+
+(*val intCompare : int -> int -> ordering*)
+
+let instance_Basic_classes_Ord_Num_int_dict =({
+
+  compare_method = compare;
+
+  isLess_method = (<);
+
+  isLessEqual_method = (<=);
+
+  isGreater_method = (>);
+
+  isGreaterEqual_method = (>=)})
+
+let instance_Basic_classes_SetType_Num_int_dict =({
+
+  setElemCompare_method = compare})
+
+(*val intNegate : int -> int*)
+
+let instance_Num_NumNegate_Num_int_dict =({
+
+  numNegate_method = (fun i->(~- i))})
+
+(*val intAbs : int -> int*) (* TODO: check *)
+
+let instance_Num_NumAbs_Num_int_dict =({
+
+  abs_method = abs})
+
+(*val intAdd : int -> int -> int*)
+
+let instance_Num_NumAdd_Num_int_dict =({
+
+  numAdd_method = (+)})
+
+(*val intMinus : int -> int -> int*)
+
+let instance_Num_NumMinus_Num_int_dict =({
+
+  numMinus_method = (-)})
+
+(*val intSucc : int -> int*)
+let instance_Num_NumSucc_Num_int_dict =({
+
+  succ_method = succ})
+
+(*val intPred : int -> int*)
+let instance_Num_NumPred_Num_int_dict =({
+
+  pred_method = pred})
+
+(*val intMult : int -> int -> int*)
+
+let instance_Num_NumMult_Num_int_dict =({
+
+  numMult_method = ( * )})
+
+
+(*val intPow : int -> nat -> int*)
+let intPow = (gen_pow( 1) ( * ))
+
+let instance_Num_NumPow_Num_int_dict =({
+
+  numPow_method = intPow})
+
+(*val intDiv : int -> int -> int*)
+
+let instance_Num_NumIntegerDivision_Num_int_dict =({
+
+  div_method = Nat_num.int_div})
+
+let instance_Num_NumDivision_Num_int_dict =({
+
+  numDivision_method = Nat_num.int_div})
+
+(*val intMod : int -> int -> int*)
+
+let instance_Num_NumRemainder_Num_int_dict =({
+
+  mod_method = Nat_num.int_mod})
+
+(*val intMin : int -> int -> int*)
+
+(*val intMax : int -> int -> int*)
+
+let instance_Basic_classes_OrdMaxMin_Num_int_dict =({
+
+  max_method = max;
+
+  min_method = min})
+
+(* ----------------------- *)
+(* int32                   *)
+(* ----------------------- *)
+(*val int32FromNumeral : numeral -> int32*)
+
+(*val int32Eq : int32 -> int32 -> bool*)
+
+let instance_Basic_classes_Eq_Num_int32_dict =({
+
+  isEqual_method = (=);
+
+  isInequal_method = (fun n1 n2->not (n1 = n2))})
+
+(*val int32Less : int32 -> int32 -> bool*)
+(*val int32LessEqual : int32 -> int32 -> bool*)
+(*val int32Greater : int32 -> int32 -> bool*)
+(*val int32GreaterEqual : int32 -> int32 -> bool*)
+
+(*val int32Compare : int32 -> int32 -> ordering*)
+
+let instance_Basic_classes_Ord_Num_int32_dict =({
+
+  compare_method = Int32.compare;
+
+  isLess_method = (<);
+
+  isLessEqual_method = (<=);
+
+  isGreater_method = (>);
+
+  isGreaterEqual_method = (>=)})
+
+let instance_Basic_classes_SetType_Num_int32_dict =({
+
+  setElemCompare_method = Int32.compare})
+
+(*val int32Negate : int32 -> int32*)
+
+let instance_Num_NumNegate_Num_int32_dict =({
+
+  numNegate_method = Int32.neg})
+
+(*val int32Abs : int32 -> int32*)
+(*let int32Abs i = (if (Instance_Basic_classes_Ord_Num_int32.<=) 0 i then i else Instance_Num_NumNegate_Num_int32.~ i)*)
+
+let instance_Num_NumAbs_Num_int32_dict =({
+
+  abs_method = Int32.abs})
+
+
+(*val int32Add : int32 -> int32 -> int32*)
+
+let instance_Num_NumAdd_Num_int32_dict =({
+
+  numAdd_method = Int32.add})
+
+(*val int32Minus : int32 -> int32 -> int32*)
+
+let instance_Num_NumMinus_Num_int32_dict =({
+
+  numMinus_method = Int32.sub})
+
+(*val int32Succ : int32 -> int32*)
+
+let instance_Num_NumSucc_Num_int32_dict =({
+
+  succ_method = Int32.succ})
+
+(*val int32Pred : int32 -> int32*)
+let instance_Num_NumPred_Num_int32_dict =({
+
+  pred_method = Int32.pred})
+
+(*val int32Mult : int32 -> int32 -> int32*)
+
+let instance_Num_NumMult_Num_int32_dict =({
+
+  numMult_method = Int32.mul})
+
+
+(*val int32Pow : int32 -> nat -> int32*)
+let int32Pow = (gen_pow(Int32.of_int 1) Int32.mul)
+
+let instance_Num_NumPow_Num_int32_dict =({
+
+  numPow_method = int32Pow})
+
+(*val int32Div : int32 -> int32 -> int32*)
+
+let instance_Num_NumIntegerDivision_Num_int32_dict =({
+
+  div_method = Nat_num.int32_div})
+
+let instance_Num_NumDivision_Num_int32_dict =({
+
+  numDivision_method = Nat_num.int32_div})
+
+(*val int32Mod : int32 -> int32 -> int32*)
+
+let instance_Num_NumRemainder_Num_int32_dict =({
+
+  mod_method = Nat_num.int32_mod})
+
+(*val int32Min : int32 -> int32 -> int32*)
+
+(*val int32Max : int32 -> int32 -> int32*)
+
+let instance_Basic_classes_OrdMaxMin_Num_int32_dict =({
+
+  max_method = max;
+
+  min_method = min})
+
+
+
+(* ----------------------- *)
+(* int64                   *)
+(* ----------------------- *)
+(*val int64FromNumeral : numeral -> int64*)
+
+(*val int64Eq : int64 -> int64 -> bool*)
+
+let instance_Basic_classes_Eq_Num_int64_dict =({
+
+  isEqual_method = (=);
+
+  isInequal_method = (fun n1 n2->not (n1 = n2))})
+
+(*val int64Less : int64 -> int64 -> bool*)
+(*val int64LessEqual : int64 -> int64 -> bool*)
+(*val int64Greater : int64 -> int64 -> bool*)
+(*val int64GreaterEqual : int64 -> int64 -> bool*)
+
+(*val int64Compare : int64 -> int64 -> ordering*)
+
+let instance_Basic_classes_Ord_Num_int64_dict =({
+
+  compare_method = Int64.compare;
+
+  isLess_method = (<);
+
+  isLessEqual_method = (<=);
+
+  isGreater_method = (>);
+
+  isGreaterEqual_method = (>=)})
+
+let instance_Basic_classes_SetType_Num_int64_dict =({
+
+  setElemCompare_method = Int64.compare})
+
+(*val int64Negate : int64 -> int64*)
+
+let instance_Num_NumNegate_Num_int64_dict =({
+
+  numNegate_method = Int64.neg})
+
+(*val int64Abs : int64 -> int64*)
+(*let int64Abs i = (if (Instance_Basic_classes_Ord_Num_int64.<=) 0 i then i else Instance_Num_NumNegate_Num_int64.~ i)*)
+
+let instance_Num_NumAbs_Num_int64_dict =({
+
+  abs_method = Int64.abs})
+
+
+(*val int64Add : int64 -> int64 -> int64*)
+
+let instance_Num_NumAdd_Num_int64_dict =({
+
+  numAdd_method = Int64.add})
+
+(*val int64Minus : int64 -> int64 -> int64*)
+
+let instance_Num_NumMinus_Num_int64_dict =({
+
+  numMinus_method = Int64.sub})
+
+(*val int64Succ : int64 -> int64*)
+
+let instance_Num_NumSucc_Num_int64_dict =({
+
+  succ_method = Int64.succ})
+
+(*val int64Pred : int64 -> int64*)
+let instance_Num_NumPred_Num_int64_dict =({
+
+  pred_method = Int64.pred})
+
+(*val int64Mult : int64 -> int64 -> int64*)
+
+let instance_Num_NumMult_Num_int64_dict =({
+
+  numMult_method = Int64.mul})
+
+
+(*val int64Pow : int64 -> nat -> int64*)
+let int64Pow = (gen_pow(Int64.of_int 1) Int64.mul)
+
+let instance_Num_NumPow_Num_int64_dict =({
+
+  numPow_method = int64Pow})
+
+(*val int64Div : int64 -> int64 -> int64*)
+
+let instance_Num_NumIntegerDivision_Num_int64_dict =({
+
+  div_method = Nat_num.int64_div})
+
+let instance_Num_NumDivision_Num_int64_dict =({
+
+  numDivision_method = Nat_num.int64_div})
+
+(*val int64Mod : int64 -> int64 -> int64*)
+
+let instance_Num_NumRemainder_Num_int64_dict =({
+
+  mod_method = Nat_num.int64_mod})
+
+(*val int64Min : int64 -> int64 -> int64*)
+
+(*val int64Max : int64 -> int64 -> int64*)
+
+let instance_Basic_classes_OrdMaxMin_Num_int64_dict =({
+
+  max_method = max;
+
+  min_method = min})
+
+
+(* ----------------------- *)
+(* integer                 *)
+(* ----------------------- *)
+
+(*val integerFromNumeral : numeral -> integer*)
+
+(*val integerEq : integer -> integer -> bool*)
+let instance_Basic_classes_Eq_Num_integer_dict =({
+
+  isEqual_method = Big_int.eq_big_int;
+
+  isInequal_method = (fun n1 n2->not (Big_int.eq_big_int n1 n2))})
+
+(*val integerLess : integer -> integer -> bool*)
+(*val integerLessEqual : integer -> integer -> bool*)
+(*val integerGreater : integer -> integer -> bool*)
+(*val integerGreaterEqual : integer -> integer -> bool*)
+
+(*val integerCompare : integer -> integer -> ordering*)
+
+let instance_Basic_classes_Ord_Num_integer_dict =({
+
+  compare_method = Big_int.compare_big_int;
+
+  isLess_method = Big_int.lt_big_int;
+
+  isLessEqual_method = Big_int.le_big_int;
+
+  isGreater_method = Big_int.gt_big_int;
+
+  isGreaterEqual_method = Big_int.ge_big_int})
+
+let instance_Basic_classes_SetType_Num_integer_dict =({
+
+  setElemCompare_method = Big_int.compare_big_int})
+
+(*val integerNegate : integer -> integer*)
+
+let instance_Num_NumNegate_Num_integer_dict =({
+
+  numNegate_method = Big_int.minus_big_int})
+
+(*val integerAbs : integer -> integer*) (* TODO: check *)
+
+let instance_Num_NumAbs_Num_integer_dict =({
+
+  abs_method = Big_int.abs_big_int})
+
+(*val integerAdd : integer -> integer -> integer*)
+
+let instance_Num_NumAdd_Num_integer_dict =({
+
+  numAdd_method = Big_int.add_big_int})
+
+(*val integerMinus : integer -> integer -> integer*)
+
+let instance_Num_NumMinus_Num_integer_dict =({
+
+  numMinus_method = Big_int.sub_big_int})
+
+(*val integerSucc : integer -> integer*)
+let instance_Num_NumSucc_Num_integer_dict =({
+
+  succ_method = Big_int.succ_big_int})
+
+(*val integerPred : integer -> integer*)
+let instance_Num_NumPred_Num_integer_dict =({
+
+  pred_method = Big_int.pred_big_int})
+
+(*val integerMult : integer -> integer -> integer*)
+
+let instance_Num_NumMult_Num_integer_dict =({
+
+  numMult_method = Big_int.mult_big_int})
+
+
+(*val integerPow : integer -> nat -> integer*)
+
+let instance_Num_NumPow_Num_integer_dict =({
+
+  numPow_method = Big_int.power_big_int_positive_int})
+
+(*val integerDiv : integer -> integer -> integer*)
+
+let instance_Num_NumIntegerDivision_Num_integer_dict =({
+
+  div_method = Big_int.div_big_int})
+
+let instance_Num_NumDivision_Num_integer_dict =({
+
+  numDivision_method = Big_int.div_big_int})
+
+(*val integerMod : integer -> integer -> integer*)
+
+let instance_Num_NumRemainder_Num_integer_dict =({
+
+  mod_method = Big_int.mod_big_int})
+
+(*val integerMin : integer -> integer -> integer*)
+
+(*val integerMax : integer -> integer -> integer*)
+
+let instance_Basic_classes_OrdMaxMin_Num_integer_dict =({
+
+  max_method = Big_int.max_big_int;
+
+  min_method = Big_int.min_big_int})
+
+
+
+(* ========================================================================== *)
+(* Translation between number types                                           *)
+(* ========================================================================== *)
+
+(******************)
+(* integerFrom... *)
+(******************)
+
+(*val integerFromInt : int -> integer*)
+
+
+(*val integerFromNat : nat -> integer*)
+
+(*val integerFromNatural : natural -> integer*)
+
+
+(*val integerFromInt32 : int32 -> integer*)
+
+
+(*val integerFromInt64 : int64 -> integer*)
+
+
+(******************)
+(* naturalFrom... *)
+(******************)
+
+(*val naturalFromNat : nat -> natural*)
+
+(*val naturalFromInteger : integer -> natural*)
+
+
+(******************)
+(* intFrom ...    *)
+(******************)
+
+(*val intFromInteger : integer -> int*)
+
+(*val intFromNat : nat -> int*)
+
+
+(******************)
+(* natFrom ...    *)
+(******************)
+
+(*val natFromNatural : natural -> nat*)
+
+(*val natFromInt : int -> nat*)
+
+
+(******************)
+(* int32From ...  *)
+(******************)
+
+(*val int32FromNat : nat -> int32*)
+
+(*val int32FromNatural : natural -> int32*)
+
+(*val int32FromInteger : integer -> int32*)
+(*let int32FromInteger i = (
+  let abs_int32 = int32FromNatural (naturalFromInteger i) in
+  if ((Instance_Basic_classes_Ord_Num_integer.<) i 0) then (Instance_Num_NumNegate_Num_int32.~ abs_int32) else abs_int32 
+)*)
+
+(*val int32FromInt : int -> int32*)
+(*let int32FromInt i = int32FromInteger (integerFromInt i)*)
+
+
+(*val int32FromInt64 : int64 -> int32*)
+(*let int32FromInt64 i = int32FromInteger (integerFromInt64 i)*)
+
+
+
+
+(******************)
+(* int64From ...  *)
+(******************)
+
+(*val int64FromNat : nat -> int64*)
+
+(*val int64FromNatural : natural -> int64*)
+
+(*val int64FromInteger : integer -> int64*)
+(*let int64FromInteger i = (
+  let abs_int64 = int64FromNatural (naturalFromInteger i) in
+  if ((Instance_Basic_classes_Ord_Num_integer.<) i 0) then (Instance_Num_NumNegate_Num_int64.~ abs_int64) else abs_int64 
+)*)
+
+(*val int64FromInt : int -> int64*)
+(*let int64FromInt i = int64FromInteger (integerFromInt i)*)
+
+
+(*val int64FromInt32 : int32 -> int64*)
+(*let int64FromInt32 i = int64FromInteger (integerFromInt32 i)*)
+
+
+(******************)
+(* what's missing *)
+(******************)
+
+(*val naturalFromInt : int -> natural*)
+(*val naturalFromInt32 : int32 -> natural*)
+(*val naturalFromInt64 : int64 -> natural*)
+
+
+(*val intFromNatural : natural -> int*)
+(*val intFromInt32 : int32 -> int*)
+(*val intFromInt64 : int64 -> int*)
+
+(*val natFromInteger : integer -> nat*)
+(*val natFromInt32 : int32 -> nat*)
+(*val natFromInt64 : int64 -> nat*)
+
+(*val string_of_natural : natural -> string*)
diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_pervasives.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_pervasives.ml
new file mode 100644
index 00000000..729d9b79
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/lem_pervasives.ml
@@ -0,0 +1,18 @@
+(*Generated by Lem from pervasives.lem.*)
+ 
+
+include Lem_basic_classes
+include Lem_bool
+include Lem_tuple
+include Lem_maybe
+include Lem_either
+include Lem_function
+include Lem_num
+include Lem_map
+include Lem_set
+include Lem_list
+include Lem_string
+include Lem_word
+
+(*import Sorting Relation*)
+
diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_pervasives_extra.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_pervasives_extra.ml
new file mode 100644
index 00000000..121429c6
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/lem_pervasives_extra.ml
@@ -0,0 +1,12 @@
+(*Generated by Lem from pervasives_extra.lem.*)
+ 
+
+include Lem_pervasives 
+include Lem_function_extra
+include Lem_maybe_extra
+include Lem_map_extra
+include Lem_set_extra
+include Lem_set_helpers
+include Lem_list_extra
+include Lem_string_extra
+include Lem_assert_extra
diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_relation.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_relation.ml
new file mode 100644
index 00000000..f2e8114b
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/lem_relation.ml
@@ -0,0 +1,424 @@
+(*Generated by Lem from relation.lem.*)
+
+
+open Lem_bool
+open Lem_basic_classes
+open Lem_tuple
+open Lem_set
+open Lem_num
+
+(* ========================================================================== *)
+(* The type of relations                                                      *)
+(* ========================================================================== *)
+
+type( 'a, 'b) rel_pred = 'a -> 'b -> bool
+type( 'a, 'b) rel_set = ('a * 'b) Pset.set
+
+(* Binary relations are usually represented as either
+   sets of pairs (rel_set) or as curried functions (rel_pred). 
+   
+   The choice depends on taste and the backend. Lem should not take a 
+   decision, but supports both representations. There is an abstract type
+   pred, which can be converted to both representations. The representation
+   of pred itself then depends on the backend. However, for the time beeing,
+   let's implement relations as sets to get them working more quickly. *)
+
+type( 'a, 'b) rel = ('a, 'b) rel_set
+
+(*val relToSet : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b -> rel_set 'a 'b*)
+(*val relFromSet : forall 'a 'b. SetType 'a, SetType 'b => rel_set 'a 'b -> rel 'a 'b*)
+
+(*val relEq : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b -> rel 'a 'b -> bool*)
+let relEq dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b r1 r2 = ( Pset.equal r1 r2)
+
+(*val relToPred : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a, Eq 'b => rel 'a 'b -> rel_pred 'a 'b*)
+(*val relFromPred : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a, Eq 'b => set 'a -> set 'b -> rel_pred 'a 'b -> rel 'a 'b*)
+
+let relToPred dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b dict_Basic_classes_Eq_a dict_Basic_classes_Eq_b r = (fun x y ->  Pset.mem(x, y) r)
+let relFromPred dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b dict_Basic_classes_Eq_a dict_Basic_classes_Eq_b xs ys p = (Pset.filter (fun (x,y) -> p x y) ((Pset.cross (pairCompare  
+  dict_Basic_classes_SetType_a.setElemCompare_method  dict_Basic_classes_SetType_b.setElemCompare_method) xs ys)))
+
+ 
+(* ========================================================================== *)
+(* Basic Operations                                                           *)
+(* ========================================================================== *)
+
+(* ----------------------- *)
+(* membership test         *)
+(* ----------------------- *)
+
+(*val inRel : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a, Eq 'b => 'a -> 'b -> rel 'a 'b -> bool*)
+
+
+(* ----------------------- *)
+(* empty relation          *)
+(* ----------------------- *)
+
+(*val relEmpty : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b*)
+
+(* ----------------------- *)
+(* Insertion               *)
+(* ----------------------- *)
+
+(*val relAdd : forall 'a 'b. SetType 'a, SetType 'b => 'a -> 'b -> rel 'a 'b -> rel 'a 'b*)
+
+
+(* ----------------------- *)
+(* Identity relation       *)
+(* ----------------------- *)
+
+(*val relIdOn : forall 'a. SetType 'a, Eq 'a => set 'a -> rel 'a 'a*)
+let relIdOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a s = (relFromPred 
+  dict_Basic_classes_SetType_a dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a dict_Basic_classes_Eq_a s s  dict_Basic_classes_Eq_a.isEqual_method)
+
+(*val relId : forall 'a. SetType 'a, Eq 'a => rel 'a 'a*)
+
+(* ----------------------- *)
+(* relation union          *)
+(* ----------------------- *)
+
+(*val relUnion : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b -> rel 'a 'b -> rel 'a 'b*) 
+
+(* ----------------------- *)
+(* relation intersection   *)
+(* ----------------------- *)
+
+(*val relIntersection : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a, Eq 'b => rel 'a 'b -> rel 'a 'b -> rel 'a 'b*) 
+
+(* ----------------------- *)
+(* Relation Composition    *)
+(* ----------------------- *)
+
+(*val relComp : forall 'a 'b 'c. SetType 'a, SetType 'b, SetType 'c, Eq 'a, Eq 'b => rel 'a 'b -> rel 'b 'c -> rel 'a 'c*)
+let relComp dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b dict_Basic_classes_SetType_c dict_Basic_classes_Eq_a dict_Basic_classes_Eq_b r1 r2 = (let x2 =(Pset.from_list (pairCompare  
+  dict_Basic_classes_SetType_a.setElemCompare_method  dict_Basic_classes_SetType_c.setElemCompare_method) []) in  Pset.fold
+   (fun(e1,e2) x2 -> Pset.fold
+                       (fun(e2',e3) x2 ->
+                        if dict_Basic_classes_Eq_b.isEqual_method e2 e2' then
+                          Pset.add (e1, e3) x2 else x2) (r2) x2) (r1) 
+ x2)
+
+(* ----------------------- *)
+(* restrict                *)
+(* ----------------------- *)
+
+(*val relRestrict : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> rel 'a 'a*)
+let relRestrict dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (let x2 =(Pset.from_list (pairCompare  
+  dict_Basic_classes_SetType_a.setElemCompare_method  dict_Basic_classes_SetType_a.setElemCompare_method) []) in  Pset.fold
+   (fun a x2 -> Pset.fold
+                  (fun b x2 ->
+                   if Pset.mem (a, b) r then Pset.add (a, b) x2 else x2) 
+                s x2) s x2)
+
+
+(* ----------------------- *)
+(* Converse                *)
+(* ----------------------- *)
+
+(*val relConverse : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b -> rel 'b 'a*)
+let relConverse dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b r = ((Pset.map (pairCompare  
+  dict_Basic_classes_SetType_b.setElemCompare_method  dict_Basic_classes_SetType_a.setElemCompare_method) Lem.pair_swap (r)))
+
+
+(* ----------------------- *)
+(* domain                  *)
+(* ----------------------- *)
+
+(*val relDomain : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b -> set 'a*)
+let relDomain dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b r = (Pset.map  
+  dict_Basic_classes_SetType_a.setElemCompare_method (fun x -> fst x) (r))
+
+(* ----------------------- *)
+(* range                   *)
+(* ----------------------- *)
+
+(*val relRange : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b -> set 'b*)
+let relRange dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b r = (Pset.map  
+  dict_Basic_classes_SetType_b.setElemCompare_method (fun x -> snd x) (r))
+
+
+(* ----------------------- *)
+(* field / definedOn       *)
+(*                         *)
+(* avoid the keyword field *)
+(* ----------------------- *)
+
+(*val relDefinedOn : forall 'a. SetType 'a => rel 'a 'a -> set 'a*)
+
+(* ----------------------- *)
+(* relOver                 *)
+(*                         *)
+(* avoid the keyword field *)
+(* ----------------------- *)
+
+(*val relOver : forall 'a. SetType 'a => rel 'a 'a -> set 'a -> bool*)
+let relOver dict_Basic_classes_SetType_a r s = ( Pset.subset(( Pset.(union)(relDomain 
+  dict_Basic_classes_SetType_a dict_Basic_classes_SetType_a r) (relRange dict_Basic_classes_SetType_a dict_Basic_classes_SetType_a r))) s)
+
+
+(* ----------------------- *)
+(* apply a relation        *)
+(* ----------------------- *)
+
+(* Given a relation r and a set s, relApply r s applies s to r, i.e.
+   it returns the set of all value reachable via r from a value in s.
+   This operation can be seen as a generalisation of function application. *)
+   
+(*val relApply : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a => rel 'a 'b -> set 'a -> set 'b*)
+let relApply dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b dict_Basic_classes_Eq_a r s = (let x2 =(Pset.from_list  
+  dict_Basic_classes_SetType_b.setElemCompare_method  []) in  Pset.fold (fun(x, y) x2 -> if Pset.mem x s then Pset.add y x2 else x2) 
+ (r) x2)
+
+
+(* ========================================================================== *)
+(* Properties                                                                 *)
+(* ========================================================================== *)
+
+(* ----------------------- *)
+(* subrel                  *)
+(* ----------------------- *)
+
+(*val isSubrel : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a, Eq 'b => rel 'a 'b -> rel 'a 'b -> bool*)
+
+(* ----------------------- *)
+(* reflexivity             *)
+(* ----------------------- *)
+
+(*val isReflexiveOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+let isReflexiveOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (Pset.for_all  
+  (fun e -> Pset.mem (e, e) r) s)
+
+(*val isReflexive : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+
+
+(* ----------------------- *)
+(* irreflexivity           *)
+(* ----------------------- *)
+
+(*val isIrreflexiveOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+let isIrreflexiveOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (Pset.for_all  
+  (fun e -> not ( Pset.mem (e, e) r)) s)
+
+(*val isIrreflexive : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+let isIrreflexive dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r = (Pset.for_all  
+  (fun (e1, e2) -> not ( dict_Basic_classes_Eq_a.isEqual_method e1 e2)) (r))
+
+
+(* ----------------------- *)
+(* symmetry                *)
+(* ----------------------- *)
+
+(*val isSymmetricOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+let isSymmetricOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (Pset.for_all  
+  (fun e1 -> Pset.for_all
+               (fun e2 -> ((not ( Pset.mem (e1, e2) r)) ||
+                             ( Pset.mem (e2, e1) r))) s) s)
+
+(*val isSymmetric : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+let isSymmetric dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r = (Pset.for_all  
+  (fun (e1, e2) -> Pset.mem (e2, e1) r) r)
+
+
+(* ----------------------- *)
+(* antisymmetry            *)
+(* ----------------------- *)
+
+(*val isAntisymmetricOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+let isAntisymmetricOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (Pset.for_all  
+  (fun e1 -> Pset.for_all
+               (fun e2 -> ((not ( Pset.mem (e1, e2) r)) ||
+                             ((not ( Pset.mem (e2, e1) r)) ||
+                                ( dict_Basic_classes_Eq_a.isEqual_method 
+                                  e1 e2)))) s) s)
+
+(*val isAntisymmetric : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+let isAntisymmetric dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r = (Pset.for_all  
+  (fun (e1, e2) -> ((not ( Pset.mem (e2, e1) r)) ||
+                      ( dict_Basic_classes_Eq_a.isEqual_method e1 e2))) r)
+
+
+(* ----------------------- *)
+(* transitivity            *)
+(* ----------------------- *)
+
+(*val isTransitiveOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+let isTransitiveOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (Pset.for_all  
+  (fun e1 -> Pset.for_all
+               (fun e2 -> Pset.for_all
+                            (fun e3 -> ((not ( Pset.mem (e1, e2) r)) ||
+                                          ((not ( Pset.mem (e2, e3) r)) ||
+                                             ( Pset.mem (e1, e3) r)))) 
+                          s) s) s)
+
+(*val isTransitive : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+let isTransitive dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r = (Pset.for_all  
+  (fun (e1, e2) -> Pset.for_all (fun e3 -> Pset.mem (e1, e3) r)
+                     (relApply dict_Basic_classes_SetType_a
+                        dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a
+                        r
+                        (Pset.from_list
+                           dict_Basic_classes_SetType_a.setElemCompare_method
+                           [e2]))) r)
+
+(* ----------------------- *)
+(* total                   *)
+(* ----------------------- *)
+
+(*val isTotalOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+let isTotalOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (Pset.for_all  
+  (fun e1 -> Pset.for_all
+               (fun e2 -> ( Pset.mem (e1, e2) r) || ( Pset.mem (e2, e1) r)) 
+             s) s)
+
+
+(*val isTotal : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+
+
+(*val isTrichotomousOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+let isTrichotomousOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (Pset.for_all  
+  (fun e1 -> Pset.for_all
+               (fun e2 -> ( Pset.mem (e1, e2) r) ||
+                            (( dict_Basic_classes_Eq_a.isEqual_method e1 e2)
+                               || ( Pset.mem (e2, e1) r))) s) s)
+
+(*val isTrichotomous : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+
+
+(* ----------------------- *)
+(* is_single_valued        *)
+(* ----------------------- *)
+
+(*val isSingleValued : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a, Eq 'b => rel 'a 'b -> bool*)
+let isSingleValued dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b dict_Basic_classes_Eq_a dict_Basic_classes_Eq_b r = (Pset.for_all  
+  (fun (e1, e2a) -> Pset.for_all
+                      (fun e2b -> dict_Basic_classes_Eq_b.isEqual_method 
+                                  e2a e2b)
+                      (relApply dict_Basic_classes_SetType_a
+                         dict_Basic_classes_SetType_b dict_Basic_classes_Eq_a
+                         r
+                         (Pset.from_list
+                            dict_Basic_classes_SetType_a.setElemCompare_method
+                            [e1]))) r)
+
+
+(* ----------------------- *)
+(* equivalence relation    *)
+(* ----------------------- *)
+
+(*val isEquivalenceOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+let isEquivalenceOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (isReflexiveOn 
+  dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s && (isSymmetricOn 
+  dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s && isTransitiveOn 
+  dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s))
+
+
+(*val isEquivalence : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+
+
+(* ----------------------- *)
+(* well founded            *)
+(* ----------------------- *)
+
+(*val isWellFounded : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+
+
+(* ========================================================================== *)
+(* Orders                                                                     *)
+(* ========================================================================== *)
+
+
+(* ----------------------- *)
+(* pre- or quasiorders     *)
+(* ----------------------- *)
+
+(*val isPreorderOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+let isPreorderOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (isReflexiveOn 
+  dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s && isTransitiveOn 
+  dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s)
+
+(*val isPreorder : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+
+
+(* ----------------------- *)
+(* partial orders          *)
+(* ----------------------- *)
+
+(*val isPartialOrderOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+let isPartialOrderOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (isReflexiveOn 
+  dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s && (isTransitiveOn 
+  dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s && isAntisymmetricOn 
+  dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s))
+
+
+(*val isStrictPartialOrderOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+let isStrictPartialOrderOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (isIrreflexiveOn 
+  dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s && isTransitiveOn 
+  dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s)
+
+
+(*val isStrictPartialOrder : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+let isStrictPartialOrder dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r = (isIrreflexive 
+  dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r && isTransitive dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r)
+
+(*val isPartialOrder : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+
+(* ----------------------- *)
+(* total / linear orders   *)
+(* ----------------------- *)
+
+(*val isTotalOrderOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+let isTotalOrderOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (isPartialOrderOn 
+  dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s && isTotalOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s)
+
+(*val isStrictTotalOrderOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*)
+let isStrictTotalOrderOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (isStrictPartialOrderOn 
+  dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s && isTrichotomousOn 
+  dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s)
+
+(*val isTotalOrder : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+
+(*val isStrictTotalOrder : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*)
+
+
+
+(* ========================================================================== *)
+(* closures                                                                   *)
+(* ========================================================================== *)
+
+(* ----------------------- *)
+(* transitive closure      *)
+(* ----------------------- *)
+
+(*val transitiveClosure : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> rel 'a 'a*)
+(*val transitiveClosureByEq  : forall 'a. ('a -> 'a -> bool) -> rel 'a 'a -> rel 'a 'a*)
+(*val transitiveClosureByCmp : forall 'a. ('a * 'a -> 'a * 'a -> ordering) -> rel 'a 'a -> rel 'a 'a*)
+
+
+(* ----------------------- *)
+(* transitive closure step *)
+(* ----------------------- *)
+
+(*val transitiveClosureAdd : forall 'a. SetType 'a, Eq 'a => 'a -> 'a -> rel 'a 'a -> rel 'a 'a*)
+
+let transitiveClosureAdd dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a x y r = 
+  (( Pset.(union)(((Pset.add (x,y) (r)))) ((( Pset.(union)((let x2 =(Pset.from_list (pairCompare  
+  dict_Basic_classes_SetType_a.setElemCompare_method  dict_Basic_classes_SetType_a.setElemCompare_method) []) in  Pset.fold (fun z x2 -> if Pset.mem (y, z) r then Pset.add (x, z) x2 else x2)
+   (relRange dict_Basic_classes_SetType_a dict_Basic_classes_SetType_a r) 
+ x2)) ((let x2 =(Pset.from_list (pairCompare  
+  dict_Basic_classes_SetType_a.setElemCompare_method  dict_Basic_classes_SetType_a.setElemCompare_method) []) in  Pset.fold (fun z x2 -> if Pset.mem (z, x) r then Pset.add (z, y) x2 else x2)
+   (relDomain dict_Basic_classes_SetType_a dict_Basic_classes_SetType_a r) 
+ x2)))))))
+
+
+(* ========================================================================== *)
+(* reflexiv closures                                                          *)
+(* ========================================================================== *)
+
+(*val reflexivTransitiveClosureOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> rel 'a 'a*)
+let reflexivTransitiveClosureOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (Pset.tc (pairCompare  
+  dict_Basic_classes_SetType_a.setElemCompare_method  dict_Basic_classes_SetType_a.setElemCompare_method) (( Pset.(union)(r) ((relIdOn 
+  dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a s)))))
+
+
+(*val reflexivTransitiveClosure : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> rel 'a 'a*)
+
diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_set.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_set.ml
new file mode 100644
index 00000000..1cd7c3fa
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/lem_set.ml
@@ -0,0 +1,290 @@
+(*Generated by Lem from set.lem.*)
+(******************************************************************************)
+(* A library for sets                                                         *)
+(*                                                                            *)
+(* It mainly follows the Haskell Set-library                                  *)
+(******************************************************************************)
+
+(* Sets in Lem are a bit tricky. On the one hand, we want efficiently executable sets.
+   OCaml and Haskell both represent sets by some kind of balancing trees. This means
+   that sets are finite and an order on the element type is required. 
+   Such sets are constructed by simple, executable operations like inserting or
+   deleting elements, union, intersection, filtering etc.
+
+   On the other hand, we want to use sets for specifications. This leads often
+   infinite sets, which are specificied in complicated, perhaps even undecidable
+   ways.
+
+   The set library in this file, chooses the first approach. It describes 
+   *finite* sets with an underlying order. Infinite sets should in the medium
+   run be represented by a separate type. Since this would require some significant
+   changes to Lem, for the moment also infinite sets are represented using this
+   class. However, a run-time exception might occour when using these sets. 
+   This problem needs adressing in the future. *)
+   
+
+(* ========================================================================== *)
+(* Header                                                                     *)
+(* ========================================================================== *)
+
+open Lem_bool
+open Lem_basic_classes
+open Lem_maybe
+open Lem_function
+open Lem_num
+open Lem_list
+open Lem_set_helpers
+
+(* ----------------------- *)
+(* Equality check          *)
+(* ----------------------- *)
+
+(*val setEqualBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> bool*)
+
+(*val setEqual : forall 'a. SetType 'a => set 'a -> set 'a -> bool*)
+
+let instance_Basic_classes_Eq_set_dict dict_Basic_classes_SetType_a =({
+
+  isEqual_method = Pset.equal;
+
+  isInequal_method = (fun s1 s2->not (Pset.equal s1 s2))})
+
+
+
+(* ----------------------- *)
+(* compare                 *)
+(* ----------------------- *)
+
+(*val setCompareBy: forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> ordering*)
+
+(*val setCompare : forall 'a. SetType 'a => set 'a -> set 'a -> ordering*)
+
+let instance_Basic_classes_SetType_set_dict dict_Basic_classes_SetType_a =({
+
+  setElemCompare_method = Pset.compare})
+
+
+(* ----------------------- *)
+(* Empty set               *)
+(* ----------------------- *)
+
+(*val empty : forall 'a. SetType 'a => set 'a*) 
+(*val emptyBy : forall 'a. ('a -> 'a -> ordering) -> set 'a*)
+
+(* ----------------------- *)
+(* any / all               *)
+(* ----------------------- *)
+
+(*val any : forall 'a. SetType 'a => ('a -> bool) -> set 'a -> bool*)
+
+(*val all : forall 'a. SetType 'a => ('a -> bool) -> set 'a -> bool*)
+
+
+(* ----------------------- *)
+(* (IN)                    *)
+(* ----------------------- *)
+
+(*val IN [member] : forall 'a. SetType 'a => 'a -> set 'a -> bool*) 
+(*val memberBy : forall 'a. ('a -> 'a -> ordering) -> 'a -> set 'a -> bool*)
+
+(* ----------------------- *)
+(* not (IN)                *)
+(* ----------------------- *)
+
+(*val NIN [notMember] : forall 'a. SetType 'a => 'a -> set 'a -> bool*)
+
+
+
+(* ----------------------- *)
+(* Emptyness check         *)
+(* ----------------------- *)
+
+(*val null : forall 'a. SetType 'a => set 'a -> bool*)
+
+
+(* ------------------------ *)
+(* singleton                *)
+(* ------------------------ *)
+
+(*val singleton : forall 'a. SetType 'a => 'a -> set 'a*)
+
+
+(* ----------------------- *)
+(* size                    *)
+(* ----------------------- *)
+
+(*val size : forall 'a. SetType 'a => set 'a -> nat*)
+
+
+(* ----------------------------*)
+(* setting up pattern matching *)
+(* --------------------------- *)
+
+(*val set_case : forall 'a 'b. SetType 'a => set 'a -> 'b -> ('a -> 'b) -> 'b -> 'b*)
+
+
+(* ------------------------ *)
+(* union                    *)
+(* ------------------------ *)
+
+(*val unionBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> set 'a*)
+(*val union : forall 'a. SetType 'a => set 'a -> set 'a -> set 'a*)
+
+(* ----------------------- *)
+(* insert                  *)
+(* ----------------------- *)
+
+(*val insert : forall 'a. SetType 'a => 'a -> set 'a -> set 'a*)
+
+(* ----------------------- *)
+(* filter                  *)
+(* ----------------------- *)
+
+(*val filter : forall 'a. SetType 'a => ('a -> bool) -> set 'a -> set 'a*) 
+(*let filter P s = {e | forall (e IN s) | P e}*)
+
+
+(* ----------------------- *)
+(* partition               *)
+(* ----------------------- *)
+
+(*val partition : forall 'a. SetType 'a => ('a -> bool) -> set 'a -> set 'a * set 'a*)
+let partition dict_Basic_classes_SetType_a p0 s = (Pset.filter p0 s, Pset.filter (fun e -> not (p0 e)) s)
+
+
+(* ----------------------- *)
+(* split                   *)
+(* ----------------------- *)
+
+(*val split : forall 'a. SetType 'a, Ord 'a => 'a -> set 'a -> set 'a * set 'a*)
+let split dict_Basic_classes_SetType_a dict_Basic_classes_Ord_a p s = (Pset.filter (
+  dict_Basic_classes_Ord_a.isLess_method p) s, Pset.filter (dict_Basic_classes_Ord_a.isGreater_method p) s)
+
+(*val splitMember : forall 'a. SetType 'a, Ord 'a => 'a -> set 'a -> set 'a * bool * set 'a*)
+let splitMember dict_Basic_classes_SetType_a dict_Basic_classes_Ord_a p s = (Pset.filter (
+  dict_Basic_classes_Ord_a.isLess_method p) s,  Pset.mem p s, Pset.filter (
+  dict_Basic_classes_Ord_a.isGreater_method p) s)
+
+
+(* ------------------------ *)
+(* subset and proper subset *)
+(* ------------------------ *)
+
+(*val isSubsetOfBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> bool*)
+(*val isProperSubsetOfBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> bool*)
+
+(*val isSubsetOf : forall 'a. SetType 'a => set 'a -> set 'a -> bool*)
+(*val isProperSubsetOf : forall 'a. SetType 'a => set 'a -> set 'a -> bool*)
+
+
+(* ------------------------ *)
+(* delete                   *)
+(* ------------------------ *)
+
+(*val delete : forall 'a. SetType 'a, Eq 'a => 'a -> set 'a -> set 'a*)
+(*val deleteBy : forall 'a. SetType 'a => ('a -> 'a -> bool) -> 'a -> set 'a -> set 'a*)
+
+
+(* ------------------------ *)
+(* bigunion                 *)
+(* ------------------------ *)
+
+(*val bigunion : forall 'a. SetType 'a => set (set 'a) -> set 'a*)
+(*val bigunionBy : forall 'a. ('a -> 'a -> ordering) -> set (set 'a) -> set 'a*)
+
+(*let bigunion bs = {x | forall (s IN bs) (x IN s) | true}*)
+
+
+(* ------------------------ *)
+(* difference               *)
+(* ------------------------ *)
+
+(*val differenceBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> set 'a*)
+(*val difference : forall 'a. SetType 'a => set 'a -> set 'a -> set 'a*)
+
+(* ------------------------ *)
+(* intersection             *)
+(* ------------------------ *)
+
+(*val intersection : forall 'a. SetType 'a => set 'a -> set 'a -> set 'a*)
+(*val intersectionBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> set 'a*)
+
+
+(* ------------------------ *)
+(* map                      *)
+(* ------------------------ *)
+
+(*val map : forall 'a 'b. SetType 'a, SetType 'b => ('a -> 'b) -> set 'a -> set 'b*) (* before image *)
+(*let map f s = { f e | forall (e IN s) | true }*)
+
+(*val mapBy : forall 'a 'b. ('b -> 'b -> ordering) -> ('a -> 'b) -> set 'a -> set 'b*) 
+
+
+(* ------------------------ *)
+(* bigunionMap              *)
+(* ------------------------ *)
+
+(* In order to avoid providing an comparison function for sets of sets,
+   it might be better to combine bigunion and map sometimes into a single operation. *)
+
+(*val bigunionMap : forall 'a 'b. SetType 'a, SetType 'b => ('a -> set 'b) -> set 'a -> set 'b*)
+(*val bigunionMapBy : forall 'a 'b. ('b -> 'b -> ordering) -> ('a -> set 'b) -> set 'a -> set 'b*)
+
+(* ------------------------ *)
+(* min and max              *)
+(* ------------------------ *)
+
+(*val findMin : forall 'a.  SetType 'a, Eq 'a => set 'a -> maybe 'a*) 
+(*val findMax : forall 'a.  SetType 'a, Eq 'a => set 'a -> maybe 'a*) 
+
+
+
+(* ------------------------ *)
+(* fromList                 *)
+(* ------------------------ *)
+
+(*val fromList : forall 'a.  SetType 'a => list 'a -> set 'a*) (* before from_list *)
+(*val fromListBy : forall 'a.  ('a -> 'a -> ordering) -> list 'a -> set 'a*) 
+
+
+(* ------------------------ *)
+(* Sigma                    *)
+(* ------------------------ *)
+
+(*val sigma : forall 'a 'b. SetType 'a, SetType 'b => set 'a -> ('a -> set 'b) -> set ('a * 'b)*)
+(*val sigmaBy : forall 'a 'b. (('a * 'b) -> ('a * 'b) -> ordering) -> set 'a -> ('a -> set 'b) -> set ('a * 'b)*)
+
+(*let sigma sa sb = { (a, b) | forall (a IN sa) (b IN sb a) | true }*)
+
+
+(* ------------------------ *)
+(* cross product            *)
+(* ------------------------ *)
+
+(*val cross : forall 'a 'b. SetType 'a, SetType 'b => set 'a -> set 'b -> set ('a * 'b)*)
+(*val crossBy : forall 'a 'b. (('a * 'b) -> ('a * 'b) -> ordering) -> set 'a -> set 'b -> set ('a * 'b)*)
+
+(*let cross s1 s2 = { (e1, e2) | forall (e1 IN s1) (e2 IN s2) | true }*)
+
+
+(* ------------------------ *)
+(* finite                   *)
+(* ------------------------ *)
+
+(*val finite : forall 'a. SetType 'a => set 'a -> bool*)
+
+
+(* ----------------------------*)
+(* fixed point                 *)
+(* --------------------------- *)
+
+(*val leastFixedPoint : forall 'a. SetType 'a 
+  => nat -> (set 'a -> set 'a) -> set 'a -> set 'a*)
+let rec leastFixedPoint dict_Basic_classes_SetType_a bound f x = 
+  (
+  if(bound =  0) then x else
+    (let bound'0 =(Nat_num.nat_monus bound ( 1)) in
+     let fx = (f x) in
+     if Pset.subset fx x then x else
+       leastFixedPoint dict_Basic_classes_SetType_a bound'0 f
+         ( Pset.(union) fx x))) 
diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_set_extra.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_set_extra.ml
new file mode 100644
index 00000000..505f2d3e
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/lem_set_extra.ml
@@ -0,0 +1,66 @@
+(*Generated by Lem from set_extra.lem.*)
+(******************************************************************************)
+(* A library for sets                                                         *)
+(*                                                                            *)
+(* It mainly follows the Haskell Set-library                                  *)
+(******************************************************************************)
+
+(* ========================================================================== *)
+(* Header                                                                     *)
+(* ========================================================================== *)
+
+open Lem_bool
+open Lem_basic_classes
+open Lem_maybe
+open Lem_function
+open Lem_num
+open Lem_list
+open Lem_sorting
+open Lem_set
+
+
+(* ----------------------------*)
+(* set choose (be careful !)   *)
+(* --------------------------- *)
+
+(*val choose : forall 'a. SetType 'a => set 'a -> 'a*)
+
+
+(* ----------------------------*)
+(* universal set               *)
+(* --------------------------- *)
+
+(*val universal : forall 'a. SetType 'a => set 'a*)
+
+
+(* ----------------------------*)
+(* toList                      *)
+(* --------------------------- *)
+
+(*val toList        : forall 'a. SetType 'a => set 'a -> list 'a*)
+
+
+(* ----------------------------*)
+(* toOrderedList               *)
+(* --------------------------- *)
+
+(* "toOrderedList" returns a sorted list. Therefore the result is (given a suitable order) deterministic.
+   Therefore, it is much preferred to "toList". However, it still is only defined for finite sets. So, please
+   use carefully and consider using set-operations instead of translating sets to lists, performing list manipulations
+   and then transforming back to sets. *) 
+
+(*val toOrderedListBy : forall 'a. ('a -> 'a -> bool) -> set 'a -> list 'a*)
+
+(*val toOrderedList : forall 'a. SetType 'a, Ord 'a => set 'a -> list 'a*)
+
+(* ----------------------------*)
+(* unbounded fixed point       *)
+(* --------------------------- *)
+
+(* Is NOT supported by the coq backend! *)
+(*val leastFixedPointUnbounded : forall 'a. SetType 'a => (set 'a -> set 'a) -> set 'a -> set 'a*)
+let rec leastFixedPointUnbounded dict_Basic_classes_SetType_a f x =   
+(let fx = (f x) in
+   if Pset.subset fx x then x
+   else leastFixedPointUnbounded 
+  dict_Basic_classes_SetType_a f ( Pset.(union) fx x))
diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_set_helpers.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_set_helpers.ml
new file mode 100644
index 00000000..25aa739f
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/lem_set_helpers.ml
@@ -0,0 +1,38 @@
+(*Generated by Lem from set_helpers.lem.*)
+(******************************************************************************)
+(* Helper functions for sets                                                  *)
+(******************************************************************************)
+
+(* Usually there is a something.lem file containing the main definitions and a 
+   something_extra.lem one containing functions that might cause problems for
+   some backends or are just seldomly used.
+
+   For sets the situation is different. folding is not well defined, since it
+   is only sensibly defined for finite sets and it the traversel 
+   order is underspecified. *) 
+
+(* ========================================================================== *)
+(* Header                                                                     *)
+(* ========================================================================== *)
+
+open Lem_bool
+open Lem_basic_classes
+open Lem_maybe
+open Lem_function
+open Lem_num
+
+(* ------------------------ *)
+(* fold                     *)
+(* ------------------------ *)
+
+(* fold is suspicious, because if given a function, for which
+   the order, in which the arguments are given, matters, it's
+   results are undefined. On the other hand, it is very handy to
+   define other - non suspicious functions. 
+
+   Moreover, fold is central for OCaml, size it is used to
+   compile set comprehensions *)
+
+(*val fold : forall 'a 'b. ('a -> 'b -> 'b) -> set 'a -> 'b -> 'b*)
+
+
diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_sorting.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_sorting.ml
new file mode 100644
index 00000000..fa16f70c
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/lem_sorting.ml
@@ -0,0 +1,83 @@
+(*Generated by Lem from sorting.lem.*)
+
+
+open Lem_bool
+open Lem_basic_classes
+open Lem_maybe
+open Lem_list
+open Lem_num
+
+(* ------------------------- *)
+(* permutations              *)
+(* ------------------------- *)
+
+(*val isPermutation : forall 'a. Eq 'a => list 'a -> list 'a -> bool*)
+(*val isPermutationBy : forall 'a. ('a -> 'a -> bool) -> list 'a -> list 'a -> bool*)
+
+let rec isPermutationBy eq l1 l2 = ((match l1 with
+  | [] -> list_null l2
+  | (x :: xs) -> begin
+      (match list_delete_first (eq x) l2 with
+        | None -> false
+        | Some ys -> isPermutationBy eq xs ys
+      )
+    end
+))
+
+
+
+(* ------------------------- *)
+(* isSorted                  *)
+(* ------------------------- *)
+
+(* isSortedBy R l 
+   checks, whether the list l is sorted by ordering R. 
+   R should represent an order, i.e. it should be transitive.
+   Different backends defined "isSorted" slightly differently. However,
+   the definitions coincide for transitive R. Therefore there is the
+   following restriction:
+
+   WARNING: Use isSorted and isSortedBy only with transitive relations!
+*)
+
+(*val isSorted : forall 'a. Ord 'a => list 'a -> bool*)
+(*val isSortedBy : forall 'a. ('a -> 'a -> bool) -> list 'a -> bool*)
+
+(* DPM: rejigged the definition with a nested match to get past Coq's termination checker. *)
+let rec isSortedBy cmp l = ((match l with
+  | [] -> true
+  | x1 :: xs ->
+    (match xs with
+      | [] -> true
+      | x2 :: _ -> (cmp x1 x2 && isSortedBy cmp xs)
+    )
+))
+
+
+(* ----------------------- *)
+(* insertion sort          *)
+(* ----------------------- *) 
+
+(*val insert : forall 'a. Ord 'a => 'a -> list 'a -> list 'a*)
+(*val insertBy : forall 'a. ('a -> 'a -> bool) -> 'a -> list 'a -> list 'a*)
+
+(*val insertSort: forall 'a. Ord 'a => list 'a -> list 'a*)
+(*val insertSortBy: forall 'a. ('a -> 'a -> bool) -> list 'a -> list 'a*)
+
+let rec insertBy cmp e l = ((match l with
+  | [] -> [e]
+  | x :: xs -> if cmp x e then x :: (insertBy cmp e xs) else (e :: (x :: xs))
+))
+
+let insertSortBy cmp l = (List.fold_left (fun l e -> insertBy cmp e l) [] l)
+
+
+(* ----------------------- *)
+(* general sorting         *)
+(* ----------------------- *) 
+
+(*val sort: forall 'a. Ord 'a => list 'a -> list 'a*)
+(*val sortBy: forall 'a. ('a -> 'a -> bool) -> list 'a -> list 'a*)
+(*val sortByOrd: forall 'a. ('a -> 'a -> ordering) -> list 'a -> list 'a*)
+
+
diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_string.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_string.ml
new file mode 100644
index 00000000..f193f7dd
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/lem_string.ml
@@ -0,0 +1,53 @@
+(*Generated by Lem from string.lem.*)
+
+
+open Lem_bool
+open Lem_basic_classes
+open Lem_list
+open Xstring
+
+(* ------------------------------------------- *)
+(* translations between strings and char lists *)
+(* ------------------------------------------- *)
+
+(*val toCharList : string -> list char*)
+
+(*val toString : list char -> string*)
+
+
+(* ----------------------- *)
+(* generating strings      *)
+(* ----------------------- *)
+
+(*val makeString : nat -> char -> string*)
+(*let makeString len c = toString (replicate len c)*)
+
+(* ----------------------- *)
+(* length                  *)
+(* ----------------------- *)
+
+(*val stringLength : string -> nat*)
+
+(* ----------------------- *)
+(* string concatenation    *)
+(* ----------------------- *)
+
+(*val ^ [stringAppend] : string -> string -> string*)
+
+
+(* ----------------------------*)
+(* setting up pattern matching *)
+(* --------------------------- *)
+
+(*val string_case : forall 'a. string -> 'a -> (char -> string -> 'a) -> 'a*)
+
+(*let string_case s c_empty c_cons = 
+  match (toCharList s) with
+    | [] -> c_empty
+    | c :: cs -> c_cons c (toString cs)
+  end*)
+
+(*val empty_string : string*)
+
+(*val cons_string : char -> string -> string*)
+
diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_string_extra.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_string_extra.ml
new file mode 100644
index 00000000..a3c8fe7b
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/lem_string_extra.ml
@@ -0,0 +1,91 @@
+(*Generated by Lem from string_extra.lem.*)
+(******************************************************************************)
+(* String functions                                                           *)
+(******************************************************************************)
+
+open Lem_basic_classes
+open Lem_num
+open Lem_list
+open Lem_string
+open Lem_list_extra
+
+
+(******************************************************************************)
+(* Character's to numbers                                                     *)
+(******************************************************************************)
+
+(*val ord : char -> nat*)
+
+(*val chr : nat -> char*)
+
+(******************************************************************************)
+(* Converting to strings                                                      *)
+(******************************************************************************)
+
+type 'a show_class={
+  show_method : 'a -> string
+}
+
+(*val natToStringHelper : nat -> list char -> list char*)
+let rec natToStringHelper n acc =  
+(if n = 0 then
+    acc
+  else
+    natToStringHelper (n / 10) (Char.chr ((n mod  10) + 48) :: acc))
+
+(*val natToString : nat -> string*)
+let natToString n = (Xstring.implode (natToStringHelper n []))
+
+let instance_String_extra_Show_nat_dict =({
+
+  show_method = natToString})
+
+(*val naturalToStringHelper : natural -> list char -> list char*)
+let rec naturalToStringHelper n acc =  
+(if Big_int.eq_big_int n(Big_int.big_int_of_int 0) then
+    acc
+  else
+    naturalToStringHelper ( Big_int.div_big_int n(Big_int.big_int_of_int 10)) (Char.chr (Big_int.int_of_big_int ( Big_int.add_big_int (Big_int.mod_big_int n(Big_int.big_int_of_int 10))(Big_int.big_int_of_int 48))) :: acc))
+
+(*val naturalToString : natural -> string*)
+let naturalToString n = (Xstring.implode (naturalToStringHelper n []))
+
+let instance_String_extra_Show_Num_natural_dict =({
+
+  show_method = naturalToString})
+
+
+(******************************************************************************)
+(* List-like operations                                                       *)
+(******************************************************************************)
+
+(*val nth : string -> nat -> char*)
+(*let nth s n = List_extra.nth (toCharList s) n*)
+
+(*val stringConcat : list string -> string*)
+(*let stringConcat s =
+  List.foldr (^) "" s*)
+
+(******************************************************************************)
+(* String comparison                                                          *)
+(******************************************************************************)
+
+(*val stringCompare : string -> string -> ordering*)
+
+let stringLess x y = (Lem.orderingIsLess (compare x y))
+let stringLessEq x y = (not (Lem.orderingIsGreater (compare x y)))
+let stringGreater x y = (stringLess y x)
+let stringGreaterEq x y = (stringLessEq y x)
+
+let instance_Basic_classes_Ord_string_dict =({
+
+  compare_method = compare;
+
+  isLess_method = stringLess;
+
+  isLessEqual_method = stringLessEq;
+
+  isGreater_method = stringGreater;
+
+  isGreaterEqual_method = stringGreaterEq})
+ 
diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_tuple.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_tuple.ml
new file mode 100644
index 00000000..8b7aec27
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/lem_tuple.ml
@@ -0,0 +1,41 @@
+(*Generated by Lem from tuple.lem.*)
+ 
+
+open Lem_bool
+open Lem_basic_classes
+
+(* ----------------------- *)
+(* fst                     *)
+(* ----------------------- *)
+
+(*val fst : forall 'a 'b. 'a * 'b -> 'a*)
+(*let fst (v1, v2) = v1*)
+
+(* ----------------------- *)
+(* snd                     *)
+(* ----------------------- *)
+
+(*val snd : forall 'a 'b. 'a * 'b -> 'b*)
+(*let snd (v1, v2) = v2*)
+
+
+(* ----------------------- *)
+(* curry                   *)
+(* ----------------------- *)
+
+(*val curry : forall 'a 'b 'c. ('a * 'b -> 'c) -> ('a -> 'b -> 'c)*)
+
+(* ----------------------- *)
+(* uncurry                 *)
+(* ----------------------- *)
+
+(*val uncurry : forall 'a 'b 'c. ('a -> 'b -> 'c) -> ('a * 'b -> 'c)*)
+
+
+(* ----------------------- *)
+(* swap                    *)
+(* ----------------------- *)
+
+(*val swap : forall 'a 'b. ('a * 'b) -> ('b * 'a)*) 
+(*let swap (v1, v2) = (v2, v1)*)
+
diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_word.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_word.ml
new file mode 100644
index 00000000..b446f885
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/lem_word.ml
@@ -0,0 +1,731 @@
+(*Generated by Lem from word.lem.*)
+
+
+open Lem_bool
+open Lem_maybe
+open Lem_num
+open Lem_basic_classes
+open Lem_list
+
+
+(* ========================================================================== *)
+(* Define general purpose word, i.e. sequences of bits of arbitrary length    *)
+(* ========================================================================== *)
+
+type bitSequence = BitSeq of 
+    int option  * (* length of the sequence, Nothing means infinite length *)
+   bool * bool       (* sign of the word, used to fill up after concrete value is exhausted *)
+   list    (* the initial part of the sequence, least significant bit first *)
+
+(*val bitSeqEq : bitSequence -> bitSequence -> bool*)
+let instance_Basic_classes_Eq_Word_bitSequence_dict =({
+
+  isEqual_method = (=);
+
+  isInequal_method = (fun n1 n2->not (n1 = n2))})
+
+(*val boolListFrombitSeq : nat -> bitSequence -> list bool*)
+
+let rec boolListFrombitSeqAux n s bl =  
+(if n = 0 then [] else
+  (match bl with
+    | []       -> replicate n s
+    | b :: bl' -> b :: (boolListFrombitSeqAux (Nat_num.nat_monus n( 1)) s bl')
+  ))
+
+let boolListFrombitSeq n (BitSeq( _, s, bl)) = (boolListFrombitSeqAux n s bl)
+
+
+(*val bitSeqFromBoolList : list bool -> maybe bitSequence*)
+let bitSeqFromBoolList bl =  
+((match dest_init bl with
+    | None -> None
+    | Some (bl', s) -> Some (BitSeq( (Some (List.length bl)), s, bl'))
+  ))
+
+
+(* cleans up the representation of a bitSequence without changing its semantics *)
+(*val cleanBitSeq : bitSequence -> bitSequence*)
+let cleanBitSeq (BitSeq( len, s, bl)) = ((match len with
+  | None -> (BitSeq( len, s, (List.rev (dropWhile ((=) s) (List.rev bl)))))
+  | Some n  -> (BitSeq( len, s, (List.rev (dropWhile ((=) s) (List.rev (Lem_list.take (Nat_num.nat_monus n( 1)) bl))))))
+))
+
+
+(*val bitSeqTestBit : bitSequence -> nat -> maybe bool*)
+let bitSeqTestBit (BitSeq( len, s, bl)) pos =  
+ ((match len with
+    | None -> if pos < List.length bl then list_index bl pos else Some s
+    | Some l -> if (pos >= l) then None else
+                if ((pos = ( Nat_num.nat_monus l( 1))) || (pos >= List.length bl)) then Some s else
+                list_index bl pos
+  ))
+
+(*val bitSeqSetBit : bitSequence -> nat -> bool -> bitSequence*)
+let bitSeqSetBit (BitSeq( len, s, bl)) pos v =  
+(let bl' = (if (pos < List.length bl) then bl else  List.append bl (replicate pos s)) in
+  let bl'' = (Lem_list.list_update bl' pos v) in
+  let bs' = (BitSeq( len, s, bl'')) in
+  cleanBitSeq bs')
+
+
+(*val resizeBitSeq : maybe nat -> bitSequence -> bitSequence*)
+let resizeBitSeq new_len bs =  
+(let (BitSeq( len, s, bl)) = (cleanBitSeq bs) in
+  let shorten_opt = ((match (new_len, len) with
+     | (None, _) -> None
+     | (Some l1, None) -> Some l1
+     | (Some l1, Some l2) -> if (l1 < l2) then Some l1 else None
+  )) in
+  (match shorten_opt with
+    | None -> BitSeq( new_len, s, bl)
+    | Some l1 -> (
+        let bl' = (Lem_list.take l1 ( List.append bl [s])) in
+        (match dest_init bl' with
+          | None -> (BitSeq( len, s, bl)) (* do nothing if size 0 is requested *)
+          | Some (bl'', s') -> cleanBitSeq (BitSeq( new_len, s', bl''))
+	))
+  )) 
+
+(*val bitSeqNot : bitSequence -> bitSequence*)
+let bitSeqNot (BitSeq( len, s, bl)) = (BitSeq( len, (not s), (List.map not bl)))
+
+(*val bitSeqBinop : (bool -> bool -> bool) -> bitSequence -> bitSequence -> bitSequence*)
+
+(*val bitSeqBinopAux : (bool -> bool -> bool) -> bool -> list bool -> bool -> list bool -> list bool*)
+let rec bitSeqBinopAux binop s1 bl1 s2 bl2 =  
+((match (bl1, bl2) with
+    | ([], []) -> []
+    | (b1 :: bl1', []) -> (binop b1 s2) :: bitSeqBinopAux binop s1 bl1' s2 []
+    | ([], b2 :: bl2') -> (binop s1 b2) :: bitSeqBinopAux binop s1 []   s2 bl2'
+    | (b1 :: bl1', b2 :: bl2') -> (binop b1 b2) :: bitSeqBinopAux binop s1 bl1' s2 bl2'
+  ))
+
+let bitSeqBinop binop bs1 bs2 = (
+  let (BitSeq( len1, s1, bl1)) = (cleanBitSeq bs1) in
+  let (BitSeq( len2, s2, bl2)) = (cleanBitSeq bs2) in
+
+  let len = ((match (len1, len2) with
+    | (Some l1, Some l2) -> Some (max l1 l2)
+    | _ -> None
+  )) in
+  let s = (binop s1 s2) in
+  let bl = (bitSeqBinopAux binop s1 bl1 s2 bl2) in
+  cleanBitSeq (BitSeq( len, s, bl))
+)
+
+let bitSeqAnd = (bitSeqBinop (&&))
+let bitSeqOr = (bitSeqBinop (||))
+let bitSeqXor = (bitSeqBinop (fun b1 b2->not (b1 = b2)))
+
+(*val bitSeqShiftLeft : bitSequence -> nat -> bitSequence*)
+let bitSeqShiftLeft (BitSeq( len, s, bl)) n = (cleanBitSeq (BitSeq( len, s, ( List.append(replicate n false) bl))))
+
+(*val bitSeqArithmeticShiftRight : bitSequence -> nat -> bitSequence*)
+let bitSeqArithmeticShiftRight bs n =  
+ (let (BitSeq( len, s, bl)) = (cleanBitSeq bs) in
+  cleanBitSeq (BitSeq( len, s, (drop n bl))))
+
+(*val bitSeqLogicalShiftRight : bitSequence -> nat -> bitSequence*)
+let bitSeqLogicalShiftRight bs n =  
+ (if (n = 0) then cleanBitSeq bs else
+  let (BitSeq( len, s, bl)) = (cleanBitSeq bs) in
+  (match len with
+    | None -> cleanBitSeq (BitSeq( len, s, (drop n bl)))
+    | Some l -> cleanBitSeq (BitSeq( len, false, ( List.append(drop n bl) (replicate l s))))
+  ))
+
+
+(* integerFromBoolList sign bl creates an integer from a list of bits
+   (least significant bit first) and an explicitly given sign bit.
+   It uses two's complement encoding. *)
+(*val integerFromBoolList : (bool * list bool) -> integer*)
+
+let rec integerFromBoolListAux (acc : Big_int.big_int) (bl : bool list) =  
+ ((match bl with 
+    | [] -> acc
+    | (true :: bl') -> integerFromBoolListAux ( Big_int.add_big_int( Big_int.mult_big_int acc(Big_int.big_int_of_int 2))(Big_int.big_int_of_int 1)) bl'
+    | (false :: bl') -> integerFromBoolListAux ( Big_int.mult_big_int acc(Big_int.big_int_of_int 2)) bl'
+  ))
+
+let integerFromBoolList (sign, bl) =   
+ (if sign then 
+     Big_int.minus_big_int( Big_int.add_big_int(integerFromBoolListAux(Big_int.big_int_of_int 0) (List.rev_map not bl))(Big_int.big_int_of_int 1))
+   else integerFromBoolListAux(Big_int.big_int_of_int 0) (List.rev bl))
+
+(* [boolListFromInteger i] creates a sign bit and a list of booleans from an integer. The len_opt tells it when to stop.*)
+(*val boolListFromInteger :    integer -> bool * list bool*)
+
+let rec boolListFromNatural acc (remainder : Big_int.big_int) = 
+(if ( Big_int.gt_big_int remainder(Big_int.big_int_of_int 0)) then 
+   (boolListFromNatural (( Big_int.eq_big_int( Big_int.mod_big_int remainder(Big_int.big_int_of_int 2))(Big_int.big_int_of_int 1)) :: acc) 
+      ( Big_int.div_big_int remainder(Big_int.big_int_of_int 2)))
+ else
+   List.rev acc)
+
+let boolListFromInteger (i : Big_int.big_int) =  
+ (if ( Big_int.lt_big_int i(Big_int.big_int_of_int 0)) then
+    (true, List.map not (boolListFromNatural [] (Big_int.abs_big_int (Big_int.minus_big_int( Big_int.add_big_int i(Big_int.big_int_of_int 1))))))
+  else
+    (false, boolListFromNatural [] (Big_int.abs_big_int i)))
+
+
+(* [bitSeqFromInteger len_opt i] encodes [i] as a bitsequence with [len_opt] bits. If there are not enough
+   bits, truncation happens *)
+(*val bitSeqFromInteger : maybe nat -> integer -> bitSequence*)
+let bitSeqFromInteger len_opt i =  
+(let (s, bl) = (boolListFromInteger i) in
+  resizeBitSeq len_opt (BitSeq( None, s, bl)))
+
+
+(*val integerFromBitSeq : bitSequence -> integer*)
+let integerFromBitSeq bs =  
+(let (BitSeq( len, s, bl)) = (cleanBitSeq bs) in
+  integerFromBoolList (s, bl))
+
+
+(* Now we can via translation to integers map arithmetic operations to bitSequences *)
+
+(*val bitSeqArithUnaryOp : (integer -> integer) -> bitSequence -> bitSequence*)
+let bitSeqArithUnaryOp uop bs =  
+(let (BitSeq( len, _, _)) = bs in
+  bitSeqFromInteger len (uop (integerFromBitSeq bs)))
+
+(*val bitSeqArithBinOp : (integer -> integer -> integer) -> bitSequence -> bitSequence -> bitSequence*)
+let bitSeqArithBinOp binop bs1 bs2 =  
+(let (BitSeq( len1, _, _)) = bs1 in
+  let (BitSeq( len2, _, _)) = bs2 in
+  let len = ((match (len1, len2) with 
+    | (Some l1, Some l2) -> Some (max l1 l2)
+    | _ -> None
+  )) in
+  bitSeqFromInteger len (binop (integerFromBitSeq bs1) (integerFromBitSeq bs2)))
+
+(*val bitSeqArithBinTest : forall 'a. (integer -> integer -> 'a) -> bitSequence -> bitSequence -> 'a*)
+let bitSeqArithBinTest binop bs1 bs2 = (binop (integerFromBitSeq bs1) (integerFromBitSeq bs2))
+
+
+(* now instantiate the number interface for bit-sequences *)
+
+(*val bitSeqFromNumeral : numeral -> bitSequence*)
+
+(*val bitSeqLess : bitSequence -> bitSequence -> bool*)
+let bitSeqLess bs1 bs2 = (bitSeqArithBinTest Big_int.lt_big_int bs1 bs2)
+
+(*val bitSeqLessEqual : bitSequence -> bitSequence -> bool*)
+let bitSeqLessEqual bs1 bs2 = (bitSeqArithBinTest Big_int.le_big_int bs1 bs2)
+
+(*val bitSeqGreater : bitSequence -> bitSequence -> bool*)
+let bitSeqGreater bs1 bs2 = (bitSeqArithBinTest Big_int.gt_big_int bs1 bs2)
+
+(*val bitSeqGreaterEqual : bitSequence -> bitSequence -> bool*)
+let bitSeqGreaterEqual bs1 bs2 = (bitSeqArithBinTest Big_int.ge_big_int bs1 bs2)
+
+(*val bitSeqCompare : bitSequence -> bitSequence -> ordering*)
+let bitSeqCompare bs1 bs2 = (bitSeqArithBinTest Big_int.compare_big_int bs1 bs2)
+
+let instance_Basic_classes_Ord_Word_bitSequence_dict =({
+
+  compare_method = bitSeqCompare;
+
+  isLess_method = bitSeqLess;
+
+  isLessEqual_method = bitSeqLessEqual;
+
+  isGreater_method = bitSeqGreater;
+
+  isGreaterEqual_method = bitSeqGreaterEqual})
+
+let instance_Basic_classes_SetType_Word_bitSequence_dict =({
+
+  setElemCompare_method = bitSeqCompare})
+
+(* arithmetic negation, don't mix up with bitwise negation *)
+(*val bitSeqNegate : bitSequence -> bitSequence*) 
+let bitSeqNegate bs = (bitSeqArithUnaryOp Big_int.minus_big_int bs)
+
+let instance_Num_NumNegate_Word_bitSequence_dict =({
+
+  numNegate_method = bitSeqNegate})
+
+
+(*val bitSeqAdd : bitSequence -> bitSequence -> bitSequence*)
+let bitSeqAdd bs1 bs2 = (bitSeqArithBinOp Big_int.add_big_int bs1 bs2)
+
+let instance_Num_NumAdd_Word_bitSequence_dict =({
+
+  numAdd_method = bitSeqAdd})
+
+(*val bitSeqMinus : bitSequence -> bitSequence -> bitSequence*)
+let bitSeqMinus bs1 bs2 = (bitSeqArithBinOp Big_int.sub_big_int bs1 bs2)
+
+let instance_Num_NumMinus_Word_bitSequence_dict =({
+
+  numMinus_method = bitSeqMinus})
+
+(*val bitSeqSucc : bitSequence -> bitSequence*)
+let bitSeqSucc bs = (bitSeqArithUnaryOp Big_int.succ_big_int bs)
+
+let instance_Num_NumSucc_Word_bitSequence_dict =({
+
+  succ_method = bitSeqSucc})
+
+(*val bitSeqPred : bitSequence -> bitSequence*)
+let bitSeqPred bs = (bitSeqArithUnaryOp Big_int.pred_big_int bs)
+
+let instance_Num_NumPred_Word_bitSequence_dict =({
+
+  pred_method = bitSeqPred})
+
+(*val bitSeqMult : bitSequence -> bitSequence -> bitSequence*)
+let bitSeqMult bs1 bs2 = (bitSeqArithBinOp Big_int.mult_big_int bs1 bs2)
+
+let instance_Num_NumMult_Word_bitSequence_dict =({
+
+  numMult_method = bitSeqMult})
+
+
+(*val bitSeqPow : bitSequence -> nat -> bitSequence*)
+let bitSeqPow bs n = (bitSeqArithUnaryOp (fun i -> Big_int.power_big_int_positive_int i n) bs)
+
+let instance_Num_NumPow_Word_bitSequence_dict =({
+
+  numPow_method = bitSeqPow})
+
+(*val bitSeqDiv : bitSequence -> bitSequence -> bitSequence*)
+let bitSeqDiv bs1 bs2 = (bitSeqArithBinOp Big_int.div_big_int bs1 bs2)
+
+let instance_Num_NumIntegerDivision_Word_bitSequence_dict =({
+
+  div_method = bitSeqDiv})
+
+let instance_Num_NumDivision_Word_bitSequence_dict =({
+
+  numDivision_method = bitSeqDiv})
+
+(*val bitSeqMod : bitSequence -> bitSequence -> bitSequence*)
+let bitSeqMod bs1 bs2 = (bitSeqArithBinOp Big_int.mod_big_int bs1 bs2)
+
+let instance_Num_NumRemainder_Word_bitSequence_dict =({
+
+  mod_method = bitSeqMod})
+
+(*val bitSeqMin : bitSequence -> bitSequence -> bitSequence*)
+let bitSeqMin bs1 bs2 = (bitSeqArithBinOp Big_int.min_big_int bs1 bs2)
+
+(*val bitSeqMax : bitSequence -> bitSequence -> bitSequence*)
+let bitSeqMax bs1 bs2 = (bitSeqArithBinOp Big_int.max_big_int bs1 bs2)
+
+let instance_Basic_classes_OrdMaxMin_Word_bitSequence_dict =({
+
+  max_method = bitSeqMax;
+
+  min_method = bitSeqMin})
+
+
+
+
+(* ========================================================================== *)
+(* Interface for bitoperations                                                *)
+(* ========================================================================== *)
+
+type 'a wordNot_class= {
+  lnot_method : 'a -> 'a
+}
+
+type 'a wordAnd_class= {
+  land_method  : 'a -> 'a -> 'a
+}
+
+type 'a wordOr_class= {
+  lor_method : 'a -> 'a -> 'a
+}
+
+
+type 'a wordXor_class= {
+  lxor_method : 'a -> 'a -> 'a
+}
+
+type 'a wordLsl_class= {
+  lsl_method : 'a -> int -> 'a
+}
+
+type 'a wordLsr_class= {
+  lsr_method : 'a -> int -> 'a
+}
+
+type 'a wordAsr_class= {
+  asr_method : 'a -> int -> 'a
+}
+
+(* ----------------------- *)
+(* bitSequence             *)
+(* ----------------------- *)
+
+let instance_Word_WordNot_Word_bitSequence_dict =({
+
+  lnot_method = bitSeqNot})
+
+let instance_Word_WordAnd_Word_bitSequence_dict =({
+
+  land_method = bitSeqAnd})
+
+let instance_Word_WordOr_Word_bitSequence_dict =({
+
+  lor_method = bitSeqOr})
+
+let instance_Word_WordXor_Word_bitSequence_dict =({
+
+  lxor_method = bitSeqXor})
+
+let instance_Word_WordLsl_Word_bitSequence_dict =({
+
+  lsl_method = bitSeqShiftLeft})
+
+let instance_Word_WordLsr_Word_bitSequence_dict =({
+
+  lsr_method = bitSeqLogicalShiftRight})
+
+let instance_Word_WordAsr_Word_bitSequence_dict =({
+
+  asr_method = bitSeqArithmeticShiftRight})
+
+
+(* ----------------------- *)
+(* int32                   *)
+(* ----------------------- *)
+
+(*val int32Lnot : int32 -> int32*) (* XXX: fix *)
+
+let instance_Word_WordNot_Num_int32_dict =({
+
+  lnot_method = Int32.lognot})
+
+
+(*val int32Lor  : int32 -> int32 -> int32*) (* XXX: fix *)
+
+let instance_Word_WordOr_Num_int32_dict =({
+
+  lor_method = Int32.logor})
+
+(*val int32Lxor : int32 -> int32 -> int32*) (* XXX: fix *)
+
+let instance_Word_WordXor_Num_int32_dict =({
+
+  lxor_method = Int32.logxor})
+
+(*val int32Land : int32 -> int32 -> int32*) (* XXX: fix *)
+
+let instance_Word_WordAnd_Num_int32_dict =({
+
+  land_method = Int32.logand})
+
+(*val int32Lsl  : int32 -> nat -> int32*) (* XXX: fix *)
+
+let instance_Word_WordLsl_Num_int32_dict =({
+
+  lsl_method = Int32.shift_left})
+
+(*val int32Lsr  : int32 -> nat -> int32*) (* XXX: fix *)
+
+let instance_Word_WordLsr_Num_int32_dict =({
+
+  lsr_method = Int32.shift_right_logical})
+
+
+(*val int32Asr  : int32 -> nat -> int32*) (* XXX: fix *)
+
+let instance_Word_WordAsr_Num_int32_dict =({
+
+  asr_method = Int32.shift_right})
+
+
+(* ----------------------- *)
+(* int64                   *)
+(* ----------------------- *)
+
+(*val int64Lnot : int64 -> int64*) (* XXX: fix *)
+
+let instance_Word_WordNot_Num_int64_dict =({
+
+  lnot_method = Int64.lognot})
+
+(*val int64Lor  : int64 -> int64 -> int64*) (* XXX: fix *)
+
+let instance_Word_WordOr_Num_int64_dict =({
+
+  lor_method = Int64.logor})
+
+(*val int64Lxor : int64 -> int64 -> int64*) (* XXX: fix *)
+
+let instance_Word_WordXor_Num_int64_dict =({
+
+  lxor_method = Int64.logxor})
+
+(*val int64Land : int64 -> int64 -> int64*) (* XXX: fix *)
+
+let instance_Word_WordAnd_Num_int64_dict =({
+
+  land_method = Int64.logand})
+
+(*val int64Lsl  : int64 -> nat -> int64*) (* XXX: fix *)
+
+let instance_Word_WordLsl_Num_int64_dict =({
+
+  lsl_method = Int64.shift_left})
+
+(*val int64Lsr  : int64 -> nat -> int64*) (* XXX: fix *)
+
+let instance_Word_WordLsr_Num_int64_dict =({
+
+  lsr_method = Int64.shift_right_logical})
+
+(*val int64Asr  : int64 -> nat -> int64*) (* XXX: fix *)
+
+let instance_Word_WordAsr_Num_int64_dict =({
+
+  asr_method = Int64.shift_right})
+
+
+(* ----------------------- *)
+(* Words via bit sequences *)
+(* ----------------------- *)
+
+(*val defaultLnot : forall 'a. (bitSequence -> 'a) -> ('a -> bitSequence) -> 'a -> 'a*) 
+let defaultLnot fromBitSeq toBitSeq x = (fromBitSeq (bitSeqNegate (toBitSeq x)))
+
+(*val defaultLand : forall 'a. (bitSequence -> 'a) -> ('a -> bitSequence) -> 'a -> 'a -> 'a*)
+let defaultLand fromBitSeq toBitSeq x1 x2 = (fromBitSeq (bitSeqAnd (toBitSeq x1) (toBitSeq x2)))
+
+(*val defaultLor : forall 'a. (bitSequence -> 'a) -> ('a -> bitSequence) -> 'a -> 'a -> 'a*)
+let defaultLor fromBitSeq toBitSeq x1 x2 = (fromBitSeq (bitSeqOr (toBitSeq x1) (toBitSeq x2)))
+
+(*val defaultLxor : forall 'a. (bitSequence -> 'a) -> ('a -> bitSequence) -> 'a -> 'a -> 'a*)
+let defaultLxor fromBitSeq toBitSeq x1 x2 = (fromBitSeq (bitSeqXor (toBitSeq x1) (toBitSeq x2)))
+
+(*val defaultLsl : forall 'a. (bitSequence -> 'a) -> ('a -> bitSequence) -> 'a -> nat -> 'a*)
+let defaultLsl fromBitSeq toBitSeq x n = (fromBitSeq (bitSeqShiftLeft (toBitSeq x) n))
+
+(*val defaultLsr : forall 'a. (bitSequence -> 'a) -> ('a -> bitSequence) -> 'a -> nat -> 'a*)
+let defaultLsr fromBitSeq toBitSeq x n = (fromBitSeq (bitSeqLogicalShiftRight (toBitSeq x) n))
+
+(*val defaultAsr : forall 'a. (bitSequence -> 'a) -> ('a -> bitSequence) -> 'a -> nat -> 'a*)
+let defaultAsr fromBitSeq toBitSeq x n = (fromBitSeq (bitSeqArithmeticShiftRight (toBitSeq x) n))
+
+(* ----------------------- *)
+(* integer                 *)
+(* ----------------------- *)
+
+(*val integerLnot : integer -> integer*)
+let integerLnot i = (Big_int.minus_big_int( Big_int.add_big_int i(Big_int.big_int_of_int 1)))
+
+let instance_Word_WordNot_Num_integer_dict =({
+
+  lnot_method = integerLnot})
+
+
+(*val integerLor  : integer -> integer -> integer*)
+(*let integerLor i1 i2 = defaultLor integerFromBitSeq (bitSeqFromInteger Nothing) i1 i2*)
+
+let instance_Word_WordOr_Num_integer_dict =({
+
+  lor_method = Big_int.or_big_int})
+
+(*val integerLxor : integer -> integer -> integer*)
+(*let integerLxor i1 i2 = defaultLxor integerFromBitSeq (bitSeqFromInteger Nothing) i1 i2*)
+
+let instance_Word_WordXor_Num_integer_dict =({
+
+  lxor_method = Big_int.xor_big_int})
+
+(*val integerLand : integer -> integer -> integer*)
+(*let integerLand i1 i2 = defaultLand integerFromBitSeq (bitSeqFromInteger Nothing) i1 i2*)
+
+let instance_Word_WordAnd_Num_integer_dict =({
+
+  land_method = Big_int.and_big_int})
+
+(*val integerLsl  : integer -> nat -> integer*)
+(*let integerLsl i n = defaultLsl integerFromBitSeq (bitSeqFromInteger Nothing) i n*)
+
+let instance_Word_WordLsl_Num_integer_dict =({
+
+  lsl_method = Big_int.shift_left_big_int})
+
+(*val integerAsr  : integer -> nat -> integer*)
+(*let integerAsr i n = defaultAsr integerFromBitSeq (bitSeqFromInteger Nothing) i n*)
+
+let instance_Word_WordLsr_Num_integer_dict =({
+
+  lsr_method = Big_int.shift_right_big_int})
+
+let instance_Word_WordAsr_Num_integer_dict =({
+
+  asr_method = Big_int.shift_right_big_int})
+
+
+(* ----------------------- *)
+(* int                     *)
+(* ----------------------- *)
+
+(* sometimes it is convenient to be able to perform bit-operations on ints.
+   However, since int is not well-defined (it has different size on different systems),
+   it should be used very carefully and only for operations that don't depend on the
+   bitwidth of int *)
+
+(*val intFromBitSeq : bitSequence -> int*)
+let intFromBitSeq bs = (Big_int.int_of_big_int (integerFromBitSeq (resizeBitSeq (Some( 31)) bs)))
+
+
+(*val bitSeqFromInt : int -> bitSequence*) 
+let bitSeqFromInt i = (bitSeqFromInteger (Some( 31)) (Big_int.big_int_of_int i))
+
+
+(*val intLnot : int -> int*)
+(*let intLnot i = Instance_Num_NumNegate_Num_int.~((Instance_Num_NumAdd_Num_int.+) i 1)*)
+
+let instance_Word_WordNot_Num_int_dict =({
+
+  lnot_method = lnot})
+
+(*val intLor  : int -> int -> int*)
+(*let intLor i1 i2 = defaultLor intFromBitSeq bitSeqFromInt i1 i2*)
+
+let instance_Word_WordOr_Num_int_dict =({
+
+  lor_method = (lor)})
+
+(*val intLxor : int -> int -> int*)
+(*let intLxor i1 i2 = defaultLxor intFromBitSeq bitSeqFromInt i1 i2*)
+
+let instance_Word_WordXor_Num_int_dict =({
+
+  lxor_method = (lxor)})
+
+(*val intLand : int -> int -> int*)
+(*let intLand i1 i2 = defaultLand intFromBitSeq bitSeqFromInt i1 i2*)
+
+let instance_Word_WordAnd_Num_int_dict =({
+
+  land_method = (land)})
+
+(*val intLsl  : int -> nat -> int*)
+(*let intLsl i n = defaultLsl intFromBitSeq bitSeqFromInt i n*)
+
+let instance_Word_WordLsl_Num_int_dict =({
+
+  lsl_method = (lsl)})
+
+(*val intAsr  : int -> nat -> int*)
+(*let intAsr i n = defaultAsr intFromBitSeq bitSeqFromInt i n*)
+
+let instance_Word_WordAsr_Num_int_dict =({
+
+  asr_method = (asr)})
+
+
+
+(* ----------------------- *)
+(* natural                 *)
+(* ----------------------- *)
+
+(* some operations work also on positive numbers *)
+
+(*val naturalFromBitSeq : bitSequence -> natural*)
+let naturalFromBitSeq bs = (Big_int.abs_big_int (integerFromBitSeq bs))
+
+(*val bitSeqFromNatural : maybe nat -> natural -> bitSequence*)
+let bitSeqFromNatural len n = (bitSeqFromInteger len ( n))
+
+(*val naturalLor  : natural -> natural -> natural*)
+(*let naturalLor i1 i2 = defaultLor naturalFromBitSeq (bitSeqFromNatural Nothing) i1 i2*)
+
+let instance_Word_WordOr_Num_natural_dict =({
+
+  lor_method = Big_int.or_big_int})
+
+(*val naturalLxor : natural -> natural -> natural*)
+(*let naturalLxor i1 i2 = defaultLxor naturalFromBitSeq (bitSeqFromNatural Nothing) i1 i2*)
+
+let instance_Word_WordXor_Num_natural_dict =({
+
+  lxor_method = Big_int.xor_big_int})
+
+(*val naturalLand : natural -> natural -> natural*)
+(*let naturalLand i1 i2 = defaultLand naturalFromBitSeq (bitSeqFromNatural Nothing) i1 i2*)
+
+let instance_Word_WordAnd_Num_natural_dict =({
+
+  land_method = Big_int.and_big_int})
+
+(*val naturalLsl  : natural -> nat -> natural*)
+(*let naturalLsl i n = defaultLsl naturalFromBitSeq (bitSeqFromNatural Nothing) i n*)
+
+let instance_Word_WordLsl_Num_natural_dict =({
+
+  lsl_method = Big_int.shift_left_big_int})
+
+(*val naturalAsr  : natural -> nat -> natural*)
+(*let naturalAsr i n = defaultAsr naturalFromBitSeq (bitSeqFromNatural Nothing) i n*)
+
+let instance_Word_WordLsr_Num_natural_dict =({
+
+  lsr_method = Big_int.shift_right_big_int})
+
+let instance_Word_WordAsr_Num_natural_dict =({
+
+  asr_method = Big_int.shift_right_big_int})
+
+
+(* ----------------------- *)
+(* nat                     *)
+(* ----------------------- *)
+
+(* sometimes it is convenient to be able to perform bit-operations on nats.
+   However, since nat is not well-defined (it has different size on different systems),
+   it should be used very carefully and only for operations that don't depend on the
+   bitwidth of nat *)
+
+(*val natFromBitSeq : bitSequence -> nat*)
+let natFromBitSeq bs = (Big_int.int_of_big_int (naturalFromBitSeq (resizeBitSeq (Some( 31)) bs)))
+
+
+(*val bitSeqFromNat : nat -> bitSequence*) 
+let bitSeqFromNat i = (bitSeqFromNatural (Some( 31)) (Big_int.big_int_of_int i))
+
+
+(*val natLor  : nat -> nat -> nat*)
+(*let natLor i1 i2 = defaultLor natFromBitSeq bitSeqFromNat i1 i2*)
+
+let instance_Word_WordOr_nat_dict =({
+
+  lor_method = (lor)})
+
+(*val natLxor : nat -> nat -> nat*)
+(*let natLxor i1 i2 = defaultLxor natFromBitSeq bitSeqFromNat i1 i2*)
+
+let instance_Word_WordXor_nat_dict =({
+
+  lxor_method = (lxor)})
+
+(*val natLand : nat -> nat -> nat*)
+(*let natLand i1 i2 = defaultLand natFromBitSeq bitSeqFromNat i1 i2*)
+
+let instance_Word_WordAnd_nat_dict =({
+
+  land_method = (land)})
+
+(*val natLsl  : nat -> nat -> nat*)
+(*let natLsl i n = defaultLsl natFromBitSeq bitSeqFromNat i n*)
+
+let instance_Word_WordLsl_nat_dict =({
+
+  lsl_method = (lsl)})
+
+(*val natAsr  : nat -> nat -> nat*)
+(*let natAsr i n = defaultAsr natFromBitSeq bitSeqFromNat i n*)
+
+let instance_Word_WordAsr_nat_dict =({
+
+  asr_method = (asr)})
+
diff --git a/lib/ocaml_rts/linksem/src_lem_library/nat_big_num.ml b/lib/ocaml_rts/linksem/src_lem_library/nat_big_num.ml
new file mode 100644
index 00000000..2320188c
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/nat_big_num.ml
@@ -0,0 +1,18 @@
+module BI = Big_int
+
+type num = BI.big_int
+let (<) = BI.lt_big_int
+let (<=) = BI.le_big_int
+let (>) = BI.gt_big_int
+let (>=) = BI.ge_big_int
+let (+) = BI.add_big_int
+let (-) x y =
+  let d = BI.sub_big_int x y in
+    if d < BI.zero_big_int then
+      BI.zero_big_int
+    else
+      d
+let ( * ) = BI.mult_big_int
+let (/) = BI.div_big_int
+let (mod) = BI.mod_big_int
+let string_of_num = BI.string_of_big_int
diff --git a/lib/ocaml_rts/linksem/src_lem_library/nat_big_num.mli b/lib/ocaml_rts/linksem/src_lem_library/nat_big_num.mli
new file mode 100644
index 00000000..b6f6eb63
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/nat_big_num.mli
@@ -0,0 +1,11 @@
+type num
+val (<) : num -> num -> bool
+val (<=) : num -> num -> bool
+val (>) : num -> num -> bool
+val (>=) : num -> num -> bool
+val (+) : num -> num -> num
+val (-) : num -> num -> num
+val ( * ) : num -> num -> num
+val (/) : num -> num -> num
+val (mod) : num -> num -> num
+val string_of_num : num -> string
diff --git a/lib/ocaml_rts/linksem/src_lem_library/nat_num.ml b/lib/ocaml_rts/linksem/src_lem_library/nat_num.ml
new file mode 100755
index 00000000..50165e6d
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/nat_num.ml
@@ -0,0 +1,43 @@
+type nat = int
+type natural = Big_int.big_int
+
+let nat_monus x y =
+  let d = x - y in
+    if d < 0 then
+      0
+    else
+      d
+
+let natural_monus x y =
+    (if Big_int.le_big_int x y then
+      Big_int.zero_big_int
+    else
+      (Big_int.sub_big_int x y))
+
+let nat_pred x = nat_monus x 1
+let natural_pred x = natural_monus x Big_int.unit_big_int
+
+let int_mod i n = 
+  let r = i mod n in
+  if (r < 0) then r + n else r
+
+let int_div i n = 
+  let r = i / n in
+  if (i mod n < 0) then r - 1 else r
+
+let int32_mod i n = 
+  let r = Int32.rem i n in
+  if (r < Int32.zero) then Int32.add r n else r
+
+let int32_div i n = 
+  let r = Int32.div i n in
+  if (Int32.rem i n < Int32.zero) then Int32.pred r else r
+
+let int64_mod i n = 
+  let r = Int64.rem i n in
+  if (r < Int64.zero) then Int64.add r n else r
+
+let int64_div i n = 
+  let r = Int64.div i n in
+  if (Int64.rem i n < Int64.zero) then Int64.pred r else r
+
diff --git a/lib/ocaml_rts/linksem/src_lem_library/nat_num.mli b/lib/ocaml_rts/linksem/src_lem_library/nat_num.mli
new file mode 100755
index 00000000..d918b9df
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/nat_num.mli
@@ -0,0 +1,14 @@
+type nat = int
+type natural = Big_int.big_int
+
+val natural_monus : natural -> natural -> natural
+val natural_pred : natural -> natural
+
+val nat_pred  : nat -> nat
+val nat_monus : nat -> nat -> nat
+val int_div   : int -> int -> int
+val int32_div : Int32.t -> Int32.t -> Int32.t
+val int64_div : Int64.t -> Int64.t -> Int64.t
+val int_mod   : int -> int -> int
+val int32_mod : Int32.t -> Int32.t -> Int32.t
+val int64_mod : Int64.t -> Int64.t -> Int64.t
diff --git a/lib/ocaml_rts/linksem/src_lem_library/pmap.ml b/lib/ocaml_rts/linksem/src_lem_library/pmap.ml
new file mode 100755
index 00000000..9e9f607b
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/pmap.ml
@@ -0,0 +1,321 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                           Objective Caml                            *)
+(*                                                                     *)
+(*            Xavier Leroy, projet Cristal, INRIA Rocquencourt         *)
+(*                                                                     *)
+(*  Copyright 1996 Institut National de Recherche en Informatique et   *)
+(*  en Automatique.  All rights reserved.  This file is distributed    *)
+(*  under the terms of the GNU Library General Public License, with    *)
+(*  the special exception on linking described in file ../LICENSE.     *)
+(*                                                                     *)
+(***********************************************************************)
+
+(* Modified by Susmit Sarkar 2010-11-30 *)
+(* $Id: map.ml 10468 2010-05-25 13:29:43Z frisch $ *)
+
+(* A map from ordered keys *)
+
+type ('key,'a) rep =
+    Empty
+  | Node of ('key,'a) rep * 'key * 'a * ('key,'a) rep * int
+
+let height = function
+    Empty -> 0
+  | Node(_,_,_,_,h) -> h
+
+let create l x d r =
+  let hl = height l and hr = height r in
+  Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1))
+
+let singleton x d = Node(Empty, x, d, Empty, 1)
+    
+let bal l x d r =
+  let hl = match l with Empty -> 0 | Node(_,_,_,_,h) -> h in
+  let hr = match r with Empty -> 0 | Node(_,_,_,_,h) -> h in
+  if hl > hr + 2 then begin
+    match l with
+      Empty -> invalid_arg "Map.bal"
+    | Node(ll, lv, ld, lr, _) ->
+        if height ll >= height lr then
+          create ll lv ld (create lr x d r)
+        else begin
+          match lr with
+                Empty -> invalid_arg "Map.bal"
+          | Node(lrl, lrv, lrd, lrr, _)->
+              create (create ll lv ld lrl) lrv lrd (create lrr x d r)
+        end
+  end else if hr > hl + 2 then begin
+    match r with
+      Empty -> invalid_arg "Map.bal"
+    | Node(rl, rv, rd, rr, _) ->
+        if height rr >= height rl then
+          create (create l x d rl) rv rd rr
+        else begin
+          match rl with
+            Empty -> invalid_arg "Map.bal"
+          | Node(rll, rlv, rld, rlr, _) ->
+              create (create l x d rll) rlv rld (create rlr rv rd rr)
+        end
+  end else
+    Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1))
+      
+let empty = Empty
+    
+let is_empty = function Empty -> true | _ -> false
+    
+let rec add cmp x data = function
+    Empty ->
+      Node(Empty, x, data, Empty, 1)
+  | Node(l, v, d, r, h) ->
+      let c = cmp x v in
+      if c = 0 then
+        Node(l, x, data, r, h)
+      else if c < 0 then
+        bal (add cmp x data l) v d r
+      else
+        bal l v d (add cmp x data r)
+	  
+let rec find cmp x = function
+        Empty ->
+          raise Not_found
+      | Node(l, v, d, r, _) ->
+          let c = cmp x v in
+          if c = 0 then d
+          else find cmp x (if c < 0 then l else r)
+
+let rec mem cmp x = function
+    Empty ->
+      false
+  | Node(l, v, d, r, _) ->
+      let c = cmp x v in
+      c = 0 || mem cmp x (if c < 0 then l else r)
+
+let rec min_binding = function
+    Empty -> raise Not_found
+  | Node(Empty, x, d, r, _) -> (x, d)
+  | Node(l, x, d, r, _) -> min_binding l
+
+let rec max_binding = function
+    Empty -> raise Not_found
+  | Node(l, x, d, Empty, _) -> (x, d)
+  | Node(l, x, d, r, _) -> max_binding r
+	
+let rec remove_min_binding = function
+    Empty -> invalid_arg "Map.remove_min_elt"
+  | Node(Empty, x, d, r, _) -> r
+  | Node(l, x, d, r, _) -> bal (remove_min_binding l) x d r
+
+let merge t1 t2 =
+  match (t1, t2) with
+    (Empty, t) -> t
+  | (t, Empty) -> t
+  | (_, _) ->
+      let (x, d) = min_binding t2 in
+      bal t1 x d (remove_min_binding t2)
+	
+let rec remove cmp x = function
+    Empty ->
+      Empty
+  | Node(l, v, d, r, h) ->
+      let c = cmp x v in
+      if c = 0 then
+        merge l r
+      else if c < 0 then
+        bal (remove cmp x l) v d r
+      else
+        bal l v d (remove cmp x r)
+
+let rec iter f = function
+    Empty -> ()
+  | Node(l, v, d, r, _) ->
+      iter f l; f v d; iter f r
+
+let rec map f = function
+    Empty ->
+      Empty
+  | Node(l, v, d, r, h) ->
+      let l' = map f l in
+      let d' = f d in
+      let r' = map f r in
+      Node(l', v, d', r', h)
+	
+let rec mapi f = function
+    Empty ->
+      Empty
+  | Node(l, v, d, r, h) ->
+      let l' = mapi f l in
+      let d' = f v d in
+      let r' = mapi f r in
+      Node(l', v, d', r', h)
+
+let rec fold f m accu =
+  match m with
+    Empty -> accu
+  | Node(l, v, d, r, _) ->
+      fold f r (f v d (fold f l accu))
+
+let rec for_all p = function
+    Empty -> true
+  | Node(l, v, d, r, _) -> p v d && for_all p l && for_all p r
+
+let rec exists p = function
+    Empty -> false
+  | Node(l, v, d, r, _) -> p v d || exists p l || exists p r
+      
+let filter cmp p s =
+  let rec filt accu = function
+    | Empty -> accu
+    | Node(l, v, d, r, _) ->
+        filt (filt (if p v d then add cmp v d accu else accu) l) r in
+  filt Empty s
+
+let partition cmp p s =
+  let rec part (t, f as accu) = function
+    | Empty -> accu
+    | Node(l, v, d, r, _) ->
+        part (part (if p v d then (add cmp v d t, f) else (t, add cmp v d f)) l) r in
+  part (Empty, Empty) s
+    
+    (* Same as create and bal, but no assumptions are made on the
+       relative heights of l and r. *)
+
+let rec join cmp l v d r =
+  match (l, r) with
+    (Empty, _) -> add cmp v d r
+  | (_, Empty) -> add cmp v d l
+  | (Node(ll, lv, ld, lr, lh), Node(rl, rv, rd, rr, rh)) ->
+      if lh > rh + 2 then bal ll lv ld (join cmp lr v d r) else
+      if rh > lh + 2 then bal (join cmp l v d rl) rv rd rr else
+      create l v d r
+
+	(* Merge two trees l and r into one.
+	   All elements of l must precede the elements of r.
+	   No assumption on the heights of l and r. *)
+
+let concat cmp t1 t2 =
+  match (t1, t2) with
+    (Empty, t) -> t
+  | (t, Empty) -> t
+  | (_, _) ->
+      let (x, d) = min_binding t2 in
+      join cmp t1 x d (remove_min_binding t2)
+
+let concat_or_join cmp t1 v d t2 =
+  match d with
+  | Some d -> join cmp t1 v d t2
+  | None -> concat cmp t1 t2
+
+let rec split cmp x = function
+    Empty ->
+      (Empty, None, Empty)
+  | Node(l, v, d, r, _) ->
+      let c = cmp x v in
+      if c = 0 then (l, Some d, r)
+      else if c < 0 then
+        let (ll, pres, rl) = split cmp x l in (ll, pres, join cmp rl v d r)
+      else
+        let (lr, pres, rr) = split cmp x r in (join cmp l v d lr, pres, rr)
+	  
+let rec merge cmp f s1 s2 =
+  match (s1, s2) with
+    (Empty, Empty) -> Empty
+  | (Node (l1, v1, d1, r1, h1), _) when h1 >= height s2 ->
+      let (l2, d2, r2) = split cmp v1 s2 in
+      concat_or_join cmp (merge cmp f l1 l2) v1 (f v1 (Some d1) d2) (merge cmp f r1 r2)
+  | (_, Node (l2, v2, d2, r2, h2)) ->
+      let (l1, d1, r1) = split cmp v2 s1 in
+      concat_or_join cmp (merge cmp f l1 l2) v2 (f v2 d1 (Some d2)) (merge cmp f r1 r2)
+  | _ ->
+      assert false
+
+type ('key,'a) enumeration = End | More of 'key * 'a * ('key,'a) rep * ('key,'a) enumeration
+
+let rec cons_enum m e =
+  match m with
+    Empty -> e
+  | Node(l, v, d, r, _) -> cons_enum l (More(v, d, r, e))
+	
+let compare cmp_key cmp_a m1 m2 =
+  let rec compare_aux e1 e2 =
+    match (e1, e2) with
+      (End, End) -> 0
+    | (End, _)  -> -1
+    | (_, End) -> 1
+    | (More(v1, d1, r1, e1), More(v2, d2, r2, e2)) ->
+        let c = cmp_key v1 v2 in
+        if c <> 0 then c else
+        let c = cmp_a d1 d2 in
+        if c <> 0 then c else
+        compare_aux (cons_enum r1 e1) (cons_enum r2 e2)
+  in compare_aux (cons_enum m1 End) (cons_enum m2 End)
+
+let equal cmp_key cmp_a m1 m2 =
+  let rec equal_aux e1 e2 =
+    match (e1, e2) with
+      (End, End) -> true
+    | (End, _)  -> false
+    | (_, End) -> false
+    | (More(v1, d1, r1, e1), More(v2, d2, r2, e2)) ->
+        cmp_key v1 v2 = 0 && cmp_a d1 d2 &&
+        equal_aux (cons_enum r1 e1) (cons_enum r2 e2)
+      in equal_aux (cons_enum m1 End) (cons_enum m2 End)
+
+let rec cardinal = function
+    Empty -> 0
+  | Node(l, _, _, r, _) -> cardinal l + 1 + cardinal r
+
+let rec bindings_aux accu = function
+    Empty -> accu
+  | Node(l, v, d, r, _) -> bindings_aux ((v, d) :: bindings_aux accu r) l
+
+let bindings s =
+  bindings_aux [] s
+    
+let choose = min_binding
+
+
+(* Wrapper functions now *)
+
+type ('key,'a) map = {cmp:'key -> 'key -> int; m:('key,'a) rep}
+
+let empty cmp = {cmp = cmp; m = Empty}
+let is_empty m = is_empty m.m
+let mem k m = mem m.cmp k m.m
+let add k a m = {m with m = add m.cmp k a m.m}
+let singleton cmp k a = {cmp = cmp; m = singleton k a} 
+let remove k m = {m with m = remove m.cmp k m.m}
+let merge f a b = {cmp = a.cmp; (* does not matter, a and b should have the same comparison function *)
+		   m = merge a.cmp f a.m b.m;}
+let union a b = merge (fun k o1 o2 ->
+  match (o1, o2) with
+    | (_, Some v) -> Some v
+    | (Some v, _) -> Some v
+    | (_, _) -> None) a b
+ let compare f a b = compare a.cmp f a.m b.m
+let equal f a b = equal a.cmp f a.m b.m
+let iter f m = iter f m.m
+let fold f m b = fold f m.m b
+let for_all f m = for_all f m.m
+let exist f m = exists f m.m
+let filter f m = {m with m = filter m.cmp f m.m}
+let partition f m = 
+  let m1,m2 = partition m.cmp f m.m in
+  ({m with m = m1},{m with m = m2})
+let cardinal m = cardinal m.m
+let domain m = Pset.from_list m.cmp (List.map fst (bindings m.m))
+let range cmp m = Pset.from_list cmp (List.map snd (bindings m.m))
+let bindings_list m = bindings m.m
+let bindings cmp m = Pset.from_list cmp (bindings m.m)
+let min_binding m = min_binding m.m
+let max_binding m = max_binding m.m
+let choose m = choose m.m
+let split k m = 
+  let (m1,opt,m2) = split m.cmp k m.m in
+  ({m with m = m1},opt,{m with m = m2})
+let find k m = find m.cmp k m.m
+let lookup k m = try Some (find k m) with Not_found -> None
+let map f m = {m with m = map f m.m}
+let mapi f m = {m with m = mapi f m.m}
+
+let from_set f s = Pset.fold (fun k m -> (add k (f k) m)) s (empty (Pset.get_elem_compare s))
diff --git a/lib/ocaml_rts/linksem/src_lem_library/pmap.mli b/lib/ocaml_rts/linksem/src_lem_library/pmap.mli
new file mode 100755
index 00000000..f2016418
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/pmap.mli
@@ -0,0 +1,190 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                           Objective Caml                            *)
+(*                                                                     *)
+(*            Xavier Leroy, projet Cristal, INRIA Rocquencourt         *)
+(*                                                                     *)
+(*  Copyright 1996 Institut National de Recherche en Informatique et   *)
+(*  en Automatique.  All rights reserved.  This file is distributed    *)
+(*  under the terms of the GNU Library General Public License, with    *)
+(*  the special exception on linking described in file ../LICENSE.     *)
+(*                                                                     *)
+(***********************************************************************)
+
+(* Modified by Susmit Sarkar 2010-11-30 *)
+(* $Id: map.mli 10632 2010-07-24 14:16:58Z garrigue $ *)
+
+(** Association tables over ordered types.
+
+   This module implements applicative association tables, also known as
+   finite maps or dictionaries, given a total ordering function
+   over the keys.
+   All operations over maps are purely applicative (no side-effects).
+   The implementation uses balanced binary trees, and therefore searching
+   and insertion take time logarithmic in the size of the map.
+*)
+
+type ('key,+'a) map
+    (** The type of maps from type ['key] to type ['a]. *)
+
+val empty: ('key -> 'key -> int) -> ('key,'a) map
+    (** The empty map. *)
+
+val is_empty: ('key,'a) map -> bool
+    (** Test whether a map is empty or not. *)
+
+val mem: 'key -> ('key,'a) map -> bool
+    (** [mem x m] returns [true] if [m] contains a binding for [x],
+       and [false] otherwise. *)
+
+val add: 'key -> 'a -> ('key,'a) map -> ('key,'a) map
+    (** [add x y m] returns a map containing the same bindings as
+	[m], plus a binding of [x] to [y]. If [x] was already bound
+       in [m], its previous binding disappears. *)
+
+val singleton: ('key -> 'key -> int) -> 'key -> 'a -> ('key,'a) map
+    (** [singleton x y] returns the one-element map that contains a binding [y]
+        for [x].
+        @since 3.12.0
+     *)
+
+val remove: 'key -> ('key,'a) map -> ('key,'a) map
+    (** [remove x m] returns a map containing the same bindings as
+	[m], except for [x] which is unbound in the returned map. *)
+
+val merge:
+    ('key -> 'a option -> 'b option -> 'c option) -> ('key,'a) map -> ('key,'b) map -> ('key,'c) map
+    (** [merge f m1 m2] computes a map whose keys is a subset of keys of [m1]
+        and of [m2]. The presence of each such binding, and the corresponding
+        value, is determined with the function [f].
+        @since 3.12.0
+     *)
+
+val union: ('key,'a) map -> ('key,'a) map -> ('key,'a) map
+    (** [union m1 m2] computes a map whose keys is a subset of keys of [m1]
+        and of [m2]. The bindings in m2 take precedence.
+        @since 3.12.0
+     *)
+
+val compare: ('a -> 'a -> int) -> ('key,'a) map -> ('key,'a) map -> int
+    (** Total ordering between maps.  The first argument is a total ordering
+        used to compare data associated with equal keys in the two maps. *)
+
+val equal: ('a -> 'a -> bool) -> ('key,'a) map -> ('key,'a) map -> bool
+    (** [equal cmp m1 m2] tests whether the maps [m1] and [m2] are
+	equal, that is, contain equal keys and associate them with
+       equal data.  [cmp] is the equality predicate used to compare
+       the data associated with the keys. *)
+
+val iter: ('key -> 'a -> unit) -> ('key,'a) map -> unit
+    (** [iter f m] applies [f] to all bindings in map [m].
+       [f] receives the key as first argument, and the associated value
+       as second argument.  The bindings are passed to [f] in increasing
+       order with respect to the ordering over the type of the keys. *)
+
+val fold: ('key -> 'a -> 'b -> 'b) -> ('key,'a) map -> 'b -> 'b
+    (** [fold f m a] computes [(f kN dN ... (f k1 d1 a)...)],
+       where [k1 ... kN] are the keys of all bindings in [m]
+       (in increasing order), and [d1 ... dN] are the associated data. *)
+
+val for_all: ('key -> 'a -> bool) -> ('key,'a) map -> bool
+    (** [for_all p m] checks if all the bindings of the map
+        satisfy the predicate [p].
+        @since 3.12.0
+     *)
+
+val exist: ('key -> 'a -> bool) -> ('key,'a) map -> bool
+    (** [exists p m] checks if at least one binding of the map
+        satisfy the predicate [p].
+        @since 3.12.0
+     *)
+
+val filter: ('key -> 'a -> bool) -> ('key,'a) map -> ('key,'a) map
+    (** [filter p m] returns the map with all the bindings in [m]
+        that satisfy predicate [p].
+        @since 3.12.0
+     *)
+
+val partition: ('key -> 'a -> bool) -> ('key,'a) map -> ('key,'a) map * ('key,'a) map
+    (** [partition p m] returns a pair of maps [(m1, m2)], where
+        [m1] contains all the bindings of [s] that satisfy the
+        predicate [p], and [m2] is the map with all the bindings of
+        [s] that do not satisfy [p].
+        @since 3.12.0
+     *)
+
+val cardinal: ('key,'a) map -> int
+    (** Return the number of bindings of a map.
+        @since 3.12.0
+     *)
+
+val bindings_list: ('key,'a) map -> ('key * 'a) list
+    (** Return the list of all bindings of the given map.
+       The returned list is sorted in increasing order with respect
+       to the ordering [Ord.compare], where [Ord] is the argument
+       given to {!Map.Make}.
+        @since 3.12.0
+     *)
+
+val bindings: (('key * 'a) -> ('key * 'a) -> int) -> ('key,'a) map -> ('key * 'a) Pset.set
+    (** Return a set of all bindings of the given map. *)
+
+(** [domain m] returns the domain of the map [m], i.e. the
+    set of keys of this map. *)
+val domain : ('key,'a) map -> 'key Pset.set
+
+(** [range m] returns the range of the map [m], i.e. the
+    set of all values stored in this map. *)
+val range : ('a -> 'a -> int) -> ('key,'a) map -> 'a Pset.set
+
+val min_binding: ('key,'a) map -> ('key * 'a)
+    (** Return the smallest binding of the given map
+       (with respect to the [Ord.compare] ordering), or raise
+       [Not_found] if the map is empty.
+        @since 3.12.0
+     *)
+
+val max_binding: ('key,'a) map -> ('key * 'a)
+    (** Same as {!Map.S.min_binding}, but returns the largest binding
+        of the given map.
+        @since 3.12.0
+     *)
+
+val choose: ('key,'a) map -> ('key * 'a)
+    (** Return one binding of the given map, or raise [Not_found] if
+       the map is empty. Which binding is chosen is unspecified,
+       but equal bindings will be chosen for equal maps.
+        @since 3.12.0
+     *)
+
+val split: 'key -> ('key,'a) map -> ('key,'a) map * 'a option * ('key,'a) map
+    (** [split x m] returns a triple [(l, data, r)], where
+          [l] is the map with all the bindings of [m] whose key
+        is strictly less than [x];
+          [r] is the map with all the bindings of [m] whose key
+        is strictly greater than [x];
+          [data] is [None] if [m] contains no binding for [x],
+          or [Some v] if [m] binds [v] to [x].
+        @since 3.12.0
+     *)
+
+val find: 'key -> ('key,'a) map -> 'a
+    (** [find x m] returns the current binding of [x] in [m],
+       or raises [Not_found] if no such binding exists. *)
+
+val lookup: 'key -> ('key,'a) map -> 'a option
+    (** [lookup x m] returns the current binding of [x] in [m]. In contrast to [find],
+       it returns [None] instead of raising an exception, if no such binding exists. *)
+
+val map: ('a -> 'b) -> ('key,'a) map -> ('key,'b) map
+    (** [map f m] returns a map with same domain as [m], where the
+       associated value [a] of all bindings of [m] has been
+       replaced by the result of the application of [f] to [a].
+       The bindings are passed to [f] in increasing order
+       with respect to the ordering over the type of the keys. *)
+
+val mapi: ('key -> 'a -> 'b) -> ('key,'a) map -> ('key,'b) map
+    (** Same as {!Map.S.map}, but the function receives as arguments both the
+       key and the associated value for each binding of the map. *)
+
+val from_set : ('key -> 'v) -> ('key Pset.set) -> ('key, 'v) map
diff --git a/lib/ocaml_rts/linksem/src_lem_library/pset.ml b/lib/ocaml_rts/linksem/src_lem_library/pset.ml
new file mode 100755
index 00000000..35335e88
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/pset.ml
@@ -0,0 +1,522 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                           Objective Caml                            *)
+(*                                                                     *)
+(*            Xavier Leroy, projet Cristal, INRIA Rocquencourt         *)
+(*                                                                     *)
+(*  Copyright 1996 Institut National de Recherche en Informatique et   *)
+(*  en Automatique.  All rights reserved.  This file is distributed    *)
+(*  under the terms of the GNU Library General Public License, with    *)
+(*  the special exception on linking described in file ../LICENSE.     *)
+(*                                                                     *)
+(***********************************************************************)
+
+(* Modified by Scott Owens 2010-10-28 *)
+
+(* $Id: set.ml 6694 2004-11-25 00:06:06Z doligez $ *)
+
+(* Sets over ordered types *)
+
+type 'a rep = Empty | Node of 'a rep * 'a * 'a rep * int
+
+(* Sets are represented by balanced binary trees (the heights of the
+ children differ by at most 2 *)
+
+let height = function
+    Empty -> 0
+  | Node(_, _, _, h) -> h
+
+(* Creates a new node with left son l, value v and right son r.
+ We must have all elements of l < v < all elements of r.
+ l and r must be balanced and | height l - height r | <= 2.
+ Inline expansion of height for better speed. *)
+
+let create l v r =
+  let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in
+  let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in
+    Node(l, v, r, (if hl >= hr then hl + 1 else hr + 1))
+
+(* Same as create, but performs one step of rebalancing if necessary.
+ Assumes l and r balanced and | height l - height r | <= 3.
+ Inline expansion of create for better speed in the most frequent case
+ where no rebalancing is required. *)
+
+let bal l v r =
+  let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in
+  let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in
+    if hl > hr + 2 then begin
+      match l with
+          Empty -> invalid_arg "Set.bal"
+        | Node(ll, lv, lr, _) ->
+            if height ll >= height lr then
+              create ll lv (create lr v r)
+            else begin
+              match lr with
+                  Empty -> invalid_arg "Set.bal"
+                | Node(lrl, lrv, lrr, _)->
+                    create (create ll lv lrl) lrv (create lrr v r)
+            end
+    end else if hr > hl + 2 then begin
+      match r with
+          Empty -> invalid_arg "Set.bal"
+        | Node(rl, rv, rr, _) ->
+            if height rr >= height rl then
+              create (create l v rl) rv rr
+            else begin
+              match rl with
+                  Empty -> invalid_arg "Set.bal"
+                | Node(rll, rlv, rlr, _) ->
+                    create (create l v rll) rlv (create rlr rv rr)
+            end
+    end else
+      Node(l, v, r, (if hl >= hr then hl + 1 else hr + 1))
+
+(* Insertion of one element *)
+
+let rec add cmp x = function
+    Empty -> Node(Empty, x, Empty, 1)
+  | Node(l, v, r, _) as t ->
+      let c = cmp x v in
+        if c = 0 then t else
+          if c < 0 then bal (add cmp x l) v r else bal l v (add cmp x r)
+
+(* Same as create and bal, but no assumptions are made on the
+ relative heights of l and r. *)
+
+let rec join cmp l v r =
+  match (l, r) with
+      (Empty, _) -> add cmp v r
+    | (_, Empty) -> add cmp v l
+    | (Node(ll, lv, lr, lh), Node(rl, rv, rr, rh)) ->
+        if lh > rh + 2 then bal ll lv (join cmp lr v r) else
+          if rh > lh + 2 then bal (join cmp l v rl) rv rr else
+            create l v r
+
+(* Smallest and greatest element of a set *)
+
+let rec min_elt = function
+    Empty -> raise Not_found
+  | Node(Empty, v, r, _) -> v
+  | Node(l, v, r, _) -> min_elt l
+
+let rec max_elt = function
+    Empty -> raise Not_found
+  | Node(l, v, Empty, _) -> v
+  | Node(l, v, r, _) -> max_elt r
+
+(* Remove the smallest element of the given set *)
+
+let rec remove_min_elt = function
+    Empty -> invalid_arg "Set.remove_min_elt"
+  | Node(Empty, v, r, _) -> r
+  | Node(l, v, r, _) -> bal (remove_min_elt l) v r
+
+(* Merge two trees l and r into one.
+ All elements of l must precede the elements of r.
+ Assume | height l - height r | <= 2. *)
+
+let merge t1 t2 =
+  match (t1, t2) with
+      (Empty, t) -> t
+    | (t, Empty) -> t
+    | (_, _) -> bal t1 (min_elt t2) (remove_min_elt t2)
+
+(* Merge two trees l and r into one.
+ All elements of l must precede the elements of r.
+ No assumption on the heights of l and r. *)
+
+let concat cmp t1 t2 =
+  match (t1, t2) with
+      (Empty, t) -> t
+    | (t, Empty) -> t
+    | (_, _) -> join cmp t1 (min_elt t2) (remove_min_elt t2)
+
+(* Splitting.  split x s returns a triple (l, present, r) where
+ - l is the set of elements of s that are < x
+ - r is the set of elements of s that are > x
+ - present is false if s contains no element equal to x,
+ or true if s contains an element equal to x. *)
+
+let rec split cmp x = function
+    Empty ->
+      (Empty, false, Empty)
+  | Node(l, v, r, _) ->
+      let c = cmp x v in
+        if c = 0 then (l, true, r)
+        else if c < 0 then
+          let (ll, pres, rl) = split cmp x l in (ll, pres, join cmp rl v r)
+          else
+            let (lr, pres, rr) = split cmp x r in (join cmp l v lr, pres, rr)
+
+(* Implementation of the set operations *)
+
+let empty = Empty
+
+let is_empty = function Empty -> true | _ -> false
+
+let rec mem cmp x = function
+    Empty -> false
+  | Node(l, v, r, _) ->
+      let c = cmp x v in
+        c = 0 || mem cmp x (if c < 0 then l else r)
+
+let singleton x = Node(Empty, x, Empty, 1)
+
+let rec remove cmp x = function
+    Empty -> Empty
+  | Node(l, v, r, _) ->
+      let c = cmp x v in
+        if c = 0 then merge l r else
+          if c < 0 then bal (remove cmp x l) v r else bal l v (remove cmp x r)
+
+let rec union cmp s1 s2 =
+  match (s1, s2) with
+      (Empty, t2) -> t2
+    | (t1, Empty) -> t1
+    | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) ->
+        if h1 >= h2 then
+          if h2 = 1 then add cmp v2 s1 else begin
+            let (l2, _, r2) = split cmp v1 s2 in
+              join cmp (union cmp l1 l2) v1 (union cmp r1 r2)
+          end
+        else
+          if h1 = 1 then add cmp v1 s2 else begin
+            let (l1, _, r1) = split cmp v2 s1 in
+              join cmp (union cmp l1 l2) v2 (union cmp r1 r2)
+          end
+
+let rec inter cmp s1 s2 =
+  match (s1, s2) with
+      (Empty, t2) -> Empty
+    | (t1, Empty) -> Empty
+    | (Node(l1, v1, r1, _), t2) ->
+        match split cmp v1 t2 with
+            (l2, false, r2) ->
+              concat cmp (inter cmp l1 l2) (inter cmp r1 r2)
+          | (l2, true, r2) ->
+              join cmp (inter cmp l1 l2) v1 (inter cmp r1 r2)
+
+let rec diff cmp s1 s2 =
+  match (s1, s2) with
+      (Empty, t2) -> Empty
+    | (t1, Empty) -> t1
+    | (Node(l1, v1, r1, _), t2) ->
+        match split cmp v1 t2 with
+            (l2, false, r2) ->
+              join cmp (diff cmp l1 l2) v1 (diff cmp r1 r2)
+          | (l2, true, r2) ->
+              concat cmp (diff cmp l1 l2) (diff cmp r1 r2)
+
+type 'a enumeration = End | More of 'a * 'a rep * 'a enumeration
+
+let rec cons_enum s e =
+  match s with
+      Empty -> e
+    | Node(l, v, r, _) -> cons_enum l (More(v, r, e))
+
+let rec compare_aux cmp e1 e2 =
+  match (e1, e2) with
+      (End, End) -> 0
+    | (End, _)  -> -1
+    | (_, End) -> 1
+    | (More(v1, r1, e1), More(v2, r2, e2)) ->
+        let c = cmp v1 v2 in
+          if c <> 0
+          then c
+          else compare_aux cmp (cons_enum r1 e1) (cons_enum r2 e2)
+
+let compare cmp s1 s2 =
+  compare_aux cmp (cons_enum s1 End) (cons_enum s2 End)
+
+let equal cmp s1 s2 =
+  compare cmp s1 s2 = 0
+
+let rec subset cmp s1 s2 =
+  match (s1, s2) with
+      Empty, _ ->
+        true
+    | _, Empty ->
+        false
+    | Node (l1, v1, r1, _), (Node (l2, v2, r2, _) as t2) ->
+        let c = cmp v1 v2 in
+          if c = 0 then
+            subset cmp l1 l2 && subset cmp r1 r2
+          else if c < 0 then
+            subset cmp (Node (l1, v1, Empty, 0)) l2 && subset cmp r1 t2
+          else
+            subset cmp (Node (Empty, v1, r1, 0)) r2 && subset cmp l1 t2
+
+let rec iter f = function
+    Empty -> ()
+  | Node(l, v, r, _) -> iter f l; f v; iter f r
+
+let rec fold f s accu =
+  match s with
+      Empty -> accu
+    | Node(l, v, r, _) -> fold f r (f v (fold f l accu))
+
+let map cmp f s = fold (fun e s -> add cmp (f e) s) s empty
+
+let map_union cmp f s = fold (fun e s -> union cmp (f e) s) s empty
+
+
+let rec for_all p = function
+    Empty -> true
+  | Node(l, v, r, _) -> p v && for_all p l && for_all p r
+
+let rec exists p = function
+    Empty -> false
+  | Node(l, v, r, _) -> p v || exists p l || exists p r
+
+let filter cmp p s =
+  let rec filt accu = function
+    | Empty -> accu
+    | Node(l, v, r, _) ->
+        filt (filt (if p v then add cmp v accu else accu) l) r in
+    filt Empty s
+
+let partition cmp p s =
+  let rec part (t, f as accu) = function
+    | Empty -> accu
+    | Node(l, v, r, _) ->
+        part (part (if p v then (add cmp v t, f) else (t, add cmp v f)) l) r in
+    part (Empty, Empty) s
+
+let rec cardinal = function
+    Empty -> 0
+  | Node(l, v, r, _) -> cardinal l + 1 + cardinal r
+
+let rec elements_aux accu = function
+    Empty -> accu
+  | Node(l, v, r, _) -> elements_aux (v :: elements_aux accu r) l
+
+let elements s =
+  elements_aux [] s
+
+let choose = min_elt
+
+type 'a set = { cmp : 'a -> 'a -> int; s : 'a rep }
+                
+let empty c = { cmp = c; s = Empty; }
+
+let is_empty s = is_empty s.s
+
+let mem x s = mem s.cmp x s.s
+
+let add x s = { s with s = add s.cmp x s.s }
+
+let singleton c x = { cmp = c; s = singleton x }
+
+let remove x s = { s with s = remove s.cmp x s.s }
+
+let union s1 s2 = { s1 with s = union s1.cmp s1.s s2.s }
+
+let map_union c f s1 = { cmp = c; s = map_union c (fun x -> (f x).s) s1.s}
+
+let inter s1 s2 = { s1 with s = inter s1.cmp s1.s s2.s }
+
+let diff s1 s2 = { s1 with s = diff s1.cmp s1.s s2.s }
+
+let compare_by cmp s1 s2 = compare cmp s1.s s2.s
+
+let compare s1 s2 = compare s1.cmp s1.s s2.s
+
+let equal s1 s2 = equal s1.cmp s1.s s2.s
+
+let subset s1 s2 = subset s1.cmp s1.s s2.s
+let subset_proper s1 s2 = (subset s1 s2) && not (equal s1 s2)
+
+let iter f s = iter f s.s
+
+let fold f s a = fold f s.s a
+
+let map c f s = {cmp = c; s = map c f s.s}
+
+let for_all p s = for_all p s.s
+
+let exists p s = exists p s.s
+
+let filter p s = { s with s = filter s.cmp p s.s }
+
+let partition p s =
+  let (r1,r2) = partition s.cmp p s.s in
+    ({s with s = r1}, {s with s = r2})
+
+let cardinal s = cardinal s.s
+
+let elements s = elements s.s
+
+let min_elt s = min_elt s.s
+
+let min_elt_opt s = try Some (min_elt s) with Not_found -> None
+
+let max_elt s = max_elt s.s
+
+let max_elt_opt s = try Some (max_elt s) with Not_found -> None
+
+let choose s = choose s.s
+
+let set_case s c_emp c_sing c_else = match s.s with
+    Empty -> c_emp
+  | Node(Empty, v, Empty, _) -> c_sing v
+  | _ -> c_else
+
+let split x s =
+  let (l,present,r) = split s.cmp x s.s in
+    ({ s with s = l }, present, { s with s = r })
+
+let from_list c l =
+  List.fold_left (fun s x -> add x s) (empty c) l
+
+let comprehension1 cmp f p s =
+  fold (fun x s -> if p x then add (f x) s else s) s (empty cmp) 
+
+let comprehension2 cmp f p s1 s2 =
+  fold
+    (fun x1 s -> 
+       fold 
+         (fun x2 s ->
+            if p x1 x2 then add (f x1 x2) s else s)
+         s2
+         s) 
+    s1 
+    (empty cmp) 
+
+let comprehension3 cmp f p s1 s2 s3 =
+  fold 
+    (fun x1 s -> 
+       fold 
+         (fun x2 s -> 
+            fold 
+              (fun x3 s ->
+                 if p x1 x2 x3 then add (f x1 x2 x3) s else s)
+              s3
+              s)
+         s2
+         s) 
+    s1 
+    (empty cmp) 
+
+let comprehension4 cmp f p s1 s2 s3 s4 =
+  fold 
+    (fun x1 s -> 
+       fold 
+         (fun x2 s -> 
+            fold 
+              (fun x3 s -> 
+                 fold 
+                   (fun x4 s ->
+                      if p x1 x2 x3 x4 then add (f x1 x2 x3 x4) s else s)
+                   s4
+                   s)
+              s3
+              s)
+         s2
+         s) 
+    s1 
+    (empty cmp) 
+
+let comprehension5 cmp f p s1 s2 s3 s4 s5 =
+  fold 
+    (fun x1 s -> 
+       fold 
+         (fun x2 s -> 
+            fold 
+              (fun x3 s -> 
+                 fold 
+                   (fun x4 s -> 
+                      fold 
+                        (fun x5 s ->
+                           if p x1 x2 x3 x4 x5 then add (f x1 x2 x3 x4 x5) s else s)
+                        s5
+                        s)
+                   s4
+                   s)
+              s3
+              s)
+         s2
+         s) 
+    s1 
+    (empty cmp) 
+
+let comprehension6 cmp f p s1 s2 s3 s4 s5 s6 =
+  fold 
+    (fun x1 s -> 
+       fold 
+         (fun x2 s -> 
+            fold 
+              (fun x3 s -> 
+                 fold 
+                   (fun x4 s -> 
+                      fold 
+                        (fun x5 s -> 
+                           fold 
+                             (fun x6 s -> 
+                                if p x1 x2 x3 x4 x5 x6 then add (f x1 x2 x3 x4 x5 x6) s else s)
+                             s6
+                             s)
+                        s5
+                        s)
+                   s4
+                   s)
+              s3
+              s)
+         s2
+         s) 
+    s1 
+    (empty cmp) 
+
+let comprehension7 cmp f p s1 s2 s3 s4 s5 s6 s7 =
+  fold 
+    (fun x1 s -> 
+       fold 
+         (fun x2 s -> 
+            fold 
+              (fun x3 s -> 
+                 fold 
+                   (fun x4 s -> 
+                      fold 
+                        (fun x5 s -> 
+                           fold 
+                             (fun x6 s -> 
+                                fold 
+                                  (fun x7 s -> 
+                                     if p x1 x2 x3 x4 x5 x6 x7 then add (f x1 x2 x3 x4 x5 x6 x7) s else s)
+                                  s7
+                                  s)
+                             s6
+                             s)
+                        s5
+                        s)
+                   s4
+                   s)
+              s3
+              s)
+         s2
+         s) 
+    s1 
+    (empty cmp) 
+
+let bigunion c xss =
+  fold union xss (empty c)
+
+let sigma c xs ys = 
+  fold (fun x xys -> fold (fun y xys -> add (x,y) xys) (ys x) xys) xs (empty c)
+
+let cross c xs ys = sigma c xs (fun _ -> ys)
+
+let rec lfp s f =
+  let s' = f s in
+    if subset s' s then
+      s
+    else
+      lfp (union s' s) f
+
+let tc c r =
+  let one_step r = fold (fun (x,y) xs -> fold (fun (y',z) xs ->
+     if c (y,y) (y',y') = 0 then add (x,z) xs else xs) r xs) r (empty c) in
+  lfp r one_step
+
+
+let get_elem_compare s = s.cmp
+
diff --git a/lib/ocaml_rts/linksem/src_lem_library/pset.mli b/lib/ocaml_rts/linksem/src_lem_library/pset.mli
new file mode 100755
index 00000000..162d5f3b
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/pset.mli
@@ -0,0 +1,174 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                           Objective Caml                            *)
+(*                                                                     *)
+(*            Xavier Leroy, projet Cristal, INRIA Rocquencourt         *)
+(*                                                                     *)
+(*  Copyright 1996 Institut National de Recherche en Informatique et   *)
+(*  en Automatique.  All rights reserved.  This file is distributed    *)
+(*  under the terms of the GNU Library General Public License, with    *)
+(*  the special exception on linking described in file ../LICENSE.     *)
+(*                                                                     *)
+(***********************************************************************)
+
+(* Modified by Scott Owens 2010-10-28 *)
+
+(* $Id: set.mli 6974 2005-07-21 14:52:45Z doligez $ *)
+
+(** Sets over ordered types.
+
+  This module implements the set data structure, given a total ordering
+  function over the set elements. All operations over sets
+  are purely applicative (no side-effects).
+  The implementation uses balanced binary trees, and is therefore
+  reasonably efficient: insertion and membership take time
+  logarithmic in the size of the set, for instance.
+  *)
+
+type 'a set
+(** The type of sets. *)
+
+val empty: ('a -> 'a -> int) -> 'a set
+(** The empty set. *)
+
+val is_empty: 'a set -> bool
+(** Test whether a set is empty or not. *)
+
+val from_list: ('a -> 'a -> int) -> 'a list -> 'a set
+
+val mem: 'a -> 'a set -> bool
+(** [mem x s] tests whether [x] belongs to the set [s]. *)
+
+val add: 'a -> 'a set -> 'a set
+(** [add x s] returns a set containing all elements of [s],
+  plus [x]. If [x] was already in [s], [s] is returned unchanged. *)
+
+val singleton: ('a -> 'a -> int) -> 'a -> 'a set
+(** [singleton x] returns the one-element set containing only [x]. *)
+
+val remove: 'a -> 'a set -> 'a set
+(** [remove x s] returns a set containing all elements of [s],
+  except [x]. If [x] was not in [s], [s] is returned unchanged. *)
+
+val union: 'a set -> 'a set -> 'a set
+(** Set union. *)
+
+val inter: 'a set -> 'a set -> 'a set
+(** Set intersection. *)
+
+(** Set difference. *)
+val diff: 'a set -> 'a set -> 'a set
+
+val compare: 'a set -> 'a set -> int
+(** Total ordering between sets. Can be used as the ordering function
+  for doing sets of sets. *)
+
+val equal: 'a set -> 'a set -> bool
+(** [equal s1 s2] tests whether the sets [s1] and [s2] are
+  equal, that is, contain equal elements. *)
+
+val subset: 'a set -> 'a set -> bool
+(** [subset s1 s2] tests whether the set [s1] is a subset of
+  the set [s2]. This includes the case where [s1] and [s2] are equal. *)
+
+val subset_proper : 'a set -> 'a set -> bool
+(** [subset_proper s1 s2] tests whether the set [s1] is a proper subset of
+  the set [s2]. *)
+
+val iter: ('a -> unit) -> 'a set -> unit
+(** [iter f s] applies [f] in turn to all elements of [s].
+  The elements of [s] are presented to [f] in increasing order
+  with respect to the ordering over the type of the elements. *)
+
+val fold: ('a -> 'b -> 'b) -> 'a set -> 'b -> 'b
+(** [fold f s a] computes [(f xN ... (f x2 (f x1 a))...)],
+  where [x1 ... xN] are the elements of [s], in increasing order. *)
+
+val map: ('b -> 'b -> int) -> ('a -> 'b) -> 'a set -> 'b set
+
+val map_union: ('b -> 'b -> int) -> ('a -> 'b set) -> 'a set -> 'b set
+(** [map_union cmp f s] does the same as [bigunion cmp (map cmp' f s)].
+    Because the set of sets is internally not constructed though the comparison function [cmp'] is
+    not needed. *)
+
+val for_all: ('a -> bool) -> 'a set -> bool
+(** [for_all p s] checks if all elements of the set
+  satisfy the predicate [p]. *)
+
+val exists: ('a -> bool) -> 'a set -> bool
+(** [exists p s] checks if at least one element of
+  the set satisfies the predicate [p]. *)
+
+val filter: ('a -> bool) -> 'a set -> 'a set
+(** [filter p s] returns the set of all elements in [s]
+  that satisfy predicate [p]. *)
+
+val partition: ('a -> bool) -> 'a set -> 'a set * 'a set
+(** [partition p s] returns a pair of sets [(s1, s2)], where
+  [s1] is the set of all the elements of [s] that satisfy the
+  predicate [p], and [s2] is the set of all the elements of
+  [s] that do not satisfy [p]. *)
+
+val cardinal: 'a set -> int
+(** Return the number of elements of a set. *)
+
+val elements: 'a set -> 'a list
+(** Return the list of all elements of the given set.
+  The returned list is sorted in increasing order with respect
+  to the ordering [Ord.compare], where [Ord] is the argument
+  given to {!Set.Make}. *)
+
+val min_elt: 'a set -> 'a
+(** Return the smallest element of the given set
+  (with respect to the [Ord.compare] ordering), or raise
+  [Not_found] if the set is empty. *)
+
+val max_elt: 'a set -> 'a
+(** Same as {!Set.S.min_elt}, but returns the largest element of the
+  given set. *)
+
+val min_elt_opt: 'a set -> 'a option
+(** an optional version of [min_elt] *)
+
+val max_elt_opt: 'a set -> 'a option
+(** an optional version of [max_elt] *)
+
+val choose: 'a set -> 'a
+(** Return one element of the given set, or raise [Not_found] if
+  the set is empty. Which element is chosen is unspecified,
+  but equal elements will be chosen for equal sets. *)
+
+val set_case: 'a set -> 'b -> ('a -> 'b) -> 'b -> 'b
+(** case-split function for sets *)
+
+val split: 'a -> 'a set -> 'a set * bool * 'a set
+    (** [split x s] returns a triple [(l, present, r)], where
+      [l] is the set of elements of [s] that are
+      strictly less than [x];
+      [r] is the set of elements of [s] that are
+      strictly greater than [x];
+      [present] is [false] if [s] contains no element equal to [x],
+      or [true] if [s] contains an element equal to [x]. *)
+
+val comprehension1 : ('b -> 'b -> int) -> ('a -> 'b) -> ('a -> bool) -> 'a set -> 'b set
+val comprehension2 : ('c -> 'c -> int) -> ('a -> 'b -> 'c) -> ('a -> 'b -> bool) -> 'a set -> 'b set -> 'c set
+val comprehension3 : ('d -> 'd -> int) -> ('a -> 'b -> 'c -> 'd) -> ('a -> 'b -> 'c -> bool) -> 'a set -> 'b set -> 'c set -> 'd set
+val comprehension4 : ('e -> 'e -> int) -> ('a -> 'b -> 'c -> 'd -> 'e) -> ('a -> 'b -> 'c -> 'd -> bool) -> 'a set -> 'b set -> 'c set -> 'd set -> 'e set
+val comprehension5 : ('f -> 'f -> int) -> ('a -> 'b -> 'c -> 'd -> 'e -> 'f) -> ('a -> 'b -> 'c -> 'd -> 'e -> bool) -> 'a set -> 'b set -> 'c set -> 'd set -> 'e set -> 'f set
+val comprehension6 : ('g -> 'g -> int) -> ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g) -> ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> bool) -> 'a set -> 'b set -> 'c set -> 'd set -> 'e set -> 'f set -> 'g set
+val comprehension7 : ('h -> 'h -> int) -> ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) -> ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> bool) -> 'a set -> 'b set -> 'c set -> 'd set -> 'e set -> 'f set -> 'g set -> 'h set
+
+val bigunion : ('a -> 'a -> int) -> 'a set set -> 'a set
+
+val lfp : 'a set -> ('a set -> 'a set) -> 'a set
+val tc : ('a * 'a -> 'a * 'a -> int) -> ('a * 'a) set -> ('a * 'a) set
+
+
+val sigma : ('a * 'b -> 'a * 'b -> int) -> 'a set -> ('a -> 'b set) -> ('a * 'b) set
+val cross : ('a * 'b -> 'a * 'b -> int) -> 'a set -> 'b set -> ('a * 'b) set
+
+val get_elem_compare : 'a set -> ('a -> 'a -> int)
+
+val compare_by: ('a->'a->int) -> 'a set -> 'a set -> int
+(** set comparison parameterised by element comparison (ignoring the comparison functions of the argument sets*)
+
diff --git a/lib/ocaml_rts/linksem/src_lem_library/pset_using_lists.ml b/lib/ocaml_rts/linksem/src_lem_library/pset_using_lists.ml
new file mode 100644
index 00000000..1fadd8f7
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/pset_using_lists.ml
@@ -0,0 +1,336 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                           Objective Caml                            *)
+(*                                                                     *)
+(*            Xavier Leroy, projet Cristal, INRIA Rocquencourt         *)
+(*                                                                     *)
+(*  Copyright 1996 Institut National de Recherche en Informatique et   *)
+(*  en Automatique.  All rights reserved.  This file is distributed    *)
+(*  under the terms of the GNU Library General Public License, with    *)
+(*  the special exception on linking described in file ../LICENSE.     *)
+(*                                                                     *)
+(***********************************************************************)
+
+(* Modified by Scott Owens 2010-10-28 *)
+(* Modified by Kyndylan Nienhuis 2013-04-.. *)
+
+(* $Id: set.ml 6694 2004-11-25 00:06:06Z doligez $ *)
+
+(* Sets over ordered types *)
+
+
+
+(* Implementation of the set operations *)
+
+type 'a rep = 'a list
+
+exception Not_implemented
+
+let rec add cmp x list =
+  x::list
+  
+let empty = []
+
+let is_empty = function [] -> true | _ -> false
+
+let rec mem cmp x = function
+    [] -> false
+  | v::l ->
+      let c = cmp x v in
+        c = 0 || mem cmp x l
+
+let singleton x = [x]
+
+let rec remove cmp x = function
+    [] -> []
+  | v::l ->
+      let c = cmp x v in
+        if c = 0 then remove cmp x l else
+          v::(remove cmp x l)
+
+let compare cmp s1 s2 =
+  raise Not_implemented
+
+let equal cmp s1 s2 =
+  compare cmp s1 s2 = 0
+
+let rec iter f = function
+    [] -> ()
+  | v::l -> iter f l; f v
+
+let rec fold f s accu =
+  match s with
+      [] -> accu
+    | v::l -> f v (fold f l accu)
+
+let map cmp f s = fold (fun e s -> add cmp (f e) s) s empty
+
+let rec for_all p = function
+    [] -> true
+  | v::l -> p v && for_all p l
+
+let rec exists p = function
+    [] -> false
+  | v::l -> p v || exists p l
+  
+let rec subset cmp s1 s2 =
+  for_all (fun e -> mem cmp e s2) s1
+
+let filter cmp p s =
+  let rec filt accu = function
+    | [] -> accu
+    | v::r ->
+        filt (if p v then add cmp v accu else accu) r in
+    filt [] s
+
+let partition cmp p s =
+  let rec part (l, r as accu) = function
+    | [] -> accu
+    | h::t ->
+        part (if p h then (add cmp h l, r) else (l, add cmp h r)) t in
+    part ([], []) s
+
+let rec union cmp s1 s2 =
+  match s1 with 
+      [] -> s2
+    | v::l -> v::(union cmp l s2)
+
+let rec inter cmp s1 s2 =
+  filter cmp (fun e -> mem cmp e s2) s1
+
+let rec cardinal cmp = function
+    [] -> 0
+  | h::t -> (cardinal cmp (remove cmp h t)) + 1
+
+let elements s =
+  s
+  
+let diff cmp s s = 
+  raise Not_implemented
+  
+let min_elt s = 
+  raise Not_implemented
+
+let max_elt s = 
+  raise Not_implemented
+
+let split cmp x s =
+  raise Not_implemented
+
+(* It's not determenistic in the sense that s1.choose = s2.choose given that s1 equals s2 *)
+let choose = function
+    [] -> raise Not_found
+  | h::_ -> h
+
+type 'a set = { cmp : 'a -> 'a -> int; s : 'a rep }
+             
+let empty c = { cmp = c; s = []; }
+
+let is_empty s = is_empty s.s
+
+let mem x s = mem s.cmp x s.s
+
+let add x s = { s with s = add s.cmp x s.s }
+
+let singleton c x = { cmp = c; s = singleton x }
+
+let remove x s = { s with s = remove s.cmp x s.s }
+
+let union s1 s2 = { s1 with s = union s1.cmp s1.s s2.s }
+
+let inter s1 s2 = { s1 with s = inter s1.cmp s1.s s2.s }
+
+let diff s1 s2 = { s1 with s = diff s1.cmp s1.s s2.s }
+
+let compare s1 s2 = compare s1.cmp s1.s s2.s
+
+let equal s1 s2 = equal s1.cmp s1.s s2.s
+
+let subset s1 s2 = subset s1.cmp s1.s s2.s
+
+let iter f s = iter f s.s
+
+let fold f s a = fold f s.s a
+
+let map c f s = {cmp = c; s = map c f s.s}
+
+let for_all p s = for_all p s.s
+
+let exists p s = exists p s.s
+
+let filter p s = { s with s = filter s.cmp p s.s }
+
+let partition p s =
+  let (r1,r2) = partition s.cmp p s.s in
+    ({s with s = r1}, {s with s = r2})
+
+let cardinal s = cardinal s.cmp s.s
+
+let elements s = elements s.s
+
+let min_elt s = min_elt s.s
+
+let max_elt s = max_elt s.s
+
+let choose s = choose s.s
+
+let split x s =
+  let (l,present,r) = split s.cmp x s.s in
+    ({ s with s = l }, present, { s with s = r })
+
+let from_list c l =
+  {cmp = c; s = l}
+
+let comprehension1 cmp f p s =
+  fold (fun x s -> if p x then add (f x) s else s) s (empty cmp) 
+
+let comprehension2 cmp f p s1 s2 =
+  fold
+    (fun x1 s -> 
+       fold 
+         (fun x2 s ->
+            if p x1 x2 then add (f x1 x2) s else s)
+         s2
+         s) 
+    s1 
+    (empty cmp) 
+
+let comprehension3 cmp f p s1 s2 s3 =
+  fold 
+    (fun x1 s -> 
+       fold 
+         (fun x2 s -> 
+            fold 
+              (fun x3 s ->
+                 if p x1 x2 x3 then add (f x1 x2 x3) s else s)
+              s3
+              s)
+         s2
+         s) 
+    s1 
+    (empty cmp) 
+
+let comprehension4 cmp f p s1 s2 s3 s4 =
+  fold 
+    (fun x1 s -> 
+       fold 
+         (fun x2 s -> 
+            fold 
+              (fun x3 s -> 
+                 fold 
+                   (fun x4 s ->
+                      if p x1 x2 x3 x4 then add (f x1 x2 x3 x4) s else s)
+                   s4
+                   s)
+              s3
+              s)
+         s2
+         s) 
+    s1 
+    (empty cmp) 
+
+let comprehension5 cmp f p s1 s2 s3 s4 s5 =
+  fold 
+    (fun x1 s -> 
+       fold 
+         (fun x2 s -> 
+            fold 
+              (fun x3 s -> 
+                 fold 
+                   (fun x4 s -> 
+                      fold 
+                        (fun x5 s ->
+                           if p x1 x2 x3 x4 x5 then add (f x1 x2 x3 x4 x5) s else s)
+                        s5
+                        s)
+                   s4
+                   s)
+              s3
+              s)
+         s2
+         s) 
+    s1 
+    (empty cmp) 
+
+let comprehension6 cmp f p s1 s2 s3 s4 s5 s6 =
+  fold 
+    (fun x1 s -> 
+       fold 
+         (fun x2 s -> 
+            fold 
+              (fun x3 s -> 
+                 fold 
+                   (fun x4 s -> 
+                      fold 
+                        (fun x5 s -> 
+                           fold 
+                             (fun x6 s -> 
+                                if p x1 x2 x3 x4 x5 x6 then add (f x1 x2 x3 x4 x5 x6) s else s)
+                             s6
+                             s)
+                        s5
+                        s)
+                   s4
+                   s)
+              s3
+              s)
+         s2
+         s) 
+    s1 
+    (empty cmp) 
+
+let comprehension7 cmp f p s1 s2 s3 s4 s5 s6 s7 =
+  fold 
+    (fun x1 s -> 
+       fold 
+         (fun x2 s -> 
+            fold 
+              (fun x3 s -> 
+                 fold 
+                   (fun x4 s -> 
+                      fold 
+                        (fun x5 s -> 
+                           fold 
+                             (fun x6 s -> 
+                                fold 
+                                  (fun x7 s -> 
+                                     if p x1 x2 x3 x4 x5 x6 x7 then add (f x1 x2 x3 x4 x5 x6 x7) s else s)
+                                  s7
+                                  s)
+                             s6
+                             s)
+                        s5
+                        s)
+                   s4
+                   s)
+              s3
+              s)
+         s2
+         s) 
+    s1 
+    (empty cmp) 
+
+let bigunion c xss =
+  fold union xss (empty c)
+
+let rec lfp s f =
+  let s' = f s in
+    if subset s' s then
+      s
+    else
+      lfp (union s' s) f
+
+let cross c xs ys = 
+  fold (fun x xys -> fold (fun y xys -> add (x,y) xys) ys xys) xs (empty c)
+
+let rec lfp s f =
+  let s' = f s in
+    if subset s' s then
+      s
+    else
+      lfp (union s' s) f
+
+let tc c r =
+  let one_step r = fold (fun (x,y) xs -> fold (fun (y',z) xs ->
+     if y = y' then add (x,z) xs else xs) r xs) r (empty c) in
+  lfp r one_step
diff --git a/lib/ocaml_rts/linksem/src_lem_library/sum.ml b/lib/ocaml_rts/linksem/src_lem_library/sum.ml
new file mode 100644
index 00000000..a9ea35ae
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/sum.ml
@@ -0,0 +1,4 @@
+type ('a, 'b) sum  = 
+  | Inl of ('a)
+  | Inr of ('b)
+
diff --git a/lib/ocaml_rts/linksem/src_lem_library/vector.ml b/lib/ocaml_rts/linksem/src_lem_library/vector.ml
new file mode 100644
index 00000000..ff9ddb24
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/vector.ml
@@ -0,0 +1,35 @@
+open Nat_num
+
+type 'a vector = Vector of 'a array
+
+let vconcat (Vector a) (Vector b) = Vector(Array.append a b)
+
+let vmap f (Vector a) = Vector(Array.map f a)
+
+let vfold f base (Vector a) = Array.fold_left f base a
+
+let vzip (Vector a) (Vector b) =
+    Vector( Array.of_list (List.combine (Array.to_list a) (Array.to_list b)))
+
+let vmapacc f (Vector a) base =
+  let rec mapacc vl b = match vl with
+         | [] -> ([],b)
+         | v::vl -> let (v',b') = f v b in 
+                    let (vl',b'') = mapacc vl b' in
+                    (v'::vl',b'') in
+  let vls,b = mapacc (Array.to_list a) base in
+  Vector(Array.of_list vls),b
+
+let vmapi f (Vector a) = Vector(Array.mapi f a)
+
+let extend default size (Vector a) = Vector(Array.append (Array.make size default) a)
+
+let duplicate (Vector a) = Vector(Array.append a (Array.copy a))
+
+let vlength (Vector a) = Array.length a
+
+let vector_access n (Vector a) = a.(n)
+
+let vector_slice n1 n2 (Vector a) = Vector(Array.sub a n1 n2)
+
+let make_vector vs l = Vector(Array.of_list vs)
\ No newline at end of file
diff --git a/lib/ocaml_rts/linksem/src_lem_library/vector.mli b/lib/ocaml_rts/linksem/src_lem_library/vector.mli
new file mode 100644
index 00000000..fbbe11ab
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/vector.mli
@@ -0,0 +1,28 @@
+open Nat_num
+
+type 'a vector = Vector of  'a array
+
+val vconcat : 'a vector -> 'a vector -> 'a vector 
+
+val vmap : ('a ->'b) ->  'a vector  -> 'b vector 
+
+val vfold :  ('b -> 'a -> 'b) -> 'b -> 'a vector -> 'b
+
+val vzip : 'a vector -> 'b vector -> ('a * 'b) vector 
+
+val vmapacc : ('a -> 'c -> ('b * 'c)) -> 'a vector -> 'c -> ('b vector) * 'c
+
+val vmapi : (nat -> 'a -> 'b) -> 'a vector -> 'b vector
+
+val extend : 'a -> nat -> 'a vector -> 'a vector
+
+val duplicate : 'a vector -> 'a vector
+
+val vlength : 'a vector -> nat
+
+val vector_access : nat ->'a vector -> 'a
+
+val vector_slice : nat -> nat ->'a vector -> 'a vector
+
+val make_vector : 'a list -> nat -> 'a vector
+
diff --git a/lib/ocaml_rts/linksem/src_lem_library/xstring.ml b/lib/ocaml_rts/linksem/src_lem_library/xstring.ml
new file mode 100644
index 00000000..7a705aeb
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/xstring.ml
@@ -0,0 +1,22 @@
+let explode s = 
+  let rec exp i l =
+    if i < 0 then l else exp (i - 1) (s.[i] :: l) in
+  exp (String.length s - 1) [];;
+
+let implode l = 
+  let res = String.create (List.length l) in
+  let rec imp i = function
+  | [] -> res
+  | c :: l -> res.[i] <- c; imp (i + 1) l in
+  imp 0 l;;
+
+let string_case s c_empty c_cons = begin
+  let len = String.length s in
+  if (len = 0) then c_empty else
+  c_cons (String.get s 0) (String.sub s 1 (len - 1))
+end;;
+
+let cons_string c s = begin
+  let cs = String.make 1 c in
+  cs ^ s
+end;;
diff --git a/lib/ocaml_rts/linksem/src_lem_library/xstring.mli b/lib/ocaml_rts/linksem/src_lem_library/xstring.mli
new file mode 100644
index 00000000..aa9182d7
--- /dev/null
+++ b/lib/ocaml_rts/linksem/src_lem_library/xstring.mli
@@ -0,0 +1,4 @@
+val explode : string -> char list
+val implode : char list -> string
+val cons_string : char -> string -> string
+val string_case : string -> 'a -> (char -> string -> 'a) -> 'a