(0) Obligation:

JBC Problem based on JBC Program:
package AlternatingGrowReduce;

public class AlternatingGrowReduce {
AlternatingGrowReduce next;

public static void main(String[] argv) {
Random.args = argv;
AlternatingGrowReduce list = createList(Random.random());

int mode = 0;
while (list != null) {
if (mode == 0) {
list = list.next.next.next.next;
} else if (mode == 1) {
list = new AlternatingGrowReduce(list);
} else if (mode > 1) {
list = new AlternatingGrowReduce(new AlternatingGrowReduce(list));
}

mode++;
if (mode > 2) {
mode = 0;
}
}
}

public AlternatingGrowReduce(AlternatingGrowReduce old) {
this.next = old;
}

public static AlternatingGrowReduce createList(int length) {
AlternatingGrowReduce res = new AlternatingGrowReduce(null);
while (length > 0) {
res = new AlternatingGrowReduce(res);
length--;
}
return res;
}
}


package AlternatingGrowReduce;

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

public static int random() {
String string = args[index];
index++;
return string.length();
}
}


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

AlternatingGrowReduce.AlternatingGrowReduce.createList(I)LAlternatingGrowReduce/AlternatingGrowReduce;: Graph of 33 nodes with 1 SCC.


(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 2 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: AlternatingGrowReduce.AlternatingGrowReduce.createList(I)LAlternatingGrowReduce/AlternatingGrowReduce;
SCC calls the following helper methods:
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
  • Marker field analysis yielded the following relations that could be markers:

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 17 IRules

P rules:
f348_0_createList_LE(EOS, i38, i38) → f354_0_createList_LE(EOS, i38, i38)
f354_0_createList_LE(EOS, i38, i38) → f363_0_createList_New(EOS, i38) | >(i38, 0)
f363_0_createList_New(EOS, i38) → f370_0_createList_Duplicate(EOS, i38)
f370_0_createList_Duplicate(EOS, i38) → f377_0_createList_Load(EOS, i38)
f377_0_createList_Load(EOS, i38) → f389_0_createList_InvokeMethod(EOS, i38)
f389_0_createList_InvokeMethod(EOS, i38) → f404_0__init__Load(EOS, i38)
f404_0__init__Load(EOS, i38) → f409_0__init__InvokeMethod(EOS, i38)
f409_0__init__InvokeMethod(EOS, i38) → f415_0__init__Load(EOS, i38)
f415_0__init__Load(EOS, i38) → f420_0__init__Load(EOS, i38)
f420_0__init__Load(EOS, i38) → f425_0__init__FieldAccess(EOS, i38)
f425_0__init__FieldAccess(EOS, i38) → f433_0__init__Return(EOS, i38)
f433_0__init__Return(EOS, i38) → f437_0_createList_Store(EOS, i38)
f437_0_createList_Store(EOS, i38) → f440_0_createList_Inc(EOS, i38)
f440_0_createList_Inc(EOS, i38) → f445_0_createList_JMP(EOS, +(i38, -1)) | >(i38, 0)
f445_0_createList_JMP(EOS, i51) → f452_0_createList_Load(EOS, i51)
f452_0_createList_Load(EOS, i51) → f340_0_createList_Load(EOS, i51)
f340_0_createList_Load(EOS, i31) → f348_0_createList_LE(EOS, i31, i31)

Combined rules. Obtained 1 IRules

P rules:
f348_0_createList_LE(EOS, x0, x0) → f348_0_createList_LE(EOS, -(x0, 1), -(x0, 1)) | >(x0, 0)

Filtered ground terms:


f348_0_createList_LE(x1, x2, x3) → f348_0_createList_LE(x2, x3)
Cond_f348_0_createList_LE(x1, x2, x3, x4) → Cond_f348_0_createList_LE(x1, x3, x4)

Filtered duplicate terms:


f348_0_createList_LE(x1, x2) → f348_0_createList_LE(x2)
Cond_f348_0_createList_LE(x1, x2, x3) → Cond_f348_0_createList_LE(x1, x3)

Prepared 1 rules for path length conversion:

P rules:
f348_0_createList_LE(x0) → f348_0_createList_LE(-(x0, 1)) | >(x0, 0)

Finished conversion. Obtained 1 rules.

P rules:
f348_0_createList_LE(x0) → f348_0_createList_LE(-(x0, 1)) | >(x0, 0)

(7) Obligation:

Rules:
f348_0_createList_LE(x0) → f348_0_createList_LE(-(x0, 1)) | >(x0, 0)

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f348_0_createList_LE(x2)] = x2

