Step
*
1
2
1
of Lemma
sdata-pair-free-from-atom
1. b : Atom1
2. d1 : SecurityData
3. d2 : SecurityData
⊢ Ax ∈ ∩:b#d1:SecurityData ∧ b#d2:SecurityData. b#<d1, d2>:SecurityData
BY
{ (Assert ⌈Ax ∈ ∩%:b#d1:SecurityData ∧ b#d2:SecurityData. b#<d1, d2>:SecurityData⌉⋅
THEN Try (Trivial)
THEN At ⌈Type⌉ (ISectMemTypeCD THEN Auto)⋅)⋅ }
1
1. b : Atom1
2. d1 : SecurityData
3. d2 : SecurityData
4. b#d1:SecurityData
5. b#d2:SecurityData
⊢ Ax ∈ b#<d1, d2>:SecurityData
Latex:
Latex:
1. b : Atom1
2. d1 : SecurityData
3. d2 : SecurityData
\mvdash{} Ax \mmember{} \mcap{}:b\#d1:SecurityData \mwedge{} b\#d2:SecurityData. b\#<d1, d2>:SecurityData
By
Latex:
(Assert \mkleeneopen{}Ax \mmember{} \mcap{}\%:b\#d1:SecurityData \mwedge{} b\#d2:SecurityData. b\#<d1, d2>:SecurityData\mkleeneclose{}\mcdot{}
THEN Try (Trivial)
THEN At \mkleeneopen{}Type\mkleeneclose{} (ISectMemTypeCD THEN Auto)\mcdot{})\mcdot{}
Home
Index