---

Step * 2 2 2 of Lemma l_find_wf

.....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)
7. l_find(v;P) ∈ (∃x:T [(∃i:ℕ||v||. ((x = v[i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P v[j])))))]) ∨ (↓∀i:ℕ||v||. (¬↑(P v[i])))
8. l_find(v;P)
= l_find(v;P)
∈ ((∃x:T [(∃i:ℕ||v||. ((x = v[i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P v[j])))))]) ∨ (↓∀i:ℕ||v||. (¬↑(P v[i]))))
⊢ (∃x:T [(∃i:ℕ||v||. ((x = v[i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P v[j])))))]) ∨ (↓∀i:ℕ||v||. (¬↑(P v[i]))) ∈ Type
BY
{ (Auto'
   THEN Try (Complete (((MemTypeCD THEN Auto)
                        THEN (RW ListC 0 THEN Auto)
                        THEN (OrRight THEN Auto)
                        THEN (HypSubst' (-1) 0 THENA Auto)
                        THEN GenListD 0)))
   THEN (InstLemma `list-subtype` [⌜T⌝;⌜v⌝]⋅ THENA Auto)
   THEN DoSubsume
   THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
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.  \mneg{}\muparrow{}(P  u)
7.  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])))
8.  l\_find(v;P)  =  l\_find(v;P)
\mvdash{}  (\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])))
    \mmember{}  Type


By

---

Latex:
(Auto'
  THEN  Try  (Complete  (((MemTypeCD  THEN  Auto)
                                            THEN  (RW  ListC  0  THEN  Auto)
                                            THEN  (OrRight  THEN  Auto)
                                            THEN  (HypSubst'  (-1)  0  THENA  Auto)
                                            THEN  GenListD  0)))
  THEN  (InstLemma  `list-subtype`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  DoSubsume
  THEN  Auto)

---

Home Index