---

Step * 1 1 1 of Lemma empty-bag-union


1. [] ∈ Top List
⊢ ∀bs:Top List List. ((reduce(λl,l'. (l @ l');[];bs) = [] ∈ (Top List)) ⇒ (bs ~ primrec(||bs||;[];λi,r. [[] / r])))
BY
{ (InductionOnList
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN Reduce 0
   THEN AutoSplit
   THEN Auto'
   THEN (RWO "append_is_nil" (-1)
         THEN Auto
         THEN Try (((Subst' (||v|| + 1) - 1 ~ ||v|| 0 THEN Auto) THEN BackThruSomeHyp))⋅
         THEN DVar `u'
         THEN Auto)⋅)⋅ }

---

Latex:

---

Latex:

1.  []  \mmember{}  Top  List
\mvdash{}  \mforall{}bs:Top  List  List.  ((reduce(\mlambda{}l,l'.  (l  @  l');[];bs)  =  [])  {}\mRightarrow{}  (bs  \msim{}  primrec(||bs||;[];\mlambda{}i,r.  [[]  /  r]\000C)))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  Auto'
  THEN  (RWO  "append\_is\_nil"  (-1)
              THEN  Auto
              THEN  Try  (((Subst'  (||v||  +  1)  -  1  \msim{}  ||v||  0  THEN  Auto)  THEN  BackThruSomeHyp))\mcdot{}
              THEN  DVar  `u'
              THEN  Auto)\mcdot{})\mcdot{}

---

Home Index