public static void equateEquivalentFunctionPropositions(Proposition self) {
    { Surrogate relationref = ((Surrogate)(self.operator));
      int nofargs = self.arguments.length();
      List candidatepropositions = List.newList();

      { Stella_Object arg = null;
        Vector vector000 = self.arguments;
        int index000 = 0;
        int length000 = vector000.length();
        int i = Stella.NULL_INTEGER;
        int iter000 = 1;

        for (;index000 < length000; index000 = index000 + 1, iter000 = iter000 + 1) {
          arg = (vector000.theArray)[index000];
          i = iter000;
          if (!(i == nofargs)) {
            { Surrogate testValue000 = Stella_Object.safePrimaryType(arg);

              if (Surrogate.subtypeOfP(testValue000, Logic.SGT_LOGIC_SKOLEM)) {
                { Skolem arg000 = ((Skolem)(arg));

                  if ((((Stella_Object)(Stella_Object.accessInContext(arg000.variableValue, arg000.homeContext, false))) != null) &&
                      Stella_Object.isaP(((Stella_Object)(Stella_Object.accessInContext(arg000.variableValue, arg000.homeContext, false))), Logic.SGT_LOGIC_LOGIC_OBJECT)) {
                    { Proposition prop = null;
                      Iterator iter001 = Logic.unfilteredDependentPropositions(((Stella_Object)(Stella_Object.accessInContext(arg000.variableValue, arg000.homeContext, false))), relationref).allocateIterator();

                      while (iter001.nextP()) {
                        prop = ((Proposition)(iter001.value));
                        if ((((Surrogate)(prop.operator)) == relationref) &&
                            (!(prop == self))) {
                          candidatepropositions.insertNew(prop);
                        }
                      }
                    }
                  }
                  { LogicObject invarg = null;
                    Cons iter002 = arg000.variableValueInverse();

                    for (;!(iter002 == Stella.NIL); iter002 = iter002.rest) {
                      invarg = ((LogicObject)(iter002.value));
                      { Proposition prop = null;
                        Iterator iter003 = Logic.unfilteredDependentPropositions(invarg, relationref).allocateIterator();

                        while (iter003.nextP()) {
                          prop = ((Proposition)(iter003.value));
                          if ((((Surrogate)(prop.operator)) == relationref) &&
                              (!(prop == self))) {
                            candidatepropositions.insertNew(prop);
                          }
                        }
                      }
                    }
                  }
                }
              }
              else if (Surrogate.subtypeOfP(testValue000, Logic.SGT_LOGIC_LOGIC_OBJECT)) {
                { LogicObject arg000 = ((LogicObject)(arg));

                  { LogicObject invarg = null;
                    Cons iter004 = arg000.variableValueInverse();

                    for (;!(iter004 == Stella.NIL); iter004 = iter004.rest) {
                      invarg = ((LogicObject)(iter004.value));
                      { Proposition prop = null;
                        Iterator iter005 = Logic.unfilteredDependentPropositions(invarg, relationref).allocateIterator();

                        while (iter005.nextP()) {
                          prop = ((Proposition)(iter005.value));
                          if ((((Surrogate)(prop.operator)) == relationref) &&
                              (!(prop == self))) {
                            candidatepropositions.insertNew(prop);
                          }
                        }
                      }
                    }
                  }
                }
              }
              else {
              }
            }
          }
        }
      }
      { Proposition prop = null;
        Cons iter006 = candidatepropositions.theConsList;

        for (;!(iter006 == Stella.NIL); iter006 = iter006.rest) {
          prop = ((Proposition)(iter006.value));
          { boolean alwaysP000 = true;

            { Stella_Object arg1 = null;
              Vector vector001 = self.arguments;
              int index001 = 0;
              int length001 = vector001.length();
              Stella_Object arg2 = null;
              Vector vector002 = prop.arguments;
              int index002 = 0;
              int length002 = vector002.length();
              int i = Stella.NULL_INTEGER;
              int iter007 = 1;

              loop007 : for (;(index001 < length001) &&
                        (index002 < length002); 
                    index001 = index001 + 1,
                    index002 = index002 + 1,
                    iter007 = iter007 + 1) {
                arg1 = (vector001.theArray)[index001];
                arg2 = (vector002.theArray)[index002];
                i = iter007;
                if (!(i == nofargs)) {
                  if (!Stella_Object.eqlP(Logic.innermostOf(arg1), Logic.innermostOf(arg2))) {
                    alwaysP000 = false;
                    break loop007;
                  }
                }
              }
            }
            if (alwaysP000) {
              Proposition.equateValues(self, Logic.innermostOf(self.arguments.last()), Logic.innermostOf(prop.arguments.last()));
            }
          }
        }
      }
      candidatepropositions.free();
    }
  }