BasicSpec.sentences.output revision dece9056c18ada64bcc8f2fba285270374139ee8
(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, s1, s2, t, x0123456789,
����������������������������������������������������������
sorts a = b = c = d = e; s = t; Data1 < Data2; Nat < Int;
Pos < Nat; Int < Rat; s1, s2 < s
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 %(ga_selector_pre)%,
forall v1, v2 : Nat . suc(v1) = suc(v2) <=> v1 = v2
%(ga_injective_suc)%,
forall v1 : Nat . not 0 = suc(v1) %(ga_disjoint_0_suc)%,
not def pre(0) %(ga_selector_undef_pre_0)%,
%% free
generated type Nat ::= 0 | suc(Nat) %(ga_generated_Nat)%,
forall v1 : Nat . 0 <= v1 %(Nat_leq_def1)%,
forall v1 : Nat . not suc(v1) <= 0 %(Nat_leq_def2)%,
forall v1, v2 : Nat . suc(v1) <= suc(v2) <=> v1 <= v2
%(Nat_leq_def3)%,
forall v1, v2 : Nat . v1 >= v2 <=> v2 <= v1 %(Nat_geq_def)%,
forall v1, v2 : Nat . v1 < v2 <=> v1 <= v2 /\ not v1 = v2
%(Nat_less_def)%,
forall v1, v2 : Nat . v1 > v2 <=> v1 < v2 %(Nat_greater_def)%,
forall v1 : Nat . 0 + v1 = v1 %(Nat_add_0)%,
forall v1, v2 : Nat . suc(v2) + v1 = suc(v2 + v1) %(Nat_add_suc)%,
forall v1 : Nat . 0 * v1 = 0 %(Nat_mult_0)%,
forall v1, v2 : Nat . suc(v2) * v1 = v2 * v1 + v1 %(Nat_mult_suc)%,
forall v1 : Nat . v1 ^ 0 = 1 %(Nat_power_0)%,
forall v1, v2 : Nat . v1 ^ suc(v2) = v1 * v1 ^ v2
%(Nat_power_suc)%,
forall v1, v2 : Nat . min(v1, v2) = v1 when v1 <= v2 else v2
%(Nat_min_def)%,
forall v1, v2 : Nat . max(v1, v2) = v2 when v1 <= v2 else v1
%(Nat_max_def)%,
forall v1 : Nat . + v1 = v1 %(plus_def)%,
forall v1 : Nat . abs(v1) = v1 %(Nat_abs)%,
forall v1 : Nat . odd(v1) <=> not even(v1) %(Nat_odd_def)%,
even(0) %(Nat_even_0)%,
forall v1 : Nat . even(suc(v1)) <=> odd(v1) %(Nat_even_suc)%,
0 ! = 1 %(Nat_factorial_0)%,
forall v1 : Nat . suc(v1) ! = suc(v1) * v1 ! %(Nat_factorial_suc)%,
forall v1, v2, v3 : Nat . v1 -? v2 = v3 <=> v1 = v3 + v2
%(Nat_sub_def)%,
forall v1 : Nat . not def v1 /? 0 %(Nat_divide_0)%,
forall v1, v2, v3 : Nat
. (v1 /? v2 = v3 <=> v1 = v3 * v2) if v2 > 0 %(Nat_divide_Pos)%,
forall v1, v2, v3 : Nat
. v1 div v2 = v3 <=> exists v4 : Nat . v1 = v2 * v3 + v4 /\ v4 < v2
%(Nat_div)%,
forall v1, v2, v3 : Nat
. v1 mod v2 = v3 <=> exists v4 : Nat . v1 = v2 * v4 + v3 /\ v3 < v2
%(Nat_mod)%,
forall v1, v2 : Nat . v1 quot v2 = v1 div v2 %(Nat_quot)%,
forall v1, v2 : Nat . v1 rem v2 = v1 mod v2 %(Nat_rem)%,
1 = suc(0) %(Nat_1_def)%, 2 = suc(1) %(Nat_2_def)%,
3 = suc(2) %(Nat_3_def)%, 4 = suc(3) %(Nat_4_def)%,
5 = suc(4) %(Nat_5_def)%, 6 = suc(5) %(Nat_6_def)%,
7 = suc(6) %(Nat_7_def)%, 8 = suc(7) %(Nat_8_def)%,
9 = suc(8) %(Nat_9_def)%,
forall v1, v2 : Nat . v1 @@ v2 = v1 * suc(9) + v2
%(Nat_decimal_def)%,
forall v1 : Nat . v1 in Pos <=> v1 > 0,
forall v1, v2 : Nat . min(v1, v2) = min(v2, v1) %(ga_comm_min)%,
forall v1, v2 : Nat . max(v1, v2) = max(v2, v1) %(ga_comm_max)%,
forall v1, v2, v3 : Nat
. min(min(v1, v2), v3) = min(v1, min(v2, v3)) %(ga_assoc_min)%,
forall v1, v2, v3 : Nat
. max(max(v1, v2), v3) = max(v1, max(v2, v3)) %(ga_assoc_max)%,
forall v1, v2, v3 : Nat
. min(v1, min(v2, v3)) = min(v2, min(v1, v3)) %(ga_left_comm_min)%,
forall v1, v2, v3 : Nat
. max(v1, max(v2, v3)) = max(v2, max(v1, v3)) %(ga_left_comm_max)%,
forall v1, v2 : Nat . def v1 -? v2 <=> v1 >= v2 %(Nat_sub_dom)%,
forall v1, v2 : Nat . def v1 /? v2 <=> v1 mod v2 = 0
%(Nat_divide_dom)%,
forall v1, v2 : Nat . def v1 div v2 <=> not v2 = 0 %(Nat_div_dom)%,
forall v1, v2 : Nat . def v1 mod v2 <=> not v2 = 0 %(Nat_mod_dom)%,
forall v1, v2 : Nat . def v1 quot v2 <=> not v2 = 0
%(Nat_quot_dom)%,
forall v1, v2 : Nat . def v1 rem v2 <=> not v2 = 0 %(Nat_rem_dom)%,
forall v1, v2, v3 : Nat . (v1 + v2) * v3 = v1 * v3 + v2 * v3
%(Nat_distr)%,
forall v1 : Nat . max(v1, 0) = v1 %(Nat_max_unit)%,
forall v1 : Nat . min(v1, 0) = 0 %(Nat_min_0)%,
generated type Int ::= __-__(Nat; Nat) %(ga_generated_Int)%,
forall v1, v2, v3, v4 : Nat
. v1 - v2 = v3 - v4 <=> v1 + v4 = v3 + v2 %(Int_equality)%,
forall v1 : Nat . v1 = v1 - 0 %(Int_Nat_embedding)%,
forall v1, v2, v3, v4 : Nat
. (v1 - v2) + (v3 - v4) = (v1 + v3) - (v2 + v4) %(Int_add_def)%,
forall v1, v2, v3, v4 : Nat
. (v1 - v2) * (v3 - v4) = (v1 * v3 + v2 * v4) - (v2 * v3 + v1 * v4)
%(Int_mult_def)%,
forall v1, v2 : Int . v1 - v2 = v1 + - v2 %(Int_sub_def)%,
forall v1 : Int . + v1 = v1 %(Int_pos_def)%,
forall v1 : Int
. sign(v1) = 0 when v1 = 0 else 1 when v1 > 0 else - 1
%(Int_sign_def)%,
forall v1, v2 : Int . v1 <= v2 <=> v2 - v1 in Nat %(Int_leq_def)%,
forall v1, v2 : Int . v1 >= v2 <=> v2 <= v1 %(Int_geq_def)%,
forall v1, v2 : Int . v1 < v2 <=> v1 <= v2 /\ not v1 = v2
%(Int_less_def)%,
forall v1, v2 : Int . v1 > v2 <=> v1 < v2 %(Int_greater_def)%,
forall v1, v2 : Int . min(v1, v2) = v1 when v1 <= v2 else v2
%(Int_min_def)%,
forall v1, v2 : Int . max(v1, v2) = v2 when v1 <= v2 else v1
%(Int_max_def)%,
forall v1 : Int . abs(v1) = - v1 if v1 < 0 %(Int_abs_def)%,
forall v1 : Nat . - 1 ^ v1 = 1 when even(v1) else - 1
%(Int_neg1_power_def)%,
forall v1 : Int; v2 : Nat . v1 ^ v2 = sign(v1) ^ v2 * abs(v1) ^ v2
%(Int_power_def)%,
forall v1 : Int . even(v1) <=> even(abs(v1)) %(Int_even_def)%,
forall v1 : Int . odd(v1) <=> not even(v1) %(Int_odd_def)%,
forall v1, v2 : Int
. v1 /? v2 = sign(v1) * sign(v2) * (abs(v1) /? abs(v2))
%(Int_divide)%,
forall v1, v2 : Int . v1 mod v2 < abs(v2) if not v2 = 0
%(Int_mod_range)%,
forall v1, v2 : Int
. v1 = (v1 div v2) * v2 + (v1 mod v2) if not v2 = 0
%(Int_mod__div_def)%,
forall v1 : Int . not def v1 mod 0 %(Int_mod_zero)%,
forall v1 : Int . not def v1 div 0 %(Int_div_zero)%,
forall v1, v2 : Int
. v1 quot v2 = sign(v1) * sign(v2) * (abs(v1) quot abs(v2))
%(Int_quot_def)%,
forall v1, v2 : Int
. v1 rem v2 = sign(v1) * sign(v2) * (abs(v1) rem abs(v2))
%(Int_rem_def)%,
forall v1, v2 : Nat . def v1 -? v2 => v1 -? v2 = v1 - v2
%(Int_Nat_sub_compat)%,
forall v1 : Int . v1 = sign(v1) * abs(v1) %(Int_abs_decomp)%,
forall v1 : Int . odd(v1) <=> odd(abs(v1)) %(Int_odd_alt)%,
forall v1, v2, v3 : Int
. v1 /? v2 = v3 <=> not v2 = 0 /\ v2 * v3 = v2 %(Int_divide_dom1)%,
forall v1, v2 : Int . def v1 /? v2 <=> v1 mod v2 = 0
%(Int_divide_dom2)%,
forall v1, v2 : Int . def v1 mod v2 <=> not v2 = 0 %(Int_mod_dom)%,
forall v1, v2 : Int . v1 mod v2 = v1 mod abs(v2) %(Int_mod_abs)%,
forall v1, v2 : Int . def v1 div v2 <=> not v2 = 0 %(Int_div_dom)%,
forall v1, v2 : Int . def v1 quot v2 <=> not v2 = 0
%(Int_quot_dom)%,
forall v1, v2 : Int . def v1 rem v2 <=> not v2 = 0 %(Int_rem_dom)%,
forall v1, v2 : Int
. v1 = (v1 quot v2) * v2 + (v1 rem v2) if not v2 = 0
%(Int_quot_rem)%,
generated type Rat ::= __/__(Int; Pos) %(ga_generated_Rat)%,
forall v1, v2 : Int; v3, v4 : Pos
. v1 / v3 = v2 / v4 <=> v1 * v4 = v2 * v3 %(Rat_equality)%,
forall v1 : Int . v1 / 1 = v1 %(embeddingIntToRat)%,
forall v1, v2 : Pos; v3, v4 : Int
. v3 / v1 <= v4 / v2 <=> v3 * v2 <= v4 * v1 %(Rat_leq_def)%,
forall v1, v2 : Rat . v1 >= v2 <=> v2 <= v1 %(Rat_geq_def)%,
forall v1, v2 : Rat . v1 < v2 <=> v1 <= v2 /\ not v1 = v2
%(Rat_less_def)%,
forall v1, v2 : Rat . v1 > v2 <=> v2 < v1 %(Rat_greater_def)%,
forall v1, v2 : Pos; v3, v4 : Int
. (v3 / v1) + (v4 / v2) = (v3 * v2 + v4 * v1) / (v1 * v2)
%(Rat_add_def)%,
forall v1, v2 : Rat . v1 - v2 = v1 + - v2 %(Rat_sub_def)%,
forall v1, v2 : Pos; v3, v4 : Int
. (v3 / v1) * (v4 / v2) = (v3 * v4) / (v1 * v2) %(Rat_mult_def)%,
forall v1 : Rat . not def v1 / 0 %(Rat_divide_def1)%,
forall v1, v2, v3 : Rat
. (v1 / v2 = v3 <=> v3 = v1 * v2) if not v2 = 0
%(Rat_divide_def2)%,
forall v1 : Rat . + v1 = v1 %(Rat_plus_def)%,
forall v1 : Pos; v2 : Int . abs(v2 / v1) = abs(v2) / v1
%(Rat_abs_def)%,
forall v1 : Rat . v1 ^ 0 = 1 %(Rat_power_0)%,
forall v1 : Nat; v2 : Rat . v2 ^ suc(v1) = v2 * v2 ^ v1
%(Rat_power_suc)%,
forall v1 : Pos; v2 : Rat . v2 ^ - v1 = 1 / (v2 ^ v1)
%(Rat_power_neg)%,
forall v1, v2 : Rat . min(v1, v2) = v1 when v1 <= v2 else v2
%(Rat_min_def)%,
forall v1, v2 : Rat . max(v1, v2) = v2 when v1 <= v2 else v1
%(Rat_max_def)%,
forall v1, v2 : Int; v3, v4 : Pos
. (v1 / v3) / (v2 / v4) = (v1 / v3) * (v4 / v2) if not v2 = 0
%(Rat_divide_rule)%,
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
%(ga_selector_a)%,
forall v1 : a; v2, v3, v4, v5 : t . b(c(v1, v2, v3, v4, v5)) = v3
%(ga_selector_b)%,
forall v1 : a; v2, v3, v4, v5 : t . a(c(v1, v2, v3, v4, v5)) = v4
%(ga_selector_a)%,
forall v1 : a; v2, v3, v4, v5 : t . d(c(v1, v2, v3, v4, v5)) = v5
%(ga_selector_d)%,
forall v1 : a; v2, v3, v4 : t . a(c(v1, v2, v3, v4)) = v2
%(ga_selector_a)%,
forall v1 : a; v2, v3, v4 : t . b(c(v1, v2, v3, v4)) = v3
%(ga_selector_b)%,
forall v1 : a; v2, v3, v4 : t . d(c(v1, v2, v3, v4)) = v4
%(ga_selector_d)%,
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 %(ga_injective_c)%,
forall v1, v2 : a . c(v1) = c(v2) <=> v1 = v2 %(ga_injective_c)%,
forall v1 : s . not (v1 in s2 /\ v1 in s1)
%(ga_disjoint_sorts_s2_s1)%,
not c : s in s2 %(ga_disjoint_c_sort_s2)%,
not c : s in s1 %(ga_disjoint_c_sort_s1)%,
forall v1 : a; v2, v3, v4 : t . not c(v1, v2, v3, v4) in s2
%(ga_disjoint_c_sort_s2)%,
forall v1 : a; v2, v3, v4 : t . not c(v1, v2, v3, v4) in s1
%(ga_disjoint_c_sort_s1)%,
forall v1 : a . not c(v1) in s2 %(ga_disjoint_c_sort_s2)%,
forall v1 : a . not c(v1) in s1 %(ga_disjoint_c_sort_s1)%,
forall v1 : a; v2, v3, v4 : t . not c = c(v1, v2, v3, v4)
%(ga_disjoint_c_c)%,
forall v1 : a . not c = c(v1) %(ga_disjoint_c_c)%,
forall v1 : a; v2, v3, v4 : t; v5 : a
. not c(v1, v2, v3, v4) = c(v5) %(ga_disjoint_c_c)%,
not def a(c) %(ga_selector_undef_a_c)%,
forall v1 : a . not def a(c(v1)) %(ga_selector_undef_a_c)%,
not def b(c) %(ga_selector_undef_b_c)%,
forall v1 : a . not def b(c(v1)) %(ga_selector_undef_b_c)%,
not def d(c) %(ga_selector_undef_d_c)%,
forall v1 : a . not def d(c(v1)) %(ga_selector_undef_d_c)%,
%% free
generated type s ::= c | c(a)? | c(a; t; t; t) | sort s1 | sort s2
%(ga_generated_s)%,
forall v1 : a; v2, v3, v4 : t . a(c(v1, v2, v3, v4)) = v2
%(ga_selector_a)%,
forall v1 : a; v2, v3, v4 : t . b(c(v1, v2, v3, v4)) = v3
%(ga_selector_b)%,
forall v1 : a; v2, v3, v4 : t . d(c(v1, v2, v3, v4)) = v4
%(ga_selector_d)%,
generated type s ::= c | c(a)? | c(a; t; t; t) | sort s1 | sort s2
%(ga_generated_s)%,
forall v1 : a; v2, v3, v4 : t . a(c(v1, v2, v3, v4)) = v2
%(ga_selector_a)%,
forall v1 : a; v2, v3, v4 : t . b(c(v1, v2, v3, v4)) = v3
%(ga_selector_b)%,
forall v1 : a; v2, v3, v4 : t . d(c(v1, v2, v3, v4)) = v4
%(ga_selector_d)%,
generated types
s ::= c | c(a)? | c(a; t; t; t) | sort s1 | sort s2 | sort t;
t ::= sort t %(ga_generated_s_t)%,
true %(The true formula)%,
true
%(and this also goes along several lines! and with special stuff: -*/\&=<>BCDEFGHIJKLM!%)%,
forall v1 : b . v1 in a <=> true,
forall v1, v2, v3 : s . c(c(v1, v2), v3) = c(v1, c(v2, v3))
%(ga_assoc_c)%,
forall v1, v2 : s . c(v1, v2) = c(v2, v1) %(ga_comm_c)%,
forall v1 : s . c(v1, v1) = v1 %(ga_idem_c)%,
forall v1 : s . c(v1, a) = v1 %(ga_right_unit_c)%,
forall v1 : s . c(a, v1) = v1 %(ga_left_unit_c)%,
forall v1, v2, v3 : s . c(v1, c(v2, v3)) = c(v2, c(v1, v3))
%(ga_left_comm_c)%,
forall v1, v2, v3 : s . c(c(v1, v2), v3) = c(v1, c(v2, v3))
%(ga_assoc_c)%,
forall v1, v2 : s . c(v1, v2) = c(v2, v1) %(ga_comm_c)%,
forall v1 : s . c(v1, v1) = v1 %(ga_idem_c)%,
forall v1 : s . c(v1, a) = v1 %(ga_right_unit_c)%,
forall v1 : s . c(a, v1) = v1 %(ga_left_unit_c)%,
forall v1, v2, v3 : s . c(v1, c(v2, v3)) = c(v2, c(v1, v3))
%(ga_left_comm_c)%,
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
%(ga_selector_sel1)%,
forall v1 : Data1; v2 : Data2 . sel2(Cons31(v1, v2)) = v2
%(ga_selector_sel2)%,
forall v1 : Data2; v2 : Data1 . sel2(Cons32(v1, v2)) = v1
%(ga_selector_sel2)%,
forall v1 : Data2; v2 : Data1 . sel1(Cons32(v1, v2)) = v2
%(ga_selector_sel1)%,
forall v1 : Data1; v2 : Data2 . sel1(Cons41(v1, v2)) = v1
%(ga_selector_sel1)%,
forall v1 : Data1; v2 : Data2 . sel2(Cons41(v1, v2)) = v2
%(ga_selector_sel2)%,
forall v1 : Data2; v2 : Data1 . sel2(Cons42(v1, v2)) = v1
%(ga_selector_sel2)%,
forall v1 : Data2; v2 : Data1 . sel1(Cons42(v1, v2)) = v2
%(ga_selector_sel1)%,
forall v1 : Data1; v2 : List; v3 : Data1; v4 : List
. Cons(v1, v2) = Cons(v3, v4) <=> v1 = v3 /\ v2 = v4
%(ga_injective_Cons)%,
forall v1 : Data1; v2 : List . not Nil = Cons(v1, v2)
%(ga_disjoint_Nil_Cons)%,
%% free
generated type List ::= Cons(Data1; List) | Nil
%(ga_generated_List)%,
generated type Set ::= Add(Data1; Set) | Mt %(ga_generated_Set)%,
generated type Set ::= Add(Data1; Set) | Mt %(ga_generated_Set)%,
generated type nat ::= 0 | succ(nat) %(ga_generated_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) as s,
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 %(ga_disjoint_True_False)%,
%% free
generated type Boolean ::= False | True %(ga_generated_Boolean)%,
Not False = True %(Not_False)%, Not True = False %(Not_True)%,
False And False = False %(And_def1)%,
False And True = False %(And_def2)%,
True And False = False %(And_def3)%,
True And True = True %(And_def4)%,
forall v1, v2 : Boolean . v1 Or v2 = Not (Not v1 And Not v2)
%(Or_def)%,
forall v1 : Nat . def chr(v1) <=> v1 <= 255 %(chr_dom)%,
forall v1 : Char . chr(ord(v1)) = v1 %(chr_def)%,
forall v1 : Nat . ord(chr(v1)) = v1 if v1 <= 255 %(ord_def)%,
'\000' = chr(0) %(slash_000)%, '\001' = chr(1) %(slash_001)%,
'\002' = chr(2) %(slash_002)%, '\003' = chr(3) %(slash_003)%,
'\004' = chr(4) %(slash_004)%, '\005' = chr(5) %(slash_005)%,
'\006' = chr(6) %(slash_006)%, '\007' = chr(7) %(slash_007)%,
'\008' = chr(8) %(slash_008)%, '\009' = chr(9) %(slash_009)%,
'\010' = chr(10) %(slash_010)%,
'\011' = chr(1 : Nat @@ 1 : Nat) %(slash_011)%,
'\012' = chr(1 : Nat @@ 2 : Nat) %(slash_012)%,
'\013' = chr(1 : Nat @@ 3 : Nat) %(slash_013)%,
'\014' = chr(1 : Nat @@ 4 : Nat) %(slash_014)%,
'\015' = chr(15) %(slash_015)%, '\016' = chr(16) %(slash_016)%,
'\017' = chr(17) %(slash_017)%, '\018' = chr(18) %(slash_018)%,
'\019' = chr(19) %(slash_019)%, '\020' = chr(20) %(slash_020)%,
'\021' = chr(2 : Nat @@ 1 : Nat) %(slash_021)%,
'\022' = chr(2 : Nat @@ 2 : Nat) %(slash_022)%,
'\023' = chr(2 : Nat @@ 3 : Nat) %(slash_023)%,
'\024' = chr(2 : Nat @@ 4 : Nat) %(slash_024)%,
'\025' = chr(25) %(slash_025)%, '\026' = chr(26) %(slash_026)%,
'\027' = chr(27) %(slash_027)%, '\028' = chr(28) %(slash_028)%,
'\029' = chr(29) %(slash_029)%, '\030' = chr(30) %(slash_030)%,
'\031' = chr(3 : Nat @@ 1 : Nat) %(slash_031)%,
'\032' = chr(3 : Nat @@ 2 : Nat) %(slash_032)%,
'\033' = chr(3 : Nat @@ 3 : Nat) %(slash_033)%,
'\034' = chr(3 : Nat @@ 4 : Nat) %(slash_034)%,
'\035' = chr(35) %(slash_035)%, '\036' = chr(36) %(slash_036)%,
'\037' = chr(37) %(slash_037)%, '\038' = chr(38) %(slash_038)%,
'\039' = chr(39) %(slash_039)%, '\040' = chr(40) %(slash_040)%,
'\041' = chr(4 : Nat @@ 1 : Nat) %(slash_041)%,
'\042' = chr(4 : Nat @@ 2 : Nat) %(slash_042)%,
'\043' = chr(4 : Nat @@ 3 : Nat) %(slash_043)%,
'\044' = chr(4 : Nat @@ 4 : Nat) %(slash_044)%,
'\045' = chr(45) %(slash_045)%, '\046' = chr(46) %(slash_046)%,
'\047' = chr(47) %(slash_047)%, '\048' = chr(48) %(slash_048)%,
'\049' = chr(49) %(slash_049)%, '\050' = chr(50) %(slash_050)%,
'\051' = chr(51) %(slash_051)%, '\052' = chr(52) %(slash_052)%,
'\053' = chr(53) %(slash_053)%, '\054' = chr(54) %(slash_054)%,
'\055' = chr(55) %(slash_055)%, '\056' = chr(56) %(slash_056)%,
'\057' = chr(57) %(slash_057)%, '\058' = chr(58) %(slash_058)%,
'\059' = chr(59) %(slash_059)%, '\060' = chr(60) %(slash_060)%,
'\061' = chr(61) %(slash_061)%, '\062' = chr(62) %(slash_062)%,
'\063' = chr(63) %(slash_063)%, '\064' = chr(64) %(slash_064)%,
'\065' = chr(65) %(slash_065)%, '\066' = chr(66) %(slash_066)%,
'\067' = chr(67) %(slash_067)%, '\068' = chr(68) %(slash_068)%,
'\069' = chr(69) %(slash_069)%, '\070' = chr(70) %(slash_070)%,
'\071' = chr(71) %(slash_071)%, '\072' = chr(72) %(slash_072)%,
'\073' = chr(73) %(slash_073)%, '\074' = chr(74) %(slash_074)%,
'\075' = chr(75) %(slash_075)%, '\076' = chr(76) %(slash_076)%,
'\077' = chr(77) %(slash_077)%, '\078' = chr(78) %(slash_078)%,
'\079' = chr(79) %(slash_079)%, '\080' = chr(80) %(slash_080)%,
'\081' = chr(81) %(slash_081)%, '\082' = chr(82) %(slash_082)%,
'\083' = chr(83) %(slash_083)%, '\084' = chr(84) %(slash_084)%,
'\085' = chr(85) %(slash_085)%, '\086' = chr(86) %(slash_086)%,
'\087' = chr(87) %(slash_087)%, '\088' = chr(88) %(slash_088)%,
'\089' = chr(89) %(slash_089)%, '\090' = chr(90) %(slash_090)%,
'\091' = chr(91) %(slash_091)%, '\092' = chr(92) %(slash_092)%,
'\093' = chr(93) %(slash_093)%, '\094' = chr(94) %(slash_094)%,
'\095' = chr(95) %(slash_095)%, '\096' = chr(96) %(slash_096)%,
'\097' = chr(97) %(slash_097)%, '\098' = chr(98) %(slash_098)%,
'\099' = chr(99) %(slash_099)%, '\100' = chr(100) %(slash_100)%,
'\101' = chr(101) %(slash_101)%, '\102' = chr(102) %(slash_102)%,
'\103' = chr(103) %(slash_103)%, '\104' = chr(104) %(slash_104)%,
'\105' = chr(105) %(slash_105)%, '\106' = chr(106) %(slash_106)%,
'\107' = chr(107) %(slash_107)%, '\108' = chr(108) %(slash_108)%,
'\109' = chr(109) %(slash_109)%, '\110' = chr(110) %(slash_110)%,
'\111' = chr(1 @@ (1 : Nat @@ 1 : Nat)) %(slash_111)%,
'\112' = chr(1 @@ (1 : Nat @@ 2 : Nat)) %(slash_112)%,
'\113' = chr(1 @@ (1 : Nat @@ 3 : Nat)) %(slash_113)%,
'\114' = chr(1 @@ (1 : Nat @@ 4 : Nat)) %(slash_114)%,
'\115' = chr(115) %(slash_115)%, '\116' = chr(116) %(slash_116)%,
'\117' = chr(117) %(slash_117)%, '\118' = chr(118) %(slash_118)%,
'\119' = chr(119) %(slash_119)%, '\120' = chr(120) %(slash_120)%,
'\121' = chr(1 @@ (2 : Nat @@ 1 : Nat)) %(slash_121)%,
'\122' = chr(1 @@ (2 : Nat @@ 2 : Nat)) %(slash_122)%,
'\123' = chr(1 @@ (2 : Nat @@ 3 : Nat)) %(slash_123)%,
'\124' = chr(1 @@ (2 : Nat @@ 4 : Nat)) %(slash_124)%,
'\125' = chr(125) %(slash_125)%, '\126' = chr(126) %(slash_126)%,
'\127' = chr(127) %(slash_127)%, '\128' = chr(128) %(slash_128)%,
'\129' = chr(129) %(slash_129)%, '\130' = chr(130) %(slash_130)%,
'\131' = chr(1 @@ (3 : Nat @@ 1 : Nat)) %(slash_131)%,
'\132' = chr(1 @@ (3 : Nat @@ 2 : Nat)) %(slash_132)%,
'\133' = chr(1 @@ (3 : Nat @@ 3 : Nat)) %(slash_133)%,
'\134' = chr(1 @@ (3 : Nat @@ 4 : Nat)) %(slash_134)%,
'\135' = chr(135) %(slash_135)%, '\136' = chr(136) %(slash_136)%,
'\137' = chr(137) %(slash_137)%, '\138' = chr(138) %(slash_138)%,
'\139' = chr(139) %(slash_139)%, '\140' = chr(140) %(slash_140)%,
'\141' = chr(1 @@ (4 : Nat @@ 1 : Nat)) %(slash_141)%,
'\142' = chr(1 @@ (4 : Nat @@ 2 : Nat)) %(slash_142)%,
'\143' = chr(1 @@ (4 : Nat @@ 3 : Nat)) %(slash_143)%,
'\144' = chr(1 @@ (4 : Nat @@ 4 : Nat)) %(slash_144)%,
'\145' = chr(145) %(slash_145)%, '\146' = chr(146) %(slash_146)%,
'\147' = chr(147) %(slash_147)%, '\148' = chr(148) %(slash_148)%,
'\149' = chr(149) %(slash_149)%, '\150' = chr(150) %(slash_150)%,
'\151' = chr(151) %(slash_151)%, '\152' = chr(152) %(slash_152)%,
'\153' = chr(153) %(slash_153)%, '\154' = chr(154) %(slash_154)%,
'\155' = chr(155) %(slash_155)%, '\156' = chr(156) %(slash_156)%,
'\157' = chr(157) %(slash_157)%, '\158' = chr(158) %(slash_158)%,
'\159' = chr(159) %(slash_159)%, '\160' = chr(160) %(slash_160)%,
'\161' = chr(161) %(slash_161)%, '\162' = chr(162) %(slash_162)%,
'\163' = chr(163) %(slash_163)%, '\164' = chr(164) %(slash_164)%,
'\165' = chr(165) %(slash_165)%, '\166' = chr(166) %(slash_166)%,
'\167' = chr(167) %(slash_167)%, '\168' = chr(168) %(slash_168)%,
'\169' = chr(169) %(slash_169)%, '\170' = chr(170) %(slash_170)%,
'\171' = chr(171) %(slash_171)%, '\172' = chr(172) %(slash_172)%,
'\173' = chr(173) %(slash_173)%, '\174' = chr(174) %(slash_174)%,
'\175' = chr(175) %(slash_175)%, '\176' = chr(176) %(slash_176)%,
'\177' = chr(177) %(slash_177)%, '\178' = chr(178) %(slash_178)%,
'\179' = chr(179) %(slash_179)%, '\180' = chr(180) %(slash_180)%,
'\181' = chr(181) %(slash_181)%, '\182' = chr(182) %(slash_182)%,
'\183' = chr(183) %(slash_183)%, '\184' = chr(184) %(slash_184)%,
'\185' = chr(185) %(slash_185)%, '\186' = chr(186) %(slash_186)%,
'\187' = chr(187) %(slash_187)%, '\188' = chr(188) %(slash_188)%,
'\189' = chr(189) %(slash_189)%, '\190' = chr(190) %(slash_190)%,
'\191' = chr(191) %(slash_191)%, '\192' = chr(192) %(slash_192)%,
'\193' = chr(193) %(slash_193)%, '\194' = chr(194) %(slash_194)%,
'\195' = chr(195) %(slash_195)%, '\196' = chr(196) %(slash_196)%,
'\197' = chr(197) %(slash_197)%, '\198' = chr(198) %(slash_198)%,
'\199' = chr(199) %(slash_199)%, '\200' = chr(200) %(slash_200)%,
'\201' = chr(201) %(slash_201)%, '\202' = chr(202) %(slash_202)%,
'\203' = chr(203) %(slash_203)%, '\204' = chr(204) %(slash_204)%,
'\205' = chr(205) %(slash_205)%, '\206' = chr(206) %(slash_206)%,
'\207' = chr(207) %(slash_207)%, '\208' = chr(208) %(slash_208)%,
'\209' = chr(209) %(slash_209)%, '\210' = chr(210) %(slash_210)%,
'\211' = chr(2 @@ (1 : Nat @@ 1 : Nat)) %(slash_211)%,
'\212' = chr(2 @@ (1 : Nat @@ 2 : Nat)) %(slash_212)%,
'\213' = chr(2 @@ (1 : Nat @@ 3 : Nat)) %(slash_213)%,
'\214' = chr(2 @@ (1 : Nat @@ 4 : Nat)) %(slash_214)%,
'\215' = chr(215) %(slash_215)%, '\216' = chr(216) %(slash_216)%,
'\217' = chr(217) %(slash_217)%, '\218' = chr(218) %(slash_218)%,
'\219' = chr(219) %(slash_219)%, '\220' = chr(220) %(slash_220)%,
'\221' = chr(2 @@ (2 : Nat @@ 1 : Nat)) %(slash_221)%,
'\222' = chr(2 @@ (2 : Nat @@ 2 : Nat)) %(slash_222)%,
'\223' = chr(2 @@ (2 : Nat @@ 3 : Nat)) %(slash_223)%,
'\224' = chr(2 @@ (2 : Nat @@ 4 : Nat)) %(slash_224)%,
'\225' = chr(225) %(slash_225)%, '\226' = chr(226) %(slash_226)%,
'\227' = chr(227) %(slash_227)%, '\228' = chr(228) %(slash_228)%,
'\229' = chr(229) %(slash_229)%, '\230' = chr(230) %(slash_230)%,
'\231' = chr(2 @@ (3 : Nat @@ 1 : Nat)) %(slash_231)%,
'\232' = chr(2 @@ (3 : Nat @@ 2 : Nat)) %(slash_232)%,
'\233' = chr(2 @@ (3 : Nat @@ 3 : Nat)) %(slash_233)%,
'\234' = chr(2 @@ (3 : Nat @@ 4 : Nat)) %(slash_234)%,
'\235' = chr(235) %(slash_235)%, '\236' = chr(236) %(slash_236)%,
'\237' = chr(237) %(slash_237)%, '\238' = chr(238) %(slash_238)%,
'\239' = chr(239) %(slash_239)%, '\240' = chr(240) %(slash_240)%,
'\241' = chr(2 @@ (4 : Nat @@ 1 : Nat)) %(slash_241)%,
'\242' = chr(2 @@ (4 : Nat @@ 2 : Nat)) %(slash_242)%,
'\243' = chr(2 @@ (4 : Nat @@ 3 : Nat)) %(slash_243)%,
'\244' = chr(2 @@ (4 : Nat @@ 4 : Nat)) %(slash_244)%,
'\245' = chr(245) %(slash_245)%, '\246' = chr(246) %(slash_246)%,
'\247' = chr(247) %(slash_247)%, '\248' = chr(248) %(slash_248)%,
'\249' = chr(249) %(slash_249)%, '\250' = chr(250) %(slash_250)%,
'\251' = chr(251) %(slash_251)%, '\252' = chr(252) %(slash_252)%,
'\253' = chr(253) %(slash_253)%, '\254' = chr(254) %(slash_254)%,
'\255' = chr(255) %(slash_255)%, ' ' = '\032' %(printable_32)%,
'!' = '\033' %(printable_33)%, '\"' = '\034' %(printable_34)%,
'#' = '\035' %(printable_35)%, '$' = '\036' %(printable_36)%,
'%' = '\037' %(printable_37)%, '&' = '\038' %(printable_38)%,
'\'' = '\039' %(printable_39)%, '(' = '\040' %(printable_40)%,
')' = '\041' %(printable_41)%, '*' = '\042' %(printable_42)%,
'+' = '\043' %(printable_43)%, ',' = '\044' %(printable_44)%,
'-' = '\045' %(printable_45)%, '.' = '\046' %(printable_46)%,
'/' = '\047' %(printable_47)%, '0' = '\048' %(printable_48)%,
'1' = '\049' %(printable_49)%, '2' = '\050' %(printable_50)%,
'3' = '\051' %(printable_51)%, '4' = '\052' %(printable_52)%,
'5' = '\053' %(printable_53)%, '6' = '\054' %(printable_54)%,
'7' = '\055' %(printable_55)%, '8' = '\056' %(printable_56)%,
'9' = '\057' %(printable_57)%, ':' = '\058' %(printable_58)%,
';' = '\059' %(printable_59)%, '<' = '\060' %(printable_60)%,
'=' = '\061' %(printable_61)%, '>' = '\062' %(printable_62)%,
'?' = '\063' %(printable_63)%, '@' = '\064' %(printable_64)%,
'A' = '\065' %(printable_65)%, 'B' = '\066' %(printable_66)%,
'C' = '\067' %(printable_67)%, 'D' = '\068' %(printable_68)%,
'E' = '\069' %(printable_69)%, 'F' = '\070' %(printable_70)%,
'G' = '\071' %(printable_71)%, 'H' = '\072' %(printable_72)%,
'I' = '\073' %(printable_73)%, 'J' = '\074' %(printable_74)%,
'K' = '\075' %(printable_75)%, 'L' = '\076' %(printable_76)%,
'M' = '\077' %(printable_77)%, 'N' = '\078' %(printable_78)%,
'O' = '\079' %(printable_79)%, 'P' = '\080' %(printable_80)%,
'Q' = '\081' %(printable_81)%, 'R' = '\082' %(printable_82)%,
'S' = '\083' %(printable_83)%, 'T' = '\084' %(printable_84)%,
'U' = '\085' %(printable_85)%, 'V' = '\086' %(printable_86)%,
'W' = '\087' %(printable_87)%, 'X' = '\088' %(printable_88)%,
'Y' = '\089' %(printable_89)%, 'Z' = '\090' %(printable_90)%,
'[' = '\091' %(printable_91)%, '\\' = '\092' %(printable_92)%,
']' = '\093' %(printable_93)%, '^' = '\094' %(printable_94)%,
'_' = '\095' %(printable_95)%, '`' = '\096' %(printable_96)%,
'a' = '\097' %(printable_97)%, 'b' = '\098' %(printable_98)%,
'c' = '\099' %(printable_99)%, 'd' = '\100' %(printable_100)%,
'e' = '\101' %(printable_101)%, 'f' = '\102' %(printable_102)%,
'g' = '\103' %(printable_103)%, 'h' = '\104' %(printable_104)%,
'i' = '\105' %(printable_105)%, 'j' = '\106' %(printable_106)%,
'k' = '\107' %(printable_107)%, 'l' = '\108' %(printable_108)%,
'm' = '\109' %(printable_109)%, 'n' = '\110' %(printable_110)%,
'o' = '\111' %(printable_111)%, 'p' = '\112' %(printable_112)%,
'q' = '\113' %(printable_113)%, 'r' = '\114' %(printable_114)%,
's' = '\115' %(printable_115)%, 't' = '\116' %(printable_116)%,
'u' = '\117' %(printable_117)%, 'v' = '\118' %(printable_118)%,
'w' = '\119' %(printable_119)%, 'x' = '\120' %(printable_120)%,
'y' = '\121' %(printable_121)%, 'z' = '\122' %(printable_122)%,
'{' = '\123' %(printable_123)%, '|' = '\124' %(printable_124)%,
'}' = '\125' %(printable_125)%, '~' = '\126' %(printable_126)%,
' ' = '\160' %(printable_160)%, '�' = '\161' %(printable_161)%,
'�' = '\162' %(printable_162)%, '�' = '\163' %(printable_163)%,
'�' = '\164' %(printable_164)%, '�' = '\165' %(printable_165)%,
'�' = '\166' %(printable_166)%, '�' = '\167' %(printable_167)%,
'�' = '\168' %(printable_168)%, '�' = '\169' %(printable_169)%,
'�' = '\170' %(printable_170)%, '�' = '\171' %(printable_171)%,
'�' = '\172' %(printable_172)%, '�' = '\173' %(printable_173)%,
'�' = '\174' %(printable_174)%, '�' = '\175' %(printable_175)%,
'�' = '\176' %(printable_176)%, '�' = '\177' %(printable_177)%,
'�' = '\178' %(printable_178)%, '�' = '\179' %(printable_179)%,
'�' = '\180' %(printable_180)%, '�' = '\181' %(printable_181)%,
'�' = '\182' %(printable_182)%, '�' = '\183' %(printable_183)%,
'�' = '\184' %(printable_184)%, '�' = '\185' %(printable_185)%,
'�' = '\186' %(printable_186)%, '�' = '\187' %(printable_187)%,
'�' = '\188' %(printable_188)%, '�' = '\189' %(printable_189)%,
'�' = '\190' %(printable_190)%, '�' = '\191' %(printable_191)%,
'�' = '\192' %(printable_192)%, '�' = '\193' %(printable_193)%,
'�' = '\194' %(printable_194)%, '�' = '\195' %(printable_195)%,
'�' = '\196' %(printable_196)%, '�' = '\197' %(printable_197)%,
'�' = '\198' %(printable_198)%, '�' = '\199' %(printable_199)%,
'�' = '\200' %(printable_200)%, '�' = '\201' %(printable_201)%,
'�' = '\202' %(printable_202)%, '�' = '\203' %(printable_203)%,
'�' = '\204' %(printable_204)%, '�' = '\205' %(printable_205)%,
'�' = '\206' %(printable_206)%, '�' = '\207' %(printable_207)%,
'�' = '\208' %(printable_208)%, '�' = '\209' %(printable_209)%,
'�' = '\210' %(printable_210)%, '�' = '\211' %(printable_211)%,
'�' = '\212' %(printable_212)%, '�' = '\213' %(printable_213)%,
'�' = '\214' %(printable_214)%, '�' = '\215' %(printable_215)%,
'�' = '\216' %(printable_216)%, '�' = '\217' %(printable_217)%,
'�' = '\218' %(printable_218)%, '�' = '\219' %(printable_219)%,
'�' = '\220' %(printable_220)%, '�' = '\221' %(printable_221)%,
'�' = '\222' %(printable_222)%, '�' = '\223' %(printable_223)%,
'�' = '\224' %(printable_224)%, '�' = '\225' %(printable_225)%,
'�' = '\226' %(printable_226)%, '�' = '\227' %(printable_227)%,
'�' = '\228' %(printable_228)%, '�' = '\229' %(printable_229)%,
'�' = '\230' %(printable_230)%, '�' = '\231' %(printable_231)%,
'�' = '\232' %(printable_232)%, '�' = '\233' %(printable_233)%,
'�' = '\234' %(printable_234)%, '�' = '\235' %(printable_235)%,
'�' = '\236' %(printable_236)%, '�' = '\237' %(printable_237)%,
'�' = '\238' %(printable_238)%, '�' = '\239' %(printable_239)%,
'�' = '\240' %(printable_240)%, '�' = '\241' %(printable_241)%,
'�' = '\242' %(printable_242)%, '�' = '\243' %(printable_243)%,
'�' = '\244' %(printable_244)%, '�' = '\245' %(printable_245)%,
'�' = '\246' %(printable_246)%, '�' = '\247' %(printable_247)%,
'�' = '\248' %(printable_248)%, '�' = '\249' %(printable_249)%,
'�' = '\250' %(printable_250)%, '�' = '\251' %(printable_251)%,
'�' = '\252' %(printable_252)%, '�' = '\253' %(printable_253)%,
'�' = '\254' %(printable_254)%, '�' = '\255' %(printable_255)%,
forall v1 : Char
. isLetter(v1)
<=> (ord('A') <= ord(v1) /\ ord(v1) <= ord('Z'))
\/ (ord('a') <= ord(v1) /\ ord(v1) <= ord('z'))
%(isLetter_def)%,
forall v1 : Char
. isDigit(v1) <=> ord('0') <= ord(v1) /\ ord(v1) <= ord('9')
%(isDigit_def)%,
forall v1 : Char
. isPrintable(v1)
<=> (ord(' ') <= ord(v1) /\ ord(v1) <= ord('~'))
\/ (ord(' ') <= ord(v1) /\ ord(v1) <= ord('�'))
%(isPrintable_def)%,
'\o000' : Char = '\000' : Char %(slash_o000)%,
'\o001' = '\001' %(slash_o001)%, '\o002' = '\002' %(slash_o002)%,
'\o003' = '\003' %(slash_o003)%, '\o004' = '\004' %(slash_o004)%,
'\o005' = '\005' %(slash_o005)%, '\o006' = '\006' %(slash_o006)%,
'\o007' = '\007' %(slash_o007)%, '\o010' = '\008' %(slash_o010)%,
'\o011' = '\009' %(slash_o011)%, '\o012' = '\010' %(slash_o012)%,
'\o013' = '\011' %(slash_o013)%, '\o014' = '\012' %(slash_o014)%,
'\o015' = '\013' %(slash_o015)%, '\o016' = '\014' %(slash_o016)%,
'\o017' = '\015' %(slash_o017)%, '\o020' = '\016' %(slash_o020)%,
'\o021' = '\017' %(slash_o021)%, '\o022' = '\018' %(slash_o022)%,
'\o023' = '\019' %(slash_o023)%, '\o024' = '\020' %(slash_o024)%,
'\o025' = '\021' %(slash_o025)%, '\o026' = '\022' %(slash_o026)%,
'\o027' = '\023' %(slash_o027)%, '\o030' = '\024' %(slash_o030)%,
'\o031' = '\025' %(slash_o031)%, '\o032' = '\026' %(slash_o032)%,
'\o033' = '\027' %(slash_o033)%, '\o034' = '\028' %(slash_o034)%,
'\o035' = '\029' %(slash_o035)%, '\o036' = '\030' %(slash_o036)%,
'\o037' = '\031' %(slash_o037)%, '\o040' = '\032' %(slash_o040)%,
'\o041' = '\033' %(slash_o041)%, '\o042' = '\034' %(slash_o042)%,
'\o043' = '\035' %(slash_o043)%, '\o044' = '\036' %(slash_o044)%,
'\o045' = '\037' %(slash_o045)%, '\o046' = '\038' %(slash_o046)%,
'\o047' = '\039' %(slash_o047)%, '\o050' = '\040' %(slash_o050)%,
'\o051' = '\041' %(slash_o051)%, '\o052' = '\042' %(slash_o052)%,
'\o053' = '\043' %(slash_o053)%, '\o054' = '\044' %(slash_o054)%,
'\o055' = '\045' %(slash_o055)%, '\o056' = '\046' %(slash_o056)%,
'\o057' = '\047' %(slash_o057)%, '\o060' = '\048' %(slash_o060)%,
'\o061' = '\049' %(slash_o061)%, '\o062' = '\050' %(slash_o062)%,
'\o063' = '\051' %(slash_o063)%, '\o064' = '\052' %(slash_o064)%,
'\o065' = '\053' %(slash_o065)%, '\o066' = '\054' %(slash_o066)%,
'\o067' = '\055' %(slash_o067)%, '\o070' = '\056' %(slash_o070)%,
'\o071' = '\057' %(slash_o071)%, '\o072' = '\058' %(slash_o072)%,
'\o073' = '\059' %(slash_o073)%, '\o074' = '\060' %(slash_o074)%,
'\o075' = '\061' %(slash_o075)%, '\o076' = '\062' %(slash_o076)%,
'\o077' = '\063' %(slash_o077)%, '\o100' = '\064' %(slash_o100)%,
'\o101' = '\065' %(slash_o101)%, '\o102' = '\066' %(slash_o102)%,
'\o103' = '\067' %(slash_o103)%, '\o104' = '\068' %(slash_o104)%,
'\o105' = '\069' %(slash_o105)%, '\o106' = '\070' %(slash_o106)%,
'\o107' = '\071' %(slash_o107)%, '\o110' = '\072' %(slash_o110)%,
'\o111' = '\073' %(slash_o111)%, '\o112' = '\074' %(slash_o112)%,
'\o113' = '\075' %(slash_o113)%, '\o114' = '\076' %(slash_o114)%,
'\o115' = '\077' %(slash_o115)%, '\o116' = '\078' %(slash_o116)%,
'\o117' = '\079' %(slash_o117)%, '\o120' = '\080' %(slash_o120)%,
'\o121' = '\081' %(slash_o121)%, '\o122' = '\082' %(slash_o122)%,
'\o123' = '\083' %(slash_o123)%, '\o124' = '\084' %(slash_o124)%,
'\o125' = '\085' %(slash_o125)%, '\o126' = '\086' %(slash_o126)%,
'\o127' = '\087' %(slash_o127)%, '\o130' = '\088' %(slash_o130)%,
'\o131' = '\089' %(slash_o131)%, '\o132' = '\090' %(slash_o132)%,
'\o133' = '\091' %(slash_o133)%, '\o134' = '\092' %(slash_o134)%,
'\o135' = '\093' %(slash_o135)%, '\o136' = '\094' %(slash_o136)%,
'\o137' = '\095' %(slash_o137)%, '\o140' = '\096' %(slash_o140)%,
'\o141' = '\097' %(slash_o141)%, '\o142' = '\098' %(slash_o142)%,
'\o143' = '\099' %(slash_o143)%, '\o144' = '\100' %(slash_o144)%,
'\o145' = '\101' %(slash_o145)%, '\o146' = '\102' %(slash_o146)%,
'\o147' = '\103' %(slash_o147)%, '\o150' = '\104' %(slash_o150)%,
'\o151' = '\105' %(slash_o151)%, '\o152' = '\106' %(slash_o152)%,
'\o153' = '\107' %(slash_o153)%, '\o154' = '\108' %(slash_o154)%,
'\o155' = '\109' %(slash_o155)%, '\o156' = '\110' %(slash_o156)%,
'\o157' = '\111' %(slash_o157)%, '\o160' = '\112' %(slash_o160)%,
'\o161' = '\113' %(slash_o161)%, '\o162' = '\114' %(slash_o162)%,
'\o163' = '\115' %(slash_o163)%, '\o164' = '\116' %(slash_o164)%,
'\o165' = '\117' %(slash_o165)%, '\o166' = '\118' %(slash_o166)%,
'\o167' = '\119' %(slash_o167)%, '\o170' = '\120' %(slash_o170)%,
'\o171' = '\121' %(slash_o171)%, '\o172' = '\122' %(slash_o172)%,
'\o173' = '\123' %(slash_o173)%, '\o174' = '\124' %(slash_o174)%,
'\o175' = '\125' %(slash_o175)%, '\o176' = '\126' %(slash_o176)%,
'\o177' = '\127' %(slash_o177)%, '\o200' = '\128' %(slash_o200)%,
'\o201' = '\129' %(slash_o201)%, '\o202' = '\130' %(slash_o202)%,
'\o203' = '\131' %(slash_o203)%, '\o204' = '\132' %(slash_o204)%,
'\o205' = '\133' %(slash_o205)%, '\o206' = '\134' %(slash_o206)%,
'\o207' = '\135' %(slash_o207)%, '\o210' = '\136' %(slash_o210)%,
'\o211' = '\137' %(slash_o211)%, '\o212' = '\138' %(slash_o212)%,
'\o213' = '\139' %(slash_o213)%, '\o214' = '\140' %(slash_o214)%,
'\o215' = '\141' %(slash_o215)%, '\o216' = '\142' %(slash_o216)%,
'\o217' = '\143' %(slash_o217)%, '\o220' = '\144' %(slash_o220)%,
'\o221' = '\145' %(slash_o221)%, '\o222' = '\146' %(slash_o222)%,
'\o223' = '\147' %(slash_o223)%, '\o224' = '\148' %(slash_o224)%,
'\o225' = '\149' %(slash_o225)%, '\o226' = '\150' %(slash_o226)%,
'\o227' = '\151' %(slash_o227)%, '\o230' = '\152' %(slash_o230)%,
'\o231' = '\153' %(slash_o231)%, '\o232' = '\154' %(slash_o232)%,
'\o233' = '\155' %(slash_o233)%, '\o234' = '\156' %(slash_o234)%,
'\o235' = '\157' %(slash_o235)%, '\o236' = '\158' %(slash_o236)%,
'\o237' = '\159' %(slash_o237)%, '\o240' = '\160' %(slash_o240)%,
'\o241' = '\161' %(slash_o241)%, '\o242' = '\162' %(slash_o242)%,
'\o243' = '\163' %(slash_o243)%, '\o244' = '\164' %(slash_o244)%,
'\o245' = '\165' %(slash_o245)%, '\o246' = '\166' %(slash_o246)%,
'\o247' = '\167' %(slash_o247)%, '\o250' = '\168' %(slash_o250)%,
'\o251' = '\169' %(slash_o251)%, '\o252' = '\170' %(slash_o252)%,
'\o253' = '\171' %(slash_o253)%, '\o254' = '\172' %(slash_o254)%,
'\o255' = '\173' %(slash_o255)%, '\o256' = '\174' %(slash_o256)%,
'\o257' = '\175' %(slash_o257)%, '\o260' = '\176' %(slash_o260)%,
'\o261' = '\177' %(slash_o261)%, '\o262' = '\178' %(slash_o262)%,
'\o263' = '\179' %(slash_o263)%, '\o264' = '\180' %(slash_o264)%,
'\o265' = '\181' %(slash_o265)%, '\o266' = '\182' %(slash_o266)%,
'\o267' = '\183' %(slash_o267)%, '\o270' = '\184' %(slash_o270)%,
'\o271' = '\185' %(slash_o271)%, '\o272' = '\186' %(slash_o272)%,
'\o273' = '\187' %(slash_o273)%, '\o274' = '\188' %(slash_o274)%,
'\o275' = '\189' %(slash_o275)%, '\o276' = '\190' %(slash_o276)%,
'\o277' = '\191' %(slash_o277)%, '\o300' = '\192' %(slash_o300)%,
'\o301' = '\193' %(slash_o301)%, '\o302' = '\194' %(slash_o302)%,
'\o303' = '\195' %(slash_o303)%, '\o304' = '\196' %(slash_o304)%,
'\o305' = '\197' %(slash_o305)%, '\o306' = '\198' %(slash_o306)%,
'\o307' = '\199' %(slash_o307)%, '\o310' = '\200' %(slash_o310)%,
'\o311' = '\201' %(slash_o311)%, '\o312' = '\202' %(slash_o312)%,
'\o313' = '\203' %(slash_o313)%, '\o314' = '\204' %(slash_o314)%,
'\o315' = '\205' %(slash_o315)%, '\o316' = '\206' %(slash_o316)%,
'\o317' = '\207' %(slash_o317)%, '\o320' = '\208' %(slash_o320)%,
'\o321' = '\209' %(slash_o321)%, '\o322' = '\210' %(slash_o322)%,
'\o323' = '\211' %(slash_o323)%, '\o324' = '\212' %(slash_o324)%,
'\o325' = '\213' %(slash_o325)%, '\o326' = '\214' %(slash_o326)%,
'\o327' = '\215' %(slash_o327)%, '\o330' = '\216' %(slash_o330)%,
'\o331' = '\217' %(slash_o331)%, '\o332' = '\218' %(slash_o332)%,
'\o333' = '\219' %(slash_o333)%, '\o334' = '\220' %(slash_o334)%,
'\o335' = '\221' %(slash_o335)%, '\o336' = '\222' %(slash_o336)%,
'\o337' = '\223' %(slash_o337)%, '\o340' = '\224' %(slash_o340)%,
'\o341' = '\225' %(slash_o341)%, '\o342' = '\226' %(slash_o342)%,
'\o343' = '\227' %(slash_o343)%, '\o344' = '\228' %(slash_o344)%,
'\o345' = '\229' %(slash_o345)%, '\o346' = '\230' %(slash_o346)%,
'\o347' = '\231' %(slash_o347)%, '\o350' = '\232' %(slash_o350)%,
'\o351' = '\233' %(slash_o351)%, '\o352' = '\234' %(slash_o352)%,
'\o353' = '\235' %(slash_o353)%, '\o354' = '\236' %(slash_o354)%,
'\o355' = '\237' %(slash_o355)%, '\o356' = '\238' %(slash_o356)%,
'\o357' = '\239' %(slash_o357)%, '\o360' = '\240' %(slash_o360)%,
'\o361' = '\241' %(slash_o361)%, '\o362' = '\242' %(slash_o362)%,
'\o363' = '\243' %(slash_o363)%, '\o364' = '\244' %(slash_o364)%,
'\o365' = '\245' %(slash_o365)%, '\o366' = '\246' %(slash_o366)%,
'\o367' = '\247' %(slash_o367)%, '\o370' = '\248' %(slash_o370)%,
'\o371' = '\249' %(slash_o371)%, '\o372' = '\250' %(slash_o372)%,
'\o373' = '\251' %(slash_o373)%, '\o374' = '\252' %(slash_o374)%,
'\o375' = '\253' %(slash_o375)%, '\o376' = '\254' %(slash_o376)%,
'\o377' : Char = '\255' : Char %(slash_o377)%,
'\x00' : Char = '\000' : Char %(slash_x00)%,
'\x01' = '\001' %(slash_x01)%, '\x02' = '\002' %(slash_x02)%,
'\x03' = '\003' %(slash_x03)%, '\x04' = '\004' %(slash_x04)%,
'\x05' = '\005' %(slash_x05)%, '\x06' = '\006' %(slash_x06)%,
'\x07' = '\007' %(slash_x07)%, '\x08' = '\008' %(slash_x08)%,
'\x09' = '\009' %(slash_x09)%, '\x0A' = '\010' %(slash_x0A)%,
'\x0B' = '\011' %(slash_x0B)%, '\x0C' = '\012' %(slash_x0C)%,
'\x0D' = '\013' %(slash_x0D)%, '\x0E' = '\014' %(slash_x0E)%,
'\x0F' = '\015' %(slash_x0F)%, '\x10' = '\016' %(slash_x10)%,
'\x11' = '\017' %(slash_x11)%, '\x12' = '\018' %(slash_x12)%,
'\x13' = '\019' %(slash_x13)%, '\x14' = '\020' %(slash_x14)%,
'\x15' = '\021' %(slash_x15)%, '\x16' = '\022' %(slash_x16)%,
'\x17' = '\023' %(slash_x17)%, '\x18' = '\024' %(slash_x18)%,
'\x19' = '\025' %(slash_x19)%, '\x1A' = '\026' %(slash_x1A)%,
'\x1B' = '\027' %(slash_x1B)%, '\x1C' = '\028' %(slash_x1C)%,
'\x1D' = '\029' %(slash_x1D)%, '\x1E' = '\030' %(slash_x1E)%,
'\x1F' = '\031' %(slash_x1F)%, '\x20' = '\032' %(slash_x20)%,
'\x21' = '\033' %(slash_x21)%, '\x22' = '\034' %(slash_x22)%,
'\x23' = '\035' %(slash_x23)%, '\x24' = '\036' %(slash_x24)%,
'\x25' = '\037' %(slash_x25)%, '\x26' = '\038' %(slash_x26)%,
'\x27' = '\039' %(slash_x27)%, '\x28' = '\040' %(slash_x28)%,
'\x29' = '\041' %(slash_x29)%, '\x2A' = '\042' %(slash_x2A)%,
'\x2B' = '\043' %(slash_x2B)%, '\x2C' = '\044' %(slash_x2C)%,
'\x2D' = '\045' %(slash_x2D)%, '\x2E' = '\046' %(slash_x2E)%,
'\x2F' = '\047' %(slash_x2F)%, '\x30' = '\048' %(slash_x30)%,
'\x31' = '\049' %(slash_x31)%, '\x32' = '\050' %(slash_x32)%,
'\x33' = '\051' %(slash_x33)%, '\x34' = '\052' %(slash_x34)%,
'\x35' = '\053' %(slash_x35)%, '\x36' = '\054' %(slash_x36)%,
'\x37' = '\055' %(slash_x37)%, '\x38' = '\056' %(slash_x38)%,
'\x39' = '\057' %(slash_x39)%, '\x3A' = '\058' %(slash_x3A)%,
'\x3B' = '\059' %(slash_x3B)%, '\x3C' = '\060' %(slash_x3C)%,
'\x3D' = '\061' %(slash_x3D)%, '\x3E' = '\062' %(slash_x3E)%,
'\x3F' = '\063' %(slash_x3F)%, '\x40' = '\064' %(slash_x40)%,
'\x41' = '\065' %(slash_x41)%, '\x42' = '\066' %(slash_x42)%,
'\x43' = '\067' %(slash_x43)%, '\x44' = '\068' %(slash_x44)%,
'\x45' = '\069' %(slash_x45)%, '\x46' = '\070' %(slash_x46)%,
'\x47' = '\071' %(slash_x47)%, '\x48' = '\072' %(slash_x48)%,
'\x49' = '\073' %(slash_x49)%, '\x4A' = '\074' %(slash_x4A)%,
'\x4B' = '\075' %(slash_x4B)%, '\x4C' = '\076' %(slash_x4C)%,
'\x4D' = '\077' %(slash_x4D)%, '\x4E' = '\078' %(slash_x4E)%,
'\x4F' = '\079' %(slash_x4F)%, '\x50' = '\080' %(slash_x50)%,
'\x51' = '\081' %(slash_x51)%, '\x52' = '\082' %(slash_x52)%,
'\x53' = '\083' %(slash_x53)%, '\x54' = '\084' %(slash_x54)%,
'\x55' = '\085' %(slash_x55)%, '\x56' = '\086' %(slash_x56)%,
'\x57' = '\087' %(slash_x57)%, '\x58' = '\088' %(slash_x58)%,
'\x59' = '\089' %(slash_x59)%, '\x5A' = '\090' %(slash_x5A)%,
'\x5B' = '\091' %(slash_x5B)%, '\x5C' = '\092' %(slash_x5C)%,
'\x5D' = '\093' %(slash_x5D)%, '\x5E' = '\094' %(slash_x5E)%,
'\x5F' = '\095' %(slash_x5F)%, '\x60' = '\096' %(slash_x60)%,
'\x61' = '\097' %(slash_x61)%, '\x62' = '\098' %(slash_x62)%,
'\x63' = '\099' %(slash_x63)%, '\x64' = '\100' %(slash_x64)%,
'\x65' = '\101' %(slash_x65)%, '\x66' = '\102' %(slash_x66)%,
'\x67' = '\103' %(slash_x67)%, '\x68' = '\104' %(slash_x68)%,
'\x69' = '\105' %(slash_x69)%, '\x6A' = '\106' %(slash_x6A)%,
'\x6B' = '\107' %(slash_x6B)%, '\x6C' = '\108' %(slash_x6C)%,
'\x6D' = '\109' %(slash_x6D)%, '\x6E' = '\110' %(slash_x6E)%,
'\x6F' = '\111' %(slash_x6F)%, '\x70' = '\112' %(slash_x70)%,
'\x71' = '\113' %(slash_x71)%, '\x72' = '\114' %(slash_x72)%,
'\x73' = '\115' %(slash_x73)%, '\x74' = '\116' %(slash_x74)%,
'\x75' = '\117' %(slash_x75)%, '\x76' = '\118' %(slash_x76)%,
'\x77' = '\119' %(slash_x77)%, '\x78' = '\120' %(slash_x78)%,
'\x79' = '\121' %(slash_x79)%, '\x7A' = '\122' %(slash_x7A)%,
'\x7B' = '\123' %(slash_x7B)%, '\x7C' = '\124' %(slash_x7C)%,
'\x7D' = '\125' %(slash_x7D)%, '\x7E' = '\126' %(slash_x7E)%,
'\x7F' = '\127' %(slash_x7F)%, '\x80' = '\128' %(slash_x80)%,
'\x81' = '\129' %(slash_x81)%, '\x82' = '\130' %(slash_x82)%,
'\x83' = '\131' %(slash_x83)%, '\x84' = '\132' %(slash_x84)%,
'\x85' = '\133' %(slash_x85)%, '\x86' = '\134' %(slash_x86)%,
'\x87' = '\135' %(slash_x87)%, '\x88' = '\136' %(slash_x88)%,
'\x89' = '\137' %(slash_x89)%, '\x8A' = '\138' %(slash_x8A)%,
'\x8B' = '\139' %(slash_x8B)%, '\x8C' = '\140' %(slash_x8C)%,
'\x8D' = '\141' %(slash_x8D)%, '\x8E' = '\142' %(slash_x8E)%,
'\x8F' = '\143' %(slash_x8F)%, '\x90' = '\144' %(slash_x90)%,
'\x91' = '\145' %(slash_x91)%, '\x92' = '\146' %(slash_x92)%,
'\x93' = '\147' %(slash_x93)%, '\x94' = '\148' %(slash_x94)%,
'\x95' = '\149' %(slash_x95)%, '\x96' = '\150' %(slash_x96)%,
'\x97' = '\151' %(slash_x97)%, '\x98' = '\152' %(slash_x98)%,
'\x99' = '\153' %(slash_x99)%, '\x9A' = '\154' %(slash_x9A)%,
'\x9B' = '\155' %(slash_x9B)%, '\x9C' = '\156' %(slash_x9C)%,
'\x9D' = '\157' %(slash_x9D)%, '\x9E' = '\158' %(slash_x9E)%,
'\x9F' = '\159' %(slash_x9F)%, '\xA0' = '\160' %(slash_xA0)%,
'\xA1' = '\161' %(slash_xA1)%, '\xA2' = '\162' %(slash_xA2)%,
'\xA3' = '\163' %(slash_xA3)%, '\xA4' = '\164' %(slash_xA4)%,
'\xA5' = '\165' %(slash_xA5)%, '\xA6' = '\166' %(slash_xA6)%,
'\xA7' = '\167' %(slash_xA7)%, '\xA8' = '\168' %(slash_xA8)%,
'\xA9' = '\169' %(slash_xA9)%, '\xAA' = '\170' %(slash_xAA)%,
'\xAB' = '\171' %(slash_xAB)%, '\xAC' = '\172' %(slash_xAC)%,
'\xAD' = '\173' %(slash_xAD)%, '\xAE' = '\174' %(slash_xAE)%,
'\xAF' = '\175' %(slash_xAF)%, '\xB0' = '\176' %(slash_xB0)%,
'\xB1' = '\177' %(slash_xB1)%, '\xB2' = '\178' %(slash_xB2)%,
'\xB3' = '\179' %(slash_xB3)%, '\xB4' = '\180' %(slash_xB4)%,
'\xB5' = '\181' %(slash_xB5)%, '\xB6' = '\182' %(slash_xB6)%,
'\xB7' = '\183' %(slash_xB7)%, '\xB8' = '\184' %(slash_xB8)%,
'\xB9' = '\185' %(slash_xB9)%, '\xBA' = '\186' %(slash_xBA)%,
'\xBB' = '\187' %(slash_xBB)%, '\xBC' = '\188' %(slash_xBC)%,
'\xBD' = '\189' %(slash_xBD)%, '\xBE' = '\190' %(slash_xBE)%,
'\xBF' = '\191' %(slash_xBF)%, '\xC0' = '\192' %(slash_xC0)%,
'\xC1' = '\193' %(slash_xC1)%, '\xC2' = '\194' %(slash_xC2)%,
'\xC3' = '\195' %(slash_xC3)%, '\xC4' = '\196' %(slash_xC4)%,
'\xC5' = '\197' %(slash_xC5)%, '\xC6' = '\198' %(slash_xC6)%,
'\xC7' = '\199' %(slash_xC7)%, '\xC8' = '\200' %(slash_xC8)%,
'\xC9' = '\201' %(slash_xC9)%, '\xCA' = '\202' %(slash_xCA)%,
'\xCB' = '\203' %(slash_xCB)%, '\xCC' = '\204' %(slash_xCC)%,
'\xCD' = '\205' %(slash_xCD)%, '\xCE' = '\206' %(slash_xCE)%,
'\xCF' = '\207' %(slash_xCF)%, '\xD0' = '\208' %(slash_xD0)%,
'\xD1' = '\209' %(slash_xD1)%, '\xD2' = '\210' %(slash_xD2)%,
'\xD3' = '\211' %(slash_xD3)%, '\xD4' = '\212' %(slash_xD4)%,
'\xD5' = '\213' %(slash_xD5)%, '\xD6' = '\214' %(slash_xD6)%,
'\xD7' = '\215' %(slash_xD7)%, '\xD8' = '\216' %(slash_xD8)%,
'\xD9' = '\217' %(slash_xD9)%, '\xDA' = '\218' %(slash_xDA)%,
'\xDB' = '\219' %(slash_xDB)%, '\xDC' = '\220' %(slash_xDC)%,
'\xDD' = '\221' %(slash_xDD)%, '\xDE' = '\222' %(slash_xDE)%,
'\xDF' = '\223' %(slash_xDF)%, '\xE0' = '\224' %(slash_xE0)%,
'\xE1' = '\225' %(slash_xE1)%, '\xE2' = '\226' %(slash_xE2)%,
'\xE3' = '\227' %(slash_xE3)%, '\xE4' = '\228' %(slash_xE4)%,
'\xE5' = '\229' %(slash_xE5)%, '\xE6' = '\230' %(slash_xE6)%,
'\xE7' = '\231' %(slash_xE7)%, '\xE8' = '\232' %(slash_xE8)%,
'\xE9' = '\233' %(slash_xE9)%, '\xEA' = '\234' %(slash_xEA)%,
'\xEB' = '\235' %(slash_xEB)%, '\xEC' = '\236' %(slash_xEC)%,
'\xED' = '\237' %(slash_xED)%, '\xEE' = '\238' %(slash_xEE)%,
'\xEF' = '\239' %(slash_xEF)%, '\xF0' = '\240' %(slash_xF0)%,
'\xF1' = '\241' %(slash_xF1)%, '\xF2' = '\242' %(slash_xF2)%,
'\xF3' = '\243' %(slash_xF3)%, '\xF4' = '\244' %(slash_xF4)%,
'\xF5' = '\245' %(slash_xF5)%, '\xF6' = '\246' %(slash_xF6)%,
'\xF7' = '\247' %(slash_xF7)%, '\xF8' = '\248' %(slash_xF8)%,
'\xF9' = '\249' %(slash_xF9)%, '\xFA' = '\250' %(slash_xFA)%,
'\xFB' = '\251' %(slash_xFB)%, '\xFC' = '\252' %(slash_xFC)%,
'\xFD' = '\253' %(slash_xFD)%, '\xFE' = '\254' %(slash_xFE)%,
'\xFF' : Char = '\255' : Char %(slash_xFF)%,
NUL = '\000' %(NUL_def)%, SOH = '\001' %(SOH_def)%,
SYX = '\002' %(SYX_def)%, ETX = '\003' %(ETX_def)%,
EOT = '\004' %(EOT_def)%, ENQ = '\005' %(ENQ_def)%,
ACK = '\006' %(ACK_def)%, BEL = '\007' %(BEL_def)%,
BS = '\008' %(BS_def)%, HT = '\009' %(HT_def)%,
LF = '\010' %(LF_def)%, VT = '\011' %(VT_def)%,
FF = '\012' %(FF_def)%, CR = '\013' %(CR_def)%,
SO = '\014' %(SO_def)%, SI = '\015' %(SI_def)%,
DLE = '\016' %(DLE_def)%, DC1 = '\017' %(DC1_def)%,
DC2 = '\018' %(DC2_def)%, DC3 = '\019' %(DC3_def)%,
DC4 = '\020' %(DC4_def)%, NAK = '\021' %(NAK_def)%,
SYN = '\022' %(SYN_def)%, ETB = '\023' %(ETB_def)%,
CAN = '\024' %(CAN_def)%, EM = '\025' %(EM_def)%,
SUB = '\026' %(SUB_def)%, ESC = '\027' %(ESC_def)%,
FS = '\028' %(FS_def)%, GS = '\029' %(GS_def)%,
RS = '\030' %(RS_def)%, US = '\031' %(US_def)%,
SP = '\032' %(SP_def)%, DEL = '\127' %(DEL_def)%,
NL = LF %(NL_def)%, NP = FF %(NP_def)%, '\n' = NL %(slash_n)%,
'\t' = HT %(slash_t)%, '\v' = VT %(slash_v)%,
'\b' = BS %(slash_b)%, '\r' = CR %(slash_r)%,
'\f' = FF %(slash_f)%, '\a' = BEL %(slash_a)%,
'\?' = '?' %(slash_quest)%,
forall v1, v2, v3 : a . (v1 || v2) || v3 = v1 || (v2 || v3)
%(ga_assoc___||__)%,
(b || b) || b = b])
### Hint 17.9-17.11, redeclared as total 'min'
### Hint 17.14-17.16, 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-98.12, redeclared op 'min'
### Hint 98.15-98.17, redeclared op 'max'
### Hint 121.18-121.20, redeclared sort 'Int'
### Hint 121.12-121.14, redeclared sort 'Nat'
*** Error 147.8-147.16,
ambiguous mixfix term
-__(__-__(a, b))
-(__-__(a, b))
### Hint 209.17-209.19, redeclared sort 'Rat'
### Hint 209.11-209.13, 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.4-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-285.18, unknown sort 's2'
*** Error 285.20-285.21, unknown sort 's1'
*** Error 285.31, unknown sort 'a'
### Warning 285.34, new 'op a' is also known as 'var a'
### Warning 285.36, new 'op b' is also known as 'var b'
### Hint 285.41, redeclared op 'a'
### Warning 285.41, new 'op a' is also known as 'var a'
*** Error 285.34, duplicates at '(285,41)' for 'a : s -> t'
*** Error 285.52, unknown sort 'a'
### Warning 285.25,
total selectors 'a : s -> t, b : s -> t, d : s -> t'
should be in alternative
'c : s'
### Warning 285.50,
total selectors 'a : s -> t, b : s -> t, d : s -> t'
should be in alternative
'c : a ->? s'
### Hint 286.11, redeclared sort 's'
### Hint 286.22, redeclared subsort 's2 < s'
### 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'
### Warning 286.39, new 'op a' is also known as 'var a'
### Hint 286.41, redeclared op 'b'
### Warning 286.41, new 'op b' is also known as 'var b'
### Hint 286.46, redeclared op 'd'
*** Error 286.55, unknown sort 'a'
### Hint 286.53, redeclared op 'c'
### Warning 286.30,
total selectors 'a : s -> t, b : s -> t, d : s -> t'
should be in alternative
'c : s'
### Warning 286.53,
total selectors 'a : s -> t, b : s -> t, d : s -> t'
should be in alternative
'c : a ->? s'
*** Error 286.53, illegal free partial constructor 'c'
### Hint 287.16, redeclared sort 's'
### Hint 287.27, redeclared subsort 's2 < s'
### 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'
### Warning 287.44, new 'op a' is also known as 'var a'
### Hint 287.46, redeclared op 'b'
### Warning 287.46, new 'op b' is also known as 'var b'
### Hint 287.51, redeclared op 'd'
*** Error 287.60, unknown sort 'a'
### Hint 287.58, redeclared op 'c'
### Warning 287.35,
total selectors 'a : s -> t, b : s -> t, d : s -> t'
should be in alternative
'c : s'
### Warning 287.58,
total selectors 'a : s -> t, b : s -> t, d : s -> t'
should be in alternative
'c : a ->? s'
*** Error 290.16, unknown sort 'a'
*** Error 290.20, unknown sort 'a'
### Hint 290.6-290.12, redeclared pred '__<__'
*** Error 292.7, unknown sort 'b'
### Warning 292.4, new 'op a' is also known as 'var 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'
### Hint 294.17, redeclared subsort 's2 < s'
### 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'
### Warning 294.41, new 'op a' is also known as 'var a'
### Hint 294.43, redeclared op 'b'
### Warning 294.43, new 'op b' is also known as 'var 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'
### Warning 294.25,
total selectors 'a : s -> t, b : s -> t, d : s -> t'
should be in alternative
'c : s'
### Warning 294.29,
total selectors 'a : s -> t, b : s -> t, d : s -> t'
should be in alternative
'c : a -> s'
### Warning 294.55,
total selectors 'a : s -> t, b : s -> t, d : s -> t'
should be in alternative
'c : a ->? s'
### Warning 293.9, generated sorts without constructor '{t}'
### Warning 292.13, non-generated sorts as constructor result '{b}'
### Hint 300.6, redeclared sort 's'
### Hint 301.6, redeclared sort 't'
*** Error 304.6, unknown sort 'b'
### Hint 304.4, redeclared op 'a'
### Warning 304.4, new 'op a' is also known as 'var a'
*** Error 305.6, unknown sort 'd'
### Hint 308.6, known variable shadowed 'a'
### Warning 308.6, new 'var a' is also known as 'op a'
### Hint 309.9, known variable shadowed 'a'
### Warning 309.9, new 'var a' is also known as 'op a'
### Hint 309.11, known variable shadowed 'b'
### Warning 309.11, new 'var b' is also known as 'op 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-336.50, 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.9-351.16, 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, new 'op a' is also known as 'var a'
### Warning 360.9, new 'op b' is also known as 'var b'
### Warning 363.9, partially redeclared 'a'
### Warning 363.9, new 'op a' is also known as 'var a'
### Warning 364.9, partially redeclared 'b'
### Warning 364.9, new 'op b' is also known as 'var b'
### Warning 365.9, partially redeclared 'c'
### Warning 366.9, partially redeclared 'c'
### Hint 367.9, redeclared op 'a'
### Warning 367.9, new 'op a' is also known as 'var a'
### Warning 368.11, unused local variable 'x'
### Warning 368.13, unused local variable 'y'
### Warning 368.17, unused local variable 'z'
### Warning 369.9, partially redeclared 'a'
### Warning 369.9, new 'op a' is also known as 'var a'
### Warning 370.9, partially redeclared 'c'
### Warning 370.11, unused local variable 'x'
### Warning 370.13, unused local variable 'y'
### Warning 370.17, unused local variable 'z'
### Hint 373.12, redeclared sort 's'
### Hint 373.14, redeclared sort 't'
### Warning 374.11, new 'pred a' is also known as 'op a'
### Warning 374.11, new 'pred a' is also known as 'var a'
### Warning 375.11, new 'pred b' is also known as 'op b'
### Warning 375.11, new 'pred b' is also known as 'var b'
### Warning 376.12, new 'pred c' is also known as 'op c'
### Warning 377.12, new 'pred c' is also known as 'op c'
### Warning 381.11, new 'pred c' is also known as 'op c'
### Warning 382.21, new 'op a' is also known as 'pred a'
### Warning 382.21, new 'op a' is also known as 'var a'
### Warning 382.25, new 'op b' is also known as 'pred b'
### Warning 382.25, new 'op b' is also known as 'var b'
### Warning 382.29, new 'op c' is also known as 'pred c'
### Hint 384.64-384.67, redeclared op 'sel2'
### Hint 384.77-384.80, redeclared op 'sel1'
### Hint 386.65-386.68, redeclared op 'sel2'
### Hint 386.78-386.81, redeclared op 'sel1'
### Hint 388.27-388.31, redeclared sort 'Data1'
### Hint 388.34-388.38, redeclared sort 'Data2'
### Hint 388.41-388.45, redeclared sort 'Data3'
### Hint 393.22-393.24, redeclared sort 'Set'
### Hint 393.30-393.31, redeclared op 'Mt'
### Hint 393.35-393.37, 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'
### Hint 426.26,
no matching predicate with 0 arguments found for 'e'
*** Error 426.26, not a formula 'e'
### Hint 427.8, known variable shadowed 'x'
### Hint 427.12,
no matching predicate with 0 arguments found for 'e'
*** Error 427.12, not a formula '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, new 'var c' is also known as 'op c'
### Warning 451.20, new 'var c' is also known as 'pred c'
### Hint 811.11-811.13, redeclared op '' ''
### Hint 1486.6, redeclared sort 'a'
### Warning 1489.4, new 'op b' is also known as 'pred b'
### Warning 1489.4, new 'op b' is also known as 'var b'
### Warning 309.11, unused variable 'b'
### Warning 402.20-402.21, unused variable 'r2'