Step
*
1
1
of Lemma
mem_diff
1. s : DSet
2. as : DisList{s}
3. bs : |s| List
4. c : |s|
5. (c #∈ as) ≤ 1
⊢ ((c #∈ as) -- (c #∈ bs)) > 0
⇐⇒ ((c #∈ as) > 0) ∧ (¬((c #∈ bs) > 0))
BY
{ TACTIC:(Unfold `ndiff` 0 THEN (RWO "imax_unfold" 0 THENA Auto) THEN AutoSplit THEN Auto') }
Latex:
Latex:
1. s : DSet
2. as : DisList\{s\}
3. bs : |s| List
4. c : |s|
5. (c \#\mmember{} as) \mleq{} 1
\mvdash{} ((c \#\mmember{} as) -- (c \#\mmember{} bs)) > 0 \mLeftarrow{}{}\mRightarrow{} ((c \#\mmember{} as) > 0) \mwedge{} (\mneg{}((c \#\mmember{} bs) > 0))
By
Latex:
TACTIC:(Unfold `ndiff` 0 THEN (RWO "imax\_unfold" 0 THENA Auto) THEN AutoSplit THEN Auto')
Home
Index