---

Step * 1 1 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. pre : pi_prefix()
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(pi_prefix_ind(pre;
                        pisend(c,v)⇒ let c1 = if name_eq(c;x) then t else c fi  in
                                       let v1 = if name_eq(v;x) then t else v fi  in
                                       picomm(pisend(c1;v1);pi-simple-subst-aux(t;x;P2;avoid));
                        pircv(c,v)⇒ let w = maybe-new(v;avoid) in
                                      let c1 = if name_eq(c;x) then t else c fi  in
                                      let R1 = pi-replace(w;v;P2) in
                                      picomm(pircv(c1;w);pi-simple-subst-aux(t;x;R1;[w / avoid]))) )
= (pi-rank(P2) + 1)
∈ ℤ
BY
{ (D 3
   THEN Reduce 0
   THEN RepUR ``let`` 0
   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.  pre  :  pi\_prefix()
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(pi\_prefix\_ind(pre;
                                                pisend(c,v){}\mRightarrow{}  let  c1  =  if  name\_eq(c;x)  then  t  else  c  fi    in
                                                                              let  v1  =  if  name\_eq(v;x)  then  t  else  v  fi    in
                                                                              picomm(pisend(c1;v1);pi-simple-subst-aux(t;x;P2;avoid));
                                                pircv(c,v){}\mRightarrow{}  let  w  =  maybe-new(v;avoid)  in
                                                                            let  c1  =  if  name\_eq(c;x)  then  t  else  c  fi    in
                                                                            let  R1  =  pi-replace(w;v;P2)  in
                                                                            picomm(pircv(c1;w);pi-simple-subst-aux(t;x;R1;[w  /  avoid])))  )
=  (pi-rank(P2)  +  1)


By

---

Latex:
(D  3
  THEN  Reduce  0
  THEN  RepUR  ``let``  0
  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{})

---

Home Index