---

Step * of Lemma pv11_p1_overlapping_accs

∀[accpts,as,bs,cs:bag(Id)].
  (↓∃i:Id. (i ↓∈ bs ∧ i ↓∈ cs)) supposing 
     (#([i∈accpts|¬bbag-deq-member(IdDeq;i;bs)]) < pv11_p1_threshold(accpts) and 
     #(as) < pv11_p1_threshold(accpts) and 
     (accpts = (as + cs) ∈ bag(Id)))
BY
{ (Auto
   THEN All (RepUR ``pv11_p1_threshold``)
   THEN (InstLemma `pv11_p1_about_threshold` [⌜Id⌝;⌜as⌝;⌜cs⌝]⋅ THENA Auto)
   THEN (InstLemma `bag-split` [⌜Id⌝;⌜λ2i.bag-deq-member(IdDeq;i;bs)⌝;⌜accpts⌝]⋅ THENA Auto)
   THEN (InstLemma `pv11_p1_about_threshold` [⌜Id⌝;⌜[x∈accpts|¬bbag-deq-member(IdDeq;x;bs)]⌝;
         ⌜[x∈accpts|bag-deq-member(IdDeq;x;bs)]⌝]⋅
         THENA (Auto
                THEN Try ((DoSubsume THEN Auto))
                THEN RWO "bag-append-comm" (-1)
                THEN Auto
                THEN DoSubsume
                THEN Auto)
         )
   THEN (InstLemma `bag-intersection` [⌜Id⌝;⌜cs⌝;⌜as⌝;⌜[x∈accpts|bag-deq-member(IdDeq;x;bs)]⌝;
         ⌜[x∈accpts|¬bbag-deq-member(IdDeq;x;bs)]⌝]⋅
         THENA (Auto
                THEN Try ((DoSubsume THEN Auto))
                THEN (RevHypSubst' (-2) 0 THENA Auto)
                THEN RWO "bag-append-comm" 0
                THEN Auto)
         )
   THEN SquashExRepD
   THEN D 0
   THEN InstConcl [⌜x⌝]⋅
   THEN Auto
   THEN BagMemberD (-1)
   THEN RepD
   THEN AllPushDown
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[accpts,as,bs,cs:bag(Id)].
    (\mdownarrow{}\mexists{}i:Id.  (i  \mdownarrow{}\mmember{}  bs  \mwedge{}  i  \mdownarrow{}\mmember{}  cs))  supposing 
          (\#([i\mmember{}accpts|\mneg{}\msubb{}bag-deq-member(IdDeq;i;bs)])  <  pv11\_p1\_threshold(accpts)  and 
          \#(as)  <  pv11\_p1\_threshold(accpts)  and 
          (accpts  =  (as  +  cs)))


By

---

Latex:
(Auto
  THEN  All  (RepUR  ``pv11\_p1\_threshold``)
  THEN  (InstLemma  `pv11\_p1\_about\_threshold`  [\mkleeneopen{}Id\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{};\mkleeneopen{}cs\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `bag-split`  [\mkleeneopen{}Id\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.bag-deq-member(IdDeq;i;bs)\mkleeneclose{};\mkleeneopen{}accpts\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `pv11\_p1\_about\_threshold`  [\mkleeneopen{}Id\mkleeneclose{};\mkleeneopen{}[x\mmember{}accpts|\mneg{}\msubb{}bag-deq-member(IdDeq;x;bs)]\mkleeneclose{};
              \mkleeneopen{}[x\mmember{}accpts|bag-deq-member(IdDeq;x;bs)]\mkleeneclose{}]\mcdot{}
              THENA  (Auto
                            THEN  Try  ((DoSubsume  THEN  Auto))
                            THEN  RWO  "bag-append-comm"  (-1)
                            THEN  Auto
                            THEN  DoSubsume
                            THEN  Auto)
              )
  THEN  (InstLemma  `bag-intersection`  [\mkleeneopen{}Id\mkleeneclose{};\mkleeneopen{}cs\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{};\mkleeneopen{}[x\mmember{}accpts|bag-deq-member(IdDeq;x;bs)]\mkleeneclose{};
              \mkleeneopen{}[x\mmember{}accpts|\mneg{}\msubb{}bag-deq-member(IdDeq;x;bs)]\mkleeneclose{}]\mcdot{}
              THENA  (Auto
                            THEN  Try  ((DoSubsume  THEN  Auto))
                            THEN  (RevHypSubst'  (-2)  0  THENA  Auto)
                            THEN  RWO  "bag-append-comm"  0
                            THEN  Auto)
              )
  THEN  SquashExRepD
  THEN  D  0
  THEN  InstConcl  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  BagMemberD  (-1)
  THEN  RepD
  THEN  AllPushDown
  THEN  Auto)

---

Home Index