Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

public class FactSLR {

    public static int factorial(int n){
	if (n  < 1) return 1;
	else return n*factorial(n-1);	  
    }

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

    public static void main(String [] args) {
	Random.args = args;
	List l = List.mk(3*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:
FactSLR.main([Ljava/lang/String;)V: Graph of 114 nodes with 0 SCCs.

List.mk(I)LList;: Graph of 120 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:
f1654_0_mk_Inc(EOS, i312, i312) → f1656_0_mk_LE(EOS, +(i312, -1), i312)
f1656_0_mk_LE(EOS, i321, i326) → f1658_0_mk_LE(EOS, i321, i326)
f1658_0_mk_LE(EOS, i321, i326) → f1662_0_mk_New(EOS, i321) | >(i326, 0)
f1662_0_mk_New(EOS, i321) → f1665_0_mk_Duplicate(EOS, i321)
f1665_0_mk_Duplicate(EOS, i321) → f1668_0_mk_InvokeMethod(EOS, i321)
f1668_0_mk_InvokeMethod(EOS, i321) → f1686_0_random_FieldAccess(EOS, i321)
f1686_0_random_FieldAccess(EOS, i321) → f1691_0_random_FieldAccess(EOS, i321, i311)
f1691_0_random_FieldAccess(EOS, i321, i311) → f1693_0_random_ArrayLength(EOS, i321, i311, java.lang.Object(ARRAY(i26)))
f1693_0_random_ArrayLength(EOS, i321, i311, java.lang.Object(ARRAY(i26))) → f1695_0_random_LT(EOS, i321, i311, i26) | >=(i26, 0)
f1695_0_random_LT(EOS, i321, i311, i26) → f1696_0_random_LT(EOS, i321, i311, i26)
f1695_0_random_LT(EOS, i321, i311, i26) → f1697_0_random_LT(EOS, i321, i311, i26)
f1696_0_random_LT(EOS, i321, i311, i26) → f1699_0_random_FieldAccess(EOS, i321) | <(i311, i26)
f1699_0_random_FieldAccess(EOS, i321) → f1702_0_random_FieldAccess(EOS, i321, java.lang.Object(ARRAY(i26)))
f1702_0_random_FieldAccess(EOS, i321, java.lang.Object(ARRAY(i26))) → f1706_0_random_ArrayAccess(EOS, i321, java.lang.Object(ARRAY(i26)), i311)
f1706_0_random_ArrayAccess(EOS, i321, java.lang.Object(ARRAY(i26)), i311) → f1709_0_random_ArrayAccess(EOS, i321, java.lang.Object(ARRAY(i26)), i311)
f1709_0_random_ArrayAccess(EOS, i321, java.lang.Object(ARRAY(i26)), i311) → f1714_0_random_Store(EOS, i321, o337)
f1714_0_random_Store(EOS, i321, o337) → f1718_0_random_FieldAccess(EOS, i321, o337)
f1718_0_random_FieldAccess(EOS, i321, o337) → f1721_0_random_ConstantStackPush(EOS, i321, o337, i311)
f1721_0_random_ConstantStackPush(EOS, i321, o337, i311) → f1726_0_random_IntArithmetic(EOS, i321, o337, i311, 1)
f1726_0_random_IntArithmetic(EOS, i321, o337, i311, matching1) → f1732_0_random_FieldAccess(EOS, i321, o337, +(i311, 1)) | &&(>=(i311, 0), =(matching1, 1))
f1732_0_random_FieldAccess(EOS, i321, o337, i345) → f1735_0_random_Load(EOS, i321, o337)
f1735_0_random_Load(EOS, i321, o337) → f1741_0_random_InvokeMethod(EOS, i321, o337)
f1741_0_random_InvokeMethod(EOS, i321, java.lang.Object(o340sub)) → f1744_0_random_InvokeMethod(EOS, i321, java.lang.Object(o340sub))
f1744_0_random_InvokeMethod(EOS, i321, java.lang.Object(o340sub)) → f1748_0_length_Load(EOS, i321, java.lang.Object(o340sub), java.lang.Object(o340sub))
f1748_0_length_Load(EOS, i321, java.lang.Object(o340sub), java.lang.Object(o340sub)) → f1761_0_length_FieldAccess(EOS, i321, java.lang.Object(o340sub), java.lang.Object(o340sub))
f1761_0_length_FieldAccess(EOS, i321, java.lang.Object(java.lang.String(o345sub, i354)), java.lang.Object(java.lang.String(o345sub, i354))) → f1765_0_length_FieldAccess(EOS, i321, java.lang.Object(java.lang.String(o345sub, i354)), java.lang.Object(java.lang.String(o345sub, i354)))
f1765_0_length_FieldAccess(EOS, i321, java.lang.Object(java.lang.String(o345sub, i354)), java.lang.Object(java.lang.String(o345sub, i354))) → f1772_0_length_Return(EOS, i321, java.lang.Object(java.lang.String(o345sub, i354)))
f1772_0_length_Return(EOS, i321, java.lang.Object(java.lang.String(o345sub, i354))) → f1780_0_random_Return(EOS, i321)
f1780_0_random_Return(EOS, i321) → f1782_0_mk_Load(EOS, i321)
f1782_0_mk_Load(EOS, i321) → f1789_0_mk_InvokeMethod(EOS, i321)
f1789_0_mk_InvokeMethod(EOS, i321) → f1794_0__init__Load(EOS, i321)
f1794_0__init__Load(EOS, i321) → f1803_0__init__InvokeMethod(EOS, i321)
f1803_0__init__InvokeMethod(EOS, i321) → f1809_0__init__Load(EOS, i321)
f1809_0__init__Load(EOS, i321) → f1813_0__init__Load(EOS, i321)
f1813_0__init__Load(EOS, i321) → f1819_0__init__FieldAccess(EOS, i321)
f1819_0__init__FieldAccess(EOS, i321) → f1826_0__init__Load(EOS, i321)
f1826_0__init__Load(EOS, i321) → f1832_0__init__Load(EOS, i321)
f1832_0__init__Load(EOS, i321) → f1839_0__init__FieldAccess(EOS, i321)
f1839_0__init__FieldAccess(EOS, i321) → f1845_0__init__Return(EOS, i321)
f1845_0__init__Return(EOS, i321) → f1852_0_mk_Store(EOS, i321)
f1852_0_mk_Store(EOS, i321) → f1857_0_mk_JMP(EOS, i321)
f1857_0_mk_JMP(EOS, i321) → f1864_0_mk_Load(EOS, i321)
f1864_0_mk_Load(EOS, i321) → f1649_0_mk_Load(EOS, i321)
f1649_0_mk_Load(EOS, i312) → f1654_0_mk_Inc(EOS, i312, i312)
f1697_0_random_LT(EOS, i321, i311, i26) → f1701_0_random_ConstantStackPush(EOS, i321) | >=(i311, i26)
f1701_0_random_ConstantStackPush(EOS, i321) → f1704_0_random_Return(EOS, i321)
f1704_0_random_Return(EOS, i321) → f1707_0_mk_Load(EOS, i321)
f1707_0_mk_Load(EOS, i321) → f1712_0_mk_InvokeMethod(EOS, i321)
f1712_0_mk_InvokeMethod(EOS, i321) → f1717_0__init__Load(EOS, i321)
f1717_0__init__Load(EOS, i321) → f1724_0__init__InvokeMethod(EOS, i321)
f1724_0__init__InvokeMethod(EOS, i321) → f1730_0__init__Load(EOS, i321)
f1730_0__init__Load(EOS, i321) → f1733_0__init__Load(EOS, i321)
f1733_0__init__Load(EOS, i321) → f1738_0__init__FieldAccess(EOS, i321)
f1738_0__init__FieldAccess(EOS, i321) → f1743_0__init__Load(EOS, i321)
f1743_0__init__Load(EOS, i321) → f1746_0__init__Load(EOS, i321)
f1746_0__init__Load(EOS, i321) → f1753_0__init__FieldAccess(EOS, i321)
f1753_0__init__FieldAccess(EOS, i321) → f1759_0__init__Return(EOS, i321)
f1759_0__init__Return(EOS, i321) → f1763_0_mk_Store(EOS, i321)
f1763_0_mk_Store(EOS, i321) → f1770_0_mk_JMP(EOS, i321)
f1770_0_mk_JMP(EOS, i321) → f1778_0_mk_Load(EOS, i321)
f1778_0_mk_Load(EOS, i321) → f1649_0_mk_Load(EOS, i321)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:

f1654_0_mk_Inc(x1, x2, x3) → f1654_0_mk_Inc(x2, x3)
Cond_f1654_0_mk_Inc(x1, x2, x3, x4) → Cond_f1654_0_mk_Inc(x1, x3, x4)

Filtered duplicate terms:

f1654_0_mk_Inc(x1, x2) → f1654_0_mk_Inc(x2)
Cond_f1654_0_mk_Inc(x1, x2, x3) → Cond_f1654_0_mk_Inc(x1, x3)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(6) Obligation:

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

(7) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f1654_0_mk_Inc(x2)] = x2

Therefore the following rule(s) have been dropped:

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

(8) YES