---

Step * of Lemma rank-rep

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

---

Latex:

---

Latex:
\mforall{}[P:pi\_term()].  (pi-rank(pirep(P))  =  (pi-rank(P)  +  1))


By

---

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

---

Home Index