Termination proof of /tmp/tmpOmgMTn/Power.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 829 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 45 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIntTRSProof (⇒, 117 ms)

        ↳7 intTRS

        ↳8 PolynomialOrderProcessor (⇔, 0 ms)

        ↳9 YES

    ↳10 JBCTerminationSCC

        ↳11 SCCToIntTRSProof (⇒, 5 ms)

        ↳12 intTRS

        ↳13 PolynomialOrderProcessor (⇔, 0 ms)

        ↳14 YES

    ↳15 JBCTerminationSCC

        ↳16 SCCToIntTRSProof (⇒, 446 ms)

        ↳17 intTRS

        ↳18 PolynomialOrderProcessor (⇒, 93 ms)

        ↳19 intTRS

        ↳20 TerminationGraphProcessor (⇔, 0 ms)

        ↳21 YES

(0) Obligation:

JBC Problem based on JBC Program:

public class Power {
    public static void main(String args[]) {
	for (int i = 0; i < args.length; i++) {
	    even(power(args.length, args[i].length()));
	    odd( power(args.length, args[i].length()));
	}
	// power(args.length, args.length);
    }

    public static int power(int a, int n) {
	if (n <= 0) return 1;
	else if (n == 1) return a;
	else {
	    int r = power(a * a, n/2);
	    if (n % 2 == 0) return r;
	    else return a * r;
	}
    }

    public static boolean even(int n) {
	if (n <= 0) return true;
	else if (n == 1) return false;
	else return odd(n - 1);
    }

