import java.util.*;

public class ModLattice {

    public static int DEPTH = 5;       //complexity of computations
    public static int DEPTH2 = 5;      //used when answer is already known
    public static int M = 100;      //M and N affect how much work is done
    public static int N = 10;       //in the computeCongruence() method.

    protected Element [][] table;      //join and meet table
    protected int currentRow, currentColumn;   //next position in table to fill
    protected Element [] elements;
    protected int currentSize;
    protected int elementCount;     
    protected int auto;               //number of automorphisms
    protected int [] inverse;    //associates each automorphism to its inverse
    protected EqRel myEqRel;

    public ModLattice(int initialSize, int [] inverse)
    {
        currentSize = initialSize;
        elements = new Element[currentSize];
        table = new Element[currentSize][currentSize];
        currentRow = 0;
        currentColumn = 0;
        this.inverse = inverse;
        auto = inverse.length;
        myEqRel = new EqRel(currentSize);
    }

    public void makeNewElements(int total)
      /* Fills squares in the table, creating new elements when necessary, 
until elementCount equals total.     */
    {
          if (total <= elementCount)
              return;
          if (total > currentSize) {
              System.out.println ("Lattice can't hold that many elements.");
              return;
          }
          try {
              do {
                  fillCurrentSquare();
                  updatePointer();
              }
              while (total > elementCount);
          } catch(TableCompleteException e) {
              System.out.println("Lattice completed with " + elementCount + " elements.");
          }
          computeAllConjugates();
    } //makeNewElements

    protected void updatePointer() throws TableCompleteException
    {
       if (currentRow == currentColumn) {
            currentRow = 0;
            currentColumn++;
            if (currentColumn == elementCount)
               throw new TableCompleteException();
       }
       else if (currentRow < currentColumn) {
            currentRow++;
            if (currentRow == currentColumn)
                currentColumn = 0;
       }
       else
            currentColumn++;
    }

    protected Element join(Element e1, Element e2)
    {
        return join(e1.myNumber, e2.myNumber);
    }

    protected Element join(int x, int y)
    {
        if (x < y)
            return table[x][y];
        else
            return table[y][x];
    }

    protected Element meet(Element e1, Element e2)
    {
        return meet(e1.myNumber, e2.myNumber);
    }

    protected Element meet(int x, int y)
    {
        if (x > y)
            return table[x][y];
        else
            return table[y][x];
    }

    protected void identify(Element a, Element b)
    {
        if (a != b && a != null && b != null) 
            myEqRel.relate(a.myNumber, b.myNumber);
    }

    public boolean computeConjugate(Element e, int i)
    //return value indicates if conjugate was successfully computed
    {
        Element answer;
        int alt;

        if (e.myTerm.op != 'v' && e.myTerm.op != '^')
            return true;           //variables should have their conjugates already entered manually
        answer = computeConjugate(e.myTerm, i);
        for (alt = 0; answer == null && alt < e.altsUsed; alt++) 
             answer = computeConjugate(e.altTerms[alt], i);
        if (answer == null)
             return false;
        if (e.conjugates[i] == null)
             e.conjugates[i] = answer;
        else
             identify(e.conjugates[i], answer);
        return true;
    }

    public void computeAllConjugates()
    {
         for (int i = 0; i < auto; i++)
             for (int j = 0; j < elementCount; j++)
                 computeConjugate(elements[j], i);
    }

    private Element computeConjugate(Term aTerm, int i)
    {
        Element e1 = aTerm.arg1.conjugates[i];
        Element e2 = aTerm.arg2.conjugates[i];
        if (e1 == null || e2 == null)
            return null;
        return (aTerm.op == '^') ? meet(e1, e2) : join(e1, e2);
    }

/*
      Term types
1 a v b v c v d
2 a v b v (c ^ d)
3 (a ^ b) v (c ^ d)
4 a v ((b v c) ^ d)
5 a v (b ^ c ^ d)
6 a v b v c                       only c can be fresh
7 a v (b ^ c)                    only a and c can be fresh
8 a v b                             only b can be fresh
9 a ^ b ^ c ^ d
10 a ^ b ^ (c v d)
11 (a v b) ^ (c v d)
12 a ^ ((b ^ c) v d)
13 a ^ (b v c v d)
14 a ^ b ^ c                       only c can be fresh
15 a ^ (b v c)                    only a and c can be fresh
16 a ^ b                             only b can be fresh
*/

