---

Step * of Lemma rank-new

∀[v:Name]. ∀[P:pi_term()].  (pi-rank(pinew(v;P)) = (pi-rank(P) + 1) ∈ ℕ)
BY
{ Auto
THEN RepUR ``pi-rank`` 0⋅
THEN Fold
`pi-rank` 0⋅
THEN Auto' }

---

Latex:

---

Latex:
\mforall{}[v:Name].  \mforall{}[P:pi\_term()].    (pi-rank(pinew(v;P))  =  (pi-rank(P)  +  1))


By

---

Latex:
Auto
THEN  RepUR  ``pi-rank``  0\mcdot{}
THEN  Fold
`pi-rank`  0\mcdot{}
THEN  Auto'

---

Home Index