---

Step * of Lemma sys-antecedent-fixedpoint

∀[Info:Type]
  ∀es:EO+(Info). ∀Sys:EClass(Top). ∀f:sys-antecedent(es;Sys). ∀e:E(Sys).
    ∃n:ℕ. (((f (f^n e)) = (f^n e) ∈ E(Sys)) ∧ ¬((f (f^n - 1 e)) = (f^n - 1 e) ∈ E(Sys)) supposing 0 < n)
BY
{ (InstLemma `num-antecedents-property` []
   THEN RepeatFor 5 (ParallelLast')
   THEN D -1
   THEN DVar `f'
   THEN InstConcl [⌈#f(e)⌉]⋅
   THEN Auto) }

---

Latex:


\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}Sys:EClass(Top).  \mforall{}f:sys-antecedent(es;Sys).  \mforall{}e:E(Sys).
        \mexists{}n:\mBbbN{}.  (((f  (f\^{}n  e))  =  (f\^{}n  e))  \mwedge{}  \mneg{}((f  (f\^{}n  -  1  e))  =  (f\^{}n  -  1  e))  supposing  0  <  n)


By

(InstLemma  `num-antecedents-property`  []
  THEN  RepeatFor  5  (ParallelLast')
  THEN  D  -1
  THEN  DVar  `f'
  THEN  InstConcl  [\mkleeneopen{}\#f(e)\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index