---

Step * 1 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) =z k))
⊢ <k, v> = m[index-of-first x in m.(fst(x) =z k) - 1] ∈ (ℤ × Value)
BY
{ (InstLemma `first_index_property` [⌜ℤ × Value⌝;⌜λ2x.(fst(x) =z k)⌝;⌜m⌝]⋅
   THEN Auto
   THEN Repeat (AllPushDown)
   THEN (Assert ⌜(m[index-of-first x in m.(fst(x) =z k) - 1] ∈ m)⌝⋅ THENA GenListD 0)
   THEN InstLemma `int-decr-map-fun` [⌜Value⌝;⌜m⌝;⌜k⌝;⌜v⌝;⌜snd(m[index-of-first x in m.(fst(x) =z k) - 1])⌝]⋅
   THEN Auto) }

1
.....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)

2
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)

---

Latex:

---

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


By

---

Latex:
(InstLemma  `first\_index\_property`  [\mkleeneopen{}\mBbbZ{}  \mtimes{}  Value\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.(fst(x)  =\msubz{}  k)\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Repeat  (AllPushDown)
  THEN  (Assert  \mkleeneopen{}(m[index-of-first  x  in  m.(fst(x)  =\msubz{}  k)  -  1]  \mmember{}  m)\mkleeneclose{}\mcdot{}  THENA  GenListD  0)
  THEN  InstLemma  `int-decr-map-fun`  [\mkleeneopen{}Value\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{};
  \mkleeneopen{}snd(m[index-of-first  x  in  m.(fst(x)  =\msubz{}  k)  -  1])\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index