Termination proof of /tmp/tmp2P5AEQ/Log.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBC2FIG (⇐)

↳2 FIGraph

↳3 FIGtoITRSProof (⇐)

↳4 ITRS

↳5 GroundTermsRemoverProof (⇔)

↳6 ITRS

↳7 ITRStoIDPProof (⇔)

↳8 IDP

↳9 UsableRulesProof (⇔)

↳10 IDP

↳11 IDPNonInfProof (⇐)

↳12 AND

    ↳13 IDP

        ↳14 IDependencyGraphProof (⇔)

        ↳15 IDP

        ↳16 IDPNonInfProof (⇐)

        ↳17 AND

            ↳18 IDP

                ↳19 IDependencyGraphProof (⇔)

                ↳20 TRUE

            ↳21 IDP

                ↳22 IDependencyGraphProof (⇔)

                ↳23 TRUE

    ↳24 IDP

        ↳25 IDependencyGraphProof (⇔)

        ↳26 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: Log

public class Log{
  public static int half(int x) {

    int res = 0;

    while (x > 1) {

      x = x-2;
      res++;

    }

    return res;

  }


  public static int log(int x) {

    int res = 0;

    while (x > 1) {

      x = half(x);
      res++;

    }

    return res;

  }


  public static void main(String[] args) {
    Random.args = args;
    int x = Random.random();
    log(x);
  }
}


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

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

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 157 nodes with 1 SCC.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph to ITRS rules

(4) Obligation:

ITRS problem:

The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load872(1, i63, i53) → Cond_Load872(i63 > 1, 1, i63, i53)
Cond_Load872(TRUE, 1, i63, i53) → Load1049(1, i53, i63, 0)
Load1049(1, i53, i91, i84) → Cond_Load1049(i91 > 1 && i84 + 1 > 0, 1, i53, i91, i84)
Cond_Load1049(TRUE, 1, i53, i91, i84) → Load1049(1, i53, i91 - 2, i84 + 1)
Load1049(1, i53, i91, i84) → Cond_Load10491(i91 > 0 && i91 <= 1, 1, i53, i91, i84)
Cond_Load10491(TRUE, 1, i53, i91, i84) → Load1065(1, i53, i84)
Load1065(1, i53, i84) → Load872(1, i84, i53 + 1)
Load1049(1, i53, i90, i84) → Cond_Load10492(i90 <= 1 && i53 + 1 > 0, 1, i53, i90, i84)
Cond_Load10492(TRUE, 1, i53, i90, i84) → Load872(1, i84, i53 + 1)
The set Q consists of the following terms:
Load872(1, x0, x1)
Cond_Load872(TRUE, 1, x0, x1)
Load1049(1, x0, x1, x2)
Cond_Load1049(TRUE, 1, x0, x1, x2)
Cond_Load10491(TRUE, 1, x0, x1, x2)
Load1065(1, x0, x1)
Cond_Load10492(TRUE, 1, x0, x1, x2)

(5) GroundTermsRemoverProof (EQUIVALENT transformation)

Some arguments are removed because they always contain the same ground term.
We removed the following ground terms:

We removed arguments according to the following replacements:

Cond_Load10492(x1, x2, x3, x4, x5) → Cond_Load10492(x1, x3, x4, x5)
Load1049(x1, x2, x3, x4) → Load1049(x2, x3, x4)
Load872(x1, x2, x3) → Load872(x2, x3)
Load1065(x1, x2, x3) → Load1065(x2, x3)
Cond_Load10491(x1, x2, x3, x4, x5) → Cond_Load10491(x1, x3, x4, x5)
Cond_Load1049(x1, x2, x3, x4, x5) → Cond_Load1049(x1, x3, x4, x5)
Cond_Load872(x1, x2, x3, x4) → Cond_Load872(x1, x3, x4)

(6) Obligation:

ITRS problem:

The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load872(i63, i53) → Cond_Load872(i63 > 1, i63, i53)
Cond_Load872(TRUE, i63, i53) → Load1049(i53, i63, 0)
Load1049(i53, i91, i84) → Cond_Load1049(i91 > 1 && i84 + 1 > 0, i53, i91, i84)
Cond_Load1049(TRUE, i53, i91, i84) → Load1049(i53, i91 - 2, i84 + 1)
Load1049(i53, i91, i84) → Cond_Load10491(i91 > 0 && i91 <= 1, i53, i91, i84)
Cond_Load10491(TRUE, i53, i91, i84) → Load1065(i53, i84)
Load1065(i53, i84) → Load872(i84, i53 + 1)
Load1049(i53, i90, i84) → Cond_Load10492(i90 <= 1 && i53 + 1 > 0, i53, i90, i84)
Cond_Load10492(TRUE, i53, i90, i84) → Load872(i84, i53 + 1)
The set Q consists of the following terms:
Load872(x0, x1)
Cond_Load872(TRUE, x0, x1)
Load1049(x0, x1, x2)
Cond_Load1049(TRUE, x0, x1, x2)
Cond_Load10491(TRUE, x0, x1, x2)
Load1065(x0, x1)
Cond_Load10492(TRUE, x0, x1, x2)

(7) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(8) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

The ITRS R consists of the following rules:
Load872(i63, i53) → Cond_Load872(i63 > 1, i63, i53)
Cond_Load872(TRUE, i63, i53) → Load1049(i53, i63, 0)
Load1049(i53, i91, i84) → Cond_Load1049(i91 > 1 && i84 + 1 > 0, i53, i91, i84)
Cond_Load1049(TRUE, i53, i91, i84) → Load1049(i53, i91 - 2, i84 + 1)
Load1049(i53, i91, i84) → Cond_Load10491(i91 > 0 && i91 <= 1, i53, i91, i84)
Cond_Load10491(TRUE, i53, i91, i84) → Load1065(i53, i84)
Load1065(i53, i84) → Load872(i84, i53 + 1)
Load1049(i53, i90, i84) → Cond_Load10492(i90 <= 1 && i53 + 1 > 0, i53, i90, i84)
Cond_Load10492(TRUE, i53, i90, i84) → Load872(i84, i53 + 1)

