Termination proof of /tmp/tmpSJv

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 4008 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIntTRSProof (⇒, 187 ms)

        ↳7 intTRS

        ↳8 PolynomialOrderProcessor (⇔, 4 ms)

        ↳9 YES

    ↳10 JBCTerminationSCC

        ↳11 SCCToIntTRSProof (⇒, 227 ms)

        ↳12 intTRS

        ↳13 PolynomialOrderProcessor (⇔, 0 ms)

        ↳14 YES

    ↳15 JBCTerminationSCC

        ↳16 SCCToIntTRSProof (⇒, 372 ms)

        ↳17 intTRS

        ↳18 PolynomialOrderProcessor (⇔, 9 ms)

        ↳19 YES

    ↳20 JBCTerminationSCC

        ↳21 SCCToIntTRSProof (⇒, 389 ms)

        ↳22 intTRS

        ↳23 PolynomialOrderProcessor (⇔, 0 ms)

        ↳24 YES

    ↳25 JBCTerminationSCC

        ↳26 SCCToIntTRSProof (⇒, 14 ms)

        ↳27 intTRS

        ↳28 PolynomialOrderProcessor (⇔, 4 ms)

        ↳29 YES

    ↳30 JBCTerminationSCC

        ↳31 SCCToIntTRSProof (⇒, 24 ms)

        ↳32 intTRS

        ↳33 LinearRankingProcessor (⇔, 15 ms)

        ↳34 YES

    ↳35 JBCTerminationSCC

        ↳36 SCCToIntTRSProof (⇒, 527 ms)

        ↳37 intTRS

        ↳38 PolynomialOrderProcessor (⇔, 0 ms)

        ↳39 YES

    ↳40 JBCTerminationSCC

        ↳41 SCCToIntTRSProof (⇒, 381 ms)

        ↳42 intTRS

        ↳43 PolynomialOrderProcessor (⇔, 0 ms)

        ↳44 YES

    ↳45 JBCTerminationSCC

        ↳46 SCCToIntTRSProof (⇒, 364 ms)

        ↳47 intTRS

        ↳48 PolynomialOrderProcessor (⇒, 0 ms)

        ↳49 intTRS

        ↳50 PolynomialOrderProcessor (⇔, 0 ms)

        ↳51 YES

    ↳52 JBCTerminationSCC

        ↳53 SCCToIntTRSProof (⇒, 1453 ms)

        ↳54 intTRS

        ↳55 PolynomialOrderProcessor (⇔, 0 ms)

        ↳56 YES

(0) Obligation:

JBC Problem based on JBC Program:

class Domino {
    int gauche, droite;

    Domino(int g, int d) {
	gauche = g;
	droite = d;
    }

    /*
    public String toString() {
	return gauche + "-" + droite;
    }
    */

    public boolean equals(Object o) {
	if(this==o) return true;
	if(o instanceof Domino) {
	    Domino d = (Domino) o;
	    return (gauche==d.gauche && droite==d.droite) 
		|| (gauche==d.droite && droite==d.gauche);
	}
	return false;
    }

    void retourne() {
	int d = droite;
	droite = gauche;
	gauche = d;
    }
}

/* Question 2.1 */
class Liste {
    Domino dom;
    Liste suite;

    Liste(Domino d, Liste s) {
	dom = d;
	suite = s;
    }
}

/* Question 4.1 */
class Sequence {
    private Liste gauche;

    Sequence(Domino d) {
	gauche = new Liste(d, null);
    }

    void imprimer() {
	//System.out.println("Sur la table :");
	Partie.lister(gauche);
	//System.out.println("\n------");
    }

    /* Question 4.2 */
    int valeurGauche(){
	return gauche.dom.gauche;
    }

    void ajouterAGauche(Domino d) {
	gauche = new Liste(d, gauche);
    }

    /* Question 4.3 */
    int valeurDroite(){
	Liste l = gauche;
	for(; l.suite!=null; l = l.suite);
	return l.dom.droite;
    }

    void ajouterADroite(Domino d) {
	if(gauche==null) {
	    gauche = new Liste(d, null);
	    return;
	}
	Liste l = gauche;
	for(; l.suite!=null; l = l.suite);
	l.suite = new Liste(d,null);
    }
}

class Partie {
    final static int TAILLEDOMINO = 6;//Le plus grand nombre sur un domino
    final static int[] TAILLEMAIN = {0,0,7,6,6};//La taille des mains en fonction
    //du nombre de joueurs.
    private Liste pioche;
    private Liste[] mains;

    public Partie(int nombreDeJoueurs) {
	mains = new Liste[nombreDeJoueurs];
	creerPioche();
	for(int i=0; i<nombreDeJoueurs; i++) {
	    creerMain(i, TAILLEMAIN[nombreDeJoueurs]);
	    imprimeMain(i);
	}
	int joueur = plusForteMain();
	//System.out.println("Le joueur "+joueur+" commence.");
	Sequence jeu = premierCoup(joueur);
	joueur = (joueur + 1) % nombreDeJoueurs;
	int bloques = 0;
	//while(bloques<nombreDeJoueurs){
	for(int i=28; i>=0; i--){
	    jeu.imprimer();
	    imprimeMain(joueur);
	    if (jouer(joueur, jeu)) bloques = 0; 
	    else bloques++;
	    if (mains[joueur]==null) {
		//System.out.println("Le joueur " + joueur + " a gagne.");
		return;
	    }
	    joueur = (joueur + 1) % nombreDeJoueurs;
	}
	imprimeGagnants();
    }

    /* Question 2.2 */
    static int longueur(Liste l) {
	if(l==null) return 0;
	return 1 + longueur(l.suite);
    }

    /* Question 2.3 */
    static void lister(Liste l) {
	if(l==null) return;
	//System.out.print(l.dom + " ");
	lister(l.suite);
    }

    /* Question 3.1 */
    void creerPioche(){
	pioche = null;
	for(int i = 0; i<TAILLEDOMINO+1; i++) {
	    for(int j = i; j<7; j++)
		pioche = new Liste(new Domino(i,j), pioche);
	}
    }

    /* Question 3.2 */
    static Domino nieme(Liste l, int n) {
	if(n<=0) return l.dom;
	return nieme(l.suite, n-1);
    }

    /* Question 3.3 */
    static Liste supprimer(Liste l, Domino d) {
	if(l==null) return null;
	if(l.dom.equals(d)) return l.suite;
	return new Liste(l.dom, supprimer(l.suite, d));
    }

    private int lastRandom = 0;

    int entierAuHasard(int max) {
	return lastRandom = (lastRandom + 100) % max;
    }

    /* Question 3.4 */
    Domino piocher(){
	int l = longueur(pioche);
	Domino d = nieme(pioche, entierAuHasard(l));
	pioche = supprimer(pioche, d);
	return d;
    }

    /* Question 3.5 */
    void creerMain(int joueur, int nombre) {
	mains[joueur] = null;
	for(int i=0; i<nombre; i++) {
	    mains[joueur] = new Liste(piocher(), mains[joueur]);
	}
    }

    /* Question 3.6 */
    int valeurDomino(Domino d){
	if(d.gauche > d.droite) return d.gauche * 10 + d.droite;
	return d.droite * 10 + d.gauche;
    }

    int valeurMain(int joueur) {
	int res = 0;
	for(Liste l = mains[joueur]; l != null; l = l.suite) {
	    int v = valeurDomino(l.dom);
	    res = (v>res)?v:res;
	}
	return res;
    }

    int plusForteMain() {
	int res = valeurMain(0);
	int j = 0;
	for(int i = 0; i<mains.length; i++){
	    int v = valeurMain(i);
	    if(v>res) {
		res = v;
		j = i;
	    }
	}
	return j;
    }

    Sequence premierCoup(int joueur) {
	Domino aJouer = nieme(mains[joueur], 
			      entierAuHasard(longueur(mains[joueur])));
	mains[joueur] = supprimer(mains[joueur], aJouer);
	return new Sequence(aJouer);
    }

    boolean jouer(int joueur, Sequence jeu) {
	Liste l = null;
	/* Pour la question 5.3, on avantage le joueur 1 */
	if(joueur==1)
	    mains[1]=mettreMeilleurDevant(mains[1], jeu);
	Domino aJouer=null;
	int g = jeu.valeurGauche();
	int d = jeu.valeurDroite(); 
	int longueur = longueur(mains[joueur]);
	for(l = mains[joueur]; l != null; l = l.suite) {
	    if(l.dom.gauche == g)
		l.dom.retourne(); //l.dom = retourne(l.dom);
	    else if(l.dom.droite == d)
		l.dom.retourne(); //l.dom = retourne(l.dom);
	    if(l.dom.droite == g) {
		jeu.ajouterAGauche(l.dom);
		aJouer = l.dom;
		break;
	    } else if (l.dom.gauche == d) {
		jeu.ajouterADroite(l.dom);
		aJouer = l.dom;
		break;
	    }
	}
	if(aJouer != null) {
	    //System.out.println("Le joueur " + joueur + " joue le domino " + aJouer);
	    mains[joueur] = supprimer(mains[joueur], aJouer);
	    return true;
	}
	if(pioche == null) {
	    //System.out.println("Le joueur "+ joueur +" boude.");
	    return false;
	}
	//System.out.print("Le joueur "+ joueur +" pioche");
	mains[joueur] = new Liste(piocher(), mains[joueur]);
	//System.out.println(" le domino " + mains[joueur].dom);
	return true;
    }

    /* Question 5.2 */
    void imprimeMain(int joueur) {
	//System.out.println("Main du joueur "+joueur+" :");
	lister(mains[joueur]);
	//System.out.println("\n");
    }

    void imprimeGagnants(){
	int dominos = longueur(mains[0]);
	int[] gagnants = {0};
	for(int i=1; i<mains.length; i++) {
	    int l = longueur(mains[i]);
	    if(l<dominos) {
		dominos = l;
		gagnants = new int[1];
		gagnants[0] = i;
	    }
	    else if(l==dominos) {
		int[] g = new int[gagnants.length + 1];
		for(int j=0; j<gagnants.length; j++) g[j] = gagnants[j];
		gagnants = g;
		gagnants[g.length-1] = i;
	    }
	}
	if(gagnants.length == 1) {
	    //System.out.println("\nLe joueur " + gagnants[0] + " a gagne.");
	    return;
	}
	if(gagnants.length == mains.length) {
	    //System.out.println("\nMatch nul.");
	    for(int i=0; i<gagnants.length; i++)
		//System.out.println("Le joueur " + i + " a " +  sommeValeursMain(i) + " points.");
		return;
	}
    }

    /* Question 5.3 */
    int sommeValeursMain(int joueur) {
	int res = 0;
	for(Liste l = mains[joueur]; l!=null; l = l.suite) 
	    res += valeurDomino(l.dom);
	return res;
    }

    static boolean jouable(Domino d, Sequence jeu) {
	int x = jeu.valeurGauche();
	int y = jeu.valeurDroite();
	return d.gauche==x || d.droite==x || d.gauche==y || d.droite==y;
    }

    Liste mettreMeilleurDevant(Liste l, Sequence jeu) {
	if(l==null || l.suite==null) return l;
	Liste ll = mettreMeilleurDevant(l.suite,jeu);
	boolean jouableTrouve = jouable(ll.dom, jeu);
	if(jouable(l.dom, jeu) && (
	   (jouableTrouve && valeurDomino(l.dom) > valeurDomino(ll.dom) )
	   || !jouableTrouve )) {
	    l.suite = ll;
	    return l;
	}
	l.suite = ll.suite;
	ll.suite = l;
	return ll;
    }

    public static void main(String[] args) {
	Partie p = new Partie(args.length);
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Partie.main([Ljava/lang/String;)V: Graph of 721 nodes with 1 SCC.

Partie.creerPioche()V: Graph of 60 nodes with 1 SCC.

Partie.plusForteMain()I: Graph of 163 nodes with 2 SCCs.

Partie.creerMain(II)V: Graph of 136 nodes with 0 SCCs.

Partie.lister(LListe;)V: Graph of 20 nodes with 0 SCCs.

Partie.longueur(LListe;)I: Graph of 27 nodes with 0 SCCs.

Partie.valeurMain(I)I: Graph of 111 nodes with 1 SCC.

Partie.nieme(LListe;I)LDomino;: Graph of 132 nodes with 0 SCCs.

Partie.supprimer(LListe;LDomino;)LListe;: Graph of 65 nodes with 0 SCCs.

Domino.equals(Ljava/lang/Object;)Z: Graph of 9 nodes with 0 SCCs.

Partie.jouer(ILSequence;)Z: Graph of 139 nodes with 0 SCCs.

Partie.mettreMeilleurDevant(LListe;LSequence;)LListe;: Graph of 58 nodes with 0 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 10 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Partie.mettreMeilleurDevant(LListe;LSequence;)LListe;
SCC calls the following helper methods: Partie.mettreMeilleurDevant(LListe;LSequence;)LListe;
Performed SCC analyses:

Used field analysis yielded the following read fields:
- Liste: [suite]
Marker field analysis yielded the following relations that could be markers:

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 16 IRules

P rules:
f11615_0_mettreMeilleurDevant_NULL(EOS, java.lang.Object(o7567sub), java.lang.Object(Sequence(EOC)), java.lang.Object(o7567sub), java.lang.Object(Sequence(EOC)), java.lang.Object(o7567sub)) → f11619_0_mettreMeilleurDevant_NULL(EOS, java.lang.Object(o7567sub), java.lang.Object(Sequence(EOC)), java.lang.Object(o7567sub), java.lang.Object(Sequence(EOC)), java.lang.Object(o7567sub))
f11619_0_mettreMeilleurDevant_NULL(EOS, java.lang.Object(o7567sub), java.lang.Object(Sequence(EOC)), java.lang.Object(o7567sub), java.lang.Object(Sequence(EOC)), java.lang.Object(o7567sub)) → f11623_0_mettreMeilleurDevant_Load(EOS, java.lang.Object(o7567sub), java.lang.Object(Sequence(EOC)), java.lang.Object(o7567sub), java.lang.Object(Sequence(EOC)))
f11623_0_mettreMeilleurDevant_Load(EOS, java.lang.Object(o7567sub), java.lang.Object(Sequence(EOC)), java.lang.Object(o7567sub), java.lang.Object(Sequence(EOC))) → f11633_0_mettreMeilleurDevant_FieldAccess(EOS, java.lang.Object(o7567sub), java.lang.Object(Sequence(EOC)), java.lang.Object(o7567sub), java.lang.Object(Sequence(EOC)), java.lang.Object(o7567sub))
f11633_0_mettreMeilleurDevant_FieldAccess(EOS, java.lang.Object(Liste(o7575sub, o7577)), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(o7575sub, o7577)), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(o7575sub, o7577))) → f11638_0_mettreMeilleurDevant_FieldAccess(EOS, java.lang.Object(Liste(o7575sub, o7577)), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(o7575sub, o7577)), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(o7575sub, o7577)))
f11638_0_mettreMeilleurDevant_FieldAccess(EOS, java.lang.Object(Liste(o7575sub, o7577)), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(o7575sub, o7577)), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(o7575sub, o7577))) → f11645_0_mettreMeilleurDevant_NONNULL(EOS, java.lang.Object(Liste(o7575sub, o7577)), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(o7575sub, o7577)), java.lang.Object(Sequence(EOC)), o7577)
f11645_0_mettreMeilleurDevant_NONNULL(EOS, java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(o7596sub)) → f11665_0_mettreMeilleurDevant_NONNULL(EOS, java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(o7596sub))
f11665_0_mettreMeilleurDevant_NONNULL(EOS, java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(o7596sub)) → f11670_0_mettreMeilleurDevant_Load(EOS, java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)))
f11670_0_mettreMeilleurDevant_Load(EOS, java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC))) → f11680_0_mettreMeilleurDevant_Load(EOS, java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)))
f11680_0_mettreMeilleurDevant_Load(EOS, java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC))) → f11687_0_mettreMeilleurDevant_FieldAccess(EOS, java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))))
f11687_0_mettreMeilleurDevant_FieldAccess(EOS, java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub)))) → f11694_0_mettreMeilleurDevant_Load(EOS, java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(o7596sub))
f11694_0_mettreMeilleurDevant_Load(EOS, java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(o7596sub)) → f11725_0_mettreMeilleurDevant_InvokeMethod(EOS, java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(o7596sub), java.lang.Object(Sequence(EOC)))
f11725_0_mettreMeilleurDevant_InvokeMethod(EOS, java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(o7596sub), java.lang.Object(Sequence(EOC))) → f11727_0_mettreMeilleurDevant_Load(EOS, java.lang.Object(o7596sub), java.lang.Object(Sequence(EOC)), java.lang.Object(o7596sub), java.lang.Object(Sequence(EOC)))
f11725_0_mettreMeilleurDevant_InvokeMethod(EOS, java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(o7596sub), java.lang.Object(Sequence(EOC))) → f11727_1_mettreMeilleurDevant_Load(EOS, java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(o7575sub, java.lang.Object(o7596sub))), java.lang.Object(Sequence(EOC)), java.lang.Object(o7596sub), java.lang.Object(Sequence(EOC)), java.lang.Object(o7596sub), java.lang.Object(Sequence(EOC)))
f11727_0_mettreMeilleurDevant_Load(EOS, java.lang.Object(o7596sub), java.lang.Object(Sequence(EOC)), java.lang.Object(o7596sub), java.lang.Object(Sequence(EOC))) → f11737_0_mettreMeilleurDevant_Load(EOS, java.lang.Object(o7596sub), java.lang.Object(Sequence(EOC)), java.lang.Object(o7596sub), java.lang.Object(Sequence(EOC)))
f11737_0_mettreMeilleurDevant_Load(EOS, java.lang.Object(o7596sub), java.lang.Object(Sequence(EOC)), java.lang.Object(o7596sub), java.lang.Object(Sequence(EOC))) → f11612_0_mettreMeilleurDevant_Load(EOS, java.lang.Object(o7596sub), java.lang.Object(Sequence(EOC)), java.lang.Object(o7596sub), java.lang.Object(Sequence(EOC)))
f11612_0_mettreMeilleurDevant_Load(EOS, o7553, java.lang.Object(Sequence(EOC)), o7553, java.lang.Object(Sequence(EOC))) → f11615_0_mettreMeilleurDevant_NULL(EOS, o7553, java.lang.Object(Sequence(EOC)), o7553, java.lang.Object(Sequence(EOC)), o7553)

