Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

public class FibSLR {

    public static int fib(int n){
	if (n  < 2) return 1;
	else return fib(n-1) + fib(n-2);	  
    }

    public static int doSum(List x){
	if (x==null) return 1;
	else return fib(x.head) + doSum(x.tail);	
    }

    public static void main(String [] args) {
	Random.args = args;
	List l = List.mk(Random.random()*Random.random());
	//System.out.println(doSum(l));
    }
}



public class List {
    public int head;
    public List tail;

    public List(int head, List tail) {
	this.head = head;
	this.tail = tail;
    }

    public List getTail() {
	return tail;
    }

    public static List mk(int len) {
	List result = null;

	while (len-- > 0)
	    result = new List(Random.random(), result);

	return result;
    }
}

public class Random {
  static String[] args;
  static int index = 0;

  public static int random() {
      if (index >= args.length)
	  return 0;

      String string = args[index];
      index++;
      return string.length();
  }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

List.mk(I)LList;: Graph of 119 nodes with 1 SCC.

(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: List.mk(I)LList;
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:
  

(5) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 61 IRules

P rules:
f1716_0_mk_Inc(EOS, i328, i328) → f1718_0_mk_LE(EOS, +(i328, -1), i328)
f1718_0_mk_LE(EOS, i331, i336) → f1721_0_mk_LE(EOS, i331, i336)
f1721_0_mk_LE(EOS, i331, i336) → f1724_0_mk_New(EOS, i331) | >(i336, 0)
f1724_0_mk_New(EOS, i331) → f1727_0_mk_Duplicate(EOS, i331)
f1727_0_mk_Duplicate(EOS, i331) → f1730_0_mk_InvokeMethod(EOS, i331)
f1730_0_mk_InvokeMethod(EOS, i331) → f1755_0_random_FieldAccess(EOS, i331)
f1755_0_random_FieldAccess(EOS, i331) → f1760_0_random_FieldAccess(EOS, i331, i327)
f1760_0_random_FieldAccess(EOS, i331, i327) → f1762_0_random_ArrayLength(EOS, i331, i327, java.lang.Object(ARRAY(i73)))
f1762_0_random_ArrayLength(EOS, i331, i327, java.lang.Object(ARRAY(i73))) → f1764_0_random_LT(EOS, i331, i327, i73) | >=(i73, 0)
f1764_0_random_LT(EOS, i331, i327, i73) → f1765_0_random_LT(EOS, i331, i327, i73)
f1764_0_random_LT(EOS, i331, i327, i73) → f1766_0_random_LT(EOS, i331, i327, i73)
f1765_0_random_LT(EOS, i331, i327, i73) → f1768_0_random_FieldAccess(EOS, i331) | <(i327, i73)
f1768_0_random_FieldAccess(EOS, i331) → f1771_0_random_FieldAccess(EOS, i331, java.lang.Object(ARRAY(i73)))
f1771_0_random_FieldAccess(EOS, i331, java.lang.Object(ARRAY(i73))) → f1775_0_random_ArrayAccess(EOS, i331, java.lang.Object(ARRAY(i73)), i327)
f1775_0_random_ArrayAccess(EOS, i331, java.lang.Object(ARRAY(i73)), i327) → f1778_0_random_ArrayAccess(EOS, i331, java.lang.Object(ARRAY(i73)), i327)
f1778_0_random_ArrayAccess(EOS, i331, java.lang.Object(ARRAY(i73)), i327) → f1782_0_random_Store(EOS, i331, o419)
f1782_0_random_Store(EOS, i331, o419) → f1787_0_random_FieldAccess(EOS, i331, o419)
f1787_0_random_FieldAccess(EOS, i331, o419) → f1789_0_random_ConstantStackPush(EOS, i331, o419, i327)
f1789_0_random_ConstantStackPush(EOS, i331, o419, i327) → f1794_0_random_IntArithmetic(EOS, i331, o419, i327, 1)
f1794_0_random_IntArithmetic(EOS, i331, o419, i327, matching1) → f1799_0_random_FieldAccess(EOS, i331, o419, +(i327, 1)) | &&(>=(i327, 0), =(matching1, 1))
f1799_0_random_FieldAccess(EOS, i331, o419, i357) → f1803_0_random_Load(EOS, i331, o419)
f1803_0_random_Load(EOS, i331, o419) → f1808_0_random_InvokeMethod(EOS, i331, o419)
f1808_0_random_InvokeMethod(EOS, i331, java.lang.Object(o422sub)) → f1813_0_random_InvokeMethod(EOS, i331, java.lang.Object(o422sub))
f1813_0_random_InvokeMethod(EOS, i331, java.lang.Object(o422sub)) → f1816_0_length_Load(EOS, i331, java.lang.Object(o422sub), java.lang.Object(o422sub))
f1816_0_length_Load(EOS, i331, java.lang.Object(o422sub), java.lang.Object(o422sub)) → f1828_0_length_FieldAccess(EOS, i331, java.lang.Object(o422sub), java.lang.Object(o422sub))
f1828_0_length_FieldAccess(EOS, i331, java.lang.Object(java.lang.String(o426sub, i367)), java.lang.Object(java.lang.String(o426sub, i367))) → f1832_0_length_FieldAccess(EOS, i331, java.lang.Object(java.lang.String(o426sub, i367)), java.lang.Object(java.lang.String(o426sub, i367)))
f1832_0_length_FieldAccess(EOS, i331, java.lang.Object(java.lang.String(o426sub, i367)), java.lang.Object(java.lang.String(o426sub, i367))) → f1838_0_length_Return(EOS, i331, java.lang.Object(java.lang.String(o426sub, i367)))
f1838_0_length_Return(EOS, i331, java.lang.Object(java.lang.String(o426sub, i367))) → f1847_0_random_Return(EOS, i331)
f1847_0_random_Return(EOS, i331) → f1850_0_mk_Load(EOS, i331)
f1850_0_mk_Load(EOS, i331) → f1855_0_mk_InvokeMethod(EOS, i331)
f1855_0_mk_InvokeMethod(EOS, i331) → f1859_0__init__Load(EOS, i331)
f1859_0__init__Load(EOS, i331) → f1867_0__init__InvokeMethod(EOS, i331)
f1867_0__init__InvokeMethod(EOS, i331) → f1874_0__init__Load(EOS, i331)
f1874_0__init__Load(EOS, i331) → f1878_0__init__Load(EOS, i331)
f1878_0__init__Load(EOS, i331) → f1885_0__init__FieldAccess(EOS, i331)
f1885_0__init__FieldAccess(EOS, i331) → f1891_0__init__Load(EOS, i331)
f1891_0__init__Load(EOS, i331) → f1897_0__init__Load(EOS, i331)
f1897_0__init__Load(EOS, i331) → f1903_0__init__FieldAccess(EOS, i331)
f1903_0__init__FieldAccess(EOS, i331) → f1914_0__init__Return(EOS, i331)
f1914_0__init__Return(EOS, i331) → f1920_0_mk_Store(EOS, i331)
f1920_0_mk_Store(EOS, i331) → f1928_0_mk_JMP(EOS, i331)
f1928_0_mk_JMP(EOS, i331) → f1933_0_mk_Load(EOS, i331)
f1933_0_mk_Load(EOS, i331) → f1711_0_mk_Load(EOS, i331)
f1711_0_mk_Load(EOS, i328) → f1716_0_mk_Inc(EOS, i328, i328)
f1766_0_random_LT(EOS, i331, i327, i73) → f1769_0_random_ConstantStackPush(EOS, i331) | >=(i327, i73)
f1769_0_random_ConstantStackPush(EOS, i331) → f1773_0_random_Return(EOS, i331)
f1773_0_random_Return(EOS, i331) → f1776_0_mk_Load(EOS, i331)
f1776_0_mk_Load(EOS, i331) → f1780_0_mk_InvokeMethod(EOS, i331)
f1780_0_mk_InvokeMethod(EOS, i331) → f1786_0__init__Load(EOS, i331)
f1786_0__init__Load(EOS, i331) → f1792_0__init__InvokeMethod(EOS, i331)
f1792_0__init__InvokeMethod(EOS, i331) → f1797_0__init__Load(EOS, i331)
f1797_0__init__Load(EOS, i331) → f1801_0__init__Load(EOS, i331)
f1801_0__init__Load(EOS, i331) → f1806_0__init__FieldAccess(EOS, i331)
f1806_0__init__FieldAccess(EOS, i331) → f1811_0__init__Load(EOS, i331)
f1811_0__init__Load(EOS, i331) → f1815_0__init__Load(EOS, i331)
f1815_0__init__Load(EOS, i331) → f1821_0__init__FieldAccess(EOS, i331)
f1821_0__init__FieldAccess(EOS, i331) → f1826_0__init__Return(EOS, i331)
f1826_0__init__Return(EOS, i331) → f1830_0_mk_Store(EOS, i331)
f1830_0_mk_Store(EOS, i331) → f1837_0_mk_JMP(EOS, i331)
f1837_0_mk_JMP(EOS, i331) → f1846_0_mk_Load(EOS, i331)
f1846_0_mk_Load(EOS, i331) → f1711_0_mk_Load(EOS, i331)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:

f1716_0_mk_Inc(x1, x2, x3) → f1716_0_mk_Inc(x2, x3)
Cond_f1716_0_mk_Inc(x1, x2, x3, x4) → Cond_f1716_0_mk_Inc(x1, x3, x4)

Filtered duplicate terms:

f1716_0_mk_Inc(x1, x2) → f1716_0_mk_Inc(x2)
Cond_f1716_0_mk_Inc(x1, x2, x3) → Cond_f1716_0_mk_Inc(x1, x3)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(6) Obligation:

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

(7) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f1716_0_mk_Inc(x2)] = x2

Therefore the following rule(s) have been dropped:

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

(8) YES