---

Step * of Lemma rank-comm

∀[P:pi_term()]. ∀[pre:pi_prefix()].  (pi-rank(picomm(pre;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()].  \mforall{}[pre:pi\_prefix()].    (pi-rank(picomm(pre;P))  =  (pi-rank(P)  +  1))


By

---

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

---

Home Index