Definition: set-sig
set-sig{i:l}(Item) ==
  "set":{s:Type| valueall-type(Item)  valueall-type(s)} 
  "member":Item ─→ self."set" ─→ 𝔹
  "empty":{s:self."set"| ∀x:Item. (¬↑(self."member" s))} 
  "isEmpty":{f:self."set" ─→ 𝔹| ∀s:self."set". (↑(f s) ⇐⇒ ∀x:Item. (¬↑(self."member" s)))} 
  "singleton":{f:Item ─→ self."set"| ∀x,y:Item.  (↑(self."member" (f y)) ⇐⇒ y ∈ Item)} 
  "add":{f:Item ─→ self."set" ─→ self."set"| 
         ∀s:self."set". ∀x,y:Item.  (↑(self."member" (f s)) ⇐⇒ (x y ∈ Item) ∨ (↑(self."member" s)))} 
  "union":{f:self."set" ─→ self."set" ─→ self."set"| 
           ∀s1,s2:self."set". ∀x:Item.
             (↑(self."member" (f s1 s2)) ⇐⇒ (↑(self."member" s1)) ∨ (↑(self."member" s2)))} 
  "remove":{f:Item ─→ self."set" ─→ self."set"| 
            ∀s:self."set". ∀x,y:Item.  (↑(self."member" (f s)) ⇐⇒ (x y ∈ Item)) ∧ (↑(self."member" s)))} 

Lemma: set-sig_wf
[Item:Type]. (set-sig{i:l}(Item) ∈ 𝕌')

Definition: mk-set
mk-set(Item;set;member;empty;isEmpty;singleton;add;union;remove) ==
  λx.x["set" := set]["member" := member]["empty" := empty]["isEmpty" := isEmpty]["singleton" := singleton]["add" := add]
  ["union" := union]["remove" := remove]

Lemma: mk-set_wf
[Item:Type]. ∀[set:{s:Type| valueall-type(Item)  valueall-type(s)} ]. ∀[member:Item ─→ set ─→ 𝔹].
[empty:{s:set| ∀x:Item. (¬↑(member s))} ]. ∀[isEmpty:{f:set ─→ 𝔹| ∀s:set. (↑(f s) ⇐⇒ ∀x:Item. (¬↑(member s)))} ].
[singleton:{f:Item ─→ set| ∀x,y:Item.  (↑(member (f y)) ⇐⇒ y ∈ Item)} ]. ∀[add:{f:Item ─→ set ─→ set| 
                                                                                       ∀s:set. ∀x,y:Item.
                                                                                         (↑(member (f s))
                                                                                         ⇐⇒ (x y ∈ Item)
                                                                                             ∨ (↑(member s)))} ].
[union:{f:set ─→ set ─→ set| ∀s1,s2:set. ∀x:Item.  (↑(member (f s1 s2)) ⇐⇒ (↑(member s1)) ∨ (↑(member s2)))} ].
[remove:{f:Item ─→ set ─→ set| ∀s:set. ∀x,y:Item.  (↑(member (f s)) ⇐⇒ (x y ∈ Item)) ∧ (↑(member s)))} ].
  (mk-set(Item;set;member;empty;isEmpty;singleton;add;union;remove) ∈ set-sig{i:l}(Item))

Definition: set-sig-set
set-sig-set(s) ==  s."set"

Lemma: set-sig-set_wf
[Item:Type]. ∀[s:set-sig{i:l}(Item)].  (set-sig-set(s) ∈ Type)

Lemma: set-sig-set-squash
[Item:Type]. ∀[s:set-sig{i:l}(Item)].  (↓set-sig-set(s))

Lemma: set-sig-set-vatype
[Item:Type]. ∀[s:set-sig{i:l}(Item)].  valueall-type(set-sig-set(s)) supposing valueall-type(Item)

Definition: set-sig-member
set-sig-member(s) ==  s."member"

Lemma: set-sig-member_wf
[Item:Type]. ∀[s:set-sig{i:l}(Item)].  (set-sig-member(s) ∈ Item ─→ set-sig-set(s) ─→ 𝔹)

Definition: set-sig-empty
set-sig-empty(s) ==  s."empty"

Lemma: set-sig-empty_wf
[Item:Type]. ∀[s:set-sig{i:l}(Item)].  (set-sig-empty(s) ∈ set-sig-set(s))

