feedback-df-halt(G;L;B;halt) ==
x:tuple-type(map(
dfp.(Top?);L))
((
(halt x))
(
S:
||L|| List
((buf:bag(B). strict-bag-function(x.(G x buf);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),
bag: bag(T),
select-tuple: x.n,
tuple-type: tuple-type(L)
Definitions :
tuple-type: tuple-type(L),
map: map(f;as),
union: left + right,
top: Top,
unit: Unit,
implies: P Q,
exists: x:A. B[x],
list: type List,
and: P Q,
all: x:A. B[x],
bag: bag(T),
strict-bag-function: strict-bag-function(G;L;B;S),
lambda: x.A[x],
apply: f a,
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 :
feedback-df-halt
feedback-df-halt(G;L;B;halt) ==
\mforall{}x:tuple-type(map(\mlambda{}dfp.(Top?);L))
((\muparrow{}(halt x))
{}\mRightarrow{} (\mexists{}S:\mBbbN{}||L|| List
((\mforall{}buf:bag(B). strict-bag-function(\mlambda{}x.(G x buf);L;B;S)) \mwedge{} (\mforall{}i\mmember{}S.\muparrow{}\mneg{}\msubb{}isl(x.i)))))
Date html generated:
2011_08_16-AM-09_40_51
Last ObjectModification:
2011_06_09-PM-05_29_55
Home
Index