---

Step * of Lemma int-decr-map-type-member-sq-stable

∀[Value:Type]. ∀k:ℤ. ∀v:Value. ∀m:int-decr-map-type(Value).  SqStable((<k, v> ∈ m))
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN Unfold `l_member` 0
   THEN InstConcl [⌈index-of-first x in m.(fst(x) =z k) - 1⌉]⋅
   THEN Auto
   THEN InstLemma `first_index_bounds` [⌈ℤ × Value⌉;⌈λ2x.(fst(x) =z k)⌉;⌈m⌉]⋅
   THEN Auto
   THEN InstLemma `first_index-positive` [⌈ℤ × Value⌉;⌈λ2x.(fst(x) =z k)⌉;⌈m⌉]⋅
   THEN Auto
   THEN Try ((Unhide THENA Auto))
   THEN (D (-1) THENA (UnfoldTopAb 0 THEN (All(Unfold `l_member`) THEN ExRepD) THEN InstConcl [⌈i⌉]⋅ THEN Auto))
   THEN Auto) }

1
1. Value : Type
2. k : ℤ@i
3. v : Value@i
4. m : int-decr-map-type(Value)@i
5. (<k, v> ∈ m)@i
6. index-of-first x in m.(fst(x) =z k) - 1 < ||m||
7. index-of-first x in m.(fst(x) =z k) ∈ ℕ||m|| + 1
8. 0 < index-of-first x in m.(fst(x) =z k)
9. (∃x∈m. ↑(fst(x) =z k))
⊢ <k, v> = m[index-of-first x in m.(fst(x) =z k) - 1] ∈ (ℤ × Value)

---

Latex:


\mforall{}[Value:Type].  \mforall{}k:\mBbbZ{}.  \mforall{}v:Value.  \mforall{}m:int-decr-map-type(Value).    SqStable((<k,  v>  \mmember{}  m))


By

(Auto
  THEN  (D  0  THENA  Auto)
  THEN  Unfold  `l\_member`  0
  THEN  InstConcl  [\mkleeneopen{}index-of-first  x  in  m.(fst(x)  =\msubz{}  k)  -  1\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  InstLemma  `first\_index\_bounds`  [\mkleeneopen{}\mBbbZ{}  \mtimes{}  Value\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.(fst(x)  =\msubz{}  k)\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  InstLemma  `first\_index-positive`  [\mkleeneopen{}\mBbbZ{}  \mtimes{}  Value\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.(fst(x)  =\msubz{}  k)\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  ((Unhide  THENA  Auto))
  THEN  (D  (-1)
              THENA  (UnfoldTopAb  0
                            THEN  (All(Unfold  `l\_member`)  THEN  ExRepD)
                            THEN  InstConcl  [\mkleeneopen{}i\mkleeneclose{}]\mcdot{}
                            THEN  Auto)
              )
  THEN  Auto)

---

Home Index