Termination proof of /tmp/tmpfxdpb5/Carre.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 1330 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 230 ms)

        ↳7 IDP

        ↳8 IDPNonInfProof (⇒, 2080 ms)

        ↳9 IDP

        ↳10 IDependencyGraphProof (⇔, 0 ms)

        ↳11 IDP

        ↳12 IDPNonInfProof (⇒, 370 ms)

        ↳13 IDP

        ↳14 IDependencyGraphProof (⇔, 0 ms)

        ↳15 TRUE

    ↳16 JBCTerminationSCC

        ↳17 SCCToIDPv1Proof (⇒, 670 ms)

        ↳18 IDP

        ↳19 IDPNonInfProof (⇒, 350 ms)

        ↳20 AND

            ↳21 IDP

                ↳22 IDependencyGraphProof (⇔, 0 ms)

                ↳23 IDP

                ↳24 IDPNonInfProof (⇒, 200 ms)

                ↳25 AND

                    ↳26 IDP

                        ↳27 IDependencyGraphProof (⇔, 0 ms)

                        ↳28 TRUE

                    ↳29 IDP

                        ↳30 IDependencyGraphProof (⇔, 0 ms)

                        ↳31 TRUE

            ↳32 IDP

                ↳33 IDependencyGraphProof (⇔, 0 ms)

                ↳34 IDP

                ↳35 IDPNonInfProof (⇒, 110 ms)

                ↳36 AND

                    ↳37 IDP

                        ↳38 IDependencyGraphProof (⇔, 0 ms)

                        ↳39 TRUE

                    ↳40 IDP

                        ↳41 IDependencyGraphProof (⇔, 0 ms)

                        ↳42 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_20 (Apple Inc.) Main-Class: Carre

class Curseur{
	private int X=0, Y=0, maxX, maxY;
	private boolean torique=false;

	public Curseur(int maxX, int maxY, boolean espaceTorique){
		super();
		this.maxX=maxX;
		this.maxY=maxY;
		this.torique=espaceTorique;		
	}

	public void centrer(){
		
			int cX=maxX/2;
			int cY=maxY/2;
			X=cX;
			Y=cY;
		
	}

	public void haut(){

			Y--;
			if(torique&&Y<0) Y=maxY-1;
	}

	public void bas(){
			Y++;
			if(torique&&Y==maxY) Y=0;
	}

	public void droite(){
			X++;
			if(torique&&X==maxX) X=0;
	}

	public void gauche(){
			X--;
			if(torique&&X<0) X=maxX-1;
	}

	public int getX(){
			return X;
	}

	public int getY(){
			return Y;
	}
	
	public void imprimer(){
	    //System.out.println("Curseur@["+getX()+","+getY()+"]");
	}
}

public class Carre {

	private Curseur curseur=null;
	private int cote=0;

	public Carre(int cote){
		if(cote>1&cote%2==1){
			this.cote=cote; 
		}else{
		    //System.out.println("Cette classe ne genere pas les carres magiques d\'ordre pair.");
		    //System.exit(0);
		}
		this.curseur=new Curseur(cote,cote,true);
	}
	
	private int [][] carre=null;

	public void init(){
		carre=new int[cote][cote];
		int n=0;
		for(int x=0;x<3;x++) for(int y=0;y<3;y++) carre[x][y]=0;
		curseur.centrer();
	}

	public void peupler(){
		curseur.bas();
		int nbre=1;
		int cpteur=1;
		while(cpteur<3){			
			if(!ajouter(nbre,curseur.getX(),curseur.getY())){
				curseur.bas();
				curseur.gauche();
				cpteur++;
			}else{
				cpteur=1;
				curseur.bas();
				curseur.droite();
				nbre++;
			}
		}
	}

	public Curseur curseur(){
		return curseur;
	}

	public int cote(){
		return cote;
	}

	public boolean ajouter(int nombre, int X, int Y){
		if(carre[X][Y]!=0) return false; 
		carre[X][Y]=nombre;
		return true;
	}

	public void imprimer(){
		for(int j=0;j<cote;j++){
			for(int i=0;i<cote;i++){
			    //System.out.print(carre[i][j]+"\t");
			}
			//System.out.println();
		}
	}

	public static void main(String args[]){
	    Random.args = args;
	    Carre carre=new Carre(2*Random.random()+1);
	    carre.init();
	    //carre.peupler();
	    carre.imprimer();
	}
    
}

public class Random {
  static String[] args;
  static int index = 0;

