Termination of the given JBC could be proven:

0 JBC
↳1 JBC2FIG (⇒)
↳2 JBCTerminationGraph
↳3 FIGtoITRSProof (⇒)
↳4 IDP
↳5 IDPNonInfProof (⇒)
↳6 IDP
↳7 IDependencyGraphProof (⇔)
↳8 IDP
↳9 UsableRulesProof (⇔)
↳10 IDP
↳11 IDPtoQDPProof (⇒)
↳12 QDP
↳13 UsableRulesProof (⇔)
↳14 QDP
↳15 QReductionProof (⇔)
↳16 QDP
↳17 Instantiation (⇔)
↳18 QDP
↳19 Induction-Processor (⇒)
↳20 AND
    ↳21 QDP
        ↳22 DependencyGraphProof (⇔)
        ↳23 TRUE
    ↳24 QTRS
        ↳25 QTRSRRRProof (⇔)
        ↳26 QTRS
        ↳27 RisEmptyProof (⇔)
        ↳28 YES

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: DivWithoutMinus 
public class DivWithoutMinus{
  // adaption of the algorithm from [Kolbe 95]
  public static void main(String[] args) {
    Random.args = args;

    int x = Random.random();
    int y = Random.random();
    int z = y;
    int res = 0;

    while (z > 0 && (y == 0 || y > 0 && x > 0))	{

      if (y == 0) {
        res++;
        y = z;
      }
      else {
        x--;
        y--;
      }
    }
  }
}



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

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


