---

Step * of Lemma assert-b-exists

∀n:ℕ. ∀P:ℕn ⟶ 𝔹.  (↑(∃i<n.P[i])_b ⇐⇒ ∃i:ℕn. (↑P[i]))
BY
{ (InductionOnNat
   THEN RepUR ``b-exists`` 0
   THEN Try (Complete ((Auto THEN D -1 THEN Auto)))
   THEN ParallelLast
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN (SplitOnConclITE THENA Auto)
   THEN Try (Complete (Auto))
   THEN Fold `b-exists` 0
   THEN Reduce 0
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN (RWO "-2" 0 THENA Auto)) }

1
1. n : ℤ
2. [%1] : 0 < n
3. ∀P:ℕn - 1 ⟶ 𝔹. (↑(∃i<n - 1.P[i])_b ⇐⇒ ∃i:ℕn - 1. (↑P[i]))
4. P : ℕn ⟶ 𝔹
5. ↑(∃i<n - 1.P[i])_b ⇐⇒ ∃i:ℕn - 1. (↑P[i])
6. 1 ≤ n
⊢ (↑P[n - 1]) ∨ (∃i:ℕn - 1. (↑P[i])) ⇐⇒ ∃i:ℕn. (↑P[i])

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}P:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}.    (\muparrow{}(\mexists{}i<n.P[i])\_b  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}n.  (\muparrow{}P[i]))


By

---

Latex:
(InductionOnNat
  THEN  RepUR  ``b-exists``  0
  THEN  Try  (Complete  ((Auto  THEN  D  -1  THEN  Auto)))
  THEN  ParallelLast
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Try  (Complete  (Auto))
  THEN  Fold  `b-exists`  0
  THEN  Reduce  0
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  (RWO  "-2"  0  THENA  Auto))

---

Home Index