Nuprl Lemma : equals-null-dataflow
M,B,S:Type. F:S 
M (S? 
bag(B)). y:Unit.
(null-dataflow() = rec-dataflow(inr y ;s,a.case s of inl(s1) => F s1 a | inr(x) => <s, {}>))
Proof not projected
Definitions occuring in Statement :
null-dataflow: null-dataflow(),
rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),
dataflow: dataflow(A;B),
all: x:A. B[x],
unit: Unit,
apply: f a,
function: x:A B[x],
pair: <a, b>,
product: x:A B[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inr: inr x ,
union: left + right,
universe: Type,
equal: s = t,
empty-bag: {},
bag: bag(T)
Definitions :
all: x:A. B[x],
member: t 
T,
so_lambda: 
x y.t[x; y],
uall: [x:A]. B[x],
uimplies: b supposing a,
so_apply: x[s1;s2]
Lemmas :
dataflow-extensionality,
bag_wf,
null-dataflow_wf,
rec-dataflow_wf,
empty-bag_wf,
unit_wf2
\mforall{}M,B,S:Type. \mforall{}F:S {}\mrightarrow{} M {}\mrightarrow{} (S? \mtimes{} bag(B)). \mforall{}y:Unit.
(null-dataflow() = rec-dataflow(inr y ;s,a.case s of inl(s1) => F s1 a | inr(x) => <s, \{\}>))
Date html generated:
2012_01_23-AM-11_57_14
Last ObjectModification:
2011_12_21-PM-12_39_03
Home
Index