    void fillCurrentSquare()
    {
        Vector termResults = new Vector(10);
        Vector elementResults = new Vector(10);
        Vector unknownTerms = new Vector(10);
        char op = (currentRow < currentColumn) ? 'v' : '^';
        Element lhs = elements[currentRow];
        Element rhs = elements[currentColumn];
        Element newElement;
        char leftOp = lhs.myTerm.op;
        char rightOp = rhs.myTerm.op;
        boolean leftVar = (leftOp != 'v' && leftOp != '^');
        boolean rightVar = (rightOp != 'v' && rightOp != '^');

        if (handleTrivialCases(op, leftOp, rightOp, lhs, rhs))
            return;    //We don't do any more calculation in the trivial cases.
        preparation(op, lhs, rhs, elementResults);
        handleEasyCases(op, lhs, rhs, leftOp, rightOp, elementResults);
        dispatchOnOps(op, lhs, rhs, leftOp, rightOp, leftVar, rightVar, termResults, elementResults);
        turnTermsToElements(termResults, elementResults, unknownTerms);
        if (elementResults.size() == 0) 
            elementResults.addElement(makeNewElement(op, lhs, rhs));
        if (elementResults.size() > 1) 
            for (int i = 1; i < elementResults.size(); i++)
                identify((Element) elementResults.elementAt(0), (Element) elementResults.elementAt(i));
        table[currentRow][currentColumn] = (Element) elementResults.elementAt(0);
        fillOtherSquares(unknownTerms);
    }  //fillCurrentSquare

    boolean handleTrivialCases(char op, char leftOp, char rightOp, Element lhs, Element rhs)
      //Returns true if a trivial case was detected.
    {
        if (leftOp == '0') {
            table[currentRow][currentColumn] = (op == 'v') ? rhs : lhs;
	    return true;
        }
        if (rightOp == '0') {
            table[currentRow][currentColumn] = (op == 'v') ? lhs : rhs;
	    return true;
        }
        if (leftOp == '1') {
            table[currentRow][currentColumn] = (op == '^') ? rhs : lhs;
	    return true;
        }
        if (rightOp == '1') {
            table[currentRow][currentColumn] = (op == 'v') ? rhs : lhs;
	    return true;
        }
        if (currentRow == currentColumn) {
            table[currentRow][currentRow] = elements[currentRow];
	    return true;
        }
        return false;
    }  //handleTrivialCases

    protected void preparation(char op, Element lhs, Element rhs, Vector elementResults)
    {
        Element conj1, conj2, conj;

        if (table[currentRow][currentColumn] != null)
            elementResults.addElement(table[currentRow][currentColumn]);
        for (int i = 0; i < auto; i++) {
            conj1 = lhs.conjugates[i];
            conj2 = rhs.conjugates[i];
            if (conj1 != null && conj2 != null) {
                conj = (op == 'v') ? join(conj1, conj2) : meet(conj1, conj2);
                if (conj != null && conj.conjugates[inverse[i]] != null)
                    elementResults.addElement(conj.conjugates[inverse[i]]);
            }
        }
    }

    void handleEasyCases(char op, Element lhs, Element rhs, char leftOp, char rightOp, Vector elementResults)
    {
        Element leftArg1 = lhs.myTerm.arg1;
        Element leftArg2 = lhs.myTerm.arg2;
        Element rightArg1 = rhs.myTerm.arg1;
        Element rightArg2 = rhs.myTerm.arg2;

        if (op == 'v') {
            if (rightOp == '^' && (rightArg1 == lhs || rightArg2 == lhs))
                elementResults.addElement(lhs);
            if (leftOp == '^' && (leftArg1 == rhs || leftArg2 == rhs))
                elementResults.addElement(rhs);
            if (leftOp == '^' && rightOp == 'v' && (leftArg1 == rightArg1 || leftArg1 == rightArg2 || leftArg2 == rightArg1 || leftArg2 == rightArg2))
                elementResults.addElement(rhs);
            if (leftOp == 'v' && rightOp == '^' && (leftArg1 == rightArg1 || leftArg1 == rightArg2 || leftArg2 == rightArg1 || leftArg2 == rightArg2))
                elementResults.addElement(lhs);
         }
         else {  //op == '^' 
            if (rightOp == 'v' && (rightArg1 == lhs || rightArg2 == lhs))
                elementResults.addElement(lhs);
            if (leftOp == 'v' && (leftArg1 == rhs || leftArg2 == rhs))
                elementResults.addElement(rhs);
            if (leftOp == '^' && rightOp == 'v' && (leftArg1 == rightArg1 || leftArg1 == rightArg2 || leftArg2 == rightArg1 || leftArg2 == rightArg2))
                elementResults.addElement(lhs);
            if (leftOp == 'v' && rightOp == '^' && (leftArg1 == rightArg1 || leftArg1 == rightArg2 || leftArg2 == rightArg1 || leftArg2 == rightArg2))
                elementResults.addElement(rhs);
         }
    }  //handleEasyCases

