Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 210 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 10 ms)
↳4 JBCTerminationSCC
↳5 SCCToIDPv1Proof (⇒, 90 ms)
↳6 IDP
↳7 IDPNonInfProof (⇒, 440 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 (⇒, 200 ms)
↳18 AND
    ↳19 QDP
        ↳20 DependencyGraphProof (⇔, 0 ms)
        ↳21 TRUE
    ↳22 QTRS
        ↳23 QTRSRRRProof (⇔, 30 ms)
        ↳24 QTRS
        ↳25 QTRSRRRProof (⇔, 0 ms)
        ↳26 QTRS
        ↳27 QTRSRRRProof (⇔, 0 ms)
        ↳28 QTRS
        ↳29 RisEmptyProof (⇔, 0 ms)
        ↳30 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:
780_0_main_LE(EOS(STATIC_780), i73, i162, i175, i175) → 784_0_main_LE(EOS(STATIC_784), i73, i162, i175, i175)
784_0_main_LE(EOS(STATIC_784), i73, i162, i175, i175) → 788_0_main_Load(EOS(STATIC_788), i73, i162, i175) | >(i175, 0)
788_0_main_Load(EOS(STATIC_788), i73, i162, i175) → 791_0_main_EQ(EOS(STATIC_791), i73, i162, i175, i162)
791_0_main_EQ(EOS(STATIC_791), i73, i179, i175, i179) → 793_0_main_EQ(EOS(STATIC_793), i73, i179, i175, i179)
791_0_main_EQ(EOS(STATIC_791), i73, matching1, i175, matching2) → 794_0_main_EQ(EOS(STATIC_794), i73, 0, i175, 0) | &&(=(matching1, 0), =(matching2, 0))
793_0_main_EQ(EOS(STATIC_793), i73, i179, i175, i179) → 797_0_main_Load(EOS(STATIC_797), i73, i179, i175) | !(=(i179, 0))
797_0_main_Load(EOS(STATIC_797), i73, i179, i175) → 801_0_main_LE(EOS(STATIC_801), i73, i179, i175, i179)
801_0_main_LE(EOS(STATIC_801), i73, i186, i175, i186) → 806_0_main_LE(EOS(STATIC_806), i73, i186, i175, i186)
806_0_main_LE(EOS(STATIC_806), i73, i186, i175, i186) → 813_0_main_Load(EOS(STATIC_813), i73, i186, i175) | >(i186, 0)
813_0_main_Load(EOS(STATIC_813), i73, i186, i175) → 818_0_main_LE(EOS(STATIC_818), i73, i186, i175, i73)
818_0_main_LE(EOS(STATIC_818), i189, i186, i175, i189) → 824_0_main_LE(EOS(STATIC_824), i189, i186, i175, i189)
824_0_main_LE(EOS(STATIC_824), i189, i186, i175, i189) → 831_0_main_Load(EOS(STATIC_831), i189, i186, i175) | >(i189, 0)
831_0_main_Load(EOS(STATIC_831), i189, i186, i175) → 838_0_main_NE(EOS(STATIC_838), i189, i186, i175, i186)
838_0_main_NE(EOS(STATIC_838), i189, i186, i175, i186) → 840_0_main_Inc(EOS(STATIC_840), i189, i186, i175) | >(i186, 0)
840_0_main_Inc(EOS(STATIC_840), i189, i186, i175) → 842_0_main_Inc(EOS(STATIC_842), +(i189, -1), i186, i175) | >(i189, 0)
842_0_main_Inc(EOS(STATIC_842), i193, i186, i175) → 843_0_main_JMP(EOS(STATIC_843), i193, +(i186, -1), i175) | >(i186, 0)
843_0_main_JMP(EOS(STATIC_843), i193, i194, i175) → 848_0_main_Load(EOS(STATIC_848), i193, i194, i175)
848_0_main_Load(EOS(STATIC_848), i193, i194, i175) → 777_0_main_Load(EOS(STATIC_777), i193, i194, i175)
777_0_main_Load(EOS(STATIC_777), i73, i162, i163) → 780_0_main_LE(EOS(STATIC_780), i73, i162, i163, i163)
794_0_main_EQ(EOS(STATIC_794), i73, matching1, i175, matching2) → 798_0_main_Load(EOS(STATIC_798), i73, 0, i175) | &&(=(matching1, 0), =(matching2, 0))
798_0_main_Load(EOS(STATIC_798), i73, matching1, i175) → 802_0_main_NE(EOS(STATIC_802), i73, 0, i175, 0) | =(matching1, 0)
802_0_main_NE(EOS(STATIC_802), i73, matching1, i175, matching2) → 808_0_main_Inc(EOS(STATIC_808), i73, i175) | &&(=(matching1, 0), =(matching2, 0))
808_0_main_Inc(EOS(STATIC_808), i73, i175) → 815_0_main_Load(EOS(STATIC_815), i73, i175)
815_0_main_Load(EOS(STATIC_815), i73, i175) → 820_0_main_Store(EOS(STATIC_820), i73, i175, i175)
820_0_main_Store(EOS(STATIC_820), i73, i175, i175) → 825_0_main_JMP(EOS(STATIC_825), i73, i175, i175)
825_0_main_JMP(EOS(STATIC_825), i73, i175, i175) → 834_0_main_Load(EOS(STATIC_834), i73, i175, i175)
834_0_main_Load(EOS(STATIC_834), i73, i175, i175) → 777_0_main_Load(EOS(STATIC_777), i73, i175, i175)
R rules:

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


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

Filtered ground terms:



780_0_main_LE(x1, x2, x3, x4, x5) → 780_0_main_LE(x2, x3, x4, x5)
EOS(x1) → EOS
Cond_780_0_main_LE1(x1, x2, x3, x4, x5, x6) → Cond_780_0_main_LE1(x1, x3, x5, x6)
Cond_780_0_main_LE(x1, x2, x3, x4, x5, x6) → Cond_780_0_main_LE(x1, x3, x4, x5, x6)

Filtered duplicate args:



780_0_main_LE(x1, x2, x3, x4) → 780_0_main_LE(x1, x2, x4)
Cond_780_0_main_LE(x1, x2, x3, x4, x5) → Cond_780_0_main_LE(x1, x2, x3, x5)
Cond_780_0_main_LE1(x1, x2, x3, x4) → Cond_780_0_main_LE1(x1, x2, x4)

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


P rules:
780_0_main_LE(x0, x1, x2) → 780_0_main_LE(+(x0, -1), +(x1, -1), x2) | &&(&&(>(x2, 0), >(x1, 0)), >(x0, 0))
780_0_main_LE(x0, 0, x2) → 780_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:
780_0_MAIN_LE(x0, x1, x2) → COND_780_0_MAIN_LE(&&(&&(>(x2, 0), >(x1, 0)), >(x0, 0)), x0, x1, x2)
COND_780_0_MAIN_LE(TRUE, x0, x1, x2) → 780_0_MAIN_LE(+(x0, -1), +(x1, -1), x2)
780_0_MAIN_LE(x0, 0, x2) → COND_780_0_MAIN_LE1(>(x2, 0), x0, 0, x2)
COND_780_0_MAIN_LE1(TRUE, x0, 0, x2) → 780_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): 780_0_MAIN_LE(x0[0], x1[0], x2[0]) → COND_780_0_MAIN_LE(x2[0] > 0 && x1[0] > 0 && x0[0] > 0, x0[0], x1[0], x2[0])
(1): COND_780_0_MAIN_LE(TRUE, x0[1], x1[1], x2[1]) → 780_0_MAIN_LE(x0[1] + -1, x1[1] + -1, x2[1])
(2): 780_0_MAIN_LE(x0[2], 0, x2[2]) → COND_780_0_MAIN_LE1(x2[2] > 0, x0[2], 0, x2[2])
(3): COND_780_0_MAIN_LE1(TRUE, x0[3], 0, x2[3]) → 780_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@1f0112ed 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 780_0_MAIN_LE(x0, x1, x2) → COND_780_0_MAIN_LE(&&(&&(>(x2, 0), >(x1, 0)), >(x0, 0)), x0, x1, x2) the following chains were created:
  • We consider the chain 780_0_MAIN_LE(x0[0], x1[0], x2[0]) → COND_780_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0]), COND_780_0_MAIN_LE(TRUE, x0[1], x1[1], x2[1]) → 780_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] ⇒ 780_0_MAIN_LE(x0[0], x1[0], x2[0])≥NonInfC∧780_0_MAIN_LE(x0[0], x1[0], x2[0])≥COND_780_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])∧(UIncreasing(COND_780_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 ⇒ 780_0_MAIN_LE(x0[0], x1[0], x2[0])≥NonInfC∧780_0_MAIN_LE(x0[0], x1[0], x2[0])≥COND_780_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])∧(UIncreasing(COND_780_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_780_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])), ≥)∧[bni_19 + (-1)Bound*bni_19] + [bni_19]x0[0] ≥ 0∧[(-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_780_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])), ≥)∧[bni_19 + (-1)Bound*bni_19] + [bni_19]x0[0] ≥ 0∧[(-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_780_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])), ≥)∧[bni_19 + (-1)Bound*bni_19] + [bni_19]x0[0] ≥ 0∧[(-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_780_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])), ≥)∧[(2)bni_19 + (-1)Bound*bni_19] + [bni_19]x0[0] ≥ 0∧[(-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_780_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])), ≥)∧[(2)bni_19 + (-1)Bound*bni_19] + [bni_19]x0[0] ≥ 0∧[(-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_780_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])), ≥)∧[(2)bni_19 + (-1)Bound*bni_19] + [bni_19]x0[0] ≥ 0∧[(-1)bso_20] ≥ 0)







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



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







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







