spec Boolean =
sort
  Boolean
ops
  False : Boolean;
  Not__ : Boolean->Boolean;
  True : Boolean;
  __And__ : Boolean*Boolean->Boolean;
  __Or__ : Boolean*Boolean->Boolean

end

spec Char =
sorts
  Char;
  Pos < Nat;
  Pos
ops
  ' ' : Char;
  '!' : Char;
  '#' : Char;
  '$' : Char;
  '%' : Char;
  '&' : Char;
  '(' : Char;
  ')' : Char;
  '*' : Char;
  '+' : Char;
  ',' : Char;
  '-' : Char;
  '.' : Char;
  '/' : Char;
  '0' : Char;
  '1' : Char;
  '2' : Char;
  '3' : Char;
  '4' : Char;
  '5' : Char;
  '6' : Char;
  '7' : Char;
  '8' : Char;
  '9' : Char;
  ':' : Char;
  ';' : Char;
  '<' : Char;
  '=' : Char;
  '>' : Char;
  '?' : Char;
  '@' : Char;
  'A' : Char;
  'B' : Char;
  'C' : Char;
  'D' : Char;
  'E' : Char;
  'F' : Char;
  'G' : Char;
  'H' : Char;
  'I' : Char;
  'J' : Char;
  'K' : Char;
  'L' : Char;
  'M' : Char;
  'N' : Char;
  'O' : Char;
  'P' : Char;
  'Q' : Char;
  'R' : Char;
  'S' : Char;
  'T' : Char;
  'U' : Char;
  'V' : Char;
  'W' : Char;
  'X' : Char;
  'Y' : Char;
  'Z' : Char;
  '[' : Char;
  '\"' : Char;
  '\'' : Char;
  '\000' : Char;
  '\001' : Char;
  '\002' : Char;
  '\003' : Char;
  '\004' : Char;
  '\005' : Char;
  '\006' : Char;
  '\007' : Char;
  '\008' : Char;
  '\009' : Char;
  '\010' : Char;
  '\011' : Char;
  '\012' : Char;
  '\013' : Char;
  '\014' : Char;
  '\015' : Char;
  '\016' : Char;
  '\017' : Char;
  '\018' : Char;
  '\019' : Char;
  '\020' : Char;
  '\021' : Char;
  '\022' : Char;
  '\023' : Char;
  '\024' : Char;
  '\025' : Char;
  '\026' : Char;
  '\027' : Char;
  '\028' : Char;
  '\029' : Char;
  '\030' : Char;
  '\031' : Char;
  '\032' : Char;
  '\033' : Char;
  '\034' : Char;
  '\035' : Char;
  '\036' : Char;
  '\037' : Char;
  '\038' : Char;
  '\039' : Char;
  '\040' : Char;
  '\041' : Char;
  '\042' : Char;
  '\043' : Char;
  '\044' : Char;
  '\045' : Char;
  '\046' : Char;
  '\047' : Char;
  '\048' : Char;
  '\049' : Char;
  '\050' : Char;
  '\051' : Char;
  '\052' : Char;
  '\053' : Char;
  '\054' : Char;
  '\055' : Char;
  '\056' : Char;
  '\057' : Char;
  '\058' : Char;
  '\059' : Char;
  '\060' : Char;
  '\061' : Char;
  '\062' : Char;
  '\063' : Char;
  '\064' : Char;
  '\065' : Char;
  '\066' : Char;
  '\067' : Char;
  '\068' : Char;
  '\069' : Char;
  '\070' : Char;
  '\071' : Char;
  '\072' : Char;
  '\073' : Char;
  '\074' : Char;
  '\075' : Char;
  '\076' : Char;
  '\077' : Char;
  '\078' : Char;
  '\079' : Char;
  '\080' : Char;
  '\081' : Char;
  '\082' : Char;
  '\083' : Char;
  '\084' : Char;
  '\085' : Char;
  '\086' : Char;
  '\087' : Char;
  '\088' : Char;
  '\089' : Char;
  '\090' : Char;
  '\091' : Char;
  '\092' : Char;
  '\093' : Char;
  '\094' : Char;
  '\095' : Char;
  '\096' : Char;
  '\097' : Char;
  '\098' : Char;
  '\099' : Char;
  '\100' : Char;
  '\101' : Char;
  '\102' : Char;
  '\103' : Char;
  '\104' : Char;
  '\105' : Char;
  '\106' : Char;
  '\107' : Char;
  '\108' : Char;
  '\109' : Char;
  '\110' : Char;
  '\111' : Char;
  '\112' : Char;
  '\113' : Char;
  '\114' : Char;
  '\115' : Char;
  '\116' : Char;
  '\117' : Char;
  '\118' : Char;
  '\119' : Char;
  '\120' : Char;
  '\121' : Char;
  '\122' : Char;
  '\123' : Char;
  '\124' : Char;
  '\125' : Char;
  '\126' : Char;
  '\127' : Char;
  '\128' : Char;
  '\129' : Char;
  '\130' : Char;
  '\131' : Char;
  '\132' : Char;
  '\133' : Char;
  '\134' : Char;
  '\135' : Char;
  '\136' : Char;
  '\137' : Char;
  '\138' : Char;
  '\139' : Char;
  '\140' : Char;
  '\141' : Char;
  '\142' : Char;
  '\143' : Char;
  '\144' : Char;
  '\145' : Char;
  '\146' : Char;
  '\147' : Char;
  '\148' : Char;
  '\149' : Char;
  '\150' : Char;
  '\151' : Char;
  '\152' : Char;
  '\153' : Char;
  '\154' : Char;
  '\155' : Char;
  '\156' : Char;
  '\157' : Char;
  '\158' : Char;
  '\159' : Char;
  '\160' : Char;
  '\161' : Char;
  '\162' : Char;
  '\163' : Char;
  '\164' : Char;
  '\165' : Char;
  '\166' : Char;
  '\167' : Char;
  '\168' : Char;
  '\169' : Char;
  '\170' : Char;
  '\171' : Char;
  '\172' : Char;
  '\173' : Char;
  '\174' : Char;
  '\175' : Char;
  '\176' : Char;
  '\177' : Char;
  '\178' : Char;
  '\179' : Char;
  '\180' : Char;
  '\181' : Char;
  '\182' : Char;
  '\183' : Char;
  '\184' : Char;
  '\185' : Char;
  '\186' : Char;
  '\187' : Char;
  '\188' : Char;
  '\189' : Char;
  '\190' : Char;
  '\191' : Char;
  '\192' : Char;
  '\193' : Char;
  '\194' : Char;
  '\195' : Char;
  '\196' : Char;
  '\197' : Char;
  '\198' : Char;
  '\199' : Char;
  '\200' : Char;
  '\201' : Char;
  '\202' : Char;
  '\203' : Char;
  '\204' : Char;
  '\205' : Char;
  '\206' : Char;
  '\207' : Char;
  '\208' : Char;
  '\209' : Char;
  '\210' : Char;
  '\211' : Char;
  '\212' : Char;
  '\213' : Char;
  '\214' : Char;
  '\215' : Char;
  '\216' : Char;
  '\217' : Char;
  '\218' : Char;
  '\219' : Char;
  '\220' : Char;
  '\221' : Char;
  '\222' : Char;
  '\223' : Char;
  '\224' : Char;
  '\225' : Char;
  '\226' : Char;
  '\227' : Char;
  '\228' : Char;
  '\229' : Char;
  '\230' : Char;
  '\231' : Char;
  '\232' : Char;
  '\233' : Char;
  '\234' : Char;
  '\235' : Char;
  '\236' : Char;
  '\237' : Char;
  '\238' : Char;
  '\239' : Char;
  '\240' : Char;
  '\241' : Char;
  '\242' : Char;
  '\243' : Char;
  '\244' : Char;
  '\245' : Char;
  '\246' : Char;
  '\247' : Char;
  '\248' : Char;
  '\249' : Char;
  '\250' : Char;
  '\251' : Char;
  '\252' : Char;
  '\253' : Char;
  '\254' : Char;
  '\255' : Char;
  '\?' : Char;
  '\\' : Char;
  '\a' : Char;
  '\b' : Char;
  '\f' : Char;
  '\n' : Char;
  '\o000' : Char;
  '\o001' : Char;
  '\o002' : Char;
  '\o003' : Char;
  '\o004' : Char;
  '\o005' : Char;
  '\o006' : Char;
  '\o007' : Char;
  '\o010' : Char;
  '\o011' : Char;
  '\o012' : Char;
  '\o013' : Char;
  '\o014' : Char;
  '\o015' : Char;
  '\o016' : Char;
  '\o017' : Char;
  '\o020' : Char;
  '\o021' : Char;
  '\o022' : Char;
  '\o023' : Char;
  '\o024' : Char;
  '\o025' : Char;
  '\o026' : Char;
  '\o027' : Char;
  '\o030' : Char;
  '\o031' : Char;
  '\o032' : Char;
  '\o033' : Char;
  '\o034' : Char;
  '\o035' : Char;
  '\o036' : Char;
  '\o037' : Char;
  '\o040' : Char;
  '\o041' : Char;
  '\o042' : Char;
  '\o043' : Char;
  '\o044' : Char;
  '\o045' : Char;
  '\o046' : Char;
  '\o047' : Char;
  '\o050' : Char;
  '\o051' : Char;
  '\o052' : Char;
  '\o053' : Char;
  '\o054' : Char;
  '\o055' : Char;
  '\o056' : Char;
  '\o057' : Char;
  '\o060' : Char;
  '\o061' : Char;
  '\o062' : Char;
  '\o063' : Char;
  '\o064' : Char;
  '\o065' : Char;
  '\o066' : Char;
  '\o067' : Char;
  '\o070' : Char;
  '\o071' : Char;
  '\o072' : Char;
  '\o073' : Char;
  '\o074' : Char;
  '\o075' : Char;
  '\o076' : Char;
  '\o077' : Char;
  '\o100' : Char;
  '\o101' : Char;
  '\o102' : Char;
  '\o103' : Char;
  '\o104' : Char;
  '\o105' : Char;
  '\o106' : Char;
  '\o107' : Char;
  '\o110' : Char;
  '\o111' : Char;
  '\o112' : Char;
  '\o113' : Char;
  '\o114' : Char;
  '\o115' : Char;
  '\o116' : Char;
  '\o117' : Char;
  '\o120' : Char;
  '\o121' : Char;
  '\o122' : Char;
  '\o123' : Char;
  '\o124' : Char;
  '\o125' : Char;
  '\o126' : Char;
  '\o127' : Char;
  '\o130' : Char;
  '\o131' : Char;
  '\o132' : Char;
  '\o133' : Char;
  '\o134' : Char;
  '\o135' : Char;
  '\o136' : Char;
  '\o137' : Char;
  '\o140' : Char;
  '\o141' : Char;
  '\o142' : Char;
  '\o143' : Char;
  '\o144' : Char;
  '\o145' : Char;
  '\o146' : Char;
  '\o147' : Char;
  '\o150' : Char;
  '\o151' : Char;
  '\o152' : Char;
  '\o153' : Char;
  '\o154' : Char;
  '\o155' : Char;
  '\o156' : Char;
  '\o157' : Char;
  '\o160' : Char;
  '\o161' : Char;
  '\o162' : Char;
  '\o163' : Char;
  '\o164' : Char;
  '\o165' : Char;
  '\o166' : Char;
  '\o167' : Char;
  '\o170' : Char;
  '\o171' : Char;
  '\o172' : Char;
  '\o173' : Char;
  '\o174' : Char;
  '\o175' : Char;
  '\o176' : Char;
  '\o177' : Char;
  '\o200' : Char;
  '\o201' : Char;
  '\o202' : Char;
  '\o203' : Char;
  '\o204' : Char;
  '\o205' : Char;
  '\o206' : Char;
  '\o207' : Char;
  '\o210' : Char;
  '\o211' : Char;
  '\o212' : Char;
  '\o213' : Char;
  '\o214' : Char;
  '\o215' : Char;
  '\o216' : Char;
  '\o217' : Char;
  '\o220' : Char;
  '\o221' : Char;
  '\o222' : Char;
  '\o223' : Char;
  '\o224' : Char;
  '\o225' : Char;
  '\o226' : Char;
  '\o227' : Char;
  '\o230' : Char;
  '\o231' : Char;
  '\o232' : Char;
  '\o233' : Char;
  '\o234' : Char;
  '\o235' : Char;
  '\o236' : Char;
  '\o237' : Char;
  '\o240' : Char;
  '\o241' : Char;
  '\o242' : Char;
  '\o243' : Char;
  '\o244' : Char;
  '\o245' : Char;
  '\o246' : Char;
  '\o247' : Char;
  '\o250' : Char;
  '\o251' : Char;
  '\o252' : Char;
  '\o253' : Char;
  '\o254' : Char;
  '\o255' : Char;
  '\o256' : Char;
  '\o257' : Char;
  '\o260' : Char;
  '\o261' : Char;
  '\o262' : Char;
  '\o263' : Char;
  '\o264' : Char;
  '\o265' : Char;
  '\o266' : Char;
  '\o267' : Char;
  '\o270' : Char;
  '\o271' : Char;
  '\o272' : Char;
  '\o273' : Char;
  '\o274' : Char;
  '\o275' : Char;
  '\o276' : Char;
  '\o277' : Char;
  '\o300' : Char;
  '\o301' : Char;
  '\o302' : Char;
  '\o303' : Char;
  '\o304' : Char;
  '\o305' : Char;
  '\o306' : Char;
  '\o307' : Char;
  '\o310' : Char;
  '\o311' : Char;
  '\o312' : Char;
  '\o313' : Char;
  '\o314' : Char;
  '\o315' : Char;
  '\o316' : Char;
  '\o317' : Char;
  '\o320' : Char;
  '\o321' : Char;
  '\o322' : Char;
  '\o323' : Char;
  '\o324' : Char;
  '\o325' : Char;
  '\o326' : Char;
  '\o327' : Char;
  '\o330' : Char;
  '\o331' : Char;
  '\o332' : Char;
  '\o333' : Char;
  '\o334' : Char;
  '\o335' : Char;
  '\o336' : Char;
  '\o337' : Char;
  '\o340' : Char;
  '\o341' : Char;
  '\o342' : Char;
  '\o343' : Char;
  '\o344' : Char;
  '\o345' : Char;
  '\o346' : Char;
  '\o347' : Char;
  '\o350' : Char;
  '\o351' : Char;
  '\o352' : Char;
  '\o353' : Char;
  '\o354' : Char;
  '\o355' : Char;
  '\o356' : Char;
  '\o357' : Char;
  '\o360' : Char;
  '\o361' : Char;
  '\o362' : Char;
  '\o363' : Char;
  '\o364' : Char;
  '\o365' : Char;
  '\o366' : Char;
  '\o367' : Char;
  '\o370' : Char;
  '\o371' : Char;
  '\o372' : Char;
  '\o373' : Char;
  '\o374' : Char;
  '\o375' : Char;
  '\o376' : Char;
  '\o377' : Char;
  '\r' : Char;
  '\t' : Char;
  '\v' : Char;
  '\x00' : Char;
  '\x01' : Char;
  '\x02' : Char;
  '\x03' : Char;
  '\x04' : Char;
  '\x05' : Char;
  '\x06' : Char;
  '\x07' : Char;
  '\x08' : Char;
  '\x09' : Char;
  '\x0A' : Char;
  '\x0B' : Char;
  '\x0C' : Char;
  '\x0D' : Char;
  '\x0E' : Char;
  '\x0F' : Char;
  '\x10' : Char;
  '\x11' : Char;
  '\x12' : Char;
  '\x13' : Char;
  '\x14' : Char;
  '\x15' : Char;
  '\x16' : Char;
  '\x17' : Char;
  '\x18' : Char;
  '\x19' : Char;
  '\x1A' : Char;
  '\x1B' : Char;
  '\x1C' : Char;
  '\x1D' : Char;
  '\x1E' : Char;
  '\x1F' : Char;
  '\x20' : Char;
  '\x21' : Char;
  '\x22' : Char;
  '\x23' : Char;
  '\x24' : Char;
  '\x25' : Char;
  '\x26' : Char;
  '\x27' : Char;
  '\x28' : Char;
  '\x29' : Char;
  '\x2A' : Char;
  '\x2B' : Char;
  '\x2C' : Char;
  '\x2D' : Char;
  '\x2E' : Char;
  '\x2F' : Char;
  '\x30' : Char;
  '\x31' : Char;
  '\x32' : Char;
  '\x33' : Char;
  '\x34' : Char;
  '\x35' : Char;
  '\x36' : Char;
  '\x37' : Char;
  '\x38' : Char;
  '\x39' : Char;
  '\x3A' : Char;
  '\x3B' : Char;
  '\x3C' : Char;
  '\x3D' : Char;
  '\x3E' : Char;
  '\x3F' : Char;
  '\x40' : Char;
  '\x41' : Char;
  '\x42' : Char;
  '\x43' : Char;
  '\x44' : Char;
  '\x45' : Char;
  '\x46' : Char;
  '\x47' : Char;
  '\x48' : Char;
  '\x49' : Char;
  '\x4A' : Char;
  '\x4B' : Char;
  '\x4C' : Char;
  '\x4D' : Char;
  '\x4E' : Char;
  '\x4F' : Char;
  '\x50' : Char;
  '\x51' : Char;
  '\x52' : Char;
  '\x53' : Char;
  '\x54' : Char;
  '\x55' : Char;
  '\x56' : Char;
  '\x57' : Char;
  '\x58' : Char;
  '\x59' : Char;
  '\x5A' : Char;
  '\x5B' : Char;
  '\x5C' : Char;
  '\x5D' : Char;
  '\x5E' : Char;
  '\x5F' : Char;
  '\x60' : Char;
  '\x61' : Char;
  '\x62' : Char;
  '\x63' : Char;
  '\x64' : Char;
  '\x65' : Char;
  '\x66' : Char;
  '\x67' : Char;
  '\x68' : Char;
  '\x69' : Char;
  '\x6A' : Char;
  '\x6B' : Char;
  '\x6C' : Char;
  '\x6D' : Char;
  '\x6E' : Char;
  '\x6F' : Char;
  '\x70' : Char;
  '\x71' : Char;
  '\x72' : Char;
  '\x73' : Char;
  '\x74' : Char;
  '\x75' : Char;
  '\x76' : Char;
  '\x77' : Char;
  '\x78' : Char;
  '\x79' : Char;
  '\x7A' : Char;
  '\x7B' : Char;
  '\x7C' : Char;
  '\x7D' : Char;
  '\x7E' : Char;
  '\x7F' : Char;
  '\x80' : Char;
  '\x81' : Char;
  '\x82' : Char;
  '\x83' : Char;
  '\x84' : Char;
  '\x85' : Char;
  '\x86' : Char;
  '\x87' : Char;
  '\x88' : Char;
  '\x89' : Char;
  '\x8A' : Char;
  '\x8B' : Char;
  '\x8C' : Char;
  '\x8D' : Char;
  '\x8E' : Char;
  '\x8F' : Char;
  '\x90' : Char;
  '\x91' : Char;
  '\x92' : Char;
  '\x93' : Char;
  '\x94' : Char;
  '\x95' : Char;
  '\x96' : Char;
  '\x97' : Char;
  '\x98' : Char;
  '\x99' : Char;
  '\x9A' : Char;
  '\x9B' : Char;
  '\x9C' : Char;
  '\x9D' : Char;
  '\x9E' : Char;
  '\x9F' : Char;
  '\xA0' : Char;
  '\xA1' : Char;
  '\xA2' : Char;
  '\xA3' : Char;
  '\xA4' : Char;
  '\xA5' : Char;
  '\xA6' : Char;
  '\xA7' : Char;
  '\xA8' : Char;
  '\xA9' : Char;
  '\xAA' : Char;
  '\xAB' : Char;
  '\xAC' : Char;
  '\xAD' : Char;
  '\xAE' : Char;
  '\xAF' : Char;
  '\xB0' : Char;
  '\xB1' : Char;
  '\xB2' : Char;
  '\xB3' : Char;
  '\xB4' : Char;
  '\xB5' : Char;
  '\xB6' : Char;
  '\xB7' : Char;
  '\xB8' : Char;
  '\xB9' : Char;
  '\xBA' : Char;
  '\xBB' : Char;
  '\xBC' : Char;
  '\xBD' : Char;
  '\xBE' : Char;
  '\xBF' : Char;
  '\xC0' : Char;
  '\xC1' : Char;
  '\xC2' : Char;
  '\xC3' : Char;
  '\xC4' : Char;
  '\xC5' : Char;
  '\xC6' : Char;
  '\xC7' : Char;
  '\xC8' : Char;
  '\xC9' : Char;
  '\xCA' : Char;
  '\xCB' : Char;
  '\xCC' : Char;
  '\xCD' : Char;
  '\xCE' : Char;
  '\xCF' : Char;
  '\xD0' : Char;
  '\xD1' : Char;
  '\xD2' : Char;
  '\xD3' : Char;
  '\xD4' : Char;
  '\xD5' : Char;
  '\xD6' : Char;
  '\xD7' : Char;
  '\xD8' : Char;
  '\xD9' : Char;
  '\xDA' : Char;
  '\xDB' : Char;
  '\xDC' : Char;
  '\xDD' : Char;
  '\xDE' : Char;
  '\xDF' : Char;
  '\xE0' : Char;
  '\xE1' : Char;
  '\xE2' : Char;
  '\xE3' : Char;
  '\xE4' : Char;
  '\xE5' : Char;
  '\xE6' : Char;
  '\xE7' : Char;
  '\xE8' : Char;
  '\xE9' : Char;
  '\xEA' : Char;
  '\xEB' : Char;
  '\xEC' : Char;
  '\xED' : Char;
  '\xEE' : Char;
  '\xEF' : Char;
  '\xF0' : Char;
  '\xF1' : Char;
  '\xF2' : Char;
  '\xF3' : Char;
  '\xF4' : Char;
  '\xF5' : Char;
  '\xF6' : Char;
  '\xF7' : Char;
  '\xF8' : Char;
  '\xF9' : Char;
  '\xFA' : Char;
  '\xFB' : Char;
  '\xFC' : Char;
  '\xFD' : Char;
  '\xFE' : Char;
  '\xFF' : Char;
  ']' : Char;
  '^' : Char;
  '_' : Char;
  '`' : Char;
  'a' : Char;
  'b' : Char;
  'c' : Char;
  'd' : Char;
  'e' : Char;
  'f' : Char;
  'g' : Char;
  'h' : Char;
  'i' : Char;
  'j' : Char;
  'k' : Char;
  'l' : Char;
  'm' : Char;
  'n' : Char;
  'o' : Char;
  'p' : Char;
  'q' : Char;
  'r' : Char;
  's' : Char;
  't' : Char;
  'u' : Char;
  'v' : Char;
  'w' : Char;
  'x' : Char;
  'y' : Char;
  'z' : Char;
  '{' : Char;
  '|' : Char;
  '}' : Char;
  '~' : Char;
  '¡' : Char;
  '¢' : Char;
  '£' : Char;
  '¤' : Char;
  '¥' : Char;
  '¦' : Char;
  '§' : Char;
  '¨' : Char;
  '©' : Char;
  'ª' : Char;
  '«' : Char;
  '¬' : Char;
  '­' : Char;
  '®' : Char;
  '¯' : Char;
  '°' : Char;
  '±' : Char;
  '²' : Char;
  '³' : Char;
  '´' : Char;
  'µ' : Char;
  '¶' : Char;
  '·' : Char;
  '¸' : Char;
  '¹' : Char;
  'º' : Char;
  '»' : Char;
  '¼' : Char;
  '½' : Char;
  '¾' : Char;
  '¿' : Char;
  'À' : Char;
  'Á' : Char;
  'Â' : Char;
  'Ã' : Char;
  'Ä' : Char;
  'Å' : Char;
  'Æ' : Char;
  'Ç' : Char;
  'È' : Char;
  'É' : Char;
  'Ê' : Char;
  'Ë' : Char;
  'Ì' : Char;
  'Í' : Char;
  'Î' : Char;
  'Ï' : Char;
  'Ð' : Char;
  'Ñ' : Char;
  'Ò' : Char;
  'Ó' : Char;
  'Ô' : Char;
  'Õ' : Char;
  'Ö' : Char;
  '×' : Char;
  'Ø' : Char;
  'Ù' : Char;
  'Ú' : Char;
  'Û' : Char;
  'Ü' : Char;
  'Ý' : Char;
  'Þ' : Char;
  'ß' : Char;
  'à' : Char;
  'á' : Char;
  'â' : Char;
  'ã' : Char;
  'ä' : Char;
  'å' : Char;
  'æ' : Char;
  'ç' : Char;
  'è' : Char;
  'é' : Char;
  'ê' : Char;
  'ë' : Char;
  'ì' : Char;
  'í' : Char;
  'î' : Char;
  'ï' : Char;
  'ð' : Char;
  'ñ' : Char;
  'ò' : Char;
  'ó' : Char;
  'ô' : Char;
  'õ' : Char;
  'ö' : Char;
  '÷' : Char;
  'ø' : Char;
  'ù' : Char;
  'ú' : Char;
  'û' : Char;
  'ü' : Char;
  'ý' : Char;
  'þ' : Char;
  'ÿ' : Char;
  +__ : Nat->Nat;
  0 : Nat;
  1 : Nat;
  1 : Pos;
  2 : Nat;
  3 : Nat;
  4 : Nat;
  5 : Nat;
  6 : Nat;
  7 : Nat;
  8 : Nat;
  9 : Nat;
  ACK : Char;
  BEL : Char;
  BS : Char;
  CAN : Char;
  CR : Char;
  DC1 : Char;
  DC2 : Char;
  DC3 : Char;
  DC4 : Char;
  DEL : Char;
  DLE : Char;
  EM : Char;
  ENQ : Char;
  EOT : Char;
  ESC : Char;
  ETB : Char;
  ETX : Char;
  FF : Char;
  FS : Char;
  GS : Char;
  HT : Char;
  LF : Char;
  NAK : Char;
  NL : Char;
  NP : Char;
  NUL : Char;
  RS : Char;
  SI : Char;
  SO : Char;
  SOH : Char;
  SP : Char;
  SUB : Char;
  SYN : Char;
  SYX : Char;
  US : Char;
  VT : Char;
  __! : Nat->Nat;
  __*__ : Nat*Nat->Nat;
  __*__ : Pos*Pos->Pos;
  __+__ : Nat*Nat->Nat;
  __+__ : Nat*Pos->Pos;
  __+__ : Pos*Nat->Pos;
  __-?__ : Nat*Nat->?Nat;
  __/?__ : Nat*Nat->?Nat;
  __@@__ : Nat*Nat->Nat;
  __^__ : Nat*Nat->Nat;
  __div__ : Nat*Nat->?Nat;
  __mod__ : Nat*Nat->?Nat;
  __quot__ : Nat*Nat->?Nat;
  __rem__ : Nat*Nat->?Nat;
  abs : Nat->Nat;
  chr : Nat->?Char;
  max : Nat*Nat->Nat;
  min : Nat*Nat->Nat;
  ord : Char->Nat;
  pre : Nat->?Nat;
  suc : Nat->Nat;
  suc : Nat->Pos
