Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

public class Test9 {
    public static void main(String[] args) {
	long l = args.length;

	while (l > 0) {
	    for (int i = (int) l ; i < 100; i++)
		test(i);
	    l--;
	}
    }

    private static void test(int i) {
	int j, k, l, m;

	for (j = i; j > 0; j--);
	for (k = i; k > 0; k--);
	for (l = i; l > 0; l--);
	for (m = i; m > 0; m--);
	for (j = i; j > 0; j--);
	for (k = i; k > 0; k--);
	for (l = i; l > 0; l--);
	for (m = i; m > 0; m--);
	for (j = i; j > 0; j--);
	for (k = i; k > 0; k--);
	for (l = i; l > 0; l--);
	for (m = i; m > 0; m--);
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

Test9.test(I)V: Graph of 122 nodes with 12 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 13 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test9.test(I)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 6 IRules

P rules:
f892_0_test_LE(EOS, i239, i239) → f895_0_test_LE(EOS, i239, i239)
f895_0_test_LE(EOS, i239, i239) → f900_0_test_Inc(EOS, i239) | >(i239, 0)
f900_0_test_Inc(EOS, i239) → f906_0_test_JMP(EOS, +(i239, -1)) | >(i239, 0)
f906_0_test_JMP(EOS, i242) → f959_0_test_Load(EOS, i242)
f959_0_test_Load(EOS, i242) → f887_0_test_Load(EOS, i242)
f887_0_test_Load(EOS, i231) → f892_0_test_LE(EOS, i231, i231)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:

f892_0_test_LE(x1, x2, x3) → f892_0_test_LE(x2, x3)
Cond_f892_0_test_LE(x1, x2, x3, x4) → Cond_f892_0_test_LE(x1, x3, x4)

Filtered duplicate terms:

f892_0_test_LE(x1, x2) → f892_0_test_LE(x2)
Cond_f892_0_test_LE(x1, x2, x3) → Cond_f892_0_test_LE(x1, x3)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(7) Obligation:

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

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f892_0_test_LE(x2)] = x2

Therefore the following rule(s) have been dropped:

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

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test9.test(I)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 6 IRules

P rules:
f838_0_test_LE(EOS, i221, i221) → f842_0_test_LE(EOS, i221, i221)
f842_0_test_LE(EOS, i221, i221) → f847_0_test_Inc(EOS, i221) | >(i221, 0)
f847_0_test_Inc(EOS, i221) → f852_0_test_JMP(EOS, +(i221, -1)) | >(i221, 0)
f852_0_test_JMP(EOS, i222) → f862_0_test_Load(EOS, i222)
f862_0_test_Load(EOS, i222) → f833_0_test_Load(EOS, i222)
f833_0_test_Load(EOS, i212) → f838_0_test_LE(EOS, i212, i212)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:

f838_0_test_LE(x1, x2, x3) → f838_0_test_LE(x2, x3)
Cond_f838_0_test_LE(x1, x2, x3, x4) → Cond_f838_0_test_LE(x1, x3, x4)

Filtered duplicate terms:

f838_0_test_LE(x1, x2) → f838_0_test_LE(x2)
Cond_f838_0_test_LE(x1, x2, x3) → Cond_f838_0_test_LE(x1, x3)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(12) Obligation:

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

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f838_0_test_LE(x2)] = x2

Therefore the following rule(s) have been dropped:

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

(14) YES

(15) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test9.test(I)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:
  

(16) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 6 IRules

P rules:
f780_0_test_LE(EOS, i203, i203) → f784_0_test_LE(EOS, i203, i203)
f784_0_test_LE(EOS, i203, i203) → f789_0_test_Inc(EOS, i203) | >(i203, 0)
f789_0_test_Inc(EOS, i203) → f795_0_test_JMP(EOS, +(i203, -1)) | >(i203, 0)
f795_0_test_JMP(EOS, i205) → f805_0_test_Load(EOS, i205)
f805_0_test_Load(EOS, i205) → f776_0_test_Load(EOS, i205)
f776_0_test_Load(EOS, i197) → f780_0_test_LE(EOS, i197, i197)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:

