Termination proof of /tmp/tmptNaQ53/PastaB17.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBC2FIG (⇐)

↳2 FIGraph

↳3 FIGtoITRSProof (⇐)

↳4 ITRS

↳5 ITRStoIDPProof (⇔)

↳6 IDP

↳7 UsableRulesProof (⇔)

↳8 IDP

↳9 IDPNonInfProof (⇐)

↳10 AND

    ↳11 IDP

        ↳12 IDependencyGraphProof (⇔)

        ↳13 IDP

        ↳14 IDPNonInfProof (⇐)

        ↳15 AND

            ↳16 IDP

                ↳17 IDependencyGraphProof (⇔)

                ↳18 TRUE

            ↳19 IDP

                ↳20 IDependencyGraphProof (⇔)

                ↳21 TRUE

    ↳22 IDP

        ↳23 IDependencyGraphProof (⇔)

        ↳24 IDP

        ↳25 IDPNonInfProof (⇐)

        ↳26 AND

            ↳27 IDP

                ↳28 IDependencyGraphProof (⇔)

                ↳29 TRUE

            ↳30 IDP

                ↳31 IDependencyGraphProof (⇔)

                ↳32 TRUE

(0) Obligation:

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

/**
 * Example taken from "A Term Rewriting Approach to the Automated Termination
 * Analysis of Imperative Programs" (http://www.cs.unm.edu/~spf/papers/2009-02.pdf)
 * and converted to Java.
 */

