CombinatorDef ==
n:
m:{m:| 0 < (n + m)}
rec:
wf:{L:Type List| ||L|| = (n + m)} 
'
T:{L:Type List| (||L|| = (n + m)) 
(wf L)} Type
(
L:{L:Type List| (||L|| = (n + m)) (wf L)}
{f:k:||L|| bag(L[k]) if rec
then bag(T L) bag(T L)
else bag(T L)
fi |
if rec then (f (
k.{}) {}) = {} else (f (k.{})) = {} fi } )
Definitions occuring in Statement :
select: l[i],
length: ||as||,
ifthenelse: if b then t else f fi ,
bool: ,
int_seg: {i..j
},
nat: ,
prop: ,
and: P Q,
less_than: a < b,
set: {x:A| B[x]} ,
apply: f a,
lambda: x.A[x],
isect: x:A. B[x],
function: x:A B[x],
product: x:A B[x],
list: type List,
add: n + m,
natural_number: $n,
int: 
,
universe: Type,
equal: s = t,
empty-bag: {},
bag: bag(T)
Definitions :
nat: ,
less_than: a < b,
bool: ,
prop: ,
product: x:A B[x],
isect: x:A. B[x],
list: type List,
universe: Type,
and: P Q,
int: ,
add: n + m,
set: {x:A| B[x]} ,
int_seg: {i..j},
natural_number: $n,
length: ||as||,
select: l[i],
function: x:A B[x],
ifthenelse: if b then t else f fi ,
equal: s = t,
bag: bag(T),
apply: f a,
lambda: x.A[x],
empty-bag: {}
FDL editor aliases :
combinator-def
CombinatorDef ==
n:\mBbbN{}
\mtimes{} m:\{m:\mBbbN{}| 0 < (n + m)\}
\mtimes{} rec:\mBbbB{}
\mtimes{} wf:\{L:Type List| ||L|| = (n + m)\} {}\mrightarrow{} \mBbbP{}'
\mtimes{} T:\{L:Type List| (||L|| = (n + m)) \mwedge{} (wf L)\} {}\mrightarrow{} Type
\mtimes{} (\mcap{}L:\{L:Type List| (||L|| = (n + m)) \mwedge{} (wf L)\}
\{f:k:\mBbbN{}||L|| {}\mrightarrow{} bag(L[k]) {}\mrightarrow{} if rec then bag(T L) {}\mrightarrow{} bag(T L) else bag(T L) fi |
if rec then (f (\mlambda{}k.\{\}) \{\}) = \{\} else (f (\mlambda{}k.\{\})) = \{\} fi \} )
Date html generated:
2011_08_17-PM-04_29_35
Last ObjectModification:
2011_01_19-PM-09_13_23
Home
Index