  public static int random() {
      if (index >= args.length)
	  return 0;

      String string = args[index];
      index++;
      return string.length();
  }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Carre.main([Ljava/lang/String;)V: Graph of 611 nodes with 2 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 2 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Carre.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses: UsedFieldsAnalysis

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 24 rules for P and 0 rules for R.

P rules:
2695_0_imprimer_Load(EOS(STATIC_2695), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i407) → 2696_0_imprimer_FieldAccess(EOS(STATIC_2696), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i407, java.lang.Object(Carre(EOC, i27)))
2696_0_imprimer_FieldAccess(EOS(STATIC_2696), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i407, java.lang.Object(Carre(EOC, i27))) → 2698_0_imprimer_GE(EOS(STATIC_2698), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i407, i27)
2698_0_imprimer_GE(EOS(STATIC_2698), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i407, i27) → 2700_0_imprimer_GE(EOS(STATIC_2700), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i407, i27)
2700_0_imprimer_GE(EOS(STATIC_2700), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i407, i27) → 2703_0_imprimer_ConstantStackPush(EOS(STATIC_2703), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407) | <(i407, i27)
2703_0_imprimer_ConstantStackPush(EOS(STATIC_2703), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407) → 2706_0_imprimer_Store(EOS(STATIC_2706), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, 0)
2706_0_imprimer_Store(EOS(STATIC_2706), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, matching1) → 2708_0_imprimer_Load(EOS(STATIC_2708), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, 0) | =(matching1, 0)
2708_0_imprimer_Load(EOS(STATIC_2708), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, matching1) → 2719_0_imprimer_Load(EOS(STATIC_2719), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, 0) | =(matching1, 0)
2719_0_imprimer_Load(EOS(STATIC_2719), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i409) → 2731_0_imprimer_Load(EOS(STATIC_2731), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i409)
2731_0_imprimer_Load(EOS(STATIC_2731), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i412) → 2749_0_imprimer_Load(EOS(STATIC_2749), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i412)
2749_0_imprimer_Load(EOS(STATIC_2749), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i417) → 2768_0_imprimer_Load(EOS(STATIC_2768), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i417)
2768_0_imprimer_Load(EOS(STATIC_2768), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i422) → 2770_0_imprimer_Load(EOS(STATIC_2770), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i422, i422)
2770_0_imprimer_Load(EOS(STATIC_2770), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i422, i422) → 2771_0_imprimer_FieldAccess(EOS(STATIC_2771), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i422, i422, java.lang.Object(Carre(EOC, i27)))
2771_0_imprimer_FieldAccess(EOS(STATIC_2771), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i422, i422, java.lang.Object(Carre(EOC, i27))) → 2773_0_imprimer_GE(EOS(STATIC_2773), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i422, i422, i27)
2773_0_imprimer_GE(EOS(STATIC_2773), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i422, i422, i27) → 2774_0_imprimer_GE(EOS(STATIC_2774), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i422, i422, i27)
2773_0_imprimer_GE(EOS(STATIC_2773), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i422, i422, i27) → 2775_0_imprimer_GE(EOS(STATIC_2775), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i422, i422, i27)
2774_0_imprimer_GE(EOS(STATIC_2774), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i422, i422, i27) → 2776_0_imprimer_Inc(EOS(STATIC_2776), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407) | >=(i422, i27)
2776_0_imprimer_Inc(EOS(STATIC_2776), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407) → 2779_0_imprimer_JMP(EOS(STATIC_2779), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), +(i407, 1)) | >=(i407, 0)
2779_0_imprimer_JMP(EOS(STATIC_2779), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i424) → 2784_0_imprimer_Load(EOS(STATIC_2784), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i424)
2784_0_imprimer_Load(EOS(STATIC_2784), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i424) → 2694_0_imprimer_Load(EOS(STATIC_2694), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i424)
2694_0_imprimer_Load(EOS(STATIC_2694), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407) → 2695_0_imprimer_Load(EOS(STATIC_2695), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i407)
2775_0_imprimer_GE(EOS(STATIC_2775), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i422, i422, i27) → 2778_0_imprimer_Inc(EOS(STATIC_2778), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i422) | <(i422, i27)
2778_0_imprimer_Inc(EOS(STATIC_2778), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i422) → 2780_0_imprimer_JMP(EOS(STATIC_2780), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, +(i422, 1)) | >=(i422, 0)
2780_0_imprimer_JMP(EOS(STATIC_2780), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i425) → 2787_0_imprimer_Load(EOS(STATIC_2787), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i425)
2787_0_imprimer_Load(EOS(STATIC_2787), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i425) → 2768_0_imprimer_Load(EOS(STATIC_2768), java.lang.Object(Carre(EOC, i27)), java.lang.Object(Carre(EOC, i27)), i407, i425)
R rules:

Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.

P rules:
2773_0_imprimer_GE(EOS(STATIC_2773), java.lang.Object(Carre(EOC, x0)), java.lang.Object(Carre(EOC, x0)), x1, x2, x2, x0) → 2773_0_imprimer_GE(EOS(STATIC_2773), java.lang.Object(Carre(EOC, x0)), java.lang.Object(Carre(EOC, x0)), +(x1, 1), 0, 0, x0) | &&(&&(>=(x2, x0), >(+(x1, 1), 0)), >(x0, +(x1, 1)))
2773_0_imprimer_GE(EOS(STATIC_2773), java.lang.Object(Carre(EOC, x0)), java.lang.Object(Carre(EOC, x0)), x1, x2, x2, x0) → 2773_0_imprimer_GE(EOS(STATIC_2773), java.lang.Object(Carre(EOC, x0)), java.lang.Object(Carre(EOC, x0)), x1, +(x2, 1), +(x2, 1), x0) | &&(>(+(x2, 1), 0), <(x2, x0))
R rules:

Filtered ground terms:

2773_0_imprimer_GE(x1, x2, x3, x4, x5, x6, x7) → 2773_0_imprimer_GE(x2, x3, x4, x5, x6, x7)
Carre(x1, x2) → Carre(x2)
EOS(x1) → EOS
Cond_2773_0_imprimer_GE1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_2773_0_imprimer_GE1(x1, x3, x4, x5, x6, x7, x8)
Cond_2773_0_imprimer_GE(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_2773_0_imprimer_GE(x1, x3, x4, x5, x6, x7, x8)

Filtered duplicate args:

2773_0_imprimer_GE(x1, x2, x3, x4, x5, x6) → 2773_0_imprimer_GE(x2, x3, x5)
Cond_2773_0_imprimer_GE(x1, x2, x3, x4, x5, x6, x7) → Cond_2773_0_imprimer_GE(x1, x3, x4, x6)
Cond_2773_0_imprimer_GE1(x1, x2, x3, x4, x5, x6, x7) → Cond_2773_0_imprimer_GE1(x1, x3, x4, x6)

Filtered unneeded arguments:

Cond_2773_0_imprimer_GE(x1, x2, x3, x4) → Cond_2773_0_imprimer_GE(x1, x2, x3)

Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.

P rules:
2773_0_imprimer_GE(java.lang.Object(Carre(x0)), x1, x2) → 2773_0_imprimer_GE(java.lang.Object(Carre(x0)), +(x1, 1), 0) | &&(&&(>=(x2, x0), >(x1, -1)), >(x0, +(x1, 1)))
2773_0_imprimer_GE(java.lang.Object(Carre(x0)), x1, x2) → 2773_0_imprimer_GE(java.lang.Object(Carre(x0)), x1, +(x2, 1)) | &&(>(x2, -1), <(x2, x0))
R rules:

Finished conversion. Obtained 4 rules for P and 0 rules for R. System has predefined symbols.

P rules:
2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0)), x1, x2) → COND_2773_0_IMPRIMER_GE(&&(&&(>=(x2, x0), >(x1, -1)), >(x0, +(x1, 1))), java.lang.Object(Carre(x0)), x1, x2)
COND_2773_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0)), x1, x2) → 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0)), +(x1, 1), 0)
2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0)), x1, x2) → COND_2773_0_IMPRIMER_GE1(&&(>(x2, -1), <(x2, x0)), java.lang.Object(Carre(x0)), x1, x2)
COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0)), x1, x2) → 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0)), x1, +(x2, 1))
R rules:

(7) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0]) → COND_2773_0_IMPRIMER_GE(x2[0] >= x0[0] && x1[0] > -1 && x0[0] > x1[0] + 1, java.lang.Object(Carre(x0[0])), x1[0], x2[0])
(1): COND_2773_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[1])), x1[1], x2[1]) → 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), x1[1] + 1, 0)
(2): 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_2773_0_IMPRIMER_GE1(x2[2] > -1 && x2[2] < x0[2], java.lang.Object(Carre(x0[2])), x1[2], x2[2])
(3): COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], x2[3] + 1)

(0) -> (1), if (x2[0] >= x0[0] && x1[0] > -1 && x0[0] > x1[0] + 1 ∧java.lang.Object(Carre(x0[0])) →^* java.lang.Object(Carre(x0[1]))∧x1[0] →^* x1[1]∧x2[0] →^* x2[1])

(1) -> (0), if (java.lang.Object(Carre(x0[1])) →^* java.lang.Object(Carre(x0[0]))∧x1[1] + 1 →^* x1[0]∧0 →^* x2[0])

(1) -> (2), if (java.lang.Object(Carre(x0[1])) →^* java.lang.Object(Carre(x0[2]))∧x1[1] + 1 →^* x1[2]∧0 →^* x2[2])

(2) -> (3), if (x2[2] > -1 && x2[2] < x0[2] ∧java.lang.Object(Carre(x0[2])) →^* java.lang.Object(Carre(x0[3]))∧x1[2] →^* x1[3]∧x2[2] →^* x2[3])

(3) -> (0), if (java.lang.Object(Carre(x0[3])) →^* java.lang.Object(Carre(x0[0]))∧x1[3] →^* x1[0]∧x2[3] + 1 →^* x2[0])

(3) -> (2), if (java.lang.Object(Carre(x0[3])) →^* java.lang.Object(Carre(x0[2]))∧x1[3] →^* x1[2]∧x2[3] + 1 →^* x2[2])

The set Q is empty.

(8) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpDefaultShapeHeuristic@92341f1 Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 1 Max Right Steps: 1

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0)), x1, x2) → COND_2773_0_IMPRIMER_GE(&&(&&(>=(x2, x0), >(x1, -1)), >(x0, +(x1, 1))), java.lang.Object(Carre(x0)), x1, x2) the following chains were created:

We consider the chain 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0]) → COND_2773_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0]), COND_2773_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[1])), x1[1], x2[1]) → 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0) which results in the following constraint:
(1)    (&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1)))=TRUE∧java.lang.Object(Carre(x0[0]))=java.lang.Object(Carre(x0[1]))∧x1[0]=x1[1]∧x2[0]=x2[1] ⇒ 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0])≥NonInfC∧2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0])≥COND_2773_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0])∧(U^Increasing(COND_2773_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0])), ≥))

We simplified constraint (1) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(2)    (>(x0[0], +(x1[0], 1))=TRUE∧>=(x2[0], x0[0])=TRUE∧>(x1[0], -1)=TRUE ⇒ 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0])≥NonInfC∧2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0])≥COND_2773_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0])∧(U^Increasing(COND_2773_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x2[0] + [-1]x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2773_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0])), ≥)∧[bni_25 + (-1)Bound*bni_25] + [(-1)bni_25]x1[0] + [bni_25]x0[0] ≥ 0∧[(-1)bso_26] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x2[0] + [-1]x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2773_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0])), ≥)∧[bni_25 + (-1)Bound*bni_25] + [(-1)bni_25]x1[0] + [bni_25]x0[0] ≥ 0∧[(-1)bso_26] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x2[0] + [-1]x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2773_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0])), ≥)∧[bni_25 + (-1)Bound*bni_25] + [(-1)bni_25]x1[0] + [bni_25]x0[0] ≥ 0∧[(-1)bso_26] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x0[0] ≥ 0∧x2[0] + [-2] + [-1]x1[0] + [-1]x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2773_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0])), ≥)∧[(3)bni_25 + (-1)Bound*bni_25] + [bni_25]x0[0] ≥ 0∧[(-1)bso_26] ≥ 0)

