---

Step * of Lemma lifting-bag-combine-decide

∀[a,F,G,f:Top].
  (⋃b∈case a of inl(x) => F[x] | inr(x) => G[x].f[b] ~ case a of inl(x) => ⋃b∈F[x].f[b] | inr(x) => ⋃b∈G[x].f[b])
BY
{ ((UnivCD THENA Auto)
   THEN InstLemma `lifting-strict-decide` 
   [⌜so_lambda(u,v,w,z.⋃b∈u.v[b])⌝;⌜f⌝;⌜⋅⌝;⌜⋅⌝;⌜a⌝;⌜F⌝;⌜G⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,F,G,f:Top].
    (\mcup{}b\mmember{}case  a  of  inl(x)  =>  F[x]  |  inr(x)  =>  G[x].f[b]  \msim{}  case  a
      of  inl(x)  =>
      \mcup{}b\mmember{}F[x].f[b]
      |  inr(x)  =>
      \mcup{}b\mmember{}G[x].f[b])


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  InstLemma  `lifting-strict-decide` 
  [\mkleeneopen{}so\_lambda(u,v,w,z.\mcup{}b\mmember{}u.v[b])\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index