Termination of the given JBC could be proven:

0 JBC
↳1 JBC2FIG (⇐)
↳2 FIGraph
↳3 FIGtoITRSProof (⇐)
↳4 AND
    ↳5 ITRS
        ↳6 ITRStoIDPProof (⇔)
        ↳7 IDP
        ↳8 UsableRulesProof (⇔)
        ↳9 IDP
        ↳10 IDPNonInfProof (⇐)
        ↳11 AND
            ↳12 IDP
                ↳13 IDependencyGraphProof (⇔)
                ↳14 TRUE
            ↳15 IDP
                ↳16 IDependencyGraphProof (⇔)
                ↳17 IDP
                ↳18 IDPNonInfProof (⇐)
                ↳19 IDP
                ↳20 IDependencyGraphProof (⇔)
                ↳21 TRUE
    ↳22 ITRS
        ↳23 ITRStoIDPProof (⇔)
        ↳24 IDP
        ↳25 UsableRulesProof (⇔)
        ↳26 IDP
        ↳27 IDPNonInfProof (⇐)
        ↳28 IDP
        ↳29 IDependencyGraphProof (⇔)
        ↳30 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: Mod 
public class Mod {
  public static void main(String[] args) {
    int x = args[0].length();
    int y = args[1].length();
    mod(x, y);
  }
  public static int mod(int x, int y) {
   
    while (x >= y && y > 0) {
      x = minus(x,y);
     
    }
    return x;
  }

  public static int minus(int x, int y) {
    while (y != 0) {
      if (y > 0)  {
        y--;
        x--;
      } else  {
        y++;
        x++;
      }
    }
    return x;
  }

}


(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 222 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:
JMP981(i59, i59, i59, i148, i162) → Cond_JMP981(i162 > 0, i59, i59, i59, i148, i162)
Cond_JMP981(TRUE, i59, i59, i59, i148, i162) → JMP981(i59, i59, i59, i148 + -1, i162 + -1)
JMP873(i59, i71, i59) → Cond_JMP873(i59 > 0 && i71 >= i59, i59, i71, i59)
Cond_JMP873(TRUE, i59, i71, i59) → JMP981(i59, i59, i59, i71 + -1 + -1, i59 + -1 + -1)
JMP981(i59, i59, i59, i148, 0) → JMP873(i59, i148, i59)
JMP873(1, i71, 1) → Cond_JMP8731(1 > 0 && i71 >= 1, 1, i71, 1)
Cond_JMP8731(TRUE, 1, i71, 1) → JMP873(1, i71 + -1, 1)
The set Q consists of the following terms:
JMP981(x0, x0, x0, x1, x2)
Cond_JMP981(TRUE, x0, x0, x0, x1, x2)
JMP873(x0, x1, x0)
Cond_JMP873(TRUE, x0, x1, x0)
Cond_JMP8731(TRUE, 1, x0, 1)

(6) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(7) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Integer, Boolean


The ITRS R consists of the following rules:
JMP981(i59, i59, i59, i148, i162) → Cond_JMP981(i162 > 0, i59, i59, i59, i148, i162)
Cond_JMP981(TRUE, i59, i59, i59, i148, i162) → JMP981(i59, i59, i59, i148 + -1, i162 + -1)
JMP873(i59, i71, i59) → Cond_JMP873(i59 > 0 && i71 >= i59, i59, i71, i59)
Cond_JMP873(TRUE, i59, i71, i59) → JMP981(i59, i59, i59, i71 + -1 + -1, i59 + -1 + -1)
JMP981(i59, i59, i59, i148, 0) → JMP873(i59, i148, i59)
JMP873(1, i71, 1) → Cond_JMP8731(1 > 0 && i71 >= 1, 1, i71, 1)
Cond_JMP8731(TRUE, 1, i71, 1) → JMP873(1, i71 + -1, 1)

The integer pair graph contains the following rules and edges:
(0): JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0]) → COND_JMP981(i162[0] > 0, i59[0], i59[0], i59[0], i148[0], i162[0])
(1): COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], i148[1] + -1, i162[1] + -1)
(2): JMP873'(i59[2], i71[2], i59[2]) → COND_JMP873(i59[2] > 0 && i71[2] >= i59[2], i59[2], i71[2], i59[2])
(3): COND_JMP873(TRUE, i59[3], i71[3], i59[3]) → JMP981'(i59[3], i59[3], i59[3], i71[3] + -1 + -1, i59[3] + -1 + -1)
(4): JMP981'(i59[4], i59[4], i59[4], i148[4], 0) → JMP873'(i59[4], i148[4], i59[4])
(5): JMP873'(1, i71[5], 1) → COND_JMP8731(1 > 0 && i71[5] >= 1, 1, i71[5], 1)
(6): COND_JMP8731(TRUE, 1, i71[6], 1) → JMP873'(1, i71[6] + -1, 1)

(0) -> (1), if ((i162[0] > 0 →* TRUE)∧(i162[0] →* i162[1])∧(i148[0] →* i148[1])∧(i59[0] →* i59[1]))


(1) -> (0), if ((i162[1] + -1 →* i162[0])∧(i59[1] →* i59[0])∧(i148[1] + -1 →* i148[0]))


(1) -> (4), if ((i59[1] →* i59[4])∧(i162[1] + -1 →* 0)∧(i148[1] + -1 →* i148[4]))


