Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 489 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 AND
    ↳5 JBCTerminationSCC
        ↳6 SCCToIntTRSProof (⇒, 51 ms)
        ↳7 intTRS
        ↳8 PolynomialOrderProcessor (⇔, 0 ms)
        ↳9 YES
    ↳10 JBCTerminationSCC
        ↳11 SCCToIntTRSProof (⇒, 286 ms)
        ↳12 intTRS
        ↳13 PolynomialOrderProcessor (⇔, 0 ms)
        ↳14 YES
    ↳15 JBCTerminationSCC
        ↳16 SCCToIntTRSProof (⇒, 368 ms)
        ↳17 intTRS
        ↳18 PolynomialOrderProcessor (⇔, 0 ms)
        ↳19 YES
    ↳20 JBCTerminationSCC
        ↳21 SCCToIntTRSProof (⇒, 124 ms)
        ↳22 intTRS
        ↳23 PolynomialOrderProcessor (⇔, 5 ms)
        ↳24 YES
    ↳25 JBCTerminationSCC
        ↳26 SCCToIntTRSProof (⇒, 176 ms)
        ↳27 intTRS
        ↳28 PolynomialOrderProcessor (⇔, 0 ms)
        ↳29 YES
    ↳30 JBCTerminationSCC
        ↳31 SCCToIntTRSProof (⇒, 181 ms)
        ↳32 intTRS
        ↳33 PolynomialOrderProcessor (⇔, 0 ms)
        ↳34 YES

(0) Obligation:

JBC Problem based on JBC Program:
public class Recursions {
    public static void main(String args[]) {
	for (int i = 0; i < args.length; i++)
	    rec0(0, args.length);
    }

    public static void rec0(int i, int stop) {
        if (i <= stop) {
            rec1(0, 2*i, i);
            rec0(i+1, stop);
        }
    }

    public static void rec1(int j, int stop, int i) {
        if (j <= stop) {
            rec2(i+j, 0, i, j);
            rec1(j+1, stop, i);
        }
    }

    public static void rec2(int k, int stop, int i, int j) {
        if (k >= stop) {
            rec3(0, 2*i + 3*j + 4*k, i, j ,k);
            rec2(k-1, stop, i, j);
        }
    }

    public static void rec3(int l, int stop, int i, int j, int k) {
        if (l <= stop) {
            rec4(1000*i+100*j+10*k+l, 0);
            rec3(l+1, stop, i, j, k);
        }
    }

    public static void rec4(int m, int stop) {
        if (m >= stop)
            rec4(m-1, stop);
    }
}


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

Recursions.rec0(II)V: Graph of 28 nodes with 0 SCCs.

Recursions.rec1(III)V: Graph of 29 nodes with 0 SCCs.

Recursions.rec2(IIII)V: Graph of 41 nodes with 0 SCCs.

Recursions.rec3(IIIII)V: Graph of 38 nodes with 0 SCCs.

Recursions.rec4(II)V: Graph of 19 nodes with 0 SCCs.