Therefore the following rule(s) have been dropped:


f348_0_createList_LE(x0) → f348_0_createList_LE(-(x0, 1)) | >(x0, 0)

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: AlternatingGrowReduce.AlternatingGrowReduce.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
    • AlternatingGrowReduce.AlternatingGrowReduce: [next]
  • Marker field analysis yielded the following relations that could be markers:

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 81 IRules

P rules:
f805_0_main_NULL(EOS, java.lang.Object(o222sub), i84, java.lang.Object(o222sub)) → f807_0_main_NULL(EOS, java.lang.Object(o222sub), i84, java.lang.Object(o222sub))
f807_0_main_NULL(EOS, java.lang.Object(o222sub), i84, java.lang.Object(o222sub)) → f809_0_main_Load(EOS, java.lang.Object(o222sub), i84)
f809_0_main_Load(EOS, java.lang.Object(o222sub), i84) → f813_0_main_NE(EOS, java.lang.Object(o222sub), i84, i84)
f813_0_main_NE(EOS, java.lang.Object(o222sub), i87, i87) → f817_0_main_NE(EOS, java.lang.Object(o222sub), i87, i87)
f813_0_main_NE(EOS, java.lang.Object(o222sub), matching1, matching2) → f819_0_main_NE(EOS, java.lang.Object(o222sub), 0, 0) | &&(=(matching1, 0), =(matching2, 0))
f817_0_main_NE(EOS, java.lang.Object(o222sub), i87, i87) → f821_0_main_Load(EOS, java.lang.Object(o222sub), i87) | >(i87, 0)
f821_0_main_Load(EOS, java.lang.Object(o222sub), i87) → f825_0_main_ConstantStackPush(EOS, java.lang.Object(o222sub), i87, i87)
f825_0_main_ConstantStackPush(EOS, java.lang.Object(o222sub), i87, i87) → f830_0_main_NE(EOS, java.lang.Object(o222sub), i87, i87, 1)
f830_0_main_NE(EOS, java.lang.Object(o222sub), matching1, matching2, matching3) → f835_0_main_NE(EOS, java.lang.Object(o222sub), 1, 1, 1) | &&(&&(&&(=(i87, 1), =(matching1, 1)), =(matching2, 1)), =(matching3, 1))
f830_0_main_NE(EOS, java.lang.Object(o222sub), matching1, matching2, matching3) → f836_0_main_NE(EOS, java.lang.Object(o222sub), 2, 2, 1) | &&(&&(&&(=(i87, 2), =(matching1, 2)), =(matching2, 2)), =(matching3, 1))
f835_0_main_NE(EOS, java.lang.Object(o222sub), matching1, matching2, matching3) → f840_0_main_New(EOS, java.lang.Object(o222sub), 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
f840_0_main_New(EOS, java.lang.Object(o222sub), matching1) → f848_0_main_Duplicate(EOS, java.lang.Object(o222sub), 1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL))) | =(matching1, 1)
f848_0_main_Duplicate(EOS, java.lang.Object(o222sub), matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL))) → f853_0_main_Load(EOS, java.lang.Object(o222sub), 1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL))) | =(matching1, 1)
f853_0_main_Load(EOS, java.lang.Object(o222sub), matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL))) → f861_0_main_InvokeMethod(EOS, 1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub)) | =(matching1, 1)
f861_0_main_InvokeMethod(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub)) → f869_0__init__Load(EOS, 1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub)) | =(matching1, 1)
f869_0__init__Load(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub)) → f887_0__init__InvokeMethod(EOS, 1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL))) | =(matching1, 1)
f887_0__init__InvokeMethod(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL))) → f895_0__init__Load(EOS, 1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub)) | =(matching1, 1)
f895_0__init__Load(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub)) → f909_0__init__Load(EOS, 1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub), java.lang.Object(o222sub), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL))) | =(matching1, 1)
f909_0__init__Load(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub), java.lang.Object(o222sub), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL))) → f919_0__init__FieldAccess(EOS, 1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub)) | =(matching1, 1)
f919_0__init__FieldAccess(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub)) → f928_0__init__Return(EOS, 1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), java.lang.Object(o222sub)) | =(matching1, 1)
f928_0__init__Return(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), java.lang.Object(o222sub)) → f949_0_main_Store(EOS, 1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub)))) | =(matching1, 1)
f949_0_main_Store(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub)))) → f965_0_main_JMP(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), 1) | =(matching1, 1)
f965_0_main_JMP(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), matching1) → f975_0_main_Inc(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), 1) | =(matching1, 1)
f975_0_main_Inc(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), matching1) → f1001_0_main_Load(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), 2) | =(matching1, 1)
f1001_0_main_Load(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), matching1) → f1021_0_main_ConstantStackPush(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), 2, 2) | =(matching1, 2)
f1021_0_main_ConstantStackPush(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), matching1, matching2) → f1033_0_main_LE(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), 2, 2, 2) | &&(=(matching1, 2), =(matching2, 2))
f1033_0_main_LE(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), matching1, matching2, matching3) → f1055_0_main_Load(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), 2) | &&(&&(=(matching1, 2), =(matching2, 2)), =(matching3, 2))
f1055_0_main_Load(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), matching1) → f795_0_main_Load(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), 2) | =(matching1, 2)
f795_0_main_Load(EOS, o215, i84) → f805_0_main_NULL(EOS, o215, i84, o215)
f836_0_main_NE(EOS, java.lang.Object(o222sub), matching1, matching2, matching3) → f842_0_main_Load(EOS, java.lang.Object(o222sub), 2) | &&(&&(=(matching1, 2), =(matching2, 2)), =(matching3, 1))
f842_0_main_Load(EOS, java.lang.Object(o222sub), matching1) → f849_0_main_ConstantStackPush(EOS, java.lang.Object(o222sub), 2, 2) | =(matching1, 2)
f849_0_main_ConstantStackPush(EOS, java.lang.Object(o222sub), matching1, matching2) → f855_0_main_LE(EOS, java.lang.Object(o222sub), 2, 2, 1) | &&(=(matching1, 2), =(matching2, 2))
f855_0_main_LE(EOS, java.lang.Object(o222sub), matching1, matching2, matching3) → f863_0_main_New(EOS, java.lang.Object(o222sub), 2) | &&(&&(=(matching1, 2), =(matching2, 2)), =(matching3, 1))
f863_0_main_New(EOS, java.lang.Object(o222sub), matching1) → f870_0_main_Duplicate(EOS, java.lang.Object(o222sub), 2, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL))) | =(matching1, 2)
f870_0_main_Duplicate(EOS, java.lang.Object(o222sub), matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL))) → f879_0_main_New(EOS, java.lang.Object(o222sub), 2, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL))) | =(matching1, 2)
f879_0_main_New(EOS, java.lang.Object(o222sub), matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL))) → f890_0_main_Duplicate(EOS, java.lang.Object(o222sub), 2, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL))) | =(matching1, 2)
f890_0_main_Duplicate(EOS, java.lang.Object(o222sub), matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL))) → f897_0_main_Load(EOS, java.lang.Object(o222sub), 2, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL))) | =(matching1, 2)
f897_0_main_Load(EOS, java.lang.Object(o222sub), matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL))) → f910_0_main_InvokeMethod(EOS, 2, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub)) | =(matching1, 2)
f910_0_main_InvokeMethod(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub)) → f921_0__init__Load(EOS, 2, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub)) | =(matching1, 2)
f921_0__init__Load(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub)) → f954_0__init__InvokeMethod(EOS, 2, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL))) | =(matching1, 2)
f954_0__init__InvokeMethod(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL))) → f969_0__init__Load(EOS, 2, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub)) | =(matching1, 2)
f969_0__init__Load(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub)) → f976_0__init__Load(EOS, 2, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub), java.lang.Object(o222sub), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL))) | =(matching1, 2)
f976_0__init__Load(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub), java.lang.Object(o222sub), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL))) → f1006_0__init__FieldAccess(EOS, 2, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub)) | =(matching1, 2)
f1006_0__init__FieldAccess(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(o222sub)) → f1026_0__init__Return(EOS, 2, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), java.lang.Object(o222sub)) | =(matching1, 2)
f1026_0__init__Return(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), java.lang.Object(o222sub)) → f1035_0_main_InvokeMethod(EOS, 2, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub)))) | =(matching1, 2)
f1035_0_main_InvokeMethod(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub)))) → f1056_0__init__Load(EOS, 2, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub)))) | =(matching1, 2)
f1056_0__init__Load(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub)))) → f1080_0__init__InvokeMethod(EOS, 2, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL))) | =(matching1, 2)
f1080_0__init__InvokeMethod(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL))) → f1100_0__init__Load(EOS, 2, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub)))) | =(matching1, 2)
f1100_0__init__Load(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub)))) → f1120_0__init__Load(EOS, 2, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL))) | =(matching1, 2)
f1120_0__init__Load(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL))) → f1138_0__init__FieldAccess(EOS, 2, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub)))) | =(matching1, 2)
f1138_0__init__FieldAccess(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, NULL)), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub)))) → f1159_0__init__Return(EOS, 2, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))))), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))))), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub)))) | =(matching1, 2)
f1159_0__init__Return(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))))), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))))), java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub)))) → f1178_0_main_Store(EOS, 2, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub)))))) | =(matching1, 2)
f1178_0_main_Store(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub)))))) → f1195_0_main_Inc(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))))), 2) | =(matching1, 2)
f1195_0_main_Inc(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))))), matching1) → f1210_0_main_Load(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub)))))) | =(matching1, 2)
f1210_0_main_Load(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub)))))) → f1224_0_main_ConstantStackPush(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))))))
f1224_0_main_ConstantStackPush(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub)))))) → f1234_0_main_LE(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))))))
f1234_0_main_LE(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub)))))) → f1244_0_main_ConstantStackPush(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))))))
f1244_0_main_ConstantStackPush(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub)))))) → f1250_0_main_Store(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))))), 0)
f1250_0_main_Store(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))))), matching1) → f1254_0_main_JMP(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))))), 0) | =(matching1, 0)
f1254_0_main_JMP(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))))), matching1) → f1263_0_main_Load(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))))), 0) | =(matching1, 0)
f1263_0_main_Load(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))))), matching1) → f795_0_main_Load(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(o222sub))))), 0) | =(matching1, 0)
f819_0_main_NE(EOS, java.lang.Object(o222sub), matching1, matching2) → f823_0_main_Load(EOS, java.lang.Object(o222sub), 0) | &&(=(matching1, 0), =(matching2, 0))
f823_0_main_Load(EOS, java.lang.Object(o222sub), matching1) → f827_0_main_FieldAccess(EOS, 0, java.lang.Object(o222sub)) | =(matching1, 0)
f827_0_main_FieldAccess(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, o227))) → f832_0_main_FieldAccess(EOS, 0, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, o227))) | =(matching1, 0)
f832_0_main_FieldAccess(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, o227))) → f838_0_main_FieldAccess(EOS, 0, o227) | =(matching1, 0)
f838_0_main_FieldAccess(EOS, matching1, java.lang.Object(o229sub)) → f845_0_main_FieldAccess(EOS, 0, java.lang.Object(o229sub)) | =(matching1, 0)
f845_0_main_FieldAccess(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, o232))) → f851_0_main_FieldAccess(EOS, 0, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, o232))) | =(matching1, 0)
f851_0_main_FieldAccess(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, o232))) → f857_0_main_FieldAccess(EOS, 0, o232) | =(matching1, 0)
f857_0_main_FieldAccess(EOS, matching1, java.lang.Object(o235sub)) → f865_0_main_FieldAccess(EOS, 0, java.lang.Object(o235sub)) | =(matching1, 0)
f865_0_main_FieldAccess(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, o238))) → f872_0_main_FieldAccess(EOS, 0, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, o238))) | =(matching1, 0)
f872_0_main_FieldAccess(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, o238))) → f882_0_main_FieldAccess(EOS, 0, o238) | =(matching1, 0)
f882_0_main_FieldAccess(EOS, matching1, java.lang.Object(o243sub)) → f892_0_main_FieldAccess(EOS, 0, java.lang.Object(o243sub)) | =(matching1, 0)
f892_0_main_FieldAccess(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, o246))) → f899_0_main_FieldAccess(EOS, 0, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, o246))) | =(matching1, 0)
f899_0_main_FieldAccess(EOS, matching1, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, o246))) → f912_0_main_Store(EOS, 0, o246) | =(matching1, 0)
f912_0_main_Store(EOS, matching1, o246) → f923_0_main_JMP(EOS, o246, 0) | =(matching1, 0)
f923_0_main_JMP(EOS, o246, matching1) → f931_0_main_Inc(EOS, o246, 0) | =(matching1, 0)
f931_0_main_Inc(EOS, o246, matching1) → f956_0_main_Load(EOS, o246, 1) | =(matching1, 0)
f956_0_main_Load(EOS, o246, matching1) → f971_0_main_ConstantStackPush(EOS, o246, 1, 1) | =(matching1, 1)
f971_0_main_ConstantStackPush(EOS, o246, matching1, matching2) → f978_0_main_LE(EOS, o246, 1, 1) | &&(=(matching1, 1), =(matching2, 1))
f978_0_main_LE(EOS, o246, matching1, matching2) → f1011_0_main_Load(EOS, o246, 1) | &&(=(matching1, 1), =(matching2, 1))
f1011_0_main_Load(EOS, o246, matching1) → f795_0_main_Load(EOS, o246, 1) | =(matching1, 1)