(2) -> (3), if ((i59[2] →* i59[3])∧(i59[2] > 0 && i71[2] >= i59[2] →* TRUE)∧(i71[2] →* i71[3]))


(3) -> (0), if ((i59[3] →* i59[0])∧(i59[3] + -1 + -1 →* i162[0])∧(i71[3] + -1 + -1 →* i148[0]))


(3) -> (4), if ((i59[3] + -1 + -1 →* 0)∧(i59[3] →* i59[4])∧(i71[3] + -1 + -1 →* i148[4]))


(4) -> (2), if ((i59[4] →* i59[2])∧(i148[4] →* i71[2]))


(4) -> (5), if ((i59[4] →* 1)∧(i148[4] →* i71[5]))


(5) -> (6), if ((i71[5] →* i71[6])∧(1 > 0 && i71[5] >= 1 →* TRUE))


(6) -> (2), if ((i71[6] + -1 →* i71[2])∧(1 →* i59[2]))


(6) -> (5), if (i71[6] + -1 →* i71[5])



The set Q consists of the following terms:
JMP981(x0, x0, x0, x1, x2)
Cond_JMP981(TRUE, x0, x0, x0, x1, x2)
JMP873(x0, x1, x0)
Cond_JMP873(TRUE, x0, x1, x0)
Cond_JMP8731(TRUE, 1, x0, 1)

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

(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, Boolean


R is empty.

The integer pair graph contains the following rules and edges:
(0): JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0]) → COND_JMP981(i162[0] > 0, i59[0], i59[0], i59[0], i148[0], i162[0])
(1): COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], i148[1] + -1, i162[1] + -1)
(2): JMP873'(i59[2], i71[2], i59[2]) → COND_JMP873(i59[2] > 0 && i71[2] >= i59[2], i59[2], i71[2], i59[2])
(3): COND_JMP873(TRUE, i59[3], i71[3], i59[3]) → JMP981'(i59[3], i59[3], i59[3], i71[3] + -1 + -1, i59[3] + -1 + -1)
(4): JMP981'(i59[4], i59[4], i59[4], i148[4], 0) → JMP873'(i59[4], i148[4], i59[4])
(5): JMP873'(1, i71[5], 1) → COND_JMP8731(1 > 0 && i71[5] >= 1, 1, i71[5], 1)
(6): COND_JMP8731(TRUE, 1, i71[6], 1) → JMP873'(1, i71[6] + -1, 1)

(0) -> (1), if ((i162[0] > 0 →* TRUE)∧(i162[0] →* i162[1])∧(i148[0] →* i148[1])∧(i59[0] →* i59[1]))


(1) -> (0), if ((i162[1] + -1 →* i162[0])∧(i59[1] →* i59[0])∧(i148[1] + -1 →* i148[0]))


(1) -> (4), if ((i59[1] →* i59[4])∧(i162[1] + -1 →* 0)∧(i148[1] + -1 →* i148[4]))


(2) -> (3), if ((i59[2] →* i59[3])∧(i59[2] > 0 && i71[2] >= i59[2] →* TRUE)∧(i71[2] →* i71[3]))


(3) -> (0), if ((i59[3] →* i59[0])∧(i59[3] + -1 + -1 →* i162[0])∧(i71[3] + -1 + -1 →* i148[0]))


(3) -> (4), if ((i59[3] + -1 + -1 →* 0)∧(i59[3] →* i59[4])∧(i71[3] + -1 + -1 →* i148[4]))


(4) -> (2), if ((i59[4] →* i59[2])∧(i148[4] →* i71[2]))


(4) -> (5), if ((i59[4] →* 1)∧(i148[4] →* i71[5]))


(5) -> (6), if ((i71[5] →* i71[6])∧(1 > 0 && i71[5] >= 1 →* TRUE))


(6) -> (2), if ((i71[6] + -1 →* i71[2])∧(1 →* i59[2]))


(6) -> (5), if (i71[6] + -1 →* i71[5])



The set Q consists of the following terms:
JMP981(x0, x0, x0, x1, x2)
Cond_JMP981(TRUE, x0, x0, x0, x1, x2)
JMP873(x0, x1, x0)
Cond_JMP873(TRUE, x0, x1, x0)
Cond_JMP8731(TRUE, 1, x0, 1)

(10) 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 JMP981'(i59, i59, i59, i148, i162) → COND_JMP981(>(i162, 0), i59, i59, i59, i148, i162) the following chains were created:
  • We consider the chain JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0]) → COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0]), COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1)) which results in the following constraint:

    (1)    (>(i162[0], 0)=TRUE∧i162[0]=i162[1]∧i148[0]=i148[1]∧i59[0]=i59[1] ⇒ JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0])≥NonInfC∧JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0])≥COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])∧(UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥))



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

    (2)    (>(i162[0], 0)=TRUE ⇒ JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0])≥NonInfC∧JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0])≥COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])∧(UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥))



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

    (3)    (i162[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥)∧[(-1)bni_21 + (-1)Bound*bni_21] + [bni_21]i148[0] + [(2)bni_21]i59[0] ≥ 0∧[(-1)bso_22] ≥ 0)



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

    (4)    (i162[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥)∧[(-1)bni_21 + (-1)Bound*bni_21] + [bni_21]i148[0] + [(2)bni_21]i59[0] ≥ 0∧[(-1)bso_22] ≥ 0)



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

    (5)    (i162[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥)∧[(-1)bni_21 + (-1)Bound*bni_21] + [bni_21]i148[0] + [(2)bni_21]i59[0] ≥ 0∧[(-1)bso_22] ≥ 0)



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

    (6)    (i162[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥)∧[bni_21] = 0∧[(2)bni_21] = 0∧[(-1)bni_21 + (-1)Bound*bni_21] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_22] ≥ 0)



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

    (7)    (i162[0] ≥ 0 ⇒ (UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥)∧[bni_21] = 0∧[(2)bni_21] = 0∧[(-1)bni_21 + (-1)Bound*bni_21] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_22] ≥ 0)







