Termination proof of /tmp/tmpffPdkW/MirrorTree.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBC2FIG (⇐)

↳2 FIGraph

↳3 FIGtoITRSProof (⇐)

↳4 AND

    ↳5 ITRS

        ↳6 ITRStoQTRSProof (⇔)

        ↳7 QTRS

        ↳8 QTRSRRRProof (⇔)

        ↳9 QTRS

        ↳10 RisEmptyProof (⇔)

        ↳11 TRUE

    ↳12 ITRS

        ↳13 GroundTermsRemoverProof (⇔)

        ↳14 ITRS

        ↳15 ITRSFilterProcessorProof (⇐)

        ↳16 ITRS

        ↳17 ITRSFSMergerProof (⇐)

        ↳18 ITRS

        ↳19 ITRStoIDPProof (⇔)

        ↳20 IDP

        ↳21 UsableRulesProof (⇔)

        ↳22 IDP

        ↳23 ItpfGraphProof (⇔)

        ↳24 IDP

        ↳25 IDPNonInfProof (⇐)

        ↳26 AND

            ↳27 IDP

                ↳28 IDependencyGraphProof (⇔)

                ↳29 TRUE

            ↳30 IDP

                ↳31 IDependencyGraphProof (⇔)

                ↳32 IDP

                ↳33 IDPNonInfProof (⇐)

                ↳34 IDP

                ↳35 IDependencyGraphProof (⇔)

                ↳36 TRUE

(0) Obligation:

JBC Problem based on JBC Program:

No human-readable program information known.

Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: MirrorTree

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 856 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:
Load23205(java.lang.Object(Tree(o34690, o34691, o34692))) → Load23205(o34690)
The set Q consists of the following terms:
Load23205(java.lang.Object(Tree(x0, x1, x2)))

(6) ITRStoQTRSProof (EQUIVALENT transformation)

Represented integers and predefined function symbols by Terms

(7) Obligation:

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

Load23205(java.lang.Object(Tree(o34690, o34691, o34692))) → Load23205(o34690)

The set Q consists of the following terms:

Load23205(java.lang.Object(Tree(x0, x1, x2)))

