public static Proposition oldFindSimilarProposition(Proposition proposition, KeyValueMap mapping) {
    if (proposition.kind == Logic.KWD_CONSTANT) {
      return (null);
    }
    { Keyword kind = proposition.kind;
      GeneralizedSymbol operator = proposition.operator;
      Stella_Object argmapsto = null;
      SequenceIndex dependentslist = null;
      boolean hasdiscouragedargumentP = false;

      { Stella_Object arg = null;
        Vector vector000 = proposition.arguments;
        int index000 = 0;
        int length000 = vector000.length();

        loop000 : for (;index000 < length000; index000 = index000 + 1) {
          arg = (vector000.theArray)[index000];
          if (false) {
            hasdiscouragedargumentP = true;
            continue loop000;
          }
          { Stella_Object mapsto = Logic.mappedValueOf(arg, mapping, false);

            if ((mapsto != null) &&
                Logic.instanceHasBacklinksP(mapsto)) {
              argmapsto = mapsto;
              break loop000;
            }
          }
        }
      }
      if ((argmapsto == null) &&
          hasdiscouragedargumentP) {
        { Stella_Object arg = null;
          Vector vector001 = proposition.arguments;
          int index001 = 0;
          int length001 = vector001.length();

          loop001 : for (;index001 < length001; index001 = index001 + 1) {
            arg = (vector001.theArray)[index001];
            if (false) {
              { Stella_Object mapsto = Logic.mappedValueOf(arg, mapping, false);

                if ((mapsto != null) &&
                    Logic.instanceHasBacklinksP(mapsto)) {
                  argmapsto = mapsto;
                  break loop001;
                }
              }
            }
          }
        }
      }
      if (argmapsto == null) {
        return (null);
      }
      if (Surrogate.subtypeOfP(Stella_Object.safePrimaryType(argmapsto), Logic.SGT_LOGIC_LOGIC_OBJECT)) {
        { LogicObject argmapsto000 = ((LogicObject)(argmapsto));

          dependentslist = Logic.unfilteredDependentPropositions(argmapsto000, ((Surrogate)(operator)));
          if (kind == Logic.KWD_FUNCTION) {
            { Proposition value000 = null;

              { Proposition p = null;
                Iterator iter000 = dependentslist.allocateIterator();

                loop002 : while (iter000.nextP()) {
                  p = ((Proposition)(iter000.value));
                  { boolean testValue000 = false;

                    testValue000 = p.kind == kind;
                    if (testValue000) {
                      testValue000 = p.operator == operator;
                      if (testValue000) {
                        { boolean alwaysP000 = true;

                          { Stella_Object arg1 = null;
                            Iterator iter001 = proposition.arguments.butLast();
                            Stella_Object arg2 = null;
                            Iterator iter002 = p.arguments.butLast();

                            loop003 : while (iter001.nextP() &&
                                iter002.nextP()) {
                              arg1 = iter001.value;
                              arg2 = iter002.value;
                              if (!Logic.equalUpToSkolemIdentityP(arg1, arg2, mapping)) {
                                alwaysP000 = false;
                                break loop003;
                              }
                            }
                          }
                          testValue000 = alwaysP000;
                        }
                      }
                    }
                    if (testValue000) {
                      value000 = p;
                      break loop002;
                    }
                  }
                }
              }
              { Proposition value001 = value000;

                return (value001);
              }
            }
          }
          else {
            { Proposition value002 = null;

              { Proposition p = null;
                Iterator iter003 = dependentslist.allocateIterator();

                loop004 : while (iter003.nextP()) {
                  p = ((Proposition)(iter003.value));
                  { boolean testValue001 = false;

                    testValue001 = p.kind == kind;
                    if (testValue001) {
                      testValue001 = p.operator == operator;
                      if (testValue001) {
                        { boolean alwaysP001 = true;

                          { Stella_Object arg1 = null;
                            Vector vector002 = proposition.arguments;
                            int index002 = 0;
                            int length002 = vector002.length();
                            Stella_Object arg2 = null;
                            Vector vector003 = p.arguments;
                            int index003 = 0;
                            int length003 = vector003.length();

                            loop005 : for (;(index002 < length002) &&
                                      (index003 < length003); index002 = index002 + 1, index003 = index003 + 1) {
                              arg1 = (vector002.theArray)[index002];
                              arg2 = (vector003.theArray)[index003];
                              if (!Logic.equalUpToSkolemIdentityP(arg1, arg2, mapping)) {
                                alwaysP001 = false;
                                break loop005;
                              }
                            }
                          }
                          testValue001 = alwaysP001;
                        }
                      }
                    }
                    if (testValue001) {
                      value002 = p;
                      break loop004;
                    }
                  }
                }
              }
              { Proposition value003 = value002;

                return (value003);
              }
            }
          }
        }
      }
      else {
      }
      return (null);
    }
  }