Combined rules. Obtained 2 IRules

P rules:
f11615_0_mettreMeilleurDevant_NULL(EOS, java.lang.Object(Liste(x0, java.lang.Object(x1))), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(x0, java.lang.Object(x1))), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(x0, java.lang.Object(x1)))) → f11727_1_mettreMeilleurDevant_Load(EOS, java.lang.Object(Liste(x0, java.lang.Object(x1))), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(x0, java.lang.Object(x1))), java.lang.Object(Sequence(EOC)), java.lang.Object(x1), java.lang.Object(Sequence(EOC)), java.lang.Object(x1), java.lang.Object(Sequence(EOC)))
f11615_0_mettreMeilleurDevant_NULL(EOS, java.lang.Object(Liste(x0, java.lang.Object(x1))), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(x0, java.lang.Object(x1))), java.lang.Object(Sequence(EOC)), java.lang.Object(Liste(x0, java.lang.Object(x1)))) → f11615_0_mettreMeilleurDevant_NULL(EOS, java.lang.Object(x1), java.lang.Object(Sequence(EOC)), java.lang.Object(x1), java.lang.Object(Sequence(EOC)), java.lang.Object(x1))

Filtered ground terms:

f11615_0_mettreMeilleurDevant_NULL(x1, x2, x3, x4, x5, x6) → f11615_0_mettreMeilleurDevant_NULL(x2, x4, x6)
f11727_1_mettreMeilleurDevant_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → f11727_1_mettreMeilleurDevant_Load(x2, x4, x6, x8)
Sequence(x1) → Sequence

Filtered duplicate terms:

f11615_0_mettreMeilleurDevant_NULL(x1, x2, x3) → f11615_0_mettreMeilleurDevant_NULL(x3)
f11727_1_mettreMeilleurDevant_Load(x1, x2, x3, x4) → f11727_1_mettreMeilleurDevant_Load(x2)

Filtered unneeded terms:

Liste(x1, x2) → Liste(x2)

Prepared 2 rules for path length conversion:

P rules:
f11615_0_mettreMeilleurDevant_NULL(java.lang.Object(Liste(java.lang.Object(x1)))) → f11727_1_mettreMeilleurDevant_Load(java.lang.Object(Liste(java.lang.Object(x1))))
f11615_0_mettreMeilleurDevant_NULL(java.lang.Object(Liste(java.lang.Object(x1)))) → f11615_0_mettreMeilleurDevant_NULL(java.lang.Object(x1))

Finished conversion. Obtained 1 rules.

P rules:
f11615_0_mettreMeilleurDevant_NULL(v3) → f11615_0_mettreMeilleurDevant_NULL(v4) | &&(&&(>(+(v4, 1), 1), <=(+(v4, 2), v3)), >(+(v3, 1), 3))

(7) Obligation:

Rules:
f11615_0_mettreMeilleurDevant_NULL(v3) → f11615_0_mettreMeilleurDevant_NULL(v4) | &&(&&(>(+(v4, 1), 1), <=(+(v4, 2), v3)), >(+(v3, 1), 3))

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f11615_0_mettreMeilleurDevant_NULL(x3)] = x3

Therefore the following rule(s) have been dropped:

f11615_0_mettreMeilleurDevant_NULL(x0) → f11615_0_mettreMeilleurDevant_NULL(x1) | &&(&&(>(+(x1, 1), 1), <=(+(x1, 2), x0)), >(+(x0, 1), 3))

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Partie.supprimer(LListe;LDomino;)LListe;
SCC calls the following helper methods: Domino.equals(Ljava/lang/Object;)Z, Partie.supprimer(LListe;LDomino;)LListe;
Performed SCC analyses:

Used field analysis yielded the following read fields:
- Liste: [dom, suite]
Marker field analysis yielded the following relations that could be markers:

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 25 IRules

P rules:
f5007_0_supprimer_NONNULL(EOS, java.lang.Object(o2185sub), NULL, java.lang.Object(o2185sub), NULL, java.lang.Object(o2185sub)) → f5016_0_supprimer_NONNULL(EOS, java.lang.Object(o2185sub), NULL, java.lang.Object(o2185sub), NULL, java.lang.Object(o2185sub))
f5016_0_supprimer_NONNULL(EOS, java.lang.Object(o2185sub), NULL, java.lang.Object(o2185sub), NULL, java.lang.Object(o2185sub)) → f5030_0_supprimer_Load(EOS, java.lang.Object(o2185sub), NULL, java.lang.Object(o2185sub), NULL)
f5030_0_supprimer_Load(EOS, java.lang.Object(o2185sub), NULL, java.lang.Object(o2185sub), NULL) → f5049_0_supprimer_FieldAccess(EOS, java.lang.Object(o2185sub), NULL, java.lang.Object(o2185sub), NULL, java.lang.Object(o2185sub))
f5049_0_supprimer_FieldAccess(EOS, java.lang.Object(Liste(o2202sub, o2203, o2204)), NULL, java.lang.Object(Liste(o2202sub, o2203, o2204)), NULL, java.lang.Object(Liste(o2202sub, o2203, o2204))) → f5064_0_supprimer_FieldAccess(EOS, java.lang.Object(Liste(o2202sub, o2203, o2204)), NULL, java.lang.Object(Liste(o2202sub, o2203, o2204)), NULL, java.lang.Object(Liste(o2202sub, o2203, o2204)))
f5064_0_supprimer_FieldAccess(EOS, java.lang.Object(Liste(o2202sub, o2203, o2204)), NULL, java.lang.Object(Liste(o2202sub, o2203, o2204)), NULL, java.lang.Object(Liste(o2202sub, o2203, o2204))) → f5081_0_supprimer_Load(EOS, java.lang.Object(Liste(o2202sub, o2203, o2204)), NULL, java.lang.Object(Liste(o2202sub, o2203, o2204)), NULL, o2203)
f5081_0_supprimer_Load(EOS, java.lang.Object(Liste(o2202sub, o2203, o2204)), NULL, java.lang.Object(Liste(o2202sub, o2203, o2204)), NULL, o2203) → f5140_0_supprimer_InvokeMethod(EOS, java.lang.Object(Liste(o2202sub, o2203, o2204)), NULL, java.lang.Object(Liste(o2202sub, o2203, o2204)), NULL, o2203, NULL)
f5140_0_supprimer_InvokeMethod(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2260sub), o2204)), NULL, java.lang.Object(Liste(o2202sub, java.lang.Object(o2260sub), o2204)), NULL, java.lang.Object(o2260sub), NULL) → f5165_0_supprimer_InvokeMethod(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2260sub), o2204)), NULL, java.lang.Object(Liste(o2202sub, java.lang.Object(o2260sub), o2204)), NULL, java.lang.Object(o2260sub), NULL)
f5165_0_supprimer_InvokeMethod(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2260sub), o2204)), NULL, java.lang.Object(Liste(o2202sub, java.lang.Object(o2260sub), o2204)), NULL, java.lang.Object(o2260sub), NULL) → f5206_0_equals_Load(EOS, java.lang.Object(o2260sub), NULL, java.lang.Object(o2260sub), NULL)
f5165_0_supprimer_InvokeMethod(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2260sub), o2204)), NULL, java.lang.Object(Liste(o2202sub, java.lang.Object(o2260sub), o2204)), NULL, java.lang.Object(o2260sub), NULL) → f5206_1_equals_Load(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2260sub), o2204)), NULL, java.lang.Object(Liste(o2202sub, java.lang.Object(o2260sub), o2204)), NULL, java.lang.Object(o2260sub), NULL, java.lang.Object(o2260sub), NULL)
f5206_0_equals_Load(EOS, java.lang.Object(o2260sub), NULL, java.lang.Object(o2260sub), NULL) → f5261_0_equals_Load(EOS, java.lang.Object(o2260sub), NULL, java.lang.Object(o2260sub), NULL)
f5501_0_equals_Return(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(o2482sub), NULL, matching1) → f5551_0_supprimer_EQ(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, 0) | =(matching1, 0)
f5551_0_supprimer_EQ(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, matching1) → f5609_0_supprimer_New(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL) | =(matching1, 0)
f5609_0_supprimer_New(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL) → f5660_0_supprimer_Duplicate(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL)
f5660_0_supprimer_Duplicate(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL) → f5688_0_supprimer_Load(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL)
f5688_0_supprimer_Load(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL) → f5719_0_supprimer_FieldAccess(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)))
f5719_0_supprimer_FieldAccess(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204))) → f5740_0_supprimer_Load(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(o2482sub))
f5740_0_supprimer_Load(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(o2482sub)) → f5838_0_supprimer_FieldAccess(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, NULL, java.lang.Object(o2482sub), java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)))
f5838_0_supprimer_FieldAccess(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, NULL, java.lang.Object(o2482sub), java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204))) → f5860_0_supprimer_Load(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, NULL, java.lang.Object(o2482sub), o2204)
f5860_0_supprimer_Load(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, NULL, java.lang.Object(o2482sub), o2204) → f5877_0_supprimer_InvokeMethod(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(o2482sub), o2204, NULL)
f5877_0_supprimer_InvokeMethod(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(o2482sub), o2204, NULL) → f5888_0_supprimer_Load(EOS, o2204, NULL, o2204, NULL)
f5877_0_supprimer_InvokeMethod(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(o2482sub), o2204, NULL) → f5888_1_supprimer_Load(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(o2482sub), o2204, NULL, o2204, NULL)
f5888_0_supprimer_Load(EOS, o2204, NULL, o2204, NULL) → f5906_0_supprimer_Load(EOS, o2204, NULL, o2204, NULL)
f5906_0_supprimer_Load(EOS, o2204, NULL, o2204, NULL) → f4998_0_supprimer_Load(EOS, o2204, NULL, o2204, NULL)
f4998_0_supprimer_Load(EOS, o2031, NULL, o2031, NULL) → f5007_0_supprimer_NONNULL(EOS, o2031, NULL, o2031, NULL, o2031)
f5206_1_equals_Load(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(o2482sub), NULL, java.lang.Object(o2482sub), NULL) → f5501_0_equals_Return(EOS, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(Liste(o2202sub, java.lang.Object(o2482sub), o2204)), NULL, java.lang.Object(o2482sub), NULL, 0)

Combined rules. Obtained 3 IRules

P rules:
f5501_0_equals_Return(EOS, java.lang.Object(Liste(x0, java.lang.Object(x1), x2)), NULL, java.lang.Object(Liste(x0, java.lang.Object(x1), x2)), NULL, java.lang.Object(x1), NULL, 0) → f5888_1_supprimer_Load(EOS, java.lang.Object(Liste(x0, java.lang.Object(x1), x2)), NULL, java.lang.Object(x1), x2, NULL, x2, NULL)
f5501_0_equals_Return(EOS, java.lang.Object(Liste(x0, java.lang.Object(x1), java.lang.Object(Liste(x2, java.lang.Object(x3), x4)))), NULL, java.lang.Object(Liste(x0, java.lang.Object(x1), java.lang.Object(Liste(x2, java.lang.Object(x3), x4)))), NULL, java.lang.Object(x1), NULL, 0) → f5261_0_equals_Load(EOS, java.lang.Object(x3), NULL, java.lang.Object(x3), NULL)
f5501_0_equals_Return(EOS, java.lang.Object(Liste(x0, java.lang.Object(x1), java.lang.Object(Liste(x2, java.lang.Object(x3), x4)))), NULL, java.lang.Object(Liste(x0, java.lang.Object(x1), java.lang.Object(Liste(x2, java.lang.Object(x3), x4)))), NULL, java.lang.Object(x1), NULL, 0) → f5501_0_equals_Return(EOS, java.lang.Object(Liste(x2, java.lang.Object(x3), x4)), NULL, java.lang.Object(Liste(x2, java.lang.Object(x3), x4)), NULL, java.lang.Object(x3), NULL, 0)

Filtered ground terms:

f5501_0_equals_Return(x1, x2, x3, x4, x5, x6, x7, x8) → f5501_0_equals_Return(x2, x4, x6)
f5888_1_supprimer_Load(x1, x2, x3, x4, x5, x6, x7, x8) → f5888_1_supprimer_Load(x2, x4, x5, x7)
f5261_0_equals_Load(x1, x2, x3, x4, x5) → f5261_0_equals_Load(x2, x4)

Filtered duplicate terms:

f5501_0_equals_Return(x1, x2, x3) → f5501_0_equals_Return(x2)
f5888_1_supprimer_Load(x1, x2, x3, x4) → f5888_1_supprimer_Load(x1)
f5261_0_equals_Load(x1, x2) → f5261_0_equals_Load(x2)

Filtered unneeded terms:

Liste(x1, x2, x3) → Liste(x3)

Prepared 3 rules for path length conversion:

P rules:
f5501_0_equals_Return(java.lang.Object(Liste(x2))) → f5888_1_supprimer_Load(java.lang.Object(Liste(x2)))
f5501_0_equals_Return(java.lang.Object(Liste(java.lang.Object(Liste(x4))))) → f5261_0_equals_Load(java.lang.Object(x3))
f5501_0_equals_Return(java.lang.Object(Liste(java.lang.Object(Liste(x4))))) → f5501_0_equals_Return(java.lang.Object(Liste(x4)))

Finished conversion. Obtained 1 rules.

P rules:
f5501_0_equals_Return(v5) → f5501_0_equals_Return(v6) | &&(&&(>(+(v6, 1), 1), <=(+(v6, 2), v5)), >(+(v5, 1), 3))

(12) Obligation:

Rules:
f5501_0_equals_Return(v5) → f5501_0_equals_Return(v6) | &&(&&(>(+(v6, 1), 1), <=(+(v6, 2), v5)), >(+(v5, 1), 3))

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f5501_0_equals_Return(x3)] = x3

Therefore the following rule(s) have been dropped:

f5501_0_equals_Return(x0) → f5501_0_equals_Return(x1) | &&(&&(>(+(x1, 1), 1), <=(+(x1, 2), x0)), >(+(x0, 1), 3))

(14) YES

(15) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Partie.nieme(LListe;I)LDomino;
SCC calls the following helper methods: Partie.nieme(LListe;I)LDomino;
Performed SCC analyses:

Used field analysis yielded the following read fields:
- Liste: [suite]
Marker field analysis yielded the following relations that could be markers:

(16) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 29 IRules

