/* Copyright (C) 2008  Hugh McGuire   http://www.cis.gvsu.edu/~mcguire/
 *                     Grand Valley State University, MI  49401-9403
 */
/*
This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 3
of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

For a copy of the GNU General Public License, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth floor, Boston, MA  02110-1301, USA.
Another option as of January 1, 2008 is to browse the following URL:
    http://www.gnu.org/copyleft/gpl.html
*/



import java.util.*;

/**
 * Information beyond the fundamentals/basics for mathematical symbols.
 * Aspects that may be different in different proofs, e.g. choices of
 * which symbols are used for implication.
 * @author Hugh McGuire
 */
    // "Expressions_Management" appeared inconveniently long
    // when listing files.
class Expressions_Mgmt implements java.io.Serializable {

    // NEED TO HANDLE THIS ISSUE BETTER
    private boolean use_tilde_for_not;
    private boolean use_prime_for_not;
    private boolean start_N_at_1;
    private Symbol.Specifier logical_negation_sym_spec = Symbol.Specifier.NOT;
    //private boolean nonneg_int_vars;

    		// was |TreeSet| so |get_identifiers()| would
		// present identifiers alphabetically; but
		// I'm no longer seeing use of |get_identifiers()|
    private final TreeSet<String> identifiers = new TreeSet<String>();
    private final HashSet<String> variables = new HashSet<String>();
    private final HashSet<String> skolem_ids = new HashSet<String>();
    private final HashSet<String> identifiers_appearing_without_args
    				// identifiers_appearing_sometimes_without_args
	= new HashSet<String>();

    // NEED TO CHANGE THE FOLLOWING NON-FUNDAMENTAL |static|S
    // TO A FIELD IN |Symbols_Info| (OR CONSIDERED IN |class PB_TableModel|)
    // FOR PURPOSES SUCH AS SAVING;
    // THEN AS NECESSARY METHODS HERE WOULD TAKE A |Symbols_Info| AS AN ARG.
    private EnumMap<Symbol.Specifier,String> spec_String_map;

    private EnumSet<Symbol.Specifier> user_spec_String_set;

    private int user_uppercase, user_lowercase, user_ascii, user_unicode,
	user_one_bar_imp_eqv, user_two_bars_imp_eqv;


    final static String ERR_POSNS_SEP = "@";
    // Rem. |String.split(String regex, int limit);|

    static String fmt_illargexc_msg(
            int selection_start, int selection_end,
            String message
            )
        {
        return
            selection_start + ERR_POSNS_SEP + selection_end + ERR_POSNS_SEP
            + message;
        }


    /* INT and IDENTIFIER don't 'morph' to any particular forms; they're
     * just always whatever.  (Like the squiggle in "The Dot and the Line"? ;-)
     */
    static boolean affects_presentation(Symbol symbol) {
	return  symbol.is_quantifier()  ||  symbol.spec_id_arg_boolean();
	}

    private void note_user_spec_String(Symbol symbol) {
        if ( user_spec_String_set != null
                &&  !user_spec_String_set.contains(symbol.get_specifier())
                )
            {
            spec_String_map.put(symbol.get_specifier(), symbol.get_text());
            user_spec_String_set.add(symbol.get_specifier());
            }
        }

    void prep_for_user_to_spec_Strings() {
        user_spec_String_set = EnumSet.noneOf(Symbol.Specifier.class);
        }

    void complete_spec_String_map() {
        boolean
            pref_unicode = false,
            pref_ascii = false,
            pref_lowercase = false,
            pref_uppercase = false;
        if ( user_unicode >= user_uppercase
                &&  user_unicode >= user_lowercase
                &&  user_unicode >= user_ascii
                )
            pref_unicode = true;
        else if ( user_ascii >= user_uppercase  &&  user_ascii >= user_lowercase
                )
            pref_ascii = true;
        else if ( user_lowercase >= user_uppercase )
            pref_lowercase = true;
        else
            pref_uppercase = true;

        //spec_String_map.put(Symbol.Specifier.ENDMARKER, "");
        if ( !user_spec_String_set.contains(Symbol.Specifier.FORALL) )
            spec_String_map.put(
                Symbol.Specifier.FORALL,
                pref_unicode
                    ? Character.toString(Symbol.FORALL_UNICODE)
                    : pref_lowercase
                        ? Symbol.Specifier.FORALL.toString().toLowerCase()
                        : Symbol.Specifier.FORALL.toString()
                );
        if ( !user_spec_String_set.contains(Symbol.Specifier.EXISTS) )
            spec_String_map.put(
                Symbol.Specifier.EXISTS,
                pref_unicode
                    ? Character.toString(Symbol.EXISTS_UNICODE)
                    : pref_lowercase
                        ? Symbol.Specifier.EXISTS.toString().toLowerCase()
                        : Symbol.Specifier.EXISTS.toString()
                );
        spec_String_map.put(Symbol.Specifier.COMMA, ",");
        spec_String_map.put(Symbol.Specifier.SUCH_THAT, ":");
	/*
        spec_String_map.put(
		Symbol.Specifier.BECOMES,
		Symbol.COLON_EQUALS_ASCII
		);
	*/
        spec_String_map.put(Symbol.Specifier.IS, "is");
        if ( !user_spec_String_set.contains(Symbol.Specifier.EQUIV) )
            spec_String_map.put(
                Symbol.Specifier.EQUIV,
                pref_unicode
		    ? Character.toString(
			    user_one_bar_imp_eqv > user_two_bars_imp_eqv
			    ?  Symbol.ARROW_LEFT_RIGHT_ONE_BAR_UNICODE
			    :  Symbol.ARROW_LEFT_RIGHT_TWO_BARS_UNICODE
			    )
                    : pref_ascii
                        ? (user_one_bar_imp_eqv > user_two_bars_imp_eqv
			    ?  Symbol.ARROW_LEFT_RIGHT_ONE_BAR_ASCII
			    :  Symbol.ARROW_LEFT_RIGHT_TWO_BARS_ASCII
			    )
                        : pref_lowercase
                            ? Symbol.Specifier.EQUIV.toString().toLowerCase()
                            : Symbol.Specifier.EQUIV.toString()
                );
        if ( !user_spec_String_set.contains(Symbol.Specifier.IMPLIES) )
            spec_String_map.put(
                Symbol.Specifier.IMPLIES,
                pref_unicode
		    ? Character.toString(
			    user_one_bar_imp_eqv > user_two_bars_imp_eqv
			    ?  Symbol.ARROW_RIGHT_ONE_BAR_UNICODE
			    :  Symbol.ARROW_RIGHT_TWO_BARS_UNICODE
			    )
                    : pref_ascii
                        ? (user_one_bar_imp_eqv > user_two_bars_imp_eqv
			    ?  Symbol.ARROW_RIGHT_ONE_BAR_ASCII
			    :  Symbol.ARROW_RIGHT_TWO_BARS_ASCII
			    )
                        : pref_lowercase
                            ? Symbol.Specifier.IMPLIES.toString().toLowerCase()
                            : Symbol.Specifier.IMPLIES.toString()
                );
        spec_String_map.put(
		Symbol.Specifier.SUM,
		Character.toString(Symbol.SUM_UNICODE)
		);
        spec_String_map.put(
		Symbol.Specifier.PROD,
		Character.toString(Symbol.PROD_UNICODE)
		);
	spec_String_map.put(Symbol.Specifier.PMOD, Symbol.PMOD_);
        if ( !user_spec_String_set.contains(Symbol.Specifier.OR) )
            spec_String_map.put(
                Symbol.Specifier.OR,
                pref_unicode
                    ? Character.toString(Symbol.OR_UNICODE)
                    : pref_ascii
                        ? Symbol.OR_ASCII
                        : pref_lowercase
                            ? Symbol.Specifier.OR.toString().toLowerCase()
                            : Symbol.Specifier.OR.toString()
                );
        if ( !user_spec_String_set.contains(Symbol.Specifier.AND) )
            spec_String_map.put(
                Symbol.Specifier.AND,
                pref_unicode
                    ? Character.toString(Symbol.AND_UNICODE)
                    : pref_ascii
                        ? Symbol.AND_ASCII
                        : pref_lowercase
                            ? Symbol.Specifier.AND.toString().toLowerCase()
                            : Symbol.Specifier.AND.toString()
                );
        if ( !user_spec_String_set.contains(Symbol.Specifier.QUANT_SEP) )
            spec_String_map.put(
		    Symbol.Specifier.QUANT_SEP,
		    Character.toString(Symbol.THIN_SPACE_UNICODE)
		    );
        if ( !user_spec_String_set.contains(Symbol.Specifier.SUBST) )
            spec_String_map.put(Symbol.Specifier.SUBST, "@");
        spec_String_map.put(Symbol.Specifier.CONGRUENT,
			    Character.toString(Symbol.THREE_BAR_UNICODE)
			    );
        spec_String_map.put(Symbol.Specifier.EQUALS, "=");
        spec_String_map.put(Symbol.Specifier.NEQ,
			    Character.toString(Symbol.NEQ_UNICODE)
			    );
        spec_String_map.put(Symbol.Specifier.LEQ,
			    Character.toString(Symbol.LEQ_UNICODE)
			    );
        spec_String_map.put(Symbol.Specifier.GEQ,
			    Character.toString(Symbol.GEQ_UNICODE)
			    );
        spec_String_map.put(Symbol.Specifier.LESS_THAN, "<");
        spec_String_map.put(Symbol.Specifier.GREATER_THAN, ">");
        if ( !user_spec_String_set.contains(Symbol.Specifier.DIVIDES) )
            spec_String_map.put(Symbol.Specifier.DIVIDES, "|");
        spec_String_map.put(Symbol.Specifier.BMOD, "mod");
        spec_String_map.put(Symbol.Specifier.REMAINDER_CODE, "%");
        spec_String_map.put(Symbol.Specifier.PLUS, "+");
        spec_String_map.put(Symbol.Specifier.MINUS, "-");
        if ( !user_spec_String_set.contains(Symbol.Specifier.TIMES) )
            spec_String_map.put(Symbol.Specifier.TIMES, "");
        spec_String_map.put(Symbol.Specifier.QUOTIENT, "/");
        if ( !user_spec_String_set.contains(Symbol.Specifier.EXP) )
            spec_String_map.put(Symbol.Specifier.EXP, "^");
        spec_String_map.put(Symbol.Specifier.FACTORIAL, "!");
        if ( !user_spec_String_set.contains(Symbol.Specifier.PRIME) )
            spec_String_map.put(
		    Symbol.Specifier.PRIME,
		    Character.toString(Symbol.PRIME_UNICODE)
		    );
	spec_String_map.put(
		Symbol.Specifier.TILDE,
		Character.toString(Symbol.TILDE_ASCII)
		);
        spec_String_map.put(Symbol.Specifier.NEGATIVE, "-");
        spec_String_map.put(Symbol.Specifier.LN, "ln");
        spec_String_map.put(Symbol.Specifier.LOG10, "log10");
        spec_String_map.put(Symbol.Specifier.LG, "lg");
        spec_String_map.put(Symbol.Specifier.LOG, "log");
        spec_String_map.put(Symbol.Specifier.LOG_, "log_");
        if ( !user_spec_String_set.contains(Symbol.Specifier.NOT) )
            spec_String_map.put(
                Symbol.Specifier.NOT,
                pref_uppercase
                    ? Symbol.Specifier.NOT.toString()
                    : pref_lowercase
                        ? Symbol.Specifier.NOT.toString().toLowerCase()
                        /*      // discourage |NOT_ASCII|
                        : pref_ascii
                            ? NOT_ASCII
                            */
                            : Character.toString(Symbol.NOT_UNICODE)
                );
        spec_String_map.put(Symbol.Specifier.INFINITY,
			    Character.toString(Symbol.INFINITY_UNICODE)
			    );
        if ( !user_spec_String_set.contains(Symbol.Specifier.TRUE) )
            spec_String_map.put(
                Symbol.Specifier.TRUE,
                user_uppercase > user_lowercase
                    ? Symbol.Specifier.TRUE.toString()
                    : Symbol.Specifier.TRUE.toString().toLowerCase()
                );
        if ( !user_spec_String_set.contains(Symbol.Specifier.FALSE) )
            spec_String_map.put(
                Symbol.Specifier.FALSE,
                user_lowercase >= user_uppercase
                    ? Symbol.Specifier.FALSE.toString().toLowerCase()
                    : Symbol.Specifier.FALSE.toString()
                );
        }

    boolean is_id_being_used(String id) { return  identifiers.contains(id); }

    //String get_identifiers() { return  identifiers.toString(); }

    void add_identifier(String id) { identifiers.add(id); }

    void expunge_identifier(String id) { identifiers.remove(id); }

    //void clear_identifiers() { identifiers.clear(); }


    void add_skolem_id(String s) {
        add_identifier(s);
        skolem_ids.add(s);
        }

    boolean is_skolem_id(String id) { return  skolem_ids.contains(id); }

    boolean is_variable_id(String id) { return  variables.contains(id); }

    void add_variable_id(String v) {
        add_identifier(v);
        variables.add(v);
        }

	    // forget_variable
    void expunge_variable_id(String v) {
        expunge_identifier(v);
        variables.remove(v);
        }

    boolean is_variable(Expression expr) {
        return  
            expr.op_spec_equals(Symbol.Specifier.IDENTIFIER)
            &&  is_variable_id(expr.get_operator().get_text())
            &&  expr.get_argument1() == null
            &&  expr.get_argument2() == null;
        }

    /*
    // NEED TO HANDLE THIS MORE PROPERLY
    static ArrayList<Expression> constant_terms = new ArrayList<Expression>();
    static ArrayList<String> constant_terms_texts = new ArrayList<String>();
    */

    /*
    Symbols_Info(boolean quiet) {
	if ( !quiet )
	    System.out.print("checking for preferences...");
	try {
	    java.util.Scanner prefs_scanner =
		new java.util.Scanner(new java.io.File("PBprefs.txt"));
	    if ( !quiet )
		System.out.print(" handling preferences...");
	    while ( prefs_scanner.hasNextLine() ) {
		String preference = prefs_scanner.nextLine();
		Expression.use_prime_for_not |=
		    preference.equalsIgnoreCase("useprimefornot");
		table_model.hilbert_style |=
		    preference.equalsIgnoreCase("hilbertstyle");
		}
	    }
	catch ( java.io.FileNotFoundException filenotfoundexception ) {
	    // in this case do nothing
	    }
	if ( !quiet )
	    System.out.println("\nfinished checking preferences\n");
	}
    */