Lemma: set-sig-empty-prop
[Item:Type]. ∀[s:set-sig{i:l}(Item)]. ∀[x:Item].  (¬↑(set-sig-member(s) set-sig-empty(s)))

Lemma: set-sig-empty-prop2
[Item:Type]. ∀[s:set-sig{i:l}(Item)]. ∀[x:Item].  uiff(↑(set-sig-member(s) set-sig-empty(s));False)

Definition: set-sig-isEmpty
set-sig-isEmpty(s) ==  s."isEmpty"

Lemma: set-sig-isEmpty_wf
[Item:Type]. ∀[s:set-sig{i:l}(Item)].  (set-sig-isEmpty(s) ∈ set-sig-set(s) ─→ 𝔹)

Definition: set-sig-singleton
set-sig-singleton(s) ==  s."singleton"

Lemma: set-sig-singleton_wf
[Item:Type]. ∀[s:set-sig{i:l}(Item)].  (set-sig-singleton(s) ∈ Item ─→ set-sig-set(s))

Definition: set-sig-add
set-sig-add(s) ==  s."add"

Lemma: set-sig-add_wf
[Item:Type]. ∀[s:set-sig{i:l}(Item)].  (set-sig-add(s) ∈ Item ─→ set-sig-set(s) ─→ set-sig-set(s))

Lemma: set-sig-add-prop
[Item:Type]
  ∀s:set-sig{i:l}(Item). ∀set:set-sig-set(s). ∀x,y:Item.
    (↑(set-sig-member(s) (set-sig-add(s) set)) ⇐⇒ (x y ∈ Item) ∨ (↑(set-sig-member(s) set)))

Definition: set-sig-union
set-sig-union(s) ==  s."union"

Lemma: set-sig-union_wf
[Item:Type]. ∀[s:set-sig{i:l}(Item)].  (set-sig-union(s) ∈ set-sig-set(s) ─→ set-sig-set(s) ─→ set-sig-set(s))

Definition: set-sig-remove
set-sig-remove(s) ==  s."remove"

Lemma: set-sig-remove_wf
[Item:Type]. ∀[s:set-sig{i:l}(Item)].  (set-sig-remove(s) ∈ Item ─→ set-sig-set(s) ─→ set-sig-set(s))

Definition: in-missing
in-missing(i;missing) ==  reduce(λx,r. (x ≤i ∧b ((x =z i) ∨br));ff;missing)

Lemma: in-missing_wf
[i:ℤ]. ∀[missing:ℤ List].  (in-missing(i;missing) ∈ 𝔹)

Lemma: assert-in-missing
i:ℤ. ∀missing:ℤ List.  ((↑in-missing(i;missing))  (i ∈ missing))

Lemma: assert-in-missing-iff
i:ℤ. ∀missing:{l:ℤ List| l-ordered(ℤ;x,y.x < y;l)} .  (↑in-missing(i;missing) ⇐⇒ (i ∈ missing))

Lemma: assert-in-missing-nat
i:ℕ. ∀missing:ℕ List.  ((↑in-missing(i;missing))  (i ∈ missing))

Lemma: assert-in-missing-nat-iff
i:ℕ. ∀missing:{l:ℕ List| l-ordered(ℕ;x,y.x < y;l)} .  (↑in-missing(i;missing) ⇐⇒ (i ∈ missing))

Definition: nat-missing-type
nat-missing-type() ==  m:{m:ℤ(-1) ≤ m}  × {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} 

Lemma: nat-missing-type_wf
nat-missing-type() ∈ Type

Definition: member-nat-missing
member-nat-missing(i;s) ==  let max,missing in i ≤max ∧b bin-missing(i;missing))

Lemma: member-nat-missing_wf
[i:ℕ]. ∀[s:nat-missing-type()].  (member-nat-missing(i;s) ∈ 𝔹)

Lemma: assert-member-nat-missing
[i:ℕ]. ∀[s:nat-missing-type()].  (↑member-nat-missing(i;s) ⇐⇒ (i ≤ (fst(s))) ∧ (i ∈ snd(s))))

Definition: empty-nat-missing
empty-nat-missing() ==  <-1, []>

Lemma: empty-nat-missing_wf
empty-nat-missing() ∈ nat-missing-type()

Lemma: empty-nat-missing-prop
x:ℕ(¬↑member-nat-missing(x;empty-nat-missing()))

Definition: isEmpty-nat-missing
isEmpty-nat-missing(s) ==  let max,missing in max <0 ∧b null(missing)