(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 6 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Recursions.rec4(II)V
SCC calls the following helper methods: Recursions.rec4(II)V
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 12 IRules

P rules:
f1003_0_rec4_Load(EOS, i135, matching1, i135, matching2, i135) → f1010_0_rec4_LT(EOS, i135, 0, i135, 0, i135, 0) | &&(=(matching1, 0), =(matching2, 0))
f1010_0_rec4_LT(EOS, i140, matching1, i140, matching2, i140, matching3) → f1014_0_rec4_LT(EOS, i140, 0, i140, 0, i140, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f1014_0_rec4_LT(EOS, i140, matching1, i140, matching2, i140, matching3) → f1034_0_rec4_Load(EOS, i140, 0, i140, 0) | &&(&&(&&(>=(i140, 0), =(matching1, 0)), =(matching2, 0)), =(matching3, 0))
f1034_0_rec4_Load(EOS, i140, matching1, i140, matching2) → f1046_0_rec4_ConstantStackPush(EOS, i140, 0, 0, i140) | &&(=(matching1, 0), =(matching2, 0))
f1046_0_rec4_ConstantStackPush(EOS, i140, matching1, matching2, i140) → f1067_0_rec4_IntArithmetic(EOS, i140, 0, 0, i140, 1) | &&(=(matching1, 0), =(matching2, 0))
f1067_0_rec4_IntArithmetic(EOS, i140, matching1, matching2, i140, matching3) → f1074_0_rec4_Load(EOS, i140, 0, 0, -(i140, 1)) | &&(&&(&&(>=(i140, 0), =(matching1, 0)), =(matching2, 0)), =(matching3, 1))
f1074_0_rec4_Load(EOS, i140, matching1, matching2, i174) → f1084_0_rec4_InvokeMethod(EOS, i140, 0, i174, 0) | &&(=(matching1, 0), =(matching2, 0))
f1084_0_rec4_InvokeMethod(EOS, i140, matching1, i174, matching2) → f1089_0_rec4_Load(EOS, i174, 0, i174, 0) | &&(=(matching1, 0), =(matching2, 0))
f1084_0_rec4_InvokeMethod(EOS, i140, matching1, i174, matching2) → f1089_1_rec4_Load(EOS, i140, 0, i174, 0, i174, 0) | &&(=(matching1, 0), =(matching2, 0))
f1089_0_rec4_Load(EOS, i174, matching1, i174, matching2) → f1093_0_rec4_Load(EOS, i174, 0, i174, 0) | &&(=(matching1, 0), =(matching2, 0))
f1093_0_rec4_Load(EOS, i174, matching1, i174, matching2) → f998_0_rec4_Load(EOS, i174, 0, i174, 0) | &&(=(matching1, 0), =(matching2, 0))
f998_0_rec4_Load(EOS, i135, matching1, i135, matching2) → f1003_0_rec4_Load(EOS, i135, 0, i135, 0, i135) | &&(=(matching1, 0), =(matching2, 0))

Combined rules. Obtained 2 IRules

P rules:
f1003_0_rec4_Load(EOS, x0, 0, x0, 0, x0) → f1089_1_rec4_Load(EOS, x0, 0, -(x0, 1), 0, -(x0, 1), 0) | >(+(x0, 1), 0)
f1003_0_rec4_Load(EOS, x0, 0, x0, 0, x0) → f1003_0_rec4_Load(EOS, -(x0, 1), 0, -(x0, 1), 0, -(x0, 1)) | >(+(x0, 1), 0)

Filtered ground terms:


f1003_0_rec4_Load(x1, x2, x3, x4, x5, x6) → f1003_0_rec4_Load(x2, x4, x6)
Cond_f1003_0_rec4_Load(x1, x2, x3, x4, x5, x6, x7) → Cond_f1003_0_rec4_Load(x1, x3, x5, x7)
f1089_1_rec4_Load(x1, x2, x3, x4, x5, x6, x7) → f1089_1_rec4_Load(x2, x4, x6)
Cond_f1003_0_rec4_Load1(x1, x2, x3, x4, x5, x6, x7) → Cond_f1003_0_rec4_Load1(x1, x3, x5, x7)

Filtered duplicate terms:


f1003_0_rec4_Load(x1, x2, x3) → f1003_0_rec4_Load(x3)
Cond_f1003_0_rec4_Load(x1, x2, x3, x4) → Cond_f1003_0_rec4_Load(x1, x4)
f1089_1_rec4_Load(x1, x2, x3) → f1089_1_rec4_Load(x3)
Cond_f1003_0_rec4_Load1(x1, x2, x3, x4) → Cond_f1003_0_rec4_Load1(x1, x4)

Filtered unneeded terms:


Cond_f1003_0_rec4_Load(x1, x2) → Cond_f1003_0_rec4_Load(x1)

Prepared 2 rules for path length conversion:

P rules:
f1003_0_rec4_Load(x0) → f1089_1_rec4_Load(-(x0, 1)) | >(+(x0, 1), 0)
f1003_0_rec4_Load(x0) → f1003_0_rec4_Load(-(x0, 1)) | >(+(x0, 1), 0)

Finished conversion. Obtained 1 rules.

P rules:
f1003_0_rec4_Load(x1) → f1003_0_rec4_Load(-(x1, 1)) | >(x1, -1)

(7) Obligation:

Rules:
f1003_0_rec4_Load(x1) → f1003_0_rec4_Load(-(x1, 1)) | >(x1, -1)

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f1003_0_rec4_Load(x2)] = x2

Therefore the following rule(s) have been dropped:


f1003_0_rec4_Load(x0) → f1003_0_rec4_Load(-(x0, 1)) | >(x0, -1)

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Recursions.rec3(IIIII)V
SCC calls the following helper methods: Recursions.rec4(II)V, Recursions.rec3(IIIII)V
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 34 IRules

P rules:
f1371_0_rec3_Load(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i368) → f1373_0_rec3_GT(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i368, i68)
f1373_0_rec3_GT(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i368, i68) → f1377_0_rec3_GT(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i368, i68)
f1377_0_rec3_GT(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i368, i68) → f1382_0_rec3_ConstantStackPush(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71) | <=(i368, i68)
f1382_0_rec3_ConstantStackPush(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71) → f1387_0_rec3_Load(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, 1000)
f1387_0_rec3_Load(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, matching1) → f1389_0_rec3_IntArithmetic(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, 1000, i69) | =(matching1, 1000)
f1389_0_rec3_IntArithmetic(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, matching1, i69) → f1390_0_rec3_ConstantStackPush(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, *(1000, i69)) | =(matching1, 1000)
f1390_0_rec3_ConstantStackPush(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i371) → f1395_0_rec3_Load(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i371, 100)
f1395_0_rec3_Load(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i371, matching1) → f1397_0_rec3_IntArithmetic(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i371, 100, i70) | =(matching1, 100)
f1397_0_rec3_IntArithmetic(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i371, matching1, i70) → f1400_0_rec3_IntArithmetic(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i371, *(100, i70)) | =(matching1, 100)
f1400_0_rec3_IntArithmetic(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i371, i390) → f1402_0_rec3_ConstantStackPush(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, +(i371, i390)) | &&(>=(i371, 0), >=(i390, 0))
f1402_0_rec3_ConstantStackPush(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i391) → f1405_0_rec3_Load(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i391, 10)
f1405_0_rec3_Load(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i391, matching1) → f1408_0_rec3_IntArithmetic(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i391, 10, i71) | =(matching1, 10)
f1408_0_rec3_IntArithmetic(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i391, matching1, i71) → f1410_0_rec3_IntArithmetic(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i391, *(10, i71)) | =(matching1, 10)
f1410_0_rec3_IntArithmetic(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i391, i393) → f1412_0_rec3_Load(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, +(i391, i393)) | &&(>=(i391, 0), >=(i393, 0))
f1412_0_rec3_Load(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i394) → f1415_0_rec3_IntArithmetic(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i394, i368)
f1415_0_rec3_IntArithmetic(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i394, i368) → f1417_0_rec3_ConstantStackPush(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, +(i394, i368)) | &&(>=(i394, 0), >=(i368, 0))
f1417_0_rec3_ConstantStackPush(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i395) → f1420_0_rec3_InvokeMethod(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i395, 0)
f1420_0_rec3_InvokeMethod(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i395, matching1) → f1421_0_rec4_Load(EOS, i395, 0, i395, 0) | =(matching1, 0)
f1420_0_rec3_InvokeMethod(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i395, matching1) → f1421_1_rec4_Load(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i395, 0, i395, 0) | =(matching1, 0)
f1421_0_rec4_Load(EOS, i395, matching1, i395, matching2) → f1426_0_rec4_Load(EOS, i395, 0, i395, 0) | &&(=(matching1, 0), =(matching2, 0))
f1438_0_rec4_Return(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i414, matching1) → f1443_0_rec3_Load(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71) | =(matching1, 0)
f1443_0_rec3_Load(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71) → f1449_0_rec3_ConstantStackPush(EOS, i368, i68, i69, i70, i71, i68, i69, i70, i71, i368)
f1449_0_rec3_ConstantStackPush(EOS, i368, i68, i69, i70, i71, i68, i69, i70, i71, i368) → f1453_0_rec3_IntArithmetic(EOS, i368, i68, i69, i70, i71, i68, i69, i70, i71, i368, 1)
f1453_0_rec3_IntArithmetic(EOS, i368, i68, i69, i70, i71, i68, i69, i70, i71, i368, matching1) → f1457_0_rec3_Load(EOS, i368, i68, i69, i70, i71, i68, i69, i70, i71, +(i368, 1)) | &&(>=(i368, 0), =(matching1, 1))
f1457_0_rec3_Load(EOS, i368, i68, i69, i70, i71, i68, i69, i70, i71, i438) → f1461_0_rec3_Load(EOS, i368, i68, i69, i70, i71, i69, i70, i71, i438, i68)
f1461_0_rec3_Load(EOS, i368, i68, i69, i70, i71, i69, i70, i71, i438, i68) → f1467_0_rec3_Load(EOS, i368, i68, i69, i70, i71, i70, i71, i438, i68, i69)
f1467_0_rec3_Load(EOS, i368, i68, i69, i70, i71, i70, i71, i438, i68, i69) → f1471_0_rec3_Load(EOS, i368, i68, i69, i70, i71, i71, i438, i68, i69, i70)
f1471_0_rec3_Load(EOS, i368, i68, i69, i70, i71, i71, i438, i68, i69, i70) → f1473_0_rec3_InvokeMethod(EOS, i368, i68, i69, i70, i71, i438, i68, i69, i70, i71)
f1473_0_rec3_InvokeMethod(EOS, i368, i68, i69, i70, i71, i438, i68, i69, i70, i71) → f1476_0_rec3_Load(EOS, i438, i68, i69, i70, i71, i438, i68, i69, i70, i71)
f1473_0_rec3_InvokeMethod(EOS, i368, i68, i69, i70, i71, i438, i68, i69, i70, i71) → f1476_1_rec3_Load(EOS, i368, i68, i69, i70, i71, i438, i68, i69, i70, i71, i438, i68, i69, i70, i71)
f1476_0_rec3_Load(EOS, i438, i68, i69, i70, i71, i438, i68, i69, i70, i71) → f1478_0_rec3_Load(EOS, i438, i68, i69, i70, i71, i438, i68, i69, i70, i71)
f1478_0_rec3_Load(EOS, i438, i68, i69, i70, i71, i438, i68, i69, i70, i71) → f1368_0_rec3_Load(EOS, i438, i68, i69, i70, i71, i438, i68, i69, i70, i71)
f1368_0_rec3_Load(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71) → f1371_0_rec3_Load(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i368)
f1421_1_rec4_Load(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i414, matching1, i414, matching2) → f1438_0_rec4_Return(EOS, i368, i68, i69, i70, i71, i368, i68, i69, i70, i71, i414, 0) | &&(=(matching1, 0), =(matching2, 0))

Combined rules. Obtained 3 IRules

P rules:
f1438_0_rec4_Return(EOS, x0, x1, x2, x3, x4, x0, x1, x2, x3, x4, x5, 0) → f1476_1_rec3_Load(EOS, x0, x1, x2, x3, x4, +(x0, 1), x1, x2, x3, x4, +(x0, 1), x1, x2, x3, x4) | >(+(x0, 1), 0)
f1438_0_rec4_Return(EOS, x0, x1, x2, x3, x4, x0, x1, x2, x3, x4, x5, 0) → f1426_0_rec4_Load(EOS, +(+(+(*(1000, x2), *(100, x3)), *(10, x4)), +(x0, 1)), 0, +(+(+(*(1000, x2), *(100, x3)), *(10, x4)), +(x0, 1)), 0) | &&(&&(&&(&&(&&(&&(>=(x1, +(x0, 1)), >(+(x0, 1), 0)), >=(*(1000, x2), 0)), >=(+(*(1000, x2), *(100, x3)), 0)), >=(+(+(*(1000, x2), *(100, x3)), *(10, x4)), 0)), >=(*(10, x4), 0)), >=(*(100, x3), 0))
f1438_0_rec4_Return(EOS, x0, x1, x2, x3, x4, x0, x1, x2, x3, x4, x5, 0) → f1438_0_rec4_Return(EOS, +(x0, 1), x1, x2, x3, x4, +(x0, 1), x1, x2, x3, x4, +(+(+(*(1000, x2), *(100, x3)), *(10, x4)), +(x0, 1)), 0) | &&(&&(&&(&&(&&(&&(>=(x1, +(x0, 1)), >(+(x0, 1), 0)), >=(*(1000, x2), 0)), >=(+(*(1000, x2), *(100, x3)), 0)), >=(+(+(*(1000, x2), *(100, x3)), *(10, x4)), 0)), >=(*(10, x4), 0)), >=(*(100, x3), 0))

Filtered ground terms:


f1438_0_rec4_Return(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) → f1438_0_rec4_Return(x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
Cond_f1438_0_rec4_Return(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14) → Cond_f1438_0_rec4_Return(x1, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)
f1476_1_rec3_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16) → f1476_1_rec3_Load(x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16)
Cond_f1438_0_rec4_Return1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14) → Cond_f1438_0_rec4_Return1(x1, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)
f1426_0_rec4_Load(x1, x2, x3, x4, x5) → f1426_0_rec4_Load(x2, x4)
Cond_f1438_0_rec4_Return2(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14) → Cond_f1438_0_rec4_Return2(x1, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)

