Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

package example_1;

public class A {

	int incr(int i) {
		return i=i+1;
	}
}


package example_1;

public class B extends A {
	int incr(int i) {
		return i = i+2;
	}
}



package example_1;

public class C extends B {
	int incr(int i) {
		return i=i+3;
	}
}


package example_1;

public class Test {

	public int add(int n,A o){
		int res=0;
		int i=0;
		while (i<=n){
			res=res+i;
			i=o.incr(i);
		}    
		return res;
	}

	public static void main(String[] args) {
		int test = 1000;
		Test testClass = new Test();
		A a = new A();
		int result1 = testClass.add(test,a);
		a = new B();
		int result2 = testClass.add(test,a);
		a = new C(); 
		int result3 = testClass.add(test,a);     
		// System.out.println("Result: "+result1 + result2 + result3);
	}
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
example_1.Test.main([Ljava/lang/String;)V: Graph of 175 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: example_1.Test.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 20 IRules

P rules:
f15613_0_add_Load(EOS, matching1, matching2, i166, i166) → f15614_0_add_GT(EOS, 1000, 1000, i166, i166, 1000) | &&(=(matching1, 1000), =(matching2, 1000))
f15614_0_add_GT(EOS, matching1, matching2, i171, i171, matching3) → f15615_0_add_GT(EOS, 1000, 1000, i171, i171, 1000) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f15615_0_add_GT(EOS, matching1, matching2, i171, i171, matching3) → f15617_0_add_Load(EOS, 1000, 1000, i171) | &&(&&(&&(<=(i171, 1000), =(matching1, 1000)), =(matching2, 1000)), =(matching3, 1000))
f15617_0_add_Load(EOS, matching1, matching2, i171) → f15619_0_add_Load(EOS, 1000, 1000, i171) | &&(=(matching1, 1000), =(matching2, 1000))
f15619_0_add_Load(EOS, matching1, matching2, i171) → f15621_0_add_IntArithmetic(EOS, 1000, 1000, i171, i171) | &&(=(matching1, 1000), =(matching2, 1000))
f15621_0_add_IntArithmetic(EOS, matching1, matching2, i171, i171) → f15623_0_add_Store(EOS, 1000, 1000, i171) | &&(&&(>=(i171, 0), =(matching1, 1000)), =(matching2, 1000))
f15623_0_add_Store(EOS, matching1, matching2, i171) → f15625_0_add_Load(EOS, 1000, 1000, i171) | &&(=(matching1, 1000), =(matching2, 1000))
f15625_0_add_Load(EOS, matching1, matching2, i171) → f15627_0_add_Load(EOS, 1000, 1000, i171) | &&(=(matching1, 1000), =(matching2, 1000))
f15627_0_add_Load(EOS, matching1, matching2, i171) → f15628_0_add_InvokeMethod(EOS, 1000, 1000, i171) | &&(=(matching1, 1000), =(matching2, 1000))
f15628_0_add_InvokeMethod(EOS, matching1, matching2, i171) → f15629_0_incr_Load(EOS, 1000, 1000, i171, i171) | &&(=(matching1, 1000), =(matching2, 1000))
f15629_0_incr_Load(EOS, matching1, matching2, i171, i171) → f15630_0_incr_ConstantStackPush(EOS, 1000, 1000, i171, i171) | &&(=(matching1, 1000), =(matching2, 1000))
f15630_0_incr_ConstantStackPush(EOS, matching1, matching2, i171, i171) → f15631_0_incr_IntArithmetic(EOS, 1000, 1000, i171, i171, 3) | &&(=(matching1, 1000), =(matching2, 1000))
f15631_0_incr_IntArithmetic(EOS, matching1, matching2, i171, i171, matching3) → f15632_0_incr_Duplicate(EOS, 1000, 1000, i171, +(i171, 3)) | &&(&&(&&(>=(i171, 0), =(matching1, 1000)), =(matching2, 1000)), =(matching3, 3))
f15632_0_incr_Duplicate(EOS, matching1, matching2, i171, i178) → f15633_0_incr_Store(EOS, 1000, 1000, i171, i178, i178) | &&(=(matching1, 1000), =(matching2, 1000))
f15633_0_incr_Store(EOS, matching1, matching2, i171, i178, i178) → f15634_0_incr_Return(EOS, 1000, 1000, i171, i178) | &&(=(matching1, 1000), =(matching2, 1000))
f15634_0_incr_Return(EOS, matching1, matching2, i171, i178) → f15635_0_add_Store(EOS, 1000, 1000, i178) | &&(=(matching1, 1000), =(matching2, 1000))
f15635_0_add_Store(EOS, matching1, matching2, i178) → f15636_0_add_JMP(EOS, 1000, 1000, i178) | &&(=(matching1, 1000), =(matching2, 1000))
f15636_0_add_JMP(EOS, matching1, matching2, i178) → f15637_0_add_Load(EOS, 1000, 1000, i178) | &&(=(matching1, 1000), =(matching2, 1000))
f15637_0_add_Load(EOS, matching1, matching2, i178) → f15612_0_add_Load(EOS, 1000, 1000, i178) | &&(=(matching1, 1000), =(matching2, 1000))
f15612_0_add_Load(EOS, matching1, matching2, i166) → f15613_0_add_Load(EOS, 1000, 1000, i166, i166) | &&(=(matching1, 1000), =(matching2, 1000))

Combined rules. Obtained 1 IRules

P rules:
f15613_0_add_Load(EOS, 1000, 1000, x2, x2) → f15613_0_add_Load(EOS, 1000, 1000, +(x2, 3), +(x2, 3)) | &&(>(+(x2, 1), 0), <=(x2, 1000))

Filtered ground terms:

f15613_0_add_Load(x1, x2, x3, x4, x5) → f15613_0_add_Load(x4, x5)
Cond_f15613_0_add_Load(x1, x2, x3, x4, x5, x6) → Cond_f15613_0_add_Load(x1, x5, x6)

Filtered duplicate terms:

f15613_0_add_Load(x1, x2) → f15613_0_add_Load(x2)
Cond_f15613_0_add_Load(x1, x2, x3) → Cond_f15613_0_add_Load(x1, x3)

Prepared 1 rules for path length conversion:

P rules:
f15613_0_add_Load(x2) → f15613_0_add_Load(+(x2, 3)) | &&(>(+(x2, 1), 0), <=(x2, 1000))

Finished conversion. Obtained 1 rules.

P rules:
f15613_0_add_Load(x0) → f15613_0_add_Load(+(x0, 3)) | &&(<=(x0, 1000), >(x0, -1))

(7) Obligation:

Rules:
f15613_0_add_Load(x0) → f15613_0_add_Load(+(x0, 3)) | &&(<=(x0, 1000), >(x0, -1))

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f15613_0_add_Load(x2)] = 1000 - x2

Therefore the following rule(s) have been dropped:

f15613_0_add_Load(x0) → f15613_0_add_Load(+(x0, 3)) | &&(<=(x0, 1000), >(x0, -1))

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: example_1.Test.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 20 IRules

P rules:
f11324_0_add_Load(EOS, matching1, matching2, matching3, i63, i63) → f11327_0_add_GT(EOS, 1000, 1000, 1000, i63, i63, 1000) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f11327_0_add_GT(EOS, matching1, matching2, matching3, i69, i69, matching4) → f11328_0_add_GT(EOS, 1000, 1000, 1000, i69, i69, 1000) | &&(&&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000)), =(matching4, 1000))
f11328_0_add_GT(EOS, matching1, matching2, matching3, i69, i69, matching4) → f11331_0_add_Load(EOS, 1000, 1000, 1000, i69) | &&(&&(&&(&&(<=(i69, 1000), =(matching1, 1000)), =(matching2, 1000)), =(matching3, 1000)), =(matching4, 1000))
f11331_0_add_Load(EOS, matching1, matching2, matching3, i69) → f11334_0_add_Load(EOS, 1000, 1000, 1000, i69) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f11334_0_add_Load(EOS, matching1, matching2, matching3, i69) → f11338_0_add_IntArithmetic(EOS, 1000, 1000, 1000, i69, i69) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f11338_0_add_IntArithmetic(EOS, matching1, matching2, matching3, i69, i69) → f11341_0_add_Store(EOS, 1000, 1000, 1000, i69) | &&(&&(&&(>=(i69, 0), =(matching1, 1000)), =(matching2, 1000)), =(matching3, 1000))
f11341_0_add_Store(EOS, matching1, matching2, matching3, i69) → f11345_0_add_Load(EOS, 1000, 1000, 1000, i69) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f11345_0_add_Load(EOS, matching1, matching2, matching3, i69) → f11348_0_add_Load(EOS, 1000, 1000, 1000, i69) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f11348_0_add_Load(EOS, matching1, matching2, matching3, i69) → f11352_0_add_InvokeMethod(EOS, 1000, 1000, 1000, i69) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f11352_0_add_InvokeMethod(EOS, matching1, matching2, matching3, i69) → f11355_0_incr_Load(EOS, 1000, 1000, 1000, i69, i69) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f11355_0_incr_Load(EOS, matching1, matching2, matching3, i69, i69) → f11358_0_incr_ConstantStackPush(EOS, 1000, 1000, 1000, i69, i69) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f11358_0_incr_ConstantStackPush(EOS, matching1, matching2, matching3, i69, i69) → f11361_0_incr_IntArithmetic(EOS, 1000, 1000, 1000, i69, i69, 2) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f11361_0_incr_IntArithmetic(EOS, matching1, matching2, matching3, i69, i69, matching4) → f11363_0_incr_Duplicate(EOS, 1000, 1000, 1000, i69, +(i69, 2)) | &&(&&(&&(&&(>=(i69, 0), =(matching1, 1000)), =(matching2, 1000)), =(matching3, 1000)), =(matching4, 2))
f11363_0_incr_Duplicate(EOS, matching1, matching2, matching3, i69, i74) → f11365_0_incr_Store(EOS, 1000, 1000, 1000, i69, i74, i74) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f11365_0_incr_Store(EOS, matching1, matching2, matching3, i69, i74, i74) → f11367_0_incr_Return(EOS, 1000, 1000, 1000, i69, i74) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f11367_0_incr_Return(EOS, matching1, matching2, matching3, i69, i74) → f11370_0_add_Store(EOS, 1000, 1000, 1000, i74) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f11370_0_add_Store(EOS, matching1, matching2, matching3, i74) → f11372_0_add_JMP(EOS, 1000, 1000, 1000, i74) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f11372_0_add_JMP(EOS, matching1, matching2, matching3, i74) → f11377_0_add_Load(EOS, 1000, 1000, 1000, i74) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f11377_0_add_Load(EOS, matching1, matching2, matching3, i74) → f11322_0_add_Load(EOS, 1000, 1000, 1000, i74) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f11322_0_add_Load(EOS, matching1, matching2, matching3, i63) → f11324_0_add_Load(EOS, 1000, 1000, 1000, i63, i63) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))

