---

Step * of Lemma es-fix-fun-exp

∀[Info:Type]. ∀es:EO+(Info). ∀X:EClass(Top). ∀f:sys-antecedent(es;X). ∀e:E(X).  (↓∃n:ℕ. (f**(e) = (f^n e) ∈ E(X)))
BY
{ (Auto THEN MoveToConcl (-1) THEN CausalInd'⋅ THEN ((RWO "es-fix-cases" 0 THENA Auto) THEN AutoSplit)⋅) }

1
1. Info : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : sys-antecedent(es;X)@i
5. e : E(X)@i
6. ∀e1:E(X). ((e1 < e) ⇒ (↓∃n:ℕ. (f**(e1) = (f^n e1) ∈ E(X))))
7. e = (f e) ∈ E
⊢ ↓∃n:ℕ. (e = (f^n e) ∈ E(X))

2
1. Info : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : sys-antecedent(es;X)@i
5. e : E(X)@i
6. ¬(e = (f e) ∈ E)
7. ∀e1:E(X). ((e1 < e) ⇒ (↓∃n:ℕ. (f**(e1) = (f^n e1) ∈ E(X))))
⊢ ↓∃n:ℕ. (f**(f e) = (f^n e) ∈ E(X))

---

Latex:


\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}f:sys-antecedent(es;X).  \mforall{}e:E(X).    (\mdownarrow{}\mexists{}n:\mBbbN{}.  (f**(e)  =  (f\^{}n  e)))


By

(Auto
  THEN  MoveToConcl  (-1)
  THEN  CausalInd'\mcdot{}
  THEN  ((RWO  "es-fix-cases"  0  THENA  Auto)  THEN  AutoSplit)\mcdot{})

---

Home Index