public static Keyword continueConditionalAntecedentProof(ControlFrame frame, Keyword lastmove) {
    { ConditionalAntecedentProofAdjunct proofadjunct = ((ConditionalAntecedentProofAdjunct)(((ProofAdjunct)(KeyValueList.dynamicSlotValue(frame.dynamicSlots, Logic.SYM_LOGIC_PROOF_ADJUNCT, null)))));
      Proposition provablerule = proofadjunct.provableRule;

      if (lastmove == Logic.KWD_DOWN) {
        ControlFrame.createSubgoalFrame(frame, provablerule, Logic.KWD_FORWARD_GOALS);
        return (Logic.KWD_MOVE_DOWN);
      }
      else if (lastmove == Logic.KWD_UP_TRUE) {
        if (proofadjunct.phase == Logic.KWD_ORIGINAL_GOAL) {
          frame.truthValue = TruthValue.weakenTruthValue(ControlFrame.propagateFrameTruthValue(frame.result, frame), ((TruthValue)(Stella_Object.accessInContext(provablerule.truthValue, provablerule.homeContext, false))));
          return (Logic.selectProofResult(true, frame.down != null, false));
        }
        Proposition.assignTruthValue(provablerule, frame.result.truthValue);
        { ControlFrame downframe = ControlFrame.createSubgoalFrame(frame, frame.proposition, Logic.KWD_ANTECEDENTS);

          KeyValueList.setDynamicSlotValue(downframe.dynamicSlots, Logic.SYM_STELLA_ITERATOR, Cons.consList(Cons.cons(provablerule, Stella.NIL)).allocateIterator(), null);
          proofadjunct.phase = Logic.KWD_ORIGINAL_GOAL;
          return (Logic.KWD_MOVE_DOWN);
        }
      }
      else if (lastmove == Logic.KWD_UP_FAIL) {
        ControlFrame.propagateFrameTruthValue(frame.result, frame);
        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()));
        }
      }
    }
  }