For Pair COND_780_0_MAIN_LE1(TRUE, x0, 0, x2) → 780_0_MAIN_LE(x0, x2, x2) the following chains were created:
  • We consider the chain COND_780_0_MAIN_LE1(TRUE, x0[3], 0, x2[3]) → 780_0_MAIN_LE(x0[3], x2[3], x2[3]), 780_0_MAIN_LE(x0[0], x1[0], x2[0]) → COND_780_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_780_0_MAIN_LE1(TRUE, x0[3], 0, x2[3])≥NonInfC∧COND_780_0_MAIN_LE1(TRUE, x0[3], 0, x2[3])≥780_0_MAIN_LE(x0[3], x2[3], x2[3])∧(UIncreasing(780_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_780_0_MAIN_LE1(TRUE, x0[3], 0, x2[3])≥NonInfC∧COND_780_0_MAIN_LE1(TRUE, x0[3], 0, x2[3])≥780_0_MAIN_LE(x0[3], x2[3], x2[3])∧(UIncreasing(780_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(780_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(780_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(780_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(780_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_780_0_MAIN_LE1(TRUE, x0[3], 0, x2[3]) → 780_0_MAIN_LE(x0[3], x2[3], x2[3]), 780_0_MAIN_LE(x0[2], 0, x2[2]) → COND_780_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_780_0_MAIN_LE1(TRUE, x0[3], 0, x2[3])≥NonInfC∧COND_780_0_MAIN_LE1(TRUE, x0[3], 0, x2[3])≥780_0_MAIN_LE(x0[3], x2[3], x2[3])∧(UIncreasing(780_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_780_0_MAIN_LE1(TRUE, x0[3], 0, 0)≥NonInfC∧COND_780_0_MAIN_LE1(TRUE, x0[3], 0, 0)≥780_0_MAIN_LE(x0[3], 0, 0)∧(UIncreasing(780_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(780_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(780_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(780_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(780_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.
  • 780_0_MAIN_LE(x0, x1, x2) → COND_780_0_MAIN_LE(&&(&&(>(x2, 0), >(x1, 0)), >(x0, 0)), x0, x1, x2)
    • (x0[0] ≥ 0∧x2[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_780_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])), ≥)∧[(2)bni_19 + (-1)Bound*bni_19] + [bni_19]x0[0] ≥ 0∧[(-1)bso_20] ≥ 0)

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

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

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

The following pairs are in P>:

COND_780_0_MAIN_LE(TRUE, x0[1], x1[1], x2[1]) → 780_0_MAIN_LE(+(x0[1], -1), +(x1[1], -1), x2[1])

The following pairs are in Pbound:

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

The following pairs are in P≥:

780_0_MAIN_LE(x0[0], x1[0], x2[0]) → COND_780_0_MAIN_LE(&&(&&(>(x2[0], 0), >(x1[0], 0)), >(x0[0], 0)), x0[0], x1[0], x2[0])
780_0_MAIN_LE(x0[2], 0, x2[2]) → COND_780_0_MAIN_LE1(>(x2[2], 0), x0[2], 0, x2[2])
COND_780_0_MAIN_LE1(TRUE, x0[3], 0, x2[3]) → 780_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:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): 780_0_MAIN_LE(x0[0], x1[0], x2[0]) → COND_780_0_MAIN_LE(x2[0] > 0 && x1[0] > 0 && x0[0] > 0, x0[0], x1[0], x2[0])
(2): 780_0_MAIN_LE(x0[2], 0, x2[2]) → COND_780_0_MAIN_LE1(x2[2] > 0, x0[2], 0, x2[2])
(3): COND_780_0_MAIN_LE1(TRUE, x0[3], 0, x2[3]) → 780_0_MAIN_LE(x0[3], x2[3], 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])


(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_780_0_MAIN_LE1(TRUE, x0[3], 0, x2[3]) → 780_0_MAIN_LE(x0[3], x2[3], x2[3])
(2): 780_0_MAIN_LE(x0[2], 0, x2[2]) → COND_780_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_780_0_MAIN_LE1(true, x0[3], pos(01), x2[3]) → 780_0_MAIN_LE(x0[3], x2[3], x2[3])
780_0_MAIN_LE(x0[2], pos(01), x2[2]) → COND_780_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_780_0_MAIN_LE1(true, x0[3], pos(01), x2[3]) → 780_0_MAIN_LE(x0[3], x2[3], x2[3])
780_0_MAIN_LE(x0[2], pos(01), x2[2]) → COND_780_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 780_0_MAIN_LE(x0[2], pos(01), x2[2]) → COND_780_0_MAIN_LE1(greater_int(x2[2], pos(01)), x0[2], pos(01), x2[2]) we obtained the following new rules [LPAR04]:

780_0_MAIN_LE(z0, pos(01), pos(01)) → COND_780_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_780_0_MAIN_LE1(true, x0[3], pos(01), x2[3]) → 780_0_MAIN_LE(x0[3], x2[3], x2[3])
780_0_MAIN_LE(z0, pos(01), pos(01)) → COND_780_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:
780_0_MAIN_LE(z0, pos(01), pos(01)) → COND_780_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(780_0_MAIN_LE(x1, x2, x3)) = 1 + x1   
POL(COND_780_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: 0ed2840efdf9f991ffef2ebbd05a57b963a74414 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_780_0_MAIN_LE1(true, x0[3], pos(01), x2[3]) → 780_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:
Polynomial interpretation [POLO]:

POL(01) = 0   
POL(and(x1, x2)) = 2 + x1 + x2   
POL(equal_bool(x1, x2)) = 1 + x1 + x2   
POL(equal_sort[a0](x1, x2)) = 1 + 2·x1 + x2   
POL(equal_sort[a10](x1, x2)) = 2 + 2·x1 + x2   
POL(equal_sort[a21](x1, x2)) = 2 + 2·x1 + x2   
POL(equal_sort[a2](x1, x2)) = 2·x1 + x2   
POL(equal_sort[a7](x1, x2)) = 1 + x1 + 2·x2   
POL(equal_sort[a9](x1, x2)) = 2 + 2·x1 + x2   
POL(false) = 0   
POL(false_renamed) = 0   
POL(greater_int(x1, x2)) = x1 + 2·x2   
POL(greater_int'(x1, x2)) = 1 + 2·x1 + 2·x2   
POL(isa_false(x1)) = 1 + x1   
POL(isa_true(x1)) = 1 + x1   
POL(neg(x1)) = 2 + x1   
POL(not(x1)) = 1 + 2·x1   
POL(or(x1, x2)) = 2 + 2·x1 + x2   
POL(pos(x1)) = x1   
POL(s(x1)) = 2 + 2·x1   
POL(true) = 1   
POL(true_renamed) = 0   
POL(witness_sort[a0]) = 2   
POL(witness_sort[a21]) = 2   
POL(witness_sort[a2]) = 1   
POL(witness_sort[a9]) = 0   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

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(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(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
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
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), 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, true_renamed) → false
equal_sort[a7](true_renamed, false_renamed) → false
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:
The TRS R consists of the following rules:

greater_int'(pos(01), pos(01)) → true
greater_int(pos(01), pos(01)) → false_renamed
greater_int(pos(01), witness_sort[a9]) → false_renamed
greater_int(witness_sort[a9], v19) → false_renamed
equal_bool(false, false) → true
not(false) → true
isa_false(false) → true
equal_sort[a9](pos(v36), pos(v37)) → equal_sort[a10](v36, v37)
equal_sort[a7](false_renamed, false_renamed) → true
equal_sort[a7](true_renamed, true_renamed) → true

Q is empty.

(25) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(01) = 0   
POL(equal_bool(x1, x2)) = 1 + 2·x1 + 2·x2   
POL(equal_sort[a10](x1, x2)) = 1 + x1 + x2   
POL(equal_sort[a7](x1, x2)) = 2 + 2·x1 + x2   
POL(equal_sort[a9](x1, x2)) = 2 + 2·x1 + x2   
POL(false) = 0   
POL(false_renamed) = 2   
POL(greater_int(x1, x2)) = 1 + 2·x1 + x2   
POL(greater_int'(x1, x2)) = 2·x1 + x2   
POL(isa_false(x1)) = 1 + x1   
POL(not(x1)) = 1 + 2·x1   
POL(pos(x1)) = 2 + x1   
POL(true) = 1   
POL(true_renamed) = 2   
POL(witness_sort[a9]) = 1   
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(pos(01), pos(01)) → false_renamed
greater_int(pos(01), witness_sort[a9]) → false_renamed
greater_int(witness_sort[a9], v19) → false_renamed
equal_sort[a9](pos(v36), pos(v37)) → equal_sort[a10](v36, v37)
equal_sort[a7](false_renamed, false_renamed) → true
equal_sort[a7](true_renamed, true_renamed) → true


(26) Obligation:

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

equal_bool(false, false) → true
not(false) → true
isa_false(false) → true

Q is empty.

(27) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(equal_bool(x1, x2)) = 2 + 2·x1 + x2   
POL(false) = 2   
POL(isa_false(x1)) = 2 + 2·x1   
POL(not(x1)) = 2 + 2·x1   
POL(true) = 1   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

equal_bool(false, false) → true
not(false) → true
isa_false(false) → true


(28) Obligation:

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

(29) RisEmptyProof (EQUIVALENT transformation)

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

(30) YES