(8) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(Load23205(x₁)) = x₁
POL(Tree(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(java.lang.Object(x₁)) = 1 + x₁

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

Load23205(java.lang.Object(Tree(o34690, o34691, o34692))) → Load23205(o34690)

(9) Obligation:

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

Load23205(java.lang.Object(Tree(x0, x1, x2)))

(10) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(11) TRUE

(12) 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:
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(o37609, o37610, o37611)), java.lang.Object(List(o34683, java.lang.Object(Tree(o37609, o37610, o37611)))), i4190) → Load23140ARR1(java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(o37609, o37610, o37611)), java.lang.Object(List(o34683, java.lang.Object(Tree(o37609, o37610, o37611)))), i4190, java.lang.Object(java.lang.String(0, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758)))
Load23140ARR1(java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(NULL, NULL, o37611)), java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, NULL, o37611)))), i4190, java.lang.Object(java.lang.String(0, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758))) → Cond_Load23140ARR1(i4188 + 1 > 0 && i4188 + 1 < i2 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(NULL, NULL, o37611)), java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, NULL, o37611)))), i4190, java.lang.Object(java.lang.String(0, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758)))
Cond_Load23140ARR1(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(NULL, NULL, o37611)), java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, NULL, o37611)))), i4190, java.lang.Object(java.lang.String(0, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758))) → New25279(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, java.lang.Object(Tree(NULL, NULL, o37611)), o34683, i4190, NULL, NULL)
Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, o34683, i4190) → Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, o34683, i4190 + -1)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, NULL)), i4190) → Cond_Load23140(i4190 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, NULL)), i4190)
Cond_Load23140(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, NULL)), i4190) → Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, o34683, i4190 + -1)
New25279(java.lang.Object(ARRAY(i2, a34307data)), i4570, o34666, o34683, i4190, NULL, NULL) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4570, o34666, java.lang.Object(List(java.lang.Object(List(o34683, NULL)), NULL)), i4190)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(o37604, o37605, o37606)))), i4190) → Load23140ARR2(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(o37604, o37605, o37606)))), i4190, java.lang.Object(java.lang.String(0, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758)))
Load23140ARR2(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, o37605, o37606)))), i4190, java.lang.Object(java.lang.String(0, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758))) → Cond_Load23140ARR2(i4188 + 1 > 0 && i4188 + 1 < i2 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, o37605, o37606)))), i4190, java.lang.Object(java.lang.String(0, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758)))
Cond_Load23140ARR2(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, o37605, o37606)))), i4190, java.lang.Object(java.lang.String(0, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758))) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, o34666new, java.lang.Object(List(java.lang.Object(List(o34683, NULL)), NULL)), i4190)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(o38693, o38694, o38695)))), i4190) → Load23140ARR3(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(o38693, o38694, o38695)))), i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758)))
Load23140ARR3(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, o38694, o38695)))), i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758))) → Cond_Load23140ARR3(i4836 > 0 && i4188 + 1 > 0 && i4188 + 1 < i2 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, o38694, o38695)))), i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758)))
Cond_Load23140ARR3(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, o38694, o38695)))), i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758))) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, o34666new, java.lang.Object(List(java.lang.Object(List(o34683, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)))), i4190)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(o38708, o38709, o38710)), java.lang.Object(List(o34683, java.lang.Object(Tree(o38708, o38709, o38710)))), i4190) → Load23140ARR4(java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(o38708, o38709, o38710)), java.lang.Object(List(o34683, java.lang.Object(Tree(o38708, o38709, o38710)))), i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758)))
Load23140ARR4(java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL, NULL)), o38710)), java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL, NULL)), o38710)))), i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758))) → Cond_Load23140ARR4(i4836 > 0 && i4188 + 1 > 0 && i4188 + 1 < i2 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL, NULL)), o38710)), java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL, NULL)), o38710)))), i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758)))
Cond_Load23140ARR4(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL, NULL)), o38710)), java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL, NULL)), o38710)))), i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758))) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL, NULL)), o38710)), java.lang.Object(List(java.lang.Object(List(o34683, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)))), i4190)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(o38755, o38756, o38757)))), i4190) → Load23140ARR5(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(o38755, o38756, o38757)))), i4190, java.lang.Object(java.lang.String(0, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Load23140ARR5(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), o38756, o38757)))), i4190, java.lang.Object(java.lang.String(0, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Cond_Load23140ARR5(i4188 + 1 > 0 && i4188 + 1 < i2 && i4327 > 0 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), o38756, o38757)))), i4190, java.lang.Object(java.lang.String(0, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Cond_Load23140ARR5(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), o38756, o38757)))), i4190, java.lang.Object(java.lang.String(0, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, o34666new, java.lang.Object(List(java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, NULL, NULL)))), NULL)), i4190)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(o38770, o38771, o38772)), java.lang.Object(List(o34683, java.lang.Object(Tree(o38770, o38771, o38772)))), i4190) → Load23140ARR6(java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(o38770, o38771, o38772)), java.lang.Object(List(o34683, java.lang.Object(Tree(o38770, o38771, o38772)))), i4190, java.lang.Object(java.lang.String(0, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Load23140ARR6(java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), NULL, o38772)), java.lang.Object(List(o34683, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), NULL, o38772)))), i4190, java.lang.Object(java.lang.String(0, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Cond_Load23140ARR6(i4188 + 1 > 0 && i4188 + 1 < i2 && i4327 > 0 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), NULL, o38772)), java.lang.Object(List(o34683, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), NULL, o38772)))), i4190, java.lang.Object(java.lang.String(0, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Cond_Load23140ARR6(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), NULL, o38772)), java.lang.Object(List(o34683, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), NULL, o38772)))), i4190, java.lang.Object(java.lang.String(0, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), NULL, o38772)), java.lang.Object(List(java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, NULL, NULL)))), NULL)), i4190)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(o39999, o40000, o40001)))), i4190) → Load23140ARR7(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(o39999, o40000, o40001)))), i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Load23140ARR7(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), o40000, o40001)))), i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Cond_Load23140ARR7(i5213 > 0 && i4188 + 1 > 0 && i4188 + 1 < i2 && i4327 > 0 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), o40000, o40001)))), i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Cond_Load23140ARR7(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), o40000, o40001)))), i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, o34666new, java.lang.Object(List(java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, NULL, NULL)))), java.lang.Object(Tree(NULL, NULL, NULL)))), i4190)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(o40020, o40021, o40022)), java.lang.Object(List(o34683, java.lang.Object(Tree(o40020, o40021, o40022)))), i4190) → Load23140ARR8(java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(o40020, o40021, o40022)), java.lang.Object(List(o34683, java.lang.Object(Tree(o40020, o40021, o40022)))), i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Load23140ARR8(java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)), o40022)), java.lang.Object(List(o34683, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)), o40022)))), i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Cond_Load23140ARR8(i5213 > 0 && i4188 + 1 > 0 && i4188 + 1 < i2 && i4327 > 0 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)), o40022)), java.lang.Object(List(o34683, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)), o40022)))), i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Cond_Load23140ARR8(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)), o40022)), java.lang.Object(List(o34683, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)), o40022)))), i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)), o40022)), java.lang.Object(List(java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, NULL, NULL)))), java.lang.Object(Tree(NULL, NULL, NULL)))), i4190)
The set Q consists of the following terms:
Load23140ARR1(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(NULL, NULL, x3)), java.lang.Object(List(x4, java.lang.Object(Tree(NULL, NULL, x3)))), x5, java.lang.Object(java.lang.String(0, x6, x7, x8)), java.lang.Object(java.lang.String(0, x9, x10, x11)))
Cond_Load23140ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(NULL, NULL, x3)), java.lang.Object(List(x4, java.lang.Object(Tree(NULL, NULL, x3)))), x5, java.lang.Object(java.lang.String(0, x6, x7, x8)), java.lang.Object(java.lang.String(0, x9, x10, x11)))
Inc23255(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Load23140(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(x4, NULL)), x5)
Cond_Load23140(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(x4, NULL)), x5)
New25279(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5, NULL, NULL)
Load23140(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(x4, java.lang.Object(Tree(x5, x6, x7)))), x8)
Load23140ARR2(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(x4, java.lang.Object(Tree(NULL, x5, x6)))), x7, java.lang.Object(java.lang.String(0, x8, x9, x10)), java.lang.Object(java.lang.String(0, x11, x12, x13)))
Cond_Load23140ARR2(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(x4, java.lang.Object(Tree(NULL, x5, x6)))), x7, java.lang.Object(java.lang.String(0, x8, x9, x10)), java.lang.Object(java.lang.String(0, x11, x12, x13)))
Load23140ARR3(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(x4, java.lang.Object(Tree(NULL, x5, x6)))), x7, java.lang.Object(java.lang.String(x8, x9, x10, x11)), java.lang.Object(java.lang.String(0, x12, x13, x14)))
Cond_Load23140ARR3(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(x4, java.lang.Object(Tree(NULL, x5, x6)))), x7, java.lang.Object(java.lang.String(x8, x9, x10, x11)), java.lang.Object(java.lang.String(0, x12, x13, x14)))
Load23140ARR4(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL, NULL)), x3)), java.lang.Object(List(x4, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL, NULL)), x3)))), x5, java.lang.Object(java.lang.String(x6, x7, x8, x9)), java.lang.Object(java.lang.String(0, x10, x11, x12)))
Cond_Load23140ARR4(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL, NULL)), x3)), java.lang.Object(List(x4, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL, NULL)), x3)))), x5, java.lang.Object(java.lang.String(x6, x7, x8, x9)), java.lang.Object(java.lang.String(0, x10, x11, x12)))
Load23140ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(x4, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), x5, x6)))), x7, java.lang.Object(java.lang.String(0, x8, x9, x10)), java.lang.Object(java.lang.String(x11, x12, x13, x14)))
Cond_Load23140ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(x4, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), x5, x6)))), x7, java.lang.Object(java.lang.String(0, x8, x9, x10)), java.lang.Object(java.lang.String(x11, x12, x13, x14)))
Load23140ARR6(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), NULL, x3)), java.lang.Object(List(x4, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), NULL, x3)))), x5, java.lang.Object(java.lang.String(0, x6, x7, x8)), java.lang.Object(java.lang.String(x9, x10, x11, x12)))
Cond_Load23140ARR6(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), NULL, x3)), java.lang.Object(List(x4, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), NULL, x3)))), x5, java.lang.Object(java.lang.String(0, x6, x7, x8)), java.lang.Object(java.lang.String(x9, x10, x11, x12)))
Load23140ARR7(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(x4, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), x5, x6)))), x7, java.lang.Object(java.lang.String(x8, x9, x10, x11)), java.lang.Object(java.lang.String(x12, x13, x14, x15)))
Cond_Load23140ARR7(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(x4, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), x5, x6)))), x7, java.lang.Object(java.lang.String(x8, x9, x10, x11)), java.lang.Object(java.lang.String(x12, x13, x14, x15)))
Load23140ARR8(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)), x3)), java.lang.Object(List(x4, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)), x3)))), x5, java.lang.Object(java.lang.String(x6, x7, x8, x9)), java.lang.Object(java.lang.String(x10, x11, x12, x13)))
Cond_Load23140ARR8(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)), x3)), java.lang.Object(List(x4, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)), x3)))), x5, java.lang.Object(java.lang.String(x6, x7, x8, x9)), java.lang.Object(java.lang.String(x10, x11, x12, x13)))

(13) GroundTermsRemoverProof (EQUIVALENT transformation)

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

NULL

We removed arguments according to the following replacements:

New25279(x1, x2, x3, x4, x5, x6, x7) → New25279(x1, x2, x3, x4, x5)

