public static void substituteVariablesInTree(Cons tree, Cons substitution) {
    { Stella_Object operator = tree.value;

      { GeneralizedSymbol testValue000 = ((GeneralizedSymbol)(operator));

        if ((testValue000 == Logic.SYM_STELLA_EXISTS) ||
            ((testValue000 == Logic.SYM_LOGIC_FOR_SOME) ||
             (testValue000 == Logic.SYM_STELLA_FORALL))) {
          if (operator == Logic.SYM_LOGIC_FOR_SOME) {
            tree.firstSetter(Logic.SYM_STELLA_EXISTS);
          }
          { Stella_Object variables = tree.rest.value;

            if (!Stella_Object.consP(variables)) {
              variables = Cons.consList(Cons.cons(variables, Stella.NIL));
            }
            { Stella_Object v1 = null;
              Cons iter000 = ((Cons)(variables));

              for (;!(iter000 == Stella.NIL); iter000 = iter000.rest) {
                v1 = iter000.value;
                if (substitution.memberP(v1)) {
                  { Symbol v2 = null;
                    Cons iter001 = Logic.SYSTEM_DEFINED_ARGUMENT_NAMES;

                    loop001 : for (;!(iter001 == Stella.NIL); iter001 = iter001.rest) {
                      v2 = ((Symbol)(iter001.value));
                      if (!substitution.memberP(v2)) {
                        substitution = Cons.cons(v2, substitution);
                        substitution = Cons.cons(v1, substitution);
                        break loop001;
                      }
                    }
                  }
                }
              }
            }
          }
          Logic.substituteVariablesInTree(tree.rest, substitution);
        }
        else {
          { ConsIterator it1 = tree.allocateIterator();

            while (it1.nextP()) {
              { Stella_Object arg = it1.value;

                { Surrogate testValue001 = Stella_Object.safePrimaryType(arg);

                  if (Surrogate.subtypeOfSymbolP(testValue001)) {
                    { Symbol arg000 = ((Symbol)(arg));

                      if (Logic.questionMarkSymbolP(arg000)) {
                        { ConsIterator it2 = substitution.allocateIterator();

                          loop003 : while (it2.nextP()) {
                            if (it2.value == arg000) {
                              it2.nextP();
                              it1.valueSetter(it2.value);
                              break loop003;
                            }
                          }
                        }
                      }
                    }
                  }
                  else if (testValue001 == Logic.SGT_STELLA_CONS) {
                    { Cons arg000 = ((Cons)(arg));

                      Logic.substituteVariablesInTree(arg000, substitution);
                    }
                  }
                  else {
                  }
                }
              }
            }
          }
        }
      }
    }
  }