Termination proof of /tmp/tmpRW2Qqh/Shuffle.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBC2FIG (⇐)

↳2 FIGraph

↳3 FIGtoITRSProof (⇐)

↳4 AND

    ↳5 ITRS

        ↳6 DuplicateArgsRemoverProof (⇔)

        ↳7 ITRS

        ↳8 ITRStoQTRSProof (⇔)

        ↳9 QTRS

        ↳10 DependencyPairsProof (⇔)

        ↳11 QDP

        ↳12 DependencyGraphProof (⇔)

        ↳13 QDP

        ↳14 UsableRulesProof (⇔)

        ↳15 QDP

        ↳16 QReductionProof (⇔)

        ↳17 QDP

        ↳18 Instantiation (⇔)

        ↳19 QDP

        ↳20 QDPOrderProof (⇔)

        ↳21 QDP

        ↳22 DependencyGraphProof (⇔)

        ↳23 QDP

        ↳24 QDPSizeChangeProof (⇔)

        ↳25 TRUE

    ↳26 ITRS

        ↳27 ITRSFilterProcessorProof (⇐)

        ↳28 ITRS

        ↳29 ITRStoIDPProof (⇔)

        ↳30 IDP

        ↳31 UsableRulesProof (⇔)

        ↳32 IDP

        ↳33 ItpfGraphProof (⇔)

        ↳34 IDP

        ↳35 IDPNonInfProof (⇐)

        ↳36 AND

            ↳37 IDP

                ↳38 IDependencyGraphProof (⇔)

                ↳39 TRUE

            ↳40 IDP

                ↳41 IDependencyGraphProof (⇔)

                ↳42 TRUE

(0) Obligation:

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

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

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


public class Shuffle{

  // adapted from [Walther, 94]
  public static void main(String[] args) {
    Random.args = args;
    IntList l = IntList.createIntList();
    IntList res = null;

    while (l != null) {

      res = new IntList(l.value, res);
      l = l.next;
      if (l != null) l = l.reverse();

    }

  }
}


class IntList {
  int value;
  IntList next;

  public IntList(int value, IntList next) {
    this.value = value;
    this.next = next;
  }


  public static IntList createIntList() {

    int i = Random.random();
    int j;

    IntList l = null;

    while (i > 0) {
      j = Random.random();
      l = new IntList(j, l);
      i--;
    }

    return l;
  }

  public IntList reverse() {

    IntList res = null;
    IntList l = this;

    while (l != null) {
      res = new IntList(l.value, res);
      l = l.next;

    }

    return res;
  }
}

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 303 nodes with 2 SCCs.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph to ITRS rules

(4) Complex Obligation (AND)

(5) 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:
Load2367(java.lang.Object(IntList(i185, java.lang.Object(IntList(o2144Field0, o2144Field1))))) → Load2801(java.lang.Object(IntList(o2144Field0, o2144Field1)), java.lang.Object(IntList(o2144Field0, o2144Field1)), NULL, java.lang.Object(IntList(o2144Field0, o2144Field1)))
JMP3331(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414) → Load2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414)
Load2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(o2363Field0, o2363Field1)), o2361, java.lang.Object(IntList(i252, o2414))) → Load2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414)
Load2801(java.lang.Object(IntList(i253, o2419)), java.lang.Object(IntList(i253, o2419)), o2361, java.lang.Object(IntList(i253, o2419))) → JMP3331(java.lang.Object(IntList(i253, o2419)), java.lang.Object(IntList(i253, o2419)), java.lang.Object(IntList(i253, o2361)), o2419)
Load2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(o2363Field0, o2363Field1)), o2361, NULL) → Load2367(o2361)
Load2367(java.lang.Object(IntList(i185, NULL))) → Load2367(NULL)
The set Q consists of the following terms:
Load2367(java.lang.Object(IntList(x0, java.lang.Object(IntList(x1, x2)))))
JMP3331(java.lang.Object(IntList(x0, x1)), java.lang.Object(IntList(x0, x1)), java.lang.Object(IntList(x2, x3)), x4)
Load2801(java.lang.Object(IntList(x0, x1)), java.lang.Object(IntList(x0, x1)), x2, java.lang.Object(IntList(x3, x4)))
Load2801(java.lang.Object(IntList(x0, x1)), java.lang.Object(IntList(x0, x1)), x2, NULL)
Load2367(java.lang.Object(IntList(x0, NULL)))

(6) DuplicateArgsRemoverProof (EQUIVALENT transformation)

Some arguments are removed because they only appear as duplicates.
We removed arguments according to the following replacements:

Load2801(x1, x2, x3, x4) → Load2801(x2, x3, x4)
JMP3331(x1, x2, x3, x4) → JMP3331(x2, x3, x4)

(7) 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:
Load2367(java.lang.Object(IntList(i185, java.lang.Object(IntList(o2144Field0, o2144Field1))))) → Load2801(java.lang.Object(IntList(o2144Field0, o2144Field1)), NULL, java.lang.Object(IntList(o2144Field0, o2144Field1)))
JMP3331(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414) → Load2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414)
Load2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), o2361, java.lang.Object(IntList(i252, o2414))) → Load2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414)
Load2801(java.lang.Object(IntList(i253, o2419)), o2361, java.lang.Object(IntList(i253, o2419))) → JMP3331(java.lang.Object(IntList(i253, o2419)), java.lang.Object(IntList(i253, o2361)), o2419)
Load2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), o2361, NULL) → Load2367(o2361)
Load2367(java.lang.Object(IntList(i185, NULL))) → Load2367(NULL)
The set Q consists of the following terms:
Load2367(java.lang.Object(IntList(x0, java.lang.Object(IntList(x1, x2)))))
JMP3331(java.lang.Object(IntList(x0, x1)), java.lang.Object(IntList(x2, x3)), x4)
Load2801(java.lang.Object(IntList(x0, x1)), x2, java.lang.Object(IntList(x3, x4)))
Load2801(java.lang.Object(IntList(x0, x1)), x2, NULL)
Load2367(java.lang.Object(IntList(x0, NULL)))