Lemma: isEmpty-nat-missing_wf
[s:nat-missing-type()]. (isEmpty-nat-missing(s) ∈ 𝔹)

Lemma: isEmpty-nat-missing-prop
s:nat-missing-type(). (↑isEmpty-nat-missing(s) ⇐⇒ ∀x:ℕ(¬↑member-nat-missing(x;s)))

Definition: singleton-nat-missing
singleton-nat-missing(i) ==  <i, [0, i)>

Lemma: singleton-nat-missing_wf
[i:ℕ]. (singleton-nat-missing(i) ∈ nat-missing-type())

Lemma: singleton-nat-missing-prop
x,y:ℕ.  (↑member-nat-missing(x;singleton-nat-missing(y)) ⇐⇒ y ∈ ℕ)

Definition: add-nat-missing
add-nat-missing(i;s) ==
  let max,missing 
  in if max <then <i, missing [max 1, i)>
     if (max =z i) then <max, missing>
     else <max, remove-combine(λx.(x i);missing)>
     fi 

Lemma: add-nat-missing_wf
[i:ℕ]. ∀[s:nat-missing-type()].  (add-nat-missing(i;s) ∈ nat-missing-type())

Lemma: add-nat-missing-prop
s:nat-missing-type(). ∀x,y:ℕ.
  (↑member-nat-missing(x;add-nat-missing(y;s)) ⇐⇒ (x y ∈ ℕ) ∨ (↑member-nat-missing(x;s)))

Definition: union-nat-missing-pos
union-nat-missing-pos(s1;max;missing) ==
  primrec(max 1;s1;λm,s. if in-missing(m;missing) then else add-nat-missing(m;s) fi )

Lemma: union-nat-missing-pos_wf
[s1:nat-missing-type()]. ∀[max:ℕ]. ∀[missing:ℕ List].  (union-nat-missing-pos(s1;max;missing) ∈ nat-missing-type())

Lemma: union-nat-missing-pos-prop
s1:nat-missing-type(). ∀max:ℕ. ∀missing:{l:ℕ List| l-ordered(ℕ;x,y.x < y;l)} . ∀x:ℕ.
  (↑member-nat-missing(x;union-nat-missing-pos(s1;max;missing))
  ⇐⇒ (↑member-nat-missing(x;s1)) ∨ ((x ≤ max) ∧ (x ∈ missing))))

Definition: union-nat-missing
union-nat-missing(s1;s2) ==  let max,missing s2 in if 0 ≤max then union-nat-missing-pos(s1;max;missing) else s1 fi 

Lemma: union-nat-missing_wf
[s1,s2:nat-missing-type()].  (union-nat-missing(s1;s2) ∈ nat-missing-type())

Lemma: union-nat-missing-prop
s1,s2:nat-missing-type(). ∀x:ℕ.
  (↑member-nat-missing(x;union-nat-missing(s1;s2)) ⇐⇒ (↑member-nat-missing(x;s1)) ∨ (↑member-nat-missing(x;s2)))

Definition: select-last-in-nat-missing
select-last-in-nat-missing(max;missing) ==
  primrec(max;if in-missing(0;missing) then -1 else fi m,r. if in-missing(m;missing) then else fi )

Lemma: select-last-in-nat-missing_wf
[max:ℕ]. ∀[missing:{l:ℕ List| l-ordered(ℕ;x,y.x < y;l)} ].
  (select-last-in-nat-missing(max;missing) ∈ {x:ℤ
                                              ((-1) ≤ x)
                                              ∧ (x ≤ max)
                                              ∧ ((0 ≤ x)  (x ∈ missing)))
                                              ∧ (∀y:ℕ((¬(y ∈ missing))  y < max  (y ≤ x)))
                                              ∧ (∀y:ℕ(y < max  x <  (y ∈ missing)))} )

Definition: remove-nat-missing
remove-nat-missing(i;s) ==
  let max,missing 
  in if (i =z max)
       then if null(missing)
            then <max 1, []>
            else eval last(missing) in
                 if (x =z max 1) then eval select-last-in-nat-missing(x;missing) in <n, filter(λx.x <n;missing)>\000C else <max 1, missing> fi 
            fi 
     if max <then <max, missing>
     else <max, insert-combine(int-minus-comparison-inc(λx.x);λi,a. i;i;missing)>
     fi 

