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 ITRStoIDPProof (⇔)
        ↳9 IDP
        ↳10 UsableRulesProof (⇔)
        ↳11 IDP
        ↳12 ItpfGraphProof (⇔)
        ↳13 IDP
        ↳14 IDPNonInfProof (⇐)
        ↳15 AND
            ↳16 IDP
                ↳17 IDependencyGraphProof (⇔)
                ↳18 TRUE
            ↳19 IDP
                ↳20 IDependencyGraphProof (⇔)
                ↳21 TRUE
    ↳22 ITRS
        ↳23 ITRStoIDPProof (⇔)
        ↳24 IDP
        ↳25 UsableRulesProof (⇔)
        ↳26 IDP
        ↳27 IDPNonInfProof (⇐)
        ↳28 AND
            ↳29 IDP
                ↳30 IDependencyGraphProof (⇔)
                ↳31 TRUE
            ↳32 IDP
                ↳33 IDependencyGraphProof (⇔)
                ↳34 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
No human-readable program information known.

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

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 252 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:
Inc4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500)))), i561, java.lang.Object(CyclicList(o2500))) → Cond_Inc4460(i561 + -1 > 0, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500)))), i561, java.lang.Object(CyclicList(o2500)))
Cond_Inc4460(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500)))), i561, java.lang.Object(CyclicList(o2500))) → JMP4853(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500)))), i561 + -1, o2500)
JMP4853(java.lang.Object(CyclicList(o2469)), i568, o2495) → Inc4460(java.lang.Object(CyclicList(o2469)), i568, o2495)
Inc4460(java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2495))) → Cond_Inc44601(i561 + -1 > 0, java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2495)))
Cond_Inc44601(TRUE, java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2495))) → Inc4460(java.lang.Object(CyclicList(o2469)), i561 + -1, o2495)
Inc4460(java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2494rec))) → Cond_Inc44602(i561 + -1 > 0, java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2494rec)))
Cond_Inc44602(TRUE, java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2494rec))) → Inc4460(java.lang.Object(CyclicList(o2469)), i561 + -1, java.lang.Object(CyclicList(o2494rec)))
JMP4687(java.lang.Object(CyclicList(o2469)), i568, o2469) → Inc4460(java.lang.Object(CyclicList(o2469)), i568, o2469)
Inc4460(java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2469))) → Cond_Inc44603(i561 + -1 > 0, java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2469)))
Cond_Inc44603(TRUE, java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2469))) → Inc4460(java.lang.Object(CyclicList(o2469)), i561 + -1, o2469)
Inc4460(java.lang.Object(CyclicList(o2468rec)), i561, java.lang.Object(CyclicList(o2468rec))) → Cond_Inc44604(i561 + -1 > 0, java.lang.Object(CyclicList(o2468rec)), i561, java.lang.Object(CyclicList(o2468rec)))
Cond_Inc44604(TRUE, java.lang.Object(CyclicList(o2468rec)), i561, java.lang.Object(CyclicList(o2468rec))) → Inc4460(java.lang.Object(CyclicList(o2468rec)), i561 + -1, java.lang.Object(CyclicList(o2468rec)))
Inc4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec)))), i561, java.lang.Object(CyclicList(o2499rec))) → Cond_Inc44605(i561 + -1 > 0, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec)))), i561, java.lang.Object(CyclicList(o2499rec)))
Cond_Inc44605(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec)))), i561, java.lang.Object(CyclicList(o2499rec))) → JMP4687(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec)))), i561 + -1, java.lang.Object(CyclicList(o2499rec)))
The set Q consists of the following terms:
Cond_Inc4460(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(x0)))), x1, java.lang.Object(CyclicList(x0)))
JMP4853(java.lang.Object(CyclicList(x0)), x1, x2)
Inc4460(java.lang.Object(CyclicList(x0)), x1, java.lang.Object(CyclicList(x2)))
Cond_Inc44601(TRUE, java.lang.Object(CyclicList(x0)), x1, java.lang.Object(CyclicList(x2)))
Cond_Inc44602(TRUE, java.lang.Object(CyclicList(x0)), x1, java.lang.Object(CyclicList(x2)))
JMP4687(java.lang.Object(CyclicList(x0)), x1, x0)
Cond_Inc44603(TRUE, java.lang.Object(CyclicList(x0)), x1, java.lang.Object(CyclicList(x0)))
Cond_Inc44604(TRUE, java.lang.Object(CyclicList(x0)), x1, java.lang.Object(CyclicList(x0)))
Cond_Inc44605(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(x0)))), x1, java.lang.Object(CyclicList(x0)))

(6) DuplicateArgsRemoverProof (EQUIVALENT transformation)

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

Cond_Inc44604(x1, x2, x3, x4) → Cond_Inc44604(x1, x3, x4)
Cond_Inc44603(x1, x2, x3, x4) → Cond_Inc44603(x1, 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:
Inc4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500)))), i561, java.lang.Object(CyclicList(o2500))) → Cond_Inc4460(i561 + -1 > 0, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500)))), i561, java.lang.Object(CyclicList(o2500)))
Cond_Inc4460(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500)))), i561, java.lang.Object(CyclicList(o2500))) → JMP4853(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500)))), i561 + -1, o2500)
JMP4853(java.lang.Object(CyclicList(o2469)), i568, o2495) → Inc4460(java.lang.Object(CyclicList(o2469)), i568, o2495)
Inc4460(java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2495))) → Cond_Inc44601(i561 + -1 > 0, java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2495)))
Cond_Inc44601(TRUE, java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2495))) → Inc4460(java.lang.Object(CyclicList(o2469)), i561 + -1, o2495)
Inc4460(java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2494rec))) → Cond_Inc44602(i561 + -1 > 0, java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2494rec)))
Cond_Inc44602(TRUE, java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2494rec))) → Inc4460(java.lang.Object(CyclicList(o2469)), i561 + -1, java.lang.Object(CyclicList(o2494rec)))
JMP4687(java.lang.Object(CyclicList(o2469)), i568, o2469) → Inc4460(java.lang.Object(CyclicList(o2469)), i568, o2469)
Inc4460(java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2469))) → Cond_Inc44603(i561 + -1 > 0, i561, java.lang.Object(CyclicList(o2469)))
Cond_Inc44603(TRUE, i561, java.lang.Object(CyclicList(o2469))) → Inc4460(java.lang.Object(CyclicList(o2469)), i561 + -1, o2469)
Inc4460(java.lang.Object(CyclicList(o2468rec)), i561, java.lang.Object(CyclicList(o2468rec))) → Cond_Inc44604(i561 + -1 > 0, i561, java.lang.Object(CyclicList(o2468rec)))
Cond_Inc44604(TRUE, i561, java.lang.Object(CyclicList(o2468rec))) → Inc4460(java.lang.Object(CyclicList(o2468rec)), i561 + -1, java.lang.Object(CyclicList(o2468rec)))
Inc4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec)))), i561, java.lang.Object(CyclicList(o2499rec))) → Cond_Inc44605(i561 + -1 > 0, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec)))), i561, java.lang.Object(CyclicList(o2499rec)))
Cond_Inc44605(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec)))), i561, java.lang.Object(CyclicList(o2499rec))) → JMP4687(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec)))), i561 + -1, java.lang.Object(CyclicList(o2499rec)))
The set Q consists of the following terms:
Cond_Inc4460(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(x0)))), x1, java.lang.Object(CyclicList(x0)))
JMP4853(java.lang.Object(CyclicList(x0)), x1, x2)
Inc4460(java.lang.Object(CyclicList(x0)), x1, java.lang.Object(CyclicList(x2)))
Cond_Inc44601(TRUE, java.lang.Object(CyclicList(x0)), x1, java.lang.Object(CyclicList(x2)))
Cond_Inc44602(TRUE, java.lang.Object(CyclicList(x0)), x1, java.lang.Object(CyclicList(x2)))
JMP4687(java.lang.Object(CyclicList(x0)), x1, x0)
Cond_Inc44603(TRUE, x0, java.lang.Object(CyclicList(x1)))
Cond_Inc44604(TRUE, x0, java.lang.Object(CyclicList(x1)))
Cond_Inc44605(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(x0)))), x1, java.lang.Object(CyclicList(x0)))

(8) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

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


The ITRS R consists of the following rules:
Inc4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500)))), i561, java.lang.Object(CyclicList(o2500))) → Cond_Inc4460(i561 + -1 > 0, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500)))), i561, java.lang.Object(CyclicList(o2500)))
Cond_Inc4460(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500)))), i561, java.lang.Object(CyclicList(o2500))) → JMP4853(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500)))), i561 + -1, o2500)
JMP4853(java.lang.Object(CyclicList(o2469)), i568, o2495) → Inc4460(java.lang.Object(CyclicList(o2469)), i568, o2495)
Inc4460(java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2495))) → Cond_Inc44601(i561 + -1 > 0, java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2495)))
Cond_Inc44601(TRUE, java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2495))) → Inc4460(java.lang.Object(CyclicList(o2469)), i561 + -1, o2495)
Inc4460(java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2494rec))) → Cond_Inc44602(i561 + -1 > 0, java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2494rec)))
Cond_Inc44602(TRUE, java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2494rec))) → Inc4460(java.lang.Object(CyclicList(o2469)), i561 + -1, java.lang.Object(CyclicList(o2494rec)))
JMP4687(java.lang.Object(CyclicList(o2469)), i568, o2469) → Inc4460(java.lang.Object(CyclicList(o2469)), i568, o2469)
Inc4460(java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2469))) → Cond_Inc44603(i561 + -1 > 0, i561, java.lang.Object(CyclicList(o2469)))
Cond_Inc44603(TRUE, i561, java.lang.Object(CyclicList(o2469))) → Inc4460(java.lang.Object(CyclicList(o2469)), i561 + -1, o2469)
Inc4460(java.lang.Object(CyclicList(o2468rec)), i561, java.lang.Object(CyclicList(o2468rec))) → Cond_Inc44604(i561 + -1 > 0, i561, java.lang.Object(CyclicList(o2468rec)))
Cond_Inc44604(TRUE, i561, java.lang.Object(CyclicList(o2468rec))) → Inc4460(java.lang.Object(CyclicList(o2468rec)), i561 + -1, java.lang.Object(CyclicList(o2468rec)))
Inc4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec)))), i561, java.lang.Object(CyclicList(o2499rec))) → Cond_Inc44605(i561 + -1 > 0, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec)))), i561, java.lang.Object(CyclicList(o2499rec)))
Cond_Inc44605(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec)))), i561, java.lang.Object(CyclicList(o2499rec))) → JMP4687(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec)))), i561 + -1, java.lang.Object(CyclicList(o2499rec)))

The integer pair graph contains the following rules and edges:
(0): INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0]))) → COND_INC4460(i561[0] + -1 > 0, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0])))
(1): COND_INC4460(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))), i561[1], java.lang.Object(CyclicList(o2500[1]))) → JMP4853'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))), i561[1] + -1, o2500[1])
(2): JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2]) → INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])
(3): INC4460(java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3]))) → COND_INC44601(i561[3] + -1 > 0, java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3])))
(4): COND_INC44601(TRUE, java.lang.Object(CyclicList(o2469[4])), i561[4], java.lang.Object(CyclicList(o2495[4]))) → INC4460(java.lang.Object(CyclicList(o2469[4])), i561[4] + -1, o2495[4])
(5): INC4460(java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5]))) → COND_INC44602(i561[5] + -1 > 0, java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5])))
(6): COND_INC44602(TRUE, java.lang.Object(CyclicList(o2469[6])), i561[6], java.lang.Object(CyclicList(o2494rec[6]))) → INC4460(java.lang.Object(CyclicList(o2469[6])), i561[6] + -1, java.lang.Object(CyclicList(o2494rec[6])))
(7): JMP4687'(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7]) → INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])
(8): INC4460(java.lang.Object(CyclicList(o2469[8])), i561[8], java.lang.Object(CyclicList(o2469[8]))) → COND_INC44603(i561[8] + -1 > 0, i561[8], java.lang.Object(CyclicList(o2469[8])))
(9): COND_INC44603(TRUE, i561[9], java.lang.Object(CyclicList(o2469[9]))) → INC4460(java.lang.Object(CyclicList(o2469[9])), i561[9] + -1, o2469[9])
(10): INC4460(java.lang.Object(CyclicList(o2468rec[10])), i561[10], java.lang.Object(CyclicList(o2468rec[10]))) → COND_INC44604(i561[10] + -1 > 0, i561[10], java.lang.Object(CyclicList(o2468rec[10])))
(11): COND_INC44604(TRUE, i561[11], java.lang.Object(CyclicList(o2468rec[11]))) → INC4460(java.lang.Object(CyclicList(o2468rec[11])), i561[11] + -1, java.lang.Object(CyclicList(o2468rec[11])))
(12): INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12]))) → COND_INC44605(i561[12] + -1 > 0, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12])))
(13): COND_INC44605(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13])))), i561[13], java.lang.Object(CyclicList(o2499rec[13]))) → JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13])))), i561[13] + -1, java.lang.Object(CyclicList(o2499rec[13])))

(0) -> (1), if ((i561[0] →* i561[1])∧(i561[0] + -1 > 0 →* TRUE)∧(java.lang.Object(CyclicList(o2500[0])) →* java.lang.Object(CyclicList(o2500[1])))∧(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1]))))))


(1) -> (2), if ((i561[1] + -1 →* i568[2])∧(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))) →* java.lang.Object(CyclicList(o2469[2])))∧(o2500[1] →* o2495[2]))


(2) -> (0), if ((o2495[2] →* java.lang.Object(CyclicList(o2500[0])))∧(java.lang.Object(CyclicList(o2469[2])) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))))∧(i568[2] →* i561[0]))


(2) -> (3), if ((java.lang.Object(CyclicList(o2469[2])) →* java.lang.Object(CyclicList(o2469[3])))∧(i568[2] →* i561[3])∧(o2495[2] →* java.lang.Object(CyclicList(o2495[3]))))


(2) -> (5), if ((java.lang.Object(CyclicList(o2469[2])) →* java.lang.Object(CyclicList(o2469[5])))∧(i568[2] →* i561[5])∧(o2495[2] →* java.lang.Object(CyclicList(o2494rec[5]))))


(2) -> (8), if ((i568[2] →* i561[8])∧(java.lang.Object(CyclicList(o2469[2])) →* java.lang.Object(CyclicList(o2469[8])))∧(o2495[2] →* java.lang.Object(CyclicList(o2469[8]))))


(2) -> (10), if ((o2495[2] →* java.lang.Object(CyclicList(o2468rec[10])))∧(java.lang.Object(CyclicList(o2469[2])) →* java.lang.Object(CyclicList(o2468rec[10])))∧(i568[2] →* i561[10]))


