public static Keyword resumeProofStrategyAfterSubgoal(ControlFrame frame, Keyword lastmove) {
    { Keyword result = null;

      { Keyword testValue000 = frame.currentStrategy;

        if (testValue000 == Logic.KWD_SPECIALIST) {
          result = ControlFrame.continueSpecialistProof(frame, lastmove);
        }
        else if (testValue000 == Logic.KWD_ANTECEDENTS) {
          if (frame.partialMatchFrame != null) {
            result = frame.partialMatchFrame.continuePartialAntecedentsProof(lastmove);
          }
          else {
            result = ControlFrame.continueAntecedentsProof(frame, lastmove);
          }
        }
        else if (testValue000 == Logic.KWD_CLUSTERED_CONJUNCTION) {
          result = ControlFrame.continueClusteredConjunctionProof(frame, lastmove);
        }
        else if (testValue000 == Logic.KWD_CONDITIONAL_ANTECEDENT) {
          result = ControlFrame.continueConditionalAntecedentProof(frame, lastmove);
        }
        else if (testValue000 == Logic.KWD_DISJUNCTIVE_IMPLICATION_INTRODUCTION) {
          result = ControlFrame.resumeDisjunctiveImplicationProof(frame, lastmove);
        }
        else {
          ControlFrame.propagateFrameTruthValue(frame.result, frame);
          if (frame.result.partialMatchFrame != null) {
            frame.result.partialMatchFrame.propagateFramePartialTruth(frame);
          }
          if (lastmove == Logic.KWD_UP_TRUE) {
            if (frame.down != null) {
              result = Logic.KWD_CONTINUING_SUCCESS;
            }
            else {
              result = Logic.KWD_FINAL_SUCCESS;
            }
          }
          else if (lastmove == Logic.KWD_UP_FAIL) {
            if ((frame.truthValue == Logic.FALSE_TRUTH_VALUE) ||
                (frame.truthValue == Logic.DEFAULT_FALSE_TRUTH_VALUE)) {
              result = Logic.KWD_TERMINAL_FAILURE;
            }
            else {
              result = 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()));
            }
          }
        }
      }
      if (result == Logic.KWD_CONTINUING_SUCCESS) {
        if (((Boolean)(Logic.$GENERATE_ALL_PROOFSp$.get())).booleanValue() &&
            ((frame.state == Logic.KWD_ATOMIC_GOAL) &&
             ((!((((QueryIterator)(Logic.$QUERYITERATOR$.get())) != null) &&
            (((QueryIterator)(Logic.$QUERYITERATOR$.get())).partialMatchStrategy != null))) &&
              (!ControlFrame.newBindingsSinceLastChoicePointP(frame))))) {
          frame.justifications.push(Logic.KWD_DUMMY_JUSTIFICATION);
          result = Logic.KWD_MOVE_DOWN;
        }
      }
      else if ((result == Logic.KWD_FINAL_SUCCESS) ||
          (result == Logic.KWD_TERMINAL_FAILURE)) {
        frame.nextStrategies = Stella.NIL;
        frame.currentStrategy = null;
        if (result == Logic.KWD_TERMINAL_FAILURE) {
          result = Logic.KWD_FAILURE;
        }
      }
      else if (result == Logic.KWD_FAILURE) {
        frame.currentStrategy = null;
      }
      else if ((result == Logic.KWD_MOVE_DOWN) ||
          (result == Logic.KWD_MOVE_IN_PLACE)) {
      }
      else {
        { OutputStringStream stream001 = OutputStringStream.newOutputStringStream();

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