diff options
author | lianah <lianahady@gmail.com> | 2013-03-21 11:41:39 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-03-21 11:41:39 -0400 |
commit | 80697ed7280ac2462ec05e29754a0a563f19de44 (patch) | |
tree | e247d9f4e031bba8ec03b0f972ae2af97d3c4312 | |
parent | 6aa211751e7dc697035cf110c253cc36ace69066 (diff) | |
parent | 80919c47ee899b85d626b0af923b77144b21e9f3 (diff) |
Merge branch 'master' into bv-core
-rw-r--r-- | NEWS | 1 | ||||
-rw-r--r-- | src/Makefile.am | 2 | ||||
-rw-r--r-- | src/decision/decision_engine.cpp | 2 | ||||
-rw-r--r-- | src/decision/decision_engine.h | 4 | ||||
-rw-r--r-- | src/decision/justification_heuristic.cpp | 25 | ||||
-rw-r--r-- | src/decision/justification_heuristic.h | 6 | ||||
-rw-r--r-- | src/main/interactive_shell.cpp | 46 | ||||
-rw-r--r-- | src/main/options_handlers.h | 6 | ||||
-rw-r--r-- | src/parser/antlr_input.cpp | 14 | ||||
-rw-r--r-- | src/parser/antlr_input.h | 2 | ||||
-rw-r--r-- | src/parser/antlr_input_imports.cpp | 2 | ||||
-rw-r--r-- | src/parser/cvc/Cvc.g | 3 | ||||
-rw-r--r-- | src/parser/input.h | 2 | ||||
-rw-r--r-- | src/parser/parser_exception.h | 24 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 17 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 23 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 121 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.h | 41 | ||||
-rw-r--r-- | src/theory/uf/equality_engine_types.h | 42 | ||||
-rw-r--r-- | src/util/configuration.cpp | 7 | ||||
-rw-r--r-- | test/regress/regress0/Makefile.am | 4 | ||||
-rw-r--r-- | test/regress/regress0/bug497.cvc | 920 | ||||
-rw-r--r-- | test/regress/regress0/smt2output.smt2 | 15 | ||||
-rw-r--r-- | test/unit/main/interactive_shell_black.h | 4 |
24 files changed, 1182 insertions, 151 deletions
@@ -10,6 +10,7 @@ Changes since 1.0 * for printing commands as they're invoked from the driver, you now need verbosity of 3 or higher (e.g. -vvv) instead of verbosity 1 or higher (-v). This allows tracing the solver's activities without having too much output. +* multiline support in interactive mode * To make CVC4 quieter in abnormal (e.g., "warning" conditions), you can use -q. Previously, this would silence all output (including "sat" or "unsat") as well. Now, single -q silences messages and warnings, and diff --git a/src/Makefile.am b/src/Makefile.am index 3d90f302e..b505750d4 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -137,7 +137,7 @@ gitinfo: gitinfo.tmp # .PHONY ensures the .tmp version is always rebuilt (to check for any changes) .PHONY: gitinfo.tmp gitinfo.tmp: - $(AM_V_GEN)(cd "$(top_srcdir)" && sed 's,^ref: refs/heads/,,' .git/HEAD && git show-ref refs/heads/`sed 's,^ref: refs/heads/,,' .git/HEAD` && echo "Modifications: `test -z \"\`git status -s -uno\`\" && echo false || echo true`") >"$@" 2>/dev/null || true + $(AM_V_GEN)(cd "$(top_srcdir)"; if ! grep -q '^ref: refs/heads/' .git/HEAD; then echo; fi; sed 's,^ref: refs/heads/,,' .git/HEAD; git show-ref refs/heads/`sed 's,^ref: refs/heads/,,' .git/HEAD`; echo "Modifications: `test -z \"\`git status -s -uno\`\" && echo false || echo true`") >"$@" 2>/dev/null || true install-data-local: (echo include/cvc4.h; \ diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index 08a3e49d0..98294f92b 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -29,7 +29,7 @@ using namespace std; namespace CVC4 { DecisionEngine::DecisionEngine(context::Context *sc, - context::Context *uc) : + context::UserContext *uc) : d_enabledStrategies(), d_needIteSkolemMap(), d_relevancyStrategy(NULL), diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index ea16cec16..859443d00 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -50,7 +50,7 @@ class DecisionEngine { DPLLSatSolverInterface* d_satSolver; context::Context* d_satContext; - context::Context* d_userContext; + context::UserContext* d_userContext; // Does decision engine know the answer? context::CDO<SatValue> d_result; @@ -64,7 +64,7 @@ public: // Necessary functions /** Constructor */ - DecisionEngine(context::Context *sc, context::Context *uc); + DecisionEngine(context::Context *sc, context::UserContext *uc); /** Destructor, currently does nothing */ ~DecisionEngine() { diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index 0b63dfbe1..b77d3ba6b 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -28,7 +28,7 @@ using namespace CVC4; JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de, - context::Context *uc, + context::UserContext *uc, context::Context *c): ITEDecisionStrategy(de, c), d_justified(c), @@ -38,7 +38,7 @@ JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de, d_timestat("decision::jh::time"), d_assertions(uc), d_iteAssertions(uc), - d_iteCache(), + d_iteCache(uc), d_visited(), d_visitedComputeITE(), d_curDecision() { @@ -199,19 +199,20 @@ SatValue JustificationHeuristic::tryGetSatValue(Node n) }//end of else } -const JustificationHeuristic::IteList& +JustificationHeuristic::IteList JustificationHeuristic::getITEs(TNode n) { IteCache::iterator it = d_iteCache.find(n); if(it != d_iteCache.end()) { - return it->second; + return (*it).second; } else { // Compute the list of ITEs // TODO: optimize by avoiding multiple lookup for d_iteCache[n] - d_iteCache[n] = IteList(); d_visitedComputeITE.clear(); - computeITEs(n, d_iteCache[n]); - return d_iteCache[n]; + IteList ilist; + computeITEs(n, ilist); + d_iteCache.insert(n, ilist); + return ilist; } } @@ -462,15 +463,15 @@ bool JustificationHeuristic::handleITE(TNode node, SatValue desiredVal) bool JustificationHeuristic::handleEmbeddedITEs(TNode node) { - const IteList& l = getITEs(node); + const IteList l = getITEs(node); Trace("decision::jh::ite") << " ite size = " << l.size() << std::endl; for(IteList::const_iterator i = l.begin(); i != l.end(); ++i) { - if(d_visited.find(i->first) == d_visited.end()) { - d_visited.insert(i->first); - if(findSplitterRec(i->second, SAT_VALUE_TRUE)) + if(d_visited.find((*i).first) == d_visited.end()) { + d_visited.insert((*i).first); + if(findSplitterRec((*i).second, SAT_VALUE_TRUE)) return true; - d_visited.erase(i->first); + d_visited.erase((*i).first); } } return false; diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 91c21d981..d8f9a15a8 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -38,7 +38,7 @@ namespace decision { class JustificationHeuristic : public ITEDecisionStrategy { typedef std::vector<pair<TNode,TNode> > IteList; - typedef hash_map<TNode,IteList,TNodeHashFunction> IteCache; + typedef context::CDHashMap<TNode,IteList,TNodeHashFunction> IteCache; typedef context::CDHashMap<TNode,TNode,TNodeHashFunction> SkolemMap; // being 'justified' is monotonic with respect to decisions @@ -82,7 +82,7 @@ class JustificationHeuristic : public ITEDecisionStrategy { SatLiteral d_curDecision; public: JustificationHeuristic(CVC4::DecisionEngine* de, - context::Context *uc, + context::UserContext *uc, context::Context *c); ~JustificationHeuristic(); @@ -110,7 +110,7 @@ private: SatValue tryGetSatValue(Node n); /* Get list of all term-ITEs for the atomic formula v */ - const JustificationHeuristic::IteList& getITEs(TNode n); + JustificationHeuristic::IteList getITEs(TNode n); /* Compute all term-ITEs in a node recursively */ void computeITEs(TNode n, IteList &l); diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index c1d2c2bb1..cba896e4e 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -162,9 +162,15 @@ InteractiveShell::~InteractiveShell() { } Command* InteractiveShell::readCommand() { + char* lineBuf = NULL; + string line = ""; + +restart: + /* Don't do anything if the input is closed or if we've seen a * QuitCommand. */ - if( d_in.eof() || d_quit ) { + if(d_in.eof() || d_quit) { + d_out << endl; return NULL; } @@ -173,30 +179,32 @@ Command* InteractiveShell::readCommand() { throw ParserException("Interactive input broken."); } - char* lineBuf = NULL; - string input; - stringbuf sb; - string line; - /* Prompt the user for input. */ if(d_usingReadline) { #if HAVE_LIBREADLINE - lineBuf = ::readline(d_options[options::verbosity] >= 0 ? "CVC4> " : ""); + lineBuf = ::readline(d_options[options::verbosity] >= 0 ? (line == "" ? "CVC4> " : "... > ") : ""); if(lineBuf != NULL && lineBuf[0] != '\0') { ::add_history(lineBuf); } - line = lineBuf == NULL ? "" : lineBuf; + line += lineBuf == NULL ? "" : lineBuf; free(lineBuf); #endif /* HAVE_LIBREADLINE */ } else { if(d_options[options::verbosity] >= 0) { - d_out << "CVC4> " << flush; + if(line == "") { + d_out << "CVC4> " << flush; + } else { + d_out << "... > " << flush; + } } /* Read a line */ - d_in.get(sb,'\n'); - line = sb.str(); + stringbuf sb; + d_in.get(sb); + line += sb.str(); } + + string input = ""; while(true) { Debug("interactive") << "Input now '" << input << line << "'" << endl << flush; @@ -221,20 +229,24 @@ Command* InteractiveShell::readCommand() { (d_usingReadline && lineBuf == NULL) ) { input += line; - if( input.empty() ) { + if(input.empty()) { /* Nothing left to parse. */ + d_out << endl; return NULL; } /* Some input left to parse, but nothing left to read. Jump out of input loop. */ - break; + d_out << endl; + input = line = ""; + d_in.clear(); + goto restart; } if(!d_usingReadline) { /* Extract the newline delimiter from the stream too */ int c CVC4_UNUSED = d_in.get(); - assert( c == '\n' ); + assert(c == '\n'); Debug("interactive") << "Next char is '" << (char)c << "'" << endl << flush; } @@ -259,7 +271,8 @@ Command* InteractiveShell::readCommand() { } /* Read a line */ - d_in.get(sb,'\n'); + stringbuf sb; + d_in.get(sb); line = sb.str(); } } else { @@ -296,6 +309,9 @@ Command* InteractiveShell::readCommand() { #endif /* HAVE_LIBREADLINE */ } } + } catch(ParserEndOfFileException& pe) { + line += "\n"; + goto restart; } catch(ParserException& pe) { d_out << pe << endl; // We can't really clear out the sequence and abort the current line, diff --git a/src/main/options_handlers.h b/src/main/options_handlers.h index f14a67d5f..4bb4841fe 100644 --- a/src/main/options_handlers.h +++ b/src/main/options_handlers.h @@ -27,8 +27,12 @@ inline void showConfiguration(std::string option, SmtEngine* smt) { printf("\n"); printf("version : %s\n", Configuration::getVersionString().c_str()); if(Configuration::isGitBuild()) { + const char* branchName = Configuration::getGitBranchName(); + if(*branchName == '\0') { + branchName = "-"; + } printf("scm : git [%s %s%s]\n", - Configuration::getGitBranchName(), + branchName, std::string(Configuration::getGitCommit()).substr(0, 8).c_str(), Configuration::hasGitModifications() ? " (with modifications)" : ""); diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index fbf2b8650..2279865ae 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -283,16 +283,22 @@ void AntlrInput::warning(const std::string& message) { Warning() << getInputStream()->getName() << ':' << d_lexer->getLine(d_lexer) << '.' << d_lexer->getCharPositionInLine(d_lexer) << ": " << message << endl; } -void AntlrInput::parseError(const std::string& message) +void AntlrInput::parseError(const std::string& message, bool eofException) throw (ParserException) { Debug("parser") << "Throwing exception: " << getInputStream()->getName() << ":" << d_lexer->getLine(d_lexer) << "." << d_lexer->getCharPositionInLine(d_lexer) << ": " << message << endl; - throw ParserException(message, getInputStream()->getName(), - d_lexer->getLine(d_lexer), - d_lexer->getCharPositionInLine(d_lexer)); + if(eofException) { + throw ParserEndOfFileException(message, getInputStream()->getName(), + d_lexer->getLine(d_lexer), + d_lexer->getCharPositionInLine(d_lexer)); + } else { + throw ParserException(message, getInputStream()->getName(), + d_lexer->getLine(d_lexer), + d_lexer->getCharPositionInLine(d_lexer)); + } } diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index a2fe99f52..020db0d50 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -209,7 +209,7 @@ protected: /** * Throws a <code>ParserException</code> with the given message. */ - void parseError(const std::string& msg) + void parseError(const std::string& msg, bool eofException = false) throw (ParserException); /** Set the ANTLR3 lexer for this input. */ diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp index 9c92846bb..07283f1af 100644 --- a/src/parser/antlr_input_imports.cpp +++ b/src/parser/antlr_input_imports.cpp @@ -261,7 +261,7 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { } // Call the error display routine - input->parseError(ss.str()); + input->parseError(ss.str(), ((pANTLR3_COMMON_TOKEN)ex->token)->type == ANTLR3_TOKEN_EOF); } /// diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index b8ec160e8..e5e26c9a2 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -625,8 +625,7 @@ mainCommand[CVC4::Command*& cmd] : ASSERT_TOK formula[f] { cmd = new AssertCommand(f); } | QUERY_TOK formula[f] { cmd = new QueryCommand(f); } - | CHECKSAT_TOK formula[f] { cmd = new CheckSatCommand(f); } - | CHECKSAT_TOK { cmd = new CheckSatCommand(); } + | CHECKSAT_TOK formula[f]? { cmd = f.isNull() ? new CheckSatCommand() : new CheckSatCommand(f); } /* options */ | OPTION_TOK diff --git a/src/parser/input.h b/src/parser/input.h index f4b36469b..5fd3611be 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -178,7 +178,7 @@ protected: /** * Throws a <code>ParserException</code> with the given message. */ - virtual void parseError(const std::string& msg) + virtual void parseError(const std::string& msg, bool eofException = false) throw (ParserException) = 0; /** Parse an expression from the input by invoking the diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h index 8abc04c15..6eae3047d 100644 --- a/src/parser/parser_exception.h +++ b/src/parser/parser_exception.h @@ -89,6 +89,30 @@ protected: unsigned long d_column; };/* class ParserException */ +class CVC4_PUBLIC ParserEndOfFileException : public ParserException { +public: + + // Constructors same as ParserException's + + ParserEndOfFileException() throw() : + ParserException() { + } + + ParserEndOfFileException(const std::string& msg) throw() : + ParserException(msg) { + } + + ParserEndOfFileException(const char* msg) throw() : + ParserException(msg) { + } + + ParserEndOfFileException(const std::string& msg, const std::string& filename, + unsigned long line, unsigned long column) throw() : + ParserException(msg, filename, line, column) { + } + +};/* class ParserEndOfFileException */ + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 8541ca6ae..ef4fd5fea 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -74,6 +74,17 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, } } +static std::string maybeQuoteSymbol(const std::string& s) { + // this is the set of SMT-LIBv2 permitted characters in "simple" (non-quoted) symbols + if(s.find_first_not_of("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789~!@$%^&*_-+=<>.?/") != string::npos) { + // need to quote it + stringstream ss; + ss << '|' << s << '|'; + return ss.str(); + } + return s; +} + void Smt2Printer::toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw() { // null @@ -86,7 +97,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, if(n.isVar()) { string s; if(n.getAttribute(expr::VarNameAttr(), s)) { - out << s; + out << maybeQuoteSymbol(s); } else { if(n.getKind() == kind::VARIABLE) { out << "var_"; @@ -175,7 +186,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, break; case kind::DATATYPE_TYPE: - out << n.getConst<Datatype>().getName(); + out << maybeQuoteSymbol(n.getConst<Datatype>().getName()); break; case kind::UNINTERPRETED_CONSTANT: { @@ -196,7 +207,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, if(n.getKind() == kind::SORT_TYPE) { string name; if(n.getAttribute(expr::VarNameAttr(), name)) { - out << name; + out << maybeQuoteSymbol(name); return; } } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 50cdf33a3..2a73cb444 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -136,6 +136,12 @@ struct SmtEngineStatistics { IntStat d_numAssertionsPost; /** time spent in checkModel() */ TimerStat d_checkModelTime; + /** time spent in PropEngine::checkSat() */ + TimerStat d_solveTime; + /** time spent in pushing/popping */ + TimerStat d_pushPopTime; + /** time spent in processAssertions() */ + TimerStat d_processAssertionsTime; SmtEngineStatistics() : d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"), @@ -152,7 +158,10 @@ struct SmtEngineStatistics { d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"), d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0), d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0), - d_checkModelTime("smt::SmtEngine::checkModelTime") { + d_checkModelTime("smt::SmtEngine::checkModelTime"), + d_solveTime("smt::SmtEngine::solveTime"), + d_pushPopTime("smt::SmtEngine::pushPopTime"), + d_processAssertionsTime("smt::SmtEngine::processAssertionsTime") { StatisticsRegistry::registerStat(&d_definitionExpansionTime); StatisticsRegistry::registerStat(&d_rewriteBooleanTermsTime); @@ -169,6 +178,9 @@ struct SmtEngineStatistics { StatisticsRegistry::registerStat(&d_numAssertionsPre); StatisticsRegistry::registerStat(&d_numAssertionsPost); StatisticsRegistry::registerStat(&d_checkModelTime); + StatisticsRegistry::registerStat(&d_solveTime); + StatisticsRegistry::registerStat(&d_pushPopTime); + StatisticsRegistry::registerStat(&d_processAssertionsTime); } ~SmtEngineStatistics() { @@ -187,6 +199,9 @@ struct SmtEngineStatistics { StatisticsRegistry::unregisterStat(&d_numAssertionsPre); StatisticsRegistry::unregisterStat(&d_numAssertionsPost); StatisticsRegistry::unregisterStat(&d_checkModelTime); + StatisticsRegistry::unregisterStat(&d_solveTime); + StatisticsRegistry::unregisterStat(&d_pushPopTime); + StatisticsRegistry::unregisterStat(&d_processAssertionsTime); } };/* struct SmtEngineStatistics */ @@ -2480,6 +2495,8 @@ Result SmtEngine::check() { resource = d_resourceBudgetPerCall; } + TimerStat::CodeTimer solveTimer(d_stats->d_solveTime); + Chat() << "solving..." << endl; Trace("smt") << "SmtEngine::check(): running check" << endl; Result result = d_propEngine->checkSat(millis, resource); @@ -2562,6 +2579,8 @@ bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, } void SmtEnginePrivate::processAssertions() { + TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime); + Assert(d_smt.d_fullyInited); Assert(d_smt.d_pendingPops == 0); @@ -3538,6 +3557,7 @@ void SmtEngine::internalPush() { doPendingPops(); if(options::incrementalSolving()) { d_private->processAssertions(); + TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime); d_userContext->push(); // the d_context push is done inside of the SAT solver d_propEngine->push(); @@ -3558,6 +3578,7 @@ void SmtEngine::internalPop(bool immediate) { void SmtEngine::doPendingPops() { Assert(d_pendingPops == 0 || options::incrementalSolving()); while(d_pendingPops > 0) { + TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime); d_propEngine->pop(); // the d_context pop is done inside of the SAT solver d_userContext->pop(); diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index f4d79b468..2fcf43054 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -90,7 +90,7 @@ EqualityEngine::EqualityEngine(context::Context* context, std::string name) , d_nodesCount(context, 0) , d_assertedEqualitiesCount(context, 0) , d_equalityTriggersCount(context, 0) -, d_nodesThatEvaluateSize(context, 0) +, d_subtermEvaluatesSize(context, 0) , d_stats(name) , d_inPropagate(false) , d_triggerDatabaseSize(context, 0) @@ -114,7 +114,7 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* c , d_nodesCount(context, 0) , d_assertedEqualitiesCount(context, 0) , d_equalityTriggersCount(context, 0) -, d_nodesThatEvaluateSize(context, 0) +, d_subtermEvaluatesSize(context, 0) , d_stats(name) , d_inPropagate(false) , d_triggerDatabaseSize(context, 0) @@ -141,18 +141,18 @@ void EqualityEngine::enqueue(const MergeCandidate& candidate, bool back) { } } -EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2, bool isEquality) { +EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2, FunctionApplicationType type) { Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ")" << std::endl; ++ d_stats.functionTermsCount; // Get another id for this EqualityNodeId funId = newNode(original); - FunctionApplication funOriginal(isEquality, t1, t2); + FunctionApplication funOriginal(type, t1, t2); // The function application we're creating EqualityNodeId t1ClassId = getEqualityNode(t1).getFind(); EqualityNodeId t2ClassId = getEqualityNode(t2).getFind(); - FunctionApplication funNormalized(isEquality, t1ClassId, t2ClassId); + FunctionApplication funNormalized(type, t1ClassId, t2ClassId); // We add the original version d_applications[funId] = FunctionApplicationPair(funOriginal, funNormalized); @@ -203,8 +203,8 @@ EqualityNodeId EqualityEngine::newNode(TNode node) { d_nodeIndividualTrigger.push_back(+null_set_id); // Mark non-constant by default d_isConstant.push_back(false); - // Makr non-evaluate by default - d_evaluates.push_back(false); + // No terms to evaluate by defaul + d_subtermsToEvaluate.push_back(0); // Mark Boolean nodes d_isBoolean.push_back(false); // Mark the node as internal by default @@ -227,12 +227,29 @@ EqualityNodeId EqualityEngine::newNode(TNode node) { void EqualityEngine::addFunctionKind(Kind fun, bool interpreted) { d_congruenceKinds |= fun; - if (interpreted) { + if (interpreted && fun != kind::EQUAL) { Debug("equality::evaluation") << d_name << "::eq::addFunctionKind(): " << fun << " is interpreted " << std::endl; d_congruenceKindsInterpreted |= fun; } } +bool isOperator(TNode node) { + if (node.getKind() == kind::BUILTIN) { + return true; + } + return false; +} + +void EqualityEngine::subtermEvaluates(EqualityNodeId id) { + Debug("equality::evaluation") << d_name << "::eq::subtermEvaluates(" << d_nodes[id] << "): " << d_subtermsToEvaluate[id] << std::endl; + Assert(!d_isInternal[id]); + Assert(d_subtermsToEvaluate[id] > 0); + d_subtermsToEvaluate[id] --; + d_subtermEvaluates.push_back(id); + d_subtermEvaluatesSize = d_subtermEvaluates.size(); + Debug("equality::evaluation") << d_name << "::eq::subtermEvaluates(" << d_nodes[id] << "): new " << d_subtermsToEvaluate[id] << std::endl; +} + void EqualityEngine::addTerm(TNode t) { Debug("equality") << d_name << "::eq::addTerm(" << t << ")" << std::endl; @@ -254,45 +271,48 @@ void EqualityEngine::addTerm(TNode t) { addTerm(t[1]); EqualityNodeId t0id = getNodeId(t[0]); EqualityNodeId t1id = getNodeId(t[1]); - result = newApplicationNode(t, t0id, t1id, true); + result = newApplicationNode(t, t0id, t1id, APP_EQUALITY); d_isInternal[result] = false; - } else if (t.getNumChildren() > 0 && d_congruenceKinds[t.getKind()]) { TNode tOp = t.getOperator(); // Add the operator addTerm(tOp); result = getNodeId(tOp); d_isInternal[result] = true; - d_isConstant[result] = isInterpretedFunctionKind(t.getKind()); - d_evaluates[result] = isInterpretedFunctionKind(t.getKind()); // Add all the children and Curryfy + bool isInterpreted = isInterpretedFunctionKind(t.getKind()); for (unsigned i = 0; i < t.getNumChildren(); ++ i) { // Add the child addTerm(t[i]); + EqualityNodeId tiId = getNodeId(t[i]); // Add the application - result = newApplicationNode(t, result, getNodeId(t[i]), false); + result = newApplicationNode(t, result, tiId, isInterpreted ? APP_INTERPRETED : APP_UNINTERPRETED); } d_isInternal[result] = false; - if (t.isConst()) { - d_isConstant[result] = true; - d_evaluates[result] = true; + d_isConstant[result] = t.isConst(); + // If interpreted, set the number of non-interpreted children + if (isInterpreted) { + // How many children are not constants yet + d_subtermsToEvaluate[result] = t.getNumChildren(); + for (unsigned i = 0; i < t.getNumChildren(); ++ i) { + if (isConstant(getNodeId(t[i]))) { + subtermEvaluates(result); + } + } } } else { // Otherwise we just create the new id result = newNode(t); // Is this an operator d_isInternal[result] = false; - if (t.isConst()) { - d_isConstant[result] = true; - d_evaluates[result] = true; - } + d_isConstant[result] = t.isConst() && !isOperator(t); } if (t.getType().isBoolean()) { // We set this here as this only applies to actual terms, not the // intermediate application terms d_isBoolean[result] = true; - } else if (t.isConst()) { + } else if (d_isConstant[result]) { // Non-Boolean constants are trigger terms for all tags EqualityNodeId tId = getNodeId(t); d_newSetTags = 0; @@ -585,10 +605,16 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect EqualityNodeId funId = useNode.getApplicationId(); Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): " << d_nodes[currentId] << " in " << d_nodes[funId] << std::endl; const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized; - // Check if there is an application with find arguments + // If it's interpreted and we can interpret + if (fun.isInterpreted() && class1isConstant && !d_isInternal[class2Id]) { + // Get the actual term id + TNode term = d_nodes[useNode.getApplicationId()]; + subtermEvaluates(getNodeId(term)); + } + // Check if there is an application with find arguments EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind(); EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind(); - FunctionApplication funNormalized(fun.isEquality, aNormalized, bNormalized); + FunctionApplication funNormalized(fun.type, aNormalized, bNormalized); ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized); if (find != d_applicationLookup.end()) { // Applications fun and the funNormalized can be merged due to congruence @@ -788,10 +814,11 @@ void EqualityEngine::backtrack() { d_applicationLookups.resize(d_applicationLookupsCount); } - if (d_nodesThatEvaluate.size() > d_nodesThatEvaluateSize) { - for(int i = d_nodesThatEvaluate.size() - 1, i_end = (int)d_nodesThatEvaluateSize; i >= i_end; --i) { - d_evaluates[d_nodesThatEvaluate[i]] = false; + if (d_subtermEvaluates.size() > d_subtermEvaluatesSize) { + for(int i = d_subtermEvaluates.size() - 1, i_end = (int)d_subtermEvaluatesSize; i >= i_end; --i) { + d_subtermsToEvaluate[d_subtermEvaluates[i]] ++; } + d_subtermEvaluates.resize(d_subtermEvaluatesSize); } if (d_nodes.size() > d_nodesCount) { @@ -802,7 +829,7 @@ void EqualityEngine::backtrack() { d_nodeIds.erase(d_nodes[i]); const FunctionApplication& app = d_applications[i].original; - if (app.isApplication()) { + if (!app.isNull()) { // Remove b from use-list getEqualityNode(app.b).removeTopFromUseList(d_useListNodes); // Remove a from use-list @@ -816,7 +843,7 @@ void EqualityEngine::backtrack() { d_nodeTriggers.resize(d_nodesCount); d_nodeIndividualTrigger.resize(d_nodesCount); d_isConstant.resize(d_nodesCount); - d_evaluates.resize(d_nodesCount); + d_subtermsToEvaluate.resize(d_nodesCount); d_isBoolean.resize(d_nodesCount); d_isInternal.resize(d_nodesCount); d_equalityGraph.resize(d_nodesCount); @@ -994,7 +1021,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st Debug("equality") << d_name << "::eq::getExplanation(): due to reflexivity, going deeper" << std::endl; EqualityNodeId eqId = currentNode == d_trueId ? edgeNode : currentNode; const FunctionApplication& eq = d_applications[eqId].original; - Assert(eq.isEquality, "Must be an equality"); + Assert(eq.isEquality(), "Must be an equality"); // Explain why a = b constant Debug("equality") << push; @@ -1211,20 +1238,6 @@ void EqualityEngine::processEvaluationQueue() { Debug("equality::evaluation") << d_name << "::eq::processEvaluationQueue(): done" << std::endl; } -void EqualityEngine::evaluateApplication(const FunctionApplication& funNormalized, EqualityNodeId funId) { - - // Evaluate special for equality and other - if (!funNormalized.isEquality) { - // We can't add new terms - d_evaluationQueue.push(funId); - } else { - if (funNormalized.a != funNormalized.b) { - // We don't enqueue fun -> true, as this is convered with reflexivity - enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null())); - } - } -} - void EqualityEngine::propagate() { if (d_inPropagate) { @@ -1466,7 +1479,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const } // Create the equality - FunctionApplication eqNormalized(true, t1ClassId, t2ClassId); + FunctionApplication eqNormalized(APP_EQUALITY, t1ClassId, t2ClassId); ApplicationIdsMap::const_iterator find = d_applicationLookup.find(eqNormalized); if (find != d_applicationLookup.end()) { if (getEqualityNode(find->second).getFind() == getEqualityNode(d_falseId).getFind()) { @@ -1618,19 +1631,11 @@ void EqualityEngine::storeApplicationLookup(FunctionApplication& funNormalized, Assert(d_applicationLookupsCount == d_applicationLookups.size()); // If an equality over constants we merge to false - if (funNormalized.isEquality && funNormalized.a == funNormalized.b) { - enqueue(MergeCandidate(funId, d_trueId, MERGED_THROUGH_REFLEXIVITY, TNode::null())); - } - - // Now check for application evaluation - if (!d_evaluates[funId]) { - if (d_evaluates[funNormalized.a] && d_evaluates[funNormalized.b]) { - // Depending on the "internal" - if (d_isInternal[funId]) { - setEvaluates(funId); - } else { - evaluateApplication(funNormalized, funId); - } + if (funNormalized.isEquality()) { + if (funNormalized.a == funNormalized.b) { + enqueue(MergeCandidate(funId, d_trueId, MERGED_THROUGH_REFLEXIVITY, TNode::null())); + } else if (d_isConstant[funNormalized.a] && d_isConstant[funNormalized.b]) { + enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null())); } } } @@ -1798,7 +1803,7 @@ void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classI const FunctionApplication& fun = d_applications[useListNode.getApplicationId()].original; // If it's an equality asserted to false, we do the work - if (fun.isEquality && getEqualityNode(funId).getFind() == getEqualityNode(d_false).getFind()) { + if (fun.isEquality() && getEqualityNode(funId).getFind() == getEqualityNode(d_false).getFind()) { // Get the other equality member bool lhs = false; EqualityNodeId toCompare = fun.b; diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 3d80c486a..0a5d70a9c 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -418,20 +418,11 @@ private: std::vector<bool> d_isConstant; /** - * Map from ids to whether they evaluate. A node evaluates - * (1) if it is a constant - * (2) if it is internal and it's children evaluate - * (3) if it is non-internal and it's children are constants + * Map from ids of proper terms, to the number of non-constant direct subterms. If we update an interpreted + * application to a constant, we can decrease this value. If we hit 0, we can evaluate the term. * - * Example: - * - * f(x) + g(y) - * - * If f and g are interpreted, in the context x = 0, the nodes - * f(x) and g(y) evaluate, but not f(x) + g(y). The term f(x) + g(y) - * evaluates if we evaluate f(0) and g(0) to constants c1 and c2. */ - std::vector<bool> d_evaluates; + std::vector<unsigned> d_subtermsToEvaluate; /** * For nodes that we need to postpone evaluation. @@ -443,32 +434,14 @@ private: */ void processEvaluationQueue(); - /** - * Check whether the node evaluates in the current context - */ - bool evaluates(EqualityNodeId id) const { - return d_evaluates[id]; - } - /** Vector of nodes that evaluate. */ - std::vector<EqualityNodeId> d_nodesThatEvaluate; + std::vector<EqualityNodeId> d_subtermEvaluates; /** Size of the nodes that evaluate vector. */ - context::CDO<unsigned> d_nodesThatEvaluateSize; + context::CDO<unsigned> d_subtermEvaluatesSize; /** Set the node evaluate flag */ - void setEvaluates(EqualityNodeId id) { - Assert(!d_evaluates[id]); - d_evaluates[id] = true; - d_nodesThatEvaluate.push_back(id); - d_nodesThatEvaluateSize = d_nodesThatEvaluate.size(); - } - - /** - * Propagate something that evaluates. - * @param fragile if true, no new terms are added, but - */ - void evaluateApplication(const FunctionApplication& funNormalized, EqualityNodeId funId); + void subtermEvaluates(EqualityNodeId id); /** * Returns the evaluation of the term when all (direct) children are replaced with @@ -503,7 +476,7 @@ private: Statistics d_stats; /** Add a new function application node to the database, i.e APP t1 t2 */ - EqualityNodeId newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2, bool isEquality); + EqualityNodeId newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2, FunctionApplicationType type); /** Add a new node to the database */ EqualityNodeId newNode(TNode t); diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h index e05000160..f993b941b 100644 --- a/src/theory/uf/equality_engine_types.h +++ b/src/theory/uf/equality_engine_types.h @@ -264,6 +264,15 @@ struct EqualityPairHashFunction { } }; +enum FunctionApplicationType { + /** This application is an equality a = b */ + APP_EQUALITY, + /** This is a part of an uninterpreted application f(t1, ...., tn) */ + APP_UNINTERPRETED, + /** This is a part of an interpreted application f(t1, ..., tn) */ + APP_INTERPRETED +}; + /** * Represents the function APPLY a b. If isEquality is true then it * represents the predicate (a = b). Note that since one can not @@ -271,16 +280,35 @@ struct EqualityPairHashFunction { * function below are still well defined. */ struct FunctionApplication { - bool isEquality; + /** Type of application */ + FunctionApplicationType type; + /** The actuall application elements */ EqualityNodeId a, b; - FunctionApplication(bool isEquality = false, EqualityNodeId a = null_id, EqualityNodeId b = null_id) - : isEquality(isEquality), a(a), b(b) {} + + /** Construct an application */ + FunctionApplication(FunctionApplicationType type = APP_EQUALITY, EqualityNodeId a = null_id, EqualityNodeId b = null_id) + : type(type), a(a), b(b) {} + + /** Equality of two applications */ bool operator == (const FunctionApplication& other) const { - return isEquality == other.isEquality && a == other.a && b == other.b; + return type == other.type && a == other.a && b == other.b; } - bool isApplication() const { - return a != null_id && b != null_id; + + /** Is this a null application */ + bool isNull() const { + return a == null_id || b == null_id; } + + /** Is this an equality */ + bool isEquality() const { + return type == APP_EQUALITY; + } + + /** Is this an interpreted application (equality is special, i.e. not interpreted) */ + bool isInterpreted() const { + return type == APP_INTERPRETED; + } + }; struct FunctionApplicationHashFunction { @@ -303,7 +331,7 @@ struct FunctionApplicationPair { FunctionApplicationPair(const FunctionApplication& original, const FunctionApplication& normalized) : original(original), normalized(normalized) {} bool isNull() const { - return !original.isApplication(); + return original.isNull(); } }; diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index 9be4e4104..ce6273a13 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -216,8 +216,13 @@ std::string Configuration::getGitId() { return ""; } + const char* branchName = getGitBranchName(); + if(*branchName == '\0') { + branchName = "-"; + } + stringstream ss; - ss << "git " << getGitBranchName() << " " << string(getGitCommit()).substr(0, 8) + ss << "git " << branchName << " " << string(getGitCommit()).substr(0, 8) << ( ::CVC4::Configuration::hasGitModifications() ? " (with modifications)" : "" ); return ss.str(); } diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index cc385327e..96d07d7f3 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -113,6 +113,7 @@ TPTP_TESTS = \ # Regression tests derived from bug reports BUG_TESTS = \ + smt2output.smt2 \ bug32.cvc \ bug49.smt \ bug161.smt \ @@ -144,7 +145,8 @@ BUG_TESTS = \ bug421b.smt2 \ bug425.cvc \ bug480.smt2 \ - bug486.cvc + bug486.cvc \ + bug497.cvc TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/bug497.cvc b/test/regress/regress0/bug497.cvc new file mode 100644 index 000000000..ce34ab6ad --- /dev/null +++ b/test/regress/regress0/bug497.cvc @@ -0,0 +1,920 @@ +% COMMAND-LINE: --decision=justification --incremental +% EXPECT: sat +% EXPECT: sat +% EXIT: 10 +OPTION "logic" "QF_UFLIA"; +_nat : TYPE = INT; +_base : INT; +ASSERT _base <= 0; +_n : _nat; +ASSERT _n >= _base; +_check_quant : BOOLEAN; + +% maxdepth = 1 +x100 : _nat -> INT; + % Chart_main_simp_rlt_node_state126_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState % LOCAL/200 +x101 : _nat -> INT; + % Chart_main_simp_rlt_node_state122_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState % LOCAL/201 +x2 : _nat -> INT; + % GroundTrack_OrbitalPosition % INPUT,STATE(1,)/102 +x102 : _nat -> INT; + % Chart_main_simp_rlt_node_state221_rlt_chart_data_vars_Chart_OrbitalState_Attitude % LOCAL,STATE(1,)/202 +x3 : _nat -> INT; + % GroundTrack_OrbitalVelocity % INPUT,STATE(1,)/103 +x103 : _nat -> INT; + % Chart_main_simp_rlt_node_state221_rlt_chart_data_vars_Chart_InertialNavigation_AbsoluteVelocity % LOCAL/203 +x4 : _nat -> INT; + % dockVisibility_status % INPUT,STATE(1,)/104 +x104 : _nat -> INT; + % Chart_main_simp_rlt_node_state221_rlt_chart_data_vars_Chart_InertialNavigation_AbsolutePosition % LOCAL/204 +x5 : _nat -> BOOLEAN; + % opticsAvailability_status % INPUT,STATE(1,)/105 +x105 : _nat -> INT; + % Chart_main_simp_rlt_node_state221_rlt_chart_data_vars_Chart_InertialNavigation_timer % LOCAL/205 +x6 : _nat -> BOOLEAN; + % sunlight_status % INPUT,STATE(1,)/106 +x106 : _nat -> INT; + % Chart_main_simp_rlt_node_state221_rlt_chart_data_vars_Chart_OrbitalState_Velocity % LOCAL,STATE(1,)/206 +x7 : _nat -> INT; + % GPS_satelliteVisibility_status % INPUT,STATE(1,)/107 +x107 : _nat -> INT; + % Chart_main_simp_rlt_node_state221_rlt_chart_data_vars_Chart_OrbitalState_Position % LOCAL,STATE(1,)/207 +x8 : _nat -> BOOLEAN; + % GPS_receiverAvailability_status % INPUT,STATE(1,)/108 +x108 : _nat -> INT; + % Chart_main_simp_rlt_node_state221_rlt_chart_data_vars_Chart_InertialNavigation_AbsoluteAttitude % LOCAL/208 +x9 : _nat -> INT; + % StarPlanetTracker_planetVisibility % INPUT,STATE(1,)/109 +x109 : _nat -> INT; + % Chart_main_simp_rlt_node_state221_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState % LOCAL,STATE(1,)/209 +x10 : _nat -> INT; + % StarPlanetTracker_starVisibility % INPUT,STATE(1,)/110 +x110 : _nat -> INT; + % Chart_main_simp_rlt_node_state221_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_InertialNavigation % LOCAL/210 +x11 : _nat -> BOOLEAN; + % InertialNavigation_time % INPUT/111 +x111 : _nat -> INT; + % Chart_main_simp_rlt_node_state367_rlt_chart_data_vars_Chart_OrbitalState_Time % LOCAL,STATE(1,)/211 +x12 : _nat -> INT; + % GroundTrack_Time % INPUT/112 +x112 : _nat -> INT; + % Chart_main_simp_rlt_node_state367_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState2 % LOCAL,STATE(1,)/212 +x13 : _nat -> INT; + % RealTimeClock_time % INPUT,STATE(1,)/113 +x113 : _nat -> INT; + % Chart_main_simp_rlt_node_state499_rlt_chart_data_vars_Chart_InertialNavigation_AbsoluteVelocity % LOCAL,STATE(1,)/213 +x14 : _nat -> INT; + % StageTransition % INPUT,STATE(1,)/114 +x114 : _nat -> INT; + % Chart_main_simp_rlt_node_state499_rlt_chart_data_vars_Chart_InertialNavigation_AbsolutePosition % LOCAL,STATE(1,)/214 +x15 : _nat -> BOOLEAN; + % CaptureApproachComplete % OUTPUT,STATE(1,)/115 +x115 : _nat -> INT; + % Chart_main_simp_rlt_node_state499_rlt_chart_data_vars_Chart_InertialNavigation_AbsoluteAttitude % LOCAL,STATE(1,)/215 +x16 : _nat -> BOOLEAN; + % DockingApproachComplete % OUTPUT,STATE(1,)/116 +x116 : _nat -> INT; + % Chart_main_simp_rlt_node_state499_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_InertialNavigation % LOCAL,STATE(1,)/216 +x17 : _nat -> BOOLEAN; + % AttemptingToDock % OUTPUT,STATE(1,)/117 +x117 : _nat -> INT; + % Chart_main_simp_rlt_node_state627_rlt_chart_data_states_Chart_MissionPhaseStates_DockingApproach_dockingSensor % LOCAL,STATE(1,)/217 +x118 : _nat -> INT; + % Chart_main_simp_rlt_node_state545_rlt_chart_data_vars_Chart_dockingSensor_timer % LOCAL/218 +x119 : _nat -> INT; + % Chart_main_simp_rlt_node_state545_rlt_chart_data_states_Chart_MissionPhaseStates_DockingApproach_dockingSensor % LOCAL/219 +x20 : _nat -> BOOLEAN; + % ApproachOrbitComplete % OUTPUT,STATE(1,)/120 +x120 : _nat -> INT; + % Chart_main_simp_rlt_node_state542_rlt_chart_data_states_Chart_MissionPhaseStates_DockingApproach_dockingSensor % LOCAL/220 +x21 : _nat -> BOOLEAN; + % FarApproachComplete % OUTPUT,STATE(1,)/121 +x121 : _nat -> INT; + % Chart_main_simp_rlt_node_state540_rlt_chart_data_states_Chart_MissionPhaseStates_DockingApproach_dockingSensor % LOCAL/221 +x22 : _nat -> BOOLEAN; + % ProximityOperationsComplete % OUTPUT,STATE(1,)/122 +x122 : _nat -> INT; + % Chart_main_simp_rlt_node_state765_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_latch % LOCAL,STATE(1,)/222 +x123 : _nat -> INT; + % Chart_main_simp_rlt_node_state690_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_LatchCaptureCheck % LOCAL,STATE(1,)/223 +x124 : _nat -> INT; + % Chart_main_simp_rlt_node_state706_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_latch % LOCAL/224 +x125 : _nat -> INT; + % Chart_main_simp_rlt_node_state702_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_latch % LOCAL/225 +x26 : _nat -> INT; + % MWI_FcnMin_Out110 % LOCAL,STATE(1,)/126 +x126 : _nat -> INT; + % Chart_main_simp_rlt_node_state759_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_latch % LOCAL/226 +x27 : _nat -> INT; + % MWI_FcnMin_Out19 % LOCAL,STATE(1,)/127 +x127 : _nat -> INT; + % Chart_main_simp_rlt_node_state757_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_latch % LOCAL/227 +x28 : _nat -> INT; + % MWI_FcnMin_In1n8 % LOCAL/128 +x128 : _nat -> INT; + % Chart_main_simp_rlt_node_state753_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_latch % LOCAL/228 +x29 : _nat -> INT; + % MWI_FcnMin_Out18 % LOCAL,STATE(1,)/129 +x129 : _nat -> BOOLEAN; + % sequence1 % LOCAL/229 +x30 : _nat -> INT; + % MWI_FcnMin_Out17 % LOCAL/130 +x31 : _nat -> INT; + % MWI_FcnMin_Out13 % LOCAL,STATE(1,)/131 +x32 : _nat -> INT; + % MWI_FcnMin_Out12 % LOCAL,STATE(1,)/132 +x33 : _nat -> INT; + % MWI_FcnMin_Out11 % LOCAL,STATE(1,)/133 +x34 : _nat -> INT; + % MWI_FcnMin_In1n % LOCAL/134 +x35 : _nat -> INT; + % MWI_FcnMin_Out1 % LOCAL,STATE(1,)/135 +x36 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_OrbitalState_Time % LOCAL,STATE(1,)/136 +x37 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_LatchCapture_timer % LOCAL,STATE(1,)/137 +x38 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_StarPlanetTracker_timer % LOCAL,STATE(1,)/138 +x39 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_OrbitalState_Attitude % LOCAL,STATE(1,)/139 +x40 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_CaptureApproach_timer % LOCAL,STATE(1,)/140 +x41 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_GPS_timer % LOCAL,STATE(1,)/141 +x42 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_InertialNavigation_AbsoluteVelocity % LOCAL,STATE(1,)/142 +x43 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_InertialNavigation_AbsolutePosition % LOCAL,STATE(1,)/143 +x44 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_InertialNavigation_timer % LOCAL,STATE(1,)/144 +x45 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_latch_status % LOCAL,STATE(1,)/145 +x46 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_dockingSensor_timer % LOCAL,STATE(1,)/146 +x47 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_OrbitalState_Velocity % LOCAL,STATE(1,)/147 +x48 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_OrbitalState_Position % LOCAL,STATE(1,)/148 +x49 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_dockingSensor_RelativeAttitude % LOCAL,STATE(1,)/149 +x50 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_GPS_AbsolutePosition % LOCAL,STATE(1,)/150 +x51 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_DockingApproach_timer % LOCAL,STATE(1,)/151 +x52 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_InertialNavigation_AbsoluteAttitude % LOCAL,STATE(1,)/152 +x53 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_vars_Chart_StarPlanetTracker_AbsolutePosition % LOCAL,STATE(1,)/153 +x54 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_DockingApproach_dockingSensor % LOCAL,STATE(1,)/154 +x55 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_DockingApproach_DockingApproach % LOCAL,STATE(1,)/155 +x56 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_latch % LOCAL,STATE(1,)/156 +x57 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_LatchCapture_LatchCaptureCheck % LOCAL,STATE(1,)/157 +x58 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_GPS % LOCAL,STATE(1,)/158 +x59 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart % LOCAL,STATE(1,)/159 +x60 : _nat -> [0..2]; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState2 % LOCAL,STATE(1,)/160 +x61 : _nat -> [0..4]; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState % LOCAL,STATE(1,)/161 +x62 : _nat -> [0..3]; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_StarPlanetTracker % LOCAL,STATE(1,)/162 +x63 : _nat -> [0..5]; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_CaptureApproach % LOCAL,STATE(1,)/163 +x64 : _nat -> [0..3]; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_InertialNavigation % LOCAL,STATE(1,)/164 +x65 : _nat -> INT; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_states_Chart_MissionPhaseStates % LOCAL,STATE(1,)/165 +x66 : _nat -> BOOLEAN; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_outports_FarApproachComplete % LOCAL/166 +x68 : _nat -> BOOLEAN; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_outports_AttemptingToDock % LOCAL/168 +x71 : _nat -> BOOLEAN; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_outports_ProximityOperationsComplete % LOCAL/171 +x73 : _nat -> BOOLEAN; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_outports_DockingApproachComplete % LOCAL/173 +x74 : _nat -> BOOLEAN; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_outports_ApproachOrbitComplete % LOCAL/174 +x76 : _nat -> BOOLEAN; + % Chart_main_simp_rlt_node_state1_rlt_chart_data_outports_CaptureApproachComplete % LOCAL/176 +x77 : _nat -> INT; + % Chart_main_simp_rlt_node_state364_rlt_chart_data_vars_Chart_InertialNavigation_AbsoluteVelocity % LOCAL,STATE(1,)/177 +x78 : _nat -> INT; + % Chart_main_simp_rlt_node_state364_rlt_chart_data_vars_Chart_InertialNavigation_AbsolutePosition % LOCAL,STATE(1,)/178 +x79 : _nat -> INT; + % Chart_main_simp_rlt_node_state364_rlt_chart_data_vars_Chart_InertialNavigation_AbsoluteAttitude % LOCAL,STATE(1,)/179 +x80 : _nat -> INT; + % Chart_main_simp_rlt_node_state364_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_InertialNavigation % LOCAL,STATE(1,)/180 +x81 : _nat -> INT; + % Chart_main_simp_rlt_node_state155_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_GPS % LOCAL,STATE(1,)/181 +x82 : _nat -> INT; + % Chart_main_simp_rlt_node_state155_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState2 % LOCAL,STATE(1,)/182 +x83 : _nat -> INT; + % Chart_main_simp_rlt_node_state155_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState % LOCAL,STATE(1,)/183 +x84 : _nat -> INT; + % Chart_main_simp_rlt_node_state155_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_StarPlanetTracker % LOCAL,STATE(1,)/184 +x85 : _nat -> INT; + % Chart_main_simp_rlt_node_state155_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_InertialNavigation % LOCAL/185 +x86 : _nat -> INT; + % Chart_main_simp_rlt_node_state155_rlt_chart_data_states_Chart_MissionPhaseStates % LOCAL,STATE(1,)/186 +x87 : _nat -> INT; + % Chart_main_simp_rlt_node_state104_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_InertialNavigation % LOCAL/187 +x88 : _nat -> INT; + % Chart_main_simp_rlt_node_state100_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_StarPlanetTracker % LOCAL/188 +x89 : _nat -> INT; + % Chart_main_simp_rlt_node_state98_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_StarPlanetTracker % LOCAL/189 +x90 : _nat -> INT; + % Chart_main_simp_rlt_node_state96_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_StarPlanetTracker % LOCAL/190 +x91 : _nat -> INT; + % Chart_main_simp_rlt_node_state82_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState % LOCAL/191 +x92 : _nat -> INT; + % Chart_main_simp_rlt_node_state78_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState % LOCAL/192 +x93 : _nat -> INT; + % Chart_main_simp_rlt_node_state148_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_InertialNavigation % LOCAL/193 +x94 : _nat -> INT; + % Chart_main_simp_rlt_node_state144_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_InertialNavigation % LOCAL/194 +x95 : _nat -> INT; + % Chart_main_simp_rlt_node_state136_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_GPS % LOCAL/195 +x96 : _nat -> INT; + % Chart_main_simp_rlt_node_state134_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_GPS % LOCAL/196 +x97 : _nat -> INT; + % Chart_main_simp_rlt_node_state132_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_GPS % LOCAL/197 +x98 : _nat -> INT; + % Chart_main_simp_rlt_node_state130_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState2 % LOCAL/198 +x99 : _nat -> INT; + % Chart_main_simp_rlt_node_state128_rlt_chart_data_states_Chart_MissionPhaseStates_CaptureApproach_OrbitalState_Active_OrbitalState_Complex_OrbitalState2 % LOCAL/199 + + +% Generic definitions +DEF__174 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x74(_M)) = (IF (_M = _base) THEN FALSE ELSE (x20((_M - 1))) ENDIF)); +DEF__176 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x76(_M)) = (IF (_M = _base) THEN FALSE ELSE (x15((_M - 1))) ENDIF)); +DEF__177 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x77(_M)) = (IF ((x83(_M)) = 1) THEN (x42(_M)) ELSE (IF ((x83(_M)) = 2) THEN (x42(_M)) ELSE (IF ((x83(_M)) = 3) THEN (x103(_M)) ELSE (IF ((x83(_M)) = 4) THEN (IF ((NOT ((((((((x2(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x2(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x2(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52(_M)) = 2) OR ((x53(_M)) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x3(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x3(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (x42(_M)) ELSE (x103(_M)) ENDIF) ELSE (x103(_M)) ENDIF) ELSE (x103(_M)) ENDIF) ELSE (x42(_M)) ENDIF) ENDIF) ENDIF) ENDIF)); +DEF__178 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x78(_M)) = (IF ((x83(_M)) = 1) THEN (x43(_M)) ELSE (IF ((x83(_M)) = 2) THEN (x43(_M)) ELSE (IF ((x83(_M)) = 3) THEN (x104(_M)) ELSE (IF ((x83(_M)) = 4) THEN (IF ((NOT ((((((((x2(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x2(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x2(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52(_M)) = 2) OR ((x53(_M)) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x3(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x3(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (x43(_M)) ELSE (x104(_M)) ENDIF) ELSE (x104(_M)) ENDIF) ELSE (x104(_M)) ENDIF) ELSE (x43(_M)) ENDIF) ENDIF) ENDIF) ENDIF)); +DEF__179 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x79(_M)) = (IF ((x83(_M)) = 1) THEN (x52(_M)) ELSE (IF ((x83(_M)) = 2) THEN (x52(_M)) ELSE (IF ((x83(_M)) = 3) THEN (x108(_M)) ELSE (IF ((x83(_M)) = 4) THEN (IF ((NOT ((((((((x2(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x2(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x2(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52(_M)) = 2) OR ((x53(_M)) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x3(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x3(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (x52(_M)) ELSE (x108(_M)) ENDIF) ELSE (x108(_M)) ENDIF) ELSE (x108(_M)) ENDIF) ELSE (x52(_M)) ENDIF) ENDIF) ENDIF) ENDIF)); +DEF__180 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x80(_M)) = (IF ((x83(_M)) = 1) THEN (x85(_M)) ELSE (IF ((x83(_M)) = 2) THEN (x85(_M)) ELSE (IF ((x83(_M)) = 3) THEN (x110(_M)) ELSE (IF ((x83(_M)) = 4) THEN (IF ((NOT ((((((((x2(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x2(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x2(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52(_M)) = 2) OR ((x53(_M)) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x3(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x3(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (x85(_M)) ELSE (x110(_M)) ENDIF) ELSE (x110(_M)) ENDIF) ELSE (x110(_M)) ENDIF) ELSE (x85(_M)) ENDIF) ENDIF) ENDIF) ENDIF)); +DEF__181 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x81(_M)) = (IF ((x63(_M)) = 1) THEN (x58(_M)) ELSE (IF ((x63(_M)) = 2) THEN (x58(_M)) ELSE (IF ((x63(_M)) = 3) THEN (x58(_M)) ELSE (IF ((x63(_M)) = 4) THEN (x95(_M)) ELSE (IF ((x63(_M)) = 5) THEN (x95(_M)) ELSE (x58(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF)); +DEF__182 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x82(_M)) = (IF ((x63(_M)) = 1) THEN (x60(_M)) ELSE (IF ((x63(_M)) = 2) THEN (x60(_M)) ELSE (IF ((x63(_M)) = 3) THEN (x60(_M)) ELSE (IF ((x63(_M)) = 4) THEN (x98(_M)) ELSE (IF ((x63(_M)) = 5) THEN (x98(_M)) ELSE (x60(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF)); +DEF__183 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x83(_M)) = (IF ((x63(_M)) = 1) THEN (x61(_M)) ELSE (IF ((x63(_M)) = 2) THEN (x61(_M)) ELSE (IF ((x63(_M)) = 3) THEN (x61(_M)) ELSE (IF ((x63(_M)) = 4) THEN (x100(_M)) ELSE (IF ((x63(_M)) = 5) THEN (x100(_M)) ELSE (x61(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF)); +DEF__184 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x84(_M)) = (IF ((x63(_M)) = 1) THEN (x62(_M)) ELSE (IF ((x63(_M)) = 2) THEN (x62(_M)) ELSE (IF ((x63(_M)) = 3) THEN (x62(_M)) ELSE (IF ((x63(_M)) = 4) THEN (x88(_M)) ELSE (IF ((x63(_M)) = 5) THEN (x88(_M)) ELSE (x62(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF)); +DEF__185 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x85(_M)) = (IF ((x63(_M)) = 1) THEN (x64(_M)) ELSE (IF ((x63(_M)) = 2) THEN (x64(_M)) ELSE (IF ((x63(_M)) = 3) THEN (x64(_M)) ELSE (IF ((x63(_M)) = 4) THEN (x93(_M)) ELSE (IF ((x63(_M)) = 5) THEN (x93(_M)) ELSE (x64(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF)); +DEF__186 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x86(_M)) = (IF ((x63(_M)) = 1) THEN (x65(_M)) ELSE (IF ((x63(_M)) = 2) THEN (x65(_M)) ELSE (IF ((x63(_M)) = 3) THEN (x65(_M)) ELSE (IF ((x63(_M)) = 4) THEN 10 ELSE (IF ((x63(_M)) = 5) THEN 2 ELSE (x65(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF)); +DEF__187 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x87(_M)) = (IF ((x94(_M)) = 2) THEN 0 ELSE (x94(_M)) ENDIF)); +DEF__188 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x88(_M)) = (IF ((x89(_M)) = 3) THEN 0 ELSE (x89(_M)) ENDIF)); +DEF__189 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x89(_M)) = (IF ((x90(_M)) = 2) THEN 0 ELSE (x90(_M)) ENDIF)); +DEF__190 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x90(_M)) = (IF ((x62(_M)) = 1) THEN 0 ELSE (x62(_M)) ENDIF)); +DEF__191 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x91(_M)) = (IF ((x101(_M)) = 3) THEN 0 ELSE (x101(_M)) ENDIF)); +DEF__192 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x92(_M)) = (IF ((x61(_M)) = 1) THEN 0 ELSE (x61(_M)) ENDIF)); +DEF__193 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x93(_M)) = (IF ((x87(_M)) = 3) THEN 0 ELSE (x87(_M)) ENDIF)); +DEF__194 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x94(_M)) = (IF ((x64(_M)) = 1) THEN 0 ELSE (x64(_M)) ENDIF)); +DEF__195 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x95(_M)) = (IF ((x96(_M)) = 3) THEN 0 ELSE (x96(_M)) ENDIF)); +DEF__196 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x96(_M)) = (IF ((x97(_M)) = 2) THEN 0 ELSE (x97(_M)) ENDIF)); +DEF__197 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x97(_M)) = (IF ((x58(_M)) = 1) THEN 0 ELSE (x58(_M)) ENDIF)); +DEF__198 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x98(_M)) = (IF ((x99(_M)) = 2) THEN 0 ELSE (x99(_M)) ENDIF)); +DEF__199 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x99(_M)) = (IF ((x60(_M)) = 1) THEN 0 ELSE (x60(_M)) ENDIF)); +DEF__200 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x100(_M)) = (IF ((x91(_M)) = 4) THEN 0 ELSE (x91(_M)) ENDIF)); +DEF__201 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x101(_M)) = (IF ((x92(_M)) = 2) THEN 0 ELSE (x92(_M)) ENDIF)); +DEF__202 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x102(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN 2 ELSE (x39(_M)) ENDIF)); +DEF__115 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x15(_M)) = (IF ((NOT ((x59(_M)) = 0)) <=> TRUE) THEN (IF ((x65(_M)) = 1) THEN (x76(_M)) ELSE (IF ((x65(_M)) = 2) THEN ((NOT ((x14(_M)) = 8)) AND ((NOT ((x14(_M)) = 6)) AND (x76(_M)))) ELSE (IF ((x65(_M)) = 3) THEN (x76(_M)) ELSE (IF ((x65(_M)) = 4) THEN (x76(_M)) ELSE (IF ((x65(_M)) = 5) THEN (x76(_M)) ELSE (IF ((x65(_M)) = 6) THEN (x76(_M)) ELSE (IF ((x65(_M)) = 7) THEN (x76(_M)) ELSE (IF ((x65(_M)) = 8) THEN (x76(_M)) ELSE (IF ((x65(_M)) = 9) THEN (IF ((x63(_M)) = 1) THEN (x76(_M)) ELSE (IF ((x63(_M)) = 2) THEN (x76(_M)) ELSE (IF ((x63(_M)) = 3) THEN (x76(_M)) ELSE (((x63(_M)) = 4) OR (x76(_M))) ENDIF) ENDIF) ENDIF) ELSE (x76(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x76(_M)) ENDIF)); +DEF__203 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x103(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN (IF ((x86(_M)) = 9) THEN (IF ((x85(_M)) = 1) THEN 2 ELSE (IF ((x85(_M)) = 2) THEN (IF ((x30(_M)) = 6) THEN 1 ELSE (IF ((x30(_M)) < 6) THEN 2 ELSE (IF ((x11(_M)) <=> TRUE) THEN 0 ELSE (x42(_M)) ENDIF) ENDIF) ENDIF) ELSE (IF ((x85(_M)) = 3) THEN 2 ELSE (x42(_M)) ENDIF) ENDIF) ENDIF) ELSE (x42(_M)) ENDIF) ELSE (x42(_M)) ENDIF)); +DEF__116 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x16(_M)) = (IF ((NOT ((x59(_M)) = 0)) <=> TRUE) THEN (IF ((x65(_M)) = 1) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 2) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 3) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 4) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 5) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 6) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 7) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 8) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 9) THEN (IF ((x63(_M)) = 1) THEN (x73(_M)) ELSE (IF ((x63(_M)) = 2) THEN (x73(_M)) ELSE (IF ((x63(_M)) = 3) THEN (x73(_M)) ELSE ((NOT ((x63(_M)) = 4)) AND (x73(_M))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65(_M)) = 10) THEN (IF ((x55(_M)) = 1) THEN (x73(_M)) ELSE (IF ((x55(_M)) = 2) THEN (x73(_M)) ELSE (((x55(_M)) = 3) OR (x73(_M))) ENDIF) ENDIF) ELSE (IF ((x65(_M)) = 11) THEN (x73(_M)) ELSE (IF ((x65(_M)) = 12) THEN (IF ((x57(_M)) = 1) THEN (x73(_M)) ELSE (IF ((x57(_M)) = 2) THEN (x73(_M)) ELSE ((NOT ((x57(_M)) = 3)) AND (x73(_M))) ENDIF) ENDIF) ELSE (x73(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x73(_M)) ENDIF)); +DEF__204 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x104(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN (IF ((x86(_M)) = 9) THEN (IF ((x85(_M)) = 1) THEN 2 ELSE (IF ((x85(_M)) = 2) THEN (IF ((x30(_M)) = 6) THEN 1 ELSE (IF ((x30(_M)) < 6) THEN 2 ELSE (IF ((x11(_M)) <=> TRUE) THEN 0 ELSE (x43(_M)) ENDIF) ENDIF) ENDIF) ELSE (IF ((x85(_M)) = 3) THEN 2 ELSE (x43(_M)) ENDIF) ENDIF) ENDIF) ELSE (x43(_M)) ENDIF) ELSE (x43(_M)) ENDIF)); +DEF__117 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x17(_M)) = (IF ((NOT ((x59(_M)) = 0)) <=> TRUE) THEN (IF ((x65(_M)) = 1) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 2) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 3) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 4) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 5) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 6) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 7) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 8) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 9) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 10) THEN (IF ((x55(_M)) = 1) THEN (x68(_M)) ELSE (IF ((x55(_M)) = 2) THEN (x68(_M)) ELSE (((x55(_M)) = 3) OR (x68(_M))) ENDIF) ENDIF) ELSE (IF ((x65(_M)) = 11) THEN (x68(_M)) ELSE (IF ((x65(_M)) = 12) THEN (IF ((x57(_M)) = 1) THEN (x68(_M)) ELSE (IF ((x57(_M)) = 2) THEN (x68(_M)) ELSE ((NOT ((x57(_M)) = 3)) AND ((NOT ((x57(_M)) = 4)) AND (x68(_M)))) ENDIF) ENDIF) ELSE (x68(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x68(_M)) ENDIF)); +DEF__205 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x105(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN (IF ((x86(_M)) = 9) THEN (IF ((x85(_M)) = 1) THEN 0 ELSE (IF ((x85(_M)) = 2) THEN (IF ((x30(_M)) = 6) THEN (x30(_M)) ELSE (IF ((x30(_M)) < 6) THEN 0 ELSE (x30(_M)) ENDIF) ENDIF) ELSE (IF ((x85(_M)) = 3) THEN 0 ELSE (x30(_M)) ENDIF) ENDIF) ENDIF) ELSE (x44(_M)) ENDIF) ELSE (x44(_M)) ENDIF)); +DEF__206 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x106(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN 2 ELSE (x47(_M)) ENDIF)); +DEF__207 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x107(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN 2 ELSE (x48(_M)) ENDIF)); +DEF__120 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x20(_M)) = (IF ((NOT ((x59(_M)) = 0)) <=> TRUE) THEN (IF ((x65(_M)) = 1) THEN (x74(_M)) ELSE (IF ((x65(_M)) = 2) THEN ((NOT ((x14(_M)) = 8)) AND ((NOT ((x14(_M)) = 6)) AND (x74(_M)))) ELSE (IF ((x65(_M)) = 3) THEN (((x14(_M)) = 2) OR (x74(_M))) ELSE (IF ((x65(_M)) = 4) THEN ((NOT ((x14(_M)) = 1)) AND (x74(_M))) ELSE (x74(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x74(_M)) ENDIF)); +DEF__208 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x108(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN (IF ((x86(_M)) = 9) THEN (IF ((x85(_M)) = 1) THEN 2 ELSE (IF ((x85(_M)) = 2) THEN (IF ((x30(_M)) = 6) THEN 1 ELSE (IF ((x30(_M)) < 6) THEN 2 ELSE (IF ((x11(_M)) <=> TRUE) THEN 0 ELSE (x52(_M)) ENDIF) ENDIF) ENDIF) ELSE (IF ((x85(_M)) = 3) THEN 2 ELSE (x52(_M)) ENDIF) ENDIF) ENDIF) ELSE (x52(_M)) ENDIF) ELSE (x52(_M)) ENDIF)); +DEF__121 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x21(_M)) = (IF ((NOT ((x59(_M)) = 0)) <=> TRUE) THEN (IF ((x65(_M)) = 1) THEN (x66(_M)) ELSE (IF ((x65(_M)) = 2) THEN ((NOT ((x14(_M)) = 8)) AND ((NOT ((x14(_M)) = 6)) AND (x66(_M)))) ELSE (IF ((x65(_M)) = 3) THEN (x66(_M)) ELSE (IF ((x65(_M)) = 4) THEN (x66(_M)) ELSE (IF ((x65(_M)) = 5) THEN (x66(_M)) ELSE (IF ((x65(_M)) = 6) THEN (IF ((x14(_M)) = 5) THEN (x66(_M)) ELSE (((x14(_M)) = 4) OR (x66(_M))) ENDIF) ELSE (x66(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x66(_M)) ENDIF)); +DEF__209 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x109(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN 4 ELSE (x83(_M)) ENDIF)); +DEF__122 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x22(_M)) = (IF ((NOT ((x59(_M)) = 0)) <=> TRUE) THEN (IF ((x65(_M)) = 1) THEN (x71(_M)) ELSE (IF ((x65(_M)) = 2) THEN ((NOT ((x14(_M)) = 8)) AND ((NOT ((x14(_M)) = 6)) AND (x71(_M)))) ELSE (IF ((x65(_M)) = 3) THEN (x71(_M)) ELSE (IF ((x65(_M)) = 4) THEN (IF ((x14(_M)) = 1) THEN (x71(_M)) ELSE (((x14(_M)) = 3) OR (x71(_M))) ENDIF) ELSE (x71(_M)) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x71(_M)) ENDIF)); +DEF__210 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x110(_M)) = (IF (((((((x2(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) AND ((((x3(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2))) AND ((x53(_M)) = 2)) <=> TRUE) THEN (IF ((x86(_M)) = 9) THEN (IF ((x85(_M)) = 1) THEN 2 ELSE (IF ((x85(_M)) = 2) THEN (IF ((x30(_M)) = 6) THEN 3 ELSE (IF ((x30(_M)) < 6) THEN 2 ELSE (IF ((x11(_M)) <=> TRUE) THEN 1 ELSE (x85(_M)) ENDIF) ENDIF) ENDIF) ELSE (IF ((x85(_M)) = 3) THEN 2 ELSE (x85(_M)) ENDIF) ENDIF) ENDIF) ELSE (x85(_M)) ENDIF) ELSE (x85(_M)) ENDIF)); +DEF__211 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x111(_M)) = (IF (((((x12(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) <=> TRUE) THEN 2 ELSE (x36(_M)) ENDIF)); +DEF__212 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x112(_M)) = (IF (((((x12(_M)) = 2) OR ((x50(_M)) = 2)) OR ((x53(_M)) = 2)) <=> TRUE) THEN 2 ELSE (x82(_M)) ENDIF)); +DEF__126 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x26(_M)) = (IF (((x37(_M)) + 1) < 9) THEN ((x37(_M)) + 1) ELSE 9 ENDIF)); +DEF__213 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x113(_M)) = (IF ((x11(_M)) <=> TRUE) THEN 0 ELSE (x77(_M)) ENDIF)); +DEF__127 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x27(_M)) = (IF (((x51(_M)) + 1) < 9) THEN ((x51(_M)) + 1) ELSE 9 ENDIF)); +DEF__214 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x114(_M)) = (IF ((x11(_M)) <=> TRUE) THEN 0 ELSE (x78(_M)) ENDIF)); +DEF__128 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x28(_M)) = ((IF ((x55(_M)) = 1) THEN (x46(_M)) ELSE (IF ((x55(_M)) = 2) THEN (x46(_M)) ELSE (IF ((x55(_M)) = 3) THEN (x118(_M)) ELSE (IF ((x55(_M)) = 4) THEN (x118(_M)) ELSE (x46(_M)) ENDIF) ENDIF) ENDIF) ENDIF) + 1)); +DEF__215 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x115(_M)) = (IF ((x11(_M)) <=> TRUE) THEN 0 ELSE (x79(_M)) ENDIF)); +DEF__216 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x116(_M)) = (IF ((x11(_M)) <=> TRUE) THEN 1 ELSE (x80(_M)) ENDIF)); +DEF__129 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x29(_M)) = (IF ((x28(_M)) < 6) THEN (x28(_M)) ELSE 6 ENDIF)); +DEF__217 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x117(_M)) = (IF ((x55(_M)) = 1) THEN (x54(_M)) ELSE (IF ((x55(_M)) = 2) THEN (x54(_M)) ELSE (IF ((x55(_M)) = 3) THEN (x119(_M)) ELSE (IF ((x55(_M)) = 4) THEN (x119(_M)) ELSE (x54(_M)) ENDIF) ENDIF) ENDIF) ENDIF)); +DEF__130 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x30(_M)) = (IF (((x44(_M)) + 1) < 6) THEN ((x44(_M)) + 1) ELSE 6 ENDIF)); +DEF__131 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x31(_M)) = (IF (((x40(_M)) + 1) < 11) THEN ((x40(_M)) + 1) ELSE 11 ENDIF)); +DEF__218 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x118(_M)) = (IF ((x120(_M)) = 3) THEN 0 ELSE (IF ((x54(_M)) = 1) THEN 0 ELSE (x46(_M)) ENDIF) ENDIF)); +DEF__132 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x32(_M)) = (IF (((x41(_M)) + 1) < 6) THEN ((x41(_M)) + 1) ELSE 6 ENDIF)); +DEF__219 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x119(_M)) = (IF ((x120(_M)) = 3) THEN 0 ELSE (x120(_M)) ENDIF)); +DEF__133 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x33(_M)) = (IF (((x38(_M)) + 1) < 6) THEN ((x38(_M)) + 1) ELSE 6 ENDIF)); +DEF__220 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x120(_M)) = (IF ((x121(_M)) = 2) THEN 0 ELSE (x121(_M)) ENDIF)); +DEF__134 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x34(_M)) = ((IF ((x83(_M)) = 1) THEN (x44(_M)) ELSE (IF ((x83(_M)) = 2) THEN (x44(_M)) ELSE (IF ((x83(_M)) = 3) THEN (x105(_M)) ELSE (IF ((x83(_M)) = 4) THEN (IF ((NOT ((((((((x2(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x2(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x2(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x43(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52(_M)) = 2) OR ((x53(_M)) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3(_M)) = 2) AND ((x50(_M)) = 2)) OR (((x3(_M)) = 2) AND ((x53(_M)) = 2))) OR (((x53(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x3(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x50(_M)) = 2))) OR (((x42(_M)) = 2) AND ((x53(_M)) = 2)))) <=> TRUE) THEN (x44(_M)) ELSE (x105(_M)) ENDIF) ELSE (x105(_M)) ENDIF) ELSE (x105(_M)) ENDIF) ELSE (x44(_M)) ENDIF) ENDIF) ENDIF) ENDIF) + 1)); +DEF__221 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x121(_M)) = (IF ((x54(_M)) = 1) THEN 0 ELSE (x54(_M)) ENDIF)); +DEF__222 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x122(_M)) = (IF ((x57(_M)) = 1) THEN (x56(_M)) ELSE (IF ((x57(_M)) = 2) THEN (x56(_M)) ELSE (IF ((x57(_M)) = 3) THEN (x126(_M)) ELSE (IF ((x57(_M)) = 4) THEN (x126(_M)) ELSE (x56(_M)) ENDIF) ENDIF) ENDIF) ENDIF)); +DEF__135 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x35(_M)) = (IF ((x34(_M)) < 6) THEN (x34(_M)) ELSE 6 ENDIF)); +DEF__223 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x123(_M)) = (IF ((x26(_M)) = 8) THEN 3 ELSE (x57(_M)) ENDIF)); +DEF__136 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x36(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x36((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x36((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x36((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x36((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x36((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x36((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 1 ELSE (x36((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x36((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x36((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x82((_M - 1))) = 1) THEN (x111((_M - 1))) ELSE (IF ((x82((_M - 1))) = 2) THEN (IF ((NOT ((x13((_M - 1))) = 2)) <=> TRUE) THEN 1 ELSE (x111((_M - 1))) ENDIF) ELSE (x36((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x36((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x36((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x36((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 1 ELSE (x36((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x36((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x36((_M - 1))) ENDIF) ENDIF)); +DEF__224 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x124(_M)) = (IF ((x128(_M)) = 3) THEN 0 ELSE (x128(_M)) ENDIF)); +DEF__137 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x37(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x37((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x37((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN 0 ELSE (x37((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 11) THEN (x37((_M - 1))) ELSE (IF ((x65((_M - 1))) = 12) THEN (x26((_M - 1))) ELSE (x37((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x37((_M - 1))) ENDIF) ENDIF)); +DEF__225 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x125(_M)) = (IF ((x56(_M)) = 1) THEN 0 ELSE (x56(_M)) ENDIF)); +DEF__138 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x38(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x38((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x38((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x38((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x38((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x38((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x38((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x38((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x38((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x84((_M - 1))) = 1) THEN (IF (((NOT (((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0))) AND (x5((_M - 1)))) <=> TRUE) THEN 0 ELSE (x33((_M - 1))) ENDIF) ELSE (IF ((x84((_M - 1))) = 2) THEN (IF ((((x33((_M - 1))) = 6) AND ((((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0)) OR (NOT (x5((_M - 1)))))) <=> TRUE) THEN (x33((_M - 1))) ELSE (IF (((((((x33((_M - 1))) = 6) AND ((x9((_M - 1))) = 2)) AND ((x10((_M - 1))) = 2)) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN (x33((_M - 1))) ELSE (IF (((((x33((_M - 1))) < 6) AND ((((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0)) OR (NOT (x5((_M - 1)))))) OR ((x5((_M - 1))) AND (((x6((_M - 1))) OR ((x9((_M - 1))) = 1)) OR ((x10((_M - 1))) = 1)))) <=> TRUE) THEN 0 ELSE (x33((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x84((_M - 1))) = 3) THEN (IF (((((NOT ((x9((_M - 1))) = 2)) AND (NOT ((x10((_M - 1))) = 2))) AND (NOT (x5((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 0 ELSE (x33((_M - 1))) ENDIF) ELSE (x33((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (x38((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x38((_M - 1))) ENDIF) ENDIF)); +DEF__226 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x126(_M)) = (IF ((x127(_M)) = 5) THEN 0 ELSE (x127(_M)) ENDIF)); +DEF__139 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x39(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x39((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x39((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x39((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x39((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x39((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x39((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x39((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x39((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x39((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x83((_M - 1))) = 1) THEN (IF (((NOT ((((x50((_M - 1))) = 0) AND ((x53((_M - 1))) = 0)) AND ((x2((_M - 1))) = 0))) AND (NOT ((((x50((_M - 1))) = 0) AND ((x53((_M - 1))) = 0)) AND ((x3((_M - 1))) = 0)))) <=> TRUE) THEN 0 ELSE (IF ((((((((x50((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((x2((_M - 1))) = 0)) AND ((x3((_M - 1))) = 0)) <=> TRUE) THEN 0 ELSE (x39((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x83((_M - 1))) = 2) THEN (IF ((((((x2((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((((x3((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0))) <=> TRUE) THEN 0 ELSE (IF (((((((((x2((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x2((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x2((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF (((((((((x3((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x3((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x3((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF ((((x52((_M - 1))) = 2) OR ((x53((_M - 1))) = 2)) <=> TRUE) THEN 1 ELSE (x39((_M - 1))) ENDIF) ELSE (x39((_M - 1))) ENDIF) ELSE (x39((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x83((_M - 1))) = 3) THEN (x102((_M - 1))) ELSE (IF ((x83((_M - 1))) = 4) THEN (IF ((NOT ((((((((x2((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x2((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x2((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x53((_M - 1))) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52((_M - 1))) = 2) OR ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x3((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x3((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x53((_M - 1))) = 2)))) <=> TRUE) THEN 0 ELSE (x102((_M - 1))) ENDIF) ELSE (x102((_M - 1))) ENDIF) ELSE (x102((_M - 1))) ENDIF) ELSE (x39((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x39((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x39((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x39((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x39((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x39((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x39((_M - 1))) ENDIF) ENDIF)); +DEF__227 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x127(_M)) = (IF ((x124(_M)) = 4) THEN 0 ELSE (x124(_M)) ENDIF)); +DEF__140 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x40(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x40((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x40((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x40((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x40((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x40((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x40((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x40((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x40((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x40((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (x31((_M - 1))) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x40((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x40((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x40((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x40((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x40((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x40((_M - 1))) ENDIF) ENDIF)); +DEF__228 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x128(_M)) = (IF ((x125(_M)) = 2) THEN 0 ELSE (x125(_M)) ENDIF)); +DEF__141 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x41(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x41((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x41((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x41((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x41((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x41((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x41((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x41((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x41((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x81((_M - 1))) = 1) THEN (IF (((NOT ((x7((_M - 1))) = 0)) AND (x8((_M - 1)))) <=> TRUE) THEN 0 ELSE (x32((_M - 1))) ENDIF) ELSE (IF ((x81((_M - 1))) = 2) THEN (IF ((((x32((_M - 1))) = 6) AND (((x7((_M - 1))) = 0) OR (NOT (x8((_M - 1)))))) <=> TRUE) THEN (x32((_M - 1))) ELSE (IF ((((((x32((_M - 1))) = 6) AND ((x7((_M - 1))) = 2)) AND (x8((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN (x32((_M - 1))) ELSE (IF (((((x32((_M - 1))) < 6) AND (((x7((_M - 1))) = 0) OR (NOT (x8((_M - 1)))))) OR ((x8((_M - 1))) AND (((x7((_M - 1))) = 1) OR (x6((_M - 1)))))) <=> TRUE) THEN 0 ELSE (x32((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x81((_M - 1))) = 3) THEN (IF (((NOT (((x7((_M - 1))) = 2) AND (x8((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 0 ELSE (x32((_M - 1))) ENDIF) ELSE (x32((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (x41((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x41((_M - 1))) ENDIF) ENDIF)); +DEF__229 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x129(_M)) = ((NOT (x17(_M))) OR (((((x20(_M)) AND (x22(_M))) AND (x21(_M))) AND (x15(_M))) AND (x16(_M))))); +DEF__142 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x42(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x42((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x42((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x42((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x42((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x42((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x42((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x42((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x42((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x42((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x80((_M - 1))) = 1) THEN (x77((_M - 1))) ELSE (IF ((x80((_M - 1))) = 2) THEN (IF ((x35((_M - 1))) = 6) THEN 1 ELSE (IF ((x35((_M - 1))) < 6) THEN 2 ELSE (x113((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x80((_M - 1))) = 3) THEN (x113((_M - 1))) ELSE (x77((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x42((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x42((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x42((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x42((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x42((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x42((_M - 1))) ENDIF) ENDIF)); +DEF__143 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x43(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x43((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x43((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x43((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x43((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x43((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x43((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x43((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x43((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x43((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x80((_M - 1))) = 1) THEN (x78((_M - 1))) ELSE (IF ((x80((_M - 1))) = 2) THEN (IF ((x35((_M - 1))) = 6) THEN 1 ELSE (IF ((x35((_M - 1))) < 6) THEN 2 ELSE (x114((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x80((_M - 1))) = 3) THEN (x114((_M - 1))) ELSE (x78((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x43((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x43((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x43((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x43((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x43((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x43((_M - 1))) ENDIF) ENDIF)); +DEF__144 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x44(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x44((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x44((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x44((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x44((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x44((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x44((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x44((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x44((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x80((_M - 1))) = 1) THEN (x35((_M - 1))) ELSE (IF ((x80((_M - 1))) = 2) THEN (IF ((x35((_M - 1))) = 6) THEN (x35((_M - 1))) ELSE (IF ((x35((_M - 1))) < 6) THEN 0 ELSE (x35((_M - 1))) ENDIF) ENDIF) ELSE (x35((_M - 1))) ENDIF) ENDIF) ELSE (x44((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x44((_M - 1))) ENDIF) ENDIF)); +DEF__145 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x45(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x45((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x45((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN 0 ELSE (x45((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 11) THEN (x45((_M - 1))) ELSE (IF ((x65((_M - 1))) = 12) THEN (IF ((x122((_M - 1))) = 1) THEN 1 ELSE (IF ((x122((_M - 1))) = 2) THEN 0 ELSE (IF ((x122((_M - 1))) = 3) THEN 3 ELSE (IF ((x122((_M - 1))) = 4) THEN 0 ELSE (IF ((x122((_M - 1))) = 5) THEN 0 ELSE (x45((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x45((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x45((_M - 1))) ENDIF) ENDIF)); +DEF__146 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x46(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (x46((_M - 1))) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x117((_M - 1))) = 1) THEN (IF (((NOT ((x4((_M - 1))) = 0)) AND (x5((_M - 1)))) <=> TRUE) THEN 0 ELSE (IF ((((x4((_M - 1))) = 0) OR (NOT (x5((_M - 1))))) <=> TRUE) THEN 0 ELSE (x29((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x117((_M - 1))) = 2) THEN (x29((_M - 1))) ELSE (IF ((x117((_M - 1))) = 3) THEN (IF ((((NOT ((x4((_M - 1))) = 2)) AND (NOT (x5((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 0 ELSE (IF (((((x4((_M - 1))) = 2) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 0 ELSE (x29((_M - 1))) ENDIF) ENDIF) ELSE (x29((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (x46((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x46((_M - 1))) ENDIF) ENDIF)); +DEF__147 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x47(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x47((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x47((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x47((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x47((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x47((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x47((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x47((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x47((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x47((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x83((_M - 1))) = 1) THEN (IF (((NOT ((((x50((_M - 1))) = 0) AND ((x53((_M - 1))) = 0)) AND ((x2((_M - 1))) = 0))) AND (NOT ((((x50((_M - 1))) = 0) AND ((x53((_M - 1))) = 0)) AND ((x3((_M - 1))) = 0)))) <=> TRUE) THEN 1 ELSE (IF ((((((((x50((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((x2((_M - 1))) = 0)) AND ((x3((_M - 1))) = 0)) <=> TRUE) THEN 0 ELSE (x47((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x83((_M - 1))) = 2) THEN (IF ((((((x2((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((((x3((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0))) <=> TRUE) THEN 0 ELSE (IF (((((((((x2((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x2((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x2((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF (((((((((x3((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x3((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x3((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF ((((x52((_M - 1))) = 2) OR ((x53((_M - 1))) = 2)) <=> TRUE) THEN 2 ELSE (x47((_M - 1))) ENDIF) ELSE (x47((_M - 1))) ENDIF) ELSE (x47((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x83((_M - 1))) = 3) THEN (x106((_M - 1))) ELSE (IF ((x83((_M - 1))) = 4) THEN (IF ((NOT ((((((((x2((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x2((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x2((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x53((_M - 1))) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52((_M - 1))) = 2) OR ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x3((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x3((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x53((_M - 1))) = 2)))) <=> TRUE) THEN 1 ELSE (x106((_M - 1))) ENDIF) ELSE (x106((_M - 1))) ENDIF) ELSE (x106((_M - 1))) ENDIF) ELSE (x47((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x47((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x47((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x47((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x47((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x47((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x47((_M - 1))) ENDIF) ENDIF)); +DEF__148 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x48(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x48((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x48((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x48((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x48((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x48((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x48((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x48((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x48((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x48((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x83((_M - 1))) = 1) THEN (IF (((NOT ((((x50((_M - 1))) = 0) AND ((x53((_M - 1))) = 0)) AND ((x2((_M - 1))) = 0))) AND (NOT ((((x50((_M - 1))) = 0) AND ((x53((_M - 1))) = 0)) AND ((x3((_M - 1))) = 0)))) <=> TRUE) THEN 1 ELSE (IF ((((((((x50((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((x2((_M - 1))) = 0)) AND ((x3((_M - 1))) = 0)) <=> TRUE) THEN 0 ELSE (x48((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x83((_M - 1))) = 2) THEN (IF ((((((x2((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((((x3((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0))) <=> TRUE) THEN 0 ELSE (IF (((((((((x2((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x2((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x2((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF (((((((((x3((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x3((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x3((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF ((((x52((_M - 1))) = 2) OR ((x53((_M - 1))) = 2)) <=> TRUE) THEN 2 ELSE (x48((_M - 1))) ENDIF) ELSE (x48((_M - 1))) ENDIF) ELSE (x48((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x83((_M - 1))) = 3) THEN (x107((_M - 1))) ELSE (IF ((x83((_M - 1))) = 4) THEN (IF ((NOT ((((((((x2((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x2((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x2((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x53((_M - 1))) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52((_M - 1))) = 2) OR ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x3((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x3((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x53((_M - 1))) = 2)))) <=> TRUE) THEN 1 ELSE (x107((_M - 1))) ENDIF) ELSE (x107((_M - 1))) ENDIF) ELSE (x107((_M - 1))) ENDIF) ELSE (x48((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x48((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x48((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x48((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x48((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x48((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x48((_M - 1))) ENDIF) ENDIF)); +DEF__149 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x49(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x63((_M - 1))) = 1) THEN (x49((_M - 1))) ELSE (IF ((x63((_M - 1))) = 2) THEN (x49((_M - 1))) ELSE (IF ((x63((_M - 1))) = 3) THEN (x49((_M - 1))) ELSE (IF ((x63((_M - 1))) = 4) THEN 0 ELSE (x49((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x117((_M - 1))) = 1) THEN (IF (((NOT ((x4((_M - 1))) = 0)) AND (x5((_M - 1)))) <=> TRUE) THEN 1 ELSE (IF ((((x4((_M - 1))) = 0) OR (NOT (x5((_M - 1))))) <=> TRUE) THEN 0 ELSE (x49((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x117((_M - 1))) = 2) THEN (IF ((((x29((_M - 1))) = 6) AND (((x4((_M - 1))) = 0) OR (NOT (x5((_M - 1)))))) <=> TRUE) THEN 0 ELSE (IF ((((((x29((_M - 1))) < 6) AND ((x4((_M - 1))) = 2)) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 2 ELSE (IF (((((x29((_M - 1))) < 6) AND (((x4((_M - 1))) = 0) OR (NOT (x5((_M - 1)))))) OR ((x5((_M - 1))) AND (((x4((_M - 1))) = 1) OR (x6((_M - 1)))))) <=> TRUE) THEN 1 ELSE (x49((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x117((_M - 1))) = 3) THEN (IF ((((NOT ((x4((_M - 1))) = 2)) AND (NOT (x5((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 1 ELSE (IF (((((x4((_M - 1))) = 2) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 2 ELSE (x49((_M - 1))) ENDIF) ENDIF) ELSE (x49((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 11) THEN (x49((_M - 1))) ELSE (IF ((x65((_M - 1))) = 12) THEN (IF ((x57((_M - 1))) = 1) THEN (x49((_M - 1))) ELSE (IF ((x57((_M - 1))) = 2) THEN (x49((_M - 1))) ELSE (IF ((x57((_M - 1))) = 3) THEN 0 ELSE (x49((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (x49((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x49((_M - 1))) ENDIF) ENDIF)); +DEF__150 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x50(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x50((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x50((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x50((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x50((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x50((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x50((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x50((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x50((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x50((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x81((_M - 1))) = 1) THEN (IF (((NOT ((x7((_M - 1))) = 0)) AND (x8((_M - 1)))) <=> TRUE) THEN 1 ELSE (IF ((((x7((_M - 1))) = 0) OR (NOT (x8((_M - 1))))) <=> TRUE) THEN 0 ELSE (x50((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x81((_M - 1))) = 2) THEN (IF ((((x32((_M - 1))) = 6) AND (((x7((_M - 1))) = 0) OR (NOT (x8((_M - 1)))))) <=> TRUE) THEN 0 ELSE (IF ((((((x32((_M - 1))) = 6) AND ((x7((_M - 1))) = 2)) AND (x8((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 2 ELSE (IF (((((x32((_M - 1))) < 6) AND (((x7((_M - 1))) = 0) OR (NOT (x8((_M - 1)))))) OR ((x8((_M - 1))) AND (((x7((_M - 1))) = 1) OR (x6((_M - 1)))))) <=> TRUE) THEN 1 ELSE (x50((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x81((_M - 1))) = 3) THEN (IF (((NOT (((x7((_M - 1))) = 2) AND (x8((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 1 ELSE 2 ENDIF) ELSE (x50((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x50((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x50((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x50((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x50((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x50((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x50((_M - 1))) ENDIF) ENDIF)); +DEF__151 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x51(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x63((_M - 1))) = 1) THEN (x51((_M - 1))) ELSE (IF ((x63((_M - 1))) = 2) THEN (x51((_M - 1))) ELSE (IF ((x63((_M - 1))) = 3) THEN (x51((_M - 1))) ELSE (IF ((x63((_M - 1))) = 4) THEN 0 ELSE (x51((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (x27((_M - 1))) ELSE (IF ((x65((_M - 1))) = 11) THEN (x51((_M - 1))) ELSE (IF ((x65((_M - 1))) = 12) THEN (IF ((x57((_M - 1))) = 1) THEN (x51((_M - 1))) ELSE (IF ((x57((_M - 1))) = 2) THEN (x51((_M - 1))) ELSE (IF ((x57((_M - 1))) = 3) THEN 0 ELSE (x51((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (x51((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x51((_M - 1))) ENDIF) ENDIF)); +DEF__152 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x52(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x52((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x52((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x52((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x52((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x52((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x52((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x52((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x52((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x52((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x80((_M - 1))) = 1) THEN (x79((_M - 1))) ELSE (IF ((x80((_M - 1))) = 2) THEN (IF ((x35((_M - 1))) = 6) THEN 1 ELSE (IF ((x35((_M - 1))) < 6) THEN 2 ELSE (x115((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x80((_M - 1))) = 3) THEN (x115((_M - 1))) ELSE (x79((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x52((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x52((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x52((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x52((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x52((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x52((_M - 1))) ENDIF) ENDIF)); +DEF__153 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x53(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x53((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x53((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x53((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x53((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x53((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x53((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 0 ELSE (x53((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x53((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x53((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x84((_M - 1))) = 1) THEN (IF (((NOT (((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0))) AND (x5((_M - 1)))) <=> TRUE) THEN 1 ELSE 0 ENDIF) ELSE (IF ((x84((_M - 1))) = 2) THEN (IF ((((x33((_M - 1))) = 6) AND ((((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0)) OR (NOT (x5((_M - 1)))))) <=> TRUE) THEN 0 ELSE (IF (((((((x33((_M - 1))) = 6) AND ((x9((_M - 1))) = 2)) AND ((x10((_M - 1))) = 2)) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 2 ELSE (IF (((((x33((_M - 1))) < 6) AND ((((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0)) OR (NOT (x5((_M - 1)))))) OR ((x5((_M - 1))) AND (((x6((_M - 1))) OR ((x9((_M - 1))) = 1)) OR ((x10((_M - 1))) = 1)))) <=> TRUE) THEN 1 ELSE (x53((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x84((_M - 1))) = 3) THEN (IF (((((NOT ((x9((_M - 1))) = 2)) AND (NOT ((x10((_M - 1))) = 2))) AND (NOT (x5((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 1 ELSE (IF ((((((x9((_M - 1))) = 2) AND ((x10((_M - 1))) = 2)) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 2 ELSE (x53((_M - 1))) ENDIF) ENDIF) ELSE (x53((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x53((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x53((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x53((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (x53((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x53((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x53((_M - 1))) ENDIF) ENDIF)); +DEF__154 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x54(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x63((_M - 1))) = 1) THEN (x54((_M - 1))) ELSE (IF ((x63((_M - 1))) = 2) THEN (x54((_M - 1))) ELSE (IF ((x63((_M - 1))) = 3) THEN (x54((_M - 1))) ELSE (IF ((x63((_M - 1))) = 4) THEN 1 ELSE (x54((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x117((_M - 1))) = 1) THEN (IF (((NOT ((x4((_M - 1))) = 0)) AND (x5((_M - 1)))) <=> TRUE) THEN 2 ELSE (IF ((((x4((_M - 1))) = 0) OR (NOT (x5((_M - 1))))) <=> TRUE) THEN 1 ELSE (x117((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x117((_M - 1))) = 2) THEN (IF ((((x29((_M - 1))) = 6) AND (((x4((_M - 1))) = 0) OR (NOT (x5((_M - 1)))))) <=> TRUE) THEN 1 ELSE (IF ((((((x29((_M - 1))) < 6) AND ((x4((_M - 1))) = 2)) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 3 ELSE (IF (((((x29((_M - 1))) < 6) AND (((x4((_M - 1))) = 0) OR (NOT (x5((_M - 1)))))) OR ((x5((_M - 1))) AND (((x4((_M - 1))) = 1) OR (x6((_M - 1)))))) <=> TRUE) THEN 2 ELSE (x117((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x117((_M - 1))) = 3) THEN (IF ((((NOT ((x4((_M - 1))) = 2)) AND (NOT (x5((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 2 ELSE (IF (((((x4((_M - 1))) = 2) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 3 ELSE (x117((_M - 1))) ENDIF) ENDIF) ELSE (x117((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 11) THEN (x54((_M - 1))) ELSE (IF ((x65((_M - 1))) = 12) THEN (IF ((x57((_M - 1))) = 1) THEN (x54((_M - 1))) ELSE (IF ((x57((_M - 1))) = 2) THEN (x54((_M - 1))) ELSE (IF ((x57((_M - 1))) = 3) THEN 1 ELSE (x54((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (x54((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x54((_M - 1))) ENDIF) ENDIF)); +DEF__155 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x55(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x63((_M - 1))) = 1) THEN (x55((_M - 1))) ELSE (IF ((x63((_M - 1))) = 2) THEN (x55((_M - 1))) ELSE (IF ((x63((_M - 1))) = 3) THEN (x55((_M - 1))) ELSE (IF ((x63((_M - 1))) = 4) THEN 1 ELSE (x55((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (IF (((((NOT ((x49((_M - 1))) = 0)) AND (NOT ((x49((_M - 1))) = 0))) AND (NOT ((x49((_M - 1))) = 0))) AND ((x27((_M - 1))) < 9)) <=> TRUE) THEN 2 ELSE (IF ((x27((_M - 1))) = 9) THEN 4 ELSE (x55((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x55((_M - 1))) = 2) THEN (IF (((((x49((_M - 1))) = 2) AND (((x49((_M - 1))) = 2) AND ((x49((_M - 1))) = 2))) AND ((x49((_M - 1))) = 2)) <=> TRUE) THEN 3 ELSE (IF ((((((x49((_M - 1))) = 1) AND ((x49((_M - 1))) = 1)) AND ((x49((_M - 1))) = 1)) AND ((x49((_M - 1))) = 1)) <=> TRUE) THEN 5 ELSE (IF ((x27((_M - 1))) = 9) THEN 4 ELSE (IF (((((x49((_M - 1))) = 0) OR ((x49((_M - 1))) = 0)) OR ((x49((_M - 1))) = 0)) <=> TRUE) THEN 4 ELSE (IF ((NOT ((x49((_M - 1))) = 2)) <=> TRUE) THEN 4 ELSE (x55((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x55((_M - 1))) = 3) THEN 0 ELSE (IF ((x55((_M - 1))) = 4) THEN 0 ELSE (IF ((x55((_M - 1))) = 5) THEN 4 ELSE (x55((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 11) THEN (x55((_M - 1))) ELSE (IF ((x65((_M - 1))) = 12) THEN (IF ((x57((_M - 1))) = 1) THEN (x55((_M - 1))) ELSE (IF ((x57((_M - 1))) = 2) THEN (x55((_M - 1))) ELSE (IF ((x57((_M - 1))) = 3) THEN 1 ELSE (x55((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (x55((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x55((_M - 1))) ENDIF) ENDIF)); +DEF__156 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x56(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x56((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x56((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN 1 ELSE (x56((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 11) THEN (x56((_M - 1))) ELSE (IF ((x65((_M - 1))) = 12) THEN (IF ((x122((_M - 1))) = 1) THEN 2 ELSE (IF ((x122((_M - 1))) = 2) THEN 3 ELSE (IF ((x122((_M - 1))) = 3) THEN 4 ELSE (IF ((x122((_M - 1))) = 4) THEN 1 ELSE (IF ((x122((_M - 1))) = 5) THEN 1 ELSE (x122((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x56((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x56((_M - 1))) ENDIF) ENDIF)); +DEF__157 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x57(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 7) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x57((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x57((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN 1 ELSE (x57((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 11) THEN (x57((_M - 1))) ELSE (IF ((x65((_M - 1))) = 12) THEN (IF ((x57((_M - 1))) = 1) THEN (IF ((x45((_M - 1))) = 1) THEN 2 ELSE (x123((_M - 1))) ENDIF) ELSE (IF ((x57((_M - 1))) = 2) THEN (IF ((x45((_M - 1))) = 3) THEN 4 ELSE (IF ((x45((_M - 1))) = 2) THEN 3 ELSE (x123((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x57((_M - 1))) = 3) THEN 0 ELSE (IF ((x57((_M - 1))) = 4) THEN 0 ELSE (x57((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x57((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x57((_M - 1))) ENDIF) ENDIF)); +DEF__158 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x58(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x58((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x58((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x58((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x58((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x58((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x58((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 1 ELSE (x58((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x58((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x58((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x81((_M - 1))) = 1) THEN (IF (((NOT ((x7((_M - 1))) = 0)) AND (x8((_M - 1)))) <=> TRUE) THEN 2 ELSE (IF ((((x7((_M - 1))) = 0) OR (NOT (x8((_M - 1))))) <=> TRUE) THEN 1 ELSE (x81((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x81((_M - 1))) = 2) THEN (IF ((((x32((_M - 1))) = 6) AND (((x7((_M - 1))) = 0) OR (NOT (x8((_M - 1)))))) <=> TRUE) THEN 1 ELSE (IF ((((((x32((_M - 1))) = 6) AND ((x7((_M - 1))) = 2)) AND (x8((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 3 ELSE (IF (((((x32((_M - 1))) < 6) AND (((x7((_M - 1))) = 0) OR (NOT (x8((_M - 1)))))) OR ((x8((_M - 1))) AND (((x7((_M - 1))) = 1) OR (x6((_M - 1)))))) <=> TRUE) THEN 2 ELSE (x81((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x81((_M - 1))) = 3) THEN (IF (((NOT (((x7((_M - 1))) = 2) AND (x8((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 2 ELSE 3 ENDIF) ELSE (x81((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x58((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x58((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x58((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 1 ELSE (x58((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x58((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x58((_M - 1))) ENDIF) ENDIF)); +DEF__159 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x59(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (x59((_M - 1))) ELSE 1 ENDIF) ENDIF)); +DEF__160 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x60(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x60((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x60((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x60((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x60((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x60((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x60((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 1 ELSE (x60((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x60((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x60((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x82((_M - 1))) = 1) THEN (x112((_M - 1))) ELSE (IF ((x82((_M - 1))) = 2) THEN (IF ((NOT ((x13((_M - 1))) = 2)) <=> TRUE) THEN 1 ELSE (x112((_M - 1))) ENDIF) ELSE (x82((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x60((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x60((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x60((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 1 ELSE (x60((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x60((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x60((_M - 1))) ENDIF) ENDIF)); +DEF__161 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x61(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x61((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x61((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x61((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x61((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x61((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x61((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 1 ELSE (x61((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x61((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x61((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x83((_M - 1))) = 1) THEN (IF (((NOT ((((x50((_M - 1))) = 0) AND ((x53((_M - 1))) = 0)) AND ((x2((_M - 1))) = 0))) AND (NOT ((((x50((_M - 1))) = 0) AND ((x53((_M - 1))) = 0)) AND ((x3((_M - 1))) = 0)))) <=> TRUE) THEN 2 ELSE (IF ((((((((x50((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((x2((_M - 1))) = 0)) AND ((x3((_M - 1))) = 0)) <=> TRUE) THEN 1 ELSE (x83((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x83((_M - 1))) = 2) THEN (IF ((((((x2((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0)) AND ((((x3((_M - 1))) = 0) AND ((x50((_M - 1))) = 0)) AND ((x53((_M - 1))) = 0))) <=> TRUE) THEN 1 ELSE (IF (((((((((x2((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x2((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x2((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF (((((((((x3((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x3((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x3((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF ((((x52((_M - 1))) = 2) OR ((x53((_M - 1))) = 2)) <=> TRUE) THEN 3 ELSE (x83((_M - 1))) ENDIF) ELSE (x83((_M - 1))) ENDIF) ELSE (x83((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x83((_M - 1))) = 3) THEN (x109((_M - 1))) ELSE (IF ((x83((_M - 1))) = 4) THEN (IF ((NOT ((((((((x2((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x2((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x2((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x43((_M - 1))) = 2) AND ((x53((_M - 1))) = 2)))) <=> TRUE) THEN (IF ((NOT (((x52((_M - 1))) = 2) OR ((x53((_M - 1))) = 2))) <=> TRUE) THEN (IF ((NOT ((((((((x3((_M - 1))) = 2) AND ((x50((_M - 1))) = 2)) OR (((x3((_M - 1))) = 2) AND ((x53((_M - 1))) = 2))) OR (((x53((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x3((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x50((_M - 1))) = 2))) OR (((x42((_M - 1))) = 2) AND ((x53((_M - 1))) = 2)))) <=> TRUE) THEN 2 ELSE (x109((_M - 1))) ENDIF) ELSE (x109((_M - 1))) ENDIF) ELSE (x109((_M - 1))) ENDIF) ELSE (x83((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x61((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x61((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x61((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 1 ELSE (x61((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x61((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x61((_M - 1))) ENDIF) ENDIF)); +DEF__162 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x62(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x62((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x62((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x62((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x62((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x62((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x62((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 1 ELSE (x62((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x62((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x62((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x84((_M - 1))) = 1) THEN (IF (((NOT (((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0))) AND (x5((_M - 1)))) <=> TRUE) THEN 2 ELSE 1 ENDIF) ELSE (IF ((x84((_M - 1))) = 2) THEN (IF ((((x33((_M - 1))) = 6) AND ((((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0)) OR (NOT (x5((_M - 1)))))) <=> TRUE) THEN 1 ELSE (IF (((((((x33((_M - 1))) = 6) AND ((x9((_M - 1))) = 2)) AND ((x10((_M - 1))) = 2)) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 3 ELSE (IF (((((x33((_M - 1))) < 6) AND ((((x9((_M - 1))) = 0) OR ((x10((_M - 1))) = 0)) OR (NOT (x5((_M - 1)))))) OR ((x5((_M - 1))) AND (((x6((_M - 1))) OR ((x9((_M - 1))) = 1)) OR ((x10((_M - 1))) = 1)))) <=> TRUE) THEN 2 ELSE (x84((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x84((_M - 1))) = 3) THEN (IF (((((NOT ((x9((_M - 1))) = 2)) AND (NOT ((x10((_M - 1))) = 2))) AND (NOT (x5((_M - 1))))) OR (x6((_M - 1)))) <=> TRUE) THEN 2 ELSE (IF ((((((x9((_M - 1))) = 2) AND ((x10((_M - 1))) = 2)) AND (x5((_M - 1)))) AND (NOT (x6((_M - 1))))) <=> TRUE) THEN 3 ELSE (x84((_M - 1))) ENDIF) ENDIF) ELSE (x84((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x62((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x62((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x62((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 1 ELSE (x62((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x62((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x62((_M - 1))) ENDIF) ENDIF)); +DEF__163 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x63(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x63((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x63((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x63((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x63((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x63((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x63((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 1 ELSE (x63((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x63((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x63((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x63((_M - 1))) = 1) THEN (IF ((((((NOT ((x48((_M - 1))) = 0)) AND (NOT ((x47((_M - 1))) = 0))) AND (NOT ((x39((_M - 1))) = 0))) AND (NOT ((x36((_M - 1))) = 0))) AND ((x31((_M - 1))) < 11)) <=> TRUE) THEN 2 ELSE (IF ((x31((_M - 1))) = 11) THEN 5 ELSE (x63((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x63((_M - 1))) = 2) THEN (IF ((((((x48((_M - 1))) = 2) AND ((x47((_M - 1))) = 2)) AND (NOT ((x39((_M - 1))) = 0))) AND ((x36((_M - 1))) = 2)) <=> TRUE) THEN 4 ELSE (IF ((((((x48((_M - 1))) = 1) AND ((x47((_M - 1))) = 1)) AND ((x39((_M - 1))) = 0)) AND ((x36((_M - 1))) = 1)) <=> TRUE) THEN 3 ELSE (IF (((((((x48((_M - 1))) = 0) OR ((x47((_M - 1))) = 0)) OR ((x39((_M - 1))) = 0)) OR ((x36((_M - 1))) = 0)) OR ((x31((_M - 1))) = 11)) <=> TRUE) THEN 5 ELSE (x63((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x63((_M - 1))) = 3) THEN 5 ELSE (IF ((x63((_M - 1))) = 4) THEN 0 ELSE (IF ((x63((_M - 1))) = 5) THEN 0 ELSE (x63((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x63((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x63((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x63((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 1 ELSE (x63((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x63((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x63((_M - 1))) ENDIF) ENDIF)); +DEF__164 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x64(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (x64((_M - 1))) ELSE (IF ((x65((_M - 1))) = 2) THEN (x64((_M - 1))) ELSE (IF ((x65((_M - 1))) = 3) THEN (x64((_M - 1))) ELSE (IF ((x65((_M - 1))) = 4) THEN (x64((_M - 1))) ELSE (IF ((x65((_M - 1))) = 5) THEN (x64((_M - 1))) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN (x64((_M - 1))) ELSE (IF ((x14((_M - 1))) = 4) THEN 1 ELSE (x64((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x64((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x64((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (IF ((x80((_M - 1))) = 1) THEN (x80((_M - 1))) ELSE (IF ((x80((_M - 1))) = 2) THEN (IF ((x35((_M - 1))) = 6) THEN 3 ELSE (IF ((x35((_M - 1))) < 6) THEN 2 ELSE (x116((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x80((_M - 1))) = 3) THEN (x116((_M - 1))) ELSE (x80((_M - 1))) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x64((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x64((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN (x64((_M - 1))) ELSE (IF ((x55((_M - 1))) = 4) THEN 1 ELSE (x64((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x64((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x64((_M - 1))) ENDIF) ENDIF)); +DEF__165 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x65(_M)) = (IF (_M = _base) THEN 0 ELSE (IF ((NOT ((x59((_M - 1))) = 0)) <=> TRUE) THEN (IF ((x65((_M - 1))) = 1) THEN (IF ((x14((_M - 1))) = 0) THEN 3 ELSE (x65((_M - 1))) ENDIF) ELSE (IF ((x65((_M - 1))) = 2) THEN (IF ((x14((_M - 1))) = 8) THEN 7 ELSE (IF ((x14((_M - 1))) = 6) THEN 3 ELSE (x65((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 3) THEN (IF ((x14((_M - 1))) = 2) THEN 4 ELSE (x65((_M - 1))) ENDIF) ELSE (IF ((x65((_M - 1))) = 4) THEN (IF ((x14((_M - 1))) = 1) THEN 3 ELSE (IF ((x14((_M - 1))) = 3) THEN 6 ELSE (x65((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 5) THEN (IF ((x14((_M - 1))) = 7) THEN 2 ELSE (x65((_M - 1))) ENDIF) ELSE (IF ((x65((_M - 1))) = 6) THEN (IF ((x14((_M - 1))) = 5) THEN 2 ELSE (IF ((x14((_M - 1))) = 4) THEN 9 ELSE (x65((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 7) THEN (x65((_M - 1))) ELSE (IF ((x65((_M - 1))) = 8) THEN (x65((_M - 1))) ELSE (IF ((x65((_M - 1))) = 9) THEN (x86((_M - 1))) ELSE (IF ((x65((_M - 1))) = 10) THEN (IF ((x55((_M - 1))) = 1) THEN (x65((_M - 1))) ELSE (IF ((x55((_M - 1))) = 2) THEN (x65((_M - 1))) ELSE (IF ((x55((_M - 1))) = 3) THEN 12 ELSE (IF ((x55((_M - 1))) = 4) THEN 9 ELSE (x65((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 11) THEN (IF ((x14((_M - 1))) = 9) THEN 5 ELSE (IF ((x14((_M - 1))) = 10) THEN 8 ELSE (x65((_M - 1))) ENDIF) ENDIF) ELSE (IF ((x65((_M - 1))) = 12) THEN (IF ((x57((_M - 1))) = 1) THEN (x65((_M - 1))) ELSE (IF ((x57((_M - 1))) = 2) THEN (x65((_M - 1))) ELSE (IF ((x57((_M - 1))) = 3) THEN 10 ELSE (IF ((x57((_M - 1))) = 4) THEN 11 ELSE (x65((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ELSE (x65((_M - 1))) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ENDIF) ELSE 1 ENDIF) ENDIF)); +DEF__166 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x66(_M)) = (IF (_M = _base) THEN FALSE ELSE (x21((_M - 1))) ENDIF)); +DEF__168 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x68(_M)) = (IF (_M = _base) THEN FALSE ELSE (x17((_M - 1))) ENDIF)); +DEF__171 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x71(_M)) = (IF (_M = _base) THEN FALSE ELSE (x22((_M - 1))) ENDIF)); +DEF__173 : _nat -> BOOLEAN = LAMBDA( _M : _nat): ((x73(_M)) = (IF (_M = _base) THEN FALSE ELSE (x16((_M - 1))) ENDIF)); +% Property(ies) + +P : _nat -> BOOLEAN = LAMBDA(_M : _nat): (x129(_M)); + + + + +% INDUCT : Single property verification. +% INDUCT : MAIN. +% INDUCT : not refinement_pass. +% INDUCT : Checking K = 2. No message received. +% INDUCT : setup step loop - initialize step. +PUSH; +% INDUCT : ;4b +ASSERT (DEF__174( (_n + 0))); +ASSERT (DEF__176( (_n + 0))); +ASSERT (DEF__177( (_n + 0))); +ASSERT (DEF__178( (_n + 0))); +ASSERT (DEF__179( (_n + 0))); +ASSERT (DEF__180( (_n + 0))); +ASSERT (DEF__181( (_n + 0))); +ASSERT (DEF__182( (_n + 0))); +ASSERT (DEF__183( (_n + 0))); +ASSERT (DEF__184( (_n + 0))); +ASSERT (DEF__185( (_n + 0))); +ASSERT (DEF__186( (_n + 0))); +ASSERT (DEF__187( (_n + 0))); +ASSERT (DEF__188( (_n + 0))); +ASSERT (DEF__189( (_n + 0))); +ASSERT (DEF__190( (_n + 0))); +ASSERT (DEF__191( (_n + 0))); +ASSERT (DEF__192( (_n + 0))); +ASSERT (DEF__193( (_n + 0))); +ASSERT (DEF__194( (_n + 0))); +ASSERT (DEF__195( (_n + 0))); +ASSERT (DEF__196( (_n + 0))); +ASSERT (DEF__197( (_n + 0))); +ASSERT (DEF__198( (_n + 0))); +ASSERT (DEF__199( (_n + 0))); +ASSERT (DEF__200( (_n + 0))); +ASSERT (DEF__201( (_n + 0))); +ASSERT (DEF__202( (_n + 0))); +ASSERT (DEF__115( (_n + 0))); +ASSERT (DEF__203( (_n + 0))); +ASSERT (DEF__116( (_n + 0))); +ASSERT (DEF__204( (_n + 0))); +ASSERT (DEF__117( (_n + 0))); +ASSERT (DEF__205( (_n + 0))); +ASSERT (DEF__206( (_n + 0))); +ASSERT (DEF__207( (_n + 0))); +ASSERT (DEF__120( (_n + 0))); +ASSERT (DEF__208( (_n + 0))); +ASSERT (DEF__121( (_n + 0))); +ASSERT (DEF__209( (_n + 0))); +ASSERT (DEF__122( (_n + 0))); +ASSERT (DEF__210( (_n + 0))); +ASSERT (DEF__211( (_n + 0))); +ASSERT (DEF__212( (_n + 0))); +ASSERT (DEF__126( (_n + 0))); +ASSERT (DEF__213( (_n + 0))); +ASSERT (DEF__127( (_n + 0))); +ASSERT (DEF__214( (_n + 0))); +ASSERT (DEF__128( (_n + 0))); +ASSERT (DEF__215( (_n + 0))); +ASSERT (DEF__216( (_n + 0))); +ASSERT (DEF__129( (_n + 0))); +ASSERT (DEF__217( (_n + 0))); +ASSERT (DEF__130( (_n + 0))); +ASSERT (DEF__131( (_n + 0))); +ASSERT (DEF__218( (_n + 0))); +ASSERT (DEF__132( (_n + 0))); +ASSERT (DEF__219( (_n + 0))); +ASSERT (DEF__133( (_n + 0))); +ASSERT (DEF__220( (_n + 0))); +ASSERT (DEF__134( (_n + 0))); +ASSERT (DEF__221( (_n + 0))); +ASSERT (DEF__222( (_n + 0))); +ASSERT (DEF__135( (_n + 0))); +ASSERT (DEF__223( (_n + 0))); +ASSERT (DEF__136( (_n + 0))); +ASSERT (DEF__224( (_n + 0))); +ASSERT (DEF__137( (_n + 0))); +ASSERT (DEF__225( (_n + 0))); +ASSERT (DEF__138( (_n + 0))); +ASSERT (DEF__226( (_n + 0))); +ASSERT (DEF__139( (_n + 0))); +ASSERT (DEF__227( (_n + 0))); +ASSERT (DEF__140( (_n + 0))); +ASSERT (DEF__228( (_n + 0))); +ASSERT (DEF__141( (_n + 0))); +ASSERT (DEF__229( (_n + 0))); +ASSERT (DEF__142( (_n + 0))); +ASSERT (DEF__143( (_n + 0))); +ASSERT (DEF__144( (_n + 0))); +ASSERT (DEF__145( (_n + 0))); +ASSERT (DEF__146( (_n + 0))); +ASSERT (DEF__147( (_n + 0))); +ASSERT (DEF__148( (_n + 0))); +ASSERT (DEF__149( (_n + 0))); +ASSERT (DEF__150( (_n + 0))); +ASSERT (DEF__151( (_n + 0))); +ASSERT (DEF__152( (_n + 0))); +ASSERT (DEF__153( (_n + 0))); +ASSERT (DEF__154( (_n + 0))); +ASSERT (DEF__155( (_n + 0))); +ASSERT (DEF__156( (_n + 0))); +ASSERT (DEF__157( (_n + 0))); +ASSERT (DEF__158( (_n + 0))); +ASSERT (DEF__159( (_n + 0))); +ASSERT (DEF__160( (_n + 0))); +ASSERT (DEF__161( (_n + 0))); +ASSERT (DEF__162( (_n + 0))); +ASSERT (DEF__163( (_n + 0))); +ASSERT (DEF__164( (_n + 0))); +ASSERT (DEF__165( (_n + 0))); +ASSERT (DEF__166( (_n + 0))); +ASSERT (DEF__168( (_n + 0))); +ASSERT (DEF__171( (_n + 0))); +ASSERT (DEF__173( (_n + 0))); +ASSERT (DEF__174( (_n - 1))); +ASSERT (DEF__176( (_n - 1))); +ASSERT (DEF__177( (_n - 1))); +ASSERT (DEF__178( (_n - 1))); +ASSERT (DEF__179( (_n - 1))); +ASSERT (DEF__180( (_n - 1))); +ASSERT (DEF__181( (_n - 1))); +ASSERT (DEF__182( (_n - 1))); +ASSERT (DEF__183( (_n - 1))); +ASSERT (DEF__184( (_n - 1))); +ASSERT (DEF__185( (_n - 1))); +ASSERT (DEF__186( (_n - 1))); +ASSERT (DEF__187( (_n - 1))); +ASSERT (DEF__188( (_n - 1))); +ASSERT (DEF__189( (_n - 1))); +ASSERT (DEF__190( (_n - 1))); +ASSERT (DEF__191( (_n - 1))); +ASSERT (DEF__192( (_n - 1))); +ASSERT (DEF__193( (_n - 1))); +ASSERT (DEF__194( (_n - 1))); +ASSERT (DEF__195( (_n - 1))); +ASSERT (DEF__196( (_n - 1))); +ASSERT (DEF__197( (_n - 1))); +ASSERT (DEF__198( (_n - 1))); +ASSERT (DEF__199( (_n - 1))); +ASSERT (DEF__200( (_n - 1))); +ASSERT (DEF__201( (_n - 1))); +ASSERT (DEF__202( (_n - 1))); +ASSERT (DEF__115( (_n - 1))); +ASSERT (DEF__203( (_n - 1))); +ASSERT (DEF__116( (_n - 1))); +ASSERT (DEF__204( (_n - 1))); +ASSERT (DEF__117( (_n - 1))); +ASSERT (DEF__205( (_n - 1))); +ASSERT (DEF__206( (_n - 1))); +ASSERT (DEF__207( (_n - 1))); +ASSERT (DEF__120( (_n - 1))); +ASSERT (DEF__208( (_n - 1))); +ASSERT (DEF__121( (_n - 1))); +ASSERT (DEF__209( (_n - 1))); +ASSERT (DEF__122( (_n - 1))); +ASSERT (DEF__210( (_n - 1))); +ASSERT (DEF__211( (_n - 1))); +ASSERT (DEF__212( (_n - 1))); +ASSERT (DEF__126( (_n - 1))); +ASSERT (DEF__213( (_n - 1))); +ASSERT (DEF__127( (_n - 1))); +ASSERT (DEF__214( (_n - 1))); +ASSERT (DEF__128( (_n - 1))); +ASSERT (DEF__215( (_n - 1))); +ASSERT (DEF__216( (_n - 1))); +ASSERT (DEF__129( (_n - 1))); +ASSERT (DEF__217( (_n - 1))); +ASSERT (DEF__130( (_n - 1))); +ASSERT (DEF__131( (_n - 1))); +ASSERT (DEF__218( (_n - 1))); +ASSERT (DEF__132( (_n - 1))); +ASSERT (DEF__219( (_n - 1))); +ASSERT (DEF__133( (_n - 1))); +ASSERT (DEF__220( (_n - 1))); +ASSERT (DEF__134( (_n - 1))); +ASSERT (DEF__221( (_n - 1))); +ASSERT (DEF__222( (_n - 1))); +ASSERT (DEF__135( (_n - 1))); +ASSERT (DEF__223( (_n - 1))); +ASSERT (DEF__136( (_n - 1))); +ASSERT (DEF__224( (_n - 1))); +ASSERT (DEF__137( (_n - 1))); +ASSERT (DEF__225( (_n - 1))); +ASSERT (DEF__138( (_n - 1))); +ASSERT (DEF__226( (_n - 1))); +ASSERT (DEF__139( (_n - 1))); +ASSERT (DEF__227( (_n - 1))); +ASSERT (DEF__140( (_n - 1))); +ASSERT (DEF__228( (_n - 1))); +ASSERT (DEF__141( (_n - 1))); +ASSERT (DEF__229( (_n - 1))); +ASSERT (DEF__142( (_n - 1))); +ASSERT (DEF__143( (_n - 1))); +ASSERT (DEF__144( (_n - 1))); +ASSERT (DEF__145( (_n - 1))); +ASSERT (DEF__146( (_n - 1))); +ASSERT (DEF__147( (_n - 1))); +ASSERT (DEF__148( (_n - 1))); +ASSERT (DEF__149( (_n - 1))); +ASSERT (DEF__150( (_n - 1))); +ASSERT (DEF__151( (_n - 1))); +ASSERT (DEF__152( (_n - 1))); +ASSERT (DEF__153( (_n - 1))); +ASSERT (DEF__154( (_n - 1))); +ASSERT (DEF__155( (_n - 1))); +ASSERT (DEF__156( (_n - 1))); +ASSERT (DEF__157( (_n - 1))); +ASSERT (DEF__158( (_n - 1))); +ASSERT (DEF__159( (_n - 1))); +ASSERT (DEF__160( (_n - 1))); +ASSERT (DEF__161( (_n - 1))); +ASSERT (DEF__162( (_n - 1))); +ASSERT (DEF__163( (_n - 1))); +ASSERT (DEF__164( (_n - 1))); +ASSERT (DEF__165( (_n - 1))); +ASSERT (DEF__166( (_n - 1))); +ASSERT (DEF__168( (_n - 1))); +ASSERT (DEF__171( (_n - 1))); +ASSERT (DEF__173( (_n - 1))); +ASSERT (P( (_n - 1))); +ASSERT (NOT (P( _n))); +% PUSH; %safe +ASSERT TRUE; +CHECKSAT; +%ECHO "__DONE__"; +% INDUCT : sat +% INDUCT : __DONE__ +% POP; %safe +% INDUCT : Inductive step is Invalid at K = 2. Continuing search. +POP; +ASSERT (P( (_n - 1))); +ASSERT (P( (_n - 2))); +ASSERT (DEF__174( (_n + 0))); +ASSERT (DEF__176( (_n + 0))); +ASSERT (DEF__177( (_n + 0))); +ASSERT (DEF__178( (_n + 0))); +ASSERT (DEF__179( (_n + 0))); +ASSERT (DEF__180( (_n + 0))); +ASSERT (DEF__181( (_n + 0))); +ASSERT (DEF__182( (_n + 0))); +ASSERT (DEF__183( (_n + 0))); +ASSERT (DEF__184( (_n + 0))); +ASSERT (DEF__185( (_n + 0))); +ASSERT (DEF__186( (_n + 0))); +ASSERT (DEF__187( (_n + 0))); +ASSERT (DEF__188( (_n + 0))); +ASSERT (DEF__189( (_n + 0))); +ASSERT (DEF__190( (_n + 0))); +ASSERT (DEF__191( (_n + 0))); +ASSERT (DEF__192( (_n + 0))); +ASSERT (DEF__193( (_n + 0))); +ASSERT (DEF__194( (_n + 0))); +ASSERT (DEF__195( (_n + 0))); +ASSERT (DEF__196( (_n + 0))); +ASSERT (DEF__197( (_n + 0))); +ASSERT (DEF__198( (_n + 0))); +ASSERT (DEF__199( (_n + 0))); +ASSERT (DEF__200( (_n + 0))); +ASSERT (DEF__201( (_n + 0))); +ASSERT (DEF__202( (_n + 0))); +ASSERT (DEF__115( (_n + 0))); +ASSERT (DEF__203( (_n + 0))); +ASSERT (DEF__116( (_n + 0))); +ASSERT (DEF__204( (_n + 0))); +ASSERT (DEF__117( (_n + 0))); +ASSERT (DEF__205( (_n + 0))); +ASSERT (DEF__206( (_n + 0))); +ASSERT (DEF__207( (_n + 0))); +ASSERT (DEF__120( (_n + 0))); +ASSERT (DEF__208( (_n + 0))); +ASSERT (DEF__121( (_n + 0))); +ASSERT (DEF__209( (_n + 0))); +ASSERT (DEF__122( (_n + 0))); +ASSERT (DEF__210( (_n + 0))); +ASSERT (DEF__211( (_n + 0))); +ASSERT (DEF__212( (_n + 0))); +ASSERT (DEF__126( (_n + 0))); +ASSERT (DEF__213( (_n + 0))); +ASSERT (DEF__127( (_n + 0))); +ASSERT (DEF__214( (_n + 0))); +ASSERT (DEF__128( (_n + 0))); +ASSERT (DEF__215( (_n + 0))); +ASSERT (DEF__216( (_n + 0))); +ASSERT (DEF__129( (_n + 0))); +ASSERT (DEF__217( (_n + 0))); +ASSERT (DEF__130( (_n + 0))); +ASSERT (DEF__131( (_n + 0))); +ASSERT (DEF__218( (_n + 0))); +ASSERT (DEF__132( (_n + 0))); +ASSERT (DEF__219( (_n + 0))); +ASSERT (DEF__133( (_n + 0))); +ASSERT (DEF__220( (_n + 0))); +ASSERT (DEF__134( (_n + 0))); +ASSERT (DEF__221( (_n + 0))); +ASSERT (DEF__222( (_n + 0))); +ASSERT (DEF__135( (_n + 0))); +ASSERT (DEF__223( (_n + 0))); +ASSERT (DEF__136( (_n + 0))); +ASSERT (DEF__224( (_n + 0))); +ASSERT (DEF__137( (_n + 0))); +ASSERT (DEF__225( (_n + 0))); +ASSERT (DEF__138( (_n + 0))); +ASSERT (DEF__226( (_n + 0))); +ASSERT (DEF__139( (_n + 0))); +ASSERT (DEF__227( (_n + 0))); +ASSERT (DEF__140( (_n + 0))); +ASSERT (DEF__228( (_n + 0))); +ASSERT (DEF__141( (_n + 0))); +ASSERT (DEF__229( (_n + 0))); +ASSERT (DEF__142( (_n + 0))); +ASSERT (DEF__143( (_n + 0))); +ASSERT (DEF__144( (_n + 0))); +ASSERT (DEF__145( (_n + 0))); +ASSERT (DEF__146( (_n + 0))); +ASSERT (DEF__147( (_n + 0))); +ASSERT (DEF__148( (_n + 0))); +ASSERT (DEF__149( (_n + 0))); +ASSERT (DEF__150( (_n + 0))); +ASSERT (DEF__151( (_n + 0))); +ASSERT (DEF__152( (_n + 0))); +ASSERT (DEF__153( (_n + 0))); +ASSERT (DEF__154( (_n + 0))); +ASSERT (DEF__155( (_n + 0))); +ASSERT (DEF__156( (_n + 0))); +ASSERT (DEF__157( (_n + 0))); +ASSERT (DEF__158( (_n + 0))); +ASSERT (DEF__159( (_n + 0))); +ASSERT (DEF__160( (_n + 0))); +ASSERT (DEF__161( (_n + 0))); +ASSERT (DEF__162( (_n + 0))); +ASSERT (DEF__163( (_n + 0))); +ASSERT (DEF__164( (_n + 0))); +ASSERT (DEF__165( (_n + 0))); +ASSERT (DEF__166( (_n + 0))); +ASSERT (DEF__168( (_n + 0))); +ASSERT (DEF__171( (_n + 0))); +ASSERT (DEF__173( (_n + 0))); +% INDUCT : not refinement_pass. +% INDUCT : Checking K = 3. No message received. +% INDUCT : setup step loop - initialize step. +PUSH; +% INDUCT : ;4b +ASSERT (DEF__174( (_n - 1))); +ASSERT (DEF__176( (_n - 1))); +ASSERT (DEF__177( (_n - 1))); +ASSERT (DEF__178( (_n - 1))); +ASSERT (DEF__179( (_n - 1))); +ASSERT (DEF__180( (_n - 1))); +ASSERT (DEF__181( (_n - 1))); +ASSERT (DEF__182( (_n - 1))); +ASSERT (DEF__183( (_n - 1))); +ASSERT (DEF__184( (_n - 1))); +ASSERT (DEF__185( (_n - 1))); +ASSERT (DEF__186( (_n - 1))); +ASSERT (DEF__187( (_n - 1))); +ASSERT (DEF__188( (_n - 1))); +ASSERT (DEF__189( (_n - 1))); +ASSERT (DEF__190( (_n - 1))); +ASSERT (DEF__191( (_n - 1))); +ASSERT (DEF__192( (_n - 1))); +ASSERT (DEF__193( (_n - 1))); +ASSERT (DEF__194( (_n - 1))); +ASSERT (DEF__195( (_n - 1))); +ASSERT (DEF__196( (_n - 1))); +ASSERT (DEF__197( (_n - 1))); +ASSERT (DEF__198( (_n - 1))); +ASSERT (DEF__199( (_n - 1))); +ASSERT (DEF__200( (_n - 1))); +ASSERT (DEF__201( (_n - 1))); +ASSERT (DEF__202( (_n - 1))); +ASSERT (DEF__115( (_n - 1))); +ASSERT (DEF__203( (_n - 1))); +ASSERT (DEF__116( (_n - 1))); +ASSERT (DEF__204( (_n - 1))); +ASSERT (DEF__117( (_n - 1))); +ASSERT (DEF__205( (_n - 1))); +ASSERT (DEF__206( (_n - 1))); +ASSERT (DEF__207( (_n - 1))); +ASSERT (DEF__120( (_n - 1))); +ASSERT (DEF__208( (_n - 1))); +ASSERT (DEF__121( (_n - 1))); +ASSERT (DEF__209( (_n - 1))); +ASSERT (DEF__122( (_n - 1))); +ASSERT (DEF__210( (_n - 1))); +ASSERT (DEF__211( (_n - 1))); +ASSERT (DEF__212( (_n - 1))); +ASSERT (DEF__126( (_n - 1))); +ASSERT (DEF__213( (_n - 1))); +ASSERT (DEF__127( (_n - 1))); +ASSERT (DEF__214( (_n - 1))); +ASSERT (DEF__128( (_n - 1))); +ASSERT (DEF__215( (_n - 1))); +ASSERT (DEF__216( (_n - 1))); +ASSERT (DEF__129( (_n - 1))); +ASSERT (DEF__217( (_n - 1))); +ASSERT (DEF__130( (_n - 1))); +ASSERT (DEF__131( (_n - 1))); +ASSERT (DEF__218( (_n - 1))); +ASSERT (DEF__132( (_n - 1))); +ASSERT (DEF__219( (_n - 1))); +ASSERT (DEF__133( (_n - 1))); +ASSERT (DEF__220( (_n - 1))); +ASSERT (DEF__134( (_n - 1))); +ASSERT (DEF__221( (_n - 1))); +ASSERT (DEF__222( (_n - 1))); +ASSERT (DEF__135( (_n - 1))); +ASSERT (DEF__223( (_n - 1))); +ASSERT (DEF__136( (_n - 1))); +ASSERT (DEF__224( (_n - 1))); +ASSERT (DEF__137( (_n - 1))); +ASSERT (DEF__225( (_n - 1))); +ASSERT (DEF__138( (_n - 1))); +ASSERT (DEF__226( (_n - 1))); +ASSERT (DEF__139( (_n - 1))); +ASSERT (DEF__227( (_n - 1))); +ASSERT (DEF__140( (_n - 1))); +ASSERT (DEF__228( (_n - 1))); +ASSERT (DEF__141( (_n - 1))); +ASSERT (DEF__229( (_n - 1))); +ASSERT (DEF__142( (_n - 1))); +ASSERT (DEF__143( (_n - 1))); +ASSERT (DEF__144( (_n - 1))); +ASSERT (DEF__145( (_n - 1))); +ASSERT (DEF__146( (_n - 1))); +ASSERT (DEF__147( (_n - 1))); +ASSERT (DEF__148( (_n - 1))); +ASSERT (DEF__149( (_n - 1))); +ASSERT (DEF__150( (_n - 1))); +ASSERT (DEF__151( (_n - 1))); +ASSERT (DEF__152( (_n - 1))); +ASSERT (DEF__153( (_n - 1))); +ASSERT (DEF__154( (_n - 1))); +ASSERT (DEF__155( (_n - 1))); +ASSERT (DEF__156( (_n - 1))); +ASSERT (DEF__157( (_n - 1))); +ASSERT (DEF__158( (_n - 1))); +ASSERT (DEF__159( (_n - 1))); +ASSERT (DEF__160( (_n - 1))); +ASSERT (DEF__161( (_n - 1))); +ASSERT (DEF__162( (_n - 1))); +ASSERT (DEF__163( (_n - 1))); +ASSERT (DEF__164( (_n - 1))); +ASSERT (DEF__165( (_n - 1))); +ASSERT (DEF__166( (_n - 1))); +ASSERT (DEF__168( (_n - 1))); +ASSERT (DEF__171( (_n - 1))); +ASSERT (DEF__173( (_n - 1))); +ASSERT (DEF__174( (_n - 2))); +ASSERT (DEF__176( (_n - 2))); +ASSERT (DEF__177( (_n - 2))); +ASSERT (DEF__178( (_n - 2))); +ASSERT (DEF__179( (_n - 2))); +ASSERT (DEF__180( (_n - 2))); +ASSERT (DEF__181( (_n - 2))); +ASSERT (DEF__182( (_n - 2))); +ASSERT (DEF__183( (_n - 2))); +ASSERT (DEF__184( (_n - 2))); +ASSERT (DEF__185( (_n - 2))); +ASSERT (DEF__186( (_n - 2))); +ASSERT (DEF__187( (_n - 2))); +ASSERT (DEF__188( (_n - 2))); +ASSERT (DEF__189( (_n - 2))); +ASSERT (DEF__190( (_n - 2))); +ASSERT (DEF__191( (_n - 2))); +ASSERT (DEF__192( (_n - 2))); +ASSERT (DEF__193( (_n - 2))); +ASSERT (DEF__194( (_n - 2))); +ASSERT (DEF__195( (_n - 2))); +ASSERT (DEF__196( (_n - 2))); +ASSERT (DEF__197( (_n - 2))); +ASSERT (DEF__198( (_n - 2))); +ASSERT (DEF__199( (_n - 2))); +ASSERT (DEF__200( (_n - 2))); +ASSERT (DEF__201( (_n - 2))); +ASSERT (DEF__202( (_n - 2))); +ASSERT (DEF__115( (_n - 2))); +ASSERT (DEF__203( (_n - 2))); +ASSERT (DEF__116( (_n - 2))); +ASSERT (DEF__204( (_n - 2))); +ASSERT (DEF__117( (_n - 2))); +ASSERT (DEF__205( (_n - 2))); +ASSERT (DEF__206( (_n - 2))); +ASSERT (DEF__207( (_n - 2))); +ASSERT (DEF__120( (_n - 2))); +ASSERT (DEF__208( (_n - 2))); +ASSERT (DEF__121( (_n - 2))); +ASSERT (DEF__209( (_n - 2))); +ASSERT (DEF__122( (_n - 2))); +ASSERT (DEF__210( (_n - 2))); +ASSERT (DEF__211( (_n - 2))); +ASSERT (DEF__212( (_n - 2))); +ASSERT (DEF__126( (_n - 2))); +ASSERT (DEF__213( (_n - 2))); +ASSERT (DEF__127( (_n - 2))); +ASSERT (DEF__214( (_n - 2))); +ASSERT (DEF__128( (_n - 2))); +ASSERT (DEF__215( (_n - 2))); +ASSERT (DEF__216( (_n - 2))); +ASSERT (DEF__129( (_n - 2))); +ASSERT (DEF__217( (_n - 2))); +ASSERT (DEF__130( (_n - 2))); +ASSERT (DEF__131( (_n - 2))); +ASSERT (DEF__218( (_n - 2))); +ASSERT (DEF__132( (_n - 2))); +ASSERT (DEF__219( (_n - 2))); +ASSERT (DEF__133( (_n - 2))); +ASSERT (DEF__220( (_n - 2))); +ASSERT (DEF__134( (_n - 2))); +ASSERT (DEF__221( (_n - 2))); +ASSERT (DEF__222( (_n - 2))); +ASSERT (DEF__135( (_n - 2))); +ASSERT (DEF__223( (_n - 2))); +ASSERT (DEF__136( (_n - 2))); +ASSERT (DEF__224( (_n - 2))); +ASSERT (DEF__137( (_n - 2))); +ASSERT (DEF__225( (_n - 2))); +ASSERT (DEF__138( (_n - 2))); +ASSERT (DEF__226( (_n - 2))); +ASSERT (DEF__139( (_n - 2))); +ASSERT (DEF__227( (_n - 2))); +ASSERT (DEF__140( (_n - 2))); +ASSERT (DEF__228( (_n - 2))); +ASSERT (DEF__141( (_n - 2))); +ASSERT (DEF__229( (_n - 2))); +ASSERT (DEF__142( (_n - 2))); +ASSERT (DEF__143( (_n - 2))); +ASSERT (DEF__144( (_n - 2))); +ASSERT (DEF__145( (_n - 2))); +ASSERT (DEF__146( (_n - 2))); +ASSERT (DEF__147( (_n - 2))); +ASSERT (DEF__148( (_n - 2))); +ASSERT (DEF__149( (_n - 2))); +ASSERT (DEF__150( (_n - 2))); +ASSERT (DEF__151( (_n - 2))); +ASSERT (DEF__152( (_n - 2))); +ASSERT (DEF__153( (_n - 2))); +ASSERT (DEF__154( (_n - 2))); +ASSERT (DEF__155( (_n - 2))); +ASSERT (DEF__156( (_n - 2))); +ASSERT (DEF__157( (_n - 2))); +ASSERT (DEF__158( (_n - 2))); +ASSERT (DEF__159( (_n - 2))); +ASSERT (DEF__160( (_n - 2))); +ASSERT (DEF__161( (_n - 2))); +ASSERT (DEF__162( (_n - 2))); +ASSERT (DEF__163( (_n - 2))); +ASSERT (DEF__164( (_n - 2))); +ASSERT (DEF__165( (_n - 2))); +ASSERT (DEF__166( (_n - 2))); +ASSERT (DEF__168( (_n - 2))); +ASSERT (DEF__171( (_n - 2))); +ASSERT (DEF__173( (_n - 2))); +ASSERT (NOT (P( _n))); +% PUSH; %safe +ASSERT TRUE; +CHECKSAT; +%ECHO "__DONE__"; +% INDUCT : Abort in 3 step. diff --git a/test/regress/regress0/smt2output.smt2 b/test/regress/regress0/smt2output.smt2 new file mode 100644 index 000000000..26050d931 --- /dev/null +++ b/test/regress/regress0/smt2output.smt2 @@ -0,0 +1,15 @@ +; This test checks the correct output behavior of SMT-LIBv2 symbols +; (sometimes they have to be |quoted| with pipes). +; +; COMMAND-LINE: -qm +; EXIT: 10 +(declare-fun |toto| () Bool) +(declare-fun |to to| () Bool) +(assert (and toto |to to|)) +(check-sat) +; EXPECT: sat +(get-model) +; EXPECT: (model +; EXPECT: (define-fun toto () Bool true) +; EXPECT: (define-fun |to to| () Bool true) +; EXPECT: ) diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h index 664027c49..66fcabed0 100644 --- a/test/unit/main/interactive_shell_black.h +++ b/test/unit/main/interactive_shell_black.h @@ -69,13 +69,13 @@ private: } void testAssertTrue() { - *d_sin << "ASSERT TRUE;" << flush; + *d_sin << "ASSERT TRUE;\n" << flush; InteractiveShell shell(*d_exprManager, d_options); countCommands( shell, 1, 1 ); } void testQueryFalse() { - *d_sin << "QUERY FALSE;" << flush; + *d_sin << "QUERY FALSE;\n" << flush; InteractiveShell shell(*d_exprManager, d_options); countCommands( shell, 1, 1 ); } |