---

Step * 1 of Lemma member-es-fix-prior-fixedpoints


1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : E(X) ─→ E(X)@i
5. ∀x:E(X). f x c≤ x@i
6. e : E(X)@i
⊢ (f**(e) ∈ prior-f-fixedpoints(f**(e)))
BY
{ (RecUnfold `es-prior-fixedpoints` 0
   THEN (SplitOn ⌈f f**(e) = f**(e)⌉⋅
         THENA (Try (Complete (Auto)) THEN Try ((GenConclTerm ⌈f**(e)⌉⋅ THEN Complete (Auto))))
         )
   ) }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : E(X) ─→ E(X)@i
5. ∀x:E(X). f x c≤ x@i
6. e : E(X)@i
7. f f**(e) = f**(e) = tt
8. (f f**(e)) = f**(e) ∈ E
⊢ (f**(e) ∈ if f**(e) ∈b prior(X) then prior-f-fixedpoints(prior(X)(f**(e))) @ [f**(e)] else [f**(e)] fi )

2
1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : E(X) ─→ E(X)@i
5. ∀x:E(X). f x c≤ x@i
6. e : E(X)@i
7. f f**(e) = f**(e) = ff
8. ¬((f f**(e)) = f**(e) ∈ E)
⊢ (f**(e) ∈ prior-f-fixedpoints(f**(f**(e))))

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  X  :  EClass(Top)@i'
4.  f  :  E(X)  {}\mrightarrow{}  E(X)@i
5.  \mforall{}x:E(X).  f  x  c\mleq{}  x@i
6.  e  :  E(X)@i
\mvdash{}  (f**(e)  \mmember{}  prior-f-fixedpoints(f**(e)))


By

---

Latex:
(RecUnfold  `es-prior-fixedpoints`  0
  THEN  (SplitOn  \mkleeneopen{}f  f**(e)  =  f**(e)\mkleeneclose{}\mcdot{}
              THENA  (Try  (Complete  (Auto))  THEN  Try  ((GenConclTerm  \mkleeneopen{}f**(e)\mkleeneclose{}\mcdot{}  THEN  Complete  (Auto))))
              )
  )

---

Home Index