---

Step * 1 2 of Lemma pi-rank-pi-simple-subst-aux


1. r : ℕ
2. ∀P:pi_term()
     (pi-rank(P) < r ⇒ (∀t,x:Name. ∀avoid:Name List.  (pi-rank(pi-simple-subst-aux(t;x;P;avoid)) = pi-rank(P) ∈ ℤ)))
3. name : Name
4. P2 : pi_term()
5. (pi-rank(P2) + 1) = r ∈ ℕ@i
6. t : Name@i
7. x : Name@i
8. avoid : Name List@i
⊢ pi-rank(let w = maybe-new(name;avoid) in
           let P1 = pi-replace(w;name;P2) in
           pinew(w;pi-simple-subst-aux(t;x;P1;[w / avoid])))
= (pi-rank(P2) + 1)
∈ ℤ
BY
{ (RepUR ``let`` 0⋅
   THEN (Auto THEN Auto')
   THEN (Unfold `pi-rank` 0
         THEN Reduce 0
         THEN Fold `pi-rank` 0
         THEN RWO "2" 0
         THEN Auto
         THEN (RWO "pi-rank-pi-replace" 0 THEN Auto THEN Auto')⋅)⋅)⋅ }

---

Latex:

---

Latex:

1.  r  :  \mBbbN{}
2.  \mforall{}P:pi\_term()
          (pi-rank(P)  <  r
          {}\mRightarrow{}  (\mforall{}t,x:Name.  \mforall{}avoid:Name  List.    (pi-rank(pi-simple-subst-aux(t;x;P;avoid))  =  pi-rank(P))))
3.  name  :  Name
4.  P2  :  pi\_term()
5.  (pi-rank(P2)  +  1)  =  r@i
6.  t  :  Name@i
7.  x  :  Name@i
8.  avoid  :  Name  List@i
\mvdash{}  pi-rank(let  w  =  maybe-new(name;avoid)  in
                      let  P1  =  pi-replace(w;name;P2)  in
                      pinew(w;pi-simple-subst-aux(t;x;P1;[w  /  avoid])))
=  (pi-rank(P2)  +  1)


By

---

Latex:
(RepUR  ``let``  0\mcdot{}
  THEN  (Auto  THEN  Auto')
  THEN  (Unfold  `pi-rank`  0
              THEN  Reduce  0
              THEN  Fold  `pi-rank`  0
              THEN  RWO  "2"  0
              THEN  Auto
              THEN  (RWO  "pi-rank-pi-replace"  0  THEN  Auto  THEN  Auto')\mcdot{})\mcdot{})\mcdot{}

---

Home Index