f780_0_test_LE(x1, x2, x3) → f780_0_test_LE(x2, x3)
Cond_f780_0_test_LE(x1, x2, x3, x4) → Cond_f780_0_test_LE(x1, x3, x4)

Filtered duplicate terms:

f780_0_test_LE(x1, x2) → f780_0_test_LE(x2)
Cond_f780_0_test_LE(x1, x2, x3) → Cond_f780_0_test_LE(x1, x3)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(17) Obligation:

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

(18) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f780_0_test_LE(x2)] = x2

Therefore the following rule(s) have been dropped:

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

(19) YES

(20) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test9.test(I)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:
  

(21) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 6 IRules

P rules:
f733_0_test_LE(EOS, i192, i192) → f736_0_test_LE(EOS, i192, i192)
f736_0_test_LE(EOS, i192, i192) → f740_0_test_Inc(EOS, i192) | >(i192, 0)
f740_0_test_Inc(EOS, i192) → f745_0_test_JMP(EOS, +(i192, -1)) | >(i192, 0)
f745_0_test_JMP(EOS, i194) → f752_0_test_Load(EOS, i194)
f752_0_test_Load(EOS, i194) → f730_0_test_Load(EOS, i194)
f730_0_test_Load(EOS, i186) → f733_0_test_LE(EOS, i186, i186)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:

f733_0_test_LE(x1, x2, x3) → f733_0_test_LE(x2, x3)
Cond_f733_0_test_LE(x1, x2, x3, x4) → Cond_f733_0_test_LE(x1, x3, x4)

Filtered duplicate terms:

f733_0_test_LE(x1, x2) → f733_0_test_LE(x2)
Cond_f733_0_test_LE(x1, x2, x3) → Cond_f733_0_test_LE(x1, x3)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(22) Obligation:

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

(23) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f733_0_test_LE(x2)] = x2

Therefore the following rule(s) have been dropped:

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

(24) YES

(25) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test9.test(I)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:
  

(26) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 6 IRules

P rules:
f692_0_test_LE(EOS, i177, i177) → f695_0_test_LE(EOS, i177, i177)
f695_0_test_LE(EOS, i177, i177) → f699_0_test_Inc(EOS, i177) | >(i177, 0)
f699_0_test_Inc(EOS, i177) → f703_0_test_JMP(EOS, +(i177, -1)) | >(i177, 0)
f703_0_test_JMP(EOS, i179) → f709_0_test_Load(EOS, i179)
f709_0_test_Load(EOS, i179) → f688_0_test_Load(EOS, i179)
f688_0_test_Load(EOS, i170) → f692_0_test_LE(EOS, i170, i170)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:

f692_0_test_LE(x1, x2, x3) → f692_0_test_LE(x2, x3)
Cond_f692_0_test_LE(x1, x2, x3, x4) → Cond_f692_0_test_LE(x1, x3, x4)

Filtered duplicate terms:

f692_0_test_LE(x1, x2) → f692_0_test_LE(x2)
Cond_f692_0_test_LE(x1, x2, x3) → Cond_f692_0_test_LE(x1, x3)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(27) Obligation:

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

(28) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f692_0_test_LE(x2)] = x2

Therefore the following rule(s) have been dropped:

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

(29) YES

(30) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test9.test(I)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:
  

(31) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 6 IRules

P rules:
f650_0_test_LE(EOS, i165, i165) → f654_0_test_LE(EOS, i165, i165)
f654_0_test_LE(EOS, i165, i165) → f658_0_test_Inc(EOS, i165) | >(i165, 0)
f658_0_test_Inc(EOS, i165) → f662_0_test_JMP(EOS, +(i165, -1)) | >(i165, 0)
f662_0_test_JMP(EOS, i166) → f669_0_test_Load(EOS, i166)
f669_0_test_Load(EOS, i166) → f647_0_test_Load(EOS, i166)
f647_0_test_Load(EOS, i161) → f650_0_test_LE(EOS, i161, i161)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:

f650_0_test_LE(x1, x2, x3) → f650_0_test_LE(x2, x3)
Cond_f650_0_test_LE(x1, x2, x3, x4) → Cond_f650_0_test_LE(x1, x3, x4)

