avl example continued (WIP)

examples/in_progress/avl/association_list.mlw

+
+(* Association lists. *)
+
+(* Association with respect to an equivalence relation. *)
+module Assoc
+  
+  clone import key_type.KeyType as K
+  clone import relations_params.EquivalenceParam as Eq with type t = key
+  
+  use import list.List
+  use import list.Mem
+  use import option.Option
+  use import HighOrd
+  
+  predicate appear (p:param 'a) (k:key 'a) (l:list (t 'a 'b)) =
+    exists x. mem x l /\ correct_for p k /\ Eq.rel p k (key x)
+  
+  (* Correction. *)
+  predicate correct (p:param 'a) (l:list (t 'a 'b)) = match l with
+    | Nil -> true
+    | Cons x q -> let kx = key x in correct_for p kx /\ correct p q
+    end
+  
+  (* Unique occurence (a desirable property of an association list). *)
+  predicate unique (p:param 'a) (l:list (t 'a 'b)) = match l with
+    | Nil -> true
+    | Cons x q -> not appear p (key x) q /\ unique p q
+    end
+  
+  (* functional update with equivalence classes. *)
+  function param_update (p:param 'a) (f:key 'a -> 'b)
+    (k:key 'a) (b:'b) : key 'a -> 'b = \k2.
+      if Eq.rel p k k2 then b else f k2
+  
+  (* functional model of an association list. *)
+  function model (p:param 'a) (l:list (t 'a 'b)) : key 'a -> option (t 'a 'b) =
+    match l with
+    | Nil -> \x. None
+    | Cons d q -> param_update p (model p q) (key d) (Some d)
+    end
+  
+  (* A key is bound iff it occurs in the association lists. *)
+  let rec lemma model_occurence (p:param 'a) (k:key 'a)
+    (l:list (t 'a 'b)) : unit
+    requires { correct p l }
+    requires { correct_for p k }
+    ensures { appear p k l <-> match model p l k with None -> false
+      | Some _ -> true end }
+    variant { l }
+  = match l with Cons _ q -> model_occurence p k q | _ -> () end
+  
+  (* A key is bound to a value with an equivalent key. *)
+  let rec lemma model_link (p:param 'a) (k:key 'a) (l:list (t 'a 'b)) : unit
+    requires { correct p l }
+    requires { correct_for p k }
+    ensures { match model p l k with None -> true
+      | Some d -> Eq.rel p k (key d) end }
+    variant { l }
+  = match l with Cons _ q -> model_link p k q | _ -> () end
+  
+  (* Two equivalent keys are bound to the same value. *)
+  let rec lemma model_equal (p:param 'a) (k1 k2:key 'a)
+    (l:list (t 'a 'b)) : unit
+    requires { correct p l }
+    requires { correct_for p k1 /\ correct_for p k2 }
+    requires { Eq.rel p k1 k2 }
+    ensures { model p l k1 = model p l k2 }
+    variant { l }
+  = match l with Cons _ q -> model_equal p k1 k2 q | _ -> () end
+  
+  (* If the list satisfies the uniqueness property,
+     then every value occuring in the list is the image of its key. *)
+  let rec lemma model_unique (p:param 'a) (k:key 'a) (l:list (t 'a 'b)) : unit
+    requires { correct p l }
+    requires { unique p l }
+    requires { correct_for p k }
+    ensures { forall d. mem d l -> model p l (key d) = Some d }
+    variant { l }
+  = match l with Cons _ q -> model_unique p k q | _ -> () end
+  
+end
+
+
+(* Sorted (increasing) association list. *)
+
+module AssocSorted
+  
+  use import list.List
+  use import list.Append
+  use import list.Mem
+  use import option.Option
+  
+  clone import key_type.KeyType as K
+  clone import preorder.FullParam as O with type t = key
+  (* The commented out part do not work, unfortunately. *)
+  clone export Assoc with namespace K = K,(*namespace Eq = O.Eq*)
+      type Eq.param = O.order,
+      predicate Eq.correct_for = O.correct_for,
+      predicate Eq.rel = O.eq,
+      (* Duplicates, there is no need to keep them. *)
+      goal Eq.trans,
+      goal Eq.refl,
+      goal Eq.symm
+  clone sorted.Increasing as S with namespace K = K,
+    (*namespace O = O.Lt*)
+    type O.param = O.order,
+    predicate O.correct_for = O.correct_for,
+    predicate O.rel = O.lt,
+    goal O.trans
+  
+  (* Sorted lists are correct association lists with unicity property. *)
+  let rec lemma increasing_unique_and_correct (o:order 'a)
+    (l:list (t 'a 'b)) : unit
+    requires { S.increasing o l }
+    ensures { correct o l }
+    ensures { unique o l }
+    variant { l }
+  = match l with Cons _ q -> increasing_unique_and_correct o q | _ -> () end
+  
+  let lemma absent (o:order 'a) (k:key 'a) (l r:list (t 'a 'b)) : unit
+    requires { correct_for o k }
+    requires { S.increasing o l }
+    requires { S.increasing o r }
+    requires { S.majorate o k l }
+    requires { S.minorate o k r }
+    ensures { model o (l++r) k = None }
+  = assert { S.precede o l r && not appear o k (l++r) &&
+    match model o (l++r) k with None -> true | _ -> false end }
+  
+  let lemma present (o:order 'a) (k:key 'a) (l r:list (t 'a 'b))
+    (d:t 'a 'b) : unit
+    requires { correct_for o k }
+    requires { correct_for o (key d) }
+    requires { S.increasing o l }
+    requires { S.increasing o r }
+    requires { S.majorate o k l }
+    requires { S.minorate o k r }
+    requires { eq o k (key d) }
+    ensures { model o (l++Cons d r) k = Some d }
+  = assert { S.increasing o (l++Cons d r) }
+  
+end
+

examples/in_progress/avl/key_type.mlw

+
+(* Type with a key. Intended to factor elements/bindings representations
+   in sets/map-like structures.
+   Typical instantiation:
+     - Set elements, t 'a 'b = key 'a, get_key = id:
+       the only information one can retrieve
+       from a key is presence.
+     - Map bindings, t 'a 'b = (key 'a,value 'b),get_key = fst:
+       one can also retrieve a value from a present binding. *)
+theory KeyType
+  
+  type t 'a 'b
+  type key 'a
+  function key (t 'a 'b) : key 'a
+  
+end
+
+(* program version. *)
+module ProgramKeyType
+  
+  clone export program_type.Type2
+  clone program_type.Type1 as Key
+  function key_m (m 'a 'b) : Key.m 'a
+  val key (x:t 'a 'b) : Key.t 'a
+    requires { c x }
+    ensures { Key.c result }
+    ensures { x.m.key_m = result.Key.m }
+  
+end
+

examples/in_progress/avl/key_type/why3session.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="4">
+ <file
+  name="../key_type.mlw"
+  verified="true"
+  expanded="true">
+  <theory
+   name="KeyType"
+   locfile="../key_type.mlw"
+   loclnum="3" loccnumb="7" loccnume="14"
+   verified="true"
+   expanded="true">
+  </theory>
+  <theory
+   name="ProgramKeyType"
+   locfile="../key_type.mlw"
+   loclnum="12" loccnumb="7" loccnume="21"
+   verified="true"
+   expanded="true">
+  </theory>
+ </file>
+</why3session>

examples/in_progress/avl/preorder.mlw

+
+(* Full preorder theory,
+   containing lt and eq as well. *)
+theory FullParam
+  
+  type t 'a
+  type order 'a
+  predicate le (order 'a) (t 'a) (t 'a)
+  clone export relations_params.PreOrderParam with type t = t,
+    type param = order, predicate rel = le
+  predicate eq (order 'a) (t 'a) (t 'a)
+  axiom eq_def : forall o:order 'a,x y:t 'a.
+    correct_for o x /\ correct_for o y ->
+      (eq o x y <-> le o x y /\ le o y x)
+  predicate lt (order 'a) (t 'a) (t 'a)
+  axiom lt_def : forall o:order 'a,x y:t 'a.
+    correct_for o x /\ correct_for o y ->
+      (lt o x y <-> le o x y /\ not le o y x)
+  
+  clone relations_params.EquivalenceParam as Eq with type t = t,
+    type param = order, predicate correct_for = correct_for,
+    predicate rel = eq, lemma trans, lemma refl, lemma symm
+  
+  clone relations_params.PartialStrictOrderParam as Lt with type t = t,
+    type param = order, predicate correct_for = correct_for,
+    predicate rel = lt, lemma trans, lemma asymm
+  
+end
+
+(* Preorder + corresponding computable comparison. *)
+module ComputableParam
+  
+  use import int.Int
+  clone export program_type.Type1
+  clone program_type.Type1 as O
+  clone export FullParam with type t = m, type order = O.m
+  
+  (* Comparison is computable. *)
+  val compare (o:O.t 'a) (x y:t 'a) : int
+    requires { O.c o }
+    requires { correct_for o.O.m x.m /\ c x }
+    requires { correct_for o.O.m y.m /\ c y }
+    ensures { result > 0 <-> lt o.O.m y.m x.m }
+    ensures { result < 0 <-> lt o.O.m x.m y.m }
+    ensures { result = 0 <-> eq o.O.m x.m y.m }
+  
+end
+

examples/in_progress/avl/preorder/why3session.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="4">
+ <prover
+  id="0"
+  name="Alt-Ergo"
+  version="0.95.2"/>
+ <file
+  name="../preorder.mlw"
+  verified="true"
+  expanded="false">
+  <theory
+   name="FullParam"
+   locfile="../preorder.mlw"
+   loclnum="4" loccnumb="7" loccnume="16"
+   verified="true"
+   expanded="false">
+   <goal
+    name="refl"
+    locfile="../relations_params.mlw"
+    loclnum="14" loccnumb="8" loccnume="12"
+    sum="16f7adfc697259216b2d1f4f975bf261"
+    proved="true"
+    expanded="false"
+    shape="aeqV0V1V1Iacorrect_forV0V1F">
+    <proof
+     prover="0"
+     timelimit="5"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.01"/>
+    </proof>
+   </goal>
+   <goal
+    name="trans"
+    locfile="../relations_params.mlw"
+    loclnum="26" loccnumb="8" loccnume="13"
+    sum="687df4d536017126286fd2decd0627fe"
+    proved="true"
+    expanded="false"
+    shape="aeqV0V1V3IaeqV0V2V3AaeqV0V1V2Iacorrect_forV0V3Aacorrect_forV0V2Aacorrect_forV0V1F">
+    <proof
+     prover="0"
+     timelimit="5"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.02"/>
+    </proof>
+   </goal>
+   <goal
+    name="symm"
+    locfile="../relations_params.mlw"
+    loclnum="33" loccnumb="8" loccnume="12"
+    sum="a45949b88a62cfa03ff9331b96331060"
+    proved="true"
+    expanded="false"
+    shape="aeqV0V2V1IaeqV0V1V2Iacorrect_forV0V2Aacorrect_forV0V1F">
+    <proof
+     prover="0"
+     timelimit="5"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.01"/>
+    </proof>
+   </goal>
+   <goal
+    name="trans"
+    locfile="../relations_params.mlw"
+    loclnum="26" loccnumb="8" loccnume="13"
+    sum="b8987b6c37bc8fc438d2d31c10ea5758"
+    proved="true"
+    expanded="false"
+    shape="altV0V1V3IaltV0V2V3AaltV0V1V2Iacorrect_forV0V3Aacorrect_forV0V2Aacorrect_forV0V1F">
+    <proof
+     prover="0"
+     timelimit="5"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.02"/>
+    </proof>
+   </goal>
+   <goal
+    name="asymm"
+    locfile="../relations_params.mlw"
+    loclnum="39" loccnumb="8" loccnume="13"
+    sum="2c95d9822b30bcc26431c15fb6a137cc"
+    proved="true"
+    expanded="false"
+    shape="NaltV0V2V1IaltV0V1V2Iacorrect_forV0V2Aacorrect_forV0V1F">
+    <proof
+     prover="0"
+     timelimit="5"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.01"/>
+    </proof>
+   </goal>
+  </theory>
+  <theory
+   name="ComputableParam"
+   locfile="../preorder.mlw"
+   loclnum="31" loccnumb="7" loccnume="22"
+   verified="true"
+   expanded="false">
+  </theory>
+ </file>
+</why3session>

examples/in_progress/avl/program_type.mlw

+
+module Type0
+  
+  (* Program version of the type. *)
+  type t
+  (* Its logical model. *)
+  type m
+  (* Type invariant (c for correct). *)
+  predicate c t
+  (* get logical model (m for model). *)
+  function m t : m
+  
+end
+
+(* Variants with different number of type variables. *)
+
+module Type1
+  
+  type t 'a
+  type m 'a
+  predicate c (t 'a)
+  function m (t 'a) : m 'a
+  
+end
+
+module Type2
+  
+  type t 'a 'b
+  type m 'a 'b
+  predicate c (t 'a 'b)
+  function m (t 'a 'b) : m 'a 'b
+  
+end
+
+

examples/in_progress/avl/program_type/why3session.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="4">
+ <file
+  name="../program_type.mlw"
+  verified="true"
+  expanded="true">
+  <theory
+   name="Type0"
+   locfile="../program_type.mlw"
+   loclnum="2" loccnumb="7" loccnume="12"
+   verified="true"
+   expanded="true">
+  </theory>
+  <theory
+   name="Type1"
+   locfile="../program_type.mlw"
+   loclnum="17" loccnumb="7" loccnume="12"
+   verified="true"
+   expanded="true">
+  </theory>
+  <theory
+   name="Type2"
+   locfile="../program_type.mlw"
+   loclnum="26" loccnumb="7" loccnume="12"
+   verified="true"
+   expanded="true">
+  </theory>
+ </file>
+</why3session>

examples/in_progress/avl/relations_params.mlw

+
+theory EndoRelationParam
+  
+  type param 'a
+  type t 'a
+  predicate correct_for (param 'a) (t 'a)
+  predicate rel (param 'a) (t 'a) (t 'a)
+  
+end
+
+theory ReflexiveParam
+  
+  clone export EndoRelationParam
+  axiom refl : forall p:param 'a,x:t 'a. correct_for p x ->
+    rel p x x
+  
+end
+
+theory IrreflexiveParam
+  clone export EndoRelationParam
+  axiom strict : forall p:param 'a,x:t 'a. correct_for p x -> not rel p x x
+end
+
+theory TransitiveParam
+  clone export EndoRelationParam
+  axiom trans : forall p:param 'a,x y z:t 'a.
+    correct_for p x /\ correct_for p y /\ correct_for p z ->
+      rel p x y /\ rel p y z -> rel p x z
+end
+
+theory SymmetricParam
+  clone export EndoRelationParam
+  axiom symm : forall p:param 'a,x y:t 'a.
+    correct_for p x /\ correct_for p y -> rel p x y -> rel p y x
+end
+
+theory AsymmetricParam
+  clone export EndoRelationParam
+  axiom asymm : forall p:param 'a,x y:t 'a.
+    correct_for p x /\ correct_for p y -> rel p x y -> not rel p y x
+end
+
+theory AntisymmetricParam
+  clone export EndoRelationParam
+  axiom antisymm : forall p:param 'a,x y:t 'a.
+    correct_for p x /\ correct_for p y -> rel p x y -> rel p y x -> x = y
+end
+
+theory TotalParam
+  clone export EndoRelationParam
+  axiom total : forall p:param 'a,x y:t 'a.
+    correct_for p x /\ correct_for p y -> rel p x y \/ rel p y x
+end
+
+theory PreOrderParam
+  clone export ReflexiveParam
+  clone export TransitiveParam with type t = t,
+    type param = param, predicate correct_for = correct_for,
+    predicate rel = rel
+end
+
+theory EquivalenceParam
+  clone export PreOrderParam
+  clone export SymmetricParam with type t = t,
+    type param = param, predicate correct_for = correct_for,
+    predicate rel = rel
+end
+
+theory TotalPreOrderParam
+  clone export PreOrderParam
+  clone export TotalParam with type t = t,
+    type param = param, predicate correct_for = correct_for,
+    predicate rel = rel
+end
+
+theory PartialOrderParam
+  clone export PreOrderParam
+  clone export AntisymmetricParam with type t = t,
+    type param = param, predicate correct_for = correct_for,
+    predicate rel = rel
+end
+
+theory TotalOrderParam
+  clone export PartialOrderParam
+  clone export TotalParam with type t = t,
+    type param = param, predicate correct_for = correct_for,
+    predicate rel = rel
+end
+
+theory PartialStrictOrderParam
+  clone export TransitiveParam
+  clone export AsymmetricParam with type t = t,
+    type param = param, predicate correct_for = correct_for,
+    predicate rel = rel
+end
+
+theory TotalStrictOrderParam
+  clone export PartialStrictOrderParam
+  axiom trichotomy : forall p:param 'a,x y:t 'a.
+    correct_for p x /\ correct_for p y ->
+      rel p x y \/ rel p y x \/ x = y
+end
+
+theory InverseParam
+  
+  clone export EndoRelationParam
+  predicate inv_rel (p:param 'a) (x y : t 'a) = rel p y x
+  
+end
+
+

examples/in_progress/avl/relations_params/why3session.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="4">
+ <file
+  name="../relations_params.mlw"
+  verified="true"
+  expanded="false">
+  <theory
+   name="EndoRelationParam"
+   locfile="../relations_params.mlw"
+   loclnum="2" loccnumb="7" loccnume="24"
+   verified="true"
+   expanded="false">
+  </theory>
+  <theory
+   name="ReflexiveParam"
+   locfile="../relations_params.mlw"
+   loclnum="11" loccnumb="7" loccnume="21"
+   verified="true"
+   expanded="false">
+  </theory>
+  <theory
+   name="IrreflexiveParam"
+   locfile="../relations_params.mlw"
+   loclnum="19" loccnumb="7" loccnume="23"
+   verified="true"
+   expanded="false">
+  </theory>
+  <theory
+   name="TransitiveParam"
+   locfile="../relations_params.mlw"
+   loclnum="24" loccnumb="7" loccnume="22"
+   verified="true"
+   expanded="false">
+  </theory>
+  <theory
+   name="SymmetricParam"
+   locfile="../relations_params.mlw"
+   loclnum="31" loccnumb="7" loccnume="21"
+   verified="true"
+   expanded="false">
+  </theory>
+  <theory
+   name="AsymmetricParam"
+   locfile="../relations_params.mlw"
+   loclnum="37" loccnumb="7" loccnume="22"
+   verified="true"
+   expanded="false">
+  </theory>
+  <theory
+   name="AntisymmetricParam"
+   locfile="../relations_params.mlw"
+   loclnum="43" loccnumb="7" loccnume="25"
+   verified="true"
+   expanded="false">
+  </theory>
+  <theory
+   name="TotalParam"
+   locfile="../relations_params.mlw"
+   loclnum="49" loccnumb="7" loccnume="17"
+   verified="true"
+   expanded="false">
+  </theory>
+  <theory
+   name="PreOrderParam"
+   locfile="../relations_params.mlw"
+   loclnum="55" loccnumb="7" loccnume="20"
+   verified="true"
+   expanded="false">
+  </theory>
+  <theory
+   name="EquivalenceParam"
+   locfile="../relations_params.mlw"
+   loclnum="62" loccnumb="7" loccnume="23"
+   verified="true"
+   expanded="false">
+  </theory>
+  <theory
+   name="TotalPreOrderParam"
+   locfile="../relations_params.mlw"
+   loclnum="69" loccnumb="7" loccnume="25"
+   verified="true"
+   expanded="false">
+  </theory>
+  <theory
+   name="PartialOrderParam"
+   locfile="../relations_params.mlw"
+   loclnum="76" loccnumb="7" loccnume="24"
+   verified="true"
+   expanded="false">
+  </theory>
+  <theory
+   name="TotalOrderParam"
+   locfile="../relations_params.mlw"
+   loclnum="83" loccnumb="7" loccnume="22"
+   verified="true"
+   expanded="false">
+  </theory>
+  <theory
+   name="PartialStrictOrderParam"
+   locfile="../relations_params.mlw"
+   loclnum="90" loccnumb="7" loccnume="30"
+   verified="true"
+   expanded="false">
+  </theory>
+  <theory
+   name="TotalStrictOrderParam"
+   locfile="../relations_params.mlw"
+   loclnum="97" loccnumb="7" loccnume="28"
+   verified="true"
+   expanded="false">
+  </theory>
+  <theory
+   name="InverseParam"
+   locfile="../relations_params.mlw"
+   loclnum="104" loccnumb="7" loccnume="19"
+   verified="true"
+   expanded="false">
+  </theory>
+ </file>
+</why3session>

examples/in_progress/avl/sorted.mlw

+
+(* sorted list, with respect to a key and an ordering parameter. *)
+
+theory Base
+  
+  use import list.List
+  use import list.Mem
+  
+  clone import key_type.KeyType as K
+  clone import relations_params.TransitiveParam as O with type t = key
+  
+  predicate minorate (o:param 'a) (x:key 'a) (l:list (t 'a 'b)) =
+    (forall y. mem y l -> let ky = key y in
+      correct_for o ky /\ rel o x ky)
+  
+  predicate majorate (o:param 'a) (x:key 'a) (l:list (t 'a 'b)) =
+    (forall y. mem y l -> let ky = key y in
+      correct_for o ky /\ rel o ky x)
+  
+  predicate precede (o:param 'a) (l1 l2:list (t 'a 'b)) =
+    (forall x y. mem x l1 /\ mem y l2 -> let kx = key x in
+      let ky = key y in
+      correct_for o kx /\ correct_for o ky /\ rel o kx ky)
+  
+  lemma minorate_by_smaller : forall o:param 'a,kdown kup:key 'a,
+    l:list (t 'a 'b).
+    correct_for o kdown /\ correct_for o kup /\
+    minorate o kup l /\ rel o kdown kup -> minorate o kdown l
+  
+  lemma majorate_by_bigger : forall p:param 'a,kdown kup:key 'a,
+    l:list (t 'a 'b).
+    correct_for p kdown /\ correct_for p kup /\
+    majorate p kdown l /\ rel p kdown kup -> majorate p kup l
+  
+end
+
+module Increasing
+  
+  clone export Base
+  use import list.List
+  use import list.Append
+  use import list.Mem
+  
+  predicate increasing (o:O.param 'a) (l:list (K.t 'a 'b)) =
+    match l with
+    | Nil -> true
+    | Cons x q -> let kx = K.key x in
+      O.correct_for o kx /\ minorate o kx q /\ increasing o q
+    end
+  
+  let rec lemma increasing_precede (o:O.param 'a) (l r:list (K.t 'a 'b))
+    ensures { increasing o l /\ increasing o r /\ precede o l r <->
+      increasing o (l++r) }
+    variant { l }
+  = match l with
+    | Nil -> ()
+    | Cons x q -> let kx = K.key x in
+      assert { increasing o (l++r) <-> increasing o (q++r) /\
+        minorate o kx (q++r) /\ O.correct_for o kx };
+      increasing_precede o q r
+    end
+  
+  let lemma increasing_midpoint (o:O.param 'a) (l:list (K.t 'a 'b))
+    (x:K.t 'a 'b) (r:list (K.t 'a 'b)) : unit
+    ensures { let kx = K.key x in
+      increasing o l /\ increasing o r /\ O.correct_for o kx /\
+      minorate o kx r /\ majorate o kx l <-> increasing o (l++Cons x r) }
+  = ()
+  
+  let lemma increasing_snoc (o:O.param 'a) (l:list (K.t 'a 'b))
+    (x:K.t 'a 'b) : unit
+    ensures { let kx = K.key x in
+      increasing o (l++Cons x Nil) <-> increasing o l /\ majorate o kx l /\
+        O.correct_for o kx }
+  = ()
+  
+end