public static void simplifyProposition(Proposition proposition) {
    { Keyword testValue000 = proposition.kind;

      if (testValue000 == Logic.KWD_FORALL) {
      }
      else if (testValue000 == Logic.KWD_AND) {
        Proposition.simplifyConjunction(proposition);
      }
      else {
        { Stella_Object arg = null;
          Vector vector000 = proposition.arguments;
          int index000 = 0;
          int length000 = vector000.length();

          for (;index000 < length000; index000 = index000 + 1) {
            arg = (vector000.theArray)[index000];
            { Surrogate testValue001 = Stella_Object.safePrimaryType(arg);

              if (Surrogate.subtypeOfP(testValue001, Logic.SGT_LOGIC_PROPOSITION)) {
                { Proposition arg000 = ((Proposition)(arg));

                  Proposition.simplifyProposition(arg000);
                }
              }
              else if (Surrogate.subtypeOfP(testValue001, Logic.SGT_LOGIC_DESCRIPTION)) {
                { Description arg000 = ((Description)(arg));

                  Description.simplifyDescription(arg000, ((Boolean)(Logic.$POSTOPTIMIZATIONp$.get())).booleanValue());
                }
              }
              else {
              }
            }
          }
        }
      }
    }
  }