BasicSpec.sentences.output revision b1c32a0faa63e0c13687f36a2faae5969ec0a9d5
(sorts ABCDEFGHIJKLMONOPQRSTUVWXYZ, Boolean, Char, Data1, Data2,
Data3, Data4, Forest, Int, List, Nat, Pos, Rat, Set, Tree, a, a',
a'b''2, a_b_c, ab2, ab_2_3_a, abc, abcdefghijlklmnopqrstuvwxyz, b,
c, d, e, nat, s, t, x0123456789,
����������������������������������������������������������
sorts Data1 < Data2; Nat, Pos < Int; Pos < Nat;
Int, Nat, Pos < Rat; a, b, c, d, e < a; a, b, c, d, e < b;
a, b, c, d, e < c; a, b, c, d, e < d; a, b, c, d, e < e;
s, s1, s2, t < s; s, s1, s2, t < t
op ' ' : Char
op '!' : Char
op '!' : s
op '#' : Char
op '$' : Char
op '$' : s
op '%' : Char
op '&' : Char
op '&' : s
op '(' : Char
op '(' : s
op ')' : Char
op ')' : s
op '*' : Char
op '+' : Char
op ',' : Char
op '-' : Char
op '.' : Char
op '/' : Char
op '/' : s
op '0' : Char
op '0' : s
op '1' : Char
op '1' : s
op '2' : Char
op '2' : s
op '3' : Char
op '3' : s
op '4' : Char
op '4' : s
op '5' : Char
op '5' : s
op '6' : Char
op '6' : s
op '7' : Char
op '7' : s
op '8' : Char
op '8' : s
op '9' : Char
op '9' : s
op ':' : Char
op ';' : Char
op '<' : Char
op '=' : Char
op '=' : s
op '>' : Char
op '?' : Char
op '?' : s
op '@' : Char
op 'A' : Char
op 'B' : Char
op 'C' : Char
op 'D' : Char
op 'E' : Char
op 'F' : Char
op 'G' : Char
op 'H' : Char
op 'I' : Char
op 'J' : Char
op 'K' : Char
op 'L' : Char
op 'M' : Char
op 'N' : Char
op 'O' : Char
op 'P' : Char
op 'Q' : Char
op 'R' : Char
op 'S' : Char
op 'T' : Char
op 'U' : Char
op 'V' : Char
op 'W' : Char
op 'X' : Char
op 'Y' : Char
op 'Z' : Char
op '[' : Char
op '\"' : Char
op '\"' : s
op '\'' : Char
op '\000' : Char
op '\000' : s
op '\001' : Char
op '\002' : Char
op '\003' : Char
op '\004' : Char
op '\005' : Char
op '\006' : Char
op '\007' : Char
op '\008' : Char
op '\009' : Char
op '\010' : Char
op '\011' : Char
op '\012' : Char
op '\013' : Char
op '\014' : Char
op '\015' : Char
op '\016' : Char
op '\017' : Char
op '\018' : Char
op '\019' : Char
op '\020' : Char
op '\021' : Char
op '\022' : Char
op '\023' : Char
op '\024' : Char
op '\025' : Char
op '\026' : Char
op '\027' : Char
op '\028' : Char
op '\029' : Char
op '\030' : Char
op '\031' : Char
op '\032' : Char
op '\033' : Char
op '\034' : Char
op '\035' : Char
op '\036' : Char
op '\037' : Char
op '\038' : Char
op '\039' : Char
op '\040' : Char
op '\041' : Char
op '\042' : Char
op '\043' : Char
op '\044' : Char
op '\045' : Char
op '\046' : Char
op '\047' : Char
op '\048' : Char
op '\049' : Char
op '\050' : Char
op '\051' : Char
op '\052' : Char
op '\053' : Char
op '\054' : Char
op '\055' : Char
op '\056' : Char
op '\057' : Char
op '\058' : Char
op '\059' : Char
op '\060' : Char
op '\061' : Char
op '\062' : Char
op '\063' : Char
op '\064' : Char
op '\065' : Char
op '\066' : Char
op '\067' : Char
op '\068' : Char
op '\069' : Char
op '\070' : Char
op '\071' : Char
op '\072' : Char
op '\073' : Char
op '\074' : Char
op '\075' : Char
op '\076' : Char
op '\077' : Char
op '\078' : Char
op '\079' : Char
op '\080' : Char
op '\081' : Char
op '\082' : Char
op '\083' : Char
op '\084' : Char
op '\085' : Char
op '\086' : Char
op '\087' : Char
op '\088' : Char
op '\089' : Char
op '\090' : Char
op '\091' : Char
op '\092' : Char
op '\093' : Char
op '\094' : Char
op '\095' : Char
op '\096' : Char
op '\097' : Char
op '\098' : Char
op '\099' : Char
op '\100' : Char
op '\101' : Char
op '\102' : Char
op '\103' : Char
op '\104' : Char
op '\105' : Char
op '\106' : Char
op '\107' : Char
op '\108' : Char
op '\109' : Char
op '\110' : Char
op '\111' : Char
op '\112' : Char
op '\113' : Char
op '\114' : Char
op '\115' : Char
op '\116' : Char
op '\117' : Char
op '\118' : Char
op '\119' : Char
op '\120' : Char
op '\121' : Char
op '\122' : Char
op '\123' : Char
op '\124' : Char
op '\125' : Char
op '\126' : Char
op '\127' : Char
op '\128' : Char
op '\129' : Char
op '\130' : Char
op '\131' : Char
op '\132' : Char
op '\133' : Char
op '\134' : Char
op '\135' : Char
op '\136' : Char
op '\137' : Char
op '\138' : Char
op '\139' : Char
op '\140' : Char
op '\141' : Char
op '\142' : Char
op '\143' : Char
op '\144' : Char
op '\145' : Char
op '\146' : Char
op '\147' : Char
op '\148' : Char
op '\149' : Char
op '\150' : Char
op '\151' : Char
op '\152' : Char
op '\153' : Char
op '\154' : Char
op '\155' : Char
op '\156' : Char
op '\157' : Char
op '\158' : Char
op '\159' : Char
op '\160' : Char
op '\161' : Char
op '\162' : Char
op '\163' : Char
op '\164' : Char
op '\165' : Char
op '\166' : Char
op '\167' : Char
op '\168' : Char
op '\169' : Char
op '\170' : Char
op '\171' : Char
op '\172' : Char
op '\173' : Char
op '\174' : Char
op '\175' : Char
op '\176' : Char
op '\177' : Char
op '\178' : Char
op '\179' : Char
op '\180' : Char
op '\181' : Char
op '\182' : Char
op '\183' : Char
op '\184' : Char
op '\185' : Char
op '\186' : Char
op '\187' : Char
op '\188' : Char
op '\189' : Char
op '\190' : Char
op '\191' : Char
op '\192' : Char
op '\193' : Char
op '\194' : Char
op '\195' : Char
op '\196' : Char
op '\197' : Char
op '\198' : Char
op '\199' : Char
op '\200' : Char
op '\201' : Char
op '\202' : Char
op '\203' : Char
op '\204' : Char
op '\205' : Char
op '\206' : Char
op '\207' : Char
op '\208' : Char
op '\209' : Char
op '\210' : Char
op '\211' : Char
op '\212' : Char
op '\213' : Char
op '\214' : Char
op '\215' : Char
op '\216' : Char
op '\217' : Char
op '\218' : Char
op '\219' : Char
op '\220' : Char
op '\221' : Char
op '\222' : Char
op '\223' : Char
op '\224' : Char
op '\225' : Char
op '\226' : Char
op '\227' : Char
op '\228' : Char
op '\229' : Char
op '\230' : Char
op '\231' : Char
op '\232' : Char
op '\233' : Char
op '\234' : Char
op '\235' : Char
op '\236' : Char
op '\237' : Char
op '\238' : Char
op '\239' : Char
op '\240' : Char
op '\241' : Char
op '\242' : Char
op '\243' : Char
op '\244' : Char
op '\245' : Char
op '\246' : Char
op '\247' : Char
op '\248' : Char
op '\249' : Char
op '\250' : Char
op '\251' : Char
op '\252' : Char
op '\253' : Char
op '\254' : Char
op '\255' : Char
op '\255' : s
op '\?' : Char
op '\\' : Char
op '\\' : s
op '\a' : Char
op '\b' : Char
op '\f' : Char
op '\n' : Char
op '\n' : s
op '\o000' : Char
op '\o000' : s
op '\o001' : Char
op '\o002' : Char
op '\o003' : Char
op '\o004' : Char
op '\o005' : Char
op '\o006' : Char
op '\o007' : Char
op '\o010' : Char
op '\o011' : Char
op '\o012' : Char
op '\o013' : Char
op '\o014' : Char
op '\o015' : Char
op '\o016' : Char
op '\o017' : Char
op '\o020' : Char
op '\o021' : Char
op '\o022' : Char
op '\o023' : Char
op '\o024' : Char
op '\o025' : Char
op '\o026' : Char
op '\o027' : Char
op '\o030' : Char
op '\o031' : Char
op '\o032' : Char
op '\o033' : Char
op '\o034' : Char
op '\o035' : Char
op '\o036' : Char
op '\o037' : Char
op '\o040' : Char
op '\o041' : Char
op '\o042' : Char
op '\o043' : Char
op '\o044' : Char
op '\o045' : Char
op '\o046' : Char
op '\o047' : Char
op '\o050' : Char
op '\o051' : Char
op '\o052' : Char
op '\o053' : Char
op '\o054' : Char
op '\o055' : Char
op '\o056' : Char
op '\o057' : Char
op '\o060' : Char
op '\o061' : Char
op '\o062' : Char
op '\o063' : Char
op '\o064' : Char
op '\o065' : Char
op '\o066' : Char
op '\o067' : Char
op '\o070' : Char
op '\o071' : Char
op '\o072' : Char
op '\o073' : Char
op '\o074' : Char
op '\o075' : Char
op '\o076' : Char
op '\o077' : Char
op '\o100' : Char
op '\o101' : Char
op '\o102' : Char
op '\o103' : Char
op '\o104' : Char
op '\o105' : Char
op '\o106' : Char
op '\o107' : Char
op '\o110' : Char
op '\o111' : Char
op '\o112' : Char
op '\o113' : Char
op '\o114' : Char
op '\o115' : Char
op '\o116' : Char
op '\o117' : Char
op '\o120' : Char
op '\o121' : Char
op '\o122' : Char
op '\o123' : Char
op '\o124' : Char
op '\o125' : Char
op '\o126' : Char
op '\o127' : Char
op '\o130' : Char
op '\o131' : Char
op '\o132' : Char
op '\o133' : Char
op '\o134' : Char
op '\o135' : Char
op '\o136' : Char
op '\o137' : Char
op '\o140' : Char
op '\o141' : Char
op '\o142' : Char
op '\o143' : Char
op '\o144' : Char
op '\o145' : Char
op '\o146' : Char
op '\o147' : Char
op '\o150' : Char
op '\o151' : Char
op '\o152' : Char
op '\o153' : Char
op '\o154' : Char
op '\o155' : Char
op '\o156' : Char
op '\o157' : Char
op '\o160' : Char
op '\o161' : Char
op '\o162' : Char
op '\o163' : Char
op '\o164' : Char
op '\o165' : Char
op '\o166' : Char
op '\o167' : Char
op '\o170' : Char
op '\o171' : Char
op '\o172' : Char
op '\o173' : Char
op '\o174' : Char
op '\o175' : Char
op '\o176' : Char
op '\o177' : Char
op '\o200' : Char
op '\o201' : Char
op '\o202' : Char
op '\o203' : Char
op '\o204' : Char
op '\o205' : Char
op '\o206' : Char
op '\o207' : Char
op '\o210' : Char
op '\o211' : Char
op '\o212' : Char
op '\o213' : Char
op '\o214' : Char
op '\o215' : Char
op '\o216' : Char
op '\o217' : Char
op '\o220' : Char
op '\o221' : Char
op '\o222' : Char
op '\o223' : Char
op '\o224' : Char
op '\o225' : Char
op '\o226' : Char
op '\o227' : Char
op '\o230' : Char
op '\o231' : Char
op '\o232' : Char
op '\o233' : Char
op '\o234' : Char
op '\o235' : Char
op '\o236' : Char
op '\o237' : Char
op '\o240' : Char
op '\o241' : Char
op '\o242' : Char
op '\o243' : Char
op '\o244' : Char
op '\o245' : Char
op '\o246' : Char
op '\o247' : Char
op '\o250' : Char
op '\o251' : Char
op '\o252' : Char
op '\o253' : Char
op '\o254' : Char
op '\o255' : Char
op '\o256' : Char
op '\o257' : Char
op '\o260' : Char
op '\o261' : Char
op '\o262' : Char
op '\o263' : Char
op '\o264' : Char
op '\o265' : Char
op '\o266' : Char
op '\o267' : Char
op '\o270' : Char
op '\o271' : Char
op '\o272' : Char
op '\o273' : Char
op '\o274' : Char
op '\o275' : Char
op '\o276' : Char
op '\o277' : Char
op '\o300' : Char
op '\o301' : Char
op '\o302' : Char
op '\o303' : Char
op '\o304' : Char
op '\o305' : Char
op '\o306' : Char
op '\o307' : Char
op '\o310' : Char
op '\o311' : Char
op '\o312' : Char
op '\o313' : Char
op '\o314' : Char
op '\o315' : Char
op '\o316' : Char
op '\o317' : Char
op '\o320' : Char
op '\o321' : Char
op '\o322' : Char
op '\o323' : Char
op '\o324' : Char
op '\o325' : Char
op '\o326' : Char
op '\o327' : Char
op '\o330' : Char
op '\o331' : Char
op '\o332' : Char
op '\o333' : Char
op '\o334' : Char
op '\o335' : Char
op '\o336' : Char
op '\o337' : Char
op '\o340' : Char
op '\o341' : Char
op '\o342' : Char
op '\o343' : Char
op '\o344' : Char
op '\o345' : Char
op '\o346' : Char
op '\o347' : Char
op '\o350' : Char
op '\o351' : Char
op '\o352' : Char
op '\o353' : Char
op '\o354' : Char
op '\o355' : Char
op '\o356' : Char
op '\o357' : Char
op '\o360' : Char
op '\o361' : Char
op '\o362' : Char
op '\o363' : Char
op '\o364' : Char
op '\o365' : Char
op '\o366' : Char
op '\o367' : Char
op '\o370' : Char
op '\o371' : Char
op '\o372' : Char
op '\o373' : Char
op '\o374' : Char
op '\o375' : Char
op '\o376' : Char
op '\o377' : Char
op '\o377' : s
op '\r' : Char
op '\t' : Char
op '\v' : Char
op '\x00' : Char
op '\x00' : s
op '\x01' : Char
op '\x02' : Char
op '\x03' : Char
op '\x04' : Char
op '\x05' : Char
op '\x06' : Char
op '\x07' : Char
op '\x08' : Char
op '\x09' : Char
op '\x0A' : Char
op '\x0B' : Char
op '\x0C' : Char
op '\x0D' : Char
op '\x0E' : Char
op '\x0F' : Char
op '\x10' : Char
op '\x11' : Char
op '\x12' : Char
op '\x13' : Char
op '\x14' : Char
op '\x15' : Char
op '\x16' : Char
op '\x17' : Char
op '\x18' : Char
op '\x19' : Char
op '\x1A' : Char
op '\x1B' : Char
op '\x1C' : Char
op '\x1D' : Char
op '\x1E' : Char
op '\x1F' : Char
op '\x20' : Char
op '\x21' : Char
op '\x22' : Char
op '\x23' : Char
op '\x24' : Char
op '\x25' : Char
op '\x26' : Char
op '\x27' : Char
op '\x28' : Char
op '\x29' : Char
op '\x2A' : Char
op '\x2B' : Char
op '\x2C' : Char
op '\x2D' : Char
op '\x2E' : Char
op '\x2F' : Char
op '\x30' : Char
op '\x31' : Char
op '\x32' : Char
op '\x33' : Char
op '\x34' : Char
op '\x35' : Char
op '\x36' : Char
op '\x37' : Char
op '\x38' : Char
op '\x39' : Char
op '\x3A' : Char
op '\x3B' : Char
op '\x3C' : Char
op '\x3D' : Char
op '\x3E' : Char
op '\x3F' : Char
op '\x40' : Char
op '\x41' : Char
op '\x42' : Char
op '\x43' : Char
op '\x44' : Char
op '\x45' : Char
op '\x46' : Char
op '\x47' : Char
op '\x48' : Char
op '\x49' : Char
op '\x4A' : Char
op '\x4B' : Char
op '\x4C' : Char
op '\x4D' : Char
op '\x4E' : Char
op '\x4F' : Char
op '\x50' : Char
op '\x51' : Char
op '\x52' : Char
op '\x53' : Char
op '\x54' : Char
op '\x55' : Char
op '\x56' : Char
op '\x57' : Char
op '\x58' : Char
op '\x59' : Char
op '\x5A' : Char
op '\x5B' : Char
op '\x5C' : Char
op '\x5D' : Char
op '\x5E' : Char
op '\x5F' : Char
op '\x60' : Char
op '\x61' : Char
op '\x62' : Char
op '\x63' : Char
op '\x64' : Char
op '\x65' : Char
op '\x66' : Char
op '\x67' : Char
op '\x68' : Char
op '\x69' : Char
op '\x6A' : Char
op '\x6B' : Char
op '\x6C' : Char
op '\x6D' : Char
op '\x6E' : Char
op '\x6F' : Char
op '\x70' : Char
op '\x71' : Char
op '\x72' : Char
op '\x73' : Char
op '\x74' : Char
op '\x75' : Char
op '\x76' : Char
op '\x77' : Char
op '\x78' : Char
op '\x79' : Char
op '\x7A' : Char
op '\x7B' : Char
op '\x7C' : Char
op '\x7D' : Char
op '\x7E' : Char
op '\x7F' : Char
op '\x80' : Char
op '\x81' : Char
op '\x82' : Char
op '\x83' : Char
op '\x84' : Char
op '\x85' : Char
op '\x86' : Char
op '\x87' : Char
op '\x88' : Char
op '\x89' : Char
op '\x8A' : Char
op '\x8B' : Char
op '\x8C' : Char
op '\x8D' : Char
op '\x8E' : Char
op '\x8F' : Char
op '\x90' : Char
op '\x91' : Char
op '\x92' : Char
op '\x93' : Char
op '\x94' : Char
op '\x95' : Char
op '\x96' : Char
op '\x97' : Char
op '\x98' : Char
op '\x99' : Char
op '\x9A' : Char
op '\x9B' : Char
op '\x9C' : Char
op '\x9D' : Char
op '\x9E' : Char
op '\x9F' : Char
op '\xA0' : Char
op '\xA1' : Char
op '\xA2' : Char
op '\xA3' : Char
op '\xA4' : Char
op '\xA5' : Char
op '\xA6' : Char
op '\xA7' : Char
op '\xA8' : Char
op '\xA9' : Char
op '\xAA' : Char
op '\xAB' : Char
op '\xAC' : Char
op '\xAD' : Char
op '\xAE' : Char
op '\xAF' : Char
op '\xB0' : Char
op '\xB1' : Char
op '\xB2' : Char
op '\xB3' : Char
op '\xB4' : Char
op '\xB5' : Char
op '\xB6' : Char
op '\xB7' : Char
op '\xB8' : Char
op '\xB9' : Char
op '\xBA' : Char
op '\xBB' : Char
op '\xBC' : Char
op '\xBD' : Char
op '\xBE' : Char
op '\xBF' : Char
op '\xC0' : Char
op '\xC1' : Char
op '\xC2' : Char
op '\xC3' : Char
op '\xC4' : Char
op '\xC5' : Char
op '\xC6' : Char
op '\xC7' : Char
op '\xC8' : Char
op '\xC9' : Char
op '\xCA' : Char
op '\xCB' : Char
op '\xCC' : Char
op '\xCD' : Char
op '\xCE' : Char
op '\xCF' : Char
op '\xD0' : Char
op '\xD1' : Char
op '\xD2' : Char
op '\xD3' : Char
op '\xD4' : Char
op '\xD5' : Char
op '\xD6' : Char
op '\xD7' : Char
op '\xD8' : Char
op '\xD9' : Char
op '\xDA' : Char
op '\xDB' : Char
op '\xDC' : Char
op '\xDD' : Char
op '\xDE' : Char
op '\xDF' : Char
op '\xE0' : Char
op '\xE1' : Char
op '\xE2' : Char
op '\xE3' : Char
op '\xE4' : Char
op '\xE5' : Char
op '\xE6' : Char
op '\xE7' : Char
op '\xE8' : Char
op '\xE9' : Char
op '\xEA' : Char
op '\xEB' : Char
op '\xEC' : Char
op '\xED' : Char
op '\xEE' : Char
op '\xEF' : Char
op '\xF0' : Char
op '\xF1' : Char
op '\xF2' : Char
op '\xF3' : Char
op '\xF4' : Char
op '\xF5' : Char
op '\xF6' : Char
op '\xF7' : Char
op '\xF8' : Char
op '\xF9' : Char
op '\xFA' : Char
op '\xFB' : Char
op '\xFC' : Char
op '\xFD' : Char
op '\xFE' : Char
op '\xFF' : Char
op '\xFF' : s
op ']' : Char
op '^' : Char
op '^' : s
op '_' : Char
op '`' : Char
op 'a' : Char
op 'a' : s
op 'b' : Char
op 'c' : Char
op 'd' : Char
op 'e' : Char
op 'f' : Char
op 'g' : Char
op 'h' : Char
op 'i' : Char
op 'j' : Char
op 'k' : Char
op 'l' : Char
op 'm' : Char
op 'n' : Char
op 'o' : Char
op 'p' : Char
op 'q' : Char
op 'r' : Char
op 's' : Char
op 't' : Char
op 'u' : Char
op 'v' : Char
op 'w' : Char
op 'x' : Char
op 'y' : Char
op 'z' : Char
op '{' : Char
op '|' : Char
op '}' : Char
op '~' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : s
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : s
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op '�' : Char
op +__ : Int -> Int
op +__ : Nat -> Nat
op +__ : Rat -> Rat
op - : s -> s
op -__ : Int -> Int
op -__ : Rat -> Rat
op 0 : Int
op 0 : Nat
op 0 : Rat
op 0 : nat
op 1 : Int
op 1 : Nat
op 1 : Pos
op 1 : Rat
op 1 : s
op 2 : Nat
op 2 : s
op 3 : Nat
op 3 : s
op 4 : Nat
op 4 : s
op 5 : Nat
op 6 : Nat
op 7 : Nat
op 8 : Nat
op 9 : Nat
op ACK : Char
op Add : Data1 * Set -> Set
op BEL : Char
op BS : Char
op CAN : Char
op CR : Char
op Cons : Data1 * List -> List
op Cons : Tree * Forest -> Forest
op Cons21 : Data1 * Data2 -> Data2
op Cons22 : Data2 * Data1 -> Data2
op Cons31 : Data1 * Data2 -> Data3
op Cons32 : Data2 * Data1 -> Data3
op Cons41 : Data1 * Data2 ->? Data4
op Cons42 : Data2 * Data1 ->? Data4
op DC1 : Char
op DC2 : Char
op DC3 : Char
op DC4 : Char
op DEL : Char
op DLE : Char
op EM : Char
op ENQ : Char
op EOT : Char
op ESC : Char
op ETB : Char
op ETX : Char
op FF : Char
op FS : Char
op False : Boolean
op Forest : Tree
op GS : Char
op HT : Char
op LF : Char
op Leaf : Data1 -> Tree
op Mt : Set
op NAK : Char
op NL : Char
op NP : Char
op NUL : Char
op Nil : Forest
op Nil : List
op Not__ : Boolean -> Boolean
op RS : Char
op SI : Char
op SO : Char
op SOH : Char
op SP : Char
op SUB : Char
op SYN : Char
op SYX : Char
op True : Boolean
op US : Char
op VT : Char
op __! : Nat -> Nat
op __*__ : Int * Int -> Int
op __*__ : Nat * Nat -> Nat
op __*__ : Pos * Pos -> Pos
op __*__ : Rat * Rat -> Rat
op __*__ : s * s -> s
op __+__ : Int * Int -> Int
op __+__ : Nat * Nat -> Nat
op __+__ : Nat * Pos -> Pos
op __+__ : Pos * Nat -> Pos
op __+__ : Rat * Rat -> Rat
op __+__ : s * s -> s
op __+-*/\&=<>!?:.$@#^~�����������������|__ : s * s -> s
op __-__ : Int * Int -> Int
op __-__ : Nat * Nat -> Int
op __-__ : Rat * Rat -> Rat
op __-__ : s * s -> s
op __-?__ : Nat * Nat ->? Nat
op __/__ : Int * Pos -> Rat
op __/__ : s * s -> s
op __/__ : Rat * Rat ->? Rat
op __/?__ : Int * Int ->? Int
op __/?__ : Nat * Nat ->? Nat
op __@@__ : Nat * Nat -> Nat
op __@@__ : s * s -> s
op __And__ : Boolean * Boolean -> Boolean
op __Or__ : Boolean * Boolean -> Boolean
op __^__ : Int * Nat -> Int
op __^__ : Nat * Nat -> Nat
op __^__ : Rat * Int -> Rat
op __a : b
op __and'__ : s
op __div__ : Int * Int ->? Int
op __div__ : Nat * Nat ->? Nat
op __exp__ : s * s -> s
op __frac__ : s * s -> s
op __mod__ : Int * Int ->? Nat
op __mod__ : Nat * Nat ->? Nat
op __quot__ : Int * Int ->? Int
op __quot__ : Nat * Nat ->? Nat
op __rem__ : Int * Int ->? Int
op __rem__ : Nat * Nat ->? Nat
op __||__ : a * a -> a
op a : Data1
op a : b
op a : s
op a : s -> t
op abs : Int -> Nat
op abs : Nat -> Nat
op abs : Rat -> Rat
op b : Data1
op b : a
op b : s -> s
op b : s -> t
op c : Data1
op c : b
op c : d
op c : s
op c : t
op c : a -> s
op c : a * t * t * t -> s
op c : a * t * t * t * t -> s
op c : s * s -> s
op c : s * s * s -> s
op c : s * s * t -> s
op chr : Nat ->? Char
op d : t
op d : s -> t
op e : t
op f : s ->? s
op g : s -> t
op g : s ->? s
op max : Int * Int -> Int
op max : Nat * Nat -> Nat
op max : Rat * Rat -> Rat
op min : Int * Int -> Int
op min : Nat * Nat -> Nat
op min : Rat * Rat -> Rat
op ord : Char -> Nat
op pre : Nat ->? Nat
op sel1 : Data3 ->? Data1
op sel1 : Data4 ->? Data1
op sel2 : Data3 ->? Data2
op sel2 : Data4 ->? Data2
op sign : Int -> Int
op suc : Nat -> Nat
op suc : Nat -> Pos
op succ : nat -> nat
op {__} : s -> s
op {} : s
pred __<__ : Int * Int
pred __<__ : Nat * Nat
pred __<__ : Rat * Rat
pred __<__ : a * a
pred __<=__ : Int * Int
pred __<=__ : Nat * Nat
pred __<=__ : Rat * Rat
pred __>__ : Int * Int
pred __>__ : Nat * Nat
pred __>__ : Rat * Rat
pred __>=__ : Int * Int
pred __>=__ : Nat * Nat
pred __>=__ : Rat * Rat
pred a : ()
pred b : s
pred c : s * s
pred c : s * s * s
pred c : s * s * t
pred even : Int
pred even : Nat
pred isDigit : Char
pred isLetter : Char
pred isPrintable : Char
pred odd : Int
pred odd : Nat
pred p : ()
pred q : s,[ . forall v1: Nat . pre(suc(v1)) = v1,
. forall v1, v2: Nat . suc(v1) = suc(v2) <=> v1 = v2,
. forall v1: Nat . not 0 = suc(v1), . not def pre(0),
generated{sort Nat; op 0 : Nat; op suc : Nat -> Nat},
. forall v1: Nat . 0 <= v1, . forall v1: Nat . not suc(v1) <= 0,
. forall v1, v2: Nat . suc(v1) <= suc(v2) <=> v1 <= v2,
. forall v1, v2: Nat . v1 >= v2 <=> v2 <= v1,
. forall v1, v2: Nat . v1 < v2 <=> v1 <= v2 /\ not v1 = v2,
. forall v1, v2: Nat . v1 > v2 <=> v1 < v2,
. forall v1: Nat . 0 + v1 = v1,
. forall v1, v2: Nat . suc(v2) + v1 = suc(v2 + v1),
. forall v1: Nat . 0 * v1 = 0,
. forall v1, v2: Nat . suc(v2) * v1 = v2 * v1 + v1,
. forall v1: Nat . v1 ^ 0 = 1,
. forall v1, v2: Nat . v1 ^ suc(v2) = v1 * v1 ^ v2,
. forall v1, v2: Nat . min(v1, v2) = v1 when v1 <= v2 else v2,
. forall v1, v2: Nat . max(v1, v2) = v2 when v1 <= v2 else v1,
. forall v1: Nat . + v1 = v1, . forall v1: Nat . abs(v1) = v1,
. forall v1: Nat . odd(v1) <=> not even(v1), . even(0),
. forall v1: Nat . even(suc(v1)) <=> odd(v1), . 0 ! = 1,
. forall v1: Nat . suc(v1) ! = suc(v1) * v1 !,
. forall v1, v2, v3: Nat . v1 -? v2 = v3 <=> v1 = v3 + v2,
. forall v1: Nat . not def v1 /? 0,
. forall v1, v2, v3: Nat
. (v1 /? v2 = v3 <=> v1 = v3 * v2) if v2 > 0,
. forall v1, v2, v3: Nat
. v1 div v2 = v3 <=>
(exists v4: Nat . v1 = v2 * v3 + v4 /\ v4 < v2),
. forall v1, v2, v3: Nat
. v1 mod v2 = v3 <=>
(exists v4: Nat . v1 = v2 * v4 + v3 /\ v3 < v2),
. forall v1, v2: Nat . v1 quot v2 = v1 div v2,
. forall v1, v2: Nat . v1 rem v2 = v1 mod v2, . 1 = suc(0),
. 2 = suc(1), . 3 = suc(2), . 4 = suc(3), . 5 = suc(4),
. 6 = suc(5), . 7 = suc(6), . 8 = suc(7), . 9 = suc(8),
. forall v1, v2: Nat . v1 @@ v2 = v1 * suc(9) + v2,
. forall v1: Nat . v1 in Pos <=> v1 > 0,
. forall v1, v2: Nat . min(v1, v2) = min(v2, v1),
. forall v1, v2: Nat . max(v1, v2) = max(v2, v1),
. forall v1, v2, v3: Nat
. min(v1, min(v2, v3)) = min(min(v1, v2), v3),
. forall v1, v2, v3: Nat
. max(v1, max(v2, v3)) = max(max(v1, v2), v3),
. forall v1, v2: Nat . def v1 -? v2 <=> v1 >= v2,
. forall v1, v2: Nat . def v1 /? v2 <=> v1 mod v2 = 0,
. forall v1, v2: Nat . def v1 div v2 <=> not v2 = 0,
. forall v1, v2: Nat . def v1 mod v2 <=> not v2 = 0,
. forall v1, v2: Nat . def v1 quot v2 <=> not v2 = 0,
. forall v1, v2: Nat . def v1 rem v2 <=> not v2 = 0,
. forall v1, v2, v3: Nat . (v1 + v2) * v3 = v1 * v3 + v2 * v3,
. forall v1: Nat . max(v1, 0) = v1,
. forall v1: Nat . min(v1, 0) = 0,
generated{sort Int; op __-__ : Nat * Nat -> Int},
. forall v1, v2, v3, v4: Nat
. v1 - v2 = v3 - v4 <=> v1 + v4 = v3 + v2,
. forall v1: Nat . v1 = v1 - 0,
. forall v1, v2, v3, v4: Nat
. (v1 - v2) + (v3 - v4) = (v1 + v3) - (v2 + v4),
. forall v1, v2, v3, v4: Nat
. (v1 - v2) * (v3 - v4) =
(v1 * v3 + v2 * v4) - (v2 * v3 + v1 * v4),
. forall v1, v2: Int . v1 - v2 = v1 + - v2,
. forall v1: Int . + v1 = v1,
. forall v1, v2: Nat . - (v1 - v2) = v2 - v1,
. forall v1: Int
. sign(v1) = 0 when v1 = 0 else 1 when v1 > 0 else - 1,
. forall v1, v2: Int . v1 <= v2 <=> v2 - v1 in Nat,
. forall v1, v2: Int . v1 >= v2 <=> v2 <= v1,
. forall v1, v2: Int . v1 < v2 <=> v1 <= v2 /\ not v1 = v2,
. forall v1, v2: Int . v1 > v2 <=> v1 < v2,
. forall v1, v2: Int . min(v1, v2) = v1 when v1 <= v2 else v2,
. forall v1, v2: Int . max(v1, v2) = v2 when v1 <= v2 else v1,
. forall v1: Int . abs(v1) = - v1 if v1 < 0,
. forall v1: Nat . - 1 ^ v1 = 1 when even(v1) else - 1,
. forall v1: Int; v2: Nat
. v1 ^ v2 = sign(v1) ^ v2 * abs(v1) ^ v2,
. forall v1: Int . even(v1) <=> even(abs(v1)),
. forall v1: Int . odd(v1) <=> not even(v1),
. forall v1, v2: Int
. v1 /? v2 = sign(v1) * sign(v2) * (abs(v1) /? abs(v2)),
. forall v1, v2: Int . (v1 mod v2) < abs(v2) if not v2 = 0,
. forall v1, v2: Int
. v1 = (v1 div v2) * v2 + (v1 mod v2) if not v2 = 0,
. forall v1: Int . not def v1 mod 0,
. forall v1: Int . not def v1 div 0,
. forall v1, v2: Int
. v1 quot v2 = sign(v1) * sign(v2) * (abs(v1) quot abs(v2)),
. forall v1, v2: Int
. v1 rem v2 = sign(v1) * sign(v2) * (abs(v1) rem abs(v2)),
. forall v1, v2: Nat . def v1 -? v2 => v1 -? v2 = v1 - v2,
. forall v1: Int . v1 = sign(v1) * abs(v1),
. forall v1: Int . odd(v1) <=> odd(abs(v1)),
. forall v1, v2, v3: Int
. v1 /? v2 = v3 <=> not v2 = 0 /\ v2 * v3 = v2,
. forall v1, v2: Int . def v1 /? v2 <=> v1 mod v2 = 0,
. forall v1, v2: Int . def v1 mod v2 <=> not v2 = 0,
. forall v1, v2: Int . v1 mod v2 = v1 mod abs(v2),
. forall v1, v2: Int . def v1 div v2 <=> not v2 = 0,
. forall v1, v2: Int . def v1 quot v2 <=> not v2 = 0,
. forall v1, v2: Int . def v1 rem v2 <=> not v2 = 0,
. forall v1, v2: Int
. v1 = (v1 quot v2) * v2 + (v1 rem v2) if not v2 = 0,
generated{sort Rat; op __/__ : Int * Pos -> Rat},
. forall v1, v2: Int; v3, v4: Pos
. v1 / v3 = v2 / v4 <=> v1 * v4 = v2 * v3,
. forall v1: Int . v1 / 1 = v1,
. forall v1, v2: Pos; v3, v4: Int
. (v3 / v1) <= (v4 / v2) <=> (v3 * v2) <= (v4 * v1),
. forall v1, v2: Rat . v1 >= v2 <=> v2 <= v1,
. forall v1, v2: Rat . v1 < v2 <=> v1 <= v2 /\ not v1 = v2,
. forall v1, v2: Rat . v1 > v2 <=> v2 < v1,
. forall v1, v2: Pos; v3, v4: Int
. (v3 / v1) + (v4 / v2) = (v3 * v2 + v4 * v1) / (v1 * v2),
. forall v1, v2: Rat . v1 - v2 = v1 + - v2,
. forall v1, v2: Pos; v3, v4: Int
. (v3 / v1) * (v4 / v2) = (v3 * v4) / (v1 * v2),
. forall v1: Rat . not def v1 / 0,
. forall v1, v2, v3: Rat
. (v1 / v2 = v3 <=> v3 = v1 * v2) if not v2 = 0,
. forall v1: Rat . + v1 = v1,
. forall v1: Pos; v2: Int . - (v2 / v1) = - v2 / v1,
. forall v1: Pos; v2: Int . abs(v2 / v1) = abs(v2) / v1,
. forall v1: Rat . v1 ^ 0 = 1,
. forall v1: Nat; v2: Rat . v2 ^ suc(v1) = v2 * v2 ^ v1,
. forall v1: Pos; v2: Rat . v2 ^ - v1 = 1 / (v2 ^ v1),
. forall v1, v2: Rat . min(v1, v2) = v1 when v1 <= v2 else v2,
. forall v1, v2: Rat . max(v1, v2) = v2 when v1 <= v2 else v1,
. forall v1, v2: Int; v3, v4: Pos
. (v1 / v3) / (v2 / v4) = (v1 / v3) * (v4 / v2) if not v2 = 0,
. forall v1: s . v1 = v1, . forall v1: s . v1 = v1,
. forall v1: s . v1 = v1, . forall v1: s . v1 = v1,
. forall v1: s . v1 = v1, . forall v1: s . v1 = v1,
. forall v1: s . v1 = v1, . forall v1: s . v1 = v1,
. forall v1: a; v2, v3, v4, v5: t . a(c(v1, v2, v3, v4, v5)) = v2,
. forall v1: a; v2, v3, v4, v5: t . b(c(v1, v2, v3, v4, v5)) = v3,
. forall v1: a; v2, v3, v4, v5: t . a(c(v1, v2, v3, v4, v5)) = v4,
. forall v1: a; v2, v3, v4, v5: t . d(c(v1, v2, v3, v4, v5)) = v5,
. forall v1: a; v2, v3, v4: t . a(c(v1, v2, v3, v4)) = v2,
. forall v1: a; v2, v3, v4: t . b(c(v1, v2, v3, v4)) = v3,
. forall v1: a; v2, v3, v4: t . d(c(v1, v2, v3, v4)) = v4,
. forall v1: a; v2, v3, v4: t; v5: a; v6, v7, v8: t
. c(v1, v2, v3, v4) = c(v5, v6, v7, v8) <=>
v1 = v5 /\ v2 = v6 /\ v3 = v7 /\ v4 = v8,
. forall v1, v2: a . c(v1) = c(v2) <=> v1 = v2,
. forall v1: s . not (v1 in s2 /\ v1 in s1), . not c: s in s2,
. not c: s in s1,
. forall v1: a; v2, v3, v4: t . not c(v1, v2, v3, v4) in s2,
. forall v1: a; v2, v3, v4: t . not c(v1, v2, v3, v4) in s1,
. forall v1: a . not c(v1) in s2,
. forall v1: a . not c(v1) in s1,
. forall v1: a; v2, v3, v4: t . not c = c(v1, v2, v3, v4),
. forall v1: a . not c = c(v1),
. forall v1: a; v2, v3, v4: t; v5: a
. not c(v1, v2, v3, v4) = c(v5),
. not def a(c), . forall v1: a . not def a(c(v1)),
. not def b(c), . forall v1: a . not def b(c(v1)),
. not def d(c), . forall v1: a . not def d(c(v1)),
generated{sort s; op c : s; op c : a ->? s;
op c : a * t * t * t -> s; op g__inj : s1 -> s;
op g__inj : s2 -> s},
. forall v1: a; v2, v3, v4: t . a(c(v1, v2, v3, v4)) = v2,
. forall v1: a; v2, v3, v4: t . b(c(v1, v2, v3, v4)) = v3,
. forall v1: a; v2, v3, v4: t . d(c(v1, v2, v3, v4)) = v4,
generated{sort s; op c : s; op c : a ->? s;
op c : a * t * t * t -> s; op g__inj : s1 -> s;
op g__inj : s2 -> s},
. forall v1: a; v2, v3, v4: t . a(c(v1, v2, v3, v4)) = v2,
. forall v1: a; v2, v3, v4: t . b(c(v1, v2, v3, v4)) = v3,
. forall v1: a; v2, v3, v4: t . d(c(v1, v2, v3, v4)) = v4,
generated{sort s, t; op c : s; op c : a ->? s;
op c : a * t * t * t -> s; op g__inj : s1 -> s;
op g__inj : s2 -> s; op g__inj : t -> s},
. true, . true, . forall v1: b . v1 in a <=> true,
. forall v1, v2, v3: s . c(v1, c(v2, v3)) = c(c(v1, v2), v3),
. forall v1, v2: s . c(v1, v2) = c(v2, v1),
. forall v1: s . c(v1, v1) = v1, . forall v1: s . c(v1, a) = v1,
. forall v1: s . c(a, v1) = v1,
. forall v1, v2, v3: s . c(v1, c(v2, v3)) = c(c(v1, v2), v3),
. forall v1, v2: s . c(v1, v2) = c(v2, v1),
. forall v1: s . c(v1, v1) = v1, . forall v1: s . c(v1, a) = v1,
. forall v1: s . c(a, v1) = v1, . a: s = a: s,
. forall v1, v2: s; v3: t . c(v1, v2, v3) = a, . a: s = a: s,
. forall v1, v2: s; v3: t . c(v1, v2, v3) = a,
. forall v1, v2: s; v3: t . c(v1, v2, v3) <=> false,
. forall v1: Data1; v2: Data2 . sel1(Cons31(v1, v2)) = v1,
. forall v1: Data1; v2: Data2 . sel2(Cons31(v1, v2)) = v2,
. forall v1: Data2; v2: Data1 . sel2(Cons32(v1, v2)) = v1,
. forall v1: Data2; v2: Data1 . sel1(Cons32(v1, v2)) = v2,
. forall v1: Data1; v2: Data2 . sel1(Cons41(v1, v2)) = v1,
. forall v1: Data1; v2: Data2 . sel2(Cons41(v1, v2)) = v2,
. forall v1: Data2; v2: Data1 . sel2(Cons42(v1, v2)) = v1,
. forall v1: Data2; v2: Data1 . sel1(Cons42(v1, v2)) = v2,
. forall v1: Data1; v2: List; v3: Data1; v4: List
. Cons(v1, v2) = Cons(v3, v4) <=> v1 = v3 /\ v2 = v4,
. forall v1: Data1; v2: List . not Nil = Cons(v1, v2),
generated{sort List; op Cons : Data1 * List -> List;
op Nil : List},
generated{sort Set; op Add : Data1 * Set -> Set; op Mt : Set},
generated{sort Set; op Add : Data1 * Set -> Set; op Mt : Set},
generated{sort nat; op 0 : nat; op succ : nat -> nat}, . false,
. true, . forall v1: s . not p /\ not q(v1) /\ q(v1),
. forall v1: s . not p \/ not q(v1) \/ q(v1),
. forall v1: s
. not p /\ not q(v1) /\ q(v1) =>
not p \/ not q(v1) \/ q(v1) => not p /\ not q(v1) /\ q(v1),
. forall v1: s
. not p /\ not q(v1) /\ q(v1) if not p \/ not q(v1) \/ q(v1) if
not p /\ not q(v1) /\ q(v1),
. forall v1: s
. not p /\ not q(v1) /\ q(v1) <=>
(exists v2: s
. not p \/ not q(v2) \/ q(v2) <=>
(exists! v3: s . not p /\ not q(v3) /\ q(v3))),
. forall v1: s . def f(v1), . forall v1: s . f(v1) =e= g(v1),
. forall v1: s . f(v1) = g(v1), . forall v1: t . v1 in s,
. forall v1: s . def g(v1), . forall v1: s . def g(v1),
. forall v1: s . def f(v1), . forall v1: s . def g(v1), . p,
. forall v1: s . q(v1),
. forall v1, v2, v3: s . def v3 * v1 * v2 + v2 * v1 * v3,
. def {}, . forall v1: s . def { v1 }, . true,
. not True = False,
generated{sort Boolean; op False : Boolean; op True : Boolean},
. Not False = True, . Not True = False,
. False And False = False, . False And True = False,
. True And False = False, . True And True = True,
. forall v1, v2: Boolean . v1 Or v2 = Not (Not v1 And Not v2),
. forall v1: Nat . def chr(v1) <=> v1 <= 255,
. forall v1: Char . chr(ord(v1)) = v1,
. forall v1: Nat . ord(chr(v1)) = v1 if v1 <= 255,
. '\000' = chr(0), . '\001' = chr(1), . '\002' = chr(2),
. '\003' = chr(3), . '\004' = chr(4), . '\005' = chr(5),
. '\006' = chr(6), . '\007' = chr(7), . '\008' = chr(8),
. '\009' = chr(9), . '\010' = chr(10),
. '\011' = chr(1: Nat @@ 1: Nat),
. '\012' = chr(1: Nat @@ 2: Nat),
. '\013' = chr(1: Nat @@ 3: Nat),
. '\014' = chr(1: Nat @@ 4: Nat), . '\015' = chr(15),
. '\016' = chr(16), . '\017' = chr(17), . '\018' = chr(18),
. '\019' = chr(19), . '\020' = chr(20),
. '\021' = chr(2: Nat @@ 1: Nat),
. '\022' = chr(2: Nat @@ 2: Nat),
. '\023' = chr(2: Nat @@ 3: Nat),
. '\024' = chr(2: Nat @@ 4: Nat), . '\025' = chr(25),
. '\026' = chr(26), . '\027' = chr(27), . '\028' = chr(28),
. '\029' = chr(29), . '\030' = chr(30),
. '\031' = chr(3: Nat @@ 1: Nat),
. '\032' = chr(3: Nat @@ 2: Nat),
. '\033' = chr(3: Nat @@ 3: Nat),
. '\034' = chr(3: Nat @@ 4: Nat), . '\035' = chr(35),
. '\036' = chr(36), . '\037' = chr(37), . '\038' = chr(38),
. '\039' = chr(39), . '\040' = chr(40),
. '\041' = chr(4: Nat @@ 1: Nat),
. '\042' = chr(4: Nat @@ 2: Nat),
. '\043' = chr(4: Nat @@ 3: Nat),
. '\044' = chr(4: Nat @@ 4: Nat), . '\045' = chr(45),
. '\046' = chr(46), . '\047' = chr(47), . '\048' = chr(48),
. '\049' = chr(49), . '\050' = chr(50), . '\051' = chr(51),
. '\052' = chr(52), . '\053' = chr(53), . '\054' = chr(54),
. '\055' = chr(55), . '\056' = chr(56), . '\057' = chr(57),
. '\058' = chr(58), . '\059' = chr(59), . '\060' = chr(60),
. '\061' = chr(61), . '\062' = chr(62), . '\063' = chr(63),
. '\064' = chr(64), . '\065' = chr(65), . '\066' = chr(66),
. '\067' = chr(67), . '\068' = chr(68), . '\069' = chr(69),
. '\070' = chr(70), . '\071' = chr(71), . '\072' = chr(72),
. '\073' = chr(73), . '\074' = chr(74), . '\075' = chr(75),
. '\076' = chr(76), . '\077' = chr(77), . '\078' = chr(78),
. '\079' = chr(79), . '\080' = chr(80), . '\081' = chr(81),
. '\082' = chr(82), . '\083' = chr(83), . '\084' = chr(84),
. '\085' = chr(85), . '\086' = chr(86), . '\087' = chr(87),
. '\088' = chr(88), . '\089' = chr(89), . '\090' = chr(90),
. '\091' = chr(91), . '\092' = chr(92), . '\093' = chr(93),
. '\094' = chr(94), . '\095' = chr(95), . '\096' = chr(96),
. '\097' = chr(97), . '\098' = chr(98), . '\099' = chr(99),
. '\100' = chr(100), . '\101' = chr(101), . '\102' = chr(102),
. '\103' = chr(103), . '\104' = chr(104), . '\105' = chr(105),
. '\106' = chr(106), . '\107' = chr(107), . '\108' = chr(108),
. '\109' = chr(109), . '\110' = chr(110),
. '\111' = chr(1 @@ (1: Nat @@ 1: Nat)),
. '\112' = chr(1 @@ (1: Nat @@ 2: Nat)),
. '\113' = chr(1 @@ (1: Nat @@ 3: Nat)),
. '\114' = chr(1 @@ (1: Nat @@ 4: Nat)), . '\115' = chr(115),
. '\116' = chr(116), . '\117' = chr(117), . '\118' = chr(118),
. '\119' = chr(119), . '\120' = chr(120),
. '\121' = chr(1 @@ (2: Nat @@ 1: Nat)),
. '\122' = chr(1 @@ (2: Nat @@ 2: Nat)),
. '\123' = chr(1 @@ (2: Nat @@ 3: Nat)),
. '\124' = chr(1 @@ (2: Nat @@ 4: Nat)), . '\125' = chr(125),
. '\126' = chr(126), . '\127' = chr(127), . '\128' = chr(128),
. '\129' = chr(129), . '\130' = chr(130),
. '\131' = chr(1 @@ (3: Nat @@ 1: Nat)),
. '\132' = chr(1 @@ (3: Nat @@ 2: Nat)),
. '\133' = chr(1 @@ (3: Nat @@ 3: Nat)),
. '\134' = chr(1 @@ (3: Nat @@ 4: Nat)), . '\135' = chr(135),
. '\136' = chr(136), . '\137' = chr(137), . '\138' = chr(138),
. '\139' = chr(139), . '\140' = chr(140),
. '\141' = chr(1 @@ (4: Nat @@ 1: Nat)),
. '\142' = chr(1 @@ (4: Nat @@ 2: Nat)),
. '\143' = chr(1 @@ (4: Nat @@ 3: Nat)),
. '\144' = chr(1 @@ (4: Nat @@ 4: Nat)), . '\145' = chr(145),
. '\146' = chr(146), . '\147' = chr(147), . '\148' = chr(148),
. '\149' = chr(149), . '\150' = chr(150), . '\151' = chr(151),
. '\152' = chr(152), . '\153' = chr(153), . '\154' = chr(154),
. '\155' = chr(155), . '\156' = chr(156), . '\157' = chr(157),
. '\158' = chr(158), . '\159' = chr(159), . '\160' = chr(160),
. '\161' = chr(161), . '\162' = chr(162), . '\163' = chr(163),
. '\164' = chr(164), . '\165' = chr(165), . '\166' = chr(166),
. '\167' = chr(167), . '\168' = chr(168), . '\169' = chr(169),
. '\170' = chr(170), . '\171' = chr(171), . '\172' = chr(172),
. '\173' = chr(173), . '\174' = chr(174), . '\175' = chr(175),
. '\176' = chr(176), . '\177' = chr(177), . '\178' = chr(178),
. '\179' = chr(179), . '\180' = chr(180), . '\181' = chr(181),
. '\182' = chr(182), . '\183' = chr(183), . '\184' = chr(184),
. '\185' = chr(185), . '\186' = chr(186), . '\187' = chr(187),
. '\188' = chr(188), . '\189' = chr(189), . '\190' = chr(190),
. '\191' = chr(191), . '\192' = chr(192), . '\193' = chr(193),
. '\194' = chr(194), . '\195' = chr(195), . '\196' = chr(196),
. '\197' = chr(197), . '\198' = chr(198), . '\199' = chr(199),
. '\200' = chr(200), . '\201' = chr(201), . '\202' = chr(202),
. '\203' = chr(203), . '\204' = chr(204), . '\205' = chr(205),
. '\206' = chr(206), . '\207' = chr(207), . '\208' = chr(208),
. '\209' = chr(209), . '\210' = chr(210),
. '\211' = chr(2 @@ (1: Nat @@ 1: Nat)),
. '\212' = chr(2 @@ (1: Nat @@ 2: Nat)),
. '\213' = chr(2 @@ (1: Nat @@ 3: Nat)),
. '\214' = chr(2 @@ (1: Nat @@ 4: Nat)), . '\215' = chr(215),
. '\216' = chr(216), . '\217' = chr(217), . '\218' = chr(218),
. '\219' = chr(219), . '\220' = chr(220),
. '\221' = chr(2 @@ (2: Nat @@ 1: Nat)),
. '\222' = chr(2 @@ (2: Nat @@ 2: Nat)),
. '\223' = chr(2 @@ (2: Nat @@ 3: Nat)),
. '\224' = chr(2 @@ (2: Nat @@ 4: Nat)), . '\225' = chr(225),
. '\226' = chr(226), . '\227' = chr(227), . '\228' = chr(228),
. '\229' = chr(229), . '\230' = chr(230),
. '\231' = chr(2 @@ (3: Nat @@ 1: Nat)),
. '\232' = chr(2 @@ (3: Nat @@ 2: Nat)),
. '\233' = chr(2 @@ (3: Nat @@ 3: Nat)),
. '\234' = chr(2 @@ (3: Nat @@ 4: Nat)), . '\235' = chr(235),
. '\236' = chr(236), . '\237' = chr(237), . '\238' = chr(238),
. '\239' = chr(239), . '\240' = chr(240),
. '\241' = chr(2 @@ (4: Nat @@ 1: Nat)),
. '\242' = chr(2 @@ (4: Nat @@ 2: Nat)),
. '\243' = chr(2 @@ (4: Nat @@ 3: Nat)),
. '\244' = chr(2 @@ (4: Nat @@ 4: Nat)), . '\245' = chr(245),
. '\246' = chr(246), . '\247' = chr(247), . '\248' = chr(248),
. '\249' = chr(249), . '\250' = chr(250), . '\251' = chr(251),
. '\252' = chr(252), . '\253' = chr(253), . '\254' = chr(254),
. '\255' = chr(255), . ' ' = '\032', . '!' = '\033',
. '\"' = '\034', . '#' = '\035', . '$' = '\036',
. '%' = '\037', . '&' = '\038', . '\'' = '\039',
. '(' = '\040', . ')' = '\041', . '*' = '\042', . '+' = '\043',
. ',' = '\044', . '-' = '\045', . '.' = '\046', . '/' = '\047',
. '0' = '\048', . '1' = '\049', . '2' = '\050', . '3' = '\051',
. '4' = '\052', . '5' = '\053', . '6' = '\054', . '7' = '\055',
. '8' = '\056', . '9' = '\057', . ':' = '\058', . ';' = '\059',
. '<' = '\060', . '=' = '\061', . '>' = '\062', . '?' = '\063',
. '@' = '\064', . 'A' = '\065', . 'B' = '\066', . 'C' = '\067',
. 'D' = '\068', . 'E' = '\069', . 'F' = '\070', . 'G' = '\071',
. 'H' = '\072', . 'I' = '\073', . 'J' = '\074', . 'K' = '\075',
. 'L' = '\076', . 'M' = '\077', . 'N' = '\078', . 'O' = '\079',
. 'P' = '\080', . 'Q' = '\081', . 'R' = '\082', . 'S' = '\083',
. 'T' = '\084', . 'U' = '\085', . 'V' = '\086', . 'W' = '\087',
. 'X' = '\088', . 'Y' = '\089', . 'Z' = '\090', . '[' = '\091',
. '\\' = '\092', . ']' = '\093', . '^' = '\094',
. '_' = '\095', . '`' = '\096', . 'a' = '\097', . 'b' = '\098',
. 'c' = '\099', . 'd' = '\100', . 'e' = '\101', . 'f' = '\102',
. 'g' = '\103', . 'h' = '\104', . 'i' = '\105', . 'j' = '\106',
. 'k' = '\107', . 'l' = '\108', . 'm' = '\109', . 'n' = '\110',
. 'o' = '\111', . 'p' = '\112', . 'q' = '\113', . 'r' = '\114',
. 's' = '\115', . 't' = '\116', . 'u' = '\117', . 'v' = '\118',
. 'w' = '\119', . 'x' = '\120', . 'y' = '\121', . 'z' = '\122',
. '{' = '\123', . '|' = '\124', . '}' = '\125', . '~' = '\126',
. ' ' = '\160', . '�' = '\161', . '�' = '\162', . '�' = '\163',
. '�' = '\164', . '�' = '\165', . '�' = '\166', . '�' = '\167',
. '�' = '\168', . '�' = '\169', . '�' = '\170', . '�' = '\171',
. '�' = '\172', . '�' = '\173', . '�' = '\174', . '�' = '\175',
. '�' = '\176', . '�' = '\177', . '�' = '\178', . '�' = '\179',
. '�' = '\180', . '�' = '\181', . '�' = '\182', . '�' = '\183',
. '�' = '\184', . '�' = '\185', . '�' = '\186', . '�' = '\187',
. '�' = '\188', . '�' = '\189', . '�' = '\190', . '�' = '\191',
. '�' = '\192', . '�' = '\193', . '�' = '\194', . '�' = '\195',
. '�' = '\196', . '�' = '\197', . '�' = '\198', . '�' = '\199',
. '�' = '\200', . '�' = '\201', . '�' = '\202', . '�' = '\203',
. '�' = '\204', . '�' = '\205', . '�' = '\206', . '�' = '\207',
. '�' = '\208', . '�' = '\209', . '�' = '\210', . '�' = '\211',
. '�' = '\212', . '�' = '\213', . '�' = '\214', . '�' = '\215',
. '�' = '\216', . '�' = '\217', . '�' = '\218', . '�' = '\219',
. '�' = '\220', . '�' = '\221', . '�' = '\222', . '�' = '\223',
. '�' = '\224', . '�' = '\225', . '�' = '\226', . '�' = '\227',
. '�' = '\228', . '�' = '\229', . '�' = '\230', . '�' = '\231',
. '�' = '\232', . '�' = '\233', . '�' = '\234', . '�' = '\235',
. '�' = '\236', . '�' = '\237', . '�' = '\238', . '�' = '\239',
. '�' = '\240', . '�' = '\241', . '�' = '\242', . '�' = '\243',
. '�' = '\244', . '�' = '\245', . '�' = '\246', . '�' = '\247',
. '�' = '\248', . '�' = '\249', . '�' = '\250', . '�' = '\251',
. '�' = '\252', . '�' = '\253', . '�' = '\254', . '�' = '\255',
. forall v1: Char
. isLetter(v1) <=>
(ord('A') <= ord(v1) /\ ord(v1) <= ord('Z'))
\/ (ord('a') <= ord(v1) /\ ord(v1) <= ord('z')),
. forall v1: Char
. isDigit(v1) <=> ord('0') <= ord(v1) /\ ord(v1) <= ord('9'),
. forall v1: Char
. isPrintable(v1) <=>
(ord(' ') <= ord(v1) /\ ord(v1) <= ord('~'))
\/ (ord(' ') <= ord(v1) /\ ord(v1) <= ord('�')),
. '\o000': Char = '\000': Char, . '\o001' = '\001',
. '\o002' = '\002', . '\o003' = '\003', . '\o004' = '\004',
. '\o005' = '\005', . '\o006' = '\006', . '\o007' = '\007',
. '\o010' = '\008', . '\o011' = '\009', . '\o012' = '\010',
. '\o013' = '\011', . '\o014' = '\012', . '\o015' = '\013',
. '\o016' = '\014', . '\o017' = '\015', . '\o020' = '\016',
. '\o021' = '\017', . '\o022' = '\018', . '\o023' = '\019',
. '\o024' = '\020', . '\o025' = '\021', . '\o026' = '\022',
. '\o027' = '\023', . '\o030' = '\024', . '\o031' = '\025',
. '\o032' = '\026', . '\o033' = '\027', . '\o034' = '\028',
. '\o035' = '\029', . '\o036' = '\030', . '\o037' = '\031',
. '\o040' = '\032', . '\o041' = '\033', . '\o042' = '\034',
. '\o043' = '\035', . '\o044' = '\036', . '\o045' = '\037',
. '\o046' = '\038', . '\o047' = '\039', . '\o050' = '\040',
. '\o051' = '\041', . '\o052' = '\042', . '\o053' = '\043',
. '\o054' = '\044', . '\o055' = '\045', . '\o056' = '\046',
. '\o057' = '\047', . '\o060' = '\048', . '\o061' = '\049',
. '\o062' = '\050', . '\o063' = '\051', . '\o064' = '\052',
. '\o065' = '\053', . '\o066' = '\054', . '\o067' = '\055',
. '\o070' = '\056', . '\o071' = '\057', . '\o072' = '\058',
. '\o073' = '\059', . '\o074' = '\060', . '\o075' = '\061',
. '\o076' = '\062', . '\o077' = '\063', . '\o100' = '\064',
. '\o101' = '\065', . '\o102' = '\066', . '\o103' = '\067',
. '\o104' = '\068', . '\o105' = '\069', . '\o106' = '\070',
. '\o107' = '\071', . '\o110' = '\072', . '\o111' = '\073',
. '\o112' = '\074', . '\o113' = '\075', . '\o114' = '\076',
. '\o115' = '\077', . '\o116' = '\078', . '\o117' = '\079',
. '\o120' = '\080', . '\o121' = '\081', . '\o122' = '\082',
. '\o123' = '\083', . '\o124' = '\084', . '\o125' = '\085',
. '\o126' = '\086', . '\o127' = '\087', . '\o130' = '\088',
. '\o131' = '\089', . '\o132' = '\090', . '\o133' = '\091',
. '\o134' = '\092', . '\o135' = '\093', . '\o136' = '\094',
. '\o137' = '\095', . '\o140' = '\096', . '\o141' = '\097',
. '\o142' = '\098', . '\o143' = '\099', . '\o144' = '\100',
. '\o145' = '\101', . '\o146' = '\102', . '\o147' = '\103',
. '\o150' = '\104', . '\o151' = '\105', . '\o152' = '\106',
. '\o153' = '\107', . '\o154' = '\108', . '\o155' = '\109',
. '\o156' = '\110', . '\o157' = '\111', . '\o160' = '\112',
. '\o161' = '\113', . '\o162' = '\114', . '\o163' = '\115',
. '\o164' = '\116', . '\o165' = '\117', . '\o166' = '\118',
. '\o167' = '\119', . '\o170' = '\120', . '\o171' = '\121',
. '\o172' = '\122', . '\o173' = '\123', . '\o174' = '\124',
. '\o175' = '\125', . '\o176' = '\126', . '\o177' = '\127',
. '\o200' = '\128', . '\o201' = '\129', . '\o202' = '\130',
. '\o203' = '\131', . '\o204' = '\132', . '\o205' = '\133',
. '\o206' = '\134', . '\o207' = '\135', . '\o210' = '\136',
. '\o211' = '\137', . '\o212' = '\138', . '\o213' = '\139',
. '\o214' = '\140', . '\o215' = '\141', . '\o216' = '\142',
. '\o217' = '\143', . '\o220' = '\144', . '\o221' = '\145',
. '\o222' = '\146', . '\o223' = '\147', . '\o224' = '\148',
. '\o225' = '\149', . '\o226' = '\150', . '\o227' = '\151',
. '\o230' = '\152', . '\o231' = '\153', . '\o232' = '\154',
. '\o233' = '\155', . '\o234' = '\156', . '\o235' = '\157',
. '\o236' = '\158', . '\o237' = '\159', . '\o240' = '\160',
. '\o241' = '\161', . '\o242' = '\162', . '\o243' = '\163',
. '\o244' = '\164', . '\o245' = '\165', . '\o246' = '\166',
. '\o247' = '\167', . '\o250' = '\168', . '\o251' = '\169',
. '\o252' = '\170', . '\o253' = '\171', . '\o254' = '\172',
. '\o255' = '\173', . '\o256' = '\174', . '\o257' = '\175',
. '\o260' = '\176', . '\o261' = '\177', . '\o262' = '\178',
. '\o263' = '\179', . '\o264' = '\180', . '\o265' = '\181',
. '\o266' = '\182', . '\o267' = '\183', . '\o270' = '\184',
. '\o271' = '\185', . '\o272' = '\186', . '\o273' = '\187',
. '\o274' = '\188', . '\o275' = '\189', . '\o276' = '\190',
. '\o277' = '\191', . '\o300' = '\192', . '\o301' = '\193',
. '\o302' = '\194', . '\o303' = '\195', . '\o304' = '\196',
. '\o305' = '\197', . '\o306' = '\198', . '\o307' = '\199',
. '\o310' = '\200', . '\o311' = '\201', . '\o312' = '\202',
. '\o313' = '\203', . '\o314' = '\204', . '\o315' = '\205',
. '\o316' = '\206', . '\o317' = '\207', . '\o320' = '\208',
. '\o321' = '\209', . '\o322' = '\210', . '\o323' = '\211',
. '\o324' = '\212', . '\o325' = '\213', . '\o326' = '\214',
. '\o327' = '\215', . '\o330' = '\216', . '\o331' = '\217',
. '\o332' = '\218', . '\o333' = '\219', . '\o334' = '\220',
. '\o335' = '\221', . '\o336' = '\222', . '\o337' = '\223',
. '\o340' = '\224', . '\o341' = '\225', . '\o342' = '\226',
. '\o343' = '\227', . '\o344' = '\228', . '\o345' = '\229',
. '\o346' = '\230', . '\o347' = '\231', . '\o350' = '\232',
. '\o351' = '\233', . '\o352' = '\234', . '\o353' = '\235',
. '\o354' = '\236', . '\o355' = '\237', . '\o356' = '\238',
. '\o357' = '\239', . '\o360' = '\240', . '\o361' = '\241',
. '\o362' = '\242', . '\o363' = '\243', . '\o364' = '\244',
. '\o365' = '\245', . '\o366' = '\246', . '\o367' = '\247',
. '\o370' = '\248', . '\o371' = '\249', . '\o372' = '\250',
. '\o373' = '\251', . '\o374' = '\252', . '\o375' = '\253',
. '\o376' = '\254', . '\o377': Char = '\255': Char,
. '\x00': Char = '\000': Char, . '\x01' = '\001',
. '\x02' = '\002', . '\x03' = '\003', . '\x04' = '\004',
. '\x05' = '\005', . '\x06' = '\006', . '\x07' = '\007',
. '\x08' = '\008', . '\x09' = '\009', . '\x0A' = '\010',
. '\x0B' = '\011', . '\x0C' = '\012', . '\x0D' = '\013',
. '\x0E' = '\014', . '\x0F' = '\015', . '\x10' = '\016',
. '\x11' = '\017', . '\x12' = '\018', . '\x13' = '\019',
. '\x14' = '\020', . '\x15' = '\021', . '\x16' = '\022',
. '\x17' = '\023', . '\x18' = '\024', . '\x19' = '\025',
. '\x1A' = '\026', . '\x1B' = '\027', . '\x1C' = '\028',
. '\x1D' = '\029', . '\x1E' = '\030', . '\x1F' = '\031',
. '\x20' = '\032', . '\x21' = '\033', . '\x22' = '\034',
. '\x23' = '\035', . '\x24' = '\036', . '\x25' = '\037',
. '\x26' = '\038', . '\x27' = '\039', . '\x28' = '\040',
. '\x29' = '\041', . '\x2A' = '\042', . '\x2B' = '\043',
. '\x2C' = '\044', . '\x2D' = '\045', . '\x2E' = '\046',
. '\x2F' = '\047', . '\x30' = '\048', . '\x31' = '\049',
. '\x32' = '\050', . '\x33' = '\051', . '\x34' = '\052',
. '\x35' = '\053', . '\x36' = '\054', . '\x37' = '\055',
. '\x38' = '\056', . '\x39' = '\057', . '\x3A' = '\058',
. '\x3B' = '\059', . '\x3C' = '\060', . '\x3D' = '\061',
. '\x3E' = '\062', . '\x3F' = '\063', . '\x40' = '\064',
. '\x41' = '\065', . '\x42' = '\066', . '\x43' = '\067',
. '\x44' = '\068', . '\x45' = '\069', . '\x46' = '\070',
. '\x47' = '\071', . '\x48' = '\072', . '\x49' = '\073',
. '\x4A' = '\074', . '\x4B' = '\075', . '\x4C' = '\076',
. '\x4D' = '\077', . '\x4E' = '\078', . '\x4F' = '\079',
. '\x50' = '\080', . '\x51' = '\081', . '\x52' = '\082',
. '\x53' = '\083', . '\x54' = '\084', . '\x55' = '\085',
. '\x56' = '\086', . '\x57' = '\087', . '\x58' = '\088',
. '\x59' = '\089', . '\x5A' = '\090', . '\x5B' = '\091',
. '\x5C' = '\092', . '\x5D' = '\093', . '\x5E' = '\094',
. '\x5F' = '\095', . '\x60' = '\096', . '\x61' = '\097',
. '\x62' = '\098', . '\x63' = '\099', . '\x64' = '\100',
. '\x65' = '\101', . '\x66' = '\102', . '\x67' = '\103',
. '\x68' = '\104', . '\x69' = '\105', . '\x6A' = '\106',
. '\x6B' = '\107', . '\x6C' = '\108', . '\x6D' = '\109',
. '\x6E' = '\110', . '\x6F' = '\111', . '\x70' = '\112',
. '\x71' = '\113', . '\x72' = '\114', . '\x73' = '\115',
. '\x74' = '\116', . '\x75' = '\117', . '\x76' = '\118',
. '\x77' = '\119', . '\x78' = '\120', . '\x79' = '\121',
. '\x7A' = '\122', . '\x7B' = '\123', . '\x7C' = '\124',
. '\x7D' = '\125', . '\x7E' = '\126', . '\x7F' = '\127',
. '\x80' = '\128', . '\x81' = '\129', . '\x82' = '\130',
. '\x83' = '\131', . '\x84' = '\132', . '\x85' = '\133',
. '\x86' = '\134', . '\x87' = '\135', . '\x88' = '\136',
. '\x89' = '\137', . '\x8A' = '\138', . '\x8B' = '\139',
. '\x8C' = '\140', . '\x8D' = '\141', . '\x8E' = '\142',
. '\x8F' = '\143', . '\x90' = '\144', . '\x91' = '\145',
. '\x92' = '\146', . '\x93' = '\147', . '\x94' = '\148',
. '\x95' = '\149', . '\x96' = '\150', . '\x97' = '\151',
. '\x98' = '\152', . '\x99' = '\153', . '\x9A' = '\154',
. '\x9B' = '\155', . '\x9C' = '\156', . '\x9D' = '\157',
. '\x9E' = '\158', . '\x9F' = '\159', . '\xA0' = '\160',
. '\xA1' = '\161', . '\xA2' = '\162', . '\xA3' = '\163',
. '\xA4' = '\164', . '\xA5' = '\165', . '\xA6' = '\166',
. '\xA7' = '\167', . '\xA8' = '\168', . '\xA9' = '\169',
. '\xAA' = '\170', . '\xAB' = '\171', . '\xAC' = '\172',
. '\xAD' = '\173', . '\xAE' = '\174', . '\xAF' = '\175',
. '\xB0' = '\176', . '\xB1' = '\177', . '\xB2' = '\178',
. '\xB3' = '\179', . '\xB4' = '\180', . '\xB5' = '\181',
. '\xB6' = '\182', . '\xB7' = '\183', . '\xB8' = '\184',
. '\xB9' = '\185', . '\xBA' = '\186', . '\xBB' = '\187',
. '\xBC' = '\188', . '\xBD' = '\189', . '\xBE' = '\190',
. '\xBF' = '\191', . '\xC0' = '\192', . '\xC1' = '\193',
. '\xC2' = '\194', . '\xC3' = '\195', . '\xC4' = '\196',
. '\xC5' = '\197', . '\xC6' = '\198', . '\xC7' = '\199',
. '\xC8' = '\200', . '\xC9' = '\201', . '\xCA' = '\202',
. '\xCB' = '\203', . '\xCC' = '\204', . '\xCD' = '\205',
. '\xCE' = '\206', . '\xCF' = '\207', . '\xD0' = '\208',
. '\xD1' = '\209', . '\xD2' = '\210', . '\xD3' = '\211',
. '\xD4' = '\212', . '\xD5' = '\213', . '\xD6' = '\214',
. '\xD7' = '\215', . '\xD8' = '\216', . '\xD9' = '\217',
. '\xDA' = '\218', . '\xDB' = '\219', . '\xDC' = '\220',
. '\xDD' = '\221', . '\xDE' = '\222', . '\xDF' = '\223',
. '\xE0' = '\224', . '\xE1' = '\225', . '\xE2' = '\226',
. '\xE3' = '\227', . '\xE4' = '\228', . '\xE5' = '\229',
. '\xE6' = '\230', . '\xE7' = '\231', . '\xE8' = '\232',
. '\xE9' = '\233', . '\xEA' = '\234', . '\xEB' = '\235',
. '\xEC' = '\236', . '\xED' = '\237', . '\xEE' = '\238',
. '\xEF' = '\239', . '\xF0' = '\240', . '\xF1' = '\241',
. '\xF2' = '\242', . '\xF3' = '\243', . '\xF4' = '\244',
. '\xF5' = '\245', . '\xF6' = '\246', . '\xF7' = '\247',
. '\xF8' = '\248', . '\xF9' = '\249', . '\xFA' = '\250',
. '\xFB' = '\251', . '\xFC' = '\252', . '\xFD' = '\253',
. '\xFE' = '\254', . '\xFF': Char = '\255': Char,
. NUL = '\000', . SOH = '\001', . SYX = '\002', . ETX = '\003',
. EOT = '\004', . ENQ = '\005', . ACK = '\006', . BEL = '\007',
. BS = '\008', . HT = '\009', . LF = '\010', . VT = '\011',
. FF = '\012', . CR = '\013', . SO = '\014', . SI = '\015',
. DLE = '\016', . DC1 = '\017', . DC2 = '\018', . DC3 = '\019',
. DC4 = '\020', . NAK = '\021', . SYN = '\022', . ETB = '\023',
. CAN = '\024', . EM = '\025', . SUB = '\026', . ESC = '\027',
. FS = '\028', . GS = '\029', . RS = '\030', . US = '\031',
. SP = '\032', . DEL = '\127', . NL = LF, . NP = FF,
. '\n' = NL, . '\t' = HT, . '\v' = VT, . '\b' = BS,
. '\r' = CR, . '\f' = FF, . '\a' = BEL, . '\?' = '?',
. forall v1, v2, v3: a . v1 || (v2 || v3) = (v1 || v2) || v3,
. (b || b) || b = b ])
*** Hint 17.9, redeclared as total 'min'
*** Hint 17.14, redeclared as total 'max'
*** Error 90.19, no typing for: suc(0): Pos
*** Hint 98.10, redeclared op 'min'
*** Hint 98.15, redeclared op 'max'
*** Hint 121.18, redeclared sort 'Int'
*** Hint 121.12, redeclared sort 'Nat'
*** Hint 209.17, redeclared sort 'Rat'
*** Hint 209.11, redeclared sort 'Int'
*** Error 261.9-261.21, ambiguous mixfix term
__*__(i, __-__(q, __*__(j, p)))
__-__(__*__(i, q), __*__(j, p))
__*__(__*__(i, __-__(q, j)), p)
*** Error 266.16, unknown sort 'a'
*** Error 266.20, unknown sort 'a'
*** Error 268.9, unknown sort 'b'
*** Error 268.6, wrong number of places '__a'
*** Error 268.15, unknown sort 'b'
*** Hint 269.6, redeclared sort 's'
*** Warning 269.6, void reflexive subsort 's'
*** Error 270.3, no operation with 0 arguments found for 'a'
*** Warning 271.11, known variable shadowed 'a'
*** Warning 272.6, known variable shadowed 'a'
*** Warning 272.11, known variable shadowed 'a'
*** Warning 272.13, known variable shadowed 'b'
*** Warning 275.8, known variable shadowed 'a'
*** Warning 275.13, known variable shadowed 'a'
*** Warning 275.15, known variable shadowed 'b'
*** Hint 285.6, redeclared sort 's'
*** Error 285.17, unknown sort 's2'
*** Error 285.20, unknown sort 's1'
*** Error 285.31, unknown sort 'a'
*** Warning 285.34, also known as variable 'a'
*** Warning 285.36, also known as variable 'b'
*** Hint 285.41, redeclared op 'a'
*** Error 285.34, duplicates at '(285,41)' for 'a : s -> t'
*** Error 285.52, unknown sort 'a'
*** Error 285.25, total selectors 'a : s -> t,b : s -> t,d : s -> t'
must appear in alternative 'c : s'
*** Error 285.50, total selectors 'a : s -> t,b : s -> t,d : s -> t'
must appear in alternative 'c : a ->? s'
*** Hint 286.11, redeclared sort 's'
*** Error 286.22, unknown sort 's2'
*** Hint 286.22, redeclared subsort 's2 < s'
*** Error 286.25, unknown sort 's1'
*** Hint 286.25, redeclared subsort 's1 < s'
*** Hint 286.30, redeclared op 'c'
*** Error 286.36, unknown sort 'a'
*** Hint 286.39, redeclared op 'a'
*** Hint 286.41, redeclared op 'b'
*** Hint 286.46, redeclared op 'd'
*** Error 286.55, unknown sort 'a'
*** Hint 286.53, redeclared op 'c'
*** Error 286.30, total selectors 'a : s -> t,b : s -> t,d : s -> t'
must appear in alternative 'c : s'
*** Error 286.53, total selectors 'a : s -> t,b : s -> t,d : s -> t'
must appear in alternative 'c : a ->? s'
*** Hint 287.16, redeclared sort 's'
*** Error 287.27, unknown sort 's2'
*** Hint 287.27, redeclared subsort 's2 < s'
*** Error 287.30, unknown sort 's1'
*** Hint 287.30, redeclared subsort 's1 < s'
*** Hint 287.35, redeclared op 'c'
*** Error 287.41, unknown sort 'a'
*** Hint 287.39, redeclared op 'c'
*** Hint 287.44, redeclared op 'a'
*** Hint 287.46, redeclared op 'b'
*** Hint 287.51, redeclared op 'd'
*** Error 287.60, unknown sort 'a'
*** Hint 287.58, redeclared op 'c'
*** Error 287.35, total selectors 'a : s -> t,b : s -> t,d : s -> t'
must appear in alternative 'c : s'
*** Error 287.58, total selectors 'a : s -> t,b : s -> t,d : s -> t'
must appear in alternative 'c : a ->? s'
*** Error 290.16, unknown sort 'a'
*** Error 290.20, unknown sort 'a'
*** Hint 290.9, redeclared pred '__<__'
*** Error 292.7, unknown sort 'b'
*** Warning 292.4, also known as variable 'a'
*** Error 292.13, unknown sort 'b'
*** Hint 292.10, redeclared op 'c'
*** Hint 293.13, redeclared sort 's'
*** Hint 293.6, redeclared sort 's'
*** Hint 293.9, redeclared sort 't'
*** Warning 293.6, void reflexive subsort 's'
*** Hint 293.9, redeclared subsort 't < s'
*** Hint 294.6, redeclared sort 's'
*** Error 294.17, unknown sort 's2'
*** Hint 294.17, redeclared subsort 's2 < s'
*** Error 294.20, unknown sort 's1'
*** Hint 294.20, redeclared subsort 's1 < s'
*** Hint 294.25, redeclared op 'c'
*** Error 294.31, unknown sort 'a'
*** Hint 294.29, redeclared as total 'c'
*** Error 294.38, unknown sort 'a'
*** Hint 294.36, redeclared op 'c'
*** Hint 294.41, redeclared op 'a'
*** Hint 294.43, redeclared op 'b'
*** Hint 294.48, redeclared op 'd'
*** Error 294.57, unknown sort 'a'
*** Warning 294.55, partially redeclared 'c'
*** Error 294.29, duplicates at '(294,55)' for 'c : a -> s'
*** Error 294.25, total selectors 'a : s -> t,b : s -> t,d : s -> t'
must appear in alternative 'c : s'
*** Error 294.29, total selectors 'a : s -> t,b : s -> t,d : s -> t'
must appear in alternative 'c : a -> s'
*** Error 294.55, total selectors 'a : s -> t,b : s -> t,d : s -> t'
must appear in alternative 'c : a ->? s'
*** Hint 300.6, redeclared sort 's'
*** Hint 301.6, redeclared sort 't'
*** Error 304.6, unknown sort 'b'
*** Hint 304.4, redeclared op 'a'
*** Error 305.6, unknown sort 'd'
*** Warning 308.6, known variable shadowed 'a'
*** Warning 308.6, also known as operation 'a'
*** Warning 309.9, known variable shadowed 'a'
*** Warning 309.9, also known as operation 'a'
*** Warning 309.11, known variable shadowed 'b'
*** Warning 309.11, also known as operation 'b'
*** Hint 312.6, redeclared sort 't'
*** Error 316.3, ambiguous term
. (op a : b) = (op a : b)
. (var a : s) = (var a : s)
*** Error 317.3, ambiguous term
. (op a : b) = (op a : b)
. (var a : s) = (var a : s)
*** Error 320.5, ambiguous term
. (op a : b) = (op a : b)
. (var a : s) = (var a : s)
*** Error 321.5, ambiguous term
. (op a : b) = (op a : b)
. (var a : s) = (var a : s)
*** Hint 323.6, redeclared sort 's'
*** Hint 325.9, redeclared sort 's'
*** Hint 336.47, redeclared op ''\\''
*** Error, ambiguous term
(op __@@__ : Nat * Nat -> Nat)((op 1 : Pos), (op 2 : Nat))
(op __@@__ : s * s -> s)((op 1 : s), (op 2 : s))
*** Error 342.20, no operation with 2 arguments found for '__E__'
*** Error 342.32, no operation with 2 arguments found for '__E__'
*** Error 342.45, no operation with 2 arguments found for '__:::__'
*** Error 343.14, no operation with 2 arguments found for '__E__'
*** Error 343.29, no operation with 2 arguments found for '__E__'
*** Error 343.45, no operation with 2 arguments found for '__E__'
*** Hint 350.11, redeclared sort 's'
*** Error 351.11, wrong number of places '__and'__'
*** Hint 353.12, redeclared sort 'a'
*** Hint 354.13, redeclared sort 'b'
*** Hint 354.11, redeclared sort 'a'
*** Hint 355.12, redeclared sort 'a'
*** Hint 355.14, redeclared sort 'b'
*** Hint 355.16, redeclared sort 'c'
*** Hint 356.12, redeclared sort 'a'
*** Hint 356.14, redeclared sort 'b'
*** Hint 356.16, redeclared sort 'c'
*** Hint 356.18, redeclared sort 'd'
*** Hint 356.20, redeclared sort 'e'
*** Warning 356.12, subsort 'a' made isomorphic by 'a = b'
*** Warning 356.18, subsort 'd' made isomorphic by 'd = e'
*** Hint 357.11, redeclared sort 'a'
*** Warning 357.11, sorts are isomorphic 'a < b'
*** Hint 358.12, redeclared sort 's'
*** Hint 358.14, redeclared sort 't'
*** Warning 359.9, also known as variable 'a'
*** Warning 360.9, also known as variable 'b'
*** Warning 363.9, partially redeclared 'a'
*** Warning 364.9, partially redeclared 'b'
*** Warning 365.9, partially redeclared 'c'
*** Warning 366.9, partially redeclared 'c'
*** Hint 367.9, redeclared op 'a'
*** Warning 369.9, partially redeclared 'a'
*** Warning 370.9, partially redeclared 'c'
*** Hint 373.12, redeclared sort 's'
*** Hint 373.14, redeclared sort 't'
*** Warning 374.11, also known as operation 'a'
*** Warning 374.11, also known as variable 'a'
*** Warning 375.11, also known as operation 'b'
*** Warning 375.11, also known as variable 'b'
*** Warning 376.12, also known as operation 'c'
*** Warning 377.12, also known as operation 'c'
*** Warning 381.11, also known as operation 'c'
*** Warning 382.21, also known as predicate 'a'
*** Warning 382.21, also known as variable 'a'
*** Warning 382.25, also known as predicate 'b'
*** Warning 382.25, also known as variable 'b'
*** Warning 382.29, also known as predicate 'c'
*** Hint 384.64, redeclared op 'sel2'
*** Hint 384.77, redeclared op 'sel1'
*** Hint 386.65, redeclared op 'sel2'
*** Hint 386.78, redeclared op 'sel1'
*** Hint 388.27, redeclared sort 'Data1'
*** Hint 388.34, redeclared sort 'Data2'
*** Hint 388.41, redeclared sort 'Data3'
*** Hint 393.22, redeclared sort 'Set'
*** Hint 393.30, redeclared op 'Mt'
*** Hint 393.35, redeclared op 'Add'
*** Hint 395.11, redeclared sort 't'
*** Hint 395.9, redeclared sort 's'
*** Warning 395.9, added subsort cycle by 's < t'
*** Warning 404.7, known variable shadowed 'x'
*** Warning 410.10, known variable shadowed 'x'
*** Error 426.26, no predicate with 0 arguments found for 'e'
*** Warning 427.8, known variable shadowed 'x'
*** Error 427.12, no predicate with 0 arguments found for 'e'
*** Warning 436.13, known variable shadowed 'x'
*** Warning 436.15, known variable shadowed 'y'
*** Warning 436.17, known variable shadowed 'z'
*** Warning 451.20, also known as operation 'c'
*** Warning 451.20, also known as predicate 'c'
*** Hint 811.11, redeclared op '' ''
*** Hint 1486.6, redeclared sort 'a'
*** Warning 1489.4, also known as predicate 'b'
*** Warning 1489.4, also known as variable 'b'