---

Step * 1 of Lemma num-antecedents-fun_exp


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)) ∈ ℤ
⊢ #f(f^n e) = (#f(e) - n) ∈ ℤ
BY
{ ((InstHyp [⌈f e⌉] (-4)⋅ THEN Auto)⋅ THEN NthHypEq (-1) THEN RepeatFor 2 ((EqCD THEN Auto'))) }

1
.....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)

---

Latex:



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))
\mvdash{}  \#f(f\^{}n  e)  =  (\#f(e)  -  n)


By

((InstHyp  [\mkleeneopen{}f  e\mkleeneclose{}]  (-4)\mcdot{}  THEN  Auto)\mcdot{}  THEN  NthHypEq  (-1)  THEN  RepeatFor  2  ((EqCD  THEN  Auto')))

---

Home Index