(8) ITRStoQTRSProof (EQUIVALENT transformation)

Represented integers and predefined function symbols by Terms

(9) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

Load2367(java.lang.Object(IntList(i185, java.lang.Object(IntList(o2144Field0, o2144Field1))))) → Load2801(java.lang.Object(IntList(o2144Field0, o2144Field1)), NULL, java.lang.Object(IntList(o2144Field0, o2144Field1)))
JMP3331(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414) → Load2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414)
Load2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), o2361, java.lang.Object(IntList(i252, o2414))) → Load2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414)
Load2801(java.lang.Object(IntList(i253, o2419)), o2361, java.lang.Object(IntList(i253, o2419))) → JMP3331(java.lang.Object(IntList(i253, o2419)), java.lang.Object(IntList(i253, o2361)), o2419)
Load2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), o2361, NULL) → Load2367(o2361)
Load2367(java.lang.Object(IntList(i185, NULL))) → Load2367(NULL)

The set Q consists of the following terms:

Load2367(java.lang.Object(IntList(x0, java.lang.Object(IntList(x1, x2)))))
JMP3331(java.lang.Object(IntList(x0, x1)), java.lang.Object(IntList(x2, x3)), x4)
Load2801(java.lang.Object(IntList(x0, x1)), x2, java.lang.Object(IntList(x3, x4)))
Load2801(java.lang.Object(IntList(x0, x1)), x2, NULL)
Load2367(java.lang.Object(IntList(x0, NULL)))

(10) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LOAD2367(java.lang.Object(IntList(i185, java.lang.Object(IntList(o2144Field0, o2144Field1))))) → LOAD2801(java.lang.Object(IntList(o2144Field0, o2144Field1)), NULL, java.lang.Object(IntList(o2144Field0, o2144Field1)))
JMP3331¹(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414) → LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414)
LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), o2361, java.lang.Object(IntList(i252, o2414))) → LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414)
LOAD2801(java.lang.Object(IntList(i253, o2419)), o2361, java.lang.Object(IntList(i253, o2419))) → JMP3331¹(java.lang.Object(IntList(i253, o2419)), java.lang.Object(IntList(i253, o2361)), o2419)
LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), o2361, NULL) → LOAD2367(o2361)
LOAD2367(java.lang.Object(IntList(i185, NULL))) → LOAD2367(NULL)

The TRS R consists of the following rules:

Load2367(java.lang.Object(IntList(i185, java.lang.Object(IntList(o2144Field0, o2144Field1))))) → Load2801(java.lang.Object(IntList(o2144Field0, o2144Field1)), NULL, java.lang.Object(IntList(o2144Field0, o2144Field1)))
JMP3331(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414) → Load2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414)
Load2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), o2361, java.lang.Object(IntList(i252, o2414))) → Load2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414)
Load2801(java.lang.Object(IntList(i253, o2419)), o2361, java.lang.Object(IntList(i253, o2419))) → JMP3331(java.lang.Object(IntList(i253, o2419)), java.lang.Object(IntList(i253, o2361)), o2419)
Load2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), o2361, NULL) → Load2367(o2361)
Load2367(java.lang.Object(IntList(i185, NULL))) → Load2367(NULL)

The set Q consists of the following terms:

Load2367(java.lang.Object(IntList(x0, java.lang.Object(IntList(x1, x2)))))
JMP3331(java.lang.Object(IntList(x0, x1)), java.lang.Object(IntList(x2, x3)), x4)
Load2801(java.lang.Object(IntList(x0, x1)), x2, java.lang.Object(IntList(x3, x4)))
Load2801(java.lang.Object(IntList(x0, x1)), x2, NULL)
Load2367(java.lang.Object(IntList(x0, NULL)))

We have to consider all minimal (P,Q,R)-chains.

(12) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), o2361, java.lang.Object(IntList(i252, o2414))) → LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414)
LOAD2801(java.lang.Object(IntList(i253, o2419)), o2361, java.lang.Object(IntList(i253, o2419))) → JMP3331¹(java.lang.Object(IntList(i253, o2419)), java.lang.Object(IntList(i253, o2361)), o2419)
JMP3331¹(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414) → LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414)
LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), o2361, NULL) → LOAD2367(o2361)
LOAD2367(java.lang.Object(IntList(i185, java.lang.Object(IntList(o2144Field0, o2144Field1))))) → LOAD2801(java.lang.Object(IntList(o2144Field0, o2144Field1)), NULL, java.lang.Object(IntList(o2144Field0, o2144Field1)))

The TRS R consists of the following rules:

