Nuprl Lemma : rec-bind-df-program_wf
[Info,A,B:Type].
[dfpX,dfpY:A 
DataflowProgram(Info)].
((a:A. (df-program-type(dfpX a) 
r B))
(a:A. (df-program-type(dfpY a) r A))
rec-bind-df-program(A;B;dfpX;dfpY) 
A DataflowProgram(Info)
supposing a,a':A. s:df-program-statetype(dfpY a). m:Info.
(a' 
snd((df-program-transition(dfpY a) s m))
(
bag-null(snd((df-program-transition(dfpY a') (fst(snd(snd((dfpY a'))))) m))))))
supposing valueall-type(A) 
valueall-type(B) (Info)
Proof not projected
Definitions occuring in Statement :
rec-bind-df-program: rec-bind-df-program(A;B;dfpX;dfpY),
df-program-transition: df-program-transition(dfp),
df-program-statetype: df-program-statetype(dfp),
df-program-type: df-program-type(dfp),
dataflow-program: DataflowProgram(A),
subtype_rel: A r B,
assert: b,
uimplies: b supposing a,
uall: [x:A]. B[x],
pi1: fst(t),
pi2: snd(t),
all: x:A. B[x],
squash: T,
implies: P Q,
and: P Q,
member: t T,
apply: f a,
function: x:A B[x],
universe: Type,
bag-member: x bs,
bag-null: bag-null(bs),
valueall-type: valueall-type(T)
Definitions :
df-program-transition: df-program-transition(dfp),
df-program-type: df-program-type(dfp),
vatype: ValueAllType,
subtype: S T,
suptype: suptype(S; T),
rec-bind-df-init: rec-bind-df-init(ix;iy),
squash: T,
rec-bind-df-statetype: rec-bind-df-statetype(A;Sx;Sy),
uall: [x:A]. B[x],
unit: Unit,
uimplies: b supposing a,
type-monotone: Monotone(T.F[T]),
true: True,
dataflow-program: DataflowProgram(A),
all: x:A. B[x],
df-program-statetype: df-program-statetype(dfp),
implies: P Q,
pi2: snd(t),
pi1: fst(t),
member: t T,
rec-bind-df-program: rec-bind-df-program(A;B;dfpX;dfpY),
let: let,
prop: 
,
so_lambda: 
x.t[x],
top: Top,
sq_stable: SqStable(P),
and: P Q,
so_apply: x[s],
guard: {T}
Lemmas :
top_wf,
subtype_top,
assert-bag-null-sq,
rec-bind-df-trans_wf,
df-program-statetype-valueall-type,
empty-bag_wf,
rec-bind-df-statetype_wf,
rec-valueall-type,
subtype_rel_product,
subtype_rel_simple_product,
subtype_rel_sum,
product-valueall-type,
union-valueall-type,
sq_stable__valueall-type,
equal-valueall-type,
bag-valueall-type,
valueall-type_wf,
unit_wf2,
bag_wf,
all_wf,
df-program-statetype_wf,
bag-member_wf,
df-program-transition_wf,
pi2_wf,
df-program-type_wf,
subtype_rel_bag,
assert_wf,
bag-null_wf,
pi1_wf_top,
dataflow-program_wf,
subtype_rel_wf,
and_wf,
squash_wf
\mforall{}[Info,A,B:Type].
\mforall{}[dfpX,dfpY:A {}\mrightarrow{} DataflowProgram(Info)].
((\mforall{}a:A. (df-program-type(dfpX a) \msubseteq{}r B))
{}\mRightarrow{} (\mforall{}a:A. (df-program-type(dfpY a) \msubseteq{}r A))
{}\mRightarrow{} rec-bind-df-program(A;B;dfpX;dfpY) \mmember{} A {}\mrightarrow{} DataflowProgram(Info)
supposing \mforall{}a,a':A. \mforall{}s:df-program-statetype(dfpY a). \mforall{}m:Info.
(a' \mdownarrow{}\mmember{} snd((df-program-transition(dfpY a) s m))
{}\mRightarrow{} (\muparrow{}bag-null(snd((df-program-transition(dfpY a') (fst(snd(snd((dfpY a')))))
m))))))
supposing valueall-type(A) \mwedge{} valueall-type(B) \mwedge{} (\mdownarrow{}Info)
Date html generated:
2012_02_20-PM-02_43_35
Last ObjectModification:
2012_02_14-PM-12_31_58
Home
Index