Combined rules. Obtained 1 IRules

P rules:
f11324_0_add_Load(EOS, 1000, 1000, 1000, x3, x3) → f11324_0_add_Load(EOS, 1000, 1000, 1000, +(x3, 2), +(x3, 2)) | &&(>(+(x3, 1), 0), <=(x3, 1000))

Filtered ground terms:

f11324_0_add_Load(x1, x2, x3, x4, x5, x6) → f11324_0_add_Load(x5, x6)
Cond_f11324_0_add_Load(x1, x2, x3, x4, x5, x6, x7) → Cond_f11324_0_add_Load(x1, x6, x7)

Filtered duplicate terms:

f11324_0_add_Load(x1, x2) → f11324_0_add_Load(x2)
Cond_f11324_0_add_Load(x1, x2, x3) → Cond_f11324_0_add_Load(x1, x3)

Prepared 1 rules for path length conversion:

P rules:
f11324_0_add_Load(x3) → f11324_0_add_Load(+(x3, 2)) | &&(>(+(x3, 1), 0), <=(x3, 1000))

Finished conversion. Obtained 1 rules.

P rules:
f11324_0_add_Load(x0) → f11324_0_add_Load(+(x0, 2)) | &&(<=(x0, 1000), >(x0, -1))

(12) Obligation:

Rules:
f11324_0_add_Load(x0) → f11324_0_add_Load(+(x0, 2)) | &&(<=(x0, 1000), >(x0, -1))

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f11324_0_add_Load(x2)] = 1000 - x2

Therefore the following rule(s) have been dropped:

f11324_0_add_Load(x0) → f11324_0_add_Load(+(x0, 2)) | &&(<=(x0, 1000), >(x0, -1))

(14) YES

(15) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: example_1.Test.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:
  

(16) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 20 IRules

P rules:
f372_0_add_Load(EOS, matching1, matching2, matching3, i18, i18) → f380_0_add_GT(EOS, 1000, 1000, 1000, i18, i18, 1000) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f380_0_add_GT(EOS, matching1, matching2, matching3, i23, i23, matching4) → f383_0_add_GT(EOS, 1000, 1000, 1000, i23, i23, 1000) | &&(&&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000)), =(matching4, 1000))
f383_0_add_GT(EOS, matching1, matching2, matching3, i23, i23, matching4) → f386_0_add_Load(EOS, 1000, 1000, 1000, i23) | &&(&&(&&(&&(<=(i23, 1000), =(matching1, 1000)), =(matching2, 1000)), =(matching3, 1000)), =(matching4, 1000))
f386_0_add_Load(EOS, matching1, matching2, matching3, i23) → f390_0_add_Load(EOS, 1000, 1000, 1000, i23) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f390_0_add_Load(EOS, matching1, matching2, matching3, i23) → f394_0_add_IntArithmetic(EOS, 1000, 1000, 1000, i23, i23) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f394_0_add_IntArithmetic(EOS, matching1, matching2, matching3, i23, i23) → f399_0_add_Store(EOS, 1000, 1000, 1000, i23) | &&(&&(&&(>=(i23, 0), =(matching1, 1000)), =(matching2, 1000)), =(matching3, 1000))
f399_0_add_Store(EOS, matching1, matching2, matching3, i23) → f404_0_add_Load(EOS, 1000, 1000, 1000, i23) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f404_0_add_Load(EOS, matching1, matching2, matching3, i23) → f408_0_add_Load(EOS, 1000, 1000, 1000, i23) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f408_0_add_Load(EOS, matching1, matching2, matching3, i23) → f412_0_add_InvokeMethod(EOS, 1000, 1000, 1000, i23) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f412_0_add_InvokeMethod(EOS, matching1, matching2, matching3, i23) → f417_0_incr_Load(EOS, 1000, 1000, 1000, i23, i23) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f417_0_incr_Load(EOS, matching1, matching2, matching3, i23, i23) → f421_0_incr_ConstantStackPush(EOS, 1000, 1000, 1000, i23, i23) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f421_0_incr_ConstantStackPush(EOS, matching1, matching2, matching3, i23, i23) → f425_0_incr_IntArithmetic(EOS, 1000, 1000, 1000, i23, i23, 1) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f425_0_incr_IntArithmetic(EOS, matching1, matching2, matching3, i23, i23, matching4) → f429_0_incr_Duplicate(EOS, 1000, 1000, 1000, i23, +(i23, 1)) | &&(&&(&&(&&(>=(i23, 0), =(matching1, 1000)), =(matching2, 1000)), =(matching3, 1000)), =(matching4, 1))
f429_0_incr_Duplicate(EOS, matching1, matching2, matching3, i23, i26) → f432_0_incr_Store(EOS, 1000, 1000, 1000, i23, i26, i26) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f432_0_incr_Store(EOS, matching1, matching2, matching3, i23, i26, i26) → f437_0_incr_Return(EOS, 1000, 1000, 1000, i23, i26) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f437_0_incr_Return(EOS, matching1, matching2, matching3, i23, i26) → f443_0_add_Store(EOS, 1000, 1000, 1000, i26) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f443_0_add_Store(EOS, matching1, matching2, matching3, i26) → f447_0_add_JMP(EOS, 1000, 1000, 1000, i26) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f447_0_add_JMP(EOS, matching1, matching2, matching3, i26) → f476_0_add_Load(EOS, 1000, 1000, 1000, i26) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f476_0_add_Load(EOS, matching1, matching2, matching3, i26) → f369_0_add_Load(EOS, 1000, 1000, 1000, i26) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))
f369_0_add_Load(EOS, matching1, matching2, matching3, i18) → f372_0_add_Load(EOS, 1000, 1000, 1000, i18, i18) | &&(&&(=(matching1, 1000), =(matching2, 1000)), =(matching3, 1000))