For Pair COND_JMP981(TRUE, i59, i59, i59, i148, i162) → JMP981'(i59, i59, i59, +(i148, -1), +(i162, -1)) the following chains were created:
  • We consider the chain COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1)) which results in the following constraint:

    (8)    (COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1])≥NonInfC∧COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1])≥JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))∧(UIncreasing(JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))), ≥))



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

    (9)    ((UIncreasing(JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))), ≥)∧[1 + (-1)bso_24] ≥ 0)



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

    (10)    ((UIncreasing(JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))), ≥)∧[1 + (-1)bso_24] ≥ 0)



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

    (11)    ((UIncreasing(JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))), ≥)∧[1 + (-1)bso_24] ≥ 0)



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

    (12)    ((UIncreasing(JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_24] ≥ 0)







For Pair JMP873'(i59, i71, i59) → COND_JMP873(&&(>(i59, 0), >=(i71, i59)), i59, i71, i59) the following chains were created:
  • We consider the chain JMP873'(i59[2], i71[2], i59[2]) → COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2]), COND_JMP873(TRUE, i59[3], i71[3], i59[3]) → JMP981'(i59[3], i59[3], i59[3], +(+(i71[3], -1), -1), +(+(i59[3], -1), -1)) which results in the following constraint:

    (13)    (i59[2]=i59[3]∧&&(>(i59[2], 0), >=(i71[2], i59[2]))=TRUE∧i71[2]=i71[3] ⇒ JMP873'(i59[2], i71[2], i59[2])≥NonInfC∧JMP873'(i59[2], i71[2], i59[2])≥COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2])∧(UIncreasing(COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2])), ≥))



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

    (14)    (>(i59[2], 0)=TRUE∧>=(i71[2], i59[2])=TRUE ⇒ JMP873'(i59[2], i71[2], i59[2])≥NonInfC∧JMP873'(i59[2], i71[2], i59[2])≥COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2])∧(UIncreasing(COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2])), ≥))



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

    (15)    (i59[2] + [-1] ≥ 0∧i71[2] + [-1]i59[2] ≥ 0 ⇒ (UIncreasing(COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2])), ≥)∧[(-1)bni_25 + (-1)Bound*bni_25] + [(2)bni_25]i59[2] + [bni_25]i71[2] ≥ 0∧[(-1)bso_26] ≥ 0)



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

    (16)    (i59[2] + [-1] ≥ 0∧i71[2] + [-1]i59[2] ≥ 0 ⇒ (UIncreasing(COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2])), ≥)∧[(-1)bni_25 + (-1)Bound*bni_25] + [(2)bni_25]i59[2] + [bni_25]i71[2] ≥ 0∧[(-1)bso_26] ≥ 0)



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

    (17)    (i59[2] + [-1] ≥ 0∧i71[2] + [-1]i59[2] ≥ 0 ⇒ (UIncreasing(COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2])), ≥)∧[(-1)bni_25 + (-1)Bound*bni_25] + [(2)bni_25]i59[2] + [bni_25]i71[2] ≥ 0∧[(-1)bso_26] ≥ 0)



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

    (18)    (i59[2] ≥ 0∧i71[2] + [-1] + [-1]i59[2] ≥ 0 ⇒ (UIncreasing(COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2])), ≥)∧[bni_25 + (-1)Bound*bni_25] + [(2)bni_25]i59[2] + [bni_25]i71[2] ≥ 0∧[(-1)bso_26] ≥ 0)



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

    (19)    (i59[2] ≥ 0∧i71[2] ≥ 0 ⇒ (UIncreasing(COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2])), ≥)∧[(2)bni_25 + (-1)Bound*bni_25] + [(3)bni_25]i59[2] + [bni_25]i71[2] ≥ 0∧[(-1)bso_26] ≥ 0)