Filtered duplicate terms:


f1438_0_rec4_Return(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) → f1438_0_rec4_Return(x6, x7, x8, x9, x10, x11)
Cond_f1438_0_rec4_Return(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) → Cond_f1438_0_rec4_Return(x1, x7, x8, x9, x10, x11, x12)
f1476_1_rec3_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) → f1476_1_rec3_Load(x11, x12, x13, x14, x15)
Cond_f1438_0_rec4_Return1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) → Cond_f1438_0_rec4_Return1(x1, x7, x8, x9, x10, x11, x12)
f1426_0_rec4_Load(x1, x2) → f1426_0_rec4_Load(x2)
Cond_f1438_0_rec4_Return2(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) → Cond_f1438_0_rec4_Return2(x1, x7, x8, x9, x10, x11, x12)

Filtered unneeded terms:


Cond_f1438_0_rec4_Return(x1, x2, x3, x4, x5, x6, x7) → Cond_f1438_0_rec4_Return(x1)
Cond_f1438_0_rec4_Return1(x1, x2, x3, x4, x5, x6, x7) → Cond_f1438_0_rec4_Return1(x1)
Cond_f1438_0_rec4_Return2(x1, x2, x3, x4, x5, x6, x7) → Cond_f1438_0_rec4_Return2(x1, x2, x3, x4, x5, x6)
f1438_0_rec4_Return(x1, x2, x3, x4, x5, x6) → f1438_0_rec4_Return(x1, x2, x3, x4, x5)

Prepared 3 rules for path length conversion:

P rules:
f1438_0_rec4_Return(x0, x1, x2, x3, x4) → f1476_1_rec3_Load(+(x0, 1), x1, x2, x3, x4) | >(+(x0, 1), 0)
f1438_0_rec4_Return(x0, x1, x2, x3, x4) → f1426_0_rec4_Load(+(+(+(*(1000, x2), *(100, x3)), *(10, x4)), +(x0, 1))) | &&(&&(&&(&&(&&(&&(>=(x1, +(x0, 1)), >(+(x0, 1), 0)), >=(*(1000, x2), 0)), >=(+(*(1000, x2), *(100, x3)), 0)), >=(+(+(*(1000, x2), *(100, x3)), *(10, x4)), 0)), >=(*(10, x4), 0)), >=(*(100, x3), 0))
f1438_0_rec4_Return(x0, x1, x2, x3, x4) → f1438_0_rec4_Return(+(x0, 1), x1, x2, x3, x4) | &&(&&(&&(&&(&&(&&(>=(x1, +(x0, 1)), >(+(x0, 1), 0)), >=(*(1000, x2), 0)), >=(+(*(1000, x2), *(100, x3)), 0)), >=(+(+(*(1000, x2), *(100, x3)), *(10, x4)), 0)), >=(*(10, x4), 0)), >=(*(100, x3), 0))

Finished conversion. Obtained 1 rules.

P rules:
f1438_0_rec4_Return(x10, x11, x12, x13, x14) → f1438_0_rec4_Return(+(x10, 1), x11, x12, x13, x14) | &&(&&(&&(&&(&&(&&(>=(x11, +(x10, 1)), >(x10, -1)), >=(*(1000, x12), 0)), >=(+(*(1000, x12), *(100, x13)), 0)), >=(+(+(*(1000, x12), *(100, x13)), *(10, x14)), 0)), >=(*(10, x14), 0)), >=(*(100, x13), 0))

(12) Obligation:

Rules:
f1438_0_rec4_Return(x10, x11, x12, x13, x14) → f1438_0_rec4_Return(+(x10, 1), x11, x12, x13, x14) | &&(&&(&&(&&(&&(&&(>=(x11, +(x10, 1)), >(x10, -1)), >=(*(1000, x12), 0)), >=(+(*(1000, x12), *(100, x13)), 0)), >=(+(+(*(1000, x12), *(100, x13)), *(10, x14)), 0)), >=(*(10, x14), 0)), >=(*(100, x13), 0))

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f1438_0_rec4_Return(x6, x8, x10, x12, x14)] = -x6 + x8

Therefore the following rule(s) have been dropped:


f1438_0_rec4_Return(x0, x1, x2, x3, x4) → f1438_0_rec4_Return(+(x0, 1), x1, x2, x3, x4) | &&(&&(&&(&&(&&(&&(>=(x1, +(x0, 1)), >(x0, -1)), >=(*(1000, x2), 0)), >=(+(*(1000, x2), *(100, x3)), 0)), >=(+(+(*(1000, x2), *(100, x3)), *(10, x4)), 0)), >=(*(10, x4), 0)), >=(*(100, x3), 0))

(14) YES

(15) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Recursions.rec2(IIII)V
SCC calls the following helper methods: Recursions.rec3(IIIII)V, Recursions.rec2(IIII)V, Recursions.rec4(II)V
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
  • Marker field analysis yielded the following relations that could be markers:

(16) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 36 IRules

