Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

public class AProVERec01 {
	public static void main(String[] args){
		List a = new List(args[0].length(), null);
		rec(args[1].length(), a);
	}

	public static void rec(int y, List res){
		int x = 3 * y;
		if(x < 100000){
			rec(x+1, res);
		}
		x = x*2;
		res.add(x);
	}
}

class List {
	int val = 0;
	List next = null;
	
	List (int v,List n){
		val = v;
		next = n;
	}

	public void add(int newVal){
		if (next == null) {
			next = new List(newVal, null);
		} else {
			next.add(newVal);
		}
	}
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

AProVERec01.rec(ILList;)V: Graph of 49 nodes with 0 SCCs.

List.add(I)V: Graph of 42 nodes with 0 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 2 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: List.add(I)V
SCC calls the following helper methods: List.add(I)V
Performed SCC analyses:

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

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 12 IRules

P rules:
f675_0_add_FieldAccess(EOS, java.lang.Object(List(EOC, o200)), i91, java.lang.Object(List(EOC, o200)), i91, java.lang.Object(List(EOC, o200))) → f677_0_add_FieldAccess(EOS, java.lang.Object(List(EOC, o200)), i91, java.lang.Object(List(EOC, o200)), i91, java.lang.Object(List(EOC, o200)))
f677_0_add_FieldAccess(EOS, java.lang.Object(List(EOC, o200)), i91, java.lang.Object(List(EOC, o200)), i91, java.lang.Object(List(EOC, o200))) → f679_0_add_NONNULL(EOS, java.lang.Object(List(EOC, o200)), i91, java.lang.Object(List(EOC, o200)), i91, o200)
f679_0_add_NONNULL(EOS, java.lang.Object(List(EOC, java.lang.Object(o202sub))), i91, java.lang.Object(List(EOC, java.lang.Object(o202sub))), i91, java.lang.Object(o202sub)) → f682_0_add_NONNULL(EOS, java.lang.Object(List(EOC, java.lang.Object(o202sub))), i91, java.lang.Object(List(EOC, java.lang.Object(o202sub))), i91, java.lang.Object(o202sub))
f682_0_add_NONNULL(EOS, java.lang.Object(List(EOC, java.lang.Object(o202sub))), i91, java.lang.Object(List(EOC, java.lang.Object(o202sub))), i91, java.lang.Object(o202sub)) → f684_0_add_Load(EOS, java.lang.Object(List(EOC, java.lang.Object(o202sub))), i91, java.lang.Object(List(EOC, java.lang.Object(o202sub))), i91)
f684_0_add_Load(EOS, java.lang.Object(List(EOC, java.lang.Object(o202sub))), i91, java.lang.Object(List(EOC, java.lang.Object(o202sub))), i91) → f688_0_add_FieldAccess(EOS, java.lang.Object(List(EOC, java.lang.Object(o202sub))), i91, i91, java.lang.Object(List(EOC, java.lang.Object(o202sub))))
f688_0_add_FieldAccess(EOS, java.lang.Object(List(EOC, java.lang.Object(o202sub))), i91, i91, java.lang.Object(List(EOC, java.lang.Object(o202sub)))) → f692_0_add_Load(EOS, java.lang.Object(List(EOC, java.lang.Object(o202sub))), i91, i91, java.lang.Object(o202sub))
f692_0_add_Load(EOS, java.lang.Object(List(EOC, java.lang.Object(o202sub))), i91, i91, java.lang.Object(o202sub)) → f696_0_add_InvokeMethod(EOS, java.lang.Object(List(EOC, java.lang.Object(o202sub))), i91, java.lang.Object(o202sub), i91)
f696_0_add_InvokeMethod(EOS, java.lang.Object(List(EOC, java.lang.Object(o202sub))), i91, java.lang.Object(o202sub), i91) → f700_0_add_Load(EOS, java.lang.Object(o202sub), i91, java.lang.Object(o202sub), i91)
f696_0_add_InvokeMethod(EOS, java.lang.Object(List(EOC, java.lang.Object(o202sub))), i91, java.lang.Object(o202sub), i91) → f700_1_add_Load(EOS, java.lang.Object(List(EOC, java.lang.Object(o202sub))), i91, java.lang.Object(o202sub), i91, java.lang.Object(o202sub), i91)
f700_0_add_Load(EOS, java.lang.Object(o202sub), i91, java.lang.Object(o202sub), i91) → f704_0_add_Load(EOS, java.lang.Object(o202sub), i91, java.lang.Object(o202sub), i91)
f704_0_add_Load(EOS, java.lang.Object(o202sub), i91, java.lang.Object(o202sub), i91) → f672_0_add_Load(EOS, java.lang.Object(o202sub), i91, java.lang.Object(o202sub), i91)
f672_0_add_Load(EOS, java.lang.Object(o195sub), i91, java.lang.Object(o195sub), i91) → f675_0_add_FieldAccess(EOS, java.lang.Object(o195sub), i91, java.lang.Object(o195sub), i91, java.lang.Object(o195sub))

Combined rules. Obtained 2 IRules

P rules:
f675_0_add_FieldAccess(EOS, java.lang.Object(List(EOC, java.lang.Object(x0))), x1, java.lang.Object(List(EOC, java.lang.Object(x0))), x1, java.lang.Object(List(EOC, java.lang.Object(x0)))) → f700_1_add_Load(EOS, java.lang.Object(List(EOC, java.lang.Object(x0))), x1, java.lang.Object(x0), x1, java.lang.Object(x0), x1)
f675_0_add_FieldAccess(EOS, java.lang.Object(List(EOC, java.lang.Object(x0))), x1, java.lang.Object(List(EOC, java.lang.Object(x0))), x1, java.lang.Object(List(EOC, java.lang.Object(x0)))) → f675_0_add_FieldAccess(EOS, java.lang.Object(x0), x1, java.lang.Object(x0), x1, java.lang.Object(x0))

Filtered ground terms:

f675_0_add_FieldAccess(x1, x2, x3, x4, x5, x6) → f675_0_add_FieldAccess(x2, x3, x4, x5, x6)
f700_1_add_Load(x1, x2, x3, x4, x5, x6, x7) → f700_1_add_Load(x2, x3, x4, x5, x6, x7)
List(x1, x2) → List(x2)

Filtered duplicate terms:

f675_0_add_FieldAccess(x1, x2, x3, x4, x5) → f675_0_add_FieldAccess(x4, x5)
f700_1_add_Load(x1, x2, x3, x4, x5, x6) → f700_1_add_Load(x1, x6)

Filtered unneeded terms:

f675_0_add_FieldAccess(x1, x2) → f675_0_add_FieldAccess(x2)

Prepared 2 rules for path length conversion:

P rules:
f675_0_add_FieldAccess(java.lang.Object(List(java.lang.Object(x0)))) → f700_1_add_Load(java.lang.Object(List(java.lang.Object(x0))), x1)
f675_0_add_FieldAccess(java.lang.Object(List(java.lang.Object(x0)))) → f675_0_add_FieldAccess(java.lang.Object(x0))

Finished conversion. Obtained 1 rules.

P rules:
f675_0_add_FieldAccess(v4) → f675_0_add_FieldAccess(v5) | &&(&&(>(+(v5, 1), 1), <=(+(v5, 2), v4)), >(+(v4, 1), 3))

(7) Obligation:

Rules:
f675_0_add_FieldAccess(v4) → f675_0_add_FieldAccess(v5) | &&(&&(>(+(v5, 1), 1), <=(+(v5, 2), v4)), >(+(v4, 1), 3))

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f675_0_add_FieldAccess(x3)] = x3