For Pair COND_JMP873(TRUE, i59, i71, i59) → JMP981'(i59, i59, i59, +(+(i71, -1), -1), +(+(i59, -1), -1)) the following chains were created:
  • We consider the chain COND_JMP873(TRUE, i59[3], i71[3], i59[3]) → JMP981'(i59[3], i59[3], i59[3], +(+(i71[3], -1), -1), +(+(i59[3], -1), -1)) which results in the following constraint:

    (20)    (COND_JMP873(TRUE, i59[3], i71[3], i59[3])≥NonInfC∧COND_JMP873(TRUE, i59[3], i71[3], i59[3])≥JMP981'(i59[3], i59[3], i59[3], +(+(i71[3], -1), -1), +(+(i59[3], -1), -1))∧(UIncreasing(JMP981'(i59[3], i59[3], i59[3], +(+(i71[3], -1), -1), +(+(i59[3], -1), -1))), ≥))



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

    (21)    ((UIncreasing(JMP981'(i59[3], i59[3], i59[3], +(+(i71[3], -1), -1), +(+(i59[3], -1), -1))), ≥)∧[2 + (-1)bso_28] ≥ 0)



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

    (22)    ((UIncreasing(JMP981'(i59[3], i59[3], i59[3], +(+(i71[3], -1), -1), +(+(i59[3], -1), -1))), ≥)∧[2 + (-1)bso_28] ≥ 0)



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

    (23)    ((UIncreasing(JMP981'(i59[3], i59[3], i59[3], +(+(i71[3], -1), -1), +(+(i59[3], -1), -1))), ≥)∧[2 + (-1)bso_28] ≥ 0)



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

    (24)    ((UIncreasing(JMP981'(i59[3], i59[3], i59[3], +(+(i71[3], -1), -1), +(+(i59[3], -1), -1))), ≥)∧0 = 0∧0 = 0∧[2 + (-1)bso_28] ≥ 0)







For Pair JMP981'(i59, i59, i59, i148, 0) → JMP873'(i59, i148, i59) the following chains were created:
  • We consider the chain JMP981'(i59[4], i59[4], i59[4], i148[4], 0) → JMP873'(i59[4], i148[4], i59[4]), JMP873'(i59[2], i71[2], i59[2]) → COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2]) which results in the following constraint:

    (25)    (i59[4]=i59[2]∧i148[4]=i71[2] ⇒ JMP981'(i59[4], i59[4], i59[4], i148[4], 0)≥NonInfC∧JMP981'(i59[4], i59[4], i59[4], i148[4], 0)≥JMP873'(i59[4], i148[4], i59[4])∧(UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥))



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

    (26)    (JMP981'(i59[4], i59[4], i59[4], i148[4], 0)≥NonInfC∧JMP981'(i59[4], i59[4], i59[4], i148[4], 0)≥JMP873'(i59[4], i148[4], i59[4])∧(UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥))



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

    (27)    ((UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥)∧[(-1)bso_30] ≥ 0)



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

    (28)    ((UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥)∧[(-1)bso_30] ≥ 0)



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

    (29)    ((UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥)∧[(-1)bso_30] ≥ 0)



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

    (30)    ((UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_30] ≥ 0)



  • We consider the chain JMP981'(i59[4], i59[4], i59[4], i148[4], 0) → JMP873'(i59[4], i148[4], i59[4]), JMP873'(1, i71[5], 1) → COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1) which results in the following constraint:

    (31)    (i59[4]=1∧i148[4]=i71[5] ⇒ JMP981'(i59[4], i59[4], i59[4], i148[4], 0)≥NonInfC∧JMP981'(i59[4], i59[4], i59[4], i148[4], 0)≥JMP873'(i59[4], i148[4], i59[4])∧(UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥))



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

    (32)    (JMP981'(1, 1, 1, i148[4], 0)≥NonInfC∧JMP981'(1, 1, 1, i148[4], 0)≥JMP873'(1, i148[4], 1)∧(UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥))



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

    (33)    ((UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥)∧[(-1)bso_30] ≥ 0)



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

    (34)    ((UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥)∧[(-1)bso_30] ≥ 0)



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

    (35)    ((UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥)∧[(-1)bso_30] ≥ 0)



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

    (36)    ((UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥)∧0 = 0∧[(-1)bso_30] ≥ 0)







For Pair JMP873'(1, i71, 1) → COND_JMP8731(&&(>(1, 0), >=(i71, 1)), 1, i71, 1) the following chains were created:
  • We consider the chain JMP873'(1, i71[5], 1) → COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1), COND_JMP8731(TRUE, 1, i71[6], 1) → JMP873'(1, +(i71[6], -1), 1) which results in the following constraint:

    (37)    (i71[5]=i71[6]∧&&(>(1, 0), >=(i71[5], 1))=TRUE ⇒ JMP873'(1, i71[5], 1)≥NonInfC∧JMP873'(1, i71[5], 1)≥COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1)∧(UIncreasing(COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1)), ≥))



    We simplified constraint (37) using rules (IV), (IDP_CONSTANT_FOLD), (DELETE_TRIVIAL_REDUCESTO), (IDP_BOOLEAN) which results in the following new constraint:

    (38)    (>=(i71[5], 1)=TRUE ⇒ JMP873'(1, i71[5], 1)≥NonInfC∧JMP873'(1, i71[5], 1)≥COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1)∧(UIncreasing(COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1)), ≥))



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

    (39)    (i71[5] + [-1] ≥ 0 ⇒ (UIncreasing(COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1)), ≥)∧[bni_31 + (-1)Bound*bni_31] + [bni_31]i71[5] ≥ 0∧[1 + (-1)bso_32] ≥ 0)



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

    (40)    (i71[5] + [-1] ≥ 0 ⇒ (UIncreasing(COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1)), ≥)∧[bni_31 + (-1)Bound*bni_31] + [bni_31]i71[5] ≥ 0∧[1 + (-1)bso_32] ≥ 0)



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

    (41)    (i71[5] + [-1] ≥ 0 ⇒ (UIncreasing(COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1)), ≥)∧[bni_31 + (-1)Bound*bni_31] + [bni_31]i71[5] ≥ 0∧[1 + (-1)bso_32] ≥ 0)



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

    (42)    (i71[5] ≥ 0 ⇒ (UIncreasing(COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1)), ≥)∧[(2)bni_31 + (-1)Bound*bni_31] + [bni_31]i71[5] ≥ 0∧[1 + (-1)bso_32] ≥ 0)







For Pair COND_JMP8731(TRUE, 1, i71, 1) → JMP873'(1, +(i71, -1), 1) the following chains were created:
  • We consider the chain COND_JMP8731(TRUE, 1, i71[6], 1) → JMP873'(1, +(i71[6], -1), 1) which results in the following constraint:

    (43)    (COND_JMP8731(TRUE, 1, i71[6], 1)≥NonInfC∧COND_JMP8731(TRUE, 1, i71[6], 1)≥JMP873'(1, +(i71[6], -1), 1)∧(UIncreasing(JMP873'(1, +(i71[6], -1), 1)), ≥))



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

    (44)    ((UIncreasing(JMP873'(1, +(i71[6], -1), 1)), ≥)∧[(-1)bso_34] ≥ 0)



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

    (45)    ((UIncreasing(JMP873'(1, +(i71[6], -1), 1)), ≥)∧[(-1)bso_34] ≥ 0)



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

    (46)    ((UIncreasing(JMP873'(1, +(i71[6], -1), 1)), ≥)∧[(-1)bso_34] ≥ 0)



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

    (47)    ((UIncreasing(JMP873'(1, +(i71[6], -1), 1)), ≥)∧0 = 0∧[(-1)bso_34] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • JMP981'(i59, i59, i59, i148, i162) → COND_JMP981(>(i162, 0), i59, i59, i59, i148, i162)
    • (i162[0] ≥ 0 ⇒ (UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥)∧[bni_21] = 0∧[(2)bni_21] = 0∧[(-1)bni_21 + (-1)Bound*bni_21] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_22] ≥ 0)

  • COND_JMP981(TRUE, i59, i59, i59, i148, i162) → JMP981'(i59, i59, i59, +(i148, -1), +(i162, -1))
    • ((UIncreasing(JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_24] ≥ 0)

  • JMP873'(i59, i71, i59) → COND_JMP873(&&(>(i59, 0), >=(i71, i59)), i59, i71, i59)
    • (i59[2] ≥ 0∧i71[2] ≥ 0 ⇒ (UIncreasing(COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2])), ≥)∧[(2)bni_25 + (-1)Bound*bni_25] + [(3)bni_25]i59[2] + [bni_25]i71[2] ≥ 0∧[(-1)bso_26] ≥ 0)

  • COND_JMP873(TRUE, i59, i71, i59) → JMP981'(i59, i59, i59, +(+(i71, -1), -1), +(+(i59, -1), -1))
    • ((UIncreasing(JMP981'(i59[3], i59[3], i59[3], +(+(i71[3], -1), -1), +(+(i59[3], -1), -1))), ≥)∧0 = 0∧0 = 0∧[2 + (-1)bso_28] ≥ 0)

  • JMP981'(i59, i59, i59, i148, 0) → JMP873'(i59, i148, i59)
    • ((UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_30] ≥ 0)
    • ((UIncreasing(JMP873'(i59[4], i148[4], i59[4])), ≥)∧0 = 0∧[(-1)bso_30] ≥ 0)

  • JMP873'(1, i71, 1) → COND_JMP8731(&&(>(1, 0), >=(i71, 1)), 1, i71, 1)
    • (i71[5] ≥ 0 ⇒ (UIncreasing(COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1)), ≥)∧[(2)bni_31 + (-1)Bound*bni_31] + [bni_31]i71[5] ≥ 0∧[1 + (-1)bso_32] ≥ 0)

  • COND_JMP8731(TRUE, 1, i71, 1) → JMP873'(1, +(i71, -1), 1)
    • ((UIncreasing(JMP873'(1, +(i71[6], -1), 1)), ≥)∧0 = 0∧[(-1)bso_34] ≥ 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(JMP981'(x1, x2, x3, x4, x5)) = [-1] + x4 + [-1]x3 + x2 + [2]x1   
POL(COND_JMP981(x1, x2, x3, x4, x5, x6)) = [-1] + [2]x4 + x3 + x5 + [-1]x2   
POL(>(x1, x2)) = [-1]   
POL(0) = 0   
POL(+(x1, x2)) = x1 + x2   
POL(-1) = [-1]   
POL(JMP873'(x1, x2, x3)) = [-1] + x1 + x3 + x2   
POL(COND_JMP873(x1, x2, x3, x4)) = [-1] + x4 + x2 + x3   
POL(&&(x1, x2)) = [-1]   
POL(>=(x1, x2)) = [-1]   
POL(1) = [1]   
POL(COND_JMP8731(x1, x2, x3, x4)) = x3   

The following pairs are in P>:

COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))
COND_JMP873(TRUE, i59[3], i71[3], i59[3]) → JMP981'(i59[3], i59[3], i59[3], +(+(i71[3], -1), -1), +(+(i59[3], -1), -1))
JMP873'(1, i71[5], 1) → COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1)

The following pairs are in Pbound:

JMP873'(i59[2], i71[2], i59[2]) → COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2])
JMP873'(1, i71[5], 1) → COND_JMP8731(&&(>(1, 0), >=(i71[5], 1)), 1, i71[5], 1)

The following pairs are in P≥:

JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0]) → COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])
JMP873'(i59[2], i71[2], i59[2]) → COND_JMP873(&&(>(i59[2], 0), >=(i71[2], i59[2])), i59[2], i71[2], i59[2])
JMP981'(i59[4], i59[4], i59[4], i148[4], 0) → JMP873'(i59[4], i148[4], i59[4])
COND_JMP8731(TRUE, 1, i71[6], 1) → JMP873'(1, +(i71[6], -1), 1)

There are no usable rules.

(11) Complex Obligation (AND)

(12) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Integer, Boolean


R is empty.

The integer pair graph contains the following rules and edges:
(0): JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0]) → COND_JMP981(i162[0] > 0, i59[0], i59[0], i59[0], i148[0], i162[0])
(2): JMP873'(i59[2], i71[2], i59[2]) → COND_JMP873(i59[2] > 0 && i71[2] >= i59[2], i59[2], i71[2], i59[2])
(4): JMP981'(i59[4], i59[4], i59[4], i148[4], 0) → JMP873'(i59[4], i148[4], i59[4])
(6): COND_JMP8731(TRUE, 1, i71[6], 1) → JMP873'(1, i71[6] + -1, 1)

(4) -> (2), if ((i59[4] →* i59[2])∧(i148[4] →* i71[2]))


(6) -> (2), if ((i71[6] + -1 →* i71[2])∧(1 →* i59[2]))



The set Q consists of the following terms:
JMP981(x0, x0, x0, x1, x2)
Cond_JMP981(TRUE, x0, x0, x0, x1, x2)
JMP873(x0, x1, x0)
Cond_JMP873(TRUE, x0, x1, x0)
Cond_JMP8731(TRUE, 1, x0, 1)

(13) IDependencyGraphProof (EQUIVALENT transformation)

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

(14) TRUE

(15) 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): JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0]) → COND_JMP981(i162[0] > 0, i59[0], i59[0], i59[0], i148[0], i162[0])
(1): COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], i148[1] + -1, i162[1] + -1)
(3): COND_JMP873(TRUE, i59[3], i71[3], i59[3]) → JMP981'(i59[3], i59[3], i59[3], i71[3] + -1 + -1, i59[3] + -1 + -1)
(4): JMP981'(i59[4], i59[4], i59[4], i148[4], 0) → JMP873'(i59[4], i148[4], i59[4])
(6): COND_JMP8731(TRUE, 1, i71[6], 1) → JMP873'(1, i71[6] + -1, 1)

(1) -> (0), if ((i162[1] + -1 →* i162[0])∧(i59[1] →* i59[0])∧(i148[1] + -1 →* i148[0]))


(3) -> (0), if ((i59[3] →* i59[0])∧(i59[3] + -1 + -1 →* i162[0])∧(i71[3] + -1 + -1 →* i148[0]))


(0) -> (1), if ((i162[0] > 0 →* TRUE)∧(i162[0] →* i162[1])∧(i148[0] →* i148[1])∧(i59[0] →* i59[1]))


(1) -> (4), if ((i59[1] →* i59[4])∧(i162[1] + -1 →* 0)∧(i148[1] + -1 →* i148[4]))


(3) -> (4), if ((i59[3] + -1 + -1 →* 0)∧(i59[3] →* i59[4])∧(i71[3] + -1 + -1 →* i148[4]))



The set Q consists of the following terms:
JMP981(x0, x0, x0, x1, x2)
Cond_JMP981(TRUE, x0, x0, x0, x1, x2)
JMP873(x0, x1, x0)
Cond_JMP873(TRUE, x0, x1, x0)
Cond_JMP8731(TRUE, 1, x0, 1)

(16) IDependencyGraphProof (EQUIVALENT transformation)

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

(17) 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_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], i148[1] + -1, i162[1] + -1)
(0): JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0]) → COND_JMP981(i162[0] > 0, i59[0], i59[0], i59[0], i148[0], i162[0])

(1) -> (0), if ((i162[1] + -1 →* i162[0])∧(i59[1] →* i59[0])∧(i148[1] + -1 →* i148[0]))


(0) -> (1), if ((i162[0] > 0 →* TRUE)∧(i162[0] →* i162[1])∧(i148[0] →* i148[1])∧(i59[0] →* i59[1]))



The set Q consists of the following terms:
JMP981(x0, x0, x0, x1, x2)
Cond_JMP981(TRUE, x0, x0, x0, x1, x2)
JMP873(x0, x1, x0)
Cond_JMP873(TRUE, x0, x1, x0)
Cond_JMP8731(TRUE, 1, x0, 1)

(18) 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 COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1)) the following chains were created:
  • We consider the chain COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1)) which results in the following constraint:

    (1)    (COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1])≥NonInfC∧COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1])≥JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))∧(UIncreasing(JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))), ≥))



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

    (2)    ((UIncreasing(JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))), ≥)∧[(-1)bso_7] ≥ 0)



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

    (3)    ((UIncreasing(JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))), ≥)∧[(-1)bso_7] ≥ 0)



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

    (4)    ((UIncreasing(JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))), ≥)∧[(-1)bso_7] ≥ 0)



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

    (5)    ((UIncreasing(JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_7] ≥ 0)







For Pair JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0]) → COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0]) the following chains were created:
  • We consider the chain JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0]) → COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0]), COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1)) which results in the following constraint:

    (6)    (>(i162[0], 0)=TRUE∧i162[0]=i162[1]∧i148[0]=i148[1]∧i59[0]=i59[1] ⇒ JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0])≥NonInfC∧JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0])≥COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])∧(UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥))



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

    (7)    (>(i162[0], 0)=TRUE ⇒ JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0])≥NonInfC∧JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0])≥COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])∧(UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥))



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

    (8)    (i162[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥)∧[(2)bni_8 + (-1)Bound*bni_8] + [(2)bni_8]i162[0] ≥ 0∧[2 + (-1)bso_9] ≥ 0)



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

    (9)    (i162[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥)∧[(2)bni_8 + (-1)Bound*bni_8] + [(2)bni_8]i162[0] ≥ 0∧[2 + (-1)bso_9] ≥ 0)



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

    (10)    (i162[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥)∧[(2)bni_8 + (-1)Bound*bni_8] + [(2)bni_8]i162[0] ≥ 0∧[2 + (-1)bso_9] ≥ 0)



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

    (11)    (i162[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥)∧0 = 0∧[(2)bni_8 + (-1)Bound*bni_8] + [(2)bni_8]i162[0] ≥ 0∧0 = 0∧[2 + (-1)bso_9] ≥ 0)



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

    (12)    (i162[0] ≥ 0 ⇒ (UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥)∧0 = 0∧[(4)bni_8 + (-1)Bound*bni_8] + [(2)bni_8]i162[0] ≥ 0∧0 = 0∧[2 + (-1)bso_9] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))
    • ((UIncreasing(JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_7] ≥ 0)

  • JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0]) → COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])
    • (i162[0] ≥ 0 ⇒ (UIncreasing(COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])), ≥)∧0 = 0∧[(4)bni_8 + (-1)Bound*bni_8] + [(2)bni_8]i162[0] ≥ 0∧0 = 0∧[2 + (-1)bso_9] ≥ 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(COND_JMP981(x1, x2, x3, x4, x5, x6)) = [2]x6   
