---

Step * 1 1 1 of Lemma make-strict_wf


1. alpha : ℕ ⟶ ℕ
2. make-strict(alpha) ∈ ℕ ⟶ ℕ
3. i : ℤ
⊢ make-strict(alpha) 0 < if alpha 0 <z alpha 1 then alpha 1 else (alpha 0) + 1 fi 
BY
{ xxx(AutoSplit THEN RepUR ``make-strict`` 0 THEN Auto)xxx }

---

Latex:

---

Latex:

1.  alpha  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  make-strict(alpha)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
3.  i  :  \mBbbZ{}
\mvdash{}  make-strict(alpha)  0  <  if  alpha  0  <z  alpha  1  then  alpha  1  else  (alpha  0)  +  1  fi 


By

---

Latex:
xxx(AutoSplit  THEN  RepUR  ``make-strict``  0  THEN  Auto)xxx

---

Home Index