---

Step * 1 1 of Lemma pi-rank-pi-replace


1. t : Name
2. x : Name
3. name : Name@i
4. body : pi_term()@i
5. pi-rank(pi-replace(t;x;body)) = pi-rank(body) ∈ ℤ@i
⊢ (pi-rank(pi-replace(t;x;body)) + 1) = (pi-rank(body) + 1) ∈ ℤ
BY
{ Auto }

---

Latex:

---

Latex:

1.  t  :  Name
2.  x  :  Name
3.  name  :  Name@i
4.  body  :  pi\_term()@i
5.  pi-rank(pi-replace(t;x;body))  =  pi-rank(body)@i
\mvdash{}  (pi-rank(pi-replace(t;x;body))  +  1)  =  (pi-rank(body)  +  1)


By

---

Latex:
Auto

---

Home Index