We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(7)    (x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2773_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0])), ≥)∧[(3)bni_25 + (-1)Bound*bni_25] + [bni_25]x0[0] ≥ 0∧[(-1)bso_26] ≥ 0)

For Pair COND_2773_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0)), x1, x2) → 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0)), +(x1, 1), 0) the following chains were created:

We consider the chain 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0]) → COND_2773_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0]), COND_2773_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[1])), x1[1], x2[1]) → 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0), 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0]) → COND_2773_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0]) which results in the following constraint:
(8)    (&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1)))=TRUE∧java.lang.Object(Carre(x0[0]))=java.lang.Object(Carre(x0[1]))∧x1[0]=x1[1]∧x2[0]=x2[1]∧java.lang.Object(Carre(x0[1]))=java.lang.Object(Carre(x0[0]1))∧+(x1[1], 1)=x1[0]1∧0=x2[0]1 ⇒ COND_2773_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[1])), x1[1], x2[1])≥NonInfC∧COND_2773_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[1])), x1[1], x2[1])≥2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)∧(U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥))

We simplified constraint (8) using rules (I), (II), (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(9)    (>(x0[0], +(x1[0], 1))=TRUE∧>=(x2[0], x0[0])=TRUE∧>(x1[0], -1)=TRUE ⇒ COND_2773_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[0])), x1[0], x2[0])≥NonInfC∧COND_2773_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[0])), x1[0], x2[0])≥2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), +(x1[0], 1), 0)∧(U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥))

We simplified constraint (9) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(10)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x2[0] + [-1]x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥)∧[bni_27 + (-1)Bound*bni_27] + [(-1)bni_27]x1[0] + [bni_27]x0[0] ≥ 0∧[1 + (-1)bso_28] ≥ 0)

We simplified constraint (10) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(11)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x2[0] + [-1]x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥)∧[bni_27 + (-1)Bound*bni_27] + [(-1)bni_27]x1[0] + [bni_27]x0[0] ≥ 0∧[1 + (-1)bso_28] ≥ 0)

We simplified constraint (11) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(12)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x2[0] + [-1]x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥)∧[bni_27 + (-1)Bound*bni_27] + [(-1)bni_27]x1[0] + [bni_27]x0[0] ≥ 0∧[1 + (-1)bso_28] ≥ 0)

We simplified constraint (12) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(13)    (x0[0] ≥ 0∧x2[0] + [-2] + [-1]x1[0] + [-1]x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥)∧[(3)bni_27 + (-1)Bound*bni_27] + [bni_27]x0[0] ≥ 0∧[1 + (-1)bso_28] ≥ 0)

We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(14)    (x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥)∧[(3)bni_27 + (-1)Bound*bni_27] + [bni_27]x0[0] ≥ 0∧[1 + (-1)bso_28] ≥ 0)
We consider the chain 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0]) → COND_2773_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0]), COND_2773_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[1])), x1[1], x2[1]) → 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0), 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2]) which results in the following constraint:
(15)    (&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1)))=TRUE∧java.lang.Object(Carre(x0[0]))=java.lang.Object(Carre(x0[1]))∧x1[0]=x1[1]∧x2[0]=x2[1]∧java.lang.Object(Carre(x0[1]))=java.lang.Object(Carre(x0[2]))∧+(x1[1], 1)=x1[2]∧0=x2[2] ⇒ COND_2773_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[1])), x1[1], x2[1])≥NonInfC∧COND_2773_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[1])), x1[1], x2[1])≥2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)∧(U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥))

We simplified constraint (15) using rules (I), (II), (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(16)    (>(x0[0], +(x1[0], 1))=TRUE∧>=(x2[0], x0[0])=TRUE∧>(x1[0], -1)=TRUE ⇒ COND_2773_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[0])), x1[0], x2[0])≥NonInfC∧COND_2773_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[0])), x1[0], x2[0])≥2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), +(x1[0], 1), 0)∧(U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥))

We simplified constraint (16) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(17)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x2[0] + [-1]x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥)∧[bni_27 + (-1)Bound*bni_27] + [(-1)bni_27]x1[0] + [bni_27]x0[0] ≥ 0∧[1 + (-1)bso_28] ≥ 0)

We simplified constraint (17) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(18)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x2[0] + [-1]x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥)∧[bni_27 + (-1)Bound*bni_27] + [(-1)bni_27]x1[0] + [bni_27]x0[0] ≥ 0∧[1 + (-1)bso_28] ≥ 0)

We simplified constraint (18) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(19)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x2[0] + [-1]x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥)∧[bni_27 + (-1)Bound*bni_27] + [(-1)bni_27]x1[0] + [bni_27]x0[0] ≥ 0∧[1 + (-1)bso_28] ≥ 0)

We simplified constraint (19) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(20)    (x0[0] ≥ 0∧x2[0] + [-2] + [-1]x1[0] + [-1]x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥)∧[(3)bni_27 + (-1)Bound*bni_27] + [bni_27]x0[0] ≥ 0∧[1 + (-1)bso_28] ≥ 0)

We simplified constraint (20) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(21)    (x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥)∧[(3)bni_27 + (-1)Bound*bni_27] + [bni_27]x0[0] ≥ 0∧[1 + (-1)bso_28] ≥ 0)

For Pair 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0)), x1, x2) → COND_2773_0_IMPRIMER_GE1(&&(>(x2, -1), <(x2, x0)), java.lang.Object(Carre(x0)), x1, x2) the following chains were created:

We consider the chain 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2]), COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1)) which results in the following constraint:
(22)    (&&(>(x2[2], -1), <(x2[2], x0[2]))=TRUE∧java.lang.Object(Carre(x0[2]))=java.lang.Object(Carre(x0[3]))∧x1[2]=x1[3]∧x2[2]=x2[3] ⇒ 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥NonInfC∧2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])∧(U^Increasing(COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥))

We simplified constraint (22) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(23)    (>(x2[2], -1)=TRUE∧<(x2[2], x0[2])=TRUE ⇒ 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥NonInfC∧2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])∧(U^Increasing(COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥))

We simplified constraint (23) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(24)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥)∧[bni_29 + (-1)Bound*bni_29] + [(-1)bni_29]x1[2] + [bni_29]x0[2] ≥ 0∧[(-1)bso_30] ≥ 0)

We simplified constraint (24) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(25)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥)∧[bni_29 + (-1)Bound*bni_29] + [(-1)bni_29]x1[2] + [bni_29]x0[2] ≥ 0∧[(-1)bso_30] ≥ 0)

We simplified constraint (25) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(26)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥)∧[bni_29 + (-1)Bound*bni_29] + [(-1)bni_29]x1[2] + [bni_29]x0[2] ≥ 0∧[(-1)bso_30] ≥ 0)

We simplified constraint (26) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(27)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥)∧[(-1)bni_29] = 0∧[bni_29 + (-1)Bound*bni_29] + [bni_29]x0[2] ≥ 0∧0 = 0∧[(-1)bso_30] ≥ 0)

We simplified constraint (27) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(28)    (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥)∧[(-1)bni_29] = 0∧[(2)bni_29 + (-1)Bound*bni_29] + [bni_29]x2[2] + [bni_29]x0[2] ≥ 0∧0 = 0∧[(-1)bso_30] ≥ 0)

For Pair COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0)), x1, x2) → 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0)), x1, +(x2, 1)) the following chains were created:

We consider the chain 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2]), COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1)), 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0]) → COND_2773_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0]) which results in the following constraint:
(29)    (&&(>(x2[2], -1), <(x2[2], x0[2]))=TRUE∧java.lang.Object(Carre(x0[2]))=java.lang.Object(Carre(x0[3]))∧x1[2]=x1[3]∧x2[2]=x2[3]∧java.lang.Object(Carre(x0[3]))=java.lang.Object(Carre(x0[0]))∧x1[3]=x1[0]∧+(x2[3], 1)=x2[0] ⇒ COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3])≥NonInfC∧COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3])≥2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))∧(U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥))

We simplified constraint (29) using rules (I), (II), (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(30)    (>(x2[2], -1)=TRUE∧<(x2[2], x0[2])=TRUE ⇒ COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥NonInfC∧COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], +(x2[2], 1))∧(U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥))

We simplified constraint (30) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(31)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[bni_31 + (-1)Bound*bni_31] + [(-1)bni_31]x1[2] + [bni_31]x0[2] ≥ 0∧[(-1)bso_32] ≥ 0)

