Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

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:

• Used field analysis yielded the following read fields:
  
  • Carre: [cote]
• Marker field analysis yielded the following relations that could be markers:
  

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 24 IRules

P rules:
f4250_0_imprimer_Load(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i412) → f4252_0_imprimer_FieldAccess(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i412, java.lang.Object(Carre(EOC, i28)))
f4252_0_imprimer_FieldAccess(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i412, java.lang.Object(Carre(EOC, i28))) → f4254_0_imprimer_GE(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i412, i28)
f4254_0_imprimer_GE(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i412, i28) → f4258_0_imprimer_GE(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i412, i28)
f4258_0_imprimer_GE(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i412, i28) → f4261_0_imprimer_ConstantStackPush(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412) | <(i412, i28)
f4261_0_imprimer_ConstantStackPush(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412) → f4265_0_imprimer_Store(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, 0)
f4265_0_imprimer_Store(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, matching1) → f4268_0_imprimer_Load(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, 0) | =(matching1, 0)
f4268_0_imprimer_Load(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, matching1) → f4302_0_imprimer_Load(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, 0) | =(matching1, 0)
f4302_0_imprimer_Load(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i414) → f4341_0_imprimer_Load(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i414)
f4341_0_imprimer_Load(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i417) → f4394_0_imprimer_Load(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i417)
f4394_0_imprimer_Load(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i422) → f5062_0_imprimer_Load(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i422)
f5062_0_imprimer_Load(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i450) → f5606_0_imprimer_Load(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i450, i450)
f5606_0_imprimer_Load(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i450, i450) → f5607_0_imprimer_FieldAccess(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i450, i450, java.lang.Object(Carre(EOC, i28)))
f5607_0_imprimer_FieldAccess(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i450, i450, java.lang.Object(Carre(EOC, i28))) → f5609_0_imprimer_GE(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i450, i450, i28)
f5609_0_imprimer_GE(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i450, i450, i28) → f5611_0_imprimer_GE(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i450, i450, i28)
f5609_0_imprimer_GE(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i450, i450, i28) → f5612_0_imprimer_GE(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i450, i450, i28)
f5611_0_imprimer_GE(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i450, i450, i28) → f5613_0_imprimer_Inc(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412) | >=(i450, i28)
f5613_0_imprimer_Inc(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412) → f5616_0_imprimer_JMP(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), +(i412, 1)) | >=(i412, 0)
f5616_0_imprimer_JMP(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i474) → f5625_0_imprimer_Load(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i474)
f5625_0_imprimer_Load(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i474) → f4247_0_imprimer_Load(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i474)
f4247_0_imprimer_Load(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412) → f4250_0_imprimer_Load(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i412)
f5612_0_imprimer_GE(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i450, i450, i28) → f5615_0_imprimer_Inc(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i450) | <(i450, i28)
f5615_0_imprimer_Inc(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i450) → f5618_0_imprimer_JMP(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, +(i450, 1)) | >=(i450, 0)
f5618_0_imprimer_JMP(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i475) → f5632_0_imprimer_Load(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i475)
f5632_0_imprimer_Load(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i475) → f5062_0_imprimer_Load(EOS, java.lang.Object(Carre(EOC, i28)), java.lang.Object(Carre(EOC, i28)), i412, i475)

Combined rules. Obtained 2 IRules

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

Filtered ground terms:

