---

Step * 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(let v1 = if name_eq(name;x) then t else name fi  in pinew(v1;pi-replace(t;x;body))) = (pi-rank(body) + 1) ∈ ℤ
BY
{ (RepUR ``let`` 0 THEN Unfolds ``pi-rank`` 0 THEN Reduce 0 THEN Fold `pi-rank` 0) }

1
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) ∈ ℤ

---

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(let  v1  =  if  name\_eq(name;x)  then  t  else  name  fi    in
                            pinew(v1;pi-replace(t;x;body)))
=  (pi-rank(body)  +  1)


By

---

Latex:
(RepUR  ``let``  0  THEN  Unfolds  ``pi-rank``  0  THEN  Reduce  0  THEN  Fold  `pi-rank`  0)

---

Home Index