We simplified constraint (31) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(32)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[bni_31 + (-1)Bound*bni_31] + [(-1)bni_31]x1[2] + [bni_31]x0[2] ≥ 0∧[(-1)bso_32] ≥ 0)

We simplified constraint (32) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(33)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[bni_31 + (-1)Bound*bni_31] + [(-1)bni_31]x1[2] + [bni_31]x0[2] ≥ 0∧[(-1)bso_32] ≥ 0)

We simplified constraint (33) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(34)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[(-1)bni_31] = 0∧[bni_31 + (-1)Bound*bni_31] + [bni_31]x0[2] ≥ 0∧0 = 0∧[(-1)bso_32] ≥ 0)

We simplified constraint (34) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(35)    (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[(-1)bni_31] = 0∧[(2)bni_31 + (-1)Bound*bni_31] + [bni_31]x2[2] + [bni_31]x0[2] ≥ 0∧0 = 0∧[(-1)bso_32] ≥ 0)
We consider the chain 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2]), COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1)), 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2]) which results in the following constraint:
(36)    (&&(>(x2[2], -1), <(x2[2], x0[2]))=TRUE∧java.lang.Object(Carre(x0[2]))=java.lang.Object(Carre(x0[3]))∧x1[2]=x1[3]∧x2[2]=x2[3]∧java.lang.Object(Carre(x0[3]))=java.lang.Object(Carre(x0[2]1))∧x1[3]=x1[2]1∧+(x2[3], 1)=x2[2]1 ⇒ COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3])≥NonInfC∧COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3])≥2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))∧(U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥))

We simplified constraint (36) using rules (I), (II), (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(37)    (>(x2[2], -1)=TRUE∧<(x2[2], x0[2])=TRUE ⇒ COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥NonInfC∧COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], +(x2[2], 1))∧(U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥))

We simplified constraint (37) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(38)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[bni_31 + (-1)Bound*bni_31] + [(-1)bni_31]x1[2] + [bni_31]x0[2] ≥ 0∧[(-1)bso_32] ≥ 0)

We simplified constraint (38) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(39)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[bni_31 + (-1)Bound*bni_31] + [(-1)bni_31]x1[2] + [bni_31]x0[2] ≥ 0∧[(-1)bso_32] ≥ 0)

We simplified constraint (39) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(40)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[bni_31 + (-1)Bound*bni_31] + [(-1)bni_31]x1[2] + [bni_31]x0[2] ≥ 0∧[(-1)bso_32] ≥ 0)

We simplified constraint (40) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(41)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[(-1)bni_31] = 0∧[bni_31 + (-1)Bound*bni_31] + [bni_31]x0[2] ≥ 0∧0 = 0∧[(-1)bso_32] ≥ 0)

We simplified constraint (41) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(42)    (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[(-1)bni_31] = 0∧[(2)bni_31 + (-1)Bound*bni_31] + [bni_31]x2[2] + [bni_31]x0[2] ≥ 0∧0 = 0∧[(-1)bso_32] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0)), x1, x2) → COND_2773_0_IMPRIMER_GE(&&(&&(>=(x2, x0), >(x1, -1)), >(x0, +(x1, 1))), java.lang.Object(Carre(x0)), x1, x2)
- (x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2773_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0])), ≥)∧[(3)bni_25 + (-1)Bound*bni_25] + [bni_25]x0[0] ≥ 0∧[(-1)bso_26] ≥ 0)
COND_2773_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0)), x1, x2) → 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0)), +(x1, 1), 0)
- (x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥)∧[(3)bni_27 + (-1)Bound*bni_27] + [bni_27]x0[0] ≥ 0∧[1 + (-1)bso_28] ≥ 0)
- (x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)), ≥)∧[(3)bni_27 + (-1)Bound*bni_27] + [bni_27]x0[0] ≥ 0∧[1 + (-1)bso_28] ≥ 0)
2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0)), x1, x2) → COND_2773_0_IMPRIMER_GE1(&&(>(x2, -1), <(x2, x0)), java.lang.Object(Carre(x0)), x1, x2)
- (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥)∧[(-1)bni_29] = 0∧[(2)bni_29 + (-1)Bound*bni_29] + [bni_29]x2[2] + [bni_29]x0[2] ≥ 0∧0 = 0∧[(-1)bso_30] ≥ 0)
COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0)), x1, x2) → 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0)), x1, +(x2, 1))
- (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[(-1)bni_31] = 0∧[(2)bni_31 + (-1)Bound*bni_31] + [bni_31]x2[2] + [bni_31]x0[2] ≥ 0∧0 = 0∧[(-1)bso_32] ≥ 0)
- (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[(-1)bni_31] = 0∧[(2)bni_31 + (-1)Bound*bni_31] + [bni_31]x2[2] + [bni_31]x0[2] ≥ 0∧0 = 0∧[(-1)bso_32] ≥ 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0
POL(FALSE) = [2]
POL(2773_0_IMPRIMER_GE(x₁, x₂, x₃)) = [-1] + [-1]x₂ + [-1]x₁
POL(java.lang.Object(x₁)) = [-1] + x₁
POL(Carre(x₁)) = [-1] + [-1]x₁
POL(COND_2773_0_IMPRIMER_GE(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + [-1]x₂ + [-1]x₁
POL(&&(x₁, x₂)) = 0
POL(>=(x₁, x₂)) = [-1]
POL(>(x₁, x₂)) = [-1]
POL(-1) = [-1]
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(0) = 0
POL(COND_2773_0_IMPRIMER_GE1(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + [-1]x₂ + [-1]x₁
POL(<(x₁, x₂)) = [-1]

The following pairs are in P_>:

COND_2773_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[1])), x1[1], x2[1]) → 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)

The following pairs are in P_bound:

2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0]) → COND_2773_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0])
COND_2773_0_IMPRIMER_GE(TRUE, java.lang.Object(Carre(x0[1])), x1[1], x2[1]) → 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[1])), +(x1[1], 1), 0)

The following pairs are in P_≥:

2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0]) → COND_2773_0_IMPRIMER_GE(&&(&&(>=(x2[0], x0[0]), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), java.lang.Object(Carre(x0[0])), x1[0], x2[0])
2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])
COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))

At least the following rules have been oriented under context sensitive arithmetic replacement:

TRUE¹ → &&(TRUE, TRUE)¹
FALSE¹ → &&(TRUE, FALSE)¹
FALSE¹ → &&(FALSE, TRUE)¹
FALSE¹ → &&(FALSE, FALSE)¹

(9) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[0])), x1[0], x2[0]) → COND_2773_0_IMPRIMER_GE(x2[0] >= x0[0] && x1[0] > -1 && x0[0] > x1[0] + 1, java.lang.Object(Carre(x0[0])), x1[0], x2[0])
(2): 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_2773_0_IMPRIMER_GE1(x2[2] > -1 && x2[2] < x0[2], java.lang.Object(Carre(x0[2])), x1[2], x2[2])
(3): COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], x2[3] + 1)

(3) -> (0), if (java.lang.Object(Carre(x0[3])) →^* java.lang.Object(Carre(x0[0]))∧x1[3] →^* x1[0]∧x2[3] + 1 →^* x2[0])

(3) -> (2), if (java.lang.Object(Carre(x0[3])) →^* java.lang.Object(Carre(x0[2]))∧x1[3] →^* x1[2]∧x2[3] + 1 →^* x2[2])

(2) -> (3), if (x2[2] > -1 && x2[2] < x0[2] ∧java.lang.Object(Carre(x0[2])) →^* java.lang.Object(Carre(x0[3]))∧x1[2] →^* x1[3]∧x2[2] →^* x2[3])

The set Q is empty.

(10) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(11) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(3): COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], x2[3] + 1)
(2): 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_2773_0_IMPRIMER_GE1(x2[2] > -1 && x2[2] < x0[2], java.lang.Object(Carre(x0[2])), x1[2], x2[2])

(3) -> (2), if (java.lang.Object(Carre(x0[3])) →^* java.lang.Object(Carre(x0[2]))∧x1[3] →^* x1[2]∧x2[3] + 1 →^* x2[2])

(2) -> (3), if (x2[2] > -1 && x2[2] < x0[2] ∧java.lang.Object(Carre(x0[2])) →^* java.lang.Object(Carre(x0[3]))∧x1[2] →^* x1[3]∧x2[2] →^* x2[3])