    void dispatchOnOps(char op, Element lhs, Element rhs, char leftOp, char rightOp, boolean leftVar, boolean rightVar, Vector termResults, Vector elementResults)
    {
        Element leftArg1 = lhs.myTerm.arg1;
        Element leftArg2 = lhs.myTerm.arg2;
        Element rightArg1 = rhs.myTerm.arg1;
        Element rightArg2 = rhs.myTerm.arg2;
        int deep = (elementResults.isEmpty()) ? DEPTH : DEPTH2;

        if (op == 'v') 
            if (leftVar)
                if (rightOp == 'v') 
                    handle6(lhs, rightArg1, rightArg2, 0, deep, termResults, elementResults);
                else if (rightOp == '^')
                    handle7(lhs, rightArg1, rightArg2, 0, deep, termResults, elementResults);
                else  //rightVar
                    handle8(lhs, rhs, 0, deep, termResults, elementResults);
            else if (leftOp == 'v')
                if (rightVar)
                    handle6(leftArg1, leftArg2, rhs, 0, deep, termResults, elementResults);
                else if (rightOp == 'v') 
                    handle1(leftArg1, leftArg2, rightArg1, rightArg2, 0, deep, termResults, elementResults);
                else  //rightOp == '^'
                    handle2(leftArg1, leftArg2, rightArg1, rightArg2, 0, deep, termResults, elementResults);
            else  //leftOp == '^'
                if (rightVar)
                    handle7(rhs, leftArg1, leftArg2, 0, deep, termResults, elementResults);
                else if (rightOp == 'v') 
                    handle2(rightArg1, rightArg2, leftArg1, leftArg2, 0, deep, termResults, elementResults);
                else  //rightOp == '^'
                    handle3(leftArg1, leftArg2, rightArg1, rightArg2, 0, deep, termResults, elementResults);
        else     //op == '^'
            if (leftVar)
                if (rightOp == 'v') 
                    handle15(lhs, rightArg1, rightArg2, 0, deep, termResults, elementResults);
                else if (rightOp == '^')
                    handle14(lhs, rightArg1, rightArg2, 0, deep, termResults, elementResults);
                else //rightVar
                    handle16(lhs, rhs, 0, deep, termResults, elementResults);
            else if (leftOp == 'v')
                if (rightVar)
                    handle15(rhs, leftArg1, leftArg2, 0, deep, termResults, elementResults);
                else if (rightOp == 'v') 
                    handle11(leftArg1, leftArg2, rightArg1, rightArg2, 0, deep, termResults, elementResults);
                else  //rightOp == '^'
                    handle10(rightArg1, rightArg2, leftArg1, leftArg2, 0, deep, termResults, elementResults);
            else  //leftOp == '^'
                if (rightVar)
                    handle14(rhs, leftArg1, leftArg2, 0, deep, termResults, elementResults);
                else if (rightOp == 'v') 
                    handle10(leftArg1, leftArg2, rightArg1, rightArg2, 0, deep, termResults, elementResults);
                else  //rightOp == '^'
                    handle9(leftArg1, leftArg2, rightArg1, rightArg2, 0, deep, termResults, elementResults);
    } //dispatchOnOps

    void turnTermsToElements(Vector termResults, Vector elementResults, Vector unknownTerms)
    {
        Element answer;
        Term currentTerm;

        for (int i = 0; i < termResults.size(); i++) {
            currentTerm = (Term) termResults.elementAt(i);
            answer = (currentTerm.op == 'v') ? join(currentTerm.arg1, currentTerm.arg2) : meet(currentTerm.arg1, currentTerm.arg2);
            if (answer == null)
                unknownTerms.addElement(currentTerm);
            else
                elementResults.addElement(answer);
        }
    }

    protected Element makeNewElement(char op, Element lhs, Element rhs)
    {
        Element newElement = new Element(this, op, lhs, rhs);
        for (int i = 0; i < auto; i++)
            computeConjugate(newElement, i);
        return newElement;
    }

    void fillOtherSquares(Vector unknownTerms)
    {
        Term currentTerm;
        int num0 = table[currentRow][currentColumn].myNumber;
        int num1, num2;

        for (int i = 0; i < unknownTerms.size(); i++) {
            currentTerm = (Term) unknownTerms.elementAt(i);
            num1 = currentTerm.arg1.myNumber;
            num2 = currentTerm.arg2.myNumber;
            if (num1 < num0 && num2 < num0)
                table[currentRow][currentColumn].addAlt(currentTerm);
     /* We only want to describe elements in terms of lower-numbered elements, which are 
         presumably simpler.  */
            if (currentTerm.op == 'v')
                if (num1 < num2)
                    table[num1][num2] = table[currentRow][currentColumn];
                else
                    table[num2][num1] = table[currentRow][currentColumn];
            else  // currentTerm.op == '^'
                if (num1 > num2)
                    table[num1][num2] = table[currentRow][currentColumn];
                else
                    table[num2][num1] = table[currentRow][currentColumn];
        } //for
    }  //fillOtherSquares