(2) -> (12), if ((o2495[2] →* java.lang.Object(CyclicList(o2499rec[12])))∧(java.lang.Object(CyclicList(o2469[2])) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))))∧(i568[2] →* i561[12]))


(3) -> (4), if ((i561[3] →* i561[4])∧(i561[3] + -1 > 0 →* TRUE)∧(java.lang.Object(CyclicList(o2495[3])) →* java.lang.Object(CyclicList(o2495[4])))∧(java.lang.Object(CyclicList(o2469[3])) →* java.lang.Object(CyclicList(o2469[4]))))


(4) -> (0), if ((java.lang.Object(CyclicList(o2469[4])) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))))∧(i561[4] + -1 →* i561[0])∧(o2495[4] →* java.lang.Object(CyclicList(o2500[0]))))


(4) -> (3), if ((java.lang.Object(CyclicList(o2469[4])) →* java.lang.Object(CyclicList(o2469[3])))∧(i561[4] + -1 →* i561[3])∧(o2495[4] →* java.lang.Object(CyclicList(o2495[3]))))


(4) -> (5), if ((o2495[4] →* java.lang.Object(CyclicList(o2494rec[5])))∧(i561[4] + -1 →* i561[5])∧(java.lang.Object(CyclicList(o2469[4])) →* java.lang.Object(CyclicList(o2469[5]))))


(4) -> (8), if ((o2495[4] →* java.lang.Object(CyclicList(o2469[8])))∧(i561[4] + -1 →* i561[8])∧(java.lang.Object(CyclicList(o2469[4])) →* java.lang.Object(CyclicList(o2469[8]))))


(4) -> (10), if ((i561[4] + -1 →* i561[10])∧(java.lang.Object(CyclicList(o2469[4])) →* java.lang.Object(CyclicList(o2468rec[10])))∧(o2495[4] →* java.lang.Object(CyclicList(o2468rec[10]))))


(4) -> (12), if ((o2495[4] →* java.lang.Object(CyclicList(o2499rec[12])))∧(java.lang.Object(CyclicList(o2469[4])) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))))∧(i561[4] + -1 →* i561[12]))


(5) -> (6), if ((java.lang.Object(CyclicList(o2494rec[5])) →* java.lang.Object(CyclicList(o2494rec[6])))∧(i561[5] →* i561[6])∧(i561[5] + -1 > 0 →* TRUE)∧(java.lang.Object(CyclicList(o2469[5])) →* java.lang.Object(CyclicList(o2469[6]))))


(6) -> (0), if ((java.lang.Object(CyclicList(o2494rec[6])) →* java.lang.Object(CyclicList(o2500[0])))∧(i561[6] + -1 →* i561[0])∧(java.lang.Object(CyclicList(o2469[6])) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0]))))))


(6) -> (3), if ((java.lang.Object(CyclicList(o2469[6])) →* java.lang.Object(CyclicList(o2469[3])))∧(i561[6] + -1 →* i561[3])∧(java.lang.Object(CyclicList(o2494rec[6])) →* java.lang.Object(CyclicList(o2495[3]))))


(6) -> (5), if ((i561[6] + -1 →* i561[5])∧(java.lang.Object(CyclicList(o2494rec[6])) →* java.lang.Object(CyclicList(o2494rec[5])))∧(java.lang.Object(CyclicList(o2469[6])) →* java.lang.Object(CyclicList(o2469[5]))))


(6) -> (8), if ((java.lang.Object(CyclicList(o2469[6])) →* java.lang.Object(CyclicList(o2469[8])))∧(i561[6] + -1 →* i561[8])∧(java.lang.Object(CyclicList(o2494rec[6])) →* java.lang.Object(CyclicList(o2469[8]))))


(6) -> (10), if ((java.lang.Object(CyclicList(o2494rec[6])) →* java.lang.Object(CyclicList(o2468rec[10])))∧(java.lang.Object(CyclicList(o2469[6])) →* java.lang.Object(CyclicList(o2468rec[10])))∧(i561[6] + -1 →* i561[10]))


(6) -> (12), if ((java.lang.Object(CyclicList(o2494rec[6])) →* java.lang.Object(CyclicList(o2499rec[12])))∧(java.lang.Object(CyclicList(o2469[6])) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))))∧(i561[6] + -1 →* i561[12]))


(7) -> (0), if ((o2469[7] →* java.lang.Object(CyclicList(o2500[0])))∧(i568[7] →* i561[0])∧(java.lang.Object(CyclicList(o2469[7])) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0]))))))


(7) -> (3), if ((o2469[7] →* java.lang.Object(CyclicList(o2495[3])))∧(i568[7] →* i561[3])∧(java.lang.Object(CyclicList(o2469[7])) →* java.lang.Object(CyclicList(o2469[3]))))


(7) -> (5), if ((i568[7] →* i561[5])∧(java.lang.Object(CyclicList(o2469[7])) →* java.lang.Object(CyclicList(o2469[5])))∧(o2469[7] →* java.lang.Object(CyclicList(o2494rec[5]))))


(7) -> (8), if ((o2469[7] →* java.lang.Object(CyclicList(o2469[8])))∧(i568[7] →* i561[8])∧(java.lang.Object(CyclicList(o2469[7])) →* java.lang.Object(CyclicList(o2469[8]))))


(7) -> (10), if ((java.lang.Object(CyclicList(o2469[7])) →* java.lang.Object(CyclicList(o2468rec[10])))∧(i568[7] →* i561[10])∧(o2469[7] →* java.lang.Object(CyclicList(o2468rec[10]))))


(7) -> (12), if ((java.lang.Object(CyclicList(o2469[7])) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))))∧(i568[7] →* i561[12])∧(o2469[7] →* java.lang.Object(CyclicList(o2499rec[12]))))


(8) -> (9), if ((i561[8] + -1 > 0 →* TRUE)∧(java.lang.Object(CyclicList(o2469[8])) →* java.lang.Object(CyclicList(o2469[9])))∧(i561[8] →* i561[9]))


(9) -> (0), if ((i561[9] + -1 →* i561[0])∧(java.lang.Object(CyclicList(o2469[9])) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))))∧(o2469[9] →* java.lang.Object(CyclicList(o2500[0]))))


(9) -> (3), if ((java.lang.Object(CyclicList(o2469[9])) →* java.lang.Object(CyclicList(o2469[3])))∧(o2469[9] →* java.lang.Object(CyclicList(o2495[3])))∧(i561[9] + -1 →* i561[3]))


(9) -> (5), if ((i561[9] + -1 →* i561[5])∧(java.lang.Object(CyclicList(o2469[9])) →* java.lang.Object(CyclicList(o2469[5])))∧(o2469[9] →* java.lang.Object(CyclicList(o2494rec[5]))))


(9) -> (8), if ((o2469[9] →* java.lang.Object(CyclicList(o2469[8])))∧(i561[9] + -1 →* i561[8])∧(java.lang.Object(CyclicList(o2469[9])) →* java.lang.Object(CyclicList(o2469[8]))))


(9) -> (10), if ((i561[9] + -1 →* i561[10])∧(java.lang.Object(CyclicList(o2469[9])) →* java.lang.Object(CyclicList(o2468rec[10])))∧(o2469[9] →* java.lang.Object(CyclicList(o2468rec[10]))))


(9) -> (12), if ((i561[9] + -1 →* i561[12])∧(o2469[9] →* java.lang.Object(CyclicList(o2499rec[12])))∧(java.lang.Object(CyclicList(o2469[9])) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12]))))))


(10) -> (11), if ((i561[10] + -1 > 0 →* TRUE)∧(i561[10] →* i561[11])∧(java.lang.Object(CyclicList(o2468rec[10])) →* java.lang.Object(CyclicList(o2468rec[11]))))


(11) -> (0), if ((i561[11] + -1 →* i561[0])∧(java.lang.Object(CyclicList(o2468rec[11])) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))))∧(java.lang.Object(CyclicList(o2468rec[11])) →* java.lang.Object(CyclicList(o2500[0]))))


(11) -> (3), if ((i561[11] + -1 →* i561[3])∧(java.lang.Object(CyclicList(o2468rec[11])) →* java.lang.Object(CyclicList(o2469[3])))∧(java.lang.Object(CyclicList(o2468rec[11])) →* java.lang.Object(CyclicList(o2495[3]))))


(11) -> (5), if ((java.lang.Object(CyclicList(o2468rec[11])) →* java.lang.Object(CyclicList(o2494rec[5])))∧(java.lang.Object(CyclicList(o2468rec[11])) →* java.lang.Object(CyclicList(o2469[5])))∧(i561[11] + -1 →* i561[5]))


(11) -> (8), if ((i561[11] + -1 →* i561[8])∧(java.lang.Object(CyclicList(o2468rec[11])) →* java.lang.Object(CyclicList(o2469[8]))))


(11) -> (10), if ((java.lang.Object(CyclicList(o2468rec[11])) →* java.lang.Object(CyclicList(o2468rec[10])))∧(i561[11] + -1 →* i561[10]))


(11) -> (12), if ((java.lang.Object(CyclicList(o2468rec[11])) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))))∧(i561[11] + -1 →* i561[12])∧(java.lang.Object(CyclicList(o2468rec[11])) →* java.lang.Object(CyclicList(o2499rec[12]))))


(12) -> (13), if ((i561[12] →* i561[13])∧(i561[12] + -1 > 0 →* TRUE)∧(java.lang.Object(CyclicList(o2499rec[12])) →* java.lang.Object(CyclicList(o2499rec[13])))∧(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13]))))))


(13) -> (7), if ((i561[13] + -1 →* i568[7])∧(java.lang.Object(CyclicList(o2499rec[13])) →* o2469[7])∧(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13])))) →* java.lang.Object(CyclicList(o2469[7]))))



The set Q consists of the following terms:
Cond_Inc4460(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(x0)))), x1, java.lang.Object(CyclicList(x0)))
JMP4853(java.lang.Object(CyclicList(x0)), x1, x2)
Inc4460(java.lang.Object(CyclicList(x0)), x1, java.lang.Object(CyclicList(x2)))
Cond_Inc44601(TRUE, java.lang.Object(CyclicList(x0)), x1, java.lang.Object(CyclicList(x2)))
Cond_Inc44602(TRUE, java.lang.Object(CyclicList(x0)), x1, java.lang.Object(CyclicList(x2)))
JMP4687(java.lang.Object(CyclicList(x0)), x1, x0)
Cond_Inc44603(TRUE, x0, java.lang.Object(CyclicList(x1)))
Cond_Inc44604(TRUE, x0, java.lang.Object(CyclicList(x1)))
Cond_Inc44605(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(x0)))), x1, java.lang.Object(CyclicList(x0)))

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

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


R is empty.

The integer pair graph contains the following rules and edges:
(0): INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0]))) → COND_INC4460(i561[0] + -1 > 0, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0])))
(1): COND_INC4460(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))), i561[1], java.lang.Object(CyclicList(o2500[1]))) → JMP4853'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))), i561[1] + -1, o2500[1])
(2): JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2]) → INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])
(3): INC4460(java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3]))) → COND_INC44601(i561[3] + -1 > 0, java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3])))
(4): COND_INC44601(TRUE, java.lang.Object(CyclicList(o2469[4])), i561[4], java.lang.Object(CyclicList(o2495[4]))) → INC4460(java.lang.Object(CyclicList(o2469[4])), i561[4] + -1, o2495[4])
(5): INC4460(java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5]))) → COND_INC44602(i561[5] + -1 > 0, java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5])))
(6): COND_INC44602(TRUE, java.lang.Object(CyclicList(o2469[6])), i561[6], java.lang.Object(CyclicList(o2494rec[6]))) → INC4460(java.lang.Object(CyclicList(o2469[6])), i561[6] + -1, java.lang.Object(CyclicList(o2494rec[6])))
(7): JMP4687'(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7]) → INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])
(8): INC4460(java.lang.Object(CyclicList(o2469[8])), i561[8], java.lang.Object(CyclicList(o2469[8]))) → COND_INC44603(i561[8] + -1 > 0, i561[8], java.lang.Object(CyclicList(o2469[8])))
(9): COND_INC44603(TRUE, i561[9], java.lang.Object(CyclicList(o2469[9]))) → INC4460(java.lang.Object(CyclicList(o2469[9])), i561[9] + -1, o2469[9])
(10): INC4460(java.lang.Object(CyclicList(o2468rec[10])), i561[10], java.lang.Object(CyclicList(o2468rec[10]))) → COND_INC44604(i561[10] + -1 > 0, i561[10], java.lang.Object(CyclicList(o2468rec[10])))
(11): COND_INC44604(TRUE, i561[11], java.lang.Object(CyclicList(o2468rec[11]))) → INC4460(java.lang.Object(CyclicList(o2468rec[11])), i561[11] + -1, java.lang.Object(CyclicList(o2468rec[11])))
(12): INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12]))) → COND_INC44605(i561[12] + -1 > 0, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12])))
(13): COND_INC44605(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13])))), i561[13], java.lang.Object(CyclicList(o2499rec[13]))) → JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13])))), i561[13] + -1, java.lang.Object(CyclicList(o2499rec[13])))

(0) -> (1), if ((i561[0] →* i561[1])∧(i561[0] + -1 > 0 →* TRUE)∧(java.lang.Object(CyclicList(o2500[0])) →* java.lang.Object(CyclicList(o2500[1])))∧(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1]))))))


(1) -> (2), if ((i561[1] + -1 →* i568[2])∧(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))) →* java.lang.Object(CyclicList(o2469[2])))∧(o2500[1] →* o2495[2]))


(2) -> (0), if ((o2495[2] →* java.lang.Object(CyclicList(o2500[0])))∧(java.lang.Object(CyclicList(o2469[2])) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))))∧(i568[2] →* i561[0]))


(2) -> (3), if ((java.lang.Object(CyclicList(o2469[2])) →* java.lang.Object(CyclicList(o2469[3])))∧(i568[2] →* i561[3])∧(o2495[2] →* java.lang.Object(CyclicList(o2495[3]))))


(2) -> (5), if ((java.lang.Object(CyclicList(o2469[2])) →* java.lang.Object(CyclicList(o2469[5])))∧(i568[2] →* i561[5])∧(o2495[2] →* java.lang.Object(CyclicList(o2494rec[5]))))


(2) -> (8), if ((i568[2] →* i561[8])∧(java.lang.Object(CyclicList(o2469[2])) →* java.lang.Object(CyclicList(o2469[8])))∧(o2495[2] →* java.lang.Object(CyclicList(o2469[8]))))


(2) -> (10), if ((o2495[2] →* java.lang.Object(CyclicList(o2468rec[10])))∧(java.lang.Object(CyclicList(o2469[2])) →* java.lang.Object(CyclicList(o2468rec[10])))∧(i568[2] →* i561[10]))


