---

Step * 2 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)
⊢ 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])))
BY
{ (Fold `l_find` 0 THEN (InstHyp [⌜P⌝] (-3)⋅ THENA Auto) THEN DoSubsume) }

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)
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])))
⊢ l_find(v;P) ∈ (∃x:T [(∃i:ℕ||v||. ((x = v[i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P v[j])))))]) ∨ (↓∀i:ℕ||v||. (¬↑(P 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)
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])))) ⊆r ((∃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:

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)
\mvdash{}  reduce(\mlambda{}h,r.  if  P  h  then  inl  h  else  r  fi  ;inr  \mcdot{}  ;v)  \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:
(Fold  `l\_find`  0  THEN  (InstHyp  [\mkleeneopen{}P\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)  THEN  DoSubsume)

---

Home Index