public static void helpCollectSinglyBoundVariables(Proposition proposition, List boundvariables, boolean recursiveP) {
    { Keyword testValue000 = proposition.kind;

      if (testValue000 == Logic.KWD_AND) {
        { Stella_Object arg = null;
          Vector vector000 = proposition.arguments;
          int index000 = 0;
          int length000 = vector000.length();

          for (;index000 < length000; index000 = index000 + 1) {
            arg = (vector000.theArray)[index000];
            Proposition.helpCollectSinglyBoundVariables(((Proposition)(arg)), boundvariables, recursiveP);
          }
        }
      }
      else if ((testValue000 == Logic.KWD_FUNCTION) ||
          (testValue000 == Logic.KWD_PREDICATE)) {
        if (proposition.arguments.length() > 0) {
          { Stella_Object lastarg = (proposition.arguments.theArray)[(proposition.arguments.length() - 1)];

            { boolean testValue001 = false;

              testValue001 = Logic.variableP(lastarg);
              if (testValue001) {
                testValue001 = !boundvariables.memberP(lastarg);
                if (testValue001) {
                  testValue001 = (proposition.kind == Logic.KWD_FUNCTION) ||
                      ((recursiveP &&
                      Logic.singleValuedTermP(Logic.getDescription(((Surrogate)(proposition.operator))))) ||
                       ((!recursiveP) &&
                        Logic.nonRecursiveSingleValuedTermP(Logic.getDescription(((Surrogate)(proposition.operator))))));
                  if (testValue001) {
                    { boolean alwaysP000 = true;

                      { Stella_Object arg = null;
                        Iterator iter000 = proposition.arguments.butLast();

                        loop001 : while (iter000.nextP()) {
                          arg = iter000.value;
                          if (!((!Logic.variableP(arg)) ||
                              boundvariables.memberP(arg))) {
                            alwaysP000 = false;
                            break loop001;
                          }
                        }
                      }
                      testValue001 = alwaysP000;
                    }
                  }
                }
              }
              if (testValue001) {
                boundvariables.push(((PatternVariable)(lastarg)));
              }
            }
          }
        }
      }
      else if (testValue000 == Logic.KWD_EQUIVALENT) {
        { Cons unboundvariables = Stella.NIL;

          { Stella_Object arg = null;
            Vector vector001 = proposition.arguments;
            int index001 = 0;
            int length001 = vector001.length();

            for (;index001 < length001; index001 = index001 + 1) {
              arg = (vector001.theArray)[index001];
              if (Logic.variableP(arg) &&
                  (!boundvariables.memberP(arg))) {
                unboundvariables = Cons.cons(arg, unboundvariables);
              }
            }
          }
          if (unboundvariables.length() == 1) {
            boundvariables.push(((PatternVariable)(unboundvariables.value)));
          }
        }
      }
      else {
      }
    }
  }