public static Keyword continueExistsProof(ControlFrame frame, Keyword lastmove) {
    if (lastmove == Logic.KWD_DOWN) {
      return (Logic.KWD_MOVE_DOWN);
    }
    else if (lastmove == Logic.KWD_UP_TRUE) {
      { ControlFrame result = frame.result;

        if (result.partialMatchFrame != null) {
          result.partialMatchFrame.propagateFramePartialTruth(frame);
        }
        ControlFrame.propagateFrameTruthValue(result, frame);
        if (((Boolean)(Logic.$RECORD_JUSTIFICATIONSp$.get())).booleanValue()) {
          ControlFrame.recordExistentialIntroductionJustification(frame, lastmove);
        }
        if (frame.down == null) {
          return (Logic.KWD_FINAL_SUCCESS);
        }
        else {
          return (Logic.KWD_CONTINUING_SUCCESS);
        }
      }
    }
    else if (lastmove == Logic.KWD_UP_FAIL) {
      { ControlFrame result = frame.result;

        if (result.partialMatchFrame != null) {
          result.partialMatchFrame.propagateFramePartialTruth(frame);
        }
        ControlFrame.propagateFrameTruthValue(result, frame);
        if (frame.down == null) {
          return (Logic.KWD_FAILURE);
        }
        else {
          throw ((StellaException)(StellaException.newStellaException("Failed subgoal of 'exists' didn't remove itself from stack.").fillInStackTrace()));
        }
      }
    }
    else {
      { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

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