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

      if ((testValue000 == Logic.KWD_ISA) ||
          ((testValue000 == Logic.KWD_PREDICATE) ||
           ((testValue000 == Logic.KWD_FUNCTION) ||
            (testValue000 == Logic.KWD_EQUIVALENT)))) {
        Proposition.invertAtomicProposition(self);
      }
      else if (testValue000 == Logic.KWD_AND) {
        { int argumentcount = self.arguments.length();

          Proposition.simplifyProposition(self);
          if (self.arguments.length() < argumentcount) {
            return (Proposition.invertProposition(self));
          }
        }
        self.kind = Logic.KWD_OR;
        self.operator = Logic.SGT_LOGIC_OR;
        { int i = Stella.NULL_INTEGER;
          int iter000 = 0;
          int upperBound000 = self.arguments.length() - 1;

          for (;iter000 <= upperBound000; iter000 = iter000 + 1) {
            i = iter000;
            (self.arguments.theArray)[i] = (Proposition.safelyInvertProposition(((Proposition)((self.arguments.theArray)[i]))));
          }
        }
      }
      else if (testValue000 == Logic.KWD_OR) {
        self.kind = Logic.KWD_AND;
        self.operator = Logic.SGT_LOGIC_AND;
        { int i = Stella.NULL_INTEGER;
          int iter001 = 0;
          int upperBound001 = self.arguments.length() - 1;

          for (;iter001 <= upperBound001; iter001 = iter001 + 1) {
            i = iter001;
            (self.arguments.theArray)[i] = (Proposition.safelyInvertProposition(((Proposition)((self.arguments.theArray)[i]))));
          }
        }
      }
      else if (testValue000 == Logic.KWD_NOT) {
        Proposition.overlayProposition(self, ((Proposition)((self.arguments.theArray)[0])));
        Proposition.normalizeProposition(self);
      }
      else if (testValue000 == Logic.KWD_EXISTS) {
        if (Proposition.functionInducedExistsP(self)) {
          Proposition.embedNegationWithinFunctionInducedExists(self);
        }
        else {
          Proposition.invertExistsProposition(self);
        }
      }
      else if (testValue000 == Logic.KWD_FORALL) {
        Proposition.invertForallProposition(self);
      }
      else if (testValue000 == Logic.KWD_IMPLIES) {
        Proposition.invertImpliesProposition(self);
      }
      else if (testValue000 == Logic.KWD_CONSTANT) {
        { GeneralizedSymbol testValue001 = self.operator;

          if (testValue001 == Logic.SGT_STELLA_TRUE) {
            return (Logic.FALSE_PROPOSITION);
          }
          else if (testValue001 == Logic.SGT_STELLA_FALSE) {
            return (Logic.TRUE_PROPOSITION);
          }
          else {
            { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

              stream000.nativeStream.print("`" + testValue001 + "' is not a valid case option");
              throw ((StellaException)(StellaException.newStellaException(stream000.theStringReader()).fillInStackTrace()));
            }
          }
        }
      }
      else if (testValue000 == Logic.KWD_FAIL) {
        Proposition.invertAtomicProposition(self);
      }
      else {
        { OutputStringStream stream001 = OutputStringStream.newOutputStringStream();

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