public static Keyword continueAndProof(ControlFrame frame, Keyword lastmove) {
    { Proposition proposition = frame.proposition;
      Vector conjuncts = null;

      if (lastmove == Logic.KWD_DOWN) {
        if (proposition.clusteredConjunctionP()) {
          ControlFrame.overlayWithStrategyFrame(frame, Logic.KWD_CLUSTERED_CONJUNCTION);
          return (Logic.KWD_MOVE_IN_PLACE);
        }
        else if (frame.reversePolarityP &&
            Proposition.closedPropositionP(proposition)) {
          return (ControlFrame.overlayWithFailFrame(frame, proposition));
        }
        else {
          conjuncts = ((Vector)(KeyValueList.dynamicSlotValue(frame.dynamicSlots, Logic.SYM_STELLA_ARGUMENTS, null)));
          if (conjuncts == null) {
            conjuncts = Vector.newVector(proposition.arguments.length());
            KeyValueList.setDynamicSlotValue(frame.dynamicSlots, Logic.SYM_STELLA_ARGUMENTS, conjuncts, null);
            if (Proposition.dynamicallyOptimizePropositionP(proposition)) {
              proposition = Proposition.shallowCopyProposition(proposition);
              frame.proposition = proposition;
            }
          }
          if (Proposition.dynamicallyOptimizePropositionP(proposition) &&
              (frame.down == null)) {
            Logic.dynamicallyReoptimizeArguments(proposition.arguments, frame.argumentCursor);
          }
          return (Logic.KWD_MOVE_DOWN);
        }
      }
      else if (lastmove == Logic.KWD_UP_TRUE) {
        conjuncts = ((Vector)(KeyValueList.dynamicSlotValue(frame.dynamicSlots, Logic.SYM_STELLA_ARGUMENTS, null)));
        (conjuncts.theArray)[(frame.argumentCursor)] = (frame.result);
        if (frame.argumentCursor == (conjuncts.length() - 1)) {
          frame.down = null;
          { ControlFrame conjunct = null;
            Vector vector000 = conjuncts;
            int index000 = 0;
            int length000 = vector000.length();
            int i = Stella.NULL_INTEGER;
            int iter000 = 0;

            for (;index000 < length000; index000 = index000 + 1, iter000 = iter000 + 1) {
              conjunct = ((ControlFrame)((vector000.theArray)[index000]));
              i = iter000;
              frame.truthValue = ((i == 0) ? conjunct.truthValue : TruthValue.conjoinTruthValues(frame.truthValue, conjunct.truthValue));
              if (!(conjunct.state == Logic.KWD_POPPED)) {
                frame.argumentCursor = i;
                frame.down = conjunct;
              }
            }
          }
          if (((Boolean)(Logic.$RECORD_JUSTIFICATIONSp$.get())).booleanValue()) {
            ControlFrame.recordAndIntroductionJustification(frame, lastmove);
          }
          if (frame.down != null) {
            return (Logic.KWD_CONTINUING_SUCCESS);
          }
          else {
            return (Logic.KWD_FINAL_SUCCESS);
          }
        }
        else {
          frame.down = null;
          frame.argumentCursor = frame.argumentCursor + 1;
          if (Proposition.dynamicallyOptimizePropositionP(proposition)) {
            Logic.dynamicallyReoptimizeArguments(proposition.arguments, frame.argumentCursor);
          }
          return (Logic.KWD_MOVE_DOWN);
        }
      }
      else if (lastmove == Logic.KWD_UP_FAIL) {
        conjuncts = ((Vector)(KeyValueList.dynamicSlotValue(frame.dynamicSlots, Logic.SYM_STELLA_ARGUMENTS, null)));
        if (conjuncts == null) {
          frame.truthValue = TruthValue.conjoinTruthValues(Logic.UNKNOWN_TRUTH_VALUE, frame.result.truthValue);
          return (Logic.KWD_FAILURE);
        }
        frame.down = null;
        { ControlFrame conjunct = null;
          Vector vector001 = conjuncts;
          int index001 = 0;
          int length001 = vector001.length();
          int i = Stella.NULL_INTEGER;
          int iter001 = 0;

          loop001 : for (;index001 < length001; index001 = index001 + 1, iter001 = iter001 + 1) {
            conjunct = ((ControlFrame)((vector001.theArray)[index001]));
            i = iter001;
            if (conjunct == null) {
              break loop001;
            }
            if (!(conjunct.state == Logic.KWD_POPPED)) {
              frame.argumentCursor = i;
              frame.down = conjunct;
            }
          }
        }
        if (frame.down != null) {
          return (Logic.KWD_MOVE_DOWN);
        }
        else {
          ControlFrame.propagateFrameTruthValue(frame.result, frame);
          (conjuncts.theArray)[(frame.argumentCursor)] = (frame.result);
          { ControlFrame conjunct = null;
            Vector vector002 = conjuncts;
            int index002 = 0;
            int length002 = vector002.length();
            int i = Stella.NULL_INTEGER;
            int iter002 = 0;
            int upperBound000 = frame.argumentCursor;
            boolean unboundedP000 = upperBound000 == Stella.NULL_INTEGER;

            loop002 : for (;(index002 < length002) &&
                      (unboundedP000 ||
                       (iter002 <= upperBound000)); index002 = index002 + 1, iter002 = iter002 + 1) {
              conjunct = ((ControlFrame)((vector002.theArray)[index002]));
              i = iter002;
              i = i;
              if (conjunct == null) {
                break loop002;
              }
              frame.truthValue = TruthValue.conjoinTruthValues(frame.truthValue, conjunct.truthValue);
            }
          }
          return (Logic.KWD_FAILURE);
        }
      }
      else {
        { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

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