---

Step * 2 of Lemma bag-separate-merge


1. as : Top List
2. bs : Top List
⊢ map(λt.outr(t);filter(λx.(¬bisl(x));map(λx.(inl x);as))) @ map(λt.outr(t);filter(λx.(¬bisl(x));map(λx.(inr x );bs))) 
~ bs
BY
{ (Subst ⌜map(λt.outr(t);filter(λx.(¬bisl(x));map(λx.(inl x);as))) ~ []⌝ 0⋅
   THEN Reduce 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.outr(t);filter(\mlambda{}x.(\mneg{}\msubb{}isl(x));map(\mlambda{}x.(inl  x);as)))
@  map(\mlambda{}t.outr(t);filter(\mlambda{}x.(\mneg{}\msubb{}isl(x));map(\mlambda{}x.(inr  x  );bs)))  \msim{}  bs


By

---

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

---

Home Index