---

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

.....antecedent..... 
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)
⊢ (<k, snd(m[index-of-first x in m.(fst(x) =z k) - 1])> ∈ m)
BY
{ ((RW (AddrC [1;1] (RevHypC (-3))) 0 THENA Auto) THEN RWO "pair-eta<" 0 THEN Auto) }

---

Latex:


.....antecedent..... 
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)
\mvdash{}  (<k,  snd(m[index-of-first  x  in  m.(fst(x)  =\msubz{}  k)  -  1])>  \mmember{}  m)


By

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

---

Home Index