parallel-df-halt(G;L;B;halt) ==
x:tuple-type(map(
dfp.(Top?);L))
((
(halt x))
(
S:
||L|| List. (strict-bag-function(G;L;B;S) 
(i
S.
isl(x.i)))))
Definitions occuring in Statement :
map: map(f;as),
length: ||as||,
isl: isl(x),
bnot: b,
assert: b,
int_seg: {i..j
},
top: Top,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
and: P Q,
unit: Unit,
apply: f a,
lambda: x.A[x],
union: left + right,
list: type List,
natural_number: $n,
l_all: (xL.P[x]),
strict-bag-function: strict-bag-function(G;L;B;S),
select-tuple: x.n,
tuple-type: tuple-type(L)
Definitions :
all: x:A. B[x],
tuple-type: tuple-type(L),
map: map(f;as),
lambda: x.A[x],
union: left + right,
top: Top,
unit: Unit,
implies: P Q,
apply: f a,
exists: x:A. B[x],
list: type List,
and: P Q,
strict-bag-function: strict-bag-function(G;L;B;S),
l_all: (xL.P[x]),
int_seg: {i..j},
natural_number: $n,
assert: b,
bnot: b,
isl: isl(x),
select-tuple: x.n,
length: ||as||
FDL editor aliases :
parallel-df-halt
parallel-df-halt(G;L;B;halt) ==
\mforall{}x:tuple-type(map(\mlambda{}dfp.(Top?);L))
((\muparrow{}(halt x)) {}\mRightarrow{} (\mexists{}S:\mBbbN{}||L|| List. (strict-bag-function(G;L;B;S) \mwedge{} (\mforall{}i\mmember{}S.\muparrow{}\mneg{}\msubb{}isl(x.i)))))
Date html generated:
2011_08_16-AM-09_37_25
Last ObjectModification:
2011_06_09-PM-03_57_56
Home
Index