---

Step * 1 of Lemma bag-separate-merge


1. as : Top List
2. bs : Top List
⊢ map(λt.outl(t);filter(λx.isl(x);map(λx.(inl x);as))) @ map(λt.outl(t);filter(λx.isl(x);map(λx.(inr x );bs))) ~ as
BY
{ (Subst ⌜map(λt.outl(t);filter(λx.isl(x);map(λx.(inr x );bs))) ~ []⌝ 0⋅
   THEN All Thin
   THEN ListInd 1
   THEN Reduce 0
   THEN Try (EqCD)
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  as  :  Top  List
2.  bs  :  Top  List
\mvdash{}  map(\mlambda{}t.outl(t);filter(\mlambda{}x.isl(x);map(\mlambda{}x.(inl  x);as)))
@  map(\mlambda{}t.outl(t);filter(\mlambda{}x.isl(x);map(\mlambda{}x.(inr  x  );bs)))  \msim{}  as


By

---

Latex:
(Subst  \mkleeneopen{}map(\mlambda{}t.outl(t);filter(\mlambda{}x.isl(x);map(\mlambda{}x.(inr  x  );bs)))  \msim{}  []\mkleeneclose{}  0\mcdot{}
  THEN  All  Thin
  THEN  ListInd  1
  THEN  Reduce  0
  THEN  Try  (EqCD)
  THEN  Auto)\mcdot{}

---

Home Index