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