Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 530 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 JBCTerminationSCC
↳5 SCCToIDPv1Proof (⇒, 90 ms)
↳6 IDP
↳7 IDPNonInfProof (⇒, 500 ms)
↳8 IDP
↳9 IDependencyGraphProof (⇔, 0 ms)
↳10 IDP
↳11 IDPtoQDPProof (⇒, 0 ms)
↳12 QDP
↳13 UsableRulesProof (⇔, 0 ms)
↳14 QDP
↳15 Instantiation (⇔, 0 ms)
↳16 QDP
↳17 Induction-Processor (⇒, 180 ms)
↳18 AND
    ↳19 QDP
        ↳20 DependencyGraphProof (⇔, 0 ms)
        ↳21 TRUE
    ↳22 QTRS
        ↳23 QTRSRRRProof (⇔, 50 ms)
        ↳24 QTRS
        ↳25 RisEmptyProof (⇔, 0 ms)
        ↳26 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) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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


(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 1 SCCs.

(4) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: DivWithoutMinus.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses: UsedFieldsAnalysis

(5) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 27 rules for P and 0 rules for R.


P rules:
730_0_main_LE(EOS(STATIC_730), i70, i153, i168, i168) → 733_0_main_LE(EOS(STATIC_733), i70, i153, i168, i168)
733_0_main_LE(EOS(STATIC_733), i70, i153, i168, i168) → 737_0_main_Load(EOS(STATIC_737), i70, i153, i168) | >(i168, 0)
737_0_main_Load(EOS(STATIC_737), i70, i153, i168) → 741_0_main_EQ(EOS(STATIC_741), i70, i153, i168, i153)
741_0_main_EQ(EOS(STATIC_741), i70, i172, i168, i172) → 743_0_main_EQ(EOS(STATIC_743), i70, i172, i168, i172)
741_0_main_EQ(EOS(STATIC_741), i70, matching1, i168, matching2) → 744_0_main_EQ(EOS(STATIC_744), i70, 0, i168, 0) | &&(=(matching1, 0), =(matching2, 0))
743_0_main_EQ(EOS(STATIC_743), i70, i172, i168, i172) → 746_0_main_Load(EOS(STATIC_746), i70, i172, i168) | !(=(i172, 0))
746_0_main_Load(EOS(STATIC_746), i70, i172, i168) → 750_0_main_LE(EOS(STATIC_750), i70, i172, i168, i172)
750_0_main_LE(EOS(STATIC_750), i70, i178, i168, i178) → 755_0_main_LE(EOS(STATIC_755), i70, i178, i168, i178)
755_0_main_LE(EOS(STATIC_755), i70, i178, i168, i178) → 763_0_main_Load(EOS(STATIC_763), i70, i178, i168) | >(i178, 0)
763_0_main_Load(EOS(STATIC_763), i70, i178, i168) → 769_0_main_LE(EOS(STATIC_769), i70, i178, i168, i70)
769_0_main_LE(EOS(STATIC_769), i181, i178, i168, i181) → 774_0_main_LE(EOS(STATIC_774), i181, i178, i168, i181)
774_0_main_LE(EOS(STATIC_774), i181, i178, i168, i181) → 781_0_main_Load(EOS(STATIC_781), i181, i178, i168) | >(i181, 0)
781_0_main_Load(EOS(STATIC_781), i181, i178, i168) → 798_0_main_NE(EOS(STATIC_798), i181, i178, i168, i178)
798_0_main_NE(EOS(STATIC_798), i181, i178, i168, i178) → 1065_0_main_Inc(EOS(STATIC_1065), i181, i178, i168) | >(i178, 0)
1065_0_main_Inc(EOS(STATIC_1065), i181, i178, i168) → 1067_0_main_Inc(EOS(STATIC_1067), +(i181, -1), i178, i168) | >(i181, 0)
1067_0_main_Inc(EOS(STATIC_1067), i375, i178, i168) → 1068_0_main_JMP(EOS(STATIC_1068), i375, +(i178, -1), i168) | >(i178, 0)
1068_0_main_JMP(EOS(STATIC_1068), i375, i376, i168) → 1071_0_main_Load(EOS(STATIC_1071), i375, i376, i168)
1071_0_main_Load(EOS(STATIC_1071), i375, i376, i168) → 726_0_main_Load(EOS(STATIC_726), i375, i376, i168)
726_0_main_Load(EOS(STATIC_726), i70, i153, i154) → 730_0_main_LE(EOS(STATIC_730), i70, i153, i154, i154)
744_0_main_EQ(EOS(STATIC_744), i70, matching1, i168, matching2) → 748_0_main_Load(EOS(STATIC_748), i70, 0, i168) | &&(=(matching1, 0), =(matching2, 0))
748_0_main_Load(EOS(STATIC_748), i70, matching1, i168) → 752_0_main_NE(EOS(STATIC_752), i70, 0, i168, 0) | =(matching1, 0)
752_0_main_NE(EOS(STATIC_752), i70, matching1, i168, matching2) → 757_0_main_Inc(EOS(STATIC_757), i70, i168) | &&(=(matching1, 0), =(matching2, 0))
757_0_main_Inc(EOS(STATIC_757), i70, i168) → 765_0_main_Load(EOS(STATIC_765), i70, i168)
765_0_main_Load(EOS(STATIC_765), i70, i168) → 770_0_main_Store(EOS(STATIC_770), i70, i168, i168)
770_0_main_Store(EOS(STATIC_770), i70, i168, i168) → 776_0_main_JMP(EOS(STATIC_776), i70, i168, i168)
776_0_main_JMP(EOS(STATIC_776), i70, i168, i168) → 793_0_main_Load(EOS(STATIC_793), i70, i168, i168)
793_0_main_Load(EOS(STATIC_793), i70, i168, i168) → 726_0_main_Load(EOS(STATIC_726), i70, i168, i168)
R rules:

Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.


P rules:
730_0_main_LE(EOS(STATIC_730), x0, x1, x2, x2) → 730_0_main_LE(EOS(STATIC_730), +(x0, -1), +(x1, -1), x2, x2) | &&(&&(>(x2, 0), >(x1, 0)), >(x0, 0))
730_0_main_LE(EOS(STATIC_730), x0, 0, x2, x2) → 730_0_main_LE(EOS(STATIC_730), x0, x2, x2, x2) | >(x2, 0)
R rules:

Filtered ground terms:



730_0_main_LE(x1, x2, x3, x4, x5) → 730_0_main_LE(x2, x3, x4, x5)
EOS(x1) → EOS
Cond_730_0_main_LE1(x1, x2, x3, x4, x5, x6) → Cond_730_0_main_LE1(x1, x3, x5, x6)
Cond_730_0_main_LE(x1, x2, x3, x4, x5, x6) → Cond_730_0_main_LE(x1, x3, x4, x5, x6)

Filtered duplicate args:



730_0_main_LE(x1, x2, x3, x4) → 730_0_main_LE(x1, x2, x4)
Cond_730_0_main_LE(x1, x2, x3, x4, x5) → Cond_730_0_main_LE(x1, x2, x3, x5)
Cond_730_0_main_LE1(x1, x2, x3, x4) → Cond_730_0_main_LE1(x1, x2, x4)

Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.


P rules:
730_0_main_LE(x0, x1, x2) → 730_0_main_LE(+(x0, -1), +(x1, -1), x2) | &&(&&(>(x2, 0), >(x1, 0)), >(x0, 0))
730_0_main_LE(x0, 0, x2) → 730_0_main_LE(x0, x2, x2) | >(x2, 0)
R rules:

Finished conversion. Obtained 4 rules for P and 0 rules for R. System has predefined symbols.


P rules:
730_0_MAIN_LE(x0, x1, x2) → COND_730_0_MAIN_LE(&&(&&(>(x2, 0), >(x1, 0)), >(x0, 0)), x0, x1, x2)
COND_730_0_MAIN_LE(TRUE, x0, x1, x2) → 730_0_MAIN_LE(+(x0, -1), +(x1, -1), x2)
730_0_MAIN_LE(x0, 0, x2) → COND_730_0_MAIN_LE1(>(x2, 0), x0, 0, x2)
COND_730_0_MAIN_LE1(TRUE, x0, 0, x2) → 730_0_MAIN_LE(x0, x2, x2)
R rules:

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

Boolean, Integer


R is empty.

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

(0) -> (1), if (x2[0] > 0 && x1[0] > 0 && x0[0] > 0 ∧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 ∧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 is empty.

(7) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpDefaultShapeHeuristic@59b3ef14 Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 1 Max Right Steps: 1

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 730_0_MAIN_LE(x0, x1, x2) → COND_730_0_MAIN_LE(&&(&&(>(x2, 0), >(x1, 0)), >(x0, 0)), x0, x1, x2) the following chains were created:
  • We consider the chain 730_0_MAIN_LE(x0[0], x1[0], x2[0]) → COND_730_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0]), COND_730_0_MAIN_LE(TRUE, x0[1], x1[1], x2[1]) → 730_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] ⇒ 730_0_MAIN_LE(x0[0], x1[0], x2[0])≥NonInfC∧730_0_MAIN_LE(x0[0], x1[0], x2[0])≥COND_730_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])∧(UIncreasing(COND_730_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 ⇒ 730_0_MAIN_LE(x0[0], x1[0], x2[0])≥NonInfC∧730_0_MAIN_LE(x0[0], x1[0], x2[0])≥COND_730_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])∧(UIncreasing(COND_730_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_730_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])), ≥)∧[(-1)bni_19 + (-1)Bound*bni_19] + [bni_19]x0[0] ≥ 0∧[1 + (-1)bso_20] ≥ 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_730_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])), ≥)∧[(-1)bni_19 + (-1)Bound*bni_19] + [bni_19]x0[0] ≥ 0∧[1 + (-1)bso_20] ≥ 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_730_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])), ≥)∧[(-1)bni_19 + (-1)Bound*bni_19] + [bni_19]x0[0] ≥ 0∧[1 + (-1)bso_20] ≥ 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_730_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])), ≥)∧[(-1)Bound*bni_19] + [bni_19]x0[0] ≥ 0∧[1 + (-1)bso_20] ≥ 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_730_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])), ≥)∧[(-1)Bound*bni_19] + [bni_19]x0[0] ≥ 0∧[1 + (-1)bso_20] ≥ 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_730_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])), ≥)∧[(-1)Bound*bni_19] + [bni_19]x0[0] ≥ 0∧[1 + (-1)bso_20] ≥ 0)