    public Expressions_Mgmt(String preferences_lc) {
	assert
	    preferences_lc.equals(preferences_lc.toLowerCase())
	    : "preferences_lc.equals(preferences_lc.toLowerCase())";
	use_tilde_for_not |= preferences_lc.contains("usetildefornot");
	use_prime_for_not |= preferences_lc.contains("useprimefornot");
	start_N_at_1 |= preferences_lc.contains("startnat1");

	spec_String_map =
	    new EnumMap<Symbol.Specifier,String>(Symbol.Specifier.class);
	spec_String_map.put(Symbol.Specifier.ENDMARKER, "");
	spec_String_map.put(
		Symbol.Specifier.FORALL,
		Character.toString(Symbol.FORALL_UNICODE)
		);
	spec_String_map.put(
		Symbol.Specifier.EXISTS,
		Character.toString(Symbol.EXISTS_UNICODE)
		);
	spec_String_map.put(Symbol.Specifier.SUM,
			    Character.toString(Symbol.SUM_UNICODE)
			    );
	spec_String_map.put(Symbol.Specifier.PROD,
			    Character.toString(Symbol.PROD_UNICODE)
			    );
	spec_String_map.put(Symbol.Specifier.PMOD, Symbol.PMOD_);
	spec_String_map.put(
		Symbol.Specifier.EQUIV,
		Character.toString(Symbol.ARROW_LEFT_RIGHT_TWO_BARS_UNICODE)
		);
	spec_String_map.put(
		Symbol.Specifier.IMPLIES,
		Character.toString(Symbol.ARROW_RIGHT_TWO_BARS_UNICODE)
		);
	spec_String_map.put(Symbol.Specifier.OR,
			    Character.toString(Symbol.OR_UNICODE)
			    );
	spec_String_map.put(Symbol.Specifier.AND,
			    Character.toString(Symbol.AND_UNICODE)
			    );
	spec_String_map.put(
		Symbol.Specifier.QUANT_SEP,
		Character.toString(Symbol.THIN_SPACE_UNICODE)
		);
	spec_String_map.put(Symbol.Specifier.SUBST, "@");
	/*
	spec_String_map.put(
	    Symbol.Specifier.EQUALS_DEF,
	    Character.toString(Symbol.EQUALS_DEF_UNICODE)
	    );
	*/
	/*
        spec_String_map.put(Symbol.Specifier.CONGRUENT,
			    Character.toString(Symbol.THREE_BAR_UNICODE)
			    );
	*/
	spec_String_map.put(Symbol.Specifier.EQUALS, "=");
	spec_String_map.put(Symbol.Specifier.NEQ,
			    Character.toString(Symbol.NEQ_UNICODE)
			    );
	spec_String_map.put(Symbol.Specifier.LEQ,
			    Character.toString(Symbol.LEQ_UNICODE)
			    );
	spec_String_map.put(Symbol.Specifier.GEQ,
			    Character.toString(Symbol.GEQ_UNICODE)
			    );
	spec_String_map.put(Symbol.Specifier.LESS_THAN, "<");
	spec_String_map.put(Symbol.Specifier.GREATER_THAN, ">");
	spec_String_map.put(Symbol.Specifier.DIVIDES, "|");
	spec_String_map.put(Symbol.Specifier.COMMA, ",");
	spec_String_map.put(Symbol.Specifier.SUCH_THAT, ":");
	spec_String_map.put(Symbol.Specifier.BMOD, "mod");
        spec_String_map.put(Symbol.Specifier.REMAINDER_CODE, "%");
	spec_String_map.put(Symbol.Specifier.PLUS, "+");
	spec_String_map.put(Symbol.Specifier.MINUS, "-");
	spec_String_map.put(Symbol.Specifier.TIMES, "");
	spec_String_map.put(Symbol.Specifier.QUOTIENT, "/");
	spec_String_map.put(
		Symbol.Specifier.GROUP_OP,
		Character.toString(Symbol.GROUP_OP_ASCII)
		    // the Unicode one appears terrible
		);
	spec_String_map.put(Symbol.Specifier.EXP, "^");
	spec_String_map.put(
		Symbol.Specifier.PRIME,
		Character.toString(Symbol.PRIME_UNICODE)
		);
	spec_String_map.put(Symbol.Specifier.COMPLEMENT_POST,
			    Character.toString(Symbol.SUPERSCRIPT_MINUS_UNICODE)
			    );
	spec_String_map.put(
		Symbol.Specifier.TILDE,
		Character.toString(Symbol.TILDE_ASCII)
		);
	spec_String_map.put(Symbol.Specifier.NEGATIVE, "-");
	spec_String_map.put(Symbol.Specifier.LN, "ln");
	spec_String_map.put(Symbol.Specifier.LOG10, "log10");
	spec_String_map.put(Symbol.Specifier.LG, "lg");
	spec_String_map.put(Symbol.Specifier.LOG, "log");
	spec_String_map.put(Symbol.Specifier.LOG_, "log_");
	spec_String_map.put(Symbol.Specifier.NOT,
			    Character.toString(Symbol.NOT_UNICODE)
			    );
	spec_String_map.put(Symbol.Specifier.INFINITY,
			    Character.toString(Symbol.INFINITY_UNICODE)
			    );
	spec_String_map.put(
		Symbol.Specifier.TRUE,
		Symbol.Specifier.TRUE.toString().toLowerCase()
		);
	spec_String_map.put(
		Symbol.Specifier.FALSE,
		Symbol.Specifier.FALSE.toString().toLowerCase()
		);

	prep_for_user_to_spec_Strings();	// originally done only in
						// |User_Entry.get_theorem()|
	}

    String get_spec_String(Symbol.Specifier specifier) {
	return  spec_String_map.get(specifier);
	}

    // macro
    Symbol new_Symbol(Symbol.Specifier specifier) {
	return  new Symbol(specifier, get_spec_String(specifier));
	}

    boolean get_usetildefornot() { return  use_tilde_for_not; }

    boolean get_useprimefornot() { return  use_prime_for_not; }

    boolean get_startNat1() { return  start_N_at_1; }

    Symbol.Specifier get_lognegsymspec() { return  logical_negation_sym_spec; }

    boolean note_usetildefornot() {
	logical_negation_sym_spec = Symbol.Specifier.TILDE;
	return  use_tilde_for_not = true;
	}

    boolean note_useprimefornot() {
	logical_negation_sym_spec = Symbol.Specifier.PRIME;
	return  use_prime_for_not = true;
	}

    boolean note_startNat1() { return  start_N_at_1 = true; }

    boolean consider_usingtildefornot(Expression expr) {
	return
	    !using_not(expr)
	    &&  (using_tilde_for_not(expr)
		    ||  expr.ungrp_op_spec_equals(Symbol.Specifier.TILDE)
		    )
	    &&  note_usetildefornot();
	}

    boolean consider_usingprimefornot(Expression expr) {
	return
	    !using_not(expr)
	    &&  (using_prime_for_not(expr)
		    ||  expr.ungrp_op_spec_equals(Symbol.Specifier.PRIME)
		    )
	    &&  note_useprimefornot();
	}

    boolean using_not(Expression expr) {
	return
	    expr != null
	    && (expr.op_spec_equals(Symbol.Specifier.NOT)
		|| using_not(expr.get_argument1())
		|| using_not(expr.get_argument2())
		);
	}

    boolean using_tilde_for_not(Expression expr) {
	return
	    expr != null
	    && (expr.op_spec_equals(Symbol.Specifier.TILDE)
		    && expr.get_argument1().ungroup().get_operator()
			    .spec_boolean()
		|| expr.get_operator().spec_boolean()
		    &&  (expr.get_argument1().ungrp_op_spec_equals(
				Symbol.Specifier.TILDE
				)
			    ||  expr.get_argument2() != null
				&&  expr.get_argument2()
					    .ungrp_op_spec_equals(
						Symbol.Specifier.TILDE
						)
			    )
		|| using_tilde_for_not(expr.get_argument1())
		|| using_tilde_for_not(expr.get_argument2())
		);
	}

    boolean using_prime_for_not(Expression expr) {
	return
	    expr != null
	    && (expr.op_spec_equals(Symbol.Specifier.PRIME)
		    && expr.get_argument1().ungroup().get_operator()
			    .spec_boolean()
		|| expr.get_operator().spec_boolean()
		    &&  (expr.get_argument1().ungrp_op_spec_equals(
				Symbol.Specifier.PRIME
				)
			    ||  expr.get_argument2() != null
				&&  expr.get_argument2()
					    .ungrp_op_spec_equals(
						Symbol.Specifier.PRIME
						)
			    )
		|| using_prime_for_not(expr.get_argument1())
		|| using_prime_for_not(expr.get_argument2())
		);
	}

    //void assume_nonneg_int_vars() { nonneg_int_vars = true; }

    //boolean get_nonnegintvars() { return  nonneg_int_vars; }

    // C++ |pair<String,Expression>|
    static class Variable_Binding_to_Expression {
	final String variable;
	Expression expression;

	public Variable_Binding_to_Expression(
		String variable_given,
		Expression expression_given
		)
	    {
	    variable = variable_given;
	    // Do NOT |expression_given.clone()| so continuing unifying
	    // will affect expression(s) here
	    expression = expression_given;
	    }

	/*
	public String toString() {
	    return  variable + " := " + expression.gen_text();
	    }
	*/
	}

    LinkedList<Variable_Binding_to_Expression> unify(
	    Expression expr1,
	    Expression other,
	    Expression root,
	    Expression other_root,
	    Collection<String> nonfree_vars
	    )
	{
	LinkedList<Variable_Binding_to_Expression> accumulator =
	    new LinkedList<Variable_Binding_to_Expression>();
	LinkedList<Variable_Binding_to_Expression> result =
	    unify(accumulator, expr1, other, root, other_root, nonfree_vars);
	if ( result != null )
	    for ( Variable_Binding_to_Expression vbe : result ) {
		vbe.expression.clear_excessive_basic_grps_internal();
		vbe.expression = vbe.expression.ungroup();
		}
	return  result;
	}

    LinkedList<Variable_Binding_to_Expression> unify(
	    Expression expr1,
	    Expression other,
	    Expression root,
	    Expression other_root
	    )
	{
	return  unify(expr1, other, root, other_root, null);
	}

    /**
     * prefers assigning to variables of |expr1| (object for which invoked)
     * rather than |other|
     * @return |null| if ununifiable, otherwise the unifying substitutions
     */
    // I THINK I HAVEN'T ADDRESSED CAPTURING
    LinkedList<Variable_Binding_to_Expression> unify(
	    LinkedList<Variable_Binding_to_Expression> accumulator,
	    Expression expr1,
	    Expression other,
	    Expression root,
	    Expression other_root,
	    Collection<String> nonfree_vars
	    )
	{
        /*
        if ( other == null )
            return  null;
        */
        if ( expr1.equivalent_form(other) )   // expensive
            return  accumulator;
        if ( expr1.is_group() )
            return  unify(accumulator, expr1.get_argument1(), other, root, other_root, nonfree_vars);
        if ( other.is_group() )
            return  unify(accumulator, expr1, other.get_argument1(), root, other_root, nonfree_vars);
        if ( !expr1.get_operator().equivalent_form(other.get_operator()) ) {
            String op_text = expr1.get_operator().get_text();
            String other_op_text = other.get_operator().get_text();
            if ( is_variable(expr1)
		    &&  (nonfree_vars == null
			    ||  !nonfree_vars.contains(op_text)
			    )
			// here is "occurs" check which avoids self-inclusion
			// (or ~~infinite replacement):
                    &&  !variables_unquantified(other).contains(op_text)
                    )
                {
		Expression replacement = other.ensure_group();
		accumulator.add(
			new Variable_Binding_to_Expression(
				op_text,
				other.get_operator().is_binary_infix()
				    ? replacement
				    : other
				)
			);
		// replacing will affect expressions in |accumulator|
                root.replace_throughout_scope(op_text, replacement);
                other_root.replace_throughout_scope(op_text, replacement);
		return  accumulator;
                }
            if ( is_variable(other)
			// here is "occurs" check which avoids self-inclusion
			// (or ~~infinite replacement):
		    &&  (nonfree_vars == null
			    ||  !nonfree_vars.contains(other_op_text)
			    )
		    &&  !variables_unquantified(expr1).contains(other_op_text)
		    )
                {
		Expression replacement = expr1.ensure_group();
		accumulator.add(
			new Variable_Binding_to_Expression(
				other_op_text,
				expr1.get_operator().is_binary_infix()
				    ? replacement
				    : expr1
				)
			);
		// replacing will affect expressions in |accumulator|
                root.replace_throughout_scope(other_op_text, replacement);
                other_root.replace_throughout_scope(other_op_text, replacement);
		return  accumulator;
                }
	    return  null;
            }
        if ( expr1.get_argument1() == null ) {
            if ( other.get_argument1() != null )
                return  null;
            }
        else {
            if ( other.get_argument1() == null )
                return  null;
            if ( unify(accumulator, expr1.get_argument1(), other.get_argument1(), root, other_root, nonfree_vars)
		    == null
		    )
                return  null;
            }
        if ( expr1.get_argument2() == null ) {
            if ( other.get_argument2() != null )
                return  null;
            }
        else {
            if ( other.get_argument2() == null )
                return  null;
            if ( unify(accumulator, expr1.get_argument2(), other.get_argument2(), root, other_root, nonfree_vars)
		    == null
		    )
                return  null;
            }
        return  accumulator;
        }

	// consider |TreeSet| so |toString()|
	// (used implicitly in |User_Entry.java|)
	// would present identifiers alphabetically
    HashSet<String> variables_unquantified(Expression expr) {
        HashSet<String> result = new HashSet<String>();
        String op_text = expr.get_operator().get_text();
        if ( variables.contains(op_text) )
            result.add(op_text);
        HashSet<String> arg1_vars =
            expr.get_argument1() == null
            ? new HashSet<String>()
            : variables_unquantified(expr.get_argument1());
        if ( expr.get_argument2() != null )
            result = variables_unquantified(expr.get_argument2());
        if ( expr.op_spec_equals(Symbol.Specifier.QUANT_SEP) )
            result.removeAll(arg1_vars);
        else
            result.addAll(arg1_vars);
        return  result;
        }

    void analyze_quant_vars(Expression expr, Set<String> new_ids) {
        if ( expr.op_spec_equals(Symbol.Specifier.COMMA) ) {
            analyze_quant_vars(expr.get_argument1(), new_ids);
            analyze_quant_vars(expr.get_argument2(), new_ids);
            }
        else if ( expr.get_operator().is_relation()
		    &&  !expr.get_argument1().get_operator().is_relation()
		)
            analyze_quant_vars(expr.get_argument1(), new_ids);
        else {
            String op_text = expr.get_operator().get_text();
            if ( !expr.op_spec_equals(Symbol.Specifier.IDENTIFIER)
                    ||  expr.get_argument1() != null
                    ||  expr.get_argument2() != null
                    )
                throw new IllegalArgumentException(
                    fmt_illargexc_msg(
                        expr.get_begin(),
                        expr.get_limit(),
                        "quantifier needs to be applied to variables"
                            + "\n(separated by commas)"
                            + "\nbut you have \""
                            + op_text
                            + "\" ("
                            + expr.get_operator().get_specifier()
                            + ')'
                            + (expr.get_argument1() != null
				    ||  expr.get_argument2() != null
                                ? " applied to argument(s)"
                                : ""
                                )
                        )
                    );
	    if ( new_ids.contains(op_text) || !is_id_being_used(op_text) )
		add_variable_id(op_text);
	    else if ( !is_variable_id(op_text) )
                throw new IllegalArgumentException(
                    fmt_illargexc_msg(
                        expr.get_begin(),
                        expr.get_limit(),
			"You can't use this symbol \""
			    + op_text
			    + "\" as a variable"
			    + " because it's being used already in this proof"
			    + "\nas a constant."
                        )
                    );
            }
        }

    boolean constant_term(Expression expr) {
	if ( expr.op_spec_equals(Symbol.Specifier.OPENING_DELIMITER)
		&&  !expr.get_operator().get_text().equalsIgnoreCase("IF")
		)
	    return  constant_term(expr.get_argument1());
	if ( !(expr.get_operator().spec_domainval()
		    || expr.op_spec_equals(Symbol.Specifier.IDENTIFIER)
		    )
		)
	    return  false;
	if ( expr.op_spec_equals(Symbol.Specifier.IDENTIFIER) )
	    if ( is_variable_id(expr.get_operator().get_text()) )
		return  false;
	assert
	    // (expr.get_argument1() == null  ==>  expr.get_argument2() == null)
	    expr.get_argument1() != null  ||  expr.get_argument2() == null
	    :  "expr.get_argument1() != null  ||  expr.get_argument2() == null";
	if ( expr.get_argument1() == null )
	    return  true;
	if ( expr.get_argument2() != null
		&&  !constant_term(expr.get_argument2())
		)
	    return  false;
	return  constant_term(expr.get_argument1());
	}

    // Enable viewing parser information:
    private static LinkedList<Symbol> parse_input_symbols_given;
    private static Stack<Grammar_Construct> parse_results;
    public static String get_parse_input_symbols_given() {
	String result = "";
        for ( Symbol item : parse_input_symbols_given ) {
	    String item_text = item.get_text();
            result +=
		"["
		+ item.get_specifier()
		+ " \""
		+ (item_text.equals("\n") ? "\\n" : item_text)
		+ "\"  @"
		+ item.get_begin()
		+ "]\n";
	    }
	return  result;
	}
    public static Stack<Grammar_Construct> get_parse_results() {
	return  parse_results;
	}

    /**
     * @return  -1 if none
     */
    private int index_topmost_noncomment(Stack<Grammar_Construct> gc_stack) {
	for ( ListIterator<Grammar_Construct> gc_stack_it =
		    gc_stack.listIterator(gc_stack.size());
		gc_stack_it.hasPrevious();
		)
	    {
	    Grammar_Construct gc = gc_stack_it.previous();
	    if ( gc.getClass() != Symbol.class
		    ||  ((Symbol) gc).get_specifier()
			!= Symbol.Specifier.COMMENT
		    )
		return  gc_stack_it.nextIndex();
	    }
	return  -1;
	}

    // I wonder whether this discarding is good:
    // (I did this to avoid the hassle of trying to retain
    // comments inside expressions.)
    private Grammar_Construct pop_discarding_comments(
	    Stack<Grammar_Construct> gc_stack
	    )
	{
	/* removeRange(int,int) has protected access in java.util.Vector
	gc_stack.removeRange(
		index_topmost_noncomment(gc_stack) + 1,
		gc_stack.size()
		);
	*/
	gc_stack.setSize(index_topmost_noncomment(gc_stack) + 1);
	return  gc_stack.pop();
	}

