---

Step * 2 of Lemma isl-list-index


1. [T] : Type
2. eq : EqDecider(T)
3. x : T
4. u : T
5. v : T List
6. ↑isl(list-index(eq;v;x)) ⇐⇒ (x ∈ v)
⊢ ↑isl(case list-index(eq;v;x)
   of inl(n) =>
   inl (n + 1)
   | inr(a) =>
   if eqof(eq) u x then inl 0 else list-index(eq;v;x) fi )
⇐⇒ (x ∈ [u / v])
BY
{ (MoveToConcl (-1) THEN GenConclAtAddr [1;1;1;1] THEN D -2 THEN Reduce 0) }

1
1. [T] : Type
2. eq : EqDecider(T)
3. x : T
4. u : T
5. v : T List
6. x1 : ℕ||v||
7. list-index(eq;v;x) = (inl x1) ∈ (ℕ||v|| + Top)
⊢ (True ⇐⇒ (x ∈ v)) ⇒ (True ⇐⇒ (x ∈ [u / v]))

2
1. [T] : Type
2. eq : EqDecider(T)
3. x : T
4. u : T
5. v : T List
6. y : Top
7. list-index(eq;v;x) = (inr y ) ∈ (ℕ||v|| + Top)
⊢ (False ⇐⇒ (x ∈ v)) ⇒ (↑isl(if eqof(eq) u x then inl 0 else inr y  fi ) ⇐⇒ (x ∈ [u / v]))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  T
4.  u  :  T
5.  v  :  T  List
6.  \muparrow{}isl(list-index(eq;v;x))  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  v)
\mvdash{}  \muparrow{}isl(case  list-index(eq;v;x)
      of  inl(n)  =>
      inl  (n  +  1)
      |  inr(a)  =>
      if  eqof(eq)  u  x  then  inl  0  else  list-index(eq;v;x)  fi  )
\mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  [u  /  v])


By

---

Latex:
(MoveToConcl  (-1)  THEN  GenConclAtAddr  [1;1;1;1]  THEN  D  -2  THEN  Reduce  0)

---

Home Index