Load2367(java.lang.Object(IntList(i185, java.lang.Object(IntList(o2144Field0, o2144Field1))))) → Load2801(java.lang.Object(IntList(o2144Field0, o2144Field1)), NULL, java.lang.Object(IntList(o2144Field0, o2144Field1)))
JMP3331(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414) → Load2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414)
Load2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), o2361, java.lang.Object(IntList(i252, o2414))) → Load2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414)
Load2801(java.lang.Object(IntList(i253, o2419)), o2361, java.lang.Object(IntList(i253, o2419))) → JMP3331(java.lang.Object(IntList(i253, o2419)), java.lang.Object(IntList(i253, o2361)), o2419)
Load2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), o2361, NULL) → Load2367(o2361)
Load2367(java.lang.Object(IntList(i185, NULL))) → Load2367(NULL)

The set Q consists of the following terms:

Load2367(java.lang.Object(IntList(x0, java.lang.Object(IntList(x1, x2)))))
JMP3331(java.lang.Object(IntList(x0, x1)), java.lang.Object(IntList(x2, x3)), x4)
Load2801(java.lang.Object(IntList(x0, x1)), x2, java.lang.Object(IntList(x3, x4)))
Load2801(java.lang.Object(IntList(x0, x1)), x2, NULL)
Load2367(java.lang.Object(IntList(x0, NULL)))

We have to consider all minimal (P,Q,R)-chains.

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

(15) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), o2361, java.lang.Object(IntList(i252, o2414))) → LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414)
LOAD2801(java.lang.Object(IntList(i253, o2419)), o2361, java.lang.Object(IntList(i253, o2419))) → JMP3331¹(java.lang.Object(IntList(i253, o2419)), java.lang.Object(IntList(i253, o2361)), o2419)
JMP3331¹(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414) → LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414)
LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), o2361, NULL) → LOAD2367(o2361)
LOAD2367(java.lang.Object(IntList(i185, java.lang.Object(IntList(o2144Field0, o2144Field1))))) → LOAD2801(java.lang.Object(IntList(o2144Field0, o2144Field1)), NULL, java.lang.Object(IntList(o2144Field0, o2144Field1)))

R is empty.
The set Q consists of the following terms:

Load2367(java.lang.Object(IntList(x0, java.lang.Object(IntList(x1, x2)))))
JMP3331(java.lang.Object(IntList(x0, x1)), java.lang.Object(IntList(x2, x3)), x4)
Load2801(java.lang.Object(IntList(x0, x1)), x2, java.lang.Object(IntList(x3, x4)))
Load2801(java.lang.Object(IntList(x0, x1)), x2, NULL)
Load2367(java.lang.Object(IntList(x0, NULL)))

We have to consider all minimal (P,Q,R)-chains.

(16) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

Load2367(java.lang.Object(IntList(x0, java.lang.Object(IntList(x1, x2)))))
JMP3331(java.lang.Object(IntList(x0, x1)), java.lang.Object(IntList(x2, x3)), x4)
Load2801(java.lang.Object(IntList(x0, x1)), x2, java.lang.Object(IntList(x3, x4)))
Load2801(java.lang.Object(IntList(x0, x1)), x2, NULL)
Load2367(java.lang.Object(IntList(x0, NULL)))

(17) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), o2361, java.lang.Object(IntList(i252, o2414))) → LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414)
LOAD2801(java.lang.Object(IntList(i253, o2419)), o2361, java.lang.Object(IntList(i253, o2419))) → JMP3331¹(java.lang.Object(IntList(i253, o2419)), java.lang.Object(IntList(i253, o2361)), o2419)
JMP3331¹(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414) → LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414)
LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), o2361, NULL) → LOAD2367(o2361)
LOAD2367(java.lang.Object(IntList(i185, java.lang.Object(IntList(o2144Field0, o2144Field1))))) → LOAD2801(java.lang.Object(IntList(o2144Field0, o2144Field1)), NULL, java.lang.Object(IntList(o2144Field0, o2144Field1)))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(18) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule JMP3331¹(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414) → LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414) we obtained the following new rules [LPAR04]:

JMP3331¹(java.lang.Object(IntList(z0, z1)), java.lang.Object(IntList(z0, z2)), z1) → LOAD2801(java.lang.Object(IntList(z0, z1)), java.lang.Object(IntList(z0, z2)), z1)

(19) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), o2361, java.lang.Object(IntList(i252, o2414))) → LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414)
LOAD2801(java.lang.Object(IntList(i253, o2419)), o2361, java.lang.Object(IntList(i253, o2419))) → JMP3331¹(java.lang.Object(IntList(i253, o2419)), java.lang.Object(IntList(i253, o2361)), o2419)
LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), o2361, NULL) → LOAD2367(o2361)
LOAD2367(java.lang.Object(IntList(i185, java.lang.Object(IntList(o2144Field0, o2144Field1))))) → LOAD2801(java.lang.Object(IntList(o2144Field0, o2144Field1)), NULL, java.lang.Object(IntList(o2144Field0, o2144Field1)))
JMP3331¹(java.lang.Object(IntList(z0, z1)), java.lang.Object(IntList(z0, z2)), z1) → LOAD2801(java.lang.Object(IntList(z0, z1)), java.lang.Object(IntList(z0, z2)), z1)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(20) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

LOAD2367(java.lang.Object(IntList(i185, java.lang.Object(IntList(o2144Field0, o2144Field1))))) → LOAD2801(java.lang.Object(IntList(o2144Field0, o2144Field1)), NULL, java.lang.Object(IntList(o2144Field0, o2144Field1)))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(IntList(x₁, x₂)) = x₂
POL(JMP3331¹(x₁, x₂, x₃)) = x₂ + x₃
POL(LOAD2367(x₁)) = x₁
POL(LOAD2801(x₁, x₂, x₃)) = x₂ + x₃
POL(NULL) = 0
POL(java.lang.Object(x₁)) = 1 + x₁

