Termination proof of /tmp/tmphvvLjq/NestedLoop.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 1006 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIntTRSProof (⇒, 3 ms)

        ↳7 intTRS

        ↳8 PolynomialOrderProcessor (⇔, 0 ms)

        ↳9 YES

    ↳10 JBCTerminationSCC

        ↳11 SCCToIntTRSProof (⇒, 146 ms)

        ↳12 intTRS

        ↳13 PolynomialOrderProcessor (⇒, 0 ms)

        ↳14 intTRS

        ↳15 LinearRankingProcessor (⇔, 0 ms)

        ↳16 YES

    ↳17 JBCTerminationSCC

        ↳18 SCCToIntTRSProof (⇒, 162 ms)

        ↳19 intTRS

        ↳20 PolynomialOrderProcessor (⇔, 0 ms)

        ↳21 YES

(0) Obligation:

JBC Problem based on JBC Program:

public class NestedLoop {
	public static void main(String[] args) {
		int i, j, z, n;
		n = args.length;
		int[] a = new int[n];
		for(i = 0;i< n-1;i++){
			a[i] = args[i].length();
		}

		for (i = 0; i < n - 1; i++) {
			for (j = i + 1; j < n; j++) {
				if(a[i]< a[j]){
					z = a[i]; a[i] = a[j]; a[j] = z;
				}
			}
		}
		for(i = 0;i< n -1;i++){
		}
	}
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
NestedLoop.main([Ljava/lang/String;)V: Graph of 349 nodes with 3 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: NestedLoop.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses:

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

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 9 IRules

P rules:
f2671_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i614, i241, i614) → f2698_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i241)), i614, i241, i614, i241)
f2698_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i241)), i614, i241, i614, i241) → f2772_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i241)), i614, i241, i614, i241, 1)
f2772_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i241)), i614, i241, i614, i241, matching1) → f2824_0_main_GE(EOS, java.lang.Object(ARRAY(i241)), i614, i241, i614, -(i241, 1)) | &&(>=(i241, 0), =(matching1, 1))
f2824_0_main_GE(EOS, java.lang.Object(ARRAY(i241)), i614, i241, i614, i628) → f2883_0_main_GE(EOS, java.lang.Object(ARRAY(i241)), i614, i241, i614, i628)
f2883_0_main_GE(EOS, java.lang.Object(ARRAY(i241)), i614, i241, i614, i628) → f3183_0_main_Inc(EOS, java.lang.Object(ARRAY(i241)), i614, i241) | <(i614, i628)
f3183_0_main_Inc(EOS, java.lang.Object(ARRAY(i241)), i614, i241) → f3232_0_main_JMP(EOS, java.lang.Object(ARRAY(i241)), +(i614, 1), i241) | >=(i614, 0)
f3232_0_main_JMP(EOS, java.lang.Object(ARRAY(i241)), i667, i241) → f3289_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i667, i241)
f3289_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i667, i241) → f2643_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i667, i241)
f2643_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i614, i241) → f2671_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i614, i241, i614)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:

f2671_0_main_Load(x1, x2, x3, x4, x5) → f2671_0_main_Load(x2, x3, x4, x5)
Cond_f2671_0_main_Load(x1, x2, x3, x4, x5, x6) → Cond_f2671_0_main_Load(x1, x3, x4, x5, x6)

Filtered duplicate terms:

f2671_0_main_Load(x1, x2, x3, x4) → f2671_0_main_Load(x1, x4)
Cond_f2671_0_main_Load(x1, x2, x3, x4, x5) → Cond_f2671_0_main_Load(x1, x2, x5)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

P rules:
f2671_0_main_Load(v5, x1, x0) → f2671_0_main_Load(v6, +(x1, 1), x0) | &&(&&(&&(&&(&&(>(x1, -1), <(x1, -(x0, 1))), >(x0, -1)), >(+(v6, 1), 1)), <=(v6, v5)), >(+(v5, 1), 1))

(7) Obligation:

Rules:
f2671_0_main_Load(v5, x1, x0) → f2671_0_main_Load(v6, +(x1, 1), x0) | &&(&&(&&(&&(&&(>(x1, -1), <(x1, -(x0, 1))), >(x0, -1)), >(+(v6, 1), 1)), <=(v6, v5)), >(+(v5, 1), 1))

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

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

Therefore the following rule(s) have been dropped:

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

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: NestedLoop.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses:

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

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 53 IRules

