{ 
[Info:Type]
es:EO+(Info). [A:Type]. X,Y:EClass(A). {[X?Y]} 
{X} 
{Y} }
{ Proof }
Definitions occuring in Statement :
es-interface-predicate: {I},
cond-class: [X?Y],
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-E: E,
uall: [x:A]. B[x],
all: x:A. B[x],
universe: Type,
predicate_equivalent: P1 P2,
predicate_or: P1 P2
Definitions :
predicate_equivalent: P1 P2,
es-interface-predicate: {I},
predicate_or: P1 P2
Lemmas :
es-interface-conditional-domain-iff
\mforall{}[Info:Type]. \mforall{}es:EO+(Info). \mforall{}[A:Type]. \mforall{}X,Y:EClass(A). \{[X?Y]\} \mLeftarrow{}{}\mRightarrow{} \{X\} \mvee{} \{Y\}
Date html generated:
2011_08_16-AM-11_42_56
Last ObjectModification:
2011_06_20-AM-00_33_35
Home
Index