The following usable rules [FROCOS05] were oriented: none

(21) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), o2361, java.lang.Object(IntList(i252, o2414))) → LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414)
LOAD2801(java.lang.Object(IntList(i253, o2419)), o2361, java.lang.Object(IntList(i253, o2419))) → JMP3331¹(java.lang.Object(IntList(i253, o2419)), java.lang.Object(IntList(i253, o2361)), o2419)
LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), o2361, NULL) → LOAD2367(o2361)
JMP3331¹(java.lang.Object(IntList(z0, z1)), java.lang.Object(IntList(z0, z2)), z1) → LOAD2801(java.lang.Object(IntList(z0, z1)), java.lang.Object(IntList(z0, z2)), z1)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(22) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(23) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LOAD2801(java.lang.Object(IntList(i253, o2419)), o2361, java.lang.Object(IntList(i253, o2419))) → JMP3331¹(java.lang.Object(IntList(i253, o2419)), java.lang.Object(IntList(i253, o2361)), o2419)
JMP3331¹(java.lang.Object(IntList(z0, z1)), java.lang.Object(IntList(z0, z2)), z1) → LOAD2801(java.lang.Object(IntList(z0, z1)), java.lang.Object(IntList(z0, z2)), z1)
LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), o2361, java.lang.Object(IntList(i252, o2414))) → LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(24) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

JMP3331¹(java.lang.Object(IntList(z0, z1)), java.lang.Object(IntList(z0, z2)), z1) → LOAD2801(java.lang.Object(IntList(z0, z1)), java.lang.Object(IntList(z0, z2)), z1)
The graph contains the following edges 1 >= 1, 2 >= 2, 1 > 3, 3 >= 3
LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), o2361, java.lang.Object(IntList(i252, o2414))) → LOAD2801(java.lang.Object(IntList(o2363Field0, o2363Field1)), java.lang.Object(IntList(i252, o2361)), o2414)
The graph contains the following edges 1 >= 1, 3 > 3
LOAD2801(java.lang.Object(IntList(i253, o2419)), o2361, java.lang.Object(IntList(i253, o2419))) → JMP3331¹(java.lang.Object(IntList(i253, o2419)), java.lang.Object(IntList(i253, o2361)), o2419)
The graph contains the following edges 1 >= 1, 3 >= 1, 1 > 3, 3 > 3

(25) TRUE

(26) 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:
Load1479(java.lang.Object(ARRAY(i2, a1508data)), i54, i56) → Load1479ARR1(java.lang.Object(ARRAY(i2, a1508data)), i54, i56, java.lang.Object(java.lang.String(i78)))
Load1479ARR1(java.lang.Object(ARRAY(i2, a1508data)), i54, i56, java.lang.Object(java.lang.String(i78))) → Cond_Load1479ARR1(i54 > 0 && i54 < i2 && i56 > 0 && i54 + 1 > 0, java.lang.Object(ARRAY(i2, a1508data)), i54, i56, java.lang.Object(java.lang.String(i78)))
Cond_Load1479ARR1(TRUE, java.lang.Object(ARRAY(i2, a1508data)), i54, i56, java.lang.Object(java.lang.String(i78))) → Load1479(java.lang.Object(ARRAY(i2, a1508data)), i54 + 1, i56 + -1)
The set Q consists of the following terms:
Load1479(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load1479ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))
Cond_Load1479ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4)))

(27) ITRSFilterProcessorProof (SOUND transformation)

We filter according the heuristic IdpCand1ShapeHeuristic
We removed arguments according to the following replacements:

Load1479ARR1(x1, x2, x3, x4) → Load1479ARR1(x1, x2, x3)
java.lang.String(x1) → java.lang.String
Cond_Load1479ARR1(x1, x2, x3, x4, x5) → Cond_Load1479ARR1(x1, x2, x3, x4)

(28) 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:
Load1479(java.lang.Object(ARRAY(i2, a1508data)), i54, i56) → Load1479ARR1(java.lang.Object(ARRAY(i2, a1508data)), i54, i56)
Load1479ARR1(java.lang.Object(ARRAY(i2, a1508data)), i54, i56) → Cond_Load1479ARR1(i54 > 0 && i54 < i2 && i56 > 0 && i54 + 1 > 0, java.lang.Object(ARRAY(i2, a1508data)), i54, i56)
Cond_Load1479ARR1(TRUE, java.lang.Object(ARRAY(i2, a1508data)), i54, i56) → Load1479(java.lang.Object(ARRAY(i2, a1508data)), i54 + 1, i56 + -1)
The set Q consists of the following terms:
Load1479(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load1479ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load1479ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)

(29) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(30) 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:

Boolean, Integer

The ITRS R consists of the following rules:
Load1479(java.lang.Object(ARRAY(i2, a1508data)), i54, i56) → Load1479ARR1(java.lang.Object(ARRAY(i2, a1508data)), i54, i56)
Load1479ARR1(java.lang.Object(ARRAY(i2, a1508data)), i54, i56) → Cond_Load1479ARR1(i54 > 0 && i54 < i2 && i56 > 0 && i54 + 1 > 0, java.lang.Object(ARRAY(i2, a1508data)), i54, i56)
Cond_Load1479ARR1(TRUE, java.lang.Object(ARRAY(i2, a1508data)), i54, i56) → Load1479(java.lang.Object(ARRAY(i2, a1508data)), i54 + 1, i56 + -1)