(14) 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:
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(o37609, o37610, o37611)), java.lang.Object(List(o34683, java.lang.Object(Tree(o37609, o37610, o37611)))), i4190) → Load23140ARR1(java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(o37609, o37610, o37611)), java.lang.Object(List(o34683, java.lang.Object(Tree(o37609, o37610, o37611)))), i4190, java.lang.Object(java.lang.String(0, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758)))
Load23140ARR1(java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(NULL, NULL, o37611)), java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, NULL, o37611)))), i4190, java.lang.Object(java.lang.String(0, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758))) → Cond_Load23140ARR1(i4188 + 1 > 0 && i4188 + 1 < i2 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(NULL, NULL, o37611)), java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, NULL, o37611)))), i4190, java.lang.Object(java.lang.String(0, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758)))
Cond_Load23140ARR1(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(NULL, NULL, o37611)), java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, NULL, o37611)))), i4190, java.lang.Object(java.lang.String(0, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758))) → New25279(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, java.lang.Object(Tree(NULL, NULL, o37611)), o34683, i4190)
Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, o34683, i4190) → Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, o34683, i4190 + -1)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, NULL)), i4190) → Cond_Load23140(i4190 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, NULL)), i4190)
Cond_Load23140(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, NULL)), i4190) → Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, o34683, i4190 + -1)
New25279(java.lang.Object(ARRAY(i2, a34307data)), i4570, o34666, o34683, i4190) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4570, o34666, java.lang.Object(List(java.lang.Object(List(o34683, NULL)), NULL)), i4190)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(o37604, o37605, o37606)))), i4190) → Load23140ARR2(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(o37604, o37605, o37606)))), i4190, java.lang.Object(java.lang.String(0, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758)))
Load23140ARR2(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, o37605, o37606)))), i4190, java.lang.Object(java.lang.String(0, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758))) → Cond_Load23140ARR2(i4188 + 1 > 0 && i4188 + 1 < i2 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, o37605, o37606)))), i4190, java.lang.Object(java.lang.String(0, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758)))
Cond_Load23140ARR2(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, o37605, o37606)))), i4190, java.lang.Object(java.lang.String(0, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758))) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, o34666new, java.lang.Object(List(java.lang.Object(List(o34683, NULL)), NULL)), i4190)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(o38693, o38694, o38695)))), i4190) → Load23140ARR3(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(o38693, o38694, o38695)))), i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758)))
Load23140ARR3(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, o38694, o38695)))), i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758))) → Cond_Load23140ARR3(i4836 > 0 && i4188 + 1 > 0 && i4188 + 1 < i2 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, o38694, o38695)))), i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758)))
Cond_Load23140ARR3(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, o38694, o38695)))), i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758))) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, o34666new, java.lang.Object(List(java.lang.Object(List(o34683, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)))), i4190)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(o38708, o38709, o38710)), java.lang.Object(List(o34683, java.lang.Object(Tree(o38708, o38709, o38710)))), i4190) → Load23140ARR4(java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(o38708, o38709, o38710)), java.lang.Object(List(o34683, java.lang.Object(Tree(o38708, o38709, o38710)))), i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758)))
Load23140ARR4(java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL, NULL)), o38710)), java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL, NULL)), o38710)))), i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758))) → Cond_Load23140ARR4(i4836 > 0 && i4188 + 1 > 0 && i4188 + 1 < i2 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL, NULL)), o38710)), java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL, NULL)), o38710)))), i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758)))
Cond_Load23140ARR4(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL, NULL)), o38710)), java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL, NULL)), o38710)))), i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476)), java.lang.Object(java.lang.String(0, i4281, i4283, a34758))) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL, NULL)), o38710)), java.lang.Object(List(java.lang.Object(List(o34683, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)))), i4190)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(o38755, o38756, o38757)))), i4190) → Load23140ARR5(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(o38755, o38756, o38757)))), i4190, java.lang.Object(java.lang.String(0, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Load23140ARR5(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), o38756, o38757)))), i4190, java.lang.Object(java.lang.String(0, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Cond_Load23140ARR5(i4188 + 1 > 0 && i4188 + 1 < i2 && i4327 > 0 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), o38756, o38757)))), i4190, java.lang.Object(java.lang.String(0, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Cond_Load23140ARR5(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), o38756, o38757)))), i4190, java.lang.Object(java.lang.String(0, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, o34666new, java.lang.Object(List(java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, NULL, NULL)))), NULL)), i4190)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(o38770, o38771, o38772)), java.lang.Object(List(o34683, java.lang.Object(Tree(o38770, o38771, o38772)))), i4190) → Load23140ARR6(java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(o38770, o38771, o38772)), java.lang.Object(List(o34683, java.lang.Object(Tree(o38770, o38771, o38772)))), i4190, java.lang.Object(java.lang.String(0, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Load23140ARR6(java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), NULL, o38772)), java.lang.Object(List(o34683, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), NULL, o38772)))), i4190, java.lang.Object(java.lang.String(0, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Cond_Load23140ARR6(i4188 + 1 > 0 && i4188 + 1 < i2 && i4327 > 0 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), NULL, o38772)), java.lang.Object(List(o34683, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), NULL, o38772)))), i4190, java.lang.Object(java.lang.String(0, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Cond_Load23140ARR6(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), NULL, o38772)), java.lang.Object(List(o34683, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), NULL, o38772)))), i4190, java.lang.Object(java.lang.String(0, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), NULL, o38772)), java.lang.Object(List(java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, NULL, NULL)))), NULL)), i4190)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(o39999, o40000, o40001)))), i4190) → Load23140ARR7(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(o39999, o40000, o40001)))), i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Load23140ARR7(java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), o40000, o40001)))), i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Cond_Load23140ARR7(i5213 > 0 && i4188 + 1 > 0 && i4188 + 1 < i2 && i4327 > 0 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), o40000, o40001)))), i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Cond_Load23140ARR7(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, o34666, java.lang.Object(List(o34683, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), o40000, o40001)))), i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, o34666new, java.lang.Object(List(java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, NULL, NULL)))), java.lang.Object(Tree(NULL, NULL, NULL)))), i4190)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(o40020, o40021, o40022)), java.lang.Object(List(o34683, java.lang.Object(Tree(o40020, o40021, o40022)))), i4190) → Load23140ARR8(java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(o40020, o40021, o40022)), java.lang.Object(List(o34683, java.lang.Object(Tree(o40020, o40021, o40022)))), i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Load23140ARR8(java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)), o40022)), java.lang.Object(List(o34683, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)), o40022)))), i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Cond_Load23140ARR8(i5213 > 0 && i4188 + 1 > 0 && i4188 + 1 < i2 && i4327 > 0 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)), o40022)), java.lang.Object(List(o34683, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)), o40022)))), i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Cond_Load23140ARR8(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)), o40022)), java.lang.Object(List(o34683, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)), o40022)))), i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)), o40022)), java.lang.Object(List(java.lang.Object(List(o34683, java.lang.Object(Tree(NULL, NULL, NULL)))), java.lang.Object(Tree(NULL, NULL, NULL)))), i4190)
The set Q consists of the following terms:
Load23140ARR1(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(NULL, NULL, x3)), java.lang.Object(List(x4, java.lang.Object(Tree(NULL, NULL, x3)))), x5, java.lang.Object(java.lang.String(0, x6, x7, x8)), java.lang.Object(java.lang.String(0, x9, x10, x11)))
Cond_Load23140ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(NULL, NULL, x3)), java.lang.Object(List(x4, java.lang.Object(Tree(NULL, NULL, x3)))), x5, java.lang.Object(java.lang.String(0, x6, x7, x8)), java.lang.Object(java.lang.String(0, x9, x10, x11)))
Inc23255(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Load23140(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(x4, NULL)), x5)
Cond_Load23140(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(x4, NULL)), x5)
New25279(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Load23140(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(x4, java.lang.Object(Tree(x5, x6, x7)))), x8)
Load23140ARR2(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(x4, java.lang.Object(Tree(NULL, x5, x6)))), x7, java.lang.Object(java.lang.String(0, x8, x9, x10)), java.lang.Object(java.lang.String(0, x11, x12, x13)))
Cond_Load23140ARR2(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(x4, java.lang.Object(Tree(NULL, x5, x6)))), x7, java.lang.Object(java.lang.String(0, x8, x9, x10)), java.lang.Object(java.lang.String(0, x11, x12, x13)))
Load23140ARR3(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(x4, java.lang.Object(Tree(NULL, x5, x6)))), x7, java.lang.Object(java.lang.String(x8, x9, x10, x11)), java.lang.Object(java.lang.String(0, x12, x13, x14)))
Cond_Load23140ARR3(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(x4, java.lang.Object(Tree(NULL, x5, x6)))), x7, java.lang.Object(java.lang.String(x8, x9, x10, x11)), java.lang.Object(java.lang.String(0, x12, x13, x14)))
Load23140ARR4(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL, NULL)), x3)), java.lang.Object(List(x4, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL, NULL)), x3)))), x5, java.lang.Object(java.lang.String(x6, x7, x8, x9)), java.lang.Object(java.lang.String(0, x10, x11, x12)))
Cond_Load23140ARR4(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL, NULL)), x3)), java.lang.Object(List(x4, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL, NULL)), x3)))), x5, java.lang.Object(java.lang.String(x6, x7, x8, x9)), java.lang.Object(java.lang.String(0, x10, x11, x12)))
Load23140ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(x4, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), x5, x6)))), x7, java.lang.Object(java.lang.String(0, x8, x9, x10)), java.lang.Object(java.lang.String(x11, x12, x13, x14)))
Cond_Load23140ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(x4, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), x5, x6)))), x7, java.lang.Object(java.lang.String(0, x8, x9, x10)), java.lang.Object(java.lang.String(x11, x12, x13, x14)))
Load23140ARR6(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), NULL, x3)), java.lang.Object(List(x4, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), NULL, x3)))), x5, java.lang.Object(java.lang.String(0, x6, x7, x8)), java.lang.Object(java.lang.String(x9, x10, x11, x12)))
Cond_Load23140ARR6(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), NULL, x3)), java.lang.Object(List(x4, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), NULL, x3)))), x5, java.lang.Object(java.lang.String(0, x6, x7, x8)), java.lang.Object(java.lang.String(x9, x10, x11, x12)))
Load23140ARR7(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(x4, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), x5, x6)))), x7, java.lang.Object(java.lang.String(x8, x9, x10, x11)), java.lang.Object(java.lang.String(x12, x13, x14, x15)))
Cond_Load23140ARR7(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(List(x4, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), x5, x6)))), x7, java.lang.Object(java.lang.String(x8, x9, x10, x11)), java.lang.Object(java.lang.String(x12, x13, x14, x15)))
Load23140ARR8(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)), x3)), java.lang.Object(List(x4, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)), x3)))), x5, java.lang.Object(java.lang.String(x6, x7, x8, x9)), java.lang.Object(java.lang.String(x10, x11, x12, x13)))
Cond_Load23140ARR8(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)), x3)), java.lang.Object(List(x4, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, NULL)), java.lang.Object(Tree(NULL, NULL, NULL)), x3)))), x5, java.lang.Object(java.lang.String(x6, x7, x8, x9)), java.lang.Object(java.lang.String(x10, x11, x12, x13)))