(2) -> (12), if ((o2495[2] →* java.lang.Object(CyclicList(o2499rec[12])))∧(java.lang.Object(CyclicList(o2469[2])) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))))∧(i568[2] →* i561[12]))


(3) -> (4), if ((i561[3] →* i561[4])∧(i561[3] + -1 > 0 →* TRUE)∧(java.lang.Object(CyclicList(o2495[3])) →* java.lang.Object(CyclicList(o2495[4])))∧(java.lang.Object(CyclicList(o2469[3])) →* java.lang.Object(CyclicList(o2469[4]))))


(4) -> (0), if ((java.lang.Object(CyclicList(o2469[4])) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))))∧(i561[4] + -1 →* i561[0])∧(o2495[4] →* java.lang.Object(CyclicList(o2500[0]))))


(4) -> (3), if ((java.lang.Object(CyclicList(o2469[4])) →* java.lang.Object(CyclicList(o2469[3])))∧(i561[4] + -1 →* i561[3])∧(o2495[4] →* java.lang.Object(CyclicList(o2495[3]))))


(4) -> (5), if ((o2495[4] →* java.lang.Object(CyclicList(o2494rec[5])))∧(i561[4] + -1 →* i561[5])∧(java.lang.Object(CyclicList(o2469[4])) →* java.lang.Object(CyclicList(o2469[5]))))


(4) -> (8), if ((o2495[4] →* java.lang.Object(CyclicList(o2469[8])))∧(i561[4] + -1 →* i561[8])∧(java.lang.Object(CyclicList(o2469[4])) →* java.lang.Object(CyclicList(o2469[8]))))


(4) -> (10), if ((i561[4] + -1 →* i561[10])∧(java.lang.Object(CyclicList(o2469[4])) →* java.lang.Object(CyclicList(o2468rec[10])))∧(o2495[4] →* java.lang.Object(CyclicList(o2468rec[10]))))


(4) -> (12), if ((o2495[4] →* java.lang.Object(CyclicList(o2499rec[12])))∧(java.lang.Object(CyclicList(o2469[4])) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))))∧(i561[4] + -1 →* i561[12]))


(5) -> (6), if ((java.lang.Object(CyclicList(o2494rec[5])) →* java.lang.Object(CyclicList(o2494rec[6])))∧(i561[5] →* i561[6])∧(i561[5] + -1 > 0 →* TRUE)∧(java.lang.Object(CyclicList(o2469[5])) →* java.lang.Object(CyclicList(o2469[6]))))


(6) -> (0), if ((java.lang.Object(CyclicList(o2494rec[6])) →* java.lang.Object(CyclicList(o2500[0])))∧(i561[6] + -1 →* i561[0])∧(java.lang.Object(CyclicList(o2469[6])) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0]))))))


(6) -> (3), if ((java.lang.Object(CyclicList(o2469[6])) →* java.lang.Object(CyclicList(o2469[3])))∧(i561[6] + -1 →* i561[3])∧(java.lang.Object(CyclicList(o2494rec[6])) →* java.lang.Object(CyclicList(o2495[3]))))


(6) -> (5), if ((i561[6] + -1 →* i561[5])∧(java.lang.Object(CyclicList(o2494rec[6])) →* java.lang.Object(CyclicList(o2494rec[5])))∧(java.lang.Object(CyclicList(o2469[6])) →* java.lang.Object(CyclicList(o2469[5]))))


(6) -> (8), if ((java.lang.Object(CyclicList(o2469[6])) →* java.lang.Object(CyclicList(o2469[8])))∧(i561[6] + -1 →* i561[8])∧(java.lang.Object(CyclicList(o2494rec[6])) →* java.lang.Object(CyclicList(o2469[8]))))


(6) -> (10), if ((java.lang.Object(CyclicList(o2494rec[6])) →* java.lang.Object(CyclicList(o2468rec[10])))∧(java.lang.Object(CyclicList(o2469[6])) →* java.lang.Object(CyclicList(o2468rec[10])))∧(i561[6] + -1 →* i561[10]))


(6) -> (12), if ((java.lang.Object(CyclicList(o2494rec[6])) →* java.lang.Object(CyclicList(o2499rec[12])))∧(java.lang.Object(CyclicList(o2469[6])) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))))∧(i561[6] + -1 →* i561[12]))


(7) -> (0), if ((o2469[7] →* java.lang.Object(CyclicList(o2500[0])))∧(i568[7] →* i561[0])∧(java.lang.Object(CyclicList(o2469[7])) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0]))))))


(7) -> (3), if ((o2469[7] →* java.lang.Object(CyclicList(o2495[3])))∧(i568[7] →* i561[3])∧(java.lang.Object(CyclicList(o2469[7])) →* java.lang.Object(CyclicList(o2469[3]))))


(7) -> (5), if ((i568[7] →* i561[5])∧(java.lang.Object(CyclicList(o2469[7])) →* java.lang.Object(CyclicList(o2469[5])))∧(o2469[7] →* java.lang.Object(CyclicList(o2494rec[5]))))


(7) -> (8), if ((o2469[7] →* java.lang.Object(CyclicList(o2469[8])))∧(i568[7] →* i561[8])∧(java.lang.Object(CyclicList(o2469[7])) →* java.lang.Object(CyclicList(o2469[8]))))


(7) -> (10), if ((java.lang.Object(CyclicList(o2469[7])) →* java.lang.Object(CyclicList(o2468rec[10])))∧(i568[7] →* i561[10])∧(o2469[7] →* java.lang.Object(CyclicList(o2468rec[10]))))


(7) -> (12), if ((java.lang.Object(CyclicList(o2469[7])) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))))∧(i568[7] →* i561[12])∧(o2469[7] →* java.lang.Object(CyclicList(o2499rec[12]))))


(8) -> (9), if ((i561[8] + -1 > 0 →* TRUE)∧(java.lang.Object(CyclicList(o2469[8])) →* java.lang.Object(CyclicList(o2469[9])))∧(i561[8] →* i561[9]))


(9) -> (0), if ((i561[9] + -1 →* i561[0])∧(java.lang.Object(CyclicList(o2469[9])) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))))∧(o2469[9] →* java.lang.Object(CyclicList(o2500[0]))))


(9) -> (3), if ((java.lang.Object(CyclicList(o2469[9])) →* java.lang.Object(CyclicList(o2469[3])))∧(o2469[9] →* java.lang.Object(CyclicList(o2495[3])))∧(i561[9] + -1 →* i561[3]))


(9) -> (5), if ((i561[9] + -1 →* i561[5])∧(java.lang.Object(CyclicList(o2469[9])) →* java.lang.Object(CyclicList(o2469[5])))∧(o2469[9] →* java.lang.Object(CyclicList(o2494rec[5]))))


(9) -> (8), if ((o2469[9] →* java.lang.Object(CyclicList(o2469[8])))∧(i561[9] + -1 →* i561[8])∧(java.lang.Object(CyclicList(o2469[9])) →* java.lang.Object(CyclicList(o2469[8]))))


(9) -> (10), if ((i561[9] + -1 →* i561[10])∧(java.lang.Object(CyclicList(o2469[9])) →* java.lang.Object(CyclicList(o2468rec[10])))∧(o2469[9] →* java.lang.Object(CyclicList(o2468rec[10]))))


(9) -> (12), if ((i561[9] + -1 →* i561[12])∧(o2469[9] →* java.lang.Object(CyclicList(o2499rec[12])))∧(java.lang.Object(CyclicList(o2469[9])) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12]))))))


(10) -> (11), if ((i561[10] + -1 > 0 →* TRUE)∧(i561[10] →* i561[11])∧(java.lang.Object(CyclicList(o2468rec[10])) →* java.lang.Object(CyclicList(o2468rec[11]))))


(11) -> (0), if ((i561[11] + -1 →* i561[0])∧(java.lang.Object(CyclicList(o2468rec[11])) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))))∧(java.lang.Object(CyclicList(o2468rec[11])) →* java.lang.Object(CyclicList(o2500[0]))))


(11) -> (3), if ((i561[11] + -1 →* i561[3])∧(java.lang.Object(CyclicList(o2468rec[11])) →* java.lang.Object(CyclicList(o2469[3])))∧(java.lang.Object(CyclicList(o2468rec[11])) →* java.lang.Object(CyclicList(o2495[3]))))


(11) -> (5), if ((java.lang.Object(CyclicList(o2468rec[11])) →* java.lang.Object(CyclicList(o2494rec[5])))∧(java.lang.Object(CyclicList(o2468rec[11])) →* java.lang.Object(CyclicList(o2469[5])))∧(i561[11] + -1 →* i561[5]))


(11) -> (8), if ((i561[11] + -1 →* i561[8])∧(java.lang.Object(CyclicList(o2468rec[11])) →* java.lang.Object(CyclicList(o2469[8]))))


(11) -> (10), if ((java.lang.Object(CyclicList(o2468rec[11])) →* java.lang.Object(CyclicList(o2468rec[10])))∧(i561[11] + -1 →* i561[10]))


(11) -> (12), if ((java.lang.Object(CyclicList(o2468rec[11])) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))))∧(i561[11] + -1 →* i561[12])∧(java.lang.Object(CyclicList(o2468rec[11])) →* java.lang.Object(CyclicList(o2499rec[12]))))


(12) -> (13), if ((i561[12] →* i561[13])∧(i561[12] + -1 > 0 →* TRUE)∧(java.lang.Object(CyclicList(o2499rec[12])) →* java.lang.Object(CyclicList(o2499rec[13])))∧(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))) →* java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13]))))))


(13) -> (7), if ((i561[13] + -1 →* i568[7])∧(java.lang.Object(CyclicList(o2499rec[13])) →* o2469[7])∧(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13])))) →* java.lang.Object(CyclicList(o2469[7]))))



The set Q consists of the following terms:
Cond_Inc4460(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(x0)))), x1, java.lang.Object(CyclicList(x0)))
JMP4853(java.lang.Object(CyclicList(x0)), x1, x2)
Inc4460(java.lang.Object(CyclicList(x0)), x1, java.lang.Object(CyclicList(x2)))
Cond_Inc44601(TRUE, java.lang.Object(CyclicList(x0)), x1, java.lang.Object(CyclicList(x2)))
Cond_Inc44602(TRUE, java.lang.Object(CyclicList(x0)), x1, java.lang.Object(CyclicList(x2)))
JMP4687(java.lang.Object(CyclicList(x0)), x1, x0)
Cond_Inc44603(TRUE, x0, java.lang.Object(CyclicList(x1)))
Cond_Inc44604(TRUE, x0, java.lang.Object(CyclicList(x1)))
Cond_Inc44605(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(x0)))), x1, java.lang.Object(CyclicList(x0)))

(12) ItpfGraphProof (EQUIVALENT transformation)

Applied rule ItpfICap [ICap]

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


R is empty.

The integer pair graph contains the following rules and edges:
(0): INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0]))) → COND_INC4460(i561[0] + -1 > 0, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0])))
(1): COND_INC4460(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))), i561[1], java.lang.Object(CyclicList(o2500[1]))) → JMP4853'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))), i561[1] + -1, o2500[1])
(2): JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2]) → INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])
(3): INC4460(java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3]))) → COND_INC44601(i561[3] + -1 > 0, java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3])))
(4): COND_INC44601(TRUE, java.lang.Object(CyclicList(o2469[4])), i561[4], java.lang.Object(CyclicList(o2495[4]))) → INC4460(java.lang.Object(CyclicList(o2469[4])), i561[4] + -1, o2495[4])
(5): INC4460(java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5]))) → COND_INC44602(i561[5] + -1 > 0, java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5])))
(6): COND_INC44602(TRUE, java.lang.Object(CyclicList(o2469[6])), i561[6], java.lang.Object(CyclicList(o2494rec[6]))) → INC4460(java.lang.Object(CyclicList(o2469[6])), i561[6] + -1, java.lang.Object(CyclicList(o2494rec[6])))
(7): JMP4687'(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7]) → INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])
(8): INC4460(java.lang.Object(CyclicList(o2469[8])), i561[8], java.lang.Object(CyclicList(o2469[8]))) → COND_INC44603(i561[8] + -1 > 0, i561[8], java.lang.Object(CyclicList(o2469[8])))
(9): COND_INC44603(TRUE, i561[9], java.lang.Object(CyclicList(o2469[9]))) → INC4460(java.lang.Object(CyclicList(o2469[9])), i561[9] + -1, o2469[9])
(10): INC4460(java.lang.Object(CyclicList(o2468rec[10])), i561[10], java.lang.Object(CyclicList(o2468rec[10]))) → COND_INC44604(i561[10] + -1 > 0, i561[10], java.lang.Object(CyclicList(o2468rec[10])))
(11): COND_INC44604(TRUE, i561[11], java.lang.Object(CyclicList(o2468rec[11]))) → INC4460(java.lang.Object(CyclicList(o2468rec[11])), i561[11] + -1, java.lang.Object(CyclicList(o2468rec[11])))
(12): INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12]))) → COND_INC44605(i561[12] + -1 > 0, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12])))
(13): COND_INC44605(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13])))), i561[13], java.lang.Object(CyclicList(o2499rec[13]))) → JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13])))), i561[13] + -1, java.lang.Object(CyclicList(o2499rec[13])))

(0) -> (1), if ((i561[0] →* i561[1])∧(i561[0] + -1 > 0 →* TRUE)∧((o2500[0] →* o2500[1])))


(1) -> (2), if ((i561[1] + -1 →* i568[2])∧((java.lang.Object(CyclicList(o2500[1])) →* o2469[2]))∧(o2500[1] →* o2495[2]))


(2) -> (0), if ((o2495[2] →* java.lang.Object(CyclicList(o2500[0])))∧((o2469[2] →* java.lang.Object(CyclicList(o2500[0]))))∧(i568[2] →* i561[0]))


(2) -> (3), if (((o2469[2] →* o2469[3]))∧(i568[2] →* i561[3])∧(o2495[2] →* java.lang.Object(CyclicList(o2495[3]))))


(2) -> (5), if (((o2469[2] →* o2469[5]))∧(i568[2] →* i561[5])∧(o2495[2] →* java.lang.Object(CyclicList(o2494rec[5]))))


(2) -> (8), if ((i568[2] →* i561[8])∧((o2469[2] →* o2469[8]))∧(o2495[2] →* java.lang.Object(CyclicList(o2469[8]))))


(2) -> (10), if ((o2495[2] →* java.lang.Object(CyclicList(o2468rec[10])))∧((o2469[2] →* o2468rec[10]))∧(i568[2] →* i561[10]))


(2) -> (12), if ((o2495[2] →* java.lang.Object(CyclicList(o2499rec[12])))∧((o2469[2] →* java.lang.Object(CyclicList(o2499rec[12]))))∧(i568[2] →* i561[12]))