    void handle1(Element a, Element b, Element c, Element d, int fresh, int deep, Vector termResults, Vector elementResults)
    {
        Element answer1 = join(a, c);
        Element answer2 = join(a, d);
        Element answer3 = join(b, c);
        Element answer4 = join(b, d);

        if (deep <= 0)
            return;

              //join
        if (answer1 != null)
            handle6(b, d, answer1, 3, deep - 1, termResults, elementResults);
        if (answer2 != null)
            handle6(b, c, answer2, 3, deep - 1, termResults, elementResults);        
        if (answer3 != null)
            handle6(a, d, answer3, 3, deep - 1, termResults, elementResults);
        if (answer4 != null)
            handle6(a, c, answer4, 3, deep - 1, termResults, elementResults);
    } //handle1

    void handle2(Element a, Element b, Element c, Element d, int fresh, int deep, Vector termResults, Vector elementResults)
    {
        Element answer1 = meet(c, d);
        Element answer2 = meet(a, c);
        Element answer3 = join(a, c);
        Element answer4 = meet(a, d);
        Element answer5 = join(a, d);
        Element answer6 = meet(b, c);
        Element answer7 = join(b, c);
        Element answer8 = meet(b, d);
        Element answer9 = join(b, d);

        if (deep <= 0)
            return;

             //meet
        if (answer1 != null)
            handle6(a, b, answer1, 3, deep - 1, termResults, elementResults);

             //apply modular law
         if (answer2 == a || answer3 == c)
            handle4(b, a, d, c, 0, deep - 1, termResults, elementResults);
         if (answer4 == a || answer5 == d)
            handle4(b, a, c, d, 0, deep - 1, termResults, elementResults);
         if (answer6 == b || answer7 == c)
            handle4(a, b, d, c, 0, deep - 1, termResults, elementResults);
         if (answer8 == b || answer9 == d)
            handle4(a, b, c, d, 0, deep - 1, termResults, elementResults);
    } //handle2

    void handle3(Element a, Element b, Element c, Element d, int fresh, int deep, Vector termResults, Vector elementResults)
    {
        Element answer2 = meet(a, c);
        Element answer3 = join(a, c);
        Element answer4 = meet(a, d);
        Element answer5 = join(a, d);
        Element answer6 = meet(b, c);
        Element answer7 = join(b, c);
        Element answer8 = meet(b, d);
        Element answer9 = join(b, d);

        if (deep <= 0)
            return;

              //apply modular law
        if (answer2 == a || answer3 == c || answer6 == b || answer7 == c)
            handle12(c, a, b, d, 0, deep - 1, termResults, elementResults);
        if (answer4 == a || answer5 == d || answer8 == b || answer9 == d)
            handle12(d, a, b, c, 0, deep - 1, termResults, elementResults);
        if (answer2 == c || answer3 == a || answer4 == d || answer5 == a)
            handle12(a, c, d, b, 0, deep - 1, termResults, elementResults);
        if (answer6 == c || answer7 == b || answer8 == d || answer9 == b)
            handle12(b, c, d, a, 0, deep - 1, termResults, elementResults);
    } //handle3

    void handle4(Element a, Element b, Element c, Element d, int fresh, int deep, Vector termResults, Vector elementResults)
    {
        Element answer1 = join(b, c);        
        Element answer2 = join(a, d);
        Element answer3 = meet(a, d);

        if (deep <= 0)
            return;

                //join
        if (answer1 != null)
            handle7(a, d, answer1, 3, deep - 1, termResults, elementResults);

                //apply modular law
        if (answer2 == d || answer3 == a)
            handle13(d, a, b, c, 0, deep - 1, termResults, elementResults);
    } //handle4

    void handle5(Element a, Element b, Element c, Element d, int fresh, int deep, Vector termResults, Vector elementResults)
    {
        Element answer1 = meet(b, c);
        Element answer2 = meet(b, d);
        Element answer3 = meet(c, d);
        Element answer4 = meet(a, b);
        Element answer5 = join(a, b);
        Element answer6 = meet(a, c);
        Element answer7 = join(a, c);
        Element answer8 = meet(a, d);
        Element answer9 = join(a, d);

        if (deep <= 0)
            return;

              //meet
        if (answer1 != null)
            handle7(a, d, answer1, 3, deep - 1, termResults, elementResults);
        if (answer2 != null)
            handle7(a, c, answer2, 3, deep - 1, termResults, elementResults);
        if (answer3 != null)
            handle7(a, b, answer3, 3, deep - 1, termResults, elementResults);

                //apply modular law
         if (answer4 == a || answer5 == b)
             handle12(b, c, d, a, 0, deep - 1, termResults, elementResults);
         if (answer6 == a || answer7 == c)
             handle12(c, b, d, a, 0, deep - 1, termResults, elementResults);
         if (answer8 == a || answer9 == d)
             handle12(d, b, c, a, 0, deep - 1, termResults, elementResults);

                //absorb
         if (a == b || a == c || a == d)
             elementResults.addElement (a);
    } //handle5

