---

Step * of 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))))))
BY
{ ((UnivCD THENA (Auto THEN DVar `v' THEN (MemTypeCD THEN Auto) THEN RW ListC 0 THEN Auto))
   THEN (Assert ⌜[u / v] ∈ int-decr-map-type(Value)⌝⋅
         THENA (DVar `v' THEN (MemTypeCD THEN Auto) THEN RW ListC 0 THEN Auto)
         )
   THEN (InstLemma `int-decr-map-inDom-prop1` [⌜Value⌝;⌜k⌝;⌜[u / v]⌝]⋅ THENA Auto)
   THEN (Using [`Value',⌜Value⌝] (FLemma `int-decr-map-inDom-prop` [-3])⋅ THENA Auto)
   THEN RepD
   THEN MoveToConcl (-2)
   THEN MoveToConcl (-1)
   THEN (GenConclAtAddr [1;1;1] THENA (Auto THEN Using [`T',⌜ℤ × Value⌝] (BLemma `l_all_wf`)⋅ THEN Auto))
   THEN DVar `v1'
   THEN Reduce 0
   THEN RepeatFor 2 ((D 0 THEN Try (Complete (Auto))))
   THEN (RW ListC (-1) THENA Auto)
   THEN D (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Value:Type].  \mforall{}[k:\mBbbZ{}].  \mforall{}[u:\mBbbZ{}  \mtimes{}  Value].  \mforall{}[v:int-decr-map-type(Value)].
    (k  \mleq{}  (fst(u)))  supposing 
          ((\muparrow{}int-decr-map-inDom(k;[u  /  v]))  and 
          (\mforall{}y:\mBbbZ{}  \mtimes{}  Value.  ((y  \mmember{}  v)  {}\mRightarrow{}  ((fst(u))  >  (fst(y))))))


By

---

Latex:
((UnivCD  THENA  (Auto  THEN  DVar  `v'  THEN  (MemTypeCD  THEN  Auto)  THEN  RW  ListC  0  THEN  Auto))
  THEN  (Assert  \mkleeneopen{}[u  /  v]  \mmember{}  int-decr-map-type(Value)\mkleeneclose{}\mcdot{}
              THENA  (DVar  `v'  THEN  (MemTypeCD  THEN  Auto)  THEN  RW  ListC  0  THEN  Auto)
              )
  THEN  (InstLemma  `int-decr-map-inDom-prop1`  [\mkleeneopen{}Value\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}[u  /  v]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Using  [`Value',\mkleeneopen{}Value\mkleeneclose{}]  (FLemma  `int-decr-map-inDom-prop`  [-3])\mcdot{}  THENA  Auto)
  THEN  RepD
  THEN  MoveToConcl  (-2)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclAtAddr  [1;1;1]
              THENA  (Auto  THEN  Using  [`T',\mkleeneopen{}\mBbbZ{}  \mtimes{}  Value\mkleeneclose{}]  (BLemma  `l\_all\_wf`)\mcdot{}  THEN  Auto)
              )
  THEN  DVar  `v1'
  THEN  Reduce  0
  THEN  RepeatFor  2  ((D  0  THEN  Try  (Complete  (Auto))))
  THEN  (RW  ListC  (-1)  THENA  Auto)
  THEN  D  (-1)
  THEN  Auto)

---

Home Index