Therefore the following rule(s) have been dropped:

f675_0_add_FieldAccess(x0) → f675_0_add_FieldAccess(x1) | &&(&&(>(+(x1, 1), 1), <=(+(x1, 2), x0)), >(+(x0, 1), 3))

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: AProVERec01.rec(ILList;)V
SCC calls the following helper methods: AProVERec01.rec(ILList;)V, List.add(I)V
Performed SCC analyses:

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

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 16 IRules

P rules:
f305_0_rec_Load(EOS, i37, java.lang.Object(List(EOC)), i37, java.lang.Object(List(EOC)), matching1) → f307_0_rec_IntArithmetic(EOS, i37, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), 3, i37) | =(matching1, 3)
f307_0_rec_IntArithmetic(EOS, i37, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), matching1, i37) → f309_0_rec_Store(EOS, i37, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), *(3, i37)) | =(matching1, 3)
f309_0_rec_Store(EOS, i37, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i44) → f315_0_rec_Load(EOS, i37, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i44)
f315_0_rec_Load(EOS, i37, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i44) → f319_0_rec_ConstantStackPush(EOS, i37, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i44, i44)
f319_0_rec_ConstantStackPush(EOS, i37, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i44, i44) → f326_0_rec_GE(EOS, i37, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i44, i44, 100000)
f326_0_rec_GE(EOS, i37, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i48, i48, matching1) → f332_0_rec_GE(EOS, i37, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i48, i48, 100000) | =(matching1, 100000)
f332_0_rec_GE(EOS, i37, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i48, i48, matching1) → f339_0_rec_Load(EOS, i37, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i48) | &&(<(i48, 100000), =(matching1, 100000))
f339_0_rec_Load(EOS, i37, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i48) → f350_0_rec_ConstantStackPush(EOS, i37, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i48, i48)
f350_0_rec_ConstantStackPush(EOS, i37, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i48, i48) → f364_0_rec_IntArithmetic(EOS, i37, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i48, i48, 1)
f364_0_rec_IntArithmetic(EOS, i37, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i48, i48, matching1) → f381_0_rec_Load(EOS, i37, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i48, +(i48, 1)) | &&(>=(i48, 0), =(matching1, 1))
f381_0_rec_Load(EOS, i37, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i48, i55) → f396_0_rec_InvokeMethod(EOS, i37, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i48, i55, java.lang.Object(List(EOC)))
f396_0_rec_InvokeMethod(EOS, i37, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i48, i55, java.lang.Object(List(EOC))) → f410_0_rec_ConstantStackPush(EOS, i55, java.lang.Object(List(EOC)), i55, java.lang.Object(List(EOC)))
f396_0_rec_InvokeMethod(EOS, i37, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i48, i55, java.lang.Object(List(EOC))) → f410_1_rec_ConstantStackPush(EOS, i37, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i48, i55, java.lang.Object(List(EOC)), i55, java.lang.Object(List(EOC)))
f410_0_rec_ConstantStackPush(EOS, i55, java.lang.Object(List(EOC)), i55, java.lang.Object(List(EOC))) → f425_0_rec_ConstantStackPush(EOS, i55, java.lang.Object(List(EOC)), i55, java.lang.Object(List(EOC)))
f425_0_rec_ConstantStackPush(EOS, i55, java.lang.Object(List(EOC)), i55, java.lang.Object(List(EOC))) → f301_0_rec_ConstantStackPush(EOS, i55, java.lang.Object(List(EOC)), i55, java.lang.Object(List(EOC)))
f301_0_rec_ConstantStackPush(EOS, i37, java.lang.Object(List(EOC)), i37, java.lang.Object(List(EOC))) → f305_0_rec_Load(EOS, i37, java.lang.Object(List(EOC)), i37, java.lang.Object(List(EOC)), 3)