    void handle6(Element a, Element b, Element c, int fresh, int deep, Vector termResults, Vector elementResults)
    {
        Element answer1 = join(a, b);
        Element answer2 = join(a, c);
        Element answer3 = join(b, c);
        int i;
        Term t;

        if (deep <= 0)
            return;

                //join
        if (answer1 != null)
            handle8(c, answer1, 2, deep - 1, termResults, elementResults);
        if (answer2 != null)
            handle8(b, answer2, 2, deep - 1, termResults, elementResults);
        if (answer3 != null)
            handle8(a, answer3, 2, deep - 1, termResults, elementResults);

                //recharacterize
        if (fresh == 3)
            for (i = -1; i < c.altsUsed; i++) {
                 if (i == -1)
                     t = c.myTerm;
                 else
                     t = c.altTerms[i];
                 if (t.op == 'v')
                     handle1(a, b, t.arg1, t.arg2, 0, deep - 1, termResults, elementResults);
                 if (t.op == '^')
                     handle2(a, b, t.arg1, t.arg2, 0, deep - 1, termResults, elementResults);
             }
    } //handle6

    void handle7(Element a, Element b, Element c, int fresh, int deep, Vector termResults, Vector elementResults)
    {
        Element answer1 = meet(a, b);
        Element answer2 = join(a, b);
        Element answer3 = meet(a, c);
        Element answer4 = join(a, c);
        Element answer5 = meet(b, c);
        int i;
        Term t;

        if (deep <= 0)
            return;

              //meet
        if (answer5 != null)
            handle8(a, answer5, 2, deep - 1, termResults, elementResults);

              //apply modular law
        if (answer1 == a || answer2 == b)
            handle15(b, a, c, 0, deep - 1, termResults, elementResults);
        if (answer3 == a || answer4 == c)
            handle15(c, a, b, 0, deep - 1, termResults, elementResults);

              //recharacterize
        if (fresh == 3)
            for (i = -1; i < c.altsUsed; i++) {
                 if (i == -1)
                     t = c.myTerm;
                 else
                     t = c.altTerms[i];
                 if (t.op == 'v')
                     handle4(a, t.arg1, t.arg2, b, 0, deep - 1, termResults, elementResults);
                 if (t.op == '^')
                     handle5(a, b, t.arg1, t.arg2, 0, deep - 1, termResults, elementResults);
             }
        if (fresh == 1)
            for (i = -1; i < a.altsUsed; i++) {
                 if (i == -1)
                     t = a.myTerm;
                 else
                     t = a.altTerms[i];
                 if (t.op == 'v')
                     handle2(t.arg1, t.arg2, b, c, 0, deep - 1, termResults, elementResults);
                 if (t.op == '^')
                     handle3(b, c, t.arg1, t.arg2, 0, deep - 1, termResults, elementResults);
             }

                //absorb
        if (a == b || a == c)
            elementResults.addElement(a);
    } //handle7

    void handle8(Element a, Element b, int fresh, int deep, Vector termResults, Vector elementResults)
    {
        Term t;

        termResults.addElement(new Term('v', a, b));
        if (deep <= 0)
            return;

                //recharacterize
        if (fresh == 2)
            for (int i = -1; i < b.altsUsed; i++) {
                 if (i == -1)
                     t = b.myTerm;
                 else
                     t = b.altTerms[i];
                 if (t.op == 'v')
                     handle6(t.arg1, t.arg2, a, 0, deep - 1, termResults, elementResults);
                 if (t.op == '^')
                     handle7(a, t.arg1, t.arg2, 0, deep - 1, termResults, elementResults);
             }
    } //handle8

    void handle9(Element a, Element b, Element c, Element d, int fresh, int deep, Vector termResults, Vector elementResults)
    {
        Element answer1 = meet(a, c);
        Element answer2 = meet(a, d);
        Element answer3 = meet(b, c);
        Element answer4 = meet(b, d);

        if (deep <= 0)
            return;

              //meet
        if (answer1 != null)
            handle14(b, d, answer1, 3, deep - 1, termResults, elementResults);
        if (answer2 != null)
            handle14(b, c, answer2, 3, deep - 1, termResults, elementResults);        
        if (answer3 != null)
            handle14(a, d, answer3, 3, deep - 1, termResults, elementResults);
        if (answer4 != null)
            handle14(a, c, answer4, 3, deep - 1, termResults, elementResults);
    } //handle9

