public static Proposition buildAndOrNotProposition(Cons tree) {
    { Stella_Object term = null;
      Cons arguments = Stella.NIL;
      Proposition proposition = null;
      Vector argumentsvector = null;

      { GeneralizedSymbol testValue000 = ((GeneralizedSymbol)(tree.value));

        if ((testValue000 == Logic.SYM_STELLA_AND) ||
            ((testValue000 == Logic.SYM_STELLA_OR) ||
             (testValue000 == Logic.SYM_STELLA_NOT))) {
          { Stella_Object arg = null;
            Cons iter000 = tree.rest;
            Cons collect000 = null;

            for (;!(iter000 == Stella.NIL); iter000 = iter000.rest) {
              arg = iter000.value;
              { 
                term = Logic.buildProposition(arg);
                if (term != null) {
                  if (collect000 == null) {
                    {
                      collect000 = Cons.cons(term, Stella.NIL);
                      if (arguments == Stella.NIL) {
                        arguments = collect000;
                      }
                      else {
                        Cons.addConsToEndOfConsList(arguments, collect000);
                      }
                    }
                  }
                  else {
                    {
                      collect000.rest = Cons.cons(term, Stella.NIL);
                      collect000 = collect000.rest;
                    }
                  }
                }
              }
            }
          }
        }
        else {
          { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

            stream000.nativeStream.print("`" + testValue000 + "' is not a valid case option");
            throw ((StellaException)(StellaException.newStellaException(stream000.theStringReader()).fillInStackTrace()));
          }
        }
      }
      if ((arguments == Stella.NIL) &&
          (tree.value == Logic.SYM_STELLA_NOT)) {
        { OutputStringStream stream001 = OutputStringStream.newOutputStringStream();

          { Object old$PrintreadablyP$000 = Stella.$PRINTREADABLYp$.get();

            try {
              Native.setBooleanSpecial(Stella.$PRINTREADABLYp$, true);
              stream001.nativeStream.println("ERROR: Missing argument in NOT proposition: `" + tree + "'.");
              Logic.helpSignalPropositionError(stream001, Logic.KWD_ERROR);

            } finally {
              Stella.$PRINTREADABLYp$.set(old$PrintreadablyP$000);
            }
          }
          throw ((PropositionError)(PropositionError.newPropositionError(stream001.theStringReader()).fillInStackTrace()));
        }
      }
      if ((tree.value == Logic.SYM_STELLA_NOT) &&
          (Stella_Object.isaP(arguments.value, Logic.SGT_LOGIC_PROPOSITION) &&
           Proposition.functionInducedExistsP(((Proposition)(arguments.value))))) {
        return (Proposition.embedNegationWithinFunctionInducedExists(((Proposition)(arguments.value))));
      }
      proposition = Logic.createProposition(((Symbol)(tree.value)), arguments.length());
      argumentsvector = proposition.arguments;
      { Stella_Object arg = null;
        Cons iter001 = arguments;
        int i = Stella.NULL_INTEGER;
        int iter002 = 0;

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