Lemma: remove-nat-missing_wf
[i:ℕ]. ∀[s:nat-missing-type()].  (remove-nat-missing(i;s) ∈ nat-missing-type())

Lemma: remove-nat-missing-prop
s:nat-missing-type(). ∀x,y:ℕ.
  (↑member-nat-missing(x;remove-nat-missing(y;s)) ⇐⇒ (x y ∈ ℕ)) ∧ (↑member-nat-missing(x;s)))

Definition: mk-set-nat-missing
mk-set-nat-missing() ==
  mk-set(ℕ;nat-missing-type();λi,s. member-nat-missing(i;s);empty-nat-missing();λs.isEmpty-nat-missing(s);
         λi.singleton-nat-missing(i);λi,s. add-nat-missing(i;s);λs1,s2. union-nat-missing(s1;s2);λi,s. remove-nat-missin\000Cg(i;s))

Lemma: mk-set-nat-missing_wf
mk-set-nat-missing() ∈ set-sig{i:l}(ℕ)

Definition: map-sig
map-sig{i:l}(Key;Value) ==
  "map":{m:Type| (valueall-type(m)) supposing (valueall-type(Value) and valueall-type(Key))} 
  "eqKey":EqDecider(Key)
  "find":Key ─→ self."map" ─→ (Value?)
  "inDom":{f:Key ─→ self."map" ─→ 𝔹| ∀k:Key. ∀m:self."map".  (↑(f m) ⇐⇒ ↑isl(self."find" m))} 
  "empty":{m:self."map"| ∀k:Key. (¬↑(self."inDom" m))} 
  "isEmpty":{f:self."map" ─→ 𝔹| ∀m:self."map". (↑(f m) ⇐⇒ ∀k:Key. (¬↑(self."inDom" m)))} 
  "update":{f:Key ─→ Value ─→ self."map" ─→ self."map"| 
            ∀m:self."map". ∀k1,k2:Key. ∀v:Value.
              ((self."find" k1 (f k2 m)) if self."eqKey" k1 k2 then inl else self."find" k1 fi  ∈ (Value?))} 
  "add":{f:Key ─→ Value ─→ self."map" ─→ self."map"| 
         ∀m:self."map". ∀k1,k2:Key. ∀v:Value.
           ((self."find" k1 (f k2 m))
           if (self."eqKey" k1 k2) ∧b b(self."inDom" k2 m)) then inl else self."find" k1 fi 
           ∈ (Value?))} 
  "remove":{f:Key ─→ self."map" ─→ self."map"| 
            ∀m:self."map". ∀k1,k2:Key.
              ((self."find" k1 (f k2 m)) if self."eqKey" k1 k2 then inr ⋅  else self."find" k1 fi  ∈ (Value?))} 

Lemma: map-sig_wf
[Key,Value:Type].  (map-sig{i:l}(Key;Value) ∈ 𝕌')

Definition: mk-map
mk-map(Key;Value;map;eqKey;find;inDom;empty;isEmpty;update;add;remove) ==
  λx.x["map" := map]["eqKey" := eqKey]["find" := find]["inDom" := inDom]["empty" := empty]["isEmpty" := isEmpty]
  ["update" := update]["add" := add]["remove" := remove]

Lemma: mk-map_wf
[Key,Value:Type]. ∀[map:{m:Type| (valueall-type(m)) supposing (valueall-type(Value) and valueall-type(Key))} ].
[eqKey:EqDecider(Key)]. ∀[find:Key ─→ map ─→ (Value?)]. ∀[inDom:{f:Key ─→ map ─→ 𝔹
                                                                  ∀k:Key. ∀m:map.  (↑(f m) ⇐⇒ ↑isl(find m))} ].
[empty:{m:map| ∀k:Key. (¬↑(inDom m))} ]. ∀[isEmpty:{f:map ─→ 𝔹| ∀m:map. (↑(f m) ⇐⇒ ∀k:Key. (¬↑(inDom m)))} ].
[update:{f:Key ─→ Value ─→ map ─→ map| 
          ∀m:map. ∀k1,k2:Key. ∀v:Value.
            ((find k1 (f k2 m)) if eqKey k1 k2 then inl else find k1 fi  ∈ (Value?))} ].
[add:{f:Key ─→ Value ─→ map ─→ map| 
       ∀m:map. ∀k1,k2:Key. ∀v:Value.
         ((find k1 (f k2 m)) if (eqKey k1 k2) ∧b b(inDom k2 m)) then inl else find k1 fi  ∈ (Value?))} ].
