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


/*This file does calculation 6*/


public class ProofCalc6 {

    public static void main(Manager M) {
	for(int i=0;i<8;++i) M.C.MESSAGE[i]="";
	M.C.MESSAGE[0]="start calc 6";
	M.C.MESSAGE[1]="start order-2 test";
	M.C.repaint();
	test1();
	M.C.MESSAGE[1]="order-2 test done";

	M.C.MESSAGE[2]="start containment test";
	M.C.repaint();
	test2(M);
	M.C.MESSAGE[4]="containment test done";
	M.C.MESSAGE[5]="calc 6 done";
	M.C.repaint();

    }

    public static void fail() {
	throw new ProofException("calc 6 fails");
    }

    /*Checks the order 2 tile on the interval [1,3/2].*/

    public static void test1() {
        LongPolyhedron Q1=DataPartitionExtra.order2A();
        LongPolyhedron Q2=ProofSupport.F2(Q1);
        LongPolyhedron Q3=ProofSupport.F2(Q2);
        boolean test=LongPolyCombinatorics.isSubset(Q3,Q1);
	if(test==false) fail();
    }

    public static void test2(Manager M) {
	int index=-1;
	LongPolyhedron Z=DataPartitionExtra.Z1();
	for(int i=32;i<51;++i) {
	    LongPolyhedron P=DataPartition.imagePoly(i);
	    if(LongPolyCombinatorics.isSubset(Z,P)==true) index=i;
	}
	if(index==-1) fail();
	Integer INDEX=new Integer(index);
	M.C.MESSAGE[3]=INDEX.toString();
    }

}