public static Keyword resumeDisjunctiveImplicationProof(ControlFrame frame, Keyword lastmove) {
    if (lastmove == Logic.KWD_UP_TRUE) {
      ControlFrame.propagateFrameTruthValue(frame.result, frame);
      if (frame.result.partialMatchFrame != null) {
        frame.result.partialMatchFrame.propagateFramePartialTruth(frame);
      }
      if (frame.down != null) {
        return (Logic.KWD_CONTINUING_SUCCESS);
      }
      else {
        return (Logic.KWD_FINAL_SUCCESS);
      }
    }
    else if (lastmove == Logic.KWD_UP_FAIL) {
      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()));
      }
    }
  }