// Author(s): Wieger Wesselink
// Copyright: see the accompanying file COPYING or copy at
// https://svn.win.tue.nl/trac/MCRL2/browser/trunk/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
/// \file mcrl2/core/detail/soundness_checks.h
/// \brief Add your file description here.

#ifndef MCRL2_BASIC_DETAIL_SOUNDNESS_CHECKS_H
#define MCRL2_BASIC_DETAIL_SOUNDNESS_CHECKS_H

// This file contains soundness checks for LPS terms.
// N.B. This file is automatically generated!

#include <iostream>
#include "mcrl2/utilities/logger.h"
#include "mcrl2/core/detail/function_symbols.h"
#include "mcrl2/atermpp/aterm.h"
#include "mcrl2/atermpp/aterm_list.h"
#include "mcrl2/atermpp/aterm_appl.h"
#include "mcrl2/atermpp/aterm_string.h"

namespace mcrl2
{

namespace core
{

namespace detail
{

// checks
// 1) if term t satisfies the predicate f
template <typename Term, typename CheckFunction>
bool check_term_argument(Term t, CheckFunction f)
{
  return f(t);
}

// checks
// 1) if term t is a list,
// 2) if the list has the proper minimum size
// 3) if all elements of the list satisfy the predicate f
template <typename Term, typename CheckFunction>
bool check_list_argument(Term t, CheckFunction f, unsigned int minimum_size)
{
  atermpp::aterm term(t);
  if (!t.type_is_list())
  {
    return false;
  }
  atermpp::aterm_list l(term);
  if (l.size() < minimum_size)
  {
    return false;
  }
  for (atermpp::aterm_list::iterator i = l.begin(); i != l.end(); ++i)
  {
    if (!f(*i))
    {
      return false;
    }
  }
  return true;
}

template <typename Term>
bool check_rule_String(Term t)
{
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  atermpp::aterm_appl a(term);
  if (a.size() > 0)
  {
    return false;
  }
  if (a == atermpp::empty_string())
  {
    return false;
  }
  return true;
}

template <typename Term>
bool check_rule_StringOrEmpty(Term t)
{
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  atermpp::aterm_appl a(term);
  if (a.size() > 0)
  {
    return false;
  }
  return true;
}

template <typename Term>
bool check_rule_Number(Term t)
{
  atermpp::aterm term(t);
  return term.type_is_int();
}

template <typename Term> bool check_rule_DataExpr(Term t);

// DataAppl(DataExpr, DataExpr+)
template <typename Term>
bool check_term_DataAppl(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (!gsIsDataAppl(a))
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  for (atermpp::aterm_appl::const_iterator child = a.begin(); child != a.end(); ++child)
  {
    if (!check_term_argument(*child, check_rule_DataExpr<atermpp::aterm>))
    {
      mCRL2log(log::debug, "soundness_checks") << "check_rule_DataExpr" << std::endl;
      return false;
    }
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

//--- start generated code ---//
template <typename Term> bool check_rule_SortExpr(Term t);
template <typename Term> bool check_rule_SortId(Term t);
template <typename Term> bool check_rule_SortConsType(Term t);
template <typename Term> bool check_rule_StructCons(Term t);
template <typename Term> bool check_rule_StructProj(Term t);
template <typename Term> bool check_rule_DataExpr(Term t);
template <typename Term> bool check_rule_DataVarId(Term t);
template <typename Term> bool check_rule_OpId(Term t);
template <typename Term> bool check_rule_BindingOperator(Term t);
template <typename Term> bool check_rule_WhrDecl(Term t);
template <typename Term> bool check_rule_DataVarIdInit(Term t);
template <typename Term> bool check_rule_UntypedIdentifierAssignment(Term t);
template <typename Term> bool check_rule_DataSpec(Term t);
template <typename Term> bool check_rule_SortSpec(Term t);
template <typename Term> bool check_rule_ConsSpec(Term t);
template <typename Term> bool check_rule_MapSpec(Term t);
template <typename Term> bool check_rule_DataEqnSpec(Term t);
template <typename Term> bool check_rule_SortDecl(Term t);
template <typename Term> bool check_rule_DataEqn(Term t);
template <typename Term> bool check_rule_DataExprOrNil(Term t);
template <typename Term> bool check_rule_MultAct(Term t);
template <typename Term> bool check_rule_UntypedMultAct(Term t);
template <typename Term> bool check_rule_Action(Term t);
template <typename Term> bool check_rule_UntypedAction(Term t);
template <typename Term> bool check_rule_ActId(Term t);
template <typename Term> bool check_rule_ProcExpr(Term t);
template <typename Term> bool check_rule_ProcVarId(Term t);
template <typename Term> bool check_rule_MultActName(Term t);
template <typename Term> bool check_rule_RenameExpr(Term t);
template <typename Term> bool check_rule_CommExpr(Term t);
template <typename Term> bool check_rule_ProcSpec(Term t);
template <typename Term> bool check_rule_ActSpec(Term t);
template <typename Term> bool check_rule_GlobVarSpec(Term t);
template <typename Term> bool check_rule_ProcEqnSpec(Term t);
template <typename Term> bool check_rule_ProcEqn(Term t);
template <typename Term> bool check_rule_MultActOrDelta(Term t);
template <typename Term> bool check_rule_ProcInit(Term t);
template <typename Term> bool check_rule_LinProcSpec(Term t);
template <typename Term> bool check_rule_LinearProcess(Term t);
template <typename Term> bool check_rule_LinearProcessSummand(Term t);
template <typename Term> bool check_rule_LinearProcessInit(Term t);
template <typename Term> bool check_rule_StateFrm(Term t);
template <typename Term> bool check_rule_RegFrm(Term t);
template <typename Term> bool check_rule_ActFrm(Term t);
template <typename Term> bool check_rule_ParamIdOrAction(Term t);
template <typename Term> bool check_rule_ActionRenameRules(Term t);
template <typename Term> bool check_rule_ActionRenameRule(Term t);
template <typename Term> bool check_rule_ActionRenameRuleRHS(Term t);
template <typename Term> bool check_rule_ActionRenameSpec(Term t);
template <typename Term> bool check_rule_PBES(Term t);
template <typename Term> bool check_rule_PBEqnSpec(Term t);
template <typename Term> bool check_rule_PBInit(Term t);
template <typename Term> bool check_rule_PBEqn(Term t);
template <typename Term> bool check_rule_FixPoint(Term t);
template <typename Term> bool check_rule_PropVarDecl(Term t);
template <typename Term> bool check_rule_PBExpr(Term t);
template <typename Term> bool check_rule_PropVarInst(Term t);
template <typename Term> bool check_rule_BES(Term t);
template <typename Term> bool check_rule_BooleanEquation(Term t);
template <typename Term> bool check_rule_BooleanVariable(Term t);
template <typename Term> bool check_rule_BooleanExpression(Term t);
template <typename Term> bool check_term_BooleanOr(Term t);
template <typename Term> bool check_term_StateOr(Term t);
template <typename Term> bool check_term_Hide(Term t);
template <typename Term> bool check_term_SortArrow(Term t);
template <typename Term> bool check_term_ProcessAssignment(Term t);
template <typename Term> bool check_term_Forall(Term t);
template <typename Term> bool check_term_CommExpr(Term t);
template <typename Term> bool check_term_StateNot(Term t);
template <typename Term> bool check_term_UntypedSetBagComp(Term t);
template <typename Term> bool check_term_SortFSet(Term t);
template <typename Term> bool check_term_StateImp(Term t);
template <typename Term> bool check_term_PBESExists(Term t);
template <typename Term> bool check_term_PBESImp(Term t);
template <typename Term> bool check_term_Binder(Term t);
template <typename Term> bool check_term_SortRef(Term t);
template <typename Term> bool check_term_ProcEqnSpec(Term t);
template <typename Term> bool check_term_StateForall(Term t);
template <typename Term> bool check_term_BooleanImp(Term t);
template <typename Term> bool check_term_SortId(Term t);
template <typename Term> bool check_term_UntypedAction(Term t);
template <typename Term> bool check_term_StateNu(Term t);
template <typename Term> bool check_term_RegNil(Term t);
template <typename Term> bool check_term_DataSpec(Term t);
template <typename Term> bool check_term_UntypedActMultAct(Term t);
template <typename Term> bool check_term_Tau(Term t);
template <typename Term> bool check_term_StateYaledTimed(Term t);
template <typename Term> bool check_term_SortCons(Term t);
template <typename Term> bool check_term_DataEqnSpec(Term t);
template <typename Term> bool check_term_LinearProcessSummand(Term t);
template <typename Term> bool check_term_SortSpec(Term t);
template <typename Term> bool check_term_ActionRenameRules(Term t);
template <typename Term> bool check_term_UntypedParamId(Term t);
template <typename Term> bool check_term_BooleanEquation(Term t);
template <typename Term> bool check_term_ConsSpec(Term t);
template <typename Term> bool check_term_SortList(Term t);
template <typename Term> bool check_term_Sum(Term t);
template <typename Term> bool check_term_DataVarId(Term t);
template <typename Term> bool check_term_ProcVarId(Term t);
template <typename Term> bool check_term_ProcessInit(Term t);
template <typename Term> bool check_term_UntypedIdentifier(Term t);
template <typename Term> bool check_term_BooleanFalse(Term t);
template <typename Term> bool check_term_BES(Term t);
template <typename Term> bool check_term_MapSpec(Term t);
template <typename Term> bool check_term_IfThen(Term t);
template <typename Term> bool check_term_BooleanAnd(Term t);
template <typename Term> bool check_term_LinProcSpec(Term t);
template <typename Term> bool check_term_Choice(Term t);
template <typename Term> bool check_term_LinearProcessInit(Term t);
template <typename Term> bool check_term_MultAct(Term t);
template <typename Term> bool check_term_PropVarInst(Term t);
template <typename Term> bool check_term_BagComp(Term t);
template <typename Term> bool check_term_StateDelay(Term t);
template <typename Term> bool check_term_RegAlt(Term t);
template <typename Term> bool check_term_UntypedMultAct(Term t);
template <typename Term> bool check_term_StructCons(Term t);
template <typename Term> bool check_term_Mu(Term t);
template <typename Term> bool check_term_PBEqnSpec(Term t);
template <typename Term> bool check_term_ActNot(Term t);
template <typename Term> bool check_term_BooleanTrue(Term t);
template <typename Term> bool check_term_Block(Term t);
template <typename Term> bool check_term_Rename(Term t);
template <typename Term> bool check_term_Exists(Term t);
template <typename Term> bool check_term_Sync(Term t);
template <typename Term> bool check_term_ActExists(Term t);
template <typename Term> bool check_term_ProcSpec(Term t);
template <typename Term> bool check_term_UntypedSortsPossible(Term t);
template <typename Term> bool check_term_StateMu(Term t);
template <typename Term> bool check_term_StateFalse(Term t);
template <typename Term> bool check_term_PBESFalse(Term t);
template <typename Term> bool check_term_PBESForall(Term t);
template <typename Term> bool check_term_StateTrue(Term t);
template <typename Term> bool check_term_BInit(Term t);
template <typename Term> bool check_term_UntypedSortUnknown(Term t);
template <typename Term> bool check_term_RegTrans(Term t);
template <typename Term> bool check_term_StateDelayTimed(Term t);
template <typename Term> bool check_term_Nu(Term t);
template <typename Term> bool check_term_SortStruct(Term t);
template <typename Term> bool check_term_AtTime(Term t);
template <typename Term> bool check_term_ActOr(Term t);
template <typename Term> bool check_term_Comm(Term t);
template <typename Term> bool check_term_BooleanNot(Term t);
template <typename Term> bool check_term_Delta(Term t);
template <typename Term> bool check_term_ActMultAct(Term t);
template <typename Term> bool check_term_StateAnd(Term t);
template <typename Term> bool check_term_LMerge(Term t);
template <typename Term> bool check_term_SetComp(Term t);
template <typename Term> bool check_term_ActForall(Term t);
template <typename Term> bool check_term_RenameExpr(Term t);
template <typename Term> bool check_term_Merge(Term t);
template <typename Term> bool check_term_ActSpec(Term t);
template <typename Term> bool check_term_BooleanVariable(Term t);
template <typename Term> bool check_term_Action(Term t);
template <typename Term> bool check_term_PBESAnd(Term t);
template <typename Term> bool check_term_Lambda(Term t);
template <typename Term> bool check_term_StateMust(Term t);
template <typename Term> bool check_term_Seq(Term t);
template <typename Term> bool check_term_DataVarIdInit(Term t);
template <typename Term> bool check_term_Process(Term t);
template <typename Term> bool check_term_ActAnd(Term t);
template <typename Term> bool check_term_ActionRenameSpec(Term t);
template <typename Term> bool check_term_PBES(Term t);
template <typename Term> bool check_term_StateVar(Term t);
template <typename Term> bool check_term_ActionRenameRule(Term t);
template <typename Term> bool check_term_RegSeq(Term t);
template <typename Term> bool check_term_LinearProcess(Term t);
template <typename Term> bool check_term_ActAt(Term t);
template <typename Term> bool check_term_DataEqn(Term t);
template <typename Term> bool check_term_PBESNot(Term t);
template <typename Term> bool check_term_StateExists(Term t);
template <typename Term> bool check_term_StateMay(Term t);
template <typename Term> bool check_term_PBESTrue(Term t);
template <typename Term> bool check_term_MultActName(Term t);
template <typename Term> bool check_term_IfThenElse(Term t);
template <typename Term> bool check_term_Nil(Term t);
template <typename Term> bool check_term_ProcEqn(Term t);
template <typename Term> bool check_term_StructProj(Term t);
template <typename Term> bool check_term_PBEqn(Term t);
template <typename Term> bool check_term_Whr(Term t);
template <typename Term> bool check_term_OpId(Term t);
template <typename Term> bool check_term_SortSet(Term t);
template <typename Term> bool check_term_ActFalse(Term t);
template <typename Term> bool check_term_ActId(Term t);
template <typename Term> bool check_term_StateYaled(Term t);
template <typename Term> bool check_term_PBESOr(Term t);
template <typename Term> bool check_term_UntypedProcessAssignment(Term t);
template <typename Term> bool check_term_SortFBag(Term t);
template <typename Term> bool check_term_Allow(Term t);
template <typename Term> bool check_term_PropVarDecl(Term t);
template <typename Term> bool check_term_ActImp(Term t);
template <typename Term> bool check_term_SortBag(Term t);
template <typename Term> bool check_term_PBInit(Term t);
template <typename Term> bool check_term_ActTrue(Term t);
template <typename Term> bool check_term_RegTransOrNil(Term t);
template <typename Term> bool check_term_GlobVarSpec(Term t);
template <typename Term> bool check_term_UntypedIdentifierAssignment(Term t);

template <typename Term>
bool check_rule_SortExpr(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_rule_SortId(t)
         || check_term_SortCons(t)
         || check_term_SortStruct(t)
         || check_term_SortArrow(t)
         || check_term_UntypedSortUnknown(t)
         || check_term_UntypedSortsPossible(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_SortId(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_SortId(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_SortConsType(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_SortList(t)
         || check_term_SortSet(t)
         || check_term_SortBag(t)
         || check_term_SortFSet(t)
         || check_term_SortFBag(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_StructCons(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_StructCons(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_StructProj(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_StructProj(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_DataExpr(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_rule_DataVarId(t)
         || check_rule_OpId(t)
         || check_term_DataAppl(t)
         || check_term_Binder(t)
         || check_term_Whr(t)
         || check_term_UntypedIdentifier(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_DataVarId(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_DataVarId(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_OpId(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_OpId(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_BindingOperator(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_Forall(t)
         || check_term_Exists(t)
         || check_term_SetComp(t)
         || check_term_BagComp(t)
         || check_term_Lambda(t)
         || check_term_UntypedSetBagComp(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_WhrDecl(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_rule_DataVarIdInit(t)
         || check_rule_UntypedIdentifierAssignment(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_DataVarIdInit(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_DataVarIdInit(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_UntypedIdentifierAssignment(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_UntypedIdentifierAssignment(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_DataSpec(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_DataSpec(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_SortSpec(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_SortSpec(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_ConsSpec(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_ConsSpec(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_MapSpec(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_MapSpec(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_DataEqnSpec(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_DataEqnSpec(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_SortDecl(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_rule_SortId(t)
         || check_term_SortRef(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_DataEqn(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_DataEqn(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_DataExprOrNil(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_rule_DataExpr(t)
         || check_term_Nil(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_MultAct(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_MultAct(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_UntypedMultAct(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_UntypedMultAct(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_Action(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_Action(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_UntypedAction(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_UntypedAction(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_ActId(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_ActId(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_ProcExpr(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_rule_Action(t)
         || check_term_Process(t)
         || check_term_ProcessAssignment(t)
         || check_term_Delta(t)
         || check_term_Tau(t)
         || check_term_Sum(t)
         || check_term_Block(t)
         || check_term_Hide(t)
         || check_term_Rename(t)
         || check_term_Comm(t)
         || check_term_Allow(t)
         || check_term_Sync(t)
         || check_term_AtTime(t)
         || check_term_Seq(t)
         || check_term_IfThen(t)
         || check_term_IfThenElse(t)
         || check_term_BInit(t)
         || check_term_Merge(t)
         || check_term_LMerge(t)
         || check_term_Choice(t)
         || check_term_UntypedParamId(t)
         || check_term_UntypedProcessAssignment(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_ProcVarId(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_ProcVarId(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_MultActName(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_MultActName(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_RenameExpr(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_RenameExpr(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_CommExpr(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_CommExpr(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_ProcSpec(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_ProcSpec(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_ActSpec(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_ActSpec(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_GlobVarSpec(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_GlobVarSpec(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_ProcEqnSpec(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_ProcEqnSpec(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_ProcEqn(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_ProcEqn(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_MultActOrDelta(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_rule_MultAct(t)
         || check_term_Delta(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_ProcInit(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_ProcessInit(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_LinProcSpec(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_LinProcSpec(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_LinearProcess(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_LinearProcess(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_LinearProcessSummand(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_LinearProcessSummand(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_LinearProcessInit(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_LinearProcessInit(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_StateFrm(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_rule_DataExpr(t)
         || check_term_StateTrue(t)
         || check_term_StateFalse(t)
         || check_term_StateNot(t)
         || check_term_StateAnd(t)
         || check_term_StateOr(t)
         || check_term_StateImp(t)
         || check_term_StateForall(t)
         || check_term_StateExists(t)
         || check_term_StateMust(t)
         || check_term_StateMay(t)
         || check_term_StateYaled(t)
         || check_term_StateYaledTimed(t)
         || check_term_StateDelay(t)
         || check_term_StateDelayTimed(t)
         || check_term_StateVar(t)
         || check_term_StateNu(t)
         || check_term_StateMu(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_RegFrm(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_rule_ActFrm(t)
         || check_term_RegNil(t)
         || check_term_RegSeq(t)
         || check_term_RegAlt(t)
         || check_term_RegTrans(t)
         || check_term_RegTransOrNil(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_ActFrm(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_rule_DataExpr(t)
         || check_term_ActTrue(t)
         || check_term_ActFalse(t)
         || check_term_ActNot(t)
         || check_term_ActAnd(t)
         || check_term_ActOr(t)
         || check_term_ActImp(t)
         || check_term_ActForall(t)
         || check_term_ActExists(t)
         || check_term_ActAt(t)
         || check_term_ActMultAct(t)
         || check_term_UntypedActMultAct(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_ParamIdOrAction(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_rule_UntypedAction(t)
         || check_rule_Action(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_ActionRenameRules(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_ActionRenameRules(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_ActionRenameRule(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_ActionRenameRule(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_ActionRenameRuleRHS(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_rule_UntypedAction(t)
         || check_rule_Action(t)
         || check_term_Delta(t)
         || check_term_Tau(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_ActionRenameSpec(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_ActionRenameSpec(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_PBES(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_PBES(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_PBEqnSpec(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_PBEqnSpec(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_PBInit(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_PBInit(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_PBEqn(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_PBEqn(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_FixPoint(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_Mu(t)
         || check_term_Nu(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_PropVarDecl(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_PropVarDecl(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_PBExpr(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_rule_DataExpr(t)
         || check_term_PBESTrue(t)
         || check_term_PBESFalse(t)
         || check_term_PBESNot(t)
         || check_term_PBESAnd(t)
         || check_term_PBESOr(t)
         || check_term_PBESImp(t)
         || check_term_PBESForall(t)
         || check_term_PBESExists(t)
         || check_rule_PropVarInst(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_PropVarInst(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_PropVarInst(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_BES(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_BES(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_BooleanEquation(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_BooleanEquation(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_BooleanVariable(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_BooleanVariable(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

template <typename Term>
bool check_rule_BooleanExpression(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  return check_term_BooleanTrue(t)
         || check_term_BooleanFalse(t)
         || check_rule_BooleanVariable(t)
         || check_term_BooleanNot(t)
         || check_term_BooleanAnd(t)
         || check_term_BooleanOr(t)
         || check_term_BooleanImp(t);
#else
  return true;
#endif // MCRL2_NO_SOUNDNESS_CHECKS
}

// BooleanOr(BooleanExpression, BooleanExpression)
template <typename Term>
bool check_term_BooleanOr(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::BooleanOr)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_BooleanExpression<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_BooleanExpression" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_BooleanExpression<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_BooleanExpression" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// StateOr(StateFrm, StateFrm)
template <typename Term>
bool check_term_StateOr(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::StateOr)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_StateFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_StateFrm" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_StateFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_StateFrm" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// Hide(String*, ProcExpr)
template <typename Term>
bool check_term_Hide(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::Hide)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_String<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_String" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_ProcExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// SortArrow(SortExpr+, SortExpr)
template <typename Term>
bool check_term_SortArrow(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::SortArrow)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_SortExpr<atermpp::aterm>, 1))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_SortExpr" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_SortExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_SortExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// ProcessAssignment(ProcVarId, DataVarIdInit*)
template <typename Term>
bool check_term_ProcessAssignment(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::ProcessAssignment)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_ProcVarId<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcVarId" << std::endl;
    return false;
  }
  if (!check_list_argument(a[1], check_rule_DataVarIdInit<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataVarIdInit" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// Forall()
template <typename Term>
bool check_term_Forall(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::Forall)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// CommExpr(MultActName, String)
template <typename Term>
bool check_term_CommExpr(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::CommExpr)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_MultActName<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_MultActName" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_String<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_String" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// StateNot(StateFrm)
template <typename Term>
bool check_term_StateNot(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::StateNot)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_StateFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_StateFrm" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// UntypedSetBagComp()
template <typename Term>
bool check_term_UntypedSetBagComp(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::UntypedSetBagComp)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// SortFSet()
template <typename Term>
bool check_term_SortFSet(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::SortFSet)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// StateImp(StateFrm, StateFrm)
template <typename Term>
bool check_term_StateImp(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::StateImp)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_StateFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_StateFrm" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_StateFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_StateFrm" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// PBESExists(DataVarId+, PBExpr)
template <typename Term>
bool check_term_PBESExists(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::PBESExists)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_DataVarId<atermpp::aterm>, 1))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataVarId" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_PBExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_PBExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// PBESImp(PBExpr, PBExpr)
template <typename Term>
bool check_term_PBESImp(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::PBESImp)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_PBExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_PBExpr" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_PBExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_PBExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// Binder(BindingOperator, DataVarId+, DataExpr)
template <typename Term>
bool check_term_Binder(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::Binder)
  {
    return false;
  }

  // check the children
  if (a.size() != 3)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_BindingOperator<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_BindingOperator" << std::endl;
    return false;
  }
  if (!check_list_argument(a[1], check_rule_DataVarId<atermpp::aterm>, 1))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataVarId" << std::endl;
    return false;
  }
  if (!check_term_argument(a[2], check_rule_DataExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// SortRef(SortId, SortExpr)
template <typename Term>
bool check_term_SortRef(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::SortRef)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_SortId<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_SortId" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_SortExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_SortExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// ProcEqnSpec(ProcEqn*)
template <typename Term>
bool check_term_ProcEqnSpec(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::ProcEqnSpec)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_ProcEqn<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcEqn" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// StateForall(DataVarId+, StateFrm)
template <typename Term>
bool check_term_StateForall(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::StateForall)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_DataVarId<atermpp::aterm>, 1))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataVarId" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_StateFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_StateFrm" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// BooleanImp(BooleanExpression, BooleanExpression)
template <typename Term>
bool check_term_BooleanImp(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::BooleanImp)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_BooleanExpression<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_BooleanExpression" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_BooleanExpression<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_BooleanExpression" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// SortId(String)
template <typename Term>
bool check_term_SortId(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::SortId)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_String<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_String" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// UntypedAction(String, DataExpr*)
template <typename Term>
bool check_term_UntypedAction(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::UntypedAction)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_String<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_String" << std::endl;
    return false;
  }
  if (!check_list_argument(a[1], check_rule_DataExpr<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// StateNu(String, DataVarIdInit*, StateFrm)
template <typename Term>
bool check_term_StateNu(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::StateNu)
  {
    return false;
  }

  // check the children
  if (a.size() != 3)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_String<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_String" << std::endl;
    return false;
  }
  if (!check_list_argument(a[1], check_rule_DataVarIdInit<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataVarIdInit" << std::endl;
    return false;
  }
  if (!check_term_argument(a[2], check_rule_StateFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_StateFrm" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// RegNil()
template <typename Term>
bool check_term_RegNil(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::RegNil)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// DataSpec(SortSpec, ConsSpec, MapSpec, DataEqnSpec)
template <typename Term>
bool check_term_DataSpec(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::DataSpec)
  {
    return false;
  }

  // check the children
  if (a.size() != 4)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_SortSpec<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_SortSpec" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_ConsSpec<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ConsSpec" << std::endl;
    return false;
  }
  if (!check_term_argument(a[2], check_rule_MapSpec<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_MapSpec" << std::endl;
    return false;
  }
  if (!check_term_argument(a[3], check_rule_DataEqnSpec<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataEqnSpec" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// UntypedActMultAct(UntypedAction*)
template <typename Term>
bool check_term_UntypedActMultAct(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::UntypedActMultAct)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_UntypedAction<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_UntypedAction" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// Tau()
template <typename Term>
bool check_term_Tau(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::Tau)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// StateYaledTimed(DataExpr)
template <typename Term>
bool check_term_StateYaledTimed(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::StateYaledTimed)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_DataExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// SortCons(SortConsType, SortExpr)
template <typename Term>
bool check_term_SortCons(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::SortCons)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_SortConsType<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_SortConsType" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_SortExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_SortExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// DataEqnSpec(DataEqn*)
template <typename Term>
bool check_term_DataEqnSpec(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::DataEqnSpec)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_DataEqn<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataEqn" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// LinearProcessSummand(DataVarId*, DataExpr, MultActOrDelta, DataExprOrNil, DataVarIdInit*)
template <typename Term>
bool check_term_LinearProcessSummand(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::LinearProcessSummand)
  {
    return false;
  }

  // check the children
  if (a.size() != 5)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_DataVarId<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataVarId" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_DataExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataExpr" << std::endl;
    return false;
  }
  if (!check_term_argument(a[2], check_rule_MultActOrDelta<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_MultActOrDelta" << std::endl;
    return false;
  }
  if (!check_term_argument(a[3], check_rule_DataExprOrNil<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataExprOrNil" << std::endl;
    return false;
  }
  if (!check_list_argument(a[4], check_rule_DataVarIdInit<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataVarIdInit" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// SortSpec(SortDecl*)
template <typename Term>
bool check_term_SortSpec(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::SortSpec)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_SortDecl<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_SortDecl" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// ActionRenameRules(ActionRenameRule*)
template <typename Term>
bool check_term_ActionRenameRules(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::ActionRenameRules)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_ActionRenameRule<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ActionRenameRule" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// UntypedParamId(String, DataExpr*)
template <typename Term>
bool check_term_UntypedParamId(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::UntypedParamId)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_String<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_String" << std::endl;
    return false;
  }
  if (!check_list_argument(a[1], check_rule_DataExpr<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// BooleanEquation(FixPoint, BooleanVariable, BooleanExpression)
template <typename Term>
bool check_term_BooleanEquation(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::BooleanEquation)
  {
    return false;
  }

  // check the children
  if (a.size() != 3)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_FixPoint<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_FixPoint" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_BooleanVariable<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_BooleanVariable" << std::endl;
    return false;
  }
  if (!check_term_argument(a[2], check_rule_BooleanExpression<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_BooleanExpression" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// ConsSpec(OpId*)
template <typename Term>
bool check_term_ConsSpec(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::ConsSpec)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_OpId<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_OpId" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// SortList()
template <typename Term>
bool check_term_SortList(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::SortList)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// Sum(DataVarId+, ProcExpr)
template <typename Term>
bool check_term_Sum(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::Sum)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_DataVarId<atermpp::aterm>, 1))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataVarId" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_ProcExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// DataVarId(String, SortExpr, Number)
template <typename Term>
bool check_term_DataVarId(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::DataVarId)
  {
    return false;
  }

  // check the children
  if (a.size() != 3)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_String<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_String" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_SortExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_SortExpr" << std::endl;
    return false;
  }
  if (!check_term_argument(a[2], check_rule_Number<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_Number" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// ProcVarId(String, DataVarId*, Number)
template <typename Term>
bool check_term_ProcVarId(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::ProcVarId)
  {
    return false;
  }

  // check the children
  if (a.size() != 3)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_String<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_String" << std::endl;
    return false;
  }
  if (!check_list_argument(a[1], check_rule_DataVarId<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataVarId" << std::endl;
    return false;
  }
  if (!check_term_argument(a[2], check_rule_Number<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_Number" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// ProcessInit(ProcExpr)
template <typename Term>
bool check_term_ProcessInit(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::ProcessInit)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_ProcExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// UntypedIdentifier(String)
template <typename Term>
bool check_term_UntypedIdentifier(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::UntypedIdentifier)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_String<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_String" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// BooleanFalse()
template <typename Term>
bool check_term_BooleanFalse(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::BooleanFalse)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// BES(BooleanEquation*, BooleanExpression)
template <typename Term>
bool check_term_BES(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::BES)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_BooleanEquation<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_BooleanEquation" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_BooleanExpression<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_BooleanExpression" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// MapSpec(OpId*)
template <typename Term>
bool check_term_MapSpec(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::MapSpec)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_OpId<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_OpId" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// IfThen(DataExpr, ProcExpr)
template <typename Term>
bool check_term_IfThen(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::IfThen)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_DataExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataExpr" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_ProcExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// BooleanAnd(BooleanExpression, BooleanExpression)
template <typename Term>
bool check_term_BooleanAnd(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::BooleanAnd)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_BooleanExpression<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_BooleanExpression" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_BooleanExpression<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_BooleanExpression" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// LinProcSpec(DataSpec, ActSpec, GlobVarSpec, LinearProcess, LinearProcessInit)
template <typename Term>
bool check_term_LinProcSpec(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::LinProcSpec)
  {
    return false;
  }

  // check the children
  if (a.size() != 5)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_DataSpec<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataSpec" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_ActSpec<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ActSpec" << std::endl;
    return false;
  }
  if (!check_term_argument(a[2], check_rule_GlobVarSpec<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_GlobVarSpec" << std::endl;
    return false;
  }
  if (!check_term_argument(a[3], check_rule_LinearProcess<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_LinearProcess" << std::endl;
    return false;
  }
  if (!check_term_argument(a[4], check_rule_LinearProcessInit<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_LinearProcessInit" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// Choice(ProcExpr, ProcExpr)
template <typename Term>
bool check_term_Choice(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::Choice)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_ProcExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcExpr" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_ProcExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// LinearProcessInit(DataVarIdInit*)
template <typename Term>
bool check_term_LinearProcessInit(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::LinearProcessInit)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_DataVarIdInit<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataVarIdInit" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// MultAct(Action*)
template <typename Term>
bool check_term_MultAct(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::MultAct)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_Action<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_Action" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// PropVarInst(String, DataExpr*, Number)
template <typename Term>
bool check_term_PropVarInst(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::PropVarInst)
  {
    return false;
  }

  // check the children
  if (a.size() != 3)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_String<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_String" << std::endl;
    return false;
  }
  if (!check_list_argument(a[1], check_rule_DataExpr<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataExpr" << std::endl;
    return false;
  }
  if (!check_term_argument(a[2], check_rule_Number<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_Number" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// BagComp()
template <typename Term>
bool check_term_BagComp(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::BagComp)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// StateDelay()
template <typename Term>
bool check_term_StateDelay(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::StateDelay)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// RegAlt(RegFrm, RegFrm)
template <typename Term>
bool check_term_RegAlt(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::RegAlt)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_RegFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_RegFrm" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_RegFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_RegFrm" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// UntypedMultAct(UntypedAction*)
template <typename Term>
bool check_term_UntypedMultAct(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::UntypedMultAct)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_UntypedAction<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_UntypedAction" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// StructCons(String, StructProj*, StringOrEmpty)
template <typename Term>
bool check_term_StructCons(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::StructCons)
  {
    return false;
  }

  // check the children
  if (a.size() != 3)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_String<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_String" << std::endl;
    return false;
  }
  if (!check_list_argument(a[1], check_rule_StructProj<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_StructProj" << std::endl;
    return false;
  }
  if (!check_term_argument(a[2], check_rule_StringOrEmpty<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_StringOrEmpty" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// Mu()
template <typename Term>
bool check_term_Mu(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::Mu)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// PBEqnSpec(PBEqn*)
template <typename Term>
bool check_term_PBEqnSpec(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::PBEqnSpec)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_PBEqn<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_PBEqn" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// ActNot(ActFrm)
template <typename Term>
bool check_term_ActNot(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::ActNot)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_ActFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ActFrm" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// BooleanTrue()
template <typename Term>
bool check_term_BooleanTrue(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::BooleanTrue)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// Block(String*, ProcExpr)
template <typename Term>
bool check_term_Block(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::Block)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_String<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_String" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_ProcExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// Rename(RenameExpr*, ProcExpr)
template <typename Term>
bool check_term_Rename(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::Rename)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_RenameExpr<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_RenameExpr" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_ProcExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// Exists()
template <typename Term>
bool check_term_Exists(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::Exists)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// Sync(ProcExpr, ProcExpr)
template <typename Term>
bool check_term_Sync(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::Sync)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_ProcExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcExpr" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_ProcExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// ActExists(DataVarId+, ActFrm)
template <typename Term>
bool check_term_ActExists(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::ActExists)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_DataVarId<atermpp::aterm>, 1))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataVarId" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_ActFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ActFrm" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// ProcSpec(DataSpec, ActSpec, GlobVarSpec, ProcEqnSpec, ProcInit)
template <typename Term>
bool check_term_ProcSpec(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::ProcSpec)
  {
    return false;
  }

  // check the children
  if (a.size() != 5)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_DataSpec<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataSpec" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_ActSpec<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ActSpec" << std::endl;
    return false;
  }
  if (!check_term_argument(a[2], check_rule_GlobVarSpec<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_GlobVarSpec" << std::endl;
    return false;
  }
  if (!check_term_argument(a[3], check_rule_ProcEqnSpec<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcEqnSpec" << std::endl;
    return false;
  }
  if (!check_term_argument(a[4], check_rule_ProcInit<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcInit" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// UntypedSortsPossible(SortExpr+)
template <typename Term>
bool check_term_UntypedSortsPossible(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::UntypedSortsPossible)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_SortExpr<atermpp::aterm>, 1))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_SortExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// StateMu(String, DataVarIdInit*, StateFrm)
template <typename Term>
bool check_term_StateMu(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::StateMu)
  {
    return false;
  }

  // check the children
  if (a.size() != 3)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_String<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_String" << std::endl;
    return false;
  }
  if (!check_list_argument(a[1], check_rule_DataVarIdInit<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataVarIdInit" << std::endl;
    return false;
  }
  if (!check_term_argument(a[2], check_rule_StateFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_StateFrm" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// StateFalse()
template <typename Term>
bool check_term_StateFalse(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::StateFalse)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// PBESFalse()
template <typename Term>
bool check_term_PBESFalse(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::PBESFalse)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// PBESForall(DataVarId+, PBExpr)
template <typename Term>
bool check_term_PBESForall(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::PBESForall)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_DataVarId<atermpp::aterm>, 1))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataVarId" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_PBExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_PBExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// StateTrue()
template <typename Term>
bool check_term_StateTrue(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::StateTrue)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// BInit(ProcExpr, ProcExpr)
template <typename Term>
bool check_term_BInit(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::BInit)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_ProcExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcExpr" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_ProcExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// UntypedSortUnknown()
template <typename Term>
bool check_term_UntypedSortUnknown(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::UntypedSortUnknown)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// RegTrans(RegFrm)
template <typename Term>
bool check_term_RegTrans(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::RegTrans)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_RegFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_RegFrm" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// StateDelayTimed(DataExpr)
template <typename Term>
bool check_term_StateDelayTimed(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::StateDelayTimed)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_DataExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// Nu()
template <typename Term>
bool check_term_Nu(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::Nu)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// SortStruct(StructCons+)
template <typename Term>
bool check_term_SortStruct(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::SortStruct)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_StructCons<atermpp::aterm>, 1))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_StructCons" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// AtTime(ProcExpr, DataExpr)
template <typename Term>
bool check_term_AtTime(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::AtTime)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_ProcExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcExpr" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_DataExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// ActOr(ActFrm, ActFrm)
template <typename Term>
bool check_term_ActOr(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::ActOr)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_ActFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ActFrm" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_ActFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ActFrm" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// Comm(CommExpr*, ProcExpr)
template <typename Term>
bool check_term_Comm(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::Comm)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_CommExpr<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_CommExpr" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_ProcExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// BooleanNot(BooleanExpression)
template <typename Term>
bool check_term_BooleanNot(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::BooleanNot)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_BooleanExpression<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_BooleanExpression" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// Delta()
template <typename Term>
bool check_term_Delta(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::Delta)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// ActMultAct(Action*)
template <typename Term>
bool check_term_ActMultAct(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::ActMultAct)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_Action<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_Action" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// StateAnd(StateFrm, StateFrm)
template <typename Term>
bool check_term_StateAnd(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::StateAnd)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_StateFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_StateFrm" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_StateFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_StateFrm" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// LMerge(ProcExpr, ProcExpr)
template <typename Term>
bool check_term_LMerge(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::LMerge)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_ProcExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcExpr" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_ProcExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// SetComp()
template <typename Term>
bool check_term_SetComp(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::SetComp)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// ActForall(DataVarId+, ActFrm)
template <typename Term>
bool check_term_ActForall(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::ActForall)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_DataVarId<atermpp::aterm>, 1))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataVarId" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_ActFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ActFrm" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// RenameExpr(String, String)
template <typename Term>
bool check_term_RenameExpr(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::RenameExpr)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_String<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_String" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_String<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_String" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// Merge(ProcExpr, ProcExpr)
template <typename Term>
bool check_term_Merge(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::Merge)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_ProcExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcExpr" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_ProcExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// ActSpec(ActId*)
template <typename Term>
bool check_term_ActSpec(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::ActSpec)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_ActId<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ActId" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// BooleanVariable(String, Number)
template <typename Term>
bool check_term_BooleanVariable(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::BooleanVariable)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_String<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_String" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_Number<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_Number" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// Action(ActId, DataExpr*)
template <typename Term>
bool check_term_Action(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::Action)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_ActId<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ActId" << std::endl;
    return false;
  }
  if (!check_list_argument(a[1], check_rule_DataExpr<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// PBESAnd(PBExpr, PBExpr)
template <typename Term>
bool check_term_PBESAnd(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::PBESAnd)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_PBExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_PBExpr" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_PBExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_PBExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// Lambda()
template <typename Term>
bool check_term_Lambda(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::Lambda)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// StateMust(RegFrm, StateFrm)
template <typename Term>
bool check_term_StateMust(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::StateMust)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_RegFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_RegFrm" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_StateFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_StateFrm" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// Seq(ProcExpr, ProcExpr)
template <typename Term>
bool check_term_Seq(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::Seq)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_ProcExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcExpr" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_ProcExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// DataVarIdInit(DataVarId, DataExpr)
template <typename Term>
bool check_term_DataVarIdInit(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::DataVarIdInit)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_DataVarId<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataVarId" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_DataExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// Process(ProcVarId, DataExpr*)
template <typename Term>
bool check_term_Process(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::Process)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_ProcVarId<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcVarId" << std::endl;
    return false;
  }
  if (!check_list_argument(a[1], check_rule_DataExpr<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// ActAnd(ActFrm, ActFrm)
template <typename Term>
bool check_term_ActAnd(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::ActAnd)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_ActFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ActFrm" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_ActFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ActFrm" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// ActionRenameSpec(DataSpec, ActSpec, ActionRenameRules)
template <typename Term>
bool check_term_ActionRenameSpec(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::ActionRenameSpec)
  {
    return false;
  }

  // check the children
  if (a.size() != 3)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_DataSpec<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataSpec" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_ActSpec<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ActSpec" << std::endl;
    return false;
  }
  if (!check_term_argument(a[2], check_rule_ActionRenameRules<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ActionRenameRules" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// PBES(DataSpec, GlobVarSpec, PBEqnSpec, PBInit)
template <typename Term>
bool check_term_PBES(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::PBES)
  {
    return false;
  }

  // check the children
  if (a.size() != 4)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_DataSpec<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataSpec" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_GlobVarSpec<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_GlobVarSpec" << std::endl;
    return false;
  }
  if (!check_term_argument(a[2], check_rule_PBEqnSpec<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_PBEqnSpec" << std::endl;
    return false;
  }
  if (!check_term_argument(a[3], check_rule_PBInit<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_PBInit" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// StateVar(String, DataExpr*)
template <typename Term>
bool check_term_StateVar(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::StateVar)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_String<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_String" << std::endl;
    return false;
  }
  if (!check_list_argument(a[1], check_rule_DataExpr<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// ActionRenameRule(DataVarId*, DataExpr, ParamIdOrAction, ActionRenameRuleRHS)
template <typename Term>
bool check_term_ActionRenameRule(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::ActionRenameRule)
  {
    return false;
  }

  // check the children
  if (a.size() != 4)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_DataVarId<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataVarId" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_DataExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataExpr" << std::endl;
    return false;
  }
  if (!check_term_argument(a[2], check_rule_ParamIdOrAction<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ParamIdOrAction" << std::endl;
    return false;
  }
  if (!check_term_argument(a[3], check_rule_ActionRenameRuleRHS<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ActionRenameRuleRHS" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// RegSeq(RegFrm, RegFrm)
template <typename Term>
bool check_term_RegSeq(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::RegSeq)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_RegFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_RegFrm" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_RegFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_RegFrm" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// LinearProcess(DataVarId*, LinearProcessSummand*)
template <typename Term>
bool check_term_LinearProcess(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::LinearProcess)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_DataVarId<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataVarId" << std::endl;
    return false;
  }
  if (!check_list_argument(a[1], check_rule_LinearProcessSummand<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_LinearProcessSummand" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// ActAt(ActFrm, DataExpr)
template <typename Term>
bool check_term_ActAt(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::ActAt)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_ActFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ActFrm" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_DataExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// DataEqn(DataVarId*, DataExpr, DataExpr, DataExpr)
template <typename Term>
bool check_term_DataEqn(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::DataEqn)
  {
    return false;
  }

  // check the children
  if (a.size() != 4)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_DataVarId<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataVarId" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_DataExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataExpr" << std::endl;
    return false;
  }
  if (!check_term_argument(a[2], check_rule_DataExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataExpr" << std::endl;
    return false;
  }
  if (!check_term_argument(a[3], check_rule_DataExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// PBESNot(PBExpr)
template <typename Term>
bool check_term_PBESNot(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::PBESNot)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_PBExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_PBExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// StateExists(DataVarId+, StateFrm)
template <typename Term>
bool check_term_StateExists(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::StateExists)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_DataVarId<atermpp::aterm>, 1))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataVarId" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_StateFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_StateFrm" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// StateMay(RegFrm, StateFrm)
template <typename Term>
bool check_term_StateMay(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::StateMay)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_RegFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_RegFrm" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_StateFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_StateFrm" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// PBESTrue()
template <typename Term>
bool check_term_PBESTrue(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::PBESTrue)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// MultActName(String+)
template <typename Term>
bool check_term_MultActName(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::MultActName)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_String<atermpp::aterm>, 1))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_String" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// IfThenElse(DataExpr, ProcExpr, ProcExpr)
template <typename Term>
bool check_term_IfThenElse(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::IfThenElse)
  {
    return false;
  }

  // check the children
  if (a.size() != 3)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_DataExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataExpr" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_ProcExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcExpr" << std::endl;
    return false;
  }
  if (!check_term_argument(a[2], check_rule_ProcExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// Nil()
template <typename Term>
bool check_term_Nil(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::Nil)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// ProcEqn(ProcVarId, DataVarId*, ProcExpr)
template <typename Term>
bool check_term_ProcEqn(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::ProcEqn)
  {
    return false;
  }

  // check the children
  if (a.size() != 3)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_ProcVarId<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcVarId" << std::endl;
    return false;
  }
  if (!check_list_argument(a[1], check_rule_DataVarId<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataVarId" << std::endl;
    return false;
  }
  if (!check_term_argument(a[2], check_rule_ProcExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// StructProj(StringOrEmpty, SortExpr)
template <typename Term>
bool check_term_StructProj(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::StructProj)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_StringOrEmpty<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_StringOrEmpty" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_SortExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_SortExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// PBEqn(FixPoint, PropVarDecl, PBExpr)
template <typename Term>
bool check_term_PBEqn(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::PBEqn)
  {
    return false;
  }

  // check the children
  if (a.size() != 3)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_FixPoint<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_FixPoint" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_PropVarDecl<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_PropVarDecl" << std::endl;
    return false;
  }
  if (!check_term_argument(a[2], check_rule_PBExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_PBExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// Whr(DataExpr, WhrDecl+)
template <typename Term>
bool check_term_Whr(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::Whr)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_DataExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataExpr" << std::endl;
    return false;
  }
  if (!check_list_argument(a[1], check_rule_WhrDecl<atermpp::aterm>, 1))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_WhrDecl" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// OpId(String, SortExpr, Number)
template <typename Term>
bool check_term_OpId(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::OpId)
  {
    return false;
  }

  // check the children
  if (a.size() != 3)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_String<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_String" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_SortExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_SortExpr" << std::endl;
    return false;
  }
  if (!check_term_argument(a[2], check_rule_Number<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_Number" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// SortSet()
template <typename Term>
bool check_term_SortSet(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::SortSet)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// ActFalse()
template <typename Term>
bool check_term_ActFalse(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::ActFalse)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// ActId(String, SortExpr*)
template <typename Term>
bool check_term_ActId(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::ActId)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_String<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_String" << std::endl;
    return false;
  }
  if (!check_list_argument(a[1], check_rule_SortExpr<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_SortExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// StateYaled()
template <typename Term>
bool check_term_StateYaled(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::StateYaled)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// PBESOr(PBExpr, PBExpr)
template <typename Term>
bool check_term_PBESOr(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::PBESOr)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_PBExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_PBExpr" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_PBExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_PBExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// UntypedProcessAssignment(String, UntypedIdentifierAssignment*)
template <typename Term>
bool check_term_UntypedProcessAssignment(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::UntypedProcessAssignment)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_String<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_String" << std::endl;
    return false;
  }
  if (!check_list_argument(a[1], check_rule_UntypedIdentifierAssignment<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_UntypedIdentifierAssignment" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// SortFBag()
template <typename Term>
bool check_term_SortFBag(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::SortFBag)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// Allow(MultActName*, ProcExpr)
template <typename Term>
bool check_term_Allow(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::Allow)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_MultActName<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_MultActName" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_ProcExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ProcExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// PropVarDecl(String, DataVarId*)
template <typename Term>
bool check_term_PropVarDecl(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::PropVarDecl)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_String<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_String" << std::endl;
    return false;
  }
  if (!check_list_argument(a[1], check_rule_DataVarId<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataVarId" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// ActImp(ActFrm, ActFrm)
template <typename Term>
bool check_term_ActImp(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::ActImp)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_ActFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ActFrm" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_ActFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_ActFrm" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// SortBag()
template <typename Term>
bool check_term_SortBag(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::SortBag)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// PBInit(PropVarInst)
template <typename Term>
bool check_term_PBInit(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::PBInit)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_PropVarInst<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_PropVarInst" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// ActTrue()
template <typename Term>
bool check_term_ActTrue(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::ActTrue)
  {
    return false;
  }

  // check the children
  if (a.size() != 0)
  {
    return false;
  }

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// RegTransOrNil(RegFrm)
template <typename Term>
bool check_term_RegTransOrNil(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::RegTransOrNil)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_RegFrm<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_RegFrm" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// GlobVarSpec(DataVarId*)
template <typename Term>
bool check_term_GlobVarSpec(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::GlobVarSpec)
  {
    return false;
  }

  // check the children
  if (a.size() != 1)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_list_argument(a[0], check_rule_DataVarId<atermpp::aterm>, 0))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataVarId" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}

// UntypedIdentifierAssignment(String, DataExpr)
template <typename Term>
bool check_term_UntypedIdentifierAssignment(Term t)
{
#ifndef MCRL2_NO_SOUNDNESS_CHECKS
  // check the type of the term
  atermpp::aterm term(t);
  if (!term.type_is_appl())
  {
    return false;
  }
  const atermpp::aterm_appl& a = atermpp::down_cast<atermpp::aterm_appl>(term);
  if (a.function() != core::detail::function_symbols::UntypedIdentifierAssignment)
  {
    return false;
  }

  // check the children
  if (a.size() != 2)
  {
    return false;
  }
#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
  if (!check_term_argument(a[0], check_rule_String<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_String" << std::endl;
    return false;
  }
  if (!check_term_argument(a[1], check_rule_DataExpr<atermpp::aterm>))
  {
    mCRL2log(log::debug, "soundness_checks") << "check_rule_DataExpr" << std::endl;
    return false;
  }
#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS

#endif // MCRL2_NO_SOUNDNESS_CHECKS
  return true;
}
//--- end generated code ---//

} // namespace detail

} // namespace core

} // namespace mcrl2
#endif // MCRL2_BASIC_DETAIL_SOUNDNESS_CHECKS_H
