---

Step * of Lemma es-fix-order-preserving

∀[Info:Type]
  ∀es:EO+(Info). ∀X:EClass(Top). ∀f:E(X) ⟶ E(X).
    ((∀x:E(X). f x c≤ x) ⇒ global-order-preserving(es;X;f) ⇒ interface-order-preserving(es;X;λe.f**(e)))
BY
{ (Intros
   THEN UnfoldTopAb (-1)
   THEN UnfoldTopAb 0
   THEN Reduce 0
   THEN (D 0 THENA Auto)
   THEN (((InstHyp [⌜f**(e)⌝; ⌜e⌝] (-2))⋅ THENM (Thin (-3))) THENA Auto)
   THEN (UnivCD THENM ((InstHyp [⌜f**(e')⌝; ⌜e'⌝] (-4))⋅ THENM Trivial)⋅)
   THEN Try (Complete (Auto))) }

1
.....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

2
.....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
⊢ loc(f**(e)) = loc(f**(e')) ∈ Id ∈ ℙ

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}f:E(X)  {}\mrightarrow{}  E(X).
        ((\mforall{}x:E(X).  f  x  c\mleq{}  x)
        {}\mRightarrow{}  global-order-preserving(es;X;f)
        {}\mRightarrow{}  interface-order-preserving(es;X;\mlambda{}e.f**(e)))


By

---

Latex:
(Intros
  THEN  UnfoldTopAb  (-1)
  THEN  UnfoldTopAb  0
  THEN  Reduce  0
  THEN  (D  0  THENA  Auto)
  THEN  (((InstHyp  [\mkleeneopen{}f**(e)\mkleeneclose{};  \mkleeneopen{}e\mkleeneclose{}]  (-2))\mcdot{}  THENM  (Thin  (-3)))  THENA  Auto)
  THEN  (UnivCD  THENM  ((InstHyp  [\mkleeneopen{}f**(e')\mkleeneclose{};  \mkleeneopen{}e'\mkleeneclose{}]  (-4))\mcdot{}  THENM  Trivial)\mcdot{})
  THEN  Try  (Complete  (Auto)))

---

Home Index