Combined rules. Obtained 1 IRules

P rules:
f372_0_add_Load(EOS, 1000, 1000, 1000, x3, x3) → f372_0_add_Load(EOS, 1000, 1000, 1000, +(x3, 1), +(x3, 1)) | &&(>(+(x3, 1), 0), <=(x3, 1000))

Filtered ground terms:

f372_0_add_Load(x1, x2, x3, x4, x5, x6) → f372_0_add_Load(x5, x6)
Cond_f372_0_add_Load(x1, x2, x3, x4, x5, x6, x7) → Cond_f372_0_add_Load(x1, x6, x7)

Filtered duplicate terms:

f372_0_add_Load(x1, x2) → f372_0_add_Load(x2)
Cond_f372_0_add_Load(x1, x2, x3) → Cond_f372_0_add_Load(x1, x3)

Prepared 1 rules for path length conversion:

P rules:
f372_0_add_Load(x3) → f372_0_add_Load(+(x3, 1)) | &&(>(+(x3, 1), 0), <=(x3, 1000))

Finished conversion. Obtained 1 rules.

P rules:
f372_0_add_Load(x0) → f372_0_add_Load(+(x0, 1)) | &&(<=(x0, 1000), >(x0, -1))

(17) Obligation:

Rules:
f372_0_add_Load(x0) → f372_0_add_Load(+(x0, 1)) | &&(<=(x0, 1000), >(x0, -1))

(18) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f372_0_add_Load(x2)] = 1000 - x2

Therefore the following rule(s) have been dropped:

f372_0_add_Load(x0) → f372_0_add_Load(+(x0, 1)) | &&(<=(x0, 1000), >(x0, -1))

(19) YES