The set Q is empty.

(12) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpDefaultShapeHeuristic@92341f1 Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 1 Max Right Steps: 1

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1)) the following chains were created:

We consider the chain 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2]), COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1)), 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2]) which results in the following constraint:
(1)    (&&(>(x2[2], -1), <(x2[2], x0[2]))=TRUE∧java.lang.Object(Carre(x0[2]))=java.lang.Object(Carre(x0[3]))∧x1[2]=x1[3]∧x2[2]=x2[3]∧java.lang.Object(Carre(x0[3]))=java.lang.Object(Carre(x0[2]1))∧x1[3]=x1[2]1∧+(x2[3], 1)=x2[2]1 ⇒ COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3])≥NonInfC∧COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3])≥2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))∧(U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥))

We simplified constraint (1) using rules (I), (II), (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(2)    (>(x2[2], -1)=TRUE∧<(x2[2], x0[2])=TRUE ⇒ COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥NonInfC∧COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], +(x2[2], 1))∧(U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[bni_19 + (-1)Bound*bni_19] + [(-1)bni_19]x2[2] + [bni_19]x0[2] ≥ 0∧[1 + (-1)bso_20] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[bni_19 + (-1)Bound*bni_19] + [(-1)bni_19]x2[2] + [bni_19]x0[2] ≥ 0∧[1 + (-1)bso_20] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧[bni_19 + (-1)Bound*bni_19] + [(-1)bni_19]x2[2] + [bni_19]x0[2] ≥ 0∧[1 + (-1)bso_20] ≥ 0)

We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(6)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧0 = 0∧[bni_19 + (-1)Bound*bni_19] + [(-1)bni_19]x2[2] + [bni_19]x0[2] ≥ 0∧0 = 0∧[1 + (-1)bso_20] ≥ 0)

We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(7)    (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧0 = 0∧[(2)bni_19 + (-1)Bound*bni_19] + [bni_19]x0[2] ≥ 0∧0 = 0∧[1 + (-1)bso_20] ≥ 0)

For Pair 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2]) the following chains were created:

We consider the chain 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2]), COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1)) which results in the following constraint:
(8)    (&&(>(x2[2], -1), <(x2[2], x0[2]))=TRUE∧java.lang.Object(Carre(x0[2]))=java.lang.Object(Carre(x0[3]))∧x1[2]=x1[3]∧x2[2]=x2[3] ⇒ 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥NonInfC∧2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])∧(U^Increasing(COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥))

We simplified constraint (8) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(9)    (>(x2[2], -1)=TRUE∧<(x2[2], x0[2])=TRUE ⇒ 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥NonInfC∧2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2])≥COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])∧(U^Increasing(COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥))

We simplified constraint (9) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(10)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥)∧[bni_21 + (-1)Bound*bni_21] + [(-1)bni_21]x2[2] + [bni_21]x0[2] ≥ 0∧[(-1)bso_22] ≥ 0)

We simplified constraint (10) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(11)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥)∧[bni_21 + (-1)Bound*bni_21] + [(-1)bni_21]x2[2] + [bni_21]x0[2] ≥ 0∧[(-1)bso_22] ≥ 0)

We simplified constraint (11) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(12)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥)∧[bni_21 + (-1)Bound*bni_21] + [(-1)bni_21]x2[2] + [bni_21]x0[2] ≥ 0∧[(-1)bso_22] ≥ 0)

We simplified constraint (12) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(13)    (x2[2] ≥ 0∧x0[2] + [-1] + [-1]x2[2] ≥ 0 ⇒ (U^Increasing(COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥)∧0 = 0∧[bni_21 + (-1)Bound*bni_21] + [(-1)bni_21]x2[2] + [bni_21]x0[2] ≥ 0∧0 = 0∧[(-1)bso_22] ≥ 0)

We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(14)    (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥)∧0 = 0∧[(2)bni_21 + (-1)Bound*bni_21] + [bni_21]x0[2] ≥ 0∧0 = 0∧[(-1)bso_22] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))
- (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))), ≥)∧0 = 0∧[(2)bni_19 + (-1)Bound*bni_19] + [bni_19]x0[2] ≥ 0∧0 = 0∧[1 + (-1)bso_20] ≥ 0)
2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])
- (x2[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])), ≥)∧0 = 0∧[(2)bni_21 + (-1)Bound*bni_21] + [bni_21]x0[2] ≥ 0∧0 = 0∧[(-1)bso_22] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = [2]
POL(COND_2773_0_IMPRIMER_GE1(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₄ + [-1]x₂
POL(java.lang.Object(x₁)) = [-1] + x₁
POL(Carre(x₁)) = [-1] + [-1]x₁
POL(2773_0_IMPRIMER_GE(x₁, x₂, x₃)) = [-1] + [-1]x₃ + [-1]x₁
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(&&(x₁, x₂)) = [-1]
POL(>(x₁, x₂)) = [-1]
POL(-1) = [-1]
POL(<(x₁, x₂)) = [-1]

The following pairs are in P_>:

COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))

The following pairs are in P_bound:

COND_2773_0_IMPRIMER_GE1(TRUE, java.lang.Object(Carre(x0[3])), x1[3], x2[3]) → 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[3])), x1[3], +(x2[3], 1))
2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])

The following pairs are in P_≥:

2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_2773_0_IMPRIMER_GE1(&&(>(x2[2], -1), <(x2[2], x0[2])), java.lang.Object(Carre(x0[2])), x1[2], x2[2])

At least the following rules have been oriented under context sensitive arithmetic replacement:

TRUE¹ → &&(TRUE, TRUE)¹
FALSE¹ → &&(FALSE, FALSE)¹

(13) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(2): 2773_0_IMPRIMER_GE(java.lang.Object(Carre(x0[2])), x1[2], x2[2]) → COND_2773_0_IMPRIMER_GE1(x2[2] > -1 && x2[2] < x0[2], java.lang.Object(Carre(x0[2])), x1[2], x2[2])

The set Q is empty.

(14) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(15) TRUE

(16) Obligation:

(17) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 32 rules for P and 0 rules for R.

