public static boolean equivalentFormulaeP(Stella_Object self, Stella_Object other, KeyValueMap mapping) {
    { Stella_Object surrogatevalue = null;

      if (Stella_Object.isaP(self, Logic.SGT_STELLA_SURROGATE)) {
        surrogatevalue = ((Surrogate)(self)).surrogateValue;
        if (surrogatevalue != null) {
          self = surrogatevalue;
        }
      }
      if (Stella_Object.isaP(other, Logic.SGT_STELLA_SURROGATE)) {
        surrogatevalue = ((Surrogate)(other)).surrogateValue;
        if (surrogatevalue != null) {
          other = surrogatevalue;
        }
      }
    }
    if ((mapping != null) &&
        (Stella_Object.eqlP(other, mapping.lookup(self)) ||
         Stella_Object.eqlP(self, mapping.lookup(other)))) {
      return (true);
    }
    if (Stella_Object.equalP(self, other)) {
      return (true);
    }
    if (mapping != null) {
      if (((Boolean)(Logic.$UNIFY_PROPOSITIONSp$.get())).booleanValue() &&
          (Logic.variableP(self) ||
           Logic.variableP(other))) {
        if (((QueryIterator)(Logic.$QUERYITERATOR$.get())) == null) {
          mapping.insertAt(self, other);
          return (true);
        }
        { Stella_Object value1 = Logic.argumentBoundTo(self);
          Stella_Object value2 = Logic.argumentBoundTo(other);

          if ((value1 == null) ||
              (value2 == null)) {
            mapping.insertAt(self, other);
            return (true);
          }
          else {
            return (Stella_Object.equalP(value1, value2));
          }
        }
      }
    }
    if (!(self.primaryType() == other.primaryType())) {
      return (false);
    }
    { Surrogate testValue000 = Stella_Object.safePrimaryType(self);

      if (Surrogate.subtypeOfP(testValue000, Logic.SGT_LOGIC_PROPOSITION)) {
        { Proposition self000 = ((Proposition)(self));

          return (Proposition.equivalentPropositionsP(self000, ((Proposition)(other)), mapping));
        }
      }
      else if (Surrogate.subtypeOfP(testValue000, Logic.SGT_LOGIC_DESCRIPTION)) {
        { Description self000 = ((Description)(self));

          return (Description.equivalentDescriptionsP(self000, ((Description)(other)), mapping));
        }
      }
      else if (Surrogate.subtypeOfP(testValue000, Logic.SGT_STELLA_SET)) {
        { Set self000 = ((Set)(self));

          return (Logic.equivalentEnumerationsP(self000, ((Collection)(other))));
        }
      }
      else if (Surrogate.subtypeOfP(testValue000, Logic.SGT_STELLA_LIST)) {
        { List self000 = ((List)(self));

          return (Logic.equivalentEnumerationsP(self000, ((Collection)(other))));
        }
      }
      else {
        return (false);
      }
    }
  }