---

Step * 1 of Lemma mkibs_wf


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 
BY
{ ((D 2 With ⌜i⌝  THENA Auto) THEN AutoSplit) }

---

Latex:

---

Latex:

1.  p  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
2.  \mforall{}n:\mBbbN{}.  ((\muparrow{}p[n])  {}\mRightarrow{}  (\muparrow{}p[n  +  1]))
3.  i  :  \mBbbN{}
\mvdash{}  if  p[i]  then  1  else  0  fi    \mleq{}  if  p[1  +  i]  then  1  else  0  fi 


By

---

Latex:
((D  2  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)  THEN  AutoSplit)

---

Home Index