P rules:
f4308_0_nieme_GT(EOS, o1725, i452, o1726, o1725, i452, i452) → f4315_0_nieme_GT(EOS, o1725, i452, o1726, o1725, i452, i452)
f4315_0_nieme_GT(EOS, o1725, i452, o1726, o1725, i452, i452) → f4344_0_nieme_Load(EOS, o1725, i452, o1726, o1725, i452) | >(i452, 0)
f4344_0_nieme_Load(EOS, o1725, i452, o1726, o1725, i452) → f4356_0_nieme_FieldAccess(EOS, o1725, i452, o1726, i452, o1725)
f4356_0_nieme_FieldAccess(EOS, java.lang.Object(o1799sub), i452, o1726, i452, java.lang.Object(o1799sub)) → f4394_0_nieme_FieldAccess(EOS, java.lang.Object(o1799sub), i452, o1726, i452, java.lang.Object(o1799sub))
f4394_0_nieme_FieldAccess(EOS, java.lang.Object(o1799sub), i452, o1726, i452, java.lang.Object(o1799sub)) → f4430_0_nieme_FieldAccess(EOS, java.lang.Object(o1799sub), i452, o1726, i452, java.lang.Object(o1799sub))
f4394_0_nieme_FieldAccess(EOS, java.lang.Object(o1809sub), i452, java.lang.Object(o1809sub), i452, java.lang.Object(o1809sub)) → f4431_0_nieme_FieldAccess(EOS, java.lang.Object(o1809sub), i452, java.lang.Object(o1809sub), i452, java.lang.Object(o1809sub))
f4430_0_nieme_FieldAccess(EOS, java.lang.Object(Liste(EOC, o1820)), i452, o1726, i452, java.lang.Object(Liste(EOC, o1820))) → f4450_0_nieme_FieldAccess(EOS, java.lang.Object(Liste(EOC, o1820)), i452, o1726, i452, java.lang.Object(Liste(EOC, o1820)))
f4450_0_nieme_FieldAccess(EOS, java.lang.Object(Liste(EOC, o1820)), i452, o1726, i452, java.lang.Object(Liste(EOC, o1820))) → f4509_0_nieme_Load(EOS, java.lang.Object(Liste(EOC, o1820)), i452, o1726, i452, o1820)
f4509_0_nieme_Load(EOS, java.lang.Object(Liste(EOC, o1820)), i452, o1726, i452, o1820) → f4550_0_nieme_ConstantStackPush(EOS, java.lang.Object(Liste(EOC, o1820)), i452, o1726, o1820, i452)
f4550_0_nieme_ConstantStackPush(EOS, java.lang.Object(Liste(EOC, o1820)), i452, o1726, o1820, i452) → f4654_0_nieme_IntArithmetic(EOS, java.lang.Object(Liste(EOC, o1820)), i452, o1726, o1820, i452, 1)
f4654_0_nieme_IntArithmetic(EOS, java.lang.Object(Liste(EOC, o1820)), i452, o1726, o1820, i452, matching1) → f4723_0_nieme_InvokeMethod(EOS, java.lang.Object(Liste(EOC, o1820)), i452, o1726, o1820, -(i452, 1)) | &&(>(i452, 0), =(matching1, 1))
f4723_0_nieme_InvokeMethod(EOS, java.lang.Object(Liste(EOC, o1820)), i452, o1726, o1820, i496) → f4731_0_nieme_Load(EOS, o1820, i496, o1726, java.lang.Object(Liste(EOC, o1820)), o1820, i496)
f4723_0_nieme_InvokeMethod(EOS, java.lang.Object(Liste(EOC, o1820)), i452, o1726, o1820, i496) → f4731_1_nieme_Load(EOS, java.lang.Object(Liste(EOC, o1820)), i452, o1726, o1820, i496, o1820, i496)
f4731_0_nieme_Load(EOS, o1820, i496, o1726, java.lang.Object(Liste(EOC, o1820)), o1820, i496) → f4760_0_nieme_Load(EOS, o1820, i496, o1726, java.lang.Object(Liste(EOC, o1820)), o1820, i496)
f4760_0_nieme_Load(EOS, o1820, i496, o1726, java.lang.Object(Liste(EOC, o1820)), o1820, i496) → f4790_0_nieme_Load(EOS, o1820, i496, o1726, java.lang.Object(Liste(EOC, o1820)), o1820, i496)
f4790_0_nieme_Load(EOS, o1994, i496, o1996, o1999, o1994, i496) → f4829_0_nieme_Load(EOS, o1994, i496, o1996, o1994, i496)
f4829_0_nieme_Load(EOS, o1994, i496, o1996, o1994, i496) → f4246_0_nieme_Load(EOS, o1994, i496, o1996, o1994, i496)
f4246_0_nieme_Load(EOS, o1725, i447, o1726, o1725, i447) → f4308_0_nieme_GT(EOS, o1725, i447, o1726, o1725, i447, i447)
f4431_0_nieme_FieldAccess(EOS, java.lang.Object(Liste(EOC, o1824)), i452, java.lang.Object(Liste(EOC, o1824)), i452, java.lang.Object(Liste(EOC, o1824))) → f4460_0_nieme_FieldAccess(EOS, java.lang.Object(Liste(EOC, o1824)), i452, java.lang.Object(Liste(EOC, o1824)), i452, java.lang.Object(Liste(EOC, o1824)))
f4460_0_nieme_FieldAccess(EOS, java.lang.Object(Liste(EOC, o1824)), i452, java.lang.Object(Liste(EOC, o1824)), i452, java.lang.Object(Liste(EOC, o1824))) → f4519_0_nieme_Load(EOS, java.lang.Object(Liste(EOC, o1824)), i452, java.lang.Object(Liste(EOC, o1824)), i452, o1824)
f4519_0_nieme_Load(EOS, java.lang.Object(Liste(EOC, o1824)), i452, java.lang.Object(Liste(EOC, o1824)), i452, o1824) → f4558_0_nieme_ConstantStackPush(EOS, java.lang.Object(Liste(EOC, o1824)), i452, java.lang.Object(Liste(EOC, o1824)), o1824, i452)
f4558_0_nieme_ConstantStackPush(EOS, java.lang.Object(Liste(EOC, o1824)), i452, java.lang.Object(Liste(EOC, o1824)), o1824, i452) → f4660_0_nieme_IntArithmetic(EOS, java.lang.Object(Liste(EOC, o1824)), i452, java.lang.Object(Liste(EOC, o1824)), o1824, i452, 1)
f4660_0_nieme_IntArithmetic(EOS, java.lang.Object(Liste(EOC, o1824)), i452, java.lang.Object(Liste(EOC, o1824)), o1824, i452, matching1) → f4725_0_nieme_InvokeMethod(EOS, java.lang.Object(Liste(EOC, o1824)), i452, java.lang.Object(Liste(EOC, o1824)), o1824, -(i452, 1)) | &&(>(i452, 0), =(matching1, 1))
f4725_0_nieme_InvokeMethod(EOS, java.lang.Object(Liste(EOC, o1824)), i452, java.lang.Object(Liste(EOC, o1824)), o1824, i497) → f4737_0_nieme_Load(EOS, o1824, i497, java.lang.Object(Liste(EOC, o1824)), o1824, i497)
f4725_0_nieme_InvokeMethod(EOS, java.lang.Object(Liste(EOC, o1824)), i452, java.lang.Object(Liste(EOC, o1824)), o1824, i497) → f4737_1_nieme_Load(EOS, java.lang.Object(Liste(EOC, o1824)), i452, java.lang.Object(Liste(EOC, o1824)), o1824, i497, o1824, i497)
f4737_0_nieme_Load(EOS, o1824, i497, java.lang.Object(Liste(EOC, o1824)), o1824, i497) → f4767_0_nieme_Load(EOS, o1824, i497, java.lang.Object(Liste(EOC, o1824)), o1824, i497)
f4767_0_nieme_Load(EOS, o1824, i497, java.lang.Object(Liste(EOC, o1824)), o1824, i497) → f4802_0_nieme_Load(EOS, o1824, i497, java.lang.Object(Liste(EOC, o1824)), o1824, i497)
f4802_0_nieme_Load(EOS, o2006, i497, o2009, o2006, i497) → f4838_0_nieme_Load(EOS, o2006, i497, o2009, o2006, i497)
f4838_0_nieme_Load(EOS, o2006, i497, o2009, o2006, i497) → f4246_0_nieme_Load(EOS, o2006, i497, o2009, o2006, i497)

Combined rules. Obtained 4 IRules

P rules:
f4308_0_nieme_GT(EOS, java.lang.Object(Liste(EOC, x0)), x1, x2, java.lang.Object(Liste(EOC, x0)), x1, x1) → f4731_1_nieme_Load(EOS, java.lang.Object(Liste(EOC, x0)), x1, x2, x0, -(x1, 1), x0, -(x1, 1)) | >(x1, 0)
f4308_0_nieme_GT(EOS, java.lang.Object(Liste(EOC, x0)), x1, x2, java.lang.Object(Liste(EOC, x0)), x1, x1) → f4308_0_nieme_GT(EOS, x0, -(x1, 1), x2, x0, -(x1, 1), -(x1, 1)) | >(x1, 0)
f4308_0_nieme_GT(EOS, java.lang.Object(Liste(EOC, x0)), x1, java.lang.Object(Liste(EOC, x0)), java.lang.Object(Liste(EOC, x0)), x1, x1) → f4737_1_nieme_Load(EOS, java.lang.Object(Liste(EOC, x0)), x1, java.lang.Object(Liste(EOC, x0)), x0, -(x1, 1), x0, -(x1, 1)) | >(x1, 0)
f4308_0_nieme_GT(EOS, java.lang.Object(Liste(EOC, x0)), x1, java.lang.Object(Liste(EOC, x0)), java.lang.Object(Liste(EOC, x0)), x1, x1) → f4308_0_nieme_GT(EOS, x0, -(x1, 1), java.lang.Object(Liste(EOC, x0)), x0, -(x1, 1), -(x1, 1)) | >(x1, 0)

Filtered ground terms:

f4308_0_nieme_GT(x1, x2, x3, x4, x5, x6, x7) → f4308_0_nieme_GT(x2, x3, x4, x5, x6, x7)
Cond_f4308_0_nieme_GT(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f4308_0_nieme_GT(x1, x3, x4, x5, x6, x7, x8)
f4731_1_nieme_Load(x1, x2, x3, x4, x5, x6, x7, x8) → f4731_1_nieme_Load(x2, x3, x4, x5, x6, x7, x8)
Cond_f4308_0_nieme_GT1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f4308_0_nieme_GT1(x1, x3, x4, x5, x6, x7, x8)
Cond_f4308_0_nieme_GT2(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f4308_0_nieme_GT2(x1, x3, x4, x5, x6, x7, x8)
f4737_1_nieme_Load(x1, x2, x3, x4, x5, x6, x7, x8) → f4737_1_nieme_Load(x2, x3, x4, x5, x6, x7, x8)
Cond_f4308_0_nieme_GT3(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f4308_0_nieme_GT3(x1, x3, x4, x5, x6, x7, x8)
Liste(x1, x2) → Liste(x2)

Filtered duplicate terms:

f4308_0_nieme_GT(x1, x2, x3, x4, x5, x6) → f4308_0_nieme_GT(x3, x4, x6)
Cond_f4308_0_nieme_GT(x1, x2, x3, x4, x5, x6, x7) → Cond_f4308_0_nieme_GT(x1, x4, x5, x7)
f4731_1_nieme_Load(x1, x2, x3, x4, x5, x6, x7) → f4731_1_nieme_Load(x1, x3, x7)
Cond_f4308_0_nieme_GT1(x1, x2, x3, x4, x5, x6, x7) → Cond_f4308_0_nieme_GT1(x1, x4, x5, x7)
Cond_f4308_0_nieme_GT2(x1, x2, x3, x4, x5, x6, x7) → Cond_f4308_0_nieme_GT2(x1, x5, x7)
f4737_1_nieme_Load(x1, x2, x3, x4, x5, x6, x7) → f4737_1_nieme_Load(x3, x7)
Cond_f4308_0_nieme_GT3(x1, x2, x3, x4, x5, x6, x7) → Cond_f4308_0_nieme_GT3(x1, x5, x7)

Filtered unneeded terms:

Cond_f4308_0_nieme_GT(x1, x2, x3, x4) → Cond_f4308_0_nieme_GT(x1)
Cond_f4308_0_nieme_GT2(x1, x2, x3) → Cond_f4308_0_nieme_GT2(x1)

Prepared 4 rules for path length conversion:

P rules:
f4308_0_nieme_GT(x2, java.lang.Object(Liste(x0)), x1) → f4731_1_nieme_Load(java.lang.Object(Liste(x0)), x2, -(x1, 1)) | >(x1, 0)
f4308_0_nieme_GT(x2, java.lang.Object(Liste(x0)), x1) → f4308_0_nieme_GT(x2, x0, -(x1, 1)) | >(x1, 0)
f4308_0_nieme_GT(java.lang.Object(Liste(x0)), java.lang.Object(Liste(x0)), x1) → f4737_1_nieme_Load(java.lang.Object(Liste(x0)), -(x1, 1)) | >(x1, 0)
f4308_0_nieme_GT(java.lang.Object(Liste(x0)), java.lang.Object(Liste(x0)), x1) → f4308_0_nieme_GT(java.lang.Object(Liste(x0)), x0, -(x1, 1)) | >(x1, 0)

Finished conversion. Obtained 2 rules.

P rules:
f4308_0_nieme_GT(v13, v14, x5) → f4308_0_nieme_GT(v15, v16, -(x5, 1)) | &&(&&(&&(&&(&&(&&(>(x5, 0), >(+(v16, 1), 0)), <=(+(v16, 1), v14)), >(+(v15, 1), 0)), <=(v15, v13)), >(+(v14, 1), 1)), >(+(v13, 1), 0))
f4308_0_nieme_GT(v17, v18, x9) → f4308_0_nieme_GT(v19, v20, -(x9, 1)) | &&(&&(&&(&&(&&(&&(&&(&&(>(x9, 0), >(+(v20, 1), 0)), <=(+(v20, 1), v18)), <=(+(v20, 1), v17)), >(+(v19, 1), 1)), <=(v19, v18)), <=(v19, v17)), >(+(v18, 1), 1)), >(+(v17, 1), 1))

(17) Obligation:

Rules:
f4308_0_nieme_GT(v13, v14, x5) → f4308_0_nieme_GT(v15, v16, -(x5, 1)) | &&(&&(&&(&&(&&(&&(>(x5, 0), >(+(v16, 1), 0)), <=(+(v16, 1), v14)), >(+(v15, 1), 0)), <=(v15, v13)), >(+(v14, 1), 1)), >(+(v13, 1), 0))
f4308_0_nieme_GT(v17, v18, x9) → f4308_0_nieme_GT(v19, v20, -(x9, 1)) | &&(&&(&&(&&(&&(&&(&&(&&(>(x9, 0), >(+(v20, 1), 0)), <=(+(v20, 1), v18)), <=(+(v20, 1), v17)), >(+(v19, 1), 1)), <=(v19, v18)), <=(v19, v17)), >(+(v18, 1), 1)), >(+(v17, 1), 1))

(18) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f4308_0_nieme_GT(x11, x13, x15)] = x15

Therefore the following rule(s) have been dropped:

f4308_0_nieme_GT(x0, x1, x2) → f4308_0_nieme_GT(x3, x4, -(x2, 1)) | &&(&&(&&(&&(&&(&&(>(x2, 0), >(+(x4, 1), 0)), <=(+(x4, 1), x1)), >(+(x3, 1), 0)), <=(x3, x0)), >(+(x1, 1), 1)), >(+(x0, 1), 0))
f4308_0_nieme_GT(x5, x6, x7) → f4308_0_nieme_GT(x8, x9, -(x7, 1)) | &&(&&(&&(&&(&&(&&(&&(&&(>(x7, 0), >(+(x9, 1), 0)), <=(+(x9, 1), x6)), <=(+(x9, 1), x5)), >(+(x8, 1), 1)), <=(x8, x6)), <=(x8, x5)), >(+(x6, 1), 1)), >(+(x5, 1), 1))

(19) YES

(20) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Partie.valeurMain(I)I
SCC calls the following helper methods:
Performed SCC analyses:

Used field analysis yielded the following read fields:
- Liste: [dom, suite]
- Domino: [gauche, droite]
Marker field analysis yielded the following relations that could be markers:

(21) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 52 IRules

P rules:
f8160_0_valeurMain_NULL(EOS, i1014, java.lang.Object(o4645sub), java.lang.Object(o4645sub)) → f8167_0_valeurMain_NULL(EOS, i1014, java.lang.Object(o4645sub), java.lang.Object(o4645sub))
f8167_0_valeurMain_NULL(EOS, i1014, java.lang.Object(o4645sub), java.lang.Object(o4645sub)) → f8170_0_valeurMain_Load(EOS, i1014, java.lang.Object(o4645sub))
f8170_0_valeurMain_Load(EOS, i1014, java.lang.Object(o4645sub)) → f8183_0_valeurMain_Load(EOS, i1014, java.lang.Object(o4645sub))
f8183_0_valeurMain_Load(EOS, i1014, java.lang.Object(o4645sub)) → f8211_0_valeurMain_FieldAccess(EOS, i1014, java.lang.Object(o4645sub), java.lang.Object(o4645sub))
f8211_0_valeurMain_FieldAccess(EOS, i1014, java.lang.Object(Liste(o4695sub, o4696, o4697)), java.lang.Object(Liste(o4695sub, o4696, o4697))) → f8227_0_valeurMain_FieldAccess(EOS, i1014, java.lang.Object(Liste(o4695sub, o4696, o4697)), java.lang.Object(Liste(o4695sub, o4696, o4697)))
f8227_0_valeurMain_FieldAccess(EOS, i1014, java.lang.Object(Liste(o4695sub, o4696, o4697)), java.lang.Object(Liste(o4695sub, o4696, o4697))) → f8252_0_valeurMain_InvokeMethod(EOS, i1014, java.lang.Object(Liste(o4695sub, o4696, o4697)), o4696)
f8252_0_valeurMain_InvokeMethod(EOS, i1014, java.lang.Object(Liste(o4695sub, o4696, o4697)), o4696) → f8274_0_valeurDomino_Load(EOS, i1014, java.lang.Object(Liste(o4695sub, o4696, o4697)), o4696, o4696)
f8274_0_valeurDomino_Load(EOS, i1014, java.lang.Object(Liste(o4695sub, o4696, o4697)), o4696, o4696) → f8284_0_valeurDomino_FieldAccess(EOS, i1014, java.lang.Object(Liste(o4695sub, o4696, o4697)), o4696, o4696, o4696)
f8284_0_valeurDomino_FieldAccess(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(o4742sub), o4697)), java.lang.Object(o4742sub), java.lang.Object(o4742sub), java.lang.Object(o4742sub)) → f8289_0_valeurDomino_FieldAccess(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(o4742sub), o4697)), java.lang.Object(o4742sub), java.lang.Object(o4742sub), java.lang.Object(o4742sub))
f8289_0_valeurDomino_FieldAccess(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115))) → f8304_0_valeurDomino_FieldAccess(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)))
f8304_0_valeurDomino_FieldAccess(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115))) → f8339_0_valeurDomino_Load(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1114)
f8339_0_valeurDomino_Load(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1114) → f8347_0_valeurDomino_FieldAccess(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1114, java.lang.Object(Domino(EOC, i1114, i1115)))
f8347_0_valeurDomino_FieldAccess(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1114, java.lang.Object(Domino(EOC, i1114, i1115))) → f8358_0_valeurDomino_LE(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1114, i1115)
f8358_0_valeurDomino_LE(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1114, i1115) → f8373_0_valeurDomino_LE(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1114, i1115)
f8358_0_valeurDomino_LE(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1114, i1115) → f8374_0_valeurDomino_LE(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1114, i1115)
f8373_0_valeurDomino_LE(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1114, i1115) → f8391_0_valeurDomino_Load(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115))) | <=(i1114, i1115)
f8391_0_valeurDomino_Load(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115))) → f8407_0_valeurDomino_FieldAccess(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)))
f8407_0_valeurDomino_FieldAccess(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115))) → f8424_0_valeurDomino_ConstantStackPush(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1115)
f8424_0_valeurDomino_ConstantStackPush(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1115) → f8434_0_valeurDomino_IntArithmetic(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1115, 10)
f8434_0_valeurDomino_IntArithmetic(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1115, matching1) → f8457_0_valeurDomino_Load(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), *(i1115, 10)) | =(matching1, 10)
f8457_0_valeurDomino_Load(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1154) → f8478_0_valeurDomino_FieldAccess(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), i1154, java.lang.Object(Domino(EOC, i1114, i1115)))
f8478_0_valeurDomino_FieldAccess(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), i1154, java.lang.Object(Domino(EOC, i1114, i1115))) → f8497_0_valeurDomino_IntArithmetic(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), i1154, i1114)
f8497_0_valeurDomino_IntArithmetic(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), i1154, i1114) → f8523_0_valeurDomino_Return(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), +(i1154, i1114))
f8523_0_valeurDomino_Return(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), i1169) → f8535_0_valeurMain_Store(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), i1169)
f8535_0_valeurMain_Store(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), i1169) → f8542_0_valeurMain_Store(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), i1169)
f8542_0_valeurMain_Store(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), i1170) → f8557_0_valeurMain_Load(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), i1170)
f8557_0_valeurMain_Load(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), i1170) → f8569_0_valeurMain_Load(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), i1170, i1170)
f8569_0_valeurMain_Load(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), i1170, i1170) → f8578_0_valeurMain_LE(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), i1170, i1170, i1014)
f8578_0_valeurMain_LE(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), i1170, i1170, i1014) → f8593_0_valeurMain_LE(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), i1170, i1170, i1014)
f8578_0_valeurMain_LE(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), i1170, i1170, i1014) → f8594_0_valeurMain_LE(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), i1170, i1170, i1014)
f8593_0_valeurMain_LE(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), i1170, i1170, i1014) → f8606_0_valeurMain_Load(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697))) | <=(i1170, i1014)
f8606_0_valeurMain_Load(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697))) → f8626_0_valeurMain_Store(EOS, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), i1014)
f8626_0_valeurMain_Store(EOS, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), i1014) → f8649_0_valeurMain_Store(EOS, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), i1014)
f8649_0_valeurMain_Store(EOS, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), i1170) → f8660_0_valeurMain_Load(EOS, i1170, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)))
f8660_0_valeurMain_Load(EOS, i1170, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697))) → f8670_0_valeurMain_FieldAccess(EOS, i1170, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)))
f8670_0_valeurMain_FieldAccess(EOS, i1170, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697))) → f8677_0_valeurMain_Store(EOS, i1170, o4697)
f8677_0_valeurMain_Store(EOS, i1170, o4697) → f8686_0_valeurMain_JMP(EOS, i1170, o4697)
f8686_0_valeurMain_JMP(EOS, i1170, o4697) → f8699_0_valeurMain_Load(EOS, i1170, o4697)
f8699_0_valeurMain_Load(EOS, i1170, o4697) → f7919_0_valeurMain_Load(EOS, i1170, o4697)
f7919_0_valeurMain_Load(EOS, i1014, o4403) → f8160_0_valeurMain_NULL(EOS, i1014, o4403, o4403)
f8594_0_valeurMain_LE(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), i1170, i1170, i1014) → f8610_0_valeurMain_Load(EOS, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), i1170) | >(i1170, i1014)
f8610_0_valeurMain_Load(EOS, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), i1170) → f8630_0_valeurMain_JMP(EOS, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), i1170)
f8630_0_valeurMain_JMP(EOS, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), i1170) → f8649_0_valeurMain_Store(EOS, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), i1170)
f8374_0_valeurDomino_LE(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1114, i1115) → f8401_0_valeurDomino_Load(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115))) | >(i1114, i1115)
f8401_0_valeurDomino_Load(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115))) → f8412_0_valeurDomino_FieldAccess(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)))
f8412_0_valeurDomino_FieldAccess(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115))) → f8426_0_valeurDomino_ConstantStackPush(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1114)
f8426_0_valeurDomino_ConstantStackPush(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1114) → f8439_0_valeurDomino_IntArithmetic(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1114, 10)
f8439_0_valeurDomino_IntArithmetic(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1114, matching1) → f8468_0_valeurDomino_Load(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), *(i1114, 10)) | =(matching1, 10)
f8468_0_valeurDomino_Load(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1158) → f8483_0_valeurDomino_FieldAccess(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1158, java.lang.Object(Domino(EOC, i1114, i1115)))
f8483_0_valeurDomino_FieldAccess(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1158, java.lang.Object(Domino(EOC, i1114, i1115))) → f8505_0_valeurDomino_IntArithmetic(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1158, i1115)
f8505_0_valeurDomino_IntArithmetic(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1158, i1115) → f8527_0_valeurDomino_Return(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), +(i1158, i1115))
f8527_0_valeurDomino_Return(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), java.lang.Object(Domino(EOC, i1114, i1115)), java.lang.Object(Domino(EOC, i1114, i1115)), i1170) → f8542_0_valeurMain_Store(EOS, i1014, java.lang.Object(Liste(o4695sub, java.lang.Object(Domino(EOC, i1114, i1115)), o4697)), i1170)

