---

Step * of Lemma assert-bdd-all

∀n:ℕ. ∀P:ℕn ⟶ 𝔹.  (↑bdd-all(n;i.P[i]) ⇐⇒ ∀i:ℕn. (↑P[i]))
BY
{ (InductionOnNat
   THEN RepUR ``bdd-all`` 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 `bdd-all` 0
   THEN Reduce 0
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN (RWO "-2" 0 THENA Auto)) }

1
1. n : ℤ
2. 0 < n
3. ∀P:ℕn - 1 ⟶ 𝔹. (↑bdd-all(n - 1;i.P[i]) ⇐⇒ ∀i:ℕn - 1. (↑P[i]))
4. P : ℕn ⟶ 𝔹
5. ↑bdd-all(n - 1;i.P[i]) ⇐⇒ ∀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{}bdd-all(n;i.P[i])  \mLeftarrow{}{}\mRightarrow{}  \mforall{}i:\mBbbN{}n.  (\muparrow{}P[i]))


By

---

Latex:
(InductionOnNat
  THEN  RepUR  ``bdd-all``  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  `bdd-all`  0
  THEN  Reduce  0
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  (RWO  "-2"  0  THENA  Auto))

---

Home Index