---

Step * 2 2 of Lemma bl-exists-first


1. [A] : Type
2. P : A ⟶ 𝔹
3. u : A
4. v : A List
5. (∃x∈v. ↑P[x]) ⇒ (∃i:ℕ||v||. ((↑P[v[i]]) ∧ (∀j:ℕi. (¬↑P[v[j]]))))
6. (∃x∈v. ↑P[x]) ⇐ ∃i:ℕ||v||. ((↑P[v[i]]) ∧ (∀j:ℕi. (¬↑P[v[j]])))
7. ∃i:ℕ||v|| + 1. ((↑P[[u / v][i]]) ∧ (∀j:ℕi. (¬↑P[[u / v][j]])))
⊢ (∃x∈[u / v]. ↑P[x])
BY
{ (ExRepD
   THEN (RW ListC 0 THENA Auto)
   THEN (Decide ↑P[u] THEN Auto)
   THEN BackThruSomeHyp
   THEN (Decide ⌜i = 0 ∈ ℤ⌝⋅ THENA Auto)
   THEN Try (Complete ((RWO "-1" (-4)⋅ THEN AllReduce THEN Auto)))
   THEN (RWO "select-cons-tl" (-4) THEN Auto)
   THEN (InstConcl [⌜i - 1⌝]⋅ THEN Auto)
   THEN (InstHyp [⌜j + 1⌝] (-5)⋅ THENA Auto)
   THEN RWO "select-cons-tl" (-1)
   THEN AllReduce
   THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  P  :  A  {}\mrightarrow{}  \mBbbB{}
3.  u  :  A
4.  v  :  A  List
5.  (\mexists{}x\mmember{}v.  \muparrow{}P[x])  {}\mRightarrow{}  (\mexists{}i:\mBbbN{}||v||.  ((\muparrow{}P[v[i]])  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}P[v[j]]))))
6.  (\mexists{}x\mmember{}v.  \muparrow{}P[x])  \mLeftarrow{}{}  \mexists{}i:\mBbbN{}||v||.  ((\muparrow{}P[v[i]])  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}P[v[j]])))
7.  \mexists{}i:\mBbbN{}||v||  +  1.  ((\muparrow{}P[[u  /  v][i]])  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}P[[u  /  v][j]])))
\mvdash{}  (\mexists{}x\mmember{}[u  /  v].  \muparrow{}P[x])


By

---

Latex:
(ExRepD
  THEN  (RW  ListC  0  THENA  Auto)
  THEN  (Decide  \muparrow{}P[u]  THEN  Auto)
  THEN  BackThruSomeHyp
  THEN  (Decide  \mkleeneopen{}i  =  0\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  (Complete  ((RWO  "-1"  (-4)\mcdot{}  THEN  AllReduce  THEN  Auto)))
  THEN  (RWO  "select-cons-tl"  (-4)  THEN  Auto)
  THEN  (InstConcl  [\mkleeneopen{}i  -  1\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (InstHyp  [\mkleeneopen{}j  +  1\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto)
  THEN  RWO  "select-cons-tl"  (-1)
  THEN  AllReduce
  THEN  Auto)

---

Home Index