---

Step * 1 1 of Lemma num-antecedents-fun_exp

.....subterm..... T:t
3:n
1. Info : Type
2. es : EO+(Info)
3. Sys : EClass(Top)
4. f : sys-antecedent(es;Sys)
5. n : ℤ
6. 0 < n
7. ∀[e:E(Sys)]. #f(f^n - 1 e) = (#f(e) - n - 1) ∈ ℤ supposing (n - 1) ≤ #f(e)
8. e : E(Sys)
9. n ≤ #f(e)
10. #f(e) = (1 + #f(f e)) ∈ ℤ
11. #f(f^n - 1 (f e)) = (#f(f e) - n - 1) ∈ ℤ
⊢ (f^n e) = (f^n - 1 (f e)) ∈ E(Sys)
BY
{ (Subst' f e ~ f^1 e 0 THEN RWW "fun_exp_add_sq<" 0 THEN Reduce 0 THEN Auto) }

---

Latex:


.....subterm.....  T:t
3:n
1.  Info  :  Type
2.  es  :  EO+(Info)
3.  Sys  :  EClass(Top)
4.  f  :  sys-antecedent(es;Sys)
5.  n  :  \mBbbZ{}
6.  0  <  n
7.  \mforall{}[e:E(Sys)].  \#f(f\^{}n  -  1  e)  =  (\#f(e)  -  n  -  1)  supposing  (n  -  1)  \mleq{}  \#f(e)
8.  e  :  E(Sys)
9.  n  \mleq{}  \#f(e)
10.  \#f(e)  =  (1  +  \#f(f  e))
11.  \#f(f\^{}n  -  1  (f  e))  =  (\#f(f  e)  -  n  -  1)
\mvdash{}  (f\^{}n  e)  =  (f\^{}n  -  1  (f  e))


By

(Subst'  f  e  \msim{}  f\^{}1  e  0  THEN  RWW  "fun\_exp\_add\_sq<"  0  THEN  Reduce  0  THEN  Auto)

---

Home Index