Combined rules. Obtained 2 IRules

P rules:
f305_0_rec_Load(EOS, x0, java.lang.Object(List(EOC)), x0, java.lang.Object(List(EOC)), 3) → f410_1_rec_ConstantStackPush(EOS, x0, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), *(3, x0), +(*(3, x0), 1), java.lang.Object(List(EOC)), +(*(3, x0), 1), java.lang.Object(List(EOC))) | &&(<(*(3, x0), 100000), >=(*(3, x0), 0))
f305_0_rec_Load(EOS, x0, java.lang.Object(List(EOC)), x0, java.lang.Object(List(EOC)), 3) → f305_0_rec_Load(EOS, +(*(3, x0), 1), java.lang.Object(List(EOC)), +(*(3, x0), 1), java.lang.Object(List(EOC)), 3) | &&(<(*(3, x0), 100000), >=(*(3, x0), 0))

Filtered ground terms:

f305_0_rec_Load(x1, x2, x3, x4, x5, x6) → f305_0_rec_Load(x2, x4)
Cond_f305_0_rec_Load(x1, x2, x3, x4, x5, x6, x7) → Cond_f305_0_rec_Load(x1, x3, x5)
f410_1_rec_ConstantStackPush(x1, x2, x3, x4, x5, x6, x7, x8, x9) → f410_1_rec_ConstantStackPush(x2, x5, x6, x8)
Cond_f305_0_rec_Load1(x1, x2, x3, x4, x5, x6, x7) → Cond_f305_0_rec_Load1(x1, x3, x5)
java.lang.Object(x1) → java.lang.Object
List(x1) → List

Filtered duplicate terms:

f305_0_rec_Load(x1, x2) → f305_0_rec_Load(x2)
Cond_f305_0_rec_Load(x1, x2, x3) → Cond_f305_0_rec_Load(x1, x3)
f410_1_rec_ConstantStackPush(x1, x2, x3, x4) → f410_1_rec_ConstantStackPush(x4)
Cond_f305_0_rec_Load1(x1, x2, x3) → Cond_f305_0_rec_Load1(x1, x3)

Filtered unneeded terms:

Cond_f305_0_rec_Load(x1, x2) → Cond_f305_0_rec_Load(x1)

Prepared 2 rules for path length conversion:

P rules:
f305_0_rec_Load(x0) → f410_1_rec_ConstantStackPush(+(*(3, x0), 1)) | &&(<(*(3, x0), 100000), >=(*(3, x0), 0))
f305_0_rec_Load(x0) → f305_0_rec_Load(+(*(3, x0), 1)) | &&(<(*(3, x0), 100000), >=(*(3, x0), 0))

Finished conversion. Obtained 1 rules.

P rules:
f305_0_rec_Load(x1) → f305_0_rec_Load(+(*(3, x1), 1)) | &&(<(*(3, x1), 100000), >=(*(3, x1), 0))

(12) Obligation:

Rules:
f305_0_rec_Load(x1) → f305_0_rec_Load(+(*(3, x1), 1)) | &&(<(*(3, x1), 100000), >=(*(3, x1), 0))

(13) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:

[f305_0_rec_Load(x)] = (-1)·x₁

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

Therefore the following rule(s) have been dropped:

f305_0_rec_Load(x0) → f305_0_rec_Load(+(*(3, x0), 1)) | &&(<(*(3, x0), 100000), >=(*(3, x0), 0))

(14) YES