Nuprl Lemma : rec-bind-df-trans_wf
[M:Type]. [B,A:ValueAllType]. [Sx,Sy:A 
ValueAllType]. [Xinit:a:A (Sx a)]. [Yinit:a:A (Sy a)].
[Xnxt:a:A Sx a M (Sx a? 
bag(B))]. [Ynxt:a:A Sy a M (Sy a? bag(A))].
((a:A. sy:Sy a. m:M. a':A. (a' 
snd((Ynxt a sy m)) 
((snd((Ynxt a' (Yinit a') m))) = {})))
(rec-bind-df-trans(Xinit;Yinit;Xnxt;Ynxt) rec-bind-df-statetype(A;Sx;Sy)
M
(rec-bind-df-statetype(A;Sx;Sy)? bag(B))))
Proof not projected
Definitions occuring in Statement :
rec-bind-df-trans: rec-bind-df-trans(Xinit;Yinit;Xnxt;Ynxt),
rec-bind-df-statetype: rec-bind-df-statetype(A;Sx;Sy),
uall: [x:A]. B[x],
pi2: snd(t),
all: x:A. B[x],
implies: P Q,
unit: Unit,
member: t T,
apply: f a,
function: x:A B[x],
product: x:A B[x],
union: left + right,
universe: Type,
equal: s = t,
bag-member: x bs,
empty-bag: {},
bag: bag(T),
vatype: ValueAllType
Definitions :
rev_implies: P 
Q,
iff: P Q,
outr: outr(x),
assert: 
b,
bag-combine: 
xbs.f[x],
bag-union: bag-union(bbs),
concat: concat(ll),
exposed-bfalse: exposed-bfalse,
it: 
,
exists: 
x:A. B[x],
evalall: evalall(t),
pi2: snd(t),
null: null(as),
empty-bag: {},
bag-mapfilter: bag-mapfilter(f;P;bs),
map: map(f;as),
bag-filter: [xb|p[x]],
bag-map: bag-map(f;bs),
filter: filter(P;l),
reduce: reduce(f;k;as),
pi1: fst(t),
rec-bind-df-init: rec-bind-df-init(ix;iy),
band: p 
q,
compose: f o g,
top: Top,
bnot: 
b,
uiff: uiff(P;Q),
and: P Q,
let: let,
guard: {T},
uall: [x:A]. B[x],
vatype: ValueAllType,
unit: Unit,
implies: P Q,
all: x:A. B[x],
member: t T,
rec-bind-df-statetype: rec-bind-df-statetype(A;Sx;Sy),
rec-bind-df-trans: rec-bind-df-trans(Xinit;Yinit;Xnxt;Ynxt),
uimplies: b supposing a,
type-monotone: Monotone(T.F[T]),
so_lambda: 
x.t[x],
squash: T,
true: True,
ycomb: Y,
spreadn: spread3,
ifthenelse: if b then t else f fi ,
isl: isl(x),
outl: outl(x),
btrue: tt,
bfalse: ff,
has-valueall: has-valueall(a),
subtype: S 
T,
suptype: suptype(S; T),
prop: 
,
bool: 
,
bag: bag(T),
sq_type: SQType(T),
rev_uimplies: rev_uimplies(P;Q),
le: A 
B,
nat: 
,
not: A,
false: False,
decidable: Dec(P),
or: P 
Q,
so_apply: x[s],
sq_stable: SqStable(P)
Lemmas :
squash_wf,
implies_functionality_wrt_iff,
iff_weakening_uiff,
outr_wf,
false_wf,
true_wf,
bag-combine_wf,
null_wf3,
bag-subtype-list,
eqtt_to_assert,
uiff_transitivity,
not_wf,
eqff_to_assert,
assert_of_bnot,
bag-mapfilter_wf,
top_wf,
outl_wf,
permutation_wf,
list-subtype-bag,
isect-valueall-type,
int-valueall-type,
list-valueall-type,
void-valueall-type,
pair-eta,
bag-map-map,
bag-subtype,
band_ff_simp,
subtype_base_sq,
bool_wf,
bool_subtype_base,
empty-bag-iff-size,
decidable__le,
bag-size_wf,
void_wf,
nat_wf,
bag-member-iff-size,
sq_stable_from_decidable,
le_wf,
bag-map_wf,
rec-bind-df-init_wf,
decidable__assert,
bag-null_wf,
assert-bag-null,
equal-empty-bag,
not_functionality_wrt_uiff,
assert_wf,
rec-valueall-type,
valueall-type_wf,
unit_wf2,
bag_wf,
subtype_rel_product,
subtype_rel_simple_product,
subtype_rel_sum,
subtype_rel_bag,
product-valueall-type,
sq_stable__valueall-type,
union-valueall-type,
equal-valueall-type,
bag-valueall-type,
ifthenelse_wf,
band_wf,
bnot_wf,
isl_wf,
it_wf,
empty-bag_wf,
evalall_wf,
rec-bind-df-statetype_wf,
pi1_wf_top,
pi2_wf,
bag-append_wf,
all_wf,
bag-member_wf,
equal_wf
\mforall{}[M:Type]. \mforall{}[B,A:ValueAllType]. \mforall{}[Sx,Sy:A {}\mrightarrow{} ValueAllType]. \mforall{}[Xinit:a:A {}\mrightarrow{} (Sx a)].
\mforall{}[Yinit:a:A {}\mrightarrow{} (Sy a)]. \mforall{}[Xnxt:a:A {}\mrightarrow{} Sx a {}\mrightarrow{} M {}\mrightarrow{} (Sx a? \mtimes{} bag(B))]. \mforall{}[Ynxt:a:A
{}\mrightarrow{} Sy a
{}\mrightarrow{} M
{}\mrightarrow{} (Sy a? \mtimes{} bag(A))].
((\mforall{}a:A. \mforall{}sy:Sy a. \mforall{}m:M. \mforall{}a':A.
(a' \mdownarrow{}\mmember{} snd((Ynxt a sy m)) {}\mRightarrow{} ((snd((Ynxt a' (Yinit a') m))) = \{\})))
{}\mRightarrow{} (rec-bind-df-trans(Xinit;Yinit;Xnxt;Ynxt) \mmember{} rec-bind-df-statetype(A;Sx;Sy)
{}\mrightarrow{} M
{}\mrightarrow{} (rec-bind-df-statetype(A;Sx;Sy)? \mtimes{} bag(B))))
Date html generated:
2012_02_20-PM-02_43_26
Last ObjectModification:
2012_02_14-PM-02_54_44
Home
Index