Step
*
of Lemma
rank-new-decompose
∀[P:pi_term()]. pi-rank(P) = (pi-rank(pinew-body(P)) + 1) ∈ ℕ supposing ↑pinew?(P)
BY
{ Auto }
1
1. P : pi_term()
2. ↑pinew?(P)
⊢ pi-rank(P) = (pi-rank(pinew-body(P)) + 1) ∈ ℕ
Latex:
Latex:
\mforall{}[P:pi\_term()]. pi-rank(P) = (pi-rank(pinew-body(P)) + 1) supposing \muparrow{}pinew?(P)
By
Latex:
Auto
Home
Index