Nuprl Lemma : class-opt-class-classrel2
[Info,T:Type]. [X,Y:EClass(T)]. [v:T]. [es:EO+(Info)]. [e:E].
uiff(v 
X?Y(e);((
bag-null(X es e)) 
v Y(e)) 
((
bag-null(X es e)) v X(e)))
Proof not projected
Definitions occuring in Statement :
class-opt-class: X?Y,
classrel: v X(e),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-E: E,
assert: b,
uiff: uiff(P;Q),
uall: [x:A]. B[x],
not: A,
implies: P Q,
and: P Q,
apply: f a,
universe: Type,
bag-null: bag-null(bs)
Definitions :
uall: [x:A]. B[x],
eclass: EClass(A[eo; e]),
uiff: uiff(P;Q),
classrel: v X(e),
and: P Q,
implies: P Q,
member: t T,
uimplies: b supposing a,
prop: 
,
bag-member: x 
bs,
squash: T,
true: True,
so_lambda: 
x y.t[x; y],
guard: {T},
not: A,
class-opt-class: X?Y,
ifthenelse: if b then t else f fi ,
all: x:A. B[x],
btrue: tt,
bfalse: ff,
so_apply: x[s1;s2],
or: P 
Q,
sq_type: SQType(T),
false: False,
bool: 
,
unit: Unit,
subtype: S 
T,
it: 
Lemmas :
assert_wf,
bag-null_wf,
not_wf,
classrel_wf,
class-opt-class_wf,
and_wf,
es-E_wf,
event-ordering+_inc,
event-ordering+_wf,
eclass_wf,
bool_cases,
subtype_base_sq,
bool_wf,
bool_subtype_base,
uiff_transitivity,
equal_wf,
bag_wf,
empty-bag_wf,
eqtt_to_assert,
assert-bag-null,
bnot_wf,
eqff_to_assert,
assert_of_bnot,
not_functionality_wrt_uiff
\mforall{}[Info,T:Type]. \mforall{}[X,Y:EClass(T)]. \mforall{}[v:T]. \mforall{}[es:EO+(Info)]. \mforall{}[e:E].
uiff(v \mmember{} X?Y(e);((\muparrow{}bag-null(X es e)) {}\mRightarrow{} v \mmember{} Y(e)) \mwedge{} ((\mneg{}\muparrow{}bag-null(X es e)) {}\mRightarrow{} v \mmember{} X(e)))
Date html generated:
2012_01_23-PM-12_54_59
Last ObjectModification:
2011_12_30-PM-02_40_43
Home
Index