f5609_0_imprimer_GE(x1, x2, x3, x4, x5, x6, x7) → f5609_0_imprimer_GE(x2, x3, x4, x5, x6, x7)
Cond_f5609_0_imprimer_GE(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f5609_0_imprimer_GE(x1, x3, x4, x5, x6, x7, x8)
Cond_f5609_0_imprimer_GE1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f5609_0_imprimer_GE1(x1, x3, x4, x5, x6, x7, x8)
Carre(x1, x2) → Carre(x2)

Filtered duplicate terms:

f5609_0_imprimer_GE(x1, x2, x3, x4, x5, x6) → f5609_0_imprimer_GE(x2, x3, x5)
Cond_f5609_0_imprimer_GE(x1, x2, x3, x4, x5, x6, x7) → Cond_f5609_0_imprimer_GE(x1, x3, x4, x6)
Cond_f5609_0_imprimer_GE1(x1, x2, x3, x4, x5, x6, x7) → Cond_f5609_0_imprimer_GE1(x1, x3, x4, x6)

Filtered unneeded terms:

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

Prepared 2 rules for path length conversion:

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

Finished conversion. Obtained 2 rules.

P rules:
f5609_0_imprimer_GE(v10, x1, x2, x0) → f5609_0_imprimer_GE(v11, +(x1, 1), 0, x0) | &&(&&(&&(&&(&&(&&(>=(x2, x0), >(x1, -1)), <(+(x1, 1), x0)), <=(+(x0, 2), v10)), >(+(v11, 1), 1)), <=(v11, v10)), >(+(v10, 1), 1))
f5609_0_imprimer_GE(v12, x4, x5, x3) → f5609_0_imprimer_GE(v13, x4, +(x5, 1), x3) | &&(&&(&&(&&(&&(>(x5, -1), <(x5, x3)), <=(+(x3, 2), v12)), >(+(v13, 1), 1)), <=(v13, v12)), >(+(v12, 1), 1))

(7) Obligation:

Rules:
f5609_0_imprimer_GE(v10, x1, x2, x0) → f5609_0_imprimer_GE(v11, +(x1, 1), 0, x0) | &&(&&(&&(&&(&&(&&(>=(x2, x0), >(x1, -1)), <(+(x1, 1), x0)), <=(+(x0, 2), v10)), >(+(v11, 1), 1)), <=(v11, v10)), >(+(v10, 1), 1))
f5609_0_imprimer_GE(v12, x4, x5, x3) → f5609_0_imprimer_GE(v13, x4, +(x5, 1), x3) | &&(&&(&&(&&(&&(>(x5, -1), <(x5, x3)), <=(+(x3, 2), v12)), >(+(v13, 1), 1)), <=(v13, v12)), >(+(v12, 1), 1))

(8) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:

[f5609_0_imprimer_GE(x)] = (-1)·x₂ + 1·x₄

where x = (x₁, ... ,x_n).

Therefore the following rule(s) have been dropped:

f5609_0_imprimer_GE(x0, x1, x2, x3) → f5609_0_imprimer_GE(x4, +(x1, 1), 0, x3) | &&(&&(&&(&&(&&(&&(>=(x2, x3), >(x1, -1)), <(+(x1, 1), x3)), <=(+(x3, 2), x0)), >(+(x4, 1), 1)), <=(x4, x0)), >(+(x0, 1), 1))

(9) Obligation:

Rules:
f5609_0_imprimer_GE(x5, x6, x7, x8) → f5609_0_imprimer_GE(x9, x6, +(x7, 1), x8) | &&(&&(&&(&&(&&(>(x7, -1), <(x7, x8)), <=(+(x8, 2), x5)), >(+(x9, 1), 1)), <=(x9, x5)), >(+(x5, 1), 1))

(10) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:

[f5609_0_imprimer_GE(x)] = (-1)·x₃ + 1·x₄

where x = (x₁, ... ,x_n).

Therefore the following rule(s) have been dropped:

f5609_0_imprimer_GE(x0, x1, x2, x3) → f5609_0_imprimer_GE(x4, x1, +(x2, 1), x3) | &&(&&(&&(&&(&&(>(x2, -1), <(x2, x3)), <=(+(x3, 2), x0)), >(+(x4, 1), 1)), <=(x4, x0)), >(+(x0, 1), 1))

(11) YES

(12) 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:

• Used field analysis yielded the following read fields:
  
  • Carre: [carre]
• Marker field analysis yielded the following relations that could be markers:
  

(13) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 32 IRules

P rules:
f2555_0_init_ConstantStackPush(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i266, i266) → f2561_0_init_GE(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i266, i266, 3)
f2561_0_init_GE(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i273, matching1) → f2563_0_init_GE(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i273, 3) | =(matching1, 3)
f2563_0_init_GE(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i273, matching1) → f2567_0_init_ConstantStackPush(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273) | &&(<(i273, 3), =(matching1, 3))
f2567_0_init_ConstantStackPush(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273) → f2571_0_init_Store(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, 0)
f2571_0_init_Store(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, matching1) → f2577_0_init_Load(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, 0) | =(matching1, 0)
f2577_0_init_Load(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, matching1) → f2684_0_init_Load(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, 0) | =(matching1, 0)
f2684_0_init_Load(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i291) → f2789_0_init_Load(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i291)
f2789_0_init_Load(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i313) → f2891_0_init_Load(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i313)
f2891_0_init_Load(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i333) → f2897_0_init_ConstantStackPush(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i333, i333)
f2897_0_init_ConstantStackPush(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i333, i333) → f2904_0_init_GE(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i333, i333, 3)
f2904_0_init_GE(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345, i345, matching1) → f2919_0_init_GE(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345, i345, 3) | =(matching1, 3)
f2904_0_init_GE(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, matching1, matching2, matching3) → f2920_0_init_GE(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, 3, 3, 3) | &&(&&(&&(=(i333, 3), =(matching1, 3)), =(matching2, 3)), =(matching3, 3))
f2919_0_init_GE(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345, i345, matching1) → f2923_0_init_Load(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345) | &&(<(i345, 3), =(matching1, 3))
f2923_0_init_Load(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345) → f2928_0_init_FieldAccess(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))))
f2928_0_init_FieldAccess(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28))))) → f2934_0_init_Load(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345, java.lang.Object(ARRAY(i28)))
f2934_0_init_Load(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345, java.lang.Object(ARRAY(i28))) → f2958_0_init_ArrayAccess(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345, java.lang.Object(ARRAY(i28)), i273)
f2958_0_init_ArrayAccess(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345, java.lang.Object(ARRAY(i28)), i273) → f3158_0_init_ArrayAccess(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345, java.lang.Object(ARRAY(i28)), i273)
f3158_0_init_ArrayAccess(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345, java.lang.Object(ARRAY(i28)), i273) → f3162_0_init_Load(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345, o2019) | <(i273, i28)
f3162_0_init_Load(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345, o2019) → f3165_0_init_ConstantStackPush(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345, o2019, i345)
f3165_0_init_ConstantStackPush(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345, o2019, i345) → f3168_0_init_ArrayAccess(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345, o2019, i345, 0)
f3168_0_init_ArrayAccess(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345, java.lang.Object(o2029put), i345, matching1) → f3173_0_init_ArrayAccess(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345, java.lang.Object(o2029put), i345, 0) | =(matching1, 0)
f3173_0_init_ArrayAccess(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345, java.lang.Object(ARRAY(i363)), i345, matching1) → f3177_0_init_ArrayAccess(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345, java.lang.Object(ARRAY(i363)), i345, 0) | &&(>=(i363, 0), =(matching1, 0))
f3177_0_init_ArrayAccess(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345, java.lang.Object(ARRAY(i363)), i345, matching1) → f3181_0_init_ArrayAccess(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345, java.lang.Object(ARRAY(i363)), i345, 0) | =(matching1, 0)
f3181_0_init_ArrayAccess(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345, java.lang.Object(ARRAY(i363)), i345, matching1) → f3199_0_init_Inc(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345) | &&(<(i345, i363), =(matching1, 0))
f3199_0_init_Inc(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i345) → f3203_0_init_JMP(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, +(i345, 1)) | >=(i345, 0)
f3203_0_init_JMP(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i367) → f3217_0_init_Load(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i367)
f3217_0_init_Load(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i367) → f2891_0_init_Load(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, i367)
f2920_0_init_GE(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273, matching1, matching2, matching3) → f2924_0_init_Inc(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273) | &&(&&(=(matching1, 3), =(matching2, 3)), =(matching3, 3))
f2924_0_init_Inc(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i273) → f2929_0_init_JMP(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), +(i273, 1)) | >=(i273, 0)
f2929_0_init_JMP(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i346) → f2951_0_init_Load(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i346)
f2951_0_init_Load(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i346) → f2552_0_init_Load(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i346)
f2552_0_init_Load(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i266) → f2555_0_init_ConstantStackPush(EOS, java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), java.lang.Object(Carre(EOC, java.lang.Object(ARRAY(i28)))), i266, i266)

