public static void deriveOneSatelliteRule(Proposition masterforall, Proposition goal, Keyword headortail, boolean contrapositiveP) {
    { Proposition invertedforall = null;
      Description head = null;
      Description tail = null;
      boolean overrideforwardonlyP = false;

      if ((headortail == Logic.KWD_TAIL) &&
          (((!Proposition.atomicGoalPropositionP(((Proposition)((masterforall.arguments.theArray)[0])))) ||
          Proposition.variableArityGoalPropositionP(((Proposition)((masterforall.arguments.theArray)[0])))) &&
           (!contrapositiveP))) {
        Proposition.deriveComplexForwardRule(goal, masterforall);
        return;
      }
      { Object old$Evaluationmode$000 = Logic.$EVALUATIONMODE$.get();

        try {
          Native.setSpecial(Logic.$EVALUATIONMODE$, Logic.KWD_DESCRIPTION);
          invertedforall = Proposition.invertForallAroundGoal(masterforall, goal, headortail, contrapositiveP);

        } finally {
          Logic.$EVALUATIONMODE$.set(old$Evaluationmode$000);
        }
      }
      if (invertedforall == null) {
        return;
      }
      if (contrapositiveP) {
        if (headortail == Logic.KWD_HEAD) {
          headortail = Logic.KWD_TAIL;
        }
        else if (headortail == Logic.KWD_TAIL) {
          headortail = Logic.KWD_HEAD;
        }
        else {
          { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

            stream000.nativeStream.print("`" + headortail + "' is not a valid case option");
            throw ((StellaException)(StellaException.newStellaException(stream000.theStringReader()).fillInStackTrace()));
          }
        }
      }
      if (headortail == Logic.KWD_HEAD) {
        head = Proposition.extractGoalDescription(((Proposition)((invertedforall.arguments.theArray)[1])), null);
        tail = Proposition.constructDescriptionFromForallProposition(invertedforall, Logic.KWD_TAIL);
      }
      else if (headortail == Logic.KWD_TAIL) {
        tail = Proposition.extractGoalDescription(((Proposition)((invertedforall.arguments.theArray)[0])), null);
        head = Proposition.constructDescriptionFromForallProposition(invertedforall, Logic.KWD_HEAD);
      }
      else {
        { OutputStringStream stream001 = OutputStringStream.newOutputStringStream();

          stream001.nativeStream.print("`" + headortail + "' is not a valid case option");
          throw ((StellaException)(StellaException.newStellaException(stream001.theStringReader()).fillInStackTrace()));
        }
      }
      if (((BooleanWrapper)(KeyValueList.dynamicSlotValue(masterforall.dynamicSlots, Logic.SYM_LOGIC_FORWARD_ONLYp, Stella.FALSE_WRAPPER))).wrapperValue &&
          (headortail == Logic.KWD_HEAD)) {
        overrideforwardonlyP = Description.namedDescriptionP(head) &&
            (Description.namedDescriptionP(tail) &&
             (head.arity() == tail.arity()));
        if (!overrideforwardonlyP) {
          return;
        }
      }
      { Proposition impliesprop = Logic.createImpliesProposition(tail, head);

        { Object old$Evaluationmode$001 = Logic.$EVALUATIONMODE$.get();

          try {
            Native.setSpecial(Logic.$EVALUATIONMODE$, Logic.KWD_EXTENSIONAL_ASSERTION);
            { Proposition duplicate = Proposition.recursivelyFastenDownPropositions(impliesprop, false);

              if (!(duplicate == impliesprop)) {
                impliesprop = duplicate;
              }
              else if (headortail == Logic.KWD_TAIL) {
                Proposition.markAsForwardRule(impliesprop);
              }
            }

          } finally {
            Logic.$EVALUATIONMODE$.set(old$Evaluationmode$001);
          }
        }
        if (masterforall.satellitePropositions().emptyP()) {
          KeyValueList.setDynamicSlotValue(masterforall.dynamicSlots, Logic.SYM_LOGIC_SATELLITE_PROPOSITIONS, List.newList(), null);
        }
        masterforall.satellitePropositions().insertNew(impliesprop);
        KeyValueList.setDynamicSlotValue(impliesprop.dynamicSlots, Logic.SYM_LOGIC_MASTER_PROPOSITION, masterforall, null);
        if (((BooleanWrapper)(KeyValueList.dynamicSlotValue(masterforall.dynamicSlots, Logic.SYM_LOGIC_FORWARD_ONLYp, Stella.FALSE_WRAPPER))).wrapperValue &&
            (!overrideforwardonlyP)) {
          if (contrapositiveP) {
            KeyValueList.setDynamicSlotValue(impliesprop.dynamicSlots, Logic.SYM_LOGIC_BACKWARD_ONLYp, Stella.TRUE_WRAPPER, Stella.FALSE_WRAPPER);
          }
          else {
            KeyValueList.setDynamicSlotValue(impliesprop.dynamicSlots, Logic.SYM_LOGIC_FORWARD_ONLYp, Stella.TRUE_WRAPPER, Stella.FALSE_WRAPPER);
          }
        }
        if (((BooleanWrapper)(KeyValueList.dynamicSlotValue(masterforall.dynamicSlots, Logic.SYM_LOGIC_BACKWARD_ONLYp, Stella.FALSE_WRAPPER))).wrapperValue) {
          if (contrapositiveP) {
            KeyValueList.setDynamicSlotValue(impliesprop.dynamicSlots, Logic.SYM_LOGIC_FORWARD_ONLYp, Stella.TRUE_WRAPPER, Stella.FALSE_WRAPPER);
          }
          else {
            KeyValueList.setDynamicSlotValue(impliesprop.dynamicSlots, Logic.SYM_LOGIC_BACKWARD_ONLYp, Stella.TRUE_WRAPPER, Stella.FALSE_WRAPPER);
          }
        }
        if (((BooleanWrapper)(KeyValueList.dynamicSlotValue(masterforall.dynamicSlots, Logic.SYM_LOGIC_DONT_OPTIMIZEp, Stella.FALSE_WRAPPER))).wrapperValue) {
          KeyValueList.setDynamicSlotValue(impliesprop.dynamicSlots, Logic.SYM_LOGIC_DONT_OPTIMIZEp, Stella.TRUE_WRAPPER, Stella.FALSE_WRAPPER);
          tail = ((Description)((impliesprop.arguments.theArray)[0]));
          if (tail.nativeRelation() == null) {
            KeyValueList.setDynamicSlotValue(tail.dynamicSlots, Logic.SYM_LOGIC_DONT_OPTIMIZEp, Stella.TRUE_WRAPPER, Stella.FALSE_WRAPPER);
          }
          head = ((Description)((impliesprop.arguments.theArray)[1]));
          if (head.nativeRelation() == null) {
            KeyValueList.setDynamicSlotValue(head.dynamicSlots, Logic.SYM_LOGIC_DONT_OPTIMIZEp, Stella.TRUE_WRAPPER, Stella.FALSE_WRAPPER);
          }
        }
      }
    }
  }