    // This is not |const| (see C++): it changes state of |Expressions_Mgmt|.
    // Checking further constraints here so code invoking this won't have
    // to restore |Expressions_Mgmt| if a constraint isn't met; also,
    // the constraints generally involve things managed here anyway,
    // e.g. |constant_term()|.
	// using |Vector<>| instead of say |ArrayList<>|
	// because parsing using |Stack<>| and |Stack<> extends Vector<>|
    //@SuppressWarnings("unchecked")	//(TreeSet<String>) identifiers.clone();
    Vector<Grammar_Construct> parse_and_further_constrain(
	    final String text0,
		// |final| ensures programmer doesn't
		// accidentally change this, since it's
		// needed for error messages
	    // and_further_constraints:
	    final boolean allowing_free_variables,
	    final boolean accepting_multiple_exprs,
	    final boolean seeking_constant_term,
	    final Expression desired_smply_eq_orig,
	    final String desired_smply_eq_text
	    )
        {
        if ( text0 == null )
            throw new IllegalArgumentException(
                fmt_illargexc_msg(0, 0, "text is null")
                );
        parse_input_symbols_given = new LinkedList<Symbol>();
			// identifiers_apparently
	ArrayList<String> identifiers_atfirstglance =
	    new ArrayList<String>(identifiers);
	HashSet<Symbol> broken_infix_bin_ops = new HashSet<Symbol>();
	Symbol prev_symbol = null;
	    // SHOULD CHANGE TO AVOID |prev_symbol| HERE
	    // PROBABLY BY DOING POST-LEXING PROCESSING
	    // OF SEQUENCE OF SYMBOLS
	    // not 'enhanced' |for| because need |input_position|
        for ( int input_position = 0; input_position < text0.length(); ) {
	    if ( text0.charAt(input_position) == '.' ) {
		int ip;
		for ( ip = input_position + 1;
			ip < text0.length()
			    &&  Character.isWhitespace(text0.charAt(ip));
			ip++
			)
		    ;
		if ( ip >= text0.length() )
		    break;
		}
	    if ( text0.startsWith(Symbol.UNUSED_NOTE, input_position) ) {
		input_position += Symbol.UNUSED_NOTE.length();
		continue;
		}
            if ( Character.isWhitespace(text0.charAt(input_position))
		    &&  text0.charAt(input_position) != '\n'
		    &&  text0.charAt(input_position)
			!= Symbol.THIN_SPACE_UNICODE
		    )
		{
                input_position++;
                continue;
                }
	    Symbol symbol;
	    try {
				// SHOULD CHANGE TO AVOID |prev_symbol| HERE
				// PROBABLY BY DOING POST-LEXING PROCESSING
				// OF SEQUENCE OF SYMBOLS
		symbol = new Symbol(text0, input_position, prev_symbol);
		}
	    catch ( IllegalArgumentException iae ) {
	    		// Should I not use |IllegalArgumentException|
			// as part of the processing?
		throw new IllegalArgumentException(
		    fmt_illargexc_msg(
			input_position,
			input_position,
			iae.getMessage()
			)
		    );
		}
            input_position = symbol.get_limit();
            parse_input_symbols_given.add(symbol);
	    if ( symbol.get_specifier() == Symbol.Specifier.IDENTIFIER )
		identifiers_atfirstglance.add(symbol.get_text());
	    note_user_spec_String(symbol);	// Silly for INT,ID,...
						// but so what?
	    prev_symbol = symbol;
            }
        if ( parse_input_symbols_given.isEmpty() )
            throw new IllegalArgumentException(
                fmt_illargexc_msg(
                    0,
                    text0.length(),
                    "no symbols found in input text"
                    )
                );

	/*
        // debugging:
        System.err.println("\nbefore messing, parse_input_symbols_given:");
        for ( Symbol item : parse_input_symbols_given )
            System.err.println(
                item + " :  " + item.get_specifier()
                + "  \"" + item.get_text() + '"'
                + "  @" + item.get_begin()
                );
	*/

	// Split adjacency products of identifiers.
	// Limiting to products of just two identifiers known by being
	// used elsewhere; it's not so obvious what a user wants with
	// something like "xyz" (when might such be used?).
	// (Yes, I want to say "adjacency products".)
	// I'm keeping the record of all identifiers in this class
	// instead of in |Symbol| because such information is
	// beyond any one |Symbol|.
	// (An earlier version of |Symbol.java| had such a record
	// |static|, but that wasn't good considering issues
	// such as saving proofs.)
	Collections.sort(
	    identifiers_atfirstglance,
	    new Comparator<String>() {
		public int compare(String o1, String o2) {
		    return  o1.length() - o2.length();
		    }
		}
	    );
	for ( ListIterator<Symbol> input_symbols_it =
		    parse_input_symbols_given.listIterator();
		input_symbols_it.hasNext();
		)
	    {
	    Symbol input_symbol = input_symbols_it.next();
	    if ( input_symbol.get_specifier() == Symbol.Specifier.IDENTIFIER )
		for ( String id : identifiers_atfirstglance ) {
		    		// CONSIDER AVOIDING FUNCTIONS
		    if ( id.length() == input_symbol.get_text().length() )
			break;
		    if ( input_symbol.get_text().startsWith(id) ) {
			int il = id.length();
			String id2 = input_symbol.get_text().substring(il);
			if ( !identifiers_atfirstglance.contains(id2) )
			    continue;
			input_symbols_it.remove();
			int b = input_symbol.get_begin();
			input_symbols_it.add(
				new Symbol(Symbol.Specifier.IDENTIFIER, id, b)
				);
			// Still not inserting TIMES so symbols actually input
			// still distinguished from symbols parsing.
			input_symbols_it.add(
				new Symbol(Symbol.Specifier.IDENTIFIER,
					    id2,
					    b + il
					    )
				);
			break;
			}
		    // I think the following is unnecessary/redundant;
		    // so I really should comment this out:
		    if ( input_symbol.get_text().endsWith(id) ) {
			int ii = input_symbol.get_text().length() - id.length();
			String id1 = input_symbol.get_text().substring(0, ii);
			if ( !identifiers_atfirstglance.contains(id1) )
			    continue;
			input_symbols_it.remove();
			int b = input_symbol.get_begin();
			input_symbols_it.add(
				new Symbol(Symbol.Specifier.IDENTIFIER, id1, b)
				);
			// Still not inserting TIMES so symbols actually input
			// still distinguished from symbols parsing.
			input_symbols_it.add(
				new Symbol(
					Symbol.Specifier.IDENTIFIER,
					id,
					b + ii
					)
				);
			break;
			}
		    }
	    }

	/* Occasionally deviating from strict queue operations
        Queue<Symbol> parse_symbols =
	 */
	LinkedList<Symbol> parse_symbols =
	    new LinkedList<Symbol>(parse_input_symbols_given);

	// Insert |QUANT_SEP|s:
	// My syntax for a quantifier is restricted:
	// * no spaces (though I don't ensure this in half the places ;-/
	// * quantifier symbol (FORALL or EXISTS) followed by an IDENTIFIER,
	//   then pairs of either [COMMA followed by an IDENTIFIER]
	//   or [RELATION followed by any symbol].
	// Following the material fitting that pattern, there needs to be
	// a QUANT_SEP; except if what follows the pattern is
	// a closing parenthesis, then the QUANT_SEP actually follows that.
	for ( ListIterator<Symbol> parse_symbols_it =
		    parse_symbols.listIterator();
		parse_symbols_it.hasNext();
		)
	    {
	    Symbol parse_symbol = parse_symbols_it.next();
	    if ( parse_symbol.is_quantifier() ) {
		while ( parse_symbols_it.hasNext() ) {
		    parse_symbol = parse_symbols_it.next();
		    int prev_symbol_limit = parse_symbol.get_limit();
		    if ( !parse_symbols_it.hasNext() )
			break;
		    parse_symbol = parse_symbols_it.next();
		    if ( prev_symbol_limit < parse_symbol.get_begin()
			    ||  parse_symbol.get_specifier()
				    != Symbol.Specifier.COMMA
				&&  !parse_symbol.is_relation()
			    )
			break;
		    }
		if ( parse_symbol.get_specifier() == Symbol.Specifier.QUANT_SEP)
		    continue;
		if ( !parse_symbol.get_text().equals(")") )
		    parse_symbol = parse_symbols_it.previous();
		Symbol quant_sep =
		    new Symbol(Symbol.Specifier.QUANT_SEP,
				"",
				parse_symbol.get_limit()
				);
		note_user_spec_String(quant_sep);
		parse_symbols_it.add(quant_sep);
		}
	    }

	HashSet<String> new_identifiers = new HashSet<String>();

	// Further messing:
	prev_symbol = null;
	for ( ListIterator<Symbol> parse_symbols_it =
		    parse_symbols.listIterator();
		parse_symbols_it.hasNext();
		)
	    {
	    Symbol parse_symbol = parse_symbols_it.next();
	    if ( parse_symbol.get_specifier() == Symbol.Specifier.INT ) {
		try {
		    parse_symbol.get_val();
		    }
		catch ( NumberFormatException nfe ) {
		    throw new IllegalArgumentException(
			fmt_illargexc_msg(
			    parse_symbol.get_begin(),
			    parse_symbol.get_limit(),
			    "typed integer's magnitude exceeds this"
				+ "\nsystem's capabilities for handling such"
			    )
			);
		    }
		if ( parse_symbol.text_is_superscript() ) {
		    parse_symbols_it.previous();
		    parse_symbols_it.add(
			    new Symbol(Symbol.Specifier.EXP,
					    "",
					    parse_symbol.get_begin()
					    )
			);
		    parse_symbols_it.next();
		    }
		}
	    else if ( parse_symbol.get_specifier()
			== Symbol.Specifier.IDENTIFIER
			)
		{
		if ( !is_id_being_used(parse_symbol.get_text()) )
		    new_identifiers.add(parse_symbol.get_text());
		if ( text0.length() == parse_symbol.get_limit()
			||  text0.charAt(parse_symbol.get_limit()) != '('
			)
		    // should check not already identifier
		    identifiers_appearing_without_args.add(
			    parse_symbol.get_text()
			    );
		}
	    else if ( parse_symbol.get_specifier() == Symbol.Specifier.PMOD )
		parse_symbols_it.add(
			new Symbol(
				Symbol.Specifier.OPENING_DELIMITER,
				    // trans/phantom
				"",
				parse_symbol.get_limit()
				)
		    );
	    else if ( parse_symbol.get_text()
			    .equals(
				Character.toString(Symbol.THREE_BAR_UNICODE)
				)
			&&  user_spec_String_set.contains(Symbol.Specifier.PMOD)
			&&  parse_symbol.get_specifier()
			    // == Symbol.Specifier.EQUIV
			    != Symbol.Specifier.CONGRUENT
			)
		parse_symbols_it.set(
		    new Symbol(
			Symbol.Specifier.CONGRUENT,
			parse_symbol.get_text(),
			parse_symbol.get_begin()
			)
		    );
	    else if ( parse_symbol.get_specifier() == Symbol.Specifier.BREAK ) {
		Symbol symbol_following_break = null;
		    // Instead of having this additional loop here, trying to
		    // handle all the cases with |if| conditions here firing in
		    // different iterations of the main |parse_symbols_it| loop
		    // was difficult.
		while ( parse_symbols_it.hasNext()
			&&  (symbol_following_break = parse_symbols_it.next())
				.get_specifier()
			    == Symbol.Specifier.BREAK
			)
		    {
		    parse_symbols_it.remove();
		    symbol_following_break = null;
		    }
		if ( symbol_following_break != null ) {
		    parse_symbols_it.previous();
			// yields |symbol_following_break| again [Java API]
		    parse_symbols_it.previous();
			// back to |parse_symbol|: |BREAK|
		    parse_symbols_it.next();
			// same, |parse_symbol|: |BREAK| [Java API]
			// and now proper for continuing main loop
		    boolean
			break_symbol_following =
			    symbol_following_break.is_binary_infix()
				||  symbol_following_break.get_specifier()
				    == Symbol.Specifier.CLOSING_DELIMITER,
				    // kludge in case of use of a style I like;
				    // the effect desired here is removal
				    // of the BREAK, inclusion in
				    // |broken_infix_bin_ops| is irrelevant
			break_prev_symbol =
			    // !break_symbol_following  &&
			    prev_symbol != null
				&&  prev_symbol.is_binary_infix();
		    // If could break both, will break only symbol following
		    // because two binary infix operators in a row is erroneous
		    // so needn't try hard to handle such a case
		    // ('... COMMA THEN ...' would change
		    // to '... CLOSING_DELIM THEN ...'; it wouldn't hurt
		    // to add the |COMMA| symbol to |broken_infix_bin_ops|
		    // since it'll be removed(replaced) from |parse_symbols|,
		    // but that indicates that it's also unnecessary to do so)
		    if ( break_symbol_following || break_prev_symbol ) {
			broken_infix_bin_ops.add(
			    break_symbol_following
			    ? symbol_following_break
			    : prev_symbol
			    );
			parse_symbols_it.remove();  // |parse_symbol|: |BREAK|
			parse_symbol = prev_symbol; // need to do this to
						    // avoid interesting (;-)
						    // errors (say for
						    // '... COMMA BR THEN ...')
			}
		    }
		} 	// pedagogical note:
			// the code didn't work without grouping such as this
	    else if ( parse_symbol.get_specifier() == Symbol.Specifier.IMPLIES
			&&  parse_symbol.get_text().equalsIgnoreCase("THEN")
				// parse_symbols_it.hasPrevious()
			&&  prev_symbol != null
			    // if nothing preceded this "THEN",
			    // then input was bad so do nothing here
		    )
		{
		parse_symbols_it.previous();
		    // this initial same as |parse_symbol| [Java API]
		parse_symbols_it.previous();
		    // yields |prev_symbol|
		// At this point |parse_symbols_it.set()| would set
		// the list item corresponding to |prev_symbol|
		// but |add()| at this point would add in front of |prev_symbol|
		// so:
		parse_symbols_it.next();
		    // again yields |prev_symbol| [Java API]
		// And now |parse_symbols_it.set()| would set
		// the list item corresponding to |prev_symbol|
		// and |add()| at this point would add following |prev_symbol|.

		// Needn't worry about |BREAK| preceding "THEN" because
		// other code (above) removes |BREAK| preceding infix op. "THEN"
		if ( prev_symbol.get_specifier() == Symbol.Specifier.COMMA )
		    parse_symbols_it.set(
			new Symbol(Symbol.Specifier.CLOSING_DELIMITER,
				    prev_symbol.get_text(),	// ","
				    prev_symbol.get_begin()
				    )
			);
		else
		    parse_symbols_it.add(
			new Symbol(Symbol.Specifier.CLOSING_DELIMITER,
				    "",
				    prev_symbol.get_limit()
				    )
			);
		parse_symbols_it.next();
		    // back to |parse_symbol|: "THEN"
		}
	    if ( affects_presentation(parse_symbol) ) {
		if ( parse_symbol.text_is_uppercase_letters() )
		    user_uppercase++;
		else if ( parse_symbol.text_is_letters() )
		    user_lowercase++;
		else if ( parse_symbol.get_text().length() == 1
			    &&  !parse_symbol.text_is_ASCII()
			    )
		    user_unicode++;
		else if ( parse_symbol.get_text().length() > 1
			    &&  parse_symbol.text_is_ASCII()
			    )
		    user_ascii++;
		switch ( parse_symbol.get_specifier() ) {
		    case  IMPLIES:
		    case  EQUIV:
			if ( parse_symbol.get_text()
				    .equals(
					Symbol.ARROW_LEFT_RIGHT_ONE_BAR_ASCII
					)
				||  parse_symbol.get_text().equals(
					    Symbol.ARROW_RIGHT_ONE_BAR_ASCII
					    )
				||  parse_symbol.get_text().equals(
					    Symbol.ARROW_RIGHT_ONE_BAR_ASCII_
					    )
    				||  parse_symbol.get_text().length() == 1
				    && (parse_symbol.get_text().charAt(0)
					    == Symbol
						.ARROW_RIGHT_ONE_BAR_UNICODE
					||  parse_symbol.get_text().charAt(0)
					    ==
					    Symbol
					      .ARROW_LEFT_RIGHT_ONE_BAR_UNICODE
					)
				)
			    user_one_bar_imp_eqv++;
			else if ( parse_symbol.get_text()
				    .equals(
					Symbol.ARROW_LEFT_RIGHT_TWO_BARS_ASCII
					)
				||  parse_symbol.get_text().equals(
					    Symbol.ARROW_RIGHT_TWO_BARS_ASCII
					    )
				||  parse_symbol.get_text().equals(
					    Symbol.ARROW_RIGHT_TWO_BARS_ASCII_
					    )
    				||  parse_symbol.get_text().length() == 1
				    && (parse_symbol.get_text().charAt(0)
					    == Symbol
						.ARROW_RIGHT_TWO_BARS_UNICODE
					||  parse_symbol.get_text().charAt(0)
					    ==
					    Symbol
					      .ARROW_LEFT_RIGHT_TWO_BARS_UNICODE
					)
				)
			user_two_bars_imp_eqv++;
		    }
		}
	    prev_symbol = parse_symbol;
	    }

	// consider operator 'APPLICATION' for function, predicate
	//		? ID_APPLICATION ?

	// Next insert empty-string |TIMES|s:
	prev_symbol = parse_symbols.getFirst();
	for ( ListIterator<Symbol> parse_symbols_it =
		    parse_symbols.listIterator(1);
		parse_symbols_it.hasNext();
		)
	    {
	    Symbol parse_symbol = parse_symbols_it.next();
	    if ( prev_symbol.get_limit() == parse_symbol.get_begin()
		    &&  !prev_symbol.is_binary_infix()
		    &&  !parse_symbol.is_binary_infix()
		    &&  !(prev_symbol.is_unary_prefix()
			    && (prev_symbol.taking_arguments()
				||  prev_symbol.get_specifier()
					== Symbol.Specifier.IDENTIFIER
				    // NEED TO UNIFY THIS CODE WITH USE OF
				    // Symbol.taking_arguments(Symbol)
				    &&  !identifiers_appearing_without_args
						.contains(
						    prev_symbol
						    .get_text()
						    )
				)
			    )
		    &&  !parse_symbol.is_unary_postfix()
		    )
		{
		parse_symbols_it.previous();
		parse_symbols_it.add(
			new Symbol(
				Symbol.Specifier.TIMES,
				"",
				parse_symbol.get_begin()
				)
			);
		parse_symbols_it.next();
		}
	    prev_symbol = parse_symbol;
	    }

        parse_symbols.add(
	    new Symbol(Symbol.Specifier.ENDMARKER, "", text0.length())
	    );

	/*
        // debugging:
        System.err.println("\nparse_symbols:");
        for ( Symbol item : parse_symbols )
            System.err.println(
                item + " :  " + item.get_specifier()
                + "  \"" + item.get_text() + '"'
                + "  @" + item.get_begin()
                );
	*/

        // mostly operator-precedence parsing as described in
	// the dragon book ("Compilers" by Aho, Sethi, and Ullman).
        // I'm hoping that this will be more controllable than using
        // a parser generator (which may be unwieldy and may not give
        // error messages good for novice users)
        parse_results = new Stack<Grammar_Construct>();
        parse_results.push(new Symbol(Symbol.Specifier.ENDMARKER, "", 0));
	int topmost_open_op_index = 0;
	/* (;-)
	#define	topmost_open_operator	\
	    ((Symbol) parse_results.elementAt(topmost_open_op_index))
	*/
	Symbol topmost_open_operator = (Symbol) parse_results.peek();
        while ( !((topmost_open_operator.get_specifier()
			    .equals(Symbol.Specifier.ENDMARKER)
			||  topmost_open_operator.get_specifier()
			    .equals(Symbol.Specifier.BREAK)
			)
                    && parse_symbols.element().get_specifier()
			    .equals(Symbol.Specifier.ENDMARKER)
		    )
                )
            {

	    /*
            // debugging:
            System.err.println("\n---------------------------------\nstack:");
		// not 'enhanced' |for| because processing items
		// in reverse order
            for ( ListIterator<Grammar_Construct> results_it =
                        parse_results.listIterator(parse_results.size());
                    results_it.hasPrevious();
                    )
                {
                Grammar_Construct item = results_it.previous();
                if ( item.getClass() == Symbol.class ) {
                    Symbol item_t = (Symbol) item;
                    System.err.println(
                        item_t + " :  " + item_t.get_specifier()
                        + "  \"" + item_t.get_text() + '"'
                        + "  @" + item_t.get_begin()
                        );
                    }
                else {
                    Expression item_e = (Expression) item;
                    System.err.println(
                        item_e + " :  "
                        + item_e.get_operator() + ' '
                        + item_e.get_operator().get_specifier()
                        + "  @" + item_e.get_begin()
                        );
                    }
                }
            System.err.println(
                "\ntopmost_open_operator :   "
                + topmost_open_operator + " :  "
                + topmost_open_operator.get_specifier()
                + "  \"" + topmost_open_operator.get_text() + '"'
                + "  @" + topmost_open_operator.get_begin()
                );
            if ( parse_symbols.element().get_specifier()
                        == Symbol.Specifier.COMMENT
		    )
		{
		System.err.println(
		    "\nparse_symbols.element() :   "
		    + parse_symbols.element() + " :  "
		    + parse_symbols.element().get_specifier()
		    + "  \"" + parse_symbols.element().get_text() + '"'
		    + "  @" + parse_symbols.element().get_begin()
		    );
		System.err.println("pushing COMMENT(s) onto stack");
		}
	    */

            while ( parse_symbols.element().get_specifier()
                        == Symbol.Specifier.COMMENT
                    )
                parse_results.push(parse_symbols.remove());

	    /*
	    // debugging:
            System.err.println(
                "\nparse_symbols.element() :   "
                + parse_symbols.element() + " :  "
                + parse_symbols.element().get_specifier()
                + "  \"" + parse_symbols.element().get_text() + '"'
                + "  @" + parse_symbols.element().get_begin()
                );
	    System.err.println(
		"\ntopmost_open_operator"
		+ ".stack_precedence_stronger_than(parse_symbols.element()) : "
		+ topmost_open_operator
                    .stack_precedence_stronger_than(
			parse_symbols.element(),
			broken_infix_bin_ops
			)
		);
	    */

	    // Logically, the name "...precedence_weaker..." was fine
	    // and avoided a "!" where this is used,
	    // but thinking about it always gave me ~~headaches.
            if ( !topmost_open_operator
                    .stack_precedence_stronger_than(
			parse_symbols.element(),
			broken_infix_bin_ops
			)
                    )
                    // Rem. as indicated in dragon book
                    // ("Compilers" by Aho, Sethi, & Ullman)
                    // re operator-precedence parsing,
                    // 'gerrymandering' (OK, carefully arranging dual values
                    // for) precedence values/checking
                    // also handles associativity.
                {
                Symbol symbol_from_input = parse_symbols.remove();
		/* if Java had comma operator:
                parse_results.push(
		    // THIS CODE ACCEPTS "P Q".  TO AVOID, NEED
		    // |Symbol.is_zeroary()|.  IT WOULD ALSO BE NICE TO
		    // HAVE |Symbol.Specifier.ID_APPLICATION|.
                    symbol_from_input.taking_arguments(parse_symbols.element())
                                    // NEED TO UNIFY THIS CODE WITH USE OF
                                    // identifiers_appearing_without_args
                    ?  (topmost_open_op_index = parse_results.size()),
			(topmost_open_operator = symbol_from_input)
                    :  new Expression(symbol_from_input)
                    );
		*/
                parse_results.push(
                    symbol_from_input.taking_arguments(parse_symbols.element())
                                    // NEED TO UNIFY THIS CODE WITH USE OF
                                    // identifiers_appearing_without_args
			// kludge alternative to comma operator:
			&&  (topmost_open_op_index = parse_results.size())
			    > 0
		    ?  (topmost_open_operator = symbol_from_input)
                    :  new Expression(symbol_from_input)
                    );
                continue;
                }

	    // Otherwise, 'reduce':

	    // Code to do this while accessing |parse_results| strictly from
	    // the top (with error checking) appeared twisted/inelegant.
	    // But the access here is really all in the top 'handle'.

	    Symbol op = topmost_open_operator;	// this 'save' isn't really
	    					// necessary until really
						// removing/adding things
						// from/to stack; but
						// having this short var. name
						// is convenient...
	    int handle_start_index;
	    for ( handle_start_index = topmost_open_op_index - 1;
		    handle_start_index >= 0
			&&  parse_results.elementAt(handle_start_index)
				.getClass()
			    == Symbol.class
			&&  ((Symbol)
				    parse_results.elementAt(handle_start_index)
				    )
				.get_specifier()
			    == Symbol.Specifier.COMMENT;
		    handle_start_index--
		    )
		;
            Expression expr_preceding_op;
	    if ( handle_start_index < 0
		    ||  parse_results.elementAt(handle_start_index).getClass()
			!= Expression.class
		    )
		{
		if ( !op.is_unary_prefix() )
		    throw new IllegalArgumentException(
			fmt_illargexc_msg(
			    parse_results.elementAt(handle_start_index)
				.get_limit(),
			    op.get_begin(),
			    "improper/incomplete subexpression between \""
				+  ((Symbol)
					parse_results
					    .elementAt(handle_start_index)
					)
				    .get_text()
				+ "\" ("
				+  ((Symbol)
					parse_results
					    .elementAt(handle_start_index)
					)
				    .get_specifier()
				+ ") and "
				+ op.get_text()
				+ "\" ("
				+ op.get_specifier()
				+ ')'
			    )
			);
		handle_start_index = topmost_open_op_index;
		expr_preceding_op = null;
		}
	    else
		expr_preceding_op =
		    (Expression) parse_results.elementAt(handle_start_index);
	    int handle_end_index;
	    for ( handle_end_index = topmost_open_op_index + 1;
		    handle_end_index < parse_results.size()
			&&  parse_results.elementAt(handle_end_index)
				.getClass()
			    == Symbol.class
			&&  ((Symbol) parse_results.elementAt(handle_end_index))
				.get_specifier()
			    == Symbol.Specifier.COMMENT;
		    handle_end_index++
		    )
		;
            Expression expr_following_op;
	    int expected_handle_end_index =
		index_topmost_noncomment(parse_results);
	    if ( handle_end_index >= parse_results.size()
		    ||  parse_results.elementAt(handle_end_index).getClass()
			!= Expression.class
		    ||  handle_end_index < expected_handle_end_index
		    )
		{
		if ( handle_end_index < expected_handle_end_index
			||  !op.is_unary_postfix()
			)
		    throw new IllegalArgumentException(
			fmt_illargexc_msg(
			    op.get_limit(),
			    parse_symbols.element().get_begin(),
			    "improper/incomplete subexpression between \""
				+ op.get_text()
				+ "\" ("
				+ op.get_specifier()
				+ ") and "
				+ (parse_symbols.element().get_specifier()
					.equals(Symbol.Specifier.ENDMARKER)
				    ?  "end"
				    : parse_symbols.element().get_specifier()
					    .equals(Symbol.Specifier.BREAK)
					?  "line break"
					:  '"'
					    + parse_symbols.element().get_text()
					    + "\" ("
					    + parse_symbols.element()
						.get_specifier()
					    + ')'
				    )
			    )
			);
		handle_end_index = topmost_open_op_index;
		expr_following_op = null;
		}
	    else
		expr_following_op =
		    (Expression) parse_results.elementAt(handle_end_index);

	    /*
            // debugging:
	    System.err.println();
	    System.err.println(
		"expr_following_op:  " + expr_following_op + " :  "
		+ (expr_following_op == null
		    ?  expr_following_op
		    :  expr_following_op.get_operator() + " "
			+ expr_following_op.get_operator().get_specifier()
			+ "  @" + expr_following_op.get_begin()
		    )
		);
	    System.err.println(
		"op:  "
		+ op + " :  " + op.get_specifier()
		+ "  \"" + op.get_text() + '"'
		+ "  @" + op.get_begin()
		);
	    System.err.println(
		"expr_preceding_op:  "
		+ expr_preceding_op + " :  "
		+ (expr_preceding_op == null
		    ?  expr_preceding_op
		    :  expr_preceding_op.get_operator() + " "
			+ expr_preceding_op.get_operator().get_specifier()
			+ "  @" + expr_preceding_op.get_begin()
		    )
		);

	    */

            if ( topmost_open_operator.get_specifier()
			.equals(Symbol.Specifier.OPENING_DELIMITER)
		    && !op.matching_delimiter(parse_symbols.element())
		    )
		throw new IllegalArgumentException(
		    fmt_illargexc_msg(
			op.get_begin(),
			parse_symbols.element().get_limit(),
			parse_symbols.element().get_specifier()
				== Symbol.Specifier.ENDMARKER
			    ?  "opening delimiter \""
				+ op.get_text()
				+ "\" appears never closed"
			    :  "expected symbols \""
				+ op.get_text()
				+ "\" ("
				+ op.get_specifier()
				+ ") and \""
				+ parse_symbols.element().get_text()
				+ "\" ("
				+ parse_symbols.element().get_specifier()
				+ ") to be matching delimiters,"
				+ " but they aren't."
			)
		    );

            if ( op.get_specifier().equals(Symbol.Specifier.QUANT_SEP)
                    && (expr_preceding_op.op_spec_equals(
				Symbol.Specifier.OPENING_DELIMITER
				)
                            && !expr_preceding_op.get_operator().get_text()
				.equals("(")
                        || !expr_preceding_op.ungroup().get_operator()
			    .is_quantifier()
                        )
                    )
                throw new IllegalArgumentException(
                    fmt_illargexc_msg(
                        op.get_begin(),
                        op.get_begin(),
                        "expected (parenthesized) quantifier preceding \""
                            + op.get_text()
                            + "\" ("
                            + op.get_specifier()
                            + ')'
                        )
                    );

            if ( op.is_quantifier() )
                analyze_quant_vars(expr_following_op, new_identifiers);

	    // I still think |removeRange()| would be more clear than this:
	    parse_results.subList(handle_start_index, parse_results.size())
		.clear();

	    int expected_next_topmost_open_op_index =
		index_topmost_noncomment(parse_results);
            if ( expected_next_topmost_open_op_index < 0 )
                throw new IllegalArgumentException(
                    fmt_illargexc_msg(
                        0,
                        0,
			"incomplete/improper material at beginning"
                        )
                    );
	    Grammar_Construct expected_next_topmost_open_op =
		parse_results.elementAt(expected_next_topmost_open_op_index);
            if ( expected_next_topmost_open_op.getClass() != Symbol.class )
                throw new IllegalArgumentException(
                    fmt_illargexc_msg(
                        expected_next_topmost_open_op.get_limit(),
                        expr_preceding_op.get_begin(),
                        "expected an operator between subexpressions \""
			    + text0.substring(
				expected_next_topmost_open_op.get_begin(),
				expected_next_topmost_open_op.get_limit()
				)
			    + "\" and \""
			    + text0.substring(
				expr_preceding_op.get_begin(),
				expr_preceding_op.get_limit()
				)
			    + '"'
                        )
                    );
	    topmost_open_op_index = expected_next_topmost_open_op_index;
            topmost_open_operator = (Symbol) expected_next_topmost_open_op;

            parse_results.push(
		op.get_specifier().equals(Symbol.Specifier.OPENING_DELIMITER)
                ?  new Expression(
		    op,
		    expr_following_op,
		    new Expression(parse_symbols.remove())  //kludge
		    )
		:  op.is_unary_prefix()
		    ?  new Expression(op, expr_following_op)
		    :  op.is_unary_postfix()
			?  new Expression(expr_preceding_op, op)
			:  broken_infix_bin_ops.contains(op)
			    ?  new Expression(
				op,
				expr_preceding_op.ensure_group(),
						// I wonder whether these
						// additions to the material
						// may screw up things such
						// as selecting.
				expr_following_op.ensure_group()
				)
			    :  new Expression(
				op,
				expr_preceding_op,
				expr_following_op
				)
                );

            }

	/*
        // debugging:
        System.err.println(
	    "\n---------------------------------\nat end:\nstack:"
	    );
		// not 'enhanced' |for| because processing items
		// in reverse order
        for ( ListIterator<Grammar_Construct> results_it =
                    parse_results.listIterator(parse_results.size());
                results_it.hasPrevious();
                )
            {
            Grammar_Construct item = results_it.previous();
            if ( item.getClass() == Symbol.class ) {
                Symbol item_t = (Symbol) item;
                System.err.println(
                    item_t + " :  " + item_t.get_specifier()
                    + "  \"" + item_t.get_text() + '"'
                    + "  @" + item_t.get_begin()
                    );
                }
            else {
                Expression item_e = (Expression) item;
                System.err.println(
                    item_e + " :  "
                    + item_e.get_operator() + ' '
                    + item_e.get_operator().get_specifier()
                    + "  @" + item_e.get_begin()
                    );
                }
            }
        System.err.println(
            "\ntopmost_open_operator :   "
            + topmost_open_operator + " :  "
            + topmost_open_operator.get_specifier()
            + "  \"" + topmost_open_operator.get_text() + '"'
            + "  @" + topmost_open_operator.get_begin()
            );
        System.err.println(
            "\nparse_symbols.element() :   "
            + parse_symbols.element() + " :  "
            + parse_symbols.element().get_specifier()
            + "  \"" + parse_symbols.element().get_text() + '"'
            + "  @" + parse_symbols.element().get_begin()
            );
        System.err.println("\n=================================\n");
	*/

        ListIterator<Grammar_Construct> results_it =
	    parse_results.listIterator();
        assert  results_it.hasNext() : "results_it.hasNext()";
        Grammar_Construct init_endmarker_gc = results_it.next();
        assert
            init_endmarker_gc.getClass() == Symbol.class
                &&  ((Symbol) init_endmarker_gc).get_specifier()
                        .equals(Symbol.Specifier.ENDMARKER)
            :
            "init_endmarker_gc.getClass() == Symbol.class\n"
            + "    &&  ((Symbol) init_endmarker_gc).get_specifier()\n"
            + "            .equals(Symbol.Specifier.ENDMARKER)\n";
            /*
            throw new IllegalStateException(
                "lost initial ENDMARKER"
                );
            */
        results_it.remove();
        boolean have_an_expression = false;
        while ( results_it.hasNext() )
            if ( have_an_expression
                    =
                    results_it.next().getClass() == Expression.class
                    )
                break;
        if ( !have_an_expression )
            throw new IllegalArgumentException(
                fmt_illargexc_msg(
                    0,
                    text0.length(),
                    "no expressions found in input text"
                    )
                );

	// and_further_constrain
	if ( !allowing_free_variables )
	    for ( Grammar_Construct result_gc : parse_results )
		if ( result_gc instanceof Expression ) {
		    HashSet<String> result_variables_unquantified =
			variables_unquantified((Expression) result_gc);
		    if ( !result_variables_unquantified.isEmpty() )
			throw new IllegalArgumentException(
			    fmt_illargexc_msg(
				result_gc.get_begin(),
				result_gc.get_limit(),
				"What you entered includes "
					+ (result_variables_unquantified
						.size() == 1
					    ?  "a"
					    :  "some"
					    )
					+ " free (i.e. unquantified) variable"
					+ (result_variables_unquantified
						.size() == 1
					    ?  ": \""
						+ result_variables_unquantified
						    .toArray()[0]
						+ '"'
					    :  "s: "
						+ result_variables_unquantified
					    )
				    + ".\nPlease don't try that"
					+ " because such obscures"
					+ " the universality of proofs."
				)
			    );
		    }
	Expression result = null;
	if ( !accepting_multiple_exprs ) {
	    results_it = parse_results.listIterator();
	    Grammar_Construct result_gc = null;
	    /*
	    comment_symbol = null;
	    */
	    while ( results_it.hasNext()
			&&  (result_gc = results_it.next()) instanceof Symbol
			&& (((Symbol) result_gc).get_specifier()
				    == Symbol.Specifier.BREAK
			    ||  (/*comment_symbol =*/ (Symbol) result_gc)
					.get_specifier()
				    == Symbol.Specifier.COMMENT
			    )
		    )
		;
	    assert  result_gc != null  :  "result_gc != null";
	    assert
		result_gc instanceof Expression
		:  "result_gc instanceof Expression";
	    /*
	    assert
		comment_symbol == null
		|| comment_symbol.get_specifier()
		    ==
		    Symbol.Specifier.COMMENT
		:  "comment_symbol == null\n"
		    + "||  comment_symbol.get_specifier()"
			+ " == "
			+ "Symbol.Specifier.COMMENT";
	    */
	    // By contrast with what happens here,
	    // consider allowing comment following expression.
	    if ( results_it.hasNext() ) {
		result_gc = results_it.next();
		throw new IllegalArgumentException(
		    fmt_illargexc_msg(
			result_gc.get_begin(),
			text0.length(),
			"After one expression which appears OK,"
				+ " you have extra unconnected material."
			    + "\nPlease enter only one, complete expression here."
			)
		    );
		}
	    result = (Expression) result_gc;
	    }
	assert
	    // seeking_constant_term ==> !accepting_multiple_exprs
	    !(seeking_constant_term && accepting_multiple_exprs)
	    : "!(seeking_constant_term && accepting_multiple_exprs)";
	/*
	assert
	    // seeking_smply_eq ==> !accepting_multiple_exprs
	    !(seeking_smply_eq && accepting_multiple_exprs)
	    : "!(seeking_smply_eq && accepting_multiple_exprs)";
	*/
	if ( seeking_constant_term && !constant_term(result) )
		// Checking and noting this here
		// instead of in |Ded_Action|
		// I think
		// gives user best opportunity to (re)do
		// properly.
	    throw new IllegalArgumentException(
		fmt_illargexc_msg(
		    0,
		    text0.length(),
		    "What you entered was not a constant term."
		    )
		);
	if ( desired_smply_eq_orig != null
		&&  result.equivalent_form(desired_smply_eq_orig)
		)
		// Checking and noting this here
		// instead of in |Ded_Action|
		// I think
		// gives user best opportunity to (re)do
		// properly.
	    throw new IllegalArgumentException(
		fmt_illargexc_msg(
		    0,
		    text0.length(),
		    "Um, what you have entered appears essentially unchanged"
			+ " from the original expression \""
			    + desired_smply_eq_text
			    + "\"."
		    )
		);
	if ( desired_smply_eq_orig != null
		&&  !smply_eq(desired_smply_eq_orig, result)
		)
		// Checking and noting this here
		// instead of in |Ded_Action|
		// I think
		// gives user best opportunity to (re)do
		// properly.
	    throw new IllegalArgumentException(
		fmt_illargexc_msg(
		    0,
		    text0.length(),
		    "It's not clear that what you entered"
			    + " is equivalent"
			+ "\nto the original expression \""
			    + desired_smply_eq_text
			    + "\"\nvia just one step of basic algebra/arithmetic."
			+ "\nConsider trying to do the transformation"
									// ;
				+ " that you desire in more than one step \u2014"
			+ "\nor maybe consider using a presupposition"
			    + " with a form like the following:\n\t"
			+ desired_smply_eq_text
			    + " = "
			    + text0
		    )
		);

	identifiers.addAll(new_identifiers);

        return  parse_results;
        }



