BasicSpec.sentences.output revision 59316321b20af89de1c2d4cd53183e04b72662c4
(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: 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 . 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'
### Hint 70.16, known variable shadowed 's'
### Hint 72.16, known variable shadowed 'r'
*** 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'
*** Error 147.8-147.16, ambiguous mixfix term
-__(__-__(a, b))
-(__-__(a, b))
### Hint 209.17, redeclared sort 'Rat'
### Hint 209.11, redeclared sort 'Int'
*** Error 246.8-246.14, ambiguous mixfix term
-__(__/__(i, p))
-(__/__(i, p))
*** 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'
### Hint 271.11, known variable shadowed 'a'
### Hint 272.6, known variable shadowed 'a'
### Hint 272.11, known variable shadowed 'a'
### Hint 272.13, known variable shadowed 'b'
### Hint 275.8, known variable shadowed 'a'
### Hint 275.13, known variable shadowed 'a'
### Hint 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'
### Hint 308.6, known variable shadowed 'a'
### Warning 308.6, also known as operation 'a'
### Hint 309.9, known variable shadowed 'a'
### Warning 309.9, also known as operation 'a'
### Hint 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'
### Hint 404.7, known variable shadowed 'x'
### Hint 410.10, known variable shadowed 'x'
### Hint 411.16, known variable shadowed 'x'
### Hint 411.60, known variable shadowed 'x'
### Hint 426.22, known variable shadowed 'x'
*** Error 426.26, no predicate with 0 arguments found for 'e'
### Hint 427.8, known variable shadowed 'x'
*** Error 427.12, no predicate with 0 arguments found for 'e'
### Hint 436.13, known variable shadowed 'x'
### Hint 436.15, known variable shadowed 'y'
### Hint 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'