(3) -> (4), if ((i561[3] →* i561[4])∧(i561[3] + -1 > 0 →* TRUE)∧((o2495[3] →* o2495[4]))∧((o2469[3] →* o2469[4])))


(4) -> (0), if (((o2469[4] →* java.lang.Object(CyclicList(o2500[0]))))∧(i561[4] + -1 →* i561[0])∧(o2495[4] →* java.lang.Object(CyclicList(o2500[0]))))


(4) -> (3), if (((o2469[4] →* o2469[3]))∧(i561[4] + -1 →* i561[3])∧(o2495[4] →* java.lang.Object(CyclicList(o2495[3]))))


(4) -> (5), if ((o2495[4] →* java.lang.Object(CyclicList(o2494rec[5])))∧(i561[4] + -1 →* i561[5])∧((o2469[4] →* o2469[5])))


(4) -> (8), if ((o2495[4] →* java.lang.Object(CyclicList(o2469[8])))∧(i561[4] + -1 →* i561[8])∧((o2469[4] →* o2469[8])))


(4) -> (10), if ((i561[4] + -1 →* i561[10])∧((o2469[4] →* o2468rec[10]))∧(o2495[4] →* java.lang.Object(CyclicList(o2468rec[10]))))


(4) -> (12), if ((o2495[4] →* java.lang.Object(CyclicList(o2499rec[12])))∧((o2469[4] →* java.lang.Object(CyclicList(o2499rec[12]))))∧(i561[4] + -1 →* i561[12]))


(5) -> (6), if (((o2494rec[5] →* o2494rec[6]))∧(i561[5] →* i561[6])∧(i561[5] + -1 > 0 →* TRUE)∧((o2469[5] →* o2469[6])))


(6) -> (0), if (((o2494rec[6] →* o2500[0]))∧(i561[6] + -1 →* i561[0])∧((o2469[6] →* java.lang.Object(CyclicList(o2500[0])))))


(6) -> (3), if (((o2469[6] →* o2469[3]))∧(i561[6] + -1 →* i561[3])∧((o2494rec[6] →* o2495[3])))


(6) -> (5), if ((i561[6] + -1 →* i561[5])∧((o2494rec[6] →* o2494rec[5]))∧((o2469[6] →* o2469[5])))


(6) -> (8), if (((o2469[6] →* o2469[8]))∧(i561[6] + -1 →* i561[8])∧((o2494rec[6] →* o2469[8])))


(6) -> (10), if (((o2494rec[6] →* o2468rec[10]))∧((o2469[6] →* o2468rec[10]))∧(i561[6] + -1 →* i561[10]))


(6) -> (12), if (((o2494rec[6] →* o2499rec[12]))∧((o2469[6] →* java.lang.Object(CyclicList(o2499rec[12]))))∧(i561[6] + -1 →* i561[12]))


(7) -> (0), if ((o2469[7] →* java.lang.Object(CyclicList(o2500[0])))∧(i568[7] →* i561[0])∧((o2469[7] →* java.lang.Object(CyclicList(o2500[0])))))


(7) -> (3), if ((o2469[7] →* java.lang.Object(CyclicList(o2495[3])))∧(i568[7] →* i561[3])∧((o2469[7] →* o2469[3])))


(7) -> (5), if ((i568[7] →* i561[5])∧((o2469[7] →* o2469[5]))∧(o2469[7] →* java.lang.Object(CyclicList(o2494rec[5]))))


(7) -> (8), if ((o2469[7] →* java.lang.Object(CyclicList(o2469[8])))∧(i568[7] →* i561[8])∧((o2469[7] →* o2469[8])))


(7) -> (10), if (((o2469[7] →* o2468rec[10]))∧(i568[7] →* i561[10])∧(o2469[7] →* java.lang.Object(CyclicList(o2468rec[10]))))


(7) -> (12), if (((o2469[7] →* java.lang.Object(CyclicList(o2499rec[12]))))∧(i568[7] →* i561[12])∧(o2469[7] →* java.lang.Object(CyclicList(o2499rec[12]))))


(8) -> (9), if ((i561[8] + -1 > 0 →* TRUE)∧((o2469[8] →* o2469[9]))∧(i561[8] →* i561[9]))


(9) -> (0), if ((i561[9] + -1 →* i561[0])∧((o2469[9] →* java.lang.Object(CyclicList(o2500[0]))))∧(o2469[9] →* java.lang.Object(CyclicList(o2500[0]))))


(9) -> (3), if (((o2469[9] →* o2469[3]))∧(o2469[9] →* java.lang.Object(CyclicList(o2495[3])))∧(i561[9] + -1 →* i561[3]))


(9) -> (5), if ((i561[9] + -1 →* i561[5])∧((o2469[9] →* o2469[5]))∧(o2469[9] →* java.lang.Object(CyclicList(o2494rec[5]))))


(9) -> (8), if ((o2469[9] →* java.lang.Object(CyclicList(o2469[8])))∧(i561[9] + -1 →* i561[8])∧((o2469[9] →* o2469[8])))


(9) -> (10), if ((i561[9] + -1 →* i561[10])∧((o2469[9] →* o2468rec[10]))∧(o2469[9] →* java.lang.Object(CyclicList(o2468rec[10]))))


(9) -> (12), if ((i561[9] + -1 →* i561[12])∧(o2469[9] →* java.lang.Object(CyclicList(o2499rec[12])))∧((o2469[9] →* java.lang.Object(CyclicList(o2499rec[12])))))


(10) -> (11), if ((i561[10] + -1 > 0 →* TRUE)∧(i561[10] →* i561[11])∧((o2468rec[10] →* o2468rec[11])))


(11) -> (0), if ((i561[11] + -1 →* i561[0])∧((o2468rec[11] →* java.lang.Object(CyclicList(o2500[0]))))∧((o2468rec[11] →* o2500[0])))


(11) -> (3), if ((i561[11] + -1 →* i561[3])∧((o2468rec[11] →* o2469[3]))∧((o2468rec[11] →* o2495[3])))


(11) -> (5), if (((o2468rec[11] →* o2494rec[5]))∧((o2468rec[11] →* o2469[5]))∧(i561[11] + -1 →* i561[5]))


(11) -> (8), if ((i561[11] + -1 →* i561[8])∧((o2468rec[11] →* o2469[8])))


(11) -> (10), if (((o2468rec[11] →* o2468rec[10]))∧(i561[11] + -1 →* i561[10]))


(11) -> (12), if (((o2468rec[11] →* java.lang.Object(CyclicList(o2499rec[12]))))∧(i561[11] + -1 →* i561[12])∧((o2468rec[11] →* o2499rec[12])))


(12) -> (13), if ((i561[12] →* i561[13])∧(i561[12] + -1 > 0 →* TRUE)∧((o2499rec[12] →* o2499rec[13])))


(13) -> (7), if ((i561[13] + -1 →* i568[7])∧(java.lang.Object(CyclicList(o2499rec[13])) →* o2469[7])∧((java.lang.Object(CyclicList(o2499rec[13])) →* o2469[7])))



The set Q consists of the following terms:
Cond_Inc4460(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(x0)))), x1, java.lang.Object(CyclicList(x0)))
JMP4853(java.lang.Object(CyclicList(x0)), x1, x2)
Inc4460(java.lang.Object(CyclicList(x0)), x1, java.lang.Object(CyclicList(x2)))
Cond_Inc44601(TRUE, java.lang.Object(CyclicList(x0)), x1, java.lang.Object(CyclicList(x2)))
Cond_Inc44602(TRUE, java.lang.Object(CyclicList(x0)), x1, java.lang.Object(CyclicList(x2)))
JMP4687(java.lang.Object(CyclicList(x0)), x1, x0)
Cond_Inc44603(TRUE, x0, java.lang.Object(CyclicList(x1)))
Cond_Inc44604(TRUE, x0, java.lang.Object(CyclicList(x1)))
Cond_Inc44605(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(x0)))), x1, java.lang.Object(CyclicList(x0)))

(14) 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 INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500)))), i561, java.lang.Object(CyclicList(o2500))) → COND_INC4460(>(+(i561, -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500)))), i561, java.lang.Object(CyclicList(o2500))) the following chains were created:
  • We consider the chain INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0]))) → COND_INC4460(>(+(i561[0], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0]))), COND_INC4460(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))), i561[1], java.lang.Object(CyclicList(o2500[1]))) → JMP4853'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))), +(i561[1], -1), o2500[1]) which results in the following constraint:

    (1)    (i561[0]=i561[1]∧>(+(i561[0], -1), 0)=TRUE∧o2500[0]=o2500[1] ⇒ INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0])))≥NonInfC∧INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0])))≥COND_INC4460(>(+(i561[0], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0])))∧(UIncreasing(COND_INC4460(>(+(i561[0], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0])))), ≥))



    We simplified constraint (1) using rule (IV) which results in the following new constraint:

    (2)    (>(+(i561[0], -1), 0)=TRUE ⇒ INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0])))≥NonInfC∧INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0])))≥COND_INC4460(>(+(i561[0], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0])))∧(UIncreasing(COND_INC4460(>(+(i561[0], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0])))), ≥))



    We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (3)    (i561[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_INC4460(>(+(i561[0], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0])))), ≥)∧[(-1)Bound*bni_24] + [(2)bni_24]i561[0] ≥ 0∧[(-1)bso_25] ≥ 0)



    We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (4)    (i561[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_INC4460(>(+(i561[0], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0])))), ≥)∧[(-1)Bound*bni_24] + [(2)bni_24]i561[0] ≥ 0∧[(-1)bso_25] ≥ 0)



    We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (5)    (i561[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_INC4460(>(+(i561[0], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0])))), ≥)∧[(-1)Bound*bni_24] + [(2)bni_24]i561[0] ≥ 0∧[(-1)bso_25] ≥ 0)



    We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (6)    (i561[0] ≥ 0 ⇒ (UIncreasing(COND_INC4460(>(+(i561[0], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0])))), ≥)∧[(-1)Bound*bni_24 + (4)bni_24] + [(2)bni_24]i561[0] ≥ 0∧[(-1)bso_25] ≥ 0)







For Pair COND_INC4460(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500)))), i561, java.lang.Object(CyclicList(o2500))) → JMP4853'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500)))), +(i561, -1), o2500) the following chains were created:
  • We consider the chain COND_INC4460(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))), i561[1], java.lang.Object(CyclicList(o2500[1]))) → JMP4853'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))), +(i561[1], -1), o2500[1]) which results in the following constraint:

    (7)    (COND_INC4460(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))), i561[1], java.lang.Object(CyclicList(o2500[1])))≥NonInfC∧COND_INC4460(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))), i561[1], java.lang.Object(CyclicList(o2500[1])))≥JMP4853'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))), +(i561[1], -1), o2500[1])∧(UIncreasing(JMP4853'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))), +(i561[1], -1), o2500[1])), ≥))



    We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (8)    ((UIncreasing(JMP4853'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))), +(i561[1], -1), o2500[1])), ≥)∧[(-1)bso_27] ≥ 0)



    We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (9)    ((UIncreasing(JMP4853'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))), +(i561[1], -1), o2500[1])), ≥)∧[(-1)bso_27] ≥ 0)



    We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (10)    ((UIncreasing(JMP4853'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))), +(i561[1], -1), o2500[1])), ≥)∧[(-1)bso_27] ≥ 0)



    We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (11)    ((UIncreasing(JMP4853'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))), +(i561[1], -1), o2500[1])), ≥)∧0 = 0∧[(-1)bso_27] ≥ 0)







For Pair JMP4853'(java.lang.Object(CyclicList(o2469)), i568, o2495) → INC4460(java.lang.Object(CyclicList(o2469)), i568, o2495) the following chains were created:
  • We consider the chain JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2]) → INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2]), INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0]))) → COND_INC4460(>(+(i561[0], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0]))) which results in the following constraint:

    (12)    (o2495[2]=java.lang.Object(CyclicList(o2500[0]))∧o2469[2]=java.lang.Object(CyclicList(o2500[0]))∧i568[2]=i561[0] ⇒ JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])≥NonInfC∧JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])≥INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥))



    We simplified constraint (12) using rules (III), (IV) which results in the following new constraint:

    (13)    (JMP4853'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i568[2], java.lang.Object(CyclicList(o2500[0])))≥NonInfC∧JMP4853'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i568[2], java.lang.Object(CyclicList(o2500[0])))≥INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i568[2], java.lang.Object(CyclicList(o2500[0])))∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥))



    We simplified constraint (13) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (14)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧[2 + (-1)bso_29] ≥ 0)



    We simplified constraint (14) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (15)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧[2 + (-1)bso_29] ≥ 0)



    We simplified constraint (15) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (16)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧[2 + (-1)bso_29] ≥ 0)



    We simplified constraint (16) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (17)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧0 = 0∧[2 + (-1)bso_29] ≥ 0)



  • We consider the chain JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2]) → INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2]), INC4460(java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3]))) → COND_INC44601(>(+(i561[3], -1), 0), java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3]))) which results in the following constraint:

    (18)    (o2469[2]=o2469[3]∧i568[2]=i561[3]∧o2495[2]=java.lang.Object(CyclicList(o2495[3])) ⇒ JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])≥NonInfC∧JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])≥INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥))



    We simplified constraint (18) using rules (III), (IV) which results in the following new constraint:

    (19)    (JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], java.lang.Object(CyclicList(o2495[3])))≥NonInfC∧JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], java.lang.Object(CyclicList(o2495[3])))≥INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], java.lang.Object(CyclicList(o2495[3])))∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥))



    We simplified constraint (19) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (20)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧[2 + (-1)bso_29] ≥ 0)



    We simplified constraint (20) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (21)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧[2 + (-1)bso_29] ≥ 0)



    We simplified constraint (21) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (22)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧[2 + (-1)bso_29] ≥ 0)



    We simplified constraint (22) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (23)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧0 = 0∧[2 + (-1)bso_29] ≥ 0)



  • We consider the chain JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2]) → INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2]), INC4460(java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5]))) → COND_INC44602(>(+(i561[5], -1), 0), java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5]))) which results in the following constraint:

    (24)    (o2469[2]=o2469[5]∧i568[2]=i561[5]∧o2495[2]=java.lang.Object(CyclicList(o2494rec[5])) ⇒ JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])≥NonInfC∧JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])≥INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥))



    We simplified constraint (24) using rules (III), (IV) which results in the following new constraint:

    (25)    (JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], java.lang.Object(CyclicList(o2494rec[5])))≥NonInfC∧JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], java.lang.Object(CyclicList(o2494rec[5])))≥INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], java.lang.Object(CyclicList(o2494rec[5])))∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥))



    We simplified constraint (25) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (26)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧[2 + (-1)bso_29] ≥ 0)



    We simplified constraint (26) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (27)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧[2 + (-1)bso_29] ≥ 0)



    We simplified constraint (27) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (28)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧[2 + (-1)bso_29] ≥ 0)



    We simplified constraint (28) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (29)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧0 = 0∧[2 + (-1)bso_29] ≥ 0)



  • We consider the chain JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2]) → INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2]), INC4460(java.lang.Object(CyclicList(o2469[8])), i561[8], java.lang.Object(CyclicList(o2469[8]))) → COND_INC44603(>(+(i561[8], -1), 0), i561[8], java.lang.Object(CyclicList(o2469[8]))) which results in the following constraint:

    (30)    (i568[2]=i561[8]∧o2469[2]=o2469[8]∧o2495[2]=java.lang.Object(CyclicList(o2469[8])) ⇒ JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])≥NonInfC∧JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])≥INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥))



    We simplified constraint (30) using rules (III), (IV) which results in the following new constraint:

    (31)    (JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], java.lang.Object(CyclicList(o2469[2])))≥NonInfC∧JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], java.lang.Object(CyclicList(o2469[2])))≥INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], java.lang.Object(CyclicList(o2469[2])))∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥))



    We simplified constraint (31) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (32)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧[2 + (-1)bso_29] ≥ 0)



    We simplified constraint (32) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (33)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧[2 + (-1)bso_29] ≥ 0)



    We simplified constraint (33) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (34)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧[2 + (-1)bso_29] ≥ 0)



    We simplified constraint (34) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (35)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧0 = 0∧[2 + (-1)bso_29] ≥ 0)



  • We consider the chain JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2]) → INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2]), INC4460(java.lang.Object(CyclicList(o2468rec[10])), i561[10], java.lang.Object(CyclicList(o2468rec[10]))) → COND_INC44604(>(+(i561[10], -1), 0), i561[10], java.lang.Object(CyclicList(o2468rec[10]))) which results in the following constraint:

    (36)    (o2495[2]=java.lang.Object(CyclicList(o2468rec[10]))∧o2469[2]=o2468rec[10]∧i568[2]=i561[10] ⇒ JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])≥NonInfC∧JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])≥INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥))



    We simplified constraint (36) using rules (III), (IV) which results in the following new constraint:

    (37)    (JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], java.lang.Object(CyclicList(o2469[2])))≥NonInfC∧JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], java.lang.Object(CyclicList(o2469[2])))≥INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], java.lang.Object(CyclicList(o2469[2])))∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥))



    We simplified constraint (37) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (38)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧[2 + (-1)bso_29] ≥ 0)



    We simplified constraint (38) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (39)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧[2 + (-1)bso_29] ≥ 0)



    We simplified constraint (39) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (40)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧[2 + (-1)bso_29] ≥ 0)



    We simplified constraint (40) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (41)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧0 = 0∧[2 + (-1)bso_29] ≥ 0)



  • We consider the chain JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2]) → INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2]), INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12]))) → COND_INC44605(>(+(i561[12], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12]))) which results in the following constraint:

    (42)    (o2495[2]=java.lang.Object(CyclicList(o2499rec[12]))∧o2469[2]=java.lang.Object(CyclicList(o2499rec[12]))∧i568[2]=i561[12] ⇒ JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])≥NonInfC∧JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])≥INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥))



    We simplified constraint (42) using rules (III), (IV) which results in the following new constraint:

    (43)    (JMP4853'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i568[2], java.lang.Object(CyclicList(o2499rec[12])))≥NonInfC∧JMP4853'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i568[2], java.lang.Object(CyclicList(o2499rec[12])))≥INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i568[2], java.lang.Object(CyclicList(o2499rec[12])))∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥))



    We simplified constraint (43) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (44)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧[2 + (-1)bso_29] ≥ 0)



    We simplified constraint (44) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (45)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧[2 + (-1)bso_29] ≥ 0)



    We simplified constraint (45) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (46)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧[2 + (-1)bso_29] ≥ 0)



    We simplified constraint (46) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (47)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧0 = 0∧[2 + (-1)bso_29] ≥ 0)







