---

Step * 1 1 2 1 1 of Lemma make-strict_wf


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;alpha 0;λi',v. if v <z alpha (i' + 1) then alpha (i' + 1) else v + 1 fi ) <z alpha\000C 
                                                                                                              (i + 1)
then alpha (i + 1)
else primrec(i;alpha 0;λi',v. if v <z alpha (i' + 1) then alpha (i' + 1) else v + 1 fi ) + 1
fi 
BY
{ ((Subst' primrec(i;alpha 0;λi',v. if v <z alpha (i' + 1) then alpha (i' + 1) else v + 1 fi ) ~ make-strict(alpha) i 0
    THENA Unfold `make-strict` 0
    )
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((Subst'  primrec(i;alpha  0;\mlambda{}i',v.  if  v  <z  alpha  (i'  +  1)  then  alpha  (i'  +  1)  else  v  +  1  fi  ) 
    \msim{}  make-strict(alpha)  i  0
    THENA  Unfold  `make-strict`  0
    )
  THEN  Reduce  0
  THEN  Auto)

---

Home Index