preds
  __<=__ : Nat*Nat;
  __<__ : Nat*Nat;
  __>=__ : Nat*Nat;
  __>__ : Nat*Nat;
  even : Nat;
  isDigit : Char;
  isLetter : Char;
  isPrintable : Char;
  odd : Nat

end

spec ExtBooleanAlgebra %% [...] %%  =
sort
  Elem
ops
  0 : Elem;
  1 : Elem;
  __cap__ : Elem*Elem->Elem;
  __cup__ : Elem*Elem->Elem;
  compl : Elem->Elem
preds
  __<=__ : Elem*Elem;
  __<__ : Elem*Elem;
  __>=__ : Elem*Elem;
  __>__ : Elem*Elem

end

spec Nat =
sorts
  Pos < Nat;
  Pos
ops
  +__ : Nat->Nat;
  0 : Nat;
  1 : Nat;
  1 : Pos;
  2 : Nat;
  3 : Nat;
  4 : Nat;
  5 : Nat;
  6 : Nat;
  7 : Nat;
  8 : Nat;
  9 : Nat;
  __! : Nat->Nat;
  __*__ : Nat*Nat->Nat;
  __*__ : Pos*Pos->Pos;
  __+__ : Nat*Nat->Nat;
  __+__ : Nat*Pos->Pos;
  __+__ : Pos*Nat->Pos;
  __-?__ : Nat*Nat->?Nat;
  __/?__ : Nat*Nat->?Nat;
  __@@__ : Nat*Nat->Nat;
  __^__ : Nat*Nat->Nat;
  __div__ : Nat*Nat->?Nat;
  __mod__ : Nat*Nat->?Nat;
  __quot__ : Nat*Nat->?Nat;
  __rem__ : Nat*Nat->?Nat;
  abs : Nat->Nat;
  max : Nat*Nat->Nat;
  min : Nat*Nat->Nat;
  pre : Nat->?Nat;
  suc : Nat->Nat;
  suc : Nat->Pos
preds
  __<=__ : Nat*Nat;
  __<__ : Nat*Nat;
  __>=__ : Nat*Nat;
  __>__ : Nat*Nat;
  even : Nat;
  odd : Nat

end

spec RichBoolean =
sort
  Boolean
ops
  False : Boolean;
  Not__ : Boolean->Boolean;
  True : Boolean;
  __And__ : Boolean*Boolean->Boolean;
  __Or__ : Boolean*Boolean->Boolean;
  compl : Boolean->Boolean
preds
  __<=__ : Boolean*Boolean;
  __<__ : Boolean*Boolean;
  __>=__ : Boolean*Boolean;
  __>__ : Boolean*Boolean

end