For Pair INC4460(java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2495))) → COND_INC44601(>(+(i561, -1), 0), java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2495))) the following chains were created:
  • We consider the chain INC4460(java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3]))) → COND_INC44601(>(+(i561[3], -1), 0), java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3]))), COND_INC44601(TRUE, java.lang.Object(CyclicList(o2469[4])), i561[4], java.lang.Object(CyclicList(o2495[4]))) → INC4460(java.lang.Object(CyclicList(o2469[4])), +(i561[4], -1), o2495[4]) which results in the following constraint:

    (48)    (i561[3]=i561[4]∧>(+(i561[3], -1), 0)=TRUE∧o2495[3]=o2495[4]∧o2469[3]=o2469[4] ⇒ INC4460(java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3])))≥NonInfC∧INC4460(java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3])))≥COND_INC44601(>(+(i561[3], -1), 0), java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3])))∧(UIncreasing(COND_INC44601(>(+(i561[3], -1), 0), java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3])))), ≥))



    We simplified constraint (48) using rule (IV) which results in the following new constraint:

    (49)    (>(+(i561[3], -1), 0)=TRUE ⇒ INC4460(java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3])))≥NonInfC∧INC4460(java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3])))≥COND_INC44601(>(+(i561[3], -1), 0), java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3])))∧(UIncreasing(COND_INC44601(>(+(i561[3], -1), 0), java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3])))), ≥))



    We simplified constraint (49) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (50)    (i561[3] + [-2] ≥ 0 ⇒ (UIncreasing(COND_INC44601(>(+(i561[3], -1), 0), java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3])))), ≥)∧[(-1)Bound*bni_30] + [(2)bni_30]i561[3] ≥ 0∧[(-1)bso_31] ≥ 0)



    We simplified constraint (50) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (51)    (i561[3] + [-2] ≥ 0 ⇒ (UIncreasing(COND_INC44601(>(+(i561[3], -1), 0), java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3])))), ≥)∧[(-1)Bound*bni_30] + [(2)bni_30]i561[3] ≥ 0∧[(-1)bso_31] ≥ 0)



    We simplified constraint (51) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (52)    (i561[3] + [-2] ≥ 0 ⇒ (UIncreasing(COND_INC44601(>(+(i561[3], -1), 0), java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3])))), ≥)∧[(-1)Bound*bni_30] + [(2)bni_30]i561[3] ≥ 0∧[(-1)bso_31] ≥ 0)



    We simplified constraint (52) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (53)    (i561[3] ≥ 0 ⇒ (UIncreasing(COND_INC44601(>(+(i561[3], -1), 0), java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3])))), ≥)∧[(-1)Bound*bni_30 + (4)bni_30] + [(2)bni_30]i561[3] ≥ 0∧[(-1)bso_31] ≥ 0)







For Pair COND_INC44601(TRUE, java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2495))) → INC4460(java.lang.Object(CyclicList(o2469)), +(i561, -1), o2495) the following chains were created:
  • We consider the chain COND_INC44601(TRUE, java.lang.Object(CyclicList(o2469[4])), i561[4], java.lang.Object(CyclicList(o2495[4]))) → INC4460(java.lang.Object(CyclicList(o2469[4])), +(i561[4], -1), o2495[4]) which results in the following constraint:

    (54)    (COND_INC44601(TRUE, java.lang.Object(CyclicList(o2469[4])), i561[4], java.lang.Object(CyclicList(o2495[4])))≥NonInfC∧COND_INC44601(TRUE, java.lang.Object(CyclicList(o2469[4])), i561[4], java.lang.Object(CyclicList(o2495[4])))≥INC4460(java.lang.Object(CyclicList(o2469[4])), +(i561[4], -1), o2495[4])∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[4])), +(i561[4], -1), o2495[4])), ≥))



    We simplified constraint (54) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (55)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[4])), +(i561[4], -1), o2495[4])), ≥)∧[2 + (-1)bso_33] ≥ 0)



    We simplified constraint (55) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (56)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[4])), +(i561[4], -1), o2495[4])), ≥)∧[2 + (-1)bso_33] ≥ 0)



    We simplified constraint (56) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (57)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[4])), +(i561[4], -1), o2495[4])), ≥)∧[2 + (-1)bso_33] ≥ 0)



    We simplified constraint (57) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (58)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[4])), +(i561[4], -1), o2495[4])), ≥)∧0 = 0∧[2 + (-1)bso_33] ≥ 0)







For Pair INC4460(java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2494rec))) → COND_INC44602(>(+(i561, -1), 0), java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2494rec))) the following chains were created:
  • We consider the chain INC4460(java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5]))) → COND_INC44602(>(+(i561[5], -1), 0), java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5]))), COND_INC44602(TRUE, java.lang.Object(CyclicList(o2469[6])), i561[6], java.lang.Object(CyclicList(o2494rec[6]))) → INC4460(java.lang.Object(CyclicList(o2469[6])), +(i561[6], -1), java.lang.Object(CyclicList(o2494rec[6]))) which results in the following constraint:

    (59)    (o2494rec[5]=o2494rec[6]∧i561[5]=i561[6]∧>(+(i561[5], -1), 0)=TRUE∧o2469[5]=o2469[6] ⇒ INC4460(java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5])))≥NonInfC∧INC4460(java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5])))≥COND_INC44602(>(+(i561[5], -1), 0), java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5])))∧(UIncreasing(COND_INC44602(>(+(i561[5], -1), 0), java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5])))), ≥))



    We simplified constraint (59) using rule (IV) which results in the following new constraint:

    (60)    (>(+(i561[5], -1), 0)=TRUE ⇒ INC4460(java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5])))≥NonInfC∧INC4460(java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5])))≥COND_INC44602(>(+(i561[5], -1), 0), java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5])))∧(UIncreasing(COND_INC44602(>(+(i561[5], -1), 0), java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5])))), ≥))



    We simplified constraint (60) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (61)    (i561[5] + [-2] ≥ 0 ⇒ (UIncreasing(COND_INC44602(>(+(i561[5], -1), 0), java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5])))), ≥)∧[(-1)Bound*bni_34] + [(2)bni_34]i561[5] ≥ 0∧[(-1)bso_35] ≥ 0)



    We simplified constraint (61) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (62)    (i561[5] + [-2] ≥ 0 ⇒ (UIncreasing(COND_INC44602(>(+(i561[5], -1), 0), java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5])))), ≥)∧[(-1)Bound*bni_34] + [(2)bni_34]i561[5] ≥ 0∧[(-1)bso_35] ≥ 0)



    We simplified constraint (62) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (63)    (i561[5] + [-2] ≥ 0 ⇒ (UIncreasing(COND_INC44602(>(+(i561[5], -1), 0), java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5])))), ≥)∧[(-1)Bound*bni_34] + [(2)bni_34]i561[5] ≥ 0∧[(-1)bso_35] ≥ 0)



    We simplified constraint (63) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (64)    (i561[5] ≥ 0 ⇒ (UIncreasing(COND_INC44602(>(+(i561[5], -1), 0), java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5])))), ≥)∧[(-1)Bound*bni_34 + (4)bni_34] + [(2)bni_34]i561[5] ≥ 0∧[(-1)bso_35] ≥ 0)







For Pair COND_INC44602(TRUE, java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2494rec))) → INC4460(java.lang.Object(CyclicList(o2469)), +(i561, -1), java.lang.Object(CyclicList(o2494rec))) the following chains were created:
  • We consider the chain COND_INC44602(TRUE, java.lang.Object(CyclicList(o2469[6])), i561[6], java.lang.Object(CyclicList(o2494rec[6]))) → INC4460(java.lang.Object(CyclicList(o2469[6])), +(i561[6], -1), java.lang.Object(CyclicList(o2494rec[6]))) which results in the following constraint:

    (65)    (COND_INC44602(TRUE, java.lang.Object(CyclicList(o2469[6])), i561[6], java.lang.Object(CyclicList(o2494rec[6])))≥NonInfC∧COND_INC44602(TRUE, java.lang.Object(CyclicList(o2469[6])), i561[6], java.lang.Object(CyclicList(o2494rec[6])))≥INC4460(java.lang.Object(CyclicList(o2469[6])), +(i561[6], -1), java.lang.Object(CyclicList(o2494rec[6])))∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[6])), +(i561[6], -1), java.lang.Object(CyclicList(o2494rec[6])))), ≥))



    We simplified constraint (65) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (66)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[6])), +(i561[6], -1), java.lang.Object(CyclicList(o2494rec[6])))), ≥)∧[2 + (-1)bso_37] ≥ 0)



    We simplified constraint (66) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (67)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[6])), +(i561[6], -1), java.lang.Object(CyclicList(o2494rec[6])))), ≥)∧[2 + (-1)bso_37] ≥ 0)



    We simplified constraint (67) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (68)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[6])), +(i561[6], -1), java.lang.Object(CyclicList(o2494rec[6])))), ≥)∧[2 + (-1)bso_37] ≥ 0)



    We simplified constraint (68) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (69)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[6])), +(i561[6], -1), java.lang.Object(CyclicList(o2494rec[6])))), ≥)∧0 = 0∧[2 + (-1)bso_37] ≥ 0)







