---

Step * 1 of Lemma es-fix-fun-exp


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))
BY
{ (D 0 THEN (InstConcl [⌈0⌉]⋅ THEN Reduce 0 THEN Auto)⋅) }

---

Latex:



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.  \mforall{}e1:E(X).  ((e1  <  e)  {}\mRightarrow{}  (\mdownarrow{}\mexists{}n:\mBbbN{}.  (f**(e1)  =  (f\^{}n  e1))))
7.  e  =  (f  e)
\mvdash{}  \mdownarrow{}\mexists{}n:\mBbbN{}.  (e  =  (f\^{}n  e))


By

(D  0  THEN  (InstConcl  [\mkleeneopen{}0\mkleeneclose{}]\mcdot{}  THEN  Reduce  0  THEN  Auto)\mcdot{})

---

Home Index