public static Keyword continueOrProof(ControlFrame frame, Keyword lastmove) {
    { Proposition proposition = frame.proposition;

      if (lastmove == Logic.KWD_DOWN) {
        if (frame.reversePolarityP &&
            Proposition.closedPropositionP(proposition)) {
          return (ControlFrame.overlayWithFailFrame(frame, proposition));
        }
        if (!(frame.down != null)) {
          ControlFrame.createChoicePoint(frame);
        }
        return (Logic.KWD_MOVE_DOWN);
      }
      else if (lastmove == Logic.KWD_UP_TRUE) {
        frame.truthValue = frame.result.truthValue;
        if (((Boolean)(Logic.$RECORD_JUSTIFICATIONSp$.get())).booleanValue()) {
          ControlFrame.recordOrIntroductionJustification(frame, lastmove);
        }
        if (frame.down == null) {
          frame.argumentCursor = frame.argumentCursor + 1;
        }
        if ((frame.argumentCursor >= proposition.arguments.length()) ||
            ((!ControlFrame.newBindingsSinceLastChoicePointP(frame)) &&
             (!((Boolean)(Logic.$GENERATE_ALL_PROOFSp$.get())).booleanValue()))) {
          if (frame.down != null) {
            ControlFrame.popFramesUpTo(frame.down);
          }
          return (Logic.KWD_FINAL_SUCCESS);
        }
        else {
          return (Logic.KWD_CONTINUING_SUCCESS);
        }
      }
      else if (lastmove == Logic.KWD_UP_FAIL) {
        { TruthValue chooseValue000 = null;

          if (frame.truthValue == null) {
            { TruthValue temp000 = frame.result.truthValue;

              chooseValue000 = ((temp000 != null) ? temp000 : Logic.UNKNOWN_TRUTH_VALUE);
            }
          }
          else {
            chooseValue000 = TruthValue.disjoinTruthValues(frame.truthValue, frame.result.truthValue);
          }
          frame.truthValue = chooseValue000;
        }
        frame.argumentCursor = frame.argumentCursor + 1;
        if (frame.argumentCursor < proposition.arguments.length()) {
          {
            ControlFrame.createChoicePoint(frame);
            return (Logic.KWD_MOVE_DOWN);
          }
        }
        else {
          if (Logic.currentInferenceLevel().keyword == Logic.KWD_REFUTATION) {
            ControlFrame.overlayWithStrategyFrame(frame, Logic.KWD_DISJUNCTIVE_IMPLICATION_INTRODUCTION);
            return (Logic.KWD_MOVE_IN_PLACE);
          }
          else {
            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()));
        }
      }
    }
  }