Combined rules. Obtained 3 IRules

P rules:
f805_0_main_NULL(EOS, java.lang.Object(x0), 1, java.lang.Object(x0)) → f805_0_main_NULL(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(x0))), 2, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(x0))))
f805_0_main_NULL(EOS, java.lang.Object(x0), 2, java.lang.Object(x0)) → f805_0_main_NULL(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(x0))))), 0, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(x0))))))
f805_0_main_NULL(EOS, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, x0)))))))), 0, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(EOC, x0))))))))) → f805_0_main_NULL(EOS, x0, 1, x0)

Filtered ground terms:


f805_0_main_NULL(x1, x2, x3, x4) → f805_0_main_NULL(x2, x3, x4)
AlternatingGrowReduce.AlternatingGrowReduce(x1, x2) → AlternatingGrowReduce.AlternatingGrowReduce(x2)

Filtered duplicate terms:


f805_0_main_NULL(x1, x2, x3) → f805_0_main_NULL(x2, x3)

Prepared 3 rules for path length conversion:

P rules:
f805_0_main_NULL(1, java.lang.Object(x0)) → f805_0_main_NULL(2, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(java.lang.Object(x0))))
f805_0_main_NULL(2, java.lang.Object(x0)) → f805_0_main_NULL(0, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(java.lang.Object(x0))))))
f805_0_main_NULL(0, java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(java.lang.Object(AlternatingGrowReduce.AlternatingGrowReduce(x0))))))))) → f805_0_main_NULL(1, x0)

