---

Step * of Lemma alist-domain-first

∀[A:Type]
  ∀d:A List. ∀f1:a:{a:A| (a ∈ d)}  ─→ Top. ∀x:A. ∀eq:EqDecider(A).
    ((x ∈ d)
    ⇒ (∃i:ℕ||d||. ((∀j:ℕi. (¬((fst(map(λx.<x, f1 x>;d)[j])) = x ∈ A))) ∧ ((fst(map(λx.<x, f1 x>;d)[i])) = x ∈ A))))
BY
{ (Auto
   THEN (InstLemma `l_member-first` [⌈A⌉;⌈d⌉;⌈x⌉;⌈eq⌉]⋅ THENA Auto)
   THEN D -1
   THEN InstConcl [⌈i⌉]⋅
   THEN Try (Complete (Auto))) }

1
1. [A] : Type
2. d : A List@i
3. f1 : a:{a:A| (a ∈ d)}  ─→ Top@i
4. x : A@i
5. eq : EqDecider(A)@i
6. (x ∈ d)@i
7. i : ℕ||d||
8. (∀j:ℕi. (¬(d[j] = x ∈ A))) ∧ (d[i] = x ∈ A)
⊢ (∀j:ℕi. (¬((fst(map(λx.<x, f1 x>;d)[j])) = x ∈ A))) ∧ ((fst(map(λx.<x, f1 x>;d)[i])) = x ∈ A)

---

Latex:


\mforall{}[A:Type]
    \mforall{}d:A  List.  \mforall{}f1:a:\{a:A|  (a  \mmember{}  d)\}    {}\mrightarrow{}  Top.  \mforall{}x:A.  \mforall{}eq:EqDecider(A).
        ((x  \mmember{}  d)
        {}\mRightarrow{}  (\mexists{}i:\mBbbN{}||d||
                  ((\mforall{}j:\mBbbN{}i.  (\mneg{}((fst(map(\mlambda{}x.<x,  f1  x>d)[j]))  =  x)))  \mwedge{}  ((fst(map(\mlambda{}x.<x,  f1  x>d)[i]))  =  x))))


By

(Auto
  THEN  (InstLemma  `l\_member-first`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  InstConcl  [\mkleeneopen{}i\mkleeneclose{}]\mcdot{}
  THEN  Try  (Complete  (Auto)))

---

Home Index