public static boolean freeVariableP(PatternVariable variable, Proposition proposition) {
    { Keyword testValue000 = proposition.kind;

      if ((testValue000 == Logic.KWD_FORALL) ||
          (testValue000 == Logic.KWD_EXISTS)) {
        if (((Vector)(KeyValueList.dynamicSlotValue(proposition.dynamicSlots, Logic.SYM_LOGIC_IO_VARIABLES, null))).memberP(variable)) {
          return (false);
        }
      }
      else {
      }
    }
    { boolean alwaysP000 = true;

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

        loop000 : for (;index000 < length000; index000 = index000 + 1) {
          arg = (vector000.theArray)[index000];
          if (Stella_Object.isaP(arg, Logic.SGT_LOGIC_PROPOSITION)) {
            if (!PatternVariable.freeVariableP(variable, ((Proposition)(arg)))) {
              alwaysP000 = false;
              break loop000;
            }
          }
        }
      }
      { boolean value000 = alwaysP000;

        return (value000);
      }
    }
  }