public static Cons infixToPrefixQuantificationTree(Cons tree) {
    { Stella_Object quantifier = tree.value;
      Cons generatorsclause = null;
      Stella_Object whereclause = null;
      Stella_Object alwaysclause = null;
      Cons residue = tree.rest;
      Cons otree = null;

      { Object [] caller_MV_returnarray = new Object[1];

        generatorsclause = Cons.extractGeneratorsClause(residue, caller_MV_returnarray);
        residue = ((Cons)(caller_MV_returnarray[0]));
      }
      if (generatorsclause == null) {
        return (null);
      }
      { Object [] caller_MV_returnarray = new Object[1];

        whereclause = Symbol.extractOptionAndResidue(Logic.SYM_STELLA_WHERE, residue, caller_MV_returnarray);
        residue = ((Cons)(caller_MV_returnarray[0]));
      }
      { Object [] caller_MV_returnarray = new Object[1];

        alwaysclause = Symbol.extractOptionAndResidue(Logic.SYM_STELLA_ALWAYS, residue, caller_MV_returnarray);
        residue = ((Cons)(caller_MV_returnarray[0]));
      }
      otree = Cons.cons(quantifier, Cons.cons(Logic.convertToPrefixPropositionTree(generatorsclause), (((whereclause != null) ? Cons.cons(Logic.convertToPrefixPropositionTree(whereclause), Stella.NIL) : Stella.getQuotedTree("((TRUE) \"/LOGIC\")", "/LOGIC"))).concatenate((((alwaysclause != null) ? Cons.cons(Logic.convertToPrefixPropositionTree(alwaysclause), Stella.NIL) : Stella.NIL)).concatenate(Stella.NIL, Stella.NIL), Stella.NIL)));
      if (!(residue == Stella.NIL)) {
        { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

          { Object old$PrintreadablyP$000 = Stella.$PRINTREADABLYp$.get();

            try {
              Native.setBooleanSpecial(Stella.$PRINTREADABLYp$, true);
              stream000.nativeStream.println("PARSING ERROR: Extra expressions at the end of quantified expression.");
              Logic.helpSignalPropositionError(stream000, Logic.KWD_ERROR);

            } finally {
              Stella.$PRINTREADABLYp$.set(old$PrintreadablyP$000);
            }
          }
          throw ((ParsingError)(ParsingError.newParsingError(stream000.theStringReader()).fillInStackTrace()));
        }
      }
      return (otree);
    }
  }