P rules:
f1326_0_rec2_Load(EOS, i341, matching1, i342, i343, i341, matching2, i342, i343, i341) → f1327_0_rec2_LT(EOS, i341, 0, i342, i343, i341, 0, i342, i343, i341, 0) | &&(=(matching1, 0), =(matching2, 0))
f1327_0_rec2_LT(EOS, i354, matching1, i342, i343, i354, matching2, i342, i343, i354, matching3) → f1334_0_rec2_LT(EOS, i354, 0, i342, i343, i354, 0, i342, i343, i354, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f1334_0_rec2_LT(EOS, i354, matching1, i342, i343, i354, matching2, i342, i343, i354, matching3) → f1338_0_rec2_ConstantStackPush(EOS, i354, 0, i342, i343, i354, 0, i342, i343) | &&(&&(&&(>=(i354, 0), =(matching1, 0)), =(matching2, 0)), =(matching3, 0))
f1338_0_rec2_ConstantStackPush(EOS, i354, matching1, i342, i343, i354, matching2, i342, i343) → f1343_0_rec2_ConstantStackPush(EOS, i354, 0, i342, i343, i354, 0, i342, i343, 0) | &&(=(matching1, 0), =(matching2, 0))
f1343_0_rec2_ConstantStackPush(EOS, i354, matching1, i342, i343, i354, matching2, i342, i343, matching3) → f1349_0_rec2_Load(EOS, i354, 0, i342, i343, i354, 0, i342, i343, 0, 2) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f1349_0_rec2_Load(EOS, i354, matching1, i342, i343, i354, matching2, i342, i343, matching3, matching4) → f1352_0_rec2_IntArithmetic(EOS, i354, 0, i342, i343, i354, 0, i342, i343, 0, 2, i342) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 2))
f1352_0_rec2_IntArithmetic(EOS, i354, matching1, i342, i343, i354, matching2, i342, i343, matching3, matching4, i342) → f1354_0_rec2_ConstantStackPush(EOS, i354, 0, i342, i343, i354, 0, i342, i343, 0, *(2, i342)) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 2))
f1354_0_rec2_ConstantStackPush(EOS, i354, matching1, i342, i343, i354, matching2, i342, i343, matching3, i365) → f1357_0_rec2_Load(EOS, i354, 0, i342, i343, i354, 0, i342, i343, 0, i365, 3) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f1357_0_rec2_Load(EOS, i354, matching1, i342, i343, i354, matching2, i342, i343, matching3, i365, matching4) → f1359_0_rec2_IntArithmetic(EOS, i354, 0, i342, i343, i354, 0, i342, i343, 0, i365, 3, i343) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 3))
f1359_0_rec2_IntArithmetic(EOS, i354, matching1, i342, i343, i354, matching2, i342, i343, matching3, i365, matching4, i343) → f1361_0_rec2_IntArithmetic(EOS, i354, 0, i342, i343, i354, 0, i342, i343, 0, i365, *(3, i343)) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 3))
f1361_0_rec2_IntArithmetic(EOS, i354, matching1, i342, i343, i354, matching2, i342, i343, matching3, i365, i366) → f1364_0_rec2_ConstantStackPush(EOS, i354, 0, i342, i343, i354, 0, i342, i343, 0, +(i365, i366)) | &&(&&(&&(&&(>=(i365, 0), >=(i366, 0)), =(matching1, 0)), =(matching2, 0)), =(matching3, 0))
f1364_0_rec2_ConstantStackPush(EOS, i354, matching1, i342, i343, i354, matching2, i342, i343, matching3, i367) → f1365_0_rec2_Load(EOS, i354, 0, i342, i343, i354, 0, i342, i343, 0, i367, 4) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f1365_0_rec2_Load(EOS, i354, matching1, i342, i343, i354, matching2, i342, i343, matching3, i367, matching4) → f1369_0_rec2_IntArithmetic(EOS, i354, 0, i342, i343, i354, 0, i342, i343, 0, i367, 4, i354) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 4))
f1369_0_rec2_IntArithmetic(EOS, i354, matching1, i342, i343, i354, matching2, i342, i343, matching3, i367, matching4, i354) → f1372_0_rec2_IntArithmetic(EOS, i354, 0, i342, i343, i354, 0, i342, i343, 0, i367, *(4, i354)) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 4))
f1372_0_rec2_IntArithmetic(EOS, i354, matching1, i342, i343, i354, matching2, i342, i343, matching3, i367, i369) → f1374_0_rec2_Load(EOS, i354, 0, i342, i343, i354, 0, i342, i343, 0, +(i367, i369)) | &&(&&(&&(&&(>=(i367, 0), >=(i369, 0)), =(matching1, 0)), =(matching2, 0)), =(matching3, 0))
f1374_0_rec2_Load(EOS, i354, matching1, i342, i343, i354, matching2, i342, i343, matching3, i370) → f1378_0_rec2_Load(EOS, i354, 0, i342, i343, i354, 0, i342, i343, 0, i370, i342) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f1378_0_rec2_Load(EOS, i354, matching1, i342, i343, i354, matching2, i342, i343, matching3, i370, i342) → f1381_0_rec2_Load(EOS, i354, 0, i342, i343, i354, 0, i342, i343, 0, i370, i342, i343) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f1381_0_rec2_Load(EOS, i354, matching1, i342, i343, i354, matching2, i342, i343, matching3, i370, i342, i343) → f1383_0_rec2_InvokeMethod(EOS, i354, 0, i342, i343, i354, 0, i342, i343, 0, i370, i342, i343, i354) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f1383_0_rec2_InvokeMethod(EOS, i354, matching1, i342, i343, i354, matching2, i342, i343, matching3, i370, i342, i343, i354) → f1385_0_rec3_Load(EOS, 0, i370, i342, i343, i354, 0, i370, i342, i343, i354) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f1383_0_rec2_InvokeMethod(EOS, i354, matching1, i342, i343, i354, matching2, i342, i343, matching3, i370, i342, i343, i354) → f1385_1_rec3_Load(EOS, i354, 0, i342, i343, i354, 0, i342, i343, 0, i370, i342, i343, i354, 0, i370, i342, i343, i354) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f1385_0_rec3_Load(EOS, matching1, i370, i342, i343, i354, matching2, i370, i342, i343, i354) → f1388_0_rec3_Load(EOS, 0, i370, i342, i343, i354, 0, i370, i342, i343, i354) | &&(=(matching1, 0), =(matching2, 0))
f1396_0_rec3_Return(EOS, i387, matching1, i383, i385, i387, matching2, i383, i385, matching3, i389, i383, i385, i387) → f1399_0_rec2_Load(EOS, i387, 0, i383, i385, i387, 0, i383, i385) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f1399_0_rec2_Load(EOS, i387, matching1, i383, i385, i387, matching2, i383, i385) → f1401_0_rec2_ConstantStackPush(EOS, i387, 0, i383, i385, 0, i383, i385, i387) | &&(=(matching1, 0), =(matching2, 0))
f1401_0_rec2_ConstantStackPush(EOS, i387, matching1, i383, i385, matching2, i383, i385, i387) → f1404_0_rec2_IntArithmetic(EOS, i387, 0, i383, i385, 0, i383, i385, i387, 1) | &&(=(matching1, 0), =(matching2, 0))
f1404_0_rec2_IntArithmetic(EOS, i387, matching1, i383, i385, matching2, i383, i385, i387, matching3) → f1406_0_rec2_Load(EOS, i387, 0, i383, i385, 0, i383, i385, -(i387, 1)) | &&(&&(&&(>=(i387, 0), =(matching1, 0)), =(matching2, 0)), =(matching3, 1))
f1406_0_rec2_Load(EOS, i387, matching1, i383, i385, matching2, i383, i385, i392) → f1409_0_rec2_Load(EOS, i387, 0, i383, i385, i383, i385, i392, 0) | &&(=(matching1, 0), =(matching2, 0))
f1409_0_rec2_Load(EOS, i387, matching1, i383, i385, i383, i385, i392, matching2) → f1411_0_rec2_Load(EOS, i387, 0, i383, i385, i385, i392, 0, i383) | &&(=(matching1, 0), =(matching2, 0))
f1411_0_rec2_Load(EOS, i387, matching1, i383, i385, i385, i392, matching2, i383) → f1414_0_rec2_InvokeMethod(EOS, i387, 0, i383, i385, i392, 0, i383, i385) | &&(=(matching1, 0), =(matching2, 0))
f1414_0_rec2_InvokeMethod(EOS, i387, matching1, i383, i385, i392, matching2, i383, i385) → f1416_0_rec2_Load(EOS, i392, 0, i383, i385, i392, 0, i383, i385) | &&(=(matching1, 0), =(matching2, 0))
f1414_0_rec2_InvokeMethod(EOS, i387, matching1, i383, i385, i392, matching2, i383, i385) → f1416_1_rec2_Load(EOS, i387, 0, i383, i385, i392, 0, i383, i385, i392, 0, i383, i385) | &&(=(matching1, 0), =(matching2, 0))
f1416_0_rec2_Load(EOS, i392, matching1, i383, i385, i392, matching2, i383, i385) → f1419_0_rec2_Load(EOS, i392, 0, i383, i385, i392, 0, i383, i385) | &&(=(matching1, 0), =(matching2, 0))
f1419_0_rec2_Load(EOS, i392, matching1, i383, i385, i392, matching2, i383, i385) → f1323_0_rec2_Load(EOS, i392, 0, i383, i385, i392, 0, i383, i385) | &&(=(matching1, 0), =(matching2, 0))
f1323_0_rec2_Load(EOS, i341, matching1, i342, i343, i341, matching2, i342, i343) → f1326_0_rec2_Load(EOS, i341, 0, i342, i343, i341, 0, i342, i343, i341) | &&(=(matching1, 0), =(matching2, 0))
f1504_0_rec3_Return(EOS, i515, matching1, i511, i513, i515, matching2, i511, i513, matching3, i517, i511, i513, i515) → f1396_0_rec3_Return(EOS, i515, 0, i511, i513, i515, 0, i511, i513, 0, i517, i511, i513, i515) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f1385_1_rec3_Load(EOS, i387, matching1, i383, i385, i387, matching2, i383, i385, matching3, i389, i383, i385, i387, matching4, i389, i383, i385, i387) → f1396_0_rec3_Return(EOS, i387, 0, i383, i385, i387, 0, i383, i385, 0, i389, i383, i385, i387) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
f1385_1_rec3_Load(EOS, i515, matching1, i511, i513, i515, matching2, i511, i513, matching3, i517, i511, i513, i515, matching4, i517, i511, i513, i515) → f1504_0_rec3_Return(EOS, i515, 0, i511, i513, i515, 0, i511, i513, 0, i517, i511, i513, i515) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))

Combined rules. Obtained 3 IRules

P rules:
f1396_0_rec3_Return(EOS, x0, 0, x2, x3, x0, 0, x2, x3, 0, x6, x2, x3, x0) → f1416_1_rec2_Load(EOS, x0, 0, x2, x3, -(x0, 1), 0, x2, x3, -(x0, 1), 0, x2, x3) | >(+(x0, 1), 0)
f1396_0_rec3_Return(EOS, x0, 0, x2, x3, x0, 0, x2, x3, 0, x6, x2, x3, x0) → f1388_0_rec3_Load(EOS, 0, +(+(*(2, x2), *(3, x3)), *(4, -(x0, 1))), x2, x3, -(x0, 1), 0, +(+(*(2, x2), *(3, x3)), *(4, -(x0, 1))), x2, x3, -(x0, 1)) | &&(&&(&&(&&(>(+(x0, 1), 1), >=(*(4, -(x0, 1)), 0)), >=(*(3, x3), 0)), >=(+(*(2, x2), *(3, x3)), 0)), >=(*(2, x2), 0))
f1396_0_rec3_Return(EOS, x0, 0, x2, x3, x0, 0, x2, x3, 0, x6, x2, x3, x0) → f1396_0_rec3_Return(EOS, -(x0, 1), 0, x2, x3, -(x0, 1), 0, x2, x3, 0, +(+(*(2, x2), *(3, x3)), *(4, -(x0, 1))), x2, x3, -(x0, 1)) | &&(&&(&&(&&(>(+(x0, 1), 1), >=(*(4, -(x0, 1)), 0)), >=(*(3, x3), 0)), >=(+(*(2, x2), *(3, x3)), 0)), >=(*(2, x2), 0))

