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


/**This class manages the computer-aided proofs.**/


public class ComputeProof implements Runnable {
    Manager M;
    int halt;
    ProofPinwheel1 PIN1;
    ProofPinwheel2 PIN2;
    ProofPinwheel3 PIN3;
    ProofCompact1 C1;
    ProofCompact2 C2;
    ProofRenorm1 RE1;
    ProofRenorm2 RE2;
    ProofRenorm3 RE3;
    ProofRenorm4 RE4;
    ProofRenorm5 RE5;
    ProofFundamental F;
    ProofFixedPoint FP;
    ProofReduction1 R1;
    ProofReduction2 R2;
    ProofArithmetic A;


    public ComputeProof() {
    }

    public ComputeProof(Manager MM) {
	this.M=MM;
	PIN1=new ProofPinwheel1(M);
	PIN2=new ProofPinwheel2(M);
	PIN3=new ProofPinwheel3(M);
	C1=new ProofCompact1(M);
	C2=new ProofCompact2(M);
	RE1=new ProofRenorm1(M);
	RE2=new ProofRenorm2(M);
	RE3=new ProofRenorm3(M);
	RE4=new ProofRenorm4(M);
	RE5=new ProofRenorm5(M);
	F=new ProofFundamental(M);
	FP=new ProofFixedPoint(M);
	R1=new ProofReduction1(M);
	R2=new ProofReduction2(M);
	A=new ProofArithmetic(M);
    }

    public void doHalt() {
	halt=0;
	try{PIN1.halt=0;} catch(Exception e) {}
	try{PIN2.halt=0;} catch(Exception e) {}
	try{PIN3.halt=0;} catch(Exception e) {}
	try{C1.halt=0;} catch(Exception e) {}
	try{C2.halt=0;} catch(Exception e) {}
	try{RE1.halt=0;} catch(Exception e) {}
	try{RE2.halt=0;} catch(Exception e) {}
	try{RE3.halt=0;} catch(Exception e) {}
	try{RE4.halt=0;} catch(Exception e) {}
	try{RE5.halt=0;} catch(Exception e) {}
	try{F.halt=0;} catch(Exception e) {}
	try{FP.halt=0;} catch(Exception e) {}
	try{R1.halt=0;} catch(Exception e) {}
	try{R2.halt=0;} catch(Exception e) {}
	try{A.halt=0;} catch(Exception e) {}
    }

    public void run() {
	halt=1;
	int mode=M.C.CON_X.ACTION.mode;

	/**PINWHEEL LEMMA TESTS**/

	if(mode==0) {
	    int aux=M.C.CON_X.PINWHEEL.mode;

	    if(aux<2) {
	       PIN1=new ProofPinwheel1(M);
	       new Thread(PIN1).start();
	    }
	    if(aux==2) {
	       PIN2=new ProofPinwheel2(M);
	       new Thread(PIN2).start();
	    }
	
	    if(aux==3) {
	       PIN3=new ProofPinwheel3(M);
	       new Thread(PIN3).start();
	    }
	}

	/**COMPACTIFICATION THEOREM**/


	if(mode==1) {
	    int[] aux=new int[2];
	    for(int i=0;i<2;++i) aux[i]=M.C.CON_X.COMPACT.L[i].on;
	    if(aux[0]==1) {
	       C1=new ProofCompact1(M);
	       new Thread(C1).start();
	    }
	    if(aux[1]==1) {
	       C2=new ProofCompact2(M);
	       new Thread(C2).start();
	    }
	}


	/**FUNDAMENTAL ORBIT THEOREM**/

	if(mode==2) {
	    F=new ProofFundamental(M);
	    new Thread(F).start();
	}

	/**RENORM FIXED POINT LEMMA**/

	if(mode==3) {
	    FP=new ProofFixedPoint(M);
	    new Thread(FP).start();
	}

	/**REDUCTION PROOF 1:*/

	if(mode==4) {
	    R1=new ProofReduction1(M);
	    new Thread(R1).start();
	}

	/**REDUCTION PROOF 2*/

	if(mode==5) {
	    R2=new ProofReduction2(M);
	    new Thread(R2).start();
	}



	/**RENORMALIZATION THEOREM**/

	if(mode==6) {
	    int aux=M.C.CON_X.RENORM.mode;

	    if(aux==0) {
	      RE1=new ProofRenorm1(M);
	      new Thread(RE1).start();
	    }

	    if(aux==1) {
	      RE2=new ProofRenorm2(M);
	      new Thread(RE2).start();
	    }

	    if(aux==2) {
	      RE3=new ProofRenorm3(M);
	      new Thread(RE3).start();
	    }

	    if(aux==3) {
	      RE4=new ProofRenorm4(M);
	      new Thread(RE4).start();
	    }

	    if(aux==4) {
	      RE5=new ProofRenorm5(M);
	      new Thread(RE5).start();
	    }

	}


	/**ARITHMETIC**/

	if(mode==7) {
           A=new ProofArithmetic(M);
	   new Thread(A).start();
	}
    }

}