Combined rules. Obtained 4 IRules

P rules:
f8160_0_valeurMain_NULL(EOS, x0, java.lang.Object(Liste(x1, java.lang.Object(Domino(EOC, x2, x3)), x4)), java.lang.Object(Liste(x1, java.lang.Object(Domino(EOC, x2, x3)), x4))) → f8578_0_valeurMain_LE(EOS, x0, java.lang.Object(Liste(x1, java.lang.Object(Domino(EOC, x2, x3)), x4)), +(*(x3, 10), x2), +(*(x3, 10), x2), x0) | >=(x3, x2)
f8578_0_valeurMain_LE(EOS, x0, java.lang.Object(Liste(x1, java.lang.Object(Domino(EOC, x2, x3)), x4)), x5, x5, x0) → f8160_0_valeurMain_NULL(EOS, x0, x4, x4) | <=(x5, x0)
f8578_0_valeurMain_LE(EOS, x0, java.lang.Object(Liste(x1, java.lang.Object(Domino(EOC, x2, x3)), x4)), x5, x5, x0) → f8160_0_valeurMain_NULL(EOS, x5, x4, x4) | >(x5, x0)
f8160_0_valeurMain_NULL(EOS, x0, java.lang.Object(Liste(x1, java.lang.Object(Domino(EOC, x2, x3)), x4)), java.lang.Object(Liste(x1, java.lang.Object(Domino(EOC, x2, x3)), x4))) → f8578_0_valeurMain_LE(EOS, x0, java.lang.Object(Liste(x1, java.lang.Object(Domino(EOC, x2, x3)), x4)), +(*(x2, 10), x3), +(*(x2, 10), x3), x0) | <(x3, x2)

Filtered ground terms:

f8160_0_valeurMain_NULL(x1, x2, x3, x4) → f8160_0_valeurMain_NULL(x2, x3, x4)
Cond_f8160_0_valeurMain_NULL(x1, x2, x3, x4, x5) → Cond_f8160_0_valeurMain_NULL(x1, x3, x4, x5)
f8578_0_valeurMain_LE(x1, x2, x3, x4, x5, x6) → f8578_0_valeurMain_LE(x2, x3, x4, x5, x6)
Cond_f8578_0_valeurMain_LE(x1, x2, x3, x4, x5, x6, x7) → Cond_f8578_0_valeurMain_LE(x1, x3, x4, x5, x6, x7)
Cond_f8578_0_valeurMain_LE1(x1, x2, x3, x4, x5, x6, x7) → Cond_f8578_0_valeurMain_LE1(x1, x3, x4, x5, x6, x7)
Cond_f8160_0_valeurMain_NULL1(x1, x2, x3, x4, x5) → Cond_f8160_0_valeurMain_NULL1(x1, x3, x4, x5)
Domino(x1, x2, x3) → Domino(x2, x3)

Filtered duplicate terms:

f8160_0_valeurMain_NULL(x1, x2, x3) → f8160_0_valeurMain_NULL(x1, x3)
Cond_f8160_0_valeurMain_NULL(x1, x2, x3, x4) → Cond_f8160_0_valeurMain_NULL(x1, x2, x4)
f8578_0_valeurMain_LE(x1, x2, x3, x4, x5) → f8578_0_valeurMain_LE(x2, x4, x5)
Cond_f8578_0_valeurMain_LE(x1, x2, x3, x4, x5, x6) → Cond_f8578_0_valeurMain_LE(x1, x3, x5, x6)
Cond_f8578_0_valeurMain_LE1(x1, x2, x3, x4, x5, x6) → Cond_f8578_0_valeurMain_LE1(x1, x3, x5, x6)
Cond_f8160_0_valeurMain_NULL1(x1, x2, x3, x4) → Cond_f8160_0_valeurMain_NULL1(x1, x2, x4)

Filtered unneeded terms:

Cond_f8578_0_valeurMain_LE(x1, x2, x3, x4) → Cond_f8578_0_valeurMain_LE(x1, x2, x4)
Liste(x1, x2, x3) → Liste(x2, x3)
Cond_f8578_0_valeurMain_LE1(x1, x2, x3, x4) → Cond_f8578_0_valeurMain_LE1(x1, x2, x3)

Prepared 4 rules for path length conversion:

P rules:
f8160_0_valeurMain_NULL(x0, java.lang.Object(Liste(java.lang.Object(Domino(x2, x3)), x4))) → f8578_0_valeurMain_LE(java.lang.Object(Liste(java.lang.Object(Domino(x2, x3)), x4)), +(*(x3, 10), x2), x0, x2, x3, x4) | >=(x3, x2)
f8578_0_valeurMain_LE(java.lang.Object(Liste(java.lang.Object(Domino(x2, x3)), x4)), x5, x0, x2, x3, x4) → f8160_0_valeurMain_NULL(x0, x4) | <=(x5, x0)
f8578_0_valeurMain_LE(java.lang.Object(Liste(java.lang.Object(Domino(x2, x3)), x4)), x5, x0, x2, x3, x4) → f8160_0_valeurMain_NULL(x5, x4) | >(x5, x0)
f8160_0_valeurMain_NULL(x0, java.lang.Object(Liste(java.lang.Object(Domino(x2, x3)), x4))) → f8578_0_valeurMain_LE(java.lang.Object(Liste(java.lang.Object(Domino(x2, x3)), x4)), +(*(x2, 10), x3), x0, x2, x3, x4) | <(x3, x2)

Finished conversion. Obtained 4 rules.

P rules:
f8160_0_valeurMain_NULL(x0, v26) → f8578_0_valeurMain_LE(v27, +(*(10, x2), x1), x0, x1, x2, v28) | &&(&&(&&(&&(&&(&&(&&(>=(x2, x1), <=(+(x2, 4), v26)), <=(+(x1, 4), v26)), >(+(v28, 1), 0)), <=(+(v28, 2), v26)), >(+(v27, 1), 3)), <=(v27, v26)), >(+(v26, 1), 3))
f8578_0_valeurMain_LE(v29, x7, x8, x4, x5, v30) → f8160_0_valeurMain_NULL(x8, v31) | &&(&&(&&(&&(&&(&&(&&(>=(x8, x7), <=(+(x5, 4), v29)), <=(+(x4, 4), v29)), >(+(v31, 1), 0)), <=(v31, v30)), <=(+(v31, 2), v29)), >(+(v30, 1), 0)), >(+(v29, 1), 3))
f8578_0_valeurMain_LE(v32, x12, x13, x9, x10, v33) → f8160_0_valeurMain_NULL(x12, v34) | &&(&&(&&(&&(&&(&&(&&(<=(+(x9, 4), v32), <(x13, x12)), <=(+(x10, 4), v32)), >(+(v34, 1), 0)), <=(v34, v33)), <=(+(v34, 2), v32)), >(+(v33, 1), 0)), >(+(v32, 1), 3))
f8160_0_valeurMain_NULL(x14, v35) → f8578_0_valeurMain_LE(v36, +(*(10, x15), x16), x14, x15, x16, v37) | &&(&&(&&(&&(&&(&&(&&(<(x16, x15), <=(+(x16, 4), v35)), <=(+(x15, 4), v35)), >(+(v37, 1), 0)), <=(+(v37, 2), v35)), >(+(v36, 1), 3)), <=(v36, v35)), >(+(v35, 1), 3))

(22) Obligation:

Rules:
f8160_0_valeurMain_NULL(x0, v26) → f8578_0_valeurMain_LE(v27, +(*(10, x2), x1), x0, x1, x2, v28) | &&(&&(&&(&&(&&(&&(&&(>=(x2, x1), <=(+(x2, 4), v26)), <=(+(x1, 4), v26)), >(+(v28, 1), 0)), <=(+(v28, 2), v26)), >(+(v27, 1), 3)), <=(v27, v26)), >(+(v26, 1), 3))
f8578_0_valeurMain_LE(v29, x7, x8, x4, x5, v30) → f8160_0_valeurMain_NULL(x8, v31) | &&(&&(&&(&&(&&(&&(&&(>=(x8, x7), <=(+(x5, 4), v29)), <=(+(x4, 4), v29)), >(+(v31, 1), 0)), <=(v31, v30)), <=(+(v31, 2), v29)), >(+(v30, 1), 0)), >(+(v29, 1), 3))
f8578_0_valeurMain_LE(v32, x12, x13, x9, x10, v33) → f8160_0_valeurMain_NULL(x12, v34) | &&(&&(&&(&&(&&(&&(&&(<=(+(x9, 4), v32), <(x13, x12)), <=(+(x10, 4), v32)), >(+(v34, 1), 0)), <=(v34, v33)), <=(+(v34, 2), v32)), >(+(v33, 1), 0)), >(+(v32, 1), 3))
f8160_0_valeurMain_NULL(x14, v35) → f8578_0_valeurMain_LE(v36, +(*(10, x15), x16), x14, x15, x16, v37) | &&(&&(&&(&&(&&(&&(&&(<(x16, x15), <=(+(x16, 4), v35)), <=(+(x15, 4), v35)), >(+(v37, 1), 0)), <=(+(v37, 2), v35)), >(+(v36, 1), 3)), <=(v36, v35)), >(+(v35, 1), 3))

(23) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f8160_0_valeurMain_NULL(x27, x29)] = 1 + x29
[f8578_0_valeurMain_LE(x32, x34, x36, x38, x40, x42)] = x32

Therefore the following rule(s) have been dropped:

f8160_0_valeurMain_NULL(x0, x1) → f8578_0_valeurMain_LE(x2, +(*(10, x3), x4), x0, x4, x3, x5) | &&(&&(&&(&&(&&(&&(&&(>=(x3, x4), <=(+(x3, 4), x1)), <=(+(x4, 4), x1)), >(+(x5, 1), 0)), <=(+(x5, 2), x1)), >(+(x2, 1), 3)), <=(x2, x1)), >(+(x1, 1), 3))
f8578_0_valeurMain_LE(x6, x7, x8, x9, x10, x11) → f8160_0_valeurMain_NULL(x8, x12) | &&(&&(&&(&&(&&(&&(&&(>=(x8, x7), <=(+(x10, 4), x6)), <=(+(x9, 4), x6)), >(+(x12, 1), 0)), <=(x12, x11)), <=(+(x12, 2), x6)), >(+(x11, 1), 0)), >(+(x6, 1), 3))
f8578_0_valeurMain_LE(x13, x14, x15, x16, x17, x18) → f8160_0_valeurMain_NULL(x14, x19) | &&(&&(&&(&&(&&(&&(&&(<=(+(x16, 4), x13), <(x15, x14)), <=(+(x17, 4), x13)), >(+(x19, 1), 0)), <=(x19, x18)), <=(+(x19, 2), x13)), >(+(x18, 1), 0)), >(+(x13, 1), 3))
f8160_0_valeurMain_NULL(x20, x21) → f8578_0_valeurMain_LE(x22, +(*(10, x23), x24), x20, x23, x24, x25) | &&(&&(&&(&&(&&(&&(&&(<(x24, x23), <=(+(x24, 4), x21)), <=(+(x23, 4), x21)), >(+(x25, 1), 0)), <=(+(x25, 2), x21)), >(+(x22, 1), 3)), <=(x22, x21)), >(+(x21, 1), 3))

(24) YES

(25) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Partie.longueur(LListe;)I
SCC calls the following helper methods: Partie.longueur(LListe;)I
Performed SCC analyses:

Used field analysis yielded the following read fields:
- Liste: [suite]
Marker field analysis yielded the following relations that could be markers:

(26) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 11 IRules

