---

Step * of Lemma pi-rank-pi-replace

∀[t,x:Name]. ∀[P:pi_term()].  (pi-rank(pi-replace(t;x;P)) = pi-rank(P) ∈ ℤ)
BY
{ (Auto
   THEN (MoveToConcl (-1) THEN BLemma `pi_term-induction` )
   THEN Auto
   THEN (RepUR ``pi-replace pi-rank`` 0 THEN Reduce 0 THEN Try (Folds ``pi-rank pi-replace`` 0) THEN Auto)⋅) }

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

---

Latex:

---

Latex:
\mforall{}[t,x:Name].  \mforall{}[P:pi\_term()].    (pi-rank(pi-replace(t;x;P))  =  pi-rank(P))


By

---

Latex:
(Auto
  THEN  (MoveToConcl  (-1)  THEN  BLemma  `pi\_term-induction`  )
  THEN  Auto
  THEN  (RepUR  ``pi-replace  pi-rank``  0
              THEN  Reduce  0
              THEN  Try  (Folds  ``pi-rank  pi-replace``  0)
              THEN  Auto)\mcdot{})

---

Home Index