---

Step * of Lemma rank-option-decompose

∀[P:pi_term()]. pi-rank(P) = ((pi-rank(pioption-left(P)) + pi-rank(pioption-right(P))) + 1) ∈ ℕ supposing ↑pioption?(P)
BY
{ Auto }

1
1. P : pi_term()
2. ↑pioption?(P)
⊢ pi-rank(P) = ((pi-rank(pioption-left(P)) + pi-rank(pioption-right(P))) + 1) ∈ ℕ

---

Latex:

---

Latex:
\mforall{}[P:pi\_term()]
    pi-rank(P)  =  ((pi-rank(pioption-left(P))  +  pi-rank(pioption-right(P)))  +  1) 
    supposing  \muparrow{}pioption?(P)


By

---

Latex:
Auto

---

Home Index