public static void verifyArgumentTypesAndCount(Proposition proposition) {
    if ((((Keyword)(Logic.$TYPECHECKMODE$.get())) == Logic.KWD_IGNORE_TYPE_VIOLATIONS) ||
        ((!Logic.worldStateP(((Context)(Stella.$CONTEXT$.get())))) ||
         (!Stella_Object.isaP(proposition.operator, Logic.SGT_STELLA_SURROGATE)))) {
      return;
    }
    { NamedDescription description = Logic.getDescription(((Surrogate)(proposition.operator)));
      int argumentcount = proposition.arguments.length();

      { Keyword testValue000 = proposition.kind;

        if ((testValue000 == Logic.KWD_PREDICATE) ||
            ((testValue000 == Logic.KWD_FUNCTION) ||
             (testValue000 == Logic.KWD_ISA))) {
          if (description == null) {
            return;
          }
          { int arity = description.arity();
            boolean variablearityP = !(arity > 0);
            boolean functionP = proposition.kind == Logic.KWD_FUNCTION;

            if ((!variablearityP) &&
                (!(argumentcount == arity))) {
              Proposition.handleArityViolation(proposition, arity);
            }
            { Stella_Object arg = null;
              Vector vector000 = proposition.arguments;
              int index000 = 0;
              int length000 = vector000.length();
              IntegerIntervalIterator i = Stella.interval(1, ((variablearityP &&
                  functionP) ? (argumentcount - 1) : argumentcount));
              Stella_Object type = null;
              Iterator iter000 = NamedDescription.allDomainTypes(description);

              for (;(index000 < length000) &&
                        (i.nextP() &&
                         iter000.nextP()); index000 = index000 + 1) {
                arg = (vector000.theArray)[index000];
                type = iter000.value;
                if ((type != null) &&
                    ((!(type == Logic.SGT_STELLA_THING)) &&
                     (arg != null))) {
                  Logic.verifyOneArgumentType(arg, ((Surrogate)(type)), proposition, description);
                }
              }
            }
            if (functionP) {
              Logic.verifyOneArgumentType(proposition.arguments.last(), ((Surrogate)(description.ioVariableTypes.last())), proposition, description);
            }
          }
        }
        else if (testValue000 == Logic.KWD_EQUIVALENT) {
          { Stella_Object arg1 = (proposition.arguments.theArray)[0];
            Stella_Object arg2 = (proposition.arguments.theArray)[1];
            Surrogate requiredtype = null;
            Stella_Object constrainingarg = null;
            Stella_Object offendingarg = null;
            boolean typeisokP = false;
            Stella_Object substitutevalue = null;

            requiredtype = Logic.safeLogicalType(arg2);
            { Object [] caller_MV_returnarray = new Object[1];

              typeisokP = Logic.checkCoercedTypeP(arg1, requiredtype, false, caller_MV_returnarray);
              substitutevalue = ((Stella_Object)(caller_MV_returnarray[0]));
            }
            if (!Stella_Object.eqlP(arg1, substitutevalue)) {
              (proposition.arguments.theArray)[0] = substitutevalue;
              return;
            }
            else if (!typeisokP) {
              constrainingarg = arg2;
              offendingarg = arg1;
            }
            if (typeisokP) {
              requiredtype = Logic.safeLogicalType(arg1);
              { Object [] caller_MV_returnarray = new Object[1];

                typeisokP = Logic.checkCoercedTypeP(arg2, requiredtype, false, caller_MV_returnarray);
                substitutevalue = ((Stella_Object)(caller_MV_returnarray[0]));
              }
              if (!Stella_Object.eqlP(arg2, substitutevalue)) {
                (proposition.arguments.theArray)[1] = substitutevalue;
                return;
              }
              else if (!typeisokP) {
                constrainingarg = arg1;
                offendingarg = arg2;
              }
            }
            if (!(typeisokP)) {
              { Object old$Termunderconstruction$000 = Logic.$TERMUNDERCONSTRUCTION$.get();

                try {
                  Native.setSpecial(Logic.$TERMUNDERCONSTRUCTION$, ((Stella_Object)(Logic.$TERMUNDERCONSTRUCTION$.get())));
                  if ((((Stella_Object)(Logic.$TERMUNDERCONSTRUCTION$.get())) == null) &&
                      Logic.skolemP(constrainingarg)) {
                    Native.setSpecial(Logic.$TERMUNDERCONSTRUCTION$, ((Skolem)(constrainingarg)).definingProposition);
                  }
                  Proposition.handleArgumentTypeViolation(proposition, offendingarg, requiredtype);

                } finally {
                  Logic.$TERMUNDERCONSTRUCTION$.set(old$Termunderconstruction$000);
                }
              }
            }
          }
        }
        else {
        }
      }
    }
  }