---

Step * 1 of Lemma rank-comm-decompose


1. P : pi_term()
2. ↑picomm?(P)
⊢ pi-rank(P) = (pi-rank(picomm-body(P)) + 1) ∈ ℕ
BY
{ (InstLemma `pi-comm-decompose` [⌈P⌉]⋅⋅ THENA Auto) }

1
1. P : pi_term()
2. ↑picomm?(P)
3. P = picomm(picomm-pre(P);picomm-body(P)) ∈ pi_term()
⊢ pi-rank(P) = (pi-rank(picomm-body(P)) + 1) ∈ ℕ

---

Latex:

---

Latex:

1.  P  :  pi\_term()
2.  \muparrow{}picomm?(P)
\mvdash{}  pi-rank(P)  =  (pi-rank(picomm-body(P))  +  1)


By

---

Latex:
(InstLemma  `pi-comm-decompose`  [\mkleeneopen{}P\mkleeneclose{}]\mcdot{}\mcdot{}  THENA  Auto)

---

Home Index