    public static boolean odd(int n) {
	if (n <= 0) return false;
	else if (n == 1) return true;
	else return even(n - 1);
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

Power.power(II)I: Graph of 46 nodes with 0 SCCs.

Power.even(I)Z: Graph of 28 nodes with 0 SCCs.

Power.odd(I)Z: Graph of 26 nodes with 0 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 3 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Power.even(I)Z, Power.odd(I)Z
SCC calls the following helper methods: Power.even(I)Z, Power.odd(I)Z
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 28 IRules

P rules:
f1583_0_even_GT(EOS, i429, i429, i429) → f1590_0_even_GT(EOS, i429, i429, i429)
f1590_0_even_GT(EOS, i429, i429, i429) → f1617_0_even_Load(EOS, i429, i429) | >(i429, 0)
f1617_0_even_Load(EOS, i429, i429) → f1632_0_even_ConstantStackPush(EOS, i429, i429, i429)
f1632_0_even_ConstantStackPush(EOS, i429, i429, i429) → f1654_0_even_NE(EOS, i429, i429, i429, 1)
f1654_0_even_NE(EOS, i459, i459, i459, matching1) → f1677_0_even_NE(EOS, i459, i459, i459, 1) | =(matching1, 1)
f1677_0_even_NE(EOS, i459, i459, i459, matching1) → f1689_0_even_Load(EOS, i459, i459) | &&(>(i459, 1), =(matching1, 1))
f1689_0_even_Load(EOS, i459, i459) → f1700_0_even_ConstantStackPush(EOS, i459, i459)
f1700_0_even_ConstantStackPush(EOS, i459, i459) → f1730_0_even_IntArithmetic(EOS, i459, i459, 1)
f1730_0_even_IntArithmetic(EOS, i459, i459, matching1) → f1747_0_even_InvokeMethod(EOS, i459, -(i459, 1)) | &&(>(i459, 0), =(matching1, 1))
f1747_0_even_InvokeMethod(EOS, i459, i467) → f1756_0_odd_Load(EOS, i467, i467)
f1747_0_even_InvokeMethod(EOS, i459, i467) → f1756_1_odd_Load(EOS, i459, i467, i467)
f1756_0_odd_Load(EOS, i467, i467) → f1770_0_odd_Load(EOS, i467, i467)
f1770_0_odd_Load(EOS, i467, i467) → f2101_0_odd_Load(EOS, i467, i467)
f2101_0_odd_Load(EOS, i598, i598) → f2107_0_odd_GT(EOS, i598, i598, i598)
f2107_0_odd_GT(EOS, i602, i602, i602) → f2116_0_odd_GT(EOS, i602, i602, i602)
f2116_0_odd_GT(EOS, i602, i602, i602) → f2134_0_odd_Load(EOS, i602, i602) | >(i602, 0)
f2134_0_odd_Load(EOS, i602, i602) → f2146_0_odd_ConstantStackPush(EOS, i602, i602, i602)
f2146_0_odd_ConstantStackPush(EOS, i602, i602, i602) → f2160_0_odd_NE(EOS, i602, i602, i602, 1)
f2160_0_odd_NE(EOS, i609, i609, i609, matching1) → f2186_0_odd_NE(EOS, i609, i609, i609, 1) | =(matching1, 1)
f2186_0_odd_NE(EOS, i609, i609, i609, matching1) → f2196_0_odd_Load(EOS, i609, i609) | &&(>(i609, 1), =(matching1, 1))
f2196_0_odd_Load(EOS, i609, i609) → f2208_0_odd_ConstantStackPush(EOS, i609, i609)
f2208_0_odd_ConstantStackPush(EOS, i609, i609) → f2215_0_odd_IntArithmetic(EOS, i609, i609, 1)
f2215_0_odd_IntArithmetic(EOS, i609, i609, matching1) → f2239_0_odd_InvokeMethod(EOS, i609, -(i609, 1)) | &&(>(i609, 0), =(matching1, 1))
f2239_0_odd_InvokeMethod(EOS, i609, i613) → f2245_0_even_Load(EOS, i613, i613)
f2239_0_odd_InvokeMethod(EOS, i609, i613) → f2245_1_even_Load(EOS, i609, i613, i613)
f2245_0_even_Load(EOS, i613, i613) → f2248_0_even_Load(EOS, i613, i613)
f2248_0_even_Load(EOS, i613, i613) → f1577_0_even_Load(EOS, i613, i613)
f1577_0_even_Load(EOS, i426, i426) → f1583_0_even_GT(EOS, i426, i426, i426)

Combined rules. Obtained 3 IRules

P rules:
f1583_0_even_GT(EOS, x0, x0, x0) → f1756_1_odd_Load(EOS, x0, -(x0, 1), -(x0, 1)) | >(x0, 1)
f1583_0_even_GT(EOS, x0, x0, x0) → f2245_1_even_Load(EOS, -(x0, 1), -(x0, 2), -(x0, 2)) | >(x0, 2)
f1583_0_even_GT(EOS, x0, x0, x0) → f1583_0_even_GT(EOS, -(x0, 2), -(x0, 2), -(x0, 2)) | >(x0, 2)

Filtered ground terms:

f1583_0_even_GT(x1, x2, x3, x4) → f1583_0_even_GT(x2, x3, x4)
Cond_f1583_0_even_GT(x1, x2, x3, x4, x5) → Cond_f1583_0_even_GT(x1, x3, x4, x5)
f1756_1_odd_Load(x1, x2, x3, x4) → f1756_1_odd_Load(x2, x3, x4)
Cond_f1583_0_even_GT1(x1, x2, x3, x4, x5) → Cond_f1583_0_even_GT1(x1, x3, x4, x5)
f2245_1_even_Load(x1, x2, x3, x4) → f2245_1_even_Load(x2, x3, x4)
Cond_f1583_0_even_GT2(x1, x2, x3, x4, x5) → Cond_f1583_0_even_GT2(x1, x3, x4, x5)

Filtered duplicate terms:

f1583_0_even_GT(x1, x2, x3) → f1583_0_even_GT(x3)
Cond_f1583_0_even_GT(x1, x2, x3, x4) → Cond_f1583_0_even_GT(x1, x4)
f1756_1_odd_Load(x1, x2, x3) → f1756_1_odd_Load(x3)
Cond_f1583_0_even_GT1(x1, x2, x3, x4) → Cond_f1583_0_even_GT1(x1, x4)
f2245_1_even_Load(x1, x2, x3) → f2245_1_even_Load(x1, x3)
Cond_f1583_0_even_GT2(x1, x2, x3, x4) → Cond_f1583_0_even_GT2(x1, x4)

Filtered unneeded terms:

Cond_f1583_0_even_GT(x1, x2) → Cond_f1583_0_even_GT(x1)
Cond_f1583_0_even_GT1(x1, x2) → Cond_f1583_0_even_GT1(x1)

Prepared 3 rules for path length conversion:

P rules:
f1583_0_even_GT(x0) → f1756_1_odd_Load(-(x0, 1)) | >(x0, 1)
f1583_0_even_GT(x0) → f2245_1_even_Load(-(x0, 1), -(x0, 2)) | >(x0, 2)
f1583_0_even_GT(x0) → f1583_0_even_GT(-(x0, 2)) | >(x0, 2)

Finished conversion. Obtained 1 rules.

P rules:
f1583_0_even_GT(x2) → f1583_0_even_GT(-(x2, 2)) | >(x2, 2)

(7) Obligation:

Rules:
f1583_0_even_GT(x2) → f1583_0_even_GT(-(x2, 2)) | >(x2, 2)

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f1583_0_even_GT(x2)] = x2

Therefore the following rule(s) have been dropped:

f1583_0_even_GT(x0) → f1583_0_even_GT(-(x0, 2)) | >(x0, 2)

(9) YES

(10) Obligation:

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

Used field analysis yielded the following read fields:
Marker field analysis yielded the following relations that could be markers:

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 17 IRules

P rules:
f1315_0_power_GT(EOS, i359, i359, i359) → f1321_0_power_GT(EOS, i359, i359, i359)
f1321_0_power_GT(EOS, i359, i359, i359) → f1329_0_power_Load(EOS, i359, i359) | >(i359, 0)
f1329_0_power_Load(EOS, i359, i359) → f1332_0_power_ConstantStackPush(EOS, i359, i359, i359)
f1332_0_power_ConstantStackPush(EOS, i359, i359, i359) → f1340_0_power_NE(EOS, i359, i359, i359, 1)
f1340_0_power_NE(EOS, i365, i365, i365, matching1) → f1362_0_power_NE(EOS, i365, i365, i365, 1) | =(matching1, 1)
f1362_0_power_NE(EOS, i365, i365, i365, matching1) → f1369_0_power_Load(EOS, i365, i365) | &&(>(i365, 1), =(matching1, 1))
f1369_0_power_Load(EOS, i365, i365) → f1378_0_power_Load(EOS, i365, i365)
f1378_0_power_Load(EOS, i365, i365) → f1388_0_power_IntArithmetic(EOS, i365, i365)
f1388_0_power_IntArithmetic(EOS, i365, i365) → f1408_0_power_Load(EOS, i365, i365)
f1408_0_power_Load(EOS, i365, i365) → f1417_0_power_ConstantStackPush(EOS, i365, i365, i365)
f1417_0_power_ConstantStackPush(EOS, i365, i365, i365) → f1423_0_power_IntArithmetic(EOS, i365, i365, i365, 2)
f1423_0_power_IntArithmetic(EOS, i365, i365, i365, matching1) → f1426_0_power_InvokeMethod(EOS, i365, i365, /(i365, 2)) | &&(>(i365, 1), =(matching1, 2))
f1426_0_power_InvokeMethod(EOS, i365, i365, i385) → f1429_0_power_Load(EOS, i385, i385)
f1426_0_power_InvokeMethod(EOS, i365, i365, i385) → f1429_1_power_Load(EOS, i365, i365, i385, i385)
f1429_0_power_Load(EOS, i385, i385) → f1435_0_power_Load(EOS, i385, i385)
f1435_0_power_Load(EOS, i385, i385) → f1310_0_power_Load(EOS, i385, i385)
f1310_0_power_Load(EOS, i357, i357) → f1315_0_power_GT(EOS, i357, i357, i357)

Combined rules. Obtained 2 IRules

P rules:
f1315_0_power_GT(EOS, x0, x0, x0) → f1429_1_power_Load(EOS, x0, x0, /(x0, 2), /(x0, 2)) | >(x0, 1)
f1315_0_power_GT(EOS, x0, x0, x0) → f1315_0_power_GT(EOS, /(x0, 2), /(x0, 2), /(x0, 2)) | >(x0, 1)

Filtered ground terms:

f1315_0_power_GT(x1, x2, x3, x4) → f1315_0_power_GT(x2, x3, x4)
Cond_f1315_0_power_GT(x1, x2, x3, x4, x5) → Cond_f1315_0_power_GT(x1, x3, x4, x5)
f1429_1_power_Load(x1, x2, x3, x4, x5) → f1429_1_power_Load(x2, x3, x4, x5)
Cond_f1315_0_power_GT1(x1, x2, x3, x4, x5) → Cond_f1315_0_power_GT1(x1, x3, x4, x5)

Filtered duplicate terms:

f1315_0_power_GT(x1, x2, x3) → f1315_0_power_GT(x3)
Cond_f1315_0_power_GT(x1, x2, x3, x4) → Cond_f1315_0_power_GT(x1, x4)
f1429_1_power_Load(x1, x2, x3, x4) → f1429_1_power_Load(x4)
Cond_f1315_0_power_GT1(x1, x2, x3, x4) → Cond_f1315_0_power_GT1(x1, x4)

Filtered unneeded terms:

Cond_f1315_0_power_GT(x1, x2) → Cond_f1315_0_power_GT(x1)

Prepared 2 rules for path length conversion:

P rules:
f1315_0_power_GT(x0) → f1429_1_power_Load(/(x0, 2)) | >(x0, 1)
f1315_0_power_GT(x0) → f1315_0_power_GT(/(x0, 2)) | >(x0, 1)

Finished conversion. Obtained 2 rules.

P rules:
f1315_0_power_GT(x1) → f1315_0_power_GT'(x1) | >(x1, 1)
f1315_0_power_GT'(x1) → f1315_0_power_GT(arith) | &&(&&(>(x1, 1), <(-(x1, *(2, arith)), 2)), >=(-(x1, *(2, arith)), 0))

(12) Obligation:

Rules:
f1315_0_power_GT(x1) → f1315_0_power_GT'(x1) | >(x1, 1)
f1315_0_power_GT'(x1) → f1315_0_power_GT(arith) | &&(&&(>(x1, 1), <(-(x1, *(2, arith)), 2)), >=(-(x1, *(2, arith)), 0))

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f1315_0_power_GT(x4)] = -1 + 2·x4
[f1315_0_power_GT'(x7)] = x7

Therefore the following rule(s) have been dropped:

f1315_0_power_GT(x0) → f1315_0_power_GT'(x0) | >(x0, 1)
f1315_0_power_GT'(x1) → f1315_0_power_GT(x2) | &&(&&(>(x1, 1), <(-(x1, *(2, x2)), 2)), >=(-(x1, *(2, x2)), 0))

(14) YES

(15) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Power.main([Ljava/lang/String;)V
SCC calls the following helper methods: Power.power(II)I, Power.even(I)Z, Power.odd(I)Z
Performed SCC analyses:

Used field analysis yielded the following read fields:
- java.lang.String: [count]
Marker field analysis yielded the following relations that could be markers:

(16) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 84 IRules

P rules:
f3292_0_main_Load(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i934) → f3293_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i934, java.lang.Object(ARRAY(i933)))
f3293_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i934, java.lang.Object(ARRAY(i933))) → f3295_0_main_GE(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i934, i933) | >=(i933, 0)
f3295_0_main_GE(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i934, i933) → f3298_0_main_GE(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i934, i933)
f3298_0_main_GE(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i934, i933) → f3301_0_main_Load(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934) | <(i934, i933)
f3301_0_main_Load(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934) → f3303_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, java.lang.Object(ARRAY(i933)))
f3303_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, java.lang.Object(ARRAY(i933))) → f3305_0_main_Load(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i933) | >=(i933, 0)
f3305_0_main_Load(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i933) → f3306_0_main_Load(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i933, java.lang.Object(ARRAY(i933)))
f3306_0_main_Load(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i933, java.lang.Object(ARRAY(i933))) → f3308_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i933, java.lang.Object(ARRAY(i933)), i934)
f3308_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i933, java.lang.Object(ARRAY(i933)), i934) → f3310_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i933, java.lang.Object(ARRAY(i933)), i934)
f3310_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i933, java.lang.Object(ARRAY(i933)), i934) → f3314_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i933, o916) | <(i934, i933)
f3314_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i933, java.lang.Object(o919sub)) → f3317_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i933, java.lang.Object(o919sub))
f3317_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i933, java.lang.Object(o919sub)) → f3320_0_length_Load(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i933, java.lang.Object(o919sub), java.lang.Object(o919sub))
f3320_0_length_Load(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i933, java.lang.Object(o919sub), java.lang.Object(o919sub)) → f3329_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i933, java.lang.Object(o919sub), java.lang.Object(o919sub))
f3329_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i933, java.lang.Object(java.lang.String(o923sub, i949)), java.lang.Object(java.lang.String(o923sub, i949))) → f3331_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i933, java.lang.Object(java.lang.String(o923sub, i949)), java.lang.Object(java.lang.String(o923sub, i949))) | >=(i949, 0)
f3331_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i933, java.lang.Object(java.lang.String(o923sub, i949)), java.lang.Object(java.lang.String(o923sub, i949))) → f3336_0_length_Return(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i933, java.lang.Object(java.lang.String(o923sub, i949)), i949)
f3336_0_length_Return(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i933, java.lang.Object(java.lang.String(o923sub, i949)), i949) → f3341_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i933, i949)
f3341_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i933, i949) → f3343_0_power_Load(EOS, i933, i949, i933, i949)
f3341_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i933, i949) → f3343_1_power_Load(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i933, i949, i933, i949)
f3343_0_power_Load(EOS, i933, i949, i933, i949) → f3349_0_power_Load(EOS, i933, i949, i933, i949)
f3385_0_power_Return(EOS, java.lang.Object(ARRAY(i957)), java.lang.Object(ARRAY(i957)), i934, i957, matching1, i957, matching2, matching3) → f3394_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i957)), java.lang.Object(ARRAY(i957)), i934, 1) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 1))
f3394_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i957)), java.lang.Object(ARRAY(i957)), i934, matching1) → f3404_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i957)), java.lang.Object(ARRAY(i957)), i934, 1) | =(matching1, 1)
f3404_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i966)), java.lang.Object(ARRAY(i966)), i934, i964) → f3408_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i966)), java.lang.Object(ARRAY(i966)), i934, i964)
f3408_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i971) → f3412_0_even_Load(EOS, i971, i971)
f3408_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i971) → f3412_1_even_Load(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i971, i971)
f3412_0_even_Load(EOS, i971, i971) → f3419_0_even_Load(EOS, i971, i971)
f3459_0_even_Return(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, matching1, matching2, matching3) → f3475_0_main_StackPop(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, 1) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 1))
f3475_0_main_StackPop(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, matching1) → f3484_0_main_StackPop(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, 1) | =(matching1, 1)
f3484_0_main_StackPop(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i993) → f3493_0_main_Load(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934)
f3493_0_main_Load(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934) → f3499_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, java.lang.Object(ARRAY(i974)))
f3499_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, java.lang.Object(ARRAY(i974))) → f3506_0_main_Load(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974) | >=(i974, 0)
f3506_0_main_Load(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974) → f3511_0_main_Load(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974, java.lang.Object(ARRAY(i974)))
f3511_0_main_Load(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974, java.lang.Object(ARRAY(i974))) → f3518_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974, java.lang.Object(ARRAY(i974)), i934)
f3518_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974, java.lang.Object(ARRAY(i974)), i934) → f3524_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974, java.lang.Object(ARRAY(i974)), i934)
f3524_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974, java.lang.Object(ARRAY(i974)), i934) → f3531_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974, o977) | <(i934, i974)
f3531_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974, java.lang.Object(o981sub)) → f3539_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974, java.lang.Object(o981sub))
f3539_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974, java.lang.Object(o981sub)) → f3543_0_length_Load(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974, java.lang.Object(o981sub), java.lang.Object(o981sub))
f3543_0_length_Load(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974, java.lang.Object(o981sub), java.lang.Object(o981sub)) → f3557_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974, java.lang.Object(o981sub), java.lang.Object(o981sub))
f3557_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974, java.lang.Object(java.lang.String(o991sub, i1016)), java.lang.Object(java.lang.String(o991sub, i1016))) → f3559_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974, java.lang.Object(java.lang.String(o991sub, i1016)), java.lang.Object(java.lang.String(o991sub, i1016))) | >=(i1016, 0)
f3559_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974, java.lang.Object(java.lang.String(o991sub, i1016)), java.lang.Object(java.lang.String(o991sub, i1016))) → f3567_0_length_Return(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974, java.lang.Object(java.lang.String(o991sub, i1016)), i1016)
f3567_0_length_Return(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974, java.lang.Object(java.lang.String(o991sub, i1016)), i1016) → f3572_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974, i1016)
f3572_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974, i1016) → f3574_0_power_Load(EOS, i974, i1016, i974, i1016)
f3572_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974, i1016) → f3574_1_power_Load(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974, i1016, i974, i1016)
f3574_0_power_Load(EOS, i974, i1016, i974, i1016) → f3584_0_power_Load(EOS, i974, i1016, i974, i1016)
f3624_0_power_Return(EOS, java.lang.Object(ARRAY(i1025)), java.lang.Object(ARRAY(i1025)), i934, i1025, matching1, i1025, matching2, matching3) → f3632_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i1025)), java.lang.Object(ARRAY(i1025)), i934, 1) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 1))
f3632_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i1025)), java.lang.Object(ARRAY(i1025)), i934, matching1) → f3641_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i1025)), java.lang.Object(ARRAY(i1025)), i934, 1) | =(matching1, 1)
f3641_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i1038)), java.lang.Object(ARRAY(i1038)), i934, i1034) → f3645_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i1038)), java.lang.Object(ARRAY(i1038)), i934, i1034)
f3645_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i934, i1041) → f3648_0_odd_Load(EOS, i1041, i1041)
f3645_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i934, i1041) → f3648_1_odd_Load(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i934, i1041, i1041)
f3648_0_odd_Load(EOS, i1041, i1041) → f3657_0_odd_Load(EOS, i1041, i1041)
f3699_0_odd_Return(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i934, matching1, matching2, matching3) → f3717_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i934, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f3717_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i934, matching1) → f3727_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i934, 0) | =(matching1, 0)
f3727_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i934, i1056) → f3743_0_main_Inc(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i934)
f3743_0_main_Inc(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i934) → f3757_0_main_JMP(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), +(i934, 1)) | >=(i934, 0)
f3757_0_main_JMP(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i1062) → f3774_0_main_Load(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i1062)
f3774_0_main_Load(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i1062) → f3284_0_main_Load(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i1062)
f3284_0_main_Load(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934) → f3292_0_main_Load(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i934)
f3700_0_odd_Return(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i934, matching1, matching2, matching3) → f3719_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i934, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
f3719_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i934, matching1) → f3727_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i934, 1) | =(matching1, 1)
f3701_0_odd_Return(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i934, i1058, i1056) → f3727_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i934, i1056)
f3625_0_power_Return(EOS, java.lang.Object(ARRAY(i1029)), java.lang.Object(ARRAY(i1029)), i934, i1029, matching1, i1029, matching2, i1029) → f3635_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i1029)), java.lang.Object(ARRAY(i1029)), i934, i1029) | &&(=(matching1, 1), =(matching2, 1))
f3635_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i1029)), java.lang.Object(ARRAY(i1029)), i934, i1029) → f3641_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i1029)), java.lang.Object(ARRAY(i1029)), i934, i1029)
f3626_0_power_Return(EOS, java.lang.Object(ARRAY(i1038)), java.lang.Object(ARRAY(i1038)), i934, i1038, i1036, i1038, i1034, i1034) → f3641_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i1038)), java.lang.Object(ARRAY(i1038)), i934, i1034)
f3627_0_power_Return(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i934, i1045, i1043, i1041) → f3645_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i934, i1041)
f3461_0_even_Return(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, matching1, matching2, matching3) → f3477_0_main_StackPop(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, 0) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 0))
f3477_0_main_StackPop(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, matching1) → f3484_0_main_StackPop(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, 0) | =(matching1, 0)
f3462_0_even_Return(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i995, i993) → f3484_0_main_StackPop(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i993)
f3386_0_power_Return(EOS, java.lang.Object(ARRAY(i961)), java.lang.Object(ARRAY(i961)), i934, i961, matching1, i961, matching2, i961) → f3398_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i961)), java.lang.Object(ARRAY(i961)), i934, i961) | &&(=(matching1, 1), =(matching2, 1))
f3398_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i961)), java.lang.Object(ARRAY(i961)), i934, i961) → f3404_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i961)), java.lang.Object(ARRAY(i961)), i934, i961)
f3387_0_power_Return(EOS, java.lang.Object(ARRAY(i966)), java.lang.Object(ARRAY(i966)), i934, i966, i968, i966, i964, i964) → f3404_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i966)), java.lang.Object(ARRAY(i966)), i934, i964)
f3388_0_power_Return(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974, i976, i971) → f3408_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i971)
f3343_1_power_Load(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i957, matching1, i957, matching2) → f3385_0_power_Return(EOS, java.lang.Object(ARRAY(i957)), java.lang.Object(ARRAY(i957)), i934, i957, 0, i957, 0, 1) | &&(=(matching1, 0), =(matching2, 0))
f3343_1_power_Load(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i961, matching1, i961, matching2) → f3386_0_power_Return(EOS, java.lang.Object(ARRAY(i961)), java.lang.Object(ARRAY(i961)), i934, i961, 1, i961, 1, i961) | &&(=(matching1, 1), =(matching2, 1))
f3343_1_power_Load(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i966, i968, i966, i968) → f3387_0_power_Return(EOS, java.lang.Object(ARRAY(i966)), java.lang.Object(ARRAY(i966)), i934, i966, i968, i966, i964, i964)
f3343_1_power_Load(EOS, java.lang.Object(ARRAY(i933)), java.lang.Object(ARRAY(i933)), i934, i974, i976, i974, i976) → f3388_0_power_Return(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i974, i976, i971)
f3412_1_even_Load(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, matching1, matching2) → f3459_0_even_Return(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, 0, 0, 1) | &&(=(matching1, 0), =(matching2, 0))
f3412_1_even_Load(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, matching1, matching2) → f3461_0_even_Return(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, 1, 1, 0) | &&(=(matching1, 1), =(matching2, 1))
f3412_1_even_Load(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i995, i995) → f3462_0_even_Return(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i995, i993)
f3574_1_power_Load(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i1025, matching1, i1025, matching2) → f3624_0_power_Return(EOS, java.lang.Object(ARRAY(i1025)), java.lang.Object(ARRAY(i1025)), i934, i1025, 0, i1025, 0, 1) | &&(=(matching1, 0), =(matching2, 0))
f3574_1_power_Load(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i1029, matching1, i1029, matching2) → f3625_0_power_Return(EOS, java.lang.Object(ARRAY(i1029)), java.lang.Object(ARRAY(i1029)), i934, i1029, 1, i1029, 1, i1029) | &&(=(matching1, 1), =(matching2, 1))
f3574_1_power_Load(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i1038, i1036, i1038, i1036) → f3626_0_power_Return(EOS, java.lang.Object(ARRAY(i1038)), java.lang.Object(ARRAY(i1038)), i934, i1038, i1036, i1038, i1034, i1034)
f3574_1_power_Load(EOS, java.lang.Object(ARRAY(i974)), java.lang.Object(ARRAY(i974)), i934, i1045, i1043, i1045, i1043) → f3627_0_power_Return(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i934, i1045, i1043, i1041)
f3648_1_odd_Load(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i934, matching1, matching2) → f3699_0_odd_Return(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i934, 0, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
f3648_1_odd_Load(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i934, matching1, matching2) → f3700_0_odd_Return(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i934, 1, 1, 1) | &&(=(matching1, 1), =(matching2, 1))
f3648_1_odd_Load(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i934, i1058, i1058) → f3701_0_odd_Return(EOS, java.lang.Object(ARRAY(i1045)), java.lang.Object(ARRAY(i1045)), i934, i1058, i1056)

Combined rules. Obtained 16 IRules

P rules:
f3292_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x1) → f3349_0_power_Load(EOS, x0, x2, x0, x2) | &&(&&(>(+(x2, 1), 0), <(x1, x0)), >(+(x0, 1), 0))
f3408_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2) → f3419_0_even_Load(EOS, x2, x2)
f3572_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x0, x2) → f3584_0_power_Load(EOS, x0, x2, x0, x2)
f3645_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2) → f3657_0_odd_Load(EOS, x2, x2)
f3292_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x1) → f3408_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, 1) | &&(<(x1, x0), >(+(x0, 1), 0))
f3292_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x1) → f3408_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x0) | &&(<(x1, x0), >(+(x0, 1), 0))
f3292_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x1) → f3408_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2) | &&(<(x1, x0), >(+(x0, 1), 0))
f3408_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, 0) → f3572_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x0, x3) | &&(&&(>(+(x3, 1), 0), >(+(x0, 1), 0)), <(x1, x0))
f3408_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, 1) → f3572_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x0, x3) | &&(&&(>(+(x3, 1), 0), >(+(x0, 1), 0)), <(x1, x0))
f3408_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2) → f3572_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x0, x3) | &&(&&(>(+(x3, 1), 0), >(+(x0, 1), 0)), <(x1, x0))
f3572_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x0, 0) → f3645_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, 1)
f3572_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x0, 1) → f3645_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x0)
f3572_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x0, x2) → f3645_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x3)
f3645_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, 0) → f3292_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), +(x1, 1), +(x1, 1)) | >(+(x1, 1), 0)
f3645_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, 1) → f3292_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), +(x1, 1), +(x1, 1)) | >(+(x1, 1), 0)
f3645_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2) → f3292_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), +(x1, 1), +(x1, 1)) | >(+(x1, 1), 0)

