Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

package Nest;

public class Nest{
    public static int nest(int x){
		if (x == 0) return 0;
		else return nest(nest(x-1));
    }

    
    public static void main(final String[] args) {
        final int x = args[0].length();
        final int y = nest(x);
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

Nest.Nest.nest(I)I: Graph of 23 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: Nest.Nest.nest(I)I
SCC calls the following helper methods: Nest.Nest.nest(I)I
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 20 IRules

P rules:
f131_0_nest_NE(EOS, i23, i23, i23) → f136_0_nest_NE(EOS, i23, i23, i23)
f136_0_nest_NE(EOS, i23, i23, i23) → f139_0_nest_Load(EOS, i23, i23) | >(i23, 0)
f139_0_nest_Load(EOS, i23, i23) → f143_0_nest_ConstantStackPush(EOS, i23, i23)
f143_0_nest_ConstantStackPush(EOS, i23, i23) → f150_0_nest_IntArithmetic(EOS, i23, i23, 1)
f150_0_nest_IntArithmetic(EOS, i23, i23, matching1) → f157_0_nest_InvokeMethod(EOS, i23, -(i23, 1)) | &&(>(i23, 0), =(matching1, 1))
f157_0_nest_InvokeMethod(EOS, i23, i24) → f205_0_nest_Load(EOS, i24, i24)
f157_0_nest_InvokeMethod(EOS, i23, i24) → f205_1_nest_Load(EOS, i23, i24, i24)
f205_0_nest_Load(EOS, i24, i24) → f210_0_nest_Load(EOS, i24, i24)
f210_0_nest_Load(EOS, i24, i24) → f130_0_nest_Load(EOS, i24, i24)
f130_0_nest_Load(EOS, i18, i18) → f131_0_nest_NE(EOS, i18, i18, i18)
f234_0_nest_Return(EOS, i23, matching1, matching2, matching3) → f238_0_nest_InvokeMethod(EOS, i23, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f238_0_nest_InvokeMethod(EOS, i23, matching1) → f325_0_nest_InvokeMethod(EOS, i23, 0) | =(matching1, 0)
f325_0_nest_InvokeMethod(EOS, i23, matching1) → f336_0_nest_Load(EOS, 0, 0) | =(matching1, 0)
f325_0_nest_InvokeMethod(EOS, i23, matching1) → f336_1_nest_Load(EOS, i23, 0, 0) | =(matching1, 0)
f336_0_nest_Load(EOS, matching1, matching2) → f340_0_nest_Load(EOS, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
f340_0_nest_Load(EOS, matching1, matching2) → f130_0_nest_Load(EOS, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
f399_0_nest_Return(EOS, i23, i54, matching1) → f314_0_nest_Return(EOS, i23, i54, 0) | =(matching1, 0)
f314_0_nest_Return(EOS, i23, i42, matching1) → f325_0_nest_InvokeMethod(EOS, i23, 0) | =(matching1, 0)
f205_1_nest_Load(EOS, i23, matching1, matching2) → f234_0_nest_Return(EOS, i23, 0, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
f205_1_nest_Load(EOS, i23, i54, i54) → f399_0_nest_Return(EOS, i23, i54, 0)

Combined rules. Obtained 5 IRules

P rules:
f325_0_nest_InvokeMethod(EOS, i23, 0) → f336_1_nest_Load(EOS, i23, 0, 0)
f131_0_nest_NE(EOS, x0, x0, x0) → f131_0_nest_NE(EOS, -(x0, 1), -(x0, 1), -(x0, 1)) | >(x0, 0)
f325_0_nest_InvokeMethod(EOS, x0, 0) → f131_0_nest_NE(EOS, 0, 0, 0)
f131_0_nest_NE(EOS, 1, 1, 1) → f325_0_nest_InvokeMethod(EOS, 1, 0)
f131_0_nest_NE(EOS, x0, x0, x0) → f325_0_nest_InvokeMethod(EOS, x0, 0) | >(x0, 0)

Filtered ground terms:

f325_0_nest_InvokeMethod(x1, x2, x3) → f325_0_nest_InvokeMethod(x2)
f336_1_nest_Load(x1, x2, x3, x4) → f336_1_nest_Load(x2)
f131_0_nest_NE(x1, x2, x3, x4) → f131_0_nest_NE(x2, x3, x4)
Cond_f131_0_nest_NE(x1, x2, x3, x4, x5) → Cond_f131_0_nest_NE(x1, x3, x4, x5)
Cond_f131_0_nest_NE1(x1, x2, x3, x4, x5) → Cond_f131_0_nest_NE1(x1, x3, x4, x5)

Filtered duplicate terms:

f131_0_nest_NE(x1, x2, x3) → f131_0_nest_NE(x3)
Cond_f131_0_nest_NE(x1, x2, x3, x4) → Cond_f131_0_nest_NE(x1, x4)
Cond_f131_0_nest_NE1(x1, x2, x3, x4) → Cond_f131_0_nest_NE1(x1, x4)

Filtered unneeded terms:

Cond_f131_0_nest_NE1(x1, x2) → Cond_f131_0_nest_NE1(x1)

Prepared 5 rules for path length conversion:

P rules:
f325_0_nest_InvokeMethod(i23) → f336_1_nest_Load(i23)
f131_0_nest_NE(x0) → f131_0_nest_NE(-(x0, 1)) | >(x0, 0)
f325_0_nest_InvokeMethod(x0) → f131_0_nest_NE(0)
f131_0_nest_NE(1) → f325_0_nest_InvokeMethod(1)
f131_0_nest_NE(x0) → f325_0_nest_InvokeMethod(x0) | >(x0, 0)

Finished conversion. Obtained 4 rules.

P rules:
f131_0_nest_NE(x1) → f131_0_nest_NE(-(x1, 1)) | >(x1, 0)
f325_0_nest_InvokeMethod(x2) → f131_0_nest_NE(0)
f131_0_nest_NE(c1) → f325_0_nest_InvokeMethod(1) | =(1, c1)
f131_0_nest_NE(x3) → f325_0_nest_InvokeMethod(x3) | >(x3, 0)

(6) Obligation:

Rules:
f131_0_nest_NE(x1) → f131_0_nest_NE(-(x1, 1)) | >(x1, 0)
f325_0_nest_InvokeMethod(x2) → f131_0_nest_NE(0)
f131_0_nest_NE(c1) → f325_0_nest_InvokeMethod(1) | =(1, c1)
f131_0_nest_NE(x3) → f325_0_nest_InvokeMethod(x3) | >(x3, 0)

(7) TerminationGraphProcessor (SOUND transformation)

Constructed the termination graph and obtained one non-trivial SCC.

(8) Obligation:

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

(9) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f131_0_nest_NE(x2)] = x2

Therefore the following rule(s) have been dropped:

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

(10) YES