---

Step * of 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 k m) ⇐⇒ ↑isl(find k m))} ].
∀[empty:{m:map| ∀k:Key. (¬↑(inDom k m))} ]. ∀[isEmpty:{f:map ─→ 𝔹| ∀m:map. (↑(f m) ⇐⇒ ∀k:Key. (¬↑(inDom k m)))} ].
∀[update:{f:Key ─→ Value ─→ map ─→ map| 
          ∀m:map. ∀k1,k2:Key. ∀v:Value.
            ((find k1 (f k2 v m)) = if eqKey k1 k2 then inl v else find k1 m fi  ∈ (Value?))} ].
∀[add:{f:Key ─→ Value ─→ map ─→ map| 
       ∀m:map. ∀k1,k2:Key. ∀v:Value.
         ((find k1 (f k2 v m)) = if (eqKey k1 k2) ∧b (¬b(inDom k2 m)) then inl v else find k1 m 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 m fi  ∈ (Value?))} ].
  (mk-map(Key;Value;map;eqKey;find;inDom;empty;isEmpty;update;add;remove) ∈ map-sig{i:l}(Key;Value))
BY
{ (Auto
   THEN RepUR ``mk-map map-sig`` 0
   THEN Repeat ((RecordPlusTypeCD' THEN Reduce 0 THEN Try (Trivial)))
   THEN RepUR ``record record-update`` 0
   THEN Auto) }

---

Latex:


\mforall{}[Key,Value:Type].  \mforall{}[map:\{m:Type| 
                                                    (valueall-type(m))  supposing  (valueall-type(Value)  and  valueall-type(Key))\000C\}  ].
\mforall{}[eqKey:EqDecider(Key)].  \mforall{}[find:Key  {}\mrightarrow{}  map  {}\mrightarrow{}  (Value?)].  \mforall{}[inDom:\{f:Key  {}\mrightarrow{}  map  {}\mrightarrow{}  \mBbbB{}| 
                                                                                                                                    \mforall{}k:Key.  \mforall{}m:map.
                                                                                                                                        (\muparrow{}(f  k  m)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}isl(find  k  m))\}  ]\000C.
\mforall{}[empty:\{m:map|  \mforall{}k:Key.  (\mneg{}\muparrow{}(inDom  k  m))\}  ].  \mforall{}[isEmpty:\{f:map  {}\mrightarrow{}  \mBbbB{}| 
                                                                                                            \mforall{}m:map
                                                                                                                (\muparrow{}(f  m)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}k:Key.  (\mneg{}\muparrow{}(inDom  k  m)))\}  ].
\mforall{}[update:\{f:Key  {}\mrightarrow{}  Value  {}\mrightarrow{}  map  {}\mrightarrow{}  map| 
                    \mforall{}m:map.  \mforall{}k1,k2:Key.  \mforall{}v:Value.
                        ((find  k1  (f  k2  v  m))  =  if  eqKey  k1  k2  then  inl  v  else  find  k1  m  fi  )\}  ].
\mforall{}[add:\{f:Key  {}\mrightarrow{}  Value  {}\mrightarrow{}  map  {}\mrightarrow{}  map| 
              \mforall{}m:map.  \mforall{}k1,k2:Key.  \mforall{}v:Value.
                  ((find  k1  (f  k2  v  m))
                  =  if  (eqKey  k1  k2)  \mwedge{}\msubb{}  (\mneg{}\msubb{}(inDom  k2  m))  then  inl  v  else  find  k1  m  fi  )\}  ].
\mforall{}[remove:\{f:Key  {}\mrightarrow{}  map  {}\mrightarrow{}  map| 
                    \mforall{}m:map.  \mforall{}k1,k2:Key.
                        ((find  k1  (f  k2  m))  =  if  eqKey  k1  k2  then  inr  \mcdot{}    else  find  k1  m  fi  )\}  ].
    (mk-map(Key;Value;map;eqKey;find;inDom;empty;isEmpty;update;add;remove)  \mmember{}  map-sig\{i:l\}(Key;Value))


By

(Auto
  THEN  RepUR  ``mk-map  map-sig``  0
  THEN  Repeat  ((RecordPlusTypeCD'  THEN  Reduce  0  THEN  Try  (Trivial)))
  THEN  RepUR  ``record  record-update``  0
  THEN  Auto)

---

Home Index