input-codeable(lp.M[lp];n;T) ==
code:T 
process-input'(lp.M[lp];n)
decode:process-input'(lp.M[lp];n) (T + Top)
input-code(lp.M[lp];n;T;code;decode)
Definitions :
exists: x:A. B[x],
function: x:A B[x],
process-input': process-input'(lp.M[lp];n),
union: left + right,
top: Top,
input-code: input-code(lp.M[lp];n;T;code;decode)
FDL editor aliases :
input-codeable
input-codeable(lp.M[lp];n;T) ==
\mexists{}code:T {}\mrightarrow{} process-input'(lp.M[lp];n)
\mexists{}decode:process-input'(lp.M[lp];n) {}\mrightarrow{} (T + Top). input-code(lp.M[lp];n;T;code;decode)
Date html generated:
2010_08_27-PM-08_36_09
Last ObjectModification:
2010_02_02-PM-05_48_54
Home
Index