---

Step * of Lemma int-decr-map-fun

∀[Value:Type]. ∀[m:int-decr-map-type(Value)]. ∀[k:ℤ]. ∀[v1,v2:Value].
  (v1 = v2 ∈ Value) supposing ((<k, v1> ∈ m) and (<k, v2> ∈ m))
BY
{ (Auto
   THEN All(RepUR ``int-decr-map-type l_member``)
   THEN ExRepD
   THEN DVarSets
   THEN Decide ⌈i = i1 ∈ ℤ⌉⋅
   THEN Auto
   THEN (Decide ⌈i < i1⌉⋅ THENA Auto)) }

1
1. Value : Type
2. m : (ℤ × Value) List
3. l-ordered(ℤ × Value;x,y.(fst(x)) > (fst(y));m)
4. k : ℤ
5. v1 : Value
6. v2 : Value
7. i1 : ℕ
8. i1 < ||m||
9. <k, v2> = m[i1] ∈ (ℤ × Value)
10. i : ℕ
11. i < ||m||
12. <k, v1> = m[i] ∈ (ℤ × Value)
13. ¬(i = i1 ∈ ℤ)
14. i < i1
⊢ v1 = v2 ∈ Value

2
1. Value : Type
2. m : (ℤ × Value) List
3. l-ordered(ℤ × Value;x,y.(fst(x)) > (fst(y));m)
4. k : ℤ
5. v1 : Value
6. v2 : Value
7. i1 : ℕ
8. i1 < ||m||
9. <k, v2> = m[i1] ∈ (ℤ × Value)
10. i : ℕ
11. i < ||m||
12. <k, v1> = m[i] ∈ (ℤ × Value)
13. ¬(i = i1 ∈ ℤ)
14. ¬i < i1
⊢ v1 = v2 ∈ Value

---

Latex:


\mforall{}[Value:Type].  \mforall{}[m:int-decr-map-type(Value)].  \mforall{}[k:\mBbbZ{}].  \mforall{}[v1,v2:Value].
    (v1  =  v2)  supposing  ((<k,  v1>  \mmember{}  m)  and  (<k,  v2>  \mmember{}  m))


By

(Auto
  THEN  All(RepUR  ``int-decr-map-type  l\_member``)
  THEN  ExRepD
  THEN  DVarSets
  THEN  Decide  \mkleeneopen{}i  =  i1\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (Decide  \mkleeneopen{}i  <  i1\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index