[remove:{f:Key ─→ map ─→ map| 
          ∀m:map. ∀k1,k2:Key.  ((find k1 (f k2 m)) if eqKey k1 k2 then inr ⋅  else find k1 fi  ∈ (Value?))} ].
  (mk-map(Key;Value;map;eqKey;find;inDom;empty;isEmpty;update;add;remove) ∈ map-sig{i:l}(Key;Value))

Definition: map-sig-map
map-sig-map(m) ==  m."map"

Lemma: map-sig-map_wf
[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)].  (map-sig-map(m) ∈ Type)

Lemma: map-sig-map-squash
[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)].  (↓map-sig-map(m))

Lemma: map-sig-map-vatype
[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)].
  (valueall-type(map-sig-map(m))) supposing (valueall-type(Key) and valueall-type(Value))

Definition: map-sig-eqKey
map-sig-eqKey(m) ==  m."eqKey"

Lemma: map-sig-eqKey_wf
[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)].  (map-sig-eqKey(m) ∈ EqDecider(Key))

Definition: map-sig-find
map-sig-find(m) ==  m."find"

Lemma: map-sig-find_wf
[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)].  (map-sig-find(m) ∈ Key ─→ map-sig-map(m) ─→ (Value?))

Definition: map-sig-inDom
map-sig-inDom(m) ==  m."inDom"

Lemma: map-sig-inDom_wf
[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)].  (map-sig-inDom(m) ∈ Key ─→ map-sig-map(m) ─→ 𝔹)

Lemma: map-sig-inDom-prop
[Key,Value:Type]. ∀[ms:map-sig{i:l}(Key;Value)]. ∀[k:Key]. ∀[m:map-sig-map(ms)].
  (↑(map-sig-inDom(ms) m) ⇐⇒ ↑isl(map-sig-find(ms) m))

Definition: map-sig-empty
map-sig-empty(m) ==  m."empty"

Lemma: map-sig-empty_wf
[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)].  (map-sig-empty(m) ∈ map-sig-map(m))

Definition: map-sig-isEmpty
map-sig-isEmpty(m) ==  m."isEmpty"

Lemma: map-sig-isEmpty_wf
[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)].  (map-sig-isEmpty(m) ∈ map-sig-map(m) ─→ 𝔹)

Definition: map-sig-update
map-sig-update(m) ==  m."update"

Lemma: map-sig-update_wf
[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)].  (map-sig-update(m) ∈ Key ─→ Value ─→ map-sig-map(m) ─→ map-sig-map(m))

Definition: map-sig-add
map-sig-add(m) ==  m."add"

Lemma: map-sig-add_wf
[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)].  (map-sig-add(m) ∈ Key ─→ Value ─→ map-sig-map(m) ─→ map-sig-map(m))

Definition: map-sig-remove
map-sig-remove(m) ==  m."remove"

Lemma: map-sig-remove_wf
[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)].  (map-sig-remove(m) ∈ Key ─→ map-sig-map(m) ─→ map-sig-map(m))

Definition: int-decr-map-type
int-decr-map-type(Value) ==  {l:(ℤ × Value) List| l-ordered(ℤ × Value;x,y.(fst(x)) > (fst(y));l)} 

Lemma: int-decr-map-type_wf
[Value:Type]. (int-decr-map-type(Value) ∈ Type)

Lemma: int-decr-map-fun
[Value:Type]. ∀[m:int-decr-map-type(Value)]. ∀[k:ℤ]. ∀[v1,v2:Value].
  (v1 v2 ∈ Value) supposing ((<k, v1> ∈ m) and (<k, v2> ∈ m))

Lemma: int-decr-map-type-member-sq-stable
[Value:Type]. ∀k:ℤ. ∀v:Value. ∀m:int-decr-map-type(Value).  SqStable((<k, v> ∈ m))

Definition: int-decr-map-find
int-decr-map-find(k;m) ==  case find-combine(λp.(k fst(p));m) of inl(x) => inl (snd(x)) inr(x) => inr ⋅ 

Lemma: int-decr-map-find_wf
[Value:Type]. ∀[k:ℤ]. ∀[m:int-decr-map-type(Value)].
  (int-decr-map-find(k;m) ∈ {v:Value| (¬↑null(m)) ∧ (<k, v> ∈ m)}  (↓(∀p∈m.¬(k (fst(p)) ∈ ℤ))))