For Pair JMP4687'(java.lang.Object(CyclicList(o2469)), i568, o2469) → INC4460(java.lang.Object(CyclicList(o2469)), i568, o2469) the following chains were created:
  • We consider the chain JMP4687'(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7]) → INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7]), INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0]))) → COND_INC4460(>(+(i561[0], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0]))) which results in the following constraint:

    (70)    (o2469[7]=java.lang.Object(CyclicList(o2500[0]))∧i568[7]=i561[0] ⇒ JMP4687'(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])≥NonInfC∧JMP4687'(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])≥INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥))



    We simplified constraint (70) using rules (III), (IV) which results in the following new constraint:

    (71)    (JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i568[7], java.lang.Object(CyclicList(o2500[0])))≥NonInfC∧JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i568[7], java.lang.Object(CyclicList(o2500[0])))≥INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i568[7], java.lang.Object(CyclicList(o2500[0])))∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥))



    We simplified constraint (71) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (72)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧[(-1)bso_39] ≥ 0)



    We simplified constraint (72) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (73)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧[(-1)bso_39] ≥ 0)



    We simplified constraint (73) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (74)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧[(-1)bso_39] ≥ 0)



    We simplified constraint (74) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (75)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧0 = 0∧[(-1)bso_39] ≥ 0)



  • We consider the chain JMP4687'(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7]) → INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7]), INC4460(java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3]))) → COND_INC44601(>(+(i561[3], -1), 0), java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3]))) which results in the following constraint:

    (76)    (o2469[7]=java.lang.Object(CyclicList(o2495[3]))∧i568[7]=i561[3]∧o2469[7]=o2469[3] ⇒ JMP4687'(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])≥NonInfC∧JMP4687'(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])≥INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥))



    We simplified constraint (76) using rules (III), (IV) which results in the following new constraint:

    (77)    (JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2495[3])))), i568[7], java.lang.Object(CyclicList(o2495[3])))≥NonInfC∧JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2495[3])))), i568[7], java.lang.Object(CyclicList(o2495[3])))≥INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2495[3])))), i568[7], java.lang.Object(CyclicList(o2495[3])))∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥))



    We simplified constraint (77) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (78)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧[(-1)bso_39] ≥ 0)



    We simplified constraint (78) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (79)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧[(-1)bso_39] ≥ 0)



    We simplified constraint (79) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (80)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧[(-1)bso_39] ≥ 0)



    We simplified constraint (80) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (81)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧0 = 0∧[(-1)bso_39] ≥ 0)



  • We consider the chain JMP4687'(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7]) → INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7]), INC4460(java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5]))) → COND_INC44602(>(+(i561[5], -1), 0), java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5]))) which results in the following constraint:

    (82)    (i568[7]=i561[5]∧o2469[7]=o2469[5]∧o2469[7]=java.lang.Object(CyclicList(o2494rec[5])) ⇒ JMP4687'(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])≥NonInfC∧JMP4687'(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])≥INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥))



    We simplified constraint (82) using rules (III), (IV) which results in the following new constraint:

    (83)    (JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2494rec[5])))), i568[7], java.lang.Object(CyclicList(o2494rec[5])))≥NonInfC∧JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2494rec[5])))), i568[7], java.lang.Object(CyclicList(o2494rec[5])))≥INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2494rec[5])))), i568[7], java.lang.Object(CyclicList(o2494rec[5])))∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥))



    We simplified constraint (83) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (84)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧[(-1)bso_39] ≥ 0)



    We simplified constraint (84) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (85)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧[(-1)bso_39] ≥ 0)



    We simplified constraint (85) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (86)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧[(-1)bso_39] ≥ 0)



    We simplified constraint (86) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (87)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧0 = 0∧[(-1)bso_39] ≥ 0)



  • We consider the chain JMP4687'(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7]) → INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7]), INC4460(java.lang.Object(CyclicList(o2469[8])), i561[8], java.lang.Object(CyclicList(o2469[8]))) → COND_INC44603(>(+(i561[8], -1), 0), i561[8], java.lang.Object(CyclicList(o2469[8]))) which results in the following constraint:

    (88)    (o2469[7]=java.lang.Object(CyclicList(o2469[8]))∧i568[7]=i561[8]∧o2469[7]=o2469[8] ⇒ JMP4687'(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])≥NonInfC∧JMP4687'(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])≥INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥))



    We simplified constraint (88) using rules (III), (IV) which results in the following new constraint:

    (89)    (JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2469[7])))), i568[7], java.lang.Object(CyclicList(o2469[7])))≥NonInfC∧JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2469[7])))), i568[7], java.lang.Object(CyclicList(o2469[7])))≥INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2469[7])))), i568[7], java.lang.Object(CyclicList(o2469[7])))∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥))



    We simplified constraint (89) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (90)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧[(-1)bso_39] ≥ 0)



    We simplified constraint (90) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (91)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧[(-1)bso_39] ≥ 0)



    We simplified constraint (91) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (92)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧[(-1)bso_39] ≥ 0)



    We simplified constraint (92) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (93)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧0 = 0∧[(-1)bso_39] ≥ 0)



  • We consider the chain JMP4687'(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7]) → INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7]), INC4460(java.lang.Object(CyclicList(o2468rec[10])), i561[10], java.lang.Object(CyclicList(o2468rec[10]))) → COND_INC44604(>(+(i561[10], -1), 0), i561[10], java.lang.Object(CyclicList(o2468rec[10]))) which results in the following constraint:

    (94)    (o2469[7]=o2468rec[10]∧i568[7]=i561[10]∧o2469[7]=java.lang.Object(CyclicList(o2468rec[10])) ⇒ JMP4687'(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])≥NonInfC∧JMP4687'(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])≥INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥))



    We simplified constraint (94) using rules (III), (IV) which results in the following new constraint:

    (95)    (JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2469[7])))), i568[7], java.lang.Object(CyclicList(o2469[7])))≥NonInfC∧JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2469[7])))), i568[7], java.lang.Object(CyclicList(o2469[7])))≥INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2469[7])))), i568[7], java.lang.Object(CyclicList(o2469[7])))∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥))



    We simplified constraint (95) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (96)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧[(-1)bso_39] ≥ 0)



    We simplified constraint (96) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (97)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧[(-1)bso_39] ≥ 0)



    We simplified constraint (97) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (98)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧[(-1)bso_39] ≥ 0)



    We simplified constraint (98) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (99)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧0 = 0∧[(-1)bso_39] ≥ 0)



  • We consider the chain JMP4687'(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7]) → INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7]), INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12]))) → COND_INC44605(>(+(i561[12], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12]))) which results in the following constraint:

    (100)    (o2469[7]=java.lang.Object(CyclicList(o2499rec[12]))∧i568[7]=i561[12] ⇒ JMP4687'(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])≥NonInfC∧JMP4687'(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])≥INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥))



    We simplified constraint (100) using rules (III), (IV) which results in the following new constraint:

    (101)    (JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i568[7], java.lang.Object(CyclicList(o2499rec[12])))≥NonInfC∧JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i568[7], java.lang.Object(CyclicList(o2499rec[12])))≥INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i568[7], java.lang.Object(CyclicList(o2499rec[12])))∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥))



    We simplified constraint (101) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (102)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧[(-1)bso_39] ≥ 0)



    We simplified constraint (102) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (103)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧[(-1)bso_39] ≥ 0)



    We simplified constraint (103) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (104)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧[(-1)bso_39] ≥ 0)



    We simplified constraint (104) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (105)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧0 = 0∧[(-1)bso_39] ≥ 0)







For Pair INC4460(java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2469))) → COND_INC44603(>(+(i561, -1), 0), i561, java.lang.Object(CyclicList(o2469))) the following chains were created:
  • We consider the chain INC4460(java.lang.Object(CyclicList(o2469[8])), i561[8], java.lang.Object(CyclicList(o2469[8]))) → COND_INC44603(>(+(i561[8], -1), 0), i561[8], java.lang.Object(CyclicList(o2469[8]))), COND_INC44603(TRUE, i561[9], java.lang.Object(CyclicList(o2469[9]))) → INC4460(java.lang.Object(CyclicList(o2469[9])), +(i561[9], -1), o2469[9]) which results in the following constraint:

    (106)    (>(+(i561[8], -1), 0)=TRUE∧o2469[8]=o2469[9]∧i561[8]=i561[9] ⇒ INC4460(java.lang.Object(CyclicList(o2469[8])), i561[8], java.lang.Object(CyclicList(o2469[8])))≥NonInfC∧INC4460(java.lang.Object(CyclicList(o2469[8])), i561[8], java.lang.Object(CyclicList(o2469[8])))≥COND_INC44603(>(+(i561[8], -1), 0), i561[8], java.lang.Object(CyclicList(o2469[8])))∧(UIncreasing(COND_INC44603(>(+(i561[8], -1), 0), i561[8], java.lang.Object(CyclicList(o2469[8])))), ≥))



    We simplified constraint (106) using rule (IV) which results in the following new constraint:

    (107)    (>(+(i561[8], -1), 0)=TRUE ⇒ INC4460(java.lang.Object(CyclicList(o2469[8])), i561[8], java.lang.Object(CyclicList(o2469[8])))≥NonInfC∧INC4460(java.lang.Object(CyclicList(o2469[8])), i561[8], java.lang.Object(CyclicList(o2469[8])))≥COND_INC44603(>(+(i561[8], -1), 0), i561[8], java.lang.Object(CyclicList(o2469[8])))∧(UIncreasing(COND_INC44603(>(+(i561[8], -1), 0), i561[8], java.lang.Object(CyclicList(o2469[8])))), ≥))



    We simplified constraint (107) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (108)    (i561[8] + [-2] ≥ 0 ⇒ (UIncreasing(COND_INC44603(>(+(i561[8], -1), 0), i561[8], java.lang.Object(CyclicList(o2469[8])))), ≥)∧[(-1)Bound*bni_40] + [(2)bni_40]i561[8] ≥ 0∧[1 + (-1)bso_41] ≥ 0)



    We simplified constraint (108) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (109)    (i561[8] + [-2] ≥ 0 ⇒ (UIncreasing(COND_INC44603(>(+(i561[8], -1), 0), i561[8], java.lang.Object(CyclicList(o2469[8])))), ≥)∧[(-1)Bound*bni_40] + [(2)bni_40]i561[8] ≥ 0∧[1 + (-1)bso_41] ≥ 0)



    We simplified constraint (109) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (110)    (i561[8] + [-2] ≥ 0 ⇒ (UIncreasing(COND_INC44603(>(+(i561[8], -1), 0), i561[8], java.lang.Object(CyclicList(o2469[8])))), ≥)∧[(-1)Bound*bni_40] + [(2)bni_40]i561[8] ≥ 0∧[1 + (-1)bso_41] ≥ 0)



    We simplified constraint (110) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (111)    (i561[8] ≥ 0 ⇒ (UIncreasing(COND_INC44603(>(+(i561[8], -1), 0), i561[8], java.lang.Object(CyclicList(o2469[8])))), ≥)∧[(-1)Bound*bni_40 + (4)bni_40] + [(2)bni_40]i561[8] ≥ 0∧[1 + (-1)bso_41] ≥ 0)







For Pair COND_INC44603(TRUE, i561, java.lang.Object(CyclicList(o2469))) → INC4460(java.lang.Object(CyclicList(o2469)), +(i561, -1), o2469) the following chains were created:
  • We consider the chain COND_INC44603(TRUE, i561[9], java.lang.Object(CyclicList(o2469[9]))) → INC4460(java.lang.Object(CyclicList(o2469[9])), +(i561[9], -1), o2469[9]) which results in the following constraint:

    (112)    (COND_INC44603(TRUE, i561[9], java.lang.Object(CyclicList(o2469[9])))≥NonInfC∧COND_INC44603(TRUE, i561[9], java.lang.Object(CyclicList(o2469[9])))≥INC4460(java.lang.Object(CyclicList(o2469[9])), +(i561[9], -1), o2469[9])∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[9])), +(i561[9], -1), o2469[9])), ≥))



    We simplified constraint (112) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (113)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[9])), +(i561[9], -1), o2469[9])), ≥)∧[1 + (-1)bso_43] ≥ 0)



    We simplified constraint (113) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (114)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[9])), +(i561[9], -1), o2469[9])), ≥)∧[1 + (-1)bso_43] ≥ 0)



    We simplified constraint (114) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (115)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[9])), +(i561[9], -1), o2469[9])), ≥)∧[1 + (-1)bso_43] ≥ 0)



    We simplified constraint (115) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (116)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[9])), +(i561[9], -1), o2469[9])), ≥)∧0 = 0∧[1 + (-1)bso_43] ≥ 0)







For Pair INC4460(java.lang.Object(CyclicList(o2468rec)), i561, java.lang.Object(CyclicList(o2468rec))) → COND_INC44604(>(+(i561, -1), 0), i561, java.lang.Object(CyclicList(o2468rec))) the following chains were created:
  • We consider the chain INC4460(java.lang.Object(CyclicList(o2468rec[10])), i561[10], java.lang.Object(CyclicList(o2468rec[10]))) → COND_INC44604(>(+(i561[10], -1), 0), i561[10], java.lang.Object(CyclicList(o2468rec[10]))), COND_INC44604(TRUE, i561[11], java.lang.Object(CyclicList(o2468rec[11]))) → INC4460(java.lang.Object(CyclicList(o2468rec[11])), +(i561[11], -1), java.lang.Object(CyclicList(o2468rec[11]))) which results in the following constraint:

    (117)    (>(+(i561[10], -1), 0)=TRUE∧i561[10]=i561[11]∧o2468rec[10]=o2468rec[11] ⇒ INC4460(java.lang.Object(CyclicList(o2468rec[10])), i561[10], java.lang.Object(CyclicList(o2468rec[10])))≥NonInfC∧INC4460(java.lang.Object(CyclicList(o2468rec[10])), i561[10], java.lang.Object(CyclicList(o2468rec[10])))≥COND_INC44604(>(+(i561[10], -1), 0), i561[10], java.lang.Object(CyclicList(o2468rec[10])))∧(UIncreasing(COND_INC44604(>(+(i561[10], -1), 0), i561[10], java.lang.Object(CyclicList(o2468rec[10])))), ≥))



    We simplified constraint (117) using rule (IV) which results in the following new constraint:

    (118)    (>(+(i561[10], -1), 0)=TRUE ⇒ INC4460(java.lang.Object(CyclicList(o2468rec[10])), i561[10], java.lang.Object(CyclicList(o2468rec[10])))≥NonInfC∧INC4460(java.lang.Object(CyclicList(o2468rec[10])), i561[10], java.lang.Object(CyclicList(o2468rec[10])))≥COND_INC44604(>(+(i561[10], -1), 0), i561[10], java.lang.Object(CyclicList(o2468rec[10])))∧(UIncreasing(COND_INC44604(>(+(i561[10], -1), 0), i561[10], java.lang.Object(CyclicList(o2468rec[10])))), ≥))



    We simplified constraint (118) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (119)    (i561[10] + [-2] ≥ 0 ⇒ (UIncreasing(COND_INC44604(>(+(i561[10], -1), 0), i561[10], java.lang.Object(CyclicList(o2468rec[10])))), ≥)∧[(-1)Bound*bni_44] + [(2)bni_44]i561[10] ≥ 0∧[1 + (-1)bso_45] ≥ 0)



    We simplified constraint (119) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (120)    (i561[10] + [-2] ≥ 0 ⇒ (UIncreasing(COND_INC44604(>(+(i561[10], -1), 0), i561[10], java.lang.Object(CyclicList(o2468rec[10])))), ≥)∧[(-1)Bound*bni_44] + [(2)bni_44]i561[10] ≥ 0∧[1 + (-1)bso_45] ≥ 0)



    We simplified constraint (120) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (121)    (i561[10] + [-2] ≥ 0 ⇒ (UIncreasing(COND_INC44604(>(+(i561[10], -1), 0), i561[10], java.lang.Object(CyclicList(o2468rec[10])))), ≥)∧[(-1)Bound*bni_44] + [(2)bni_44]i561[10] ≥ 0∧[1 + (-1)bso_45] ≥ 0)



    We simplified constraint (121) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (122)    (i561[10] ≥ 0 ⇒ (UIncreasing(COND_INC44604(>(+(i561[10], -1), 0), i561[10], java.lang.Object(CyclicList(o2468rec[10])))), ≥)∧[(-1)Bound*bni_44 + (4)bni_44] + [(2)bni_44]i561[10] ≥ 0∧[1 + (-1)bso_45] ≥ 0)