P rules:
f1326_0_longueur_NONNULL(EOS, java.lang.Object(o238sub), java.lang.Object(o238sub), java.lang.Object(o238sub)) → f1330_0_longueur_NONNULL(EOS, java.lang.Object(o238sub), java.lang.Object(o238sub), java.lang.Object(o238sub))
f1330_0_longueur_NONNULL(EOS, java.lang.Object(o238sub), java.lang.Object(o238sub), java.lang.Object(o238sub)) → f1348_0_longueur_ConstantStackPush(EOS, java.lang.Object(o238sub), java.lang.Object(o238sub))
f1348_0_longueur_ConstantStackPush(EOS, java.lang.Object(o238sub), java.lang.Object(o238sub)) → f1360_0_longueur_Load(EOS, java.lang.Object(o238sub), java.lang.Object(o238sub))
f1360_0_longueur_Load(EOS, java.lang.Object(o238sub), java.lang.Object(o238sub)) → f1371_0_longueur_FieldAccess(EOS, java.lang.Object(o238sub), java.lang.Object(o238sub))
f1371_0_longueur_FieldAccess(EOS, java.lang.Object(Liste(EOC, o270)), java.lang.Object(Liste(EOC, o270))) → f1386_0_longueur_FieldAccess(EOS, java.lang.Object(Liste(EOC, o270)), java.lang.Object(Liste(EOC, o270)))
f1386_0_longueur_FieldAccess(EOS, java.lang.Object(Liste(EOC, o270)), java.lang.Object(Liste(EOC, o270))) → f1414_0_longueur_InvokeMethod(EOS, java.lang.Object(Liste(EOC, o270)), o270)
f1414_0_longueur_InvokeMethod(EOS, java.lang.Object(Liste(EOC, o270)), o270) → f1423_0_longueur_Load(EOS, o270, o270)
f1414_0_longueur_InvokeMethod(EOS, java.lang.Object(Liste(EOC, o270)), o270) → f1423_1_longueur_Load(EOS, java.lang.Object(Liste(EOC, o270)), o270, o270)
f1423_0_longueur_Load(EOS, o270, o270) → f1428_0_longueur_Load(EOS, o270, o270)
f1428_0_longueur_Load(EOS, o270, o270) → f1320_0_longueur_Load(EOS, o270, o270)
f1320_0_longueur_Load(EOS, o175, o175) → f1326_0_longueur_NONNULL(EOS, o175, o175, o175)

Combined rules. Obtained 2 IRules

P rules:
f1326_0_longueur_NONNULL(EOS, java.lang.Object(Liste(EOC, x0)), java.lang.Object(Liste(EOC, x0)), java.lang.Object(Liste(EOC, x0))) → f1423_1_longueur_Load(EOS, java.lang.Object(Liste(EOC, x0)), x0, x0)
f1326_0_longueur_NONNULL(EOS, java.lang.Object(Liste(EOC, x0)), java.lang.Object(Liste(EOC, x0)), java.lang.Object(Liste(EOC, x0))) → f1326_0_longueur_NONNULL(EOS, x0, x0, x0)

Filtered ground terms:

f1326_0_longueur_NONNULL(x1, x2, x3, x4) → f1326_0_longueur_NONNULL(x2, x3, x4)
f1423_1_longueur_Load(x1, x2, x3, x4) → f1423_1_longueur_Load(x2, x3, x4)
Liste(x1, x2) → Liste(x2)

Filtered duplicate terms:

f1326_0_longueur_NONNULL(x1, x2, x3) → f1326_0_longueur_NONNULL(x3)
f1423_1_longueur_Load(x1, x2, x3) → f1423_1_longueur_Load(x1)

Prepared 2 rules for path length conversion:

P rules:
f1326_0_longueur_NONNULL(java.lang.Object(Liste(x0))) → f1423_1_longueur_Load(java.lang.Object(Liste(x0)))
f1326_0_longueur_NONNULL(java.lang.Object(Liste(x0))) → f1326_0_longueur_NONNULL(x0)

Finished conversion. Obtained 1 rules.

P rules:
f1326_0_longueur_NONNULL(v3) → f1326_0_longueur_NONNULL(v4) | &&(&&(>(+(v4, 1), 0), <=(+(v4, 1), v3)), >(+(v3, 1), 1))

(27) Obligation:

Rules:
f1326_0_longueur_NONNULL(v3) → f1326_0_longueur_NONNULL(v4) | &&(&&(>(+(v4, 1), 0), <=(+(v4, 1), v3)), >(+(v3, 1), 1))

(28) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f1326_0_longueur_NONNULL(x3)] = x3

Therefore the following rule(s) have been dropped:

f1326_0_longueur_NONNULL(x0) → f1326_0_longueur_NONNULL(x1) | &&(&&(>(+(x1, 1), 0), <=(+(x1, 1), x0)), >(+(x0, 1), 1))

(29) YES

(30) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Partie.lister(LListe;)V
SCC calls the following helper methods: Partie.lister(LListe;)V
Performed SCC analyses:

Used field analysis yielded the following read fields:
- Liste: [suite]
Marker field analysis yielded the following relations that could be markers:

(31) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 10 IRules

P rules:
f1249_0_lister_NONNULL(EOS, java.lang.Object(o221sub), java.lang.Object(o221sub), java.lang.Object(o221sub)) → f1254_0_lister_NONNULL(EOS, java.lang.Object(o221sub), java.lang.Object(o221sub), java.lang.Object(o221sub))
f1254_0_lister_NONNULL(EOS, java.lang.Object(o221sub), java.lang.Object(o221sub), java.lang.Object(o221sub)) → f1260_0_lister_Load(EOS, java.lang.Object(o221sub), java.lang.Object(o221sub))
f1260_0_lister_Load(EOS, java.lang.Object(o221sub), java.lang.Object(o221sub)) → f1268_0_lister_FieldAccess(EOS, java.lang.Object(o221sub), java.lang.Object(o221sub))
f1268_0_lister_FieldAccess(EOS, java.lang.Object(Liste(o226sub, o228)), java.lang.Object(Liste(o226sub, o228))) → f1278_0_lister_FieldAccess(EOS, java.lang.Object(Liste(o226sub, o228)), java.lang.Object(Liste(o226sub, o228)))
f1278_0_lister_FieldAccess(EOS, java.lang.Object(Liste(o226sub, o228)), java.lang.Object(Liste(o226sub, o228))) → f1303_0_lister_InvokeMethod(EOS, java.lang.Object(Liste(o226sub, o228)), o228)
f1303_0_lister_InvokeMethod(EOS, java.lang.Object(Liste(o226sub, o228)), o228) → f1311_0_lister_Load(EOS, o228, o228)
f1303_0_lister_InvokeMethod(EOS, java.lang.Object(Liste(o226sub, o228)), o228) → f1311_1_lister_Load(EOS, java.lang.Object(Liste(o226sub, o228)), o228, o228)
f1311_0_lister_Load(EOS, o228, o228) → f1322_0_lister_Load(EOS, o228, o228)
f1322_0_lister_Load(EOS, o228, o228) → f1245_0_lister_Load(EOS, o228, o228)
f1245_0_lister_Load(EOS, o218, o218) → f1249_0_lister_NONNULL(EOS, o218, o218, o218)

Combined rules. Obtained 2 IRules

P rules:
f1249_0_lister_NONNULL(EOS, java.lang.Object(Liste(x0, x1)), java.lang.Object(Liste(x0, x1)), java.lang.Object(Liste(x0, x1))) → f1311_1_lister_Load(EOS, java.lang.Object(Liste(x0, x1)), x1, x1)
f1249_0_lister_NONNULL(EOS, java.lang.Object(Liste(x0, x1)), java.lang.Object(Liste(x0, x1)), java.lang.Object(Liste(x0, x1))) → f1249_0_lister_NONNULL(EOS, x1, x1, x1)

Filtered ground terms:

f1249_0_lister_NONNULL(x1, x2, x3, x4) → f1249_0_lister_NONNULL(x2, x3, x4)
f1311_1_lister_Load(x1, x2, x3, x4) → f1311_1_lister_Load(x2, x3, x4)

Filtered duplicate terms:

f1249_0_lister_NONNULL(x1, x2, x3) → f1249_0_lister_NONNULL(x3)
f1311_1_lister_Load(x1, x2, x3) → f1311_1_lister_Load(x1)

Filtered unneeded terms:

Liste(x1, x2) → Liste(x2)

Prepared 2 rules for path length conversion:

P rules:
f1249_0_lister_NONNULL(java.lang.Object(Liste(x1))) → f1311_1_lister_Load(java.lang.Object(Liste(x1)))
f1249_0_lister_NONNULL(java.lang.Object(Liste(x1))) → f1249_0_lister_NONNULL(x1)

Finished conversion. Obtained 1 rules.

P rules:
f1249_0_lister_NONNULL(v3) → f1249_0_lister_NONNULL(v4) | &&(&&(>(+(v4, 1), 0), <=(+(v4, 1), v3)), >(+(v3, 1), 1))

(32) Obligation:

Rules:
f1249_0_lister_NONNULL(v3) → f1249_0_lister_NONNULL(v4) | &&(&&(>(+(v4, 1), 0), <=(+(v4, 1), v3)), >(+(v3, 1), 1))

(33) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:

[f1249_0_lister_NONNULL(x)] = 1·x₁

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

Therefore the following rule(s) have been dropped:

f1249_0_lister_NONNULL(x0) → f1249_0_lister_NONNULL(x1) | &&(&&(>(+(x1, 1), 0), <=(+(x1, 1), x0)), >(+(x0, 1), 1))

(34) YES

(35) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Partie.plusForteMain()I
SCC calls the following helper methods: Partie.valeurMain(I)I
Performed SCC analyses:

Used field analysis yielded the following read fields:
- Partie: [mains]
Marker field analysis yielded the following relations that could be markers:

(36) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 30 IRules

P rules:
f5837_0_plusForteMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i656, i657, i658, i658) → f5849_0_plusForteMain_FieldAccess(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i656, i657, i658, i658, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))))
f5849_0_plusForteMain_FieldAccess(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i656, i657, i658, i658, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655))))) → f5858_0_plusForteMain_ArrayLength(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i656, i657, i658, i658, java.lang.Object(ARRAY(i655)))
f5858_0_plusForteMain_ArrayLength(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i656, i657, i658, i658, java.lang.Object(ARRAY(i655))) → f5870_0_plusForteMain_GE(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i656, i657, i658, i658, i655) | >=(i655, 0)
f5870_0_plusForteMain_GE(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i656, i657, i658, i658, i655) → f5876_0_plusForteMain_GE(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i656, i657, i658, i658, i655)
f5876_0_plusForteMain_GE(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i656, i657, i658, i658, i655) → f5886_0_plusForteMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i656, i657, i658) | <(i658, i655)
f5886_0_plusForteMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i656, i657, i658) → f5904_0_plusForteMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i656, i657, i658, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))))
f5904_0_plusForteMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i656, i657, i658, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655))))) → f5925_0_plusForteMain_InvokeMethod(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i656, i657, i658, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i658)
f5925_0_plusForteMain_InvokeMethod(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i656, i657, i658, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i658) → f5965_0_valeurMain_ConstantStackPush(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i658, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i658)
f5925_0_plusForteMain_InvokeMethod(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i656, i657, i658, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i658) → f5965_1_valeurMain_ConstantStackPush(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i656, i657, i658, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i658, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i658)
f5965_0_valeurMain_ConstantStackPush(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i658, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i658) → f6026_0_valeurMain_ConstantStackPush(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i658, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i658)
f8264_0_valeurMain_Return(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1097)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1097)))), i656, i657, i1099, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1097)))), i1099, i1094) → f8265_0_valeurMain_Return(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1097)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1097)))), i656, i657, i1099, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1097)))), i1099, i1094)
f8265_0_valeurMain_Return(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i656, i657, i1104, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i1104, i1102) → f8277_0_plusForteMain_Store(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i656, i657, i1104, i1102)
f8277_0_plusForteMain_Store(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i656, i657, i1104, i1102) → f8280_0_plusForteMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i656, i657, i1104, i1102)
f8280_0_plusForteMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i656, i657, i1104, i1102) → f8285_0_plusForteMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i656, i657, i1104, i1102, i1102)
f8285_0_plusForteMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i656, i657, i1104, i1102, i1102) → f8292_0_plusForteMain_LE(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i656, i657, i1104, i1102, i1102, i656)
f8292_0_plusForteMain_LE(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i656, i657, i1104, i1102, i1102, i656) → f8306_0_plusForteMain_LE(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i656, i657, i1104, i1102, i1102, i656)
f8292_0_plusForteMain_LE(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i656, i657, i1104, i1102, i1102, i656) → f8307_0_plusForteMain_LE(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i656, i657, i1104, i1102, i1102, i656)
f8306_0_plusForteMain_LE(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i656, i657, i1104, i1102, i1102, i656) → f8330_0_plusForteMain_Inc(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i656, i657, i1104) | <=(i1102, i656)
f8330_0_plusForteMain_Inc(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i656, i657, i1104) → f8345_0_plusForteMain_JMP(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i656, i657, +(i1104, 1)) | >=(i1104, 0)
f8345_0_plusForteMain_JMP(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i656, i657, i1129) → f8386_0_plusForteMain_JMP(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i656, i657, i1129)
f8386_0_plusForteMain_JMP(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i1102, i1104, i1138) → f8396_0_plusForteMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i1102, i1104, i1138)
f8396_0_plusForteMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i1102, i1104, i1138) → f5832_0_plusForteMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i1102, i1104, i1138)
f5832_0_plusForteMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i656, i657, i658) → f5837_0_plusForteMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i655)))), i656, i657, i658, i658)
f8307_0_plusForteMain_LE(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i656, i657, i1104, i1102, i1102, i656) → f8340_0_plusForteMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i1104, i1102) | >(i1102, i656)
f8340_0_plusForteMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i1104, i1102) → f8349_0_plusForteMain_Store(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i1104, i1102)
f8349_0_plusForteMain_Store(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i1104, i1102) → f8359_0_plusForteMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i1102, i1104)
f8359_0_plusForteMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i1102, i1104) → f8369_0_plusForteMain_Store(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i1102, i1104, i1104)
f8369_0_plusForteMain_Store(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i1102, i1104, i1104) → f8377_0_plusForteMain_Inc(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i1102, i1104, i1104)
f8377_0_plusForteMain_Inc(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i1102, i1104, i1104) → f8386_0_plusForteMain_JMP(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1103)))), i1102, i1104, +(i1104, 1)) | >=(i1104, 0)
f5965_1_valeurMain_ConstantStackPush(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1097)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1097)))), i656, i657, i1099, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1097)))), i1099, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1097)))), i1099) → f8264_0_valeurMain_Return(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1097)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1097)))), i656, i657, i1099, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i1097)))), i1099, i1094)

Combined rules. Obtained 3 IRules

P rules:
f5837_0_plusForteMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x0)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x0)))), x1, x2, x3, x3) → f6026_0_valeurMain_ConstantStackPush(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x0)))), x3, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x0)))), x3) | &&(>(+(x0, 1), 0), <(x3, x0))
f5837_0_plusForteMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x0)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x0)))), x1, x2, x3, x3) → f5837_0_plusForteMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x0)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x0)))), x1, x2, +(x3, 1), +(x3, 1)) | &&(&&(>(+(x3, 1), 0), >(+(x0, 1), 0)), <(x3, x0))
f5837_0_plusForteMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x0)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x0)))), x1, x2, x3, x3) → f5837_0_plusForteMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x0)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x0)))), x4, x3, +(x3, 1), +(x3, 1)) | &&(&&(&&(>(x4, x1), >(+(x3, 1), 0)), >(+(x0, 1), 0)), <(x3, x0))

Filtered ground terms:

