handler lineq {

    class EqAtom;
    class Polynom;
    class java.lang.String;
    class java.lang.Object;
    class java.lang.Float;
    class nl;

    constraint eqr(nl,java.lang.Float);

    rules {

	variable java.lang.Float A1,A2,B,B1,B2,B3,B4,B5,factor, factor_neg, Y;
	variable nl P,P1,P2,P3,P4,P5,G;
	variable EqAtom AT1, AT2;
	variable java.lang.String X;

	// leer
	if (nl.isEmpty(P)) { eqr(P,B) } <=> { B = 0.0 } leer;

	// binden
// 	if(Polynom.atomar(P) && AT1 = Polynom.getHead(P) && X = Polynom.getVarName(AT1))
// 	    { eqr(P,B) } <=>
// 	{
// 	    AT1 = Polynom.getHead(P) &&
// 	    A1 = Polynom.getCoeff(AT1) &&
// 	    B1 = Polynom.floatDivide(B,A1) &&
// 	    Polynom.bindVar(csref,X,B1)

// 	} binden;

	// gebunden
	if(
	   Polynom.kommt_vor_in(X,P)
	   )
	    { eqr(P,B) } <=> {
		A2 = Polynom.getCoeff(X,P) &&
		P1 = Polynom.entferne(X,P) &&
		factor = Polynom.floatMultiply(A2,Y) &&
		B1 = Polynom.floatSubstract(B,factor) &&
		eqr(P1,B1)
	    } gebunden;

	// eliminiere
	if(
           Polynom.isNotEmpty(G) &&          // A1*X,P1 = B1
           AT1 = Polynom.getHead(G) &&
	   X = Polynom.getVarName(AT1) &&
           Polynom.kommt_vor_in(X,P)       //   guard kommt_vor_in(X,P)
	   )
	    { eqr(G,B1) && eqr (P,B2) } <=>
	{
	    // Bug Bindungen aus dem Guard
	    AT1 = Polynom.getHead(G) &&
	    X = Polynom.getVarName(AT1) &&
	    // Entferne A2*X aus P, erhalte so P2
	    A2 = Polynom.getCoeff(X,P) && P2 = Polynom.entferne(X,P) &&
	    // loese lokal nach erster Variablen X auf
	    // multipliziere_poly_const(B1-P1,A2/A1,B3-P3)
	    A1 = Polynom.getCoeff(AT1) && P1 = Polynom.getTail(G) &&
	    factor = Polynom.floatDivide(A2,A1) &&
	    P3 = Polynom.multipliziere_poly_const(P1,factor) &&
	    B3 = Polynom.floatMultiply(B1,factor) &&
	    // ersetze P3-B3 fuer X in zweiter Gleichung

	    P4 = Polynom.neg_poly(P2) &&
	    P5 = Polynom.addiere_poly_poly(P3,P4) &&
	    B4 = Polynom.floatNegate(B2) &&
	    B5 = Polynom.floatAdd(B3,B4) &&
	    eqr(G,B1) &&
	    eqr(P5,B5)
	} eliminiere;

    }//end of rules


    goal goal_0 {
		variable java.lang.Float X;
		variable java.lang.Float Y;
		variable java.lang.Float Z;

		instance EqAtom AT1 = new EqAtom("1.0*X");
		instance EqAtom AT2 = new EqAtom("1.0*Y");
		instance EqAtom AT3 = new EqAtom("1.0*X");
		instance EqAtom AT4 = new EqAtom("-1.0*Y");
		instance EqAtom AT5 = new EqAtom("5.0*Y");
		instance EqAtom AT6 = new EqAtom("1.5*X");
		instance EqAtom AT7 = new EqAtom("3.0*Z");

		instance nl p1 = new nl(AT1, new nl(AT2));
		instance nl p2 = new nl(AT3, new nl(AT4));
		instance nl p3 = new nl(AT5, new nl(AT6, new nl(AT7)));

		eqr(p1,7.0) && eqr(p2,3.0) && eqr(p3,1.0)
   }//end of goal_0

}//end of handler lineq