Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 443 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 JBCTerminationSCC
↳5 SCCToIntTRSProof (⇒, 118 ms)
↳6 intTRS
↳7 LinearRankingProcessor (⇔, 0 ms)
↳8 YES

(0) Obligation:

JBC Problem based on JBC Program:
public class Test1 {
    public static void main(String[] args) {
	rec(args.length, args.length % 5, args.length % 4);
    }

    private static void rec(int x, int y, int z) {
	if (x + y + 3 * z < 0)
	    return;
	else if (x > y)
	    rec(x - 1, y, z);
	else if (y > z)
	    rec (x, y - 2, z);
	else
	    rec (x, y, z - 1);
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Test1.main([Ljava/lang/String;)V: Graph of 44 nodes with 0 SCCs.

Test1.rec(III)V: Graph of 68 nodes with 0 SCCs.


(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 1 SCCs.

(4) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test1.rec(III)V
SCC calls the following helper methods: Test1.rec(III)V
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
  • Marker field analysis yielded the following relations that could be markers:

(5) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 48 IRules

P rules:
f1788_0_rec_Load(EOS, i138, i688, i388, i138, i688, i388, i138) → f1790_0_rec_IntArithmetic(EOS, i138, i688, i388, i138, i688, i388, i138, i688)
f1790_0_rec_IntArithmetic(EOS, i138, i688, i388, i138, i688, i388, i138, i688) → f1792_0_rec_ConstantStackPush(EOS, i138, i688, i388, i138, i688, i388, +(i138, i688))
f1792_0_rec_ConstantStackPush(EOS, i138, i688, i388, i138, i688, i388, i689) → f1793_0_rec_Load(EOS, i138, i688, i388, i138, i688, i388, i689, 3)
f1793_0_rec_Load(EOS, i138, i688, i388, i138, i688, i388, i689, matching1) → f1796_0_rec_IntArithmetic(EOS, i138, i688, i388, i138, i688, i388, i689, 3, i388) | =(matching1, 3)
f1796_0_rec_IntArithmetic(EOS, i138, i688, i388, i138, i688, i388, i689, matching1, i388) → f1797_0_rec_IntArithmetic(EOS, i138, i688, i388, i138, i688, i388, i689, *(3, i388)) | =(matching1, 3)
f1797_0_rec_IntArithmetic(EOS, i138, i688, i388, i138, i688, i388, i689, i690) → f1799_0_rec_GE(EOS, i138, i688, i388, i138, i688, i388, +(i689, i690))
f1799_0_rec_GE(EOS, i138, i688, i388, i138, i688, i388, i695) → f1803_0_rec_GE(EOS, i138, i688, i388, i138, i688, i388, i695)
f1803_0_rec_GE(EOS, i138, i688, i388, i138, i688, i388, i695) → f1807_0_rec_Load(EOS, i138, i688, i388, i138, i688, i388) | >=(i695, 0)
f1807_0_rec_Load(EOS, i138, i688, i388, i138, i688, i388) → f1811_0_rec_Load(EOS, i138, i688, i388, i138, i688, i388, i138)
f1811_0_rec_Load(EOS, i138, i688, i388, i138, i688, i388, i138) → f1824_0_rec_LE(EOS, i138, i688, i388, i138, i688, i388, i138, i688)
f1824_0_rec_LE(EOS, i138, i688, i388, i138, i688, i388, i138, i688) → f1831_0_rec_LE(EOS, i138, i688, i388, i138, i688, i388, i138, i688)
f1824_0_rec_LE(EOS, i138, i688, i388, i138, i688, i388, i138, i688) → f1832_0_rec_LE(EOS, i138, i688, i388, i138, i688, i388, i138, i688)
f1831_0_rec_LE(EOS, i138, i688, i388, i138, i688, i388, i138, i688) → f1835_0_rec_Load(EOS, i138, i688, i388, i138, i688, i388) | <=(i138, i688)
f1835_0_rec_Load(EOS, i138, i688, i388, i138, i688, i388) → f1838_0_rec_Load(EOS, i138, i688, i388, i138, i688, i388, i688)
f1838_0_rec_Load(EOS, i138, i688, i388, i138, i688, i388, i688) → f1843_0_rec_LE(EOS, i138, i688, i388, i138, i688, i388, i688, i388)
f1843_0_rec_LE(EOS, i138, i688, i388, i138, i688, i388, i688, i388) → f1848_0_rec_LE(EOS, i138, i688, i388, i138, i688, i388, i688, i388)
f1843_0_rec_LE(EOS, i138, i688, i388, i138, i688, i388, i688, i388) → f1849_0_rec_LE(EOS, i138, i688, i388, i138, i688, i388, i688, i388)
f1848_0_rec_LE(EOS, i138, i688, i388, i138, i688, i388, i688, i388) → f1852_0_rec_Load(EOS, i138, i688, i388, i138, i688, i388) | <=(i688, i388)
f1852_0_rec_Load(EOS, i138, i688, i388, i138, i688, i388) → f1858_0_rec_Load(EOS, i138, i688, i388, i688, i388, i138)
f1858_0_rec_Load(EOS, i138, i688, i388, i688, i388, i138) → f1863_0_rec_Load(EOS, i138, i688, i388, i388, i138, i688)
f1863_0_rec_Load(EOS, i138, i688, i388, i388, i138, i688) → f1867_0_rec_ConstantStackPush(EOS, i138, i688, i388, i138, i688, i388)
f1867_0_rec_ConstantStackPush(EOS, i138, i688, i388, i138, i688, i388) → f1872_0_rec_IntArithmetic(EOS, i138, i688, i388, i138, i688, i388, 1)
f1872_0_rec_IntArithmetic(EOS, i138, i688, i388, i138, i688, i388, matching1) → f1875_0_rec_InvokeMethod(EOS, i138, i688, i388, i138, i688, -(i388, 1)) | =(matching1, 1)
f1875_0_rec_InvokeMethod(EOS, i138, i688, i388, i138, i688, i715) → f1886_0_rec_Load(EOS, i138, i688, i715, i138, i688, i715)
f1875_0_rec_InvokeMethod(EOS, i138, i688, i388, i138, i688, i715) → f1886_1_rec_Load(EOS, i138, i688, i388, i138, i688, i715, i138, i688, i715)
f1886_0_rec_Load(EOS, i138, i688, i715, i138, i688, i715) → f1890_0_rec_Load(EOS, i138, i688, i715, i138, i688, i715)
f1890_0_rec_Load(EOS, i138, i688, i715, i138, i688, i715) → f1787_0_rec_Load(EOS, i138, i688, i715, i138, i688, i715)
f1787_0_rec_Load(EOS, i138, i688, i388, i138, i688, i388) → f1788_0_rec_Load(EOS, i138, i688, i388, i138, i688, i388, i138)
f1849_0_rec_LE(EOS, i138, i688, i388, i138, i688, i388, i688, i388) → f1854_0_rec_Load(EOS, i138, i688, i388, i138, i688, i388) | >(i688, i388)
f1854_0_rec_Load(EOS, i138, i688, i388, i138, i688, i388) → f1859_0_rec_Load(EOS, i138, i688, i388, i688, i388, i138)
f1859_0_rec_Load(EOS, i138, i688, i388, i688, i388, i138) → f1864_0_rec_ConstantStackPush(EOS, i138, i688, i388, i388, i138, i688)
f1864_0_rec_ConstantStackPush(EOS, i138, i688, i388, i388, i138, i688) → f1869_0_rec_IntArithmetic(EOS, i138, i688, i388, i388, i138, i688, 2)
f1869_0_rec_IntArithmetic(EOS, i138, i688, i388, i388, i138, i688, matching1) → f1873_0_rec_Load(EOS, i138, i688, i388, i388, i138, -(i688, 2)) | =(matching1, 2)
f1873_0_rec_Load(EOS, i138, i688, i388, i388, i138, i714) → f1876_0_rec_InvokeMethod(EOS, i138, i688, i388, i138, i714, i388)
f1876_0_rec_InvokeMethod(EOS, i138, i688, i388, i138, i714, i388) → f1887_0_rec_Load(EOS, i138, i714, i388, i138, i714, i388)
f1876_0_rec_InvokeMethod(EOS, i138, i688, i388, i138, i714, i388) → f1887_1_rec_Load(EOS, i138, i688, i388, i138, i714, i388, i138, i714, i388)
f1887_0_rec_Load(EOS, i138, i714, i388, i138, i714, i388) → f1892_0_rec_Load(EOS, i138, i714, i388, i138, i714, i388)
f1892_0_rec_Load(EOS, i138, i714, i388, i138, i714, i388) → f1787_0_rec_Load(EOS, i138, i714, i388, i138, i714, i388)
f1832_0_rec_LE(EOS, i138, i688, i388, i138, i688, i388, i138, i688) → f1836_0_rec_Load(EOS, i138, i688, i388, i138, i688, i388) | >(i138, i688)
f1836_0_rec_Load(EOS, i138, i688, i388, i138, i688, i388) → f1841_0_rec_ConstantStackPush(EOS, i138, i688, i388, i688, i388, i138)
f1841_0_rec_ConstantStackPush(EOS, i138, i688, i388, i688, i388, i138) → f1845_0_rec_IntArithmetic(EOS, i138, i688, i388, i688, i388, i138, 1)
f1845_0_rec_IntArithmetic(EOS, i138, i688, i388, i688, i388, i138, matching1) → f1850_0_rec_Load(EOS, i138, i688, i388, i688, i388, -(i138, 1)) | =(matching1, 1)
f1850_0_rec_Load(EOS, i138, i688, i388, i688, i388, i712) → f1855_0_rec_Load(EOS, i138, i688, i388, i388, i712, i688)
f1855_0_rec_Load(EOS, i138, i688, i388, i388, i712, i688) → f1861_0_rec_InvokeMethod(EOS, i138, i688, i388, i712, i688, i388)
f1861_0_rec_InvokeMethod(EOS, i138, i688, i388, i712, i688, i388) → f1866_0_rec_Load(EOS, i712, i688, i388, i712, i688, i388)
f1861_0_rec_InvokeMethod(EOS, i138, i688, i388, i712, i688, i388) → f1866_1_rec_Load(EOS, i138, i688, i388, i712, i688, i388, i712, i688, i388)
f1866_0_rec_Load(EOS, i712, i688, i388, i712, i688, i388) → f1870_0_rec_Load(EOS, i712, i688, i388, i712, i688, i388)
f1870_0_rec_Load(EOS, i712, i688, i388, i712, i688, i388) → f1787_0_rec_Load(EOS, i712, i688, i388, i712, i688, i388)

Combined rules. Obtained 6 IRules

P rules:
f1788_0_rec_Load(EOS, x0, x1, x2, x0, x1, x2, x0) → f1886_1_rec_Load(EOS, x0, x1, x2, x0, x1, -(x2, 1), x0, x1, -(x2, 1)) | &&(&&(>=(x2, x1), >=(+(+(x0, x1), *(3, x2)), 0)), >=(x1, x0))
f1788_0_rec_Load(EOS, x0, x1, x2, x0, x1, x2, x0) → f1788_0_rec_Load(EOS, x0, x1, -(x2, 1), x0, x1, -(x2, 1), x0) | &&(&&(>=(x2, x1), >=(+(+(x0, x1), *(3, x2)), 0)), >=(x1, x0))
f1788_0_rec_Load(EOS, x0, x1, x2, x0, x1, x2, x0) → f1887_1_rec_Load(EOS, x0, x1, x2, x0, -(x1, 2), x2, x0, -(x1, 2), x2) | &&(&&(<(x2, x1), >=(+(+(x0, x1), *(3, x2)), 0)), >=(x1, x0))
f1788_0_rec_Load(EOS, x0, x1, x2, x0, x1, x2, x0) → f1788_0_rec_Load(EOS, x0, -(x1, 2), x2, x0, -(x1, 2), x2, x0) | &&(&&(<(x2, x1), >=(+(+(x0, x1), *(3, x2)), 0)), >=(x1, x0))
f1788_0_rec_Load(EOS, x0, x1, x2, x0, x1, x2, x0) → f1866_1_rec_Load(EOS, x0, x1, x2, -(x0, 1), x1, x2, -(x0, 1), x1, x2) | &&(>=(+(+(x0, x1), *(3, x2)), 0), <(x1, x0))
f1788_0_rec_Load(EOS, x0, x1, x2, x0, x1, x2, x0) → f1788_0_rec_Load(EOS, -(x0, 1), x1, x2, -(x0, 1), x1, x2, -(x0, 1)) | &&(>=(+(+(x0, x1), *(3, x2)), 0), <(x1, x0))

Filtered ground terms:


f1788_0_rec_Load(x1, x2, x3, x4, x5, x6, x7, x8) → f1788_0_rec_Load(x2, x3, x4, x5, x6, x7, x8)
Cond_f1788_0_rec_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f1788_0_rec_Load(x1, x3, x4, x5, x6, x7, x8, x9)
f1886_1_rec_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → f1886_1_rec_Load(x2, x3, x4, x5, x6, x7, x8, x9, x10)
Cond_f1788_0_rec_Load1(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f1788_0_rec_Load1(x1, x3, x4, x5, x6, x7, x8, x9)
Cond_f1788_0_rec_Load2(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f1788_0_rec_Load2(x1, x3, x4, x5, x6, x7, x8, x9)
f1887_1_rec_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → f1887_1_rec_Load(x2, x3, x4, x5, x6, x7, x8, x9, x10)
Cond_f1788_0_rec_Load3(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f1788_0_rec_Load3(x1, x3, x4, x5, x6, x7, x8, x9)
Cond_f1788_0_rec_Load4(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f1788_0_rec_Load4(x1, x3, x4, x5, x6, x7, x8, x9)
f1866_1_rec_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → f1866_1_rec_Load(x2, x3, x4, x5, x6, x7, x8, x9, x10)
Cond_f1788_0_rec_Load5(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f1788_0_rec_Load5(x1, x3, x4, x5, x6, x7, x8, x9)

Filtered duplicate terms:


f1788_0_rec_Load(x1, x2, x3, x4, x5, x6, x7) → f1788_0_rec_Load(x5, x6, x7)
Cond_f1788_0_rec_Load(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1788_0_rec_Load(x1, x6, x7, x8)
f1886_1_rec_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → f1886_1_rec_Load(x7, x8, x9)
Cond_f1788_0_rec_Load1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1788_0_rec_Load1(x1, x6, x7, x8)
Cond_f1788_0_rec_Load2(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1788_0_rec_Load2(x1, x6, x7, x8)
f1887_1_rec_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → f1887_1_rec_Load(x7, x8, x9)
Cond_f1788_0_rec_Load3(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1788_0_rec_Load3(x1, x6, x7, x8)
Cond_f1788_0_rec_Load4(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1788_0_rec_Load4(x1, x6, x7, x8)
f1866_1_rec_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → f1866_1_rec_Load(x7, x8, x9)
Cond_f1788_0_rec_Load5(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1788_0_rec_Load5(x1, x6, x7, x8)

Filtered unneeded terms:


Cond_f1788_0_rec_Load(x1, x2, x3, x4) → Cond_f1788_0_rec_Load(x1)
Cond_f1788_0_rec_Load2(x1, x2, x3, x4) → Cond_f1788_0_rec_Load2(x1)
Cond_f1788_0_rec_Load4(x1, x2, x3, x4) → Cond_f1788_0_rec_Load4(x1)

Prepared 6 rules for path length conversion:

P rules:
f1788_0_rec_Load(x1, x2, x0) → f1886_1_rec_Load(x0, x1, -(x2, 1)) | &&(&&(>=(x2, x1), >=(+(+(x0, x1), *(3, x2)), 0)), >=(x1, x0))
f1788_0_rec_Load(x1, x2, x0) → f1788_0_rec_Load(x1, -(x2, 1), x0) | &&(&&(>=(x2, x1), >=(+(+(x0, x1), *(3, x2)), 0)), >=(x1, x0))
f1788_0_rec_Load(x1, x2, x0) → f1887_1_rec_Load(x0, -(x1, 2), x2) | &&(&&(<(x2, x1), >=(+(+(x0, x1), *(3, x2)), 0)), >=(x1, x0))
f1788_0_rec_Load(x1, x2, x0) → f1788_0_rec_Load(-(x1, 2), x2, x0) | &&(&&(<(x2, x1), >=(+(+(x0, x1), *(3, x2)), 0)), >=(x1, x0))
f1788_0_rec_Load(x1, x2, x0) → f1866_1_rec_Load(-(x0, 1), x1, x2) | &&(>=(+(+(x0, x1), *(3, x2)), 0), <(x1, x0))
f1788_0_rec_Load(x1, x2, x0) → f1788_0_rec_Load(x1, x2, -(x0, 1)) | &&(>=(+(+(x0, x1), *(3, x2)), 0), <(x1, x0))

Finished conversion. Obtained 3 rules.

P rules:
f1788_0_rec_Load(x3, x4, x5) → f1788_0_rec_Load(x3, -(x4, 1), x5) | &&(&&(<=(x5, x3), >=(x4, x3)), >=(+(+(x5, x3), *(3, x4)), 0))
f1788_0_rec_Load(x9, x10, x11) → f1788_0_rec_Load(-(x9, 2), x10, x11) | &&(&&(>=(x9, x11), >=(+(+(x11, x9), *(3, x10)), 0)), >(x9, x10))
f1788_0_rec_Load(x15, x16, x17) → f1788_0_rec_Load(x15, x16, -(x17, 1)) | &&(>=(+(+(x17, x15), *(3, x16)), 0), >(x17, x15))

(6) Obligation:

Rules:
f1788_0_rec_Load(x3, x4, x5) → f1788_0_rec_Load(x3, -(x4, 1), x5) | &&(&&(<=(x5, x3), >=(x4, x3)), >=(+(+(x5, x3), *(3, x4)), 0))
f1788_0_rec_Load(x9, x10, x11) → f1788_0_rec_Load(-(x9, 2), x10, x11) | &&(&&(>=(x9, x11), >=(+(+(x11, x9), *(3, x10)), 0)), >(x9, x10))
f1788_0_rec_Load(x15, x16, x17) → f1788_0_rec_Load(x15, x16, -(x17, 1)) | &&(>=(+(+(x17, x15), *(3, x16)), 0), >(x17, x15))

(7) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:


[f1788_0_rec_Load(x)] = 1·x1 + 3·x2 + 1·x3

where x = (x1, ... ,xn).



Therefore the following rule(s) have been dropped:


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

(8) YES