---

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


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)) = k ∈ ℤ)
10. (fst(m[index-of-first x in m.(fst(x) =z k) - 1])) = k ∈ ℤ
11. ¬(∃x∈firstn(index-of-first x in m.(fst(x) =z k) - 1;m). (fst(x)) = k ∈ ℤ)
12. (m[index-of-first x in m.(fst(x) =z k) - 1] ∈ m)
13. v = (snd(m[index-of-first x in m.(fst(x) =z k) - 1])) ∈ Value
⊢ <k, v> = m[index-of-first x in m.(fst(x) =z k) - 1] ∈ (ℤ × Value)
BY
{ ((RW (AddrC [2;1] (RevHypC (-4))) 0 THENA Auto) THEN (HypSubst (-1) 0 THENA Auto) THEN RWO "pair-eta<" 0 THEN Auto) }

---

Latex:



1.  Value  :  Type
2.  k  :  \mBbbZ{}@i
3.  v  :  Value@i
4.  m  :  int-decr-map-type(Value)@i
5.  (<k,  v>  \mmember{}  m)@i
6.  index-of-first  x  in  m.(fst(x)  =\msubz{}  k)  -  1  <  ||m||
7.  index-of-first  x  in  m.(fst(x)  =\msubz{}  k)  \mmember{}  \mBbbN{}||m||  +  1
8.  0  <  index-of-first  x  in  m.(fst(x)  =\msubz{}  k)
9.  (\mexists{}x\mmember{}m.  (fst(x))  =  k)
10.  (fst(m[index-of-first  x  in  m.(fst(x)  =\msubz{}  k)  -  1]))  =  k
11.  \mneg{}(\mexists{}x\mmember{}firstn(index-of-first  x  in  m.(fst(x)  =\msubz{}  k)  -  1;m).  (fst(x))  =  k)
12.  (m[index-of-first  x  in  m.(fst(x)  =\msubz{}  k)  -  1]  \mmember{}  m)
13.  v  =  (snd(m[index-of-first  x  in  m.(fst(x)  =\msubz{}  k)  -  1]))
\mvdash{}  <k,  v>  =  m[index-of-first  x  in  m.(fst(x)  =\msubz{}  k)  -  1]


By

((RW  (AddrC  [2;1]  (RevHypC  (-4)))  0  THENA  Auto)
  THEN  (HypSubst  (-1)  0  THENA  Auto)
  THEN  RWO  "pair-eta<"  0
  THEN  Auto)

---

Home Index