Finished conversion. Obtained 3 rules.

P rules:
f805_0_main_NULL(c1, v5) → f805_0_main_NULL(2, v6) | &&(&&(&&(>(+(v6, 1), 3), <=(-(v6, 2), v5)), >(+(v5, 1), 1)), =(1, c1))
f805_0_main_NULL(c2, v7) → f805_0_main_NULL(0, v8) | &&(&&(&&(>(+(v8, 1), 5), <=(-(v8, 4), v7)), >(+(v7, 1), 1)), =(2, c2))
f805_0_main_NULL(c0, v9) → f805_0_main_NULL(1, v10) | &&(&&(&&(>=(v9, +(v10, 7)), >(+(v9, 1), 7)), >(+(v10, 1), 0)), =(0, c0))

(12) Obligation:

Rules:
f805_0_main_NULL(c1, v5) → f805_0_main_NULL(2, v6) | &&(&&(&&(>(+(v6, 1), 3), <=(-(v6, 2), v5)), >(+(v5, 1), 1)), =(1, c1))
f805_0_main_NULL(c2, v7) → f805_0_main_NULL(0, v8) | &&(&&(&&(>(+(v8, 1), 5), <=(-(v8, 4), v7)), >(+(v7, 1), 1)), =(2, c2))
f805_0_main_NULL(c0, v9) → f805_0_main_NULL(1, v10) | &&(&&(&&(>=(v9, +(v10, 7)), >(+(v9, 1), 7)), >(+(v10, 1), 0)), =(0, c0))

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f805_0_main_NULL(x10, x13)] = -8 + 45·x10 - 18·x102 + 4·x13

Therefore the following rule(s) have been dropped:


f805_0_main_NULL(x0, x1) → f805_0_main_NULL(2, x2) | &&(&&(&&(>(+(x2, 1), 3), <=(-(x2, 2), x1)), >(+(x1, 1), 1)), =(1, x0))
f805_0_main_NULL(x3, x4) → f805_0_main_NULL(0, x5) | &&(&&(&&(>(+(x5, 1), 5), <=(-(x5, 4), x4)), >(+(x4, 1), 1)), =(2, x3))
f805_0_main_NULL(x6, x7) → f805_0_main_NULL(1, x8) | &&(&&(&&(>=(x7, +(x8, 7)), >(+(x7, 1), 7)), >(+(x8, 1), 0)), =(0, x6))

(14) YES