POL(JMP981'(x1, x2, x3, x4, x5)) = [2] + [2]x5   
POL(+(x1, x2)) = x1 + x2   
POL(-1) = [-1]   
POL(>(x1, x2)) = 0   
POL(0) = 0   

The following pairs are in P>:

JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0]) → COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])

The following pairs are in Pbound:

JMP981'(i59[0], i59[0], i59[0], i148[0], i162[0]) → COND_JMP981(>(i162[0], 0), i59[0], i59[0], i59[0], i148[0], i162[0])

The following pairs are in P≥:

COND_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], +(i148[1], -1), +(i162[1], -1))

There are no usable rules.

(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_JMP981(TRUE, i59[1], i59[1], i59[1], i148[1], i162[1]) → JMP981'(i59[1], i59[1], i59[1], i148[1] + -1, i162[1] + -1)


The set Q consists of the following terms:
JMP981(x0, x0, x0, x1, x2)
Cond_JMP981(TRUE, x0, x0, x0, x1, x2)
JMP873(x0, x1, x0)
Cond_JMP873(TRUE, x0, x1, x0)
Cond_JMP8731(TRUE, 1, x0, 1)

(20) IDependencyGraphProof (EQUIVALENT transformation)

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

(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:
JMP839(i71, i74) → Cond_JMP839(i74 > 0, i71, i74)
Cond_JMP839(TRUE, i71, i74) → JMP839(i71 + -1, i74 + -1)
The set Q consists of the following terms:
JMP839(x0, x1)
Cond_JMP839(TRUE, x0, x1)

(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:
JMP839(i71, i74) → Cond_JMP839(i74 > 0, i71, i74)
Cond_JMP839(TRUE, i71, i74) → JMP839(i71 + -1, i74 + -1)

The integer pair graph contains the following rules and edges:
(0): JMP839'(i71[0], i74[0]) → COND_JMP839(i74[0] > 0, i71[0], i74[0])
(1): COND_JMP839(TRUE, i71[1], i74[1]) → JMP839'(i71[1] + -1, i74[1] + -1)

(0) -> (1), if ((i74[0] →* i74[1])∧(i74[0] > 0 →* TRUE)∧(i71[0] →* i71[1]))


(1) -> (0), if ((i71[1] + -1 →* i71[0])∧(i74[1] + -1 →* i74[0]))



The set Q consists of the following terms:
JMP839(x0, x1)
Cond_JMP839(TRUE, x0, x1)

(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): JMP839'(i71[0], i74[0]) → COND_JMP839(i74[0] > 0, i71[0], i74[0])
(1): COND_JMP839(TRUE, i71[1], i74[1]) → JMP839'(i71[1] + -1, i74[1] + -1)

(0) -> (1), if ((i74[0] →* i74[1])∧(i74[0] > 0 →* TRUE)∧(i71[0] →* i71[1]))


(1) -> (0), if ((i71[1] + -1 →* i71[0])∧(i74[1] + -1 →* i74[0]))



The set Q consists of the following terms:
JMP839(x0, x1)
Cond_JMP839(TRUE, x0, x1)

(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 JMP839'(i71, i74) → COND_JMP839(>(i74, 0), i71, i74) the following chains were created:
  • We consider the chain JMP839'(i71[0], i74[0]) → COND_JMP839(>(i74[0], 0), i71[0], i74[0]), COND_JMP839(TRUE, i71[1], i74[1]) → JMP839'(+(i71[1], -1), +(i74[1], -1)) which results in the following constraint:

    (1)    (i74[0]=i74[1]∧>(i74[0], 0)=TRUE∧i71[0]=i71[1] ⇒ JMP839'(i71[0], i74[0])≥NonInfC∧JMP839'(i71[0], i74[0])≥COND_JMP839(>(i74[0], 0), i71[0], i74[0])∧(UIncreasing(COND_JMP839(>(i74[0], 0), i71[0], i74[0])), ≥))



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

    (2)    (>(i74[0], 0)=TRUE ⇒ JMP839'(i71[0], i74[0])≥NonInfC∧JMP839'(i71[0], i74[0])≥COND_JMP839(>(i74[0], 0), i71[0], i74[0])∧(UIncreasing(COND_JMP839(>(i74[0], 0), i71[0], i74[0])), ≥))



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

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



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

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



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

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



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

    (6)    (i74[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_JMP839(>(i74[0], 0), i71[0], i74[0])), ≥)∧0 = 0∧[bni_8 + (-1)Bound*bni_8] + [(2)bni_8]i74[0] ≥ 0∧0 = 0∧[2 + (-1)bso_9] ≥ 0)



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

    (7)    (i74[0] ≥ 0 ⇒ (UIncreasing(COND_JMP839(>(i74[0], 0), i71[0], i74[0])), ≥)∧0 = 0∧[(3)bni_8 + (-1)Bound*bni_8] + [(2)bni_8]i74[0] ≥ 0∧0 = 0∧[2 + (-1)bso_9] ≥ 0)







For Pair COND_JMP839(TRUE, i71, i74) → JMP839'(+(i71, -1), +(i74, -1)) the following chains were created:
  • We consider the chain COND_JMP839(TRUE, i71[1], i74[1]) → JMP839'(+(i71[1], -1), +(i74[1], -1)) which results in the following constraint:

    (8)    (COND_JMP839(TRUE, i71[1], i74[1])≥NonInfC∧COND_JMP839(TRUE, i71[1], i74[1])≥JMP839'(+(i71[1], -1), +(i74[1], -1))∧(UIncreasing(JMP839'(+(i71[1], -1), +(i74[1], -1))), ≥))



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

    (9)    ((UIncreasing(JMP839'(+(i71[1], -1), +(i74[1], -1))), ≥)∧[(-1)bso_11] ≥ 0)



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

    (10)    ((UIncreasing(JMP839'(+(i71[1], -1), +(i74[1], -1))), ≥)∧[(-1)bso_11] ≥ 0)



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

    (11)    ((UIncreasing(JMP839'(+(i71[1], -1), +(i74[1], -1))), ≥)∧[(-1)bso_11] ≥ 0)



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

    (12)    ((UIncreasing(JMP839'(+(i71[1], -1), +(i74[1], -1))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_11] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • JMP839'(i71, i74) → COND_JMP839(>(i74, 0), i71, i74)
    • (i74[0] ≥ 0 ⇒ (UIncreasing(COND_JMP839(>(i74[0], 0), i71[0], i74[0])), ≥)∧0 = 0∧[(3)bni_8 + (-1)Bound*bni_8] + [(2)bni_8]i74[0] ≥ 0∧0 = 0∧[2 + (-1)bso_9] ≥ 0)

  • COND_JMP839(TRUE, i71, i74) → JMP839'(+(i71, -1), +(i74, -1))
    • ((UIncreasing(JMP839'(+(i71[1], -1), +(i74[1], -1))), ≥)∧0 = 0∧0 = 0∧[(-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(JMP839'(x1, x2)) = [1] + [2]x2   
POL(COND_JMP839(x1, x2, x3)) = [-1] + [2]x3   
POL(>(x1, x2)) = [-1]   
POL(0) = 0   
POL(+(x1, x2)) = x1 + x2   
POL(-1) = [-1]   

The following pairs are in P>:

JMP839'(i71[0], i74[0]) → COND_JMP839(>(i74[0], 0), i71[0], i74[0])

The following pairs are in Pbound:

JMP839'(i71[0], i74[0]) → COND_JMP839(>(i74[0], 0), i71[0], i74[0])

The following pairs are in P≥:

COND_JMP839(TRUE, i71[1], i74[1]) → JMP839'(+(i71[1], -1), +(i74[1], -1))

There are no usable rules.

(28) 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_JMP839(TRUE, i71[1], i74[1]) → JMP839'(i71[1] + -1, i74[1] + -1)


The set Q consists of the following terms:
JMP839(x0, x1)
Cond_JMP839(TRUE, x0, x1)

(29) IDependencyGraphProof (EQUIVALENT transformation)

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

(30) TRUE