---

Step * 1 of Lemma l_find_wf


1. T : Type
2. u : T
3. v : T List
4. ∀[P:{x:T| (x ∈ v)}  ⟶ 𝔹]
     (l_find(v;P) ∈ (∃x:T [(∃i:ℕ||v||. ((x = v[i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P v[j])))))])
      ∨ (↓∀i:ℕ||v||. (¬↑(P v[i]))))
5. P : {x:T| (x ∈ [u / v])}  ⟶ 𝔹
6. ↑(P u)
⊢ inl u ∈ (∃x:T [(∃i:ℕ||v|| + 1. ((x = [u / v][i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P [u / v][j])))))])
  ∨ (↓∀i:ℕ||v|| + 1. (¬↑(P [u / v][i])))
BY
{ ((Auto' THEN MemTypeCD THEN Auto')
   THEN Try (Complete ((MemTypeCD THEN Auto THEN UnfoldTopAb 0 THEN InstConcl [⌜i⌝]⋅ THEN Auto')))
   THEN InstConcl [⌜0⌝]⋅
   THEN Auto'
   THEN MemTypeCD
   THEN Auto
   THEN UnfoldTopAb 0
   THEN InstConcl [⌜i⌝]⋅
   THEN Auto')⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mforall{}[P:\{x:T|  (x  \mmember{}  v)\}    {}\mrightarrow{}  \mBbbB{}]
          (l\_find(v;P)  \mmember{}  (\mexists{}x:T  [(\mexists{}i:\mBbbN{}||v||.  ((x  =  v[i])  \mwedge{}  (\muparrow{}(P  x))  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}(P  v[j])))))])
            \mvee{}  (\mdownarrow{}\mforall{}i:\mBbbN{}||v||.  (\mneg{}\muparrow{}(P  v[i]))))
5.  P  :  \{x:T|  (x  \mmember{}  [u  /  v])\}    {}\mrightarrow{}  \mBbbB{}
6.  \muparrow{}(P  u)
\mvdash{}  inl  u  \mmember{}  (\mexists{}x:T  [(\mexists{}i:\mBbbN{}||v||  +  1.  ((x  =  [u  /  v][i])  \mwedge{}  (\muparrow{}(P  x))  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}(P  [u  /  v][j])))))])
    \mvee{}  (\mdownarrow{}\mforall{}i:\mBbbN{}||v||  +  1.  (\mneg{}\muparrow{}(P  [u  /  v][i])))


By

---

Latex:
((Auto'  THEN  MemTypeCD  THEN  Auto')
  THEN  Try  (Complete  ((MemTypeCD  THEN  Auto  THEN  UnfoldTopAb  0  THEN  InstConcl  [\mkleeneopen{}i\mkleeneclose{}]\mcdot{}  THEN  Auto')))
  THEN  InstConcl  [\mkleeneopen{}0\mkleeneclose{}]\mcdot{}
  THEN  Auto'
  THEN  MemTypeCD
  THEN  Auto
  THEN  UnfoldTopAb  0
  THEN  InstConcl  [\mkleeneopen{}i\mkleeneclose{}]\mcdot{}
  THEN  Auto')\mcdot{}

---

Home Index