public class PastaB17 {
    public static void main(String[] args) {
        Random.args = args;
        int x = Random.random();
        int y = Random.random();
        int z = Random.random();

        while (x > z) {
            while (y > z) {
                y--;
            }
            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 253 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:
Load1082(i8, i23, i56) → Cond_Load1082(i23 > i56, i8, i23, i56)
Cond_Load1082(TRUE, i8, i23, i56) → Load1082(i8, i23 + -1, i56)
Load1003(i8, i23, i56) → Cond_Load1003(i23 > i56 && i8 > i56, i8, i23, i56)
Cond_Load1003(TRUE, i8, i23, i56) → Load1082(i8, i23 + -1, i56)
Load1082(i8, i23, i56) → Cond_Load10821(i23 <= i56, i8, i23, i56)
Cond_Load10821(TRUE, i8, i23, i56) → Load1003(i8 + -1, i23, i56)
Load1003(i8, i23, i56) → Cond_Load10031(i23 <= i56 && i8 > i56, i8, i23, i56)
Cond_Load10031(TRUE, i8, i23, i56) → Load1003(i8 + -1, i23, i56)
The set Q consists of the following terms:
Load1082(x0, x1, x2)
Cond_Load1082(TRUE, x0, x1, x2)
Load1003(x0, x1, x2)
Cond_Load1003(TRUE, x0, x1, x2)
Cond_Load10821(TRUE, x0, x1, x2)
Cond_Load10031(TRUE, x0, x1, x2)

(5) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(6) 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:
Load1082(i8, i23, i56) → Cond_Load1082(i23 > i56, i8, i23, i56)
Cond_Load1082(TRUE, i8, i23, i56) → Load1082(i8, i23 + -1, i56)
Load1003(i8, i23, i56) → Cond_Load1003(i23 > i56 && i8 > i56, i8, i23, i56)
Cond_Load1003(TRUE, i8, i23, i56) → Load1082(i8, i23 + -1, i56)
Load1082(i8, i23, i56) → Cond_Load10821(i23 <= i56, i8, i23, i56)
Cond_Load10821(TRUE, i8, i23, i56) → Load1003(i8 + -1, i23, i56)
Load1003(i8, i23, i56) → Cond_Load10031(i23 <= i56 && i8 > i56, i8, i23, i56)
Cond_Load10031(TRUE, i8, i23, i56) → Load1003(i8 + -1, i23, i56)

The integer pair graph contains the following rules and edges:
(0): LOAD1082(i8[0], i23[0], i56[0]) → COND_LOAD1082(i23[0] > i56[0], i8[0], i23[0], i56[0])
(1): COND_LOAD1082(TRUE, i8[1], i23[1], i56[1]) → LOAD1082(i8[1], i23[1] + -1, i56[1])
(2): LOAD1003(i8[2], i23[2], i56[2]) → COND_LOAD1003(i23[2] > i56[2] && i8[2] > i56[2], i8[2], i23[2], i56[2])
(3): COND_LOAD1003(TRUE, i8[3], i23[3], i56[3]) → LOAD1082(i8[3], i23[3] + -1, i56[3])
(4): LOAD1082(i8[4], i23[4], i56[4]) → COND_LOAD10821(i23[4] <= i56[4], i8[4], i23[4], i56[4])
(5): COND_LOAD10821(TRUE, i8[5], i23[5], i56[5]) → LOAD1003(i8[5] + -1, i23[5], i56[5])
(6): LOAD1003(i8[6], i23[6], i56[6]) → COND_LOAD10031(i23[6] <= i56[6] && i8[6] > i56[6], i8[6], i23[6], i56[6])
(7): COND_LOAD10031(TRUE, i8[7], i23[7], i56[7]) → LOAD1003(i8[7] + -1, i23[7], i56[7])

(0) -> (1), if ((i8[0] →^* i8[1])∧(i56[0] →^* i56[1])∧(i23[0] > i56[0] →^* TRUE)∧(i23[0] →^* i23[1]))

(1) -> (0), if ((i8[1] →^* i8[0])∧(i23[1] + -1 →^* i23[0])∧(i56[1] →^* i56[0]))

(1) -> (4), if ((i23[1] + -1 →^* i23[4])∧(i56[1] →^* i56[4])∧(i8[1] →^* i8[4]))

(2) -> (3), if ((i23[2] > i56[2] && i8[2] > i56[2] →^* TRUE)∧(i23[2] →^* i23[3])∧(i56[2] →^* i56[3])∧(i8[2] →^* i8[3]))

(3) -> (0), if ((i8[3] →^* i8[0])∧(i23[3] + -1 →^* i23[0])∧(i56[3] →^* i56[0]))

(3) -> (4), if ((i23[3] + -1 →^* i23[4])∧(i56[3] →^* i56[4])∧(i8[3] →^* i8[4]))

(4) -> (5), if ((i8[4] →^* i8[5])∧(i23[4] <= i56[4] →^* TRUE)∧(i56[4] →^* i56[5])∧(i23[4] →^* i23[5]))

(5) -> (2), if ((i56[5] →^* i56[2])∧(i23[5] →^* i23[2])∧(i8[5] + -1 →^* i8[2]))

(5) -> (6), if ((i23[5] →^* i23[6])∧(i8[5] + -1 →^* i8[6])∧(i56[5] →^* i56[6]))

(6) -> (7), if ((i23[6] <= i56[6] && i8[6] > i56[6] →^* TRUE)∧(i56[6] →^* i56[7])∧(i23[6] →^* i23[7])∧(i8[6] →^* i8[7]))

(7) -> (2), if ((i56[7] →^* i56[2])∧(i8[7] + -1 →^* i8[2])∧(i23[7] →^* i23[2]))

(7) -> (6), if ((i8[7] + -1 →^* i8[6])∧(i56[7] →^* i56[6])∧(i23[7] →^* i23[6]))

The set Q consists of the following terms:
Load1082(x0, x1, x2)
Cond_Load1082(TRUE, x0, x1, x2)
Load1003(x0, x1, x2)
Cond_Load1003(TRUE, x0, x1, x2)
Cond_Load10821(TRUE, x0, x1, x2)
Cond_Load10031(TRUE, x0, x1, x2)

(7) 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.

(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

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1082(i8[0], i23[0], i56[0]) → COND_LOAD1082(i23[0] > i56[0], i8[0], i23[0], i56[0])
(1): COND_LOAD1082(TRUE, i8[1], i23[1], i56[1]) → LOAD1082(i8[1], i23[1] + -1, i56[1])
(2): LOAD1003(i8[2], i23[2], i56[2]) → COND_LOAD1003(i23[2] > i56[2] && i8[2] > i56[2], i8[2], i23[2], i56[2])
(3): COND_LOAD1003(TRUE, i8[3], i23[3], i56[3]) → LOAD1082(i8[3], i23[3] + -1, i56[3])
(4): LOAD1082(i8[4], i23[4], i56[4]) → COND_LOAD10821(i23[4] <= i56[4], i8[4], i23[4], i56[4])
(5): COND_LOAD10821(TRUE, i8[5], i23[5], i56[5]) → LOAD1003(i8[5] + -1, i23[5], i56[5])
(6): LOAD1003(i8[6], i23[6], i56[6]) → COND_LOAD10031(i23[6] <= i56[6] && i8[6] > i56[6], i8[6], i23[6], i56[6])
(7): COND_LOAD10031(TRUE, i8[7], i23[7], i56[7]) → LOAD1003(i8[7] + -1, i23[7], i56[7])