The integer pair graph contains the following rules and edges:
(0): LOAD1479(java.lang.Object(ARRAY(i2[0], a1508data[0])), i54[0], i56[0]) → LOAD1479ARR1(java.lang.Object(ARRAY(i2[0], a1508data[0])), i54[0], i56[0])
(1): LOAD1479ARR1(java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1]) → COND_LOAD1479ARR1(i54[1] > 0 && i54[1] < i2[1] && i56[1] > 0 && i54[1] + 1 > 0, java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1])
(2): COND_LOAD1479ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a1508data[2])), i54[2], i56[2]) → LOAD1479(java.lang.Object(ARRAY(i2[2], a1508data[2])), i54[2] + 1, i56[2] + -1)

(0) -> (1), if ((java.lang.Object(ARRAY(i2[0], a1508data[0])) →^* java.lang.Object(ARRAY(i2[1], a1508data[1])))∧(i56[0] →^* i56[1])∧(i54[0] →^* i54[1]))

(1) -> (2), if ((i54[1] > 0 && i54[1] < i2[1] && i56[1] > 0 && i54[1] + 1 > 0 →^* TRUE)∧(i56[1] →^* i56[2])∧(java.lang.Object(ARRAY(i2[1], a1508data[1])) →^* java.lang.Object(ARRAY(i2[2], a1508data[2])))∧(i54[1] →^* i54[2]))

(2) -> (0), if ((i56[2] + -1 →^* i56[0])∧(java.lang.Object(ARRAY(i2[2], a1508data[2])) →^* java.lang.Object(ARRAY(i2[0], a1508data[0])))∧(i54[2] + 1 →^* i54[0]))

The set Q consists of the following terms:
Load1479(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load1479ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load1479ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)

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

(32) 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:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1479(java.lang.Object(ARRAY(i2[0], a1508data[0])), i54[0], i56[0]) → LOAD1479ARR1(java.lang.Object(ARRAY(i2[0], a1508data[0])), i54[0], i56[0])
(1): LOAD1479ARR1(java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1]) → COND_LOAD1479ARR1(i54[1] > 0 && i54[1] < i2[1] && i56[1] > 0 && i54[1] + 1 > 0, java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1])
(2): COND_LOAD1479ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a1508data[2])), i54[2], i56[2]) → LOAD1479(java.lang.Object(ARRAY(i2[2], a1508data[2])), i54[2] + 1, i56[2] + -1)

(0) -> (1), if ((java.lang.Object(ARRAY(i2[0], a1508data[0])) →^* java.lang.Object(ARRAY(i2[1], a1508data[1])))∧(i56[0] →^* i56[1])∧(i54[0] →^* i54[1]))

(2) -> (0), if ((i56[2] + -1 →^* i56[0])∧(java.lang.Object(ARRAY(i2[2], a1508data[2])) →^* java.lang.Object(ARRAY(i2[0], a1508data[0])))∧(i54[2] + 1 →^* i54[0]))

(33) ItpfGraphProof (EQUIVALENT transformation)

Applied rule ItpfICap [ICap]

(34) 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:

Boolean, Integer

(0) -> (1), if (((i2[0] →^* i2[1])∧(a1508data[0] →^* a1508data[1]))∧(i56[0] →^* i56[1])∧(i54[0] →^* i54[1]))

(1) -> (2), if ((i54[1] > 0 && i54[1] < i2[1] && i56[1] > 0 && i54[1] + 1 > 0 →^* TRUE)∧(i56[1] →^* i56[2])∧((i2[1] →^* i2[2])∧(a1508data[1] →^* a1508data[2]))∧(i54[1] →^* i54[2]))

(2) -> (0), if ((i56[2] + -1 →^* i56[0])∧((i2[2] →^* i2[0])∧(a1508data[2] →^* a1508data[0]))∧(i54[2] + 1 →^* i54[0]))

(35) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair LOAD1479(java.lang.Object(ARRAY(i2, a1508data)), i54, i56) → LOAD1479ARR1(java.lang.Object(ARRAY(i2, a1508data)), i54, i56) the following chains were created:

We consider the chain LOAD1479(java.lang.Object(ARRAY(i2[0], a1508data[0])), i54[0], i56[0]) → LOAD1479ARR1(java.lang.Object(ARRAY(i2[0], a1508data[0])), i54[0], i56[0]), LOAD1479ARR1(java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1]) → COND_LOAD1479ARR1(&&(&&(&&(>(i54[1], 0), <(i54[1], i2[1])), >(i56[1], 0)), >(+(i54[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1]) which results in the following constraint:
(1)    (i2[0]=i2[1]∧a1508data[0]=a1508data[1]∧i56[0]=i56[1]∧i54[0]=i54[1] ⇒ LOAD1479(java.lang.Object(ARRAY(i2[0], a1508data[0])), i54[0], i56[0])≥NonInfC∧LOAD1479(java.lang.Object(ARRAY(i2[0], a1508data[0])), i54[0], i56[0])≥LOAD1479ARR1(java.lang.Object(ARRAY(i2[0], a1508data[0])), i54[0], i56[0])∧(U^Increasing(LOAD1479ARR1(java.lang.Object(ARRAY(i2[0], a1508data[0])), i54[0], i56[0])), ≥))

We simplified constraint (1) using rule (IV) which results in the following new constraint:
(2)    (LOAD1479(java.lang.Object(ARRAY(i2[0], a1508data[0])), i54[0], i56[0])≥NonInfC∧LOAD1479(java.lang.Object(ARRAY(i2[0], a1508data[0])), i54[0], i56[0])≥LOAD1479ARR1(java.lang.Object(ARRAY(i2[0], a1508data[0])), i54[0], i56[0])∧(U^Increasing(LOAD1479ARR1(java.lang.Object(ARRAY(i2[0], a1508data[0])), i54[0], i56[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    ((U^Increasing(LOAD1479ARR1(java.lang.Object(ARRAY(i2[0], a1508data[0])), i54[0], i56[0])), ≥)∧[(-1)bso_16] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    ((U^Increasing(LOAD1479ARR1(java.lang.Object(ARRAY(i2[0], a1508data[0])), i54[0], i56[0])), ≥)∧[(-1)bso_16] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    ((U^Increasing(LOAD1479ARR1(java.lang.Object(ARRAY(i2[0], a1508data[0])), i54[0], i56[0])), ≥)∧[(-1)bso_16] ≥ 0)

We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(6)    ((U^Increasing(LOAD1479ARR1(java.lang.Object(ARRAY(i2[0], a1508data[0])), i54[0], i56[0])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_16] ≥ 0)

For Pair LOAD1479ARR1(java.lang.Object(ARRAY(i2, a1508data)), i54, i56) → COND_LOAD1479ARR1(&&(&&(&&(>(i54, 0), <(i54, i2)), >(i56, 0)), >(+(i54, 1), 0)), java.lang.Object(ARRAY(i2, a1508data)), i54, i56) the following chains were created:

We consider the chain LOAD1479ARR1(java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1]) → COND_LOAD1479ARR1(&&(&&(&&(>(i54[1], 0), <(i54[1], i2[1])), >(i56[1], 0)), >(+(i54[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1]), COND_LOAD1479ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a1508data[2])), i54[2], i56[2]) → LOAD1479(java.lang.Object(ARRAY(i2[2], a1508data[2])), +(i54[2], 1), +(i56[2], -1)) which results in the following constraint:
(7)    (&&(&&(&&(>(i54[1], 0), <(i54[1], i2[1])), >(i56[1], 0)), >(+(i54[1], 1), 0))=TRUE∧i56[1]=i56[2]∧i2[1]=i2[2]∧a1508data[1]=a1508data[2]∧i54[1]=i54[2] ⇒ LOAD1479ARR1(java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1])≥NonInfC∧LOAD1479ARR1(java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1])≥COND_LOAD1479ARR1(&&(&&(&&(>(i54[1], 0), <(i54[1], i2[1])), >(i56[1], 0)), >(+(i54[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1])∧(U^Increasing(COND_LOAD1479ARR1(&&(&&(&&(>(i54[1], 0), <(i54[1], i2[1])), >(i56[1], 0)), >(+(i54[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1])), ≥))

We simplified constraint (7) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
(8)    (>(+(i54[1], 1), 0)=TRUE∧>(i56[1], 0)=TRUE∧>(i54[1], 0)=TRUE∧<(i54[1], i2[1])=TRUE ⇒ LOAD1479ARR1(java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1])≥NonInfC∧LOAD1479ARR1(java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1])≥COND_LOAD1479ARR1(&&(&&(&&(>(i54[1], 0), <(i54[1], i2[1])), >(i56[1], 0)), >(+(i54[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1])∧(U^Increasing(COND_LOAD1479ARR1(&&(&&(&&(>(i54[1], 0), <(i54[1], i2[1])), >(i56[1], 0)), >(+(i54[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1])), ≥))

We simplified constraint (8) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(9)    (i54[1] ≥ 0∧i56[1] + [-1] ≥ 0∧i54[1] + [-1] ≥ 0∧i2[1] + [-1] + [-1]i54[1] ≥ 0 ⇒ (U^Increasing(COND_LOAD1479ARR1(&&(&&(&&(>(i54[1], 0), <(i54[1], i2[1])), >(i56[1], 0)), >(+(i54[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1])), ≥)∧[(2)bni_17 + (-1)Bound*bni_17] + [bni_17]i56[1] + [(-1)bni_17]i54[1] + [bni_17]i2[1] ≥ 0∧[(-1)bso_18] ≥ 0)

We simplified constraint (9) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(10)    (i54[1] ≥ 0∧i56[1] + [-1] ≥ 0∧i54[1] + [-1] ≥ 0∧i2[1] + [-1] + [-1]i54[1] ≥ 0 ⇒ (U^Increasing(COND_LOAD1479ARR1(&&(&&(&&(>(i54[1], 0), <(i54[1], i2[1])), >(i56[1], 0)), >(+(i54[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1])), ≥)∧[(2)bni_17 + (-1)Bound*bni_17] + [bni_17]i56[1] + [(-1)bni_17]i54[1] + [bni_17]i2[1] ≥ 0∧[(-1)bso_18] ≥ 0)

We simplified constraint (10) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(11)    (i54[1] ≥ 0∧i56[1] + [-1] ≥ 0∧i54[1] + [-1] ≥ 0∧i2[1] + [-1] + [-1]i54[1] ≥ 0 ⇒ (U^Increasing(COND_LOAD1479ARR1(&&(&&(&&(>(i54[1], 0), <(i54[1], i2[1])), >(i56[1], 0)), >(+(i54[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1])), ≥)∧[(2)bni_17 + (-1)Bound*bni_17] + [bni_17]i56[1] + [(-1)bni_17]i54[1] + [bni_17]i2[1] ≥ 0∧[(-1)bso_18] ≥ 0)

We simplified constraint (11) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(12)    (i54[1] ≥ 0∧i56[1] + [-1] ≥ 0∧i54[1] + [-1] ≥ 0∧i2[1] + [-1] + [-1]i54[1] ≥ 0 ⇒ (U^Increasing(COND_LOAD1479ARR1(&&(&&(&&(>(i54[1], 0), <(i54[1], i2[1])), >(i56[1], 0)), >(+(i54[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1])), ≥)∧0 = 0∧[(2)bni_17 + (-1)Bound*bni_17] + [bni_17]i56[1] + [(-1)bni_17]i54[1] + [bni_17]i2[1] ≥ 0∧0 = 0∧[(-1)bso_18] ≥ 0)

We simplified constraint (12) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(13)    ([1] + i54[1] ≥ 0∧i56[1] + [-1] ≥ 0∧i54[1] ≥ 0∧i2[1] + [-2] + [-1]i54[1] ≥ 0 ⇒ (U^Increasing(COND_LOAD1479ARR1(&&(&&(&&(>(i54[1], 0), <(i54[1], i2[1])), >(i56[1], 0)), >(+(i54[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1])), ≥)∧0 = 0∧[bni_17 + (-1)Bound*bni_17] + [bni_17]i56[1] + [(-1)bni_17]i54[1] + [bni_17]i2[1] ≥ 0∧0 = 0∧[(-1)bso_18] ≥ 0)

We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(14)    ([1] + i54[1] ≥ 0∧i56[1] ≥ 0∧i54[1] ≥ 0∧i2[1] + [-2] + [-1]i54[1] ≥ 0 ⇒ (U^Increasing(COND_LOAD1479ARR1(&&(&&(&&(>(i54[1], 0), <(i54[1], i2[1])), >(i56[1], 0)), >(+(i54[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1])), ≥)∧0 = 0∧[(2)bni_17 + (-1)Bound*bni_17] + [bni_17]i56[1] + [(-1)bni_17]i54[1] + [bni_17]i2[1] ≥ 0∧0 = 0∧[(-1)bso_18] ≥ 0)

We simplified constraint (14) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(15)    ([1] + i54[1] ≥ 0∧i56[1] ≥ 0∧i54[1] ≥ 0∧i2[1] ≥ 0 ⇒ (U^Increasing(COND_LOAD1479ARR1(&&(&&(&&(>(i54[1], 0), <(i54[1], i2[1])), >(i56[1], 0)), >(+(i54[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1])), ≥)∧0 = 0∧[(4)bni_17 + (-1)Bound*bni_17] + [bni_17]i56[1] + [bni_17]i2[1] ≥ 0∧0 = 0∧[(-1)bso_18] ≥ 0)

For Pair COND_LOAD1479ARR1(TRUE, java.lang.Object(ARRAY(i2, a1508data)), i54, i56) → LOAD1479(java.lang.Object(ARRAY(i2, a1508data)), +(i54, 1), +(i56, -1)) the following chains were created:

We consider the chain COND_LOAD1479ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a1508data[2])), i54[2], i56[2]) → LOAD1479(java.lang.Object(ARRAY(i2[2], a1508data[2])), +(i54[2], 1), +(i56[2], -1)) which results in the following constraint:
(16)    (COND_LOAD1479ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a1508data[2])), i54[2], i56[2])≥NonInfC∧COND_LOAD1479ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a1508data[2])), i54[2], i56[2])≥LOAD1479(java.lang.Object(ARRAY(i2[2], a1508data[2])), +(i54[2], 1), +(i56[2], -1))∧(U^Increasing(LOAD1479(java.lang.Object(ARRAY(i2[2], a1508data[2])), +(i54[2], 1), +(i56[2], -1))), ≥))

We simplified constraint (16) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(17)    ((U^Increasing(LOAD1479(java.lang.Object(ARRAY(i2[2], a1508data[2])), +(i54[2], 1), +(i56[2], -1))), ≥)∧[2 + (-1)bso_20] ≥ 0)

We simplified constraint (17) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(18)    ((U^Increasing(LOAD1479(java.lang.Object(ARRAY(i2[2], a1508data[2])), +(i54[2], 1), +(i56[2], -1))), ≥)∧[2 + (-1)bso_20] ≥ 0)

We simplified constraint (18) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(19)    ((U^Increasing(LOAD1479(java.lang.Object(ARRAY(i2[2], a1508data[2])), +(i54[2], 1), +(i56[2], -1))), ≥)∧[2 + (-1)bso_20] ≥ 0)

We simplified constraint (19) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(20)    ((U^Increasing(LOAD1479(java.lang.Object(ARRAY(i2[2], a1508data[2])), +(i54[2], 1), +(i56[2], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[2 + (-1)bso_20] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

LOAD1479(java.lang.Object(ARRAY(i2, a1508data)), i54, i56) → LOAD1479ARR1(java.lang.Object(ARRAY(i2, a1508data)), i54, i56)
- ((U^Increasing(LOAD1479ARR1(java.lang.Object(ARRAY(i2[0], a1508data[0])), i54[0], i56[0])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_16] ≥ 0)
LOAD1479ARR1(java.lang.Object(ARRAY(i2, a1508data)), i54, i56) → COND_LOAD1479ARR1(&&(&&(&&(>(i54, 0), <(i54, i2)), >(i56, 0)), >(+(i54, 1), 0)), java.lang.Object(ARRAY(i2, a1508data)), i54, i56)
- ([1] + i54[1] ≥ 0∧i56[1] ≥ 0∧i54[1] ≥ 0∧i2[1] ≥ 0 ⇒ (U^Increasing(COND_LOAD1479ARR1(&&(&&(&&(>(i54[1], 0), <(i54[1], i2[1])), >(i56[1], 0)), >(+(i54[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1])), ≥)∧0 = 0∧[(4)bni_17 + (-1)Bound*bni_17] + [bni_17]i56[1] + [bni_17]i2[1] ≥ 0∧0 = 0∧[(-1)bso_18] ≥ 0)
COND_LOAD1479ARR1(TRUE, java.lang.Object(ARRAY(i2, a1508data)), i54, i56) → LOAD1479(java.lang.Object(ARRAY(i2, a1508data)), +(i54, 1), +(i56, -1))
- ((U^Increasing(LOAD1479(java.lang.Object(ARRAY(i2[2], a1508data[2])), +(i54[2], 1), +(i56[2], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[2 + (-1)bso_20] ≥ 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(LOAD1479(x₁, x₂, x₃)) = [1] + x₃ + [-1]x₂ + [-1]x₁
POL(java.lang.Object(x₁)) = x₁
POL(ARRAY(x₁, x₂)) = [-1] + [-1]x₁
POL(LOAD1479ARR1(x₁, x₂, x₃)) = [1] + x₃ + [-1]x₂ + [-1]x₁
POL(COND_LOAD1479ARR1(x₁, x₂, x₃, x₄)) = [1] + x₄ + [-1]x₃ + [-1]x₂
POL(&&(x₁, x₂)) = [-1]
POL(>(x₁, x₂)) = [-1]
POL(0) = 0
POL(<(x₁, x₂)) = [-1]
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(-1) = [-1]

The following pairs are in P_>:

COND_LOAD1479ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a1508data[2])), i54[2], i56[2]) → LOAD1479(java.lang.Object(ARRAY(i2[2], a1508data[2])), +(i54[2], 1), +(i56[2], -1))

The following pairs are in P_bound:

LOAD1479ARR1(java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1]) → COND_LOAD1479ARR1(&&(&&(&&(>(i54[1], 0), <(i54[1], i2[1])), >(i56[1], 0)), >(+(i54[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1])

The following pairs are in P_≥:

LOAD1479(java.lang.Object(ARRAY(i2[0], a1508data[0])), i54[0], i56[0]) → LOAD1479ARR1(java.lang.Object(ARRAY(i2[0], a1508data[0])), i54[0], i56[0])
LOAD1479ARR1(java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1]) → COND_LOAD1479ARR1(&&(&&(&&(>(i54[1], 0), <(i54[1], i2[1])), >(i56[1], 0)), >(+(i54[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a1508data[1])), i54[1], i56[1])

There are no usable rules.

(36) Complex Obligation (AND)

(37) 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:

Boolean, Integer

(0) -> (1), if (((i2[0] →^* i2[1])∧(a1508data[0] →^* a1508data[1]))∧(i56[0] →^* i56[1])∧(i54[0] →^* i54[1]))

(38) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(39) TRUE

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

(2) -> (0), if ((i56[2] + -1 →^* i56[0])∧((i2[2] →^* i2[0])∧(a1508data[2] →^* a1508data[0]))∧(i54[2] + 1 →^* i54[0]))

(41) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(0) Obligation:

(1) JBC2FIG (SOUND transformation)

(2) Obligation:

(3) FIGtoITRSProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) DuplicateArgsRemoverProof (EQUIVALENT transformation)

(7) Obligation:

(8) ITRStoQTRSProof (EQUIVALENT transformation)

(9) Obligation:

(10) DependencyPairsProof (EQUIVALENT transformation)

(11) Obligation:

(12) DependencyGraphProof (EQUIVALENT transformation)

(13) Obligation:

(14) UsableRulesProof (EQUIVALENT transformation)

(15) Obligation:

(16) QReductionProof (EQUIVALENT transformation)

(17) Obligation:

(18) Instantiation (EQUIVALENT transformation)

(19) Obligation:

(20) QDPOrderProof (EQUIVALENT transformation)

(21) Obligation:

(22) DependencyGraphProof (EQUIVALENT transformation)

(23) Obligation:

(24) QDPSizeChangeProof (EQUIVALENT transformation)

(25) TRUE

(26) Obligation:

(27) ITRSFilterProcessorProof (SOUND transformation)

(28) Obligation:

(29) ITRStoIDPProof (EQUIVALENT transformation)

(30) Obligation:

(31) UsableRulesProof (EQUIVALENT transformation)

(32) Obligation:

(33) ItpfGraphProof (EQUIVALENT transformation)

(34) Obligation:

(35) IDPNonInfProof (SOUND transformation)

(36) Complex Obligation (AND)

(37) Obligation:

(38) IDependencyGraphProof (EQUIVALENT transformation)

(39) TRUE

(40) Obligation:

(41) IDependencyGraphProof (EQUIVALENT transformation)

(42) TRUE