For Pair COND_INC44604(TRUE, i561, java.lang.Object(CyclicList(o2468rec))) → INC4460(java.lang.Object(CyclicList(o2468rec)), +(i561, -1), java.lang.Object(CyclicList(o2468rec))) the following chains were created:
  • We consider the chain COND_INC44604(TRUE, i561[11], java.lang.Object(CyclicList(o2468rec[11]))) → INC4460(java.lang.Object(CyclicList(o2468rec[11])), +(i561[11], -1), java.lang.Object(CyclicList(o2468rec[11]))) which results in the following constraint:

    (123)    (COND_INC44604(TRUE, i561[11], java.lang.Object(CyclicList(o2468rec[11])))≥NonInfC∧COND_INC44604(TRUE, i561[11], java.lang.Object(CyclicList(o2468rec[11])))≥INC4460(java.lang.Object(CyclicList(o2468rec[11])), +(i561[11], -1), java.lang.Object(CyclicList(o2468rec[11])))∧(UIncreasing(INC4460(java.lang.Object(CyclicList(o2468rec[11])), +(i561[11], -1), java.lang.Object(CyclicList(o2468rec[11])))), ≥))



    We simplified constraint (123) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (124)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2468rec[11])), +(i561[11], -1), java.lang.Object(CyclicList(o2468rec[11])))), ≥)∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (124) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (125)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2468rec[11])), +(i561[11], -1), java.lang.Object(CyclicList(o2468rec[11])))), ≥)∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (125) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (126)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2468rec[11])), +(i561[11], -1), java.lang.Object(CyclicList(o2468rec[11])))), ≥)∧[1 + (-1)bso_47] ≥ 0)



    We simplified constraint (126) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (127)    ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2468rec[11])), +(i561[11], -1), java.lang.Object(CyclicList(o2468rec[11])))), ≥)∧0 = 0∧[1 + (-1)bso_47] ≥ 0)







For Pair INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec)))), i561, java.lang.Object(CyclicList(o2499rec))) → COND_INC44605(>(+(i561, -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec)))), i561, java.lang.Object(CyclicList(o2499rec))) the following chains were created:
  • We consider the chain INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12]))) → COND_INC44605(>(+(i561[12], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12]))), COND_INC44605(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13])))), i561[13], java.lang.Object(CyclicList(o2499rec[13]))) → JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13])))), +(i561[13], -1), java.lang.Object(CyclicList(o2499rec[13]))) which results in the following constraint:

    (128)    (i561[12]=i561[13]∧>(+(i561[12], -1), 0)=TRUE∧o2499rec[12]=o2499rec[13] ⇒ INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12])))≥NonInfC∧INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12])))≥COND_INC44605(>(+(i561[12], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12])))∧(UIncreasing(COND_INC44605(>(+(i561[12], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12])))), ≥))



    We simplified constraint (128) using rule (IV) which results in the following new constraint:

    (129)    (>(+(i561[12], -1), 0)=TRUE ⇒ INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12])))≥NonInfC∧INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12])))≥COND_INC44605(>(+(i561[12], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12])))∧(UIncreasing(COND_INC44605(>(+(i561[12], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12])))), ≥))



    We simplified constraint (129) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (130)    (i561[12] + [-2] ≥ 0 ⇒ (UIncreasing(COND_INC44605(>(+(i561[12], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12])))), ≥)∧[(-1)Bound*bni_48] + [(2)bni_48]i561[12] ≥ 0∧[1 + (-1)bso_49] ≥ 0)



    We simplified constraint (130) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (131)    (i561[12] + [-2] ≥ 0 ⇒ (UIncreasing(COND_INC44605(>(+(i561[12], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12])))), ≥)∧[(-1)Bound*bni_48] + [(2)bni_48]i561[12] ≥ 0∧[1 + (-1)bso_49] ≥ 0)



    We simplified constraint (131) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (132)    (i561[12] + [-2] ≥ 0 ⇒ (UIncreasing(COND_INC44605(>(+(i561[12], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12])))), ≥)∧[(-1)Bound*bni_48] + [(2)bni_48]i561[12] ≥ 0∧[1 + (-1)bso_49] ≥ 0)



    We simplified constraint (132) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (133)    (i561[12] ≥ 0 ⇒ (UIncreasing(COND_INC44605(>(+(i561[12], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12])))), ≥)∧[(-1)Bound*bni_48 + (4)bni_48] + [(2)bni_48]i561[12] ≥ 0∧[1 + (-1)bso_49] ≥ 0)







For Pair COND_INC44605(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec)))), i561, java.lang.Object(CyclicList(o2499rec))) → JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec)))), +(i561, -1), java.lang.Object(CyclicList(o2499rec))) the following chains were created:
  • We consider the chain COND_INC44605(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13])))), i561[13], java.lang.Object(CyclicList(o2499rec[13]))) → JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13])))), +(i561[13], -1), java.lang.Object(CyclicList(o2499rec[13]))) which results in the following constraint:

    (134)    (COND_INC44605(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13])))), i561[13], java.lang.Object(CyclicList(o2499rec[13])))≥NonInfC∧COND_INC44605(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13])))), i561[13], java.lang.Object(CyclicList(o2499rec[13])))≥JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13])))), +(i561[13], -1), java.lang.Object(CyclicList(o2499rec[13])))∧(UIncreasing(JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13])))), +(i561[13], -1), java.lang.Object(CyclicList(o2499rec[13])))), ≥))



    We simplified constraint (134) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (135)    ((UIncreasing(JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13])))), +(i561[13], -1), java.lang.Object(CyclicList(o2499rec[13])))), ≥)∧[1 + (-1)bso_51] ≥ 0)



    We simplified constraint (135) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (136)    ((UIncreasing(JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13])))), +(i561[13], -1), java.lang.Object(CyclicList(o2499rec[13])))), ≥)∧[1 + (-1)bso_51] ≥ 0)



    We simplified constraint (136) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (137)    ((UIncreasing(JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13])))), +(i561[13], -1), java.lang.Object(CyclicList(o2499rec[13])))), ≥)∧[1 + (-1)bso_51] ≥ 0)



    We simplified constraint (137) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (138)    ((UIncreasing(JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13])))), +(i561[13], -1), java.lang.Object(CyclicList(o2499rec[13])))), ≥)∧0 = 0∧[1 + (-1)bso_51] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500)))), i561, java.lang.Object(CyclicList(o2500))) → COND_INC4460(>(+(i561, -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500)))), i561, java.lang.Object(CyclicList(o2500)))
    • (i561[0] ≥ 0 ⇒ (UIncreasing(COND_INC4460(>(+(i561[0], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0])))), ≥)∧[(-1)Bound*bni_24 + (4)bni_24] + [(2)bni_24]i561[0] ≥ 0∧[(-1)bso_25] ≥ 0)

  • COND_INC4460(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500)))), i561, java.lang.Object(CyclicList(o2500))) → JMP4853'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500)))), +(i561, -1), o2500)
    • ((UIncreasing(JMP4853'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))), +(i561[1], -1), o2500[1])), ≥)∧0 = 0∧[(-1)bso_27] ≥ 0)

  • JMP4853'(java.lang.Object(CyclicList(o2469)), i568, o2495) → INC4460(java.lang.Object(CyclicList(o2469)), i568, o2495)
    • ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧0 = 0∧[2 + (-1)bso_29] ≥ 0)
    • ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧0 = 0∧[2 + (-1)bso_29] ≥ 0)
    • ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧0 = 0∧[2 + (-1)bso_29] ≥ 0)
    • ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧0 = 0∧[2 + (-1)bso_29] ≥ 0)
    • ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧0 = 0∧[2 + (-1)bso_29] ≥ 0)
    • ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])), ≥)∧0 = 0∧[2 + (-1)bso_29] ≥ 0)

  • INC4460(java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2495))) → COND_INC44601(>(+(i561, -1), 0), java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2495)))
    • (i561[3] ≥ 0 ⇒ (UIncreasing(COND_INC44601(>(+(i561[3], -1), 0), java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3])))), ≥)∧[(-1)Bound*bni_30 + (4)bni_30] + [(2)bni_30]i561[3] ≥ 0∧[(-1)bso_31] ≥ 0)

  • COND_INC44601(TRUE, java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2495))) → INC4460(java.lang.Object(CyclicList(o2469)), +(i561, -1), o2495)
    • ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[4])), +(i561[4], -1), o2495[4])), ≥)∧0 = 0∧[2 + (-1)bso_33] ≥ 0)

  • INC4460(java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2494rec))) → COND_INC44602(>(+(i561, -1), 0), java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2494rec)))
    • (i561[5] ≥ 0 ⇒ (UIncreasing(COND_INC44602(>(+(i561[5], -1), 0), java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5])))), ≥)∧[(-1)Bound*bni_34 + (4)bni_34] + [(2)bni_34]i561[5] ≥ 0∧[(-1)bso_35] ≥ 0)

  • COND_INC44602(TRUE, java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2494rec))) → INC4460(java.lang.Object(CyclicList(o2469)), +(i561, -1), java.lang.Object(CyclicList(o2494rec)))
    • ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[6])), +(i561[6], -1), java.lang.Object(CyclicList(o2494rec[6])))), ≥)∧0 = 0∧[2 + (-1)bso_37] ≥ 0)

  • JMP4687'(java.lang.Object(CyclicList(o2469)), i568, o2469) → INC4460(java.lang.Object(CyclicList(o2469)), i568, o2469)
    • ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧0 = 0∧[(-1)bso_39] ≥ 0)
    • ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧0 = 0∧[(-1)bso_39] ≥ 0)
    • ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧0 = 0∧[(-1)bso_39] ≥ 0)
    • ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧0 = 0∧[(-1)bso_39] ≥ 0)
    • ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧0 = 0∧[(-1)bso_39] ≥ 0)
    • ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])), ≥)∧0 = 0∧[(-1)bso_39] ≥ 0)

  • INC4460(java.lang.Object(CyclicList(o2469)), i561, java.lang.Object(CyclicList(o2469))) → COND_INC44603(>(+(i561, -1), 0), i561, java.lang.Object(CyclicList(o2469)))
    • (i561[8] ≥ 0 ⇒ (UIncreasing(COND_INC44603(>(+(i561[8], -1), 0), i561[8], java.lang.Object(CyclicList(o2469[8])))), ≥)∧[(-1)Bound*bni_40 + (4)bni_40] + [(2)bni_40]i561[8] ≥ 0∧[1 + (-1)bso_41] ≥ 0)

  • COND_INC44603(TRUE, i561, java.lang.Object(CyclicList(o2469))) → INC4460(java.lang.Object(CyclicList(o2469)), +(i561, -1), o2469)
    • ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2469[9])), +(i561[9], -1), o2469[9])), ≥)∧0 = 0∧[1 + (-1)bso_43] ≥ 0)

  • INC4460(java.lang.Object(CyclicList(o2468rec)), i561, java.lang.Object(CyclicList(o2468rec))) → COND_INC44604(>(+(i561, -1), 0), i561, java.lang.Object(CyclicList(o2468rec)))
    • (i561[10] ≥ 0 ⇒ (UIncreasing(COND_INC44604(>(+(i561[10], -1), 0), i561[10], java.lang.Object(CyclicList(o2468rec[10])))), ≥)∧[(-1)Bound*bni_44 + (4)bni_44] + [(2)bni_44]i561[10] ≥ 0∧[1 + (-1)bso_45] ≥ 0)

  • COND_INC44604(TRUE, i561, java.lang.Object(CyclicList(o2468rec))) → INC4460(java.lang.Object(CyclicList(o2468rec)), +(i561, -1), java.lang.Object(CyclicList(o2468rec)))
    • ((UIncreasing(INC4460(java.lang.Object(CyclicList(o2468rec[11])), +(i561[11], -1), java.lang.Object(CyclicList(o2468rec[11])))), ≥)∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

  • INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec)))), i561, java.lang.Object(CyclicList(o2499rec))) → COND_INC44605(>(+(i561, -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec)))), i561, java.lang.Object(CyclicList(o2499rec)))
    • (i561[12] ≥ 0 ⇒ (UIncreasing(COND_INC44605(>(+(i561[12], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12])))), ≥)∧[(-1)Bound*bni_48 + (4)bni_48] + [(2)bni_48]i561[12] ≥ 0∧[1 + (-1)bso_49] ≥ 0)

  • COND_INC44605(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec)))), i561, java.lang.Object(CyclicList(o2499rec))) → JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec)))), +(i561, -1), java.lang.Object(CyclicList(o2499rec)))
    • ((UIncreasing(JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13])))), +(i561[13], -1), java.lang.Object(CyclicList(o2499rec[13])))), ≥)∧0 = 0∧[1 + (-1)bso_51] ≥ 0)




The constraints for P> respective Pbound 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 Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(INC4460(x1, x2, x3)) = [2]x2   
POL(java.lang.Object(x1)) = [-1]   
POL(CyclicList(x1)) = [-1]   
POL(COND_INC4460(x1, x2, x3, x4)) = [2]x3   
POL(>(x1, x2)) = [-1]   
POL(+(x1, x2)) = x1 + x2   
POL(-1) = [-1]   
POL(0) = 0   
POL(JMP4853'(x1, x2, x3)) = [2] + [2]x2   
POL(COND_INC44601(x1, x2, x3, x4)) = [2]x3   
POL(COND_INC44602(x1, x2, x3, x4)) = [2]x3   
POL(JMP4687'(x1, x2, x3)) = [2]x2   
POL(COND_INC44603(x1, x2, x3)) = [-1] + [2]x2   
POL(COND_INC44604(x1, x2, x3)) = [-1] + [2]x2   
POL(COND_INC44605(x1, x2, x3, x4)) = [-1] + [2]x3   

The following pairs are in P>:

JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2]) → INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])
COND_INC44601(TRUE, java.lang.Object(CyclicList(o2469[4])), i561[4], java.lang.Object(CyclicList(o2495[4]))) → INC4460(java.lang.Object(CyclicList(o2469[4])), +(i561[4], -1), o2495[4])
COND_INC44602(TRUE, java.lang.Object(CyclicList(o2469[6])), i561[6], java.lang.Object(CyclicList(o2494rec[6]))) → INC4460(java.lang.Object(CyclicList(o2469[6])), +(i561[6], -1), java.lang.Object(CyclicList(o2494rec[6])))
INC4460(java.lang.Object(CyclicList(o2469[8])), i561[8], java.lang.Object(CyclicList(o2469[8]))) → COND_INC44603(>(+(i561[8], -1), 0), i561[8], java.lang.Object(CyclicList(o2469[8])))
COND_INC44603(TRUE, i561[9], java.lang.Object(CyclicList(o2469[9]))) → INC4460(java.lang.Object(CyclicList(o2469[9])), +(i561[9], -1), o2469[9])
INC4460(java.lang.Object(CyclicList(o2468rec[10])), i561[10], java.lang.Object(CyclicList(o2468rec[10]))) → COND_INC44604(>(+(i561[10], -1), 0), i561[10], java.lang.Object(CyclicList(o2468rec[10])))
COND_INC44604(TRUE, i561[11], java.lang.Object(CyclicList(o2468rec[11]))) → INC4460(java.lang.Object(CyclicList(o2468rec[11])), +(i561[11], -1), java.lang.Object(CyclicList(o2468rec[11])))
INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12]))) → COND_INC44605(>(+(i561[12], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12])))
COND_INC44605(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13])))), i561[13], java.lang.Object(CyclicList(o2499rec[13]))) → JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13])))), +(i561[13], -1), java.lang.Object(CyclicList(o2499rec[13])))

