---

Step * of Lemma parallel-class-bind-right

∀[Info,T,S:Type]. ∀[X:EClass(T)]. ∀[Y,Z:T ─→ EClass(S)].  (X >x> Y[x] || Z[x] = X >x> Y[x] || X >x> Z[x] ∈ EClass(S))
BY
{ (Auto
   THEN RepUR ``parallel-class eclass-compose2 bind-class eclass`` 0
   THEN RepeatFor 2 ((EqCD THENA Auto))
   THEN (Assert ≤loc(e) ∈ bag({e':E| e' ≤loc e } ) BY
               (SubsumeC ⌈{e':E| e' ≤loc e }  List⌉⋅ THEN Auto))
   THEN RWO "bag-combine-append-right<" 0
   THEN Auto
   THEN Try ((Fold `eclass` 0 THEN Auto))
   THEN ((EqCD THEN Auto) ORELSE Auto)
   THEN RepeatFor 2 ((RWO "bag-combine-append-right<" 0
                      THEN Auto
                      THEN Try ((Fold `eclass` 0 THEN Auto))
                      THEN ((EqCD THEN Auto) ORELSE Auto))⋅)) }

---

Latex:


\mforall{}[Info,T,S:Type].  \mforall{}[X:EClass(T)].  \mforall{}[Y,Z:T  {}\mrightarrow{}  EClass(S)].
    (X  >x>  Y[x]  ||  Z[x]  =  X  >x>  Y[x]  ||  X  >x>  Z[x])


By

(Auto
  THEN  RepUR  ``parallel-class  eclass-compose2  bind-class  eclass``  0
  THEN  RepeatFor  2  ((EqCD  THENA  Auto))
  THEN  (Assert  \mleq{}loc(e)  \mmember{}  bag(\{e':E|  e'  \mleq{}loc  e  \}  )  BY
                          (SubsumeC  \mkleeneopen{}\{e':E|  e'  \mleq{}loc  e  \}    List\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  RWO  "bag-combine-append-right<"  0
  THEN  Auto
  THEN  Try  ((Fold  `eclass`  0  THEN  Auto))
  THEN  ((EqCD  THEN  Auto)  ORELSE  Auto)
  THEN  RepeatFor  2  ((RWO  "bag-combine-append-right<"  0
                                        THEN  Auto
                                        THEN  Try  ((Fold  `eclass`  0  THEN  Auto))
                                        THEN  ((EqCD  THEN  Auto)  ORELSE  Auto))\mcdot{}))

---

Home Index