Filtered duplicate terms:

f650_0_test_LE(x1, x2) → f650_0_test_LE(x2)
Cond_f650_0_test_LE(x1, x2, x3) → Cond_f650_0_test_LE(x1, x3)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(32) Obligation:

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

(33) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f650_0_test_LE(x2)] = x2

Therefore the following rule(s) have been dropped:

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

(34) YES

(35) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test9.test(I)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:
  

(36) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 6 IRules

P rules:
f609_0_test_LE(EOS, i153, i153) → f613_0_test_LE(EOS, i153, i153)
f613_0_test_LE(EOS, i153, i153) → f617_0_test_Inc(EOS, i153) | >(i153, 0)
f617_0_test_Inc(EOS, i153) → f621_0_test_JMP(EOS, +(i153, -1)) | >(i153, 0)
f621_0_test_JMP(EOS, i155) → f628_0_test_Load(EOS, i155)
f628_0_test_Load(EOS, i155) → f606_0_test_Load(EOS, i155)
f606_0_test_Load(EOS, i145) → f609_0_test_LE(EOS, i145, i145)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:

f609_0_test_LE(x1, x2, x3) → f609_0_test_LE(x2, x3)
Cond_f609_0_test_LE(x1, x2, x3, x4) → Cond_f609_0_test_LE(x1, x3, x4)

Filtered duplicate terms:

f609_0_test_LE(x1, x2) → f609_0_test_LE(x2)
Cond_f609_0_test_LE(x1, x2, x3) → Cond_f609_0_test_LE(x1, x3)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(37) Obligation:

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

(38) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f609_0_test_LE(x2)] = x2

Therefore the following rule(s) have been dropped:

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

(39) YES

(40) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test9.test(I)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:
  

(41) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 6 IRules

P rules:
f566_0_test_LE(EOS, i138, i138) → f570_0_test_LE(EOS, i138, i138)
f570_0_test_LE(EOS, i138, i138) → f575_0_test_Inc(EOS, i138) | >(i138, 0)
f575_0_test_Inc(EOS, i138) → f579_0_test_JMP(EOS, +(i138, -1)) | >(i138, 0)
f579_0_test_JMP(EOS, i140) → f587_0_test_Load(EOS, i140)
f587_0_test_Load(EOS, i140) → f564_0_test_Load(EOS, i140)
f564_0_test_Load(EOS, i132) → f566_0_test_LE(EOS, i132, i132)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:

f566_0_test_LE(x1, x2, x3) → f566_0_test_LE(x2, x3)
Cond_f566_0_test_LE(x1, x2, x3, x4) → Cond_f566_0_test_LE(x1, x3, x4)

Filtered duplicate terms:

f566_0_test_LE(x1, x2) → f566_0_test_LE(x2)
Cond_f566_0_test_LE(x1, x2, x3) → Cond_f566_0_test_LE(x1, x3)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(42) Obligation:

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

(43) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f566_0_test_LE(x2)] = x2

Therefore the following rule(s) have been dropped:

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

(44) YES

(45) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test9.test(I)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:
  

(46) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 6 IRules

P rules:
f525_0_test_LE(EOS, i123, i123) → f528_0_test_LE(EOS, i123, i123)
f528_0_test_LE(EOS, i123, i123) → f533_0_test_Inc(EOS, i123) | >(i123, 0)
f533_0_test_Inc(EOS, i123) → f537_0_test_JMP(EOS, +(i123, -1)) | >(i123, 0)
f537_0_test_JMP(EOS, i127) → f544_0_test_Load(EOS, i127)
f544_0_test_Load(EOS, i127) → f521_0_test_Load(EOS, i127)
f521_0_test_Load(EOS, i118) → f525_0_test_LE(EOS, i118, i118)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:

f525_0_test_LE(x1, x2, x3) → f525_0_test_LE(x2, x3)
Cond_f525_0_test_LE(x1, x2, x3, x4) → Cond_f525_0_test_LE(x1, x3, x4)

Filtered duplicate terms:

f525_0_test_LE(x1, x2) → f525_0_test_LE(x2)
Cond_f525_0_test_LE(x1, x2, x3) → Cond_f525_0_test_LE(x1, x3)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(47) Obligation:

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

(48) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f525_0_test_LE(x2)] = x2

Therefore the following rule(s) have been dropped:

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

(49) YES

(50) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test9.test(I)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:
  

(51) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 6 IRules

P rules:
f482_0_test_LE(EOS, i110, i110) → f486_0_test_LE(EOS, i110, i110)
f486_0_test_LE(EOS, i110, i110) → f490_0_test_Inc(EOS, i110) | >(i110, 0)
f490_0_test_Inc(EOS, i110) → f494_0_test_JMP(EOS, +(i110, -1)) | >(i110, 0)
f494_0_test_JMP(EOS, i112) → f502_0_test_Load(EOS, i112)
f502_0_test_Load(EOS, i112) → f478_0_test_Load(EOS, i112)
f478_0_test_Load(EOS, i104) → f482_0_test_LE(EOS, i104, i104)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:

f482_0_test_LE(x1, x2, x3) → f482_0_test_LE(x2, x3)
Cond_f482_0_test_LE(x1, x2, x3, x4) → Cond_f482_0_test_LE(x1, x3, x4)

Filtered duplicate terms:

f482_0_test_LE(x1, x2) → f482_0_test_LE(x2)
Cond_f482_0_test_LE(x1, x2, x3) → Cond_f482_0_test_LE(x1, x3)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(52) Obligation:

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

(53) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f482_0_test_LE(x2)] = x2

Therefore the following rule(s) have been dropped:

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

(54) YES

(55) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test9.test(I)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:
  

(56) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 6 IRules

P rules:
f441_0_test_LE(EOS, i99, i99) → f444_0_test_LE(EOS, i99, i99)
f444_0_test_LE(EOS, i99, i99) → f448_0_test_Inc(EOS, i99) | >(i99, 0)
f448_0_test_Inc(EOS, i99) → f452_0_test_JMP(EOS, +(i99, -1)) | >(i99, 0)
f452_0_test_JMP(EOS, i100) → f460_0_test_Load(EOS, i100)
f460_0_test_Load(EOS, i100) → f437_0_test_Load(EOS, i100)
f437_0_test_Load(EOS, i94) → f441_0_test_LE(EOS, i94, i94)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:

f441_0_test_LE(x1, x2, x3) → f441_0_test_LE(x2, x3)
Cond_f441_0_test_LE(x1, x2, x3, x4) → Cond_f441_0_test_LE(x1, x3, x4)

Filtered duplicate terms:

f441_0_test_LE(x1, x2) → f441_0_test_LE(x2)
Cond_f441_0_test_LE(x1, x2, x3) → Cond_f441_0_test_LE(x1, x3)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(57) Obligation:

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

(58) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f441_0_test_LE(x2)] = x2

Therefore the following rule(s) have been dropped:

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

(59) YES

(60) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test9.test(I)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:
  

(61) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 6 IRules

P rules:
f399_0_test_LE(EOS, i84, i84) → f402_0_test_LE(EOS, i84, i84)
f402_0_test_LE(EOS, i84, i84) → f406_0_test_Inc(EOS, i84) | >(i84, 0)
f406_0_test_Inc(EOS, i84) → f411_0_test_JMP(EOS, +(i84, -1)) | >(i84, 0)
f411_0_test_JMP(EOS, i86) → f418_0_test_Load(EOS, i86)
f418_0_test_Load(EOS, i86) → f394_0_test_Load(EOS, i86)
f394_0_test_Load(EOS, i80) → f399_0_test_LE(EOS, i80, i80)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:

f399_0_test_LE(x1, x2, x3) → f399_0_test_LE(x2, x3)
Cond_f399_0_test_LE(x1, x2, x3, x4) → Cond_f399_0_test_LE(x1, x3, x4)

Filtered duplicate terms:

f399_0_test_LE(x1, x2) → f399_0_test_LE(x2)
Cond_f399_0_test_LE(x1, x2, x3) → Cond_f399_0_test_LE(x1, x3)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(62) Obligation:

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