The following pairs are in Pbound:

INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0]))) → COND_INC4460(>(+(i561[0], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0])))
INC4460(java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3]))) → COND_INC44601(>(+(i561[3], -1), 0), java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3])))
INC4460(java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5]))) → COND_INC44602(>(+(i561[5], -1), 0), java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5])))
INC4460(java.lang.Object(CyclicList(o2469[8])), i561[8], java.lang.Object(CyclicList(o2469[8]))) → COND_INC44603(>(+(i561[8], -1), 0), i561[8], java.lang.Object(CyclicList(o2469[8])))
INC4460(java.lang.Object(CyclicList(o2468rec[10])), i561[10], java.lang.Object(CyclicList(o2468rec[10]))) → COND_INC44604(>(+(i561[10], -1), 0), i561[10], java.lang.Object(CyclicList(o2468rec[10])))
INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12]))) → COND_INC44605(>(+(i561[12], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[12])))), i561[12], java.lang.Object(CyclicList(o2499rec[12])))

The following pairs are in P≥:

INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0]))) → COND_INC4460(>(+(i561[0], -1), 0), java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0])))
COND_INC4460(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))), i561[1], java.lang.Object(CyclicList(o2500[1]))) → JMP4853'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))), +(i561[1], -1), o2500[1])
INC4460(java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3]))) → COND_INC44601(>(+(i561[3], -1), 0), java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3])))
INC4460(java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5]))) → COND_INC44602(>(+(i561[5], -1), 0), java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5])))
JMP4687'(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7]) → INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])

There are no usable rules.

(15) Complex Obligation (AND)

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


R is empty.

The integer pair graph contains the following rules and edges:
(0): INC4460(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0]))) → COND_INC4460(i561[0] + -1 > 0, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[0])))), i561[0], java.lang.Object(CyclicList(o2500[0])))
(1): COND_INC4460(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))), i561[1], java.lang.Object(CyclicList(o2500[1]))) → JMP4853'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))), i561[1] + -1, o2500[1])
(3): INC4460(java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3]))) → COND_INC44601(i561[3] + -1 > 0, java.lang.Object(CyclicList(o2469[3])), i561[3], java.lang.Object(CyclicList(o2495[3])))
(5): INC4460(java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5]))) → COND_INC44602(i561[5] + -1 > 0, java.lang.Object(CyclicList(o2469[5])), i561[5], java.lang.Object(CyclicList(o2494rec[5])))
(7): JMP4687'(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7]) → INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])

(7) -> (0), if ((o2469[7] →* java.lang.Object(CyclicList(o2500[0])))∧(i568[7] →* i561[0])∧((o2469[7] →* java.lang.Object(CyclicList(o2500[0])))))


(0) -> (1), if ((i561[0] →* i561[1])∧(i561[0] + -1 > 0 →* TRUE)∧((o2500[0] →* o2500[1])))


(7) -> (3), if ((o2469[7] →* java.lang.Object(CyclicList(o2495[3])))∧(i568[7] →* i561[3])∧((o2469[7] →* o2469[3])))


(7) -> (5), if ((i568[7] →* i561[5])∧((o2469[7] →* o2469[5]))∧(o2469[7] →* java.lang.Object(CyclicList(o2494rec[5]))))



The set Q consists of the following terms:
Cond_Inc4460(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(x0)))), x1, java.lang.Object(CyclicList(x0)))
JMP4853(java.lang.Object(CyclicList(x0)), x1, x2)
Inc4460(java.lang.Object(CyclicList(x0)), x1, java.lang.Object(CyclicList(x2)))
Cond_Inc44601(TRUE, java.lang.Object(CyclicList(x0)), x1, java.lang.Object(CyclicList(x2)))
Cond_Inc44602(TRUE, java.lang.Object(CyclicList(x0)), x1, java.lang.Object(CyclicList(x2)))
JMP4687(java.lang.Object(CyclicList(x0)), x1, x0)
Cond_Inc44603(TRUE, x0, java.lang.Object(CyclicList(x1)))
Cond_Inc44604(TRUE, x0, java.lang.Object(CyclicList(x1)))
Cond_Inc44605(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(x0)))), x1, java.lang.Object(CyclicList(x0)))

(17) IDependencyGraphProof (EQUIVALENT transformation)

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

(18) TRUE

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


R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_INC4460(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))), i561[1], java.lang.Object(CyclicList(o2500[1]))) → JMP4853'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2500[1])))), i561[1] + -1, o2500[1])
(2): JMP4853'(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2]) → INC4460(java.lang.Object(CyclicList(o2469[2])), i568[2], o2495[2])
(4): COND_INC44601(TRUE, java.lang.Object(CyclicList(o2469[4])), i561[4], java.lang.Object(CyclicList(o2495[4]))) → INC4460(java.lang.Object(CyclicList(o2469[4])), i561[4] + -1, o2495[4])
(6): COND_INC44602(TRUE, java.lang.Object(CyclicList(o2469[6])), i561[6], java.lang.Object(CyclicList(o2494rec[6]))) → INC4460(java.lang.Object(CyclicList(o2469[6])), i561[6] + -1, java.lang.Object(CyclicList(o2494rec[6])))
(7): JMP4687'(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7]) → INC4460(java.lang.Object(CyclicList(o2469[7])), i568[7], o2469[7])
(9): COND_INC44603(TRUE, i561[9], java.lang.Object(CyclicList(o2469[9]))) → INC4460(java.lang.Object(CyclicList(o2469[9])), i561[9] + -1, o2469[9])
(11): COND_INC44604(TRUE, i561[11], java.lang.Object(CyclicList(o2468rec[11]))) → INC4460(java.lang.Object(CyclicList(o2468rec[11])), i561[11] + -1, java.lang.Object(CyclicList(o2468rec[11])))
(13): COND_INC44605(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13])))), i561[13], java.lang.Object(CyclicList(o2499rec[13]))) → JMP4687'(java.lang.Object(CyclicList(java.lang.Object(CyclicList(o2499rec[13])))), i561[13] + -1, java.lang.Object(CyclicList(o2499rec[13])))

(1) -> (2), if ((i561[1] + -1 →* i568[2])∧((java.lang.Object(CyclicList(o2500[1])) →* o2469[2]))∧(o2500[1] →* o2495[2]))


(13) -> (7), if ((i561[13] + -1 →* i568[7])∧(java.lang.Object(CyclicList(o2499rec[13])) →* o2469[7])∧((java.lang.Object(CyclicList(o2499rec[13])) →* o2469[7])))



The set Q consists of the following terms:
Cond_Inc4460(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(x0)))), x1, java.lang.Object(CyclicList(x0)))
JMP4853(java.lang.Object(CyclicList(x0)), x1, x2)
Inc4460(java.lang.Object(CyclicList(x0)), x1, java.lang.Object(CyclicList(x2)))
Cond_Inc44601(TRUE, java.lang.Object(CyclicList(x0)), x1, java.lang.Object(CyclicList(x2)))
Cond_Inc44602(TRUE, java.lang.Object(CyclicList(x0)), x1, java.lang.Object(CyclicList(x2)))
JMP4687(java.lang.Object(CyclicList(x0)), x1, x0)
Cond_Inc44603(TRUE, x0, java.lang.Object(CyclicList(x1)))
Cond_Inc44604(TRUE, x0, java.lang.Object(CyclicList(x1)))
Cond_Inc44605(TRUE, java.lang.Object(CyclicList(java.lang.Object(CyclicList(x0)))), x1, java.lang.Object(CyclicList(x0)))

(20) IDependencyGraphProof (EQUIVALENT transformation)

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

(21) TRUE

(22) 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:
Inc609(i42) → Cond_Inc609(i42 + -1 > 0, i42)
Cond_Inc609(TRUE, i42) → Inc609(i42 + -1)
The set Q consists of the following terms:
Inc609(x0)
Cond_Inc609(TRUE, x0)

(23) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

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


The ITRS R consists of the following rules:
Inc609(i42) → Cond_Inc609(i42 + -1 > 0, i42)
Cond_Inc609(TRUE, i42) → Inc609(i42 + -1)

The integer pair graph contains the following rules and edges:
(0): INC609(i42[0]) → COND_INC609(i42[0] + -1 > 0, i42[0])
(1): COND_INC609(TRUE, i42[1]) → INC609(i42[1] + -1)

(0) -> (1), if ((i42[0] →* i42[1])∧(i42[0] + -1 > 0 →* TRUE))


(1) -> (0), if ((i42[1] + -1 →* i42[0]))



The set Q consists of the following terms:
Inc609(x0)
Cond_Inc609(TRUE, x0)

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

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


R is empty.

The integer pair graph contains the following rules and edges:
(0): INC609(i42[0]) → COND_INC609(i42[0] + -1 > 0, i42[0])
(1): COND_INC609(TRUE, i42[1]) → INC609(i42[1] + -1)

(0) -> (1), if ((i42[0] →* i42[1])∧(i42[0] + -1 > 0 →* TRUE))


(1) -> (0), if ((i42[1] + -1 →* i42[0]))



The set Q consists of the following terms:
Inc609(x0)
Cond_Inc609(TRUE, x0)

(27) 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 INC609(i42) → COND_INC609(>(+(i42, -1), 0), i42) the following chains were created:
  • We consider the chain INC609(i42[0]) → COND_INC609(>(+(i42[0], -1), 0), i42[0]), COND_INC609(TRUE, i42[1]) → INC609(+(i42[1], -1)) which results in the following constraint:

    (1)    (i42[0]=i42[1]∧>(+(i42[0], -1), 0)=TRUE ⇒ INC609(i42[0])≥NonInfC∧INC609(i42[0])≥COND_INC609(>(+(i42[0], -1), 0), i42[0])∧(UIncreasing(COND_INC609(>(+(i42[0], -1), 0), i42[0])), ≥))



    We simplified constraint (1) using rule (IV) which results in the following new constraint:

    (2)    (>(+(i42[0], -1), 0)=TRUE ⇒ INC609(i42[0])≥NonInfC∧INC609(i42[0])≥COND_INC609(>(+(i42[0], -1), 0), i42[0])∧(UIncreasing(COND_INC609(>(+(i42[0], -1), 0), i42[0])), ≥))



    We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (3)    (i42[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_INC609(>(+(i42[0], -1), 0), i42[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]i42[0] ≥ 0∧[(-1)bso_9] ≥ 0)



    We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (4)    (i42[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_INC609(>(+(i42[0], -1), 0), i42[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]i42[0] ≥ 0∧[(-1)bso_9] ≥ 0)



    We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (5)    (i42[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_INC609(>(+(i42[0], -1), 0), i42[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]i42[0] ≥ 0∧[(-1)bso_9] ≥ 0)



    We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (6)    (i42[0] ≥ 0 ⇒ (UIncreasing(COND_INC609(>(+(i42[0], -1), 0), i42[0])), ≥)∧[(-1)Bound*bni_8 + (4)bni_8] + [(2)bni_8]i42[0] ≥ 0∧[(-1)bso_9] ≥ 0)







For Pair COND_INC609(TRUE, i42) → INC609(+(i42, -1)) the following chains were created:
  • We consider the chain COND_INC609(TRUE, i42[1]) → INC609(+(i42[1], -1)) which results in the following constraint:

    (7)    (COND_INC609(TRUE, i42[1])≥NonInfC∧COND_INC609(TRUE, i42[1])≥INC609(+(i42[1], -1))∧(UIncreasing(INC609(+(i42[1], -1))), ≥))



    We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (8)    ((UIncreasing(INC609(+(i42[1], -1))), ≥)∧[2 + (-1)bso_11] ≥ 0)



    We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (9)    ((UIncreasing(INC609(+(i42[1], -1))), ≥)∧[2 + (-1)bso_11] ≥ 0)



    We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (10)    ((UIncreasing(INC609(+(i42[1], -1))), ≥)∧[2 + (-1)bso_11] ≥ 0)



    We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (11)    ((UIncreasing(INC609(+(i42[1], -1))), ≥)∧0 = 0∧[2 + (-1)bso_11] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • INC609(i42) → COND_INC609(>(+(i42, -1), 0), i42)
    • (i42[0] ≥ 0 ⇒ (UIncreasing(COND_INC609(>(+(i42[0], -1), 0), i42[0])), ≥)∧[(-1)Bound*bni_8 + (4)bni_8] + [(2)bni_8]i42[0] ≥ 0∧[(-1)bso_9] ≥ 0)

  • COND_INC609(TRUE, i42) → INC609(+(i42, -1))
    • ((UIncreasing(INC609(+(i42[1], -1))), ≥)∧0 = 0∧[2 + (-1)bso_11] ≥ 0)




The constraints for P> respective Pbound 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 Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(INC609(x1)) = [2]x1   
POL(COND_INC609(x1, x2)) = [2]x2   
POL(>(x1, x2)) = [-1]   
POL(+(x1, x2)) = x1 + x2   
POL(-1) = [-1]   
POL(0) = 0   

The following pairs are in P>:

COND_INC609(TRUE, i42[1]) → INC609(+(i42[1], -1))

The following pairs are in Pbound:

INC609(i42[0]) → COND_INC609(>(+(i42[0], -1), 0), i42[0])

The following pairs are in P≥:

INC609(i42[0]) → COND_INC609(>(+(i42[0], -1), 0), i42[0])

There are no usable rules.

(28) Complex Obligation (AND)

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


R is empty.

The integer pair graph contains the following rules and edges:
(0): INC609(i42[0]) → COND_INC609(i42[0] + -1 > 0, i42[0])


The set Q consists of the following terms:
Inc609(x0)
Cond_Inc609(TRUE, x0)

(30) IDependencyGraphProof (EQUIVALENT transformation)

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

(31) TRUE

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

Integer


R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_INC609(TRUE, i42[1]) → INC609(i42[1] + -1)


The set Q consists of the following terms:
Inc609(x0)
Cond_Inc609(TRUE, x0)

(33) IDependencyGraphProof (EQUIVALENT transformation)

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

(34) TRUE