var logicProofParser = (function(){
  /*
   * Generated by PEG.js 0.7.0.
   *
   * http://pegjs.majda.cz/
   */

  function quote(s) {
    /*
     * ECMA-262, 5th ed., 7.8.4: All characters may appear literally in a
     * string literal except for the closing quote character, backslash,
     * carriage return, line separator, paragraph separator, and line feed.
     * Any character may appear in the form of an escape sequence.
     *
     * For portability, we also escape escape all control and non-ASCII
     * characters. Note that "\0" and "\v" escape sequences are not used
     * because JSHint does not like the first and IE the second.
     */
     return '"' + s
      .replace(/\\/g, '\\\\')  // backslash
      .replace(/"/g, '\\"')    // closing quote character
      .replace(/\x08/g, '\\b') // backspace
      .replace(/\t/g, '\\t')   // horizontal tab
      .replace(/\n/g, '\\n')   // line feed
      .replace(/\f/g, '\\f')   // form feed
      .replace(/\r/g, '\\r')   // carriage return
      .replace(/[\x00-\x07\x0B\x0E-\x1F\x80-\uFFFF]/g, escape)
      + '"';
  }

  var result = {
    /*
     * Parses the input with a generated parser. If the parsing is successfull,
     * returns a value explicitly or implicitly specified by the grammar from
     * which the parser was generated (see |PEG.buildParser|). If the parsing is
     * unsuccessful, throws |PEG.parser.SyntaxError| describing the error.
     */
    parse: function(input, startRule) {
      var parseFunctions = {
        "expressionTemplate": parse_expressionTemplate,
        "booleanTemplate": parse_booleanTemplate,
        "substitution": parse_substitution,
        "elementTemplate": parse_elementTemplate,
        "variableTemplate": parse_variableTemplate,
        "listOfBooleanTemplates": parse_listOfBooleanTemplates,
        "commaThenBooleanTemplate": parse_commaThenBooleanTemplate,
        "expressionTemplate2": parse_expressionTemplate2,
        "booleanTemplate2": parse_booleanTemplate2,
        "formulaLHS": parse_formulaLHS,
        "listOfVariables": parse_listOfVariables,
        "commaThenVariable": parse_commaThenVariable,
        "expression": parse_expression,
        "listOfExpressions": parse_listOfExpressions,
        "commaThenExpression": parse_commaThenExpression,
        "iffSymbol": parse_iffSymbol,
        "impliesSymbol": parse_impliesSymbol,
        "forAllSymbol": parse_forAllSymbol,
        "existsSymbol": parse_existsSymbol,
        "andSymbol": parse_andSymbol,
        "orSymbol": parse_orSymbol,
        "notSymbol": parse_notSymbol,
        "equalsSymbol": parse_equalsSymbol,
        "lessThanOrEqualsSymbol": parse_lessThanOrEqualsSymbol,
        "greaterThanOrEqualsSymbol": parse_greaterThanOrEqualsSymbol,
        "lessThanSymbol": parse_lessThanSymbol,
        "greaterThanSymbol": parse_greaterThanSymbol,
        "notEqualsSymbol": parse_notEqualsSymbol,
        "membershipSymbol": parse_membershipSymbol,
        "addition": parse_addition,
        "subtraction": parse_subtraction,
        "multiplication": parse_multiplication,
        "division": parse_division,
        "exponentiation": parse_exponentiation,
        "iffFormula": parse_iffFormula,
        "impliesFormula": parse_impliesFormula,
        "quantifierFormula": parse_quantifierFormula,
        "forAllFormula": parse_forAllFormula,
        "existsFormula": parse_existsFormula,
        "boundedForAllFormula": parse_boundedForAllFormula,
        "boundedExistsFormula": parse_boundedExistsFormula,
        "orFormula": parse_orFormula,
        "andFormula": parse_andFormula,
        "andRHS": parse_andRHS,
        "unaryFormula": parse_unaryFormula,
        "notFormula": parse_notFormula,
        "notRHS": parse_notRHS,
        "infixRelationFormula": parse_infixRelationFormula,
        "infixRelationName": parse_infixRelationName,
        "boundableInfixRelationName": parse_boundableInfixRelationName,
        "infixRelationRHS": parse_infixRelationRHS,
        "additionArgument": parse_additionArgument,
        "additionRHS": parse_additionRHS,
        "subtractionArgument": parse_subtractionArgument,
        "subtractionRHS": parse_subtractionRHS,
        "multiplicationArgument": parse_multiplicationArgument,
        "multiplicationRHS": parse_multiplicationRHS,
        "divisionArgument": parse_divisionArgument,
        "divisionRHS": parse_divisionRHS,
        "exponentiationArgument": parse_exponentiationArgument,
        "exponentiationRHS": parse_exponentiationRHS,
        "reducedArgument": parse_reducedArgument,
        "bracketExpression": parse_bracketExpression,
        "prefixFunction": parse_prefixFunction,
        "rangedFunction": parse_rangedFunction,
        "constant": parse_constant,
        "string": parse_string,
        "variable": parse_variable,
        "name": parse_name
      };

      if (startRule !== undefined) {
        if (parseFunctions[startRule] === undefined) {
          throw new Error("Invalid rule name: " + quote(startRule) + ".");
        }
      } else {
        startRule = "expression";
      }

      var pos = 0;
      var reportFailures = 0;
      var rightmostFailuresPos = 0;
      var rightmostFailuresExpected = [];
      var cache = {};

      function padLeft(input, padding, length) {
        var result = input;

        var padLength = length - input.length;
        for (var i = 0; i < padLength; i++) {
          result = padding + result;
        }

        return result;
      }

      function escape(ch) {
        var charCode = ch.charCodeAt(0);
        var escapeChar;
        var length;

        if (charCode <= 0xFF) {
          escapeChar = 'x';
          length = 2;
        } else {
          escapeChar = 'u';
          length = 4;
        }

        return '\\' + escapeChar + padLeft(charCode.toString(16).toUpperCase(), '0', length);
      }

      function matchFailed(failure) {
        if (pos < rightmostFailuresPos) {
          return;
        }

        if (pos > rightmostFailuresPos) {
          rightmostFailuresPos = pos;
          rightmostFailuresExpected = [];
        }

        rightmostFailuresExpected.push(failure);
      }

      function parse_expressionTemplate() {
        var cacheKey = "expressionTemplate@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        result0 = parse_variableTemplate();
        if (result0 === null) {
          result0 = parse_elementTemplate();
          if (result0 === null) {
            result0 = parse_booleanTemplate();
          }
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_booleanTemplate() {
        var cacheKey = "booleanTemplate@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        result0 = parse_expression();
        if (result0 !== null) {
          result1 = [];
          result2 = parse_substitution();
          while (result2 !== null) {
            result1.push(result2);
            result2 = parse_substitution();
          }
          if (result1 !== null) {
            result0 = [result0, result1];
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, expression, subs) {
              return {
                expression: expression,
                substitutions: subs,
                type: 'boolean',
              };
            })(pos0, result0[0], result0[1]);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_substitution() {
        var cacheKey = "substitution@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2, result3, result4;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        if (input.charCodeAt(pos) === 91) {
          result0 = "[";
          pos++;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\"[\"");
          }
        }
        if (result0 !== null) {
          result1 = parse_variable();
          if (result1 !== null) {
            if (input.substr(pos, 2) === "->") {
              result2 = "->";
              pos += 2;
            } else {
              result2 = null;
              if (reportFailures === 0) {
                matchFailed("\"->\"");
              }
            }
            if (result2 !== null) {
              result3 = parse_expression();
              if (result3 !== null) {
                if (input.charCodeAt(pos) === 93) {
                  result4 = "]";
                  pos++;
                } else {
                  result4 = null;
                  if (reportFailures === 0) {
                    matchFailed("\"]\"");
                  }
                }
                if (result4 !== null) {
                  result0 = [result0, result1, result2, result3, result4];
                } else {
                  result0 = null;
                  pos = pos1;
                }
              } else {
                result0 = null;
                pos = pos1;
              }
            } else {
              result0 = null;
              pos = pos1;
            }
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, from, to) {
              var output = {};
              output[from.top_operator_name] = to;
              return output;
            })(pos0, result0[1], result0[3]);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_elementTemplate() {
        var cacheKey = "elementTemplate@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        if (input.substr(pos, 2) === "{{") {
          result0 = "{{";
          pos += 2;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\"{{\"");
          }
        }
        if (result0 !== null) {
          result1 = parse_additionArgument();
          if (result1 !== null) {
            if (input.substr(pos, 10) === "|element}}") {
              result2 = "|element}}";
              pos += 10;
            } else {
              result2 = null;
              if (reportFailures === 0) {
                matchFailed("\"|element}}\"");
              }
            }
            if (result2 !== null) {
              result0 = [result0, result1, result2];
            } else {
              result0 = null;
              pos = pos1;
            }
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, element) {
              return {
                expression: element,
                substitutions: [],
                type: 'element',
              };
            })(pos0, result0[1]);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_variableTemplate() {
        var cacheKey = "variableTemplate@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        if (input.substr(pos, 2) === "{{") {
          result0 = "{{";
          pos += 2;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\"{{\"");
          }
        }
        if (result0 !== null) {
          result1 = parse_variable();
          if (result1 !== null) {
            if (input.substr(pos, 11) === "|variable}}") {
              result2 = "|variable}}";
              pos += 11;
            } else {
              result2 = null;
              if (reportFailures === 0) {
                matchFailed("\"|variable}}\"");
              }
            }
            if (result2 !== null) {
              result0 = [result0, result1, result2];
            } else {
              result0 = null;
              pos = pos1;
            }
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, variable) {
              return {
                expression: variable,
                substitutions: [],
                type: 'element',
                kind: 'variable'
              };
            })(pos0, result0[1]);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_listOfBooleanTemplates() {
        var cacheKey = "listOfBooleanTemplates@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        result0 = parse_booleanTemplate();
        result0 = result0 !== null ? result0 : "";
        if (result0 !== null) {
          result1 = [];
          result2 = parse_commaThenBooleanTemplate();
          while (result2 !== null) {
            result1.push(result2);
            result2 = parse_commaThenBooleanTemplate();
          }
          if (result1 !== null) {
            result0 = [result0, result1];
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, av, avList) {
              var result = (av === '') ? [] : [av];
              for (var i = 0; i < avList.length; i++) {
                result.push(avList[i]);
              }
              return result;
            })(pos0, result0[0], result0[1]);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_commaThenBooleanTemplate() {
        var cacheKey = "commaThenBooleanTemplate@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        if (input.charCodeAt(pos) === 44) {
          result0 = ",";
          pos++;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\",\"");
          }
        }
        if (result0 !== null) {
          result1 = parse_booleanTemplate();
          if (result1 !== null) {
            result0 = [result0, result1];
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, av) { return av; })(pos0, result0[1]);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_expressionTemplate2() {
        var cacheKey = "expressionTemplate2@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        result0 = parse_elementTemplate();
        if (result0 === null) {
          result0 = parse_variableTemplate();
          if (result0 === null) {
            result0 = parse_booleanTemplate2();
          }
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_booleanTemplate2() {
        var cacheKey = "booleanTemplate2@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2, result3;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        if (input.substr(pos, 2) === "{{") {
          result0 = "{{";
          pos += 2;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\"{{\"");
          }
        }
        if (result0 !== null) {
          result1 = parse_expression();
          if (result1 !== null) {
            result2 = [];
            result3 = parse_substitution();
            while (result3 !== null) {
              result2.push(result3);
              result3 = parse_substitution();
            }
            if (result2 !== null) {
              if (input.substr(pos, 2) === "}}") {
                result3 = "}}";
                pos += 2;
              } else {
                result3 = null;
                if (reportFailures === 0) {
                  matchFailed("\"}}\"");
                }
              }
              if (result3 !== null) {
                result0 = [result0, result1, result2, result3];
              } else {
                result0 = null;
                pos = pos1;
              }
            } else {
              result0 = null;
              pos = pos1;
            }
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, expression, subs) {
              return {
                expression: expression,
                substitutions: subs,
                type: 'boolean',
              };
            })(pos0, result0[1], result0[2]);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_formulaLHS() {
        var cacheKey = "formulaLHS@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2, result3;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        result0 = parse_name();
        if (result0 !== null) {
          if (input.charCodeAt(pos) === 40) {
            result1 = "(";
            pos++;
          } else {
            result1 = null;
            if (reportFailures === 0) {
              matchFailed("\"(\"");
            }
          }
          if (result1 !== null) {
            result2 = parse_listOfVariables();
            if (result2 !== null) {
              if (input.charCodeAt(pos) === 41) {
                result3 = ")";
                pos++;
              } else {
                result3 = null;
                if (reportFailures === 0) {
                  matchFailed("\")\"");
                }
              }
              if (result3 !== null) {
                result0 = [result0, result1, result2, result3];
              } else {
                result0 = null;
                pos = pos1;
              }
            } else {
              result0 = null;
              pos = pos1;
            }
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, name, arguments) {
              return {
                top_kind_name: 'binary_function',
                top_operator_name: name,
                arguments: arguments,
                dummies:[]
              }
            })(pos0, result0[0], result0[2]);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_listOfVariables() {
        var cacheKey = "listOfVariables@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        result0 = parse_variable();
        result0 = result0 !== null ? result0 : "";
        if (result0 !== null) {
          result1 = [];
          result2 = parse_commaThenVariable();
          while (result2 !== null) {
            result1.push(result2);
            result2 = parse_commaThenVariable();
          }
          if (result1 !== null) {
            result0 = [result0, result1];
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, av, avList) {
              var result = (av === '') ? [] : [av];
              for (var i = 0; i < avList.length; i++) {
                result.push(avList[i]);
              }
              return result;
            })(pos0, result0[0], result0[1]);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_commaThenVariable() {
        var cacheKey = "commaThenVariable@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        if (input.charCodeAt(pos) === 44) {
          result0 = ",";
          pos++;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\",\"");
          }
        }
        if (result0 !== null) {
          result1 = parse_variable();
          if (result1 !== null) {
            result0 = [result0, result1];
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, av) { return av; })(pos0, result0[1]);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_expression() {
        var cacheKey = "expression@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;
        var pos0;

        pos0 = pos;
        result0 = parse_iffFormula();
        if (result0 !== null) {
          result0 = (function(offset, a) {return a;})(pos0, result0);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_listOfExpressions() {
        var cacheKey = "listOfExpressions@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        result0 = parse_expression();
        result0 = result0 !== null ? result0 : "";
        if (result0 !== null) {
          result1 = [];
          result2 = parse_commaThenExpression();
          while (result2 !== null) {
            result1.push(result2);
            result2 = parse_commaThenExpression();
          }
          if (result1 !== null) {
            result0 = [result0, result1];
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, av, avList) {
              var result = (av === '') ? []: [av];
              for (var i = 0; i < avList.length; i++) {
                result.push(avList[i]);
              }
              return result;
            })(pos0, result0[0], result0[1]);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_commaThenExpression() {
        var cacheKey = "commaThenExpression@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        if (input.charCodeAt(pos) === 44) {
          result0 = ",";
          pos++;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\",\"");
          }
        }
        if (result0 !== null) {
          result1 = parse_expression();
          if (result1 !== null) {
            result0 = [result0, result1];
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, av) { return av; })(pos0, result0[1]);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_iffSymbol() {
        var cacheKey = "iffSymbol@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        if (input.substr(pos, 3) === "<=>") {
          result0 = "<=>";
          pos += 3;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\"<=>\"");
          }
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_impliesSymbol() {
        var cacheKey = "impliesSymbol@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        if (input.substr(pos, 2) === "=>") {
          result0 = "=>";
          pos += 2;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\"=>\"");
          }
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_forAllSymbol() {
        var cacheKey = "forAllSymbol@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        if (input.charCodeAt(pos) === 8704) {
          result0 = "\u2200";
          pos++;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\"\\u2200\"");
          }
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_existsSymbol() {
        var cacheKey = "existsSymbol@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        if (input.charCodeAt(pos) === 8707) {
          result0 = "\u2203";
          pos++;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\"\\u2203\"");
          }
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_andSymbol() {
        var cacheKey = "andSymbol@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        if (input.charCodeAt(pos) === 8743) {
          result0 = "\u2227";
          pos++;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\"\\u2227\"");
          }
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_orSymbol() {
        var cacheKey = "orSymbol@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        if (input.charCodeAt(pos) === 8744) {
          result0 = "\u2228";
          pos++;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\"\\u2228\"");
          }
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_notSymbol() {
        var cacheKey = "notSymbol@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        if (input.charCodeAt(pos) === 126) {
          result0 = "~";
          pos++;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\"~\"");
          }
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_equalsSymbol() {
        var cacheKey = "equalsSymbol@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;
        var pos0;

        pos0 = pos;
        if (input.charCodeAt(pos) === 61) {
          result0 = "=";
          pos++;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\"=\"");
          }
        }
        if (result0 !== null) {
          result0 = (function(offset) {return 'equals'})(pos0);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_lessThanOrEqualsSymbol() {
        var cacheKey = "lessThanOrEqualsSymbol@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;
        var pos0;

        pos0 = pos;
        if (input.substr(pos, 2) === "<=") {
          result0 = "<=";
          pos += 2;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\"<=\"");
          }
        }
        if (result0 !== null) {
          result0 = (function(offset) {return 'less_than_or_equals'})(pos0);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_greaterThanOrEqualsSymbol() {
        var cacheKey = "greaterThanOrEqualsSymbol@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;
        var pos0;

        pos0 = pos;
        if (input.substr(pos, 2) === ">=") {
          result0 = ">=";
          pos += 2;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\">=\"");
          }
        }
        if (result0 !== null) {
          result0 = (function(offset) {return 'greater_than_or_equals'})(pos0);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_lessThanSymbol() {
        var cacheKey = "lessThanSymbol@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;
        var pos0;

        pos0 = pos;
        if (input.charCodeAt(pos) === 60) {
          result0 = "<";
          pos++;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\"<\"");
          }
        }
        if (result0 !== null) {
          result0 = (function(offset) {return 'less_than'})(pos0);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_greaterThanSymbol() {
        var cacheKey = "greaterThanSymbol@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;
        var pos0;

        pos0 = pos;
        if (input.charCodeAt(pos) === 62) {
          result0 = ">";
          pos++;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\">\"");
          }
        }
        if (result0 !== null) {
          result0 = (function(offset) {return 'greater_than'})(pos0);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_notEqualsSymbol() {
        var cacheKey = "notEqualsSymbol@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;
        var pos0;

        pos0 = pos;
        if (input.substr(pos, 2) === "!=") {
          result0 = "!=";
          pos += 2;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\"!=\"");
          }
        }
        if (result0 !== null) {
          result0 = (function(offset) {return 'not_equals'})(pos0);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_membershipSymbol() {
        var cacheKey = "membershipSymbol@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;
        var pos0;

        pos0 = pos;
        if (input.charCodeAt(pos) === 8712) {
          result0 = "\u2208";
          pos++;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\"\\u2208\"");
          }
        }
        if (result0 !== null) {
          result0 = (function(offset) {return 'is_in';})(pos0);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_addition() {
        var cacheKey = "addition@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        if (input.charCodeAt(pos) === 43) {
          result0 = "+";
          pos++;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\"+\"");
          }
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_subtraction() {
        var cacheKey = "subtraction@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        if (input.charCodeAt(pos) === 45) {
          result0 = "-";
          pos++;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\"-\"");
          }
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_multiplication() {
        var cacheKey = "multiplication@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        if (input.charCodeAt(pos) === 42) {
          result0 = "*";
          pos++;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\"*\"");
          }
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_division() {
        var cacheKey = "division@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        if (input.charCodeAt(pos) === 47) {
          result0 = "/";
          pos++;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\"/\"");
          }
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_exponentiation() {
        var cacheKey = "exponentiation@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        if (input.charCodeAt(pos) === 94) {
          result0 = "^";
          pos++;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\"^\"");
          }
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_iffFormula() {
        var cacheKey = "iffFormula@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        result0 = parse_impliesFormula();
        if (result0 !== null) {
          result1 = parse_iffSymbol();
          if (result1 !== null) {
            result2 = parse_iffFormula();
            if (result2 !== null) {
              result0 = [result0, result1, result2];
            } else {
              result0 = null;
              pos = pos1;
            }
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, left, right) {
              return {
                top_kind_name: 'binary_connective',
                top_operator_name: 'iff',
                arguments: [left, right],
                dummies: []
              }
            })(pos0, result0[0], result0[2]);
        }
        if (result0 === null) {
          pos = pos0;
        }
        if (result0 === null) {
          result0 = parse_impliesFormula();
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_impliesFormula() {
        var cacheKey = "impliesFormula@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        result0 = parse_quantifierFormula();
        if (result0 !== null) {
          result1 = parse_impliesSymbol();
          if (result1 !== null) {
            result2 = parse_impliesFormula();
            if (result2 !== null) {
              result0 = [result0, result1, result2];
            } else {
              result0 = null;
              pos = pos1;
            }
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, left, right) {
              return {
                top_kind_name: 'binary_connective',
                top_operator_name: 'implies',
                arguments: [left, right],
                dummies: []
              }
            })(pos0, result0[0], result0[2]);
        }
        if (result0 === null) {
          pos = pos0;
        }
        if (result0 === null) {
          result0 = parse_quantifierFormula();
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_quantifierFormula() {
        var cacheKey = "quantifierFormula@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        result0 = parse_forAllFormula();
        if (result0 === null) {
          result0 = parse_orFormula();
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_forAllFormula() {
        var cacheKey = "forAllFormula@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2, result3;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        result0 = parse_forAllSymbol();
        if (result0 !== null) {
          result1 = parse_variable();
          if (result1 !== null) {
            if (input.charCodeAt(pos) === 46) {
              result2 = ".";
              pos++;
            } else {
              result2 = null;
              if (reportFailures === 0) {
                matchFailed("\".\"");
              }
            }
            result2 = result2 !== null ? result2 : "";
            if (result2 !== null) {
              result3 = parse_quantifierFormula();
              if (result3 !== null) {
                result0 = [result0, result1, result2, result3];
              } else {
                result0 = null;
                pos = pos1;
              }
            } else {
              result0 = null;
              pos = pos1;
            }
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, left, right) {
              return {
                top_kind_name: 'quantifier',
                top_operator_name: 'for_all',
                arguments: [right],
                dummies: [left]
              };
            })(pos0, result0[1], result0[3]);
        }
        if (result0 === null) {
          pos = pos0;
        }
        if (result0 === null) {
          result0 = parse_existsFormula();
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_existsFormula() {
        var cacheKey = "existsFormula@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2, result3;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        result0 = parse_existsSymbol();
        if (result0 !== null) {
          result1 = parse_variable();
          if (result1 !== null) {
            if (input.charCodeAt(pos) === 46) {
              result2 = ".";
              pos++;
            } else {
              result2 = null;
              if (reportFailures === 0) {
                matchFailed("\".\"");
              }
            }
            result2 = result2 !== null ? result2 : "";
            if (result2 !== null) {
              result3 = parse_quantifierFormula();
              if (result3 !== null) {
                result0 = [result0, result1, result2, result3];
              } else {
                result0 = null;
                pos = pos1;
              }
            } else {
              result0 = null;
              pos = pos1;
            }
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, left, right) {
              return {
                top_kind_name: 'quantifier',
                top_operator_name: 'exists',
                arguments: [right],
                dummies: [left]
              };
            })(pos0, result0[1], result0[3]);
        }
        if (result0 === null) {
          pos = pos0;
        }
        if (result0 === null) {
          result0 = parse_boundedForAllFormula();
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_boundedForAllFormula() {
        var cacheKey = "boundedForAllFormula@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2, result3, result4, result5;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        result0 = parse_forAllSymbol();
        if (result0 !== null) {
          result1 = parse_variable();
          if (result1 !== null) {
            result2 = parse_boundableInfixRelationName();
            if (result2 !== null) {
              result3 = parse_additionArgument();
              if (result3 !== null) {
                if (input.charCodeAt(pos) === 46) {
                  result4 = ".";
                  pos++;
                } else {
                  result4 = null;
                  if (reportFailures === 0) {
                    matchFailed("\".\"");
                  }
                }
                result4 = result4 !== null ? result4 : "";
                if (result4 !== null) {
                  result5 = parse_quantifierFormula();
                  if (result5 !== null) {
                    result0 = [result0, result1, result2, result3, result4, result5];
                  } else {
                    result0 = null;
                    pos = pos1;
                  }
                } else {
                  result0 = null;
                  pos = pos1;
                }
              } else {
                result0 = null;
                pos = pos1;
              }
            } else {
              result0 = null;
              pos = pos1;
            }
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, k, relation, n, A) {
              return {
                top_kind_name: 'bounded_quantifier',
                top_operator_name: 'bounded_for_all',
                arguments: [{
                  top_kind_name: 'binary_relation',
                  top_operator_name: relation,
                  arguments: [k, n],
                  dummies: []
                }, A],
                dummies: [k]
              };
            })(pos0, result0[1], result0[2], result0[3], result0[5]);
        }
        if (result0 === null) {
          pos = pos0;
        }
        if (result0 === null) {
          result0 = parse_boundedExistsFormula();
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_boundedExistsFormula() {
        var cacheKey = "boundedExistsFormula@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2, result3, result4, result5;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        result0 = parse_existsSymbol();
        if (result0 !== null) {
          result1 = parse_variable();
          if (result1 !== null) {
            result2 = parse_boundableInfixRelationName();
            if (result2 !== null) {
              result3 = parse_additionArgument();
              if (result3 !== null) {
                if (input.charCodeAt(pos) === 46) {
                  result4 = ".";
                  pos++;
                } else {
                  result4 = null;
                  if (reportFailures === 0) {
                    matchFailed("\".\"");
                  }
                }
                result4 = result4 !== null ? result4 : "";
                if (result4 !== null) {
                  result5 = parse_quantifierFormula();
                  if (result5 !== null) {
                    result0 = [result0, result1, result2, result3, result4, result5];
                  } else {
                    result0 = null;
                    pos = pos1;
                  }
                } else {
                  result0 = null;
                  pos = pos1;
                }
              } else {
                result0 = null;
                pos = pos1;
              }
            } else {
              result0 = null;
              pos = pos1;
            }
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, k, relation, n, A) {
              return {
                top_kind_name: 'bounded_quantifier',
                top_operator_name: 'bounded_exists',
                arguments: [{
                  top_kind_name: 'binary_relation',
                  top_operator_name: relation,
                  arguments: [k, n],
                  dummies: []
                }, A],
                dummies: [k]
              };
            })(pos0, result0[1], result0[2], result0[3], result0[5]);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_orFormula() {
        var cacheKey = "orFormula@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        result0 = parse_andFormula();
        if (result0 !== null) {
          result1 = parse_orSymbol();
          if (result1 !== null) {
            result2 = parse_quantifierFormula();
            if (result2 !== null) {
              result0 = [result0, result1, result2];
            } else {
              result0 = null;
              pos = pos1;
            }
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, left, right) {
              return {
                top_kind_name: 'binary_connective',
                top_operator_name: 'or',
                arguments: [left, right],
                dummies: []
              };
            })(pos0, result0[0], result0[2]);
        }
        if (result0 === null) {
          pos = pos0;
        }
        if (result0 === null) {
          result0 = parse_andFormula();
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_andFormula() {
        var cacheKey = "andFormula@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        result0 = parse_unaryFormula();
        if (result0 !== null) {
          result1 = parse_andSymbol();
          if (result1 !== null) {
            result2 = parse_andRHS();
            if (result2 !== null) {
              result0 = [result0, result1, result2];
            } else {
              result0 = null;
              pos = pos1;
            }
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, left, right) {
              return {
                top_kind_name: 'binary_connective',
                top_operator_name: 'and',
                arguments: [left, right],
                dummies: []
              }
            })(pos0, result0[0], result0[2]);
        }
        if (result0 === null) {
          pos = pos0;
        }
        if (result0 === null) {
          result0 = parse_unaryFormula();
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_andRHS() {
        var cacheKey = "andRHS@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        result0 = parse_forAllFormula();
        if (result0 === null) {
          result0 = parse_andFormula();
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_unaryFormula() {
        var cacheKey = "unaryFormula@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        result0 = parse_notFormula();
        if (result0 === null) {
          result0 = parse_infixRelationFormula();
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_notFormula() {
        var cacheKey = "notFormula@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        result0 = parse_notSymbol();
        if (result0 !== null) {
          result1 = parse_notRHS();
          if (result1 !== null) {
            result0 = [result0, result1];
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, right) {
              return {
                top_kind_name: 'unary_connective',
                top_operator_name: 'not',
                arguments: [right],
                dummies: []
              }
            })(pos0, result0[1]);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_notRHS() {
        var cacheKey = "notRHS@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        result0 = parse_forAllFormula();
        if (result0 === null) {
          result0 = parse_unaryFormula();
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_infixRelationFormula() {
        var cacheKey = "infixRelationFormula@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        result0 = parse_additionArgument();
        if (result0 !== null) {
          result1 = parse_infixRelationName();
          if (result1 !== null) {
            result2 = parse_infixRelationRHS();
            if (result2 !== null) {
              result0 = [result0, result1, result2];
            } else {
              result0 = null;
              pos = pos1;
            }
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, left, name, right) {
               return {
                top_kind_name: 'binary_relation',
                top_operator_name: name,
                arguments: [left, right],
                dummies: []
               }
            })(pos0, result0[0], result0[1], result0[2]);
        }
        if (result0 === null) {
          pos = pos0;
        }
        if (result0 === null) {
          result0 = parse_additionArgument();
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_infixRelationName() {
        var cacheKey = "infixRelationName@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        result0 = parse_equalsSymbol();
        if (result0 === null) {
          result0 = parse_lessThanOrEqualsSymbol();
          if (result0 === null) {
            result0 = parse_greaterThanOrEqualsSymbol();
            if (result0 === null) {
              result0 = parse_lessThanSymbol();
              if (result0 === null) {
                result0 = parse_greaterThanSymbol();
                if (result0 === null) {
                  result0 = parse_notEqualsSymbol();
                  if (result0 === null) {
                    result0 = parse_membershipSymbol();
                  }
                }
              }
            }
          }
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_boundableInfixRelationName() {
        var cacheKey = "boundableInfixRelationName@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        result0 = parse_lessThanOrEqualsSymbol();
        if (result0 === null) {
          result0 = parse_lessThanSymbol();
          if (result0 === null) {
            result0 = parse_membershipSymbol();
          }
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_infixRelationRHS() {
        var cacheKey = "infixRelationRHS@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        result0 = parse_forAllFormula();
        if (result0 === null) {
          result0 = parse_notFormula();
          if (result0 === null) {
            result0 = parse_infixRelationFormula();
          }
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_additionArgument() {
        var cacheKey = "additionArgument@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        result0 = parse_subtractionArgument();
        if (result0 !== null) {
          result1 = parse_addition();
          if (result1 !== null) {
            result2 = parse_additionRHS();
            if (result2 !== null) {
              result0 = [result0, result1, result2];
            } else {
              result0 = null;
              pos = pos1;
            }
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, left, right) {
              return {
                top_kind_name: 'binary_function',
                top_operator_name: 'addition',
                arguments: [left, right],
                dummies: []
              }
            })(pos0, result0[0], result0[2]);
        }
        if (result0 === null) {
          pos = pos0;
        }
        if (result0 === null) {
          result0 = parse_subtractionArgument();
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_additionRHS() {
        var cacheKey = "additionRHS@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        result0 = parse_forAllFormula();
        if (result0 === null) {
          result0 = parse_notFormula();
          if (result0 === null) {
            result0 = parse_additionArgument();
          }
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_subtractionArgument() {
        var cacheKey = "subtractionArgument@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        result0 = parse_multiplicationArgument();
        if (result0 !== null) {
          result1 = parse_subtraction();
          if (result1 !== null) {
            result2 = parse_subtractionRHS();
            if (result2 !== null) {
              result0 = [result0, result1, result2];
            } else {
              result0 = null;
              pos = pos1;
            }
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, left, right) {
              return {
                top_kind_name: 'binary_function',
                top_operator_name: 'subtraction',
                arguments: [left, right],
                dummies: []
              }
            })(pos0, result0[0], result0[2]);
        }
        if (result0 === null) {
          pos = pos0;
        }
        if (result0 === null) {
          result0 = parse_multiplicationArgument();
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_subtractionRHS() {
        var cacheKey = "subtractionRHS@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        result0 = parse_forAllFormula();
        if (result0 === null) {
          result0 = parse_notFormula();
          if (result0 === null) {
            result0 = parse_subtractionArgument();
          }
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_multiplicationArgument() {
        var cacheKey = "multiplicationArgument@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        result0 = parse_divisionArgument();
        if (result0 !== null) {
          result1 = parse_multiplication();
          if (result1 !== null) {
            result2 = parse_multiplicationRHS();
            if (result2 !== null) {
              result0 = [result0, result1, result2];
            } else {
              result0 = null;
              pos = pos1;
            }
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, left, right) {
              return {
                top_kind_name: 'binary_function',
                top_operator_name: 'multiplication',
                arguments: [left, right],
                dummies: []
              }
            })(pos0, result0[0], result0[2]);
        }
        if (result0 === null) {
          pos = pos0;
        }
        if (result0 === null) {
          result0 = parse_divisionArgument();
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_multiplicationRHS() {
        var cacheKey = "multiplicationRHS@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        result0 = parse_forAllFormula();
        if (result0 === null) {
          result0 = parse_notFormula();
          if (result0 === null) {
            result0 = parse_multiplicationArgument();
          }
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_divisionArgument() {
        var cacheKey = "divisionArgument@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        result0 = parse_exponentiationArgument();
        if (result0 !== null) {
          result1 = parse_division();
          if (result1 !== null) {
            result2 = parse_divisionRHS();
            if (result2 !== null) {
              result0 = [result0, result1, result2];
            } else {
              result0 = null;
              pos = pos1;
            }
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, left, right) {
              return {
                top_kind_name: 'binary_function',
                top_operator_name: 'division',
                arguments: [left, right],
                dummies: []
              }
            })(pos0, result0[0], result0[2]);
        }
        if (result0 === null) {
          pos = pos0;
        }
        if (result0 === null) {
          result0 = parse_exponentiationArgument();
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_divisionRHS() {
        var cacheKey = "divisionRHS@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        result0 = parse_forAllFormula();
        if (result0 === null) {
          result0 = parse_notFormula();
          if (result0 === null) {
            result0 = parse_divisionArgument();
          }
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_exponentiationArgument() {
        var cacheKey = "exponentiationArgument@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        result0 = parse_reducedArgument();
        if (result0 !== null) {
          result1 = parse_exponentiation();
          if (result1 !== null) {
            result2 = parse_exponentiationRHS();
            if (result2 !== null) {
              result0 = [result0, result1, result2];
            } else {
              result0 = null;
              pos = pos1;
            }
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, left, right) {
              return {
                top_kind_name: 'binary_function',
                top_operator_name: 'exponentiation',
                arguments: [left, right],
                dummies: []
              }
            })(pos0, result0[0], result0[2]);
        }
        if (result0 === null) {
          pos = pos0;
        }
        if (result0 === null) {
          result0 = parse_reducedArgument();
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_exponentiationRHS() {
        var cacheKey = "exponentiationRHS@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        result0 = parse_forAllFormula();
        if (result0 === null) {
          result0 = parse_notFormula();
          if (result0 === null) {
            result0 = parse_exponentiationArgument();
          }
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_reducedArgument() {
        var cacheKey = "reducedArgument@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;

        result0 = parse_bracketExpression();
        if (result0 === null) {
          result0 = parse_prefixFunction();
          if (result0 === null) {
            result0 = parse_constant();
            if (result0 === null) {
              result0 = parse_variable();
            }
          }
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_bracketExpression() {
        var cacheKey = "bracketExpression@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        if (input.charCodeAt(pos) === 40) {
          result0 = "(";
          pos++;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\"(\"");
          }
        }
        if (result0 !== null) {
          result1 = parse_expression();
          if (result1 !== null) {
            if (input.charCodeAt(pos) === 41) {
              result2 = ")";
              pos++;
            } else {
              result2 = null;
              if (reportFailures === 0) {
                matchFailed("\")\"");
              }
            }
            if (result2 !== null) {
              result0 = [result0, result1, result2];
            } else {
              result0 = null;
              pos = pos1;
            }
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, e) {return e;})(pos0, result0[1]);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_prefixFunction() {
        var cacheKey = "prefixFunction@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2, result3;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        result0 = parse_name();
        if (result0 !== null) {
          if (input.charCodeAt(pos) === 40) {
            result1 = "(";
            pos++;
          } else {
            result1 = null;
            if (reportFailures === 0) {
              matchFailed("\"(\"");
            }
          }
          if (result1 !== null) {
            result2 = parse_listOfExpressions();
            if (result2 !== null) {
              if (input.charCodeAt(pos) === 41) {
                result3 = ")";
                pos++;
              } else {
                result3 = null;
                if (reportFailures === 0) {
                  matchFailed("\")\"");
                }
              }
              if (result3 !== null) {
                result0 = [result0, result1, result2, result3];
              } else {
                result0 = null;
                pos = pos1;
              }
            } else {
              result0 = null;
              pos = pos1;
            }
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, name, arguments) {
              return {
                top_kind_name: 'prefix_function',
                top_operator_name: name,
                arguments: arguments,
                dummies: []
              }
            })(pos0, result0[0], result0[2]);
        }
        if (result0 === null) {
          pos = pos0;
        }
        if (result0 === null) {
          result0 = parse_rangedFunction();
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_rangedFunction() {
        var cacheKey = "rangedFunction@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2, result3, result4, result5, result6, result7;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        result0 = parse_name();
        if (result0 !== null) {
          if (input.charCodeAt(pos) === 123) {
            result1 = "{";
            pos++;
          } else {
            result1 = null;
            if (reportFailures === 0) {
              matchFailed("\"{\"");
            }
          }
          if (result1 !== null) {
            result2 = parse_variable();
            if (result2 !== null) {
              result3 = parse_boundableInfixRelationName();
              if (result3 !== null) {
                result4 = parse_additionArgument();
                if (result4 !== null) {
                  if (input.charCodeAt(pos) === 124) {
                    result5 = "|";
                    pos++;
                  } else {
                    result5 = null;
                    if (reportFailures === 0) {
                      matchFailed("\"|\"");
                    }
                  }
                  if (result5 !== null) {
                    result6 = parse_expression();
                    if (result6 !== null) {
                      if (input.charCodeAt(pos) === 125) {
                        result7 = "}";
                        pos++;
                      } else {
                        result7 = null;
                        if (reportFailures === 0) {
                          matchFailed("\"}\"");
                        }
                      }
                      if (result7 !== null) {
                        result0 = [result0, result1, result2, result3, result4, result5, result6, result7];
                      } else {
                        result0 = null;
                        pos = pos1;
                      }
                    } else {
                      result0 = null;
                      pos = pos1;
                    }
                  } else {
                    result0 = null;
                    pos = pos1;
                  }
                } else {
                  result0 = null;
                  pos = pos1;
                }
              } else {
                result0 = null;
                pos = pos1;
              }
            } else {
              result0 = null;
              pos = pos1;
            }
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, name, k, relation, n, A) {
              return {
                top_kind_name: 'ranged_function',
                top_operator_name: name,
                arguments: [{
                  top_kind_name: 'binary_relation',
                  top_operator_name: relation,
                  arguments: [k, n],
                  dummies: []
                }, A],
                dummies: [k]
              };
            })(pos0, result0[0], result0[2], result0[3], result0[4], result0[6]);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_constant() {
        var cacheKey = "constant@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1;
        var pos0;

        pos0 = pos;
        if (/^[0-9]/.test(input.charAt(pos))) {
          result1 = input.charAt(pos);
          pos++;
        } else {
          result1 = null;
          if (reportFailures === 0) {
            matchFailed("[0-9]");
          }
        }
        if (result1 !== null) {
          result0 = [];
          while (result1 !== null) {
            result0.push(result1);
            if (/^[0-9]/.test(input.charAt(pos))) {
              result1 = input.charAt(pos);
              pos++;
            } else {
              result1 = null;
              if (reportFailures === 0) {
                matchFailed("[0-9]");
              }
            }
          }
        } else {
          result0 = null;
        }
        if (result0 !== null) {
          result0 = (function(offset, digits) {
              return {
                top_kind_name: 'constant',
                top_operator_name: parseInt(digits.join(""), 10),
                arguments: [],
                dummies: [],
                type: 'integer'
              };
            })(pos0, result0);
        }
        if (result0 === null) {
          pos = pos0;
        }
        if (result0 === null) {
          result0 = parse_string();
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_string() {
        var cacheKey = "string@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        if (input.charCodeAt(pos) === 39) {
          result0 = "'";
          pos++;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("\"'\"");
          }
        }
        if (result0 !== null) {
          result1 = [];
          if (/^[a-zA-Z0-9_]/.test(input.charAt(pos))) {
            result2 = input.charAt(pos);
            pos++;
          } else {
            result2 = null;
            if (reportFailures === 0) {
              matchFailed("[a-zA-Z0-9_]");
            }
          }
          while (result2 !== null) {
            result1.push(result2);
            if (/^[a-zA-Z0-9_]/.test(input.charAt(pos))) {
              result2 = input.charAt(pos);
              pos++;
            } else {
              result2 = null;
              if (reportFailures === 0) {
                matchFailed("[a-zA-Z0-9_]");
              }
            }
          }
          if (result1 !== null) {
            if (input.charCodeAt(pos) === 39) {
              result2 = "'";
              pos++;
            } else {
              result2 = null;
              if (reportFailures === 0) {
                matchFailed("\"'\"");
              }
            }
            if (result2 !== null) {
              result0 = [result0, result1, result2];
            } else {
              result0 = null;
              pos = pos1;
            }
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, characters) {
              return {
                top_kind_name: 'constant',
                top_operator_name: '\'' + characters.join('') + '\'',
                arguments: [],
                dummies: [],
                type: 'string'
              }
            })(pos0, result0[1]);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_variable() {
        var cacheKey = "variable@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0;
        var pos0;

        pos0 = pos;
        result0 = parse_name();
        if (result0 !== null) {
          result0 = (function(offset, name) {
              return {
                top_kind_name: 'variable',
                top_operator_name: name,
                arguments: [],
                dummies: []
              };
            })(pos0, result0);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }

      function parse_name() {
        var cacheKey = "name@" + pos;
        var cachedResult = cache[cacheKey];
        if (cachedResult) {
          pos = cachedResult.nextPos;
          return cachedResult.result;
        }

        var result0, result1, result2;
        var pos0, pos1;

        pos0 = pos;
        pos1 = pos;
        if (/^[A-Za-z]/.test(input.charAt(pos))) {
          result0 = input.charAt(pos);
          pos++;
        } else {
          result0 = null;
          if (reportFailures === 0) {
            matchFailed("[A-Za-z]");
          }
        }
        if (result0 !== null) {
          result1 = [];
          if (/^[A-Za-z0-9_]/.test(input.charAt(pos))) {
            result2 = input.charAt(pos);
            pos++;
          } else {
            result2 = null;
            if (reportFailures === 0) {
              matchFailed("[A-Za-z0-9_]");
            }
          }
          while (result2 !== null) {
            result1.push(result2);
            if (/^[A-Za-z0-9_]/.test(input.charAt(pos))) {
              result2 = input.charAt(pos);
              pos++;
            } else {
              result2 = null;
              if (reportFailures === 0) {
                matchFailed("[A-Za-z0-9_]");
              }
            }
          }
          if (result1 !== null) {
            result0 = [result0, result1];
          } else {
            result0 = null;
            pos = pos1;
          }
        } else {
          result0 = null;
          pos = pos1;
        }
        if (result0 !== null) {
          result0 = (function(offset, first, middle) {
              return first + middle.join('');
            })(pos0, result0[0], result0[1]);
        }
        if (result0 === null) {
          pos = pos0;
        }

        cache[cacheKey] = {
          nextPos: pos,
          result:  result0
        };
        return result0;
      }


      function cleanupExpected(expected) {
        expected.sort();

        var lastExpected = null;
        var cleanExpected = [];
        for (var i = 0; i < expected.length; i++) {
          if (expected[i] !== lastExpected) {
            cleanExpected.push(expected[i]);
            lastExpected = expected[i];
          }
        }
        return cleanExpected;
      }

      function computeErrorPosition() {
        /*
         * The first idea was to use |String.split| to break the input up to the
         * error position along newlines and derive the line and column from
         * there. However IE's |split| implementation is so broken that it was
         * enough to prevent it.
         */

        var line = 1;
        var column = 1;
        var seenCR = false;

        for (var i = 0; i < Math.max(pos, rightmostFailuresPos); i++) {
          var ch = input.charAt(i);
          if (ch === "\n") {
            if (!seenCR) { line++; }
            column = 1;
            seenCR = false;
          } else if (ch === "\r" || ch === "\u2028" || ch === "\u2029") {
            line++;
            column = 1;
            seenCR = true;
          } else {
            column++;
            seenCR = false;
          }
        }

        return { line: line, column: column };
      }


      var result = parseFunctions[startRule]();

      /*
       * The parser is now in one of the following three states:
       *
       * 1. The parser successfully parsed the whole input.
       *
       *    - |result !== null|
       *    - |pos === input.length|
       *    - |rightmostFailuresExpected| may or may not contain something
       *
       * 2. The parser successfully parsed only a part of the input.
       *
       *    - |result !== null|
       *    - |pos < input.length|
       *    - |rightmostFailuresExpected| may or may not contain something
       *
       * 3. The parser did not successfully parse any part of the input.
       *
       *   - |result === null|
       *   - |pos === 0|
       *   - |rightmostFailuresExpected| contains at least one failure
       *
       * All code following this comment (including called functions) must
       * handle these states.
       */
      if (result === null || pos !== input.length) {
        var offset = Math.max(pos, rightmostFailuresPos);
        var found = offset < input.length ? input.charAt(offset) : null;
        var errorPosition = computeErrorPosition();

        throw new this.SyntaxError(
          cleanupExpected(rightmostFailuresExpected),
          found,
          offset,
          errorPosition.line,
          errorPosition.column
        );
      }

      return result;
    },

    /* Returns the parser source code. */
    toSource: function() { return this._source; }
  };

  /* Thrown when a parser encounters a syntax error. */

  result.SyntaxError = function(expected, found, offset, line, column) {
    function buildMessage(expected, found) {
      var expectedHumanized, foundHumanized;

      switch (expected.length) {
        case 0:
          expectedHumanized = "end of input";
          break;
        case 1:
          expectedHumanized = expected[0];
          break;
        default:
          expectedHumanized = expected.slice(0, expected.length - 1).join(", ")
            + " or "
            + expected[expected.length - 1];
      }

      foundHumanized = found ? quote(found) : "end of input";

      return "Expected " + expectedHumanized + " but " + foundHumanized + " found.";
    }

    this.name = "SyntaxError";
    this.expected = expected;
    this.found = found;
    this.message = buildMessage(expected, found);
    this.offset = offset;
    this.line = line;
    this.column = column;
  };

  result.SyntaxError.prototype = Error.prototype;

  return result;
})();
