Nuprl Lemma : rec-op-bind-class_wf
[Info,A,B:Type]. [X:A 
EClass(B)]. [Y:A EClass(A)]. [F:A bag(B) bag(B)].
rec-op-bind-class(X;Y;F) 
A EClass(B)
supposing x,a:A. es:EO+(Info). e:E. (a Y x(e) 
(w:A. (
w Y a(e))))
Proof not projected
Definitions occuring in Statement :
rec-op-bind-class: rec-op-bind-class(X;Y;F),
classrel: v X(e),
eclass: EClass(A[eo; e]),
eo-forward: eo.e,
event-ordering+: EO+(Info),
es-E: E,
uimplies: b supposing a,
uall: [x:A]. B[x],
all: x:A. B[x],
not: A,
implies: P Q,
member: t T,
apply: f a,
function: x:A B[x],
universe: Type,
bag: bag(T)
Definitions :
all: x:A. B[x],
implies: P Q,
member: t T,
prop: 
,
so_lambda: 
x.t[x],
es-le: e 
loc e' ,
or: P 
Q,
guard: {T},
so_lambda: x y.t[x; y],
exists: 
x:A. B[x],
not: A,
ge: i 
j ,
le: A B,
false: False,
uimplies: b supposing a,
nat: 
,
rec-op-bind-class: rec-op-bind-class(X;Y;F),
ycomb: Y,
parallel-class: X || Y,
mbind-class: X >>= Y,
eclass-compose2: eclass-compose2(f;X;Y),
bind-class: X >x> Y[x],
subtype: S 
T,
top: Top,
and: P 
Q,
cand: A c B,
rev_implies: P 
Q,
iff: P Q,
assert: 
b,
btrue: tt,
ifthenelse: if b then t else f fi ,
true: True,
squash: 
T,
label: ...$L... t,
eclass: EClass(A[eo; e]),
uall: [x:A]. B[x],
so_apply: x[s],
so_apply: x[s1;s2],
sq_type: SQType(T),
uiff: uiff(P;Q),
es-locl: (e <loc e'),
rev_uimplies: rev_uimplies(P;Q),
classrel: v X(e)
Lemmas :
all_wf,
event-ordering+_wf,
es-E_wf,
event-ordering+_inc,
classrel_wf,
not_wf,
eo-forward_wf,
member-eo-forward-E,
es-locl_wf,
equal_wf,
Id_wf,
es-loc_wf,
es-le_wf,
bag_wf,
eclass_wf,
length_wf_nat,
es-interval_wf,
es-init_wf,
length_wf,
less_than_wf,
nat_wf,
nat_properties,
ge_wf,
le_wf,
bag-append_wf,
bag-combine-member-wf,
bag-member-list,
decidable__es-E-equal,
es-le-before_wf2,
member-es-le-before,
es-le-before_wf,
list-subtype-bag,
bag-member_wf,
eo-forward-E-member,
es-le-loc,
eo-forward-loc,
eo-forward-E-subtype,
non_neg_length,
subtype_base_sq,
int_subtype_base,
es-interval-partition,
eo-forward-le,
es-locl-trichotomy,
es-first-init,
bool_wf,
bool_subtype_base,
btrue_neq_bfalse,
assert-es-first,
es-causl_weakening,
es-loc-init,
btrue_wf,
es-locl-first,
assert_elim,
es-first_wf,
and_wf,
squash_wf,
true_wf,
length_append,
es-pred_wf,
es-locl-iff,
es-interval-non-zero,
es-loc-pred,
es-pred-locl,
es-le_weakening,
equal-eo-forward-E,
event_ordering_wf,
eo-forward-forward,
es-init-forward,
eo-forward-interval,
top_wf
\mforall{}[Info,A,B:Type]. \mforall{}[X:A {}\mrightarrow{} EClass(B)]. \mforall{}[Y:A {}\mrightarrow{} EClass(A)]. \mforall{}[F:A {}\mrightarrow{} bag(B) {}\mrightarrow{} bag(B)].
rec-op-bind-class(X;Y;F) \mmember{} A {}\mrightarrow{} EClass(B)
supposing \mforall{}x,a:A. \mforall{}es:EO+(Info). \mforall{}e:E. (a \mmember{} Y x(e) {}\mRightarrow{} (\mforall{}w:A. (\mneg{}w \mmember{} Y a(e))))
Date html generated:
2012_02_20-PM-02_49_03
Last ObjectModification:
2012_02_03-PM-02_42_16
Home
Index