f5837_0_plusForteMain_Load(x1, x2, x3, x4, x5, x6, x7) → f5837_0_plusForteMain_Load(x2, x3, x4, x5, x6, x7)
Cond_f5837_0_plusForteMain_Load(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f5837_0_plusForteMain_Load(x1, x3, x4, x5, x6, x7, x8)
f6026_0_valeurMain_ConstantStackPush(x1, x2, x3, x4, x5) → f6026_0_valeurMain_ConstantStackPush(x2, x3, x4, x5)
Cond_f5837_0_plusForteMain_Load1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f5837_0_plusForteMain_Load1(x1, x3, x4, x5, x6, x7, x8)
Cond_f5837_0_plusForteMain_Load2(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f5837_0_plusForteMain_Load2(x1, x3, x4, x5, x6, x7, x8, x9)
Partie(x1, x2) → Partie(x2)

Filtered duplicate terms:

f5837_0_plusForteMain_Load(x1, x2, x3, x4, x5, x6) → f5837_0_plusForteMain_Load(x2, x3, x4, x6)
Cond_f5837_0_plusForteMain_Load(x1, x2, x3, x4, x5, x6, x7) → Cond_f5837_0_plusForteMain_Load(x1, x3, x4, x5, x7)
f6026_0_valeurMain_ConstantStackPush(x1, x2, x3, x4) → f6026_0_valeurMain_ConstantStackPush(x3, x4)
Cond_f5837_0_plusForteMain_Load1(x1, x2, x3, x4, x5, x6, x7) → Cond_f5837_0_plusForteMain_Load1(x1, x3, x4, x5, x7)
Cond_f5837_0_plusForteMain_Load2(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f5837_0_plusForteMain_Load2(x1, x3, x4, x5, x7, x8)

Filtered unneeded terms:

Cond_f5837_0_plusForteMain_Load(x1, x2, x3, x4, x5) → Cond_f5837_0_plusForteMain_Load(x1)
Cond_f5837_0_plusForteMain_Load1(x1, x2, x3, x4, x5) → Cond_f5837_0_plusForteMain_Load1(x1, x2, x3, x5)
Cond_f5837_0_plusForteMain_Load2(x1, x2, x3, x4, x5, x6) → Cond_f5837_0_plusForteMain_Load2(x1, x2, x5, x6)
f5837_0_plusForteMain_Load(x1, x2, x3, x4) → f5837_0_plusForteMain_Load(x1, x2, x4)

Prepared 3 rules for path length conversion:

P rules:
f5837_0_plusForteMain_Load(java.lang.Object(Partie(java.lang.Object(ARRAY(x0)))), x1, x3, x0) → f6026_0_valeurMain_ConstantStackPush(java.lang.Object(Partie(java.lang.Object(ARRAY(x0)))), x3) | &&(>(+(x0, 1), 0), <(x3, x0))
f5837_0_plusForteMain_Load(java.lang.Object(Partie(java.lang.Object(ARRAY(x0)))), x1, x3, x0) → f5837_0_plusForteMain_Load(java.lang.Object(Partie(java.lang.Object(ARRAY(x0)))), x1, +(x3, 1), x0) | &&(&&(>(+(x3, 1), 0), >(+(x0, 1), 0)), <(x3, x0))
f5837_0_plusForteMain_Load(java.lang.Object(Partie(java.lang.Object(ARRAY(x0)))), x1, x3, x0) → f5837_0_plusForteMain_Load(java.lang.Object(Partie(java.lang.Object(ARRAY(x0)))), x4, +(x3, 1), x0) | &&(&&(&&(>(x4, x1), >(+(x3, 1), 0)), >(+(x0, 1), 0)), <(x3, x0))

Finished conversion. Obtained 2 rules.

P rules:
f5837_0_plusForteMain_Load(v14, x4, x5, x3) → f5837_0_plusForteMain_Load(v15, x4, +(x5, 1), x3) | &&(&&(&&(&&(&&(>(x5, -1), <(x5, x3)), >(x3, -1)), >(+(v15, 1), 3)), <=(v15, v14)), >(+(v14, 1), 3))
f5837_0_plusForteMain_Load(v16, x7, x8, x6) → f5837_0_plusForteMain_Load(v17, x9, +(x8, 1), x6) | &&(&&(&&(&&(&&(&&(>(x9, x7), >(x8, -1)), <(x8, x6)), >(x6, -1)), >(+(v17, 1), 3)), <=(v17, v16)), >(+(v16, 1), 3))

(37) Obligation:

Rules:
f5837_0_plusForteMain_Load(v14, x4, x5, x3) → f5837_0_plusForteMain_Load(v15, x4, +(x5, 1), x3) | &&(&&(&&(&&(&&(>(x5, -1), <(x5, x3)), >(x3, -1)), >(+(v15, 1), 3)), <=(v15, v14)), >(+(v14, 1), 3))
f5837_0_plusForteMain_Load(v16, x7, x8, x6) → f5837_0_plusForteMain_Load(v17, x9, +(x8, 1), x6) | &&(&&(&&(&&(&&(&&(>(x9, x7), >(x8, -1)), <(x8, x6)), >(x6, -1)), >(+(v17, 1), 3)), <=(v17, v16)), >(+(v16, 1), 3))

(38) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f5837_0_plusForteMain_Load(x12, x14, x16, x18)] = -x16 + x18

Therefore the following rule(s) have been dropped:

f5837_0_plusForteMain_Load(x0, x1, x2, x3) → f5837_0_plusForteMain_Load(x4, x1, +(x2, 1), x3) | &&(&&(&&(&&(&&(>(x2, -1), <(x2, x3)), >(x3, -1)), >(+(x4, 1), 3)), <=(x4, x0)), >(+(x0, 1), 3))
f5837_0_plusForteMain_Load(x5, x6, x7, x8) → f5837_0_plusForteMain_Load(x9, x10, +(x7, 1), x8) | &&(&&(&&(&&(&&(&&(>(x10, x6), >(x7, -1)), <(x7, x8)), >(x8, -1)), >(+(x9, 1), 3)), <=(x9, x5)), >(+(x5, 1), 3))

(39) YES

(40) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Partie.plusForteMain()I
SCC calls the following helper methods:
Performed SCC analyses:

Used field analysis yielded the following read fields:
- Liste: [dom, suite]
- Domino: [gauche, droite]
Marker field analysis yielded the following relations that could be markers:

(41) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 52 IRules

P rules:
f2860_0_valeurMain_NULL(EOS, i262, java.lang.Object(o1106sub), java.lang.Object(o1106sub)) → f2871_0_valeurMain_NULL(EOS, i262, java.lang.Object(o1106sub), java.lang.Object(o1106sub))
f2871_0_valeurMain_NULL(EOS, i262, java.lang.Object(o1106sub), java.lang.Object(o1106sub)) → f2878_0_valeurMain_Load(EOS, i262, java.lang.Object(o1106sub))
f2878_0_valeurMain_Load(EOS, i262, java.lang.Object(o1106sub)) → f2893_0_valeurMain_Load(EOS, i262, java.lang.Object(o1106sub))
f2893_0_valeurMain_Load(EOS, i262, java.lang.Object(o1106sub)) → f2905_0_valeurMain_FieldAccess(EOS, i262, java.lang.Object(o1106sub), java.lang.Object(o1106sub))
f2905_0_valeurMain_FieldAccess(EOS, i262, java.lang.Object(Liste(o1117sub, o1118, o1119)), java.lang.Object(Liste(o1117sub, o1118, o1119))) → f2918_0_valeurMain_FieldAccess(EOS, i262, java.lang.Object(Liste(o1117sub, o1118, o1119)), java.lang.Object(Liste(o1117sub, o1118, o1119)))
f2918_0_valeurMain_FieldAccess(EOS, i262, java.lang.Object(Liste(o1117sub, o1118, o1119)), java.lang.Object(Liste(o1117sub, o1118, o1119))) → f2931_0_valeurMain_InvokeMethod(EOS, i262, java.lang.Object(Liste(o1117sub, o1118, o1119)), o1118)
f2931_0_valeurMain_InvokeMethod(EOS, i262, java.lang.Object(Liste(o1117sub, o1118, o1119)), o1118) → f2942_0_valeurDomino_Load(EOS, i262, java.lang.Object(Liste(o1117sub, o1118, o1119)), o1118, o1118)
f2942_0_valeurDomino_Load(EOS, i262, java.lang.Object(Liste(o1117sub, o1118, o1119)), o1118, o1118) → f2966_0_valeurDomino_FieldAccess(EOS, i262, java.lang.Object(Liste(o1117sub, o1118, o1119)), o1118, o1118, o1118)
f2966_0_valeurDomino_FieldAccess(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(o1128sub), o1119)), java.lang.Object(o1128sub), java.lang.Object(o1128sub), java.lang.Object(o1128sub)) → f2977_0_valeurDomino_FieldAccess(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(o1128sub), o1119)), java.lang.Object(o1128sub), java.lang.Object(o1128sub), java.lang.Object(o1128sub))
f2977_0_valeurDomino_FieldAccess(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299))) → f2992_0_valeurDomino_FieldAccess(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)))
f2992_0_valeurDomino_FieldAccess(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299))) → f3017_0_valeurDomino_Load(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i298)
f3017_0_valeurDomino_Load(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i298) → f3041_0_valeurDomino_FieldAccess(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i298, java.lang.Object(Domino(EOC, i298, i299)))
f3041_0_valeurDomino_FieldAccess(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i298, java.lang.Object(Domino(EOC, i298, i299))) → f3059_0_valeurDomino_LE(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i298, i299)
f3059_0_valeurDomino_LE(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i298, i299) → f3075_0_valeurDomino_LE(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i298, i299)
f3059_0_valeurDomino_LE(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i298, i299) → f3076_0_valeurDomino_LE(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i298, i299)
f3075_0_valeurDomino_LE(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i298, i299) → f3089_0_valeurDomino_Load(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299))) | <=(i298, i299)
f3089_0_valeurDomino_Load(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299))) → f3171_0_valeurDomino_FieldAccess(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)))
f3171_0_valeurDomino_FieldAccess(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299))) → f3238_0_valeurDomino_ConstantStackPush(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i299)
f3238_0_valeurDomino_ConstantStackPush(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i299) → f3318_0_valeurDomino_IntArithmetic(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i299, 10)
f3318_0_valeurDomino_IntArithmetic(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i299, matching1) → f3360_0_valeurDomino_Load(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), *(i299, 10)) | =(matching1, 10)
f3360_0_valeurDomino_Load(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i320) → f3431_0_valeurDomino_FieldAccess(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), i320, java.lang.Object(Domino(EOC, i298, i299)))
f3431_0_valeurDomino_FieldAccess(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), i320, java.lang.Object(Domino(EOC, i298, i299))) → f3483_0_valeurDomino_IntArithmetic(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), i320, i298)
f3483_0_valeurDomino_IntArithmetic(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), i320, i298) → f3532_0_valeurDomino_Return(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), +(i320, i298))
f3532_0_valeurDomino_Return(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), i342) → f3610_0_valeurMain_Store(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), i342)
f3610_0_valeurMain_Store(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), i342) → f3642_0_valeurMain_Store(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), i342)
f3642_0_valeurMain_Store(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), i344) → f3734_0_valeurMain_Load(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), i344)
f3734_0_valeurMain_Load(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), i344) → f3771_0_valeurMain_Load(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), i344, i344)
f3771_0_valeurMain_Load(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), i344, i344) → f3800_0_valeurMain_LE(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), i344, i344, i262)
f3800_0_valeurMain_LE(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), i344, i344, i262) → f3833_0_valeurMain_LE(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), i344, i344, i262)
f3800_0_valeurMain_LE(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), i344, i344, i262) → f3834_0_valeurMain_LE(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), i344, i344, i262)
f3833_0_valeurMain_LE(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), i344, i344, i262) → f3893_0_valeurMain_Load(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119))) | <=(i344, i262)
f3893_0_valeurMain_Load(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119))) → f3937_0_valeurMain_Store(EOS, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), i262)
f3937_0_valeurMain_Store(EOS, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), i262) → f3972_0_valeurMain_Store(EOS, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), i262)
f3972_0_valeurMain_Store(EOS, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), i344) → f3989_0_valeurMain_Load(EOS, i344, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)))
f3989_0_valeurMain_Load(EOS, i344, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119))) → f4000_0_valeurMain_FieldAccess(EOS, i344, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)))
f4000_0_valeurMain_FieldAccess(EOS, i344, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119))) → f4010_0_valeurMain_Store(EOS, i344, o1119)
f4010_0_valeurMain_Store(EOS, i344, o1119) → f4024_0_valeurMain_JMP(EOS, i344, o1119)
f4024_0_valeurMain_JMP(EOS, i344, o1119) → f4044_0_valeurMain_Load(EOS, i344, o1119)
f4044_0_valeurMain_Load(EOS, i344, o1119) → f2787_0_valeurMain_Load(EOS, i344, o1119)
f2787_0_valeurMain_Load(EOS, i262, o1052) → f2860_0_valeurMain_NULL(EOS, i262, o1052, o1052)
f3834_0_valeurMain_LE(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), i344, i344, i262) → f3898_0_valeurMain_Load(EOS, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), i344) | >(i344, i262)
f3898_0_valeurMain_Load(EOS, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), i344) → f3940_0_valeurMain_JMP(EOS, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), i344)
f3940_0_valeurMain_JMP(EOS, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), i344) → f3972_0_valeurMain_Store(EOS, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), i344)
f3076_0_valeurDomino_LE(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i298, i299) → f3093_0_valeurDomino_Load(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299))) | >(i298, i299)
f3093_0_valeurDomino_Load(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299))) → f3181_0_valeurDomino_FieldAccess(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)))
f3181_0_valeurDomino_FieldAccess(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299))) → f3252_0_valeurDomino_ConstantStackPush(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i298)
f3252_0_valeurDomino_ConstantStackPush(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i298) → f3330_0_valeurDomino_IntArithmetic(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i298, 10)
f3330_0_valeurDomino_IntArithmetic(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i298, matching1) → f3370_0_valeurDomino_Load(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), *(i298, 10)) | =(matching1, 10)
f3370_0_valeurDomino_Load(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i323) → f3443_0_valeurDomino_FieldAccess(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i323, java.lang.Object(Domino(EOC, i298, i299)))
f3443_0_valeurDomino_FieldAccess(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i323, java.lang.Object(Domino(EOC, i298, i299))) → f3489_0_valeurDomino_IntArithmetic(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i323, i299)
f3489_0_valeurDomino_IntArithmetic(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i323, i299) → f3548_0_valeurDomino_Return(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), +(i323, i299))
f3548_0_valeurDomino_Return(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), java.lang.Object(Domino(EOC, i298, i299)), java.lang.Object(Domino(EOC, i298, i299)), i344) → f3642_0_valeurMain_Store(EOS, i262, java.lang.Object(Liste(o1117sub, java.lang.Object(Domino(EOC, i298, i299)), o1119)), i344)

Combined rules. Obtained 4 IRules

P rules:
f2860_0_valeurMain_NULL(EOS, x0, java.lang.Object(Liste(x1, java.lang.Object(Domino(EOC, x2, x3)), x4)), java.lang.Object(Liste(x1, java.lang.Object(Domino(EOC, x2, x3)), x4))) → f3800_0_valeurMain_LE(EOS, x0, java.lang.Object(Liste(x1, java.lang.Object(Domino(EOC, x2, x3)), x4)), +(*(x3, 10), x2), +(*(x3, 10), x2), x0) | >=(x3, x2)
f3800_0_valeurMain_LE(EOS, x0, java.lang.Object(Liste(x1, java.lang.Object(Domino(EOC, x2, x3)), x4)), x5, x5, x0) → f2860_0_valeurMain_NULL(EOS, x0, x4, x4) | <=(x5, x0)
f3800_0_valeurMain_LE(EOS, x0, java.lang.Object(Liste(x1, java.lang.Object(Domino(EOC, x2, x3)), x4)), x5, x5, x0) → f2860_0_valeurMain_NULL(EOS, x5, x4, x4) | >(x5, x0)
f2860_0_valeurMain_NULL(EOS, x0, java.lang.Object(Liste(x1, java.lang.Object(Domino(EOC, x2, x3)), x4)), java.lang.Object(Liste(x1, java.lang.Object(Domino(EOC, x2, x3)), x4))) → f3800_0_valeurMain_LE(EOS, x0, java.lang.Object(Liste(x1, java.lang.Object(Domino(EOC, x2, x3)), x4)), +(*(x2, 10), x3), +(*(x2, 10), x3), x0) | <(x3, x2)

Filtered ground terms:

f2860_0_valeurMain_NULL(x1, x2, x3, x4) → f2860_0_valeurMain_NULL(x2, x3, x4)
Cond_f2860_0_valeurMain_NULL(x1, x2, x3, x4, x5) → Cond_f2860_0_valeurMain_NULL(x1, x3, x4, x5)
f3800_0_valeurMain_LE(x1, x2, x3, x4, x5, x6) → f3800_0_valeurMain_LE(x2, x3, x4, x5, x6)
Cond_f3800_0_valeurMain_LE(x1, x2, x3, x4, x5, x6, x7) → Cond_f3800_0_valeurMain_LE(x1, x3, x4, x5, x6, x7)
Cond_f3800_0_valeurMain_LE1(x1, x2, x3, x4, x5, x6, x7) → Cond_f3800_0_valeurMain_LE1(x1, x3, x4, x5, x6, x7)
Cond_f2860_0_valeurMain_NULL1(x1, x2, x3, x4, x5) → Cond_f2860_0_valeurMain_NULL1(x1, x3, x4, x5)
Domino(x1, x2, x3) → Domino(x2, x3)

Filtered duplicate terms:

f2860_0_valeurMain_NULL(x1, x2, x3) → f2860_0_valeurMain_NULL(x1, x3)
Cond_f2860_0_valeurMain_NULL(x1, x2, x3, x4) → Cond_f2860_0_valeurMain_NULL(x1, x2, x4)
f3800_0_valeurMain_LE(x1, x2, x3, x4, x5) → f3800_0_valeurMain_LE(x2, x4, x5)
Cond_f3800_0_valeurMain_LE(x1, x2, x3, x4, x5, x6) → Cond_f3800_0_valeurMain_LE(x1, x3, x5, x6)
Cond_f3800_0_valeurMain_LE1(x1, x2, x3, x4, x5, x6) → Cond_f3800_0_valeurMain_LE1(x1, x3, x5, x6)
Cond_f2860_0_valeurMain_NULL1(x1, x2, x3, x4) → Cond_f2860_0_valeurMain_NULL1(x1, x2, x4)

Filtered unneeded terms:

Cond_f3800_0_valeurMain_LE(x1, x2, x3, x4) → Cond_f3800_0_valeurMain_LE(x1, x2, x4)
Liste(x1, x2, x3) → Liste(x2, x3)
Cond_f3800_0_valeurMain_LE1(x1, x2, x3, x4) → Cond_f3800_0_valeurMain_LE1(x1, x2, x3)

Prepared 4 rules for path length conversion:

P rules:
f2860_0_valeurMain_NULL(x0, java.lang.Object(Liste(java.lang.Object(Domino(x2, x3)), x4))) → f3800_0_valeurMain_LE(java.lang.Object(Liste(java.lang.Object(Domino(x2, x3)), x4)), +(*(x3, 10), x2), x0, x2, x3, x4) | >=(x3, x2)
f3800_0_valeurMain_LE(java.lang.Object(Liste(java.lang.Object(Domino(x2, x3)), x4)), x5, x0, x2, x3, x4) → f2860_0_valeurMain_NULL(x0, x4) | <=(x5, x0)
f3800_0_valeurMain_LE(java.lang.Object(Liste(java.lang.Object(Domino(x2, x3)), x4)), x5, x0, x2, x3, x4) → f2860_0_valeurMain_NULL(x5, x4) | >(x5, x0)
f2860_0_valeurMain_NULL(x0, java.lang.Object(Liste(java.lang.Object(Domino(x2, x3)), x4))) → f3800_0_valeurMain_LE(java.lang.Object(Liste(java.lang.Object(Domino(x2, x3)), x4)), +(*(x2, 10), x3), x0, x2, x3, x4) | <(x3, x2)