    ArrayList<Expression> get_terms(Expression expr) {
        ArrayList<Expression> result = new ArrayList<Expression>();
        get_terms(expr, result);
        return  result;
        }

    private void get_terms(Expression expr, ArrayList<Expression> accumulator) {
	get_terms(expr, accumulator, false);
        }

    private void get_terms(
	    Expression expr,
	    ArrayList<Expression> accumulator,
	    boolean neg
	    )
	{
	switch ( expr.get_operator().get_specifier() ) {
	    case  OPENING_DELIMITER:
		// assert op_text equals "(" or "["
		get_terms(expr.get_argument1(), accumulator, neg);
		break;

	    case  NEGATIVE:
		get_terms(expr.get_argument1(), accumulator, !neg);
		break;

	    case  PLUS:
		get_terms(expr.get_argument1(), accumulator, neg);
		get_terms(expr.get_argument2(), accumulator, neg);
		break;

	    case  MINUS:
		get_terms(expr.get_argument1(), accumulator, neg);
		get_terms(expr.get_argument2(), accumulator, !neg);
		break;

	    case  INT:
		accumulator.add(neg ? new Expression(-expr.get_val()) : expr);
		break;

	    case  TIMES:
		Expression arg1_ungroup = expr.get_argument1().ungroup();
		if ( neg && arg1_ungroup.op_spec_equals(Symbol.Specifier.INT)
			)
		    {
		    accumulator.add(
			new Expression(
				new_Symbol(Symbol.Specifier.TIMES),
				new Expression(-arg1_ungroup.get_val()),
				expr.get_argument2()
				)
			);
		    break;
		    }
	    default:
		accumulator.add(
		    neg
			// canonicalizing with coefficient -1
			// instead of just negating
		    ? new Expression(
			    new_Symbol(Symbol.Specifier.TIMES),
			    new Expression(-1),
			    expr
			    )
		    : expr
		    );
		break;
	    }
	}