    void handle10(Element a, Element b, Element c, Element d, int fresh, int deep, Vector termResults, Vector elementResults)
    {
        Element answer1 = join(c, d);
        Element answer2 = join(a, c);
        Element answer3 = meet(a, c);
        Element answer4 = join(a, d);
        Element answer5 = meet(a, d);
        Element answer6 = join(b, c);
        Element answer7 = meet(b, c);
        Element answer8 = join(b, d);
        Element answer9 = meet(b, d);

        if (deep <= 0)
            return;

             //join
        if (answer1 != null)
            handle14(a, b, answer1, 3, deep - 1, termResults, elementResults);

             //apply modular law
         if (answer2 == a || answer3 == c)
            handle12(b, a, d, c, 0, deep - 1, termResults, elementResults);
         if (answer4 == a || answer5 == d)
            handle12(b, a, c, d, 0, deep - 1, termResults, elementResults);
         if (answer6 == b || answer7 == c)
            handle12(a, b, d, c, 0, deep - 1, termResults, elementResults);
         if (answer8 == b || answer9 == d)
            handle12(a, b, c, d, 0, deep - 1, termResults, elementResults);
    } //handle10

    void handle11(Element a, Element b, Element c, Element d, int fresh, int deep, Vector termResults, Vector elementResults)
    {
        Element answer2 = join(a, c);
        Element answer3 = meet(a, c);
        Element answer4 = join(a, d);
        Element answer5 = meet(a, d);
        Element answer6 = join(b, c);
        Element answer7 = meet(b, c);
        Element answer8 = join(b, d);
        Element answer9 = meet(b, d);

        if (deep <= 0)
            return;

              //apply modular law
        if (answer2 == a || answer3 == c || answer6 == b || answer7 == c)
            handle4(c, a, b, d, 0, deep - 1, termResults, elementResults);
        if (answer4 == a || answer5 == d || answer8 == b || answer9 == d)
            handle4(d, a, b, c, 0, deep - 1, termResults, elementResults);
        if (answer2 == c || answer3 == a || answer4 == d || answer5 == a)
            handle4(a, c, d, b, 0, deep - 1, termResults, elementResults);
        if (answer6 == c || answer7 == b || answer8 == d || answer9 == b)
            handle4(b, c, d, a, 0, deep - 1, termResults, elementResults);
    } //handle11

    void handle12(Element a, Element b, Element c, Element d, int fresh, int deep, Vector termResults, Vector elementResults)
    {
        Element answer1 = meet(b, c);        
        Element answer2 = meet(a, d);
        Element answer3 = join(a, d);

        if (deep <= 0)
            return;

                //meet
        if (answer1 != null)
            handle15(a, d, answer1, 3, deep - 1, termResults, elementResults);

                //apply modular law
        if (answer2 == d || answer3 == a)
            handle5(d, a, b, c, 0, deep - 1, termResults, elementResults);
    } //handle12

    void handle13(Element a, Element b, Element c, Element d, int fresh, int deep, Vector termResults, Vector elementResults)
    {
        Element answer1 = join(b, c);
        Element answer2 = join(b, d);
        Element answer3 = join(c, d);
        Element answer4 = join(a, b);
        Element answer5 = meet(a, b);
        Element answer6 = join(a, c);
        Element answer7 = meet(a, c);
        Element answer8 = join(a, d);
        Element answer9 = meet(a, d);

        if (deep <= 0)
            return;

              //join
        if (answer1 != null)
            handle15(a, d, answer1, 3, deep - 1, termResults, elementResults);
        if (answer2 != null)
            handle15(a, c, answer2, 3, deep - 1, termResults, elementResults);
        if (answer3 != null)
            handle15(a, b, answer3, 3, deep - 1, termResults, elementResults);

                //apply modular law
         if (answer4 == a || answer5 == b)
             handle4(b, c, d, a, 0, deep - 1, termResults, elementResults);
         if (answer6 == a || answer7 == c)
             handle4(c, b, d, a, 0, deep - 1, termResults, elementResults);
         if (answer8 == a || answer9 == d)
             handle4(d, b, c, a, 0, deep - 1, termResults, elementResults);

                //absorb
         if (a == b || a == c || a == d)
             elementResults.addElement (a);
    } //handle13