P rules:
f1660_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i241, java.lang.Object(ARRAY(i241)), i344) → f1661_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i241)), i344, i241, java.lang.Object(ARRAY(i241)), i344, i241)
f1661_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i241)), i344, i241, java.lang.Object(ARRAY(i241)), i344, i241) → f1663_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i241)), i344, i241, java.lang.Object(ARRAY(i241)), i344, i241, 1)
f1663_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i241)), i344, i241, java.lang.Object(ARRAY(i241)), i344, i241, matching1) → f1666_0_main_GE(EOS, java.lang.Object(ARRAY(i241)), i344, i241, java.lang.Object(ARRAY(i241)), i344, -(i241, 1)) | &&(>=(i241, 0), =(matching1, 1))
f1666_0_main_GE(EOS, java.lang.Object(ARRAY(i241)), i344, i241, java.lang.Object(ARRAY(i241)), i344, i346) → f1668_0_main_GE(EOS, java.lang.Object(ARRAY(i241)), i344, i241, java.lang.Object(ARRAY(i241)), i344, i346)
f1668_0_main_GE(EOS, java.lang.Object(ARRAY(i241)), i344, i241, java.lang.Object(ARRAY(i241)), i344, i346) → f1672_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i241, java.lang.Object(ARRAY(i241))) | <(i344, i346)
f1672_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i241, java.lang.Object(ARRAY(i241))) → f1676_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i241)), i344, i241, java.lang.Object(ARRAY(i241)), i344)
f1676_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i241)), i344, i241, java.lang.Object(ARRAY(i241)), i344) → f1679_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i241)), i344, i241, java.lang.Object(ARRAY(i241)), i344, 1)
f1679_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i241)), i344, i241, java.lang.Object(ARRAY(i241)), i344, matching1) → f1683_0_main_Store(EOS, java.lang.Object(ARRAY(i241)), i344, i241, java.lang.Object(ARRAY(i241)), +(i344, 1)) | &&(>=(i344, 0), =(matching1, 1))
f1683_0_main_Store(EOS, java.lang.Object(ARRAY(i241)), i344, i241, java.lang.Object(ARRAY(i241)), i347) → f1686_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)))
f1686_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241))) → f1690_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), i347)
f1690_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), i347) → f1694_0_main_GE(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), i347, i241)
f1694_0_main_GE(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), i347, i241) → f1700_0_main_GE(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), i347, i241)
f1694_0_main_GE(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), i347, i241) → f1701_0_main_GE(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), i347, i241)
f1700_0_main_GE(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), i347, i241) → f1706_0_main_Inc(EOS, java.lang.Object(ARRAY(i241)), i344, i241, java.lang.Object(ARRAY(i241))) | >=(i347, i241)
f1706_0_main_Inc(EOS, java.lang.Object(ARRAY(i241)), i344, i241, java.lang.Object(ARRAY(i241))) → f1712_0_main_JMP(EOS, java.lang.Object(ARRAY(i241)), +(i344, 1), i241, java.lang.Object(ARRAY(i241))) | >=(i344, 0)
f1712_0_main_JMP(EOS, java.lang.Object(ARRAY(i241)), i354, i241, java.lang.Object(ARRAY(i241))) → f1732_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i354, i241, java.lang.Object(ARRAY(i241)))
f1732_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i354, i241, java.lang.Object(ARRAY(i241))) → f1656_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i354, i241, java.lang.Object(ARRAY(i241)))
f1656_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i241, java.lang.Object(ARRAY(i241))) → f1660_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i241, java.lang.Object(ARRAY(i241)), i344)
f1701_0_main_GE(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), i347, i241) → f1707_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241))) | <(i347, i241)
f1707_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241))) → f1714_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)))
f1714_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241))) → f1735_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i344)
f1735_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i344) → f1997_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i344)
f1997_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i344) → f2001_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), i432) | <(i344, i241)
f2001_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), i432) → f2006_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), i432, java.lang.Object(ARRAY(i241)))
f2006_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), i432, java.lang.Object(ARRAY(i241))) → f2010_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), i432, java.lang.Object(ARRAY(i241)), i347)
f2010_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), i432, java.lang.Object(ARRAY(i241)), i347) → f2019_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), i432, java.lang.Object(ARRAY(i241)), i347)
f2019_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), i432, java.lang.Object(ARRAY(i241)), i347) → f2028_0_main_GE(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), i432, i440) | <(i347, i241)
f2028_0_main_GE(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), i432, i440) → f2035_0_main_GE(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), i432, i440)
f2028_0_main_GE(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), i432, i440) → f2036_0_main_GE(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), i432, i440)
f2035_0_main_GE(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), i432, i440) → f2052_0_main_Inc(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241))) | >=(i432, i440)
f2052_0_main_Inc(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241))) → f2706_0_main_Inc(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)))
f2706_0_main_Inc(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241))) → f2773_0_main_JMP(EOS, java.lang.Object(ARRAY(i241)), i344, +(i347, 1), i241, java.lang.Object(ARRAY(i241))) | >(i347, 0)
f2773_0_main_JMP(EOS, java.lang.Object(ARRAY(i241)), i344, i627, i241, java.lang.Object(ARRAY(i241))) → f2834_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i627, i241, java.lang.Object(ARRAY(i241)))
f2834_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i627, i241, java.lang.Object(ARRAY(i241))) → f1686_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i627, i241, java.lang.Object(ARRAY(i241)))
f2036_0_main_GE(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), i432, i440) → f2054_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241))) | <(i432, i440)
f2054_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241))) → f2066_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)))
f2066_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241))) → f2076_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i344)
f2076_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i344) → f2411_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i344)
f2411_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i344) → f2424_0_main_Store(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241))) | <(i344, i241)
f2424_0_main_Store(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241))) → f2432_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)))
f2432_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241))) → f2442_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)))
f2442_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241))) → f2461_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i344)
f2461_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i344) → f2475_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i344, java.lang.Object(ARRAY(i241)))
f2475_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i344, java.lang.Object(ARRAY(i241))) → f2485_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i344, java.lang.Object(ARRAY(i241)), i347)
f2485_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i344, java.lang.Object(ARRAY(i241)), i347) → f2502_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i344, java.lang.Object(ARRAY(i241)), i347)
f2502_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i344, java.lang.Object(ARRAY(i241)), i347) → f2515_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i344) | <(i347, i241)
f2515_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i344) → f2526_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i344)
f2526_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i344) → f2557_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241))) | <(i344, i241)
f2557_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241))) → f2583_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)))
f2583_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241))) → f2605_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i347)
f2605_0_main_Load(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i347) → f2645_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i347)
f2645_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i347) → f2673_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i347)
f2673_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241)), java.lang.Object(ARRAY(i241)), i347) → f2706_0_main_Inc(EOS, java.lang.Object(ARRAY(i241)), i344, i347, i241, java.lang.Object(ARRAY(i241))) | <(i347, i241)

