# HG changeset patch # User sultana # Date 1378241201 -3600 # Node ID f26f00cbd5739fd6e65502929064d9513d5e9875 # Parent 5278312037f8b6c7d6c7169bde04eea7134fed65 updated TPTP parser to conform to version 5.4.0; clarified abstract syntax for 'let' in TPTP_Syntax (and in the parser); improved parsing of 'let' (in TFF) -- previously it wasn't looking at the structure of the definition; fixed bug when parsing 'let' (in TFF and THF) -- was only keeping the first quantified variable, and ignoring the rest; added comments to remind that 'let' support for THF is currently broken in TPTP; diff -r 5278312037f8 -r f26f00cbd573 src/HOL/TPTP/TPTP_Parser/tptp.yacc --- a/src/HOL/TPTP/TPTP_Parser/tptp.yacc Tue Sep 03 21:46:41 2013 +0100 +++ b/src/HOL/TPTP/TPTP_Parser/tptp.yacc Tue Sep 03 21:46:41 2013 +0100 @@ -183,10 +183,13 @@ | tptp_file of tptp_problem | tptp of tptp_problem - | thf_let_defn of tptp_let list + | thf_let_term_defn of tptp_let + | thf_let_formula_defn of tptp_let | tff_let of tptp_formula - | tff_let_term_defn of tptp_let list - | tff_let_formula_defn of tptp_let list + | tff_let_term_defn of tptp_let + | tff_let_term_binding of tptp_term + | tff_let_formula_defn of tptp_let + | tff_let_formula_binding of tptp_formula | tff_quantified_type of tptp_type | tff_monotype of tptp_type | tff_type_arguments of tptp_type list @@ -229,7 +232,7 @@ Parser for TPTP languages. Latest version of the language spec can be obtained from http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html - This implements version 5.3.0. + Our parser implements version 5.4.0 of that spec. *) tptp : tptp_file (( tptp_file )) @@ -333,15 +336,28 @@ Conditional (thf_logic_formula1, thf_logic_formula2, thf_logic_formula3) )) -thf_let : LET_TF LPAREN thf_let_defn COMMA thf_formula RPAREN (( - Let (thf_let_defn, thf_formula) -)) +(*NOTE support for Let in THF is still broken (cf. the spec). + When it gets fixed, look at how TFF support is encoded in this file + (to possibly replicate some of the checks done there)*) +thf_let : LET_TF LPAREN thf_let_term_defn COMMA thf_formula RPAREN (( Let (thf_let_term_defn, thf_formula) )) + | LET_FF LPAREN thf_let_formula_defn COMMA thf_formula RPAREN (( Let (thf_let_formula_defn, thf_formula) )) -(*FIXME here could check that fmla is of right form (TPTP BNF L130-134)*) -thf_let_defn : thf_quantified_formula (( +(*FIXME here could check that fmla is of right form (TPTP BNF (v5.3.0) L130-134) + i.e. it should have "=" or "<=>" at the top level. + We deviate from the spec by not checking this here, but "Let" support in THF + is still not fully specified. +*) +thf_let_term_defn : thf_quantified_formula (( let val (_, vars, fmla) = extract_quant_info thf_quantified_formula - in [Let_fmla (hd vars, fmla)] + in Let_fmla (vars, fmla) + end +)) +(*NOTE "thf_let_formula_defn" has the same definition as "thf_let_term_defn" (as per the spec)*) +thf_let_formula_defn : thf_quantified_formula (( + let + val (_, vars, fmla) = extract_quant_info thf_quantified_formula + in Let_fmla (vars, fmla) end )) @@ -431,21 +447,19 @@ tff_let : LET_TF LPAREN tff_let_term_defn COMMA tff_formula RPAREN ((Let (tff_let_term_defn, tff_formula) )) | LET_FF LPAREN tff_let_formula_defn COMMA tff_formula RPAREN (( Let (tff_let_formula_defn, tff_formula) )) -(*FIXME here could check that fmla is of right form (TPTP BNF L210-214)*) -(*FIXME why "term" if using "Let_fmla"?*) -tff_let_term_defn : tff_quantified_formula (( - let - val (_, vars, fmla) = extract_quant_info tff_quantified_formula - in [Let_fmla (hd vars, fmla)] - end + +tff_let_term_defn : EXCLAMATION LBRKT tff_variable_list RBRKT COLON tff_let_term_binding (( Let_term (tff_variable_list, tff_let_term_binding) )) + | tff_let_term_binding (( Let_term ([], tff_let_term_binding) )) + +tff_let_term_binding : term EQUALS term (( + Term_Func (Interpreted_ExtraLogic Apply, [term1, term2]) )) -(*FIXME here could check that fmla is of right form (TPTP BNF L215-217)*) -tff_let_formula_defn : tff_quantified_formula (( - let - val (_, vars, fmla) = extract_quant_info tff_quantified_formula - in [Let_fmla (hd vars, fmla)] - end +tff_let_formula_defn : EXCLAMATION LBRKT tff_variable_list RBRKT COLON tff_let_formula_binding (( Let_fmla (tff_variable_list, tff_let_formula_binding) )) + | tff_let_formula_binding (( Let_fmla ([], tff_let_formula_binding) )) + +tff_let_formula_binding : atomic_formula IFF tff_unitary_formula (( + Fmla (Interpreted_Logic Iff, [atomic_formula, tff_unitary_formula]) )) tff_sequent : tff_tuple GENTZEN_ARROW tff_tuple (( Sequent (tff_tuple1, tff_tuple2) )) diff -r 5278312037f8 -r f26f00cbd573 src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML --- a/src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML Tue Sep 03 21:46:41 2013 +0100 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML Tue Sep 03 21:46:41 2013 +0100 @@ -1484,94 +1484,96 @@ local open LrTable in val table=let val actionRows = "\ -\\001\000\001\000\052\002\002\000\052\002\004\000\069\002\005\000\052\002\ -\\006\000\052\002\009\000\052\002\010\000\052\002\011\000\052\002\ -\\012\000\052\002\019\000\052\002\020\000\052\002\021\000\052\002\ -\\022\000\052\002\026\000\052\002\027\000\052\002\037\000\052\002\ -\\059\000\052\002\060\000\052\002\000\000\ -\\001\000\001\000\055\002\002\000\055\002\004\000\070\002\005\000\055\002\ -\\006\000\055\002\009\000\055\002\010\000\055\002\011\000\055\002\ -\\012\000\055\002\019\000\055\002\020\000\055\002\021\000\055\002\ -\\022\000\055\002\026\000\055\002\027\000\055\002\037\000\055\002\ -\\059\000\055\002\060\000\055\002\000\000\ -\\001\000\001\000\219\002\005\000\219\002\006\000\234\002\010\000\219\002\ -\\011\000\219\002\012\000\219\002\019\000\219\002\020\000\234\002\ -\\021\000\219\002\022\000\219\002\026\000\219\002\027\000\219\002\ -\\037\000\219\002\000\000\ -\\001\000\001\000\222\002\005\000\222\002\006\000\245\002\010\000\222\002\ -\\011\000\222\002\012\000\222\002\019\000\222\002\020\000\245\002\ -\\021\000\222\002\022\000\222\002\026\000\222\002\027\000\222\002\ -\\037\000\222\002\000\000\ -\\001\000\001\000\229\002\005\000\229\002\006\000\236\002\010\000\229\002\ -\\011\000\229\002\012\000\229\002\019\000\229\002\020\000\236\002\ -\\021\000\229\002\022\000\229\002\026\000\229\002\027\000\229\002\ -\\037\000\229\002\000\000\ -\\001\000\001\000\239\002\004\000\130\002\005\000\239\002\006\000\239\002\ -\\010\000\239\002\011\000\239\002\012\000\239\002\016\000\222\000\ -\\019\000\239\002\020\000\239\002\021\000\239\002\022\000\239\002\ -\\027\000\239\002\037\000\239\002\000\000\ -\\001\000\001\000\252\002\004\000\131\002\005\000\252\002\006\000\252\002\ -\\010\000\252\002\011\000\252\002\012\000\252\002\016\000\217\000\ -\\019\000\252\002\020\000\252\002\021\000\252\002\022\000\252\002\ -\\027\000\252\002\037\000\252\002\000\000\ -\\001\000\001\000\211\000\003\000\210\000\006\000\209\000\007\000\124\000\ -\\010\000\208\000\011\000\207\000\012\000\206\000\013\000\035\000\ -\\015\000\205\000\016\000\204\000\019\000\203\000\020\000\202\000\ -\\021\000\201\000\022\000\200\000\025\000\121\000\028\000\120\000\ -\\037\000\199\000\044\000\101\000\045\000\100\000\046\000\034\000\ +\\001\000\001\000\077\002\002\000\077\002\004\000\096\002\005\000\077\002\ +\\006\000\077\002\009\000\077\002\010\000\077\002\011\000\077\002\ +\\012\000\077\002\019\000\077\002\020\000\077\002\021\000\077\002\ +\\022\000\077\002\026\000\077\002\027\000\077\002\037\000\077\002\ +\\059\000\077\002\060\000\077\002\000\000\ +\\001\000\001\000\080\002\002\000\080\002\004\000\097\002\005\000\080\002\ +\\006\000\080\002\009\000\080\002\010\000\080\002\011\000\080\002\ +\\012\000\080\002\019\000\080\002\020\000\080\002\021\000\080\002\ +\\022\000\080\002\026\000\080\002\027\000\080\002\037\000\080\002\ +\\059\000\080\002\060\000\080\002\000\000\ +\\001\000\001\000\250\002\005\000\250\002\006\000\009\003\010\000\250\002\ +\\011\000\250\002\012\000\250\002\019\000\250\002\020\000\009\003\ +\\021\000\250\002\022\000\250\002\026\000\250\002\027\000\250\002\ +\\037\000\250\002\000\000\ +\\001\000\001\000\253\002\005\000\253\002\006\000\020\003\010\000\253\002\ +\\011\000\253\002\012\000\253\002\019\000\253\002\020\000\020\003\ +\\021\000\253\002\022\000\253\002\026\000\253\002\027\000\253\002\ +\\037\000\253\002\000\000\ +\\001\000\001\000\004\003\005\000\004\003\006\000\011\003\010\000\004\003\ +\\011\000\004\003\012\000\004\003\019\000\004\003\020\000\011\003\ +\\021\000\004\003\022\000\004\003\026\000\004\003\027\000\004\003\ +\\037\000\004\003\000\000\ +\\001\000\001\000\014\003\004\000\161\002\005\000\014\003\006\000\014\003\ +\\010\000\014\003\011\000\014\003\012\000\014\003\016\000\223\000\ +\\019\000\014\003\020\000\014\003\021\000\014\003\022\000\014\003\ +\\027\000\014\003\037\000\014\003\000\000\ +\\001\000\001\000\027\003\004\000\162\002\005\000\027\003\006\000\027\003\ +\\010\000\027\003\011\000\027\003\012\000\027\003\016\000\218\000\ +\\019\000\027\003\020\000\027\003\021\000\027\003\022\000\027\003\ +\\027\000\027\003\037\000\027\003\000\000\ +\\001\000\001\000\212\000\003\000\211\000\006\000\210\000\007\000\124\000\ +\\010\000\209\000\011\000\208\000\012\000\207\000\013\000\035\000\ +\\015\000\206\000\016\000\205\000\019\000\204\000\020\000\203\000\ +\\021\000\202\000\022\000\201\000\025\000\121\000\028\000\120\000\ +\\037\000\200\000\044\000\101\000\045\000\100\000\046\000\034\000\ \\047\000\033\000\049\000\032\000\050\000\099\000\051\000\031\000\ -\\053\000\098\000\055\000\198\000\056\000\197\000\057\000\196\000\ -\\058\000\195\000\062\000\194\000\063\000\193\000\064\000\097\000\ +\\053\000\098\000\055\000\199\000\056\000\198\000\057\000\197\000\ +\\058\000\196\000\062\000\195\000\063\000\194\000\064\000\097\000\ \\065\000\096\000\068\000\030\000\069\000\029\000\070\000\028\000\ -\\071\000\027\000\072\000\192\000\073\000\095\000\074\000\191\000\ -\\076\000\094\000\077\000\093\000\000\000\ -\\001\000\001\000\211\000\003\000\210\000\006\000\209\000\007\000\124\000\ -\\010\000\208\000\011\000\207\000\012\000\206\000\013\000\035\000\ -\\016\000\033\001\019\000\203\000\020\000\202\000\021\000\201\000\ -\\022\000\200\000\025\000\121\000\026\000\032\001\028\000\120\000\ -\\037\000\199\000\044\000\101\000\045\000\100\000\046\000\034\000\ +\\071\000\027\000\072\000\193\000\073\000\095\000\074\000\192\000\ +\\075\000\191\000\076\000\094\000\077\000\093\000\000\000\ +\\001\000\001\000\212\000\003\000\211\000\006\000\210\000\007\000\124\000\ +\\010\000\209\000\011\000\208\000\012\000\207\000\013\000\035\000\ +\\016\000\035\001\019\000\204\000\020\000\203\000\021\000\202\000\ +\\022\000\201\000\025\000\121\000\026\000\034\001\028\000\120\000\ +\\037\000\200\000\044\000\101\000\045\000\100\000\046\000\034\000\ \\047\000\033\000\049\000\032\000\050\000\099\000\051\000\031\000\ -\\053\000\098\000\055\000\198\000\056\000\197\000\057\000\196\000\ -\\058\000\195\000\062\000\194\000\063\000\193\000\064\000\097\000\ +\\053\000\098\000\055\000\199\000\056\000\198\000\057\000\197\000\ +\\058\000\196\000\062\000\195\000\063\000\194\000\064\000\097\000\ \\065\000\096\000\068\000\030\000\069\000\029\000\070\000\028\000\ -\\071\000\027\000\072\000\192\000\073\000\095\000\074\000\191\000\ -\\076\000\094\000\077\000\093\000\000\000\ -\\001\000\001\000\211\000\003\000\210\000\006\000\209\000\007\000\124\000\ -\\010\000\208\000\011\000\207\000\012\000\206\000\013\000\035\000\ -\\016\000\033\001\019\000\203\000\020\000\202\000\021\000\201\000\ -\\022\000\200\000\025\000\121\000\028\000\120\000\037\000\199\000\ +\\071\000\027\000\072\000\193\000\073\000\095\000\074\000\192\000\ +\\075\000\191\000\076\000\094\000\077\000\093\000\000\000\ +\\001\000\001\000\212\000\003\000\211\000\006\000\210\000\007\000\124\000\ +\\010\000\209\000\011\000\208\000\012\000\207\000\013\000\035\000\ +\\016\000\035\001\019\000\204\000\020\000\203\000\021\000\202\000\ +\\022\000\201\000\025\000\121\000\028\000\120\000\037\000\200\000\ \\044\000\101\000\045\000\100\000\046\000\034\000\047\000\033\000\ \\049\000\032\000\050\000\099\000\051\000\031\000\053\000\098\000\ -\\055\000\198\000\056\000\197\000\057\000\196\000\058\000\195\000\ -\\062\000\194\000\063\000\193\000\064\000\097\000\065\000\096\000\ +\\055\000\199\000\056\000\198\000\057\000\197\000\058\000\196\000\ +\\062\000\195\000\063\000\194\000\064\000\097\000\065\000\096\000\ \\068\000\030\000\069\000\029\000\070\000\028\000\071\000\027\000\ -\\072\000\192\000\073\000\095\000\074\000\191\000\076\000\094\000\ -\\077\000\093\000\000\000\ -\\001\000\001\000\211\000\003\000\210\000\006\000\209\000\007\000\124\000\ -\\010\000\208\000\011\000\207\000\012\000\206\000\013\000\035\000\ -\\016\000\110\001\019\000\203\000\020\000\202\000\021\000\201\000\ -\\022\000\200\000\025\000\121\000\028\000\120\000\037\000\199\000\ +\\072\000\193\000\073\000\095\000\074\000\192\000\075\000\191\000\ +\\076\000\094\000\077\000\093\000\000\000\ +\\001\000\001\000\212\000\003\000\211\000\006\000\210\000\007\000\124\000\ +\\010\000\209\000\011\000\208\000\012\000\207\000\013\000\035\000\ +\\016\000\116\001\019\000\204\000\020\000\203\000\021\000\202\000\ +\\022\000\201\000\025\000\121\000\028\000\120\000\037\000\200\000\ \\044\000\101\000\045\000\100\000\046\000\034\000\047\000\033\000\ \\049\000\032\000\050\000\099\000\051\000\031\000\053\000\098\000\ -\\055\000\198\000\056\000\197\000\057\000\196\000\058\000\195\000\ -\\062\000\194\000\063\000\193\000\064\000\097\000\065\000\096\000\ +\\055\000\199\000\056\000\198\000\057\000\197\000\058\000\196\000\ +\\062\000\195\000\063\000\194\000\064\000\097\000\065\000\096\000\ \\068\000\030\000\069\000\029\000\070\000\028\000\071\000\027\000\ -\\072\000\192\000\073\000\095\000\074\000\191\000\076\000\094\000\ -\\077\000\093\000\000\000\ -\\001\000\001\000\015\001\002\000\014\001\005\000\034\002\006\000\209\000\ -\\009\000\073\002\010\000\208\000\011\000\207\000\012\000\206\000\ -\\019\000\203\000\020\000\202\000\021\000\201\000\022\000\200\000\ -\\026\000\034\002\027\000\034\002\037\000\013\001\059\000\073\002\ -\\060\000\073\002\000\000\ -\\001\000\003\000\210\000\007\000\124\000\025\000\121\000\055\000\198\000\ -\\056\000\197\000\062\000\194\000\063\000\193\000\000\000\ -\\001\000\004\000\250\000\000\000\ -\\001\000\004\000\016\001\000\000\ -\\001\000\004\000\205\001\000\000\ -\\001\000\004\000\217\001\000\000\ -\\001\000\004\000\224\001\000\000\ -\\001\000\004\000\255\001\000\000\ -\\001\000\005\000\132\002\009\000\139\002\027\000\132\002\000\000\ +\\072\000\193\000\073\000\095\000\074\000\192\000\075\000\191\000\ +\\076\000\094\000\077\000\093\000\000\000\ +\\001\000\001\000\016\001\002\000\015\001\005\000\059\002\006\000\210\000\ +\\009\000\100\002\010\000\209\000\011\000\208\000\012\000\207\000\ +\\019\000\204\000\020\000\203\000\021\000\202\000\022\000\201\000\ +\\026\000\059\002\027\000\059\002\037\000\014\001\059\000\100\002\ +\\060\000\100\002\000\000\ +\\001\000\003\000\211\000\007\000\124\000\025\000\121\000\055\000\199\000\ +\\056\000\198\000\062\000\195\000\063\000\194\000\000\000\ +\\001\000\004\000\251\000\000\000\ +\\001\000\004\000\017\001\000\000\ +\\001\000\004\000\222\001\000\000\ +\\001\000\004\000\234\001\000\000\ +\\001\000\004\000\241\001\000\000\ +\\001\000\004\000\018\002\000\000\ +\\001\000\004\000\019\002\000\000\ +\\001\000\004\000\022\002\000\000\ +\\001\000\005\000\163\002\009\000\170\002\027\000\163\002\000\000\ \\001\000\005\000\041\000\000\000\ \\001\000\005\000\042\000\000\000\ \\001\000\005\000\043\000\000\000\ @@ -1580,19 +1582,21 @@ \\001\000\005\000\055\000\000\000\ \\001\000\005\000\056\000\000\000\ \\001\000\005\000\057\000\000\000\ -\\001\000\005\000\158\001\000\000\ -\\001\000\005\000\159\001\000\000\ -\\001\000\005\000\160\001\000\000\ -\\001\000\005\000\177\001\000\000\ -\\001\000\005\000\178\001\000\000\ -\\001\000\005\000\179\001\000\000\ -\\001\000\005\000\187\001\000\000\ -\\001\000\005\000\188\001\000\000\ -\\001\000\005\000\238\001\000\000\ -\\001\000\005\000\249\001\000\000\ -\\001\000\005\000\252\001\000\000\ -\\001\000\006\000\209\000\000\000\ -\\001\000\006\000\209\000\020\000\202\000\000\000\ +\\001\000\005\000\166\001\000\000\ +\\001\000\005\000\169\001\000\000\ +\\001\000\005\000\172\001\000\000\ +\\001\000\005\000\189\001\000\000\ +\\001\000\005\000\190\001\000\000\ +\\001\000\005\000\191\001\000\000\ +\\001\000\005\000\199\001\000\000\ +\\001\000\005\000\200\001\000\000\ +\\001\000\005\000\201\001\000\000\ +\\001\000\005\000\002\002\000\000\ +\\001\000\005\000\013\002\000\000\ +\\001\000\005\000\017\002\000\000\ +\\001\000\006\000\210\000\000\000\ +\\001\000\006\000\210\000\020\000\203\000\000\000\ +\\001\000\006\000\167\001\000\000\ \\001\000\007\000\124\000\013\000\035\000\015\000\123\000\016\000\122\000\ \\025\000\121\000\028\000\120\000\044\000\101\000\045\000\100\000\ \\046\000\034\000\047\000\033\000\049\000\032\000\050\000\099\000\ @@ -1606,64 +1610,74 @@ \\068\000\030\000\069\000\029\000\070\000\028\000\071\000\027\000\ \\072\000\149\000\073\000\095\000\074\000\148\000\075\000\147\000\ \\076\000\094\000\077\000\093\000\000\000\ -\\001\000\007\000\124\000\013\000\035\000\016\000\238\000\025\000\121\000\ -\\026\000\243\000\028\000\120\000\044\000\101\000\045\000\100\000\ +\\001\000\007\000\124\000\013\000\035\000\016\000\239\000\025\000\121\000\ +\\026\000\244\000\028\000\120\000\044\000\101\000\045\000\100\000\ \\046\000\034\000\047\000\033\000\049\000\032\000\050\000\099\000\ \\051\000\031\000\053\000\098\000\064\000\097\000\065\000\096\000\ \\068\000\030\000\069\000\029\000\070\000\028\000\071\000\027\000\ \\073\000\095\000\076\000\094\000\077\000\093\000\000\000\ -\\001\000\007\000\124\000\013\000\035\000\016\000\238\000\025\000\121\000\ +\\001\000\007\000\124\000\013\000\035\000\016\000\239\000\025\000\121\000\ \\028\000\120\000\044\000\101\000\045\000\100\000\046\000\034\000\ \\047\000\033\000\049\000\032\000\050\000\099\000\051\000\031\000\ \\053\000\098\000\064\000\097\000\065\000\096\000\068\000\030\000\ \\069\000\029\000\070\000\028\000\071\000\027\000\073\000\095\000\ \\076\000\094\000\077\000\093\000\000\000\ -\\001\000\007\000\124\000\013\000\035\000\016\000\254\000\025\000\121\000\ -\\026\000\007\001\028\000\120\000\044\000\101\000\045\000\100\000\ +\\001\000\007\000\124\000\013\000\035\000\016\000\255\000\025\000\121\000\ +\\026\000\008\001\028\000\120\000\044\000\101\000\045\000\100\000\ \\046\000\034\000\047\000\033\000\049\000\032\000\050\000\099\000\ \\051\000\031\000\053\000\098\000\064\000\097\000\065\000\096\000\ \\068\000\030\000\069\000\029\000\070\000\028\000\071\000\027\000\ \\072\000\149\000\073\000\095\000\074\000\148\000\075\000\147\000\ \\076\000\094\000\077\000\093\000\000\000\ -\\001\000\007\000\124\000\013\000\035\000\016\000\254\000\025\000\121\000\ +\\001\000\007\000\124\000\013\000\035\000\016\000\255\000\025\000\121\000\ \\028\000\120\000\044\000\101\000\045\000\100\000\046\000\034\000\ \\047\000\033\000\049\000\032\000\050\000\099\000\051\000\031\000\ \\053\000\098\000\064\000\097\000\065\000\096\000\068\000\030\000\ \\069\000\029\000\070\000\028\000\071\000\027\000\072\000\149\000\ \\073\000\095\000\074\000\148\000\075\000\147\000\076\000\094\000\ \\077\000\093\000\000\000\ -\\001\000\007\000\124\000\025\000\121\000\000\000\ -\\001\000\009\000\140\002\027\000\151\002\060\000\151\002\000\000\ -\\001\000\009\000\019\001\059\000\018\001\060\000\017\001\000\000\ -\\001\000\009\000\166\001\000\000\ -\\001\000\013\000\035\000\015\000\050\001\026\000\153\001\039\000\049\001\ -\\040\000\048\001\041\000\047\001\042\000\046\001\043\000\045\001\ +\\001\000\007\000\063\001\013\000\035\000\044\000\101\000\045\000\100\000\ +\\046\000\034\000\047\000\033\000\049\000\032\000\050\000\099\000\ +\\051\000\031\000\053\000\098\000\064\000\097\000\065\000\096\000\ +\\068\000\030\000\069\000\029\000\070\000\028\000\071\000\027\000\ +\\073\000\095\000\076\000\094\000\077\000\093\000\000\000\ +\\001\000\007\000\067\001\013\000\035\000\044\000\101\000\045\000\100\000\ +\\046\000\034\000\047\000\033\000\049\000\032\000\050\000\099\000\ +\\051\000\031\000\053\000\098\000\064\000\097\000\065\000\096\000\ +\\068\000\030\000\069\000\029\000\070\000\028\000\071\000\027\000\ +\\073\000\095\000\076\000\094\000\077\000\093\000\000\000\ +\\001\000\009\000\171\002\027\000\182\002\060\000\182\002\000\000\ +\\001\000\009\000\020\001\059\000\019\001\060\000\018\001\000\000\ +\\001\000\009\000\178\001\000\000\ +\\001\000\011\000\170\001\000\000\ +\\001\000\013\000\035\000\015\000\052\001\026\000\161\001\039\000\051\001\ +\\040\000\050\001\041\000\049\001\042\000\048\001\043\000\047\001\ \\044\000\101\000\045\000\100\000\046\000\034\000\047\000\033\000\ -\\049\000\032\000\050\000\099\000\051\000\031\000\053\000\044\001\ +\\049\000\032\000\050\000\099\000\051\000\031\000\053\000\046\001\ \\068\000\030\000\069\000\029\000\070\000\028\000\071\000\027\000\000\000\ -\\001\000\013\000\035\000\015\000\050\001\039\000\049\001\040\000\048\001\ -\\041\000\047\001\042\000\046\001\043\000\045\001\044\000\101\000\ +\\001\000\013\000\035\000\015\000\052\001\039\000\051\001\040\000\050\001\ +\\041\000\049\001\042\000\048\001\043\000\047\001\044\000\101\000\ \\045\000\100\000\046\000\034\000\047\000\033\000\049\000\032\000\ -\\050\000\099\000\051\000\031\000\053\000\044\001\068\000\030\000\ +\\050\000\099\000\051\000\031\000\053\000\046\001\068\000\030\000\ \\069\000\029\000\070\000\028\000\071\000\027\000\000\000\ \\001\000\013\000\035\000\016\000\103\000\028\000\102\000\044\000\101\000\ \\045\000\100\000\046\000\034\000\047\000\033\000\049\000\032\000\ \\050\000\099\000\051\000\031\000\053\000\098\000\064\000\097\000\ \\065\000\096\000\068\000\030\000\069\000\029\000\070\000\028\000\ \\071\000\027\000\073\000\095\000\076\000\094\000\077\000\093\000\000\000\ -\\001\000\013\000\035\000\016\000\093\001\049\000\032\000\050\000\099\000\ -\\051\000\031\000\063\000\092\001\064\000\097\000\068\000\030\000\ +\\001\000\013\000\035\000\016\000\099\001\049\000\032\000\050\000\099\000\ +\\051\000\031\000\063\000\098\001\064\000\097\000\068\000\030\000\ \\069\000\029\000\070\000\028\000\071\000\027\000\000\000\ -\\001\000\013\000\035\000\016\000\173\001\049\000\032\000\050\000\099\000\ -\\051\000\031\000\063\000\092\001\064\000\097\000\068\000\030\000\ +\\001\000\013\000\035\000\016\000\185\001\049\000\032\000\050\000\099\000\ +\\051\000\031\000\063\000\098\001\064\000\097\000\068\000\030\000\ \\069\000\029\000\070\000\028\000\071\000\027\000\000\000\ -\\001\000\013\000\035\000\016\000\005\002\049\000\032\000\050\000\099\000\ +\\001\000\013\000\035\000\016\000\030\002\049\000\032\000\050\000\099\000\ \\051\000\031\000\064\000\097\000\068\000\030\000\069\000\029\000\ \\070\000\028\000\071\000\027\000\000\000\ -\\001\000\013\000\035\000\016\000\010\002\049\000\032\000\050\000\099\000\ +\\001\000\013\000\035\000\016\000\035\002\049\000\032\000\050\000\099\000\ \\051\000\031\000\064\000\097\000\068\000\030\000\069\000\029\000\ \\070\000\028\000\071\000\027\000\000\000\ -\\001\000\013\000\035\000\016\000\012\002\049\000\032\000\050\000\099\000\ +\\001\000\013\000\035\000\016\000\037\002\049\000\032\000\050\000\099\000\ \\051\000\031\000\064\000\097\000\068\000\030\000\069\000\029\000\ \\070\000\028\000\071\000\027\000\000\000\ \\001\000\013\000\035\000\028\000\102\000\044\000\101\000\045\000\100\000\ @@ -1687,119 +1701,101 @@ \\001\000\015\000\053\000\000\000\ \\001\000\015\000\123\000\000\000\ \\001\000\015\000\151\000\000\000\ -\\001\000\015\000\205\000\000\000\ -\\001\000\015\000\236\000\000\000\ -\\001\000\015\000\252\000\000\000\ -\\001\000\015\000\023\001\000\000\ -\\001\000\015\000\050\001\000\000\ +\\001\000\015\000\206\000\000\000\ +\\001\000\015\000\237\000\000\000\ +\\001\000\015\000\253\000\000\000\ +\\001\000\015\000\024\001\000\000\ +\\001\000\015\000\052\001\000\000\ \\001\000\015\000\168\001\000\000\ +\\001\000\015\000\171\001\000\000\ +\\001\000\015\000\180\001\000\000\ \\001\000\016\000\018\000\000\000\ \\001\000\016\000\019\000\000\000\ \\001\000\016\000\020\000\000\000\ \\001\000\016\000\021\000\000\000\ \\001\000\016\000\023\000\000\000\ -\\001\000\016\000\223\000\000\000\ \\001\000\016\000\224\000\000\000\ \\001\000\016\000\225\000\000\000\ -\\001\000\016\000\255\000\000\000\ +\\001\000\016\000\226\000\000\000\ \\001\000\016\000\000\001\000\000\ \\001\000\016\000\001\001\000\000\ -\\001\000\016\000\026\001\000\000\ +\\001\000\016\000\002\001\000\000\ \\001\000\016\000\027\001\000\000\ -\\001\000\016\000\146\001\000\000\ -\\001\000\016\000\147\001\000\000\ -\\001\000\016\000\148\001\000\000\ -\\001\000\016\000\149\001\000\000\ -\\001\000\016\000\150\001\000\000\ +\\001\000\016\000\028\001\000\000\ +\\001\000\016\000\029\001\000\000\ +\\001\000\016\000\154\001\000\000\ +\\001\000\016\000\155\001\000\000\ +\\001\000\016\000\156\001\000\000\ +\\001\000\016\000\157\001\000\000\ +\\001\000\016\000\158\001\000\000\ \\001\000\023\000\058\000\000\000\ -\\001\000\023\000\141\001\000\000\ -\\001\000\023\000\161\001\000\000\ -\\001\000\023\000\165\001\000\000\ -\\001\000\023\000\181\001\000\000\ -\\001\000\026\000\212\000\000\000\ -\\001\000\026\000\076\001\000\000\ -\\001\000\026\000\106\001\000\000\ -\\001\000\026\000\140\001\000\000\ -\\001\000\026\000\162\001\000\000\ +\\001\000\023\000\149\001\000\000\ +\\001\000\023\000\173\001\000\000\ +\\001\000\023\000\177\001\000\000\ +\\001\000\023\000\193\001\000\000\ +\\001\000\026\000\213\000\000\000\ +\\001\000\026\000\082\001\000\000\ +\\001\000\026\000\112\001\000\000\ +\\001\000\026\000\148\001\000\000\ \\001\000\026\000\174\001\000\000\ -\\001\000\026\000\183\001\000\000\ -\\001\000\026\000\200\001\000\000\ -\\001\000\026\000\242\001\000\000\ +\\001\000\026\000\186\001\000\000\ +\\001\000\026\000\195\001\000\000\ +\\001\000\026\000\213\001\000\000\ +\\001\000\026\000\255\001\000\000\ +\\001\000\026\000\001\002\000\000\ +\\001\000\026\000\006\002\000\000\ \\001\000\027\000\052\000\000\000\ -\\001\000\027\000\035\001\000\000\ -\\001\000\027\000\063\001\037\000\216\000\000\000\ -\\001\000\027\000\064\001\000\000\ -\\001\000\027\000\073\001\000\000\ -\\001\000\027\000\074\001\000\000\ -\\001\000\027\000\077\001\000\000\ -\\001\000\027\000\102\001\000\000\ -\\001\000\027\000\103\001\000\000\ -\\001\000\027\000\104\001\000\000\ -\\001\000\027\000\107\001\000\000\ -\\001\000\027\000\137\001\000\000\ -\\001\000\027\000\138\001\000\000\ -\\001\000\027\000\154\001\000\000\ -\\001\000\027\000\156\001\000\000\ -\\001\000\027\000\157\001\000\000\ -\\001\000\027\000\186\001\000\000\ -\\001\000\027\000\211\001\000\000\ -\\001\000\027\000\213\001\000\000\ -\\001\000\027\000\215\001\060\000\214\001\000\000\ -\\001\000\027\000\223\001\000\000\ -\\001\000\027\000\229\001\000\000\ +\\001\000\027\000\037\001\000\000\ +\\001\000\027\000\069\001\037\000\217\000\000\000\ +\\001\000\027\000\070\001\000\000\ +\\001\000\027\000\079\001\000\000\ +\\001\000\027\000\080\001\000\000\ +\\001\000\027\000\083\001\000\000\ +\\001\000\027\000\108\001\000\000\ +\\001\000\027\000\109\001\000\000\ +\\001\000\027\000\110\001\000\000\ +\\001\000\027\000\113\001\000\000\ +\\001\000\027\000\145\001\000\000\ +\\001\000\027\000\146\001\000\000\ +\\001\000\027\000\162\001\000\000\ +\\001\000\027\000\164\001\000\000\ +\\001\000\027\000\165\001\000\000\ +\\001\000\027\000\198\001\000\000\ +\\001\000\027\000\228\001\000\000\ \\001\000\027\000\230\001\000\000\ -\\001\000\027\000\231\001\000\000\ -\\001\000\027\000\232\001\000\000\ -\\001\000\027\000\233\001\000\000\ -\\001\000\027\000\234\001\000\000\ -\\001\000\027\000\236\001\000\000\ -\\001\000\027\000\237\001\000\000\ +\\001\000\027\000\232\001\060\000\231\001\000\000\ \\001\000\027\000\240\001\000\000\ -\\001\000\027\000\245\001\060\000\214\001\000\000\ \\001\000\027\000\247\001\000\000\ \\001\000\027\000\248\001\000\000\ +\\001\000\027\000\249\001\000\000\ +\\001\000\027\000\250\001\000\000\ \\001\000\027\000\251\001\000\000\ -\\001\000\027\000\002\002\000\000\ -\\001\000\027\000\006\002\000\000\ -\\001\000\027\000\007\002\000\000\ +\\001\000\027\000\252\001\000\000\ +\\001\000\027\000\254\001\000\000\ +\\001\000\027\000\000\002\000\000\ +\\001\000\027\000\004\002\000\000\ +\\001\000\027\000\009\002\060\000\231\001\000\000\ \\001\000\027\000\011\002\000\000\ +\\001\000\027\000\012\002\000\000\ +\\001\000\027\000\015\002\000\000\ +\\001\000\027\000\016\002\000\000\ +\\001\000\027\000\027\002\000\000\ +\\001\000\027\000\031\002\000\000\ +\\001\000\027\000\032\002\000\000\ +\\001\000\027\000\036\002\000\000\ \\001\000\038\000\000\000\000\000\ \\001\000\049\000\040\000\000\000\ \\001\000\050\000\099\000\000\000\ \\001\000\051\000\048\000\000\000\ -\\001\000\061\000\235\000\000\000\ -\\001\000\061\000\251\000\000\000\ -\\001\000\061\000\022\001\000\000\ -\\014\002\000\000\ -\\015\002\000\000\ -\\016\002\000\000\ -\\017\002\013\000\016\000\052\000\015\000\068\000\014\000\069\000\013\000\ -\\070\000\012\000\071\000\011\000\000\000\ -\\018\002\000\000\ -\\019\002\000\000\ -\\020\002\000\000\ -\\021\002\000\000\ -\\022\002\000\000\ -\\023\002\000\000\ -\\024\002\000\000\ -\\025\002\000\000\ -\\026\002\000\000\ -\\027\002\000\000\ -\\028\002\000\000\ -\\029\002\005\000\215\000\000\000\ -\\030\002\000\000\ -\\031\002\000\000\ -\\032\002\000\000\ -\\033\002\000\000\ -\\035\002\000\000\ -\\036\002\000\000\ -\\037\002\000\000\ -\\038\002\000\000\ +\\001\000\061\000\236\000\000\000\ +\\001\000\061\000\252\000\000\000\ +\\001\000\061\000\023\001\000\000\ \\039\002\000\000\ \\040\002\000\000\ -\\041\002\037\000\009\001\000\000\ -\\042\002\001\000\010\001\000\000\ -\\043\002\002\000\011\001\000\000\ +\\041\002\000\000\ +\\042\002\013\000\016\000\052\000\015\000\068\000\014\000\069\000\013\000\ +\\070\000\012\000\071\000\011\000\000\000\ +\\043\002\000\000\ \\044\002\000\000\ \\045\002\000\000\ \\046\002\000\000\ @@ -1810,141 +1806,140 @@ \\051\002\000\000\ \\052\002\000\000\ \\053\002\000\000\ -\\054\002\000\000\ +\\054\002\005\000\216\000\000\000\ \\055\002\000\000\ \\056\002\000\000\ -\\057\002\005\000\184\001\000\000\ +\\057\002\000\000\ \\058\002\000\000\ -\\059\002\000\000\ -\\060\002\004\000\185\001\000\000\ +\\060\002\000\000\ \\061\002\000\000\ \\062\002\000\000\ \\063\002\000\000\ \\064\002\000\000\ \\065\002\000\000\ -\\066\002\000\000\ -\\067\002\000\000\ -\\068\002\000\000\ +\\066\002\037\000\010\001\000\000\ +\\067\002\001\000\011\001\000\000\ +\\068\002\002\000\012\001\000\000\ +\\069\002\000\000\ +\\070\002\000\000\ \\071\002\000\000\ \\072\002\000\000\ \\073\002\000\000\ \\074\002\000\000\ -\\075\002\060\000\020\001\000\000\ -\\076\002\059\000\021\001\000\000\ -\\077\002\009\000\019\001\000\000\ +\\075\002\000\000\ +\\076\002\000\000\ +\\077\002\000\000\ \\078\002\000\000\ \\079\002\000\000\ \\080\002\000\000\ \\081\002\000\000\ -\\082\002\000\000\ +\\082\002\005\000\196\001\000\000\ \\083\002\000\000\ \\084\002\000\000\ -\\085\002\000\000\ +\\085\002\004\000\197\001\000\000\ \\086\002\000\000\ -\\087\002\005\000\139\001\000\000\ +\\087\002\000\000\ \\088\002\000\000\ \\089\002\000\000\ \\090\002\000\000\ \\091\002\000\000\ \\092\002\000\000\ -\\093\002\001\000\249\000\010\000\208\000\011\000\207\000\012\000\206\000\ -\\019\000\203\000\021\000\201\000\022\000\200\000\037\000\248\000\000\000\ +\\093\002\000\000\ \\094\002\000\000\ \\095\002\000\000\ -\\096\002\000\000\ -\\097\002\037\000\245\000\000\000\ -\\098\002\001\000\246\000\000\000\ +\\098\002\000\000\ \\099\002\000\000\ \\100\002\000\000\ \\101\002\000\000\ -\\102\002\000\000\ -\\103\002\000\000\ -\\104\002\000\000\ +\\102\002\060\000\021\001\000\000\ +\\103\002\059\000\022\001\000\000\ +\\104\002\009\000\020\001\000\000\ \\105\002\000\000\ \\106\002\000\000\ \\107\002\000\000\ \\108\002\000\000\ \\109\002\000\000\ -\\110\002\005\000\175\001\000\000\ +\\110\002\000\000\ \\111\002\000\000\ \\112\002\000\000\ -\\113\002\004\000\176\001\000\000\ -\\114\002\000\000\ +\\113\002\000\000\ +\\114\002\005\000\147\001\000\000\ \\115\002\000\000\ \\116\002\000\000\ \\117\002\000\000\ \\118\002\000\000\ \\119\002\000\000\ -\\120\002\000\000\ +\\120\002\001\000\250\000\010\000\209\000\011\000\208\000\012\000\207\000\ +\\019\000\204\000\021\000\202\000\022\000\201\000\037\000\249\000\000\000\ \\121\002\000\000\ \\122\002\000\000\ \\123\002\000\000\ -\\124\002\000\000\ -\\125\002\000\000\ +\\124\002\037\000\246\000\000\000\ +\\125\002\001\000\247\000\000\000\ \\126\002\000\000\ -\\127\002\005\000\105\001\000\000\ +\\127\002\000\000\ \\128\002\000\000\ \\129\002\000\000\ +\\130\002\000\000\ +\\131\002\000\000\ +\\132\002\000\000\ \\133\002\000\000\ \\134\002\000\000\ \\135\002\000\000\ \\136\002\000\000\ -\\137\002\000\000\ +\\137\002\005\000\187\001\000\000\ \\138\002\000\000\ \\139\002\000\000\ -\\139\002\060\000\212\001\000\000\ -\\140\002\000\000\ -\\141\002\016\000\167\001\000\000\ +\\140\002\004\000\188\001\000\000\ +\\141\002\000\000\ \\142\002\000\000\ \\143\002\000\000\ \\144\002\000\000\ -\\145\002\005\000\241\001\000\000\ +\\145\002\000\000\ \\146\002\000\000\ \\147\002\000\000\ \\148\002\000\000\ \\149\002\000\000\ \\150\002\000\000\ +\\151\002\000\000\ \\152\002\000\000\ \\153\002\000\000\ \\154\002\000\000\ -\\155\002\001\000\234\000\010\000\208\000\011\000\207\000\012\000\206\000\ -\\019\000\203\000\021\000\201\000\022\000\200\000\037\000\233\000\000\000\ +\\155\002\000\000\ \\156\002\000\000\ \\157\002\000\000\ -\\158\002\000\000\ -\\159\002\037\000\230\000\000\000\ -\\160\002\001\000\231\000\000\000\ -\\161\002\000\000\ -\\162\002\000\000\ -\\163\002\000\000\ +\\158\002\005\000\111\001\000\000\ +\\159\002\000\000\ +\\160\002\000\000\ \\164\002\000\000\ \\165\002\000\000\ \\166\002\000\000\ \\167\002\000\000\ \\168\002\000\000\ \\169\002\000\000\ -\\170\002\005\000\163\001\000\000\ +\\170\002\000\000\ +\\170\002\060\000\229\001\000\000\ \\171\002\000\000\ -\\172\002\000\000\ +\\172\002\016\000\179\001\000\000\ \\173\002\000\000\ \\174\002\000\000\ \\175\002\000\000\ -\\176\002\000\000\ +\\176\002\005\000\005\002\000\000\ \\177\002\000\000\ -\\178\002\005\000\075\001\000\000\ +\\178\002\000\000\ \\179\002\000\000\ \\180\002\000\000\ -\\181\002\037\000\216\000\000\000\ -\\182\002\000\000\ +\\181\002\000\000\ \\183\002\000\000\ \\184\002\000\000\ \\185\002\000\000\ -\\186\002\000\000\ +\\186\002\001\000\235\000\010\000\209\000\011\000\208\000\012\000\207\000\ +\\019\000\204\000\021\000\202\000\022\000\201\000\037\000\234\000\000\000\ \\187\002\000\000\ \\188\002\000\000\ -\\189\002\016\000\024\001\000\000\ -\\190\002\000\000\ -\\191\002\000\000\ +\\189\002\000\000\ +\\190\002\037\000\231\000\000\000\ +\\191\002\001\000\232\000\000\000\ \\192\002\000\000\ \\193\002\000\000\ \\194\002\000\000\ @@ -1954,7 +1949,7 @@ \\198\002\000\000\ \\199\002\000\000\ \\200\002\000\000\ -\\201\002\000\000\ +\\201\002\005\000\175\001\000\000\ \\202\002\000\000\ \\203\002\000\000\ \\204\002\000\000\ @@ -1962,21 +1957,27 @@ \\206\002\000\000\ \\207\002\000\000\ \\208\002\000\000\ -\\209\002\000\000\ +\\209\002\005\000\081\001\000\000\ \\210\002\000\000\ \\211\002\000\000\ -\\212\002\000\000\ +\\212\002\037\000\217\000\000\000\ \\213\002\000\000\ \\214\002\000\000\ +\\215\002\000\000\ \\216\002\000\000\ \\217\002\000\000\ \\218\002\000\000\ -\\220\002\000\000\ +\\219\002\000\000\ +\\220\002\016\000\025\001\000\000\ \\221\002\000\000\ +\\222\002\000\000\ +\\223\002\000\000\ +\\224\002\000\000\ \\225\002\000\000\ \\226\002\000\000\ \\227\002\000\000\ \\228\002\000\000\ +\\229\002\000\000\ \\230\002\000\000\ \\231\002\000\000\ \\232\002\000\000\ @@ -1985,42 +1986,36 @@ \\235\002\000\000\ \\236\002\000\000\ \\237\002\000\000\ -\\237\002\066\000\025\001\000\000\ \\238\002\000\000\ \\239\002\000\000\ -\\239\002\016\000\222\000\000\000\ \\240\002\000\000\ \\241\002\000\000\ \\242\002\000\000\ \\243\002\000\000\ \\244\002\000\000\ \\245\002\000\000\ -\\246\002\000\000\ \\247\002\000\000\ -\\248\002\016\000\218\000\000\000\ +\\248\002\000\000\ \\249\002\000\000\ -\\250\002\000\000\ \\251\002\000\000\ -\\252\002\016\000\217\000\000\000\ -\\253\002\000\000\ -\\254\002\000\000\ -\\255\002\005\000\155\001\000\000\ +\\252\002\000\000\ \\000\003\000\000\ \\001\003\000\000\ \\002\003\000\000\ \\003\003\000\000\ -\\004\003\000\000\ -\\005\003\005\000\145\001\000\000\ +\\005\003\000\000\ \\006\003\000\000\ \\007\003\000\000\ \\008\003\000\000\ -\\009\003\005\000\046\000\000\000\ +\\009\003\000\000\ \\010\003\000\000\ -\\011\003\005\000\213\000\000\000\ -\\012\003\004\000\142\001\000\000\ +\\011\003\000\000\ +\\012\003\000\000\ +\\012\003\066\000\026\001\000\000\ \\013\003\000\000\ \\014\003\000\000\ -\\015\003\016\000\143\001\000\000\ +\\014\003\016\000\223\000\000\000\ +\\015\003\000\000\ \\016\003\000\000\ \\017\003\000\000\ \\018\003\000\000\ @@ -2028,169 +2023,207 @@ \\020\003\000\000\ \\021\003\000\000\ \\022\003\000\000\ -\\023\003\000\000\ +\\023\003\016\000\219\000\000\000\ \\024\003\000\000\ \\025\003\000\000\ \\026\003\000\000\ -\\027\003\000\000\ +\\027\003\016\000\218\000\000\000\ \\028\003\000\000\ \\029\003\000\000\ -\\030\003\005\000\199\001\000\000\ +\\030\003\005\000\163\001\000\000\ \\031\003\000\000\ \\032\003\000\000\ \\033\003\000\000\ \\034\003\000\000\ \\035\003\000\000\ -\\036\003\000\000\ +\\036\003\005\000\153\001\000\000\ \\037\003\000\000\ \\038\003\000\000\ \\039\003\000\000\ -\\040\003\000\000\ +\\040\003\005\000\046\000\000\000\ \\041\003\000\000\ -\\042\003\000\000\ -\\043\003\000\000\ +\\042\003\005\000\214\000\000\000\ +\\043\003\004\000\150\001\000\000\ \\044\003\000\000\ \\045\003\000\000\ -\\046\003\000\000\ +\\046\003\016\000\151\001\000\000\ \\047\003\000\000\ +\\048\003\000\000\ +\\049\003\000\000\ +\\050\003\000\000\ +\\051\003\000\000\ +\\052\003\000\000\ +\\053\003\000\000\ +\\054\003\000\000\ +\\055\003\000\000\ +\\056\003\000\000\ +\\057\003\000\000\ +\\058\003\000\000\ +\\059\003\000\000\ +\\060\003\000\000\ +\\061\003\005\000\212\001\000\000\ +\\062\003\000\000\ +\\063\003\000\000\ +\\064\003\000\000\ +\\065\003\000\000\ +\\066\003\000\000\ +\\067\003\000\000\ +\\068\003\000\000\ +\\069\003\000\000\ +\\070\003\000\000\ +\\071\003\000\000\ +\\072\003\000\000\ +\\073\003\000\000\ +\\074\003\000\000\ +\\075\003\000\000\ +\\076\003\000\000\ +\\077\003\000\000\ +\\078\003\000\000\ \" val actionRowNumbers = -"\153\000\150\000\153\000\155\000\ -\\154\000\156\000\157\000\158\000\ -\\159\000\073\000\074\000\075\000\ -\\076\000\153\000\077\000\151\000\ -\\061\000\061\000\061\000\061\000\ -\\152\000\144\000\158\001\157\001\ -\\020\000\164\001\163\001\162\001\ -\\161\001\159\001\160\001\168\001\ -\\169\001\165\001\021\000\022\000\ -\\023\000\135\001\173\001\146\000\ -\\146\000\146\000\146\000\105\000\ -\\064\000\024\000\166\000\025\000\ -\\026\000\027\000\091\000\061\000\ -\\053\000\041\000\042\000\007\000\ -\\133\001\096\000\137\001\123\001\ -\\119\001\101\001\165\000\055\001\ -\\056\001\060\001\058\001\089\001\ -\\090\001\092\001\093\001\091\001\ -\\100\001\098\001\002\000\105\001\ -\\103\001\111\001\112\001\003\000\ -\\116\001\004\000\120\001\122\001\ -\\118\001\040\000\109\001\170\001\ -\\113\001\099\001\110\001\078\000\ -\\079\000\080\000\167\001\166\001\ -\\114\001\124\001\172\001\171\001\ -\\060\000\059\000\165\000\026\001\ -\\028\001\030\001\031\001\033\001\ -\\034\001\029\001\039\001\040\001\ -\\027\001\147\000\047\001\068\000\ -\\044\000\041\001\087\001\078\001\ -\\041\000\043\000\077\001\240\000\ -\\165\000\222\000\225\000\227\000\ -\\228\000\230\000\231\000\226\000\ -\\236\000\237\000\223\000\013\000\ -\\239\000\224\000\148\000\249\000\ -\\069\000\046\000\238\000\006\000\ -\\005\000\081\000\082\000\083\000\ -\\042\000\045\000\165\000\167\000\ -\\169\000\172\000\173\000\176\000\ -\\177\000\178\000\011\000\185\000\ -\\186\000\170\000\014\000\171\000\ -\\049\000\174\000\207\000\208\000\ -\\209\000\000\000\189\000\188\000\ -\\168\000\149\000\199\000\070\000\ -\\061\001\063\001\065\001\073\001\ -\\062\001\074\001\072\001\071\001\ -\\102\001\106\001\115\001\104\001\ -\\198\000\084\000\085\000\067\001\ -\\068\001\076\001\075\001\070\001\ -\\069\001\085\001\083\001\082\001\ -\\097\001\084\001\007\000\008\000\ -\\080\001\079\001\081\001\096\001\ -\\066\001\086\001\134\001\061\000\ -\\106\000\052\000\059\000\060\000\ -\\060\000\060\000\060\000\095\001\ -\\060\000\047\000\047\000\046\000\ -\\059\001\039\000\107\000\108\000\ -\\044\000\044\000\044\000\044\000\ -\\044\000\065\000\145\000\046\001\ -\\044\000\109\000\110\000\052\001\ -\\097\000\050\001\111\000\046\000\ -\\046\000\046\000\046\000\046\000\ -\\054\000\066\000\145\000\248\000\ -\\046\000\047\000\047\000\046\000\ -\\112\000\113\000\114\000\004\001\ -\\098\000\001\001\115\000\010\000\ +"\165\000\162\000\165\000\167\000\ +\\166\000\168\000\169\000\170\000\ +\\171\000\081\000\082\000\083\000\ +\\084\000\165\000\085\000\163\000\ +\\067\000\067\000\067\000\067\000\ +\\164\000\156\000\176\001\175\001\ +\\022\000\182\001\181\001\180\001\ +\\179\001\177\001\178\001\186\001\ +\\187\001\183\001\023\000\024\000\ +\\025\000\153\001\191\001\158\000\ +\\158\000\158\000\158\000\116\000\ +\\070\000\026\000\178\000\027\000\ +\\028\000\029\000\100\000\067\000\ +\\059\000\045\000\046\000\007\000\ +\\151\001\105\000\155\001\141\001\ +\\137\001\119\001\177\000\073\001\ +\\074\001\078\001\076\001\107\001\ +\\108\001\110\001\111\001\109\001\ +\\118\001\116\001\002\000\123\001\ +\\121\001\129\001\130\001\003\000\ +\\134\001\004\000\138\001\140\001\ +\\136\001\043\000\127\001\188\001\ +\\131\001\117\001\128\001\086\000\ +\\087\000\088\000\185\001\184\001\ +\\132\001\142\001\190\001\189\001\ +\\066\000\065\000\177\000\044\001\ +\\046\001\048\001\049\001\051\001\ +\\052\001\047\001\057\001\058\001\ +\\045\001\159\000\065\001\074\000\ +\\048\000\059\001\105\001\096\001\ +\\045\000\047\000\095\001\254\000\ +\\177\000\236\000\239\000\241\000\ +\\242\000\244\000\245\000\240\000\ +\\250\000\251\000\237\000\013\000\ +\\253\000\238\000\160\000\007\001\ +\\075\000\050\000\252\000\006\000\ +\\005\000\089\000\090\000\091\000\ +\\046\000\049\000\177\000\179\000\ +\\181\000\184\000\185\000\188\000\ +\\189\000\190\000\011\000\197\000\ +\\198\000\182\000\014\000\183\000\ +\\054\000\186\000\221\000\222\000\ +\\223\000\000\000\201\000\200\000\ +\\180\000\161\000\211\000\076\000\ +\\079\001\081\001\083\001\091\001\ +\\080\001\092\001\090\001\089\001\ +\\120\001\124\001\133\001\122\001\ +\\210\000\092\000\093\000\094\000\ +\\085\001\086\001\094\001\093\001\ +\\088\001\087\001\103\001\101\001\ +\\100\001\115\001\102\001\007\000\ +\\008\000\098\001\097\001\099\001\ +\\114\001\084\001\104\001\152\001\ +\\067\000\117\000\058\000\065\000\ +\\066\000\066\000\066\000\066\000\ +\\113\001\066\000\051\000\052\000\ +\\050\000\077\001\042\000\118\000\ +\\119\000\048\000\048\000\048\000\ +\\048\000\048\000\071\000\157\000\ +\\064\001\048\000\120\000\121\000\ +\\070\001\106\000\068\001\122\000\ +\\050\000\050\000\050\000\050\000\ +\\050\000\060\000\072\000\157\000\ +\\006\001\050\000\052\000\051\000\ +\\050\000\123\000\124\000\125\000\ +\\022\001\107\000\019\001\126\000\ +\\010\000\010\000\010\000\010\000\ +\\010\000\010\000\010\000\009\000\ \\010\000\010\000\010\000\010\000\ -\\010\000\010\000\009\000\010\000\ -\\010\000\010\000\010\000\010\000\ -\\067\000\145\000\009\000\063\000\ -\\012\000\009\000\116\000\117\000\ -\\220\000\099\000\218\000\009\000\ -\\136\001\092\000\142\001\146\001\ -\\144\001\143\001\138\001\141\001\ -\\131\001\140\001\145\001\086\000\ -\\087\000\088\000\089\000\090\000\ -\\051\000\057\001\118\000\125\001\ -\\119\000\094\001\064\001\120\000\ -\\028\000\253\000\029\000\254\000\ -\\030\000\054\001\093\000\036\001\ -\\038\001\032\001\035\001\037\001\ -\\048\001\100\000\044\001\042\001\ -\\049\001\044\000\051\001\094\000\ -\\233\000\235\000\229\000\232\000\ -\\234\000\088\001\008\001\005\001\ -\\050\000\019\000\007\001\017\001\ -\\019\001\016\001\072\000\055\000\ -\\255\000\101\000\243\000\245\000\ -\\246\000\031\000\032\000\033\000\ -\\241\000\006\001\000\001\046\000\ -\\002\001\095\000\180\000\187\000\ -\\009\000\182\000\184\000\175\000\ -\\179\000\183\000\181\000\205\000\ -\\203\000\206\000\212\000\214\000\ -\\210\000\211\000\213\000\215\000\ -\\216\000\102\000\192\000\194\000\ -\\195\000\121\000\204\000\108\001\ -\\034\000\202\000\035\000\001\000\ -\\217\000\009\000\219\000\163\000\ -\\052\000\052\000\164\000\071\000\ -\\042\000\060\000\053\000\041\000\ -\\007\000\156\001\103\000\154\001\ -\\121\001\060\000\117\001\107\001\ -\\060\000\060\000\060\000\162\000\ -\\015\000\145\000\053\001\161\000\ -\\062\000\062\000\145\000\122\000\ -\\014\001\123\000\124\000\055\000\ -\\016\000\145\000\062\000\042\000\ -\\042\000\046\000\003\001\160\000\ -\\125\000\017\000\145\000\009\000\ -\\197\000\007\000\009\000\221\000\ -\\139\001\126\000\130\001\132\001\ -\\127\000\128\000\129\000\130\000\ -\\131\000\052\000\153\001\126\001\ -\\132\000\133\000\036\000\044\000\ -\\045\001\022\001\134\000\020\001\ -\\104\000\010\001\062\000\023\001\ -\\062\000\015\001\135\000\046\000\ -\\244\000\247\000\136\000\137\000\ -\\037\000\190\000\010\000\193\000\ -\\196\000\138\000\038\000\147\001\ -\\149\001\152\001\151\001\150\001\ -\\148\001\155\001\129\001\128\001\ -\\060\000\043\001\018\001\062\000\ -\\018\000\024\001\025\001\048\000\ -\\242\000\252\000\251\000\046\000\ -\\191\000\201\000\009\000\139\000\ -\\021\001\056\000\140\000\141\000\ -\\127\001\009\001\011\001\057\000\ -\\250\000\200\000\013\001\142\000\ -\\058\000\012\001\058\000\143\000" +\\010\000\073\000\157\000\009\000\ +\\069\000\012\000\012\000\009\000\ +\\127\000\128\000\234\000\108\000\ +\\232\000\009\000\154\001\101\000\ +\\160\001\164\001\162\001\161\001\ +\\156\001\159\001\149\001\158\001\ +\\163\001\095\000\096\000\097\000\ +\\098\000\099\000\057\000\075\001\ +\\129\000\143\001\130\000\112\001\ +\\082\001\131\000\012\001\030\000\ +\\044\000\078\000\015\001\031\000\ +\\056\000\079\000\032\000\072\001\ +\\102\000\054\001\056\001\050\001\ +\\053\001\055\001\066\001\109\000\ +\\062\001\060\001\067\001\048\000\ +\\069\001\103\000\247\000\249\000\ +\\243\000\246\000\248\000\106\001\ +\\026\001\023\001\055\000\021\000\ +\\025\001\035\001\037\001\034\001\ +\\080\000\061\000\017\001\110\000\ +\\001\001\003\001\004\001\033\000\ +\\034\000\035\000\255\000\024\001\ +\\018\001\050\000\020\001\104\000\ +\\192\000\199\000\009\000\194\000\ +\\196\000\187\000\191\000\195\000\ +\\193\000\219\000\217\000\220\000\ +\\226\000\228\000\224\000\225\000\ +\\227\000\229\000\230\000\111\000\ +\\204\000\206\000\207\000\132\000\ +\\218\000\126\001\036\000\216\000\ +\\037\000\215\000\038\000\001\000\ +\\231\000\009\000\233\000\175\000\ +\\058\000\058\000\176\000\077\000\ +\\046\000\066\000\059\000\045\000\ +\\007\000\174\001\112\000\172\001\ +\\139\001\066\000\135\001\125\001\ +\\066\000\066\000\157\000\066\000\ +\\050\000\157\000\066\000\174\000\ +\\015\000\157\000\071\001\173\000\ +\\068\000\068\000\157\000\133\000\ +\\032\001\134\000\135\000\061\000\ +\\016\000\157\000\068\000\046\000\ +\\046\000\050\000\021\001\172\000\ +\\136\000\017\000\157\000\009\000\ +\\209\000\007\000\007\000\009\000\ +\\235\000\157\001\137\000\148\001\ +\\150\001\138\000\139\000\140\000\ +\\141\000\142\000\058\000\171\001\ +\\144\001\143\000\013\001\113\000\ +\\144\000\016\001\114\000\039\000\ +\\048\000\063\001\040\001\145\000\ +\\038\001\115\000\028\001\068\000\ +\\041\001\068\000\033\001\146\000\ +\\050\000\002\001\005\001\147\000\ +\\148\000\040\000\202\000\010\000\ +\\205\000\208\000\149\000\150\000\ +\\041\000\165\001\167\001\170\001\ +\\169\001\168\001\166\001\173\001\ +\\147\001\018\000\146\001\019\000\ +\\066\000\061\001\036\001\068\000\ +\\020\000\042\001\043\001\053\000\ +\\000\001\010\001\009\001\050\000\ +\\203\000\214\000\213\000\009\000\ +\\066\000\066\000\151\000\039\001\ +\\062\000\152\000\153\000\011\001\ +\\014\001\145\001\027\001\029\001\ +\\063\000\008\001\212\000\031\001\ +\\154\000\064\000\030\001\064\000\ +\\155\000" val gotoT = "\ \\128\000\008\000\129\000\007\000\130\000\006\000\131\000\005\000\ \\132\000\004\000\133\000\003\000\134\000\002\000\135\000\001\000\ -\\136\000\011\002\000\000\ +\\136\000\036\002\000\000\ \\000\000\ \\128\000\008\000\129\000\007\000\130\000\006\000\131\000\005\000\ \\132\000\004\000\133\000\003\000\134\000\002\000\135\000\015\000\000\000\ @@ -2251,7 +2284,7 @@ \\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ \\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ \\045\000\066\000\055\000\065\000\057\000\064\000\058\000\063\000\ -\\059\000\062\000\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\059\000\062\000\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\085\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ @@ -2262,7 +2295,7 @@ \\061\000\113\000\062\000\112\000\063\000\111\000\065\000\110\000\ \\066\000\109\000\067\000\108\000\068\000\107\000\069\000\106\000\ \\070\000\105\000\071\000\104\000\072\000\103\000\073\000\102\000\ -\\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\144\000\020\000\085\000\022\000\084\000\023\000\143\000\ \\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ @@ -2273,8 +2306,8 @@ \\074\000\138\000\076\000\137\000\077\000\136\000\083\000\135\000\ \\084\000\134\000\085\000\133\000\089\000\132\000\090\000\131\000\ \\091\000\130\000\092\000\129\000\093\000\128\000\094\000\127\000\ -\\095\000\126\000\096\000\125\000\097\000\124\000\138\000\123\000\ -\\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\095\000\126\000\096\000\125\000\097\000\124\000\139\000\123\000\ +\\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\188\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ @@ -2288,37 +2321,37 @@ \\111\000\162\000\112\000\161\000\113\000\160\000\117\000\159\000\ \\118\000\158\000\119\000\157\000\120\000\156\000\121\000\155\000\ \\122\000\154\000\123\000\153\000\124\000\152\000\125\000\151\000\ -\\126\000\150\000\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\001\000\212\000\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\036\000\219\000\037\000\218\000\038\000\217\000\000\000\ +\\126\000\150\000\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\001\000\213\000\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\036\000\220\000\037\000\219\000\038\000\218\000\000\000\ \\000\000\ \\000\000\ \\000\000\ @@ -2334,28 +2367,28 @@ \\000\000\ \\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ -\\019\000\086\000\020\000\225\000\022\000\084\000\023\000\083\000\ +\\019\000\086\000\020\000\226\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ \\028\000\078\000\029\000\077\000\030\000\076\000\031\000\075\000\ \\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ \\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ -\\045\000\224\000\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\045\000\225\000\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\085\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ \\028\000\078\000\029\000\077\000\030\000\076\000\031\000\075\000\ \\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ \\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ -\\045\000\066\000\055\000\065\000\057\000\064\000\058\000\226\000\ -\\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ -\\001\000\227\000\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\050\000\230\000\000\000\ +\\045\000\066\000\055\000\065\000\057\000\064\000\058\000\227\000\ +\\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ +\\001\000\228\000\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\050\000\231\000\000\000\ \\000\000\ \\000\000\ \\000\000\ @@ -2369,8 +2402,8 @@ \\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ \\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ \\045\000\117\000\046\000\116\000\051\000\115\000\055\000\114\000\ -\\063\000\111\000\065\000\110\000\066\000\235\000\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ +\\063\000\111\000\065\000\110\000\066\000\236\000\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ \\000\000\ \\000\000\ \\000\000\ @@ -2381,10 +2414,10 @@ \\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ \\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ \\045\000\117\000\046\000\116\000\051\000\115\000\055\000\114\000\ -\\061\000\113\000\062\000\238\000\063\000\111\000\065\000\110\000\ +\\061\000\113\000\062\000\239\000\063\000\111\000\065\000\110\000\ \\066\000\109\000\067\000\108\000\068\000\107\000\069\000\106\000\ -\\070\000\105\000\071\000\104\000\072\000\237\000\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ +\\070\000\105\000\071\000\104\000\072\000\238\000\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\085\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ @@ -2392,20 +2425,20 @@ \\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ \\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ \\045\000\117\000\046\000\116\000\051\000\115\000\055\000\114\000\ -\\060\000\240\000\063\000\111\000\065\000\110\000\066\000\109\000\ +\\060\000\241\000\063\000\111\000\065\000\110\000\066\000\109\000\ \\067\000\108\000\068\000\107\000\069\000\106\000\070\000\105\000\ -\\071\000\104\000\072\000\239\000\144\000\061\000\145\000\060\000\ -\\146\000\059\000\000\000\ -\\000\000\ -\\000\000\ -\\001\000\242\000\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\050\000\245\000\000\000\ +\\071\000\104\000\072\000\240\000\147\000\061\000\148\000\060\000\ +\\149\000\059\000\000\000\ +\\000\000\ +\\000\000\ +\\001\000\243\000\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\050\000\246\000\000\000\ \\000\000\ \\000\000\ \\000\000\ @@ -2422,8 +2455,8 @@ \\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ \\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ \\045\000\142\000\046\000\141\000\051\000\140\000\055\000\139\000\ -\\077\000\136\000\085\000\133\000\089\000\132\000\090\000\251\000\ -\\138\000\123\000\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\077\000\136\000\085\000\133\000\089\000\132\000\090\000\252\000\ +\\139\000\123\000\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\000\000\ \\000\000\ \\000\000\ @@ -2437,11 +2470,11 @@ \\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ \\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ \\045\000\142\000\046\000\141\000\051\000\140\000\055\000\139\000\ -\\074\000\138\000\076\000\002\001\077\000\136\000\083\000\135\000\ -\\084\000\001\001\085\000\133\000\089\000\132\000\090\000\131\000\ +\\074\000\138\000\076\000\003\001\077\000\136\000\083\000\135\000\ +\\084\000\002\001\085\000\133\000\089\000\132\000\090\000\131\000\ \\091\000\130\000\092\000\129\000\093\000\128\000\094\000\127\000\ -\\095\000\126\000\096\000\000\001\138\000\123\000\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ +\\095\000\126\000\096\000\001\001\139\000\123\000\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\085\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ @@ -2449,19 +2482,20 @@ \\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ \\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ \\045\000\142\000\046\000\141\000\051\000\140\000\055\000\139\000\ -\\075\000\004\001\077\000\136\000\085\000\133\000\089\000\132\000\ +\\075\000\005\001\077\000\136\000\085\000\133\000\089\000\132\000\ \\090\000\131\000\091\000\130\000\092\000\129\000\093\000\128\000\ -\\094\000\127\000\095\000\126\000\096\000\003\001\138\000\123\000\ -\\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ -\\001\000\006\001\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\036\000\183\000\037\000\182\000\050\000\179\000\053\000\010\001\000\000\ +\\094\000\127\000\095\000\126\000\096\000\004\001\139\000\123\000\ +\\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ +\\001\000\007\001\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\036\000\183\000\037\000\182\000\050\000\179\000\053\000\011\001\000\000\ +\\000\000\ \\000\000\ \\000\000\ \\000\000\ @@ -2512,13 +2546,13 @@ \\032\000\184\000\033\000\073\000\034\000\072\000\036\000\183\000\ \\037\000\182\000\046\000\181\000\049\000\180\000\050\000\179\000\ \\051\000\178\000\052\000\177\000\053\000\176\000\054\000\175\000\ -\\056\000\174\000\098\000\173\000\100\000\027\001\101\000\171\000\ +\\056\000\174\000\098\000\173\000\100\000\029\001\101\000\171\000\ \\102\000\170\000\103\000\169\000\104\000\168\000\105\000\167\000\ \\106\000\166\000\107\000\165\000\108\000\164\000\110\000\163\000\ \\111\000\162\000\112\000\161\000\113\000\160\000\117\000\159\000\ \\118\000\158\000\119\000\157\000\120\000\156\000\121\000\155\000\ -\\122\000\154\000\123\000\153\000\124\000\152\000\125\000\026\001\ -\\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\122\000\154\000\123\000\153\000\124\000\152\000\125\000\028\001\ +\\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\188\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ @@ -2526,66 +2560,78 @@ \\032\000\184\000\033\000\073\000\034\000\072\000\036\000\183\000\ \\037\000\182\000\046\000\181\000\049\000\180\000\050\000\179\000\ \\051\000\178\000\052\000\177\000\053\000\176\000\054\000\175\000\ -\\056\000\174\000\099\000\029\001\101\000\171\000\102\000\170\000\ +\\056\000\174\000\099\000\031\001\101\000\171\000\102\000\170\000\ \\103\000\169\000\104\000\168\000\105\000\167\000\106\000\166\000\ \\107\000\165\000\108\000\164\000\110\000\163\000\111\000\162\000\ \\112\000\161\000\113\000\160\000\117\000\159\000\118\000\158\000\ \\119\000\157\000\120\000\156\000\121\000\155\000\122\000\154\000\ -\\123\000\153\000\124\000\152\000\125\000\028\001\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\002\000\058\000\003\000\032\001\009\000\023\000\014\000\022\000\000\000\ -\\000\000\ -\\006\000\041\001\008\000\040\001\009\000\039\001\010\000\038\001\ -\\011\000\037\001\012\000\036\001\013\000\035\001\014\000\087\000\ -\\016\000\034\001\000\000\ +\\123\000\153\000\124\000\152\000\125\000\030\001\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\002\000\058\000\003\000\034\001\009\000\023\000\014\000\022\000\000\000\ +\\000\000\ +\\006\000\043\001\008\000\042\001\009\000\041\001\010\000\040\001\ +\\011\000\039\001\012\000\038\001\013\000\037\001\014\000\087\000\ +\\016\000\036\001\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\085\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ \\028\000\078\000\029\000\077\000\030\000\076\000\031\000\075\000\ \\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ \\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ -\\045\000\066\000\055\000\065\000\057\000\049\001\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ +\\045\000\066\000\055\000\065\000\057\000\051\001\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ -\\019\000\086\000\020\000\051\001\021\000\050\001\022\000\084\000\ +\\019\000\086\000\020\000\053\001\021\000\052\001\022\000\084\000\ \\023\000\083\000\024\000\082\000\025\000\187\000\026\000\080\000\ \\027\000\186\000\028\000\078\000\029\000\077\000\030\000\076\000\ \\031\000\075\000\032\000\184\000\033\000\073\000\034\000\072\000\ -\\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ -\\019\000\086\000\020\000\051\001\021\000\052\001\022\000\084\000\ +\\019\000\086\000\020\000\053\001\021\000\054\001\022\000\084\000\ \\023\000\083\000\024\000\082\000\025\000\187\000\026\000\080\000\ \\027\000\186\000\028\000\078\000\029\000\077\000\030\000\076\000\ \\031\000\075\000\032\000\184\000\033\000\073\000\034\000\072\000\ -\\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ -\\019\000\086\000\020\000\053\001\022\000\084\000\023\000\083\000\ +\\019\000\086\000\020\000\055\001\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ \\028\000\078\000\029\000\077\000\030\000\076\000\031\000\075\000\ -\\032\000\184\000\033\000\073\000\034\000\072\000\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ +\\032\000\184\000\033\000\073\000\034\000\072\000\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ -\\019\000\086\000\020\000\054\001\022\000\084\000\023\000\083\000\ +\\019\000\086\000\020\000\056\001\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ \\028\000\078\000\029\000\077\000\030\000\076\000\031\000\075\000\ -\\032\000\184\000\033\000\073\000\034\000\072\000\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ +\\032\000\184\000\033\000\073\000\034\000\072\000\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ \\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ -\\019\000\086\000\020\000\051\001\021\000\055\001\022\000\084\000\ +\\019\000\086\000\020\000\053\001\021\000\057\001\022\000\084\000\ \\023\000\083\000\024\000\082\000\025\000\187\000\026\000\080\000\ \\027\000\186\000\028\000\078\000\029\000\077\000\030\000\076\000\ \\031\000\075\000\032\000\184\000\033\000\073\000\034\000\072\000\ -\\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ -\\051\000\140\000\089\000\057\001\139\000\056\001\000\000\ -\\051\000\140\000\089\000\059\001\140\000\058\001\000\000\ +\\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ +\\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ +\\019\000\086\000\020\000\060\001\022\000\084\000\023\000\083\000\ +\\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ +\\028\000\078\000\029\000\077\000\030\000\076\000\031\000\075\000\ +\\032\000\184\000\033\000\073\000\034\000\072\000\140\000\059\001\ +\\141\000\058\001\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ +\\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ +\\019\000\086\000\020\000\226\000\022\000\084\000\023\000\083\000\ +\\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ +\\028\000\078\000\029\000\077\000\030\000\076\000\031\000\075\000\ +\\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ +\\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ +\\045\000\064\001\142\000\063\001\143\000\062\001\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\085\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ @@ -2595,10 +2641,10 @@ \\045\000\142\000\046\000\141\000\051\000\140\000\055\000\139\000\ \\077\000\136\000\085\000\133\000\089\000\132\000\090\000\131\000\ \\091\000\130\000\092\000\129\000\093\000\128\000\094\000\127\000\ -\\095\000\126\000\096\000\060\001\138\000\123\000\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ -\\000\000\ -\\036\000\219\000\038\000\217\000\000\000\ +\\095\000\126\000\096\000\066\001\139\000\123\000\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ +\\000\000\ +\\036\000\220\000\038\000\218\000\000\000\ \\000\000\ \\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ @@ -2608,8 +2654,8 @@ \\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ \\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ \\045\000\117\000\046\000\116\000\051\000\115\000\055\000\114\000\ -\\063\000\111\000\065\000\110\000\066\000\063\001\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ +\\063\000\111\000\065\000\110\000\066\000\069\001\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\085\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ @@ -2617,8 +2663,8 @@ \\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ \\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ \\045\000\117\000\046\000\116\000\051\000\115\000\055\000\114\000\ -\\063\000\111\000\065\000\110\000\066\000\064\001\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ +\\063\000\111\000\065\000\110\000\066\000\070\001\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\085\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ @@ -2626,8 +2672,8 @@ \\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ \\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ \\045\000\117\000\046\000\116\000\051\000\115\000\055\000\114\000\ -\\063\000\111\000\065\000\110\000\066\000\065\001\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ +\\063\000\111\000\065\000\110\000\066\000\071\001\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\085\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ @@ -2635,8 +2681,8 @@ \\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ \\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ \\045\000\117\000\046\000\116\000\051\000\115\000\055\000\114\000\ -\\063\000\111\000\065\000\110\000\066\000\066\001\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ +\\063\000\111\000\065\000\110\000\066\000\072\001\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\085\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ @@ -2644,10 +2690,10 @@ \\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ \\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ \\045\000\117\000\046\000\116\000\051\000\115\000\055\000\114\000\ -\\063\000\111\000\065\000\110\000\066\000\067\001\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ -\\061\000\068\001\000\000\ -\\011\000\070\001\064\000\069\001\000\000\ +\\063\000\111\000\065\000\110\000\066\000\073\001\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ +\\061\000\074\001\000\000\ +\\011\000\076\001\064\000\075\001\000\000\ \\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\085\000\022\000\084\000\023\000\083\000\ @@ -2658,7 +2704,7 @@ \\045\000\117\000\046\000\116\000\051\000\115\000\055\000\114\000\ \\063\000\111\000\065\000\110\000\066\000\109\000\067\000\108\000\ \\068\000\107\000\069\000\106\000\070\000\105\000\071\000\104\000\ -\\072\000\237\000\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\072\000\238\000\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\000\000\ \\000\000\ \\000\000\ @@ -2672,8 +2718,8 @@ \\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ \\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ \\045\000\142\000\046\000\141\000\051\000\140\000\055\000\139\000\ -\\077\000\136\000\085\000\133\000\089\000\132\000\090\000\076\001\ -\\138\000\123\000\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\077\000\136\000\085\000\133\000\089\000\132\000\090\000\082\001\ +\\139\000\123\000\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\085\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ @@ -2681,8 +2727,8 @@ \\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ \\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ \\045\000\142\000\046\000\141\000\051\000\140\000\055\000\139\000\ -\\077\000\136\000\085\000\133\000\089\000\132\000\090\000\077\001\ -\\138\000\123\000\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\077\000\136\000\085\000\133\000\089\000\132\000\090\000\083\001\ +\\139\000\123\000\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\085\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ @@ -2690,8 +2736,8 @@ \\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ \\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ \\045\000\142\000\046\000\141\000\051\000\140\000\055\000\139\000\ -\\077\000\136\000\085\000\133\000\089\000\132\000\090\000\078\001\ -\\138\000\123\000\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\077\000\136\000\085\000\133\000\089\000\132\000\090\000\084\001\ +\\139\000\123\000\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\085\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ @@ -2699,8 +2745,8 @@ \\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ \\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ \\045\000\142\000\046\000\141\000\051\000\140\000\055\000\139\000\ -\\077\000\136\000\085\000\133\000\089\000\132\000\090\000\079\001\ -\\138\000\123\000\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\077\000\136\000\085\000\133\000\089\000\132\000\090\000\085\001\ +\\139\000\123\000\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\085\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ @@ -2708,13 +2754,13 @@ \\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ \\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ \\045\000\142\000\046\000\141\000\051\000\140\000\055\000\139\000\ -\\077\000\136\000\085\000\133\000\089\000\132\000\090\000\080\001\ -\\138\000\123\000\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ -\\009\000\089\001\011\000\088\001\047\000\087\001\079\000\086\001\ -\\080\000\085\001\081\000\084\001\082\000\083\001\141\000\082\001\ -\\145\000\081\001\000\000\ -\\074\000\092\001\000\000\ -\\011\000\096\001\086\000\095\001\087\000\094\001\088\000\093\001\000\000\ +\\077\000\136\000\085\000\133\000\089\000\132\000\090\000\086\001\ +\\139\000\123\000\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ +\\009\000\095\001\011\000\094\001\047\000\093\001\079\000\092\001\ +\\080\000\091\001\081\000\090\001\082\000\089\001\144\000\088\001\ +\\148\000\087\001\000\000\ +\\074\000\098\001\000\000\ +\\011\000\102\001\086\000\101\001\087\000\100\001\088\000\099\001\000\000\ \\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\085\000\022\000\084\000\023\000\083\000\ @@ -2725,10 +2771,22 @@ \\045\000\142\000\046\000\141\000\051\000\140\000\055\000\139\000\ \\077\000\136\000\085\000\133\000\089\000\132\000\090\000\131\000\ \\091\000\130\000\092\000\129\000\093\000\128\000\094\000\127\000\ -\\095\000\126\000\096\000\000\001\138\000\123\000\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ -\\051\000\140\000\089\000\059\001\140\000\097\001\000\000\ -\\051\000\140\000\089\000\057\001\139\000\098\001\000\000\ +\\095\000\126\000\096\000\001\001\139\000\123\000\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ +\\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ +\\019\000\086\000\020\000\226\000\022\000\084\000\023\000\083\000\ +\\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ +\\028\000\078\000\029\000\077\000\030\000\076\000\031\000\075\000\ +\\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ +\\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ +\\045\000\064\001\142\000\103\001\143\000\062\001\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ +\\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ +\\019\000\086\000\020\000\060\001\022\000\084\000\023\000\083\000\ +\\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ +\\028\000\078\000\029\000\077\000\030\000\076\000\031\000\075\000\ +\\032\000\184\000\033\000\073\000\034\000\072\000\140\000\104\001\ +\\141\000\058\001\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\085\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ @@ -2738,8 +2796,8 @@ \\045\000\142\000\046\000\141\000\051\000\140\000\055\000\139\000\ \\077\000\136\000\085\000\133\000\089\000\132\000\090\000\131\000\ \\091\000\130\000\092\000\129\000\093\000\128\000\094\000\127\000\ -\\095\000\126\000\096\000\099\001\138\000\123\000\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ +\\095\000\126\000\096\000\105\001\139\000\123\000\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ \\000\000\ \\000\000\ \\000\000\ @@ -2754,9 +2812,9 @@ \\032\000\184\000\033\000\073\000\034\000\072\000\036\000\183\000\ \\037\000\182\000\046\000\181\000\049\000\180\000\050\000\179\000\ \\051\000\178\000\052\000\177\000\053\000\176\000\054\000\175\000\ -\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\107\001\ -\\113\000\160\000\117\000\159\000\118\000\106\001\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ +\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\113\001\ +\\113\000\160\000\117\000\159\000\118\000\112\001\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\188\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ @@ -2764,9 +2822,9 @@ \\032\000\184\000\033\000\073\000\034\000\072\000\036\000\183\000\ \\037\000\182\000\046\000\181\000\049\000\180\000\050\000\179\000\ \\051\000\178\000\052\000\177\000\053\000\176\000\054\000\175\000\ -\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\107\001\ -\\113\000\160\000\117\000\159\000\118\000\109\001\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ +\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\113\001\ +\\113\000\160\000\117\000\159\000\118\000\115\001\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\188\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ @@ -2774,9 +2832,9 @@ \\032\000\184\000\033\000\073\000\034\000\072\000\036\000\183\000\ \\037\000\182\000\046\000\181\000\049\000\180\000\050\000\179\000\ \\051\000\178\000\052\000\177\000\053\000\176\000\054\000\175\000\ -\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\107\001\ -\\113\000\160\000\117\000\159\000\118\000\110\001\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ +\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\113\001\ +\\113\000\160\000\117\000\159\000\118\000\116\001\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\188\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ @@ -2784,9 +2842,9 @@ \\032\000\184\000\033\000\073\000\034\000\072\000\036\000\183\000\ \\037\000\182\000\046\000\181\000\049\000\180\000\050\000\179\000\ \\051\000\178\000\052\000\177\000\053\000\176\000\054\000\175\000\ -\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\107\001\ -\\113\000\160\000\117\000\159\000\118\000\111\001\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ +\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\113\001\ +\\113\000\160\000\117\000\159\000\118\000\117\001\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\188\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ @@ -2794,9 +2852,9 @@ \\032\000\184\000\033\000\073\000\034\000\072\000\036\000\183\000\ \\037\000\182\000\046\000\181\000\049\000\180\000\050\000\179\000\ \\051\000\178\000\052\000\177\000\053\000\176\000\054\000\175\000\ -\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\107\001\ -\\113\000\160\000\117\000\159\000\118\000\112\001\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ +\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\113\001\ +\\113\000\160\000\117\000\159\000\118\000\118\001\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\188\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ @@ -2804,9 +2862,9 @@ \\032\000\184\000\033\000\073\000\034\000\072\000\036\000\183\000\ \\037\000\182\000\046\000\181\000\049\000\180\000\050\000\179\000\ \\051\000\178\000\052\000\177\000\053\000\176\000\054\000\175\000\ -\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\107\001\ -\\113\000\160\000\117\000\159\000\118\000\113\001\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ +\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\113\001\ +\\113\000\160\000\117\000\159\000\118\000\119\001\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\188\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ @@ -2814,9 +2872,9 @@ \\032\000\184\000\033\000\073\000\034\000\072\000\036\000\183\000\ \\037\000\182\000\046\000\181\000\049\000\180\000\050\000\179\000\ \\051\000\178\000\052\000\177\000\053\000\176\000\054\000\175\000\ -\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\107\001\ -\\113\000\160\000\117\000\159\000\118\000\114\001\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ +\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\113\001\ +\\113\000\160\000\117\000\159\000\118\000\120\001\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\188\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ @@ -2826,11 +2884,11 @@ \\051\000\178\000\052\000\177\000\053\000\176\000\054\000\175\000\ \\056\000\174\000\101\000\171\000\102\000\170\000\103\000\169\000\ \\104\000\168\000\105\000\167\000\106\000\166\000\107\000\165\000\ -\\108\000\164\000\109\000\116\001\110\000\163\000\111\000\162\000\ +\\108\000\164\000\109\000\122\001\110\000\163\000\111\000\162\000\ \\112\000\161\000\113\000\160\000\117\000\159\000\118\000\158\000\ \\119\000\157\000\120\000\156\000\121\000\155\000\122\000\154\000\ -\\123\000\153\000\124\000\152\000\125\000\115\001\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ +\\123\000\153\000\124\000\152\000\125\000\121\001\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\188\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ @@ -2838,9 +2896,9 @@ \\032\000\184\000\033\000\073\000\034\000\072\000\036\000\183\000\ \\037\000\182\000\046\000\181\000\049\000\180\000\050\000\179\000\ \\051\000\178\000\052\000\177\000\053\000\176\000\054\000\175\000\ -\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\107\001\ -\\108\000\118\001\113\000\160\000\117\000\159\000\118\000\117\001\ -\\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\113\001\ +\\108\000\124\001\113\000\160\000\117\000\159\000\118\000\123\001\ +\\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\188\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ @@ -2848,9 +2906,9 @@ \\032\000\184\000\033\000\073\000\034\000\072\000\036\000\183\000\ \\037\000\182\000\046\000\181\000\049\000\180\000\050\000\179\000\ \\051\000\178\000\052\000\177\000\053\000\176\000\054\000\175\000\ -\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\107\001\ -\\108\000\119\001\113\000\160\000\117\000\159\000\118\000\117\001\ -\\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\113\001\ +\\108\000\125\001\113\000\160\000\117\000\159\000\118\000\123\001\ +\\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\188\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ @@ -2858,9 +2916,9 @@ \\032\000\184\000\033\000\073\000\034\000\072\000\036\000\183\000\ \\037\000\182\000\046\000\181\000\049\000\180\000\050\000\179\000\ \\051\000\178\000\052\000\177\000\053\000\176\000\054\000\175\000\ -\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\107\001\ -\\106\000\121\001\108\000\120\001\113\000\160\000\117\000\159\000\ -\\118\000\117\001\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\113\001\ +\\106\000\127\001\108\000\126\001\113\000\160\000\117\000\159\000\ +\\118\000\123\001\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\188\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ @@ -2868,9 +2926,9 @@ \\032\000\184\000\033\000\073\000\034\000\072\000\036\000\183\000\ \\037\000\182\000\046\000\181\000\049\000\180\000\050\000\179\000\ \\051\000\178\000\052\000\177\000\053\000\176\000\054\000\175\000\ -\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\107\001\ -\\108\000\122\001\113\000\160\000\117\000\159\000\118\000\117\001\ -\\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\113\001\ +\\108\000\128\001\113\000\160\000\117\000\159\000\118\000\123\001\ +\\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\188\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ @@ -2878,11 +2936,11 @@ \\032\000\184\000\033\000\073\000\034\000\072\000\036\000\183\000\ \\037\000\182\000\046\000\181\000\049\000\180\000\050\000\179\000\ \\051\000\178\000\052\000\177\000\053\000\176\000\054\000\175\000\ -\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\107\001\ -\\108\000\123\001\113\000\160\000\117\000\159\000\118\000\117\001\ -\\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ -\\098\000\124\001\000\000\ -\\011\000\128\001\114\000\127\001\115\000\126\001\116\000\125\001\000\000\ +\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\113\001\ +\\108\000\129\001\113\000\160\000\117\000\159\000\118\000\123\001\ +\\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ +\\098\000\130\001\000\000\ +\\011\000\134\001\114\000\133\001\115\000\132\001\116\000\131\001\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\188\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ @@ -2895,10 +2953,11 @@ \\108\000\164\000\110\000\163\000\111\000\162\000\112\000\161\000\ \\113\000\160\000\117\000\159\000\118\000\158\000\119\000\157\000\ \\120\000\156\000\121\000\155\000\122\000\154\000\123\000\153\000\ -\\124\000\152\000\125\000\129\001\144\000\061\000\145\000\060\000\ -\\146\000\059\000\000\000\ -\\009\000\090\000\019\000\131\001\031\000\130\001\000\000\ -\\051\000\178\000\054\000\175\000\117\000\133\001\137\000\132\001\000\000\ +\\124\000\152\000\125\000\135\001\147\000\061\000\148\000\060\000\ +\\149\000\059\000\000\000\ +\\009\000\090\000\019\000\137\001\031\000\136\001\000\000\ +\\051\000\178\000\054\000\175\000\117\000\139\001\138\000\138\001\000\000\ +\\051\000\178\000\054\000\175\000\117\000\141\001\137\000\140\001\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\188\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ @@ -2911,8 +2970,8 @@ \\108\000\164\000\110\000\163\000\111\000\162\000\112\000\161\000\ \\113\000\160\000\117\000\159\000\118\000\158\000\119\000\157\000\ \\120\000\156\000\121\000\155\000\122\000\154\000\123\000\153\000\ -\\124\000\152\000\125\000\134\001\144\000\061\000\145\000\060\000\ -\\146\000\059\000\000\000\ +\\124\000\152\000\125\000\142\001\147\000\061\000\148\000\060\000\ +\\149\000\059\000\000\000\ \\000\000\ \\000\000\ \\000\000\ @@ -2930,27 +2989,31 @@ \\108\000\164\000\110\000\163\000\111\000\162\000\112\000\161\000\ \\113\000\160\000\117\000\159\000\118\000\158\000\119\000\157\000\ \\120\000\156\000\121\000\155\000\122\000\154\000\123\000\153\000\ -\\124\000\152\000\125\000\026\001\144\000\061\000\145\000\060\000\ -\\146\000\059\000\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\005\000\142\001\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\006\000\041\001\007\000\150\001\008\000\149\001\009\000\039\001\ -\\010\000\038\001\011\000\037\001\012\000\036\001\013\000\035\001\ -\\014\000\087\000\016\000\034\001\000\000\ +\\124\000\152\000\125\000\028\001\147\000\061\000\148\000\060\000\ +\\149\000\059\000\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\005\000\150\001\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\006\000\043\001\007\000\158\001\008\000\157\001\009\000\041\001\ +\\010\000\040\001\011\000\039\001\012\000\038\001\013\000\037\001\ +\\014\000\087\000\016\000\036\001\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ \\000\000\ \\000\000\ \\000\000\ @@ -2982,30 +3045,30 @@ \\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ \\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ \\045\000\117\000\046\000\116\000\051\000\115\000\055\000\114\000\ -\\060\000\162\001\063\000\111\000\065\000\110\000\066\000\109\000\ +\\060\000\174\001\063\000\111\000\065\000\110\000\066\000\109\000\ \\067\000\108\000\068\000\107\000\069\000\106\000\070\000\105\000\ -\\071\000\104\000\072\000\239\000\144\000\061\000\145\000\060\000\ -\\146\000\059\000\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\009\000\089\001\011\000\088\001\047\000\087\001\078\000\170\001\ -\\079\000\169\001\080\000\168\001\081\000\084\001\141\000\167\001\ -\\145\000\081\001\000\000\ +\\071\000\104\000\072\000\240\000\147\000\061\000\148\000\060\000\ +\\149\000\059\000\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\009\000\095\001\011\000\094\001\047\000\093\001\078\000\182\001\ +\\079\000\181\001\080\000\180\001\081\000\090\001\144\000\179\001\ +\\148\000\087\001\000\000\ \\000\000\ \\000\000\ \\000\000\ @@ -3024,10 +3087,10 @@ \\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ \\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ \\045\000\142\000\046\000\141\000\051\000\140\000\055\000\139\000\ -\\075\000\178\001\077\000\136\000\085\000\133\000\089\000\132\000\ +\\075\000\190\001\077\000\136\000\085\000\133\000\089\000\132\000\ \\090\000\131\000\091\000\130\000\092\000\129\000\093\000\128\000\ -\\094\000\127\000\095\000\126\000\096\000\003\001\138\000\123\000\ -\\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\094\000\127\000\095\000\126\000\096\000\004\001\139\000\123\000\ +\\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\000\000\ \\000\000\ \\000\000\ @@ -3044,8 +3107,10 @@ \\108\000\164\000\110\000\163\000\111\000\162\000\112\000\161\000\ \\113\000\160\000\117\000\159\000\118\000\158\000\119\000\157\000\ \\120\000\156\000\121\000\155\000\122\000\154\000\123\000\153\000\ -\\124\000\152\000\125\000\180\001\144\000\061\000\145\000\060\000\ -\\146\000\059\000\000\000\ +\\124\000\152\000\125\000\192\001\147\000\061\000\148\000\060\000\ +\\149\000\059\000\000\000\ +\\000\000\ +\\000\000\ \\000\000\ \\000\000\ \\000\000\ @@ -3081,23 +3146,23 @@ \\032\000\184\000\033\000\073\000\034\000\072\000\036\000\183\000\ \\037\000\182\000\046\000\181\000\049\000\180\000\050\000\179\000\ \\051\000\178\000\052\000\177\000\053\000\176\000\054\000\175\000\ -\\056\000\174\000\099\000\187\001\101\000\171\000\102\000\170\000\ +\\056\000\174\000\099\000\200\001\101\000\171\000\102\000\170\000\ \\103\000\169\000\104\000\168\000\105\000\167\000\106\000\166\000\ \\107\000\165\000\108\000\164\000\110\000\163\000\111\000\162\000\ \\112\000\161\000\113\000\160\000\117\000\159\000\118\000\158\000\ \\119\000\157\000\120\000\156\000\121\000\155\000\122\000\154\000\ -\\123\000\153\000\124\000\152\000\125\000\028\001\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ -\\000\000\ -\\000\000\ -\\006\000\041\001\008\000\188\001\009\000\039\001\010\000\038\001\ -\\011\000\037\001\012\000\036\001\013\000\035\001\014\000\087\000\ -\\016\000\034\001\000\000\ -\\006\000\041\001\007\000\189\001\008\000\149\001\009\000\039\001\ -\\010\000\038\001\011\000\037\001\012\000\036\001\013\000\035\001\ -\\014\000\087\000\016\000\034\001\000\000\ -\\000\000\ -\\006\000\191\001\017\000\190\001\000\000\ +\\123\000\153\000\124\000\152\000\125\000\030\001\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ +\\000\000\ +\\000\000\ +\\006\000\043\001\008\000\201\001\009\000\041\001\010\000\040\001\ +\\011\000\039\001\012\000\038\001\013\000\037\001\014\000\087\000\ +\\016\000\036\001\000\000\ +\\006\000\043\001\007\000\202\001\008\000\157\001\009\000\041\001\ +\\010\000\040\001\011\000\039\001\012\000\038\001\013\000\037\001\ +\\014\000\087\000\016\000\036\001\000\000\ +\\000\000\ +\\006\000\204\001\017\000\203\001\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\144\000\020\000\085\000\022\000\084\000\023\000\143\000\ \\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ @@ -3108,14 +3173,14 @@ \\074\000\138\000\076\000\137\000\077\000\136\000\083\000\135\000\ \\084\000\134\000\085\000\133\000\089\000\132\000\090\000\131\000\ \\091\000\130\000\092\000\129\000\093\000\128\000\094\000\127\000\ -\\095\000\126\000\096\000\125\000\097\000\192\001\138\000\123\000\ -\\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\095\000\126\000\096\000\125\000\097\000\205\001\139\000\123\000\ +\\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ -\\019\000\086\000\020\000\193\001\022\000\084\000\023\000\083\000\ +\\019\000\086\000\020\000\206\001\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ \\028\000\078\000\029\000\077\000\030\000\076\000\031\000\075\000\ -\\032\000\184\000\033\000\073\000\034\000\072\000\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ +\\032\000\184\000\033\000\073\000\034\000\072\000\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\085\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ @@ -3123,7 +3188,7 @@ \\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ \\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ \\045\000\066\000\055\000\065\000\057\000\064\000\058\000\063\000\ -\\059\000\194\001\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\059\000\207\001\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\085\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ @@ -3133,8 +3198,8 @@ \\045\000\117\000\046\000\116\000\051\000\115\000\055\000\114\000\ \\061\000\113\000\062\000\112\000\063\000\111\000\065\000\110\000\ \\066\000\109\000\067\000\108\000\068\000\107\000\069\000\106\000\ -\\070\000\105\000\071\000\104\000\072\000\103\000\073\000\195\001\ -\\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\070\000\105\000\071\000\104\000\072\000\103\000\073\000\208\001\ +\\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\188\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ @@ -3148,58 +3213,75 @@ \\111\000\162\000\112\000\161\000\113\000\160\000\117\000\159\000\ \\118\000\158\000\119\000\157\000\120\000\156\000\121\000\155\000\ \\122\000\154\000\123\000\153\000\124\000\152\000\125\000\151\000\ -\\126\000\196\001\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\126\000\209\001\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\000\000\ \\000\000\ \\000\000\ \\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ -\\019\000\086\000\020\000\051\001\021\000\199\001\022\000\084\000\ +\\019\000\086\000\020\000\053\001\021\000\212\001\022\000\084\000\ \\023\000\083\000\024\000\082\000\025\000\187\000\026\000\080\000\ \\027\000\186\000\028\000\078\000\029\000\077\000\030\000\076\000\ \\031\000\075\000\032\000\184\000\033\000\073\000\034\000\072\000\ -\\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\000\000\ \\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ -\\019\000\086\000\020\000\200\001\022\000\084\000\023\000\083\000\ +\\019\000\086\000\020\000\213\001\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ \\028\000\078\000\029\000\077\000\030\000\076\000\031\000\075\000\ -\\032\000\184\000\033\000\073\000\034\000\072\000\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ +\\032\000\184\000\033\000\073\000\034\000\072\000\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ -\\019\000\086\000\020\000\201\001\022\000\084\000\023\000\083\000\ +\\019\000\086\000\020\000\214\001\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ \\028\000\078\000\029\000\077\000\030\000\076\000\031\000\075\000\ -\\032\000\184\000\033\000\073\000\034\000\072\000\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ +\\032\000\184\000\033\000\073\000\034\000\072\000\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ +\\011\000\102\001\086\000\101\001\087\000\100\001\088\000\215\001\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ -\\019\000\086\000\020\000\202\001\022\000\084\000\023\000\083\000\ +\\019\000\086\000\020\000\216\001\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ \\028\000\078\000\029\000\077\000\030\000\076\000\031\000\075\000\ -\\032\000\184\000\033\000\073\000\034\000\072\000\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ -\\000\000\ -\\000\000\ -\\011\000\070\001\064\000\204\001\000\000\ -\\000\000\ -\\000\000\ -\\009\000\089\001\011\000\088\001\047\000\087\001\080\000\205\001\ -\\145\000\081\001\000\000\ -\\009\000\089\001\011\000\088\001\047\000\087\001\080\000\207\001\ -\\143\000\206\001\145\000\081\001\000\000\ -\\011\000\096\001\086\000\095\001\087\000\094\001\088\000\208\001\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\009\000\089\001\011\000\088\001\047\000\087\001\078\000\214\001\ -\\079\000\169\001\080\000\168\001\081\000\084\001\141\000\167\001\ -\\145\000\081\001\000\000\ -\\000\000\ -\\011\000\096\001\086\000\095\001\087\000\094\001\088\000\216\001\000\000\ -\\009\000\089\001\011\000\088\001\047\000\087\001\080\000\217\001\ -\\145\000\081\001\000\000\ +\\032\000\184\000\033\000\073\000\034\000\072\000\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ +\\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ +\\019\000\086\000\020\000\085\000\022\000\084\000\023\000\083\000\ +\\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ +\\028\000\078\000\029\000\077\000\030\000\076\000\031\000\075\000\ +\\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ +\\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ +\\045\000\142\000\046\000\141\000\051\000\140\000\055\000\139\000\ +\\077\000\136\000\085\000\133\000\089\000\132\000\090\000\217\001\ +\\139\000\123\000\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ +\\011\000\102\001\086\000\101\001\087\000\100\001\088\000\218\001\000\000\ +\\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ +\\019\000\086\000\020\000\219\001\022\000\084\000\023\000\083\000\ +\\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ +\\028\000\078\000\029\000\077\000\030\000\076\000\031\000\075\000\ +\\032\000\184\000\033\000\073\000\034\000\072\000\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ +\\000\000\ +\\000\000\ +\\011\000\076\001\064\000\221\001\000\000\ +\\000\000\ +\\000\000\ +\\009\000\095\001\011\000\094\001\047\000\093\001\080\000\222\001\ +\\148\000\087\001\000\000\ +\\009\000\095\001\011\000\094\001\047\000\093\001\080\000\224\001\ +\\146\000\223\001\148\000\087\001\000\000\ +\\011\000\102\001\086\000\101\001\087\000\100\001\088\000\225\001\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\009\000\095\001\011\000\094\001\047\000\093\001\078\000\231\001\ +\\079\000\181\001\080\000\180\001\081\000\090\001\144\000\179\001\ +\\148\000\087\001\000\000\ +\\000\000\ +\\011\000\102\001\086\000\101\001\087\000\100\001\088\000\233\001\000\000\ +\\009\000\095\001\011\000\094\001\047\000\093\001\080\000\234\001\ +\\148\000\087\001\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\144\000\020\000\085\000\022\000\084\000\023\000\143\000\ \\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ @@ -3210,8 +3292,8 @@ \\074\000\138\000\076\000\137\000\077\000\136\000\083\000\135\000\ \\084\000\134\000\085\000\133\000\089\000\132\000\090\000\131\000\ \\091\000\130\000\092\000\129\000\093\000\128\000\094\000\127\000\ -\\095\000\126\000\096\000\125\000\097\000\218\001\138\000\123\000\ -\\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\095\000\126\000\096\000\125\000\097\000\235\001\139\000\123\000\ +\\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\144\000\020\000\085\000\022\000\084\000\023\000\143\000\ \\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ @@ -3222,8 +3304,8 @@ \\074\000\138\000\076\000\137\000\077\000\136\000\083\000\135\000\ \\084\000\134\000\085\000\133\000\089\000\132\000\090\000\131\000\ \\091\000\130\000\092\000\129\000\093\000\128\000\094\000\127\000\ -\\095\000\126\000\096\000\125\000\097\000\219\001\138\000\123\000\ -\\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\095\000\126\000\096\000\125\000\097\000\236\001\139\000\123\000\ +\\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\085\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ @@ -3233,13 +3315,13 @@ \\045\000\142\000\046\000\141\000\051\000\140\000\055\000\139\000\ \\077\000\136\000\085\000\133\000\089\000\132\000\090\000\131\000\ \\091\000\130\000\092\000\129\000\093\000\128\000\094\000\127\000\ -\\095\000\126\000\096\000\220\001\138\000\123\000\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\011\000\128\001\114\000\127\001\115\000\126\001\116\000\223\001\000\000\ +\\095\000\126\000\096\000\237\001\139\000\123\000\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\011\000\134\001\114\000\133\001\115\000\132\001\116\000\240\001\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\188\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ @@ -3249,11 +3331,11 @@ \\051\000\178\000\052\000\177\000\053\000\176\000\054\000\175\000\ \\056\000\174\000\101\000\171\000\102\000\170\000\103\000\169\000\ \\104\000\168\000\105\000\167\000\106\000\166\000\107\000\165\000\ -\\108\000\164\000\109\000\224\001\110\000\163\000\111\000\162\000\ +\\108\000\164\000\109\000\241\001\110\000\163\000\111\000\162\000\ \\112\000\161\000\113\000\160\000\117\000\159\000\118\000\158\000\ \\119\000\157\000\120\000\156\000\121\000\155\000\122\000\154\000\ -\\123\000\153\000\124\000\152\000\125\000\115\001\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ +\\123\000\153\000\124\000\152\000\125\000\121\001\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ \\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\188\000\022\000\084\000\023\000\083\000\ @@ -3268,7 +3350,21 @@ \\111\000\162\000\112\000\161\000\113\000\160\000\117\000\159\000\ \\118\000\158\000\119\000\157\000\120\000\156\000\121\000\155\000\ \\122\000\154\000\123\000\153\000\124\000\152\000\125\000\151\000\ -\\126\000\225\001\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\126\000\242\001\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ +\\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ +\\019\000\086\000\020\000\188\000\022\000\084\000\023\000\083\000\ +\\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ +\\028\000\078\000\029\000\077\000\030\000\076\000\031\000\185\000\ +\\032\000\184\000\033\000\073\000\034\000\072\000\036\000\183\000\ +\\037\000\182\000\046\000\181\000\049\000\180\000\050\000\179\000\ +\\051\000\178\000\052\000\177\000\053\000\176\000\054\000\175\000\ +\\056\000\174\000\098\000\173\000\100\000\172\000\101\000\171\000\ +\\102\000\170\000\103\000\169\000\104\000\168\000\105\000\167\000\ +\\106\000\166\000\107\000\165\000\108\000\164\000\110\000\163\000\ +\\111\000\162\000\112\000\161\000\113\000\160\000\117\000\159\000\ +\\118\000\158\000\119\000\157\000\120\000\156\000\121\000\155\000\ +\\122\000\154\000\123\000\153\000\124\000\152\000\125\000\151\000\ +\\126\000\243\001\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ \\019\000\086\000\020\000\188\000\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ @@ -3281,21 +3377,25 @@ \\108\000\164\000\110\000\163\000\111\000\162\000\112\000\161\000\ \\113\000\160\000\117\000\159\000\118\000\158\000\119\000\157\000\ \\120\000\156\000\121\000\155\000\122\000\154\000\123\000\153\000\ -\\124\000\152\000\125\000\226\001\144\000\061\000\145\000\060\000\ -\\146\000\059\000\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\006\000\041\001\007\000\233\001\008\000\149\001\009\000\039\001\ -\\010\000\038\001\011\000\037\001\012\000\036\001\013\000\035\001\ -\\014\000\087\000\016\000\034\001\000\000\ +\\124\000\152\000\125\000\244\001\147\000\061\000\148\000\060\000\ +\\149\000\059\000\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\006\000\043\001\007\000\251\001\008\000\157\001\009\000\041\001\ +\\010\000\040\001\011\000\039\001\012\000\038\001\013\000\037\001\ +\\014\000\087\000\016\000\036\001\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ \\000\000\ \\000\000\ \\000\000\ @@ -3308,19 +3408,19 @@ \\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ \\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ \\045\000\117\000\046\000\116\000\051\000\115\000\055\000\114\000\ -\\063\000\111\000\065\000\110\000\066\000\237\001\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\009\000\089\001\011\000\088\001\047\000\087\001\080\000\241\001\ -\\145\000\081\001\000\000\ -\\000\000\ -\\009\000\089\001\011\000\088\001\047\000\087\001\080\000\242\001\ -\\145\000\081\001\000\000\ +\\063\000\111\000\065\000\110\000\066\000\001\002\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\009\000\095\001\011\000\094\001\047\000\093\001\080\000\005\002\ +\\148\000\087\001\000\000\ +\\000\000\ +\\009\000\095\001\011\000\094\001\047\000\093\001\080\000\006\002\ +\\148\000\087\001\000\000\ \\000\000\ \\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ @@ -3330,8 +3430,8 @@ \\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ \\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ \\045\000\142\000\046\000\141\000\051\000\140\000\055\000\139\000\ -\\077\000\136\000\085\000\133\000\089\000\132\000\090\000\244\001\ -\\138\000\123\000\144\000\061\000\145\000\060\000\146\000\059\000\000\000\ +\\077\000\136\000\085\000\133\000\089\000\132\000\090\000\008\002\ +\\139\000\123\000\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ \\000\000\ \\000\000\ \\000\000\ @@ -3345,9 +3445,12 @@ \\032\000\184\000\033\000\073\000\034\000\072\000\036\000\183\000\ \\037\000\182\000\046\000\181\000\049\000\180\000\050\000\179\000\ \\051\000\178\000\052\000\177\000\053\000\176\000\054\000\175\000\ -\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\107\001\ -\\113\000\160\000\117\000\159\000\118\000\248\001\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ +\\056\000\174\000\101\000\171\000\102\000\170\000\103\000\113\001\ +\\113\000\160\000\117\000\159\000\118\000\012\002\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ \\000\000\ \\000\000\ \\000\000\ @@ -3362,15 +3465,15 @@ \\000\000\ \\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ -\\019\000\086\000\020\000\251\001\022\000\084\000\023\000\083\000\ +\\019\000\086\000\020\000\018\002\022\000\084\000\023\000\083\000\ \\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ \\028\000\078\000\029\000\077\000\030\000\076\000\031\000\075\000\ -\\032\000\184\000\033\000\073\000\034\000\072\000\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ -\\000\000\ -\\000\000\ -\\009\000\089\001\011\000\088\001\047\000\087\001\080\000\207\001\ -\\143\000\252\001\145\000\081\001\000\000\ +\\032\000\184\000\033\000\073\000\034\000\072\000\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ +\\000\000\ +\\000\000\ +\\009\000\095\001\011\000\094\001\047\000\093\001\080\000\224\001\ +\\146\000\019\002\148\000\087\001\000\000\ \\000\000\ \\000\000\ \\000\000\ @@ -3387,8 +3490,9 @@ \\045\000\142\000\046\000\141\000\051\000\140\000\055\000\139\000\ \\077\000\136\000\085\000\133\000\089\000\132\000\090\000\131\000\ \\091\000\130\000\092\000\129\000\093\000\128\000\094\000\127\000\ -\\095\000\126\000\096\000\254\001\138\000\123\000\144\000\061\000\ -\\145\000\060\000\146\000\059\000\000\000\ +\\095\000\126\000\096\000\021\002\139\000\123\000\147\000\061\000\ +\\148\000\060\000\149\000\059\000\000\000\ +\\000\000\ \\000\000\ \\000\000\ \\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ @@ -3403,32 +3507,48 @@ \\108\000\164\000\110\000\163\000\111\000\162\000\112\000\161\000\ \\113\000\160\000\117\000\159\000\118\000\158\000\119\000\157\000\ \\120\000\156\000\121\000\155\000\122\000\154\000\123\000\153\000\ -\\124\000\152\000\125\000\255\001\144\000\061\000\145\000\060\000\ -\\146\000\059\000\000\000\ -\\000\000\ -\\000\000\ -\\009\000\089\001\011\000\088\001\047\000\087\001\080\000\002\002\ -\\142\000\001\002\145\000\081\001\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\009\000\089\001\011\000\088\001\047\000\087\001\079\000\007\002\ -\\080\000\006\002\081\000\084\001\145\000\081\001\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\000\000\ -\\009\000\089\001\011\000\088\001\047\000\087\001\078\000\170\001\ -\\079\000\169\001\080\000\168\001\081\000\084\001\145\000\081\001\000\000\ -\\000\000\ -\\009\000\089\001\011\000\088\001\047\000\087\001\078\000\214\001\ -\\079\000\169\001\080\000\168\001\081\000\084\001\145\000\081\001\000\000\ +\\124\000\152\000\125\000\022\002\147\000\061\000\148\000\060\000\ +\\149\000\059\000\000\000\ +\\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ +\\019\000\086\000\020\000\060\001\022\000\084\000\023\000\083\000\ +\\024\000\082\000\025\000\187\000\026\000\080\000\027\000\186\000\ +\\028\000\078\000\029\000\077\000\030\000\076\000\031\000\075\000\ +\\032\000\184\000\033\000\073\000\034\000\072\000\141\000\023\002\ +\\147\000\061\000\148\000\060\000\149\000\059\000\000\000\ +\\009\000\090\000\011\000\089\000\012\000\088\000\014\000\087\000\ +\\019\000\086\000\020\000\226\000\022\000\084\000\023\000\083\000\ +\\024\000\082\000\025\000\081\000\026\000\080\000\027\000\079\000\ +\\028\000\078\000\029\000\077\000\030\000\076\000\031\000\075\000\ +\\032\000\074\000\033\000\073\000\034\000\072\000\035\000\071\000\ +\\039\000\070\000\042\000\069\000\043\000\068\000\044\000\067\000\ +\\045\000\064\001\143\000\024\002\147\000\061\000\148\000\060\000\ +\\149\000\059\000\000\000\ +\\000\000\ +\\000\000\ +\\009\000\095\001\011\000\094\001\047\000\093\001\080\000\027\002\ +\\145\000\026\002\148\000\087\001\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\009\000\095\001\011\000\094\001\047\000\093\001\079\000\032\002\ +\\080\000\031\002\081\000\090\001\148\000\087\001\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\000\000\ +\\009\000\095\001\011\000\094\001\047\000\093\001\078\000\182\001\ +\\079\000\181\001\080\000\180\001\081\000\090\001\148\000\087\001\000\000\ +\\000\000\ +\\009\000\095\001\011\000\094\001\047\000\093\001\078\000\231\001\ +\\079\000\181\001\080\000\180\001\081\000\090\001\148\000\087\001\000\000\ \\000\000\ \" -val numstates = 524 -val numrules = 290 +val numstates = 549 +val numrules = 296 val s = Unsynchronized.ref "" and index = Unsynchronized.ref 0 val string_to_int = fn () => let val i = !index @@ -3500,9 +3620,12 @@ | atomic_system_word of (string) | atomic_defined_word of (string) | let_term of (tptp_term) | tff_type_arguments of (tptp_type list) | tff_monotype of (tptp_type) | tff_quantified_type of (tptp_type) - | tff_let_formula_defn of (tptp_let list) - | tff_let_term_defn of (tptp_let list) | tff_let of (tptp_formula) - | thf_let_defn of (tptp_let list) | tptp of (tptp_problem) + | tff_let_formula_binding of (tptp_formula) + | tff_let_formula_defn of (tptp_let) + | tff_let_term_binding of (tptp_term) + | tff_let_term_defn of (tptp_let) | tff_let of (tptp_formula) + | thf_let_formula_defn of (tptp_let) + | thf_let_term_defn of (tptp_let) | tptp of (tptp_problem) | tptp_file of (tptp_problem) | tptp_input of (tptp_line) | include_ of (tptp_line) | annotated_formula of (tptp_line) | thf_annotated of (tptp_line) | tff_annotated of (tptp_line) @@ -4105,29 +4228,50 @@ end | ( 52, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.thf_formula -thf_formula, _, _)) :: _ :: ( _, ( MlyValue.thf_let_defn thf_let_defn, - _, _)) :: _ :: ( _, ( _, LET_TF1left, _)) :: rest671)) => let val -result = MlyValue.thf_let (( - Let (thf_let_defn, thf_formula) -)) +thf_formula, _, _)) :: _ :: ( _, ( MlyValue.thf_let_term_defn +thf_let_term_defn, _, _)) :: _ :: ( _, ( _, LET_TF1left, _)) :: +rest671)) => let val result = MlyValue.thf_let ( +( Let (thf_let_term_defn, thf_formula) )) in ( LrTable.NT 101, ( result, LET_TF1left, RPAREN1right), rest671) end -| ( 53, ( ( _, ( MlyValue.thf_quantified_formula +| ( 53, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.thf_formula +thf_formula, _, _)) :: _ :: ( _, ( MlyValue.thf_let_formula_defn +thf_let_formula_defn, _, _)) :: _ :: ( _, ( _, LET_FF1left, _)) :: +rest671)) => let val result = MlyValue.thf_let ( +( Let (thf_let_formula_defn, thf_formula) )) + in ( LrTable.NT 101, ( result, LET_FF1left, RPAREN1right), rest671) + +end +| ( 54, ( ( _, ( MlyValue.thf_quantified_formula thf_quantified_formula, thf_quantified_formula1left, thf_quantified_formula1right)) :: rest671)) => let val result = -MlyValue.thf_let_defn ( +MlyValue.thf_let_term_defn ( ( let val (_, vars, fmla) = extract_quant_info thf_quantified_formula - in [Let_fmla (hd vars, fmla)] + in Let_fmla (vars, fmla) end ) ) in ( LrTable.NT 136, ( result, thf_quantified_formula1left, thf_quantified_formula1right), rest671) end -| ( 54, ( ( _, ( MlyValue.thf_top_level_type thf_top_level_type, _, +| ( 55, ( ( _, ( MlyValue.thf_quantified_formula +thf_quantified_formula, thf_quantified_formula1left, +thf_quantified_formula1right)) :: rest671)) => let val result = +MlyValue.thf_let_formula_defn ( +( + let + val (_, vars, fmla) = extract_quant_info thf_quantified_formula + in Let_fmla (vars, fmla) + end +) +) + in ( LrTable.NT 137, ( result, thf_quantified_formula1left, +thf_quantified_formula1right), rest671) +end +| ( 56, ( ( _, ( MlyValue.thf_top_level_type thf_top_level_type, _, thf_top_level_type1right)) :: _ :: ( _, ( MlyValue.thf_typeable_formula thf_typeable_formula, thf_typeable_formula1left, _)) :: rest671)) => let val result = @@ -4136,59 +4280,59 @@ in ( LrTable.NT 111, ( result, thf_typeable_formula1left, thf_top_level_type1right), rest671) end -| ( 55, ( ( _, ( MlyValue.thf_atom thf_atom, thf_atom1left, +| ( 57, ( ( _, ( MlyValue.thf_atom thf_atom, thf_atom1left, thf_atom1right)) :: rest671)) => let val result = MlyValue.thf_typeable_formula (( thf_atom )) in ( LrTable.NT 110, ( result, thf_atom1left, thf_atom1right), rest671) end -| ( 56, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( +| ( 58, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.thf_logic_formula thf_logic_formula, _, _)) :: ( _, ( _, LPAREN1left, _)) :: rest671)) => let val result = MlyValue.thf_typeable_formula (( thf_logic_formula )) in ( LrTable.NT 110, ( result, LPAREN1left, RPAREN1right), rest671) end -| ( 57, ( ( _, ( MlyValue.constant constant2, _, constant2right)) :: +| ( 59, ( ( _, ( MlyValue.constant constant2, _, constant2right)) :: _ :: ( _, ( MlyValue.constant constant1, constant1left, _)) :: rest671)) => let val result = MlyValue.thf_subtype ( ( Subtype(constant1, constant2) )) in ( LrTable.NT 109, ( result, constant1left, constant2right), rest671) end -| ( 58, ( ( _, ( MlyValue.thf_logic_formula thf_logic_formula, +| ( 60, ( ( _, ( MlyValue.thf_logic_formula thf_logic_formula, thf_logic_formula1left, thf_logic_formula1right)) :: rest671)) => let val result = MlyValue.thf_top_level_type ( ( Fmla_type thf_logic_formula )) in ( LrTable.NT 108, ( result, thf_logic_formula1left, thf_logic_formula1right), rest671) end -| ( 59, ( ( _, ( MlyValue.thf_unitary_formula thf_unitary_formula, +| ( 61, ( ( _, ( MlyValue.thf_unitary_formula thf_unitary_formula, thf_unitary_formula1left, thf_unitary_formula1right)) :: rest671)) => let val result = MlyValue.thf_unitary_type ( ( Fmla_type thf_unitary_formula )) in ( LrTable.NT 107, ( result, thf_unitary_formula1left, thf_unitary_formula1right), rest671) end -| ( 60, ( ( _, ( MlyValue.thf_mapping_type thf_mapping_type, +| ( 62, ( ( _, ( MlyValue.thf_mapping_type thf_mapping_type, thf_mapping_type1left, thf_mapping_type1right)) :: rest671)) => let val result = MlyValue.thf_binary_type (( thf_mapping_type )) in ( LrTable.NT 106, ( result, thf_mapping_type1left, thf_mapping_type1right), rest671) end -| ( 61, ( ( _, ( MlyValue.thf_xprod_type thf_xprod_type, +| ( 63, ( ( _, ( MlyValue.thf_xprod_type thf_xprod_type, thf_xprod_type1left, thf_xprod_type1right)) :: rest671)) => let val result = MlyValue.thf_binary_type (( thf_xprod_type )) in ( LrTable.NT 106, ( result, thf_xprod_type1left, thf_xprod_type1right), rest671) end -| ( 62, ( ( _, ( MlyValue.thf_union_type thf_union_type, +| ( 64, ( ( _, ( MlyValue.thf_union_type thf_union_type, thf_union_type1left, thf_union_type1right)) :: rest671)) => let val result = MlyValue.thf_binary_type (( thf_union_type )) in ( LrTable.NT 106, ( result, thf_union_type1left, thf_union_type1right), rest671) end -| ( 63, ( ( _, ( MlyValue.thf_unitary_type thf_unitary_type2, _, +| ( 65, ( ( _, ( MlyValue.thf_unitary_type thf_unitary_type2, _, thf_unitary_type2right)) :: _ :: ( _, ( MlyValue.thf_unitary_type thf_unitary_type1, thf_unitary_type1left, _)) :: rest671)) => let val result = MlyValue.thf_mapping_type ( @@ -4196,7 +4340,7 @@ in ( LrTable.NT 105, ( result, thf_unitary_type1left, thf_unitary_type2right), rest671) end -| ( 64, ( ( _, ( MlyValue.thf_mapping_type thf_mapping_type, _, +| ( 66, ( ( _, ( MlyValue.thf_mapping_type thf_mapping_type, _, thf_mapping_type1right)) :: _ :: ( _, ( MlyValue.thf_unitary_type thf_unitary_type, thf_unitary_type1left, _)) :: rest671)) => let val result = MlyValue.thf_mapping_type ( @@ -4204,7 +4348,7 @@ in ( LrTable.NT 105, ( result, thf_unitary_type1left, thf_mapping_type1right), rest671) end -| ( 65, ( ( _, ( MlyValue.thf_unitary_type thf_unitary_type2, _, +| ( 67, ( ( _, ( MlyValue.thf_unitary_type thf_unitary_type2, _, thf_unitary_type2right)) :: _ :: ( _, ( MlyValue.thf_unitary_type thf_unitary_type1, thf_unitary_type1left, _)) :: rest671)) => let val result = MlyValue.thf_xprod_type ( @@ -4212,7 +4356,7 @@ in ( LrTable.NT 104, ( result, thf_unitary_type1left, thf_unitary_type2right), rest671) end -| ( 66, ( ( _, ( MlyValue.thf_unitary_type thf_unitary_type, _, +| ( 68, ( ( _, ( MlyValue.thf_unitary_type thf_unitary_type, _, thf_unitary_type1right)) :: _ :: ( _, ( MlyValue.thf_xprod_type thf_xprod_type, thf_xprod_type1left, _)) :: rest671)) => let val result = MlyValue.thf_xprod_type ( @@ -4220,7 +4364,7 @@ in ( LrTable.NT 104, ( result, thf_xprod_type1left, thf_unitary_type1right), rest671) end -| ( 67, ( ( _, ( MlyValue.thf_unitary_type thf_unitary_type2, _, +| ( 69, ( ( _, ( MlyValue.thf_unitary_type thf_unitary_type2, _, thf_unitary_type2right)) :: _ :: ( _, ( MlyValue.thf_unitary_type thf_unitary_type1, thf_unitary_type1left, _)) :: rest671)) => let val result = MlyValue.thf_union_type ( @@ -4228,7 +4372,7 @@ in ( LrTable.NT 103, ( result, thf_unitary_type1left, thf_unitary_type2right), rest671) end -| ( 68, ( ( _, ( MlyValue.thf_unitary_type thf_unitary_type, _, +| ( 70, ( ( _, ( MlyValue.thf_unitary_type thf_unitary_type, _, thf_unitary_type1right)) :: _ :: ( _, ( MlyValue.thf_union_type thf_union_type, thf_union_type1left, _)) :: rest671)) => let val result = MlyValue.thf_union_type ( @@ -4236,36 +4380,36 @@ in ( LrTable.NT 103, ( result, thf_union_type1left, thf_unitary_type1right), rest671) end -| ( 69, ( ( _, ( MlyValue.thf_tuple thf_tuple2, _, thf_tuple2right)) +| ( 71, ( ( _, ( MlyValue.thf_tuple thf_tuple2, _, thf_tuple2right)) :: _ :: ( _, ( MlyValue.thf_tuple thf_tuple1, thf_tuple1left, _)) :: rest671)) => let val result = MlyValue.thf_sequent ( ( Sequent(thf_tuple1, thf_tuple2) )) in ( LrTable.NT 99, ( result, thf_tuple1left, thf_tuple2right), rest671) end -| ( 70, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.thf_sequent +| ( 72, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.thf_sequent thf_sequent, _, _)) :: ( _, ( _, LPAREN1left, _)) :: rest671)) => let val result = MlyValue.thf_sequent (( thf_sequent )) in ( LrTable.NT 99, ( result, LPAREN1left, RPAREN1right), rest671) end -| ( 71, ( ( _, ( _, _, RBRKT1right)) :: ( _, ( _, LBRKT1left, _)) :: +| ( 73, ( ( _, ( _, _, RBRKT1right)) :: ( _, ( _, LBRKT1left, _)) :: rest671)) => let val result = MlyValue.thf_tuple (( [] )) in ( LrTable.NT 97, ( result, LBRKT1left, RBRKT1right), rest671) end -| ( 72, ( ( _, ( _, _, RBRKT1right)) :: ( _, ( +| ( 74, ( ( _, ( _, _, RBRKT1right)) :: ( _, ( MlyValue.thf_tuple_list thf_tuple_list, _, _)) :: ( _, ( _, LBRKT1left , _)) :: rest671)) => let val result = MlyValue.thf_tuple ( ( thf_tuple_list )) in ( LrTable.NT 97, ( result, LBRKT1left, RBRKT1right), rest671) end -| ( 73, ( ( _, ( MlyValue.thf_logic_formula thf_logic_formula, +| ( 75, ( ( _, ( MlyValue.thf_logic_formula thf_logic_formula, thf_logic_formula1left, thf_logic_formula1right)) :: rest671)) => let val result = MlyValue.thf_tuple_list (( [thf_logic_formula] )) in ( LrTable.NT 98, ( result, thf_logic_formula1left, thf_logic_formula1right), rest671) end -| ( 74, ( ( _, ( MlyValue.thf_tuple_list thf_tuple_list, _, +| ( 76, ( ( _, ( MlyValue.thf_tuple_list thf_tuple_list, _, thf_tuple_list1right)) :: _ :: ( _, ( MlyValue.thf_logic_formula thf_logic_formula, thf_logic_formula1left, _)) :: rest671)) => let val result = MlyValue.thf_tuple_list ( @@ -4273,52 +4417,52 @@ in ( LrTable.NT 98, ( result, thf_logic_formula1left, thf_tuple_list1right), rest671) end -| ( 75, ( ( _, ( MlyValue.tff_logic_formula tff_logic_formula, +| ( 77, ( ( _, ( MlyValue.tff_logic_formula tff_logic_formula, tff_logic_formula1left, tff_logic_formula1right)) :: rest671)) => let val result = MlyValue.tff_formula (( tff_logic_formula )) in ( LrTable.NT 96, ( result, tff_logic_formula1left, tff_logic_formula1right), rest671) end -| ( 76, ( ( _, ( MlyValue.tff_typed_atom tff_typed_atom, +| ( 78, ( ( _, ( MlyValue.tff_typed_atom tff_typed_atom, tff_typed_atom1left, tff_typed_atom1right)) :: rest671)) => let val result = MlyValue.tff_formula ( ( Atom (TFF_Typed_Atom tff_typed_atom) )) in ( LrTable.NT 96, ( result, tff_typed_atom1left, tff_typed_atom1right), rest671) end -| ( 77, ( ( _, ( MlyValue.tff_sequent tff_sequent, tff_sequent1left, +| ( 79, ( ( _, ( MlyValue.tff_sequent tff_sequent, tff_sequent1left, tff_sequent1right)) :: rest671)) => let val result = MlyValue.tff_formula (( tff_sequent )) in ( LrTable.NT 96, ( result, tff_sequent1left, tff_sequent1right), rest671) end -| ( 78, ( ( _, ( MlyValue.tff_binary_formula tff_binary_formula, +| ( 80, ( ( _, ( MlyValue.tff_binary_formula tff_binary_formula, tff_binary_formula1left, tff_binary_formula1right)) :: rest671)) => let val result = MlyValue.tff_logic_formula (( tff_binary_formula )) in ( LrTable.NT 95, ( result, tff_binary_formula1left, tff_binary_formula1right), rest671) end -| ( 79, ( ( _, ( MlyValue.tff_unitary_formula tff_unitary_formula, +| ( 81, ( ( _, ( MlyValue.tff_unitary_formula tff_unitary_formula, tff_unitary_formula1left, tff_unitary_formula1right)) :: rest671)) => let val result = MlyValue.tff_logic_formula (( tff_unitary_formula ) ) in ( LrTable.NT 95, ( result, tff_unitary_formula1left, tff_unitary_formula1right), rest671) end -| ( 80, ( ( _, ( MlyValue.tff_binary_nonassoc tff_binary_nonassoc, +| ( 82, ( ( _, ( MlyValue.tff_binary_nonassoc tff_binary_nonassoc, tff_binary_nonassoc1left, tff_binary_nonassoc1right)) :: rest671)) => let val result = MlyValue.tff_binary_formula ( ( tff_binary_nonassoc )) in ( LrTable.NT 94, ( result, tff_binary_nonassoc1left, tff_binary_nonassoc1right), rest671) end -| ( 81, ( ( _, ( MlyValue.tff_binary_assoc tff_binary_assoc, +| ( 83, ( ( _, ( MlyValue.tff_binary_assoc tff_binary_assoc, tff_binary_assoc1left, tff_binary_assoc1right)) :: rest671)) => let val result = MlyValue.tff_binary_formula (( tff_binary_assoc )) in ( LrTable.NT 94, ( result, tff_binary_assoc1left, tff_binary_assoc1right), rest671) end -| ( 82, ( ( _, ( MlyValue.tff_unitary_formula tff_unitary_formula2, _ +| ( 84, ( ( _, ( MlyValue.tff_unitary_formula tff_unitary_formula2, _ , tff_unitary_formula2right)) :: ( _, ( MlyValue.binary_connective binary_connective, _, _)) :: ( _, ( MlyValue.tff_unitary_formula tff_unitary_formula1, tff_unitary_formula1left, _)) :: rest671)) => @@ -4328,19 +4472,19 @@ in ( LrTable.NT 93, ( result, tff_unitary_formula1left, tff_unitary_formula2right), rest671) end -| ( 83, ( ( _, ( MlyValue.tff_or_formula tff_or_formula, +| ( 85, ( ( _, ( MlyValue.tff_or_formula tff_or_formula, tff_or_formula1left, tff_or_formula1right)) :: rest671)) => let val result = MlyValue.tff_binary_assoc (( tff_or_formula )) in ( LrTable.NT 92, ( result, tff_or_formula1left, tff_or_formula1right), rest671) end -| ( 84, ( ( _, ( MlyValue.tff_and_formula tff_and_formula, +| ( 86, ( ( _, ( MlyValue.tff_and_formula tff_and_formula, tff_and_formula1left, tff_and_formula1right)) :: rest671)) => let val result = MlyValue.tff_binary_assoc (( tff_and_formula )) in ( LrTable.NT 92, ( result, tff_and_formula1left, tff_and_formula1right), rest671) end -| ( 85, ( ( _, ( MlyValue.tff_unitary_formula tff_unitary_formula2, _ +| ( 87, ( ( _, ( MlyValue.tff_unitary_formula tff_unitary_formula2, _ , tff_unitary_formula2right)) :: _ :: ( _, ( MlyValue.tff_unitary_formula tff_unitary_formula1, tff_unitary_formula1left, _)) :: rest671)) => let val result = @@ -4350,7 +4494,7 @@ in ( LrTable.NT 91, ( result, tff_unitary_formula1left, tff_unitary_formula2right), rest671) end -| ( 86, ( ( _, ( MlyValue.tff_unitary_formula tff_unitary_formula, _, +| ( 88, ( ( _, ( MlyValue.tff_unitary_formula tff_unitary_formula, _, tff_unitary_formula1right)) :: _ :: ( _, ( MlyValue.tff_or_formula tff_or_formula, tff_or_formula1left, _)) :: rest671)) => let val result = MlyValue.tff_or_formula ( @@ -4359,7 +4503,7 @@ in ( LrTable.NT 91, ( result, tff_or_formula1left, tff_unitary_formula1right), rest671) end -| ( 87, ( ( _, ( MlyValue.tff_unitary_formula tff_unitary_formula2, _ +| ( 89, ( ( _, ( MlyValue.tff_unitary_formula tff_unitary_formula2, _ , tff_unitary_formula2right)) :: _ :: ( _, ( MlyValue.tff_unitary_formula tff_unitary_formula1, tff_unitary_formula1left, _)) :: rest671)) => let val result = @@ -4369,7 +4513,7 @@ in ( LrTable.NT 90, ( result, tff_unitary_formula1left, tff_unitary_formula2right), rest671) end -| ( 88, ( ( _, ( MlyValue.tff_unitary_formula tff_unitary_formula, _, +| ( 90, ( ( _, ( MlyValue.tff_unitary_formula tff_unitary_formula, _, tff_unitary_formula1right)) :: _ :: ( _, ( MlyValue.tff_and_formula tff_and_formula, tff_and_formula1left, _)) :: rest671)) => let val result = MlyValue.tff_and_formula ( @@ -4378,45 +4522,45 @@ in ( LrTable.NT 90, ( result, tff_and_formula1left, tff_unitary_formula1right), rest671) end -| ( 89, ( ( _, ( MlyValue.tff_quantified_formula +| ( 91, ( ( _, ( MlyValue.tff_quantified_formula tff_quantified_formula, tff_quantified_formula1left, tff_quantified_formula1right)) :: rest671)) => let val result = MlyValue.tff_unitary_formula (( tff_quantified_formula )) in ( LrTable.NT 89, ( result, tff_quantified_formula1left, tff_quantified_formula1right), rest671) end -| ( 90, ( ( _, ( MlyValue.tff_unary_formula tff_unary_formula, +| ( 92, ( ( _, ( MlyValue.tff_unary_formula tff_unary_formula, tff_unary_formula1left, tff_unary_formula1right)) :: rest671)) => let val result = MlyValue.tff_unitary_formula (( tff_unary_formula )) in ( LrTable.NT 89, ( result, tff_unary_formula1left, tff_unary_formula1right), rest671) end -| ( 91, ( ( _, ( MlyValue.atomic_formula atomic_formula, +| ( 93, ( ( _, ( MlyValue.atomic_formula atomic_formula, atomic_formula1left, atomic_formula1right)) :: rest671)) => let val result = MlyValue.tff_unitary_formula (( atomic_formula )) in ( LrTable.NT 89, ( result, atomic_formula1left, atomic_formula1right), rest671) end -| ( 92, ( ( _, ( MlyValue.tff_conditional tff_conditional, +| ( 94, ( ( _, ( MlyValue.tff_conditional tff_conditional, tff_conditional1left, tff_conditional1right)) :: rest671)) => let val result = MlyValue.tff_unitary_formula (( tff_conditional )) in ( LrTable.NT 89, ( result, tff_conditional1left, tff_conditional1right), rest671) end -| ( 93, ( ( _, ( MlyValue.tff_let tff_let, tff_let1left, +| ( 95, ( ( _, ( MlyValue.tff_let tff_let, tff_let1left, tff_let1right)) :: rest671)) => let val result = MlyValue.tff_unitary_formula (( tff_let )) in ( LrTable.NT 89, ( result, tff_let1left, tff_let1right), rest671) end -| ( 94, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( +| ( 96, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.tff_logic_formula tff_logic_formula, _, _)) :: ( _, ( _, LPAREN1left, _)) :: rest671)) => let val result = MlyValue.tff_unitary_formula (( tff_logic_formula )) in ( LrTable.NT 89, ( result, LPAREN1left, RPAREN1right), rest671) end -| ( 95, ( ( _, ( MlyValue.tff_unitary_formula tff_unitary_formula, _, +| ( 97, ( ( _, ( MlyValue.tff_unitary_formula tff_unitary_formula, _, tff_unitary_formula1right)) :: _ :: _ :: ( _, ( MlyValue.tff_variable_list tff_variable_list, _, _)) :: _ :: ( _, ( MlyValue.fol_quantifier fol_quantifier, fol_quantifier1left, _)) :: @@ -4427,39 +4571,39 @@ in ( LrTable.NT 88, ( result, fol_quantifier1left, tff_unitary_formula1right), rest671) end -| ( 96, ( ( _, ( MlyValue.tff_variable tff_variable, +| ( 98, ( ( _, ( MlyValue.tff_variable tff_variable, tff_variable1left, tff_variable1right)) :: rest671)) => let val result = MlyValue.tff_variable_list (( [tff_variable] )) in ( LrTable.NT 87, ( result, tff_variable1left, tff_variable1right), rest671) end -| ( 97, ( ( _, ( MlyValue.tff_variable_list tff_variable_list, _, +| ( 99, ( ( _, ( MlyValue.tff_variable_list tff_variable_list, _, tff_variable_list1right)) :: _ :: ( _, ( MlyValue.tff_variable tff_variable, tff_variable1left, _)) :: rest671)) => let val result = MlyValue.tff_variable_list (( tff_variable :: tff_variable_list )) in ( LrTable.NT 87, ( result, tff_variable1left, tff_variable_list1right), rest671) end -| ( 98, ( ( _, ( MlyValue.tff_typed_variable tff_typed_variable, +| ( 100, ( ( _, ( MlyValue.tff_typed_variable tff_typed_variable, tff_typed_variable1left, tff_typed_variable1right)) :: rest671)) => let val result = MlyValue.tff_variable (( tff_typed_variable )) in ( LrTable.NT 86, ( result, tff_typed_variable1left, tff_typed_variable1right), rest671) end -| ( 99, ( ( _, ( MlyValue.variable_ variable_, variable_1left, +| ( 101, ( ( _, ( MlyValue.variable_ variable_, variable_1left, variable_1right)) :: rest671)) => let val result = MlyValue.tff_variable (( (variable_, NONE) )) in ( LrTable.NT 86, ( result, variable_1left, variable_1right), rest671) end -| ( 100, ( ( _, ( MlyValue.tff_atomic_type tff_atomic_type, _, +| ( 102, ( ( _, ( MlyValue.tff_atomic_type tff_atomic_type, _, tff_atomic_type1right)) :: _ :: ( _, ( MlyValue.variable_ variable_, variable_1left, _)) :: rest671)) => let val result = MlyValue.tff_typed_variable (( (variable_, SOME tff_atomic_type) )) in ( LrTable.NT 85, ( result, variable_1left, tff_atomic_type1right), rest671) end -| ( 101, ( ( _, ( MlyValue.tff_unitary_formula tff_unitary_formula, _ +| ( 103, ( ( _, ( MlyValue.tff_unitary_formula tff_unitary_formula, _ , tff_unitary_formula1right)) :: ( _, ( MlyValue.unary_connective unary_connective, unary_connective1left, _)) :: rest671)) => let val result = MlyValue.tff_unary_formula ( @@ -4467,13 +4611,13 @@ in ( LrTable.NT 84, ( result, unary_connective1left, tff_unitary_formula1right), rest671) end -| ( 102, ( ( _, ( MlyValue.fol_infix_unary fol_infix_unary, +| ( 104, ( ( _, ( MlyValue.fol_infix_unary fol_infix_unary, fol_infix_unary1left, fol_infix_unary1right)) :: rest671)) => let val result = MlyValue.tff_unary_formula (( fol_infix_unary )) in ( LrTable.NT 84, ( result, fol_infix_unary1left, fol_infix_unary1right), rest671) end -| ( 103, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( +| ( 105, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.tff_logic_formula tff_logic_formula3, _, _)) :: _ :: ( _, ( MlyValue.tff_logic_formula tff_logic_formula2, _, _)) :: _ :: ( _, ( MlyValue.tff_logic_formula tff_logic_formula1, _, _)) :: _ :: ( _, ( _ @@ -4485,74 +4629,98 @@ ) in ( LrTable.NT 76, ( result, ITE_F1left, RPAREN1right), rest671) end -| ( 104, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.tff_formula +| ( 106, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.tff_formula tff_formula, _, _)) :: _ :: ( _, ( MlyValue.tff_let_term_defn tff_let_term_defn, _, _)) :: _ :: ( _, ( _, LET_TF1left, _)) :: rest671)) => let val result = MlyValue.tff_let ( (Let (tff_let_term_defn, tff_formula) )) - in ( LrTable.NT 137, ( result, LET_TF1left, RPAREN1right), rest671) + in ( LrTable.NT 138, ( result, LET_TF1left, RPAREN1right), rest671) end -| ( 105, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.tff_formula +| ( 107, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.tff_formula tff_formula, _, _)) :: _ :: ( _, ( MlyValue.tff_let_formula_defn tff_let_formula_defn, _, _)) :: _ :: ( _, ( _, LET_FF1left, _)) :: rest671)) => let val result = MlyValue.tff_let ( ( Let (tff_let_formula_defn, tff_formula) )) - in ( LrTable.NT 137, ( result, LET_FF1left, RPAREN1right), rest671) + in ( LrTable.NT 138, ( result, LET_FF1left, RPAREN1right), rest671) end -| ( 106, ( ( _, ( MlyValue.tff_quantified_formula -tff_quantified_formula, tff_quantified_formula1left, -tff_quantified_formula1right)) :: rest671)) => let val result = +| ( 108, ( ( _, ( MlyValue.tff_let_term_binding tff_let_term_binding, + _, tff_let_term_binding1right)) :: _ :: _ :: ( _, ( +MlyValue.tff_variable_list tff_variable_list, _, _)) :: _ :: ( _, ( _, + EXCLAMATION1left, _)) :: rest671)) => let val result = MlyValue.tff_let_term_defn ( +( Let_term (tff_variable_list, tff_let_term_binding) )) + in ( LrTable.NT 139, ( result, EXCLAMATION1left, +tff_let_term_binding1right), rest671) +end +| ( 109, ( ( _, ( MlyValue.tff_let_term_binding tff_let_term_binding, + tff_let_term_binding1left, tff_let_term_binding1right)) :: rest671)) + => let val result = MlyValue.tff_let_term_defn ( +( Let_term ([], tff_let_term_binding) )) + in ( LrTable.NT 139, ( result, tff_let_term_binding1left, +tff_let_term_binding1right), rest671) +end +| ( 110, ( ( _, ( MlyValue.term term2, _, term2right)) :: _ :: ( _, ( + MlyValue.term term1, term1left, _)) :: rest671)) => let val result = + MlyValue.tff_let_term_binding ( ( - let - val (_, vars, fmla) = extract_quant_info tff_quantified_formula - in [Let_fmla (hd vars, fmla)] - end + Term_Func (Interpreted_ExtraLogic Apply, [term1, term2]) +)) + in ( LrTable.NT 140, ( result, term1left, term2right), rest671) +end +| ( 111, ( ( _, ( MlyValue.tff_let_formula_binding +tff_let_formula_binding, _, tff_let_formula_binding1right)) :: _ :: _ + :: ( _, ( MlyValue.tff_variable_list tff_variable_list, _, _)) :: _ + :: ( _, ( _, EXCLAMATION1left, _)) :: rest671)) => let val result = +MlyValue.tff_let_formula_defn ( +( Let_fmla (tff_variable_list, tff_let_formula_binding) )) + in ( LrTable.NT 141, ( result, EXCLAMATION1left, +tff_let_formula_binding1right), rest671) +end +| ( 112, ( ( _, ( MlyValue.tff_let_formula_binding +tff_let_formula_binding, tff_let_formula_binding1left, +tff_let_formula_binding1right)) :: rest671)) => let val result = +MlyValue.tff_let_formula_defn ( +( Let_fmla ([], tff_let_formula_binding) )) + in ( LrTable.NT 141, ( result, tff_let_formula_binding1left, +tff_let_formula_binding1right), rest671) +end +| ( 113, ( ( _, ( MlyValue.tff_unitary_formula tff_unitary_formula, _ +, tff_unitary_formula1right)) :: _ :: ( _, ( MlyValue.atomic_formula +atomic_formula, atomic_formula1left, _)) :: rest671)) => let val +result = MlyValue.tff_let_formula_binding ( +( + Fmla (Interpreted_Logic Iff, [atomic_formula, tff_unitary_formula]) ) ) - in ( LrTable.NT 138, ( result, tff_quantified_formula1left, -tff_quantified_formula1right), rest671) -end -| ( 107, ( ( _, ( MlyValue.tff_quantified_formula -tff_quantified_formula, tff_quantified_formula1left, -tff_quantified_formula1right)) :: rest671)) => let val result = -MlyValue.tff_let_formula_defn ( -( - let - val (_, vars, fmla) = extract_quant_info tff_quantified_formula - in [Let_fmla (hd vars, fmla)] - end -) -) - in ( LrTable.NT 139, ( result, tff_quantified_formula1left, -tff_quantified_formula1right), rest671) -end -| ( 108, ( ( _, ( MlyValue.tff_tuple tff_tuple2, _, tff_tuple2right)) + in ( LrTable.NT 142, ( result, atomic_formula1left, +tff_unitary_formula1right), rest671) +end +| ( 114, ( ( _, ( MlyValue.tff_tuple tff_tuple2, _, tff_tuple2right)) :: _ :: ( _, ( MlyValue.tff_tuple tff_tuple1, tff_tuple1left, _)) :: rest671)) => let val result = MlyValue.tff_sequent ( ( Sequent (tff_tuple1, tff_tuple2) )) in ( LrTable.NT 75, ( result, tff_tuple1left, tff_tuple2right), rest671) end -| ( 109, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.tff_sequent +| ( 115, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.tff_sequent tff_sequent, _, _)) :: ( _, ( _, LPAREN1left, _)) :: rest671)) => let val result = MlyValue.tff_sequent (( tff_sequent )) in ( LrTable.NT 75, ( result, LPAREN1left, RPAREN1right), rest671) end -| ( 110, ( ( _, ( _, _, RBRKT1right)) :: ( _, ( _, LBRKT1left, _)) :: +| ( 116, ( ( _, ( _, _, RBRKT1right)) :: ( _, ( _, LBRKT1left, _)) :: rest671)) => let val result = MlyValue.tff_tuple (( [] )) in ( LrTable.NT 73, ( result, LBRKT1left, RBRKT1right), rest671) end -| ( 111, ( ( _, ( _, _, RBRKT1right)) :: ( _, ( +| ( 117, ( ( _, ( _, _, RBRKT1right)) :: ( _, ( MlyValue.tff_tuple_list tff_tuple_list, _, _)) :: ( _, ( _, LBRKT1left , _)) :: rest671)) => let val result = MlyValue.tff_tuple ( ( tff_tuple_list )) in ( LrTable.NT 73, ( result, LBRKT1left, RBRKT1right), rest671) end -| ( 112, ( ( _, ( MlyValue.tff_tuple_list tff_tuple_list, _, +| ( 118, ( ( _, ( MlyValue.tff_tuple_list tff_tuple_list, _, tff_tuple_list1right)) :: _ :: ( _, ( MlyValue.tff_logic_formula tff_logic_formula, tff_logic_formula1left, _)) :: rest671)) => let val result = MlyValue.tff_tuple_list ( @@ -4560,13 +4728,13 @@ in ( LrTable.NT 74, ( result, tff_logic_formula1left, tff_tuple_list1right), rest671) end -| ( 113, ( ( _, ( MlyValue.tff_logic_formula tff_logic_formula, +| ( 119, ( ( _, ( MlyValue.tff_logic_formula tff_logic_formula, tff_logic_formula1left, tff_logic_formula1right)) :: rest671)) => let val result = MlyValue.tff_tuple_list (( [tff_logic_formula] )) in ( LrTable.NT 74, ( result, tff_logic_formula1left, tff_logic_formula1right), rest671) end -| ( 114, ( ( _, ( MlyValue.tff_top_level_type tff_top_level_type, _, +| ( 120, ( ( _, ( MlyValue.tff_top_level_type tff_top_level_type, _, tff_top_level_type1right)) :: _ :: ( _, ( MlyValue.tff_untyped_atom tff_untyped_atom, tff_untyped_atom1left, _)) :: rest671)) => let val result = MlyValue.tff_typed_atom ( @@ -4574,45 +4742,45 @@ in ( LrTable.NT 83, ( result, tff_untyped_atom1left, tff_top_level_type1right), rest671) end -| ( 115, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( +| ( 121, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.tff_typed_atom tff_typed_atom, _, _)) :: ( _, ( _, LPAREN1left, _)) :: rest671)) => let val result = MlyValue.tff_typed_atom (( tff_typed_atom )) in ( LrTable.NT 83, ( result, LPAREN1left, RPAREN1right), rest671) end -| ( 116, ( ( _, ( MlyValue.functor_ functor_, functor_1left, +| ( 122, ( ( _, ( MlyValue.functor_ functor_, functor_1left, functor_1right)) :: rest671)) => let val result = MlyValue.tff_untyped_atom (( (functor_, NONE) )) in ( LrTable.NT 82, ( result, functor_1left, functor_1right), rest671 ) end -| ( 117, ( ( _, ( MlyValue.system_functor system_functor, +| ( 123, ( ( _, ( MlyValue.system_functor system_functor, system_functor1left, system_functor1right)) :: rest671)) => let val result = MlyValue.tff_untyped_atom (( (system_functor, NONE) )) in ( LrTable.NT 82, ( result, system_functor1left, system_functor1right), rest671) end -| ( 118, ( ( _, ( MlyValue.tff_atomic_type tff_atomic_type, +| ( 124, ( ( _, ( MlyValue.tff_atomic_type tff_atomic_type, tff_atomic_type1left, tff_atomic_type1right)) :: rest671)) => let val result = MlyValue.tff_top_level_type (( tff_atomic_type )) in ( LrTable.NT 81, ( result, tff_atomic_type1left, tff_atomic_type1right), rest671) end -| ( 119, ( ( _, ( MlyValue.tff_mapping_type tff_mapping_type, +| ( 125, ( ( _, ( MlyValue.tff_mapping_type tff_mapping_type, tff_mapping_type1left, tff_mapping_type1right)) :: rest671)) => let val result = MlyValue.tff_top_level_type (( tff_mapping_type )) in ( LrTable.NT 81, ( result, tff_mapping_type1left, tff_mapping_type1right), rest671) end -| ( 120, ( ( _, ( MlyValue.tff_quantified_type tff_quantified_type, +| ( 126, ( ( _, ( MlyValue.tff_quantified_type tff_quantified_type, tff_quantified_type1left, tff_quantified_type1right)) :: rest671)) => let val result = MlyValue.tff_top_level_type ( ( tff_quantified_type )) in ( LrTable.NT 81, ( result, tff_quantified_type1left, tff_quantified_type1right), rest671) end -| ( 121, ( ( _, ( MlyValue.tff_monotype tff_monotype, _, +| ( 127, ( ( _, ( MlyValue.tff_monotype tff_monotype, _, tff_monotype1right)) :: _ :: _ :: ( _, ( MlyValue.tff_variable_list tff_variable_list, _, _)) :: _ :: ( _, ( _, DEP_PROD1left, _)) :: rest671)) => let val result = MlyValue.tff_quantified_type ( @@ -4620,55 +4788,55 @@ Fmla_type (Quant (Dep_Prod, tff_variable_list, Type_fmla tff_monotype)) ) ) - in ( LrTable.NT 140, ( result, DEP_PROD1left, tff_monotype1right), + in ( LrTable.NT 143, ( result, DEP_PROD1left, tff_monotype1right), rest671) end -| ( 122, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( +| ( 128, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.tff_quantified_type tff_quantified_type, _, _)) :: ( _, ( _, LPAREN1left, _)) :: rest671)) => let val result = MlyValue.tff_quantified_type (( tff_quantified_type )) - in ( LrTable.NT 140, ( result, LPAREN1left, RPAREN1right), rest671) + in ( LrTable.NT 143, ( result, LPAREN1left, RPAREN1right), rest671) end -| ( 123, ( ( _, ( MlyValue.tff_atomic_type tff_atomic_type, +| ( 129, ( ( _, ( MlyValue.tff_atomic_type tff_atomic_type, tff_atomic_type1left, tff_atomic_type1right)) :: rest671)) => let val result = MlyValue.tff_monotype (( tff_atomic_type )) - in ( LrTable.NT 141, ( result, tff_atomic_type1left, + in ( LrTable.NT 144, ( result, tff_atomic_type1left, tff_atomic_type1right), rest671) end -| ( 124, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( +| ( 130, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.tff_mapping_type tff_mapping_type, _, _)) :: ( _, ( _, LPAREN1left, _)) :: rest671)) => let val result = MlyValue.tff_monotype (( tff_mapping_type )) - in ( LrTable.NT 141, ( result, LPAREN1left, RPAREN1right), rest671) + in ( LrTable.NT 144, ( result, LPAREN1left, RPAREN1right), rest671) end -| ( 125, ( ( _, ( MlyValue.tff_atomic_type tff_atomic_type, +| ( 131, ( ( _, ( MlyValue.tff_atomic_type tff_atomic_type, tff_atomic_type1left, tff_atomic_type1right)) :: rest671)) => let val result = MlyValue.tff_unitary_type (( tff_atomic_type )) in ( LrTable.NT 80, ( result, tff_atomic_type1left, tff_atomic_type1right), rest671) end -| ( 126, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( +| ( 132, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.tff_xprod_type tff_xprod_type, _, _)) :: ( _, ( _, LPAREN1left, _)) :: rest671)) => let val result = MlyValue.tff_unitary_type (( tff_xprod_type )) in ( LrTable.NT 80, ( result, LPAREN1left, RPAREN1right), rest671) end -| ( 127, ( ( _, ( MlyValue.atomic_word atomic_word, atomic_word1left, +| ( 133, ( ( _, ( MlyValue.atomic_word atomic_word, atomic_word1left, atomic_word1right)) :: rest671)) => let val result = MlyValue.tff_atomic_type (( Atom_type atomic_word )) in ( LrTable.NT 79, ( result, atomic_word1left, atomic_word1right), rest671) end -| ( 128, ( ( _, ( MlyValue.defined_type defined_type, +| ( 134, ( ( _, ( MlyValue.defined_type defined_type, defined_type1left, defined_type1right)) :: rest671)) => let val result = MlyValue.tff_atomic_type (( Defined_type defined_type )) in ( LrTable.NT 79, ( result, defined_type1left, defined_type1right), rest671) end -| ( 129, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( +| ( 135, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.tff_type_arguments tff_type_arguments, _, _)) :: _ :: ( _, ( MlyValue.atomic_word atomic_word, atomic_word1left, _)) :: rest671)) => let val result = MlyValue.tff_atomic_type ( @@ -4677,7 +4845,7 @@ in ( LrTable.NT 79, ( result, atomic_word1left, RPAREN1right), rest671) end -| ( 130, ( ( _, ( MlyValue.variable_ variable_, variable_1left, +| ( 136, ( ( _, ( MlyValue.variable_ variable_, variable_1left, variable_1right)) :: rest671)) => let val result = MlyValue.tff_atomic_type ( ( Fmla_type (Pred (Interpreted_ExtraLogic Apply, [Term_Var variable_])) ) @@ -4685,21 +4853,21 @@ in ( LrTable.NT 79, ( result, variable_1left, variable_1right), rest671) end -| ( 131, ( ( _, ( MlyValue.tff_atomic_type tff_atomic_type, +| ( 137, ( ( _, ( MlyValue.tff_atomic_type tff_atomic_type, tff_atomic_type1left, tff_atomic_type1right)) :: rest671)) => let val result = MlyValue.tff_type_arguments (( [tff_atomic_type] )) - in ( LrTable.NT 142, ( result, tff_atomic_type1left, + in ( LrTable.NT 145, ( result, tff_atomic_type1left, tff_atomic_type1right), rest671) end -| ( 132, ( ( _, ( MlyValue.tff_type_arguments tff_type_arguments, _, +| ( 138, ( ( _, ( MlyValue.tff_type_arguments tff_type_arguments, _, tff_type_arguments1right)) :: _ :: ( _, ( MlyValue.tff_atomic_type tff_atomic_type, tff_atomic_type1left, _)) :: rest671)) => let val result = MlyValue.tff_type_arguments ( ( tff_atomic_type :: tff_type_arguments )) - in ( LrTable.NT 142, ( result, tff_atomic_type1left, + in ( LrTable.NT 145, ( result, tff_atomic_type1left, tff_type_arguments1right), rest671) end -| ( 133, ( ( _, ( MlyValue.tff_atomic_type tff_atomic_type, _, +| ( 139, ( ( _, ( MlyValue.tff_atomic_type tff_atomic_type, _, tff_atomic_type1right)) :: _ :: ( _, ( MlyValue.tff_unitary_type tff_unitary_type, tff_unitary_type1left, _)) :: rest671)) => let val result = MlyValue.tff_mapping_type ( @@ -4707,14 +4875,14 @@ in ( LrTable.NT 78, ( result, tff_unitary_type1left, tff_atomic_type1right), rest671) end -| ( 134, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( +| ( 140, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.tff_mapping_type tff_mapping_type, _, _)) :: ( _, ( _, LPAREN1left, _)) :: rest671)) => let val result = MlyValue.tff_mapping_type (( tff_mapping_type )) in ( LrTable.NT 78, ( result, LPAREN1left, RPAREN1right), rest671) end -| ( 135, ( ( _, ( MlyValue.tff_atomic_type tff_atomic_type2, _, +| ( 141, ( ( _, ( MlyValue.tff_atomic_type tff_atomic_type2, _, tff_atomic_type2right)) :: _ :: ( _, ( MlyValue.tff_atomic_type tff_atomic_type1, tff_atomic_type1left, _)) :: rest671)) => let val result = MlyValue.tff_xprod_type ( @@ -4722,7 +4890,7 @@ in ( LrTable.NT 77, ( result, tff_atomic_type1left, tff_atomic_type2right), rest671) end -| ( 136, ( ( _, ( MlyValue.tff_atomic_type tff_atomic_type, _, +| ( 142, ( ( _, ( MlyValue.tff_atomic_type tff_atomic_type, _, tff_atomic_type1right)) :: _ :: ( _, ( MlyValue.tff_xprod_type tff_xprod_type, tff_xprod_type1left, _)) :: rest671)) => let val result = MlyValue.tff_xprod_type ( @@ -4730,52 +4898,52 @@ in ( LrTable.NT 77, ( result, tff_xprod_type1left, tff_atomic_type1right), rest671) end -| ( 137, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( +| ( 143, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.tff_xprod_type tff_xprod_type, _, _)) :: ( _, ( _, LPAREN1left, _)) :: rest671)) => let val result = MlyValue.tff_xprod_type (( tff_xprod_type )) in ( LrTable.NT 77, ( result, LPAREN1left, RPAREN1right), rest671) end -| ( 138, ( ( _, ( MlyValue.fof_logic_formula fof_logic_formula, +| ( 144, ( ( _, ( MlyValue.fof_logic_formula fof_logic_formula, fof_logic_formula1left, fof_logic_formula1right)) :: rest671)) => let val result = MlyValue.fof_formula (( fof_logic_formula )) in ( LrTable.NT 72, ( result, fof_logic_formula1left, fof_logic_formula1right), rest671) end -| ( 139, ( ( _, ( MlyValue.fof_sequent fof_sequent, fof_sequent1left, +| ( 145, ( ( _, ( MlyValue.fof_sequent fof_sequent, fof_sequent1left, fof_sequent1right)) :: rest671)) => let val result = MlyValue.fof_formula (( fof_sequent )) in ( LrTable.NT 72, ( result, fof_sequent1left, fof_sequent1right), rest671) end -| ( 140, ( ( _, ( MlyValue.fof_binary_formula fof_binary_formula, +| ( 146, ( ( _, ( MlyValue.fof_binary_formula fof_binary_formula, fof_binary_formula1left, fof_binary_formula1right)) :: rest671)) => let val result = MlyValue.fof_logic_formula (( fof_binary_formula )) in ( LrTable.NT 71, ( result, fof_binary_formula1left, fof_binary_formula1right), rest671) end -| ( 141, ( ( _, ( MlyValue.fof_unitary_formula fof_unitary_formula, +| ( 147, ( ( _, ( MlyValue.fof_unitary_formula fof_unitary_formula, fof_unitary_formula1left, fof_unitary_formula1right)) :: rest671)) => let val result = MlyValue.fof_logic_formula (( fof_unitary_formula ) ) in ( LrTable.NT 71, ( result, fof_unitary_formula1left, fof_unitary_formula1right), rest671) end -| ( 142, ( ( _, ( MlyValue.fof_binary_nonassoc fof_binary_nonassoc, +| ( 148, ( ( _, ( MlyValue.fof_binary_nonassoc fof_binary_nonassoc, fof_binary_nonassoc1left, fof_binary_nonassoc1right)) :: rest671)) => let val result = MlyValue.fof_binary_formula ( ( fof_binary_nonassoc )) in ( LrTable.NT 70, ( result, fof_binary_nonassoc1left, fof_binary_nonassoc1right), rest671) end -| ( 143, ( ( _, ( MlyValue.fof_binary_assoc fof_binary_assoc, +| ( 149, ( ( _, ( MlyValue.fof_binary_assoc fof_binary_assoc, fof_binary_assoc1left, fof_binary_assoc1right)) :: rest671)) => let val result = MlyValue.fof_binary_formula (( fof_binary_assoc )) in ( LrTable.NT 70, ( result, fof_binary_assoc1left, fof_binary_assoc1right), rest671) end -| ( 144, ( ( _, ( MlyValue.fof_unitary_formula fof_unitary_formula2, +| ( 150, ( ( _, ( MlyValue.fof_unitary_formula fof_unitary_formula2, _, fof_unitary_formula2right)) :: ( _, ( MlyValue.binary_connective binary_connective, _, _)) :: ( _, ( MlyValue.fof_unitary_formula fof_unitary_formula1, fof_unitary_formula1left, _)) :: rest671)) => @@ -4787,19 +4955,19 @@ in ( LrTable.NT 69, ( result, fof_unitary_formula1left, fof_unitary_formula2right), rest671) end -| ( 145, ( ( _, ( MlyValue.fof_or_formula fof_or_formula, +| ( 151, ( ( _, ( MlyValue.fof_or_formula fof_or_formula, fof_or_formula1left, fof_or_formula1right)) :: rest671)) => let val result = MlyValue.fof_binary_assoc (( fof_or_formula )) in ( LrTable.NT 68, ( result, fof_or_formula1left, fof_or_formula1right), rest671) end -| ( 146, ( ( _, ( MlyValue.fof_and_formula fof_and_formula, +| ( 152, ( ( _, ( MlyValue.fof_and_formula fof_and_formula, fof_and_formula1left, fof_and_formula1right)) :: rest671)) => let val result = MlyValue.fof_binary_assoc (( fof_and_formula )) in ( LrTable.NT 68, ( result, fof_and_formula1left, fof_and_formula1right), rest671) end -| ( 147, ( ( _, ( MlyValue.fof_unitary_formula fof_unitary_formula2, +| ( 153, ( ( _, ( MlyValue.fof_unitary_formula fof_unitary_formula2, _, fof_unitary_formula2right)) :: _ :: ( _, ( MlyValue.fof_unitary_formula fof_unitary_formula1, fof_unitary_formula1left, _)) :: rest671)) => let val result = @@ -4809,7 +4977,7 @@ in ( LrTable.NT 67, ( result, fof_unitary_formula1left, fof_unitary_formula2right), rest671) end -| ( 148, ( ( _, ( MlyValue.fof_unitary_formula fof_unitary_formula, _ +| ( 154, ( ( _, ( MlyValue.fof_unitary_formula fof_unitary_formula, _ , fof_unitary_formula1right)) :: _ :: ( _, ( MlyValue.fof_or_formula fof_or_formula, fof_or_formula1left, _)) :: rest671)) => let val result = MlyValue.fof_or_formula ( @@ -4818,7 +4986,7 @@ in ( LrTable.NT 67, ( result, fof_or_formula1left, fof_unitary_formula1right), rest671) end -| ( 149, ( ( _, ( MlyValue.fof_unitary_formula fof_unitary_formula2, +| ( 155, ( ( _, ( MlyValue.fof_unitary_formula fof_unitary_formula2, _, fof_unitary_formula2right)) :: _ :: ( _, ( MlyValue.fof_unitary_formula fof_unitary_formula1, fof_unitary_formula1left, _)) :: rest671)) => let val result = @@ -4828,7 +4996,7 @@ in ( LrTable.NT 66, ( result, fof_unitary_formula1left, fof_unitary_formula2right), rest671) end -| ( 150, ( ( _, ( MlyValue.fof_unitary_formula fof_unitary_formula, _ +| ( 156, ( ( _, ( MlyValue.fof_unitary_formula fof_unitary_formula, _ , fof_unitary_formula1right)) :: _ :: ( _, ( MlyValue.fof_and_formula fof_and_formula, fof_and_formula1left, _)) :: rest671)) => let val result = MlyValue.fof_and_formula ( @@ -4837,33 +5005,33 @@ in ( LrTable.NT 66, ( result, fof_and_formula1left, fof_unitary_formula1right), rest671) end -| ( 151, ( ( _, ( MlyValue.fof_quantified_formula +| ( 157, ( ( _, ( MlyValue.fof_quantified_formula fof_quantified_formula, fof_quantified_formula1left, fof_quantified_formula1right)) :: rest671)) => let val result = MlyValue.fof_unitary_formula (( fof_quantified_formula )) in ( LrTable.NT 65, ( result, fof_quantified_formula1left, fof_quantified_formula1right), rest671) end -| ( 152, ( ( _, ( MlyValue.fof_unary_formula fof_unary_formula, +| ( 158, ( ( _, ( MlyValue.fof_unary_formula fof_unary_formula, fof_unary_formula1left, fof_unary_formula1right)) :: rest671)) => let val result = MlyValue.fof_unitary_formula (( fof_unary_formula )) in ( LrTable.NT 65, ( result, fof_unary_formula1left, fof_unary_formula1right), rest671) end -| ( 153, ( ( _, ( MlyValue.atomic_formula atomic_formula, +| ( 159, ( ( _, ( MlyValue.atomic_formula atomic_formula, atomic_formula1left, atomic_formula1right)) :: rest671)) => let val result = MlyValue.fof_unitary_formula (( atomic_formula )) in ( LrTable.NT 65, ( result, atomic_formula1left, atomic_formula1right), rest671) end -| ( 154, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( +| ( 160, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.fof_logic_formula fof_logic_formula, _, _)) :: ( _, ( _, LPAREN1left, _)) :: rest671)) => let val result = MlyValue.fof_unitary_formula (( fof_logic_formula )) in ( LrTable.NT 65, ( result, LPAREN1left, RPAREN1right), rest671) end -| ( 155, ( ( _, ( MlyValue.fof_unitary_formula fof_unitary_formula, _ +| ( 161, ( ( _, ( MlyValue.fof_unitary_formula fof_unitary_formula, _ , fof_unitary_formula1right)) :: _ :: _ :: ( _, ( MlyValue.fof_variable_list fof_variable_list, _, _)) :: _ :: ( _, ( MlyValue.fol_quantifier fol_quantifier, fol_quantifier1left, _)) :: @@ -4875,20 +5043,20 @@ in ( LrTable.NT 64, ( result, fol_quantifier1left, fof_unitary_formula1right), rest671) end -| ( 156, ( ( _, ( MlyValue.variable_ variable_, variable_1left, +| ( 162, ( ( _, ( MlyValue.variable_ variable_, variable_1left, variable_1right)) :: rest671)) => let val result = MlyValue.fof_variable_list (( [variable_] )) in ( LrTable.NT 63, ( result, variable_1left, variable_1right), rest671) end -| ( 157, ( ( _, ( MlyValue.fof_variable_list fof_variable_list, _, +| ( 163, ( ( _, ( MlyValue.fof_variable_list fof_variable_list, _, fof_variable_list1right)) :: _ :: ( _, ( MlyValue.variable_ variable_, variable_1left, _)) :: rest671)) => let val result = MlyValue.fof_variable_list (( variable_ :: fof_variable_list )) in ( LrTable.NT 63, ( result, variable_1left, fof_variable_list1right ), rest671) end -| ( 158, ( ( _, ( MlyValue.fof_unitary_formula fof_unitary_formula, _ +| ( 164, ( ( _, ( MlyValue.fof_unitary_formula fof_unitary_formula, _ , fof_unitary_formula1right)) :: ( _, ( MlyValue.unary_connective unary_connective, unary_connective1left, _)) :: rest671)) => let val result = MlyValue.fof_unary_formula ( @@ -4896,42 +5064,42 @@ in ( LrTable.NT 62, ( result, unary_connective1left, fof_unitary_formula1right), rest671) end -| ( 159, ( ( _, ( MlyValue.fol_infix_unary fol_infix_unary, +| ( 165, ( ( _, ( MlyValue.fol_infix_unary fol_infix_unary, fol_infix_unary1left, fol_infix_unary1right)) :: rest671)) => let val result = MlyValue.fof_unary_formula (( fol_infix_unary )) in ( LrTable.NT 62, ( result, fol_infix_unary1left, fol_infix_unary1right), rest671) end -| ( 160, ( ( _, ( MlyValue.fof_tuple fof_tuple2, _, fof_tuple2right)) +| ( 166, ( ( _, ( MlyValue.fof_tuple fof_tuple2, _, fof_tuple2right)) :: _ :: ( _, ( MlyValue.fof_tuple fof_tuple1, fof_tuple1left, _)) :: rest671)) => let val result = MlyValue.fof_sequent ( ( Sequent (fof_tuple1, fof_tuple2) )) in ( LrTable.NT 61, ( result, fof_tuple1left, fof_tuple2right), rest671) end -| ( 161, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.fof_sequent +| ( 167, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.fof_sequent fof_sequent, _, _)) :: ( _, ( _, LPAREN1left, _)) :: rest671)) => let val result = MlyValue.fof_sequent (( fof_sequent )) in ( LrTable.NT 61, ( result, LPAREN1left, RPAREN1right), rest671) end -| ( 162, ( ( _, ( _, _, RBRKT1right)) :: ( _, ( _, LBRKT1left, _)) :: +| ( 168, ( ( _, ( _, _, RBRKT1right)) :: ( _, ( _, LBRKT1left, _)) :: rest671)) => let val result = MlyValue.fof_tuple (( [] )) in ( LrTable.NT 60, ( result, LBRKT1left, RBRKT1right), rest671) end -| ( 163, ( ( _, ( _, _, RBRKT1right)) :: ( _, ( +| ( 169, ( ( _, ( _, _, RBRKT1right)) :: ( _, ( MlyValue.fof_tuple_list fof_tuple_list, _, _)) :: ( _, ( _, LBRKT1left , _)) :: rest671)) => let val result = MlyValue.fof_tuple ( ( fof_tuple_list )) in ( LrTable.NT 60, ( result, LBRKT1left, RBRKT1right), rest671) end -| ( 164, ( ( _, ( MlyValue.fof_logic_formula fof_logic_formula, +| ( 170, ( ( _, ( MlyValue.fof_logic_formula fof_logic_formula, fof_logic_formula1left, fof_logic_formula1right)) :: rest671)) => let val result = MlyValue.fof_tuple_list (( [fof_logic_formula] )) in ( LrTable.NT 59, ( result, fof_logic_formula1left, fof_logic_formula1right), rest671) end -| ( 165, ( ( _, ( MlyValue.fof_tuple_list fof_tuple_list, _, +| ( 171, ( ( _, ( MlyValue.fof_tuple_list fof_tuple_list, _, fof_tuple_list1right)) :: _ :: ( _, ( MlyValue.fof_logic_formula fof_logic_formula, fof_logic_formula1left, _)) :: rest671)) => let val result = MlyValue.fof_tuple_list ( @@ -4939,192 +5107,192 @@ in ( LrTable.NT 59, ( result, fof_logic_formula1left, fof_tuple_list1right), rest671) end -| ( 166, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.disjunction +| ( 172, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.disjunction disjunction, _, _)) :: ( _, ( _, LPAREN1left, _)) :: rest671)) => let val result = MlyValue.cnf_formula (( disjunction )) in ( LrTable.NT 58, ( result, LPAREN1left, RPAREN1right), rest671) end -| ( 167, ( ( _, ( MlyValue.disjunction disjunction, disjunction1left, +| ( 173, ( ( _, ( MlyValue.disjunction disjunction, disjunction1left, disjunction1right)) :: rest671)) => let val result = MlyValue.cnf_formula (( disjunction )) in ( LrTable.NT 58, ( result, disjunction1left, disjunction1right), rest671) end -| ( 168, ( ( _, ( MlyValue.literal literal, literal1left, +| ( 174, ( ( _, ( MlyValue.literal literal, literal1left, literal1right)) :: rest671)) => let val result = MlyValue.disjunction (( literal )) in ( LrTable.NT 57, ( result, literal1left, literal1right), rest671) end -| ( 169, ( ( _, ( MlyValue.literal literal, _, literal1right)) :: _ +| ( 175, ( ( _, ( MlyValue.literal literal, _, literal1right)) :: _ :: ( _, ( MlyValue.disjunction disjunction, disjunction1left, _)) :: rest671)) => let val result = MlyValue.disjunction ( ( Fmla (Interpreted_Logic Or, [disjunction, literal]) )) in ( LrTable.NT 57, ( result, disjunction1left, literal1right), rest671) end -| ( 170, ( ( _, ( MlyValue.atomic_formula atomic_formula, +| ( 176, ( ( _, ( MlyValue.atomic_formula atomic_formula, atomic_formula1left, atomic_formula1right)) :: rest671)) => let val result = MlyValue.literal (( atomic_formula )) in ( LrTable.NT 56, ( result, atomic_formula1left, atomic_formula1right), rest671) end -| ( 171, ( ( _, ( MlyValue.atomic_formula atomic_formula, _, +| ( 177, ( ( _, ( MlyValue.atomic_formula atomic_formula, _, atomic_formula1right)) :: ( _, ( _, TILDE1left, _)) :: rest671)) => let val result = MlyValue.literal ( ( Fmla (Interpreted_Logic Not, [atomic_formula]) )) in ( LrTable.NT 56, ( result, TILDE1left, atomic_formula1right), rest671) end -| ( 172, ( ( _, ( MlyValue.fol_infix_unary fol_infix_unary, +| ( 178, ( ( _, ( MlyValue.fol_infix_unary fol_infix_unary, fol_infix_unary1left, fol_infix_unary1right)) :: rest671)) => let val result = MlyValue.literal (( fol_infix_unary )) in ( LrTable.NT 56, ( result, fol_infix_unary1left, fol_infix_unary1right), rest671) end -| ( 173, ( ( _, ( MlyValue.thf_pair_connective thf_pair_connective, +| ( 179, ( ( _, ( MlyValue.thf_pair_connective thf_pair_connective, thf_pair_connective1left, thf_pair_connective1right)) :: rest671)) => let val result = MlyValue.thf_conn_term (( thf_pair_connective )) in ( LrTable.NT 55, ( result, thf_pair_connective1left, thf_pair_connective1right), rest671) end -| ( 174, ( ( _, ( MlyValue.assoc_connective assoc_connective, +| ( 180, ( ( _, ( MlyValue.assoc_connective assoc_connective, assoc_connective1left, assoc_connective1right)) :: rest671)) => let val result = MlyValue.thf_conn_term (( assoc_connective )) in ( LrTable.NT 55, ( result, assoc_connective1left, assoc_connective1right), rest671) end -| ( 175, ( ( _, ( MlyValue.thf_unary_connective thf_unary_connective, +| ( 181, ( ( _, ( MlyValue.thf_unary_connective thf_unary_connective, thf_unary_connective1left, thf_unary_connective1right)) :: rest671)) => let val result = MlyValue.thf_conn_term (( thf_unary_connective ) ) in ( LrTable.NT 55, ( result, thf_unary_connective1left, thf_unary_connective1right), rest671) end -| ( 176, ( ( _, ( MlyValue.term term2, _, term2right)) :: ( _, ( +| ( 182, ( ( _, ( MlyValue.term term2, _, term2right)) :: ( _, ( MlyValue.infix_inequality infix_inequality, _, _)) :: ( _, ( MlyValue.term term1, term1left, _)) :: rest671)) => let val result = MlyValue.fol_infix_unary (( Pred (infix_inequality, [term1, term2]) )) in ( LrTable.NT 54, ( result, term1left, term2right), rest671) end -| ( 177, ( ( _, ( MlyValue.fol_quantifier fol_quantifier, +| ( 183, ( ( _, ( MlyValue.fol_quantifier fol_quantifier, fol_quantifier1left, fol_quantifier1right)) :: rest671)) => let val result = MlyValue.thf_quantifier (( fol_quantifier )) in ( LrTable.NT 53, ( result, fol_quantifier1left, fol_quantifier1right), rest671) end -| ( 178, ( ( _, ( _, CARET1left, CARET1right)) :: rest671)) => let +| ( 184, ( ( _, ( _, CARET1left, CARET1right)) :: rest671)) => let val result = MlyValue.thf_quantifier (( Lambda )) in ( LrTable.NT 53, ( result, CARET1left, CARET1right), rest671) end -| ( 179, ( ( _, ( _, DEP_PROD1left, DEP_PROD1right)) :: rest671)) => +| ( 185, ( ( _, ( _, DEP_PROD1left, DEP_PROD1right)) :: rest671)) => let val result = MlyValue.thf_quantifier (( Dep_Prod )) in ( LrTable.NT 53, ( result, DEP_PROD1left, DEP_PROD1right), rest671 ) end -| ( 180, ( ( _, ( _, DEP_SUM1left, DEP_SUM1right)) :: rest671)) => +| ( 186, ( ( _, ( _, DEP_SUM1left, DEP_SUM1right)) :: rest671)) => let val result = MlyValue.thf_quantifier (( Dep_Sum )) in ( LrTable.NT 53, ( result, DEP_SUM1left, DEP_SUM1right), rest671) end -| ( 181, ( ( _, ( _, INDEF_CHOICE1left, INDEF_CHOICE1right)) :: +| ( 187, ( ( _, ( _, INDEF_CHOICE1left, INDEF_CHOICE1right)) :: rest671)) => let val result = MlyValue.thf_quantifier (( Epsilon )) in ( LrTable.NT 53, ( result, INDEF_CHOICE1left, INDEF_CHOICE1right), rest671) end -| ( 182, ( ( _, ( _, DEFIN_CHOICE1left, DEFIN_CHOICE1right)) :: +| ( 188, ( ( _, ( _, DEFIN_CHOICE1left, DEFIN_CHOICE1right)) :: rest671)) => let val result = MlyValue.thf_quantifier (( Iota )) in ( LrTable.NT 53, ( result, DEFIN_CHOICE1left, DEFIN_CHOICE1right), rest671) end -| ( 183, ( ( _, ( MlyValue.infix_equality infix_equality, +| ( 189, ( ( _, ( MlyValue.infix_equality infix_equality, infix_equality1left, infix_equality1right)) :: rest671)) => let val result = MlyValue.thf_pair_connective (( infix_equality )) in ( LrTable.NT 52, ( result, infix_equality1left, infix_equality1right), rest671) end -| ( 184, ( ( _, ( MlyValue.infix_inequality infix_inequality, +| ( 190, ( ( _, ( MlyValue.infix_inequality infix_inequality, infix_inequality1left, infix_inequality1right)) :: rest671)) => let val result = MlyValue.thf_pair_connective (( infix_inequality )) in ( LrTable.NT 52, ( result, infix_inequality1left, infix_inequality1right), rest671) end -| ( 185, ( ( _, ( MlyValue.binary_connective binary_connective, +| ( 191, ( ( _, ( MlyValue.binary_connective binary_connective, binary_connective1left, binary_connective1right)) :: rest671)) => let val result = MlyValue.thf_pair_connective (( binary_connective )) in ( LrTable.NT 52, ( result, binary_connective1left, binary_connective1right), rest671) end -| ( 186, ( ( _, ( MlyValue.unary_connective unary_connective, +| ( 192, ( ( _, ( MlyValue.unary_connective unary_connective, unary_connective1left, unary_connective1right)) :: rest671)) => let val result = MlyValue.thf_unary_connective (( unary_connective )) in ( LrTable.NT 51, ( result, unary_connective1left, unary_connective1right), rest671) end -| ( 187, ( ( _, ( _, OPERATOR_FORALL1left, OPERATOR_FORALL1right)) :: +| ( 193, ( ( _, ( _, OPERATOR_FORALL1left, OPERATOR_FORALL1right)) :: rest671)) => let val result = MlyValue.thf_unary_connective ( ( Interpreted_Logic Op_Forall )) in ( LrTable.NT 51, ( result, OPERATOR_FORALL1left, OPERATOR_FORALL1right), rest671) end -| ( 188, ( ( _, ( _, OPERATOR_EXISTS1left, OPERATOR_EXISTS1right)) :: +| ( 194, ( ( _, ( _, OPERATOR_EXISTS1left, OPERATOR_EXISTS1right)) :: rest671)) => let val result = MlyValue.thf_unary_connective ( ( Interpreted_Logic Op_Exists )) in ( LrTable.NT 51, ( result, OPERATOR_EXISTS1left, OPERATOR_EXISTS1right), rest671) end -| ( 189, ( ( _, ( _, EXCLAMATION1left, EXCLAMATION1right)) :: rest671 +| ( 195, ( ( _, ( _, EXCLAMATION1left, EXCLAMATION1right)) :: rest671 )) => let val result = MlyValue.fol_quantifier (( Forall )) in ( LrTable.NT 50, ( result, EXCLAMATION1left, EXCLAMATION1right), rest671) end -| ( 190, ( ( _, ( _, QUESTION1left, QUESTION1right)) :: rest671)) => +| ( 196, ( ( _, ( _, QUESTION1left, QUESTION1right)) :: rest671)) => let val result = MlyValue.fol_quantifier (( Exists )) in ( LrTable.NT 50, ( result, QUESTION1left, QUESTION1right), rest671 ) end -| ( 191, ( ( _, ( _, IFF1left, IFF1right)) :: rest671)) => let val +| ( 197, ( ( _, ( _, IFF1left, IFF1right)) :: rest671)) => let val result = MlyValue.binary_connective (( Interpreted_Logic Iff )) in ( LrTable.NT 49, ( result, IFF1left, IFF1right), rest671) end -| ( 192, ( ( _, ( _, IMPLIES1left, IMPLIES1right)) :: rest671)) => +| ( 198, ( ( _, ( _, IMPLIES1left, IMPLIES1right)) :: rest671)) => let val result = MlyValue.binary_connective ( ( Interpreted_Logic If )) in ( LrTable.NT 49, ( result, IMPLIES1left, IMPLIES1right), rest671) end -| ( 193, ( ( _, ( _, FI1left, FI1right)) :: rest671)) => let val +| ( 199, ( ( _, ( _, FI1left, FI1right)) :: rest671)) => let val result = MlyValue.binary_connective (( Interpreted_Logic Fi )) in ( LrTable.NT 49, ( result, FI1left, FI1right), rest671) end -| ( 194, ( ( _, ( _, XOR1left, XOR1right)) :: rest671)) => let val +| ( 200, ( ( _, ( _, XOR1left, XOR1right)) :: rest671)) => let val result = MlyValue.binary_connective (( Interpreted_Logic Xor )) in ( LrTable.NT 49, ( result, XOR1left, XOR1right), rest671) end -| ( 195, ( ( _, ( _, NOR1left, NOR1right)) :: rest671)) => let val +| ( 201, ( ( _, ( _, NOR1left, NOR1right)) :: rest671)) => let val result = MlyValue.binary_connective (( Interpreted_Logic Nor )) in ( LrTable.NT 49, ( result, NOR1left, NOR1right), rest671) end -| ( 196, ( ( _, ( _, NAND1left, NAND1right)) :: rest671)) => let val +| ( 202, ( ( _, ( _, NAND1left, NAND1right)) :: rest671)) => let val result = MlyValue.binary_connective (( Interpreted_Logic Nand )) in ( LrTable.NT 49, ( result, NAND1left, NAND1right), rest671) end -| ( 197, ( ( _, ( _, VLINE1left, VLINE1right)) :: rest671)) => let +| ( 203, ( ( _, ( _, VLINE1left, VLINE1right)) :: rest671)) => let val result = MlyValue.assoc_connective (( Interpreted_Logic Or )) in ( LrTable.NT 48, ( result, VLINE1left, VLINE1right), rest671) end -| ( 198, ( ( _, ( _, AMPERSAND1left, AMPERSAND1right)) :: rest671)) +| ( 204, ( ( _, ( _, AMPERSAND1left, AMPERSAND1right)) :: rest671)) => let val result = MlyValue.assoc_connective ( ( Interpreted_Logic And )) in ( LrTable.NT 48, ( result, AMPERSAND1left, AMPERSAND1right), rest671) end -| ( 199, ( ( _, ( _, TILDE1left, TILDE1right)) :: rest671)) => let +| ( 205, ( ( _, ( _, TILDE1left, TILDE1right)) :: rest671)) => let val result = MlyValue.unary_connective (( Interpreted_Logic Not )) in ( LrTable.NT 45, ( result, TILDE1left, TILDE1right), rest671) end -| ( 200, ( ( _, ( MlyValue.atomic_defined_word atomic_defined_word, +| ( 206, ( ( _, ( MlyValue.atomic_defined_word atomic_defined_word, atomic_defined_word1left, atomic_defined_word1right)) :: rest671)) => let val result = MlyValue.defined_type ( ( @@ -5143,61 +5311,61 @@ in ( LrTable.NT 46, ( result, atomic_defined_word1left, atomic_defined_word1right), rest671) end -| ( 201, ( ( _, ( MlyValue.atomic_system_word atomic_system_word, +| ( 207, ( ( _, ( MlyValue.atomic_system_word atomic_system_word, atomic_system_word1left, atomic_system_word1right)) :: rest671)) => let val result = MlyValue.system_type (( atomic_system_word )) in ( LrTable.NT 47, ( result, atomic_system_word1left, atomic_system_word1right), rest671) end -| ( 202, ( ( _, ( MlyValue.plain_atomic_formula plain_atomic_formula, +| ( 208, ( ( _, ( MlyValue.plain_atomic_formula plain_atomic_formula, plain_atomic_formula1left, plain_atomic_formula1right)) :: rest671)) => let val result = MlyValue.atomic_formula ( ( plain_atomic_formula )) in ( LrTable.NT 44, ( result, plain_atomic_formula1left, plain_atomic_formula1right), rest671) end -| ( 203, ( ( _, ( MlyValue.defined_atomic_formula +| ( 209, ( ( _, ( MlyValue.defined_atomic_formula defined_atomic_formula, defined_atomic_formula1left, defined_atomic_formula1right)) :: rest671)) => let val result = MlyValue.atomic_formula (( defined_atomic_formula )) in ( LrTable.NT 44, ( result, defined_atomic_formula1left, defined_atomic_formula1right), rest671) end -| ( 204, ( ( _, ( MlyValue.system_atomic_formula +| ( 210, ( ( _, ( MlyValue.system_atomic_formula system_atomic_formula, system_atomic_formula1left, system_atomic_formula1right)) :: rest671)) => let val result = MlyValue.atomic_formula (( system_atomic_formula )) in ( LrTable.NT 44, ( result, system_atomic_formula1left, system_atomic_formula1right), rest671) end -| ( 205, ( ( _, ( MlyValue.plain_term plain_term, plain_term1left, +| ( 211, ( ( _, ( MlyValue.plain_term plain_term, plain_term1left, plain_term1right)) :: rest671)) => let val result = MlyValue.plain_atomic_formula (( Pred plain_term )) in ( LrTable.NT 43, ( result, plain_term1left, plain_term1right), rest671) end -| ( 206, ( ( _, ( MlyValue.defined_plain_formula +| ( 212, ( ( _, ( MlyValue.defined_plain_formula defined_plain_formula, defined_plain_formula1left, defined_plain_formula1right)) :: rest671)) => let val result = MlyValue.defined_atomic_formula (( defined_plain_formula )) in ( LrTable.NT 42, ( result, defined_plain_formula1left, defined_plain_formula1right), rest671) end -| ( 207, ( ( _, ( MlyValue.defined_infix_formula +| ( 213, ( ( _, ( MlyValue.defined_infix_formula defined_infix_formula, defined_infix_formula1left, defined_infix_formula1right)) :: rest671)) => let val result = MlyValue.defined_atomic_formula (( defined_infix_formula )) in ( LrTable.NT 42, ( result, defined_infix_formula1left, defined_infix_formula1right), rest671) end -| ( 208, ( ( _, ( MlyValue.defined_plain_term defined_plain_term, +| ( 214, ( ( _, ( MlyValue.defined_plain_term defined_plain_term, defined_plain_term1left, defined_plain_term1right)) :: rest671)) => let val result = MlyValue.defined_plain_formula ( ( Pred defined_plain_term )) in ( LrTable.NT 41, ( result, defined_plain_term1left, defined_plain_term1right), rest671) end -| ( 209, ( ( _, ( MlyValue.atomic_defined_word atomic_defined_word, +| ( 215, ( ( _, ( MlyValue.atomic_defined_word atomic_defined_word, atomic_defined_word1left, atomic_defined_word1right)) :: rest671)) => let val result = MlyValue.defined_prop ( ( @@ -5210,7 +5378,7 @@ in ( LrTable.NT 39, ( result, atomic_defined_word1left, atomic_defined_word1right), rest671) end -| ( 210, ( ( _, ( MlyValue.atomic_defined_word atomic_defined_word, +| ( 216, ( ( _, ( MlyValue.atomic_defined_word atomic_defined_word, atomic_defined_word1left, atomic_defined_word1right)) :: rest671)) => let val result = MlyValue.defined_pred ( ( @@ -5229,143 +5397,143 @@ in ( LrTable.NT 40, ( result, atomic_defined_word1left, atomic_defined_word1right), rest671) end -| ( 211, ( ( _, ( MlyValue.term term2, _, term2right)) :: ( _, ( +| ( 217, ( ( _, ( MlyValue.term term2, _, term2right)) :: ( _, ( MlyValue.defined_infix_pred defined_infix_pred, _, _)) :: ( _, ( MlyValue.term term1, term1left, _)) :: rest671)) => let val result = MlyValue.defined_infix_formula ( (Pred (defined_infix_pred, [term1, term2]))) in ( LrTable.NT 38, ( result, term1left, term2right), rest671) end -| ( 212, ( ( _, ( MlyValue.infix_equality infix_equality, +| ( 218, ( ( _, ( MlyValue.infix_equality infix_equality, infix_equality1left, infix_equality1right)) :: rest671)) => let val result = MlyValue.defined_infix_pred (( infix_equality )) in ( LrTable.NT 37, ( result, infix_equality1left, infix_equality1right), rest671) end -| ( 213, ( ( _, ( _, EQUALS1left, EQUALS1right)) :: rest671)) => let +| ( 219, ( ( _, ( _, EQUALS1left, EQUALS1right)) :: rest671)) => let val result = MlyValue.infix_equality (( Interpreted_Logic Equals )) in ( LrTable.NT 35, ( result, EQUALS1left, EQUALS1right), rest671) end -| ( 214, ( ( _, ( _, NEQUALS1left, NEQUALS1right)) :: rest671)) => +| ( 220, ( ( _, ( _, NEQUALS1left, NEQUALS1right)) :: rest671)) => let val result = MlyValue.infix_inequality ( ( Interpreted_Logic NEquals )) in ( LrTable.NT 36, ( result, NEQUALS1left, NEQUALS1right), rest671) end -| ( 215, ( ( _, ( MlyValue.system_term system_term, system_term1left, +| ( 221, ( ( _, ( MlyValue.system_term system_term, system_term1left, system_term1right)) :: rest671)) => let val result = MlyValue.system_atomic_formula (( Pred system_term )) in ( LrTable.NT 34, ( result, system_term1left, system_term1right), rest671) end -| ( 216, ( ( _, ( MlyValue.function_term function_term, +| ( 222, ( ( _, ( MlyValue.function_term function_term, function_term1left, function_term1right)) :: rest671)) => let val result = MlyValue.term (( function_term )) in ( LrTable.NT 19, ( result, function_term1left, function_term1right ), rest671) end -| ( 217, ( ( _, ( MlyValue.variable_ variable_, variable_1left, +| ( 223, ( ( _, ( MlyValue.variable_ variable_, variable_1left, variable_1right)) :: rest671)) => let val result = MlyValue.term ( ( Term_Var variable_ )) in ( LrTable.NT 19, ( result, variable_1left, variable_1right), rest671) end -| ( 218, ( ( _, ( MlyValue.conditional_term conditional_term, +| ( 224, ( ( _, ( MlyValue.conditional_term conditional_term, conditional_term1left, conditional_term1right)) :: rest671)) => let val result = MlyValue.term (( conditional_term )) in ( LrTable.NT 19, ( result, conditional_term1left, conditional_term1right), rest671) end -| ( 219, ( ( _, ( MlyValue.let_term let_term, let_term1left, +| ( 225, ( ( _, ( MlyValue.let_term let_term, let_term1left, let_term1right)) :: rest671)) => let val result = MlyValue.term ( ( let_term )) in ( LrTable.NT 19, ( result, let_term1left, let_term1right), rest671 ) end -| ( 220, ( ( _, ( MlyValue.plain_term plain_term, plain_term1left, +| ( 226, ( ( _, ( MlyValue.plain_term plain_term, plain_term1left, plain_term1right)) :: rest671)) => let val result = MlyValue.function_term (( Term_Func plain_term )) in ( LrTable.NT 32, ( result, plain_term1left, plain_term1right), rest671) end -| ( 221, ( ( _, ( MlyValue.defined_term defined_term, +| ( 227, ( ( _, ( MlyValue.defined_term defined_term, defined_term1left, defined_term1right)) :: rest671)) => let val result = MlyValue.function_term (( defined_term )) in ( LrTable.NT 32, ( result, defined_term1left, defined_term1right), rest671) end -| ( 222, ( ( _, ( MlyValue.system_term system_term, system_term1left, +| ( 228, ( ( _, ( MlyValue.system_term system_term, system_term1left, system_term1right)) :: rest671)) => let val result = MlyValue.function_term (( Term_Func system_term )) in ( LrTable.NT 32, ( result, system_term1left, system_term1right), rest671) end -| ( 223, ( ( _, ( MlyValue.constant constant, constant1left, +| ( 229, ( ( _, ( MlyValue.constant constant, constant1left, constant1right)) :: rest671)) => let val result = MlyValue.plain_term (( (constant, []) )) in ( LrTable.NT 31, ( result, constant1left, constant1right), rest671 ) end -| ( 224, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.arguments +| ( 230, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.arguments arguments, _, _)) :: _ :: ( _, ( MlyValue.functor_ functor_, functor_1left, _)) :: rest671)) => let val result = MlyValue.plain_term (( (functor_, arguments) )) in ( LrTable.NT 31, ( result, functor_1left, RPAREN1right), rest671) end -| ( 225, ( ( _, ( MlyValue.functor_ functor_, functor_1left, +| ( 231, ( ( _, ( MlyValue.functor_ functor_, functor_1left, functor_1right)) :: rest671)) => let val result = MlyValue.constant ( ( functor_ )) in ( LrTable.NT 30, ( result, functor_1left, functor_1right), rest671 ) end -| ( 226, ( ( _, ( MlyValue.atomic_word atomic_word, atomic_word1left, +| ( 232, ( ( _, ( MlyValue.atomic_word atomic_word, atomic_word1left, atomic_word1right)) :: rest671)) => let val result = MlyValue.functor_ (( Uninterpreted atomic_word )) in ( LrTable.NT 18, ( result, atomic_word1left, atomic_word1right), rest671) end -| ( 227, ( ( _, ( MlyValue.defined_atom defined_atom, +| ( 233, ( ( _, ( MlyValue.defined_atom defined_atom, defined_atom1left, defined_atom1right)) :: rest671)) => let val result = MlyValue.defined_term (( defined_atom )) in ( LrTable.NT 29, ( result, defined_atom1left, defined_atom1right), rest671) end -| ( 228, ( ( _, ( MlyValue.defined_atomic_term defined_atomic_term, +| ( 234, ( ( _, ( MlyValue.defined_atomic_term defined_atomic_term, defined_atomic_term1left, defined_atomic_term1right)) :: rest671)) => let val result = MlyValue.defined_term (( defined_atomic_term )) in ( LrTable.NT 29, ( result, defined_atomic_term1left, defined_atomic_term1right), rest671) end -| ( 229, ( ( _, ( MlyValue.number number, number1left, number1right)) +| ( 235, ( ( _, ( MlyValue.number number, number1left, number1right)) :: rest671)) => let val result = MlyValue.defined_atom ( ( Term_Num number )) in ( LrTable.NT 28, ( result, number1left, number1right), rest671) end -| ( 230, ( ( _, ( MlyValue.DISTINCT_OBJECT DISTINCT_OBJECT, +| ( 236, ( ( _, ( MlyValue.DISTINCT_OBJECT DISTINCT_OBJECT, DISTINCT_OBJECT1left, DISTINCT_OBJECT1right)) :: rest671)) => let val result = MlyValue.defined_atom ( ( Term_Distinct_Object DISTINCT_OBJECT )) in ( LrTable.NT 28, ( result, DISTINCT_OBJECT1left, DISTINCT_OBJECT1right), rest671) end -| ( 231, ( ( _, ( MlyValue.defined_plain_term defined_plain_term, +| ( 237, ( ( _, ( MlyValue.defined_plain_term defined_plain_term, defined_plain_term1left, defined_plain_term1right)) :: rest671)) => let val result = MlyValue.defined_atomic_term ( ( Term_Func defined_plain_term )) in ( LrTable.NT 27, ( result, defined_plain_term1left, defined_plain_term1right), rest671) end -| ( 232, ( ( _, ( MlyValue.defined_constant defined_constant, +| ( 238, ( ( _, ( MlyValue.defined_constant defined_constant, defined_constant1left, defined_constant1right)) :: rest671)) => let val result = MlyValue.defined_plain_term (( (defined_constant, []) ) ) in ( LrTable.NT 26, ( result, defined_constant1left, defined_constant1right), rest671) end -| ( 233, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.arguments +| ( 239, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.arguments arguments, _, _)) :: _ :: ( _, ( MlyValue.defined_functor defined_functor, defined_functor1left, _)) :: rest671)) => let val result = MlyValue.defined_plain_term (( (defined_functor, arguments) ) @@ -5373,13 +5541,13 @@ in ( LrTable.NT 26, ( result, defined_functor1left, RPAREN1right), rest671) end -| ( 234, ( ( _, ( MlyValue.defined_functor defined_functor, +| ( 240, ( ( _, ( MlyValue.defined_functor defined_functor, defined_functor1left, defined_functor1right)) :: rest671)) => let val result = MlyValue.defined_constant (( defined_functor )) in ( LrTable.NT 25, ( result, defined_functor1left, defined_functor1right), rest671) end -| ( 235, ( ( _, ( MlyValue.atomic_defined_word atomic_defined_word, +| ( 241, ( ( _, ( MlyValue.atomic_defined_word atomic_defined_word, atomic_defined_word1left, atomic_defined_word1right)) :: rest671)) => let val result = MlyValue.defined_functor ( ( @@ -5432,49 +5600,49 @@ in ( LrTable.NT 21, ( result, atomic_defined_word1left, atomic_defined_word1right), rest671) end -| ( 236, ( ( _, ( MlyValue.system_constant system_constant, +| ( 242, ( ( _, ( MlyValue.system_constant system_constant, system_constant1left, system_constant1right)) :: rest671)) => let val result = MlyValue.system_term (( (system_constant, []) )) in ( LrTable.NT 24, ( result, system_constant1left, system_constant1right), rest671) end -| ( 237, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.arguments +| ( 243, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.arguments arguments, _, _)) :: _ :: ( _, ( MlyValue.system_functor system_functor, system_functor1left, _)) :: rest671)) => let val result = MlyValue.system_term (( (system_functor, arguments) )) in ( LrTable.NT 24, ( result, system_functor1left, RPAREN1right), rest671) end -| ( 238, ( ( _, ( MlyValue.system_functor system_functor, +| ( 244, ( ( _, ( MlyValue.system_functor system_functor, system_functor1left, system_functor1right)) :: rest671)) => let val result = MlyValue.system_constant (( system_functor )) in ( LrTable.NT 23, ( result, system_functor1left, system_functor1right), rest671) end -| ( 239, ( ( _, ( MlyValue.atomic_system_word atomic_system_word, +| ( 245, ( ( _, ( MlyValue.atomic_system_word atomic_system_word, atomic_system_word1left, atomic_system_word1right)) :: rest671)) => let val result = MlyValue.system_functor ( ( System atomic_system_word )) in ( LrTable.NT 22, ( result, atomic_system_word1left, atomic_system_word1right), rest671) end -| ( 240, ( ( _, ( MlyValue.UPPER_WORD UPPER_WORD, UPPER_WORD1left, +| ( 246, ( ( _, ( MlyValue.UPPER_WORD UPPER_WORD, UPPER_WORD1left, UPPER_WORD1right)) :: rest671)) => let val result = MlyValue.variable_ (( UPPER_WORD )) in ( LrTable.NT 10, ( result, UPPER_WORD1left, UPPER_WORD1right), rest671) end -| ( 241, ( ( _, ( MlyValue.term term, term1left, term1right)) :: +| ( 247, ( ( _, ( MlyValue.term term, term1left, term1right)) :: rest671)) => let val result = MlyValue.arguments (( [term] )) in ( LrTable.NT 20, ( result, term1left, term1right), rest671) end -| ( 242, ( ( _, ( MlyValue.arguments arguments, _, arguments1right)) +| ( 248, ( ( _, ( MlyValue.arguments arguments, _, arguments1right)) :: _ :: ( _, ( MlyValue.term term, term1left, _)) :: rest671)) => let val result = MlyValue.arguments (( term :: arguments )) in ( LrTable.NT 20, ( result, term1left, arguments1right), rest671) end -| ( 243, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.term term2, +| ( 249, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.term term2, _, _)) :: _ :: ( _, ( MlyValue.term term1, _, _)) :: _ :: ( _, ( MlyValue.tff_logic_formula tff_logic_formula, _, _)) :: _ :: ( _, ( _, ITE_T1left, _)) :: rest671)) => let val result = @@ -5484,38 +5652,38 @@ )) in ( LrTable.NT 33, ( result, ITE_T1left, RPAREN1right), rest671) end -| ( 244, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.term term, +| ( 250, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.term term, _, _)) :: _ :: ( _, ( MlyValue.tff_let_formula_defn tff_let_formula_defn, _, _)) :: _ :: ( _, ( _, LET_FT1left, _)) :: rest671)) => let val result = MlyValue.let_term ( (Term_Let (tff_let_formula_defn, term) )) - in ( LrTable.NT 143, ( result, LET_FT1left, RPAREN1right), rest671) + in ( LrTable.NT 146, ( result, LET_FT1left, RPAREN1right), rest671) end -| ( 245, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.term term, +| ( 251, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.term term, _, _)) :: _ :: ( _, ( MlyValue.tff_let_term_defn tff_let_term_defn, _ , _)) :: _ :: ( _, ( _, LET_TT1left, _)) :: rest671)) => let val result = MlyValue.let_term ((Term_Let (tff_let_term_defn, term) )) - in ( LrTable.NT 143, ( result, LET_TT1left, RPAREN1right), rest671) + in ( LrTable.NT 146, ( result, LET_TT1left, RPAREN1right), rest671) end -| ( 246, ( ( _, ( MlyValue.useful_info useful_info, _, +| ( 252, ( ( _, ( MlyValue.useful_info useful_info, _, useful_info1right)) :: ( _, ( _, COMMA1left, _)) :: rest671)) => let val result = MlyValue.optional_info (( useful_info )) in ( LrTable.NT 4, ( result, COMMA1left, useful_info1right), rest671) end -| ( 247, ( rest671)) => let val result = MlyValue.optional_info ( +| ( 253, ( rest671)) => let val result = MlyValue.optional_info ( ( [] )) in ( LrTable.NT 4, ( result, defaultPos, defaultPos), rest671) end -| ( 248, ( ( _, ( MlyValue.general_list general_list, +| ( 254, ( ( _, ( MlyValue.general_list general_list, general_list1left, general_list1right)) :: rest671)) => let val result = MlyValue.useful_info (( general_list )) in ( LrTable.NT 16, ( result, general_list1left, general_list1right), rest671) end -| ( 249, ( ( _, ( _, _, PERIOD1right)) :: _ :: ( _, ( +| ( 255, ( ( _, ( _, _, PERIOD1right)) :: _ :: ( _, ( MlyValue.formula_selection formula_selection, _, _)) :: ( _, ( MlyValue.file_name file_name, _, _)) :: _ :: ( _, ( _, (INCLUDEleft as INCLUDE1left), INCLUDEright)) :: rest671)) => let val result = @@ -5528,80 +5696,80 @@ in ( LrTable.NT 132, ( result, INCLUDE1left, PERIOD1right), rest671) end -| ( 250, ( ( _, ( _, _, RBRKT1right)) :: ( _, ( MlyValue.name_list +| ( 256, ( ( _, ( _, _, RBRKT1right)) :: ( _, ( MlyValue.name_list name_list, _, _)) :: _ :: ( _, ( _, COMMA1left, _)) :: rest671)) => let val result = MlyValue.formula_selection (( name_list )) in ( LrTable.NT 3, ( result, COMMA1left, RBRKT1right), rest671) end -| ( 251, ( rest671)) => let val result = MlyValue.formula_selection +| ( 257, ( rest671)) => let val result = MlyValue.formula_selection (( [] )) in ( LrTable.NT 3, ( result, defaultPos, defaultPos), rest671) end -| ( 252, ( ( _, ( MlyValue.name_list name_list, _, name_list1right)) +| ( 258, ( ( _, ( MlyValue.name_list name_list, _, name_list1right)) :: _ :: ( _, ( MlyValue.name name, name1left, _)) :: rest671)) => let val result = MlyValue.name_list (( name :: name_list )) in ( LrTable.NT 2, ( result, name1left, name_list1right), rest671) end -| ( 253, ( ( _, ( MlyValue.name name, name1left, name1right)) :: +| ( 259, ( ( _, ( MlyValue.name name, name1left, name1right)) :: rest671)) => let val result = MlyValue.name_list (( [name] )) in ( LrTable.NT 2, ( result, name1left, name1right), rest671) end -| ( 254, ( ( _, ( MlyValue.general_data general_data, +| ( 260, ( ( _, ( MlyValue.general_data general_data, general_data1left, general_data1right)) :: rest671)) => let val result = MlyValue.general_term (( General_Data general_data )) in ( LrTable.NT 7, ( result, general_data1left, general_data1right), rest671) end -| ( 255, ( ( _, ( MlyValue.general_term general_term, _, +| ( 261, ( ( _, ( MlyValue.general_term general_term, _, general_term1right)) :: _ :: ( _, ( MlyValue.general_data general_data , general_data1left, _)) :: rest671)) => let val result = MlyValue.general_term (( General_Term (general_data, general_term) )) in ( LrTable.NT 7, ( result, general_data1left, general_term1right), rest671) end -| ( 256, ( ( _, ( MlyValue.general_list general_list, +| ( 262, ( ( _, ( MlyValue.general_list general_list, general_list1left, general_list1right)) :: rest671)) => let val result = MlyValue.general_term (( General_List general_list )) in ( LrTable.NT 7, ( result, general_list1left, general_list1right), rest671) end -| ( 257, ( ( _, ( MlyValue.atomic_word atomic_word, atomic_word1left, +| ( 263, ( ( _, ( MlyValue.atomic_word atomic_word, atomic_word1left, atomic_word1right)) :: rest671)) => let val result = MlyValue.general_data (( Atomic_Word atomic_word )) in ( LrTable.NT 9, ( result, atomic_word1left, atomic_word1right), rest671) end -| ( 258, ( ( _, ( MlyValue.general_function general_function, +| ( 264, ( ( _, ( MlyValue.general_function general_function, general_function1left, general_function1right)) :: rest671)) => let val result = MlyValue.general_data (( general_function )) in ( LrTable.NT 9, ( result, general_function1left, general_function1right), rest671) end -| ( 259, ( ( _, ( MlyValue.variable_ variable_, variable_1left, +| ( 265, ( ( _, ( MlyValue.variable_ variable_, variable_1left, variable_1right)) :: rest671)) => let val result = MlyValue.general_data (( V variable_ )) in ( LrTable.NT 9, ( result, variable_1left, variable_1right), rest671) end -| ( 260, ( ( _, ( MlyValue.number number, number1left, number1right)) +| ( 266, ( ( _, ( MlyValue.number number, number1left, number1right)) :: rest671)) => let val result = MlyValue.general_data ( ( Number number )) in ( LrTable.NT 9, ( result, number1left, number1right), rest671) end -| ( 261, ( ( _, ( MlyValue.DISTINCT_OBJECT DISTINCT_OBJECT, +| ( 267, ( ( _, ( MlyValue.DISTINCT_OBJECT DISTINCT_OBJECT, DISTINCT_OBJECT1left, DISTINCT_OBJECT1right)) :: rest671)) => let val result = MlyValue.general_data (( Distinct_Object DISTINCT_OBJECT )) in ( LrTable.NT 9, ( result, DISTINCT_OBJECT1left, DISTINCT_OBJECT1right), rest671) end -| ( 262, ( ( _, ( MlyValue.formula_data formula_data, +| ( 268, ( ( _, ( MlyValue.formula_data formula_data, formula_data1left, formula_data1right)) :: rest671)) => let val result = MlyValue.general_data (( formula_data )) in ( LrTable.NT 9, ( result, formula_data1left, formula_data1right), rest671) end -| ( 263, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( +| ( 269, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.general_terms general_terms, _, _)) :: _ :: ( _, ( MlyValue.atomic_word atomic_word, atomic_word1left, _)) :: rest671)) => let val result = MlyValue.general_function ( @@ -5609,145 +5777,145 @@ in ( LrTable.NT 15, ( result, atomic_word1left, RPAREN1right), rest671) end -| ( 264, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.thf_formula +| ( 270, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.thf_formula thf_formula, _, _)) :: _ :: ( _, ( _, DTHF1left, _)) :: rest671)) => let val result = MlyValue.formula_data ( ( Formula_Data (THF, thf_formula) )) in ( LrTable.NT 12, ( result, DTHF1left, RPAREN1right), rest671) end -| ( 265, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.tff_formula +| ( 271, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.tff_formula tff_formula, _, _)) :: _ :: ( _, ( _, DTFF1left, _)) :: rest671)) => let val result = MlyValue.formula_data ( ( Formula_Data (TFF, tff_formula) )) in ( LrTable.NT 12, ( result, DTFF1left, RPAREN1right), rest671) end -| ( 266, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.fof_formula +| ( 272, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.fof_formula fof_formula, _, _)) :: _ :: ( _, ( _, DFOF1left, _)) :: rest671)) => let val result = MlyValue.formula_data ( ( Formula_Data (FOF, fof_formula) )) in ( LrTable.NT 12, ( result, DFOF1left, RPAREN1right), rest671) end -| ( 267, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.cnf_formula +| ( 273, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.cnf_formula cnf_formula, _, _)) :: _ :: ( _, ( _, DCNF1left, _)) :: rest671)) => let val result = MlyValue.formula_data ( ( Formula_Data (CNF, cnf_formula) )) in ( LrTable.NT 12, ( result, DCNF1left, RPAREN1right), rest671) end -| ( 268, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.term term, +| ( 274, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( MlyValue.term term, _, _)) :: _ :: ( _, ( _, DFOT1left, _)) :: rest671)) => let val result = MlyValue.formula_data (( Term_Data term )) in ( LrTable.NT 12, ( result, DFOT1left, RPAREN1right), rest671) end -| ( 269, ( ( _, ( _, _, RBRKT1right)) :: ( _, ( +| ( 275, ( ( _, ( _, _, RBRKT1right)) :: ( _, ( MlyValue.general_terms general_terms, _, _)) :: ( _, ( _, LBRKT1left, _)) :: rest671)) => let val result = MlyValue.general_list ( ( general_terms )) in ( LrTable.NT 5, ( result, LBRKT1left, RBRKT1right), rest671) end -| ( 270, ( ( _, ( _, _, RBRKT1right)) :: ( _, ( _, LBRKT1left, _)) :: +| ( 276, ( ( _, ( _, _, RBRKT1right)) :: ( _, ( _, LBRKT1left, _)) :: rest671)) => let val result = MlyValue.general_list (( [] )) in ( LrTable.NT 5, ( result, LBRKT1left, RBRKT1right), rest671) end -| ( 271, ( ( _, ( MlyValue.general_terms general_terms, _, +| ( 277, ( ( _, ( MlyValue.general_terms general_terms, _, general_terms1right)) :: _ :: ( _, ( MlyValue.general_term general_term, general_term1left, _)) :: rest671)) => let val result = MlyValue.general_terms (( general_term :: general_terms )) in ( LrTable.NT 6, ( result, general_term1left, general_terms1right), rest671) end -| ( 272, ( ( _, ( MlyValue.general_term general_term, +| ( 278, ( ( _, ( MlyValue.general_term general_term, general_term1left, general_term1right)) :: rest671)) => let val result = MlyValue.general_terms (( [general_term] )) in ( LrTable.NT 6, ( result, general_term1left, general_term1right), rest671) end -| ( 273, ( ( _, ( MlyValue.atomic_word atomic_word, atomic_word1left, +| ( 279, ( ( _, ( MlyValue.atomic_word atomic_word, atomic_word1left, atomic_word1right)) :: rest671)) => let val result = MlyValue.name ( ( atomic_word )) in ( LrTable.NT 1, ( result, atomic_word1left, atomic_word1right), rest671) end -| ( 274, ( ( _, ( MlyValue.integer integer, integer1left, +| ( 280, ( ( _, ( MlyValue.integer integer, integer1left, integer1right)) :: rest671)) => let val result = MlyValue.name ( ( integer )) in ( LrTable.NT 1, ( result, integer1left, integer1right), rest671) end -| ( 275, ( ( _, ( MlyValue.LOWER_WORD LOWER_WORD, LOWER_WORD1left, +| ( 281, ( ( _, ( MlyValue.LOWER_WORD LOWER_WORD, LOWER_WORD1left, LOWER_WORD1right)) :: rest671)) => let val result = MlyValue.atomic_word (( LOWER_WORD )) in ( LrTable.NT 8, ( result, LOWER_WORD1left, LOWER_WORD1right), rest671) end -| ( 276, ( ( _, ( MlyValue.SINGLE_QUOTED SINGLE_QUOTED, +| ( 282, ( ( _, ( MlyValue.SINGLE_QUOTED SINGLE_QUOTED, SINGLE_QUOTED1left, SINGLE_QUOTED1right)) :: rest671)) => let val result = MlyValue.atomic_word (( dequote SINGLE_QUOTED )) in ( LrTable.NT 8, ( result, SINGLE_QUOTED1left, SINGLE_QUOTED1right) , rest671) end -| ( 277, ( ( _, ( _, THF1left, THF1right)) :: rest671)) => let val +| ( 283, ( ( _, ( _, THF1left, THF1right)) :: rest671)) => let val result = MlyValue.atomic_word (( "thf" )) in ( LrTable.NT 8, ( result, THF1left, THF1right), rest671) end -| ( 278, ( ( _, ( _, TFF1left, TFF1right)) :: rest671)) => let val +| ( 284, ( ( _, ( _, TFF1left, TFF1right)) :: rest671)) => let val result = MlyValue.atomic_word (( "tff" )) in ( LrTable.NT 8, ( result, TFF1left, TFF1right), rest671) end -| ( 279, ( ( _, ( _, FOF1left, FOF1right)) :: rest671)) => let val +| ( 285, ( ( _, ( _, FOF1left, FOF1right)) :: rest671)) => let val result = MlyValue.atomic_word (( "fof" )) in ( LrTable.NT 8, ( result, FOF1left, FOF1right), rest671) end -| ( 280, ( ( _, ( _, CNF1left, CNF1right)) :: rest671)) => let val +| ( 286, ( ( _, ( _, CNF1left, CNF1right)) :: rest671)) => let val result = MlyValue.atomic_word (( "cnf" )) in ( LrTable.NT 8, ( result, CNF1left, CNF1right), rest671) end -| ( 281, ( ( _, ( _, INCLUDE1left, INCLUDE1right)) :: rest671)) => +| ( 287, ( ( _, ( _, INCLUDE1left, INCLUDE1right)) :: rest671)) => let val result = MlyValue.atomic_word (( "include" )) in ( LrTable.NT 8, ( result, INCLUDE1left, INCLUDE1right), rest671) end -| ( 282, ( ( _, ( MlyValue.DOLLAR_WORD DOLLAR_WORD, DOLLAR_WORD1left, +| ( 288, ( ( _, ( MlyValue.DOLLAR_WORD DOLLAR_WORD, DOLLAR_WORD1left, DOLLAR_WORD1right)) :: rest671)) => let val result = MlyValue.atomic_defined_word (( DOLLAR_WORD )) - in ( LrTable.NT 144, ( result, DOLLAR_WORD1left, DOLLAR_WORD1right), + in ( LrTable.NT 147, ( result, DOLLAR_WORD1left, DOLLAR_WORD1right), rest671) end -| ( 283, ( ( _, ( MlyValue.DOLLAR_DOLLAR_WORD DOLLAR_DOLLAR_WORD, +| ( 289, ( ( _, ( MlyValue.DOLLAR_DOLLAR_WORD DOLLAR_DOLLAR_WORD, DOLLAR_DOLLAR_WORD1left, DOLLAR_DOLLAR_WORD1right)) :: rest671)) => let val result = MlyValue.atomic_system_word (( DOLLAR_DOLLAR_WORD ) ) - in ( LrTable.NT 145, ( result, DOLLAR_DOLLAR_WORD1left, + in ( LrTable.NT 148, ( result, DOLLAR_DOLLAR_WORD1left, DOLLAR_DOLLAR_WORD1right), rest671) end -| ( 284, ( ( _, ( MlyValue.UNSIGNED_INTEGER UNSIGNED_INTEGER, +| ( 290, ( ( _, ( MlyValue.UNSIGNED_INTEGER UNSIGNED_INTEGER, UNSIGNED_INTEGER1left, UNSIGNED_INTEGER1right)) :: rest671)) => let val result = MlyValue.integer (( UNSIGNED_INTEGER )) in ( LrTable.NT 13, ( result, UNSIGNED_INTEGER1left, UNSIGNED_INTEGER1right), rest671) end -| ( 285, ( ( _, ( MlyValue.SIGNED_INTEGER SIGNED_INTEGER, +| ( 291, ( ( _, ( MlyValue.SIGNED_INTEGER SIGNED_INTEGER, SIGNED_INTEGER1left, SIGNED_INTEGER1right)) :: rest671)) => let val result = MlyValue.integer (( SIGNED_INTEGER )) in ( LrTable.NT 13, ( result, SIGNED_INTEGER1left, SIGNED_INTEGER1right), rest671) end -| ( 286, ( ( _, ( MlyValue.integer integer, integer1left, +| ( 292, ( ( _, ( MlyValue.integer integer, integer1left, integer1right)) :: rest671)) => let val result = MlyValue.number ( ( (Int_num, integer) )) in ( LrTable.NT 11, ( result, integer1left, integer1right), rest671) end -| ( 287, ( ( _, ( MlyValue.REAL REAL, REAL1left, REAL1right)) :: +| ( 293, ( ( _, ( MlyValue.REAL REAL, REAL1left, REAL1right)) :: rest671)) => let val result = MlyValue.number (( (Real_num, REAL) )) in ( LrTable.NT 11, ( result, REAL1left, REAL1right), rest671) end -| ( 288, ( ( _, ( MlyValue.RATIONAL RATIONAL, RATIONAL1left, +| ( 294, ( ( _, ( MlyValue.RATIONAL RATIONAL, RATIONAL1left, RATIONAL1right)) :: rest671)) => let val result = MlyValue.number ( ( (Rat_num, RATIONAL) )) in ( LrTable.NT 11, ( result, RATIONAL1left, RATIONAL1right), rest671 ) end -| ( 289, ( ( _, ( MlyValue.SINGLE_QUOTED SINGLE_QUOTED, +| ( 295, ( ( _, ( MlyValue.SINGLE_QUOTED SINGLE_QUOTED, SINGLE_QUOTED1left, SINGLE_QUOTED1right)) :: rest671)) => let val result = MlyValue.file_name (( SINGLE_QUOTED )) in ( LrTable.NT 17, ( result, SINGLE_QUOTED1left, SINGLE_QUOTED1right diff -r 5278312037f8 -r f26f00cbd573 src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML --- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Tue Sep 03 21:46:41 2013 +0100 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Tue Sep 03 21:46:41 2013 +0100 @@ -86,7 +86,7 @@ | Term_Conditional of tptp_formula * tptp_term * tptp_term | Term_Num of number_kind * string | Term_Distinct_Object of string - | Term_Let of tptp_let list * tptp_term (*FIXME remove list?*) + | Term_Let of tptp_let * tptp_term and tptp_atom = TFF_Typed_Atom of symbol * tptp_type option (*only TFF*) @@ -99,14 +99,14 @@ | Sequent of tptp_formula list * tptp_formula list | Quant of quantifier * (string * tptp_type option) list * tptp_formula | Conditional of tptp_formula * tptp_formula * tptp_formula - | Let of tptp_let list * tptp_formula (*FIXME remove list?*) + | Let of tptp_let * tptp_formula | Atom of tptp_atom | Type_fmla of tptp_type | THF_typing of tptp_formula * tptp_type (*only THF*) and tptp_let = - Let_fmla of (string * tptp_type option) * tptp_formula - | Let_term of (string * tptp_type option) * tptp_term (*only TFF*) + Let_fmla of (string * tptp_type option) list * tptp_formula + | Let_term of (string * tptp_type option) list * tptp_term and tptp_type = Prod_type of tptp_type * tptp_type @@ -234,7 +234,7 @@ | Term_Conditional of tptp_formula * tptp_term * tptp_term | Term_Num of number_kind * string | Term_Distinct_Object of string - | Term_Let of tptp_let list * tptp_term (*FIXME remove list?*) + | Term_Let of tptp_let * tptp_term and tptp_atom = TFF_Typed_Atom of symbol * tptp_type option (*only TFF*) @@ -247,14 +247,14 @@ | Sequent of tptp_formula list * tptp_formula list | Quant of quantifier * (string * tptp_type option) list * tptp_formula | Conditional of tptp_formula * tptp_formula * tptp_formula - | Let of tptp_let list * tptp_formula + | Let of tptp_let * tptp_formula | Atom of tptp_atom | Type_fmla of tptp_type | THF_typing of tptp_formula * tptp_type and tptp_let = - Let_fmla of (string * tptp_type option) * tptp_formula - | Let_term of (string * tptp_type option) * tptp_term + Let_fmla of (string * tptp_type option) list * tptp_formula + | Let_term of (string * tptp_type option) list * tptp_term and tptp_type = Prod_type of tptp_type * tptp_type