---

Step * of Lemma mkibs_wf

∀[p:ℕ ⟶ 𝔹]. mkibs(n.p[n]) ∈ IBS supposing ∀n:ℕ. ((↑p[n]) ⇒ (↑p[n + 1]))
BY
{ (Auto THEN MemTypeCD THEN Auto THEN RepUR ``mkibs`` 0 THEN Auto) }

1
1. p : ℕ ⟶ 𝔹
2. ∀n:ℕ. ((↑p[n]) ⇒ (↑p[n + 1]))
3. i : ℕ
⊢ if p[i] then 1 else 0 fi  ≤ if p[1 + i] then 1 else 0 fi 

---

Latex:

---

Latex:
\mforall{}[p:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}].  mkibs(n.p[n])  \mmember{}  IBS  supposing  \mforall{}n:\mBbbN{}.  ((\muparrow{}p[n])  {}\mRightarrow{}  (\muparrow{}p[n  +  1]))


By

---

Latex:
(Auto  THEN  MemTypeCD  THEN  Auto  THEN  RepUR  ``mkibs``  0  THEN  Auto)

---

Home Index