---

Step * of Lemma mk-map-int-decr_wf

∀[Value:Type]. (mk-map-int-decr(Value) ∈ map-sig{i:l}(ℤ;Value))
BY
{ (RepUR ``mk-map-int-decr`` 0
   THEN Auto
   THEN Try (Complete ((BLemma `int-decr-map-find-wf` THEN Trivial)))
   THEN MemTypeCD
   THEN AllReduce
   THEN Auto
   THEN Try (Complete ((BLemma `int-decr-map-find-wf` THEN Auto)))
   THEN Try (Complete ((BLemma `int-decr-map-inDom-prop` THEN Auto)))
   THEN Try (Complete ((Using [`Value',⌈Value⌉] (BLemma `int-decr-map-empty-prop`)⋅ THEN Auto)))
   THEN Try (Complete ((BLemma `int-decr-map-isEmpty-prop` THEN Auto)))
   THEN Try (Complete ((BLemma `int-decr-map-update-prop` THEN Auto)))
   THEN Try (Complete ((BLemma `int-decr-map-add-prop` THEN Auto)))
   THEN Try (Complete ((BLemma `int-decr-map-remove-prop` THEN Auto)))
   THEN Try (Complete ((RW (SymbolicComputeC []) 0 THEN Auto)))
   THEN Try (Complete ((BLemma `int-decr-map-find-wf` THEN Auto)))) }

---

Latex:


\mforall{}[Value:Type].  (mk-map-int-decr(Value)  \mmember{}  map-sig\{i:l\}(\mBbbZ{};Value))


By

(RepUR  ``mk-map-int-decr``  0
  THEN  Auto
  THEN  Try  (Complete  ((BLemma  `int-decr-map-find-wf`  THEN  Trivial)))
  THEN  MemTypeCD
  THEN  AllReduce
  THEN  Auto
  THEN  Try  (Complete  ((BLemma  `int-decr-map-find-wf`  THEN  Auto)))
  THEN  Try  (Complete  ((BLemma  `int-decr-map-inDom-prop`  THEN  Auto)))
  THEN  Try  (Complete  ((Using  [`Value',\mkleeneopen{}Value\mkleeneclose{}]  (BLemma  `int-decr-map-empty-prop`)\mcdot{}  THEN  Auto)))
  THEN  Try  (Complete  ((BLemma  `int-decr-map-isEmpty-prop`  THEN  Auto)))
  THEN  Try  (Complete  ((BLemma  `int-decr-map-update-prop`  THEN  Auto)))
  THEN  Try  (Complete  ((BLemma  `int-decr-map-add-prop`  THEN  Auto)))
  THEN  Try  (Complete  ((BLemma  `int-decr-map-remove-prop`  THEN  Auto)))
  THEN  Try  (Complete  ((RW  (SymbolicComputeC  [])  0  THEN  Auto)))
  THEN  Try  (Complete  ((BLemma  `int-decr-map-find-wf`  THEN  Auto))))

---

Home Index