(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
DivWithoutMinus.main([Ljava/lang/String;)V: Graph of 184 nodes with 1 SCC.


(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Logs:

Log for SCC 0:

Generated 27 rules for P and 8 rules for R.


Combined rules. Obtained 2 rules for P and 1 rules for R.


Filtered ground terms:


983_0_main_LE(x1, x2, x3, x4, x5) → 983_0_main_LE(x2, x3, x4, x5)
Cond_983_0_main_LE1(x1, x2, x3, x4, x5, x6) → Cond_983_0_main_LE1(x1, x3, x5, x6)
Cond_983_0_main_LE(x1, x2, x3, x4, x5, x6) → Cond_983_0_main_LE(x1, x3, x4, x5, x6)
986_0_main_Return(x1) → 986_0_main_Return

Filtered duplicate args:


983_0_main_LE(x1, x2, x3, x4) → 983_0_main_LE(x1, x2, x4)
Cond_983_0_main_LE1(x1, x2, x3, x4) → Cond_983_0_main_LE1(x1, x2, x4)
Cond_983_0_main_LE(x1, x2, x3, x4, x5) → Cond_983_0_main_LE(x1, x2, x3, x5)

Combined rules. Obtained 2 rules for P and 1 rules for R.


Finished conversion. Obtained 2 rules for P and 1 rules for R. System has predefined symbols.


(4) 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:
983_0_main_LE(x0, x1, x2) → Cond_983_0_main_LE(x2 <= 0, x0, x1, x2)
Cond_983_0_main_LE(TRUE, x0, x1, x2) → 986_0_main_Return

The integer pair graph contains the following rules and edges:
(0): 983_0_MAIN_LE(x0[0], x1[0], x2[0]) → COND_983_0_MAIN_LE(x2[0] > 0 && x1[0] > 0 && x0[0] > 0, x0[0], x1[0], x2[0])
(1): COND_983_0_MAIN_LE(TRUE, x0[1], x1[1], x2[1]) → 983_0_MAIN_LE(x0[1] + -1, x1[1] + -1, x2[1])
(2): 983_0_MAIN_LE(x0[2], 0, x2[2]) → COND_983_0_MAIN_LE1(x2[2] > 0, x0[2], 0, x2[2])
(3): COND_983_0_MAIN_LE1(TRUE, x0[3], 0, x2[3]) → 983_0_MAIN_LE(x0[3], x2[3], x2[3])

(0) -> (1), if ((x2[0] > 0 && x1[0] > 0 && x0[0] > 0 →* TRUE)∧(x0[0] →* x0[1])∧(x1[0] →* x1[1])∧(x2[0] →* x2[1]))


(1) -> (0), if ((x0[1] + -1 →* x0[0])∧(x1[1] + -1 →* x1[0])∧(x2[1] →* x2[0]))


(1) -> (2), if ((x0[1] + -1 →* x0[2])∧(x1[1] + -1 →* 0)∧(x2[1] →* x2[2]))


(2) -> (3), if ((x2[2] > 0 →* TRUE)∧(x0[2] →* x0[3])∧(x2[2] →* x2[3]))


(3) -> (0), if ((x0[3] →* x0[0])∧(x2[3] →* x1[0])∧(x2[3] →* x2[0]))


(3) -> (2), if ((x0[3] →* x0[2])∧(x2[3] →* 0)∧(x2[3] →* x2[2]))



The set Q consists of the following terms:
983_0_main_LE(x0, x1, x2)
Cond_983_0_main_LE(TRUE, x0, x1, x2)

(5) 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 983_0_MAIN_LE(x0, x1, x2) → COND_983_0_MAIN_LE(&&(&&(>(x2, 0), >(x1, 0)), >(x0, 0)), x0, x1, x2) the following chains were created:
  • We consider the chain 983_0_MAIN_LE(x0[0], x1[0], x2[0]) → COND_983_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0]), COND_983_0_MAIN_LE(TRUE, x0[1], x1[1], x2[1]) → 983_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1]) which results in the following constraint:

    (1)    (&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0))=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1]∧x2[0]=x2[1] ⇒ 983_0_MAIN_LE(x0[0], x1[0], x2[0])≥NonInfC∧983_0_MAIN_LE(x0[0], x1[0], x2[0])≥COND_983_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])∧(UIncreasing(COND_983_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])), ≥))



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

    (2)    (>(x0[0], 0)=TRUE∧>(x2[0], 0)=TRUE∧>(x1[0], 0)=TRUE ⇒ 983_0_MAIN_LE(x0[0], x1[0], x2[0])≥NonInfC∧983_0_MAIN_LE(x0[0], x1[0], x2[0])≥COND_983_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])∧(UIncreasing(COND_983_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])), ≥))



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

    (3)    (x0[0] + [-1] ≥ 0∧x2[0] + [-1] ≥ 0∧x1[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_983_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])), ≥)∧[(2)bni_30 + (-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[1 + (-1)bso_31] ≥ 0)



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

    (4)    (x0[0] + [-1] ≥ 0∧x2[0] + [-1] ≥ 0∧x1[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_983_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])), ≥)∧[(2)bni_30 + (-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[1 + (-1)bso_31] ≥ 0)



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

    (5)    (x0[0] + [-1] ≥ 0∧x2[0] + [-1] ≥ 0∧x1[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_983_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])), ≥)∧[(2)bni_30 + (-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[1 + (-1)bso_31] ≥ 0)



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

    (6)    (x0[0] ≥ 0∧x2[0] + [-1] ≥ 0∧x1[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_983_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])), ≥)∧[(3)bni_30 + (-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[1 + (-1)bso_31] ≥ 0)



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

    (7)    (x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_983_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])), ≥)∧[(3)bni_30 + (-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[1 + (-1)bso_31] ≥ 0)



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

    (8)    (x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_983_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])), ≥)∧[(3)bni_30 + (-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[1 + (-1)bso_31] ≥ 0)







For Pair COND_983_0_MAIN_LE(TRUE, x0, x1, x2) → 983_0_MAIN_LE(+(x0, -1), +(x1, -1), x2) the following chains were created:
  • We consider the chain 983_0_MAIN_LE(x0[0], x1[0], x2[0]) → COND_983_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0]), COND_983_0_MAIN_LE(TRUE, x0[1], x1[1], x2[1]) → 983_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1]), 983_0_MAIN_LE(x0[0], x1[0], x2[0]) → COND_983_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0]) which results in the following constraint:

    (9)    (&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0))=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1]∧x2[0]=x2[1]∧+(x0[1], -1)=x0[0]1∧+(x1[1], -1)=x1[0]1∧x2[1]=x2[0]1 ⇒ COND_983_0_MAIN_LE(TRUE, x0[1], x1[1], x2[1])≥NonInfC∧COND_983_0_MAIN_LE(TRUE, x0[1], x1[1], x2[1])≥983_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])∧(UIncreasing(983_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥))



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

    (10)    (>(x0[0], 0)=TRUE∧>(x2[0], 0)=TRUE∧>(x1[0], 0)=TRUE ⇒ COND_983_0_MAIN_LE(TRUE, x0[0], x1[0], x2[0])≥NonInfC∧COND_983_0_MAIN_LE(TRUE, x0[0], x1[0], x2[0])≥983_0_MAIN_LE(+(x0[0], -1), +(x1[0], -1), x2[0])∧(UIncreasing(983_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥))



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

    (11)    (x0[0] + [-1] ≥ 0∧x2[0] + [-1] ≥ 0∧x1[0] + [-1] ≥ 0 ⇒ (UIncreasing(983_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[bni_32 + (-1)Bound*bni_32] + [bni_32]x0[0] ≥ 0∧[(-1)bso_33] ≥ 0)



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

    (12)    (x0[0] + [-1] ≥ 0∧x2[0] + [-1] ≥ 0∧x1[0] + [-1] ≥ 0 ⇒ (UIncreasing(983_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[bni_32 + (-1)Bound*bni_32] + [bni_32]x0[0] ≥ 0∧[(-1)bso_33] ≥ 0)



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

    (13)    (x0[0] + [-1] ≥ 0∧x2[0] + [-1] ≥ 0∧x1[0] + [-1] ≥ 0 ⇒ (UIncreasing(983_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[bni_32 + (-1)Bound*bni_32] + [bni_32]x0[0] ≥ 0∧[(-1)bso_33] ≥ 0)



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

    (14)    (x0[0] ≥ 0∧x2[0] + [-1] ≥ 0∧x1[0] + [-1] ≥ 0 ⇒ (UIncreasing(983_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[(2)bni_32 + (-1)Bound*bni_32] + [bni_32]x0[0] ≥ 0∧[(-1)bso_33] ≥ 0)



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

    (15)    (x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] + [-1] ≥ 0 ⇒ (UIncreasing(983_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[(2)bni_32 + (-1)Bound*bni_32] + [bni_32]x0[0] ≥ 0∧[(-1)bso_33] ≥ 0)



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

    (16)    (x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(983_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[(2)bni_32 + (-1)Bound*bni_32] + [bni_32]x0[0] ≥ 0∧[(-1)bso_33] ≥ 0)



  • We consider the chain 983_0_MAIN_LE(x0[0], x1[0], x2[0]) → COND_983_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0]), COND_983_0_MAIN_LE(TRUE, x0[1], x1[1], x2[1]) → 983_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1]), 983_0_MAIN_LE(x0[2], 0, x2[2]) → COND_983_0_MAIN_LE1(>(x2[2], 0), x0[2], 0, x2[2]) which results in the following constraint:

    (17)    (&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0))=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1]∧x2[0]=x2[1]∧+(x0[1], -1)=x0[2]∧+(x1[1], -1)=0∧x2[1]=x2[2] ⇒ COND_983_0_MAIN_LE(TRUE, x0[1], x1[1], x2[1])≥NonInfC∧COND_983_0_MAIN_LE(TRUE, x0[1], x1[1], x2[1])≥983_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])∧(UIncreasing(983_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥))



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

    (18)    (+(x1[0], -1)=0∧>(x0[0], 0)=TRUE∧>(x2[0], 0)=TRUE∧>(x1[0], 0)=TRUE ⇒ COND_983_0_MAIN_LE(TRUE, x0[0], x1[0], x2[0])≥NonInfC∧COND_983_0_MAIN_LE(TRUE, x0[0], x1[0], x2[0])≥983_0_MAIN_LE(+(x0[0], -1), +(x1[0], -1), x2[0])∧(UIncreasing(983_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥))



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

    (19)    (x1[0] + [-1] ≥ 0∧x0[0] + [-1] ≥ 0∧x2[0] + [-1] ≥ 0∧x1[0] + [-1] ≥ 0 ⇒ (UIncreasing(983_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[bni_32 + (-1)Bound*bni_32] + [bni_32]x0[0] ≥ 0∧[(-1)bso_33] ≥ 0)



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

    (20)    (x1[0] + [-1] ≥ 0∧x0[0] + [-1] ≥ 0∧x2[0] + [-1] ≥ 0∧x1[0] + [-1] ≥ 0 ⇒ (UIncreasing(983_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[bni_32 + (-1)Bound*bni_32] + [bni_32]x0[0] ≥ 0∧[(-1)bso_33] ≥ 0)



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

    (21)    (x1[0] + [-1] ≥ 0∧x0[0] + [-1] ≥ 0∧x2[0] + [-1] ≥ 0∧x1[0] + [-1] ≥ 0 ⇒ (UIncreasing(983_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[bni_32 + (-1)Bound*bni_32] + [bni_32]x0[0] ≥ 0∧[(-1)bso_33] ≥ 0)



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

    (22)    (x1[0] ≥ 0∧x0[0] + [-1] ≥ 0∧x2[0] + [-1] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(983_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[bni_32 + (-1)Bound*bni_32] + [bni_32]x0[0] ≥ 0∧[(-1)bso_33] ≥ 0)



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

    (23)    (x1[0] ≥ 0∧x0[0] ≥ 0∧x2[0] + [-1] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(983_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[(2)bni_32 + (-1)Bound*bni_32] + [bni_32]x0[0] ≥ 0∧[(-1)bso_33] ≥ 0)



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

    (24)    (x1[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(983_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[(2)bni_32 + (-1)Bound*bni_32] + [bni_32]x0[0] ≥ 0∧[(-1)bso_33] ≥ 0)







For Pair 983_0_MAIN_LE(x0, 0, x2) → COND_983_0_MAIN_LE1(>(x2, 0), x0, 0, x2) the following chains were created:
  • We consider the chain 983_0_MAIN_LE(x0[2], 0, x2[2]) → COND_983_0_MAIN_LE1(>(x2[2], 0), x0[2], 0, x2[2]), COND_983_0_MAIN_LE1(TRUE, x0[3], 0, x2[3]) → 983_0_MAIN_LE(x0[3], x2[3], x2[3]) which results in the following constraint:

    (25)    (>(x2[2], 0)=TRUE∧x0[2]=x0[3]∧x2[2]=x2[3] ⇒ 983_0_MAIN_LE(x0[2], 0, x2[2])≥NonInfC∧983_0_MAIN_LE(x0[2], 0, x2[2])≥COND_983_0_MAIN_LE1(>(x2[2], 0), x0[2], 0, x2[2])∧(UIncreasing(COND_983_0_MAIN_LE1(>(x2[2], 0), x0[2], 0, x2[2])), ≥))



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

    (26)    (>(x2[2], 0)=TRUE ⇒ 983_0_MAIN_LE(x0[2], 0, x2[2])≥NonInfC∧983_0_MAIN_LE(x0[2], 0, x2[2])≥COND_983_0_MAIN_LE1(>(x2[2], 0), x0[2], 0, x2[2])∧(UIncreasing(COND_983_0_MAIN_LE1(>(x2[2], 0), x0[2], 0, x2[2])), ≥))



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

    (27)    (x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_983_0_MAIN_LE1(>(x2[2], 0), x0[2], 0, x2[2])), ≥)∧[(2)bni_34 + (-1)Bound*bni_34] + [bni_34]x0[2] ≥ 0∧[(-1)bso_35] ≥ 0)



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

    (28)    (x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_983_0_MAIN_LE1(>(x2[2], 0), x0[2], 0, x2[2])), ≥)∧[(2)bni_34 + (-1)Bound*bni_34] + [bni_34]x0[2] ≥ 0∧[(-1)bso_35] ≥ 0)



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

    (29)    (x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_983_0_MAIN_LE1(>(x2[2], 0), x0[2], 0, x2[2])), ≥)∧[(2)bni_34 + (-1)Bound*bni_34] + [bni_34]x0[2] ≥ 0∧[(-1)bso_35] ≥ 0)



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

    (30)    (x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_983_0_MAIN_LE1(>(x2[2], 0), x0[2], 0, x2[2])), ≥)∧[bni_34] = 0∧[(2)bni_34 + (-1)Bound*bni_34] ≥ 0∧0 = 0∧[(-1)bso_35] ≥ 0)



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

    (31)    (x2[2] ≥ 0 ⇒ (UIncreasing(COND_983_0_MAIN_LE1(>(x2[2], 0), x0[2], 0, x2[2])), ≥)∧[bni_34] = 0∧[(2)bni_34 + (-1)Bound*bni_34] ≥ 0∧0 = 0∧[(-1)bso_35] ≥ 0)







For Pair COND_983_0_MAIN_LE1(TRUE, x0, 0, x2) → 983_0_MAIN_LE(x0, x2, x2) the following chains were created:
  • We consider the chain COND_983_0_MAIN_LE1(TRUE, x0[3], 0, x2[3]) → 983_0_MAIN_LE(x0[3], x2[3], x2[3]), 983_0_MAIN_LE(x0[0], x1[0], x2[0]) → COND_983_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0]) which results in the following constraint:

    (32)    (x0[3]=x0[0]∧x2[3]=x1[0]∧x2[3]=x2[0] ⇒ COND_983_0_MAIN_LE1(TRUE, x0[3], 0, x2[3])≥NonInfC∧COND_983_0_MAIN_LE1(TRUE, x0[3], 0, x2[3])≥983_0_MAIN_LE(x0[3], x2[3], x2[3])∧(UIncreasing(983_0_MAIN_LE(x0[3], x2[3], x2[3])), ≥))



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

    (33)    (COND_983_0_MAIN_LE1(TRUE, x0[3], 0, x2[3])≥NonInfC∧COND_983_0_MAIN_LE1(TRUE, x0[3], 0, x2[3])≥983_0_MAIN_LE(x0[3], x2[3], x2[3])∧(UIncreasing(983_0_MAIN_LE(x0[3], x2[3], x2[3])), ≥))



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

    (34)    ((UIncreasing(983_0_MAIN_LE(x0[3], x2[3], x2[3])), ≥)∧[(-1)bso_37] ≥ 0)



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

    (35)    ((UIncreasing(983_0_MAIN_LE(x0[3], x2[3], x2[3])), ≥)∧[(-1)bso_37] ≥ 0)



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

    (36)    ((UIncreasing(983_0_MAIN_LE(x0[3], x2[3], x2[3])), ≥)∧[(-1)bso_37] ≥ 0)



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

    (37)    ((UIncreasing(983_0_MAIN_LE(x0[3], x2[3], x2[3])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)



  • We consider the chain COND_983_0_MAIN_LE1(TRUE, x0[3], 0, x2[3]) → 983_0_MAIN_LE(x0[3], x2[3], x2[3]), 983_0_MAIN_LE(x0[2], 0, x2[2]) → COND_983_0_MAIN_LE1(>(x2[2], 0), x0[2], 0, x2[2]) which results in the following constraint:

    (38)    (x0[3]=x0[2]∧x2[3]=0∧x2[3]=x2[2] ⇒ COND_983_0_MAIN_LE1(TRUE, x0[3], 0, x2[3])≥NonInfC∧COND_983_0_MAIN_LE1(TRUE, x0[3], 0, x2[3])≥983_0_MAIN_LE(x0[3], x2[3], x2[3])∧(UIncreasing(983_0_MAIN_LE(x0[3], x2[3], x2[3])), ≥))



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

    (39)    (COND_983_0_MAIN_LE1(TRUE, x0[3], 0, 0)≥NonInfC∧COND_983_0_MAIN_LE1(TRUE, x0[3], 0, 0)≥983_0_MAIN_LE(x0[3], 0, 0)∧(UIncreasing(983_0_MAIN_LE(x0[3], x2[3], x2[3])), ≥))



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

    (40)    ((UIncreasing(983_0_MAIN_LE(x0[3], x2[3], x2[3])), ≥)∧[(-1)bso_37] ≥ 0)



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

    (41)    ((UIncreasing(983_0_MAIN_LE(x0[3], x2[3], x2[3])), ≥)∧[(-1)bso_37] ≥ 0)



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

    (42)    ((UIncreasing(983_0_MAIN_LE(x0[3], x2[3], x2[3])), ≥)∧[(-1)bso_37] ≥ 0)



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

    (43)    ((UIncreasing(983_0_MAIN_LE(x0[3], x2[3], x2[3])), ≥)∧0 = 0∧[(-1)bso_37] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • 983_0_MAIN_LE(x0, x1, x2) → COND_983_0_MAIN_LE(&&(&&(>(x2, 0), >(x1, 0)), >(x0, 0)), x0, x1, x2)
    • (x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_983_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])), ≥)∧[(3)bni_30 + (-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[1 + (-1)bso_31] ≥ 0)

  • COND_983_0_MAIN_LE(TRUE, x0, x1, x2) → 983_0_MAIN_LE(+(x0, -1), +(x1, -1), x2)
    • (x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(983_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[(2)bni_32 + (-1)Bound*bni_32] + [bni_32]x0[0] ≥ 0∧[(-1)bso_33] ≥ 0)
    • (x1[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(983_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[(2)bni_32 + (-1)Bound*bni_32] + [bni_32]x0[0] ≥ 0∧[(-1)bso_33] ≥ 0)

  • 983_0_MAIN_LE(x0, 0, x2) → COND_983_0_MAIN_LE1(>(x2, 0), x0, 0, x2)
    • (x2[2] ≥ 0 ⇒ (UIncreasing(COND_983_0_MAIN_LE1(>(x2[2], 0), x0[2], 0, x2[2])), ≥)∧[bni_34] = 0∧[(2)bni_34 + (-1)Bound*bni_34] ≥ 0∧0 = 0∧[(-1)bso_35] ≥ 0)

  • COND_983_0_MAIN_LE1(TRUE, x0, 0, x2) → 983_0_MAIN_LE(x0, x2, x2)
    • ((UIncreasing(983_0_MAIN_LE(x0[3], x2[3], x2[3])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)
    • ((UIncreasing(983_0_MAIN_LE(x0[3], x2[3], x2[3])), ≥)∧0 = 0∧[(-1)bso_37] ≥ 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(983_0_main_LE(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2 + [-1]x1   
POL(Cond_983_0_main_LE(x1, x2, x3, x4)) = [-1] + [-1]x4 + [-1]x3 + [-1]x2 + [-1]x1   
POL(<=(x1, x2)) = [-1]   
POL(0) = 0   
POL(986_0_main_Return) = [-1]   
POL(983_0_MAIN_LE(x1, x2, x3)) = [2] + x1   
POL(COND_983_0_MAIN_LE(x1, x2, x3, x4)) = [1] + x2 + [-1]x1   
POL(&&(x1, x2)) = 0   
POL(>(x1, x2)) = [-1]   
POL(+(x1, x2)) = x1 + x2   
POL(-1) = [-1]   
POL(COND_983_0_MAIN_LE1(x1, x2, x3, x4)) = [2] + [-1]x3 + x2   

The following pairs are in P>:

983_0_MAIN_LE(x0[0], x1[0], x2[0]) → COND_983_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])

The following pairs are in Pbound:

983_0_MAIN_LE(x0[0], x1[0], x2[0]) → COND_983_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])
COND_983_0_MAIN_LE(TRUE, x0[1], x1[1], x2[1]) → 983_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])

The following pairs are in P≥:

COND_983_0_MAIN_LE(TRUE, x0[1], x1[1], x2[1]) → 983_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])
983_0_MAIN_LE(x0[2], 0, x2[2]) → COND_983_0_MAIN_LE1(>(x2[2], 0), x0[2], 0, x2[2])
COND_983_0_MAIN_LE1(TRUE, x0[3], 0, x2[3]) → 983_0_MAIN_LE(x0[3], x2[3], x2[3])

At least the following rules have been oriented under context sensitive arithmetic replacement:

&&(TRUE, TRUE)1 ↔ TRUE1
&&(TRUE, FALSE)1 ↔ FALSE1
&&(FALSE, TRUE)1 ↔ FALSE1
&&(FALSE, FALSE)1 ↔ FALSE1

(6) Obligation:

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


The following domains are used:

Integer


The ITRS R consists of the following rules:
983_0_main_LE(x0, x1, x2) → Cond_983_0_main_LE(x2 <= 0, x0, x1, x2)
Cond_983_0_main_LE(TRUE, x0, x1, x2) → 986_0_main_Return

The integer pair graph contains the following rules and edges:
(1): COND_983_0_MAIN_LE(TRUE, x0[1], x1[1], x2[1]) → 983_0_MAIN_LE(x0[1] + -1, x1[1] + -1, x2[1])
(2): 983_0_MAIN_LE(x0[2], 0, x2[2]) → COND_983_0_MAIN_LE1(x2[2] > 0, x0[2], 0, x2[2])
(3): COND_983_0_MAIN_LE1(TRUE, x0[3], 0, x2[3]) → 983_0_MAIN_LE(x0[3], x2[3], x2[3])

(1) -> (2), if ((x0[1] + -1 →* x0[2])∧(x1[1] + -1 →* 0)∧(x2[1] →* x2[2]))


(3) -> (2), if ((x0[3] →* x0[2])∧(x2[3] →* 0)∧(x2[3] →* x2[2]))


(2) -> (3), if ((x2[2] > 0 →* TRUE)∧(x0[2] →* x0[3])∧(x2[2] →* x2[3]))



The set Q consists of the following terms:
983_0_main_LE(x0, x1, x2)
Cond_983_0_main_LE(TRUE, x0, x1, x2)

(7) IDependencyGraphProof (EQUIVALENT transformation)

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

(8) Obligation:

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


The following domains are used:

Integer


The ITRS R consists of the following rules:
983_0_main_LE(x0, x1, x2) → Cond_983_0_main_LE(x2 <= 0, x0, x1, x2)
Cond_983_0_main_LE(TRUE, x0, x1, x2) → 986_0_main_Return

The integer pair graph contains the following rules and edges:
(3): COND_983_0_MAIN_LE1(TRUE, x0[3], 0, x2[3]) → 983_0_MAIN_LE(x0[3], x2[3], x2[3])
(2): 983_0_MAIN_LE(x0[2], 0, x2[2]) → COND_983_0_MAIN_LE1(x2[2] > 0, x0[2], 0, x2[2])

(3) -> (2), if ((x0[3] →* x0[2])∧(x2[3] →* 0)∧(x2[3] →* x2[2]))


(2) -> (3), if ((x2[2] > 0 →* TRUE)∧(x0[2] →* x0[3])∧(x2[2] →* x2[3]))



The set Q consists of the following terms:
983_0_main_LE(x0, x1, x2)
Cond_983_0_main_LE(TRUE, x0, x1, x2)

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

(10) 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:
(3): COND_983_0_MAIN_LE1(TRUE, x0[3], 0, x2[3]) → 983_0_MAIN_LE(x0[3], x2[3], x2[3])
(2): 983_0_MAIN_LE(x0[2], 0, x2[2]) → COND_983_0_MAIN_LE1(x2[2] > 0, x0[2], 0, x2[2])

(3) -> (2), if ((x0[3] →* x0[2])∧(x2[3] →* 0)∧(x2[3] →* x2[2]))


(2) -> (3), if ((x2[2] > 0 →* TRUE)∧(x0[2] →* x0[3])∧(x2[2] →* x2[3]))



The set Q consists of the following terms:
983_0_main_LE(x0, x1, x2)
Cond_983_0_main_LE(TRUE, x0, x1, x2)

(11) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(12) Obligation:

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

COND_983_0_MAIN_LE1(true, x0[3], pos(01), x2[3]) → 983_0_MAIN_LE(x0[3], x2[3], x2[3])
983_0_MAIN_LE(x0[2], pos(01), x2[2]) → COND_983_0_MAIN_LE1(greater_int(x2[2], pos(01)), x0[2], pos(01), x2[2])

The TRS R consists of the following rules:

greater_int(pos(01), pos(01)) → false
greater_int(pos(01), neg(01)) → false
greater_int(neg(01), pos(01)) → false
greater_int(neg(01), neg(01)) → false
greater_int(pos(01), pos(s(y))) → false
greater_int(neg(01), pos(s(y))) → false
greater_int(pos(01), neg(s(y))) → true
greater_int(neg(01), neg(s(y))) → true
greater_int(pos(s(x)), pos(01)) → true
greater_int(neg(s(x)), pos(01)) → false
greater_int(pos(s(x)), neg(01)) → true
greater_int(neg(s(x)), neg(01)) → false
greater_int(pos(s(x)), neg(s(y))) → true
greater_int(neg(s(x)), pos(s(y))) → false
greater_int(pos(s(x)), pos(s(y))) → greater_int(pos(x), pos(y))
greater_int(neg(s(x)), neg(s(y))) → greater_int(neg(x), neg(y))

The set Q consists of the following terms:

983_0_main_LE(x0, x1, x2)
Cond_983_0_main_LE(true, x0, x1, x2)
greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

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

(14) Obligation:

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

COND_983_0_MAIN_LE1(true, x0[3], pos(01), x2[3]) → 983_0_MAIN_LE(x0[3], x2[3], x2[3])
983_0_MAIN_LE(x0[2], pos(01), x2[2]) → COND_983_0_MAIN_LE1(greater_int(x2[2], pos(01)), x0[2], pos(01), x2[2])

The TRS R consists of the following rules:

greater_int(pos(01), pos(01)) → false
greater_int(neg(01), pos(01)) → false
greater_int(pos(s(x)), pos(01)) → true
greater_int(neg(s(x)), pos(01)) → false

The set Q consists of the following terms:

983_0_main_LE(x0, x1, x2)
Cond_983_0_main_LE(true, x0, x1, x2)
greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

(15) QReductionProof (EQUIVALENT transformation)

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

983_0_main_LE(x0, x1, x2)
Cond_983_0_main_LE(true, x0, x1, x2)

(16) Obligation:

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

COND_983_0_MAIN_LE1(true, x0[3], pos(01), x2[3]) → 983_0_MAIN_LE(x0[3], x2[3], x2[3])
983_0_MAIN_LE(x0[2], pos(01), x2[2]) → COND_983_0_MAIN_LE1(greater_int(x2[2], pos(01)), x0[2], pos(01), x2[2])

The TRS R consists of the following rules:

greater_int(pos(01), pos(01)) → false
greater_int(neg(01), pos(01)) → false
greater_int(pos(s(x)), pos(01)) → true
greater_int(neg(s(x)), pos(01)) → false

The set Q consists of the following terms:

greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

(17) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule 983_0_MAIN_LE(x0[2], pos(01), x2[2]) → COND_983_0_MAIN_LE1(greater_int(x2[2], pos(01)), x0[2], pos(01), x2[2]) we obtained the following new rules [LPAR04]:

983_0_MAIN_LE(z0, pos(01), pos(01)) → COND_983_0_MAIN_LE1(greater_int(pos(01), pos(01)), z0, pos(01), pos(01))

(18) Obligation:

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

COND_983_0_MAIN_LE1(true, x0[3], pos(01), x2[3]) → 983_0_MAIN_LE(x0[3], x2[3], x2[3])
983_0_MAIN_LE(z0, pos(01), pos(01)) → COND_983_0_MAIN_LE1(greater_int(pos(01), pos(01)), z0, pos(01), pos(01))

The TRS R consists of the following rules:

greater_int(pos(01), pos(01)) → false
greater_int(neg(01), pos(01)) → false
greater_int(pos(s(x)), pos(01)) → true
greater_int(neg(s(x)), pos(01)) → false

The set Q consists of the following terms:

greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

(19) Induction-Processor (SOUND transformation)


This DP could be deleted by the Induction-Processor:
983_0_MAIN_LE(z0, pos(01), pos(01)) → COND_983_0_MAIN_LE1(greater_int(pos(01), pos(01)), z0, pos(01), pos(01))


This order was computed:
Polynomial interpretation [POLO]:

POL(01) = 0   
POL(983_0_MAIN_LE(x1, x2, x3)) = 1 + x1   
POL(COND_983_0_MAIN_LE1(x1, x2, x3, x4)) = x1 + x2 + x4   
POL(false) = 0   
POL(greater_int(x1, x2)) = 1 + x1   
POL(neg(x1)) = 1   
POL(pos(x1)) = x1   
POL(s(x1)) = 1   
POL(true) = 1   
POL(witness_sort[a9]) = 1   

At least one of these decreasing rules is always used after the deleted DP:
greater_int(pos(01), pos(01)) → false
greater_int(neg(01), pos(01)) → false
greater_int(pos(s(x2'')), pos(01)) → true
greater_int(neg(s(x51)), pos(01)) → false


The following formula is valid:
z0:sort[a9].(z0 =pos(01)→greaterint'(z0 , z0 )=true)


The transformed set:
greater_int'(pos(01), pos(01)) → true
greater_int'(neg(01), pos(01)) → true
greater_int'(pos(s(x2)), pos(01)) → true
greater_int'(neg(s(x5)), pos(01)) → true
greater_int'(pos(01), pos(s(x1))) → false
greater_int'(pos(01), neg(x0)) → false
greater_int'(pos(01), witness_sort[a9]) → false
greater_int'(pos(s(x0)), x1) → false
greater_int'(neg(01), pos(s(x1))) → false
greater_int'(neg(01), neg(x0)) → false
greater_int'(neg(01), witness_sort[a9]) → false
greater_int'(neg(s(x0)), pos(s(x1))) → false
greater_int'(neg(s(x0)), neg(x2)) → false
greater_int'(neg(s(x0)), witness_sort[a9]) → false
greater_int'(witness_sort[a9], x1) → false
greater_int(pos(01), pos(01)) → false
greater_int(neg(01), pos(01)) → false
greater_int(pos(s(x2)), pos(01)) → true
greater_int(neg(s(x5)), pos(01)) → false
greater_int(pos(01), pos(s(x1))) → false
greater_int(pos(01), neg(x0)) → false
greater_int(pos(01), witness_sort[a9]) → false
greater_int(pos(s(x0)), x1) → false
greater_int(neg(01), pos(s(x1))) → false
greater_int(neg(01), neg(x0)) → false
greater_int(neg(01), witness_sort[a9]) → false
greater_int(neg(s(x0)), pos(s(x1))) → false
greater_int(neg(s(x0)), neg(x2)) → false
greater_int(neg(s(x0)), witness_sort[a9]) → false
greater_int(witness_sort[a9], x1) → false
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](witness_sort[a0], witness_sort[a0]) → true
equal_sort[a2](witness_sort[a2], witness_sort[a2]) → true
equal_sort[a9](pos(x0), pos(x1)) → equal_sort[a9](x0, x1)
equal_sort[a9](pos(x0), neg(x1)) → false
equal_sort[a9](pos(x0), witness_sort[a9]) → false
equal_sort[a9](neg(x0), pos(x1)) → false
equal_sort[a9](neg(x0), neg(x1)) → equal_sort[a9](x0, x1)
equal_sort[a9](neg(x0), witness_sort[a9]) → false
equal_sort[a9](witness_sort[a9], pos(x0)) → false
equal_sort[a9](witness_sort[a9], neg(x0)) → false
equal_sort[a9](witness_sort[a9], witness_sort[a9]) → true
equal_sort[a10](01, 01) → true
equal_sort[a10](01, s(x0)) → false
equal_sort[a10](s(x0), 01) → false
equal_sort[a10](s(x0), s(x1)) → equal_sort[a10](x0, x1)
equal_sort[a21](witness_sort[a21], witness_sort[a21]) → true


The proof given by the theorem prover:
The following output was given by the internal theorem prover:
proof of internal
# AProVE Commit ID: 5e8c0853704aa87c1e40fe40458b477b7af98181 cotto 20110121


Partial correctness of the following Program

   [x, x0, x1, x2, x5]
   equal_bool(true, false) -> false
   equal_bool(false, true) -> false
   equal_bool(true, true) -> true
   equal_bool(false, false) -> true
   true and x -> x
   false and x -> false
   true or x -> true
   false or x -> x
   not(false) -> true
   not(true) -> false
   isa_true(true) -> true
   isa_true(false) -> false
   isa_false(true) -> false
   isa_false(false) -> true
   equal_sort[a0](witness_sort[a0], witness_sort[a0]) -> true
   equal_sort[a2](witness_sort[a2], witness_sort[a2]) -> true
   equal_sort[a9](pos(x0), pos(x1)) -> equal_sort[a9](x0, x1)
   equal_sort[a9](pos(x0), neg(x1)) -> false
   equal_sort[a9](pos(x0), witness_sort[a9]) -> false
   equal_sort[a9](neg(x0), pos(x1)) -> false
   equal_sort[a9](neg(x0), neg(x1)) -> equal_sort[a9](x0, x1)
   equal_sort[a9](neg(x0), witness_sort[a9]) -> false
   equal_sort[a9](witness_sort[a9], pos(x0)) -> false
   equal_sort[a9](witness_sort[a9], neg(x0)) -> false
   equal_sort[a9](witness_sort[a9], witness_sort[a9]) -> true
   equal_sort[a10](01, 01) -> true
   equal_sort[a10](01, s(x0)) -> false
   equal_sort[a10](s(x0), 01) -> false
   equal_sort[a10](s(x0), s(x1)) -> equal_sort[a10](x0, x1)
   equal_sort[a21](witness_sort[a21], witness_sort[a21]) -> true
   greater_int'(pos(01), pos(01)) -> true
   greater_int'(neg(01), pos(01)) -> true
   greater_int'(pos(s(x2)), pos(01)) -> true
   greater_int'(neg(s(x5)), pos(01)) -> true
   greater_int'(pos(01), pos(s(x1))) -> false
   greater_int'(pos(01), neg(x0)) -> false
   greater_int'(pos(01), witness_sort[a9]) -> false
   greater_int'(pos(s(x0)), x1) -> false
   greater_int'(neg(01), pos(s(x1))) -> false
   greater_int'(neg(01), neg(x0)) -> false
   greater_int'(neg(01), witness_sort[a9]) -> false
   greater_int'(neg(s(x0)), pos(s(x1))) -> false
   greater_int'(neg(s(x0)), neg(x2)) -> false
   greater_int'(neg(s(x0)), witness_sort[a9]) -> false
   greater_int'(witness_sort[a9], x1) -> false
   greater_int(pos(01), pos(01)) -> false
   greater_int(neg(01), pos(01)) -> false
   greater_int(pos(s(x2)), pos(01)) -> true
   greater_int(neg(s(x5)), pos(01)) -> false
   greater_int(pos(01), pos(s(x1))) -> false
   greater_int(pos(01), neg(x0)) -> false
   greater_int(pos(01), witness_sort[a9]) -> false
   greater_int(pos(s(x0)), x1) -> false
   greater_int(neg(01), pos(s(x1))) -> false
   greater_int(neg(01), neg(x0)) -> false
   greater_int(neg(01), witness_sort[a9]) -> false
   greater_int(neg(s(x0)), pos(s(x1))) -> false
   greater_int(neg(s(x0)), neg(x2)) -> false
   greater_int(neg(s(x0)), witness_sort[a9]) -> false
   greater_int(witness_sort[a9], x1) -> false

using the following formula:
z0:sort[a9].(z0=pos(01)->greater_int'(z0, z0)=true)

could be successfully shown:
(0) Formula
(1) Induction by data structure [EQUIVALENT]
(2) AND
    (3) Formula
        (4) Symbolic evaluation [EQUIVALENT]
        (5) Formula
        (6) Induction by data structure [EQUIVALENT]
        (7) AND
            (8) Formula
                (9) Symbolic evaluation [EQUIVALENT]
                (10) YES
            (11) Formula
                (12) Symbolic evaluation [EQUIVALENT]
                (13) YES
    (14) Formula
        (15) Symbolic evaluation [EQUIVALENT]
        (16) YES
    (17) Formula
        (18) Symbolic evaluation [EQUIVALENT]
        (19) YES


----------------------------------------

(0)
Obligation:
Formula:
z0:sort[a9].(z0=pos(01)->greater_int'(z0, z0)=true)

There are no hypotheses.




----------------------------------------

(1) Induction by data structure (EQUIVALENT)
Induction by data structure sort[a9] generates the following cases:



1. Base Case:
Formula:
(witness_sort[a9]=pos(01)->greater_int'(witness_sort[a9], witness_sort[a9])=true)

There are no hypotheses.





1. Step Case:
Formula:
n:sort[a10].(pos(n)=pos(01)->greater_int'(pos(n), pos(n))=true)

There are no hypotheses.





1. Step Case:
Formula:
n:sort[a10].(neg(n)=pos(01)->greater_int'(neg(n), neg(n))=true)

There are no hypotheses.






----------------------------------------

(2)
Complex Obligation (AND)

----------------------------------------

(3)
Obligation:
Formula:
n:sort[a10].(pos(n)=pos(01)->greater_int'(pos(n), pos(n))=true)

There are no hypotheses.




----------------------------------------

(4) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
n:sort[a10].(n=01->greater_int'(pos(n), pos(n))=true)
----------------------------------------

(5)
Obligation:
Formula:
n:sort[a10].(n=01->greater_int'(pos(n), pos(n))=true)

There are no hypotheses.




----------------------------------------

(6) Induction by data structure (EQUIVALENT)
Induction by data structure sort[a10] generates the following cases:



1. Base Case:
Formula:
(01=01->greater_int'(pos(01), pos(01))=true)

There are no hypotheses.





1. Step Case:
Formula:
n':sort[a0].(s(n')=01->greater_int'(pos(s(n')), pos(s(n')))=true)

There are no hypotheses.






----------------------------------------

(7)
Complex Obligation (AND)

----------------------------------------

(8)
Obligation:
Formula:
(01=01->greater_int'(pos(01), pos(01))=true)

There are no hypotheses.




----------------------------------------

(9) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------

(10)
YES

----------------------------------------

(11)
Obligation:
Formula:
n':sort[a0].(s(n')=01->greater_int'(pos(s(n')), pos(s(n')))=true)

There are no hypotheses.




----------------------------------------

(12) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------

(13)
YES

----------------------------------------

(14)
Obligation:
Formula:
n:sort[a10].(neg(n)=pos(01)->greater_int'(neg(n), neg(n))=true)

There are no hypotheses.




----------------------------------------

(15) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------

(16)
YES

----------------------------------------

(17)
Obligation:
Formula:
(witness_sort[a9]=pos(01)->greater_int'(witness_sort[a9], witness_sort[a9])=true)

There are no hypotheses.




----------------------------------------

(18) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------

(19)
YES

(20) Complex Obligation (AND)

(21) Obligation:

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

COND_983_0_MAIN_LE1(true, x0[3], pos(01), x2[3]) → 983_0_MAIN_LE(x0[3], x2[3], x2[3])

The TRS R consists of the following rules:

greater_int(pos(01), pos(01)) → false
greater_int(neg(01), pos(01)) → false
greater_int(pos(s(x)), pos(01)) → true
greater_int(neg(s(x)), pos(01)) → false

The set Q consists of the following terms:

greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

(22) DependencyGraphProof (EQUIVALENT transformation)

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

(23) TRUE

(24) Obligation:

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

greater_int'(pos(01), pos(01)) → true
greater_int'(neg(01), pos(01)) → true
greater_int'(pos(s(x2)), pos(01)) → true
greater_int'(neg(s(x5)), pos(01)) → true
greater_int'(pos(01), pos(s(x1))) → false
greater_int'(pos(01), neg(x0)) → false
greater_int'(pos(01), witness_sort[a9]) → false
greater_int'(pos(s(x0)), x1) → false
greater_int'(neg(01), pos(s(x1))) → false
greater_int'(neg(01), neg(x0)) → false
greater_int'(neg(01), witness_sort[a9]) → false
greater_int'(neg(s(x0)), pos(s(x1))) → false
greater_int'(neg(s(x0)), neg(x2)) → false
greater_int'(neg(s(x0)), witness_sort[a9]) → false
greater_int'(witness_sort[a9], x1) → false
greater_int(pos(01), pos(01)) → false
greater_int(neg(01), pos(01)) → false
greater_int(pos(s(x2)), pos(01)) → true
greater_int(neg(s(x5)), pos(01)) → false
greater_int(pos(01), pos(s(x1))) → false
greater_int(pos(01), neg(x0)) → false
greater_int(pos(01), witness_sort[a9]) → false
greater_int(pos(s(x0)), x1) → false
greater_int(neg(01), pos(s(x1))) → false
greater_int(neg(01), neg(x0)) → false
greater_int(neg(01), witness_sort[a9]) → false
greater_int(neg(s(x0)), pos(s(x1))) → false
greater_int(neg(s(x0)), neg(x2)) → false
greater_int(neg(s(x0)), witness_sort[a9]) → false
greater_int(witness_sort[a9], x1) → false
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](witness_sort[a0], witness_sort[a0]) → true
equal_sort[a2](witness_sort[a2], witness_sort[a2]) → true
equal_sort[a9](pos(x0), pos(x1)) → equal_sort[a9](x0, x1)
equal_sort[a9](pos(x0), neg(x1)) → false
equal_sort[a9](pos(x0), witness_sort[a9]) → false
equal_sort[a9](neg(x0), pos(x1)) → false
equal_sort[a9](neg(x0), neg(x1)) → equal_sort[a9](x0, x1)
equal_sort[a9](neg(x0), witness_sort[a9]) → false
equal_sort[a9](witness_sort[a9], pos(x0)) → false
equal_sort[a9](witness_sort[a9], neg(x0)) → false
equal_sort[a9](witness_sort[a9], witness_sort[a9]) → true
equal_sort[a10](01, 01) → true
equal_sort[a10](01, s(x0)) → false
equal_sort[a10](s(x0), 01) → false
equal_sort[a10](s(x0), s(x1)) → equal_sort[a10](x0, x1)
equal_sort[a21](witness_sort[a21], witness_sort[a21]) → true

Q is empty.

(25) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Recursive path order with status [RPO].
Quasi-Precedence:
greaterint'2 > [false, and2] > [01, true, s1, witnesssort[a9], isatrue1, witnesssort[a0]]
greaterint2 > [false, and2] > [01, true, s1, witnesssort[a9], isatrue1, witnesssort[a0]]
equalbool2 > [false, and2] > [01, true, s1, witnesssort[a9], isatrue1, witnesssort[a0]]
or2 > [01, true, s1, witnesssort[a9], isatrue1, witnesssort[a0]]
not1 > [false, and2] > [01, true, s1, witnesssort[a9], isatrue1, witnesssort[a0]]
isafalse1 > [false, and2] > [01, true, s1, witnesssort[a9], isatrue1, witnesssort[a0]]
equalsort[a0]2 > [01, true, s1, witnesssort[a9], isatrue1, witnesssort[a0]]
equalsort[a2]2 > [01, true, s1, witnesssort[a9], isatrue1, witnesssort[a0]]
equalsort[a9]2 > [false, and2] > [01, true, s1, witnesssort[a9], isatrue1, witnesssort[a0]]
equalsort[a10]2 > [false, and2] > [01, true, s1, witnesssort[a9], isatrue1, witnesssort[a0]]
equalsort[a21]2 > [01, true, s1, witnesssort[a9], isatrue1, witnesssort[a0]]

Status:
greaterint'2: multiset
pos1: multiset
01: multiset
true: multiset
neg1: multiset
s1: [1]
false: multiset
witnesssort[a9]: multiset
greaterint2: [2,1]
equalbool2: [2,1]
and2: multiset
or2: [2,1]
not1: multiset
isatrue1: [1]
isafalse1: [1]
equalsort[a0]2: [1,2]
witnesssort[a0]: multiset
equalsort[a2]2: multiset
witnesssort[a2]: multiset
equalsort[a9]2: [2,1]
equalsort[a10]2: multiset
equalsort[a21]2: [2,1]
witnesssort[a21]: multiset

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

greater_int'(pos(01), pos(01)) → true
greater_int'(neg(01), pos(01)) → true
greater_int'(pos(s(x2)), pos(01)) → true
greater_int'(neg(s(x5)), pos(01)) → true
greater_int'(pos(01), pos(s(x1))) → false
greater_int'(pos(01), neg(x0)) → false
greater_int'(pos(01), witness_sort[a9]) → false
greater_int'(pos(s(x0)), x1) → false
greater_int'(neg(01), pos(s(x1))) → false
greater_int'(neg(01), neg(x0)) → false
greater_int'(neg(01), witness_sort[a9]) → false
greater_int'(neg(s(x0)), pos(s(x1))) → false
greater_int'(neg(s(x0)), neg(x2)) → false
greater_int'(neg(s(x0)), witness_sort[a9]) → false
greater_int'(witness_sort[a9], x1) → false
greater_int(pos(01), pos(01)) → false
greater_int(neg(01), pos(01)) → false
greater_int(pos(s(x2)), pos(01)) → true
greater_int(neg(s(x5)), pos(01)) → false
greater_int(pos(01), pos(s(x1))) → false
greater_int(pos(01), neg(x0)) → false
greater_int(pos(01), witness_sort[a9]) → false
greater_int(pos(s(x0)), x1) → false
greater_int(neg(01), pos(s(x1))) → false
greater_int(neg(01), neg(x0)) → false
greater_int(neg(01), witness_sort[a9]) → false
greater_int(neg(s(x0)), pos(s(x1))) → false
greater_int(neg(s(x0)), neg(x2)) → false
greater_int(neg(s(x0)), witness_sort[a9]) → false
greater_int(witness_sort[a9], x1) → false
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](witness_sort[a0], witness_sort[a0]) → true
equal_sort[a2](witness_sort[a2], witness_sort[a2]) → true
equal_sort[a9](pos(x0), pos(x1)) → equal_sort[a9](x0, x1)
equal_sort[a9](pos(x0), neg(x1)) → false
equal_sort[a9](pos(x0), witness_sort[a9]) → false
equal_sort[a9](neg(x0), pos(x1)) → false
equal_sort[a9](neg(x0), neg(x1)) → equal_sort[a9](x0, x1)
equal_sort[a9](neg(x0), witness_sort[a9]) → false
equal_sort[a9](witness_sort[a9], pos(x0)) → false
equal_sort[a9](witness_sort[a9], neg(x0)) → false
equal_sort[a9](witness_sort[a9], witness_sort[a9]) → true
equal_sort[a10](01, 01) → true
equal_sort[a10](01, s(x0)) → false
equal_sort[a10](s(x0), 01) → false
equal_sort[a10](s(x0), s(x1)) → equal_sort[a10](x0, x1)
equal_sort[a21](witness_sort[a21], witness_sort[a21]) → true


(26) Obligation:

Q restricted rewrite system:
R is empty.
Q is empty.

(27) RisEmptyProof (EQUIVALENT transformation)

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

(28) YES