Termination proof of /tmp/tmpg-zVm-/LogAG.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: LogAG

public class LogAG{

  // adapted from Arts&Giesl, 2001

  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-2)+1;
      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 161 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:
Load945(1, i80, i70) → Cond_Load945(i80 > 1, 1, i80, i70)
Cond_Load945(TRUE, 1, i80, i70) → Load1158(1, i70, i80 - 2, 0)
Load1158(1, i70, i133, i123) → Cond_Load1158(i133 > 1 && i123 + 1 > 0, 1, i70, i133, i123)
Cond_Load1158(TRUE, 1, i70, i133, i123) → Load1158(1, i70, i133 - 2, i123 + 1)
Load1158(1, i70, i133, i123) → Cond_Load11581(i133 > 0 && i133 <= 1, 1, i70, i133, i123)
Cond_Load11581(TRUE, 1, i70, i133, i123) → Load1172(1, i70, i123)
Load1172(1, i70, i123) → Load945(1, i123 + 1, i70 + 1)
Load1158(1, i70, i132, i123) → Cond_Load11582(i132 <= 1 && i70 + 1 > 0 && i123 + 1 > 0, 1, i70, i132, i123)
Cond_Load11582(TRUE, 1, i70, i132, i123) → Load945(1, i123 + 1, i70 + 1)
The set Q consists of the following terms:
Load945(1, x0, x1)
Cond_Load945(TRUE, 1, x0, x1)
Load1158(1, x0, x1, x2)
Cond_Load1158(TRUE, 1, x0, x1, x2)
Cond_Load11581(TRUE, 1, x0, x1, x2)
Load1172(1, x0, x1)
Cond_Load11582(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_Load11582(x1, x2, x3, x4, x5) → Cond_Load11582(x1, x3, x4, x5)
Load1158(x1, x2, x3, x4) → Load1158(x2, x3, x4)
Load945(x1, x2, x3) → Load945(x2, x3)
Load1172(x1, x2, x3) → Load1172(x2, x3)
Cond_Load11581(x1, x2, x3, x4, x5) → Cond_Load11581(x1, x3, x4, x5)
Cond_Load1158(x1, x2, x3, x4, x5) → Cond_Load1158(x1, x3, x4, x5)
Cond_Load945(x1, x2, x3, x4) → Cond_Load945(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:
Load945(i80, i70) → Cond_Load945(i80 > 1, i80, i70)
Cond_Load945(TRUE, i80, i70) → Load1158(i70, i80 - 2, 0)
Load1158(i70, i133, i123) → Cond_Load1158(i133 > 1 && i123 + 1 > 0, i70, i133, i123)
Cond_Load1158(TRUE, i70, i133, i123) → Load1158(i70, i133 - 2, i123 + 1)
Load1158(i70, i133, i123) → Cond_Load11581(i133 > 0 && i133 <= 1, i70, i133, i123)
Cond_Load11581(TRUE, i70, i133, i123) → Load1172(i70, i123)
Load1172(i70, i123) → Load945(i123 + 1, i70 + 1)
Load1158(i70, i132, i123) → Cond_Load11582(i132 <= 1 && i70 + 1 > 0 && i123 + 1 > 0, i70, i132, i123)
Cond_Load11582(TRUE, i70, i132, i123) → Load945(i123 + 1, i70 + 1)
The set Q consists of the following terms:
Load945(x0, x1)
Cond_Load945(TRUE, x0, x1)
Load1158(x0, x1, x2)
Cond_Load1158(TRUE, x0, x1, x2)
Cond_Load11581(TRUE, x0, x1, x2)
Load1172(x0, x1)
Cond_Load11582(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:
Load945(i80, i70) → Cond_Load945(i80 > 1, i80, i70)
Cond_Load945(TRUE, i80, i70) → Load1158(i70, i80 - 2, 0)
Load1158(i70, i133, i123) → Cond_Load1158(i133 > 1 && i123 + 1 > 0, i70, i133, i123)
Cond_Load1158(TRUE, i70, i133, i123) → Load1158(i70, i133 - 2, i123 + 1)
Load1158(i70, i133, i123) → Cond_Load11581(i133 > 0 && i133 <= 1, i70, i133, i123)
Cond_Load11581(TRUE, i70, i133, i123) → Load1172(i70, i123)
Load1172(i70, i123) → Load945(i123 + 1, i70 + 1)
Load1158(i70, i132, i123) → Cond_Load11582(i132 <= 1 && i70 + 1 > 0 && i123 + 1 > 0, i70, i132, i123)
Cond_Load11582(TRUE, i70, i132, i123) → Load945(i123 + 1, i70 + 1)

The integer pair graph contains the following rules and edges:
(0): LOAD945(i80[0], i70[0]) → COND_LOAD945(i80[0] > 1, i80[0], i70[0])
(1): COND_LOAD945(TRUE, i80[1], i70[1]) → LOAD1158(i70[1], i80[1] - 2, 0)
(2): LOAD1158(i70[2], i133[2], i123[2]) → COND_LOAD1158(i133[2] > 1 && i123[2] + 1 > 0, i70[2], i133[2], i123[2])
(3): COND_LOAD1158(TRUE, i70[3], i133[3], i123[3]) → LOAD1158(i70[3], i133[3] - 2, i123[3] + 1)
(4): LOAD1158(i70[4], i133[4], i123[4]) → COND_LOAD11581(i133[4] > 0 && i133[4] <= 1, i70[4], i133[4], i123[4])
(5): COND_LOAD11581(TRUE, i70[5], i133[5], i123[5]) → LOAD1172(i70[5], i123[5])
(6): LOAD1172(i70[6], i123[6]) → LOAD945(i123[6] + 1, i70[6] + 1)
(7): LOAD1158(i70[7], i132[7], i123[7]) → COND_LOAD11582(i132[7] <= 1 && i70[7] + 1 > 0 && i123[7] + 1 > 0, i70[7], i132[7], i123[7])
(8): COND_LOAD11582(TRUE, i70[8], i132[8], i123[8]) → LOAD945(i123[8] + 1, i70[8] + 1)

(0) -> (1), if ((i80[0] →^* i80[1])∧(i80[0] > 1 →^* TRUE)∧(i70[0] →^* i70[1]))

(1) -> (2), if ((0 →^* i123[2])∧(i80[1] - 2 →^* i133[2])∧(i70[1] →^* i70[2]))

(1) -> (4), if ((i70[1] →^* i70[4])∧(i80[1] - 2 →^* i133[4])∧(0 →^* i123[4]))

(1) -> (7), if ((0 →^* i123[7])∧(i70[1] →^* i70[7])∧(i80[1] - 2 →^* i132[7]))

(2) -> (3), if ((i133[2] > 1 && i123[2] + 1 > 0 →^* TRUE)∧(i123[2] →^* i123[3])∧(i133[2] →^* i133[3])∧(i70[2] →^* i70[3]))

(3) -> (2), if ((i70[3] →^* i70[2])∧(i133[3] - 2 →^* i133[2])∧(i123[3] + 1 →^* i123[2]))

(3) -> (4), if ((i70[3] →^* i70[4])∧(i133[3] - 2 →^* i133[4])∧(i123[3] + 1 →^* i123[4]))

(3) -> (7), if ((i123[3] + 1 →^* i123[7])∧(i70[3] →^* i70[7])∧(i133[3] - 2 →^* i132[7]))

(4) -> (5), if ((i133[4] > 0 && i133[4] <= 1 →^* TRUE)∧(i133[4] →^* i133[5])∧(i70[4] →^* i70[5])∧(i123[4] →^* i123[5]))

(5) -> (6), if ((i123[5] →^* i123[6])∧(i70[5] →^* i70[6]))

(6) -> (0), if ((i123[6] + 1 →^* i80[0])∧(i70[6] + 1 →^* i70[0]))

(7) -> (8), if ((i132[7] <= 1 && i70[7] + 1 > 0 && i123[7] + 1 > 0 →^* TRUE)∧(i70[7] →^* i70[8])∧(i123[7] →^* i123[8])∧(i132[7] →^* i132[8]))

(8) -> (0), if ((i123[8] + 1 →^* i80[0])∧(i70[8] + 1 →^* i70[0]))

The set Q consists of the following terms:
Load945(x0, x1)
Cond_Load945(TRUE, x0, x1)
Load1158(x0, x1, x2)
Cond_Load1158(TRUE, x0, x1, x2)
Cond_Load11581(TRUE, x0, x1, x2)
Load1172(x0, x1)
Cond_Load11582(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): LOAD945(i80[0], i70[0]) → COND_LOAD945(i80[0] > 1, i80[0], i70[0])
(1): COND_LOAD945(TRUE, i80[1], i70[1]) → LOAD1158(i70[1], i80[1] - 2, 0)
(2): LOAD1158(i70[2], i133[2], i123[2]) → COND_LOAD1158(i133[2] > 1 && i123[2] + 1 > 0, i70[2], i133[2], i123[2])
(3): COND_LOAD1158(TRUE, i70[3], i133[3], i123[3]) → LOAD1158(i70[3], i133[3] - 2, i123[3] + 1)
(4): LOAD1158(i70[4], i133[4], i123[4]) → COND_LOAD11581(i133[4] > 0 && i133[4] <= 1, i70[4], i133[4], i123[4])
(5): COND_LOAD11581(TRUE, i70[5], i133[5], i123[5]) → LOAD1172(i70[5], i123[5])
(6): LOAD1172(i70[6], i123[6]) → LOAD945(i123[6] + 1, i70[6] + 1)
(7): LOAD1158(i70[7], i132[7], i123[7]) → COND_LOAD11582(i132[7] <= 1 && i70[7] + 1 > 0 && i123[7] + 1 > 0, i70[7], i132[7], i123[7])
(8): COND_LOAD11582(TRUE, i70[8], i132[8], i123[8]) → LOAD945(i123[8] + 1, i70[8] + 1)