(63) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f399_0_test_LE(x2)] = x2

Therefore the following rule(s) have been dropped:

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

(64) YES

(65) Obligation:

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

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

(66) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 29 IRules

P rules:
f59_0_main_ConstantStackPush(EOS, i3, i3) → f60_0_main_Cmp(EOS, i3, i3, 0)
f60_0_main_Cmp(EOS, i6, i6, matching1) → f64_0_main_Cmp(EOS, i6, i6, 0) | =(matching1, 0)
f64_0_main_Cmp(EOS, i6, i6, matching1) → f75_0_main_LE(EOS, i6, 1) | &&(>(i6, 0), =(matching1, 0))
f75_0_main_LE(EOS, i6, matching1) → f78_0_main_Load(EOS, i6) | &&(>(1, 0), =(matching1, 1))
f78_0_main_Load(EOS, i6) → f83_0_main_TypeCast(EOS, i6, i6)
f83_0_main_TypeCast(EOS, i6, i6) → f85_0_main_Store(EOS, i6, i10) | =(i10, i6)
f85_0_main_Store(EOS, i6, i10) → f88_0_main_Load(EOS, i6, i10)
f88_0_main_Load(EOS, i6, i10) → f89_0_main_ConstantStackPush(EOS, i6, i10, i10)
f89_0_main_ConstantStackPush(EOS, i6, i10, i10) → f90_0_main_GE(EOS, i6, i10, i10, 100)
f90_0_main_GE(EOS, i6, i13, i13, matching1) → f91_0_main_GE(EOS, i6, i13, i13, 100) | =(matching1, 100)
f90_0_main_GE(EOS, i6, i14, i14, matching1) → f92_0_main_GE(EOS, i6, i14, i14, 100) | =(matching1, 100)
f91_0_main_GE(EOS, i6, i13, i13, matching1) → f93_0_main_Load(EOS, i6, i13) | &&(<(i13, 100), =(matching1, 100))
f93_0_main_Load(EOS, i6, i13) → f95_0_main_InvokeMethod(EOS, i6, i13, i13)
f95_0_main_InvokeMethod(EOS, i6, i13, i13) → f98_0_test_Load(EOS, i13, i13)
f95_0_main_InvokeMethod(EOS, i6, i13, i13) → f98_1_test_Load(EOS, i6, i13, i13, i13)
f98_0_test_Load(EOS, i13, i13) → f101_0_test_Load(EOS, i13, i13)
f960_0_test_Return(EOS, i6, i253, i253) → f962_0_main_Inc(EOS, i6, i253)
f962_0_main_Inc(EOS, i6, i253) → f964_0_main_JMP(EOS, i6, +(i253, 1)) | >(i253, 0)
f964_0_main_JMP(EOS, i6, i259) → f971_0_main_Load(EOS, i6, i259)
f971_0_main_Load(EOS, i6, i259) → f88_0_main_Load(EOS, i6, i259)
f92_0_main_GE(EOS, i6, i14, i14, matching1) → f94_0_main_Load(EOS, i6) | &&(>=(i14, 100), =(matching1, 100))
f94_0_main_Load(EOS, i6) → f96_0_main_ConstantStackPush(EOS, i6)
f96_0_main_ConstantStackPush(EOS, i6) → f100_0_main_IntArithmetic(EOS, i6, 1)
f100_0_main_IntArithmetic(EOS, i6, matching1) → f104_0_main_Store(EOS, -(i6, 1)) | &&(>(i6, 0), =(matching1, 1))
f104_0_main_Store(EOS, i16) → f108_0_main_JMP(EOS, i16)
f108_0_main_JMP(EOS, i16) → f135_0_main_Load(EOS, i16)
f135_0_main_Load(EOS, i16) → f57_0_main_Load(EOS, i16)
f57_0_main_Load(EOS, i3) → f59_0_main_ConstantStackPush(EOS, i3, i3)
f98_1_test_Load(EOS, i6, i253, i253, i253) → f960_0_test_Return(EOS, i6, i253, i253)

Combined rules. Obtained 3 IRules

