---

Step * 1 of Lemma es-fix-order-preserving

.....wf..... 
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. ∀b,b':E(X).
     (b is f*(b') ⇒ (loc(f**(e)) = loc(b) ∈ Id) ⇒ (loc(e) = loc(b') ∈ Id) ⇒ ((f**(e) <loc b) ⇐⇒ (e <loc b')))
8. e' : E(X)@i
9. loc(e) = loc(e') ∈ Id@i
10. loc(f**(e)) = loc(f**(e')) ∈ Id@i
11. (f**(e) <loc f**(e')) ─→ (e <loc e')
⊢ (f**(e) <loc f**(e')) ∈ Type
BY
{ (MemCD THEN DoSubsume THEN Auto) }

---

Latex:


.....wf..... 
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
7.  \mforall{}b,b':E(X).
          (b  is  f*(b')
          {}\mRightarrow{}  (loc(f**(e))  =  loc(b))
          {}\mRightarrow{}  (loc(e)  =  loc(b'))
          {}\mRightarrow{}  ((f**(e)  <loc  b)  \mLeftarrow{}{}\mRightarrow{}  (e  <loc  b')))
8.  e'  :  E(X)@i
9.  loc(e)  =  loc(e')@i
10.  loc(f**(e))  =  loc(f**(e'))@i
11.  (f**(e)  <loc  f**(e'))  {}\mrightarrow{}  (e  <loc  e')
\mvdash{}  (f**(e)  <loc  f**(e'))  \mmember{}  Type


By

(MemCD  THEN  DoSubsume  THEN  Auto)

---

Home Index