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