Step
*
of Lemma
bag-diff-equal-inl
∀[T:Type]
∀eq:EqDecider(T). ∀as,bs:bag(T).
∀[cs:bag(T)]. uiff(bag-diff(eq;bs;as) = (inl cs) ∈ (bag(T)?);bs = (as + cs) ∈ bag(T))
BY
{ xxx((InstLemma `bag-diff-property` []⋅ THEN RepeatFor 4 (ParallelLast'))
THEN MoveToConcl (-1)
THEN GenConclAtAddr [1;1]
THEN D -2
THEN Reduce 0
THEN Auto)xxx }
1
.....subterm..... T:t
1:n
1. T : Type
2. eq : EqDecider(T)
3. as : bag(T)
4. bs : bag(T)
5. x : bag(T)
6. bag-diff(eq;bs;as) = (inl x) ∈ (bag(T)?)
7. bs = (as + x) ∈ bag(T)
8. cs : bag(T)
9. bs = (as + cs) ∈ bag(T)
⊢ x = cs ∈ bag(T)
2
1. T : Type
2. eq : EqDecider(T)
3. as : bag(T)
4. bs : bag(T)
5. y : Unit
6. bag-diff(eq;bs;as) = (inr y ) ∈ (bag(T)?)
7. ∀cs:bag(T). (¬(bs = (as + cs) ∈ bag(T)))
8. cs : bag(T)
9. bs = (as + cs) ∈ bag(T)
⊢ (inr y ) = (inl cs) ∈ (bag(T)?)
Latex:
Latex:
\mforall{}[T:Type]
\mforall{}eq:EqDecider(T). \mforall{}as,bs:bag(T). \mforall{}[cs:bag(T)]. uiff(bag-diff(eq;bs;as) = (inl cs);bs = (as + cs))
By
Latex:
xxx((InstLemma `bag-diff-property` []\mcdot{} THEN RepeatFor 4 (ParallelLast'))
THEN MoveToConcl (-1)
THEN GenConclAtAddr [1;1]
THEN D -2
THEN Reduce 0
THEN Auto)xxx
Home
Index