---

Step * of Lemma rank-par

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

---

Latex:

---

Latex:
\mforall{}[P,Q:pi\_term()].    (pi-rank(pipar(P;Q))  =  ((pi-rank(P)  +  pi-rank(Q))  +  1))


By

---

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

---

Home Index