P rules:
1970_0_init_ConstantStackPush(EOS(STATIC_1970), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i258, i258) → 1977_0_init_GE(EOS(STATIC_1977), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i258, i258, 3)
1977_0_init_GE(EOS(STATIC_1977), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i268, matching1) → 1979_0_init_GE(EOS(STATIC_1979), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i268, 3) | =(matching1, 3)
1979_0_init_GE(EOS(STATIC_1979), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i268, matching1) → 1983_0_init_ConstantStackPush(EOS(STATIC_1983), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268) | &&(<(i268, 3), =(matching1, 3))
1983_0_init_ConstantStackPush(EOS(STATIC_1983), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268) → 1988_0_init_Store(EOS(STATIC_1988), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, 0)
1988_0_init_Store(EOS(STATIC_1988), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, matching1) → 1992_0_init_Load(EOS(STATIC_1992), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, 0) | =(matching1, 0)
1992_0_init_Load(EOS(STATIC_1992), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, matching1) → 2097_0_init_Load(EOS(STATIC_2097), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, 0) | =(matching1, 0)
2097_0_init_Load(EOS(STATIC_2097), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i284) → 2196_0_init_Load(EOS(STATIC_2196), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i284)
2196_0_init_Load(EOS(STATIC_2196), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i314) → 2301_0_init_Load(EOS(STATIC_2301), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i314)
2301_0_init_Load(EOS(STATIC_2301), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i339) → 2306_0_init_ConstantStackPush(EOS(STATIC_2306), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i339, i339)
2306_0_init_ConstantStackPush(EOS(STATIC_2306), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i339, i339) → 2314_0_init_GE(EOS(STATIC_2314), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i339, i339, 3)
2314_0_init_GE(EOS(STATIC_2314), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351, i351, matching1) → 2323_0_init_GE(EOS(STATIC_2323), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351, i351, 3) | =(matching1, 3)
2314_0_init_GE(EOS(STATIC_2314), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, matching1, matching2, matching3) → 2324_0_init_GE(EOS(STATIC_2324), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, 3, 3, 3) | &&(&&(=(matching1, 3), =(matching2, 3)), =(matching3, 3))
2323_0_init_GE(EOS(STATIC_2323), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351, i351, matching1) → 2328_0_init_Load(EOS(STATIC_2328), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351) | &&(<(i351, 3), =(matching1, 3))
2328_0_init_Load(EOS(STATIC_2328), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351) → 2333_0_init_FieldAccess(EOS(STATIC_2333), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))))
2333_0_init_FieldAccess(EOS(STATIC_2333), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27))))) → 2338_0_init_Load(EOS(STATIC_2338), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351, java.lang.Object(ARRAY(i27)))
2338_0_init_Load(EOS(STATIC_2338), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351, java.lang.Object(ARRAY(i27))) → 2349_0_init_ArrayAccess(EOS(STATIC_2349), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351, java.lang.Object(ARRAY(i27)), i268)
2349_0_init_ArrayAccess(EOS(STATIC_2349), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351, java.lang.Object(ARRAY(i27)), i268) → 2352_0_init_ArrayAccess(EOS(STATIC_2352), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351, java.lang.Object(ARRAY(i27)), i268)
2352_0_init_ArrayAccess(EOS(STATIC_2352), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351, java.lang.Object(ARRAY(i27)), i268) → 2356_0_init_Load(EOS(STATIC_2356), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351, o1648) | <(i268, i27)
2356_0_init_Load(EOS(STATIC_2356), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351, o1648) → 2360_0_init_ConstantStackPush(EOS(STATIC_2360), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351, o1648, i351)
2360_0_init_ConstantStackPush(EOS(STATIC_2360), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351, o1648, i351) → 2363_0_init_ArrayAccess(EOS(STATIC_2363), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351, o1648, i351, 0)
2363_0_init_ArrayAccess(EOS(STATIC_2363), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351, java.lang.Object(o1657put), i351, matching1) → 2369_0_init_ArrayAccess(EOS(STATIC_2369), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351, java.lang.Object(o1657put), i351, 0) | =(matching1, 0)
2369_0_init_ArrayAccess(EOS(STATIC_2369), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351, java.lang.Object(ARRAY(i359)), i351, matching1) → 2374_0_init_ArrayAccess(EOS(STATIC_2374), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351, java.lang.Object(ARRAY(i359)), i351, 0) | &&(>=(i359, 0), =(matching1, 0))
2374_0_init_ArrayAccess(EOS(STATIC_2374), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351, java.lang.Object(ARRAY(i359)), i351, matching1) → 2378_0_init_ArrayAccess(EOS(STATIC_2378), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351, java.lang.Object(ARRAY(i359)), i351, 0) | =(matching1, 0)
2378_0_init_ArrayAccess(EOS(STATIC_2378), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351, java.lang.Object(ARRAY(i359)), i351, matching1) → 2390_0_init_Inc(EOS(STATIC_2390), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351) | &&(<(i351, i359), =(matching1, 0))
2390_0_init_Inc(EOS(STATIC_2390), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i351) → 2395_0_init_JMP(EOS(STATIC_2395), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, +(i351, 1)) | >=(i351, 0)
2395_0_init_JMP(EOS(STATIC_2395), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i362) → 2405_0_init_Load(EOS(STATIC_2405), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i362)
2405_0_init_Load(EOS(STATIC_2405), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i362) → 2301_0_init_Load(EOS(STATIC_2301), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, i362)
2324_0_init_GE(EOS(STATIC_2324), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268, matching1, matching2, matching3) → 2329_0_init_Inc(EOS(STATIC_2329), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268) | &&(&&(=(matching1, 3), =(matching2, 3)), =(matching3, 3))
2329_0_init_Inc(EOS(STATIC_2329), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i268) → 2335_0_init_JMP(EOS(STATIC_2335), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), +(i268, 1)) | >=(i268, 0)
2335_0_init_JMP(EOS(STATIC_2335), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i352) → 2341_0_init_Load(EOS(STATIC_2341), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i352)
2341_0_init_Load(EOS(STATIC_2341), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i352) → 1967_0_init_Load(EOS(STATIC_1967), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i352)
1967_0_init_Load(EOS(STATIC_1967), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i258) → 1970_0_init_ConstantStackPush(EOS(STATIC_1970), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i27)))), i258, i258)
R rules:

Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.

P rules:
2314_0_init_GE(EOS(STATIC_2314), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(x0)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(x0)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(x0)))), x1, x2, x2, 3) → 2314_0_init_GE(EOS(STATIC_2314), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(x0)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(x0)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(x0)))), x1, +(x2, 1), +(x2, 1), 3) | &&(&&(>(+(x2, 1), 0), <(x2, 3)), <(x1, x0))
2314_0_init_GE(EOS(STATIC_2314), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(x0)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(x0)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(x0)))), x1, 3, 3, 3) → 2314_0_init_GE(EOS(STATIC_2314), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(x0)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(x0)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(x0)))), +(x1, 1), 0, 0, 3) | &&(>(+(x1, 1), 0), <(x1, 2))
R rules:

Filtered ground terms:

2314_0_init_GE(x1, x2, x3, x4, x5, x6, x7, x8) → 2314_0_init_GE(x2, x3, x4, x5, x6, x7)
Carre(x1, x2) → Carre(x2)
EOS(x1) → EOS
Cond_2314_0_init_GE1(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_2314_0_init_GE1(x1, x3, x4, x5, x6)
Cond_2314_0_init_GE(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_2314_0_init_GE(x1, x3, x4, x5, x6, x7, x8)

Filtered duplicate args:

2314_0_init_GE(x1, x2, x3, x4, x5, x6) → 2314_0_init_GE(x3, x4, x6)
Cond_2314_0_init_GE(x1, x2, x3, x4, x5, x6, x7) → Cond_2314_0_init_GE(x1, x4, x5, x7)
Cond_2314_0_init_GE1(x1, x2, x3, x4, x5) → Cond_2314_0_init_GE1(x1, x4, x5)

Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.

P rules:
2314_0_init_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, x2) → 2314_0_init_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, +(x2, 1)) | &&(&&(>(x2, -1), <(x2, 3)), <(x1, x0))
2314_0_init_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, 3) → 2314_0_init_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), +(x1, 1), 0) | &&(>(x1, -1), <(x1, 2))
R rules:

Finished conversion. Obtained 4 rules for P and 0 rules for R. System has predefined symbols.

P rules:
2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, x2) → COND_2314_0_INIT_GE(&&(&&(>(x2, -1), <(x2, 3)), <(x1, x0)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, x2)
COND_2314_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, x2) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, +(x2, 1))
2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, 3) → COND_2314_0_INIT_GE1(&&(>(x1, -1), <(x1, 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, 3)
COND_2314_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, 3) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), +(x1, 1), 0)
R rules:

(18) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]) → COND_2314_0_INIT_GE(x2[0] > -1 && x2[0] < 3 && x1[0] < x0[0], java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])
(1): COND_2314_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1]) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1] + 1)
(2): 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3) → COND_2314_0_INIT_GE1(x1[2] > -1 && x1[2] < 2, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)
(3): COND_2314_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3] + 1, 0)

(0) -> (1), if (x2[0] > -1 && x2[0] < 3 && x1[0] < x0[0] ∧java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1]))))∧x1[0] →^* x1[1]∧x2[0] →^* x2[1])

(1) -> (0), if (java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0]))))∧x1[1] →^* x1[0]∧x2[1] + 1 →^* x2[0])

(1) -> (2), if (java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2]))))∧x1[1] →^* x1[2]∧x2[1] + 1 →^* 3)

(2) -> (3), if (x1[2] > -1 && x1[2] < 2 ∧java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3]))))∧x1[2] →^* x1[3])

(3) -> (0), if (java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0]))))∧x1[3] + 1 →^* x1[0]∧0 →^* x2[0])

(3) -> (2), if (java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2]))))∧x1[3] + 1 →^* x1[2]∧0 →^* 3)

The set Q is empty.

(19) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@7669bcb Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, x2) → COND_2314_0_INIT_GE(&&(&&(>(x2, -1), <(x2, 3)), <(x1, x0)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, x2) the following chains were created:

We consider the chain 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]) → COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]), COND_2314_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1]) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1)) which results in the following constraint:
(1)    (&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0]))=TRUE∧java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0]))))=java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1]))))∧x1[0]=x1[1]∧x2[0]=x2[1] ⇒ 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])≥NonInfC∧2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])≥COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])∧(U^Increasing(COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥))