P rules:
f90_0_main_GE(EOS, x0, x1, x1, 100) → f101_0_test_Load(EOS, x1, x1) | <(x1, 100)
f90_0_main_GE(EOS, x0, x1, x1, 100) → f90_0_main_GE(EOS, -(x0, 1), -(x0, 1), -(x0, 1), 100) | &&(>(x0, 1), >(+(x1, 1), 100))
f90_0_main_GE(EOS, x0, x1, x1, 100) → f90_0_main_GE(EOS, x0, +(x1, 1), +(x1, 1), 100) | &&(<(x1, 100), >(x1, 0))

Filtered ground terms:

f90_0_main_GE(x1, x2, x3, x4, x5) → f90_0_main_GE(x2, x3, x4)
Cond_f90_0_main_GE(x1, x2, x3, x4, x5, x6) → Cond_f90_0_main_GE(x1, x3, x4, x5)
f101_0_test_Load(x1, x2, x3) → f101_0_test_Load(x2, x3)
Cond_f90_0_main_GE1(x1, x2, x3, x4, x5, x6) → Cond_f90_0_main_GE1(x1, x3, x4, x5)
Cond_f90_0_main_GE2(x1, x2, x3, x4, x5, x6) → Cond_f90_0_main_GE2(x1, x3, x4, x5)

Filtered duplicate terms:

f90_0_main_GE(x1, x2, x3) → f90_0_main_GE(x1, x3)
Cond_f90_0_main_GE(x1, x2, x3, x4) → Cond_f90_0_main_GE(x1, x2, x4)
f101_0_test_Load(x1, x2) → f101_0_test_Load(x2)
Cond_f90_0_main_GE1(x1, x2, x3, x4) → Cond_f90_0_main_GE1(x1, x2, x4)
Cond_f90_0_main_GE2(x1, x2, x3, x4) → Cond_f90_0_main_GE2(x1, x2, x4)

Filtered unneeded terms:

Cond_f90_0_main_GE(x1, x2, x3) → Cond_f90_0_main_GE(x1)
Cond_f90_0_main_GE1(x1, x2, x3) → Cond_f90_0_main_GE1(x1, x2)

Prepared 3 rules for path length conversion:

P rules:
f90_0_main_GE(x0, x1) → f101_0_test_Load(x1) | <(x1, 100)
f90_0_main_GE(x0, x1) → f90_0_main_GE(-(x0, 1), -(x0, 1)) | &&(>(x0, 1), >(+(x1, 1), 100))
f90_0_main_GE(x0, x1) → f90_0_main_GE(x0, +(x1, 1)) | &&(<(x1, 100), >(x1, 0))

Finished conversion. Obtained 2 rules.

P rules:
f90_0_main_GE(x2, x3) → f90_0_main_GE(-(x2, 1), -(x2, 1)) | &&(>(x2, 1), >(x3, 99))
f90_0_main_GE(x4, x5) → f90_0_main_GE(x4, +(x5, 1)) | &&(<(x5, 100), >(x5, 0))

(67) Obligation:

Rules:
f90_0_main_GE(x2, x3) → f90_0_main_GE(-(x2, 1), -(x2, 1)) | &&(>(x2, 1), >(x3, 99))
f90_0_main_GE(x4, x5) → f90_0_main_GE(x4, +(x5, 1)) | &&(<(x5, 100), >(x5, 0))

(68) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:

[f90_0_main_GE(x5, x7)] = -1 + x5

Therefore the following rule(s) have been dropped:

f90_0_main_GE(x0, x1) → f90_0_main_GE(-(x0, 1), -(x0, 1)) | &&(>(x0, 1), >(x1, 99))

(69) Obligation:

Rules:
f90_0_main_GE(x2, x3) → f90_0_main_GE(x2, +(x3, 1)) | &&(<(x3, 100), >(x3, 0))

(70) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f90_0_main_GE(x3, x5)] = 99 - x5

Therefore the following rule(s) have been dropped:

f90_0_main_GE(x0, x1) → f90_0_main_GE(x0, +(x1, 1)) | &&(<(x1, 100), >(x1, 0))

(71) YES