---

Step * 1 1 of Lemma rank-option-decompose


1. P : pi_term()
2. ↑pioption?(P)
3. P = pioption(pioption-left(P);pioption-right(P)) ∈ pi_term()
⊢ pi-rank(P) = ((pi-rank(pioption-left(P)) + pi-rank(pioption-right(P))) + 1) ∈ ℕ
BY
{ InstLemma `rank-option` [⌈pioption-left(P)⌉; ⌈pioption-right(P)⌉]⋅
THEN Auto }

---

Latex:

---

Latex:

1.  P  :  pi\_term()
2.  \muparrow{}pioption?(P)
3.  P  =  pioption(pioption-left(P);pioption-right(P))
\mvdash{}  pi-rank(P)  =  ((pi-rank(pioption-left(P))  +  pi-rank(pioption-right(P)))  +  1)


By

---

Latex:
InstLemma  `rank-option`  [\mkleeneopen{}pioption-left(P)\mkleeneclose{};  \mkleeneopen{}pioption-right(P)\mkleeneclose{}]\mcdot{}
THEN  Auto

---

Home Index