---

Step * 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. P : pi_term()@i
4. pi-rank(P) = r ∈ ℕ@i
5. t : Name@i
6. x : Name@i
7. avoid : Name List@i
⊢ pi-rank(pi-simple-subst-aux(t;x;P;avoid)) = pi-rank(P) ∈ ℤ
BY
{ (D 3
   THEN OnMaybeHyp 3 (\h. (Unfold `pi-rank` h THEN Reduce h THEN Try (Fold `pi-rank` h)))
   THEN RecUnfold `pi-simple-subst-aux` 0
   THEN Reduce 0
   THEN Auto
   THEN Unfold `pi-rank` 0
   THEN Reduce 0
   THEN Try (Fold `pi-rank` 0)
   THEN Try ((Auto' THEN RWO "2" 0 THEN Auto')⋅)) }

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

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

---

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.  P  :  pi\_term()@i
4.  pi-rank(P)  =  r@i
5.  t  :  Name@i
6.  x  :  Name@i
7.  avoid  :  Name  List@i
\mvdash{}  pi-rank(pi-simple-subst-aux(t;x;P;avoid))  =  pi-rank(P)


By

---

Latex:
(D  3
  THEN  OnMaybeHyp  3  (\mbackslash{}h.  (Unfold  `pi-rank`  h  THEN  Reduce  h  THEN  Try  (Fold  `pi-rank`  h)))
  THEN  RecUnfold  `pi-simple-subst-aux`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  Unfold  `pi-rank`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `pi-rank`  0)
  THEN  Try  ((Auto'  THEN  RWO  "2"  0  THEN  Auto')\mcdot{}))

---

Home Index