Filtered ground terms:


f1396_0_rec3_Return(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14) → f1396_0_rec3_Return(x2, x4, x5, x6, x8, x9, x11, x12, x13, x14)
Cond_f1396_0_rec3_Return(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) → Cond_f1396_0_rec3_Return(x1, x3, x5, x6, x7, x9, x10, x12, x13, x14, x15)
f1416_1_rec2_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) → f1416_1_rec2_Load(x2, x4, x5, x6, x8, x9, x10, x12, x13)
Cond_f1396_0_rec3_Return1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) → Cond_f1396_0_rec3_Return1(x1, x3, x5, x6, x7, x9, x10, x12, x13, x14, x15)
f1388_0_rec3_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) → f1388_0_rec3_Load(x3, x4, x5, x6, x8, x9, x10, x11)
Cond_f1396_0_rec3_Return2(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) → Cond_f1396_0_rec3_Return2(x1, x3, x5, x6, x7, x9, x10, x12, x13, x14, x15)

Filtered duplicate terms:


f1396_0_rec3_Return(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → f1396_0_rec3_Return(x7, x8, x9, x10)
Cond_f1396_0_rec3_Return(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) → Cond_f1396_0_rec3_Return(x1, x8, x9, x10, x11)
f1416_1_rec2_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → f1416_1_rec2_Load(x7, x8, x9)
Cond_f1396_0_rec3_Return1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) → Cond_f1396_0_rec3_Return1(x1, x8, x9, x10, x11)
f1388_0_rec3_Load(x1, x2, x3, x4, x5, x6, x7, x8) → f1388_0_rec3_Load(x5)
Cond_f1396_0_rec3_Return2(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) → Cond_f1396_0_rec3_Return2(x1, x8, x9, x10, x11)

Filtered unneeded terms:


Cond_f1396_0_rec3_Return(x1, x2, x3, x4, x5) → Cond_f1396_0_rec3_Return(x1)
Cond_f1396_0_rec3_Return1(x1, x2, x3, x4, x5) → Cond_f1396_0_rec3_Return1(x1)
Cond_f1396_0_rec3_Return2(x1, x2, x3, x4, x5) → Cond_f1396_0_rec3_Return2(x1, x3, x4, x5)
f1396_0_rec3_Return(x1, x2, x3, x4) → f1396_0_rec3_Return(x2, x3, x4)

Prepared 3 rules for path length conversion:

P rules:
f1396_0_rec3_Return(x2, x3, x0) → f1416_1_rec2_Load(-(x0, 1), x2, x3) | >(+(x0, 1), 0)
f1396_0_rec3_Return(x2, x3, x0) → f1388_0_rec3_Load(+(+(*(2, x2), *(3, x3)), *(4, -(x0, 1)))) | &&(&&(&&(&&(>(+(x0, 1), 1), >=(*(4, -(x0, 1)), 0)), >=(*(3, x3), 0)), >=(+(*(2, x2), *(3, x3)), 0)), >=(*(2, x2), 0))
f1396_0_rec3_Return(x2, x3, x0) → f1396_0_rec3_Return(x2, x3, -(x0, 1)) | &&(&&(&&(&&(>(+(x0, 1), 1), >=(*(4, -(x0, 1)), 0)), >=(*(3, x3), 0)), >=(+(*(2, x2), *(3, x3)), 0)), >=(*(2, x2), 0))

Finished conversion. Obtained 1 rules.

P rules:
f1396_0_rec3_Return(x6, x7, x8) → f1396_0_rec3_Return(x6, x7, -(x8, 1)) | &&(&&(&&(&&(>(x8, 0), >=(*(4, x8), 4)), >=(*(3, x7), 0)), >=(+(*(2, x6), *(3, x7)), 0)), >=(*(2, x6), 0))

(17) Obligation:

Rules:
f1396_0_rec3_Return(x6, x7, x8) → f1396_0_rec3_Return(x6, x7, -(x8, 1)) | &&(&&(&&(&&(>(x8, 0), >=(*(4, x8), 4)), >=(*(3, x7), 0)), >=(+(*(2, x6), *(3, x7)), 0)), >=(*(2, x6), 0))

(18) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f1396_0_rec3_Return(x4, x6, x8)] = x8

Therefore the following rule(s) have been dropped:


f1396_0_rec3_Return(x0, x1, x2) → f1396_0_rec3_Return(x0, x1, -(x2, 1)) | &&(&&(&&(&&(>(x2, 0), >=(*(4, x2), 4)), >=(*(3, x1), 0)), >=(+(*(2, x0), *(3, x1)), 0)), >=(*(2, x0), 0))

(19) YES

(20) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Recursions.rec1(III)V
SCC calls the following helper methods: Recursions.rec2(IIII)V, Recursions.rec1(III)V, Recursions.rec3(IIIII)V, Recursions.rec4(II)V
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
  • Marker field analysis yielded the following relations that could be markers:

(21) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 25 IRules

P rules:
f1261_0_rec1_Load(EOS, i292, i56, i293, i292, i56, i293, i292) → f1263_0_rec1_GT(EOS, i292, i56, i293, i292, i56, i293, i292, i56)
f1263_0_rec1_GT(EOS, i292, i56, i293, i292, i56, i293, i292, i56) → f1275_0_rec1_GT(EOS, i292, i56, i293, i292, i56, i293, i292, i56)
f1275_0_rec1_GT(EOS, i292, i56, i293, i292, i56, i293, i292, i56) → f1285_0_rec1_Load(EOS, i292, i56, i293, i292, i56, i293) | <=(i292, i56)
f1285_0_rec1_Load(EOS, i292, i56, i293, i292, i56, i293) → f1292_0_rec1_Load(EOS, i292, i56, i293, i292, i56, i293, i293)
f1292_0_rec1_Load(EOS, i292, i56, i293, i292, i56, i293, i293) → f1301_0_rec1_IntArithmetic(EOS, i292, i56, i293, i292, i56, i293, i293, i292)
f1301_0_rec1_IntArithmetic(EOS, i292, i56, i293, i292, i56, i293, i293, i292) → f1306_0_rec1_ConstantStackPush(EOS, i292, i56, i293, i292, i56, i293, +(i293, i292)) | &&(>=(i293, 0), >=(i292, 0))
f1306_0_rec1_ConstantStackPush(EOS, i292, i56, i293, i292, i56, i293, i337) → f1308_0_rec1_Load(EOS, i292, i56, i293, i292, i56, i293, i337, 0)
f1308_0_rec1_Load(EOS, i292, i56, i293, i292, i56, i293, i337, matching1) → f1310_0_rec1_Load(EOS, i292, i56, i293, i292, i56, i293, i337, 0, i293) | =(matching1, 0)
f1310_0_rec1_Load(EOS, i292, i56, i293, i292, i56, i293, i337, matching1, i293) → f1313_0_rec1_InvokeMethod(EOS, i292, i56, i293, i292, i56, i293, i337, 0, i293, i292) | =(matching1, 0)
f1313_0_rec1_InvokeMethod(EOS, i292, i56, i293, i292, i56, i293, i337, matching1, i293, i292) → f1315_0_rec2_Load(EOS, i337, 0, i293, i292, i337, 0, i293, i292) | =(matching1, 0)
f1313_0_rec1_InvokeMethod(EOS, i292, i56, i293, i292, i56, i293, i337, matching1, i293, i292) → f1315_1_rec2_Load(EOS, i292, i56, i293, i292, i56, i293, i337, 0, i293, i292, i337, 0, i293, i292) | =(matching1, 0)
f1315_0_rec2_Load(EOS, i337, matching1, i293, i292, i337, matching2, i293, i292) → f1318_0_rec2_Load(EOS, i337, 0, i293, i292, i337, 0, i293, i292) | &&(=(matching1, 0), =(matching2, 0))
f1465_0_rec2_Return(EOS, i443, i56, i445, i443, i56, i445, i447, matching1, i445, i443) → f1442_0_rec2_Return(EOS, i443, i56, i445, i443, i56, i445, i447, 0, i445, i443) | =(matching1, 0)
f1442_0_rec2_Return(EOS, i419, i56, i421, i419, i56, i421, i423, matching1, i421, i419) → f1448_0_rec1_Load(EOS, i419, i56, i421, i419, i56, i421) | =(matching1, 0)
f1448_0_rec1_Load(EOS, i419, i56, i421, i419, i56, i421) → f1452_0_rec1_ConstantStackPush(EOS, i419, i56, i421, i56, i421, i419)
f1452_0_rec1_ConstantStackPush(EOS, i419, i56, i421, i56, i421, i419) → f1455_0_rec1_IntArithmetic(EOS, i419, i56, i421, i56, i421, i419, 1)
f1455_0_rec1_IntArithmetic(EOS, i419, i56, i421, i56, i421, i419, matching1) → f1460_0_rec1_Load(EOS, i419, i56, i421, i56, i421, +(i419, 1)) | &&(>=(i419, 0), =(matching1, 1))
f1460_0_rec1_Load(EOS, i419, i56, i421, i56, i421, i448) → f1470_0_rec1_Load(EOS, i419, i56, i421, i421, i448, i56)
f1470_0_rec1_Load(EOS, i419, i56, i421, i421, i448, i56) → f1472_0_rec1_InvokeMethod(EOS, i419, i56, i421, i448, i56, i421)
f1472_0_rec1_InvokeMethod(EOS, i419, i56, i421, i448, i56, i421) → f1474_0_rec1_Load(EOS, i448, i56, i421, i448, i56, i421)
f1472_0_rec1_InvokeMethod(EOS, i419, i56, i421, i448, i56, i421) → f1474_1_rec1_Load(EOS, i419, i56, i421, i448, i56, i421, i448, i56, i421)
f1474_0_rec1_Load(EOS, i448, i56, i421, i448, i56, i421) → f1477_0_rec1_Load(EOS, i448, i56, i421, i448, i56, i421)
f1477_0_rec1_Load(EOS, i448, i56, i421, i448, i56, i421) → f1257_0_rec1_Load(EOS, i448, i56, i421, i448, i56, i421)
f1257_0_rec1_Load(EOS, i292, i56, i293, i292, i56, i293) → f1261_0_rec1_Load(EOS, i292, i56, i293, i292, i56, i293, i292)
f1315_1_rec2_Load(EOS, i443, i56, i445, i443, i56, i445, i447, matching1, i445, i443, i447, matching2, i445, i443) → f1465_0_rec2_Return(EOS, i443, i56, i445, i443, i56, i445, i447, 0, i445, i443) | &&(=(matching1, 0), =(matching2, 0))