We simplified constraint (1) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(2)    (<(x1[0], x0[0])=TRUE∧>(x2[0], -1)=TRUE∧<(x2[0], 3)=TRUE ⇒ 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])≥NonInfC∧2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])≥COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])∧(U^Increasing(COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x0[0] + [-1] + [-1]x1[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)bni_12 + (-1)Bound*bni_12] + [(-1)bni_12]x1[0] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x0[0] + [-1] + [-1]x1[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)bni_12 + (-1)Bound*bni_12] + [(-1)bni_12]x1[0] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x0[0] + [-1] + [-1]x1[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)bni_12 + (-1)Bound*bni_12] + [(-1)bni_12]x1[0] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x0[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)

We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(7)    (x0[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)

(8)    (x0[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)

For Pair COND_2314_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, x2) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, +(x2, 1)) the following chains were created:

We consider the chain COND_2314_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1]) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1)) which results in the following constraint:
(9)    (COND_2314_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1])≥NonInfC∧COND_2314_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1])≥2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))∧(U^Increasing(2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))), ≥))

We simplified constraint (9) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(10)    ((U^Increasing(2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧[(-1)bso_15] ≥ 0)

We simplified constraint (10) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(11)    ((U^Increasing(2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧[(-1)bso_15] ≥ 0)

We simplified constraint (11) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(12)    ((U^Increasing(2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧[(-1)bso_15] ≥ 0)

We simplified constraint (12) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(13)    ((U^Increasing(2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_15] ≥ 0)

For Pair 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, 3) → COND_2314_0_INIT_GE1(&&(>(x1, -1), <(x1, 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, 3) the following chains were created:

We consider the chain 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3) → COND_2314_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3), COND_2314_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0) which results in the following constraint:
(14)    (&&(>(x1[2], -1), <(x1[2], 2))=TRUE∧java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2]))))=java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3]))))∧x1[2]=x1[3] ⇒ 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)≥NonInfC∧2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)≥COND_2314_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)∧(U^Increasing(COND_2314_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥))

We simplified constraint (14) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(15)    (>(x1[2], -1)=TRUE∧<(x1[2], 2)=TRUE ⇒ 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)≥NonInfC∧2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)≥COND_2314_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)∧(U^Increasing(COND_2314_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥))

We simplified constraint (15) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(16)    (x1[2] ≥ 0∧[1] + [-1]x1[2] ≥ 0 ⇒ (U^Increasing(COND_2314_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥)∧[(-1)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]x1[2] + [bni_16]x0[2] ≥ 0∧[(-1)bso_17] ≥ 0)

We simplified constraint (16) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(17)    (x1[2] ≥ 0∧[1] + [-1]x1[2] ≥ 0 ⇒ (U^Increasing(COND_2314_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥)∧[(-1)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]x1[2] + [bni_16]x0[2] ≥ 0∧[(-1)bso_17] ≥ 0)

We simplified constraint (17) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(18)    (x1[2] ≥ 0∧[1] + [-1]x1[2] ≥ 0 ⇒ (U^Increasing(COND_2314_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥)∧[(-1)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]x1[2] + [bni_16]x0[2] ≥ 0∧[(-1)bso_17] ≥ 0)

We simplified constraint (18) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(19)    (x1[2] ≥ 0∧[1] + [-1]x1[2] ≥ 0 ⇒ (U^Increasing(COND_2314_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥)∧[bni_16] = 0∧[(-1)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]x1[2] ≥ 0∧0 = 0∧[(-1)bso_17] ≥ 0)

For Pair COND_2314_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, 3) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), +(x1, 1), 0) the following chains were created:

We consider the chain COND_2314_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0) which results in the following constraint:
(20)    (COND_2314_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3)≥NonInfC∧COND_2314_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3)≥2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)∧(U^Increasing(2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)), ≥))

We simplified constraint (20) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(21)    ((U^Increasing(2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)), ≥)∧[bni_18] = 0∧[1 + (-1)bso_19] ≥ 0)

We simplified constraint (21) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(22)    ((U^Increasing(2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)), ≥)∧[bni_18] = 0∧[1 + (-1)bso_19] ≥ 0)

We simplified constraint (22) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(23)    ((U^Increasing(2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)), ≥)∧[bni_18] = 0∧[1 + (-1)bso_19] ≥ 0)

We simplified constraint (23) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(24)    ((U^Increasing(2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)), ≥)∧[bni_18] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_19] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, x2) → COND_2314_0_INIT_GE(&&(&&(>(x2, -1), <(x2, 3)), <(x1, x0)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, x2)
- (x0[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)
- (x0[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)
COND_2314_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, x2) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, +(x2, 1))
- ((U^Increasing(2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))), ≥)∧[bni_14] = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_15] ≥ 0)
2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, 3) → COND_2314_0_INIT_GE1(&&(>(x1, -1), <(x1, 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, 3)
- (x1[2] ≥ 0∧[1] + [-1]x1[2] ≥ 0 ⇒ (U^Increasing(COND_2314_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥)∧[bni_16] = 0∧[(-1)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]x1[2] ≥ 0∧0 = 0∧[(-1)bso_17] ≥ 0)
COND_2314_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), x1, 3) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0)))), +(x1, 1), 0)
- ((U^Increasing(2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)), ≥)∧[bni_18] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_19] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(2314_0_INIT_GE(x₁, x₂, x₃)) = [-1] + [-1]x₂ + x₁
POL(java.lang.Object(x₁)) = x₁
POL(Carre(x₁)) = x₁
POL(ARRAY(x₁)) = x₁
POL(COND_2314_0_INIT_GE(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + x₂
POL(&&(x₁, x₂)) = [-1]
POL(>(x₁, x₂)) = [-1]
POL(-1) = [-1]
POL(<(x₁, x₂)) = [-1]
POL(3) = [3]
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(COND_2314_0_INIT_GE1(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + x₂
POL(2) = [2]
POL(0) = 0

The following pairs are in P_>:

COND_2314_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)

The following pairs are in P_bound:

2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]) → COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])

The following pairs are in P_≥:

2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]) → COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])
COND_2314_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1]) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))
2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3) → COND_2314_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)

There are no usable rules.

(20) Complex Obligation (AND)

(21) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

(1) -> (0), if (java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0]))))∧x1[1] →^* x1[0]∧x2[1] + 1 →^* x2[0])

(1) -> (2), if (java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2]))))∧x1[1] →^* x1[2]∧x2[1] + 1 →^* 3)

The set Q is empty.

(22) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(23) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_2314_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1]) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1] + 1)
(0): 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]) → COND_2314_0_INIT_GE(x2[0] > -1 && x2[0] < 3 && x1[0] < x0[0], java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])

(1) -> (0), if (java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0]))))∧x1[1] →^* x1[0]∧x2[1] + 1 →^* x2[0])

The set Q is empty.

(24) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@7669bcb Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair COND_2314_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1]) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1)) the following chains were created:

We consider the chain COND_2314_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1]) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1)) which results in the following constraint:
(1)    (COND_2314_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1])≥NonInfC∧COND_2314_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1])≥2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))∧(U^Increasing(2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))), ≥))

We simplified constraint (1) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(2)    ((U^Increasing(2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))), ≥)∧[bni_10] = 0∧[1 + (-1)bso_11] ≥ 0)

We simplified constraint (2) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(3)    ((U^Increasing(2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))), ≥)∧[bni_10] = 0∧[1 + (-1)bso_11] ≥ 0)

We simplified constraint (3) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(4)    ((U^Increasing(2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))), ≥)∧[bni_10] = 0∧[1 + (-1)bso_11] ≥ 0)

We simplified constraint (4) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(5)    ((U^Increasing(2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))), ≥)∧[bni_10] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_11] ≥ 0)

For Pair 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]) → COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]) the following chains were created:

We consider the chain 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]) → COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]), COND_2314_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1]) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1)) which results in the following constraint:
(6)    (&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0]))=TRUE∧java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0]))))=java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1]))))∧x1[0]=x1[1]∧x2[0]=x2[1] ⇒ 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])≥NonInfC∧2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])≥COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])∧(U^Increasing(COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥))