    private static boolean cull_and_t_or_f(
	    Expression expr,
	    Symbol.Specifier specifier
	    )
	{
        assert
            specifier == Symbol.Specifier.AND
                ||  specifier == Symbol.Specifier.OR
            : "specifier == Symbol.Specifier.AND"
                + "  ||  specifier == Symbol.Specifier.OR";
        if ( !expr.op_spec_equals(specifier) )
            return  false;
        boolean result =
            cull_and_t_or_f(expr.get_argument1().ungroup(), specifier)
            | cull_and_t_or_f(expr.get_argument2().ungroup(), specifier);
        if ( specifier == Symbol.Specifier.OR ) {
            if ( expr.get_argument1()
		    .ungrp_op_spec_equals(Symbol.Specifier.FALSE)
		    )
                return  expr.this_structure_replace(expr.get_argument2());
            if ( expr.get_argument2()
		    .ungrp_op_spec_equals(Symbol.Specifier.FALSE)
		    )
                return  expr.this_structure_replace(expr.get_argument1());
            }
        if ( specifier == Symbol.Specifier.AND ) {
            if ( expr.get_argument1()
		    .ungrp_op_spec_equals(Symbol.Specifier.TRUE)
		    )
                return  expr.this_structure_replace(expr.get_argument2());
            if ( expr.get_argument2()
		    .ungrp_op_spec_equals(Symbol.Specifier.TRUE)
		    )
                return  expr.this_structure_replace(expr.get_argument1());
            }
        return  result;
        }

    // not just "greatest common divisor" because this code also captures
    // common negativity
    static int common_factor(int x, int y) {
	/*
	boolean negative =  x < 0  &&  y < 0;
	x = Math.abs(x);
	y = Math.abs(y);
	*/
	boolean negative = true;
	if ( x < 0 )
	    x = -x;
	else
	    negative = false;
	if ( y < 0 )
	    y = -y;
	else
	    negative = false;

        while ( y != 0 ) {
            int y_old = y;
            y = x % y_old;
            x = y_old;
            }
        return  negative ? -x : x;
	}

