---

Step * 2 of Lemma int-decr-map-fun


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
BY
{ (InstLemma `l-ordered-inst` [⌈ℤ × Value⌉;⌈m⌉;⌈λ2x.λ2y.(fst(x)) > (fst(y))⌉;⌈i⌉;⌈i1⌉]⋅
   THEN Auto
   THEN AllReduce
   THEN Auto
   THEN (RevHypSubst (-7) (-1) THENA Auto)
   THEN (RevHypSubst (-4) (-1) THENA Auto)
   THEN Reduce (-1)
   THEN Auto) }

---

Latex:



1.  Value  :  Type
2.  m  :  (\mBbbZ{}  \mtimes{}  Value)  List
3.  l-ordered(\mBbbZ{}  \mtimes{}  Value;x,y.(fst(x))  >  (fst(y));m)
4.  k  :  \mBbbZ{}
5.  v1  :  Value
6.  v2  :  Value
7.  i1  :  \mBbbN{}
8.  i1  <  ||m||
9.  <k,  v2>  =  m[i1]
10.  i  :  \mBbbN{}
11.  i  <  ||m||
12.  <k,  v1>  =  m[i]
13.  \mneg{}(i  =  i1)
14.  \mneg{}i  <  i1
\mvdash{}  v1  =  v2


By

(InstLemma  `l-ordered-inst`  [\mkleeneopen{}\mBbbZ{}  \mtimes{}  Value\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.\mlambda{}\msubtwo{}y.(fst(x))  >  (fst(y))\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}i1\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  AllReduce
  THEN  Auto
  THEN  (RevHypSubst  (-7)  (-1)  THENA  Auto)
  THEN  (RevHypSubst  (-4)  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  Auto)

---

Home Index