Combined rules. Obtained 2 IRules

P rules:
f1694_0_main_GE(EOS, java.lang.Object(ARRAY(x0)), x1, x2, x0, java.lang.Object(ARRAY(x0)), x2, x0) → f1694_0_main_GE(EOS, java.lang.Object(ARRAY(x0)), +(x1, 1), +(x1, 2), x0, java.lang.Object(ARRAY(x0)), +(x1, 2), x0) | &&(&&(&&(>=(x2, x0), >(+(x1, 1), 0)), >(+(x0, 1), 0)), <(+(x1, 1), -(x0, 1)))
f1694_0_main_GE(EOS, java.lang.Object(ARRAY(x0)), x1, x2, x0, java.lang.Object(ARRAY(x0)), x2, x0) → f1694_0_main_GE(EOS, java.lang.Object(ARRAY(x0)), x1, +(x2, 1), x0, java.lang.Object(ARRAY(x0)), +(x2, 1), x0) | &&(&&(>(x2, 0), <(x2, x0)), <(x1, x0))

Filtered ground terms:

f1694_0_main_GE(x1, x2, x3, x4, x5, x6, x7, x8) → f1694_0_main_GE(x2, x3, x4, x5, x6, x7, x8)
Cond_f1694_0_main_GE(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f1694_0_main_GE(x1, x3, x4, x5, x6, x7, x8, x9)
Cond_f1694_0_main_GE1(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f1694_0_main_GE1(x1, x3, x4, x5, x6, x7, x8, x9)

Filtered duplicate terms:

f1694_0_main_GE(x1, x2, x3, x4, x5, x6, x7) → f1694_0_main_GE(x2, x5, x6)
Cond_f1694_0_main_GE(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1694_0_main_GE(x1, x3, x6, x7)
Cond_f1694_0_main_GE1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1694_0_main_GE1(x1, x3, x6, x7)

Filtered unneeded terms:

Cond_f1694_0_main_GE(x1, x2, x3, x4) → Cond_f1694_0_main_GE(x1, x2, x3)

Prepared 2 rules for path length conversion:

P rules:
f1694_0_main_GE(x1, java.lang.Object(ARRAY(x0)), x2, x0) → f1694_0_main_GE(+(x1, 1), java.lang.Object(ARRAY(x0)), +(x1, 2), x0) | &&(&&(&&(>=(x2, x0), >(+(x1, 1), 0)), >(+(x0, 1), 0)), <(+(x1, 1), -(x0, 1)))
f1694_0_main_GE(x1, java.lang.Object(ARRAY(x0)), x2, x0) → f1694_0_main_GE(x1, java.lang.Object(ARRAY(x0)), +(x2, 1), x0) | &&(&&(>(x2, 0), <(x2, x0)), <(x1, x0))

Finished conversion. Obtained 2 rules.

P rules:
f1694_0_main_GE(x0, v10, x2, x1) → f1694_0_main_GE(+(x0, 1), v11, +(x0, 2), x1) | &&(&&(&&(&&(&&(&&(>=(x2, x1), >(x1, -1)), >(-(x1, 1), +(x0, 1))), >(x0, -1)), >(+(v11, 1), 1)), <=(v11, v10)), >(+(v10, 1), 1))
f1694_0_main_GE(x3, v12, x5, x4) → f1694_0_main_GE(x3, v13, +(x5, 1), x4) | &&(&&(&&(&&(&&(>(x5, 0), <(x5, x4)), >(x4, x3)), >(+(v13, 1), 1)), <=(v13, v12)), >(+(v12, 1), 1))

(12) Obligation:

Rules:
f1694_0_main_GE(x0, v10, x2, x1) → f1694_0_main_GE(+(x0, 1), v11, +(x0, 2), x1) | &&(&&(&&(&&(&&(&&(>=(x2, x1), >(x1, -1)), >(-(x1, 1), +(x0, 1))), >(x0, -1)), >(+(v11, 1), 1)), <=(v11, v10)), >(+(v10, 1), 1))
f1694_0_main_GE(x3, v12, x5, x4) → f1694_0_main_GE(x3, v13, +(x5, 1), x4) | &&(&&(&&(&&(&&(>(x5, 0), <(x5, x4)), >(x4, x3)), >(+(v13, 1), 1)), <=(v13, v12)), >(+(v12, 1), 1))

(13) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:

[f1694_0_main_GE(x11, x13, x15, x17)] = -3 - x11 + 2·x17

Therefore the following rule(s) have been dropped:

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

(14) Obligation:

Rules:
f1694_0_main_GE(x5, x6, x7, x8) → f1694_0_main_GE(x5, x9, +(x7, 1), x8) | &&(&&(&&(&&(&&(>(x7, 0), <(x7, x8)), >(x8, x5)), >(+(x9, 1), 1)), <=(x9, x6)), >(+(x6, 1), 1))

(15) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:

[f1694_0_main_GE(x)] = (-1)·x₃ + 1·x₄

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

Therefore the following rule(s) have been dropped:

f1694_0_main_GE(x0, x1, x2, x3) → f1694_0_main_GE(x0, x4, +(x2, 1), x3) | &&(&&(&&(&&(&&(>(x2, 0), <(x2, x3)), >(x3, x0)), >(+(x4, 1), 1)), <=(x4, x1)), >(+(x1, 1), 1))

(16) YES

(17) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: NestedLoop.main([Ljava/lang/String;)V
SCC calls the following helper methods:
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:

(18) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 23 IRules

P rules:
f785_0_main_Load(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), i186) → f788_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), i186, i51)
f788_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), i186, i51) → f790_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), i186, i51, 1)
f790_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), i186, i51, matching1) → f793_0_main_GE(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), i186, -(i51, 1)) | &&(>=(i51, 0), =(matching1, 1))
f793_0_main_GE(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), i186, i192) → f796_0_main_GE(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), i186, i192)
f796_0_main_GE(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), i186, i192) → f800_0_main_Load(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51))) | <(i186, i192)
f800_0_main_Load(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51))) → f803_0_main_Load(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)))
f803_0_main_Load(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51))) → f807_0_main_Load(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186)
f807_0_main_Load(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186) → f811_0_main_Load(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, java.lang.Object(ARRAY(i51)))
f811_0_main_Load(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, java.lang.Object(ARRAY(i51))) → f817_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, java.lang.Object(ARRAY(i51)), i186)
f817_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, java.lang.Object(ARRAY(i51)), i186) → f822_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, java.lang.Object(ARRAY(i51)), i186)
f822_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, java.lang.Object(ARRAY(i51)), i186) → f830_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, o68) | <(i186, i51)
f830_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, java.lang.Object(o72sub)) → f838_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, java.lang.Object(o72sub))
f838_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, java.lang.Object(o72sub)) → f847_0_length_Load(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, java.lang.Object(o72sub), java.lang.Object(o72sub))
f847_0_length_Load(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, java.lang.Object(o72sub), java.lang.Object(o72sub)) → f867_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, java.lang.Object(o72sub), java.lang.Object(o72sub))
f867_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, java.lang.Object(java.lang.String(o77sub, i209)), java.lang.Object(java.lang.String(o77sub, i209))) → f874_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, java.lang.Object(java.lang.String(o77sub, i209)), java.lang.Object(java.lang.String(o77sub, i209)))
f874_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, java.lang.Object(java.lang.String(o77sub, i209)), java.lang.Object(java.lang.String(o77sub, i209))) → f885_0_length_Return(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, java.lang.Object(java.lang.String(o77sub, i209)))
f885_0_length_Return(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, java.lang.Object(java.lang.String(o77sub, i209))) → f898_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186)
f898_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186) → f906_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186)
f906_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186) → f923_0_main_Inc(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51))) | <(i186, i51)
f923_0_main_Inc(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51))) → f941_0_main_JMP(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), +(i186, 1), i51, java.lang.Object(ARRAY(i51))) | >=(i186, 0)
f941_0_main_JMP(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i225, i51, java.lang.Object(ARRAY(i51))) → f974_0_main_Load(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i225, i51, java.lang.Object(ARRAY(i51)))
f974_0_main_Load(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i225, i51, java.lang.Object(ARRAY(i51))) → f778_0_main_Load(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i225, i51, java.lang.Object(ARRAY(i51)))
f778_0_main_Load(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51))) → f785_0_main_Load(EOS, java.lang.Object(ARRAY(i51)), java.lang.Object(ARRAY(i51)), i186, i51, java.lang.Object(ARRAY(i51)), i186)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:

f785_0_main_Load(x1, x2, x3, x4, x5, x6, x7) → f785_0_main_Load(x2, x3, x4, x5, x6, x7)
Cond_f785_0_main_Load(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f785_0_main_Load(x1, x3, x4, x5, x6, x7, x8)

Filtered duplicate terms:

f785_0_main_Load(x1, x2, x3, x4, x5, x6) → f785_0_main_Load(x5, x6)
Cond_f785_0_main_Load(x1, x2, x3, x4, x5, x6, x7) → Cond_f785_0_main_Load(x1, x6, x7)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

P rules:
f785_0_main_Load(v5, x1, x0) → f785_0_main_Load(v6, +(x1, 1), x0) | &&(&&(&&(&&(&&(&&(>(x1, -1), <(x1, -(x0, 1))), <(x1, x0)), >(x0, -1)), >(+(v6, 1), 1)), <=(v6, v5)), >(+(v5, 1), 1))

(19) Obligation:

Rules:
f785_0_main_Load(v5, x1, x0) → f785_0_main_Load(v6, +(x1, 1), x0) | &&(&&(&&(&&(&&(&&(>(x1, -1), <(x1, -(x0, 1))), <(x1, x0)), >(x0, -1)), >(+(v6, 1), 1)), <=(v6, v5)), >(+(v5, 1), 1))

(20) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

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

Therefore the following rule(s) have been dropped:

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

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIntTRSProof (SOUND transformation)

(7) Obligation:

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

(9) YES

(10) Obligation:

(11) SCCToIntTRSProof (SOUND transformation)

(12) Obligation:

(13) PolynomialOrderProcessor (SOUND transformation)

(14) Obligation:

(15) LinearRankingProcessor (EQUIVALENT transformation)

(16) YES

(17) Obligation:

(18) SCCToIntTRSProof (SOUND transformation)

(19) Obligation:

(20) PolynomialOrderProcessor (EQUIVALENT transformation)

(21) YES