Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

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

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

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

EqUserDefRec.eq(II)Z: Graph of 45 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: EqUserDefRec.eq(II)Z
SCC calls the following helper methods: EqUserDefRec.eq(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:
f315_0_eq_LE(EOS, i48, i36, i48, i36, i48) → f320_0_eq_LE(EOS, i48, i36, i48, i36, i48)
f320_0_eq_LE(EOS, i48, i36, i48, i36, i48) → f332_0_eq_Load(EOS, i48, i36, i48, i36) | >(i48, 0)
f332_0_eq_Load(EOS, i48, i36, i48, i36) → f349_0_eq_LE(EOS, i48, i36, i48, i36, i36)
f349_0_eq_LE(EOS, i48, i54, i48, i54, i54) → f366_0_eq_LE(EOS, i48, i54, i48, i54, i54)
f366_0_eq_LE(EOS, i48, i54, i48, i54, i54) → f397_0_eq_Load(EOS, i48, i54, i48, i54) | >(i54, 0)
f397_0_eq_Load(EOS, i48, i54, i48, i54) → f424_0_eq_ConstantStackPush(EOS, i48, i54, i48, i54, i48)
f424_0_eq_ConstantStackPush(EOS, i48, i54, i48, i54, i48) → f454_0_eq_IntArithmetic(EOS, i48, i54, i48, i54, i48, 1)
f454_0_eq_IntArithmetic(EOS, i48, i54, i48, i54, i48, matching1) → f482_0_eq_Load(EOS, i48, i54, i48, i54, -(i48, 1)) | &&(>(i48, 0), =(matching1, 1))
f482_0_eq_Load(EOS, i48, i54, i48, i54, i66) → f504_0_eq_ConstantStackPush(EOS, i48, i54, i48, i54, i66, i54)
f504_0_eq_ConstantStackPush(EOS, i48, i54, i48, i54, i66, i54) → f559_0_eq_IntArithmetic(EOS, i48, i54, i48, i54, i66, i54, 1)
f559_0_eq_IntArithmetic(EOS, i48, i54, i48, i54, i66, i54, matching1) → f583_0_eq_InvokeMethod(EOS, i48, i54, i48, i54, i66, -(i54, 1)) | &&(>(i54, 0), =(matching1, 1))
f583_0_eq_InvokeMethod(EOS, i48, i54, i48, i54, i66, i84) → f587_0_eq_Load(EOS, i66, i84, i66, i84)
f583_0_eq_InvokeMethod(EOS, i48, i54, i48, i54, i66, i84) → f587_1_eq_Load(EOS, i48, i54, i48, i54, i66, i84, i66, i84)
f587_0_eq_Load(EOS, i66, i84, i66, i84) → f601_0_eq_Load(EOS, i66, i84, i66, i84)
f601_0_eq_Load(EOS, i66, i84, i66, i84) → f305_0_eq_Load(EOS, i66, i84, i66, i84)
f305_0_eq_Load(EOS, i18, i36, i18, i36) → f315_0_eq_LE(EOS, i18, i36, i18, i36, i18)

Combined rules. Obtained 2 IRules

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

Filtered ground terms:

f315_0_eq_LE(x1, x2, x3, x4, x5, x6) → f315_0_eq_LE(x2, x3, x4, x5, x6)
Cond_f315_0_eq_LE(x1, x2, x3, x4, x5, x6, x7) → Cond_f315_0_eq_LE(x1, x3, x4, x5, x6, x7)
f587_1_eq_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → f587_1_eq_Load(x2, x3, x4, x5, x6, x7, x8, x9)
Cond_f315_0_eq_LE1(x1, x2, x3, x4, x5, x6, x7) → Cond_f315_0_eq_LE1(x1, x3, x4, x5, x6, x7)

Filtered duplicate terms:

f315_0_eq_LE(x1, x2, x3, x4, x5) → f315_0_eq_LE(x4, x5)
Cond_f315_0_eq_LE(x1, x2, x3, x4, x5, x6) → Cond_f315_0_eq_LE(x1, x5, x6)
f587_1_eq_Load(x1, x2, x3, x4, x5, x6, x7, x8) → f587_1_eq_Load(x7, x8)
Cond_f315_0_eq_LE1(x1, x2, x3, x4, x5, x6) → Cond_f315_0_eq_LE1(x1, x5, x6)

Filtered unneeded terms:

Cond_f315_0_eq_LE(x1, x2, x3) → Cond_f315_0_eq_LE(x1)

Prepared 2 rules for path length conversion:

P rules:
f315_0_eq_LE(x1, x0) → f587_1_eq_Load(-(x0, 1), -(x1, 1)) | &&(>(x1, 0), >(x0, 0))
f315_0_eq_LE(x1, x0) → f315_0_eq_LE(-(x1, 1), -(x0, 1)) | &&(>(x1, 0), >(x0, 0))

Finished conversion. Obtained 1 rules.

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

(6) Obligation:

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

(7) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f315_0_eq_LE(x3, x5)] = x3

Therefore the following rule(s) have been dropped:

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

(8) YES