    void handle14(Element a, Element b, Element c, int fresh, int deep, Vector termResults, Vector elementResults)
    {
        Element answer1 = meet(a, b);
        Element answer2 = meet(a, c);
        Element answer3 = meet(b, c);
        int i;
        Term t;

        if (deep <= 0)
            return;

                //meet
        if (answer1 != null)
            handle16(c, answer1, 2, deep - 1, termResults, elementResults);
        if (answer2 != null)
            handle16(b, answer2, 2, deep - 1, termResults, elementResults);
        if (answer3 != null)
            handle16(a, answer3, 2, deep - 1, termResults, elementResults);

                //recharacterize
        if (fresh == 3)
            for (i = -1; i < c.altsUsed; i++) {
                 if (i == -1)
                     t = c.myTerm;
                 else
                     t = c.altTerms[i];
                 if (t.op == '^')
                     handle9(a, b, t.arg1, t.arg2, 0, deep - 1, termResults, elementResults);
                 if (t.op == 'v')
                     handle10(a, b, t.arg1, t.arg2, 0, deep - 1, termResults, elementResults);
             }
    } //handle14

    void handle15(Element a, Element b, Element c, int fresh, int deep, Vector termResults, Vector elementResults)
    {
        Element answer1 = join(a, b);
        Element answer2 = meet(a, b);
        Element answer3 = join(a, c);
        Element answer4 = meet(a, c);
        Element answer5 = join(b, c);
        int i;
        Term t;

        if (deep <= 0)
            return;

              //join
        if (answer5 != null)
            handle16(a, answer5, 2, deep - 1, termResults, elementResults);

              //apply modular law
        if (answer1 == a || answer2 == b)
            handle7(b, a, c, 0, deep - 1, termResults, elementResults);
        if (answer3 == a || answer4 == c)
            handle7(c, a, b, 0, deep - 1, termResults, elementResults);

              //recharacterize
        if (fresh == 3)
            for (i = -1; i < c.altsUsed; i++) {
                 if (i == -1)
                     t = c.myTerm;
                 else
                     t = c.altTerms[i];
                 if (t.op == '^')
                     handle12(a, t.arg1, t.arg2, b, 0, deep - 1, termResults, elementResults);
                 if (t.op == 'v')
                     handle13(a, b, t.arg1, t.arg2, 0, deep - 1, termResults, elementResults);
             }
        if (fresh == 1)
            for (i = -1; i < a.altsUsed; i++) {
                 if (i == -1)
                     t = a.myTerm;
                 else
                     t = a.altTerms[i];
                 if (t.op == '^')
                     handle10(t.arg1, t.arg2, b, c, 0, deep - 1, termResults, elementResults);
                 if (t.op == 'v')
                     handle11(b, c, t.arg1, t.arg2, 0, deep - 1, termResults, elementResults);
             }

                //absorb
        if (a == b || a == c)
            elementResults.addElement (a);
    } //handle15

    void handle16(Element a, Element b, int fresh, int deep, Vector termResults, Vector elementResults)
    {
        Term t;

        termResults.addElement(new Term('^', a, b));
        if (deep <= 0)
            return;

                //recharacterize
        if (fresh == 2)
            for (int i = -1; i < b.altsUsed; i++) {
                 if (i == -1)
                     t = b.myTerm;
                 else
                     t = b.altTerms[i];
                 if (t.op == '^')
                     handle14(t.arg1, t.arg2, a, 0, deep - 1, termResults, elementResults);
                 if (t.op == 'v')
                     handle15(a, t.arg1, t.arg2, 0, deep - 1, termResults, elementResults);
             }
    } //handle16

    void computeCongruence()
    //This method doesn't really compute the congruence generated by the equivalence
    //relation; it's intended to find most of the pairs with a reasonable amount of work.
    {
        IntCell count = new IntCell(0);
        int [] repSet = myEqRel.repSet(count, elementCount);
        int [] row;
        int maxRow, maxColumn, l;
        Element e, f, g, h;

        if (count.myInt == 1)
            return;     //All elements are related already.
        for (int i = 0; i < count.myInt; i++) {
            row = myEqRel.classOf(repSet[i]);         
              //While row is being used, myEqRel can change, but row won't.
            for (int j = 0; j < row.length - 1; j++)
                for (int k = j + 1; k < row.length; k++) {
                    e = elements[row[j]];
                    f = elements[row[k]];
                    g = join(e, f);
                    h = meet(e, f);
                    if (g != null)
                        identify(e, g);
                    if (h != null)
                        identify(e, h);
                 }
        } //for (i)
        repSet = myEqRel.repSet(count, elementCount);
        if (count.myInt == 1)
            return;     //All elements are related already.
	l = 0;
	for(int i = 0; i < count.myInt && l < M; i++) {
           //This loop runs until either M nontrivial classes have been 
           //examined or there are no classes left.
            row = myEqRel.classOf(repSet[i]);         
	    if (row.length > 1) {
		l++;
            	maxColumn = Math.min(row.length - 1, N);
		for (int j = 1; j <= maxColumn; j++)
 		    for (int k = 0; k < elementCount; k++) {
				Element e1 = join(row[0], k);
				Element e2 = join(row[j], k);
				Element e3 = meet(row[0], k);
				Element e4 = meet(row[j], k);
				if (e1 == null)
				    table[Math.min(row[0], k)][Math.max(row[0], k)] = e2;
				else
                    		    identify(e1, e2);
				if (e3 == null)
				    table[Math.max(row[0], k)][Math.min(row[0], k)] =  e4;
				else
                    	    	    identify(e3, e4);
		    }	
	    } //if
 	} //for
    } //computeCongruence