Combined rules. Obtained 2 IRules

P rules:
f2904_0_init_GE(EOS, 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) → f2904_0_init_GE(EOS, 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), <(x1, x0)), <(x2, 3))
f2904_0_init_GE(EOS, 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) → f2904_0_init_GE(EOS, 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, 2), >(+(x1, 1), 0))

Filtered ground terms:

f2904_0_init_GE(x1, x2, x3, x4, x5, x6, x7, x8) → f2904_0_init_GE(x2, x3, x4, x5, x6, x7)
Cond_f2904_0_init_GE(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f2904_0_init_GE(x1, x3, x4, x5, x6, x7, x8)
Cond_f2904_0_init_GE1(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f2904_0_init_GE1(x1, x3, x4, x5, x6)
Carre(x1, x2) → Carre(x2)

Filtered duplicate terms:

f2904_0_init_GE(x1, x2, x3, x4, x5, x6) → f2904_0_init_GE(x3, x4, x6)
Cond_f2904_0_init_GE(x1, x2, x3, x4, x5, x6, x7) → Cond_f2904_0_init_GE(x1, x4, x5, x7)
Cond_f2904_0_init_GE1(x1, x2, x3, x4, x5) → Cond_f2904_0_init_GE1(x1, x4, x5)

Prepared 2 rules for path length conversion:

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

Finished conversion. Obtained 2 rules.

P rules:
f2904_0_init_GE(v9, x1, x2, x0) → f2904_0_init_GE(v10, x1, +(x2, 1), x0) | &&(&&(&&(&&(&&(>(x2, -1), <(x2, 3)), <(x1, x0)), >=(v9, v10)), >(+(v9, 1), 3)), >(+(v10, 1), 3))
f2904_0_init_GE(v11, x4, c3, x3) → f2904_0_init_GE(v12, +(x4, 1), 0, x3) | &&(&&(&&(&&(&&(>(x4, -1), <(x4, 2)), >(+(v12, 1), 3)), <=(v12, v11)), >(+(v11, 1), 3)), =(3, c3))

(14) Obligation:

Rules:
f2904_0_init_GE(v9, x1, x2, x0) → f2904_0_init_GE(v10, x1, +(x2, 1), x0) | &&(&&(&&(&&(&&(>(x2, -1), <(x2, 3)), <(x1, x0)), >=(v9, v10)), >(+(v9, 1), 3)), >(+(v10, 1), 3))
f2904_0_init_GE(v11, x4, c3, x3) → f2904_0_init_GE(v12, +(x4, 1), 0, x3) | &&(&&(&&(&&(&&(>(x4, -1), <(x4, 2)), >(+(v12, 1), 3)), <=(v12, v11)), >(+(v11, 1), 3)), =(3, c3))

(15) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:

[f2904_0_init_GE(x11, x13, x15, x17)] = 1 - x13

Therefore the following rule(s) have been dropped:

f2904_0_init_GE(x5, x6, x7, x8) → f2904_0_init_GE(x9, +(x6, 1), 0, x8) | &&(&&(&&(&&(&&(>(x6, -1), <(x6, 2)), >(+(x9, 1), 3)), <=(x9, x5)), >(+(x5, 1), 3)), =(3, x7))

(16) Obligation:

Rules:
f2904_0_init_GE(x0, x1, x2, x3) → f2904_0_init_GE(x4, x1, +(x2, 1), x3) | &&(&&(&&(&&(&&(>(x2, -1), <(x2, 3)), <(x1, x3)), >=(x0, x4)), >(+(x0, 1), 3)), >(+(x4, 1), 3))

(17) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f2904_0_init_GE(x6, x8, x10, x12)] = 2 - x10

Therefore the following rule(s) have been dropped:

f2904_0_init_GE(x0, x1, x2, x3) → f2904_0_init_GE(x4, x1, +(x2, 1), x3) | &&(&&(&&(&&(&&(>(x2, -1), <(x2, 3)), <(x1, x3)), >=(x0, x4)), >(+(x0, 1), 3)), >(+(x4, 1), 3))

(18) YES