Lemma: int-decr-map-find-wf
[Value:Type]. ∀[k:ℤ]. ∀[m:int-decr-map-type(Value)].  (int-decr-map-find(k;m) ∈ Value?)

Lemma: int-decr-map-find-prop
[Value:Type]
  ∀k:ℤ. ∀m:int-decr-map-type(Value).
    ((↑isl(int-decr-map-find(k;m)))  ((¬↑null(m)) ∧ (<k, outl(int-decr-map-find(k;m))> ∈ m)))

Lemma: int-decr-map-find-prop2
[Value:Type]. ∀[k:ℤ]. ∀[m:int-decr-map-type(Value)].
  (∀p∈m.¬(k (fst(p)) ∈ ℤ)) supposing ¬↑isl(int-decr-map-find(k;m))

Lemma: int-decr-map-find-not-in
[Value:Type]. ∀[k:ℤ]. ∀[m:int-decr-map-type(Value)].
  int-decr-map-find(k;m) (inr ⋅ ) ∈ (Value?) supposing (∀p∈m.¬(k (fst(p)) ∈ ℤ))

Definition: int-decr-map-inDom
int-decr-map-inDom(k;m) ==  isl(int-decr-map-find(k;m))

Lemma: int-decr-map-inDom_wf
[Value:Type]. ∀[k:ℤ]. ∀[m:int-decr-map-type(Value)].  (int-decr-map-inDom(k;m) ∈ 𝔹)

Lemma: int-decr-map-inDom-prop
[Value:Type]. ∀[k:ℤ]. ∀[m:int-decr-map-type(Value)].  (↑int-decr-map-inDom(k;m) ⇐⇒ ↑isl(int-decr-map-find(k;m)))

Lemma: int-decr-map-inDom-prop1
[Value:Type]
  ∀k:ℤ. ∀m:int-decr-map-type(Value).
    (¬↑null(m)) ∧ (<k, outl(int-decr-map-find(k;m))> ∈ m) supposing ↑int-decr-map-inDom(k;m)

Lemma: int-decr-map-inDom-prop2
[Value:Type]. ∀[k:ℤ]. ∀[m:int-decr-map-type(Value)].  (∀p∈m.¬(k (fst(p)) ∈ ℤ)) supposing ¬↑int-decr-map-inDom(k;m)

Lemma: int-decr-map-inDom-cons
[Value:Type]. ∀[k:ℤ]. ∀[u:ℤ × Value]. ∀[v:int-decr-map-type(Value)].
  (k ≤ (fst(u))) supposing ((↑int-decr-map-inDom(k;[u v])) and (∀y:ℤ × Value. ((y ∈ v)  ((fst(u)) > (fst(y))))))

Definition: int-decr-map-empty
int-decr-map-empty() ==  []

Lemma: int-decr-map-empty_wf
[Value:Type]. (int-decr-map-empty() ∈ int-decr-map-type(Value))

Lemma: int-decr-map-empty-prop
[Value:Type]. ∀[k:ℤ].  (¬↑int-decr-map-inDom(k;int-decr-map-empty()))

Definition: int-decr-map-isEmpty
int-decr-map-isEmpty(m) ==  null(m)

Lemma: int-decr-map-isEmpty_wf
[Value:Type]. ∀[m:int-decr-map-type(Value)].  (int-decr-map-isEmpty(m) ∈ 𝔹)

Lemma: int-decr-map-isEmpty-assert
[Value:Type]. ∀[m:int-decr-map-type(Value)].
  uiff(↑int-decr-map-isEmpty(m);m int-decr-map-empty() ∈ int-decr-map-type(Value))

Lemma: int-decr-map-isEmpty-prop
[Value:Type]. ∀[m:int-decr-map-type(Value)].  (↑int-decr-map-isEmpty(m) ⇐⇒ ∀k:ℤ(¬↑int-decr-map-inDom(k;m)))

Definition: int-decr-map-update
int-decr-map-update(k;v;m) ==  insert-combine(int-minus-comparison(λp.(fst(p)));λx,a. x;<k, v>;m)

Lemma: int-decr-map-update_wf
[Value:Type]. ∀[k:ℤ]. ∀[v:Value]. ∀[m:int-decr-map-type(Value)].
  (int-decr-map-update(k;v;m) ∈ int-decr-map-type(Value))

