---

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

∀[P:pi_term()]. ∀[t,x:Name]. ∀[avoid:Name List].  (pi-rank(pi-simple-subst-aux(t;x;P;avoid)) = pi-rank(P) ∈ ℤ)
BY
{ (RemoveUniform Auto Auto
   THEN (InductionOn ⌜r = pi-rank(P) ∈ ℕ⌝ CompNatInd⋅ THEN Try ((BHyp (-1) THEN Auto)))
   THEN Auto
   THEN (Assert ∀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) ∈ ℤ))) BY
               (Auto THEN InstHyp [⌜pi-rank(P1)⌝] 2⋅ THEN Auto))
   THEN Thin 2
   THEN PromoteHyp (-1) 2) }

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

---

Latex:

---

Latex:
\mforall{}[P:pi\_term()].  \mforall{}[t,x:Name].  \mforall{}[avoid:Name  List].
    (pi-rank(pi-simple-subst-aux(t;x;P;avoid))  =  pi-rank(P))


By

---

Latex:
(RemoveUniform  Auto  Auto
  THEN  (InductionOn  \mkleeneopen{}r  =  pi-rank(P)\mkleeneclose{}  CompNatInd\mcdot{}  THEN  Try  ((BHyp  (-1)  THEN  Auto)))
  THEN  Auto
  THEN  (Assert  \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))))  BY
                          (Auto  THEN  InstHyp  [\mkleeneopen{}pi-rank(P1)\mkleeneclose{}]  2\mcdot{}  THEN  Auto))
  THEN  Thin  2
  THEN  PromoteHyp  (-1)  2)

---

Home Index