public static boolean containsNestedArgumentP(Proposition proposition) {
    { Keyword testValue000 = proposition.kind;

      if ((testValue000 == Logic.KWD_ISA) ||
          ((testValue000 == Logic.KWD_FUNCTION) ||
           ((testValue000 == Logic.KWD_PREDICATE) ||
            ((testValue000 == Logic.KWD_EQUIVALENT) ||
             (testValue000 == Logic.KWD_IMPLIES))))) {
        { Stella_Object term = null;
          Vector vector000 = proposition.arguments;
          int index000 = 0;
          int length000 = vector000.length();

          for (;index000 < length000; index000 = index000 + 1) {
            term = (vector000.theArray)[index000];
            if (Surrogate.subtypeOfP(Stella_Object.safePrimaryType(term), Logic.SGT_LOGIC_PATTERN_VARIABLE)) {
              { PatternVariable term000 = ((PatternVariable)(term));

                if (term000.definingProposition != null) {
                  return (true);
                }
              }
            }
            else {
            }
          }
        }
      }
      else {
      }
    }
    return (false);
  }