---

Step * 1 1 2 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 + 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 
BY
{ (Subst' (i + 1) - 1 ~ i 0 THENA Auto) }

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;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 

---

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  +  1)  -  1;alpha  0;\mlambda{}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;\mlambda{}i',v.  if  v  <z  alpha  (i'  +  1)  then  alpha  (i'  +  1)  else  v  +  1  fi  )  +\000C  1
fi 


By

---

Latex:
(Subst'  (i  +  1)  -  1  \msim{}  i  0  THENA  Auto)

---

Home Index