---

Step * of Lemma eclass-disju-bind-left

∀[Info,A1,A2,B:Type]. ∀[X1:EClass(A1)]. ∀[X2:EClass(A2)]. ∀[Y1:A1 ─→ EClass(B)]. ∀[Y2:A2 ─→ EClass(B)].
  (X1 + X2 >x> case x of inl(a1) => Y1[a1] | inr(a2) => Y2[a2] = X1 >x> Y1[x] || X2 >x> Y2[x] ∈ EClass(B))
BY
{ (Auto
   THEN RepUR ``parallel-class eclass-compose2 bind-class eclass-disju eclass1 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 Try (Complete (Auto))
   THEN Try (Complete ((Fold `member` 0
                        THEN (MemCD THEN Try (Complete (Auto)))
                        THEN Using [`A',⌈A1 + A2⌉] MemCD⋅
                        THEN Auto)))
   THEN (EqCD THEN Auto)
   THEN (InstLemma `bag-combine-append-left` [⌈A1 + A2⌉;⌈B⌉;⌈bag-map(λx.(inl x);X1(e'))⌉;⌈bag-map(λx.(inr x );X2(e'))⌉;
         ⌈λ2x.case x of inl(a1) => Y1[a1] | inr(a2) => Y2[a2] es.e' e⌉]⋅
         THENA Auto
         )
   THEN (HypSubst' (-1) 0 THENA Auto)
   THEN (InstLemma `bag-combine-map` [⌈A1⌉;⌈A1 + A2⌉;⌈B⌉;⌈λ2x.case x of inl(a1) => Y1[a1] | inr(a2) => Y2[a2] es.e' e⌉;
         ⌈λx.(inl x)⌉;⌈X1(e')⌉]⋅
         THENA Auto
         )
   THEN (HypSubst' (-1) 0 THENA Auto)
   THEN Reduce 0
   THEN (InstLemma `bag-combine-map` [⌈A2⌉;⌈A1 + A2⌉;⌈B⌉;⌈λ2x.case x of inl(a1) => Y1[a1] | inr(a2) => Y2[a2] es.e' e⌉;
         ⌈λx.(inr x )⌉;⌈X2(e')⌉]⋅
         THENA Auto
         )
   THEN (HypSubst' (-1) 0 THENA Auto)
   THEN RepUR ``class-ap`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,A1,A2,B:Type].  \mforall{}[X1:EClass(A1)].  \mforall{}[X2:EClass(A2)].  \mforall{}[Y1:A1  {}\mrightarrow{}  EClass(B)].
\mforall{}[Y2:A2  {}\mrightarrow{}  EClass(B)].
    (X1  +  X2  >x>  case  x  of  inl(a1)  =>  Y1[a1]  |  inr(a2)  =>  Y2[a2]  =  X1  >x>  Y1[x]  ||  X2  >x>  Y2[x])


By

---

Latex:
(Auto
  THEN  RepUR  ``parallel-class  eclass-compose2  bind-class  eclass-disju  eclass1  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  Try  (Complete  (Auto))
  THEN  Try  (Complete  ((Fold  `member`  0
                                            THEN  (MemCD  THEN  Try  (Complete  (Auto)))
                                            THEN  Using  [`A',\mkleeneopen{}A1  +  A2\mkleeneclose{}]  MemCD\mcdot{}
                                            THEN  Auto)))
  THEN  (EqCD  THEN  Auto)
  THEN  (InstLemma  `bag-combine-append-left`  [\mkleeneopen{}A1  +  A2\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}bag-map(\mlambda{}x.(inl  x);X1(e'))\mkleeneclose{};
              \mkleeneopen{}bag-map(\mlambda{}x.(inr  x  );X2(e'))\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.case  x  of  inl(a1)  =>  Y1[a1]  |  inr(a2)  =>  Y2[a2]  es.e'  e\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  (HypSubst'  (-1)  0  THENA  Auto)
  THEN  (InstLemma  `bag-combine-map`  [\mkleeneopen{}A1\mkleeneclose{};\mkleeneopen{}A1  +  A2\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.case  x
                                                                                                                          of  inl(a1)  =>
                                                                                                                          Y1[a1]
                                                                                                                          |  inr(a2)  =>
                                                                                                                          Y2[a2] 
                                                                                                                        es.e' 
                                                                                                                        e\mkleeneclose{};\mkleeneopen{}\mlambda{}x.(inl  x)\mkleeneclose{};\mkleeneopen{}X1(e')\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  (HypSubst'  (-1)  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (InstLemma  `bag-combine-map`  [\mkleeneopen{}A2\mkleeneclose{};\mkleeneopen{}A1  +  A2\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.case  x
                                                                                                                          of  inl(a1)  =>
                                                                                                                          Y1[a1]
                                                                                                                          |  inr(a2)  =>
                                                                                                                          Y2[a2] 
                                                                                                                        es.e' 
                                                                                                                        e\mkleeneclose{};\mkleeneopen{}\mlambda{}x.(inr  x  )\mkleeneclose{};\mkleeneopen{}X2(e')\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  (HypSubst'  (-1)  0  THENA  Auto)
  THEN  RepUR  ``class-ap``  0
  THEN  Auto)

---

Home Index