---

Step * 1 1 of Lemma make-strict_wf


1. alpha : ℕ ⟶ ℕ
2. make-strict(alpha) ∈ ℕ ⟶ ℕ
3. i : ℕ
⊢ make-strict(alpha) i < make-strict(alpha) (i + 1)
BY
{ xxx(NatInd (-1) THEN RW (AddrC [2] (UnfoldC `make-strict`)) 0 THEN Reduce 0)xxx }

1
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 

2
1. alpha : ℕ ⟶ ℕ
2. make-strict(alpha) ∈ ℕ ⟶ ℕ
3. i : ℤ
4. 0 < i
5. make-strict(alpha) (i - 1) < make-strict(alpha) ((i - 1) + 1)
⊢ make-strict(alpha) i < primrec(i + 1;alpha 0;λi',v. if v <z alpha (i' + 1) then alpha (i' + 1) else v + 1 fi )

---

Latex:

---

Latex:

1.  alpha  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  make-strict(alpha)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
3.  i  :  \mBbbN{}
\mvdash{}  make-strict(alpha)  i  <  make-strict(alpha)  (i  +  1)


By

---

Latex:
xxx(NatInd  (-1)  THEN  RW  (AddrC  [2]  (UnfoldC  `make-strict`))  0  THEN  Reduce  0)xxx

---

Home Index