---

Step * 1 1 2 of Lemma make-strict_wf


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 )
BY
{ ((RWO "primrec-unroll" 0 THENA Auto) THEN AutoSplit) }

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

---

Latex:

---

Latex:

1.  alpha  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  make-strict(alpha)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
3.  i  :  \mBbbZ{}
4.  0  <  i
5.  make-strict(alpha)  (i  -  1)  <  make-strict(alpha)  ((i  -  1)  +  1)
\mvdash{}  make-strict(alpha)  i  <  primrec(i  +  1;alpha  0;\mlambda{}i',v.  if  v  <z  alpha  (i'  +  1)
                                                                                                          then  alpha  (i'  +  1)
                                                                                                          else  v  +  1
                                                                                                          fi  )


By

---

Latex:
((RWO  "primrec-unroll"  0  THENA  Auto)  THEN  AutoSplit)

---

Home Index