The integer pair graph contains the following rules and edges:
(0): LOAD872(i63[0], i53[0]) → COND_LOAD872(i63[0] > 1, i63[0], i53[0])
(1): COND_LOAD872(TRUE, i63[1], i53[1]) → LOAD1049(i53[1], i63[1], 0)
(2): LOAD1049(i53[2], i91[2], i84[2]) → COND_LOAD1049(i91[2] > 1 && i84[2] + 1 > 0, i53[2], i91[2], i84[2])
(3): COND_LOAD1049(TRUE, i53[3], i91[3], i84[3]) → LOAD1049(i53[3], i91[3] - 2, i84[3] + 1)
(4): LOAD1049(i53[4], i91[4], i84[4]) → COND_LOAD10491(i91[4] > 0 && i91[4] <= 1, i53[4], i91[4], i84[4])
(5): COND_LOAD10491(TRUE, i53[5], i91[5], i84[5]) → LOAD1065(i53[5], i84[5])
(6): LOAD1065(i53[6], i84[6]) → LOAD872(i84[6], i53[6] + 1)
(7): LOAD1049(i53[7], i90[7], i84[7]) → COND_LOAD10492(i90[7] <= 1 && i53[7] + 1 > 0, i53[7], i90[7], i84[7])
(8): COND_LOAD10492(TRUE, i53[8], i90[8], i84[8]) → LOAD872(i84[8], i53[8] + 1)

(0) -> (1), if ((i63[0] →^* i63[1])∧(i63[0] > 1 →^* TRUE)∧(i53[0] →^* i53[1]))

(1) -> (2), if ((i53[1] →^* i53[2])∧(0 →^* i84[2])∧(i63[1] →^* i91[2]))

(1) -> (4), if ((i53[1] →^* i53[4])∧(0 →^* i84[4])∧(i63[1] →^* i91[4]))

(1) -> (7), if ((i53[1] →^* i53[7])∧(i63[1] →^* i90[7])∧(0 →^* i84[7]))

(2) -> (3), if ((i84[2] →^* i84[3])∧(i91[2] →^* i91[3])∧(i53[2] →^* i53[3])∧(i91[2] > 1 && i84[2] + 1 > 0 →^* TRUE))

(3) -> (2), if ((i91[3] - 2 →^* i91[2])∧(i84[3] + 1 →^* i84[2])∧(i53[3] →^* i53[2]))

(3) -> (4), if ((i84[3] + 1 →^* i84[4])∧(i91[3] - 2 →^* i91[4])∧(i53[3] →^* i53[4]))

(3) -> (7), if ((i84[3] + 1 →^* i84[7])∧(i53[3] →^* i53[7])∧(i91[3] - 2 →^* i90[7]))

(4) -> (5), if ((i84[4] →^* i84[5])∧(i91[4] > 0 && i91[4] <= 1 →^* TRUE)∧(i91[4] →^* i91[5])∧(i53[4] →^* i53[5]))

(5) -> (6), if ((i53[5] →^* i53[6])∧(i84[5] →^* i84[6]))

(6) -> (0), if ((i53[6] + 1 →^* i53[0])∧(i84[6] →^* i63[0]))

(7) -> (8), if ((i90[7] →^* i90[8])∧(i90[7] <= 1 && i53[7] + 1 > 0 →^* TRUE)∧(i84[7] →^* i84[8])∧(i53[7] →^* i53[8]))

(8) -> (0), if ((i53[8] + 1 →^* i53[0])∧(i84[8] →^* i63[0]))

The set Q consists of the following terms:
Load872(x0, x1)
Cond_Load872(TRUE, x0, x1)
Load1049(x0, x1, x2)
Cond_Load1049(TRUE, x0, x1, x2)
Cond_Load10491(TRUE, x0, x1, x2)
Load1065(x0, x1)
Cond_Load10492(TRUE, x0, x1, x2)

(9) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(10) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD872(i63[0], i53[0]) → COND_LOAD872(i63[0] > 1, i63[0], i53[0])
(1): COND_LOAD872(TRUE, i63[1], i53[1]) → LOAD1049(i53[1], i63[1], 0)
(2): LOAD1049(i53[2], i91[2], i84[2]) → COND_LOAD1049(i91[2] > 1 && i84[2] + 1 > 0, i53[2], i91[2], i84[2])
(3): COND_LOAD1049(TRUE, i53[3], i91[3], i84[3]) → LOAD1049(i53[3], i91[3] - 2, i84[3] + 1)
(4): LOAD1049(i53[4], i91[4], i84[4]) → COND_LOAD10491(i91[4] > 0 && i91[4] <= 1, i53[4], i91[4], i84[4])
(5): COND_LOAD10491(TRUE, i53[5], i91[5], i84[5]) → LOAD1065(i53[5], i84[5])
(6): LOAD1065(i53[6], i84[6]) → LOAD872(i84[6], i53[6] + 1)
(7): LOAD1049(i53[7], i90[7], i84[7]) → COND_LOAD10492(i90[7] <= 1 && i53[7] + 1 > 0, i53[7], i90[7], i84[7])
(8): COND_LOAD10492(TRUE, i53[8], i90[8], i84[8]) → LOAD872(i84[8], i53[8] + 1)