---

Step * 1 1 1 of Lemma make-strict-agrees


1. alpha : ℕ ⟶ ℕ
2. n : ℤ
3. 0 < n
4. strictly-increasing-seq(n;alpha)
5. i : ℕn
6. ¬i < 1
7. ∀i:ℕn - 1. ((make-strict(alpha) i) = (alpha i) ∈ ℤ)
⊢ if primrec(i - 1;alpha 0;λi',v. if v <z alpha (i' + 1) then alpha (i' + 1) else v + 1 fi ) <z alpha ((i - 1) + 1)
then alpha ((i - 1) + 1)
else primrec(i - 1;alpha 0;λi',v. if v <z alpha (i' + 1) then alpha (i' + 1) else v + 1 fi ) + 1
fi 
= (alpha i)
∈ ℤ
BY
{ (Subst' primrec(i - 1;alpha 0;λi',v. if v <z alpha (i' + 1) then alpha (i' + 1) else v + 1 fi ) ~ make-strict(alpha) 
                                                                                               (i - 1) 0
   THENA (RepUR ``make-strict`` 0 THEN Auto)
   ) }

1
1. alpha : ℕ ⟶ ℕ
2. n : ℤ
3. 0 < n
4. strictly-increasing-seq(n;alpha)
5. i : ℕn
6. ¬i < 1
7. ∀i:ℕn - 1. ((make-strict(alpha) i) = (alpha i) ∈ ℤ)
⊢ if make-strict(alpha) (i - 1) <z alpha ((i - 1) + 1)
then alpha ((i - 1) + 1)
else (make-strict(alpha) (i - 1)) + 1
fi 
= (alpha i)
∈ ℤ

---

Latex:

---

Latex:

1.  alpha  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  strictly-increasing-seq(n;alpha)
5.  i  :  \mBbbN{}n
6.  \mneg{}i  <  1
7.  \mforall{}i:\mBbbN{}n  -  1.  ((make-strict(alpha)  i)  =  (alpha  i))
\mvdash{}  if  primrec(i  -  1;alpha  0;\mlambda{}i',v.  if  v  <z  alpha  (i'  +  1)  then  alpha  (i'  +  1)  else  v  +  1  fi  )  <z  alph\000Ca 
                                                                                                                                                                                      ((i  -  1)
                                                                                                                                                                                      +  1)
then  alpha  ((i  -  1)  +  1)
else  primrec(i  -  1;alpha  0;\mlambda{}i',v.  if  v  <z  alpha  (i'  +  1)  then  alpha  (i'  +  1)  else  v  +  1  fi  )  +  1
fi 
=  (alpha  i)


By

---

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

---

Home Index