---

Step * 1 of Lemma list-index-cmp-zero


1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. A : Type
5. f : A ⟶ T
6. x : {x:A| (f x ∈ L)} 
7. y : {x:A| (f x ∈ L)} 
8. (list-index-cmp(eq;L;f) x y) = 0 ∈ ℤ
⊢ (f x) = (f y) ∈ T
BY
{ TACTIC:(DSetVars
          THEN RepUR ``list-index-cmp int-minus-comparison`` -1
          THEN (InstLemma `list-index-property` [⌜T⌝;⌜eq⌝]⋅ THENA Auto)
          THEN (InstHyp [⌜f x⌝;⌜L⌝] (-1)⋅ THENA Auto)
          THEN (InstHyp [⌜f y⌝;⌜L⌝] (-2)⋅ THENA Auto)) }

1
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. A : Type
5. f : A ⟶ T
6. x : A
7. (f x ∈ L)
8. y : A
9. (f y ∈ L)
10. (outl(list-index(eq;L;f x)) - outl(list-index(eq;L;f y))) = 0 ∈ ℤ
11. ∀[x:T]. ∀[L:T List].  L[outl(list-index(eq;L;x))] = x ∈ T supposing (x ∈ L)
12. L[outl(list-index(eq;L;f x))] = (f x) ∈ T
13. L[outl(list-index(eq;L;f y))] = (f y) ∈ T
⊢ (f x) = (f y) ∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  A  :  Type
5.  f  :  A  {}\mrightarrow{}  T
6.  x  :  \{x:A|  (f  x  \mmember{}  L)\} 
7.  y  :  \{x:A|  (f  x  \mmember{}  L)\} 
8.  (list-index-cmp(eq;L;f)  x  y)  =  0
\mvdash{}  (f  x)  =  (f  y)


By

---

Latex:
TACTIC:(DSetVars
                THEN  RepUR  ``list-index-cmp  int-minus-comparison``  -1
                THEN  (InstLemma  `list-index-property`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  (InstHyp  [\mkleeneopen{}f  x\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
                THEN  (InstHyp  [\mkleeneopen{}f  y\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto))

---

Home Index