Nuprl Definition : find-hull
find-hull(g;xs) ==
let L ⟵ [2, ||xs||)
in eager-accum(hs,k.let p,q = find_transitions(λx,y. k L xy;hs)
in if isl(p) ∧b isl(q)
then hs
else eval x = outr(p) in
eval y = outr(q) in
if x <z y
then let as ⟵ firstn(x + 1;hs)
in let bs ⟵ nth_tl(y;hs)
in as @ [k / bs]
else let as ⟵ firstn((x - y) + 1;nth_tl(y;hs))
in [k / as]
fi
fi ;[0; 1];L)
Definitions occuring in Statement :
left-test: i L jk
,
from-upto: [n, m)
,
eager-accum: eager-accum(x,a.f[x; a];y;l)
,
find_transitions: find_transitions(f;L)
,
firstn: firstn(n;as)
,
length: ||as||
,
nth_tl: nth_tl(n;as)
,
append: as @ bs
,
cons: [a / b]
,
nil: []
,
band: p ∧b q
,
callbyvalueall: callbyvalueall,
callbyvalue: callbyvalue,
outr: outr(x)
,
ifthenelse: if b then t else f fi
,
isl: isl(x)
,
lt_int: i <z j
,
lambda: λx.A[x]
,
spread: spread def,
subtract: n - m
,
add: n + m
,
natural_number: $n
Definitions occuring in definition :
from-upto: [n, m)
,
length: ||as||
,
eager-accum: eager-accum(x,a.f[x; a];y;l)
,
spread: spread def,
find_transitions: find_transitions(f;L)
,
lambda: λx.A[x]
,
left-test: i L jk
,
band: p ∧b q
,
isl: isl(x)
,
callbyvalue: callbyvalue,
outr: outr(x)
,
ifthenelse: if b then t else f fi
,
lt_int: i <z j
,
append: as @ bs
,
callbyvalueall: callbyvalueall,
firstn: firstn(n;as)
,
add: n + m
,
subtract: n - m
,
nth_tl: nth_tl(n;as)
,
cons: [a / b]
,
natural_number: $n
,
nil: []
FDL editor aliases :
find-hull
Latex:
find-hull(g;xs) ==
let L \mleftarrow{}{} [2, ||xs||)
in eager-accum(hs,k.let p,q = find\_transitions(\mlambda{}x,y. k L xy;hs)
in if isl(p) \mwedge{}\msubb{} isl(q)
then hs
else eval x = outr(p) in
eval y = outr(q) in
if x <z y
then let as \mleftarrow{}{} firstn(x + 1;hs)
in let bs \mleftarrow{}{} nth\_tl(y;hs)
in as @ [k / bs]
else let as \mleftarrow{}{} firstn((x - y) + 1;nth\_tl(y;hs))
in [k / as]
fi
fi ;[0; 1];L)
Date html generated:
2017_10_02-PM-06_52_13
Last ObjectModification:
2017_08_06-PM-07_31_53
Theory : euclidean!plane!geometry
Home
Index