Combined rules. Obtained 3 IRules

P rules:
f1465_0_rec2_Return(EOS, x0, x1, x2, x0, x1, x2, x3, 0, x2, x0) → f1474_1_rec1_Load(EOS, x0, x1, x2, +(x0, 1), x1, x2, +(x0, 1), x1, x2) | >(+(x0, 1), 0)
f1465_0_rec2_Return(EOS, x0, x1, x2, x0, x1, x2, x3, 0, x2, x0) → f1318_0_rec2_Load(EOS, +(x2, +(x0, 1)), 0, x2, +(x0, 1), +(x2, +(x0, 1)), 0, x2, +(x0, 1)) | &&(&&(>(+(x2, 1), 0), >(+(x0, 1), 0)), >=(x1, +(x0, 1)))
f1465_0_rec2_Return(EOS, x0, x1, x2, x0, x1, x2, x3, 0, x2, x0) → f1465_0_rec2_Return(EOS, +(x0, 1), x1, x2, +(x0, 1), x1, x2, +(x2, +(x0, 1)), 0, x2, +(x0, 1)) | &&(&&(>(+(x2, 1), 0), >(+(x0, 1), 0)), >=(x1, +(x0, 1)))

Filtered ground terms:


f1465_0_rec2_Return(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) → f1465_0_rec2_Return(x2, x3, x4, x5, x6, x7, x8, x10, x11)
Cond_f1465_0_rec2_Return(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) → Cond_f1465_0_rec2_Return(x1, x3, x4, x5, x6, x7, x8, x9, x11, x12)
f1474_1_rec1_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → f1474_1_rec1_Load(x2, x3, x4, x5, x6, x7, x8, x9, x10)
Cond_f1465_0_rec2_Return1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) → Cond_f1465_0_rec2_Return1(x1, x3, x4, x5, x6, x7, x8, x9, x11, x12)
f1318_0_rec2_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → f1318_0_rec2_Load(x2, x4, x5, x6, x8, x9)
Cond_f1465_0_rec2_Return2(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) → Cond_f1465_0_rec2_Return2(x1, x3, x4, x5, x6, x7, x8, x9, x11, x12)

Filtered duplicate terms:


f1465_0_rec2_Return(x1, x2, x3, x4, x5, x6, x7, x8, x9) → f1465_0_rec2_Return(x5, x7, x8, x9)
Cond_f1465_0_rec2_Return(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_f1465_0_rec2_Return(x1, x6, x8, x9, x10)
f1474_1_rec1_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → f1474_1_rec1_Load(x7, x8, x9)
Cond_f1465_0_rec2_Return1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_f1465_0_rec2_Return1(x1, x6, x8, x9, x10)
f1318_0_rec2_Load(x1, x2, x3, x4, x5, x6) → f1318_0_rec2_Load(x4)
Cond_f1465_0_rec2_Return2(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_f1465_0_rec2_Return2(x1, x6, x8, x9, x10)

Filtered unneeded terms:


Cond_f1465_0_rec2_Return(x1, x2, x3, x4, x5) → Cond_f1465_0_rec2_Return(x1)
Cond_f1465_0_rec2_Return1(x1, x2, x3, x4, x5) → Cond_f1465_0_rec2_Return1(x1)
Cond_f1465_0_rec2_Return2(x1, x2, x3, x4, x5) → Cond_f1465_0_rec2_Return2(x1, x2, x4, x5)
f1465_0_rec2_Return(x1, x2, x3, x4) → f1465_0_rec2_Return(x1, x3, x4)

Prepared 3 rules for path length conversion:

P rules:
f1465_0_rec2_Return(x1, x2, x0) → f1474_1_rec1_Load(+(x0, 1), x1, x2) | >(+(x0, 1), 0)
f1465_0_rec2_Return(x1, x2, x0) → f1318_0_rec2_Load(+(x2, +(x0, 1))) | &&(&&(>(+(x2, 1), 0), >(+(x0, 1), 0)), >=(x1, +(x0, 1)))
f1465_0_rec2_Return(x1, x2, x0) → f1465_0_rec2_Return(x1, x2, +(x0, 1)) | &&(&&(>(+(x2, 1), 0), >(+(x0, 1), 0)), >=(x1, +(x0, 1)))

Finished conversion. Obtained 1 rules.

P rules:
f1465_0_rec2_Return(x6, x7, x8) → f1465_0_rec2_Return(x6, x7, +(x8, 1)) | &&(&&(>(x8, -1), >(x7, -1)), <=(+(x8, 1), x6))

(22) Obligation:

Rules:
f1465_0_rec2_Return(x6, x7, x8) → f1465_0_rec2_Return(x6, x7, +(x8, 1)) | &&(&&(>(x8, -1), >(x7, -1)), <=(+(x8, 1), x6))

(23) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f1465_0_rec2_Return(x4, x6, x8)] = x4 - x8

Therefore the following rule(s) have been dropped:


f1465_0_rec2_Return(x0, x1, x2) → f1465_0_rec2_Return(x0, x1, +(x2, 1)) | &&(&&(>(x2, -1), >(x1, -1)), <=(+(x2, 1), x0))

(24) YES

(25) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Recursions.rec0(II)V
SCC calls the following helper methods: Recursions.rec1(III)V, Recursions.rec0(II)V, Recursions.rec2(IIII)V, Recursions.rec3(IIIII)V, Recursions.rec4(II)V
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
  • Marker field analysis yielded the following relations that could be markers:

(26) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 25 IRules

P rules:
f863_0_rec0_Load(EOS, i73, i74, i73, i74, i73) → f867_0_rec0_GT(EOS, i73, i74, i73, i74, i73, i74)
f867_0_rec0_GT(EOS, i73, i74, i73, i74, i73, i74) → f873_0_rec0_GT(EOS, i73, i74, i73, i74, i73, i74)
f873_0_rec0_GT(EOS, i73, i74, i73, i74, i73, i74) → f880_0_rec0_ConstantStackPush(EOS, i73, i74, i73, i74) | <=(i73, i74)
f880_0_rec0_ConstantStackPush(EOS, i73, i74, i73, i74) → f895_0_rec0_ConstantStackPush(EOS, i73, i74, i73, i74, 0)
f895_0_rec0_ConstantStackPush(EOS, i73, i74, i73, i74, matching1) → f908_0_rec0_Load(EOS, i73, i74, i73, i74, 0, 2) | =(matching1, 0)
f908_0_rec0_Load(EOS, i73, i74, i73, i74, matching1, matching2) → f915_0_rec0_IntArithmetic(EOS, i73, i74, i73, i74, 0, 2, i73) | &&(=(matching1, 0), =(matching2, 2))
f915_0_rec0_IntArithmetic(EOS, i73, i74, i73, i74, matching1, matching2, i73) → f920_0_rec0_Load(EOS, i73, i74, i73, i74, 0, *(2, i73)) | &&(=(matching1, 0), =(matching2, 2))
f920_0_rec0_Load(EOS, i73, i74, i73, i74, matching1, i101) → f926_0_rec0_InvokeMethod(EOS, i73, i74, i73, i74, 0, i101, i73) | =(matching1, 0)
f926_0_rec0_InvokeMethod(EOS, i73, i74, i73, i74, matching1, i101, i73) → f938_0_rec1_Load(EOS, 0, i101, i73, 0, i101, i73) | =(matching1, 0)
f926_0_rec0_InvokeMethod(EOS, i73, i74, i73, i74, matching1, i101, i73) → f938_1_rec1_Load(EOS, i73, i74, i73, i74, 0, i101, i73, 0, i101, i73) | =(matching1, 0)
f938_0_rec1_Load(EOS, matching1, i101, i73, matching2, i101, i73) → f944_0_rec1_Load(EOS, 0, i101, i73, 0, i101, i73) | &&(=(matching1, 0), =(matching2, 0))
f1303_0_rec1_Return(EOS, i333, i74, i333, i74, matching1, i331, i333) → f967_0_rec1_Return(EOS, i333, i74, i333, i74, 0, i331, i333) | =(matching1, 0)
f967_0_rec1_Return(EOS, i129, i74, i129, i74, matching1, i127, i129) → f972_0_rec0_Load(EOS, i129, i74, i129, i74) | =(matching1, 0)
f972_0_rec0_Load(EOS, i129, i74, i129, i74) → f978_0_rec0_ConstantStackPush(EOS, i129, i74, i74, i129)
f978_0_rec0_ConstantStackPush(EOS, i129, i74, i74, i129) → f984_0_rec0_IntArithmetic(EOS, i129, i74, i74, i129, 1)
f984_0_rec0_IntArithmetic(EOS, i129, i74, i74, i129, matching1) → f989_0_rec0_Load(EOS, i129, i74, i74, +(i129, 1)) | &&(>=(i129, 0), =(matching1, 1))
f989_0_rec0_Load(EOS, i129, i74, i74, i133) → f993_0_rec0_InvokeMethod(EOS, i129, i74, i133, i74)
f993_0_rec0_InvokeMethod(EOS, i129, i74, i133, i74) → f1001_0_rec0_Load(EOS, i133, i74, i133, i74)
f993_0_rec0_InvokeMethod(EOS, i129, i74, i133, i74) → f1001_1_rec0_Load(EOS, i129, i74, i133, i74, i133, i74)
f1001_0_rec0_Load(EOS, i133, i74, i133, i74) → f1007_0_rec0_Load(EOS, i133, i74, i133, i74)
f1007_0_rec0_Load(EOS, i133, i74, i133, i74) → f855_0_rec0_Load(EOS, i133, i74, i133, i74)
f855_0_rec0_Load(EOS, i73, i74, i73, i74) → f863_0_rec0_Load(EOS, i73, i74, i73, i74, i73)
f1500_0_rec1_Return(EOS, i504, i74, i504, i74, matching1, i502, i504) → f967_0_rec1_Return(EOS, i504, i74, i504, i74, 0, i502, i504) | =(matching1, 0)
f938_1_rec1_Load(EOS, i333, i74, i333, i74, matching1, i331, i333, matching2, i331, i333) → f1303_0_rec1_Return(EOS, i333, i74, i333, i74, 0, i331, i333) | &&(=(matching1, 0), =(matching2, 0))
f938_1_rec1_Load(EOS, i504, i74, i504, i74, matching1, i502, i504, matching2, i502, i504) → f1500_0_rec1_Return(EOS, i504, i74, i504, i74, 0, i502, i504) | &&(=(matching1, 0), =(matching2, 0))

Combined rules. Obtained 3 IRules

P rules:
f993_0_rec0_InvokeMethod(EOS, i129, i74, i133, i74) → f1001_1_rec0_Load(EOS, i129, i74, i133, i74, i133, i74)
f993_0_rec0_InvokeMethod(EOS, x0, x1, x2, x1) → f944_0_rec1_Load(EOS, 0, *(2, x2), x2, 0, *(2, x2), x2) | <=(x2, x1)
f993_0_rec0_InvokeMethod(EOS, x0, x1, x2, x1) → f993_0_rec0_InvokeMethod(EOS, x2, x1, +(x2, 1), x1) | &&(<=(x2, x1), >(+(x2, 1), 0))

Filtered ground terms:


f993_0_rec0_InvokeMethod(x1, x2, x3, x4, x5) → f993_0_rec0_InvokeMethod(x2, x3, x4, x5)
f1001_1_rec0_Load(x1, x2, x3, x4, x5, x6, x7) → f1001_1_rec0_Load(x2, x3, x4, x5, x6, x7)
Cond_f993_0_rec0_InvokeMethod(x1, x2, x3, x4, x5, x6) → Cond_f993_0_rec0_InvokeMethod(x1, x3, x4, x5, x6)
f944_0_rec1_Load(x1, x2, x3, x4, x5, x6, x7) → f944_0_rec1_Load(x3, x4, x6, x7)
Cond_f993_0_rec0_InvokeMethod1(x1, x2, x3, x4, x5, x6) → Cond_f993_0_rec0_InvokeMethod1(x1, x3, x4, x5, x6)

Filtered duplicate terms:


f993_0_rec0_InvokeMethod(x1, x2, x3, x4) → f993_0_rec0_InvokeMethod(x1, x3, x4)
f1001_1_rec0_Load(x1, x2, x3, x4, x5, x6) → f1001_1_rec0_Load(x1, x5, x6)
Cond_f993_0_rec0_InvokeMethod(x1, x2, x3, x4, x5) → Cond_f993_0_rec0_InvokeMethod(x1, x2, x4, x5)
f944_0_rec1_Load(x1, x2, x3, x4) → f944_0_rec1_Load(x3)
Cond_f993_0_rec0_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_f993_0_rec0_InvokeMethod1(x1, x2, x4, x5)

Filtered unneeded terms:


Cond_f993_0_rec0_InvokeMethod(x1, x2, x3, x4) → Cond_f993_0_rec0_InvokeMethod(x1)
Cond_f993_0_rec0_InvokeMethod1(x1, x2, x3, x4) → Cond_f993_0_rec0_InvokeMethod1(x1, x3, x4)
f993_0_rec0_InvokeMethod(x1, x2, x3) → f993_0_rec0_InvokeMethod(x2, x3)

Prepared 3 rules for path length conversion:

P rules:
f993_0_rec0_InvokeMethod(i133, i74) → f1001_1_rec0_Load(i129, i133, i74)
f993_0_rec0_InvokeMethod(x2, x1) → f944_0_rec1_Load(*(2, x2)) | <=(x2, x1)
f993_0_rec0_InvokeMethod(x2, x1) → f993_0_rec0_InvokeMethod(+(x2, 1), x1) | &&(<=(x2, x1), >(+(x2, 1), 0))

Finished conversion. Obtained 1 rules.

P rules:
f993_0_rec0_InvokeMethod(x5, x6) → f993_0_rec0_InvokeMethod(+(x5, 1), x6) | &&(>(x5, -1), >=(x6, x5))

(27) Obligation:

Rules:
f993_0_rec0_InvokeMethod(x5, x6) → f993_0_rec0_InvokeMethod(+(x5, 1), x6) | &&(>(x5, -1), >=(x6, x5))

(28) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f993_0_rec0_InvokeMethod(x3, x5)] = -x3 + x5

Therefore the following rule(s) have been dropped:


f993_0_rec0_InvokeMethod(x0, x1) → f993_0_rec0_InvokeMethod(+(x0, 1), x1) | &&(>(x0, -1), >=(x1, x0))

(29) YES