(15) ITRSFilterProcessorProof (SOUND transformation)

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

Load23140(x1, x2, x3, x4, x5) → Load23140(x1, x2, x5)
Tree(x1, x2, x3) → Tree
List(x1, x2) → List
Load23140ARR1(x1, x2, x3, x4, x5, x6, x7) → Load23140ARR1(x1, x2, x5)
Cond_Load23140ARR1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_Load23140ARR1(x1, x2, x3, x6)
New25279(x1, x2, x3, x4, x5) → New25279(x1, x2, x5)
Inc23255(x1, x2, x3, x4, x5) → Inc23255(x1, x2, x5)
Cond_Load23140(x1, x2, x3, x4, x5, x6) → Cond_Load23140(x1, x2, x3, x6)
Load23140ARR2(x1, x2, x3, x4, x5, x6, x7) → Load23140ARR2(x1, x2, x5)
Cond_Load23140ARR2(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_Load23140ARR2(x1, x2, x3, x6)
Load23140ARR3(x1, x2, x3, x4, x5, x6, x7) → Load23140ARR3(x1, x2, x5, x6)
Cond_Load23140ARR3(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_Load23140ARR3(x1, x2, x3, x6, x7)
Load23140ARR4(x1, x2, x3, x4, x5, x6, x7) → Load23140ARR4(x1, x2, x5, x6)
Cond_Load23140ARR4(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_Load23140ARR4(x1, x2, x3, x6, x7)
Load23140ARR5(x1, x2, x3, x4, x5, x6, x7) → Load23140ARR5(x1, x2, x5, x7)
Cond_Load23140ARR5(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_Load23140ARR5(x1, x2, x3, x6, x8)
Load23140ARR6(x1, x2, x3, x4, x5, x6, x7) → Load23140ARR6(x1, x2, x5, x7)
Cond_Load23140ARR6(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_Load23140ARR6(x1, x2, x3, x6, x8)
Load23140ARR7(x1, x2, x3, x4, x5, x6, x7) → Load23140ARR7(x1, x2, x5, x6, x7)
Cond_Load23140ARR7(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_Load23140ARR7(x1, x2, x3, x6, x7, x8)
Load23140ARR8(x1, x2, x3, x4, x5, x6, x7) → Load23140ARR8(x1, x2, x5, x6, x7)
Cond_Load23140ARR8(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_Load23140ARR8(x1, x2, x3, x6, x7, x8)

(16) 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:
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → Load23140ARR1(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190)
Load23140ARR1(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → Cond_Load23140ARR1(i4188 + 1 > 0 && i4188 + 1 < i2 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190)
Cond_Load23140ARR1(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → New25279(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, i4190)
Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190 + -1)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → Cond_Load23140(i4190 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190)
Cond_Load23140(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190 + -1)
New25279(java.lang.Object(ARRAY(i2, a34307data)), i4570, i4190) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4570, i4190)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → Load23140ARR2(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190)
Load23140ARR2(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → Cond_Load23140ARR2(i4188 + 1 > 0 && i4188 + 1 < i2 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190)
Cond_Load23140ARR2(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, i4190)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → Load23140ARR3(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476)))
Load23140ARR3(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476))) → Cond_Load23140ARR3(i4836 > 0 && i4188 + 1 > 0 && i4188 + 1 < i2 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476)))
Cond_Load23140ARR3(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476))) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, i4190)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → Load23140ARR4(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476)))
Load23140ARR4(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476))) → Cond_Load23140ARR4(i4836 > 0 && i4188 + 1 > 0 && i4188 + 1 < i2 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476)))
Cond_Load23140ARR4(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476))) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, i4190)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → Load23140ARR5(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Load23140ARR5(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Cond_Load23140ARR5(i4188 + 1 > 0 && i4188 + 1 < i2 && i4327 > 0 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Cond_Load23140ARR5(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, i4190)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → Load23140ARR6(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Load23140ARR6(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Cond_Load23140ARR6(i4188 + 1 > 0 && i4188 + 1 < i2 && i4327 > 0 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Cond_Load23140ARR6(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, i4190)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → Load23140ARR7(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Load23140ARR7(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Cond_Load23140ARR7(i5213 > 0 && i4188 + 1 > 0 && i4188 + 1 < i2 && i4327 > 0 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Cond_Load23140ARR7(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, i4190)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → Load23140ARR8(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Load23140ARR8(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Cond_Load23140ARR8(i5213 > 0 && i4188 + 1 > 0 && i4188 + 1 < i2 && i4327 > 0 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Cond_Load23140ARR8(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, i4190)
The set Q consists of the following terms:
Load23140(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load23140ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load23140ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Inc23255(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load23140(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
New25279(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load23140ARR2(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load23140ARR2(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load23140ARR3(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load23140ARR3(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Load23140ARR4(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load23140ARR4(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Load23140ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load23140ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Load23140ARR6(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load23140ARR6(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Load23140ARR7(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Cond_Load23140ARR7(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Load23140ARR8(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Cond_Load23140ARR8(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))

(17) ITRSFSMergerProof (SOUND transformation)

The following function symbols have been merged:

Load23140ARR3, Load23140ARR4	>	Load23140ARR3_4
Cond_Load23140ARR3, Cond_Load23140ARR4	>	Cond_Load23140ARR3_5
Load23140ARR5, Load23140ARR6	>	Load23140ARR5_4
Cond_Load23140ARR5, Cond_Load23140ARR6	>	Cond_Load23140ARR5_5
Load23140ARR7, Load23140ARR8	>	Load23140ARR7_5
Cond_Load23140ARR7, Cond_Load23140ARR8	>	Cond_Load23140ARR7_6

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

(19) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(20) 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:
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → Load23140ARR1(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190)
Load23140ARR1(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → Cond_Load23140ARR1(i4188 + 1 > 0 && i4188 + 1 < i2 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190)
Cond_Load23140ARR1(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → New25279(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, i4190)
Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190 + -1)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → Cond_Load23140(i4190 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190)
Cond_Load23140(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190 + -1)
New25279(java.lang.Object(ARRAY(i2, a34307data)), i4570, i4190) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4570, i4190)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → Load23140ARR2(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190)
Load23140ARR2(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → Cond_Load23140ARR2(i4188 + 1 > 0 && i4188 + 1 < i2 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190)
Cond_Load23140ARR2(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, i4190)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → Load23140ARR3(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476)))
Load23140ARR3(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476))) → Cond_Load23140ARR3(i4836 > 0 && i4188 + 1 > 0 && i4188 + 1 < i2 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476)))
Cond_Load23140ARR3(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i4836, i4725, i4727, a36476))) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, i4190)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → Load23140ARR5(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Load23140ARR5(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Cond_Load23140ARR5(i4188 + 1 > 0 && i4188 + 1 < i2 && i4327 > 0 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Cond_Load23140ARR5(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, i4190)
Load23140(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190) → Load23140ARR7(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Load23140ARR7(java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Cond_Load23140ARR7(i5213 > 0 && i4188 + 1 > 0 && i4188 + 1 < i2 && i4327 > 0 && i4188 > 0 && i4188 < i2 && i4190 > 0 && i4188 + 1 + 1 > 0, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758)))
Cond_Load23140ARR7(TRUE, java.lang.Object(ARRAY(i2, a34307data)), i4188, i4190, java.lang.Object(java.lang.String(i5213, i5047, i5049, a37597)), java.lang.Object(java.lang.String(i4327, i4281, i4283, a34758))) → Inc23255(java.lang.Object(ARRAY(i2, a34307data)), i4188 + 1 + 1, i4190)

The integer pair graph contains the following rules and edges:
(0): LOAD23140(java.lang.Object(ARRAY(i2[0], a34307data[0])), i4188[0], i4190[0]) → LOAD23140ARR1(java.lang.Object(ARRAY(i2[0], a34307data[0])), i4188[0], i4190[0])
(1): LOAD23140ARR1(java.lang.Object(ARRAY(i2[1], a34307data[1])), i4188[1], i4190[1]) → COND_LOAD23140ARR1(i4188[1] + 1 > 0 && i4188[1] + 1 < i2[1] && i4188[1] > 0 && i4188[1] < i2[1] && i4190[1] > 0 && i4188[1] + 1 + 1 > 0, java.lang.Object(ARRAY(i2[1], a34307data[1])), i4188[1], i4190[1])
(2): COND_LOAD23140ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a34307data[2])), i4188[2], i4190[2]) → NEW25279(java.lang.Object(ARRAY(i2[2], a34307data[2])), i4188[2] + 1 + 1, i4190[2])
(3): INC23255(java.lang.Object(ARRAY(i2[3], a34307data[3])), i4188[3], i4190[3]) → LOAD23140(java.lang.Object(ARRAY(i2[3], a34307data[3])), i4188[3], i4190[3] + -1)
(4): LOAD23140(java.lang.Object(ARRAY(i2[4], a34307data[4])), i4188[4], i4190[4]) → COND_LOAD23140(i4190[4] > 0, java.lang.Object(ARRAY(i2[4], a34307data[4])), i4188[4], i4190[4])
(5): COND_LOAD23140(TRUE, java.lang.Object(ARRAY(i2[5], a34307data[5])), i4188[5], i4190[5]) → LOAD23140(java.lang.Object(ARRAY(i2[5], a34307data[5])), i4188[5], i4190[5] + -1)
(6): NEW25279(java.lang.Object(ARRAY(i2[6], a34307data[6])), i4570[6], i4190[6]) → INC23255(java.lang.Object(ARRAY(i2[6], a34307data[6])), i4570[6], i4190[6])
(7): LOAD23140(java.lang.Object(ARRAY(i2[7], a34307data[7])), i4188[7], i4190[7]) → LOAD23140ARR2(java.lang.Object(ARRAY(i2[7], a34307data[7])), i4188[7], i4190[7])
(8): LOAD23140ARR2(java.lang.Object(ARRAY(i2[8], a34307data[8])), i4188[8], i4190[8]) → COND_LOAD23140ARR2(i4188[8] + 1 > 0 && i4188[8] + 1 < i2[8] && i4188[8] > 0 && i4188[8] < i2[8] && i4190[8] > 0 && i4188[8] + 1 + 1 > 0, java.lang.Object(ARRAY(i2[8], a34307data[8])), i4188[8], i4190[8])
(9): COND_LOAD23140ARR2(TRUE, java.lang.Object(ARRAY(i2[9], a34307data[9])), i4188[9], i4190[9]) → INC23255(java.lang.Object(ARRAY(i2[9], a34307data[9])), i4188[9] + 1 + 1, i4190[9])
(10): LOAD23140(java.lang.Object(ARRAY(i2[10], a34307data[10])), i4188[10], i4190[10]) → LOAD23140ARR3(java.lang.Object(ARRAY(i2[10], a34307data[10])), i4188[10], i4190[10], java.lang.Object(java.lang.String(i4836[10], i4725[10], i4727[10], a36476[10])))
(11): LOAD23140ARR3(java.lang.Object(ARRAY(i2[11], a34307data[11])), i4188[11], i4190[11], java.lang.Object(java.lang.String(i4836[11], i4725[11], i4727[11], a36476[11]))) → COND_LOAD23140ARR3(i4836[11] > 0 && i4188[11] + 1 > 0 && i4188[11] + 1 < i2[11] && i4188[11] > 0 && i4188[11] < i2[11] && i4190[11] > 0 && i4188[11] + 1 + 1 > 0, java.lang.Object(ARRAY(i2[11], a34307data[11])), i4188[11], i4190[11], java.lang.Object(java.lang.String(i4836[11], i4725[11], i4727[11], a36476[11])))
(12): COND_LOAD23140ARR3(TRUE, java.lang.Object(ARRAY(i2[12], a34307data[12])), i4188[12], i4190[12], java.lang.Object(java.lang.String(i4836[12], i4725[12], i4727[12], a36476[12]))) → INC23255(java.lang.Object(ARRAY(i2[12], a34307data[12])), i4188[12] + 1 + 1, i4190[12])
(13): LOAD23140(java.lang.Object(ARRAY(i2[13], a34307data[13])), i4188[13], i4190[13]) → LOAD23140ARR5(java.lang.Object(ARRAY(i2[13], a34307data[13])), i4188[13], i4190[13], java.lang.Object(java.lang.String(i4327[13], i4281[13], i4283[13], a34758[13])))
(14): LOAD23140ARR5(java.lang.Object(ARRAY(i2[14], a34307data[14])), i4188[14], i4190[14], java.lang.Object(java.lang.String(i4327[14], i4281[14], i4283[14], a34758[14]))) → COND_LOAD23140ARR5(i4188[14] + 1 > 0 && i4188[14] + 1 < i2[14] && i4327[14] > 0 && i4188[14] > 0 && i4188[14] < i2[14] && i4190[14] > 0 && i4188[14] + 1 + 1 > 0, java.lang.Object(ARRAY(i2[14], a34307data[14])), i4188[14], i4190[14], java.lang.Object(java.lang.String(i4327[14], i4281[14], i4283[14], a34758[14])))
(15): COND_LOAD23140ARR5(TRUE, java.lang.Object(ARRAY(i2[15], a34307data[15])), i4188[15], i4190[15], java.lang.Object(java.lang.String(i4327[15], i4281[15], i4283[15], a34758[15]))) → INC23255(java.lang.Object(ARRAY(i2[15], a34307data[15])), i4188[15] + 1 + 1, i4190[15])
(16): LOAD23140(java.lang.Object(ARRAY(i2[16], a34307data[16])), i4188[16], i4190[16]) → LOAD23140ARR7(java.lang.Object(ARRAY(i2[16], a34307data[16])), i4188[16], i4190[16], java.lang.Object(java.lang.String(i5213[16], i5047[16], i5049[16], a37597[16])), java.lang.Object(java.lang.String(i4327[16], i4281[16], i4283[16], a34758[16])))
(17): LOAD23140ARR7(java.lang.Object(ARRAY(i2[17], a34307data[17])), i4188[17], i4190[17], java.lang.Object(java.lang.String(i5213[17], i5047[17], i5049[17], a37597[17])), java.lang.Object(java.lang.String(i4327[17], i4281[17], i4283[17], a34758[17]))) → COND_LOAD23140ARR7(i5213[17] > 0 && i4188[17] + 1 > 0 && i4188[17] + 1 < i2[17] && i4327[17] > 0 && i4188[17] > 0 && i4188[17] < i2[17] && i4190[17] > 0 && i4188[17] + 1 + 1 > 0, java.lang.Object(ARRAY(i2[17], a34307data[17])), i4188[17], i4190[17], java.lang.Object(java.lang.String(i5213[17], i5047[17], i5049[17], a37597[17])), java.lang.Object(java.lang.String(i4327[17], i4281[17], i4283[17], a34758[17])))
(18): COND_LOAD23140ARR7(TRUE, java.lang.Object(ARRAY(i2[18], a34307data[18])), i4188[18], i4190[18], java.lang.Object(java.lang.String(i5213[18], i5047[18], i5049[18], a37597[18])), java.lang.Object(java.lang.String(i4327[18], i4281[18], i4283[18], a34758[18]))) → INC23255(java.lang.Object(ARRAY(i2[18], a34307data[18])), i4188[18] + 1 + 1, i4190[18])

(0) -> (1), if ((i4190[0] →^* i4190[1])∧(i4188[0] →^* i4188[1])∧(java.lang.Object(ARRAY(i2[0], a34307data[0])) →^* java.lang.Object(ARRAY(i2[1], a34307data[1]))))

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

(2) -> (6), if ((java.lang.Object(ARRAY(i2[2], a34307data[2])) →^* java.lang.Object(ARRAY(i2[6], a34307data[6])))∧(i4188[2] + 1 + 1 →^* i4570[6])∧(i4190[2] →^* i4190[6]))

(3) -> (0), if ((java.lang.Object(ARRAY(i2[3], a34307data[3])) →^* java.lang.Object(ARRAY(i2[0], a34307data[0])))∧(i4190[3] + -1 →^* i4190[0])∧(i4188[3] →^* i4188[0]))

(3) -> (4), if ((i4190[3] + -1 →^* i4190[4])∧(java.lang.Object(ARRAY(i2[3], a34307data[3])) →^* java.lang.Object(ARRAY(i2[4], a34307data[4])))∧(i4188[3] →^* i4188[4]))

(3) -> (7), if ((i4188[3] →^* i4188[7])∧(i4190[3] + -1 →^* i4190[7])∧(java.lang.Object(ARRAY(i2[3], a34307data[3])) →^* java.lang.Object(ARRAY(i2[7], a34307data[7]))))

(3) -> (10), if ((java.lang.Object(ARRAY(i2[3], a34307data[3])) →^* java.lang.Object(ARRAY(i2[10], a34307data[10])))∧(i4190[3] + -1 →^* i4190[10])∧(i4188[3] →^* i4188[10]))

(3) -> (13), if ((java.lang.Object(ARRAY(i2[3], a34307data[3])) →^* java.lang.Object(ARRAY(i2[13], a34307data[13])))∧(i4190[3] + -1 →^* i4190[13])∧(i4188[3] →^* i4188[13]))

(3) -> (16), if ((java.lang.Object(ARRAY(i2[3], a34307data[3])) →^* java.lang.Object(ARRAY(i2[16], a34307data[16])))∧(i4190[3] + -1 →^* i4190[16])∧(i4188[3] →^* i4188[16]))

(4) -> (5), if ((i4188[4] →^* i4188[5])∧(i4190[4] > 0 →^* TRUE)∧(i4190[4] →^* i4190[5])∧(java.lang.Object(ARRAY(i2[4], a34307data[4])) →^* java.lang.Object(ARRAY(i2[5], a34307data[5]))))

(5) -> (0), if ((i4188[5] →^* i4188[0])∧(java.lang.Object(ARRAY(i2[5], a34307data[5])) →^* java.lang.Object(ARRAY(i2[0], a34307data[0])))∧(i4190[5] + -1 →^* i4190[0]))

(5) -> (4), if ((i4188[5] →^* i4188[4])∧(i4190[5] + -1 →^* i4190[4])∧(java.lang.Object(ARRAY(i2[5], a34307data[5])) →^* java.lang.Object(ARRAY(i2[4], a34307data[4]))))

(5) -> (7), if ((i4188[5] →^* i4188[7])∧(i4190[5] + -1 →^* i4190[7])∧(java.lang.Object(ARRAY(i2[5], a34307data[5])) →^* java.lang.Object(ARRAY(i2[7], a34307data[7]))))

(5) -> (10), if ((i4188[5] →^* i4188[10])∧(java.lang.Object(ARRAY(i2[5], a34307data[5])) →^* java.lang.Object(ARRAY(i2[10], a34307data[10])))∧(i4190[5] + -1 →^* i4190[10]))

(5) -> (13), if ((i4190[5] + -1 →^* i4190[13])∧(java.lang.Object(ARRAY(i2[5], a34307data[5])) →^* java.lang.Object(ARRAY(i2[13], a34307data[13])))∧(i4188[5] →^* i4188[13]))

(5) -> (16), if ((i4190[5] + -1 →^* i4190[16])∧(i4188[5] →^* i4188[16])∧(java.lang.Object(ARRAY(i2[5], a34307data[5])) →^* java.lang.Object(ARRAY(i2[16], a34307data[16]))))

(6) -> (3), if ((java.lang.Object(ARRAY(i2[6], a34307data[6])) →^* java.lang.Object(ARRAY(i2[3], a34307data[3])))∧(i4190[6] →^* i4190[3])∧(i4570[6] →^* i4188[3]))

(7) -> (8), if ((java.lang.Object(ARRAY(i2[7], a34307data[7])) →^* java.lang.Object(ARRAY(i2[8], a34307data[8])))∧(i4188[7] →^* i4188[8])∧(i4190[7] →^* i4190[8]))

(8) -> (9), if ((java.lang.Object(ARRAY(i2[8], a34307data[8])) →^* java.lang.Object(ARRAY(i2[9], a34307data[9])))∧(i4188[8] →^* i4188[9])∧(i4188[8] + 1 > 0 && i4188[8] + 1 < i2[8] && i4188[8] > 0 && i4188[8] < i2[8] && i4190[8] > 0 && i4188[8] + 1 + 1 > 0 →^* TRUE)∧(i4190[8] →^* i4190[9]))

(9) -> (3), if ((i4188[9] + 1 + 1 →^* i4188[3])∧(java.lang.Object(ARRAY(i2[9], a34307data[9])) →^* java.lang.Object(ARRAY(i2[3], a34307data[3])))∧(i4190[9] →^* i4190[3]))

(10) -> (11), if ((java.lang.Object(java.lang.String(i4836[10], i4725[10], i4727[10], a36476[10])) →^* java.lang.Object(java.lang.String(i4836[11], i4725[11], i4727[11], a36476[11])))∧(i4188[10] →^* i4188[11])∧(java.lang.Object(ARRAY(i2[10], a34307data[10])) →^* java.lang.Object(ARRAY(i2[11], a34307data[11])))∧(i4190[10] →^* i4190[11]))

(11) -> (12), if ((i4836[11] > 0 && i4188[11] + 1 > 0 && i4188[11] + 1 < i2[11] && i4188[11] > 0 && i4188[11] < i2[11] && i4190[11] > 0 && i4188[11] + 1 + 1 > 0 →^* TRUE)∧(i4190[11] →^* i4190[12])∧(java.lang.Object(java.lang.String(i4836[11], i4725[11], i4727[11], a36476[11])) →^* java.lang.Object(java.lang.String(i4836[12], i4725[12], i4727[12], a36476[12])))∧(java.lang.Object(ARRAY(i2[11], a34307data[11])) →^* java.lang.Object(ARRAY(i2[12], a34307data[12])))∧(i4188[11] →^* i4188[12]))

(12) -> (3), if ((i4190[12] →^* i4190[3])∧(i4188[12] + 1 + 1 →^* i4188[3])∧(java.lang.Object(ARRAY(i2[12], a34307data[12])) →^* java.lang.Object(ARRAY(i2[3], a34307data[3]))))

(13) -> (14), if ((i4188[13] →^* i4188[14])∧(java.lang.Object(ARRAY(i2[13], a34307data[13])) →^* java.lang.Object(ARRAY(i2[14], a34307data[14])))∧(java.lang.Object(java.lang.String(i4327[13], i4281[13], i4283[13], a34758[13])) →^* java.lang.Object(java.lang.String(i4327[14], i4281[14], i4283[14], a34758[14])))∧(i4190[13] →^* i4190[14]))

(14) -> (15), if ((java.lang.Object(java.lang.String(i4327[14], i4281[14], i4283[14], a34758[14])) →^* java.lang.Object(java.lang.String(i4327[15], i4281[15], i4283[15], a34758[15])))∧(i4188[14] →^* i4188[15])∧(java.lang.Object(ARRAY(i2[14], a34307data[14])) →^* java.lang.Object(ARRAY(i2[15], a34307data[15])))∧(i4190[14] →^* i4190[15])∧(i4188[14] + 1 > 0 && i4188[14] + 1 < i2[14] && i4327[14] > 0 && i4188[14] > 0 && i4188[14] < i2[14] && i4190[14] > 0 && i4188[14] + 1 + 1 > 0 →^* TRUE))

(15) -> (3), if ((i4188[15] + 1 + 1 →^* i4188[3])∧(i4190[15] →^* i4190[3])∧(java.lang.Object(ARRAY(i2[15], a34307data[15])) →^* java.lang.Object(ARRAY(i2[3], a34307data[3]))))

(16) -> (17), if ((java.lang.Object(java.lang.String(i4327[16], i4281[16], i4283[16], a34758[16])) →^* java.lang.Object(java.lang.String(i4327[17], i4281[17], i4283[17], a34758[17])))∧(java.lang.Object(ARRAY(i2[16], a34307data[16])) →^* java.lang.Object(ARRAY(i2[17], a34307data[17])))∧(i4190[16] →^* i4190[17])∧(java.lang.Object(java.lang.String(i5213[16], i5047[16], i5049[16], a37597[16])) →^* java.lang.Object(java.lang.String(i5213[17], i5047[17], i5049[17], a37597[17])))∧(i4188[16] →^* i4188[17]))

(17) -> (18), if ((i4190[17] →^* i4190[18])∧(java.lang.Object(ARRAY(i2[17], a34307data[17])) →^* java.lang.Object(ARRAY(i2[18], a34307data[18])))∧(java.lang.Object(java.lang.String(i5213[17], i5047[17], i5049[17], a37597[17])) →^* java.lang.Object(java.lang.String(i5213[18], i5047[18], i5049[18], a37597[18])))∧(i5213[17] > 0 && i4188[17] + 1 > 0 && i4188[17] + 1 < i2[17] && i4327[17] > 0 && i4188[17] > 0 && i4188[17] < i2[17] && i4190[17] > 0 && i4188[17] + 1 + 1 > 0 →^* TRUE)∧(i4188[17] →^* i4188[18])∧(java.lang.Object(java.lang.String(i4327[17], i4281[17], i4283[17], a34758[17])) →^* java.lang.Object(java.lang.String(i4327[18], i4281[18], i4283[18], a34758[18]))))

(18) -> (3), if ((i4188[18] + 1 + 1 →^* i4188[3])∧(i4190[18] →^* i4190[3])∧(java.lang.Object(ARRAY(i2[18], a34307data[18])) →^* java.lang.Object(ARRAY(i2[3], a34307data[3]))))

The set Q consists of the following terms:
Load23140(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load23140ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load23140ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Inc23255(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load23140(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
New25279(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load23140ARR2(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load23140ARR2(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load23140ARR3(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load23140ARR3(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Load23140ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load23140ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Load23140ARR7(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Cond_Load23140ARR7(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))

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

(22) 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): LOAD23140(java.lang.Object(ARRAY(i2[0], a34307data[0])), i4188[0], i4190[0]) → LOAD23140ARR1(java.lang.Object(ARRAY(i2[0], a34307data[0])), i4188[0], i4190[0])
(1): LOAD23140ARR1(java.lang.Object(ARRAY(i2[1], a34307data[1])), i4188[1], i4190[1]) → COND_LOAD23140ARR1(i4188[1] + 1 > 0 && i4188[1] + 1 < i2[1] && i4188[1] > 0 && i4188[1] < i2[1] && i4190[1] > 0 && i4188[1] + 1 + 1 > 0, java.lang.Object(ARRAY(i2[1], a34307data[1])), i4188[1], i4190[1])
(2): COND_LOAD23140ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a34307data[2])), i4188[2], i4190[2]) → NEW25279(java.lang.Object(ARRAY(i2[2], a34307data[2])), i4188[2] + 1 + 1, i4190[2])
(3): INC23255(java.lang.Object(ARRAY(i2[3], a34307data[3])), i4188[3], i4190[3]) → LOAD23140(java.lang.Object(ARRAY(i2[3], a34307data[3])), i4188[3], i4190[3] + -1)
(4): LOAD23140(java.lang.Object(ARRAY(i2[4], a34307data[4])), i4188[4], i4190[4]) → COND_LOAD23140(i4190[4] > 0, java.lang.Object(ARRAY(i2[4], a34307data[4])), i4188[4], i4190[4])
(5): COND_LOAD23140(TRUE, java.lang.Object(ARRAY(i2[5], a34307data[5])), i4188[5], i4190[5]) → LOAD23140(java.lang.Object(ARRAY(i2[5], a34307data[5])), i4188[5], i4190[5] + -1)
(6): NEW25279(java.lang.Object(ARRAY(i2[6], a34307data[6])), i4570[6], i4190[6]) → INC23255(java.lang.Object(ARRAY(i2[6], a34307data[6])), i4570[6], i4190[6])
(7): LOAD23140(java.lang.Object(ARRAY(i2[7], a34307data[7])), i4188[7], i4190[7]) → LOAD23140ARR2(java.lang.Object(ARRAY(i2[7], a34307data[7])), i4188[7], i4190[7])
(8): LOAD23140ARR2(java.lang.Object(ARRAY(i2[8], a34307data[8])), i4188[8], i4190[8]) → COND_LOAD23140ARR2(i4188[8] + 1 > 0 && i4188[8] + 1 < i2[8] && i4188[8] > 0 && i4188[8] < i2[8] && i4190[8] > 0 && i4188[8] + 1 + 1 > 0, java.lang.Object(ARRAY(i2[8], a34307data[8])), i4188[8], i4190[8])
(9): COND_LOAD23140ARR2(TRUE, java.lang.Object(ARRAY(i2[9], a34307data[9])), i4188[9], i4190[9]) → INC23255(java.lang.Object(ARRAY(i2[9], a34307data[9])), i4188[9] + 1 + 1, i4190[9])
(10): LOAD23140(java.lang.Object(ARRAY(i2[10], a34307data[10])), i4188[10], i4190[10]) → LOAD23140ARR3(java.lang.Object(ARRAY(i2[10], a34307data[10])), i4188[10], i4190[10], java.lang.Object(java.lang.String(i4836[10], i4725[10], i4727[10], a36476[10])))
(11): LOAD23140ARR3(java.lang.Object(ARRAY(i2[11], a34307data[11])), i4188[11], i4190[11], java.lang.Object(java.lang.String(i4836[11], i4725[11], i4727[11], a36476[11]))) → COND_LOAD23140ARR3(i4836[11] > 0 && i4188[11] + 1 > 0 && i4188[11] + 1 < i2[11] && i4188[11] > 0 && i4188[11] < i2[11] && i4190[11] > 0 && i4188[11] + 1 + 1 > 0, java.lang.Object(ARRAY(i2[11], a34307data[11])), i4188[11], i4190[11], java.lang.Object(java.lang.String(i4836[11], i4725[11], i4727[11], a36476[11])))
(12): COND_LOAD23140ARR3(TRUE, java.lang.Object(ARRAY(i2[12], a34307data[12])), i4188[12], i4190[12], java.lang.Object(java.lang.String(i4836[12], i4725[12], i4727[12], a36476[12]))) → INC23255(java.lang.Object(ARRAY(i2[12], a34307data[12])), i4188[12] + 1 + 1, i4190[12])
(13): LOAD23140(java.lang.Object(ARRAY(i2[13], a34307data[13])), i4188[13], i4190[13]) → LOAD23140ARR5(java.lang.Object(ARRAY(i2[13], a34307data[13])), i4188[13], i4190[13], java.lang.Object(java.lang.String(i4327[13], i4281[13], i4283[13], a34758[13])))
(14): LOAD23140ARR5(java.lang.Object(ARRAY(i2[14], a34307data[14])), i4188[14], i4190[14], java.lang.Object(java.lang.String(i4327[14], i4281[14], i4283[14], a34758[14]))) → COND_LOAD23140ARR5(i4188[14] + 1 > 0 && i4188[14] + 1 < i2[14] && i4327[14] > 0 && i4188[14] > 0 && i4188[14] < i2[14] && i4190[14] > 0 && i4188[14] + 1 + 1 > 0, java.lang.Object(ARRAY(i2[14], a34307data[14])), i4188[14], i4190[14], java.lang.Object(java.lang.String(i4327[14], i4281[14], i4283[14], a34758[14])))
(15): COND_LOAD23140ARR5(TRUE, java.lang.Object(ARRAY(i2[15], a34307data[15])), i4188[15], i4190[15], java.lang.Object(java.lang.String(i4327[15], i4281[15], i4283[15], a34758[15]))) → INC23255(java.lang.Object(ARRAY(i2[15], a34307data[15])), i4188[15] + 1 + 1, i4190[15])
(16): LOAD23140(java.lang.Object(ARRAY(i2[16], a34307data[16])), i4188[16], i4190[16]) → LOAD23140ARR7(java.lang.Object(ARRAY(i2[16], a34307data[16])), i4188[16], i4190[16], java.lang.Object(java.lang.String(i5213[16], i5047[16], i5049[16], a37597[16])), java.lang.Object(java.lang.String(i4327[16], i4281[16], i4283[16], a34758[16])))
(17): LOAD23140ARR7(java.lang.Object(ARRAY(i2[17], a34307data[17])), i4188[17], i4190[17], java.lang.Object(java.lang.String(i5213[17], i5047[17], i5049[17], a37597[17])), java.lang.Object(java.lang.String(i4327[17], i4281[17], i4283[17], a34758[17]))) → COND_LOAD23140ARR7(i5213[17] > 0 && i4188[17] + 1 > 0 && i4188[17] + 1 < i2[17] && i4327[17] > 0 && i4188[17] > 0 && i4188[17] < i2[17] && i4190[17] > 0 && i4188[17] + 1 + 1 > 0, java.lang.Object(ARRAY(i2[17], a34307data[17])), i4188[17], i4190[17], java.lang.Object(java.lang.String(i5213[17], i5047[17], i5049[17], a37597[17])), java.lang.Object(java.lang.String(i4327[17], i4281[17], i4283[17], a34758[17])))
(18): COND_LOAD23140ARR7(TRUE, java.lang.Object(ARRAY(i2[18], a34307data[18])), i4188[18], i4190[18], java.lang.Object(java.lang.String(i5213[18], i5047[18], i5049[18], a37597[18])), java.lang.Object(java.lang.String(i4327[18], i4281[18], i4283[18], a34758[18]))) → INC23255(java.lang.Object(ARRAY(i2[18], a34307data[18])), i4188[18] + 1 + 1, i4190[18])