public static boolean deriveSatelliteRulesForGoalP(Proposition forallprop, Description goaldescription, Keyword direction, boolean lazysatellitesP) {
    Logic.finalizeObjects();
    { boolean createdsatellitesP = false;
      Description goaldesc = null;
      boolean positiveonlyP = direction == Logic.KWD_POSITIVE;
      boolean contrapositiveonlyP = direction == Logic.KWD_CONTRAPOSITIVE;

      { Object old$Context$000 = Stella.$CONTEXT$.get();
        Object old$Module$000 = Stella.$MODULE$.get();

        try {
          Native.setSpecial(Stella.$CONTEXT$, forallprop.homeContext);
          Native.setSpecial(Stella.$MODULE$, ((Context)(Stella.$CONTEXT$.get())).baseModule);
          { Proposition goal = null;
            Cons iter000 = Proposition.findMatchableGoals(forallprop, Logic.KWD_HEAD).theConsList;

            for (;!(iter000 == Stella.NIL); iter000 = iter000.rest) {
              goal = ((Proposition)(iter000.value));
              if ((goaldescription == null) ||
                  (goaldescription == Proposition.extractGoalDescription(goal, Logic.KWD_HEAD))) {
                createdsatellitesP = true;
                if (lazysatellitesP) {
                  if (goaldescription == null) {
                    goaldesc = Proposition.extractGoalDescription(goal, Logic.KWD_HEAD);
                  }
                  else {
                    goaldesc = goaldescription;
                  }
                  if (((SequenceIndex)(KeyValueList.dynamicSlotValue(goaldesc.dynamicSlots, Logic.SYM_LOGIC_RULES_WITH_DEFERRED_SATELLITES, null))) == null) {
                    KeyValueList.setDynamicSlotValue(goaldesc.dynamicSlots, Logic.SYM_LOGIC_RULES_WITH_DEFERRED_SATELLITES, Logic.createSequenceIndex(Logic.KWD_NON_PAGING, Stella.NIL), null);
                  }
                  ((SequenceIndex)(KeyValueList.dynamicSlotValue(goaldesc.dynamicSlots, Logic.SYM_LOGIC_RULES_WITH_DEFERRED_SATELLITES, null))).insert(forallprop);
                }
                else if (!contrapositiveonlyP) {
                  Proposition.deriveOneSatelliteRule(forallprop, goal, Logic.KWD_HEAD, false);
                }
                if ((!positiveonlyP) &&
                    ((!((BooleanWrapper)(KeyValueList.dynamicSlotValue(forallprop.dynamicSlots, Logic.SYM_LOGIC_BACKWARD_ONLYp, Stella.FALSE_WRAPPER))).wrapperValue) &&
                     (!Proposition.atomicForallArgumentP(forallprop, Logic.KWD_TAIL)))) {
                  if (lazysatellitesP) {
                    KeyValueList.setDynamicSlotValue(goaldesc.dynamicSlots, Logic.SYM_LOGIC_DEFERRED_CONTRAPOSITIVESp, Stella.TRUE_WRAPPER, null);
                  }
                  else {
                    Proposition.deriveOneSatelliteRule(forallprop, goal, Logic.KWD_HEAD, true);
                  }
                }
              }
            }
          }
          if ((!((BooleanWrapper)(KeyValueList.dynamicSlotValue(forallprop.dynamicSlots, Logic.SYM_LOGIC_BACKWARD_ONLYp, Stella.FALSE_WRAPPER))).wrapperValue) &&
              (Proposition.atomicForallArgumentP(forallprop, Logic.KWD_TAIL) ||
               ((!Proposition.atomicForallArgumentP(forallprop, Logic.KWD_HEAD)) ||
                ((BooleanWrapper)(KeyValueList.dynamicSlotValue(forallprop.dynamicSlots, Logic.SYM_LOGIC_FORWARD_ONLYp, Stella.FALSE_WRAPPER))).wrapperValue))) {
            { Proposition goal = null;
              Cons iter001 = Proposition.findMatchableGoals(forallprop, Logic.KWD_TAIL).theConsList;

              for (;!(iter001 == Stella.NIL); iter001 = iter001.rest) {
                goal = ((Proposition)(iter001.value));
                if ((goaldescription == null) ||
                    (goaldescription == Proposition.extractGoalDescription(goal, Logic.KWD_TAIL))) {
                  createdsatellitesP = true;
                  if (lazysatellitesP) {
                    if (goaldescription == null) {
                      goaldesc = Proposition.extractGoalDescription(goal, Logic.KWD_TAIL);
                    }
                    else {
                      goaldesc = goaldescription;
                    }
                    if (((SequenceIndex)(KeyValueList.dynamicSlotValue(goaldesc.dynamicSlots, Logic.SYM_LOGIC_RULES_WITH_DEFERRED_SATELLITES, null))) == null) {
                      KeyValueList.setDynamicSlotValue(goaldesc.dynamicSlots, Logic.SYM_LOGIC_RULES_WITH_DEFERRED_SATELLITES, Logic.createSequenceIndex(Logic.KWD_NON_PAGING, Stella.NIL), null);
                    }
                    ((SequenceIndex)(KeyValueList.dynamicSlotValue(goaldesc.dynamicSlots, Logic.SYM_LOGIC_RULES_WITH_DEFERRED_SATELLITES, null))).insert(forallprop);
                  }
                  else if (!contrapositiveonlyP) {
                    Proposition.deriveOneSatelliteRule(forallprop, goal, Logic.KWD_TAIL, false);
                  }
                  if ((!positiveonlyP) &&
                      ((!((BooleanWrapper)(KeyValueList.dynamicSlotValue(forallprop.dynamicSlots, Logic.SYM_LOGIC_FORWARD_ONLYp, Stella.FALSE_WRAPPER))).wrapperValue) &&
                       (!Proposition.atomicForallArgumentP(forallprop, Logic.KWD_HEAD)))) {
                    if (lazysatellitesP) {
                      KeyValueList.setDynamicSlotValue(goaldesc.dynamicSlots, Logic.SYM_LOGIC_DEFERRED_CONTRAPOSITIVESp, Stella.TRUE_WRAPPER, null);
                    }
                    else {
                      Proposition.deriveOneSatelliteRule(forallprop, goal, Logic.KWD_TAIL, true);
                    }
                  }
                }
              }
            }
          }
          if (createdsatellitesP &&
              (((TruthValue)(Stella_Object.accessInContext(forallprop.truthValue, forallprop.homeContext, false))) != null)) {
            { Object old$Context$001 = Stella.$CONTEXT$.get();
              Object old$Module$001 = Stella.$MODULE$.get();

              try {
                Native.setSpecial(Stella.$CONTEXT$, forallprop.homeContext);
                Native.setSpecial(Stella.$MODULE$, ((Context)(Stella.$CONTEXT$.get())).baseModule);
                { Object old$InvisibleassertionP$000 = Logic.$INVISIBLEASSERTIONp$.get();

                  try {
                    Native.setBooleanSpecial(Logic.$INVISIBLEASSERTIONp$, true);
                    { Proposition satellite = null;
                      Cons iter002 = forallprop.satellitePropositions().theConsList;

                      for (;!(iter002 == Stella.NIL); iter002 = iter002.rest) {
                        satellite = ((Proposition)(iter002.value));
                        Proposition.assignTruthValue(satellite, ((TruthValue)(Stella_Object.accessInContext(forallprop.truthValue, forallprop.homeContext, false))));
                      }
                    }

                  } finally {
                    Logic.$INVISIBLEASSERTIONp$.set(old$InvisibleassertionP$000);
                  }
                }

              } finally {
                Stella.$MODULE$.set(old$Module$001);
                Stella.$CONTEXT$.set(old$Context$001);
              }
            }
          }
          return (createdsatellitesP);

        } finally {
          Stella.$MODULE$.set(old$Module$000);
          Stella.$CONTEXT$.set(old$Context$000);
        }
      }
    }
  }