Filtered ground terms:

f3292_0_main_Load(x1, x2, x3, x4, x5) → f3292_0_main_Load(x2, x3, x4, x5)
Cond_f3292_0_main_Load(x1, x2, x3, x4, x5, x6, x7) → Cond_f3292_0_main_Load(x1, x3, x4, x5, x6, x7)
f3349_0_power_Load(x1, x2, x3, x4, x5) → f3349_0_power_Load(x2, x3, x4, x5)
f3408_0_main_InvokeMethod(x1, x2, x3, x4, x5) → f3408_0_main_InvokeMethod(x2, x3, x4, x5)
f3419_0_even_Load(x1, x2, x3) → f3419_0_even_Load(x2, x3)
f3572_0_main_InvokeMethod(x1, x2, x3, x4, x5, x6) → f3572_0_main_InvokeMethod(x2, x3, x4, x5, x6)
f3584_0_power_Load(x1, x2, x3, x4, x5) → f3584_0_power_Load(x2, x3, x4, x5)
f3645_0_main_InvokeMethod(x1, x2, x3, x4, x5) → f3645_0_main_InvokeMethod(x2, x3, x4, x5)
f3657_0_odd_Load(x1, x2, x3) → f3657_0_odd_Load(x2, x3)
Cond_f3292_0_main_Load1(x1, x2, x3, x4, x5, x6) → Cond_f3292_0_main_Load1(x1, x3, x4, x5, x6)
Cond_f3292_0_main_Load2(x1, x2, x3, x4, x5, x6) → Cond_f3292_0_main_Load2(x1, x3, x4, x5, x6)
Cond_f3292_0_main_Load3(x1, x2, x3, x4, x5, x6, x7) → Cond_f3292_0_main_Load3(x1, x3, x4, x5, x6, x7)
Cond_f3408_0_main_InvokeMethod(x1, x2, x3, x4, x5, x6, x7) → Cond_f3408_0_main_InvokeMethod(x1, x3, x4, x5, x7)
Cond_f3408_0_main_InvokeMethod1(x1, x2, x3, x4, x5, x6, x7) → Cond_f3408_0_main_InvokeMethod1(x1, x3, x4, x5, x7)
Cond_f3408_0_main_InvokeMethod2(x1, x2, x3, x4, x5, x6, x7) → Cond_f3408_0_main_InvokeMethod2(x1, x3, x4, x5, x6, x7)
Cond_f3645_0_main_InvokeMethod(x1, x2, x3, x4, x5, x6) → Cond_f3645_0_main_InvokeMethod(x1, x3, x4, x5)
Cond_f3645_0_main_InvokeMethod1(x1, x2, x3, x4, x5, x6) → Cond_f3645_0_main_InvokeMethod1(x1, x3, x4, x5)
Cond_f3645_0_main_InvokeMethod2(x1, x2, x3, x4, x5, x6) → Cond_f3645_0_main_InvokeMethod2(x1, x3, x4, x5, x6)