Finished conversion. Obtained 4 rules.

P rules:
f2860_0_valeurMain_NULL(x0, v26) → f3800_0_valeurMain_LE(v27, +(*(10, x2), x1), x0, x1, x2, v28) | &&(&&(&&(&&(&&(&&(&&(>=(x2, x1), <=(+(x2, 4), v26)), <=(+(x1, 4), v26)), >(+(v28, 1), 0)), <=(+(v28, 2), v26)), >(+(v27, 1), 3)), <=(v27, v26)), >(+(v26, 1), 3))
f3800_0_valeurMain_LE(v29, x7, x8, x4, x5, v30) → f2860_0_valeurMain_NULL(x8, v31) | &&(&&(&&(&&(&&(&&(&&(>=(x8, x7), <=(+(x5, 4), v29)), <=(+(x4, 4), v29)), >(+(v31, 1), 0)), <=(v31, v30)), <=(+(v31, 2), v29)), >(+(v30, 1), 0)), >(+(v29, 1), 3))
f3800_0_valeurMain_LE(v32, x12, x13, x9, x10, v33) → f2860_0_valeurMain_NULL(x12, v34) | &&(&&(&&(&&(&&(&&(&&(<=(+(x9, 4), v32), <(x13, x12)), <=(+(x10, 4), v32)), >(+(v34, 1), 0)), <=(v34, v33)), <=(+(v34, 2), v32)), >(+(v33, 1), 0)), >(+(v32, 1), 3))
f2860_0_valeurMain_NULL(x14, v35) → f3800_0_valeurMain_LE(v36, +(*(10, x15), x16), x14, x15, x16, v37) | &&(&&(&&(&&(&&(&&(&&(<(x16, x15), <=(+(x16, 4), v35)), <=(+(x15, 4), v35)), >(+(v37, 1), 0)), <=(+(v37, 2), v35)), >(+(v36, 1), 3)), <=(v36, v35)), >(+(v35, 1), 3))

(42) Obligation:

Rules:
f2860_0_valeurMain_NULL(x0, v26) → f3800_0_valeurMain_LE(v27, +(*(10, x2), x1), x0, x1, x2, v28) | &&(&&(&&(&&(&&(&&(&&(>=(x2, x1), <=(+(x2, 4), v26)), <=(+(x1, 4), v26)), >(+(v28, 1), 0)), <=(+(v28, 2), v26)), >(+(v27, 1), 3)), <=(v27, v26)), >(+(v26, 1), 3))
f3800_0_valeurMain_LE(v29, x7, x8, x4, x5, v30) → f2860_0_valeurMain_NULL(x8, v31) | &&(&&(&&(&&(&&(&&(&&(>=(x8, x7), <=(+(x5, 4), v29)), <=(+(x4, 4), v29)), >(+(v31, 1), 0)), <=(v31, v30)), <=(+(v31, 2), v29)), >(+(v30, 1), 0)), >(+(v29, 1), 3))
f3800_0_valeurMain_LE(v32, x12, x13, x9, x10, v33) → f2860_0_valeurMain_NULL(x12, v34) | &&(&&(&&(&&(&&(&&(&&(<=(+(x9, 4), v32), <(x13, x12)), <=(+(x10, 4), v32)), >(+(v34, 1), 0)), <=(v34, v33)), <=(+(v34, 2), v32)), >(+(v33, 1), 0)), >(+(v32, 1), 3))
f2860_0_valeurMain_NULL(x14, v35) → f3800_0_valeurMain_LE(v36, +(*(10, x15), x16), x14, x15, x16, v37) | &&(&&(&&(&&(&&(&&(&&(<(x16, x15), <=(+(x16, 4), v35)), <=(+(x15, 4), v35)), >(+(v37, 1), 0)), <=(+(v37, 2), v35)), >(+(v36, 1), 3)), <=(v36, v35)), >(+(v35, 1), 3))

(43) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f2860_0_valeurMain_NULL(x27, x29)] = 1 + x29
[f3800_0_valeurMain_LE(x32, x34, x36, x38, x40, x42)] = x32

Therefore the following rule(s) have been dropped:

f2860_0_valeurMain_NULL(x0, x1) → f3800_0_valeurMain_LE(x2, +(*(10, x3), x4), x0, x4, x3, x5) | &&(&&(&&(&&(&&(&&(&&(>=(x3, x4), <=(+(x3, 4), x1)), <=(+(x4, 4), x1)), >(+(x5, 1), 0)), <=(+(x5, 2), x1)), >(+(x2, 1), 3)), <=(x2, x1)), >(+(x1, 1), 3))
f3800_0_valeurMain_LE(x6, x7, x8, x9, x10, x11) → f2860_0_valeurMain_NULL(x8, x12) | &&(&&(&&(&&(&&(&&(&&(>=(x8, x7), <=(+(x10, 4), x6)), <=(+(x9, 4), x6)), >(+(x12, 1), 0)), <=(x12, x11)), <=(+(x12, 2), x6)), >(+(x11, 1), 0)), >(+(x6, 1), 3))
f3800_0_valeurMain_LE(x13, x14, x15, x16, x17, x18) → f2860_0_valeurMain_NULL(x14, x19) | &&(&&(&&(&&(&&(&&(&&(<=(+(x16, 4), x13), <(x15, x14)), <=(+(x17, 4), x13)), >(+(x19, 1), 0)), <=(x19, x18)), <=(+(x19, 2), x13)), >(+(x18, 1), 0)), >(+(x13, 1), 3))
f2860_0_valeurMain_NULL(x20, x21) → f3800_0_valeurMain_LE(x22, +(*(10, x23), x24), x20, x23, x24, x25) | &&(&&(&&(&&(&&(&&(&&(<(x24, x23), <=(+(x24, 4), x21)), <=(+(x23, 4), x21)), >(+(x25, 1), 0)), <=(+(x25, 2), x21)), >(+(x22, 1), 3)), <=(x22, x21)), >(+(x21, 1), 3))

(44) YES

(45) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Partie.creerPioche()V
SCC calls the following helper methods:
Performed SCC analyses:

Used field analysis yielded the following read fields:
- Partie: [pioche]
Marker field analysis yielded the following relations that could be markers:

(46) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 49 IRules

P rules:
f951_0_creerPioche_ConstantStackPush(EOS, java.lang.Object(Partie(EOC, o166)), java.lang.Object(Partie(EOC, o166)), i56, i56) → f953_0_creerPioche_GE(EOS, java.lang.Object(Partie(EOC, o166)), java.lang.Object(Partie(EOC, o166)), i56, i56, 7)
f953_0_creerPioche_GE(EOS, java.lang.Object(Partie(EOC, o166)), java.lang.Object(Partie(EOC, o166)), i60, i60, matching1) → f954_0_creerPioche_GE(EOS, java.lang.Object(Partie(EOC, o166)), java.lang.Object(Partie(EOC, o166)), i60, i60, 7) | =(matching1, 7)
f954_0_creerPioche_GE(EOS, java.lang.Object(Partie(EOC, o166)), java.lang.Object(Partie(EOC, o166)), i60, i60, matching1) → f956_0_creerPioche_Load(EOS, java.lang.Object(Partie(EOC, o166)), java.lang.Object(Partie(EOC, o166)), i60) | &&(<(i60, 7), =(matching1, 7))
f956_0_creerPioche_Load(EOS, java.lang.Object(Partie(EOC, o166)), java.lang.Object(Partie(EOC, o166)), i60) → f959_0_creerPioche_Store(EOS, java.lang.Object(Partie(EOC, o166)), java.lang.Object(Partie(EOC, o166)), i60, i60)
f959_0_creerPioche_Store(EOS, java.lang.Object(Partie(EOC, o166)), java.lang.Object(Partie(EOC, o166)), i60, i60) → f963_0_creerPioche_Load(EOS, java.lang.Object(Partie(EOC, o166)), java.lang.Object(Partie(EOC, o166)), i60, i60)
f963_0_creerPioche_Load(EOS, java.lang.Object(Partie(EOC, o166)), java.lang.Object(Partie(EOC, o166)), i60, i60) → f1101_0_creerPioche_Load(EOS, java.lang.Object(Partie(EOC, o166)), java.lang.Object(Partie(EOC, o166)), i60, i60)
f1101_0_creerPioche_Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i75) → f1104_0_creerPioche_ConstantStackPush(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i75, i75)
f1104_0_creerPioche_ConstantStackPush(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i75, i75) → f1108_0_creerPioche_GE(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i75, i75, 7)
f1108_0_creerPioche_GE(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, i79, matching1) → f1113_0_creerPioche_GE(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, i79, 7) | =(matching1, 7)
f1108_0_creerPioche_GE(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i80, i80, matching1) → f1114_0_creerPioche_GE(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i80, i80, 7) | =(matching1, 7)
f1113_0_creerPioche_GE(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, i79, matching1) → f1118_0_creerPioche_Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79) | &&(<(i79, 7), =(matching1, 7))
f1118_0_creerPioche_Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79) → f1125_0_creerPioche_New(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)))
f1125_0_creerPioche_New(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190))) → f1133_0_creerPioche_Duplicate(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)))
f1133_0_creerPioche_Duplicate(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC))) → f1154_0_creerPioche_New(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)))
f1154_0_creerPioche_New(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC))) → f1160_0_creerPioche_Duplicate(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)))
f1160_0_creerPioche_Duplicate(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC))) → f1166_0_creerPioche_Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Domino(EOC)))
f1166_0_creerPioche_Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Domino(EOC))) → f1170_0_creerPioche_Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Domino(EOC)), i60)
f1170_0_creerPioche_Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Domino(EOC)), i60) → f1174_0_creerPioche_InvokeMethod(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Domino(EOC)), i60, i79)
f1174_0_creerPioche_InvokeMethod(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Domino(EOC)), i60, i79) → f1178_0__init__Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Domino(EOC)), i60, i79, java.lang.Object(Domino(EOC)), i60, i79)
f1178_0__init__Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Domino(EOC)), i60, i79, java.lang.Object(Domino(EOC)), i60, i79) → f1196_0__init__InvokeMethod(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Domino(EOC)), i60, i79, java.lang.Object(Domino(EOC)), i60, i79, java.lang.Object(Domino(EOC)))
f1196_0__init__InvokeMethod(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Domino(EOC)), i60, i79, java.lang.Object(Domino(EOC)), i60, i79, java.lang.Object(Domino(EOC))) → f1200_0__init__Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Domino(EOC)), i60, i79, java.lang.Object(Domino(EOC)), i60, i79)
f1200_0__init__Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Domino(EOC)), i60, i79, java.lang.Object(Domino(EOC)), i60, i79) → f1203_0__init__Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Domino(EOC)), i60, i79, java.lang.Object(Domino(EOC)), i60, i79, java.lang.Object(Domino(EOC)))
f1203_0__init__Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Domino(EOC)), i60, i79, java.lang.Object(Domino(EOC)), i60, i79, java.lang.Object(Domino(EOC))) → f1206_0__init__FieldAccess(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Domino(EOC)), i60, i79, java.lang.Object(Domino(EOC)), i79, java.lang.Object(Domino(EOC)), i60)
f1206_0__init__FieldAccess(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Domino(EOC)), i60, i79, java.lang.Object(Domino(EOC)), i79, java.lang.Object(Domino(EOC)), i60) → f1209_0__init__Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Domino(EOC)), i60, i79, java.lang.Object(Domino(EOC)), i79)
f1209_0__init__Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Domino(EOC)), i60, i79, java.lang.Object(Domino(EOC)), i79) → f1213_0__init__Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Domino(EOC)), i60, i79, i79, java.lang.Object(Domino(EOC)))
f1213_0__init__Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Domino(EOC)), i60, i79, i79, java.lang.Object(Domino(EOC))) → f1216_0__init__FieldAccess(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Domino(EOC)), i60, i79, java.lang.Object(Domino(EOC)), i79)
f1216_0__init__FieldAccess(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Domino(EOC)), i60, i79, java.lang.Object(Domino(EOC)), i79) → f1222_0__init__Return(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Domino(EOC)), i60, i79)
f1222_0__init__Return(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Domino(EOC)), i60, i79) → f1227_0_creerPioche_Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)))
f1227_0_creerPioche_Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC))) → f1232_0_creerPioche_FieldAccess(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Partie(EOC, o190)))
f1232_0_creerPioche_FieldAccess(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), java.lang.Object(Partie(EOC, o190))) → f1235_0_creerPioche_InvokeMethod(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190)
f1235_0_creerPioche_InvokeMethod(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190) → f1238_0__init__Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190, java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190)
f1238_0__init__Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190, java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190) → f1243_0__init__InvokeMethod(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190, java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190, java.lang.Object(Liste(EOC)))
f1243_0__init__InvokeMethod(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190, java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190, java.lang.Object(Liste(EOC))) → f1247_0__init__Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190, java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190)
f1247_0__init__Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190, java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190) → f1251_0__init__Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190, java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190, java.lang.Object(Liste(EOC)))
f1251_0__init__Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190, java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190, java.lang.Object(Liste(EOC))) → f1258_0__init__FieldAccess(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190, java.lang.Object(Liste(EOC)), o190, java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)))
f1258_0__init__FieldAccess(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190, java.lang.Object(Liste(EOC)), o190, java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC))) → f1262_0__init__Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190, java.lang.Object(Liste(EOC)), o190)
f1262_0__init__Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190, java.lang.Object(Liste(EOC)), o190) → f1266_0__init__Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190, o190, java.lang.Object(Liste(EOC)))
f1266_0__init__Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190, o190, java.lang.Object(Liste(EOC))) → f1270_0__init__FieldAccess(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190, java.lang.Object(Liste(EOC)), o190)
f1270_0__init__FieldAccess(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190, java.lang.Object(Liste(EOC)), o190) → f1274_0__init__Return(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190)
f1274_0__init__Return(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)), java.lang.Object(Liste(EOC)), java.lang.Object(Domino(EOC)), o190) → f1280_0_creerPioche_FieldAccess(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC)))
f1280_0_creerPioche_FieldAccess(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i79, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Liste(EOC))) → f1302_0_creerPioche_Inc(EOS, java.lang.Object(Partie(EOC, java.lang.Object(Liste(EOC)))), java.lang.Object(Partie(EOC, java.lang.Object(Liste(EOC)))), i60, i79)
f1302_0_creerPioche_Inc(EOS, java.lang.Object(Partie(EOC, java.lang.Object(Liste(EOC)))), java.lang.Object(Partie(EOC, java.lang.Object(Liste(EOC)))), i60, i79) → f1308_0_creerPioche_JMP(EOS, java.lang.Object(Partie(EOC, java.lang.Object(Liste(EOC)))), java.lang.Object(Partie(EOC, java.lang.Object(Liste(EOC)))), i60, +(i79, 1)) | >=(i79, 0)
f1308_0_creerPioche_JMP(EOS, java.lang.Object(Partie(EOC, java.lang.Object(Liste(EOC)))), java.lang.Object(Partie(EOC, java.lang.Object(Liste(EOC)))), i60, i93) → f1319_0_creerPioche_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(Liste(EOC)))), java.lang.Object(Partie(EOC, java.lang.Object(Liste(EOC)))), i60, i93)
f1319_0_creerPioche_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(Liste(EOC)))), java.lang.Object(Partie(EOC, java.lang.Object(Liste(EOC)))), i60, i93) → f1101_0_creerPioche_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(Liste(EOC)))), java.lang.Object(Partie(EOC, java.lang.Object(Liste(EOC)))), i60, i93)
f1114_0_creerPioche_GE(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60, i80, i80, matching1) → f1122_0_creerPioche_Inc(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60) | &&(>=(i80, 7), =(matching1, 7))
f1122_0_creerPioche_Inc(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i60) → f1129_0_creerPioche_JMP(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), +(i60, 1)) | >=(i60, 0)
f1129_0_creerPioche_JMP(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i83) → f1149_0_creerPioche_Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i83)
f1149_0_creerPioche_Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i83) → f949_0_creerPioche_Load(EOS, java.lang.Object(Partie(EOC, o190)), java.lang.Object(Partie(EOC, o190)), i83)
f949_0_creerPioche_Load(EOS, java.lang.Object(Partie(EOC, o166)), java.lang.Object(Partie(EOC, o166)), i56) → f951_0_creerPioche_ConstantStackPush(EOS, java.lang.Object(Partie(EOC, o166)), java.lang.Object(Partie(EOC, o166)), i56, i56)

Combined rules. Obtained 2 IRules

P rules:
f1108_0_creerPioche_GE(EOS, java.lang.Object(Partie(EOC, x0)), java.lang.Object(Partie(EOC, x0)), x1, x2, x2, 7) → f1108_0_creerPioche_GE(EOS, java.lang.Object(Partie(EOC, java.lang.Object(Liste(EOC)))), java.lang.Object(Partie(EOC, java.lang.Object(Liste(EOC)))), x1, +(x2, 1), +(x2, 1), 7) | &&(<(x2, 7), >(+(x2, 1), 0))
f1108_0_creerPioche_GE(EOS, java.lang.Object(Partie(EOC, x0)), java.lang.Object(Partie(EOC, x0)), x1, x2, x2, 7) → f1108_0_creerPioche_GE(EOS, java.lang.Object(Partie(EOC, x0)), java.lang.Object(Partie(EOC, x0)), +(x1, 1), +(x1, 1), +(x1, 1), 7) | &&(&&(>(+(x2, 1), 7), <(x1, 6)), >(+(x1, 1), 0))

Filtered ground terms:

