ext-codeable(lp.M[lp];n;T) ==
code:T + Top 
((Id 
process-input'(lp.M[lp];n)) List)
decode:(Id process-input'(lp.M[lp];n)) List (T + Top)
((
v:T + Top. ((decode (code v)) = v)) 
((decode []) = (inr 
)))
Definitions :
exists: x:A. B[x],
function: x:A B[x],
list: type List,
product: x:A B[x],
Id: Id,
process-input': process-input'(lp.M[lp];n),
and: P Q,
all: x:A. B[x],
equal: s = t,
union: left + right,
top: Top,
apply: f a,
nil: [],
inr: inr x ,
it:
FDL editor aliases :
ext-codeable
ext-codeable(lp.M[lp];n;T) ==
\mexists{}code:T + Top {}\mrightarrow{} ((Id \mtimes{} process-input'(lp.M[lp];n)) List)
\mexists{}decode:(Id \mtimes{} process-input'(lp.M[lp];n)) List {}\mrightarrow{} (T + Top)
((\mforall{}v:T + Top. ((decode (code v)) = v)) \mwedge{} ((decode []) = (inr \mcdot{} )))
Date html generated:
2010_08_27-PM-08_36_13
Last ObjectModification:
2010_02_02-PM-05_30_07
Home
Index