public static Cons helpUpdateTopLevelProposition(Proposition proposition, Keyword updatemode) {
    if (proposition == null) {
      return (null);
    }
    if (Proposition.lookupAnnotation(proposition, Logic.KWD_CONFIDENCE_LEVEL) == Logic.KWD_DEFAULT) {
      updatemode = Logic.defaultifyUpdateMode(updatemode);
      if ((updatemode == Logic.KWD_PRESUME_TRUE) ||
          (updatemode == Logic.KWD_PRESUME_FALSE)) {
        Proposition.removeAnnotation(proposition, Logic.KWD_CONFIDENCE_LEVEL);
      }
    }
    if (Proposition.nativeSlotPropositionP(proposition)) {
      return (Proposition.updateNativeSlotProposition(proposition, updatemode));
    }
    { Object old$Context$000 = Stella.$CONTEXT$.get();

      try {
        Native.setSpecial(Stella.$CONTEXT$, Logic.getTopLevelUpdateContext());
        { Keyword testValue000 = proposition.kind;

          if (testValue000 == Logic.KWD_AND) {
            { Cons propositions = Stella.NIL;

              { 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];
                  { Proposition p = null;
                    Cons iter000 = Proposition.helpUpdateTopLevelProposition(((Proposition)(arg)), updatemode);
                    Cons collect000 = null;

                    for (;!(iter000 == Stella.NIL); iter000 = iter000.rest) {
                      p = ((Proposition)(iter000.value));
                      if ((p != null) &&
                          (!p.deletedP())) {
                        if (collect000 == null) {
                          {
                            collect000 = Cons.cons(p, Stella.NIL);
                            if (propositions == Stella.NIL) {
                              propositions = collect000;
                            }
                            else {
                              Cons.addConsToEndOfConsList(propositions, collect000);
                            }
                          }
                        }
                        else {
                          {
                            collect000.rest = Cons.cons(p, Stella.NIL);
                            collect000 = collect000.rest;
                          }
                        }
                      }
                    }
                  }
                }
              }
              Proposition.destroyRedundantProposition(proposition);
              return (propositions);
            }
          }
          else if (testValue000 == Logic.KWD_EQUIVALENT) {
            proposition = Proposition.updateEquivalenceProposition(proposition, updatemode);
            if (proposition == null) {
              return (Stella.NIL);
            }
          }
          else if (testValue000 == Logic.KWD_NOT) {
            { Stella_Object argument = (proposition.arguments.theArray)[0];

              if ((updatemode == Logic.KWD_ASSERT_TRUE) ||
                  ((updatemode == Logic.KWD_ASSERT_FALSE) ||
                   ((updatemode == Logic.KWD_PRESUME_TRUE) ||
                    ((updatemode == Logic.KWD_PRESUME_FALSE) ||
                     ((updatemode == Logic.KWD_RETRACT_TRUE) ||
                      (updatemode == Logic.KWD_RETRACT_FALSE)))))) {
                Proposition.updatePropositionTruthValue(((Proposition)(argument)), Logic.invertUpdateMode(updatemode));
                Proposition.destroyRedundantProposition(proposition);
                if ((argument != null) &&
                    (!argument.deletedP())) {
                  return (Cons.consList(Cons.cons(argument, Stella.NIL)));
                }
                else {
                  return (Stella.NIL);
                }
              }
              else {
              }
            }
          }
          else if (testValue000 == Logic.KWD_EXISTS) {
            return (Proposition.helpUpdateTopLevelProposition(Proposition.skolemizeExistsProposition(proposition), updatemode));
          }
          else {
          }
        }
        if (!(proposition.kind == Logic.KWD_FUNCTION)) {
          Proposition.updatePropositionTruthValue(proposition, updatemode);
        }
        if (proposition.deletedP()) {
          return (Stella.NIL);
        }
        else {
          return (Cons.consList(Cons.cons(proposition, Stella.NIL)));
        }

      } finally {
        Stella.$CONTEXT$.set(old$Context$000);
      }
    }
  }