public static Stella_Object generateProposition(Proposition self) {
    { Keyword testValue000 = self.kind;

      if ((testValue000 == Logic.KWD_PREDICATE) ||
          ((testValue000 == Logic.KWD_ISA) ||
           ((testValue000 == Logic.KWD_AND) ||
            ((testValue000 == Logic.KWD_OR) ||
             (testValue000 == Logic.KWD_NOT))))) {
        { Symbol operator = Proposition.generateOperator(self);

          return (Cons.cons(operator, Logic.generateArguments(self.arguments).concatenate(Stella.NIL, Stella.NIL)));
        }
      }
      else if (testValue000 == Logic.KWD_FUNCTION) {
        return (Proposition.generateFunctionProposition(self));
      }
      else if (testValue000 == Logic.KWD_EQUIVALENT) {
        return (Cons.cons(Logic.SYM_STELLA_e, Logic.generateArguments(self.arguments).concatenate(Stella.NIL, Stella.NIL)));
      }
      else if (testValue000 == Logic.KWD_EXISTS) {
        return (Cons.list$(Cons.cons(Logic.SYM_STELLA_EXISTS, Cons.cons(Logic.generateVariables(((Vector)(KeyValueList.dynamicSlotValue(self.dynamicSlots, Logic.SYM_LOGIC_IO_VARIABLES, null))), false), Cons.cons(Cons.cons(Proposition.generateProposition(((Proposition)((self.arguments.theArray)[0]))), Stella.NIL), Stella.NIL)))));
      }
      else if (testValue000 == Logic.KWD_FORALL) {
        { boolean forwardP = !((BooleanWrapper)(KeyValueList.dynamicSlotValue(self.dynamicSlots, Logic.SYM_LOGIC_BACKWARD_ONLYp, Stella.FALSE_WRAPPER))).wrapperValue;
          Symbol arrow = Surrogate.symbolize(Proposition.chooseImplicationOperator(self, forwardP));

          return (Cons.list$(Cons.cons(Logic.SYM_STELLA_FORALL, Cons.cons(Logic.generateVariables(((Vector)(KeyValueList.dynamicSlotValue(self.dynamicSlots, Logic.SYM_LOGIC_IO_VARIABLES, null))), false), Cons.cons(Cons.cons(Cons.cons(arrow, Cons.cons(Proposition.generateProposition(((Proposition)((self.arguments.theArray)[((forwardP ? 0 : 1))]))), Cons.cons(Proposition.generateProposition(((Proposition)((self.arguments.theArray)[((forwardP ? 1 : 0))]))), Stella.NIL))), Stella.NIL), Stella.NIL)))));
        }
      }
      else if (testValue000 == Logic.KWD_IMPLIES) {
        return (Proposition.generateImpliesProposition(self));
      }
      else if (testValue000 == Logic.KWD_FAIL) {
        return (Cons.cons(Logic.SYM_LOGIC_FAIL, Logic.generateArguments(self.arguments).concatenate(Stella.NIL, Stella.NIL)));
      }
      else if (testValue000 == Logic.KWD_CONSTANT) {
        return (Proposition.generateOperator(self));
      }
      else {
        { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

          stream000.nativeStream.print("`" + testValue000 + "' is not a valid case option");
          throw ((StellaException)(StellaException.newStellaException(stream000.theStringReader()).fillInStackTrace()));
        }
      }
    }
  }