---

Step * 1 1 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 : 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
⊢ outl(list-index(eq;L;f x)) = outl(list-index(eq;L;f y)) ∈ ℕ||L||
BY
{ TACTIC:(MoveToConcl (-4)
          THEN GenConclTerms Auto [⌜outl(list-index(eq;L;f x))⌝;⌜outl(list-index(eq;L;f y))⌝]⋅
          THEN Try ((BLemma `isl-list-index` THEN Auto))
          THEN All Thin
          THEN Auto') }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  A  :  Type
5.  f  :  A  {}\mrightarrow{}  T
6.  x  :  A
7.  (f  x  \mmember{}  L)
8.  y  :  A
9.  (f  y  \mmember{}  L)
10.  (outl(list-index(eq;L;f  x))  -  outl(list-index(eq;L;f  y)))  =  0
11.  \mforall{}[x:T].  \mforall{}[L:T  List].    L[outl(list-index(eq;L;x))]  =  x  supposing  (x  \mmember{}  L)
12.  L[outl(list-index(eq;L;f  x))]  =  (f  x)
13.  L[outl(list-index(eq;L;f  y))]  =  (f  y)
\mvdash{}  outl(list-index(eq;L;f  x))  =  outl(list-index(eq;L;f  y))


By

---

Latex:
TACTIC:(MoveToConcl  (-4)
                THEN  GenConclTerms  Auto  [\mkleeneopen{}outl(list-index(eq;L;f  x))\mkleeneclose{};\mkleeneopen{}outl(list-index(eq;L;f  y))\mkleeneclose{}]\mcdot{}
                THEN  Try  ((BLemma  `isl-list-index`  THEN  Auto))
                THEN  All  Thin
                THEN  Auto')

---

Home Index