For Pair COND_730_0_MAIN_LE(TRUE, x0, x1, x2) → 730_0_MAIN_LE(+(x0, -1), +(x1, -1), x2) the following chains were created:
  • We consider the chain 730_0_MAIN_LE(x0[0], x1[0], x2[0]) → COND_730_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0]), COND_730_0_MAIN_LE(TRUE, x0[1], x1[1], x2[1]) → 730_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1]), 730_0_MAIN_LE(x0[0], x1[0], x2[0]) → COND_730_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_730_0_MAIN_LE(TRUE, x0[1], x1[1], x2[1])≥NonInfC∧COND_730_0_MAIN_LE(TRUE, x0[1], x1[1], x2[1])≥730_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])∧(UIncreasing(730_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_730_0_MAIN_LE(TRUE, x0[0], x1[0], x2[0])≥NonInfC∧COND_730_0_MAIN_LE(TRUE, x0[0], x1[0], x2[0])≥730_0_MAIN_LE(+(x0[0], -1), +(x1[0], -1), x2[0])∧(UIncreasing(730_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(730_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[(-2)bni_21 + (-1)Bound*bni_21] + [bni_21]x0[0] ≥ 0∧[(-1)bso_22] ≥ 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(730_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[(-2)bni_21 + (-1)Bound*bni_21] + [bni_21]x0[0] ≥ 0∧[(-1)bso_22] ≥ 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(730_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[(-2)bni_21 + (-1)Bound*bni_21] + [bni_21]x0[0] ≥ 0∧[(-1)bso_22] ≥ 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(730_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[(-1)bni_21 + (-1)Bound*bni_21] + [bni_21]x0[0] ≥ 0∧[(-1)bso_22] ≥ 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(730_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[(-1)bni_21 + (-1)Bound*bni_21] + [bni_21]x0[0] ≥ 0∧[(-1)bso_22] ≥ 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(730_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[(-1)bni_21 + (-1)Bound*bni_21] + [bni_21]x0[0] ≥ 0∧[(-1)bso_22] ≥ 0)



  • We consider the chain 730_0_MAIN_LE(x0[0], x1[0], x2[0]) → COND_730_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0]), COND_730_0_MAIN_LE(TRUE, x0[1], x1[1], x2[1]) → 730_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1]), 730_0_MAIN_LE(x0[2], 0, x2[2]) → COND_730_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_730_0_MAIN_LE(TRUE, x0[1], x1[1], x2[1])≥NonInfC∧COND_730_0_MAIN_LE(TRUE, x0[1], x1[1], x2[1])≥730_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])∧(UIncreasing(730_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_730_0_MAIN_LE(TRUE, x0[0], x1[0], x2[0])≥NonInfC∧COND_730_0_MAIN_LE(TRUE, x0[0], x1[0], x2[0])≥730_0_MAIN_LE(+(x0[0], -1), +(x1[0], -1), x2[0])∧(UIncreasing(730_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(730_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[(-2)bni_21 + (-1)Bound*bni_21] + [bni_21]x0[0] ≥ 0∧[(-1)bso_22] ≥ 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(730_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[(-2)bni_21 + (-1)Bound*bni_21] + [bni_21]x0[0] ≥ 0∧[(-1)bso_22] ≥ 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(730_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[(-2)bni_21 + (-1)Bound*bni_21] + [bni_21]x0[0] ≥ 0∧[(-1)bso_22] ≥ 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(730_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[(-2)bni_21 + (-1)Bound*bni_21] + [bni_21]x0[0] ≥ 0∧[(-1)bso_22] ≥ 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(730_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[(-1)bni_21 + (-1)Bound*bni_21] + [bni_21]x0[0] ≥ 0∧[(-1)bso_22] ≥ 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(730_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[(-1)bni_21 + (-1)Bound*bni_21] + [bni_21]x0[0] ≥ 0∧[(-1)bso_22] ≥ 0)







For Pair 730_0_MAIN_LE(x0, 0, x2) → COND_730_0_MAIN_LE1(>(x2, 0), x0, 0, x2) the following chains were created:
  • We consider the chain 730_0_MAIN_LE(x0[2], 0, x2[2]) → COND_730_0_MAIN_LE1(>(x2[2], 0), x0[2], 0, x2[2]), COND_730_0_MAIN_LE1(TRUE, x0[3], 0, x2[3]) → 730_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] ⇒ 730_0_MAIN_LE(x0[2], 0, x2[2])≥NonInfC∧730_0_MAIN_LE(x0[2], 0, x2[2])≥COND_730_0_MAIN_LE1(>(x2[2], 0), x0[2], 0, x2[2])∧(UIncreasing(COND_730_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 ⇒ 730_0_MAIN_LE(x0[2], 0, x2[2])≥NonInfC∧730_0_MAIN_LE(x0[2], 0, x2[2])≥COND_730_0_MAIN_LE1(>(x2[2], 0), x0[2], 0, x2[2])∧(UIncreasing(COND_730_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_730_0_MAIN_LE1(>(x2[2], 0), x0[2], 0, x2[2])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [bni_23]x0[2] ≥ 0∧[(-1)bso_24] ≥ 0)



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

    (28)    (x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_730_0_MAIN_LE1(>(x2[2], 0), x0[2], 0, x2[2])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [bni_23]x0[2] ≥ 0∧[(-1)bso_24] ≥ 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_730_0_MAIN_LE1(>(x2[2], 0), x0[2], 0, x2[2])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [bni_23]x0[2] ≥ 0∧[(-1)bso_24] ≥ 0)



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

    (30)    (x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_730_0_MAIN_LE1(>(x2[2], 0), x0[2], 0, x2[2])), ≥)∧[bni_23] = 0∧[(-1)bni_23 + (-1)Bound*bni_23] ≥ 0∧0 = 0∧[(-1)bso_24] ≥ 0)



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

    (31)    (x2[2] ≥ 0 ⇒ (UIncreasing(COND_730_0_MAIN_LE1(>(x2[2], 0), x0[2], 0, x2[2])), ≥)∧[bni_23] = 0∧[(-1)bni_23 + (-1)Bound*bni_23] ≥ 0∧0 = 0∧[(-1)bso_24] ≥ 0)







For Pair COND_730_0_MAIN_LE1(TRUE, x0, 0, x2) → 730_0_MAIN_LE(x0, x2, x2) the following chains were created:
  • We consider the chain COND_730_0_MAIN_LE1(TRUE, x0[3], 0, x2[3]) → 730_0_MAIN_LE(x0[3], x2[3], x2[3]), 730_0_MAIN_LE(x0[0], x1[0], x2[0]) → COND_730_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_730_0_MAIN_LE1(TRUE, x0[3], 0, x2[3])≥NonInfC∧COND_730_0_MAIN_LE1(TRUE, x0[3], 0, x2[3])≥730_0_MAIN_LE(x0[3], x2[3], x2[3])∧(UIncreasing(730_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_730_0_MAIN_LE1(TRUE, x0[3], 0, x2[3])≥NonInfC∧COND_730_0_MAIN_LE1(TRUE, x0[3], 0, x2[3])≥730_0_MAIN_LE(x0[3], x2[3], x2[3])∧(UIncreasing(730_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(730_0_MAIN_LE(x0[3], x2[3], x2[3])), ≥)∧[bni_25] = 0∧[(-1)bso_26] ≥ 0)



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

    (35)    ((UIncreasing(730_0_MAIN_LE(x0[3], x2[3], x2[3])), ≥)∧[bni_25] = 0∧[(-1)bso_26] ≥ 0)



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

    (36)    ((UIncreasing(730_0_MAIN_LE(x0[3], x2[3], x2[3])), ≥)∧[bni_25] = 0∧[(-1)bso_26] ≥ 0)



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

    (37)    ((UIncreasing(730_0_MAIN_LE(x0[3], x2[3], x2[3])), ≥)∧[bni_25] = 0∧0 = 0∧0 = 0∧[(-1)bso_26] ≥ 0)



  • We consider the chain COND_730_0_MAIN_LE1(TRUE, x0[3], 0, x2[3]) → 730_0_MAIN_LE(x0[3], x2[3], x2[3]), 730_0_MAIN_LE(x0[2], 0, x2[2]) → COND_730_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_730_0_MAIN_LE1(TRUE, x0[3], 0, x2[3])≥NonInfC∧COND_730_0_MAIN_LE1(TRUE, x0[3], 0, x2[3])≥730_0_MAIN_LE(x0[3], x2[3], x2[3])∧(UIncreasing(730_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_730_0_MAIN_LE1(TRUE, x0[3], 0, 0)≥NonInfC∧COND_730_0_MAIN_LE1(TRUE, x0[3], 0, 0)≥730_0_MAIN_LE(x0[3], 0, 0)∧(UIncreasing(730_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(730_0_MAIN_LE(x0[3], x2[3], x2[3])), ≥)∧[bni_25] = 0∧[(-1)bso_26] ≥ 0)



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

    (41)    ((UIncreasing(730_0_MAIN_LE(x0[3], x2[3], x2[3])), ≥)∧[bni_25] = 0∧[(-1)bso_26] ≥ 0)



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

    (42)    ((UIncreasing(730_0_MAIN_LE(x0[3], x2[3], x2[3])), ≥)∧[bni_25] = 0∧[(-1)bso_26] ≥ 0)



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

    (43)    ((UIncreasing(730_0_MAIN_LE(x0[3], x2[3], x2[3])), ≥)∧[bni_25] = 0∧0 = 0∧[(-1)bso_26] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • 730_0_MAIN_LE(x0, x1, x2) → COND_730_0_MAIN_LE(&&(&&(>(x2, 0), >(x1, 0)), >(x0, 0)), x0, x1, x2)
    • (x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_730_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])), ≥)∧[(-1)Bound*bni_19] + [bni_19]x0[0] ≥ 0∧[1 + (-1)bso_20] ≥ 0)

  • COND_730_0_MAIN_LE(TRUE, x0, x1, x2) → 730_0_MAIN_LE(+(x0, -1), +(x1, -1), x2)
    • (x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(730_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[(-1)bni_21 + (-1)Bound*bni_21] + [bni_21]x0[0] ≥ 0∧[(-1)bso_22] ≥ 0)
    • (x1[0] ≥ 0∧x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(730_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])), ≥)∧[(-1)bni_21 + (-1)Bound*bni_21] + [bni_21]x0[0] ≥ 0∧[(-1)bso_22] ≥ 0)

  • 730_0_MAIN_LE(x0, 0, x2) → COND_730_0_MAIN_LE1(>(x2, 0), x0, 0, x2)
    • (x2[2] ≥ 0 ⇒ (UIncreasing(COND_730_0_MAIN_LE1(>(x2[2], 0), x0[2], 0, x2[2])), ≥)∧[bni_23] = 0∧[(-1)bni_23 + (-1)Bound*bni_23] ≥ 0∧0 = 0∧[(-1)bso_24] ≥ 0)

  • COND_730_0_MAIN_LE1(TRUE, x0, 0, x2) → 730_0_MAIN_LE(x0, x2, x2)
    • ((UIncreasing(730_0_MAIN_LE(x0[3], x2[3], x2[3])), ≥)∧[bni_25] = 0∧0 = 0∧0 = 0∧[(-1)bso_26] ≥ 0)
    • ((UIncreasing(730_0_MAIN_LE(x0[3], x2[3], x2[3])), ≥)∧[bni_25] = 0∧0 = 0∧[(-1)bso_26] ≥ 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) = [1]   
POL(FALSE) = [1]   
POL(730_0_MAIN_LE(x1, x2, x3)) = [-1] + x1   
POL(COND_730_0_MAIN_LE(x1, x2, x3, x4)) = [-1] + x2 + [-1]x1   
POL(&&(x1, x2)) = [1]   
POL(>(x1, x2)) = [-1]   
POL(0) = 0   
POL(+(x1, x2)) = x1 + x2   
POL(-1) = [-1]   
POL(COND_730_0_MAIN_LE1(x1, x2, x3, x4)) = [-1] + [-1]x3 + x2   

The following pairs are in P>:

730_0_MAIN_LE(x0[0], x1[0], x2[0]) → COND_730_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])

The following pairs are in Pbound:

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

The following pairs are in P≥:

COND_730_0_MAIN_LE(TRUE, x0[1], x1[1], x2[1]) → 730_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])
730_0_MAIN_LE(x0[2], 0, x2[2]) → COND_730_0_MAIN_LE1(>(x2[2], 0), x0[2], 0, x2[2])
COND_730_0_MAIN_LE1(TRUE, x0[3], 0, x2[3]) → 730_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

(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


R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_730_0_MAIN_LE(TRUE, x0[1], x1[1], x2[1]) → 730_0_MAIN_LE(x0[1] + -1, x1[1] + -1, x2[1])
(2): 730_0_MAIN_LE(x0[2], 0, x2[2]) → COND_730_0_MAIN_LE1(x2[2] > 0, x0[2], 0, x2[2])
(3): COND_730_0_MAIN_LE1(TRUE, x0[3], 0, x2[3]) → 730_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 ∧x0[2] →* x0[3]∧x2[2] →* x2[3])



The set Q is empty.

(9) IDependencyGraphProof (EQUIVALENT transformation)

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

(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_730_0_MAIN_LE1(TRUE, x0[3], 0, x2[3]) → 730_0_MAIN_LE(x0[3], x2[3], x2[3])
(2): 730_0_MAIN_LE(x0[2], 0, x2[2]) → COND_730_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 ∧x0[2] →* x0[3]∧x2[2] →* x2[3])



The set Q is empty.

(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_730_0_MAIN_LE1(true, x0[3], pos(01), x2[3]) → 730_0_MAIN_LE(x0[3], x2[3], x2[3])
730_0_MAIN_LE(x0[2], pos(01), x2[2]) → COND_730_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:

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_730_0_MAIN_LE1(true, x0[3], pos(01), x2[3]) → 730_0_MAIN_LE(x0[3], x2[3], x2[3])
730_0_MAIN_LE(x0[2], pos(01), x2[2]) → COND_730_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.

(15) Instantiation (EQUIVALENT transformation)

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

730_0_MAIN_LE(z0, pos(01), pos(01)) → COND_730_0_MAIN_LE1(greater_int(pos(01), pos(01)), z0, pos(01), pos(01))

(16) Obligation:

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

COND_730_0_MAIN_LE1(true, x0[3], pos(01), x2[3]) → 730_0_MAIN_LE(x0[3], x2[3], x2[3])
730_0_MAIN_LE(z0, pos(01), pos(01)) → COND_730_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.

(17) Induction-Processor (SOUND transformation)


This DP could be deleted by the Induction-Processor:
730_0_MAIN_LE(z0, pos(01), pos(01)) → COND_730_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(730_0_MAIN_LE(x1, x2, x3)) = 1 + x1   
POL(COND_730_0_MAIN_LE1(x1, x2, x3, x4)) = x1 + x2 + x4   
POL(false_renamed) = 0   
POL(greater_int(x1, x2)) = 1 + x1   
POL(neg(x1)) = 1   
POL(pos(x1)) = x1   
POL(s(x1)) = 1   
POL(true_renamed) = 1   
POL(witness_sort[a9]) = 0   

At least one of these decreasing rules is always used after the deleted DP:
greater_int(pos(01), pos(01)) → false_renamed
greater_int(neg(01), pos(01)) → false_renamed
greater_int(pos(s(x)), pos(01)) → true_renamed
greater_int(neg(s(x')), pos(01)) → false_renamed


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


The transformed set:
greater_int'(pos(01), pos(01)) → true
greater_int'(neg(01), pos(01)) → true
greater_int'(pos(s(x)), pos(01)) → true
greater_int'(neg(s(x')), pos(01)) → true
greater_int'(pos(01), pos(s(v22))) → false
greater_int'(pos(01), neg(v23)) → false
greater_int'(pos(01), witness_sort[a9]) → false
greater_int'(pos(s(v24)), pos(s(v26))) → false
greater_int'(pos(s(v24)), neg(v27)) → false
greater_int'(pos(s(v24)), witness_sort[a9]) → false
greater_int'(neg(01), pos(s(v30))) → false
greater_int'(neg(01), neg(v31)) → false
greater_int'(neg(01), witness_sort[a9]) → false
greater_int'(neg(s(v32)), pos(s(v34))) → false
greater_int'(neg(s(v32)), neg(v35)) → false
greater_int'(neg(s(v32)), witness_sort[a9]) → false
greater_int'(witness_sort[a9], v19) → false
greater_int(pos(01), pos(01)) → false_renamed
greater_int(neg(01), pos(01)) → false_renamed
greater_int(pos(s(x)), pos(01)) → true_renamed
greater_int(neg(s(x')), pos(01)) → false_renamed
greater_int(pos(01), pos(s(v22))) → false_renamed
greater_int(pos(01), neg(v23)) → false_renamed
greater_int(pos(01), witness_sort[a9]) → false_renamed
greater_int(pos(s(v24)), pos(s(v26))) → false_renamed
greater_int(pos(s(v24)), neg(v27)) → false_renamed
greater_int(pos(s(v24)), witness_sort[a9]) → false_renamed
greater_int(neg(01), pos(s(v30))) → false_renamed
greater_int(neg(01), neg(v31)) → false_renamed
greater_int(neg(01), witness_sort[a9]) → false_renamed
greater_int(neg(s(v32)), pos(s(v34))) → false_renamed
greater_int(neg(s(v32)), neg(v35)) → false_renamed
greater_int(neg(s(v32)), witness_sort[a9]) → false_renamed
greater_int(witness_sort[a9], v19) → false_renamed
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(v36), pos(v37)) → equal_sort[a10](v36, v37)
equal_sort[a9](pos(v36), neg(v38)) → false
equal_sort[a9](pos(v36), witness_sort[a9]) → false
equal_sort[a9](neg(v39), pos(v40)) → false
equal_sort[a9](neg(v39), neg(v41)) → equal_sort[a10](v39, v41)
equal_sort[a9](neg(v39), witness_sort[a9]) → false
equal_sort[a9](witness_sort[a9], pos(v42)) → false
equal_sort[a9](witness_sort[a9], neg(v43)) → false
equal_sort[a9](witness_sort[a9], witness_sort[a9]) → true
equal_sort[a7](false_renamed, false_renamed) → true
equal_sort[a7](false_renamed, true_renamed) → false
equal_sort[a7](true_renamed, false_renamed) → false
equal_sort[a7](true_renamed, true_renamed) → true
equal_sort[a10](01, 01) → true
equal_sort[a10](01, s(v44)) → false
equal_sort[a10](s(v45), 01) → false
equal_sort[a10](s(v45), s(v46)) → equal_sort[a0](v45, v46)
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: 8debe15a911aa78e0d63fcb2a64f61d1a50cd454 marc 20110727


Partial correctness of the following Program

   [x, v36, v37, v38, v39, v40, v41, v42, v43, v44, v45, v46, x', v22, v23, v24, v26, v27, v30, v31, v32, v34, v35, v19]
   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(v36), pos(v37)) -> equal_sort[a10](v36, v37)
   equal_sort[a9](pos(v36), neg(v38)) -> false
   equal_sort[a9](pos(v36), witness_sort[a9]) -> false
   equal_sort[a9](neg(v39), pos(v40)) -> false
   equal_sort[a9](neg(v39), neg(v41)) -> equal_sort[a10](v39, v41)
   equal_sort[a9](neg(v39), witness_sort[a9]) -> false
   equal_sort[a9](witness_sort[a9], pos(v42)) -> false
   equal_sort[a9](witness_sort[a9], neg(v43)) -> false
   equal_sort[a9](witness_sort[a9], witness_sort[a9]) -> true
   equal_sort[a7](false_renamed, false_renamed) -> true
   equal_sort[a7](false_renamed, true_renamed) -> false
   equal_sort[a7](true_renamed, false_renamed) -> false
   equal_sort[a7](true_renamed, true_renamed) -> true
   equal_sort[a10](01, 01) -> true
   equal_sort[a10](01, s(v44)) -> false
   equal_sort[a10](s(v45), 01) -> false
   equal_sort[a10](s(v45), s(v46)) -> equal_sort[a0](v45, v46)
   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(x)), pos(01)) -> true
   greater_int'(neg(s(x')), pos(01)) -> true
   greater_int'(pos(01), pos(s(v22))) -> false
   greater_int'(pos(01), neg(v23)) -> false
   greater_int'(pos(01), witness_sort[a9]) -> false
   greater_int'(pos(s(v24)), pos(s(v26))) -> false
   greater_int'(pos(s(v24)), neg(v27)) -> false
   greater_int'(pos(s(v24)), witness_sort[a9]) -> false
   greater_int'(neg(01), pos(s(v30))) -> false
   greater_int'(neg(01), neg(v31)) -> false
   greater_int'(neg(01), witness_sort[a9]) -> false
   greater_int'(neg(s(v32)), pos(s(v34))) -> false
   greater_int'(neg(s(v32)), neg(v35)) -> false
   greater_int'(neg(s(v32)), witness_sort[a9]) -> false
   greater_int'(witness_sort[a9], v19) -> false
   greater_int(pos(01), pos(01)) -> false_renamed
   greater_int(neg(01), pos(01)) -> false_renamed
   greater_int(pos(s(x)), pos(01)) -> true_renamed
   greater_int(neg(s(x')), pos(01)) -> false_renamed
   greater_int(pos(01), pos(s(v22))) -> false_renamed
   greater_int(pos(01), neg(v23)) -> false_renamed
   greater_int(pos(01), witness_sort[a9]) -> false_renamed
   greater_int(pos(s(v24)), pos(s(v26))) -> false_renamed
   greater_int(pos(s(v24)), neg(v27)) -> false_renamed
   greater_int(pos(s(v24)), witness_sort[a9]) -> false_renamed
   greater_int(neg(01), pos(s(v30))) -> false_renamed
   greater_int(neg(01), neg(v31)) -> false_renamed
   greater_int(neg(01), witness_sort[a9]) -> false_renamed
   greater_int(neg(s(v32)), pos(s(v34))) -> false_renamed
   greater_int(neg(s(v32)), neg(v35)) -> false_renamed
   greater_int(neg(s(v32)), witness_sort[a9]) -> false_renamed
   greater_int(witness_sort[a9], v19) -> false_renamed

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

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


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

(0)
Obligation:
Formula:
z1:sort[a9].(z1=pos(01)->greater_int'(z1, z1)=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

(18) Complex Obligation (AND)

(19) Obligation:

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

COND_730_0_MAIN_LE1(true, x0[3], pos(01), x2[3]) → 730_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.

(20) DependencyGraphProof (EQUIVALENT transformation)

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

(21) TRUE

(22) 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(x)), pos(01)) → true
greater_int'(neg(s(x')), pos(01)) → true
greater_int'(pos(01), pos(s(v22))) → false
greater_int'(pos(01), neg(v23)) → false
greater_int'(pos(01), witness_sort[a9]) → false
greater_int'(pos(s(v24)), pos(s(v26))) → false
greater_int'(pos(s(v24)), neg(v27)) → false
greater_int'(pos(s(v24)), witness_sort[a9]) → false
greater_int'(neg(01), pos(s(v30))) → false
greater_int'(neg(01), neg(v31)) → false
greater_int'(neg(01), witness_sort[a9]) → false
greater_int'(neg(s(v32)), pos(s(v34))) → false
greater_int'(neg(s(v32)), neg(v35)) → false
greater_int'(neg(s(v32)), witness_sort[a9]) → false
greater_int'(witness_sort[a9], v19) → false
greater_int(pos(01), pos(01)) → false_renamed
greater_int(neg(01), pos(01)) → false_renamed
greater_int(pos(s(x)), pos(01)) → true_renamed
greater_int(neg(s(x')), pos(01)) → false_renamed
greater_int(pos(01), pos(s(v22))) → false_renamed
greater_int(pos(01), neg(v23)) → false_renamed
greater_int(pos(01), witness_sort[a9]) → false_renamed
greater_int(pos(s(v24)), pos(s(v26))) → false_renamed
greater_int(pos(s(v24)), neg(v27)) → false_renamed
greater_int(pos(s(v24)), witness_sort[a9]) → false_renamed
greater_int(neg(01), pos(s(v30))) → false_renamed
greater_int(neg(01), neg(v31)) → false_renamed
greater_int(neg(01), witness_sort[a9]) → false_renamed
greater_int(neg(s(v32)), pos(s(v34))) → false_renamed
greater_int(neg(s(v32)), neg(v35)) → false_renamed
greater_int(neg(s(v32)), witness_sort[a9]) → false_renamed
greater_int(witness_sort[a9], v19) → false_renamed
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(v36), pos(v37)) → equal_sort[a10](v36, v37)
equal_sort[a9](pos(v36), neg(v38)) → false
equal_sort[a9](pos(v36), witness_sort[a9]) → false
equal_sort[a9](neg(v39), pos(v40)) → false
equal_sort[a9](neg(v39), neg(v41)) → equal_sort[a10](v39, v41)
equal_sort[a9](neg(v39), witness_sort[a9]) → false
equal_sort[a9](witness_sort[a9], pos(v42)) → false
equal_sort[a9](witness_sort[a9], neg(v43)) → false
equal_sort[a9](witness_sort[a9], witness_sort[a9]) → true
equal_sort[a7](false_renamed, false_renamed) → true
equal_sort[a7](false_renamed, true_renamed) → false
equal_sort[a7](true_renamed, false_renamed) → false
equal_sort[a7](true_renamed, true_renamed) → true
equal_sort[a10](01, 01) → true
equal_sort[a10](01, s(v44)) → false
equal_sort[a10](s(v45), 01) → false
equal_sort[a10](s(v45), s(v46)) → equal_sort[a0](v45, v46)
equal_sort[a21](witness_sort[a21], witness_sort[a21]) → true

Q is empty.

(23) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Knuth-Bendix order [KBO] with precedence:
s1 > pos1 > greaterint2 > or2 > equalsort[a0]2 > isatrue1 > truerenamed > greaterint'2 > neg1 > not1 > witnesssort[a9] > and2 > witnesssort[a0] > 01 > isafalse1 > witnesssort[a21] > equalsort[a21]2 > equalsort[a7]2 > equalsort[a10]2 > equalsort[a9]2 > false > witnesssort[a2] > equalsort[a2]2 > true > falserenamed > equalbool2

and weight map:

01=1
true=5
false=6
witness_sort[a9]=4
false_renamed=4
true_renamed=3
witness_sort[a0]=1
witness_sort[a2]=1
witness_sort[a21]=1
pos_1=1
neg_1=1
s_1=0
not_1=1
isa_true_1=1
isa_false_1=2
greater_int'_2=2
greater_int_2=0
equal_bool_2=0
and_2=0
or_2=0
equal_sort[a0]_2=3
equal_sort[a2]_2=3
equal_sort[a9]_2=4
equal_sort[a10]_2=5
equal_sort[a7]_2=0
equal_sort[a21]_2=3

The variable weight is 1With 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(x)), pos(01)) → true
greater_int'(neg(s(x')), pos(01)) → true
greater_int'(pos(01), pos(s(v22))) → false
greater_int'(pos(01), neg(v23)) → false
greater_int'(pos(01), witness_sort[a9]) → false
greater_int'(pos(s(v24)), pos(s(v26))) → false
greater_int'(pos(s(v24)), neg(v27)) → false
greater_int'(pos(s(v24)), witness_sort[a9]) → false
greater_int'(neg(01), pos(s(v30))) → false
greater_int'(neg(01), neg(v31)) → false
greater_int'(neg(01), witness_sort[a9]) → false
greater_int'(neg(s(v32)), pos(s(v34))) → false
greater_int'(neg(s(v32)), neg(v35)) → false
greater_int'(neg(s(v32)), witness_sort[a9]) → false
greater_int'(witness_sort[a9], v19) → false
greater_int(pos(01), pos(01)) → false_renamed
greater_int(neg(01), pos(01)) → false_renamed
greater_int(pos(s(x)), pos(01)) → true_renamed
greater_int(neg(s(x')), pos(01)) → false_renamed
greater_int(pos(01), pos(s(v22))) → false_renamed
greater_int(pos(01), neg(v23)) → false_renamed
greater_int(pos(01), witness_sort[a9]) → false_renamed
greater_int(pos(s(v24)), pos(s(v26))) → false_renamed
greater_int(pos(s(v24)), neg(v27)) → false_renamed
greater_int(pos(s(v24)), witness_sort[a9]) → false_renamed
greater_int(neg(01), pos(s(v30))) → false_renamed
greater_int(neg(01), neg(v31)) → false_renamed
greater_int(neg(01), witness_sort[a9]) → false_renamed
greater_int(neg(s(v32)), pos(s(v34))) → false_renamed
greater_int(neg(s(v32)), neg(v35)) → false_renamed
greater_int(neg(s(v32)), witness_sort[a9]) → false_renamed
greater_int(witness_sort[a9], v19) → false_renamed
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(v36), pos(v37)) → equal_sort[a10](v36, v37)
equal_sort[a9](pos(v36), neg(v38)) → false
equal_sort[a9](pos(v36), witness_sort[a9]) → false
equal_sort[a9](neg(v39), pos(v40)) → false
equal_sort[a9](neg(v39), neg(v41)) → equal_sort[a10](v39, v41)
equal_sort[a9](neg(v39), witness_sort[a9]) → false
equal_sort[a9](witness_sort[a9], pos(v42)) → false
equal_sort[a9](witness_sort[a9], neg(v43)) → false
equal_sort[a9](witness_sort[a9], witness_sort[a9]) → true
equal_sort[a7](false_renamed, false_renamed) → true
equal_sort[a7](false_renamed, true_renamed) → false
equal_sort[a7](true_renamed, false_renamed) → false
equal_sort[a7](true_renamed, true_renamed) → true
equal_sort[a10](01, 01) → true
equal_sort[a10](01, s(v44)) → false
equal_sort[a10](s(v45), 01) → false
equal_sort[a10](s(v45), s(v46)) → equal_sort[a0](v45, v46)
equal_sort[a21](witness_sort[a21], witness_sort[a21]) → true


(24) Obligation:

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

(25) RisEmptyProof (EQUIVALENT transformation)

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

(26) YES