Lemma: int-decr-map-update-prop
[Value:Type]. ∀[m:int-decr-map-type(Value)]. ∀[k1,k2:ℤ]. ∀[v:Value].
  (int-decr-map-find(k1;int-decr-map-update(k2;v;m))
  if (k1 =z k2) then inl else int-decr-map-find(k1;m) fi 
  ∈ (Value?))

Definition: int-decr-map-add
int-decr-map-add(k;v;m) ==  insert-combine(int-minus-comparison(λp.(fst(p)));λx,a. a;<k, v>;m)

Lemma: int-decr-map-add_wf
[Value:Type]. ∀[k:ℤ]. ∀[v:Value]. ∀[m:int-decr-map-type(Value)].  (int-decr-map-add(k;v;m) ∈ int-decr-map-type(Value))

Lemma: int-decr-map-add-prop
[Value:Type]. ∀[m:int-decr-map-type(Value)]. ∀[k1,k2:ℤ]. ∀[v:Value].
  (int-decr-map-find(k1;int-decr-map-add(k2;v;m))
  if (k1 =z k2) ∧b bint-decr-map-inDom(k2;m)) then inl else int-decr-map-find(k1;m) fi 
  ∈ (Value?))

Definition: int-decr-map-remove
int-decr-map-remove(k;m) ==  remove-combine(λp.(k fst(p));m)

Lemma: int-decr-map-remove_wf
[Value:Type]. ∀[k:ℤ]. ∀[m:int-decr-map-type(Value)].  (int-decr-map-remove(k;m) ∈ int-decr-map-type(Value))

Lemma: int-decr-map-remove-prop
[Value:Type]. ∀[m:int-decr-map-type(Value)]. ∀[k1,k2:ℤ].
  (int-decr-map-find(k1;int-decr-map-remove(k2;m))
  if (k1 =z k2) then inr ⋅  else int-decr-map-find(k1;m) fi 
  ∈ (Value?))

Definition: mk-map-int-decr
mk-map-int-decr(Value) ==
  mk-map(ℤ;Value;int-decr-map-type(Value);λx,y. (x =z y);λk,m. int-decr-map-find(k;m);λk,m. int-decr-map-inDom(k;m);
         int-decr-map-empty();λm.int-decr-map-isEmpty(m);λk,v,m. int-decr-map-update(k;v;m);λk,v,m. int-decr-map-add(k;v\000C;m);
         λk,m. int-decr-map-remove(k;m))

Lemma: mk-map-int-decr_wf
[Value:Type]. (mk-map-int-decr(Value) ∈ map-sig{i:l}(ℤ;Value))

Definition: lookup-list-map-type
lookup-list-map-type(Key;Value) ==  (Key × Value) List

Lemma: lookup-list-map-type_wf
[Key,Value:Type].  (lookup-list-map-type(Key;Value) ∈ Type)

Lemma: lookup-list-map-type-prop
[Key,Value:Type].
  (valueall-type(lookup-list-map-type(Key;Value))) supposing (valueall-type(Value) and valueall-type(Key))

Definition: lookup-list-map-eqKey
lookup-list-map-eqKey(keyDeq) ==  keyDeq

Lemma: lookup-list-map-eqKey_wf
[Key:Type]. ∀[keyDeq:EqDecider(Key)].  (lookup-list-map-eqKey(keyDeq) ∈ EqDecider(Key))

Definition: lookup-list-map-find
lookup-list-map-find(deqKey;key;m) ==  apply-alist(deqKey;m;key)

Lemma: lookup-list-map-find_wf
[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key:Key]. ∀[m:lookup-list-map-type(Key;Value)].
  (lookup-list-map-find(deqKey;key;m) ∈ Value?)

Definition: lookup-list-map-inDom
lookup-list-map-inDom(deqKey;key;m) ==  rec-case(m) of [] => ff h::t => r.let k,v in (deqKey key k) ∨br

Lemma: lookup-list-map-inDom_wf
[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key:Key]. ∀[m:lookup-list-map-type(Key;Value)].
  (lookup-list-map-inDom(deqKey;key;m) ∈ 𝔹)

Lemma: lookup-list-map-inDom-prop
[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key:Key]. ∀[m:lookup-list-map-type(Key;Value)].
  (↑lookup-list-map-inDom(deqKey;key;m) ⇐⇒ ↑isl(lookup-list-map-find(deqKey;key;m)))

