Step
*
2
1
1
2
1
of Lemma
sub-bag-iff
1. [T] : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. num : T ⟶ ℕ
5. ∀x:T. ((num x) ≤ (#x in bs))
⊢ ∃B:bag(T). ∀x:T. ((#x in B) = (num x) ∈ ℤ)
BY
{ (Assert ∀x:T. ∀n:ℕ. (repn(n;x) ∈ bag(T)) BY
(Auto THEN SubsumeC ⌜T List⌝⋅ THEN Auto THEN (DoSubsume THEN Auto)⋅ THEN SubtypeReasoning THEN Auto)) }
1
1. [T] : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. num : T ⟶ ℕ
5. ∀x:T. ((num x) ≤ (#x in bs))
6. ∀x:T. ∀n:ℕ. (repn(n;x) ∈ bag(T))
⊢ ∃B:bag(T). ∀x:T. ((#x in B) = (num x) ∈ ℤ)
Latex:
Latex:
1. [T] : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. num : T {}\mrightarrow{} \mBbbN{}
5. \mforall{}x:T. ((num x) \mleq{} (\#x in bs))
\mvdash{} \mexists{}B:bag(T). \mforall{}x:T. ((\#x in B) = (num x))
By
Latex:
(Assert \mforall{}x:T. \mforall{}n:\mBbbN{}. (repn(n;x) \mmember{} bag(T)) BY
(Auto
THEN SubsumeC \mkleeneopen{}T List\mkleeneclose{}\mcdot{}
THEN Auto
THEN (DoSubsume THEN Auto)\mcdot{}
THEN SubtypeReasoning
THEN Auto))
Home
Index