We simplified constraint (6) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(7)    (<(x1[0], x0[0])=TRUE∧>(x2[0], -1)=TRUE∧<(x2[0], 3)=TRUE ⇒ 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])≥NonInfC∧2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])≥COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])∧(U^Increasing(COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    (x0[0] + [-1] + [-1]x1[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)bni_12 + (-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [(-1)bni_12]x1[0] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    (x0[0] + [-1] + [-1]x1[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)bni_12 + (-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [(-1)bni_12]x1[0] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    (x0[0] + [-1] + [-1]x1[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)bni_12 + (-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [(-1)bni_12]x1[0] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)

We simplified constraint (10) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(11)    (x0[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0 ⇒ (U^Increasing(COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)

We simplified constraint (11) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(12)    (x0[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)

(13)    (x0[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

COND_2314_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1]) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))
- ((U^Increasing(2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))), ≥)∧[bni_10] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_11] ≥ 0)
2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]) → COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])
- (x0[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)
- (x0[0] ≥ 0∧x2[0] ≥ 0∧[2] + [-1]x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])), ≥)∧[(-1)Bound*bni_12] + [(-1)bni_12]x2[0] + [bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(COND_2314_0_INIT_GE(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + x₂ + [-1]x₄
POL(java.lang.Object(x₁)) = x₁
POL(Carre(x₁)) = x₁
POL(ARRAY(x₁)) = x₁
POL(2314_0_INIT_GE(x₁, x₂, x₃)) = [-1] + [-1]x₃ + [-1]x₂ + x₁
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(&&(x₁, x₂)) = [-1]
POL(>(x₁, x₂)) = [-1]
POL(-1) = [-1]
POL(<(x₁, x₂)) = [-1]
POL(3) = [3]

The following pairs are in P_>:

COND_2314_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1]) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], +(x2[1], 1))

The following pairs are in P_bound:

2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]) → COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])

The following pairs are in P_≥:

2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0]) → COND_2314_0_INIT_GE(&&(&&(>(x2[0], -1), <(x2[0], 3)), <(x1[0], x0[0])), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[0])))), x1[0], x2[0])

There are no usable rules.

(25) Complex Obligation (AND)

(26) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

(27) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(28) TRUE

(29) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

(30) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(31) TRUE

(32) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_2314_0_INIT_GE(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1]) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))), x1[1], x2[1] + 1)
(2): 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3) → COND_2314_0_INIT_GE1(x1[2] > -1 && x1[2] < 2, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)
(3): COND_2314_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3] + 1, 0)

(1) -> (2), if (java.lang.Object(Carre(java.lang.Object(ARRAY(x0[1])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2]))))∧x1[1] →^* x1[2]∧x2[1] + 1 →^* 3)

(3) -> (2), if (java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2]))))∧x1[3] + 1 →^* x1[2]∧0 →^* 3)

(2) -> (3), if (x1[2] > -1 && x1[2] < 2 ∧java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3]))))∧x1[2] →^* x1[3])

The set Q is empty.

(33) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(34) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(3): COND_2314_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3] + 1, 0)
(2): 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3) → COND_2314_0_INIT_GE1(x1[2] > -1 && x1[2] < 2, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)

(3) -> (2), if (java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2]))))∧x1[3] + 1 →^* x1[2]∧0 →^* 3)

(2) -> (3), if (x1[2] > -1 && x1[2] < 2 ∧java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))) →^* java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3]))))∧x1[2] →^* x1[3])

The set Q is empty.

(35) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@7669bcb Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair COND_2314_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0) the following chains were created:

We consider the chain COND_2314_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0) which results in the following constraint:
(1)    (COND_2314_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3)≥NonInfC∧COND_2314_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3)≥2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)∧(U^Increasing(2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)), ≥))

We simplified constraint (1) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(2)    ((U^Increasing(2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)), ≥)∧[bni_12] = 0∧[1 + (-1)bso_13] ≥ 0)

We simplified constraint (2) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(3)    ((U^Increasing(2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)), ≥)∧[bni_12] = 0∧[1 + (-1)bso_13] ≥ 0)

We simplified constraint (3) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(4)    ((U^Increasing(2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)), ≥)∧[bni_12] = 0∧[1 + (-1)bso_13] ≥ 0)

We simplified constraint (4) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(5)    ((U^Increasing(2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)), ≥)∧[bni_12] = 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)

For Pair 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3) → COND_2314_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3) the following chains were created:

We consider the chain 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3) → COND_2314_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3), COND_2314_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0) which results in the following constraint:
(6)    (&&(>(x1[2], -1), <(x1[2], 2))=TRUE∧java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2]))))=java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3]))))∧x1[2]=x1[3] ⇒ 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)≥NonInfC∧2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)≥COND_2314_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)∧(U^Increasing(COND_2314_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥))

We simplified constraint (6) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(7)    (>(x1[2], -1)=TRUE∧<(x1[2], 2)=TRUE ⇒ 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)≥NonInfC∧2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)≥COND_2314_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)∧(U^Increasing(COND_2314_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    (x1[2] ≥ 0∧[1] + [-1]x1[2] ≥ 0 ⇒ (U^Increasing(COND_2314_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [(-1)bni_14]x1[2] ≥ 0∧[(-1)bso_15] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    (x1[2] ≥ 0∧[1] + [-1]x1[2] ≥ 0 ⇒ (U^Increasing(COND_2314_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [(-1)bni_14]x1[2] ≥ 0∧[(-1)bso_15] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    (x1[2] ≥ 0∧[1] + [-1]x1[2] ≥ 0 ⇒ (U^Increasing(COND_2314_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [(-1)bni_14]x1[2] ≥ 0∧[(-1)bso_15] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

COND_2314_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)
- ((U^Increasing(2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)), ≥)∧[bni_12] = 0∧0 = 0∧[1 + (-1)bso_13] ≥ 0)
2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3) → COND_2314_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)
- (x1[2] ≥ 0∧[1] + [-1]x1[2] ≥ 0 ⇒ (U^Increasing(COND_2314_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [(-1)bni_14]x1[2] ≥ 0∧[(-1)bso_15] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(COND_2314_0_INIT_GE1(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃
POL(java.lang.Object(x₁)) = [-1]
POL(Carre(x₁)) = [-1]
POL(ARRAY(x₁)) = [-1]
POL(3) = [3]
POL(2314_0_INIT_GE(x₁, x₂, x₃)) = [-1] + [-1]x₂
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(0) = 0
POL(&&(x₁, x₂)) = [-1]
POL(>(x₁, x₂)) = [-1]
POL(-1) = [-1]
POL(<(x₁, x₂)) = [-1]
POL(2) = [2]

The following pairs are in P_>:

COND_2314_0_INIT_GE1(TRUE, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), x1[3], 3) → 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[3])))), +(x1[3], 1), 0)

The following pairs are in P_bound:

2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3) → COND_2314_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)

The following pairs are in P_≥:

2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3) → COND_2314_0_INIT_GE1(&&(>(x1[2], -1), <(x1[2], 2)), java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)

There are no usable rules.

(36) Complex Obligation (AND)

(37) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(2): 2314_0_INIT_GE(java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3) → COND_2314_0_INIT_GE1(x1[2] > -1 && x1[2] < 2, java.lang.Object(Carre(java.lang.Object(ARRAY(x0[2])))), x1[2], 3)

The set Q is empty.

(38) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(39) TRUE

(40) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

(41) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIDPv1Proof (SOUND transformation)

(7) Obligation:

(8) IDPNonInfProof (SOUND transformation)

(9) Obligation:

(10) IDependencyGraphProof (EQUIVALENT transformation)

(11) Obligation:

(12) IDPNonInfProof (SOUND transformation)

(13) Obligation:

(14) IDependencyGraphProof (EQUIVALENT transformation)

(15) TRUE

(16) Obligation:

(17) SCCToIDPv1Proof (SOUND transformation)

(18) Obligation:

(19) IDPNonInfProof (SOUND transformation)

(20) Complex Obligation (AND)

(21) Obligation:

(22) IDependencyGraphProof (EQUIVALENT transformation)

(23) Obligation:

(24) IDPNonInfProof (SOUND transformation)

(25) Complex Obligation (AND)

(26) Obligation:

(27) IDependencyGraphProof (EQUIVALENT transformation)

(28) TRUE

(29) Obligation:

(30) IDependencyGraphProof (EQUIVALENT transformation)

(31) TRUE

(32) Obligation:

(33) IDependencyGraphProof (EQUIVALENT transformation)

(34) Obligation:

(35) IDPNonInfProof (SOUND transformation)

(36) Complex Obligation (AND)

(37) Obligation:

(38) IDependencyGraphProof (EQUIVALENT transformation)

(39) TRUE

(40) Obligation:

(41) IDependencyGraphProof (EQUIVALENT transformation)

(42) TRUE