Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

public class LeUserDefRec {
	public static void main(String[] args) {
		int x = args[0].length();
		int y = args[1].length();
		le(x, y);
	}

	public static boolean le(int x, int y) {
		if (x > 0 && y > 0) {
			return le(x-1, y-1);
		} else {
			return (x == 0);
		}
	}
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

LeUserDefRec.le(II)Z: Graph of 36 nodes with 0 SCCs.

(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: LeUserDefRec.le(II)Z
SCC calls the following helper methods: LeUserDefRec.le(II)Z
Performed SCC analyses:

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

(5) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 16 IRules

P rules:
f308_0_le_LE(EOS, i47, i36, i47, i36, i47) → f313_0_le_LE(EOS, i47, i36, i47, i36, i47)
f313_0_le_LE(EOS, i47, i36, i47, i36, i47) → f325_0_le_Load(EOS, i47, i36, i47, i36) | >(i47, 0)
f325_0_le_Load(EOS, i47, i36, i47, i36) → f341_0_le_LE(EOS, i47, i36, i47, i36, i36)
f341_0_le_LE(EOS, i47, i52, i47, i52, i52) → f357_0_le_LE(EOS, i47, i52, i47, i52, i52)
f357_0_le_LE(EOS, i47, i52, i47, i52, i52) → f388_0_le_Load(EOS, i47, i52, i47, i52) | >(i52, 0)
f388_0_le_Load(EOS, i47, i52, i47, i52) → f412_0_le_ConstantStackPush(EOS, i47, i52, i47, i52, i47)
f412_0_le_ConstantStackPush(EOS, i47, i52, i47, i52, i47) → f437_0_le_IntArithmetic(EOS, i47, i52, i47, i52, i47, 1)
f437_0_le_IntArithmetic(EOS, i47, i52, i47, i52, i47, matching1) → f491_0_le_Load(EOS, i47, i52, i47, i52, -(i47, 1)) | &&(>(i47, 0), =(matching1, 1))
f491_0_le_Load(EOS, i47, i52, i47, i52, i69) → f500_0_le_ConstantStackPush(EOS, i47, i52, i47, i69, i52)
f500_0_le_ConstantStackPush(EOS, i47, i52, i47, i69, i52) → f519_0_le_IntArithmetic(EOS, i47, i52, i47, i69, i52, 1)
f519_0_le_IntArithmetic(EOS, i47, i52, i47, i69, i52, matching1) → f524_0_le_InvokeMethod(EOS, i47, i52, i47, i69, -(i52, 1)) | &&(>(i52, 0), =(matching1, 1))
f524_0_le_InvokeMethod(EOS, i47, i52, i47, i69, i75) → f528_0_le_Load(EOS, i69, i75, i69, i75)
f524_0_le_InvokeMethod(EOS, i47, i52, i47, i69, i75) → f528_1_le_Load(EOS, i47, i52, i47, i69, i75, i69, i75)
f528_0_le_Load(EOS, i69, i75, i69, i75) → f544_0_le_Load(EOS, i69, i75, i69, i75)
f544_0_le_Load(EOS, i69, i75, i69, i75) → f298_0_le_Load(EOS, i69, i75, i69, i75)
f298_0_le_Load(EOS, i19, i36, i19, i36) → f308_0_le_LE(EOS, i19, i36, i19, i36, i19)

Combined rules. Obtained 2 IRules

P rules:
f308_0_le_LE(EOS, x0, x1, x0, x1, x0) → f528_1_le_Load(EOS, x0, x1, x0, -(x0, 1), -(x1, 1), -(x0, 1), -(x1, 1)) | &&(>(x1, 0), >(x0, 0))
f308_0_le_LE(EOS, x0, x1, x0, x1, x0) → f308_0_le_LE(EOS, -(x0, 1), -(x1, 1), -(x0, 1), -(x1, 1), -(x0, 1)) | &&(>(x1, 0), >(x0, 0))

Filtered ground terms:

f308_0_le_LE(x1, x2, x3, x4, x5, x6) → f308_0_le_LE(x2, x3, x4, x5, x6)
Cond_f308_0_le_LE(x1, x2, x3, x4, x5, x6, x7) → Cond_f308_0_le_LE(x1, x3, x4, x5, x6, x7)
f528_1_le_Load(x1, x2, x3, x4, x5, x6, x7, x8) → f528_1_le_Load(x2, x3, x4, x5, x6, x7, x8)
Cond_f308_0_le_LE1(x1, x2, x3, x4, x5, x6, x7) → Cond_f308_0_le_LE1(x1, x3, x4, x5, x6, x7)

Filtered duplicate terms:

f308_0_le_LE(x1, x2, x3, x4, x5) → f308_0_le_LE(x4, x5)
Cond_f308_0_le_LE(x1, x2, x3, x4, x5, x6) → Cond_f308_0_le_LE(x1, x5, x6)
f528_1_le_Load(x1, x2, x3, x4, x5, x6, x7) → f528_1_le_Load(x6, x7)
Cond_f308_0_le_LE1(x1, x2, x3, x4, x5, x6) → Cond_f308_0_le_LE1(x1, x5, x6)

Filtered unneeded terms:

Cond_f308_0_le_LE(x1, x2, x3) → Cond_f308_0_le_LE(x1)

Prepared 2 rules for path length conversion:

P rules:
f308_0_le_LE(x1, x0) → f528_1_le_Load(-(x0, 1), -(x1, 1)) | &&(>(x1, 0), >(x0, 0))
f308_0_le_LE(x1, x0) → f308_0_le_LE(-(x1, 1), -(x0, 1)) | &&(>(x1, 0), >(x0, 0))

Finished conversion. Obtained 1 rules.

P rules:
f308_0_le_LE(x2, x3) → f308_0_le_LE(-(x2, 1), -(x3, 1)) | &&(>(x2, 0), >(x3, 0))

(6) Obligation:

Rules:
f308_0_le_LE(x2, x3) → f308_0_le_LE(-(x2, 1), -(x3, 1)) | &&(>(x2, 0), >(x3, 0))

(7) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f308_0_le_LE(x3, x5)] = x3

Therefore the following rule(s) have been dropped:

f308_0_le_LE(x0, x1) → f308_0_le_LE(-(x0, 1), -(x1, 1)) | &&(>(x0, 0), >(x1, 0))

(8) YES