    public ModLattice collapse(boolean keepAuto)
    {
        IntCell count = new IntCell(0);
        int [] repSet = myEqRel.repSet(count, elementCount);
        ModLattice theNewLattice = new ModLattice(count.myInt, keepAuto ? inverse : new int[0]);
        int [] lookup = repSet;  
                     //For each element number in the new lattice,
                     //gives the corresponding number in the old lattice.
        Element [] lookup2 = new Element[elementCount];       
            //For each element number in the old
            //lattice, gives the corresponding element in the new lattice.
        Element oldElement, newElement;
        int oldConjugate;
        Term oldTerm, newTerm;
        int [] currentClass;

           //create elements of new lattice
        for (int i = 0; i < count.myInt; i++) { 
            oldElement = elements[repSet[i]];
            oldTerm = oldElement.myTerm;
            if (oldTerm.op == 'v' || oldTerm.op == '^') 
                newTerm = new Term(oldTerm.op, lookup2[oldTerm.arg1.myNumber], lookup2[oldTerm.arg2.myNumber]);
            else
                newTerm = new Term(oldTerm.op);
            newElement = new Element(theNewLattice, newTerm);
            currentClass = myEqRel.classOf(oldElement.myNumber);
            for (int j = 0; j < currentClass.length; j++)
                lookup2[currentClass[j]] = newElement;
            if (keepAuto)
                for (int j = 0; j < auto; j++) 
		    if (oldElement.conjugates[j] != null) {
                        oldConjugate = oldElement.conjugates[j].myNumber;
                        newElement.conjugates[j] = lookup2[oldConjugate];
                    }
            for (int j = 0; j < oldElement.altsUsed; j++) {
                oldTerm = oldElement.altTerms[j];
                if (oldTerm.op == 'v' || oldTerm.op == '^') 
                    newTerm = new Term(oldTerm.op, lookup2[oldTerm.arg1.myNumber], lookup2[oldTerm.arg2.myNumber]);
                else
                    newTerm = new Term(oldTerm.op);               
                newElement.addAlt(newTerm);
            }
        } // for (i)
           //fill table of new lattice
        for (int i = 0; i < theNewLattice.elementCount; i++)
            for (int j = 0; j < theNewLattice.elementCount; j++) {
                oldElement = table[lookup[i]][lookup[j]];
		if (oldElement != null) {
                    newElement = lookup2[oldElement.myNumber];
                    theNewLattice.table[i][j] = newElement;
	    	}
            }
        return theNewLattice;
    }  //collapse

    void resize(int newSize)
    {
        Element [][] temp = table;
        Element [] temp2 = elements;

        table = new Element[newSize][newSize];
        for (int i = 0; i < elementCount; i++)
            for (int j = 0; j < elementCount; j++)
                table[i][j] = temp[i][j];
        elements = new Element[newSize];
        for (int i = 0; i < elementCount; i++)
            elements[i] = temp2[i];
        myEqRel.resize(newSize);
        currentSize = newSize;
    }

    Element forceMeet(int x, int y)
    /* This method computes the meet of the elements numbered x, and y,
       whether or not it has already been computed.  */
    {
	int tempRow = currentRow;
	int tempColumn = currentColumn;
	Element answer;

	if (x >= elementCount || y >= elementCount || x < 0 || y < 0)
	    return null;   //invalid arguments

	currentRow = Math.max(x, y);
	currentColumn = Math.min(x, y);
	fillCurrentSquare();
	answer = table[currentRow][currentColumn];
	currentRow = tempRow;
	currentColumn = tempColumn;
	return answer;
    }

    Element forceJoin(int x, int y)
    /* This method computes the join of the elements numbered x, and y,
       whether or not it has already been computed.  */
    {
	int tempRow = currentRow;
	int tempColumn = currentColumn;
	Element answer;

	if (x >= elementCount || y >= elementCount || x < 0 || y < 0)
	    return null;   //invalid arguments

	currentRow = Math.min(x, y);
	currentColumn = Math.max(x, y);
	fillCurrentSquare();
	answer = table[currentRow][currentColumn];
	currentRow = tempRow;
	currentColumn = tempColumn;
	return answer;
    }

} //class ModLattice