f1108_0_creerPioche_GE(x1, x2, x3, x4, x5, x6, x7) → f1108_0_creerPioche_GE(x2, x3, x4, x5, x6)
Cond_f1108_0_creerPioche_GE(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1108_0_creerPioche_GE(x1, x3, x4, x5, x6, x7)
Cond_f1108_0_creerPioche_GE1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1108_0_creerPioche_GE1(x1, x3, x4, x5, x6, x7)
Partie(x1, x2) → Partie(x2)
Liste(x1) → Liste

Filtered duplicate terms:

f1108_0_creerPioche_GE(x1, x2, x3, x4, x5) → f1108_0_creerPioche_GE(x2, x3, x5)
Cond_f1108_0_creerPioche_GE(x1, x2, x3, x4, x5, x6) → Cond_f1108_0_creerPioche_GE(x1, x3, x4, x6)
Cond_f1108_0_creerPioche_GE1(x1, x2, x3, x4, x5, x6) → Cond_f1108_0_creerPioche_GE1(x1, x3, x4, x6)

Filtered unneeded terms:

Cond_f1108_0_creerPioche_GE(x1, x2, x3, x4) → Cond_f1108_0_creerPioche_GE(x1, x3, x4)
Cond_f1108_0_creerPioche_GE1(x1, x2, x3, x4) → Cond_f1108_0_creerPioche_GE1(x1, x3)

Prepared 2 rules for path length conversion:

P rules:
f1108_0_creerPioche_GE(java.lang.Object(Partie(x0)), x1, x2) → f1108_0_creerPioche_GE(java.lang.Object(Partie(java.lang.Object(Liste))), x1, +(x2, 1)) | &&(<(x2, 7), >(+(x2, 1), 0))
f1108_0_creerPioche_GE(java.lang.Object(Partie(x0)), x1, x2) → f1108_0_creerPioche_GE(java.lang.Object(Partie(x0)), +(x1, 1), +(x1, 1)) | &&(&&(>(+(x2, 1), 7), <(x1, 6)), >(+(x1, 1), 0))

Finished conversion. Obtained 2 rules.

P rules:
f1108_0_creerPioche_GE(v9, x1, x2) → f1108_0_creerPioche_GE(v10, x1, +(x2, 1)) | &&(&&(&&(&&(>(x2, -1), <(x2, 7)), >=(v9, -(v10, 2))), >(+(v9, 1), 1)), >(+(v10, 1), 3))
f1108_0_creerPioche_GE(v11, x4, x5) → f1108_0_creerPioche_GE(v12, +(x4, 1), +(x4, 1)) | &&(&&(&&(&&(&&(>(x5, 6), >(x4, -1)), <(x4, 6)), >(+(v12, 1), 1)), <=(v12, v11)), >(+(v11, 1), 1))

(47) Obligation:

Rules:
f1108_0_creerPioche_GE(v9, x1, x2) → f1108_0_creerPioche_GE(v10, x1, +(x2, 1)) | &&(&&(&&(&&(>(x2, -1), <(x2, 7)), >=(v9, -(v10, 2))), >(+(v9, 1), 1)), >(+(v10, 1), 3))
f1108_0_creerPioche_GE(v11, x4, x5) → f1108_0_creerPioche_GE(v12, +(x4, 1), +(x4, 1)) | &&(&&(&&(&&(&&(>(x5, 6), >(x4, -1)), <(x4, 6)), >(+(v12, 1), 1)), <=(v12, v11)), >(+(v11, 1), 1))

(48) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:

[f1108_0_creerPioche_GE(x9, x11, x13)] = 5 - x11

Therefore the following rule(s) have been dropped:

f1108_0_creerPioche_GE(x4, x5, x6) → f1108_0_creerPioche_GE(x7, +(x5, 1), +(x5, 1)) | &&(&&(&&(&&(&&(>(x6, 6), >(x5, -1)), <(x5, 6)), >(+(x7, 1), 1)), <=(x7, x4)), >(+(x4, 1), 1))

(49) Obligation:

Rules:
f1108_0_creerPioche_GE(x0, x1, x2) → f1108_0_creerPioche_GE(x3, x1, +(x2, 1)) | &&(&&(&&(&&(>(x2, -1), <(x2, 7)), >=(x0, -(x3, 2))), >(+(x0, 1), 1)), >(+(x3, 1), 3))

(50) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f1108_0_creerPioche_GE(x5, x7, x9)] = 6 - x9

Therefore the following rule(s) have been dropped:

f1108_0_creerPioche_GE(x0, x1, x2) → f1108_0_creerPioche_GE(x3, x1, +(x2, 1)) | &&(&&(&&(&&(>(x2, -1), <(x2, 7)), >=(x0, -(x3, 2))), >(+(x0, 1), 1)), >(+(x3, 1), 3))

(51) YES

(52) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Partie.main([Ljava/lang/String;)V
SCC calls the following helper methods: Partie.creerMain(II)V, Partie.lister(LListe;)V, Partie.longueur(LListe;)I, Partie.nieme(LListe;I)LDomino;
Performed SCC analyses:

Used field analysis yielded the following read fields:
- Partie: [mains]
Marker field analysis yielded the following relations that could be markers:

(53) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 38 IRules

P rules:
f2557_0__init__Load(EOS, java.lang.Object(ARRAY(i232)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, i233, i233) → f2562_0__init__GE(EOS, java.lang.Object(ARRAY(i232)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, i233, i233, i232)
f2562_0__init__GE(EOS, java.lang.Object(ARRAY(i232)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, i233, i233, i232) → f2569_0__init__GE(EOS, java.lang.Object(ARRAY(i232)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, i233, i233, i232)
f2569_0__init__GE(EOS, java.lang.Object(ARRAY(i232)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, i233, i233, i232) → f2583_0__init__Load(EOS, java.lang.Object(ARRAY(i232)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, i233) | <(i233, i232)
f2583_0__init__Load(EOS, java.lang.Object(ARRAY(i232)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, i233) → f2601_0__init__Load(EOS, java.lang.Object(ARRAY(i232)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, i233, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))))
f2601_0__init__Load(EOS, java.lang.Object(ARRAY(i232)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, i233, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231))))) → f2638_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i232)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, i233, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i233)
f2638_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i232)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, i233, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i233) → f2645_0__init__Load(EOS, java.lang.Object(ARRAY(i232)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, i233, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i233, java.lang.Object(ARRAY(5)))
f2645_0__init__Load(EOS, java.lang.Object(ARRAY(i232)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, i233, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i233, java.lang.Object(ARRAY(matching1))) → f2651_0__init__ArrayAccess(EOS, java.lang.Object(ARRAY(i232)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, i233, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i233, java.lang.Object(ARRAY(5)), i232) | =(matching1, 5)
f2651_0__init__ArrayAccess(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i255, i233, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i233, java.lang.Object(ARRAY(matching1)), i255) → f2688_0__init__ArrayAccess(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i255, i233, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i233, java.lang.Object(ARRAY(5)), i255) | =(matching1, 5)
f2688_0__init__ArrayAccess(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i255, i233, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i233, java.lang.Object(ARRAY(matching1)), i255) → f2699_0__init__InvokeMethod(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i255, i233, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i233, i257) | &&(<(i255, 5), =(matching1, 5))
f2699_0__init__InvokeMethod(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i255, i233, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i233, i257) → f2732_0_creerMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i233, i257, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i233, i257)
f2699_0__init__InvokeMethod(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i255, i233, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i233, i257) → f2732_1_creerMain_Load(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i255, i233, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i233, i257, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i233, i257)
f2732_0_creerMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i233, i257, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i233, i257) → f2751_0_creerMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i233, i257, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i233, i257)
f2869_0_creerMain_Return(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, i276) → f2891_0__init__Load(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274)
f2891_0__init__Load(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274) → f2908_0__init__Load(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))))
f2908_0__init__Load(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272))))) → f2929_0__init__InvokeMethod(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274)
f2929_0__init__InvokeMethod(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274) → f2947_0_imprimeMain_Load(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274)
f2947_0_imprimeMain_Load(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274) → f2971_0_imprimeMain_FieldAccess(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))))
f2971_0_imprimeMain_FieldAccess(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272))))) → f2985_0_imprimeMain_Load(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, i274, java.lang.Object(ARRAY(i272)))
f2985_0_imprimeMain_Load(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, i274, java.lang.Object(ARRAY(i272))) → f3001_0_imprimeMain_ArrayAccess(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, java.lang.Object(ARRAY(i272)), i274)
f3001_0_imprimeMain_ArrayAccess(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, java.lang.Object(ARRAY(i272)), i274) → f3015_0_imprimeMain_ArrayAccess(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, java.lang.Object(ARRAY(i272)), i274)
f3015_0_imprimeMain_ArrayAccess(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, java.lang.Object(ARRAY(i272)), i274) → f3033_0_imprimeMain_InvokeMethod(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, o1146) | <(i274, i272)
f3033_0_imprimeMain_InvokeMethod(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, o1146) → f3051_0_lister_Load(EOS, o1146, o1146)
f3033_0_imprimeMain_InvokeMethod(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, o1146) → f3051_1_lister_Load(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, o1146, o1146)
f3051_0_lister_Load(EOS, o1146, o1146) → f3070_0_lister_Load(EOS, o1146, o1146)
f3179_0_lister_Return(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, NULL, NULL) → f3266_0_imprimeMain_Return(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274)
f3266_0_imprimeMain_Return(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274) → f3316_0_imprimeMain_Return(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274)
f3316_0_imprimeMain_Return(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274) → f3359_0__init__Inc(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274)
f3359_0__init__Inc(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274) → f3393_0__init__JMP(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, +(i274, 1)) | >=(i274, 0)
f3393_0__init__JMP(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i328) → f3472_0__init__Load(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i328)
f3472_0__init__Load(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i328) → f2548_0__init__Load(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i328)
f2548_0__init__Load(EOS, java.lang.Object(ARRAY(i232)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, i233) → f2557_0__init__Load(EOS, java.lang.Object(ARRAY(i232)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i232, i233, i233)
f3197_0_lister_Return(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, java.lang.Object(Liste(o1179sub))) → f3231_0_lister_Return(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, java.lang.Object(Liste(o1179sub)))
f3231_0_lister_Return(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, java.lang.Object(Liste(o1233sub))) → f3316_0_imprimeMain_Return(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274)
f3230_0_lister_Return(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, java.lang.Object(Liste(o1189sub))) → f3231_0_lister_Return(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, java.lang.Object(Liste(o1189sub)))
f2732_1_creerMain_Load(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i274, i276, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i231)))), i274, i276) → f2869_0_creerMain_Return(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, i276)
f3051_1_lister_Load(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, NULL, NULL) → f3179_0_lister_Return(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, NULL, NULL)
f3051_1_lister_Load(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, java.lang.Object(Liste(o1179sub)), java.lang.Object(Liste(o1179sub))) → f3197_0_lister_Return(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, java.lang.Object(Liste(o1179sub)))
f3051_1_lister_Load(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, java.lang.Object(Liste(o1189sub)), java.lang.Object(Liste(o1189sub))) → f3230_0_lister_Return(EOS, java.lang.Object(ARRAY(i255)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i255, i274, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(i272)))), i274, java.lang.Object(Liste(o1189sub)))

Combined rules. Obtained 3 IRules

P rules:
f2557_0__init__Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x1)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x1)))), x0, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x1)))), x0, x2, x2) → f2751_0_creerMain_Load(EOS, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x1)))), x2, x3, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x1)))), x2, x3) | &&(<(x0, 5), <(x2, x0))
f2557_0__init__Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x1)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x1)))), x0, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x1)))), x0, x2, x2) → f3070_0_lister_Load(EOS, x3, x3) | &&(<(x0, 5), <(x2, x0))
f2557_0__init__Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x1)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x1)))), x0, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x1)))), x0, x2, x2) → f2557_0__init__Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x3)))), java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x3)))), x0, java.lang.Object(Partie(EOC, java.lang.Object(ARRAY(x3)))), x0, +(x2, 1), +(x2, 1)) | &&(&&(&&(>(x3, x2), >(+(x2, 1), 0)), <(x0, 5)), <(x2, x0))

Filtered ground terms:

f2557_0__init__Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → f2557_0__init__Load(x2, x3, x4, x5, x6, x7, x8, x9)
Cond_f2557_0__init__Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) → Cond_f2557_0__init__Load(x1, x3, x4, x5, x6, x7, x8, x9, x10, x11)
f2751_0_creerMain_Load(x1, x2, x3, x4, x5, x6, x7) → f2751_0_creerMain_Load(x2, x3, x4, x5, x6, x7)
Cond_f2557_0__init__Load1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) → Cond_f2557_0__init__Load1(x1, x3, x4, x5, x6, x7, x8, x9, x10, x11)
f3070_0_lister_Load(x1, x2, x3) → f3070_0_lister_Load(x2, x3)
Cond_f2557_0__init__Load2(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) → Cond_f2557_0__init__Load2(x1, x3, x4, x5, x6, x7, x8, x9, x10, x11)
Partie(x1, x2) → Partie(x2)

Filtered duplicate terms:

f2557_0__init__Load(x1, x2, x3, x4, x5, x6, x7, x8) → f2557_0__init__Load(x1, x5, x8)
Cond_f2557_0__init__Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_f2557_0__init__Load(x1, x2, x6, x9, x10)
f2751_0_creerMain_Load(x1, x2, x3, x4, x5, x6) → f2751_0_creerMain_Load(x4, x5, x6)
Cond_f2557_0__init__Load1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_f2557_0__init__Load1(x1, x2, x6, x9, x10)
f3070_0_lister_Load(x1, x2) → f3070_0_lister_Load(x2)
Cond_f2557_0__init__Load2(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_f2557_0__init__Load2(x1, x2, x6, x9, x10)

Filtered unneeded terms:

Cond_f2557_0__init__Load(x1, x2, x3, x4, x5) → Cond_f2557_0__init__Load(x1)
Cond_f2557_0__init__Load1(x1, x2, x3, x4, x5) → Cond_f2557_0__init__Load1(x1)
Cond_f2557_0__init__Load2(x1, x2, x3, x4, x5) → Cond_f2557_0__init__Load2(x1, x2, x4)
f2557_0__init__Load(x1, x2, x3) → f2557_0__init__Load(x1, x3)

Prepared 3 rules for path length conversion:

P rules:
f2557_0__init__Load(java.lang.Object(ARRAY(x0)), x2, x0) → f2751_0_creerMain_Load(java.lang.Object(Partie(java.lang.Object(ARRAY(x1)))), x2, x3) | &&(<(x0, 5), <(x2, x0))
f2557_0__init__Load(java.lang.Object(ARRAY(x0)), x2, x0) → f3070_0_lister_Load(x3) | &&(<(x0, 5), <(x2, x0))
f2557_0__init__Load(java.lang.Object(ARRAY(x0)), x2, x0) → f2557_0__init__Load(java.lang.Object(ARRAY(x0)), +(x2, 1), x0) | &&(&&(&&(>(x3, x2), >(+(x2, 1), 0)), <(x0, 5)), <(x2, x0))

Finished conversion. Obtained 1 rules.

P rules:
f2557_0__init__Load(v13, x8, x7) → f2557_0__init__Load(v14, +(x8, 1), x7) | &&(&&(&&(&&(&&(&&(>(x9, x8), >(x8, -1)), <(x8, x7)), <(x7, 5)), >(+(v14, 1), 1)), <=(v14, v13)), >(+(v13, 1), 1))

(54) Obligation:

Rules:
f2557_0__init__Load(v13, x8, x7) → f2557_0__init__Load(v14, +(x8, 1), x7) | &&(&&(&&(&&(&&(&&(>(x9, x8), >(x8, -1)), <(x8, x7)), <(x7, 5)), >(+(v14, 1), 1)), <=(v14, v13)), >(+(v13, 1), 1))

(55) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f2557_0__init__Load(x6, x8, x10)] = 3 - x8

Therefore the following rule(s) have been dropped:

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

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIntTRSProof (SOUND transformation)

(7) Obligation:

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

(9) YES

(10) Obligation:

(11) SCCToIntTRSProof (SOUND transformation)

(12) Obligation:

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

(14) YES

(15) Obligation:

(16) SCCToIntTRSProof (SOUND transformation)

(17) Obligation:

(18) PolynomialOrderProcessor (EQUIVALENT transformation)

(19) YES

(20) Obligation:

(21) SCCToIntTRSProof (SOUND transformation)

(22) Obligation:

(23) PolynomialOrderProcessor (EQUIVALENT transformation)

(24) YES

(25) Obligation:

(26) SCCToIntTRSProof (SOUND transformation)

(27) Obligation:

(28) PolynomialOrderProcessor (EQUIVALENT transformation)

(29) YES

(30) Obligation:

(31) SCCToIntTRSProof (SOUND transformation)

(32) Obligation:

(33) LinearRankingProcessor (EQUIVALENT transformation)

(34) YES

(35) Obligation:

(36) SCCToIntTRSProof (SOUND transformation)

(37) Obligation:

(38) PolynomialOrderProcessor (EQUIVALENT transformation)

(39) YES

(40) Obligation:

(41) SCCToIntTRSProof (SOUND transformation)

(42) Obligation:

(43) PolynomialOrderProcessor (EQUIVALENT transformation)

(44) YES

(45) Obligation:

(46) SCCToIntTRSProof (SOUND transformation)

(47) Obligation:

(48) PolynomialOrderProcessor (SOUND transformation)

(49) Obligation:

(50) PolynomialOrderProcessor (EQUIVALENT transformation)

(51) YES

(52) Obligation:

(53) SCCToIntTRSProof (SOUND transformation)

(54) Obligation:

(55) PolynomialOrderProcessor (EQUIVALENT transformation)

(56) YES