    boolean simplify(Expression expr) {
        boolean result = false;

        Expression arg1_negand = null;
        int arg1_val = -1; // note not an impossible value,
                                // but a useful signal value nonetheless
        if ( expr.get_argument1() != null ) {
            result |= simplify(expr.get_argument1());
            /*
            if ( expr.get_argument1()
			.op_spec_equals(Symbol.Specifier.OPENING_DELIMITER)
                    &&  !op_spec_equals(Symbol.Specifier.IDENTIFIER)
                    &&  expr.get_argument1().get_argument1().get_argument1()
			== null
                    &&  expr.get_argument1().get_argument1().get_argument2()
			== null
                    )
                result =
		    expr.get_argument1()
			.this_structure_replace(
			    expr.get_argument1().get_argument1()
			    );
            */
            if ( expr.get_argument1()
		    .ungrp_op_spec_equals(logical_negation_sym_spec)
		    )
                arg1_negand =
		    expr.get_argument1().ungroup().get_argument1().ungroup();
            else if ( expr.get_argument1()
			.ungrp_op_spec_equals(Symbol.Specifier.INT)
			)
                arg1_val = expr.get_argument1().ungroup().get_val();
                                // See |parse()| above re checking |get_val()|
            }

        Expression arg2_negand = null;
        int arg2_val = -1; // note not an impossible value,
                                // but a useful signal value nonetheless
        if ( expr.get_argument2() != null ) {
            result |= simplify(expr.get_argument2());
            /*
            if ( expr.get_argument2()
			.op_spec_equals(Symbol.Specifier.OPENING_DELIMITER)
                    &&  !expr.op_spec_equals(Symbol.Specifier.IDENTIFIER)
                    &&  expr.get_argument2().get_argument1().get_argument1()
			== null
                    &&  expr.get_argument2().get_argument1().get_argument2()
			== null
                    )
                result =
		    expr.get_argument2()
			    .this_structure_replace(
				expr.get_argument2().get_argument1()
				);
            */
            if ( expr.get_argument2()
		    .ungrp_op_spec_equals(logical_negation_sym_spec)
		    )
                arg2_negand =
		    expr.get_argument2().ungroup().get_argument1().ungroup();
            else if ( expr.get_argument2()
			.ungrp_op_spec_equals(Symbol.Specifier.INT)
			)
                arg2_val = expr.get_argument2().ungroup().get_val();
                                // See |parse()| above re checking |get_val()|
            }

	/* See |clear_excessive_basic_grps_internal()|
        if ( expr.is_group() ) {
            if ( expr.get_argument1().is_group()
		    && !expr.get_operator().get_text().equalsIgnoreCase("IF")
		    )
                    // Because there may be singular arguments
                    // for functions and predicates,
                    // removal of delimiters around singular things
                    // is done at the level above --- see code above
                    // initially processing |argument1| and |argument2|.
                    // Incidentally, simplifying delimiters around overall
                    // expression would need to be special anyway because
                    // overall expression could be infix...
                    // Philosophically/lexicographically, parentheses are
                    // more a concern of a parent expression than a
                    // child expression anyway.
                return  expr.this_structure_replace(expr.get_argument1());
            return  result;
            }
	*/

	if ( expr.op_spec_equals(Symbol.Specifier.OPENING_DELIMITER) ) {
	    if ( expr.get_operator().get_text().equals("{") ) {
		Expression content = expr.get_argument1();
		if ( content.op_spec_equals(Symbol.Specifier.COMMA) ) {
		    LinkedList<Expression>
			elements0 = content.multiary_op_args(),
			elements_simp = new LinkedList<Expression>();
		    for ( Expression element0 : elements0 )
			if ( !element0.equivalent_form_contained_in(
				    elements_simp
				    )
				)
			    elements_simp.add(element0);
		    if ( elements_simp.size() < elements0.size() ) {
			Expression es_expr = elements_simp.removeFirst();
			for ( Expression element_simp : elements_simp )
			    es_expr = new Expression(
					    new_Symbol(Symbol.Specifier.COMMA),
					    es_expr,
					    element_simp
					    );
			return  content.this_structure_replace(es_expr);
			}
		    }
		else if ( content.op_spec_equals(Symbol.Specifier.SUCH_THAT)
			    &&  content.get_argument2()
				    .ungrp_op_spec_equals(Symbol.Specifier.IS_IN)
			    /*
			    //&& is_variable(expr_get_argument1().get_argument1())
			    &&  content.get_argument1()
				    .op_spec_equals(Symbol.Specifier.IDENTIFIER)
			    &&  content.get_argument1().get_argument1() == null
			    */
			    &&  content.get_argument2().ungroup()
				    .get_argument1().equivalent_form(
					    content.get_argument1()
					    )
			    )
		    return
			expr.this_structure_replace(
				content.get_argument2().ungroup()
					.get_argument2()
				);
		}
	    else if ( expr.get_operator().get_text().equals("|") )
		if ( expr.get_argument1()
			.ungrp_op_spec_equals(Symbol.Specifier.INT)
			)
		    return
			expr.this_structure_replace(
			    Math.abs(expr.get_argument1().ungroup().get_val())
			    );
		if ( expr.get_argument1()
			.ungrp_op_spec_equals(Symbol.Specifier.EMPTYSET)
			)
		    return  expr.this_structure_replace(0);
		else if ( expr.get_argument1().op_spec_equals(
				Symbol.Specifier.OPENING_DELIMITER
				)
			    && expr.get_argument1().get_operator().get_text()
				.equals("{")
			    && !expr.get_argument1().get_argument1()
				.op_spec_equals(Symbol.Specifier.SUCH_THAT)
			    )
		    {
		    Expression content = expr.get_argument1().get_argument1();
		    if ( !content.op_spec_equals(Symbol.Specifier.COMMA) )
			return  expr.this_structure_replace(1);
		    LinkedList<Expression> elements
			= content.multiary_op_args(Symbol.Specifier.COMMA);
		    boolean elements_are_ints = true;
		    for ( Expression element : elements )
			if ( !(elements_are_ints &=
				    element.op_spec_equals(Symbol.Specifier.INT)
				    )
				)
			    break;
		    if ( elements_are_ints )
			return  expr.this_structure_replace(elements.size());
		    }
	    else if ( (expr.get_operator().get_text()
			    .equals(Character.toString(Symbol.LFLOOR_UNICODE))
		       || expr.get_operator().get_text()
			    .equals(Character.toString(Symbol.LCEIL_UNICODE))
		       || expr.get_operator().get_text()
			    .equals(
				Character.toString(
				    Symbol
				    .LEFT_UPPER_CORNER_UNICODE
				    )
				)
		       || expr.get_operator().get_text()
			    .equals(
				Character.toString(
				    Symbol
				    .LEFT_LOWER_CORNER_UNICODE
				    )
				)
		       )
		    )
		{
		Expression arg1_ungrp = expr.get_argument1().ungroup();
		if ( arg1_ungrp.op_spec_equals(Symbol.Specifier.INT) )
		    return  expr.this_structure_replace(arg1_ungrp);
		if ( arg1_ungrp.op_spec_equals(Symbol.Specifier.QUOTIENT) ) {
		    Expression
			numerator = arg1_ungrp.get_argument1().ungroup(),
			denominator = arg1_ungrp.get_argument2().ungroup();
		    if ( numerator.op_spec_equals(Symbol.Specifier.INT)
			    &&  denominator.op_spec_equals(Symbol.Specifier.INT)
			    &&  denominator.get_val() != 0
			    )
			{
			double quotient =
			    (double)
			    numerator.get_val() / denominator.get_val();
			int result_val;
			switch ( expr.get_operator().get_text().charAt(0) ) {
			    case Symbol.LFLOOR_UNICODE:
			    case Symbol.LEFT_LOWER_CORNER_UNICODE:
				result_val = (int) Math.floor(quotient);
				break;

			    case Symbol.LCEIL_UNICODE:
			    case Symbol.LEFT_UPPER_CORNER_UNICODE:
				result_val = (int) Math.floor(quotient);
				break;

			    default:
				throw new IllegalStateException(
				    "unexpected floor/ceiling character"
				    );
			    }
			return
			    expr.this_structure_replace(result_val);
			}
		    }
		}
	    return  result;
	    }

        if ( expr.get_operator().is_quantifier() )
            return
                !variables_unquantified(expr.get_argument1())
                    .equals(expr.get_argument1().var_seq_cull_duplicates());

        if ( expr.op_spec_equals(Symbol.Specifier.QUANT_SEP) ) {
            HashSet<String>
                vars_used = variables_unquantified(expr.get_argument2()),
                vars_quantified =
                    variables_unquantified(
			expr.get_argument1().ungroup().get_argument1()
			);
            if ( vars_used.isEmpty() || !vars_quantified.removeAll(vars_used) )
                {
                expr.this_structure_replace(expr.get_argument2());
                return  true;
                }
            if ( vars_quantified.isEmpty() )
                return  result;
            expr.get_argument1().ungroup().get_argument1()
		    .this_structure_replace(
			expr.get_argument1().ungroup().get_argument1()
				.var_seq_remove(vars_quantified)
			);
            return  true;
            }

        if ( expr.op_spec_equals(Symbol.Specifier.PMOD)   &&  arg2_val > 0 ) {
	    if ( expr.get_argument1()
		    .ungrp_op_spec_equals(Symbol.Specifier.CONGRUENT)
		    )
		{
		Expression
		    arg1_arg1_ungrp =
			expr.get_argument1().ungroup()
				.get_argument1().ungroup(),
		    arg1_arg2_ungrp =
			expr.get_argument1().ungroup()
				.get_argument2().ungroup();
		if ( arg1_arg1_ungrp.equivalent_form(arg1_arg2_ungrp) )
		    return
			expr.this_structure_replace(
				new_Symbol(Symbol.Specifier.TRUE)
				);
		if ( arg1_arg1_ungrp.op_spec_equals(Symbol.Specifier.INT)
			&& arg1_arg2_ungrp.op_spec_equals(Symbol.Specifier.INT)
			)
		    return
			expr.this_structure_replace(
				new_Symbol(
				    (arg1_arg1_ungrp.get_val()
					    - arg1_arg2_ungrp.get_val()
					    )
					    % arg2_val
					== 0
				    ? Symbol.Specifier.TRUE
				    : Symbol.Specifier.FALSE
				    )
				);
		}
            return  result;
            }

        if ( expr.op_spec_equals(Symbol.Specifier.EQUIV) ) {
            if ( expr.get_argument1()
		    .ungrp_op_spec_equals(Symbol.Specifier.TRUE)
		    )
                return  expr.this_structure_replace(expr.get_argument2());
            if ( expr.get_argument2()
		    .ungrp_op_spec_equals(Symbol.Specifier.TRUE)
		    )
                return  expr.this_structure_replace(expr.get_argument1());
            if ( expr.get_argument1()
		    .ungrp_op_spec_equals(Symbol.Specifier.FALSE)
		    )
		{
                expr.this_structure_replace(
			new_Symbol(logical_negation_sym_spec),
			expr.get_argument2()
			);
                simplify(expr);
                return  true;
                }
            if ( expr.get_argument2()
		    .ungrp_op_spec_equals(Symbol.Specifier.FALSE)
		    )
		{
                expr.this_structure_replace(
			new_Symbol(logical_negation_sym_spec),
			expr.get_argument1()
			);
                simplify(expr);
                return  true;
                }
            if ( expr.get_argument1().ungroup()
		    .equivalent_form(expr.get_argument2().ungroup())
		    )
                return
		    expr.this_structure_replace(
			    new_Symbol(Symbol.Specifier.TRUE)
			    );
            if ( arg1_negand != null
                    &&  arg1_negand
			.equivalent_form(expr.get_argument2().ungroup())
                    )
                return
		    expr.this_structure_replace(
			    new_Symbol(Symbol.Specifier.FALSE)
			    );
            if ( arg2_negand != null
                    &&  arg2_negand
			.equivalent_form(expr.get_argument1().ungroup())
                    )
                return
		    expr.this_structure_replace(
			    new_Symbol(Symbol.Specifier.FALSE)
			    );
            return  result;
            }

        if ( expr.op_spec_equals(Symbol.Specifier.IMPLIES) ) {
            if ( expr.get_argument1()
		    .ungrp_op_spec_equals(Symbol.Specifier.FALSE)
		    )
                return
		    expr.this_structure_replace(
			    new_Symbol(Symbol.Specifier.TRUE)
			    );
            if ( expr.get_argument1()
		    .ungrp_op_spec_equals(Symbol.Specifier.TRUE)
		    )
                return  expr.this_structure_replace(expr.get_argument2());
            if ( expr.get_argument2()
		    .ungrp_op_spec_equals(Symbol.Specifier.TRUE)
		    )
                return
		    expr.this_structure_replace(
			    new_Symbol(Symbol.Specifier.TRUE)
			    );
            if ( expr.get_argument2()
		    .ungrp_op_spec_equals(Symbol.Specifier.FALSE)
		    )
		{
                expr.this_structure_replace(
			new_Symbol(logical_negation_sym_spec),
			expr.get_argument1()
			);
                simplify(expr);
                return  true;
                }
            if ( expr.get_argument1().ungroup()
		    .equivalent_form(expr.get_argument2().ungroup())
		    )
                return
		    expr.this_structure_replace(
			    new_Symbol(Symbol.Specifier.TRUE)
			    );
            if ( arg1_negand != null
                    &&  arg1_negand
			.equivalent_form(expr.get_argument2().ungroup())
                    )
                return  expr.this_structure_replace(expr.get_argument2());
            if ( arg2_negand != null
                    &&  arg2_negand
			.equivalent_form(expr.get_argument1().ungroup())
                    )
                {
                expr.this_structure_replace(
			new_Symbol(logical_negation_sym_spec),
			expr.get_argument1()
			);
                simplify(expr);
                return  true;
                }
            if ( arg1_negand != null  &&  arg2_negand != null ) {
                expr.this_structure_replace(
			new_Symbol(Symbol.Specifier.IMPLIES),
			expr.get_argument1().get_operator().get_text()
				.equalsIgnoreCase("IF")
			    ? new Expression(
				new Symbol(
				    Symbol.Specifier.OPENING_DELIMITER,
				    expr.get_argument1().get_operator()
					.get_text()
				    ),
				arg2_negand
				)
			    : arg2_negand,
			arg1_negand
			);
                simplify(expr);
                return  true;
                }
            return  result;
            }

        if ( expr.op_spec_equals(Symbol.Specifier.OR)
                ||  expr.op_spec_equals(Symbol.Specifier.AND)
                )
            {
            LinkedList<Expression> multiary_args =
		expr.multiary_op_args(expr.get_operator().get_specifier());
            for ( Expression arg : multiary_args ) {
                result |= simplify(arg);
                if ( arg.ungrp_op_spec_equals(Symbol.Specifier.FALSE)
                            && expr.op_spec_equals(Symbol.Specifier.AND)
                       || arg.ungrp_op_spec_equals(Symbol.Specifier.TRUE)
                           && expr.op_spec_equals(Symbol.Specifier.OR)
                       )
                    return
			expr.this_structure_replace(
				//new_Symbol(arg.ungroup().get_operator().get_specifier())
				arg
				);
                }
                // not 'enhanced' |for| because using index as well as element
            for ( ListIterator<Expression> args_it =
                        multiary_args.listIterator();
                    args_it.hasNext();
                    )
                {
                Expression arg_ungrp = args_it.next().ungroup();
                if ( arg_ungrp.op_spec_equals(Symbol.Specifier.TRUE)
                            && expr.op_spec_equals(Symbol.Specifier.AND)
                       || arg_ungrp.op_spec_equals(Symbol.Specifier.FALSE)
                           && expr.op_spec_equals(Symbol.Specifier.OR)
                       )
                    continue;   // see below invocation of |cull_and_t_or_f()|
                                // upon which, incidentally, the intervening
                                // code relies

                if ( arg_ungrp.op_spec_equals(Symbol.Specifier.TRUE)
                        || arg_ungrp.op_spec_equals(Symbol.Specifier.FALSE)
                        || arg_ungrp.op_spec_equals(logical_negation_sym_spec)
                            && expr.some_sub_junct_matches(
				    arg_ungrp.get_argument1().ungroup()
				    )
                        )
                    return
                        expr.this_structure_replace(
				new_Symbol(
				    expr.op_spec_equals(Symbol.Specifier.OR)
				    ? Symbol.Specifier.TRUE
				    : Symbol.Specifier.FALSE
				    )
				);

		// An earlier version of the following code
		// used |multiary_args.indexOf(arg), which depended on
		// |Expression.equals()| returning the result of
		// just |equivalent_form()|.
		    // not 'enhanced' |for| because using index
		    // as well as element
		for ( ListIterator<Expression> args_it2 =
			    multiary_args.listIterator();
			args_it2.hasNext()
			    &&  args_it2.nextIndex() + 1 < args_it.nextIndex();
						// |+ 1| because already
						// did |args_it.next()|
						// but haven't yet
						// done |args_it2.next()|
			)
		    if ( args_it2.next().equivalent_form(arg_ungrp) ) {
			result |=
			    // Losing later equivalent expressions.
			    // I think proving different propositional
			    // tautologies may warrant losing earlier
			    // versus later equivalent expressions.
			    // Oh, well.
			    arg_ungrp.this_structure_replace(
				    new_Symbol(
					expr.op_spec_equals(
						Symbol.Specifier.OR
						)
					? Symbol.Specifier.FALSE
					: Symbol.Specifier.TRUE
					)
				    );
			break;
			}
                }
            result |=
		cull_and_t_or_f(expr, expr.get_operator().get_specifier());
            return  result;
            }

        if ( expr.op_spec_equals(logical_negation_sym_spec) ) {
            if ( expr.get_argument1()
		    .ungrp_op_spec_equals(Symbol.Specifier.TRUE)
		    )
                return
		    expr.this_structure_replace(
			    new_Symbol(Symbol.Specifier.FALSE)
			    );
            if ( expr.get_argument1()
		    .ungrp_op_spec_equals(Symbol.Specifier.FALSE)
		    )
                return
		    expr.this_structure_replace(
			    new_Symbol(Symbol.Specifier.TRUE)
			    );
            if ( arg1_negand != null )
                return  expr.this_structure_replace(arg1_negand);

            // Not implementing other simplifications
            // listed by Manna & Waldinger:
            // users may achieve them via rewritings....

	    if ( expr.get_argument1().ungroup().get_operator()
			.specifier_unnegate()
		    != null
		    )
                return
                    expr.this_structure_replace(
			new Expression(
			    new_Symbol(
				expr.get_argument1().get_operator()
				.specifier_unnegate()
				),
			    expr.get_argument1().ungroup().get_argument1(),
			    expr.get_argument1().ungroup().get_argument2()
			    )
			    .ensure_group()
                        );

	    if ( expr.get_argument1().ungroup()
			.op_spec_equals(Symbol.Specifier.IS)
			// without any grouping
		    &&  expr.get_argument1().ungroup().get_argument2()
			.get_operator().get_text().equalsIgnoreCase("NOT")
			// without any grouping
		    &&  expr.get_argument1().ungroup().get_argument2()
			.get_argument1()
			.op_spec_equals(Symbol.Specifier.IDENTIFIER)
		    )
		return
		    expr.this_structure_replace(
			new Expression(
			    expr.get_argument1().ungroup().get_operator(),
			    expr.get_argument1().ungroup().get_argument1(),
			    expr.get_argument1().ungroup().get_argument2()
				.get_argument1()
			    )
			    .ensure_group()
			);

            return result;
            }

        if ( expr.op_spec_equals(Symbol.Specifier.SUBST) ) {
            if ( !is_variable(expr.get_argument1()) )
		    // I'm actually not sure how
		    // appropriate this is.
                // CURRENTLY HANDLING ONLY SINGULAR, SIMPLE SUBSTITUTION:
                if ( expr.get_argument2()
			    .ungrp_op_spec_equals(Symbol.Specifier.EQUALS)
							    // BECOMES
                        &&  expr.get_argument2().ungroup().get_argument1()
                                .op_spec_equals(Symbol.Specifier.IDENTIFIER)
                        &&  expr.get_argument2().ungroup()
				    .get_argument1().get_argument1()
			    == null
			/*
                        &&  expr.get_argument2().ungroup()
				    .get_argument1().get_argument2() == null
			*/
                        )
                    {
		    expr.get_argument1().ungroup().replace_throughout_scope(
                            expr.get_argument2().ungroup()
				    .get_argument1().get_operator().get_text(),
                            expr.get_argument2().ungroup()
				    .get_argument2().ensure_group()
                            );
                    expr.this_structure_replace(expr.get_argument1());
                    simplify(expr);
                    return  true;
                    }
            return  result;
            }

            // !ProofBuilder.dont_collect_terms && ( )
        if ( expr.op_spec_equals(Symbol.Specifier.PLUS)
                || expr.op_spec_equals(Symbol.Specifier.MINUS)
                )
            {

	    /* This either undid some work or made no simplifications at
	     * all appear because a simplified expression isn't shown if
	     * it duplicates another.
	     *
	    // First doing e.g. "2(k+1)+1" --> "2k+2*1+1" (though
	    // not necessarily out of this context "2(k+1)" --> "2k+2*1")
	    Expression arg1_ungrp = expr.get_argument1().ungroup();
	    if ( arg1_ungrp.op_spec_equals(Symbol.Specifier.TIMES)
		    // Rem. simplify(TIMES) puts any INT coefficient at front.
		    && arg1_ungrp.get_argument1()
			    .ungrp_op_spec_equals(Symbol.Specifier.INT)
		    && (arg1_ungrp.get_argument2()
			    .ungrp_op_spec_equals(Symbol.Specifier.PLUS)
			||
			arg1_ungrp.get_argument2()
			    .ungrp_op_spec_equals(Symbol.Specifier.MINUS)
			)
		    )
		{
		int c = arg1_ungrp.get_argument1().ungroup().get_val();
		String ts = arg1_ungrp.get_operator().get_text();
		Expression p_or_m_ungrp = arg1_ungrp.get_argument2().ungroup();
		arg1_ungrp.this_structure_replace(
			p_or_m_ungrp.get_operator(),
			new Expression(
				new Symbol(Symbol.Specifier.TIMES, ts),
				new Expression(c),
				p_or_m_ungrp.get_argument1().ensure_group()
				),
			new Expression(
				new Symbol(Symbol.Specifier.TIMES, ts),
				new Expression(c),
				p_or_m_ungrp.get_argument2().ensure_group()
				)
			);
		simplify(arg1_ungrp);
		result = true;
		}
	    Expression arg2_ungrp = expr.get_argument2().ungroup();
	    if ( arg2_ungrp.op_spec_equals(Symbol.Specifier.TIMES)
		    // Rem. simplify(TIMES) puts any INT coefficient at front.
		    && arg2_ungrp.get_argument1()
			    .ungrp_op_spec_equals(Symbol.Specifier.INT)
		    && (arg2_ungrp.get_argument2()
			    .ungrp_op_spec_equals(Symbol.Specifier.PLUS)
			||
			arg2_ungrp.get_argument2()
			    .ungrp_op_spec_equals(Symbol.Specifier.MINUS)
			)
		    )
		{
		int c = arg2_ungrp.get_argument1().ungroup().get_val();
		String ts = arg2_ungrp.get_operator().get_text();
		Expression p_or_m_ungrp = arg2_ungrp.get_argument2().ungroup();
		arg2_ungrp.this_structure_replace(
		    new Expression(
			    p_or_m_ungrp.get_operator(),
			    new Expression(
				    new Symbol(Symbol.Specifier.TIMES, ts),
				    new Expression(c),
				    p_or_m_ungrp.get_argument1().ensure_group()
				    ),
			    new Expression(
				    new Symbol(Symbol.Specifier.TIMES, ts),
				    new Expression(c),
				    p_or_m_ungrp.get_argument2().ensure_group()
				    )
			    ).ensure_group()
		    );
		simplify(arg2_ungrp);
		result = true;
		}
	    */

	    // Consider |LinkedList| considering operations
	    // such as |remove(0)| a.k.a. |LinkedList.removeFirst()|
            ArrayList<Expression> terms = get_terms(expr);
            int terms_count_orig = terms.size();
            for ( int ti1 = 0; ti1 < terms.size(); ti1++ ) {
                                // note |terms.size()| can decrease
                Expression
                    term1 = terms.get(ti1),
                    term1_arg1_ungroup =
                        term1.get_argument1() != null
                        ? term1.get_argument1().ungroup()
                        : null,
                    term1_arg2_ungroup =
                        term1.get_argument2() != null
                        ? term1.get_argument2().ungroup()
                        : null;
                // term should be ungroupited considering |get_terms()|
                boolean term1_has_coeff =
                    term1.op_spec_equals(Symbol.Specifier.TIMES)
                    &&  term1_arg1_ungroup.op_spec_equals(
                            Symbol.Specifier.INT
                            );
                for ( int ti2 = ti1 + 1; ti2 < terms.size(); ti2++ ) {
                    Expression
                        term2 = terms.get(ti2),
                        term2_arg1_ungroup =
                            term2.get_argument1() != null
                            ? term2.get_argument1().ungroup()
                            : null,
                        term2_arg2_ungroup =
                            term2.get_argument2() != null
                            ? term2.get_argument2().ungroup()
                            : null;
                    // term should be ungroupited considering |get_terms()|
                    boolean term2_has_coeff =
                        term2.op_spec_equals(Symbol.Specifier.TIMES)
                        &&  term2_arg1_ungroup.op_spec_equals(
                                Symbol.Specifier.INT
                                );
                    Expression collected_term = null;
                    if ( term1_has_coeff )
                        if ( term2_has_coeff ) {
                            if ( term1_arg2_ungroup
                                    .equivalent_form(term2_arg2_ungroup)
                                    )
                                {
                                term1_arg1_ungroup
                                    .this_structure_replace(
					term1_arg1_ungroup.get_val()
					+ term2_arg1_ungroup.get_val()
					);
                                collected_term = term1;
                                }
                            }
                        else {
                            if ( term1_arg2_ungroup.equivalent_form(term2) ) {
                                term1_arg1_ungroup
                                    .this_structure_replace(
					term1_arg1_ungroup.get_val() + 1
					);
                                collected_term = term1;
                                }
                            }
                    else if ( term2_has_coeff ) {
                        if ( term1.equivalent_form(term2_arg2_ungroup) ) {
                            term2_arg1_ungroup
                                .this_structure_replace(
				    term2_arg1_ungroup.get_val() + 1
				    );
                            collected_term = term2;
                            }
                        }
                    else if ( term1.op_spec_equals(Symbol.Specifier.INT)
                               && term2.op_spec_equals(Symbol.Specifier.INT)
                               )
                        collected_term =
                            new Expression(
				    term1.get_val() + term2.get_val()
				    );
                    else if ( term1.equivalent_form(term2) )
                        collected_term =
                            new Expression(
                                new_Symbol(Symbol.Specifier.TIMES),
                                new Expression(2),
                                (Expression) term1.clone()
                                    // |clone()| to avoid aliasing:
                                    // once had a term "a" replaced with "2*a"
                                    // i.e. <term>'s members changed to
				    // {"*", "2", "<term>"}, which makes
				    // a recursive structure --- problematic
                                );
                    if ( collected_term != null ) {
			simplify(collected_term);
                        terms.remove(ti2--);
                        term1.this_structure_replace(collected_term);
			}
                    }
		if ( term1.op_spec_equals(Symbol.Specifier.TIMES)
			&&  term1.get_argument1()
				.ungrp_op_spec_equals(Symbol.Specifier.INT)
			&&  term1.get_argument1().ungroup().get_val() == -1
			)
		    term1.this_structure_replace(
			new_Symbol(Symbol.Specifier.NEGATIVE),
			term1.get_argument2()
			);
                }
            for ( int i = terms.size() - 1; i >= 0; i-- )
                if ( terms.get(i).ungrp_op_spec_equals(Symbol.Specifier.INT)
                        &&  terms.get(i).ungroup().get_val()
                            ==
                            0
                        )
                    terms.remove(i);
            if ( terms.size() < terms_count_orig ) {
                Expression ct = 
                        terms.isEmpty()
                        ? new Expression(0)
                        : terms.remove(0);
                for ( Expression t : terms ) {
		    Symbol op;
		    int coeff;
		    if ( t.op_spec_equals(Symbol.Specifier.INT)
			    &&  (coeff = t.get_val()) < 0
			    )
			{
			t = new Expression(Math.abs(coeff));	// -coeff
			op = new_Symbol(Symbol.Specifier.MINUS);
			}
		    else if ( t.op_spec_equals(Symbol.Specifier.NEGATIVE) ) {
			t = t.get_argument1();
			op = new_Symbol(Symbol.Specifier.MINUS);
			}
		    else if ( t.op_spec_equals(Symbol.Specifier.TIMES)
                                &&  t.get_argument1()
					.ungrp_op_spec_equals(Symbol.Specifier.INT)
				&&  (coeff =
					t.get_argument1().ungroup().get_val()
					)
				    < 0
                                )
			{
			t.get_argument1().this_structure_replace(-coeff);
			op = new_Symbol(Symbol.Specifier.MINUS);
			}
		    else
			op = new_Symbol(Symbol.Specifier.PLUS);
                    ct = new Expression(op, ct, t);
		    }
                return  expr.this_structure_replace(ct);
				// I think this is safe
                }
            return result;
            }

        if ( expr.op_spec_equals(Symbol.Specifier.TIMES) ) {
	    // Assuming argument1 and argument2 are each simplified
	    // as this code does: first coefficient if any, and then
	    // factors are collected with exponents.

            LinkedList<Expression>
		factors1 =
		    expr.get_argument1().multiary_op_args(
			Symbol.Specifier.TIMES
			),
		factors2 =
		    expr.get_argument2().multiary_op_args(
			Symbol.Specifier.TIMES
			);

	    boolean local_result = false;
	    Stack<Expression> factors_simp = new Stack<Expression>();

	    int coefficient1 = 1;
	    if ( factors1.getFirst().ungrp_op_spec_equals(Symbol.Specifier.INT)
		    )
		{
		coefficient1 = factors1.removeFirst().ungroup().get_val();
		local_result =  coefficient1 == 1;
				// See below regarding 0.
		}
	    int coefficient2 = 1;
	    if ( factors2.getFirst().ungrp_op_spec_equals(Symbol.Specifier.INT)
		    )
		{
		coefficient2 = factors2.removeFirst().ungroup().get_val();
		local_result = true;
		}
				// SHOULD CHECK FOR OVERFLOW
				// SAY BY STORING PRODUCT IN A |long|
				// AND THEN COMPARING TO |Integer.MAX_VALUE|
	    int coefficient = coefficient1 * coefficient2;
	    if ( coefficient == 0 )
		return  expr.this_structure_replace(0);
	    if ( coefficient != 1 )
		/* This took the item out of the picture, so missed e.g. 2*2^X.
		factors_simp.push(new Expression(coefficient));
		 */
		factors1.addFirst(new Expression(coefficient));

	    for ( Expression factor1;
		    !factors1.isEmpty()
		    	// ~~kludging this assignment into the condition here.
			// (In a language more like C, the condition would
			// just be the assignment, compared against 0/NULL.
			// Now, I could do it anyway and catch the
			// exception (or make my own ~~macro doing such);
			// but I think that would look worse.)
		    &&  (factor1 = factors1.removeFirst()) != null;
		    )
		{
		Expression exponent1 = null, base1 = factor1;
		if ( base1.ungrp_op_spec_equals(Symbol.Specifier.EXP) ) {
		    exponent1 = factor1.ungroup().get_argument2().ungroup();
		    base1 = factor1.ungroup().get_argument1();
		    }
		// One might think 'greediness' here (i.e. readiness to focus
		// on the expressions being raised to exponents) might engender
		// missing things such as  (X^Y)*[(X^Y)^Z]
		// but that would be simplifiable only if Y and Z were INTs
		// in which case [(X^Y)^Z] should have been
		// already simplified to [X^W], where W is the INT value Y*Z,
		// and then the simplification here applies to (X^Y)*[X^W].
		for ( ListIterator<Expression> factors2_it
			    = factors2.listIterator();
			factors2_it.hasNext();
			)
		    {
		    Expression
			exponent2 = null,
			factor2 = factors2_it.next(),
			base2 = factor2;
		    if ( base2.ungrp_op_spec_equals(Symbol.Specifier.EXP) ) {
			exponent2 = factor2.ungroup().get_argument2().ungroup();
			base2 = factor2.ungroup().get_argument1();
			}
		    if ( base1.equivalent_form(base2) ) {
			local_result = true;
			Expression exponent;
			if ( exponent1 != null
				    && !exponent1.op_spec_equals(
						    Symbol.Specifier.INT
						    )
				|| exponent2 != null
				    && !exponent2.op_spec_equals(
						    Symbol.Specifier.INT
						    )
				)
			    exponent =
				new Expression(
					new_Symbol(Symbol.Specifier.PLUS),
					/*
					exponent1 == null
					    ?  new Expression(1)
					    :  exponent1,
					exponent2 == null
					    ?  new Expression(1)
					    :  exponent2
					*/
					exponent1 == null
					    ?  exponent2
					    :  exponent1,
					exponent1 == null
					    ?  new Expression(1)
					    :  exponent2 == null
						?  new Expression(1)
						:  exponent2
					)
				    .ensure_group();
			else
			   /*
			   ( (exponent1 == null
				    || exponent1.op_spec_equals(
						    Symbol.Specifier.INT
						    )
				    )
				&& (exponent2 == null
				    || exponent2.op_spec_equals(
						    Symbol.Specifier.INT
						    )
				    )
				)
			    */
			    {
			    int exponent1_val =
				    exponent1 == null ? 1 : exponent1.get_val(),
			        exponent2_val =
				    exponent2 == null ? 1 : exponent2.get_val();
			    exponent =
				new Expression(
					new Symbol(
						Symbol.Specifier.INT,
						Symbol.superscript(
							exponent1_val
							+ exponent2_val
							)
						)
					);
			    }
			factor1 =
			    new Expression(
				exponent.op_spec_equals(Symbol.Specifier.INT)
				    ? new Symbol(Symbol.Specifier.EXP, "")
				    : exponent1 != null
					? factor1.ungroup().get_operator()
					: factor2.ungroup().get_operator(),
				(exponent2 != null  ?  base2  :  base1)
				    .ensure_group(),
				exponent
				);
			simplify(factor1);
			factors2_it.remove();
			break;
			}
		    }
		factors_simp.push(factor1);
		}
	    if ( local_result ) {
		result = true;
		Expression expr_simp;
		factors_simp.addAll(factors2);
		if ( factors_simp.isEmpty() )
		    return  expr.this_structure_replace(1);
		for ( expr_simp = factors_simp.pop().ensure_group();
			!factors_simp.isEmpty();
			)
		    expr_simp =
			// conforming to right-associativity used for TIMES
			new Expression(expr.get_operator(),
					factors_simp.pop().ensure_group(),
					expr_simp
					);
		expr.this_structure_replace(expr_simp);
		}
	    return  result;
            }

        if ( expr.get_argument1() != null
                &&  expr.get_argument1()
			.ungrp_op_spec_equals(Symbol.Specifier.INT)
                &&  expr.get_argument2() != null
                &&  expr.get_argument2()
			.ungrp_op_spec_equals(Symbol.Specifier.INT)
                )
            {
            if ( expr.get_operator().is_numeric_comparator() )
                return
                    expr.this_structure_replace(
			new_Symbol(
			    expr.op_spec_equals(Symbol.Specifier.EQUALS)
				    &&  arg1_val == arg2_val
				||  expr.op_spec_equals(Symbol.Specifier.NEQ)
				    &&  arg1_val != arg2_val
				||  expr.op_spec_equals(Symbol.Specifier.LEQ)
				    &&  arg1_val <= arg2_val
				||  expr.op_spec_equals(Symbol.Specifier.GEQ)
				    &&  arg1_val >= arg2_val
				||  expr.op_spec_equals(
					Symbol.Specifier.LESS_THAN
					)
				    &&  arg1_val < arg2_val
				||  expr.op_spec_equals(
					    Symbol.Specifier.GREATER_THAN
					    )
				    &&  arg1_val > arg2_val
				||  expr.op_spec_equals(
					Symbol.Specifier.DIVIDES
					)
				    && (arg1_val == 0
					?  arg2_val == 0
					:  arg2_val % arg1_val == 0
					)
			    ?  Symbol.Specifier.TRUE
			    :  Symbol.Specifier.FALSE
			    )
                        );
            if ( expr.op_spec_equals(Symbol.Specifier.REMAINDER_CODE) ) {
                if ( arg2_val != 0 )
                    return  expr.this_structure_replace(arg1_val % arg2_val);
                return  result;	// consider doing  a|1 := 0  below
                }
            if ( expr.op_spec_equals(Symbol.Specifier.BMOD) ) {
                if ( arg2_val != 0 ) {
		    int rslt = arg1_val % arg2_val;
		    if ( rslt < 0 )
			rslt += arg2_val;
                    return  expr.this_structure_replace(rslt);
		    }
                return  result;	// consider doing  a|1 := 0  below
                }
	    /* COLLECTING TERMS (ABOVE) SHOULD SUPERSEDE THIS:
            if ( expr.op_spec_equals(Symbol.Specifier.MINUS) ) {
                return  expr.this_structure_replace(arg1_val - arg2_val);
                }
            if ( expr.op_spec_equals(Symbol.Specifier.PLUS) )
                return  expr.this_structure_replace(arg1_val + arg2_val);
	    */
	    /* COLLECTING FACTORS (ABOVE) SHOULD SUPERSEDE THIS:
            if ( expr.op_spec_equals(Symbol.Specifier.TIMES) )
                return  expr.this_structure_replace(arg1_val * arg2_val);
	    */
            if ( expr.op_spec_equals(Symbol.Specifier.QUOTIENT) ) {
                if ( arg2_val != 0  &&  arg1_val % arg2_val == 0 )
                    return  expr.this_structure_replace(arg1_val / arg2_val);
                return  result;
                }
            if ( expr.op_spec_equals(Symbol.Specifier.EXP) ) {
                if ( (arg1_val != 0  ||  arg2_val != 0)
                        &&  Math.pow(arg1_val, arg2_val) <= Integer.MAX_VALUE
                        )
                    return
                        expr.this_structure_replace(
                            (int) Math.pow(arg1_val, arg2_val)
                            );
                }

	    return  result;
            }

        if ( expr.op_spec_equals(Symbol.Specifier.DIVIDES) ) {
            if ( arg1_val == 1
		    ||  arg2_val == 0
		    ||  expr.get_argument2()
			    .ungrp_op_spec_equals(Symbol.Specifier.TIMES)
			&&  (expr.get_argument1().equivalent_form_contained_in(
				    expr.get_argument2().ungroup()
				    .multiary_op_args()
				    )
				||  expr.get_argument2().ungroup()
					.get_argument1()
					.ungrp_op_spec_equals(
					    Symbol.Specifier.INT
					    )
				    &&  expr.get_argument1()
					    .ungrp_op_spec_equals(
						Symbol.Specifier.INT
						)
				    &&  arg1_val != 0
				    &&  expr.get_argument2().ungroup()
						.get_argument1().ungroup()
						    .get_val()
					    % arg1_val
					== 0
				)
		    )
                return
		    expr.this_structure_replace(
			new_Symbol(Symbol.Specifier.TRUE)
			);
            return  result;
            }

	if ( expr.get_operator().is_numeric_comparator() ) {
	    if ( expr.get_argument1().equivalent_form(expr.get_argument2()) )
			    // consider |unify()|
                return
                    expr.this_structure_replace(
			new_Symbol(
			    expr.op_spec_equals(Symbol.Specifier.EQUALS)
				||  expr.op_spec_equals(Symbol.Specifier.LEQ)
				||  expr.op_spec_equals(Symbol.Specifier.GEQ)
				||  expr.op_spec_equals(Symbol.Specifier.DIVIDES
							)
			    ?  Symbol.Specifier.TRUE
			    :  Symbol.Specifier.FALSE
			    )
                        );

	    // Handle relationships such as "2x < 4", "2 < 4x", "2x < 4y":
	    int coefficient1 = 1;
	    Expression main_term1 = expr.get_argument1();
	    if ( main_term1.ungrp_op_spec_equals(Symbol.Specifier.NEGATIVE) ) {
		coefficient1 = -1;
		main_term1 = main_term1.ungroup().get_argument1();
		}
	    if ( main_term1.ungrp_op_spec_equals(Symbol.Specifier.TIMES)
		    && main_term1.ungroup().get_argument1()
			.ungrp_op_spec_equals(Symbol.Specifier.INT)
		    )
		{
		coefficient1 *=
		    main_term1.ungroup().get_argument1().ungroup().get_val();
		main_term1 = main_term1.ungroup().get_argument2();
		}
	    int coefficient2 = 1;
	    Expression main_term2 = expr.get_argument2();
	    if ( main_term2.ungrp_op_spec_equals(Symbol.Specifier.NEGATIVE) ) {
		coefficient2 = -1;
		main_term2 = main_term2.ungroup().get_argument1();
		}
	    if ( main_term2.ungrp_op_spec_equals(Symbol.Specifier.TIMES)
		    && main_term2.ungroup().get_argument1()
			.ungrp_op_spec_equals(Symbol.Specifier.INT)
		    )
		{
		coefficient2 *=
		    main_term2.ungroup().get_argument1().ungroup().get_val();
		main_term2 = main_term2.ungroup().get_argument2();
		}
	    int common_factor_coeffs =
		common_factor(coefficient1, coefficient2);
	    if ( common_factor_coeffs != 1  &&  common_factor_coeffs != 0 ) {
	    					// e.g. "x > 0"
		expr.this_structure_replace(
		    common_factor_coeffs < 0
			? new_Symbol(
			    expr.get_operator().reverse_numeric_comparator()
			    )
			: expr.get_operator(),
		    new Expression(
			new_Symbol(Symbol.Specifier.TIMES),
			new Expression(coefficient1 / common_factor_coeffs),
			main_term1
			),
		    new Expression(
			new_Symbol(Symbol.Specifier.TIMES),
			new Expression(coefficient2 / common_factor_coeffs),
			main_term2
			)
		    );
		simplify(expr);
		return  true;
		}

	    if ( expr.op_spec_equals(Symbol.Specifier.DIVIDES) )
		// Following code not appropriate for |DIVIDES|.
		return  result;

	    // Handle relationships such as "k + 3 < 2":
	    if ( expr.get_argument2()
			.ungrp_op_spec_equals(Symbol.Specifier.INT)
			)
		{
		if ( expr.get_argument1()
			    .ungrp_op_spec_equals(Symbol.Specifier.PLUS)
			&&  expr.get_argument1().ungroup()
				.get_argument2()
			    .ungrp_op_spec_equals(Symbol.Specifier.INT)
			)
		    {
		    expr.get_argument2().this_structure_replace(
			    expr.get_argument2().ungroup().get_val()
			    - expr.get_argument1().ungroup()
				    .get_argument2().ungroup().get_val()
			    );
		    expr.get_argument1().this_structure_replace(
			    expr.get_argument1().ungroup().get_argument1()
			    );
		    return  true;
		    }
		if ( expr.get_argument1()
			    .ungrp_op_spec_equals(Symbol.Specifier.MINUS)
			&&  expr.get_argument1().ungroup()
				.get_argument2()
			    .ungrp_op_spec_equals(Symbol.Specifier.INT)
			)
		    {
		    expr.get_argument2().this_structure_replace(
			    expr.get_argument2().ungroup().get_val()
			    + expr.get_argument1().ungroup()
				    .get_argument2().ungroup().get_val()
			    );
		    expr.get_argument1().this_structure_replace(
			    expr.get_argument1().ungroup().get_argument1()
			    );
		    return  true;
		    }
		}
	    if ( expr.get_argument1()
			.ungrp_op_spec_equals(Symbol.Specifier.INT)
			)
		{
		if ( expr.get_argument2()
			    .ungrp_op_spec_equals(Symbol.Specifier.PLUS)
			&&  expr.get_argument2().ungroup()
				.get_argument2()
			    .ungrp_op_spec_equals(Symbol.Specifier.INT)
			)
		    {
		    expr.get_argument1().this_structure_replace(
			    expr.get_argument1().ungroup().get_val()
			    - expr.get_argument2().ungroup()
				    .get_argument2().ungroup().get_val()
			    );
		    expr.get_argument2().this_structure_replace(
			    expr.get_argument2().ungroup().get_argument1()
			    );
		    return  true;
		    }
		if ( expr.get_argument2()
			    .ungrp_op_spec_equals(Symbol.Specifier.MINUS)
			&&  expr.get_argument2().ungroup()
				.get_argument2()
			    .ungrp_op_spec_equals(Symbol.Specifier.INT)
			)
		    {
		    expr.get_argument1().this_structure_replace(
			    expr.get_argument1().ungroup().get_val()
			    + expr.get_argument2().ungroup()
				    .get_argument2().ungroup().get_val()
			    );
		    expr.get_argument2().this_structure_replace(
			    expr.get_argument2().ungroup().get_argument1()
			    );
		    return  true;
		    }
		}

	    // Handle relationships such as "x + 2 < y + 2":
	    // NEED TO COVER MORE THAN WHAT'S COVERED SO FAR HERE,
	    // E.G. OTHER ARITHMETIC OPERATORS
	    if ( (expr.get_argument1()
				.ungrp_op_spec_equals(Symbol.Specifier.PLUS)
			    && expr.get_argument2()
				.ungrp_op_spec_equals(Symbol.Specifier.PLUS)
			|| expr.get_argument2()
				.ungrp_op_spec_equals(Symbol.Specifier.MINUS)
			    && expr.get_argument1()
				.ungrp_op_spec_equals(Symbol.Specifier.MINUS)
			)
		    &&  expr.get_argument1().ungroup().get_argument2()
			    .equivalent_form(
				expr.get_argument2().ungroup().get_argument2()
				)
		    )
		{
		expr.get_argument1().this_structure_replace(
			expr.get_argument1().ungroup().get_argument1()
			);
		expr.get_argument2().this_structure_replace(
			expr.get_argument2().ungroup().get_argument1()
			);
		return  true;
		}

	    // The following code will set |left_compare_to_right|
	    // positive if left is clearly greater than right,
	    // negative if left is clearly smaller than right,
	    // and otherwise (i.e. not clearly smaller or greater) have it 0:
	    							// leave
	    int left_compare_to_right = 0;
	    if ( expr.get_argument1()
			.ungrp_op_spec_equals(Symbol.Specifier.PLUS)
		    &&  expr.get_argument1().ungroup().get_argument2()
			.ungrp_op_spec_equals(Symbol.Specifier.INT)
		    &&  expr.get_argument1().ungroup().get_argument1()
			.equivalent_form(expr.get_argument2())
		    )
		left_compare_to_right = 
		    expr.get_argument1().ungroup().get_argument2().ungroup()
			    .get_val();
	    else if ( expr.get_argument1()
			.ungrp_op_spec_equals(Symbol.Specifier.MINUS)
		    &&  expr.get_argument1().ungroup().get_argument2()
			.ungrp_op_spec_equals(Symbol.Specifier.INT)
		    &&  expr.get_argument1().ungroup().get_argument1()
			.equivalent_form(expr.get_argument2())
		    )
		left_compare_to_right = 
		    -expr.get_argument1().ungroup().get_argument2().ungroup()
			    .get_val();
	    else if ( expr.get_argument2()
			.ungrp_op_spec_equals(Symbol.Specifier.PLUS)
		    &&  expr.get_argument2().ungroup().get_argument2()
			.ungrp_op_spec_equals(Symbol.Specifier.INT)
		    &&  expr.get_argument2().ungroup().get_argument1()
			.equivalent_form(expr.get_argument1())
		    )
		left_compare_to_right = 
		    -expr.get_argument2().ungroup().get_argument2().ungroup()
			    .get_val();
	    else if ( expr.get_argument2()
			.ungrp_op_spec_equals(Symbol.Specifier.MINUS)
		    &&  expr.get_argument2().ungroup().get_argument2()
			.ungrp_op_spec_equals(Symbol.Specifier.INT)
		    &&  expr.get_argument2().ungroup().get_argument1()
			.equivalent_form(expr.get_argument1())
		    )
		left_compare_to_right = 
		    expr.get_argument2().ungroup().get_argument2().ungroup()
			    .get_val();
	    if ( left_compare_to_right != 0 )	// Rem. "<>"? (;-)
                return
                    expr.this_structure_replace(
			new_Symbol(
				expr.op_spec_equals(Symbol.Specifier.NEQ)
				||  expr.op_spec_equals(Symbol.Specifier.LEQ)
				    &&  left_compare_to_right < 0
				||  expr.op_spec_equals(Symbol.Specifier.GEQ)
				    &&  left_compare_to_right < 0
				||  expr.op_spec_equals(
					Symbol.Specifier.LESS_THAN
					)
				    &&  left_compare_to_right < 0
				||  expr.op_spec_equals(
					    Symbol.Specifier.GREATER_THAN
					    )
				    &&  left_compare_to_right > 0
			    ?  Symbol.Specifier.TRUE
			    :  Symbol.Specifier.FALSE
			    )
                        );
	    return  result;
	    }

        if ( expr.op_spec_equals(Symbol.Specifier.IS_IN) ) {
	    if ( expr.get_argument1().ungroup()
			.op_spec_equals(Symbol.Specifier.INT)
		   &&  (expr.get_argument2().ungroup()
				.op_spec_equals(Symbol.Specifier.N_NUMBERS)
			||  expr.get_argument2().ungroup()
				.op_spec_equals(Symbol.Specifier.Z_NUMBERS)
			||  expr.get_argument2().ungroup()
				.op_spec_equals(Symbol.Specifier.Q_NUMBERS)
			||  expr.get_argument2().ungroup()
				.op_spec_equals(Symbol.Specifier.R_NUMBERS)
			||  expr.get_argument2().ungroup()
				.op_spec_equals(Symbol.Specifier.C_NUMBERS)
			)
		    )
		return
		    expr.this_structure_replace(
			new_Symbol(
			    expr.get_argument2().ungroup().op_spec_equals(
					Symbol.Specifier.N_NUMBERS
					)
				&&  expr.get_argument1().ungroup().get_val()
				    < (start_N_at_1 ? 1 : 0)
			    ?  Symbol.Specifier.FALSE
			    :  Symbol.Specifier.TRUE
			    )
			);

            if ( expr.get_argument2()
			.op_spec_equals(Symbol.Specifier.OPENING_DELIMITER)
		    &&  expr.get_argument2().get_operator().get_text()
			    .equals("{")
		    )
		{
		Expression
		    item = expr.get_argument1().ungroup(),
		    content =
			expr.get_argument2().get_argument1().ungroup();
		if ( !content.op_spec_equals(Symbol.Specifier.SUCH_THAT) ) {
		    LinkedList<Expression> elements
			= content.multiary_op_args(Symbol.Specifier.COMMA);
		    boolean elements_are_ints_or_sets = true;
		    for ( Expression element : elements ) {
			if ( item.equivalent_form(element) )
			    return
				expr.this_structure_replace(
					new_Symbol(Symbol.Specifier.TRUE)
					);
			elements_are_ints_or_sets &=
			    element.ungrp_op_spec_equals(
				    Symbol.Specifier.INT
				    )
			    ||  element.ungrp_op_spec_equals(
					Symbol.Specifier.OPENING_DELIMITER
					)
				&&  element.ungroup().get_operator().get_text()
					    .equals("{");
			}
		    if ( item.op_spec_equals(Symbol.Specifier.INT)
				&&  elements_are_ints_or_sets
				)
			    return
				expr.this_structure_replace(
					new_Symbol(Symbol.Specifier.FALSE)
					);
		    }
		else	// content.op_spec_equals(Symbol.Specifier.SUCH_THAT)
		    if ( content.get_argument1()
				    .op_spec_equals(Symbol.Specifier.IDENTIFIER)
			    &&  content.get_argument1().get_argument1() == null
			    )
		    {
		    content.get_argument2()
			    .replace_throughout_scope(
				content.get_argument1()
					.get_operator().get_text(),
				item
				);
		    return
			expr.this_structure_replace(content.get_argument2());
		    }
		}
            return  result;
            }

        if ( expr.op_spec_equals(Symbol.Specifier.BMOD) ) {
            if ( arg2_val == 1 )
                return  expr.this_structure_replace(0);
            return  result;
            }

        if ( expr.op_spec_equals(Symbol.Specifier.QUOTIENT) ) {
            if ( arg2_val == 1 )
		// I think it's not worth combining this simplification
		// with the canceling below.  For example, this preserves
		// grouping of factors.
                return  expr.this_structure_replace(expr.get_argument1());

	    if ( arg2_val == 0 )
		return  result;

	    // Remember this is removing common factors.  If someone already
	    // has an expression such as (xy)/(xz), then I think it's fair for
	    // me to assume that they think x isn't zero.
	    LinkedList<Expression>
		factors_num = expr.get_argument1().multiary_op_args(
		    Symbol.Specifier.TIMES
		    ),
		factors_denom = expr.get_argument2().multiary_op_args(
		    Symbol.Specifier.TIMES
		    );
	    boolean canceled = false;	// local_result
	    for ( ListIterator<Expression> factorsnum_it =
			factors_num.listIterator();
		    factorsnum_it.hasNext();
		    )
		{
		Expression factor_num = factorsnum_it.next();
		for ( ListIterator<Expression> factorsdenom_it =
			    factors_denom.listIterator();
			factorsdenom_it.hasNext();
			)
		    {
		    Expression factor_denom = factorsdenom_it.next();
		    if ( factor_denom.equivalent_form(factor_num) ) {
			factorsdenom_it.remove();
			factorsnum_it.remove();
			canceled = true;
			}
		    }
		}
	    if ( canceled ) {
		if ( factors_num.isEmpty() && factors_denom.isEmpty() )
		    return  expr.this_structure_replace(1);
		Expression numerator;
		if ( factors_num.isEmpty() )
		    numerator = new Expression(1);
		else {
		    numerator = factors_num.removeLast();
		    while ( !factors_num.isEmpty() )
			// conforming to right-associativity used for TIMES
			numerator =
			    new Expression(
				expr.get_argument1().ungroup().get_operator(),
				factors_num.removeLast().ensure_group(),
				numerator
				);
		    }
		Expression denominator;
		if ( factors_denom.isEmpty() )
		    denominator = null;
		else {
		    denominator = factors_denom.removeLast();
		    while ( !factors_denom.isEmpty() )
			// conforming to right-associativity used for TIMES
			denominator =
			    new Expression(
				expr.get_argument2().ungroup().get_operator(),
				factors_denom.removeLast().ensure_group(),
				denominator
				);
		    }
		return
		    denominator == null
		    ?  expr.this_structure_replace(numerator)
		    :  expr.this_structure_replace(
			expr.get_operator(),
			numerator,
			denominator
			);
		}

            return  result;
            }

        if ( expr.op_spec_equals(Symbol.Specifier.EXP) ) {
            // Though it's difficult to know that arbitrary expression
            // is not zero, for binomial expansion 0^0 should be 1.
	    // (Mathematics by fiat! ;-)
            if ( arg2_val == 0  &&  arg1_val != 0 )
                return  expr.this_structure_replace(1);
            if ( arg1_val == 0  &&  arg2_val != 0 )
                return  expr.this_structure_replace(0);
	    if ( arg1_val == 1 )
		return  expr.this_structure_replace(1);
            if ( arg2_val == 1 )
                return  expr.this_structure_replace(expr.get_argument1());
            return  result;
            }

        if ( expr.op_spec_equals(Symbol.Specifier.FACTORIAL) ) {
            if ( arg1_val >= 0 ) {
                int result_val = -1;
                switch ( arg1_val ) {
                    case  0:  result_val = 1;  break;
                    case  1:  result_val = 1;  break;
                    case  2:  result_val = 2;  break;
                    case  3:  result_val = 6;  break;
                    case  4:  result_val = 24;  break;
                    case  5:  result_val = 120;  break;
                    case  6:  result_val = 720;  break;
                    case  7:  result_val = 5040;  break;
                    case  8:  result_val = 40320;  break;
                    case  9:  result_val = 362880;  break;
                    case 10:  result_val = 3628800;  break;
                    case 11:  result_val = 39916800;  break;
                    case 12:  result_val = 47900160;  break;
                    }
                if ( result_val != -1 )
                    return  expr.this_structure_replace(result_val);
                }
            return  result;
            }

        if ( expr.op_spec_equals(Symbol.Specifier.NEGATIVE) ) {
            if ( expr.get_argument1()
		    .ungrp_op_spec_equals(Symbol.Specifier.INT)
		    )
                return  expr.this_structure_replace(-arg1_val);
            if ( expr.get_argument1()
		    .ungrp_op_spec_equals(Symbol.Specifier.NEGATIVE)
		    )
                return
		    expr.this_structure_replace(
			    expr.get_argument1().ungroup().get_argument1()
			    );
            return  result;
            }

        if ( expr.op_spec_equals(Symbol.Specifier.LN) ) {
            if ( arg1_val == 1 )
                return  expr.this_structure_replace(0);
            return  result;
            }

        else if ( expr.op_spec_equals(Symbol.Specifier.LOG10) ) {
            if ( arg1_val > 0 ) {
                int result_val = -1;
                switch ( arg1_val ) {
                    case 1:  result_val = 0;  break;
                    case 10:  result_val = 1;  break;
                    case 100:  result_val = 2;  break;
                    case 1000:  result_val = 3;  break;
                    case 10000:  result_val = 4;  break;
                    case 100000:  result_val = 5;  break;
                    case 1000000:  result_val = 6;  break;
                    case 10000000:  result_val = 7;  break;
                    case 100000000:  result_val = 8;  break;
                    case 1000000000:  result_val = 9;  break;
                    }
                if ( result_val != -1 )
                    return  expr.this_structure_replace(result_val);
                }
            return  result;
            }

        if ( expr.op_spec_equals(Symbol.Specifier.LG) ) {
            if ( arg1_val > 0 ) {
                int result_val = -1;
                switch ( arg1_val ) {
                    case 1:  result_val = 0;  break;
                    case 2:  result_val = 1;  break;
                    case 4:  result_val = 2;  break;
                    case 8:  result_val = 3;  break;
                    case 16:  result_val = 4;  break;
                    case 32:  result_val = 5;  break;
                    case 64:  result_val = 6;  break;
                    case 128:  result_val = 7;  break;
                    case