(30) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Recursions.main([Ljava/lang/String;)V
SCC calls the following helper methods: Recursions.rec0(II)V, Recursions.rec1(III)V, Recursions.rec2(IIII)V, Recursions.rec3(IIIII)V, Recursions.rec4(II)V
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
  • Marker field analysis yielded the following relations that could be markers:

(31) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 18 IRules

P rules:
f1199_0_main_Load(EOS, java.lang.Object(ARRAY(i247)), java.lang.Object(ARRAY(i247)), i248, i248) → f1207_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i247)), java.lang.Object(ARRAY(i247)), i248, i248, java.lang.Object(ARRAY(i247)))
f1207_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i247)), java.lang.Object(ARRAY(i247)), i248, i248, java.lang.Object(ARRAY(i247))) → f1213_0_main_GE(EOS, java.lang.Object(ARRAY(i247)), java.lang.Object(ARRAY(i247)), i248, i248, i247) | >=(i247, 0)
f1213_0_main_GE(EOS, java.lang.Object(ARRAY(i247)), java.lang.Object(ARRAY(i247)), i248, i248, i247) → f1218_0_main_GE(EOS, java.lang.Object(ARRAY(i247)), java.lang.Object(ARRAY(i247)), i248, i248, i247)
f1218_0_main_GE(EOS, java.lang.Object(ARRAY(i247)), java.lang.Object(ARRAY(i247)), i248, i248, i247) → f1231_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i247)), java.lang.Object(ARRAY(i247)), i248) | <(i248, i247)
f1231_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i247)), java.lang.Object(ARRAY(i247)), i248) → f1243_0_main_Load(EOS, java.lang.Object(ARRAY(i247)), java.lang.Object(ARRAY(i247)), i248, 0)
f1243_0_main_Load(EOS, java.lang.Object(ARRAY(i247)), java.lang.Object(ARRAY(i247)), i248, matching1) → f1246_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i247)), java.lang.Object(ARRAY(i247)), i248, 0, java.lang.Object(ARRAY(i247))) | =(matching1, 0)
f1246_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i247)), java.lang.Object(ARRAY(i247)), i248, matching1, java.lang.Object(ARRAY(i247))) → f1251_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i247)), java.lang.Object(ARRAY(i247)), i248, 0, i247) | &&(>=(i247, 0), =(matching1, 0))
f1251_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i247)), java.lang.Object(ARRAY(i247)), i248, matching1, i247) → f1253_0_rec0_Load(EOS, 0, i247, 0, i247) | =(matching1, 0)
f1251_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i247)), java.lang.Object(ARRAY(i247)), i248, matching1, i247) → f1253_1_rec0_Load(EOS, java.lang.Object(ARRAY(i247)), java.lang.Object(ARRAY(i247)), i248, 0, i247, 0, i247) | =(matching1, 0)
f1253_0_rec0_Load(EOS, matching1, i247, matching2, i247) → f1258_0_rec0_Load(EOS, 0, i247, 0, i247) | &&(=(matching1, 0), =(matching2, 0))
f1276_0_rec0_Return(EOS, java.lang.Object(ARRAY(i299)), java.lang.Object(ARRAY(i299)), i248, matching1, i299) → f1286_0_main_Inc(EOS, java.lang.Object(ARRAY(i299)), java.lang.Object(ARRAY(i299)), i248) | =(matching1, 0)
f1286_0_main_Inc(EOS, java.lang.Object(ARRAY(i299)), java.lang.Object(ARRAY(i299)), i248) → f1290_0_main_JMP(EOS, java.lang.Object(ARRAY(i299)), java.lang.Object(ARRAY(i299)), +(i248, 1)) | >=(i248, 0)
f1290_0_main_JMP(EOS, java.lang.Object(ARRAY(i299)), java.lang.Object(ARRAY(i299)), i323) → f1295_0_main_Load(EOS, java.lang.Object(ARRAY(i299)), java.lang.Object(ARRAY(i299)), i323)
f1295_0_main_Load(EOS, java.lang.Object(ARRAY(i299)), java.lang.Object(ARRAY(i299)), i323) → f1192_0_main_Load(EOS, java.lang.Object(ARRAY(i299)), java.lang.Object(ARRAY(i299)), i323)
f1192_0_main_Load(EOS, java.lang.Object(ARRAY(i247)), java.lang.Object(ARRAY(i247)), i248) → f1199_0_main_Load(EOS, java.lang.Object(ARRAY(i247)), java.lang.Object(ARRAY(i247)), i248, i248)
f1283_0_rec0_Return(EOS, java.lang.Object(ARRAY(i303)), java.lang.Object(ARRAY(i303)), i248, matching1, i303) → f1276_0_rec0_Return(EOS, java.lang.Object(ARRAY(i303)), java.lang.Object(ARRAY(i303)), i248, 0, i303) | =(matching1, 0)
f1253_1_rec0_Load(EOS, java.lang.Object(ARRAY(i247)), java.lang.Object(ARRAY(i247)), i248, matching1, i299, matching2, i299) → f1276_0_rec0_Return(EOS, java.lang.Object(ARRAY(i299)), java.lang.Object(ARRAY(i299)), i248, 0, i299) | &&(=(matching1, 0), =(matching2, 0))
f1253_1_rec0_Load(EOS, java.lang.Object(ARRAY(i247)), java.lang.Object(ARRAY(i247)), i248, matching1, i303, matching2, i303) → f1283_0_rec0_Return(EOS, java.lang.Object(ARRAY(i303)), java.lang.Object(ARRAY(i303)), i248, 0, i303) | &&(=(matching1, 0), =(matching2, 0))

Combined rules. Obtained 2 IRules

P rules:
f1276_0_rec0_Return(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, 0, x0) → f1258_0_rec0_Load(EOS, 0, x0, 0, x0) | &&(&&(>(+(x1, 1), 0), <(+(x1, 1), x0)), >(+(x0, 1), 0))
f1276_0_rec0_Return(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, 0, x0) → f1276_0_rec0_Return(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), +(x1, 1), 0, x0) | &&(&&(>(+(x1, 1), 0), <(+(x1, 1), x0)), >(+(x0, 1), 0))

Filtered ground terms:


f1276_0_rec0_Return(x1, x2, x3, x4, x5, x6) → f1276_0_rec0_Return(x2, x3, x4, x6)
Cond_f1276_0_rec0_Return(x1, x2, x3, x4, x5, x6, x7) → Cond_f1276_0_rec0_Return(x1, x3, x4, x5, x7)
f1258_0_rec0_Load(x1, x2, x3, x4, x5) → f1258_0_rec0_Load(x3, x5)
Cond_f1276_0_rec0_Return1(x1, x2, x3, x4, x5, x6, x7) → Cond_f1276_0_rec0_Return1(x1, x3, x4, x5, x7)

Filtered duplicate terms:


f1276_0_rec0_Return(x1, x2, x3, x4) → f1276_0_rec0_Return(x2, x3)
Cond_f1276_0_rec0_Return(x1, x2, x3, x4, x5) → Cond_f1276_0_rec0_Return(x1, x3, x4)
f1258_0_rec0_Load(x1, x2) → f1258_0_rec0_Load(x2)
Cond_f1276_0_rec0_Return1(x1, x2, x3, x4, x5) → Cond_f1276_0_rec0_Return1(x1, x3, x4)

Filtered unneeded terms:


Cond_f1276_0_rec0_Return(x1, x2, x3) → Cond_f1276_0_rec0_Return(x1)

Prepared 2 rules for path length conversion:

P rules:
f1276_0_rec0_Return(java.lang.Object(ARRAY(x0)), x1, x0) → f1258_0_rec0_Load(x0) | &&(&&(>(+(x1, 1), 0), <(+(x1, 1), x0)), >(+(x0, 1), 0))
f1276_0_rec0_Return(java.lang.Object(ARRAY(x0)), x1, x0) → f1276_0_rec0_Return(java.lang.Object(ARRAY(x0)), +(x1, 1), x0) | &&(&&(>(+(x1, 1), 0), <(+(x1, 1), x0)), >(+(x0, 1), 0))

Finished conversion. Obtained 1 rules.

P rules:
f1276_0_rec0_Return(v7, x3, x2) → f1276_0_rec0_Return(v8, +(x3, 1), x2) | &&(&&(&&(&&(&&(>(x3, -1), <(+(x3, 1), x2)), >(x2, -1)), >(+(v8, 1), 1)), <=(v8, v7)), >(+(v7, 1), 1))

(32) Obligation:

Rules:
f1276_0_rec0_Return(v7, x3, x2) → f1276_0_rec0_Return(v8, +(x3, 1), x2) | &&(&&(&&(&&(&&(>(x3, -1), <(+(x3, 1), x2)), >(x2, -1)), >(+(v8, 1), 1)), <=(v8, v7)), >(+(v7, 1), 1))

(33) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f1276_0_rec0_Return(x5, x7, x9)] = -x7 + x9

Therefore the following rule(s) have been dropped:


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

(34) YES