---

Step * of Lemma isl-apply-alist

∀[A,T:Type].
  ∀eq:EqDecider(T). ∀x:T. ∀L:(T × A) List.
    ((↑isl(apply-alist(eq;L;x)) ⇐⇒ (x ∈ map(λp.(fst(p));L)))
    ∧ (<x, outl(apply-alist(eq;L;x))> ∈ L) supposing ↑isl(apply-alist(eq;L;x)))
BY
{ ((D 0 THENA Auto)
   THEN InstLemma `apply-alist-cases` []
   THEN RepeatFor 4 (ParallelLast')
   THEN (Assert ∀a,b:T.  Dec(a = b ∈ T) BY
               ((InstLemma `deq_property` [⌜T⌝;⌜eq⌝]⋅ THENA Auto) THEN RWO "-1" 0 THEN Auto))
   THEN (Decide (x ∈ map(λp.(fst(p));L)) THENA Auto)
   THEN ExRepD
   THEN ThinTrivial
   THEN Try ((RWO "-1" 0 THEN RepUR ``bfalse`` 0 THEN Auto))) }

1
1. [A] : Type
2. [T] : Type
3. eq : EqDecider(T)
4. x : T
5. L : (T × A) List
6. apply-alist(eq;L;x) ~ ff supposing ¬(x ∈ map(λp.(fst(p));L))
7. ∀[i:ℕ||L||]
     (apply-alist(eq;L;x) ~ inl (snd(L[i]))) supposing (((fst(L[i])) = x ∈ T) and (∀j:ℕi. (¬((fst(L[j])) = x ∈ T))))
8. ∀a,b:T.  Dec(a = b ∈ T)
9. (x ∈ map(λp.(fst(p));L))
⊢ (↑isl(apply-alist(eq;L;x)) ⇐⇒ (x ∈ map(λp.(fst(p));L)))
∧ (<x, outl(apply-alist(eq;L;x))> ∈ L) supposing ↑isl(apply-alist(eq;L;x))

---

Latex:

---

Latex:
\mforall{}[A,T:Type].
    \mforall{}eq:EqDecider(T).  \mforall{}x:T.  \mforall{}L:(T  \mtimes{}  A)  List.
        ((\muparrow{}isl(apply-alist(eq;L;x))  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  map(\mlambda{}p.(fst(p));L)))
        \mwedge{}  (<x,  outl(apply-alist(eq;L;x))>  \mmember{}  L)  supposing  \muparrow{}isl(apply-alist(eq;L;x)))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  InstLemma  `apply-alist-cases`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  (Assert  \mforall{}a,b:T.    Dec(a  =  b)  BY
                          ((InstLemma  `deq\_property`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  RWO  "-1"  0  THEN  Auto))
  THEN  (Decide  (x  \mmember{}  map(\mlambda{}p.(fst(p));L))  THENA  Auto)
  THEN  ExRepD
  THEN  ThinTrivial
  THEN  Try  ((RWO  "-1"  0  THEN  RepUR  ``bfalse``  0  THEN  Auto)))

---

Home Index