(*#line 57.10 "ofmc-fp.lex"*)functor OfmcFpParserLexFun(structure Tokens: OfmcFpParser_TOKENS)(*#line 1.1 "ofmc-fp.lex.sml"*) = struct structure UserDeclarations = struct (*#line 1.1 "ofmc-fp.lex"*)(***************************************************************************** * Isabelle-OFMC --- Connecting OFMC and Isabelle/HOL * * ofmc-fp.lex --- * This file is part of Isabelle-OFMC. * * Copyright (c) 2009 Achim D. Brucker, Germany * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are met: * * * Redistributions of source code must retain the above copyright notice, this * list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above copyright notice, * this list of conditions and the following disclaimer in the documentation * and/or other materials provided with the distribution. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) structure Tokens = Tokens type pos = int * int * int type svalue = Tokens.svalue type ('a,'b) token = ('a,'b) Tokens.token type lexresult= (svalue,pos) token val pos = ref (0,0,0) fun eof () = Tokens.EOF((!pos,!pos)) fun error (e,p : (int * int * int),_) = TextIO.output (TextIO.stdOut, String.concat[ "line ", (Int.toString ((#1 p)+1)), "/", (Int.toString (#2 p - #3 p)),": ", e, "\n" ]) fun inputPos yypos = ((#1 (!pos), yypos - (#3(!pos)), (#3 (!pos))), (#1 (!pos), yypos - (#3(!pos)), (#3 (!pos)))) fun inputPos_half yypos = (#1 (!pos), yypos - (#3(!pos)), (#3 (!pos))) (*#line 61.1 "ofmc-fp.lex.sml"*) end (* end of user routines *) exception LexError (* raised if illegal leaf action tried *) structure Internal = struct datatype yyfinstate = N of int type statedata = {fin : yyfinstate list, trans: string} (* transition & final state table *) val tab = let val s = [ (0, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000" ), (1, "\003\003\003\003\003\003\003\003\003\224\226\003\003\003\003\003\ \\003\003\003\003\003\003\003\003\003\003\003\003\003\003\003\003\ \\224\003\223\003\003\003\003\003\205\204\003\003\203\201\003\190\ \\007\007\007\007\007\007\007\007\007\007\189\188\003\186\003\003\ \\003\175\168\161\151\148\128\007\007\125\007\116\007\007\007\007\ \\108\007\007\098\093\007\007\007\090\007\007\089\003\088\003\007\ \\003\072\007\007\007\007\062\007\007\050\007\007\007\007\007\007\ \\007\007\039\023\007\007\007\009\007\007\007\006\005\004\003\003\ \\003" ), (7, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (9, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\017\008\008\008\008\008\008\ \\008\008\010\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (10, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\011\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (11, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\012\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (12, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\013\008\008\008\008\008\000\000\000\000\000\ \\000" ), (13, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\014\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (14, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\015\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (15, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\016\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (17, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\018\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (18, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\019\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (19, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\020\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (20, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\021\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (21, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\022\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (23, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\030\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\024\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (24, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\027\008\008\008\025\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (25, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\026\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (27, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\028\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (28, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\029\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (30, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\031\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (31, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\036\008\032\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (32, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\033\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (33, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\034\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (34, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\035\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (36, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\037\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (37, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\038\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (39, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\044\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\040\008\008\008\008\008\000\000\000\000\000\ \\000" ), (40, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\041\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (41, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\042\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (42, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\043\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (44, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\045\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (45, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\046\008\008\008\008\008\000\000\000\000\000\ \\000" ), (46, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\047\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (47, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\048\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (48, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\049\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (50, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\057\008\008\051\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (51, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\052\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (52, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\053\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (53, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\054\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (54, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\055\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (55, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\056\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (57, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\058\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (58, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\059\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (59, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\060\008\008\008\000\000\000\000\000\ \\000" ), (60, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\061\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (62, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\063\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (63, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\064\008\008\000\000\000\000\000\ \\000" ), (64, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\065\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (65, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\066\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (66, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\067\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (67, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\068\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (68, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\069\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (69, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\070\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (70, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\071\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (72, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\078\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\073\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (73, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\074\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (74, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\075\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (75, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\076\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (76, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\077\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (78, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\079\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (79, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\080\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (80, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\081\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (81, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\082\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (82, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\083\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (83, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\084\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (84, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\085\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (85, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\086\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (86, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\087\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (90, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\091\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (91, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\092\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (93, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\094\008\000\000\000\000\000\ \\000" ), (94, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\095\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (95, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\096\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (96, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\097\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (98, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\103\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\099\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (99, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\100\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (100, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\101\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (101, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\102\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (103, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\104\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (104, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\105\008\000\000\000\000\000\ \\000" ), (105, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\106\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (106, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\107\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (108, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\109\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (109, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\110\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (110, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\111\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (111, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\112\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (112, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\113\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (113, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\114\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (114, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\115\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (116, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\117\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (117, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\118\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (118, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\119\008\008\008\000\000\000\000\000\ \\000" ), (119, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\120\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (120, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\121\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (121, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\122\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (122, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\123\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (123, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\124\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (125, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\126\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (126, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\127\008\008\008\008\000\000\000\000\000\ \\000" ), (128, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\142\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\139\008\008\008\008\008\008\008\129\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (129, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\130\008\008\000\000\000\000\000\ \\000" ), (130, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\131\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (131, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\132\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (132, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\133\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (133, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\134\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000" ), (134, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\135\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000" ), (135, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\136\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000" ), (136, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\137\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000" ), (137, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\138\000\000\000\000\000\000\000\000\000\000\000\ \\000" ), (139, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\140\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (140, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\141\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (142, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\143\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (143, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\144\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (144, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\145\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (145, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\146\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (146, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\147\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (148, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\149\008\008\000\000\000\000\000\ \\000" ), (149, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\150\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (151, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\152\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (152, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\153\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (153, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\154\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (154, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\155\008\008\008\008\000\000\000\000\000\ \\000" ), (155, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\156\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (156, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\157\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (157, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\158\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (158, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\159\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (159, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\160\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (161, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\166\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\162\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (162, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\163\008\000\000\000\000\000\ \\000" ), (163, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\164\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (164, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\165\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (166, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\167\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (168, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\169\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (169, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\170\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (170, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\171\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (171, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\172\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (172, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\173\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (173, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\174\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (175, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\176\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (176, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\177\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (177, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\178\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (178, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\179\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (179, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\180\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (180, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\181\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (181, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\182\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (182, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\183\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (183, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\184\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (184, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\000\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\008\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\008\ \\000\008\008\008\008\008\008\008\008\008\008\008\008\008\185\008\ \\008\008\008\008\008\008\008\008\008\008\008\000\000\000\000\000\ \\000" ), (186, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\187\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000" ), (190, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\192\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\191\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000" ), (192, "\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193\193\193\193\193\193\193\193\193\193\194\193\193\193\193\200\ \\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193" ), (193, "\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193\193\193\193\193\193\193\193\193\193\194\193\193\193\193\193\ \\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193" ), (194, "\195\195\195\195\195\195\195\195\195\195\195\195\195\195\195\195\ \\195\195\195\195\195\195\195\195\195\195\195\195\195\195\195\195\ \\195\195\195\195\195\195\195\195\195\195\198\195\195\195\195\197\ \\195\195\195\195\195\195\195\195\195\195\195\195\195\195\195\195\ \\195\195\195\195\195\195\195\195\195\195\195\195\195\195\195\195\ \\195\195\195\195\195\195\195\195\195\195\195\195\195\195\195\195\ \\195\195\195\195\195\195\195\195\195\195\195\195\195\195\195\195\ \\195\195\195\195\195\195\195\195\195\195\195\195\195\195\195\195\ \\195" ), (195, "\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193\193\193\193\193\193\193\193\193\193\194\193\193\193\193\196\ \\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193" ), (196, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\195\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000" ), (198, "\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193\193\193\193\193\193\193\193\193\193\194\193\193\193\193\199\ \\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\193\ \\193" ), (201, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\202\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000" ), (205, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\215\000\000\000\000\206\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000" ), (206, "\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\ \\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\ \\207\207\207\207\207\207\207\207\214\207\210\207\207\207\207\208\ \\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\ \\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\ \\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\ \\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\ \\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\ \\207" ), (207, "\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\ \\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\ \\207\207\207\207\207\207\207\207\207\207\210\207\207\207\207\208\ \\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\ \\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\ \\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\ \\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\ \\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\ \\207" ), (208, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\209\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000" ), (210, "\209\209\209\209\209\209\209\209\209\209\209\209\209\209\209\209\ \\209\209\209\209\209\209\209\209\209\209\209\209\209\209\209\209\ \\209\209\209\209\209\209\209\209\209\213\211\209\209\209\209\000\ \\209\209\209\209\209\209\209\209\209\209\209\209\209\209\209\209\ \\209\209\209\209\209\209\209\209\209\209\209\209\209\209\209\209\ \\209\209\209\209\209\209\209\209\209\209\209\209\209\209\209\209\ \\209\209\209\209\209\209\209\209\209\209\209\209\209\209\209\209\ \\209\209\209\209\209\209\209\209\209\209\209\209\209\209\209\209\ \\209" ), (211, "\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\ \\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\ \\207\207\207\207\207\207\207\207\207\212\210\207\207\207\207\208\ \\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\ \\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\ \\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\ \\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\ \\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\207\ \\207" ), (215, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\216\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000" ), (216, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\217\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000" ), (217, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\218\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000" ), (218, "\000\000\000\000\000\000\000\000\000\000\219\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000" ), (219, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\220\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000" ), (220, "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\221\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000" ), (221, "\000\000\000\000\000\000\000\000\000\000\222\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000" ), (224, "\000\000\000\000\000\000\000\000\000\225\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\225\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ \\000" ), (0, "")] fun f x = x val s = map f (rev (tl (rev s))) exception LexHackingError fun look ((j,x)::r, i: int) = if i = j then x else look(r, i) | look ([], i) = raise LexHackingError fun g {fin=x, trans=i} = {fin=x, trans=look(s,i)} in Vector.fromList(map g [{fin = [], trans = 0}, {fin = [], trans = 1}, {fin = [], trans = 1}, {fin = [(N 300)], trans = 0}, {fin = [(N 44),(N 300)], trans = 0}, {fin = [(N 56),(N 300)], trans = 0}, {fin = [(N 42),(N 300)], trans = 0}, {fin = [(N 298),(N 300)], trans = 7}, {fin = [(N 298)], trans = 7}, {fin = [(N 298),(N 300)], trans = 9}, {fin = [(N 298)], trans = 10}, {fin = [(N 298)], trans = 11}, {fin = [(N 298)], trans = 12}, {fin = [(N 298)], trans = 13}, {fin = [(N 298)], trans = 14}, {fin = [(N 298)], trans = 15}, {fin = [(N 234),(N 298)], trans = 7}, {fin = [(N 298)], trans = 17}, {fin = [(N 298)], trans = 18}, {fin = [(N 298)], trans = 19}, {fin = [(N 298)], trans = 20}, {fin = [(N 298)], trans = 21}, {fin = [(N 217),(N 298)], trans = 7}, {fin = [(N 298),(N 300)], trans = 23}, {fin = [(N 298)], trans = 24}, {fin = [(N 298)], trans = 25}, {fin = [(N 257),(N 298)], trans = 7}, {fin = [(N 298)], trans = 27}, {fin = [(N 298)], trans = 28}, {fin = [(N 101),(N 298)], trans = 7}, {fin = [(N 298)], trans = 30}, {fin = [(N 298)], trans = 31}, {fin = [(N 298)], trans = 32}, {fin = [(N 298)], trans = 33}, {fin = [(N 298)], trans = 34}, {fin = [(N 81),(N 298)], trans = 7}, {fin = [(N 298)], trans = 36}, {fin = [(N 298)], trans = 37}, {fin = [(N 241),(N 298)], trans = 7}, {fin = [(N 298),(N 300)], trans = 39}, {fin = [(N 298)], trans = 40}, {fin = [(N 298)], trans = 41}, {fin = [(N 298)], trans = 42}, {fin = [(N 87),(N 298)], trans = 7}, {fin = [(N 298)], trans = 44}, {fin = [(N 298)], trans = 45}, {fin = [(N 298)], trans = 46}, {fin = [(N 298)], trans = 47}, {fin = [(N 298)], trans = 48}, {fin = [(N 225),(N 298)], trans = 7}, {fin = [(N 298),(N 300)], trans = 50}, {fin = [(N 298)], trans = 51}, {fin = [(N 298)], trans = 52}, {fin = [(N 298)], trans = 53}, {fin = [(N 298)], trans = 54}, {fin = [(N 298)], trans = 55}, {fin = [(N 95),(N 298)], trans = 7}, {fin = [(N 298)], trans = 57}, {fin = [(N 298)], trans = 58}, {fin = [(N 298)], trans = 59}, {fin = [(N 298)], trans = 60}, {fin = [(N 202),(N 298)], trans = 7}, {fin = [(N 298),(N 300)], trans = 62}, {fin = [(N 298)], trans = 63}, {fin = [(N 298)], trans = 64}, {fin = [(N 298)], trans = 65}, {fin = [(N 298)], trans = 66}, {fin = [(N 298)], trans = 67}, {fin = [(N 298)], trans = 68}, {fin = [(N 298)], trans = 69}, {fin = [(N 298)], trans = 70}, {fin = [(N 112),(N 298)], trans = 7}, {fin = [(N 298),(N 300)], trans = 72}, {fin = [(N 298)], trans = 73}, {fin = [(N 298)], trans = 74}, {fin = [(N 298)], trans = 75}, {fin = [(N 298)], trans = 76}, {fin = [(N 209),(N 298)], trans = 7}, {fin = [(N 298)], trans = 78}, {fin = [(N 298)], trans = 79}, {fin = [(N 298)], trans = 80}, {fin = [(N 298)], trans = 81}, {fin = [(N 298)], trans = 82}, {fin = [(N 298)], trans = 83}, {fin = [(N 298)], trans = 84}, {fin = [(N 298)], trans = 85}, {fin = [(N 298)], trans = 86}, {fin = [(N 124),(N 298)], trans = 7}, {fin = [(N 70),(N 300)], trans = 0}, {fin = [(N 68),(N 300)], trans = 0}, {fin = [(N 298),(N 300)], trans = 90}, {fin = [(N 298)], trans = 91}, {fin = [(N 280),(N 298)], trans = 7}, {fin = [(N 298),(N 300)], trans = 93}, {fin = [(N 298)], trans = 94}, {fin = [(N 298)], trans = 95}, {fin = [(N 298)], trans = 96}, {fin = [(N 147),(N 298)], trans = 7}, {fin = [(N 298),(N 300)], trans = 98}, {fin = [(N 298)], trans = 99}, {fin = [(N 298)], trans = 100}, {fin = [(N 298)], trans = 101}, {fin = [(N 187),(N 298)], trans = 7}, {fin = [(N 298)], trans = 103}, {fin = [(N 298)], trans = 104}, {fin = [(N 298)], trans = 105}, {fin = [(N 298)], trans = 106}, {fin = [(N 264),(N 298)], trans = 7}, {fin = [(N 298),(N 300)], trans = 108}, {fin = [(N 298)], trans = 109}, {fin = [(N 298)], trans = 110}, {fin = [(N 298)], trans = 111}, {fin = [(N 298)], trans = 112}, {fin = [(N 298)], trans = 113}, {fin = [(N 298)], trans = 114}, {fin = [(N 133),(N 298)], trans = 7}, {fin = [(N 298),(N 300)], trans = 116}, {fin = [(N 298)], trans = 117}, {fin = [(N 298)], trans = 118}, {fin = [(N 298)], trans = 119}, {fin = [(N 298)], trans = 120}, {fin = [(N 298)], trans = 121}, {fin = [(N 298)], trans = 122}, {fin = [(N 298)], trans = 123}, {fin = [(N 157),(N 298)], trans = 7}, {fin = [(N 298),(N 300)], trans = 125}, {fin = [(N 298)], trans = 126}, {fin = [(N 272),(N 298)], trans = 7}, {fin = [(N 298),(N 300)], trans = 128}, {fin = [(N 298)], trans = 129}, {fin = [(N 298)], trans = 130}, {fin = [(N 298)], trans = 131}, {fin = [(N 298)], trans = 132}, {fin = [], trans = 133}, {fin = [], trans = 134}, {fin = [], trans = 135}, {fin = [], trans = 136}, {fin = [], trans = 137}, {fin = [(N 169)], trans = 0}, {fin = [(N 298)], trans = 139}, {fin = [(N 298)], trans = 140}, {fin = [(N 246),(N 298)], trans = 7}, {fin = [(N 298)], trans = 142}, {fin = [(N 298)], trans = 143}, {fin = [(N 298)], trans = 144}, {fin = [(N 298)], trans = 145}, {fin = [(N 298)], trans = 146}, {fin = [(N 195),(N 298)], trans = 7}, {fin = [(N 298),(N 300)], trans = 148}, {fin = [(N 298)], trans = 149}, {fin = [(N 276),(N 298)], trans = 7}, {fin = [(N 298),(N 300)], trans = 151}, {fin = [(N 298)], trans = 152}, {fin = [(N 298)], trans = 153}, {fin = [(N 298)], trans = 154}, {fin = [(N 298)], trans = 155}, {fin = [(N 298)], trans = 156}, {fin = [(N 298)], trans = 157}, {fin = [(N 298)], trans = 158}, {fin = [(N 298)], trans = 159}, {fin = [(N 291),(N 298)], trans = 7}, {fin = [(N 298),(N 300)], trans = 161}, {fin = [(N 298)], trans = 162}, {fin = [(N 298)], trans = 163}, {fin = [(N 298)], trans = 164}, {fin = [(N 252),(N 298)], trans = 7}, {fin = [(N 298)], trans = 166}, {fin = [(N 268),(N 298)], trans = 7}, {fin = [(N 298),(N 300)], trans = 168}, {fin = [(N 298)], trans = 169}, {fin = [(N 298)], trans = 170}, {fin = [(N 298)], trans = 171}, {fin = [(N 298)], trans = 172}, {fin = [(N 298)], trans = 173}, {fin = [(N 141),(N 298)], trans = 7}, {fin = [(N 298),(N 300)], trans = 175}, {fin = [(N 298)], trans = 176}, {fin = [(N 298)], trans = 177}, {fin = [(N 298)], trans = 178}, {fin = [(N 298)], trans = 179}, {fin = [(N 298)], trans = 180}, {fin = [(N 298)], trans = 181}, {fin = [(N 298)], trans = 182}, {fin = [(N 298)], trans = 183}, {fin = [(N 298)], trans = 184}, {fin = [(N 181),(N 298)], trans = 7}, {fin = [(N 51),(N 300)], trans = 186}, {fin = [(N 73)], trans = 0}, {fin = [(N 62),(N 300)], trans = 0}, {fin = [(N 49),(N 300)], trans = 0}, {fin = [(N 300)], trans = 190}, {fin = [(N 54)], trans = 0}, {fin = [], trans = 192}, {fin = [], trans = 193}, {fin = [], trans = 194}, {fin = [], trans = 195}, {fin = [], trans = 196}, {fin = [(N 23)], trans = 0}, {fin = [], trans = 198}, {fin = [(N 23)], trans = 196}, {fin = [], trans = 192}, {fin = [(N 40),(N 300)], trans = 201}, {fin = [(N 47)], trans = 0}, {fin = [(N 60),(N 300)], trans = 0}, {fin = [(N 66),(N 300)], trans = 0}, {fin = [(N 64),(N 300)], trans = 205}, {fin = [], trans = 206}, {fin = [], trans = 207}, {fin = [], trans = 208}, {fin = [], trans = 207}, {fin = [], trans = 210}, {fin = [], trans = 211}, {fin = [(N 35)], trans = 207}, {fin = [(N 35)], trans = 207}, {fin = [], trans = 206}, {fin = [], trans = 215}, {fin = [], trans = 216}, {fin = [], trans = 217}, {fin = [], trans = 218}, {fin = [], trans = 219}, {fin = [], trans = 220}, {fin = [], trans = 221}, {fin = [(N 11)], trans = 0}, {fin = [(N 58),(N 300)], trans = 0}, {fin = [(N 38),(N 300)], trans = 224}, {fin = [(N 38)], trans = 224}, {fin = [(N 1)], trans = 0}]) end structure StartStates = struct datatype yystartstate = STARTSTATE of int (* start state definitions *) val INITIAL = STARTSTATE 1; end type result = UserDeclarations.lexresult exception LexerError (* raised if illegal leaf action tried *) end structure YYPosInt : INTEGER = Int fun makeLexer yyinput = let val yygone0= YYPosInt.fromInt ~1 val yyb = ref "\n" (* buffer *) val yybl = ref 1 (*buffer length *) val yybufpos = ref 1 (* location of next character to use *) val yygone = ref yygone0 (* position in file of beginning of buffer *) val yydone = ref false (* eof found yet? *) val yybegin = ref 1 (*Current 'start state' for lexer *) val YYBEGIN = fn (Internal.StartStates.STARTSTATE x) => yybegin := x fun lex () : Internal.result = let fun continue() = lex() in let fun scan (s,AcceptingLeaves : Internal.yyfinstate list list,l,i0) = let fun action (i,nil) = raise LexError | action (i,nil::l) = action (i-1,l) | action (i,(node::acts)::l) = case node of Internal.N yyk => (let fun yymktext() = substring(!yyb,i0,i-i0) val yypos = YYPosInt.+(YYPosInt.fromInt i0, !yygone) open UserDeclarations Internal.StartStates in (yybufpos := i; case yyk of (* Application actions *) 1 => ((*#line 63.14 "ofmc-fp.lex"*)pos := ((#1 (!pos)) + 1, yypos - (#3(!pos)),yypos ); lex()(*#line 2241.1 "ofmc-fp.lex.sml"*) ) | 101 => let val yytext=yymktext() in (*#line 93.20 "ofmc-fp.lex"*)Tokens.TSECSTATE(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2243.1 "ofmc-fp.lex.sml"*) end | 11 => ((*#line 65.20 "ofmc-fp.lex"*)pos := ((#1 (!pos)) + 1, yypos - (#3(!pos)),yypos ); lex()(*#line 2245.1 "ofmc-fp.lex.sml"*) ) | 112 => let val yytext=yymktext() in (*#line 94.20 "ofmc-fp.lex"*)Tokens.TFIXEDPOINT(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2247.1 "ofmc-fp.lex.sml"*) end | 124 => let val yytext=yymktext() in (*#line 95.20 "ofmc-fp.lex"*)Tokens.TABSTRACTION(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2249.1 "ofmc-fp.lex.sml"*) end | 133 => let val yytext=yymktext() in (*#line 96.20 "ofmc-fp.lex"*)Tokens.TPROTOCOL(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2251.1 "ofmc-fp.lex.sml"*) end | 141 => let val yytext=yymktext() in (*#line 97.20 "ofmc-fp.lex"*)Tokens.TBACKEND(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2253.1 "ofmc-fp.lex.sml"*) end | 147 => let val yytext=yymktext() in (*#line 98.20 "ofmc-fp.lex"*)Tokens.TTYPES(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2255.1 "ofmc-fp.lex.sml"*) end | 157 => let val yytext=yymktext() in (*#line 99.20 "ofmc-fp.lex"*)Tokens.TKNOWLEDGE(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2257.1 "ofmc-fp.lex.sml"*) end | 169 => let val yytext=yymktext() in (*#line 100.20 "ofmc-fp.lex"*)Tokens.TFIXEDPOINT(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2259.1 "ofmc-fp.lex.sml"*) end | 181 => let val yytext=yymktext() in (*#line 101.20 "ofmc-fp.lex"*)Tokens.TABSTRACTION(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2261.1 "ofmc-fp.lex.sml"*) end | 187 => let val yytext=yymktext() in (*#line 102.20 "ofmc-fp.lex"*)Tokens.TSTATE(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2263.1 "ofmc-fp.lex.sml"*) end | 195 => let val yytext=yymktext() in (*#line 103.20 "ofmc-fp.lex"*)Tokens.TFPState(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2265.1 "ofmc-fp.lex.sml"*) end | 202 => let val yytext=yymktext() in (*#line 104.20 "ofmc-fp.lex"*)Tokens.TIKNOWS(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2267.1 "ofmc-fp.lex.sml"*) end | 209 => let val yytext=yymktext() in (*#line 105.20 "ofmc-fp.lex"*)Tokens.TATTACK(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2269.1 "ofmc-fp.lex.sml"*) end | 217 => let val yytext=yymktext() in (*#line 106.20 "ofmc-fp.lex"*)Tokens.TWITNESS(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2271.1 "ofmc-fp.lex.sml"*) end | 225 => let val yytext=yymktext() in (*#line 107.20 "ofmc-fp.lex"*)Tokens.TREQUEST(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2273.1 "ofmc-fp.lex.sml"*) end | 23 => ((*#line 67.46 "ofmc-fp.lex"*)lex()(*#line 2275.1 "ofmc-fp.lex.sml"*) ) | 234 => let val yytext=yymktext() in (*#line 108.21 "ofmc-fp.lex"*)Tokens.TREQUEST(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2277.1 "ofmc-fp.lex.sml"*) end | 241 => let val yytext=yymktext() in (*#line 109.20 "ofmc-fp.lex"*)Tokens.TSECRET(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2279.1 "ofmc-fp.lex.sml"*) end | 246 => let val yytext=yymktext() in (*#line 110.20 "ofmc-fp.lex"*)Tokens.TFACT(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2281.1 "ofmc-fp.lex.sml"*) end | 252 => let val yytext=yymktext() in (*#line 111.20 "ofmc-fp.lex"*)Tokens.TCRYPT(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2283.1 "ofmc-fp.lex.sml"*) end | 257 => let val yytext=yymktext() in (*#line 112.20 "ofmc-fp.lex"*)Tokens.TSTEP(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2285.1 "ofmc-fp.lex.sml"*) end | 264 => let val yytext=yymktext() in (*#line 113.20 "ofmc-fp.lex"*)Tokens.TSCRYPT(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2287.1 "ofmc-fp.lex.sml"*) end | 268 => let val yytext=yymktext() in (*#line 114.20 "ofmc-fp.lex"*)Tokens.TCAT(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2289.1 "ofmc-fp.lex.sml"*) end | 272 => let val yytext=yymktext() in (*#line 115.20 "ofmc-fp.lex"*)Tokens.TINV(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2291.1 "ofmc-fp.lex.sml"*) end | 276 => let val yytext=yymktext() in (*#line 116.20 "ofmc-fp.lex"*)Tokens.TEXP(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2293.1 "ofmc-fp.lex.sml"*) end | 280 => let val yytext=yymktext() in (*#line 117.20 "ofmc-fp.lex"*)Tokens.TXOR(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2295.1 "ofmc-fp.lex.sml"*) end | 291 => let val yytext=yymktext() in (*#line 118.20 "ofmc-fp.lex"*)Tokens.TDERIVATION(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2297.1 "ofmc-fp.lex.sml"*) end | 298 => let val yytext=yymktext() in (*#line 120.31 "ofmc-fp.lex"*)Tokens.SIMPLE_NAME(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2299.1 "ofmc-fp.lex.sml"*) end | 300 => let val yytext=yymktext() in (*#line 122.12 "ofmc-fp.lex"*)error ("ignoring bad character "^yytext, ((#1 (!pos), yypos - (#3(!pos)), (#3 (!pos)))), ((#1 (!pos), yypos - (#3(!pos)), (#3 (!pos))))); lex()(*#line 2304.1 "ofmc-fp.lex.sml"*) end | 35 => ((*#line 69.46 "ofmc-fp.lex"*)lex()(*#line 2306.1 "ofmc-fp.lex.sml"*) ) | 38 => ((*#line 71.14 "ofmc-fp.lex"*)pos := (#1 (!pos), yypos - (#3(!pos)), (#3 (!pos))); lex()(*#line 2308.1 "ofmc-fp.lex.sml"*) ) | 40 => let val yytext=yymktext() in (*#line 74.19 "ofmc-fp.lex"*)Tokens.TMINUS(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2310.1 "ofmc-fp.lex.sml"*) end | 42 => let val yytext=yymktext() in (*#line 75.20 "ofmc-fp.lex"*)Tokens.TOBRACE(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2312.1 "ofmc-fp.lex.sml"*) end | 44 => let val yytext=yymktext() in (*#line 76.20 "ofmc-fp.lex"*)Tokens.TCBRACE(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2314.1 "ofmc-fp.lex.sml"*) end | 47 => let val yytext=yymktext() in (*#line 77.20 "ofmc-fp.lex"*)Tokens.TARROW(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2316.1 "ofmc-fp.lex.sml"*) end | 49 => let val yytext=yymktext() in (*#line 78.20 "ofmc-fp.lex"*)Tokens.TCOLON(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2318.1 "ofmc-fp.lex.sml"*) end | 51 => let val yytext=yymktext() in (*#line 79.20 "ofmc-fp.lex"*)Tokens.TEQ(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2320.1 "ofmc-fp.lex.sml"*) end | 54 => let val yytext=yymktext() in (*#line 80.20 "ofmc-fp.lex"*)Tokens.TNEQ(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2322.1 "ofmc-fp.lex.sml"*) end | 56 => let val yytext=yymktext() in (*#line 81.20 "ofmc-fp.lex"*)Tokens.TBAR(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2324.1 "ofmc-fp.lex.sml"*) end | 58 => let val yytext=yymktext() in (*#line 82.20 "ofmc-fp.lex"*)Tokens.TQUOTE(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2326.1 "ofmc-fp.lex.sml"*) end | 60 => let val yytext=yymktext() in (*#line 83.20 "ofmc-fp.lex"*)Tokens.TCOMMA(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2328.1 "ofmc-fp.lex.sml"*) end | 62 => let val yytext=yymktext() in (*#line 84.20 "ofmc-fp.lex"*)Tokens.TSEMICOLON(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2330.1 "ofmc-fp.lex.sml"*) end | 64 => let val yytext=yymktext() in (*#line 85.20 "ofmc-fp.lex"*)Tokens.TOPAREN(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2332.1 "ofmc-fp.lex.sml"*) end | 66 => let val yytext=yymktext() in (*#line 86.20 "ofmc-fp.lex"*)Tokens.TCPAREN(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2334.1 "ofmc-fp.lex.sml"*) end | 68 => let val yytext=yymktext() in (*#line 87.20 "ofmc-fp.lex"*)Tokens.TOBRACKET(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2336.1 "ofmc-fp.lex.sml"*) end | 70 => let val yytext=yymktext() in (*#line 88.20 "ofmc-fp.lex"*)Tokens.TCBRACKET(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2338.1 "ofmc-fp.lex.sml"*) end | 73 => let val yytext=yymktext() in (*#line 89.20 "ofmc-fp.lex"*)Tokens.TMETAIMPLIES(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2340.1 "ofmc-fp.lex.sml"*) end | 81 => let val yytext=yymktext() in (*#line 90.20 "ofmc-fp.lex"*)Tokens.TSECTION(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2342.1 "ofmc-fp.lex.sml"*) end | 87 => let val yytext=yymktext() in (*#line 91.20 "ofmc-fp.lex"*)Tokens.TRULES(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2344.1 "ofmc-fp.lex.sml"*) end | 95 => let val yytext=yymktext() in (*#line 92.20 "ofmc-fp.lex"*)Tokens.TINITIAL(yytext,inputPos_half yypos,inputPos_half yypos)(*#line 2346.1 "ofmc-fp.lex.sml"*) end | _ => raise Internal.LexerError ) end ) val {fin,trans} = Vector.sub(Internal.tab, s) val NewAcceptingLeaves = fin::AcceptingLeaves in if l = !yybl then if trans = #trans(Vector.sub(Internal.tab,0)) then action(l,NewAcceptingLeaves ) else let val newchars= if !yydone then "" else yyinput 1024 in if (size newchars)=0 then (yydone := true; if (l=i0) then UserDeclarations.eof () else action(l,NewAcceptingLeaves)) else (if i0=l then yyb := newchars else yyb := substring(!yyb,i0,l-i0)^newchars; yygone := YYPosInt.+(!yygone, YYPosInt.fromInt i0); yybl := size (!yyb); scan (s,AcceptingLeaves,l-i0,0)) end else let val NewChar = Char.ord(CharVector.sub(!yyb,l)) val NewChar = if NewChar<128 then NewChar else 128 val NewState = Char.ord(CharVector.sub(trans,NewChar)) in if NewState=0 then action(l,NewAcceptingLeaves) else scan(NewState,NewAcceptingLeaves,l+1,i0) end end (* val start= if substring(!yyb,!yybufpos-1,1)="\n" then !yybegin+1 else !yybegin *) in scan(!yybegin (* start *),nil,!yybufpos,!yybufpos) end end in lex end end