public static Proposition buildHoldsProposition(Cons tree) {
    { Stella_Object operatorexpression = tree.value;
      boolean explicitholdsP = operatorexpression == Logic.SYM_PL_KERNEL_KB_HOLDS;
      int argcount = tree.rest.length();
      Proposition proposition = Logic.createProposition(Logic.SYM_STELLA_PREDICATE, (explicitholdsP ? argcount : (argcount + 1)));

      proposition.operator = Logic.SGT_PL_KERNEL_KB_HOLDS;
      if (explicitholdsP) {
        { Stella_Object arg = null;
          Cons iter000 = tree.rest;
          int i = Stella.NULL_INTEGER;
          int iter001 = 0;

          for (;!(iter000 == Stella.NIL); iter000 = iter000.rest, iter001 = iter001 + 1) {
            arg = iter000.value;
            i = iter001;
            (proposition.arguments.theArray)[i] = (((i == 0) ? Logic.evaluateFirstArgument(arg, Logic.SYM_PL_KERNEL_KB_HOLDS) : Logic.evaluateTerm(arg)));
          }
        }
        return (proposition);
      }
      { Stella_Object operator = null;

        { Surrogate testValue000 = Stella_Object.safePrimaryType(operatorexpression);

          if (Surrogate.subtypeOfSymbolP(testValue000)) {
            { Symbol operatorexpression000 = ((Symbol)(operatorexpression));

              operator = Logic.lookupLogicVariableBinding(operatorexpression000);
            }
          }
          else if (testValue000 == Logic.SGT_STELLA_CONS) {
            { Cons operatorexpression000 = ((Cons)(operatorexpression));

              operator = Logic.evaluateFirstArgument(operatorexpression000, Logic.SYM_PL_KERNEL_KB_HOLDS);
            }
          }
          else {
            { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

              stream000.nativeStream.print("`" + testValue000 + "' is not a valid case option");
              throw ((StellaException)(StellaException.newStellaException(stream000.theStringReader()).fillInStackTrace()));
            }
          }
        }
        Logic.verifyEvaluableOperator(operator, Logic.KWD_PREDICATE);
        (proposition.arguments.theArray)[0] = operator;
        { Stella_Object arg = null;
          Cons iter002 = tree.rest;
          int i = Stella.NULL_INTEGER;
          int iter003 = 1;

          for (;!(iter002 == Stella.NIL); iter002 = iter002.rest, iter003 = iter003 + 1) {
            arg = iter002.value;
            i = iter003;
            (proposition.arguments.theArray)[i] = (Logic.evaluateTerm(arg));
          }
        }
        return (proposition);
      }
    }
  }