---

Step * of Lemma num-antecedents-fun_exp

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[Sys:EClass(Top)]. ∀[f:sys-antecedent(es;Sys)]. ∀[n:ℕ]. ∀[e:E(Sys)].
  #f(f^n e) = (#f(e) - n) ∈ ℤ supposing n ≤ #f(e)
BY
{ ((InductionOnNat⋅ THEN Reduce 0 THEN Auto)
   THEN (Assert #f(e) = (1 + #f(f e)) ∈ ℤ BY
               (MoveToConcl (-1)
                THEN RW (AddrC [2;2] (RecUnfoldC `num-antecedents`)) 0
                THEN RW (AddrC [1;2] (RecUnfoldC `num-antecedents`)) 0
                THEN AutoSplit))
   ) }

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

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[Sys:EClass(Top)].  \mforall{}[f:sys-antecedent(es;Sys)].  \mforall{}[n:\mBbbN{}].  \mforall{}[e:E(Sys)].
    \#f(f\^{}n  e)  =  (\#f(e)  -  n)  supposing  n  \mleq{}  \#f(e)


By

((InductionOnNat\mcdot{}  THEN  Reduce  0  THEN  Auto)
  THEN  (Assert  \#f(e)  =  (1  +  \#f(f  e))  BY
                          (MoveToConcl  (-1)
                            THEN  RW  (AddrC  [2;2]  (RecUnfoldC  `num-antecedents`))  0
                            THEN  RW  (AddrC  [1;2]  (RecUnfoldC  `num-antecedents`))  0
                            THEN  AutoSplit))
  )

---

Home Index