---

Step * 2 2 1 1 of Lemma l_find_wf

.....subterm..... T:t
1:n
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]))))
9. x1 : T
10. i : ℕ||v||
11. x1 = v[i] ∈ T
12. ↑(P x1)
13. ∀j:ℕi. (¬↑(P v[j]))
⊢ x1 ∈ ∃x:T [(∃i:ℕ||v|| + 1. ((x = [u / v][i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P [u / v][j])))))]
BY
{ ((MemTypeCD THEN Auto')
   THEN Try (Complete (((Auto' THEN MemTypeCD THEN Auto) THEN UnfoldTopAb 0 THEN InstConcl [⌜i1⌝]⋅ THEN Auto')))
   THEN (InstConcl [⌜i + 1⌝]⋅ THEN Auto')
   THEN Try (Complete ((RW ListC 0 THEN Auto THEN AutoSplit)))
   THEN (Auto' THEN MemTypeCD THEN Auto)
   THEN UnfoldTopAb 0
   THEN InstConcl [⌜i1⌝]⋅
   THEN Auto') }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
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)
9.  x1  :  T
10.  i  :  \mBbbN{}||v||
11.  x1  =  v[i]
12.  \muparrow{}(P  x1)
13.  \mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}(P  v[j]))
\mvdash{}  x1  \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])))))]


By

---

Latex:
((MemTypeCD  THEN  Auto')
  THEN  Try  (Complete  (((Auto'  THEN  MemTypeCD  THEN  Auto)
                                            THEN  UnfoldTopAb  0
                                            THEN  InstConcl  [\mkleeneopen{}i1\mkleeneclose{}]\mcdot{}
                                            THEN  Auto')))
  THEN  (InstConcl  [\mkleeneopen{}i  +  1\mkleeneclose{}]\mcdot{}  THEN  Auto')
  THEN  Try  (Complete  ((RW  ListC  0  THEN  Auto  THEN  AutoSplit)))
  THEN  (Auto'  THEN  MemTypeCD  THEN  Auto)
  THEN  UnfoldTopAb  0
  THEN  InstConcl  [\mkleeneopen{}i1\mkleeneclose{}]\mcdot{}
  THEN  Auto')

---

Home Index