---

Step * 1 1 of Lemma es-le-linorder-interface


1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. j : Id@i
5. Linorder({e:E| loc(e) = j ∈ Id} ;a,b.a ≤loc b )
⊢ Linorder({e':E(X)| loc(e') = j ∈ Id} ;a,b.a ≤loc b )
BY
{ (RepeatFor 3 (ParallelLast')
   THEN All Reduce
   THEN SplitAndConcl
   THEN SplitAndHyps
   THEN Try (OnMaybeHyp 5 (\h. (RepeatFor 2 ((ParallelOp h THENA Auto))
                                THEN Repeat (ParallelLast)
                                THEN Complete (Auto))))) }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. j : Id@i
5. Connex({e:E| loc(e) = j ∈ Id} ;a,b.a ≤loc b )
6. Refl({e:E| loc(e) = j ∈ Id} ;a,b.a ≤loc b )
7. Trans({e:E| loc(e) = j ∈ Id} ;a,b.a ≤loc b )
8. AntiSym({e:E| loc(e) = j ∈ Id} ;a,b.a ≤loc b )
⊢ AntiSym({e':E(X)| loc(e') = j ∈ Id} ;a,b.a ≤loc b )

---

Latex:



1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  X  :  EClass(Top)@i'
4.  j  :  Id@i
5.  Linorder(\{e:E|  loc(e)  =  j\}  ;a,b.a  \mleq{}loc  b  )
\mvdash{}  Linorder(\{e':E(X)|  loc(e')  =  j\}  ;a,b.a  \mleq{}loc  b  )


By

(RepeatFor  3  (ParallelLast')
  THEN  All  Reduce
  THEN  SplitAndConcl
  THEN  SplitAndHyps
  THEN  Try  (OnMaybeHyp  5  (\mbackslash{}h.  (RepeatFor  2  ((ParallelOp  h  THENA  Auto))
                                                            THEN  Repeat  (ParallelLast)
                                                            THEN  Complete  (Auto)))))

---

Home Index