---

Step * 2 1 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. ¬(e = (f e) ∈ E)
7. ∀e1:E(X). ((e1 < e) ⇒ (↓∃n:ℕ. (f**(e1) = (f^n e1) ∈ E(X))))
8. (f e < e)
9. ↓∃n:ℕ. (f**(f e) = (f^n (f e)) ∈ E(X))
⊢ ↓∃n:ℕ. (f**(f e) = (f^n e) ∈ E(X))
BY
{ (ParallelLast THEN ExRepD THEN InstConcl [⌈n + 1⌉]⋅ 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.  \mneg{}(e  =  (f  e))
7.  \mforall{}e1:E(X).  ((e1  <  e)  {}\mRightarrow{}  (\mdownarrow{}\mexists{}n:\mBbbN{}.  (f**(e1)  =  (f\^{}n  e1))))
8.  (f  e  <  e)
9.  \mdownarrow{}\mexists{}n:\mBbbN{}.  (f**(f  e)  =  (f\^{}n  (f  e)))
\mvdash{}  \mdownarrow{}\mexists{}n:\mBbbN{}.  (f**(f  e)  =  (f\^{}n  e))


By

(ParallelLast  THEN  ExRepD  THEN  InstConcl  [\mkleeneopen{}n  +  1\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index