---

Step * of Lemma l_find_wf

∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)}  ⟶ 𝔹].
  (l_find(L;P) ∈ (∃x:T [(∃i:ℕ||L||. ((x = L[i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P L[j])))))]) ∨ (↓∀i:ℕ||L||. (¬↑(P L[i]))))
BY
{ (InductionOnList
   THEN Reduce 0
   THEN (UnivCD THENA Auto)
   THEN UnfoldAtAddr [2] 0
   THEN Reduce 0
   THEN Try (Complete ((RepUR ``or it`` 0 THEN Auto)))
   THEN AutoSplit) }

1
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])))

2
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)
⊢ reduce(λh,r. if P h then inl h else r fi ;inr ⋅ ;v) ∈ (∃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])))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[P:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbB{}].
    (l\_find(L;P)  \mmember{}  (\mexists{}x:T  [(\mexists{}i:\mBbbN{}||L||.  ((x  =  L[i])  \mwedge{}  (\muparrow{}(P  x))  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}(P  L[j])))))])
      \mvee{}  (\mdownarrow{}\mforall{}i:\mBbbN{}||L||.  (\mneg{}\muparrow{}(P  L[i]))))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  (UnivCD  THENA  Auto)
  THEN  UnfoldAtAddr  [2]  0
  THEN  Reduce  0
  THEN  Try  (Complete  ((RepUR  ``or  it``  0  THEN  Auto)))
  THEN  AutoSplit)

---

Home Index