Definition: lookup-list-map-empty
lookup-list-map-empty() ==  []

Lemma: lookup-list-map-empty_wf
[Key,Value:Type].  (lookup-list-map-empty() ∈ lookup-list-map-type(Key;Value))

Lemma: lookup-list-map-empty-prop
[Key:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key:Key].  (¬↑lookup-list-map-inDom(deqKey;key;lookup-list-map-empty()))

Definition: lookup-list-map-isEmpty
lookup-list-map-isEmpty(m) ==  null(m)

Lemma: lookup-list-map-isEmpty_wf
[Key,Value:Type]. ∀[m:lookup-list-map-type(Key;Value)].  (lookup-list-map-isEmpty(m) ∈ 𝔹)

Lemma: lookup-list-map-isEmpty-prop
[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[m:lookup-list-map-type(Key;Value)].
  (↑lookup-list-map-isEmpty(m) ⇐⇒ ∀k:Key. (¬↑lookup-list-map-inDom(deqKey;k;m)))

Definition: lookup-list-map-update
lookup-list-map-update(deqKey;key;val;m) ==  update-alist(deqKey;m;key;val;v.val)

Lemma: lookup-list-map-update_wf
[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key:Key]. ∀[val:Value]. ∀[m:lookup-list-map-type(Key;Value)].
  (lookup-list-map-update(deqKey;key;val;m) ∈ lookup-list-map-type(Key;Value))

Lemma: lookup-list-map-update-prop
[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key2:Key]. ∀[val:Value]. ∀[m:lookup-list-map-type(Key;Value)].
[key1:Key].
  (lookup-list-map-find(deqKey;key1;lookup-list-map-update(deqKey;key2;val;m))
  if deqKey key1 key2 then inl val else lookup-list-map-find(deqKey;key1;m) fi 
  ∈ (Value?))

Definition: lookup-list-map-add
lookup-list-map-add(deqKey;key;val;m) ==  update-alist(deqKey;m;key;val;v.v)

Lemma: lookup-list-map-add_wf
[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key:Key]. ∀[val:Value]. ∀[m:lookup-list-map-type(Key;Value)].
  (lookup-list-map-add(deqKey;key;val;m) ∈ lookup-list-map-type(Key;Value))

Lemma: lookup-list-map-add-prop
[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key2:Key]. ∀[val:Value]. ∀[m:lookup-list-map-type(Key;Value)].
[key1:Key].
  (lookup-list-map-find(deqKey;key1;lookup-list-map-add(deqKey;key2;val;m))
  if (deqKey key1 key2) ∧b blookup-list-map-inDom(deqKey;key2;m))
    then inl val
    else lookup-list-map-find(deqKey;key1;m)
    fi 
  ∈ (Value?))

Definition: lookup-list-map-remove
lookup-list-map-remove(deqKey;key;m) ==  remove-alist(deqKey;m;key)

Lemma: lookup-list-map-remove_wf
[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key:Key]. ∀[m:lookup-list-map-type(Key;Value)].
  (lookup-list-map-remove(deqKey;key;m) ∈ lookup-list-map-type(Key;Value))

Lemma: lookup-list-map-remove-prop
[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key2:Key]. ∀[m:lookup-list-map-type(Key;Value)]. ∀[key1:Key].
  (lookup-list-map-find(deqKey;key1;lookup-list-map-remove(deqKey;key2;m))
  if deqKey key1 key2 then inr ⋅  else lookup-list-map-find(deqKey;key1;m) fi 
  ∈ (Value?))

Definition: mk-lookup-list-map
mk-lookup-list-map(Key;Value;deqKey) ==
  mk-map(Key;Value;lookup-list-map-type(Key;Value);lookup-list-map-eqKey(deqKey);λk,m. lookup-list-map-find(deqKey;k;m);
         λk,m. lookup-list-map-inDom(deqKey;k;m);lookup-list-map-empty();λm.lookup-list-map-isEmpty(m);
         λk,v,m. lookup-list-map-update(deqKey;k;v;m);λk,v,m. lookup-list-map-add(deqKey;k;v;m);
         λk,m. lookup-list-map-remove(deqKey;k;m))

Lemma: mk-lookup-list-map_wf
[Key,Value:Type]. ∀[deqKey:EqDecider(Key)].  (mk-lookup-list-map(Key;Value;deqKey) ∈ map-sig{i:l}(Key;Value))



Home Index