---

Step * of Lemma parallel-class-bind-left

∀[Info,T,S:Type]. ∀[X,Y:EClass(T)]. ∀[Z:T ─→ EClass(S)].  (X || Y >t> Z[t] = X >t> Z[t] || Y >t> Z[t] ∈ 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 GenConclAtAddr [3;1;1]
   THEN GenConclAtAddr [3;2;1]
   THEN Using [`B',⌈S⌉] (BLemma `bag-combine-append-left`)⋅
   THEN Auto
   THEN Try ((Fold `eclass` 0 THEN Auto))
   THEN Auto) }

---

Latex:


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


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  GenConclAtAddr  [3;1;1]
  THEN  GenConclAtAddr  [3;2;1]
  THEN  Using  [`B',\mkleeneopen{}S\mkleeneclose{}]  (BLemma  `bag-combine-append-left`)\mcdot{}
  THEN  Auto
  THEN  Try  ((Fold  `eclass`  0  THEN  Auto))
  THEN  Auto)

---

Home Index