Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

public class MinusMin{

  public static int min (int x, int y) {

    if (x < y) return x;
    else return y;
  }


  public static void main(String[] args) {
    Random.args = args;
    int x = Random.random();
    int y = Random.random();
    int res = 0;



    while (min(x-1,y) == y) {

      y++;
      res++;

    }


  }

}


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

  public static int random() {
    String string = args[index];
    index++;
    return string.length();
  }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
MinusMin.main([Ljava/lang/String;)V: Graph of 195 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: MinusMin.main([Ljava/lang/String;)V
SCC calls the following helper methods:
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 23 IRules

P rules:
f771_0_main_ConstantStackPush(EOS, i18, i105, i18) → f775_0_main_IntArithmetic(EOS, i18, i105, i18, 1)
f775_0_main_IntArithmetic(EOS, i18, i105, i18, matching1) → f776_0_main_Load(EOS, i18, i105, -(i18, 1)) | &&(>=(i18, 0), =(matching1, 1))
f776_0_main_Load(EOS, i18, i105, i111) → f780_0_main_InvokeMethod(EOS, i18, i105, i111, i105)
f780_0_main_InvokeMethod(EOS, i18, i105, i111, i105) → f781_0_min_Load(EOS, i18, i105, i111, i105, i111, i105)
f781_0_min_Load(EOS, i18, i105, i111, i105, i111, i105) → f784_0_min_Load(EOS, i18, i105, i111, i105, i111, i105, i111)
f784_0_min_Load(EOS, i18, i105, i111, i105, i111, i105, i111) → f787_0_min_GE(EOS, i18, i105, i111, i105, i111, i105, i111, i105)
f787_0_min_GE(EOS, i18, i105, i111, i105, i111, i105, i111, i105) → f789_0_min_GE(EOS, i18, i105, i111, i105, i111, i105, i111, i105)
f787_0_min_GE(EOS, i18, i105, i111, i105, i111, i105, i111, i105) → f790_0_min_GE(EOS, i18, i105, i111, i105, i111, i105, i111, i105)
f789_0_min_GE(EOS, i18, i105, i111, i105, i111, i105, i111, i105) → f793_0_min_Load(EOS, i18, i105, i111, i105, i105) | >=(i111, i105)
f793_0_min_Load(EOS, i18, i105, i111, i105, i105) → f797_0_min_Return(EOS, i18, i105, i111, i105, i105)
f797_0_min_Return(EOS, i18, i105, i111, i105, i105) → f801_0_main_Load(EOS, i18, i105, i105)
f801_0_main_Load(EOS, i18, i105, i105) → f811_0_main_Load(EOS, i18, i105, i105)
f811_0_main_Load(EOS, i18, i105, i111) → f816_0_main_NE(EOS, i18, i105, i111, i105)
f816_0_main_NE(EOS, i18, i105, i105, i105) → f819_0_main_NE(EOS, i18, i105, i105, i105)
f819_0_main_NE(EOS, i18, i105, i105, i105) → f824_0_main_Inc(EOS, i18, i105)
f824_0_main_Inc(EOS, i18, i105) → f827_0_main_Inc(EOS, i18, +(i105, 1)) | >=(i105, 0)
f827_0_main_Inc(EOS, i18, i117) → f831_0_main_JMP(EOS, i18, i117)
f831_0_main_JMP(EOS, i18, i117) → f858_0_main_Load(EOS, i18, i117)
f858_0_main_Load(EOS, i18, i117) → f768_0_main_Load(EOS, i18, i117)
f768_0_main_Load(EOS, i18, i105) → f771_0_main_ConstantStackPush(EOS, i18, i105, i18)
f790_0_min_GE(EOS, i18, i105, i111, i105, i111, i105, i111, i105) → f795_0_min_Load(EOS, i18, i105, i111, i105, i111, i105) | <(i111, i105)
f795_0_min_Load(EOS, i18, i105, i111, i105, i111, i105) → f799_0_min_Return(EOS, i18, i105, i111, i105, i105, i111)
f799_0_min_Return(EOS, i18, i105, i111, i105, i105, i111) → f811_0_main_Load(EOS, i18, i105, i111)

Combined rules. Obtained 2 IRules

P rules:
f771_0_main_ConstantStackPush(EOS, x0, x1, x0) → f771_0_main_ConstantStackPush(EOS, x0, +(x1, 1), x0) | &&(&&(>(+(x1, 1), 0), >(+(x0, 1), 0)), <=(x1, -(x0, 1)))
f771_0_main_ConstantStackPush(EOS, arith, -(arith, 1), arith) → f771_0_main_ConstantStackPush(EOS, arith, arith, arith) | &&(<(-(arith, 1), -(arith, 1)), >(+(arith, 1), 1))

Filtered ground terms:

f771_0_main_ConstantStackPush(x1, x2, x3, x4) → f771_0_main_ConstantStackPush(x2, x3, x4)
Cond_f771_0_main_ConstantStackPush(x1, x2, x3, x4, x5) → Cond_f771_0_main_ConstantStackPush(x1, x3, x4, x5)
Cond_f771_0_main_ConstantStackPush1(x1, x2, x3, x4, x5) → Cond_f771_0_main_ConstantStackPush1(x1, x3, x4, x5)

Filtered duplicate terms:

f771_0_main_ConstantStackPush(x1, x2, x3) → f771_0_main_ConstantStackPush(x2, x3)
Cond_f771_0_main_ConstantStackPush(x1, x2, x3, x4) → Cond_f771_0_main_ConstantStackPush(x1, x3, x4)
Cond_f771_0_main_ConstantStackPush1(x1, x2, x3, x4) → Cond_f771_0_main_ConstantStackPush1(x1, x3)

Prepared 2 rules for path length conversion:

P rules:
f771_0_main_ConstantStackPush(x1, x0) → f771_0_main_ConstantStackPush(+(x1, 1), x0) | &&(&&(>(+(x1, 1), 0), >(+(x0, 1), 0)), <=(x1, -(x0, 1)))
f771_0_main_ConstantStackPush(-(arith, 1), arith) → f771_0_main_ConstantStackPush(arith, arith) | &&(<(-(arith, 1), -(arith, 1)), >(+(arith, 1), 1))

Finished conversion. Obtained 2 rules.

P rules:
f771_0_main_ConstantStackPush(x0, x1) → f771_0_main_ConstantStackPush(+(x0, 1), x1) | &&(&&(>(x1, -1), >(x0, -1)), >=(-(x1, 1), x0))
f771_0_main_ConstantStackPush(arith, x2) → f771_0_main_ConstantStackPush(x2, x2) | &&(&&(<(-(x2, 1), -(x2, 1)), >(x2, 0)), =(arith, -(x2, 1)))

(6) Obligation:

Rules:
f771_0_main_ConstantStackPush(x0, x1) → f771_0_main_ConstantStackPush(+(x0, 1), x1) | &&(&&(>(x1, -1), >(x0, -1)), >=(-(x1, 1), x0))
f771_0_main_ConstantStackPush(arith, x2) → f771_0_main_ConstantStackPush(x2, x2) | &&(&&(<(-(x2, 1), -(x2, 1)), >(x2, 0)), =(arith, -(x2, 1)))

(7) TerminationGraphProcessor (SOUND transformation)

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

(8) Obligation:

Rules:
f771_0_main_ConstantStackPush(x0, x1) → f771_0_main_ConstantStackPush(+(x0, 1), x1) | &&(&&(>(x1, -1), >(x0, -1)), >=(-(x1, 1), x0))

(9) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f771_0_main_ConstantStackPush(x3, x5)] = -x3 + x5

Therefore the following rule(s) have been dropped:

f771_0_main_ConstantStackPush(x0, x1) → f771_0_main_ConstantStackPush(+(x0, 1), x1) | &&(&&(>(x1, -1), >(x0, -1)), >=(-(x1, 1), x0))

(10) YES