Filtered duplicate terms:

f3292_0_main_Load(x1, x2, x3, x4) → f3292_0_main_Load(x2, x4)
Cond_f3292_0_main_Load(x1, x2, x3, x4, x5, x6) → Cond_f3292_0_main_Load(x1, x3, x5, x6)
f3349_0_power_Load(x1, x2, x3, x4) → f3349_0_power_Load(x3, x4)
f3408_0_main_InvokeMethod(x1, x2, x3, x4) → f3408_0_main_InvokeMethod(x2, x3, x4)
f3419_0_even_Load(x1, x2) → f3419_0_even_Load(x2)
f3572_0_main_InvokeMethod(x1, x2, x3, x4, x5) → f3572_0_main_InvokeMethod(x2, x3, x5)
f3584_0_power_Load(x1, x2, x3, x4) → f3584_0_power_Load(x3, x4)
f3645_0_main_InvokeMethod(x1, x2, x3, x4) → f3645_0_main_InvokeMethod(x2, x3, x4)
f3657_0_odd_Load(x1, x2) → f3657_0_odd_Load(x2)
Cond_f3292_0_main_Load1(x1, x2, x3, x4, x5) → Cond_f3292_0_main_Load1(x1, x3, x5)
Cond_f3292_0_main_Load2(x1, x2, x3, x4, x5) → Cond_f3292_0_main_Load2(x1, x3, x5)
Cond_f3292_0_main_Load3(x1, x2, x3, x4, x5, x6) → Cond_f3292_0_main_Load3(x1, x3, x5, x6)
Cond_f3408_0_main_InvokeMethod(x1, x2, x3, x4, x5) → Cond_f3408_0_main_InvokeMethod(x1, x3, x4, x5)
Cond_f3408_0_main_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_f3408_0_main_InvokeMethod1(x1, x3, x4, x5)
Cond_f3408_0_main_InvokeMethod2(x1, x2, x3, x4, x5, x6) → Cond_f3408_0_main_InvokeMethod2(x1, x3, x4, x5, x6)
Cond_f3645_0_main_InvokeMethod(x1, x2, x3, x4) → Cond_f3645_0_main_InvokeMethod(x1, x3, x4)
Cond_f3645_0_main_InvokeMethod1(x1, x2, x3, x4) → Cond_f3645_0_main_InvokeMethod1(x1, x3, x4)
Cond_f3645_0_main_InvokeMethod2(x1, x2, x3, x4, x5) → Cond_f3645_0_main_InvokeMethod2(x1, x3, x4, x5)

