---

Step * 1 1 of Lemma rank-new-decompose


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

---

Latex:

---

Latex:

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


By

---

Latex:
InstLemma  `rank-new`  [\mkleeneopen{}pinew-name(P)\mkleeneclose{};\mkleeneopen{}pinew-body(P)\mkleeneclose{}]\mcdot{}
THEN  Auto

---

Home Index