import java.applet.Applet;
import java.awt.*;
import java.awt.event.*;
import java.applet.*;
import java.awt.geom.*;
import java.math.*;



public class ProofPartition {

     /*This file contains the routines that verify that
       the partition is correct.  We check 6 things::
       1. The pieces of the domain partition are contained in F1.
       2. The pieces of the range partition are contained in F1.
       3. The pieces of the domain partition under f' are contained in F2
       4. The pieces of the domain partition have pairwise disjoint interiors. 
       5. The pieces of the range  partition have pairwise disjoint interiors.
       6. The pieces of the domain partition fill the parallelotope.
       These 3 things imply that the range partition also fills.*/

    public static void main(Manager M) {
	for(int i=0;i<8;++i) M.C.MESSAGE[i]="";
	M.C.MESSAGE[0]="start containment test";
	M.C.repaint();
	proveInside();
	M.C.MESSAGE[0]="containment test done";
	M.C.repaint();

	proveDisjointInteriors1();

	M.C.MESSAGE[1]="disjointness test 1";
	M.C.repaint();
	proveInside();
	M.C.MESSAGE[1]="disjointness test 1 done";
        M.C.repaint();

	proveDisjointInteriors2();

	M.C.MESSAGE[2]="disjointness test 2";
	M.C.repaint();
	proveInside();
	M.C.MESSAGE[2]="disjointness test 2 done";
        M.C.repaint();

	proveFill();

	M.C.MESSAGE[3]="start fill test";
	M.C.repaint();
	proveInside();
	M.C.MESSAGE[3]="fill test done";
        M.C.repaint();
    }

    public static void fail() {
	throw new ProofException("partition proof fails");
    }


    /*This checks that all 51 pieces really lie in the parallelotope*/

    public static void proveInside() {
	LongPolyhedron F1=DataPartitionExtra.domainF1();
	LongPolyhedron F2=DataPartitionExtra.domainF2();
	LongPolyhedron P=new LongPolyhedron();
	boolean test=false;
	for(int i=0;i<32;++i) {
	    P=DataPartition.poly(i);
	    test=LongPolyCombinatorics.isSubset(P,F1); 
            if(test==false) fail();
	    P=DataPartition.imagePoly(i);
            test=LongPolyCombinatorics.isSubset(P,F1); 
	    if(test==false) fail();
            P=DataPartition.halfImagePoly(i); 
            test=LongPolyCombinatorics.isSubset(P,F2); 
	    if(test==false) fail();
	}
    }

    /*This checks that the polyhedra in the basic
      partition have disjoint interiors*/

    public static void proveDisjointInteriors1() {
	for(int i=0;i<51;++i) {
	    for(int j=i+1;j<51;++j) {
	        LongPolyhedron P=DataPartition.poly(i);
	        LongPolyhedron Q=DataPartition.poly(j);
		boolean test=LongPolyCombinatorics.separate(10,P,Q);
		if(test==false) fail();
	    }
	}
    }



    /*This checks that the polyhedra in the image
      partition have disjoint interiors*/


    public static void proveDisjointInteriors2() {
	for(int i=0;i<51;++i) {
	    for(int j=i+1;j<51;++j) {
	        LongPolyhedron P=DataPartition.imagePoly(i);
	        LongPolyhedron Q=DataPartition.imagePoly(j);
		boolean test=LongPolyCombinatorics.separate(10,P,Q);
		if(test==false) fail();
	    }
	}
    }

    public static void proveFill() {
	long t=0;
	for(int i=0;i<51;++i) {
	    t=t+DataPartition.volume(i);
	}
	long u=3500658000L;
	if(t!=u) fail();
    }

}