Filtered unneeded terms:

Cond_f3292_0_main_Load(x1, x2, x3, x4) → Cond_f3292_0_main_Load(x1)
Cond_f3408_0_main_InvokeMethod2(x1, x2, x3, x4, x5) → Cond_f3408_0_main_InvokeMethod2(x1, x2, x3, x5)
Cond_f3645_0_main_InvokeMethod2(x1, x2, x3, x4) → Cond_f3645_0_main_InvokeMethod2(x1, x2, x3)

Prepared 16 rules for path length conversion:

P rules:
f3292_0_main_Load(java.lang.Object(ARRAY(x0)), x1, x0) → f3349_0_power_Load(x0, x2) | &&(&&(>(+(x2, 1), 0), <(x1, x0)), >(+(x0, 1), 0))
f3408_0_main_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f3419_0_even_Load(x2)
f3572_0_main_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f3584_0_power_Load(x0, x2)
f3645_0_main_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f3657_0_odd_Load(x2)
f3292_0_main_Load(java.lang.Object(ARRAY(x0)), x1, x0) → f3408_0_main_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, 1, x0) | &&(<(x1, x0), >(+(x0, 1), 0))
f3292_0_main_Load(java.lang.Object(ARRAY(x0)), x1, x0) → f3408_0_main_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x0, x0) | &&(<(x1, x0), >(+(x0, 1), 0))
f3292_0_main_Load(java.lang.Object(ARRAY(x0)), x1, x0) → f3408_0_main_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x0) | &&(<(x1, x0), >(+(x0, 1), 0))
f3408_0_main_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, 0, x0) → f3572_0_main_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x3, x0) | &&(&&(>(+(x3, 1), 0), >(+(x0, 1), 0)), <(x1, x0))
f3408_0_main_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, 1, x0) → f3572_0_main_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x3, x0) | &&(&&(>(+(x3, 1), 0), >(+(x0, 1), 0)), <(x1, x0))
f3408_0_main_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f3572_0_main_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x3, x0) | &&(&&(>(+(x3, 1), 0), >(+(x0, 1), 0)), <(x1, x0))
f3572_0_main_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, 0, x0) → f3645_0_main_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, 1, x0)
f3572_0_main_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, 1, x0) → f3645_0_main_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x0, x0)
f3572_0_main_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f3645_0_main_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x3, x0)
f3645_0_main_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, 0, x0) → f3292_0_main_Load(java.lang.Object(ARRAY(x0)), +(x1, 1), x0) | >(+(x1, 1), 0)
f3645_0_main_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, 1, x0) → f3292_0_main_Load(java.lang.Object(ARRAY(x0)), +(x1, 1), x0) | >(+(x1, 1), 0)
f3645_0_main_InvokeMethod(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f3292_0_main_Load(java.lang.Object(ARRAY(x0)), +(x1, 1), x0) | >(+(x1, 1), 0)

Finished conversion. Obtained 12 rules.

P rules:
f3292_0_main_Load(v59, x13, x12) → f3408_0_main_InvokeMethod(v60, x13, 1, x12) | &&(&&(&&(&&(<(x13, x12), >(x12, -1)), >(+(v60, 1), 1)), <=(v60, v59)), >(+(v59, 1), 1))
f3292_0_main_Load(v61, x15, x14) → f3408_0_main_InvokeMethod(v62, x15, x14, x14) | &&(&&(&&(&&(<(x15, x14), >(x14, -1)), >(+(v62, 1), 1)), <=(v62, v61)), >(+(v61, 1), 1))
f3292_0_main_Load(v63, x17, x16) → f3408_0_main_InvokeMethod(v64, x17, x18, x16) | &&(&&(&&(&&(<(x17, x16), >(x16, -1)), >(+(v64, 1), 1)), <=(v64, v63)), >(+(v63, 1), 1))
f3408_0_main_InvokeMethod(v65, x20, c0, x19) → f3572_0_main_InvokeMethod(v66, x20, x21, x19) | &&(&&(&&(&&(&&(&&(>(x21, -1), <(x20, x19)), >(x19, -1)), >(+(v66, 1), 1)), <=(v66, v65)), >(+(v65, 1), 1)), =(0, c0))
f3408_0_main_InvokeMethod(v67, x23, c1, x22) → f3572_0_main_InvokeMethod(v68, x23, x24, x22) | &&(&&(&&(&&(&&(&&(>(x24, -1), <(x23, x22)), >(x22, -1)), >(+(v68, 1), 1)), <=(v68, v67)), >(+(v67, 1), 1)), =(1, c1))
f3408_0_main_InvokeMethod(v69, x26, x27, x25) → f3572_0_main_InvokeMethod(v70, x26, x28, x25) | &&(&&(&&(&&(&&(>(x28, -1), <(x26, x25)), >(x25, -1)), >(+(v70, 1), 1)), <=(v70, v69)), >(+(v69, 1), 1))
f3572_0_main_InvokeMethod(v71, x30, c0, x29) → f3645_0_main_InvokeMethod(v72, x30, 1, x29) | &&(&&(&&(>(+(v72, 1), 1), <=(v72, v71)), >(+(v71, 1), 1)), =(0, c0))
f3572_0_main_InvokeMethod(v73, x32, c1, x31) → f3645_0_main_InvokeMethod(v74, x32, x31, x31) | &&(&&(&&(>(+(v74, 1), 1), <=(v74, v73)), >(+(v73, 1), 1)), =(1, c1))
f3572_0_main_InvokeMethod(v75, x34, x35, x33) → f3645_0_main_InvokeMethod(v76, x34, x36, x33) | &&(&&(>(+(v76, 1), 1), <=(v76, v75)), >(+(v75, 1), 1))
f3645_0_main_InvokeMethod(v77, x38, c0, x37) → f3292_0_main_Load(v78, +(x38, 1), x37) | &&(&&(&&(&&(>(x38, -1), >(+(v78, 1), 1)), <=(v78, v77)), >(+(v77, 1), 1)), =(0, c0))
f3645_0_main_InvokeMethod(v79, x40, c1, x39) → f3292_0_main_Load(v80, +(x40, 1), x39) | &&(&&(&&(&&(>(x40, -1), >(+(v80, 1), 1)), <=(v80, v79)), >(+(v79, 1), 1)), =(1, c1))
f3645_0_main_InvokeMethod(v81, x42, x43, x41) → f3292_0_main_Load(v82, +(x42, 1), x41) | &&(&&(&&(>(x42, -1), >(+(v82, 1), 1)), <=(v82, v81)), >(+(v81, 1), 1))

(17) Obligation:

Rules:
f3292_0_main_Load(v59, x13, x12) → f3408_0_main_InvokeMethod(v60, x13, 1, x12) | &&(&&(&&(&&(<(x13, x12), >(x12, -1)), >(+(v60, 1), 1)), <=(v60, v59)), >(+(v59, 1), 1))
f3292_0_main_Load(v61, x15, x14) → f3408_0_main_InvokeMethod(v62, x15, x14, x14) | &&(&&(&&(&&(<(x15, x14), >(x14, -1)), >(+(v62, 1), 1)), <=(v62, v61)), >(+(v61, 1), 1))
f3292_0_main_Load(v63, x17, x16) → f3408_0_main_InvokeMethod(v64, x17, x18, x16) | &&(&&(&&(&&(<(x17, x16), >(x16, -1)), >(+(v64, 1), 1)), <=(v64, v63)), >(+(v63, 1), 1))
f3408_0_main_InvokeMethod(v65, x20, c0, x19) → f3572_0_main_InvokeMethod(v66, x20, x21, x19) | &&(&&(&&(&&(&&(&&(>(x21, -1), <(x20, x19)), >(x19, -1)), >(+(v66, 1), 1)), <=(v66, v65)), >(+(v65, 1), 1)), =(0, c0))
f3408_0_main_InvokeMethod(v67, x23, c1, x22) → f3572_0_main_InvokeMethod(v68, x23, x24, x22) | &&(&&(&&(&&(&&(&&(>(x24, -1), <(x23, x22)), >(x22, -1)), >(+(v68, 1), 1)), <=(v68, v67)), >(+(v67, 1), 1)), =(1, c1))
f3408_0_main_InvokeMethod(v69, x26, x27, x25) → f3572_0_main_InvokeMethod(v70, x26, x28, x25) | &&(&&(&&(&&(&&(>(x28, -1), <(x26, x25)), >(x25, -1)), >(+(v70, 1), 1)), <=(v70, v69)), >(+(v69, 1), 1))
f3572_0_main_InvokeMethod(v71, x30, c0, x29) → f3645_0_main_InvokeMethod(v72, x30, 1, x29) | &&(&&(&&(>(+(v72, 1), 1), <=(v72, v71)), >(+(v71, 1), 1)), =(0, c0))
f3572_0_main_InvokeMethod(v73, x32, c1, x31) → f3645_0_main_InvokeMethod(v74, x32, x31, x31) | &&(&&(&&(>(+(v74, 1), 1), <=(v74, v73)), >(+(v73, 1), 1)), =(1, c1))
f3572_0_main_InvokeMethod(v75, x34, x35, x33) → f3645_0_main_InvokeMethod(v76, x34, x36, x33) | &&(&&(>(+(v76, 1), 1), <=(v76, v75)), >(+(v75, 1), 1))
f3645_0_main_InvokeMethod(v77, x38, c0, x37) → f3292_0_main_Load(v78, +(x38, 1), x37) | &&(&&(&&(&&(>(x38, -1), >(+(v78, 1), 1)), <=(v78, v77)), >(+(v77, 1), 1)), =(0, c0))
f3645_0_main_InvokeMethod(v79, x40, c1, x39) → f3292_0_main_Load(v80, +(x40, 1), x39) | &&(&&(&&(&&(>(x40, -1), >(+(v80, 1), 1)), <=(v80, v79)), >(+(v79, 1), 1)), =(1, c1))
f3645_0_main_InvokeMethod(v81, x42, x43, x41) → f3292_0_main_Load(v82, +(x42, 1), x41) | &&(&&(&&(>(x42, -1), >(+(v82, 1), 1)), <=(v82, v81)), >(+(v81, 1), 1))

(18) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:

[f3292_0_main_Load(x63, x65, x67)] = 1 - 2·x65 + 2·x67
[f3408_0_main_InvokeMethod(x70, x72, x74, x76)] = -2·x72 + 2·x76
[f3572_0_main_InvokeMethod(x79, x81, x83, x85)] = -1 - 2·x81 + 2·x85
[f3645_0_main_InvokeMethod(x88, x90, x92, x94)] = -1 - 2·x90 + 2·x94

Therefore the following rule(s) have been dropped:

f3292_0_main_Load(x0, x1, x2) → f3408_0_main_InvokeMethod(x3, x1, 1, x2) | &&(&&(&&(&&(<(x1, x2), >(x2, -1)), >(+(x3, 1), 1)), <=(x3, x0)), >(+(x0, 1), 1))
f3292_0_main_Load(x4, x5, x6) → f3408_0_main_InvokeMethod(x7, x5, x6, x6) | &&(&&(&&(&&(<(x5, x6), >(x6, -1)), >(+(x7, 1), 1)), <=(x7, x4)), >(+(x4, 1), 1))
f3292_0_main_Load(x8, x9, x10) → f3408_0_main_InvokeMethod(x11, x9, x12, x10) | &&(&&(&&(&&(<(x9, x10), >(x10, -1)), >(+(x11, 1), 1)), <=(x11, x8)), >(+(x8, 1), 1))
f3408_0_main_InvokeMethod(x13, x14, x15, x16) → f3572_0_main_InvokeMethod(x17, x14, x18, x16) | &&(&&(&&(&&(&&(&&(>(x18, -1), <(x14, x16)), >(x16, -1)), >(+(x17, 1), 1)), <=(x17, x13)), >(+(x13, 1), 1)), =(0, x15))
f3408_0_main_InvokeMethod(x19, x20, x21, x22) → f3572_0_main_InvokeMethod(x23, x20, x24, x22) | &&(&&(&&(&&(&&(&&(>(x24, -1), <(x20, x22)), >(x22, -1)), >(+(x23, 1), 1)), <=(x23, x19)), >(+(x19, 1), 1)), =(1, x21))
f3408_0_main_InvokeMethod(x25, x26, x27, x28) → f3572_0_main_InvokeMethod(x29, x26, x30, x28) | &&(&&(&&(&&(&&(>(x30, -1), <(x26, x28)), >(x28, -1)), >(+(x29, 1), 1)), <=(x29, x25)), >(+(x25, 1), 1))

(19) Obligation:

Rules:
f3572_0_main_InvokeMethod(x31, x32, x33, x34) → f3645_0_main_InvokeMethod(x35, x32, 1, x34) | &&(&&(&&(>(+(x35, 1), 1), <=(x35, x31)), >(+(x31, 1), 1)), =(0, x33))
f3572_0_main_InvokeMethod(x36, x37, x38, x39) → f3645_0_main_InvokeMethod(x40, x37, x39, x39) | &&(&&(&&(>(+(x40, 1), 1), <=(x40, x36)), >(+(x36, 1), 1)), =(1, x38))
f3572_0_main_InvokeMethod(x41, x42, x43, x44) → f3645_0_main_InvokeMethod(x45, x42, x46, x44) | &&(&&(>(+(x45, 1), 1), <=(x45, x41)), >(+(x41, 1), 1))
f3645_0_main_InvokeMethod(x47, x48, x49, x50) → f3292_0_main_Load(x51, +(x48, 1), x50) | &&(&&(&&(&&(>(x48, -1), >(+(x51, 1), 1)), <=(x51, x47)), >(+(x47, 1), 1)), =(0, x49))
f3645_0_main_InvokeMethod(x52, x53, x54, x55) → f3292_0_main_Load(x56, +(x53, 1), x55) | &&(&&(&&(&&(>(x53, -1), >(+(x56, 1), 1)), <=(x56, x52)), >(+(x52, 1), 1)), =(1, x54))
f3645_0_main_InvokeMethod(x57, x58, x59, x60) → f3292_0_main_Load(x61, +(x58, 1), x60) | &&(&&(&&(>(x58, -1), >(+(x61, 1), 1)), <=(x61, x57)), >(+(x57, 1), 1))

(20) TerminationGraphProcessor (EQUIVALENT transformation)

Constructed the termination graph and obtained no non-trivial SCC(s).

(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 (SOUND transformation)

(19) Obligation:

(20) TerminationGraphProcessor (EQUIVALENT transformation)

(21) YES