Termination proof of /tmp/tmpORv3lA/TimesPlusUserDef.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 570 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 320 ms)

        ↳7 IDP

        ↳8 IDPNonInfProof (⇒, 340 ms)

        ↳9 AND

            ↳10 IDP

                ↳11 IDependencyGraphProof (⇔, 0 ms)

                ↳12 IDP

                ↳13 UsableRulesProof (⇔, 0 ms)

                ↳14 IDP

                ↳15 IDPNonInfProof (⇒, 100 ms)

                ↳16 IDP

                ↳17 IDependencyGraphProof (⇔, 0 ms)

                ↳18 TRUE

            ↳19 IDP

                ↳20 IDependencyGraphProof (⇔, 0 ms)

                ↳21 IDP

                ↳22 UsableRulesProof (⇔, 0 ms)

                ↳23 IDP

                ↳24 IDPNonInfProof (⇒, 120 ms)

                ↳25 AND

                    ↳26 IDP

                        ↳27 IDependencyGraphProof (⇔, 0 ms)

                        ↳28 TRUE

                    ↳29 IDP

                        ↳30 IDependencyGraphProof (⇔, 0 ms)

                        ↳31 TRUE

    ↳32 JBCTerminationSCC

        ↳33 SCCToIDPv1Proof (⇒, 840 ms)

        ↳34 IDP

        ↳35 IDPNonInfProof (⇒, 130 ms)

        ↳36 AND

            ↳37 IDP

                ↳38 IDependencyGraphProof (⇔, 0 ms)

                ↳39 TRUE

            ↳40 IDP

                ↳41 IDependencyGraphProof (⇔, 0 ms)

                ↳42 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_22 (Sun Microsystems Inc.) Main-Class: TimesPlusUserDef

public class TimesPlusUserDef {
	public static void main(String[] args) {
		int x, y;
		x = args[0].length();
		y = args[1].length();
		times(x, y);
	}

	public static int times(int x, int y) {
		if (y == 0)
			return 0;
		if (y > 0)
			return plus(times(x, y - 1), x);
		return 0;
	}

	public static int plus(int x, int y) {
		if (y > 0) {
			return 1 + plus(x, y-1);
		} else if (x > 0) {
			return 1 + plus(x-1, y);
		} else {
			return 0;
		}
	}
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
TimesPlusUserDef.main([Ljava/lang/String;)V: Graph of 158 nodes with 0 SCCs.

TimesPlusUserDef.times(II)I: Graph of 52 nodes with 0 SCCs.

TimesPlusUserDef.plus(II)I: Graph of 63 nodes with 0 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 2 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: TimesPlusUserDef.plus(II)I
SCC calls the following helper methods: TimesPlusUserDef.plus(II)I
Performed SCC analyses: UsedFieldsAnalysis

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 24 rules for P and 38 rules for R.

P rules:
1464_0_plus_LE(EOS(STATIC_1464), i669, i673, i673) → 1466_0_plus_LE(EOS(STATIC_1466), i669, i673, i673)
1464_0_plus_LE(EOS(STATIC_1464), i669, i674, i674) → 1467_0_plus_LE(EOS(STATIC_1467), i669, i674, i674)
1466_0_plus_LE(EOS(STATIC_1466), i669, i673, i673) → 1469_0_plus_Load(EOS(STATIC_1469), i669, i673) | <=(i673, 0)
1469_0_plus_Load(EOS(STATIC_1469), i669, i673) → 1471_0_plus_LE(EOS(STATIC_1471), i669, i673, i669)
1471_0_plus_LE(EOS(STATIC_1471), i678, i673, i678) → 1475_0_plus_LE(EOS(STATIC_1475), i678, i673, i678)
1475_0_plus_LE(EOS(STATIC_1475), i678, i673, i678) → 1479_0_plus_ConstantStackPush(EOS(STATIC_1479), i678, i673) | >(i678, 0)
1479_0_plus_ConstantStackPush(EOS(STATIC_1479), i678, i673) → 1483_0_plus_Load(EOS(STATIC_1483), i678, i673, 1)
1483_0_plus_Load(EOS(STATIC_1483), i678, i673, matching1) → 1487_0_plus_ConstantStackPush(EOS(STATIC_1487), i673, 1, i678) | =(matching1, 1)
1487_0_plus_ConstantStackPush(EOS(STATIC_1487), i673, matching1, i678) → 1491_0_plus_IntArithmetic(EOS(STATIC_1491), i673, 1, i678, 1) | =(matching1, 1)
1491_0_plus_IntArithmetic(EOS(STATIC_1491), i673, matching1, i678, matching2) → 1495_0_plus_Load(EOS(STATIC_1495), i673, 1, -(i678, 1)) | &&(&&(>(i678, 0), =(matching1, 1)), =(matching2, 1))
1495_0_plus_Load(EOS(STATIC_1495), i673, matching1, i682) → 1499_0_plus_InvokeMethod(EOS(STATIC_1499), 1, i682, i673) | =(matching1, 1)
1499_0_plus_InvokeMethod(EOS(STATIC_1499), matching1, i682, i673) → 1502_1_plus_InvokeMethod(1502_0_plus_Load(EOS(STATIC_1502), i682, i673), 1, i682, i673) | =(matching1, 1)
1502_0_plus_Load(EOS(STATIC_1502), i682, i673) → 1507_0_plus_Load(EOS(STATIC_1507), i682, i673)
1507_0_plus_Load(EOS(STATIC_1507), i682, i673) → 1463_0_plus_Load(EOS(STATIC_1463), i682, i673)
1463_0_plus_Load(EOS(STATIC_1463), i669, i670) → 1464_0_plus_LE(EOS(STATIC_1464), i669, i670, i670)
1467_0_plus_LE(EOS(STATIC_1467), i669, i674, i674) → 1470_0_plus_ConstantStackPush(EOS(STATIC_1470), i669, i674) | >(i674, 0)
1470_0_plus_ConstantStackPush(EOS(STATIC_1470), i669, i674) → 1473_0_plus_Load(EOS(STATIC_1473), i669, i674, 1)
1473_0_plus_Load(EOS(STATIC_1473), i669, i674, matching1) → 1476_0_plus_Load(EOS(STATIC_1476), i669, i674, 1, i669) | =(matching1, 1)
1476_0_plus_Load(EOS(STATIC_1476), i669, i674, matching1, i669) → 1480_0_plus_ConstantStackPush(EOS(STATIC_1480), i669, i674, 1, i669, i674) | =(matching1, 1)
1480_0_plus_ConstantStackPush(EOS(STATIC_1480), i669, i674, matching1, i669, i674) → 1484_0_plus_IntArithmetic(EOS(STATIC_1484), i669, i674, 1, i669, i674, 1) | =(matching1, 1)
1484_0_plus_IntArithmetic(EOS(STATIC_1484), i669, i674, matching1, i669, i674, matching2) → 1488_0_plus_InvokeMethod(EOS(STATIC_1488), i669, i674, 1, i669, -(i674, 1)) | &&(&&(>(i674, 0), =(matching1, 1)), =(matching2, 1))
1488_0_plus_InvokeMethod(EOS(STATIC_1488), i669, i674, matching1, i669, i679) → 1493_1_plus_InvokeMethod(1493_0_plus_Load(EOS(STATIC_1493), i669, i679), i669, i674, 1, i669, i679) | =(matching1, 1)
1493_0_plus_Load(EOS(STATIC_1493), i669, i679) → 1496_0_plus_Load(EOS(STATIC_1496), i669, i679)
1496_0_plus_Load(EOS(STATIC_1496), i669, i679) → 1463_0_plus_Load(EOS(STATIC_1463), i669, i679)
R rules:
1471_0_plus_LE(EOS(STATIC_1471), i677, i673, i677) → 1474_0_plus_LE(EOS(STATIC_1474), i677, i673, i677)
1474_0_plus_LE(EOS(STATIC_1474), i677, i673, i677) → 1477_0_plus_ConstantStackPush(EOS(STATIC_1477)) | <=(i677, 0)
1477_0_plus_ConstantStackPush(EOS(STATIC_1477)) → 1481_0_plus_Return(EOS(STATIC_1481), 0)
1493_1_plus_InvokeMethod(1481_0_plus_Return(EOS(STATIC_1481), matching1), i684, i674, matching2, i684, matching3) → 1509_0_plus_Return(EOS(STATIC_1509), i684, i674, 1, i684, 0, 0) | &&(&&(=(matching1, 0), =(matching2, 1)), =(matching3, 0))
1493_1_plus_InvokeMethod(1517_0_plus_Return(EOS(STATIC_1517), i703, i704, matching1), i703, i674, matching2, i703, i704) → 1529_0_plus_Return(EOS(STATIC_1529), i703, i674, 1, i703, i704, i703, i704, 1) | &&(=(matching1, 1), =(matching2, 1))
1493_1_plus_InvokeMethod(1527_0_plus_Return(EOS(STATIC_1527), matching1), i709, i674, matching2, i709, matching3) → 1543_0_plus_Return(EOS(STATIC_1543), i709, i674, 1, i709, 0, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 0))
1493_1_plus_InvokeMethod(1774_0_plus_Return(EOS(STATIC_1774), i1029, i1030, i1006), i1029, i674, matching1, i1029, i1030) → 1811_0_plus_Return(EOS(STATIC_1811), i1029, i674, 1, i1029, i1030, i1029, i1030, i1006) | =(matching1, 1)
1493_1_plus_InvokeMethod(1834_0_plus_Return(EOS(STATIC_1834), i1107, i1108, i1091), i1107, i674, matching1, i1107, i1108) → 1856_0_plus_Return(EOS(STATIC_1856), i1107, i674, 1, i1107, i1108, i1107, i1108, i1091) | =(matching1, 1)
1493_1_plus_InvokeMethod(1837_0_plus_Return(EOS(STATIC_1837), i1092), i1113, i674, matching1, i1113, matching2) → 1861_0_plus_Return(EOS(STATIC_1861), i1113, i674, 1, i1113, 0, i1092) | &&(=(matching1, 1), =(matching2, 0))
1502_1_plus_InvokeMethod(1481_0_plus_Return(EOS(STATIC_1481), matching1), matching2, matching3, i699) → 1518_0_plus_Return(EOS(STATIC_1518), 1, 0, i699, 0) | &&(&&(=(matching1, 0), =(matching2, 1)), =(matching3, 0))
1502_1_plus_InvokeMethod(1527_0_plus_Return(EOS(STATIC_1527), matching1), matching2, i711, i712) → 1544_0_plus_Return(EOS(STATIC_1544), 1, i711, i712, 1) | &&(=(matching1, 1), =(matching2, 1))
1502_1_plus_InvokeMethod(1837_0_plus_Return(EOS(STATIC_1837), i1092), matching1, i1115, i1116) → 1863_0_plus_Return(EOS(STATIC_1863), 1, i1115, i1116, i1092) | =(matching1, 1)
1509_0_plus_Return(EOS(STATIC_1509), i684, i674, matching1, i684, matching2, matching3) → 1513_0_plus_IntArithmetic(EOS(STATIC_1513), i684, i674, 1, 0) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
1513_0_plus_IntArithmetic(EOS(STATIC_1513), i684, i674, matching1, matching2) → 1517_0_plus_Return(EOS(STATIC_1517), i684, i674, 1) | &&(=(matching1, 1), =(matching2, 0))
1518_0_plus_Return(EOS(STATIC_1518), matching1, matching2, i699, matching3) → 1521_0_plus_IntArithmetic(EOS(STATIC_1521), 1, 0) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
1521_0_plus_IntArithmetic(EOS(STATIC_1521), matching1, matching2) → 1527_0_plus_Return(EOS(STATIC_1527), 1) | &&(=(matching1, 1), =(matching2, 0))
1529_0_plus_Return(EOS(STATIC_1529), i703, i674, matching1, i703, i704, i703, i704, matching2) → 1575_0_plus_Return(EOS(STATIC_1575), i703, i674, 1, i703, i704, i703, i704, 1) | &&(=(matching1, 1), =(matching2, 1))
1543_0_plus_Return(EOS(STATIC_1543), i709, i674, matching1, i709, matching2, matching3) → 1617_0_plus_Return(EOS(STATIC_1617), i709, i674, 1, i709, 0, 1) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 1))
1544_0_plus_Return(EOS(STATIC_1544), matching1, i711, i712, matching2) → 1621_0_plus_Return(EOS(STATIC_1621), 1, i711, i712, 1) | &&(=(matching1, 1), =(matching2, 1))
1575_0_plus_Return(EOS(STATIC_1575), i739, i674, matching1, i739, i740, i739, i740, i741) → 1607_0_plus_Return(EOS(STATIC_1607), i739, i674, 1, i739, i740, i739, i740, i741) | =(matching1, 1)
1607_0_plus_Return(EOS(STATIC_1607), i779, i674, matching1, i779, i780, i779, i780, i781) → 1671_0_plus_Return(EOS(STATIC_1671), i779, i674, 1, i779, i780, i779, i780, i781) | =(matching1, 1)
1617_0_plus_Return(EOS(STATIC_1617), i792, i674, matching1, i792, matching2, i793) → 1685_0_plus_Return(EOS(STATIC_1685), i792, i674, 1, i792, 0, i793) | &&(=(matching1, 1), =(matching2, 0))
1621_0_plus_Return(EOS(STATIC_1621), matching1, i799, i797, i798) → 1692_0_plus_Return(EOS(STATIC_1692), 1, i799, i797, i798) | =(matching1, 1)
1671_0_plus_Return(EOS(STATIC_1671), i860, i674, matching1, i860, i861, i860, i861, i862) → 1743_0_plus_Return(EOS(STATIC_1743), i860, i674, 1, i860, i861, i860, i861, i862) | =(matching1, 1)
1685_0_plus_Return(EOS(STATIC_1685), i884, i674, matching1, i884, matching2, i885) → 1757_0_plus_Return(EOS(STATIC_1757), i884, i674, 1, i884, 0, i885) | &&(=(matching1, 1), =(matching2, 0))
1692_0_plus_Return(EOS(STATIC_1692), matching1, i894, i892, i893) → 1763_0_plus_Return(EOS(STATIC_1763), 1, i894, i892, i893) | =(matching1, 1)
1743_0_plus_Return(EOS(STATIC_1743), i960, i674, matching1, i960, i961, i960, i961, i962) → 1767_0_plus_IntArithmetic(EOS(STATIC_1767), i960, i674, 1, i962) | =(matching1, 1)
1757_0_plus_Return(EOS(STATIC_1757), i984, i674, matching1, i984, matching2, i985) → 1823_0_plus_Return(EOS(STATIC_1823), i984, i674, 1, i984, 0, i985) | &&(=(matching1, 1), =(matching2, 0))
1763_0_plus_Return(EOS(STATIC_1763), matching1, i994, i992, i993) → 1827_0_plus_Return(EOS(STATIC_1827), 1, i994, i992, i993) | =(matching1, 1)
1767_0_plus_IntArithmetic(EOS(STATIC_1767), i960, i674, matching1, i962) → 1774_0_plus_Return(EOS(STATIC_1774), i960, i674, +(1, i962)) | &&(>(i962, 0), =(matching1, 1))
1811_0_plus_Return(EOS(STATIC_1811), i1029, i674, matching1, i1029, i1030, i1029, i1030, i1006) → 1743_0_plus_Return(EOS(STATIC_1743), i1029, i674, 1, i1029, i1030, i1029, i1030, i1006) | =(matching1, 1)
1823_0_plus_Return(EOS(STATIC_1823), i1071, i674, matching1, i1071, matching2, i1072) → 1830_0_plus_IntArithmetic(EOS(STATIC_1830), i1071, i674, 1, i1072) | &&(=(matching1, 1), =(matching2, 0))
1827_0_plus_Return(EOS(STATIC_1827), matching1, i1081, i1079, i1080) → 1831_0_plus_IntArithmetic(EOS(STATIC_1831), 1, i1080) | =(matching1, 1)
1830_0_plus_IntArithmetic(EOS(STATIC_1830), i1071, i674, matching1, i1072) → 1834_0_plus_Return(EOS(STATIC_1834), i1071, i674, +(1, i1072)) | &&(>(i1072, 0), =(matching1, 1))
1831_0_plus_IntArithmetic(EOS(STATIC_1831), matching1, i1080) → 1837_0_plus_Return(EOS(STATIC_1837), +(1, i1080)) | &&(>(i1080, 0), =(matching1, 1))
1856_0_plus_Return(EOS(STATIC_1856), i1107, i674, matching1, i1107, i1108, i1107, i1108, i1091) → 1743_0_plus_Return(EOS(STATIC_1743), i1107, i674, 1, i1107, i1108, i1107, i1108, i1091) | =(matching1, 1)
1861_0_plus_Return(EOS(STATIC_1861), i1113, i674, matching1, i1113, matching2, i1092) → 1823_0_plus_Return(EOS(STATIC_1823), i1113, i674, 1, i1113, 0, i1092) | &&(=(matching1, 1), =(matching2, 0))
1863_0_plus_Return(EOS(STATIC_1863), matching1, i1115, i1116, i1092) → 1827_0_plus_Return(EOS(STATIC_1827), 1, i1115, i1116, i1092) | =(matching1, 1)

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

P rules:
1464_0_plus_LE(EOS(STATIC_1464), x0, x1, x1) → 1502_1_plus_InvokeMethod(1464_0_plus_LE(EOS(STATIC_1464), -(x0, 1), x1, x1), 1, -(x0, 1), x1) | &&(<=(x1, 0), >(x0, 0))
1464_0_plus_LE(EOS(STATIC_1464), x0, x1, x1) → 1493_1_plus_InvokeMethod(1464_0_plus_LE(EOS(STATIC_1464), x0, -(x1, 1), -(x1, 1)), x0, x1, 1, x0, -(x1, 1)) | >(x1, 0)
R rules:
1493_1_plus_InvokeMethod(1481_0_plus_Return(EOS(STATIC_1481), 0), x1, x2, 1, x1, 0) → 1517_0_plus_Return(EOS(STATIC_1517), x1, x2, 1)
1502_1_plus_InvokeMethod(1481_0_plus_Return(EOS(STATIC_1481), 0), 1, 0, x3) → 1527_0_plus_Return(EOS(STATIC_1527), 1)
1493_1_plus_InvokeMethod(1774_0_plus_Return(EOS(STATIC_1774), x0, x1, x2), x0, x3, 1, x0, x1) → 1774_0_plus_Return(EOS(STATIC_1774), x0, x3, +(1, x2)) | >(x2, 0)
1493_1_plus_InvokeMethod(1834_0_plus_Return(EOS(STATIC_1834), x0, x1, x2), x0, x3, 1, x0, x1) → 1774_0_plus_Return(EOS(STATIC_1774), x0, x3, +(1, x2)) | >(x2, 0)
1493_1_plus_InvokeMethod(1517_0_plus_Return(EOS(STATIC_1517), x0, x1, 1), x0, x3, 1, x0, x1) → 1774_0_plus_Return(EOS(STATIC_1774), x0, x3, 2)
1493_1_plus_InvokeMethod(1837_0_plus_Return(EOS(STATIC_1837), x0), x1, x2, 1, x1, 0) → 1834_0_plus_Return(EOS(STATIC_1834), x1, x2, +(1, x0)) | >(x0, 0)
1493_1_plus_InvokeMethod(1527_0_plus_Return(EOS(STATIC_1527), 1), x1, x2, 1, x1, 0) → 1834_0_plus_Return(EOS(STATIC_1834), x1, x2, 2)
1502_1_plus_InvokeMethod(1837_0_plus_Return(EOS(STATIC_1837), x0), 1, x2, x3) → 1837_0_plus_Return(EOS(STATIC_1837), +(1, x0)) | >(x0, 0)
1502_1_plus_InvokeMethod(1527_0_plus_Return(EOS(STATIC_1527), 1), 1, x2, x3) → 1837_0_plus_Return(EOS(STATIC_1837), 2)

Filtered ground terms:

1493_1_plus_InvokeMethod(x1, x2, x3, x4, x5, x6) → 1493_1_plus_InvokeMethod(x1, x2, x3, x5, x6)
1464_0_plus_LE(x1, x2, x3, x4) → 1464_0_plus_LE(x2, x3, x4)
Cond_1464_0_plus_LE1(x1, x2, x3, x4, x5) → Cond_1464_0_plus_LE1(x1, x3, x4, x5)
1502_1_plus_InvokeMethod(x1, x2, x3, x4) → 1502_1_plus_InvokeMethod(x1, x3, x4)
Cond_1464_0_plus_LE(x1, x2, x3, x4, x5) → Cond_1464_0_plus_LE(x1, x3, x4, x5)
1837_0_plus_Return(x1, x2) → 1837_0_plus_Return(x2)
1527_0_plus_Return(x1, x2) → 1527_0_plus_Return
Cond_1502_1_plus_InvokeMethod(x1, x2, x3, x4, x5) → Cond_1502_1_plus_InvokeMethod(x1, x2, x4, x5)
1834_0_plus_Return(x1, x2, x3, x4) → 1834_0_plus_Return(x2, x3, x4)
Cond_1493_1_plus_InvokeMethod2(x1, x2, x3, x4, x5, x6, x7) → Cond_1493_1_plus_InvokeMethod2(x1, x2, x3, x4, x6)
1774_0_plus_Return(x1, x2, x3, x4) → 1774_0_plus_Return(x2, x3, x4)
1517_0_plus_Return(x1, x2, x3, x4) → 1517_0_plus_Return(x2, x3)
Cond_1493_1_plus_InvokeMethod1(x1, x2, x3, x4, x5, x6, x7) → Cond_1493_1_plus_InvokeMethod1(x1, x2, x3, x4, x6, x7)
Cond_1493_1_plus_InvokeMethod(x1, x2, x3, x4, x5, x6, x7) → Cond_1493_1_plus_InvokeMethod(x1, x2, x3, x4, x6, x7)
1481_0_plus_Return(x1, x2) → 1481_0_plus_Return

Filtered duplicate args:

1464_0_plus_LE(x1, x2, x3) → 1464_0_plus_LE(x1, x3)
Cond_1464_0_plus_LE(x1, x2, x3, x4) → Cond_1464_0_plus_LE(x1, x2, x4)
Cond_1464_0_plus_LE1(x1, x2, x3, x4) → Cond_1464_0_plus_LE1(x1, x2, x4)
1493_1_plus_InvokeMethod(x1, x2, x3, x4, x5) → 1493_1_plus_InvokeMethod(x1, x3, x4, x5)
Cond_1493_1_plus_InvokeMethod(x1, x2, x3, x4, x5, x6) → Cond_1493_1_plus_InvokeMethod(x1, x2, x4)
Cond_1493_1_plus_InvokeMethod1(x1, x2, x3, x4, x5, x6) → Cond_1493_1_plus_InvokeMethod1(x1, x2, x4)
Cond_1493_1_plus_InvokeMethod2(x1, x2, x3, x4, x5) → Cond_1493_1_plus_InvokeMethod2(x1, x2, x4, x5)

Filtered unneeded arguments:

1502_1_plus_InvokeMethod(x1, x2, x3) → 1502_1_plus_InvokeMethod(x1, x2)
1493_1_plus_InvokeMethod(x1, x2, x3, x4) → 1493_1_plus_InvokeMethod(x1, x4)
Cond_1493_1_plus_InvokeMethod(x1, x2, x3) → Cond_1493_1_plus_InvokeMethod(x1, x2)
Cond_1493_1_plus_InvokeMethod1(x1, x2, x3) → Cond_1493_1_plus_InvokeMethod1(x1, x2)
Cond_1493_1_plus_InvokeMethod2(x1, x2, x3, x4) → Cond_1493_1_plus_InvokeMethod2(x1, x2)
Cond_1502_1_plus_InvokeMethod(x1, x2, x3, x4) → Cond_1502_1_plus_InvokeMethod(x1, x2)
1774_0_plus_Return(x1, x2, x3) → 1774_0_plus_Return(x3)
1834_0_plus_Return(x1, x2, x3) → 1834_0_plus_Return(x3)

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

P rules:
1464_0_plus_LE(x0, x1) → 1502_1_plus_InvokeMethod(1464_0_plus_LE(-(x0, 1), x1), -(x0, 1)) | &&(<=(x1, 0), >(x0, 0))
1464_0_plus_LE(x0, x1) → 1493_1_plus_InvokeMethod(1464_0_plus_LE(x0, -(x1, 1)), -(x1, 1)) | >(x1, 0)
R rules:
1493_1_plus_InvokeMethod(1481_0_plus_Return, 0) → 1517_0_plus_Return(x1, x2)
1502_1_plus_InvokeMethod(1481_0_plus_Return, 0) → 1527_0_plus_Return
1493_1_plus_InvokeMethod(1774_0_plus_Return(x2), x1) → 1774_0_plus_Return(+(1, x2)) | >(x2, 0)
1493_1_plus_InvokeMethod(1834_0_plus_Return(x2), x1) → 1774_0_plus_Return(+(1, x2)) | >(x2, 0)
1493_1_plus_InvokeMethod(1517_0_plus_Return(x0, x1), x1) → 1774_0_plus_Return(2)
1493_1_plus_InvokeMethod(1837_0_plus_Return(x0), 0) → 1834_0_plus_Return(+(1, x0)) | >(x0, 0)
1493_1_plus_InvokeMethod(1527_0_plus_Return, 0) → 1834_0_plus_Return(2)
1502_1_plus_InvokeMethod(1837_0_plus_Return(x0), x2) → 1837_0_plus_Return(+(1, x0)) | >(x0, 0)
1502_1_plus_InvokeMethod(1527_0_plus_Return, x2) → 1837_0_plus_Return(2)

Performed bisimulation on rules. Used the following equivalence classes: {[1481_0_plus_Return, 1527_0_plus_Return]=1481_0_plus_Return, [1774_0_plus_Return_1, 1834_0_plus_Return_1, 1837_0_plus_Return_1]=1774_0_plus_Return_1, [Cond_1493_1_plus_InvokeMethod_3, Cond_1493_1_plus_InvokeMethod1_3, Cond_1502_1_plus_InvokeMethod_3]=Cond_1493_1_plus_InvokeMethod_3}

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

P rules:
1464_0_PLUS_LE(x0, x1) → COND_1464_0_PLUS_LE(&&(<=(x1, 0), >(x0, 0)), x0, x1)
COND_1464_0_PLUS_LE(TRUE, x0, x1) → 1464_0_PLUS_LE(-(x0, 1), x1)
1464_0_PLUS_LE(x0, x1) → COND_1464_0_PLUS_LE1(>(x1, 0), x0, x1)
COND_1464_0_PLUS_LE1(TRUE, x0, x1) → 1464_0_PLUS_LE(x0, -(x1, 1))
R rules:
1493_1_plus_InvokeMethod(1481_0_plus_Return, 0) → 1517_0_plus_Return(x1, x2)
1502_1_plus_InvokeMethod(1481_0_plus_Return, 0) → 1481_0_plus_Return
1493_1_plus_InvokeMethod(1774_0_plus_Return(x2), x1) → Cond_1493_1_plus_InvokeMethod(>(x2, 0), 1774_0_plus_Return(x2), x1)
Cond_1493_1_plus_InvokeMethod(TRUE, 1774_0_plus_Return(x2), x1) → 1774_0_plus_Return(+(1, x2))
1493_1_plus_InvokeMethod(1517_0_plus_Return(x0, x1), x1) → 1774_0_plus_Return(2)
1493_1_plus_InvokeMethod(1774_0_plus_Return(x0), 0) → Cond_1493_1_plus_InvokeMethod2(>(x0, 0), 1774_0_plus_Return(x0), 0)
Cond_1493_1_plus_InvokeMethod2(TRUE, 1774_0_plus_Return(x0), 0) → 1774_0_plus_Return(+(1, x0))
1493_1_plus_InvokeMethod(1481_0_plus_Return, 0) → 1774_0_plus_Return(2)
1502_1_plus_InvokeMethod(1774_0_plus_Return(x0), x2) → Cond_1493_1_plus_InvokeMethod(>(x0, 0), 1774_0_plus_Return(x0), x2)
1502_1_plus_InvokeMethod(1481_0_plus_Return, x2) → 1774_0_plus_Return(2)

(7) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

The ITRS R consists of the following rules:
1493_1_plus_InvokeMethod(1481_0_plus_Return, 0) → 1517_0_plus_Return(x1, x2)
1502_1_plus_InvokeMethod(1481_0_plus_Return, 0) → 1481_0_plus_Return
1493_1_plus_InvokeMethod(1774_0_plus_Return(x2), x1) → Cond_1493_1_plus_InvokeMethod(x2 > 0, 1774_0_plus_Return(x2), x1)
Cond_1493_1_plus_InvokeMethod(TRUE, 1774_0_plus_Return(x2), x1) → 1774_0_plus_Return(1 + x2)
1493_1_plus_InvokeMethod(1517_0_plus_Return(x0, x1), x1) → 1774_0_plus_Return(2)
1493_1_plus_InvokeMethod(1774_0_plus_Return(x0), 0) → Cond_1493_1_plus_InvokeMethod2(x0 > 0, 1774_0_plus_Return(x0), 0)
Cond_1493_1_plus_InvokeMethod2(TRUE, 1774_0_plus_Return(x0), 0) → 1774_0_plus_Return(1 + x0)
1493_1_plus_InvokeMethod(1481_0_plus_Return, 0) → 1774_0_plus_Return(2)
1502_1_plus_InvokeMethod(1774_0_plus_Return(x0), x2) → Cond_1493_1_plus_InvokeMethod(x0 > 0, 1774_0_plus_Return(x0), x2)
1502_1_plus_InvokeMethod(1481_0_plus_Return, x2) → 1774_0_plus_Return(2)

The integer pair graph contains the following rules and edges:
(0): 1464_0_PLUS_LE(x0[0], x1[0]) → COND_1464_0_PLUS_LE(x1[0] <= 0 && x0[0] > 0, x0[0], x1[0])
(1): COND_1464_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1464_0_PLUS_LE(x0[1] - 1, x1[1])
(2): 1464_0_PLUS_LE(x0[2], x1[2]) → COND_1464_0_PLUS_LE1(x1[2] > 0, x0[2], x1[2])
(3): COND_1464_0_PLUS_LE1(TRUE, x0[3], x1[3]) → 1464_0_PLUS_LE(x0[3], x1[3] - 1)

(0) -> (1), if (x1[0] <= 0 && x0[0] > 0 ∧x0[0] →^* x0[1]∧x1[0] →^* x1[1])

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

(1) -> (2), if (x0[1] - 1 →^* x0[2]∧x1[1] →^* x1[2])

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

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

(3) -> (2), if (x0[3] →^* x0[2]∧x1[3] - 1 →^* x1[2])

The set Q consists of the following terms:
1493_1_plus_InvokeMethod(1481_0_plus_Return, 0)
1493_1_plus_InvokeMethod(1774_0_plus_Return(x0), x1)
Cond_1493_1_plus_InvokeMethod(TRUE, 1774_0_plus_Return(x0), x1)
1493_1_plus_InvokeMethod(1517_0_plus_Return(x0, x1), x1)
Cond_1493_1_plus_InvokeMethod2(TRUE, 1774_0_plus_Return(x0), 0)
1502_1_plus_InvokeMethod(1774_0_plus_Return(x0), x1)
1502_1_plus_InvokeMethod(1481_0_plus_Return, x0)

(8) 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.IdpCand1ShapeHeuristic@8c1bb13 Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

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 1464_0_PLUS_LE(x0, x1) → COND_1464_0_PLUS_LE(&&(<=(x1, 0), >(x0, 0)), x0, x1) the following chains were created:

We consider the chain 1464_0_PLUS_LE(x0[0], x1[0]) → COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0]), COND_1464_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1464_0_PLUS_LE(-(x0[1], 1), x1[1]) which results in the following constraint:
(1)    (&&(<=(x1[0], 0), >(x0[0], 0))=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1] ⇒ 1464_0_PLUS_LE(x0[0], x1[0])≥NonInfC∧1464_0_PLUS_LE(x0[0], x1[0])≥COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])∧(U^Increasing(COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])), ≥))

We simplified constraint (1) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
(2)    (<=(x1[0], 0)=TRUE∧>(x0[0], 0)=TRUE ⇒ 1464_0_PLUS_LE(x0[0], x1[0])≥NonInfC∧1464_0_PLUS_LE(x0[0], x1[0])≥COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])∧(U^Increasing(COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    ([-1]x1[0] ≥ 0∧x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [bni_23]x1[0] ≥ 0∧[(-1)bso_24] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    ([-1]x1[0] ≥ 0∧x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [bni_23]x1[0] ≥ 0∧[(-1)bso_24] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    ([-1]x1[0] ≥ 0∧x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [bni_23]x1[0] ≥ 0∧[(-1)bso_24] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x1[0] ≥ 0∧x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [(-1)bni_23]x1[0] ≥ 0∧[(-1)bso_24] ≥ 0)

We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(7)    (x1[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [(-1)bni_23]x1[0] ≥ 0∧[(-1)bso_24] ≥ 0)

For Pair COND_1464_0_PLUS_LE(TRUE, x0, x1) → 1464_0_PLUS_LE(-(x0, 1), x1) the following chains were created:

We consider the chain COND_1464_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1464_0_PLUS_LE(-(x0[1], 1), x1[1]) which results in the following constraint:
(8)    (COND_1464_0_PLUS_LE(TRUE, x0[1], x1[1])≥NonInfC∧COND_1464_0_PLUS_LE(TRUE, x0[1], x1[1])≥1464_0_PLUS_LE(-(x0[1], 1), x1[1])∧(U^Increasing(1464_0_PLUS_LE(-(x0[1], 1), x1[1])), ≥))

We simplified constraint (8) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(9)    ((U^Increasing(1464_0_PLUS_LE(-(x0[1], 1), x1[1])), ≥)∧[bni_25] = 0∧[(-1)bso_26] ≥ 0)

We simplified constraint (9) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(10)    ((U^Increasing(1464_0_PLUS_LE(-(x0[1], 1), x1[1])), ≥)∧[bni_25] = 0∧[(-1)bso_26] ≥ 0)

We simplified constraint (10) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(11)    ((U^Increasing(1464_0_PLUS_LE(-(x0[1], 1), x1[1])), ≥)∧[bni_25] = 0∧[(-1)bso_26] ≥ 0)

We simplified constraint (11) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(12)    ((U^Increasing(1464_0_PLUS_LE(-(x0[1], 1), x1[1])), ≥)∧[bni_25] = 0∧0 = 0∧0 = 0∧[(-1)bso_26] ≥ 0)

For Pair 1464_0_PLUS_LE(x0, x1) → COND_1464_0_PLUS_LE1(>(x1, 0), x0, x1) the following chains were created:

We consider the chain 1464_0_PLUS_LE(x0[2], x1[2]) → COND_1464_0_PLUS_LE1(>(x1[2], 0), x0[2], x1[2]), COND_1464_0_PLUS_LE1(TRUE, x0[3], x1[3]) → 1464_0_PLUS_LE(x0[3], -(x1[3], 1)) which results in the following constraint:
(13)    (>(x1[2], 0)=TRUE∧x0[2]=x0[3]∧x1[2]=x1[3] ⇒ 1464_0_PLUS_LE(x0[2], x1[2])≥NonInfC∧1464_0_PLUS_LE(x0[2], x1[2])≥COND_1464_0_PLUS_LE1(>(x1[2], 0), x0[2], x1[2])∧(U^Increasing(COND_1464_0_PLUS_LE1(>(x1[2], 0), x0[2], x1[2])), ≥))

We simplified constraint (13) using rule (IV) which results in the following new constraint:
(14)    (>(x1[2], 0)=TRUE ⇒ 1464_0_PLUS_LE(x0[2], x1[2])≥NonInfC∧1464_0_PLUS_LE(x0[2], x1[2])≥COND_1464_0_PLUS_LE1(>(x1[2], 0), x0[2], x1[2])∧(U^Increasing(COND_1464_0_PLUS_LE1(>(x1[2], 0), x0[2], x1[2])), ≥))

We simplified constraint (14) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(15)    (x1[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_1464_0_PLUS_LE1(>(x1[2], 0), x0[2], x1[2])), ≥)∧[(-1)bni_27 + (-1)Bound*bni_27] + [bni_27]x1[2] ≥ 0∧[(-1)bso_28] ≥ 0)

We simplified constraint (15) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(16)    (x1[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_1464_0_PLUS_LE1(>(x1[2], 0), x0[2], x1[2])), ≥)∧[(-1)bni_27 + (-1)Bound*bni_27] + [bni_27]x1[2] ≥ 0∧[(-1)bso_28] ≥ 0)

We simplified constraint (16) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(17)    (x1[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_1464_0_PLUS_LE1(>(x1[2], 0), x0[2], x1[2])), ≥)∧[(-1)bni_27 + (-1)Bound*bni_27] + [bni_27]x1[2] ≥ 0∧[(-1)bso_28] ≥ 0)

We simplified constraint (17) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(18)    (x1[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_1464_0_PLUS_LE1(>(x1[2], 0), x0[2], x1[2])), ≥)∧0 = 0∧[(-1)bni_27 + (-1)Bound*bni_27] + [bni_27]x1[2] ≥ 0∧0 = 0∧[(-1)bso_28] ≥ 0)

We simplified constraint (18) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(19)    (x1[2] ≥ 0 ⇒ (U^Increasing(COND_1464_0_PLUS_LE1(>(x1[2], 0), x0[2], x1[2])), ≥)∧0 = 0∧[(-1)Bound*bni_27] + [bni_27]x1[2] ≥ 0∧0 = 0∧[(-1)bso_28] ≥ 0)

For Pair COND_1464_0_PLUS_LE1(TRUE, x0, x1) → 1464_0_PLUS_LE(x0, -(x1, 1)) the following chains were created:

We consider the chain COND_1464_0_PLUS_LE1(TRUE, x0[3], x1[3]) → 1464_0_PLUS_LE(x0[3], -(x1[3], 1)) which results in the following constraint:
(20)    (COND_1464_0_PLUS_LE1(TRUE, x0[3], x1[3])≥NonInfC∧COND_1464_0_PLUS_LE1(TRUE, x0[3], x1[3])≥1464_0_PLUS_LE(x0[3], -(x1[3], 1))∧(U^Increasing(1464_0_PLUS_LE(x0[3], -(x1[3], 1))), ≥))

We simplified constraint (20) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(21)    ((U^Increasing(1464_0_PLUS_LE(x0[3], -(x1[3], 1))), ≥)∧[bni_29] = 0∧[1 + (-1)bso_30] ≥ 0)

We simplified constraint (21) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(22)    ((U^Increasing(1464_0_PLUS_LE(x0[3], -(x1[3], 1))), ≥)∧[bni_29] = 0∧[1 + (-1)bso_30] ≥ 0)

We simplified constraint (22) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(23)    ((U^Increasing(1464_0_PLUS_LE(x0[3], -(x1[3], 1))), ≥)∧[bni_29] = 0∧[1 + (-1)bso_30] ≥ 0)

We simplified constraint (23) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(24)    ((U^Increasing(1464_0_PLUS_LE(x0[3], -(x1[3], 1))), ≥)∧[bni_29] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_30] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

1464_0_PLUS_LE(x0, x1) → COND_1464_0_PLUS_LE(&&(<=(x1, 0), >(x0, 0)), x0, x1)
- (x1[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [(-1)bni_23]x1[0] ≥ 0∧[(-1)bso_24] ≥ 0)
COND_1464_0_PLUS_LE(TRUE, x0, x1) → 1464_0_PLUS_LE(-(x0, 1), x1)
- ((U^Increasing(1464_0_PLUS_LE(-(x0[1], 1), x1[1])), ≥)∧[bni_25] = 0∧0 = 0∧0 = 0∧[(-1)bso_26] ≥ 0)
1464_0_PLUS_LE(x0, x1) → COND_1464_0_PLUS_LE1(>(x1, 0), x0, x1)
- (x1[2] ≥ 0 ⇒ (U^Increasing(COND_1464_0_PLUS_LE1(>(x1[2], 0), x0[2], x1[2])), ≥)∧0 = 0∧[(-1)Bound*bni_27] + [bni_27]x1[2] ≥ 0∧0 = 0∧[(-1)bso_28] ≥ 0)
COND_1464_0_PLUS_LE1(TRUE, x0, x1) → 1464_0_PLUS_LE(x0, -(x1, 1))
- ((U^Increasing(1464_0_PLUS_LE(x0[3], -(x1[3], 1))), ≥)∧[bni_29] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_30] ≥ 0)

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

POL(TRUE) = 0
POL(FALSE) = 0
POL(1493_1_plus_InvokeMethod(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁
POL(1481_0_plus_Return) = [-1]
POL(0) = 0
POL(1517_0_plus_Return(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁
POL(1502_1_plus_InvokeMethod(x₁, x₂)) = [-1] + [-1]x₁
POL(1774_0_plus_Return(x₁)) = x₁
POL(Cond_1493_1_plus_InvokeMethod(x₁, x₂, x₃)) = [-1] + [-1]x₃ + [-1]x₂
POL(>(x₁, x₂)) = [-1]
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(2) = [2]
POL(Cond_1493_1_plus_InvokeMethod2(x₁, x₂, x₃)) = [-1] + [-1]x₂
POL(1464_0_PLUS_LE(x₁, x₂)) = [-1] + x₂
POL(COND_1464_0_PLUS_LE(x₁, x₂, x₃)) = [-1] + x₃
POL(&&(x₁, x₂)) = [-1]
POL(<=(x₁, x₂)) = [-1]
POL(-(x₁, x₂)) = x₁ + [-1]x₂
POL(COND_1464_0_PLUS_LE1(x₁, x₂, x₃)) = [-1] + x₃

The following pairs are in P_>:

COND_1464_0_PLUS_LE1(TRUE, x0[3], x1[3]) → 1464_0_PLUS_LE(x0[3], -(x1[3], 1))

The following pairs are in P_bound:

1464_0_PLUS_LE(x0[2], x1[2]) → COND_1464_0_PLUS_LE1(>(x1[2], 0), x0[2], x1[2])

The following pairs are in P_≥:

1464_0_PLUS_LE(x0[0], x1[0]) → COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])
COND_1464_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1464_0_PLUS_LE(-(x0[1], 1), x1[1])
1464_0_PLUS_LE(x0[2], x1[2]) → COND_1464_0_PLUS_LE1(>(x1[2], 0), x0[2], x1[2])

There are no usable rules.

(9) Complex Obligation (AND)

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

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

(0) -> (1), if (x1[0] <= 0 && x0[0] > 0 ∧x0[0] →^* x0[1]∧x1[0] →^* x1[1])

(1) -> (2), if (x0[1] - 1 →^* x0[2]∧x1[1] →^* x1[2])

(11) IDependencyGraphProof (EQUIVALENT transformation)

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

(12) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

The ITRS R consists of the following rules:
1493_1_plus_InvokeMethod(1481_0_plus_Return, 0) → 1517_0_plus_Return(x1, x2)
1502_1_plus_InvokeMethod(1481_0_plus_Return, 0) → 1481_0_plus_Return
1493_1_plus_InvokeMethod(1774_0_plus_Return(x2), x1) → Cond_1493_1_plus_InvokeMethod(x2 > 0, 1774_0_plus_Return(x2), x1)
Cond_1493_1_plus_InvokeMethod(TRUE, 1774_0_plus_Return(x2), x1) → 1774_0_plus_Return(1 + x2)
1493_1_plus_InvokeMethod(1517_0_plus_Return(x0, x1), x1) → 1774_0_plus_Return(2)
1493_1_plus_InvokeMethod(1774_0_plus_Return(x0), 0) → Cond_1493_1_plus_InvokeMethod2(x0 > 0, 1774_0_plus_Return(x0), 0)
Cond_1493_1_plus_InvokeMethod2(TRUE, 1774_0_plus_Return(x0), 0) → 1774_0_plus_Return(1 + x0)
1493_1_plus_InvokeMethod(1481_0_plus_Return, 0) → 1774_0_plus_Return(2)
1502_1_plus_InvokeMethod(1774_0_plus_Return(x0), x2) → Cond_1493_1_plus_InvokeMethod(x0 > 0, 1774_0_plus_Return(x0), x2)
1502_1_plus_InvokeMethod(1481_0_plus_Return, x2) → 1774_0_plus_Return(2)

The integer pair graph contains the following rules and edges:
(1): COND_1464_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1464_0_PLUS_LE(x0[1] - 1, x1[1])
(0): 1464_0_PLUS_LE(x0[0], x1[0]) → COND_1464_0_PLUS_LE(x1[0] <= 0 && x0[0] > 0, x0[0], x1[0])

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

(0) -> (1), if (x1[0] <= 0 && x0[0] > 0 ∧x0[0] →^* x0[1]∧x1[0] →^* x1[1])

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

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_1464_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1464_0_PLUS_LE(x0[1] - 1, x1[1])
(0): 1464_0_PLUS_LE(x0[0], x1[0]) → COND_1464_0_PLUS_LE(x1[0] <= 0 && x0[0] > 0, x0[0], x1[0])

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

(0) -> (1), if (x1[0] <= 0 && x0[0] > 0 ∧x0[0] →^* x0[1]∧x1[0] →^* x1[1])

(15) 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.IdpCand1ShapeHeuristic@8c1bb13 Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair COND_1464_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1464_0_PLUS_LE(-(x0[1], 1), x1[1]) the following chains were created:

We consider the chain COND_1464_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1464_0_PLUS_LE(-(x0[1], 1), x1[1]) which results in the following constraint:
(1)    (COND_1464_0_PLUS_LE(TRUE, x0[1], x1[1])≥NonInfC∧COND_1464_0_PLUS_LE(TRUE, x0[1], x1[1])≥1464_0_PLUS_LE(-(x0[1], 1), x1[1])∧(U^Increasing(1464_0_PLUS_LE(-(x0[1], 1), x1[1])), ≥))

We simplified constraint (1) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(2)    ((U^Increasing(1464_0_PLUS_LE(-(x0[1], 1), x1[1])), ≥)∧[bni_10] = 0∧[(-1)bso_11] ≥ 0)

We simplified constraint (2) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(3)    ((U^Increasing(1464_0_PLUS_LE(-(x0[1], 1), x1[1])), ≥)∧[bni_10] = 0∧[(-1)bso_11] ≥ 0)

We simplified constraint (3) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(4)    ((U^Increasing(1464_0_PLUS_LE(-(x0[1], 1), x1[1])), ≥)∧[bni_10] = 0∧[(-1)bso_11] ≥ 0)

We simplified constraint (4) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(5)    ((U^Increasing(1464_0_PLUS_LE(-(x0[1], 1), x1[1])), ≥)∧[bni_10] = 0∧0 = 0∧0 = 0∧[(-1)bso_11] ≥ 0)

For Pair 1464_0_PLUS_LE(x0[0], x1[0]) → COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0]) the following chains were created:

We consider the chain 1464_0_PLUS_LE(x0[0], x1[0]) → COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0]), COND_1464_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1464_0_PLUS_LE(-(x0[1], 1), x1[1]) which results in the following constraint:
(6)    (&&(<=(x1[0], 0), >(x0[0], 0))=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1] ⇒ 1464_0_PLUS_LE(x0[0], x1[0])≥NonInfC∧1464_0_PLUS_LE(x0[0], x1[0])≥COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])∧(U^Increasing(COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])), ≥))

We simplified constraint (6) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
(7)    (<=(x1[0], 0)=TRUE∧>(x0[0], 0)=TRUE ⇒ 1464_0_PLUS_LE(x0[0], x1[0])≥NonInfC∧1464_0_PLUS_LE(x0[0], x1[0])≥COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])∧(U^Increasing(COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    ([-1]x1[0] ≥ 0∧x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])), ≥)∧[bni_12 + (-1)Bound*bni_12] + [(2)bni_12]x0[0] + [(-1)bni_12]x1[0] ≥ 0∧[2 + (-1)bso_13] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    ([-1]x1[0] ≥ 0∧x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])), ≥)∧[bni_12 + (-1)Bound*bni_12] + [(2)bni_12]x0[0] + [(-1)bni_12]x1[0] ≥ 0∧[2 + (-1)bso_13] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    ([-1]x1[0] ≥ 0∧x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])), ≥)∧[bni_12 + (-1)Bound*bni_12] + [(2)bni_12]x0[0] + [(-1)bni_12]x1[0] ≥ 0∧[2 + (-1)bso_13] ≥ 0)

We simplified constraint (10) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(11)    (x1[0] ≥ 0∧x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])), ≥)∧[bni_12 + (-1)Bound*bni_12] + [(2)bni_12]x0[0] + [bni_12]x1[0] ≥ 0∧[2 + (-1)bso_13] ≥ 0)

We simplified constraint (11) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(12)    (x1[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])), ≥)∧[(3)bni_12 + (-1)Bound*bni_12] + [(2)bni_12]x0[0] + [bni_12]x1[0] ≥ 0∧[2 + (-1)bso_13] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

COND_1464_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1464_0_PLUS_LE(-(x0[1], 1), x1[1])
- ((U^Increasing(1464_0_PLUS_LE(-(x0[1], 1), x1[1])), ≥)∧[bni_10] = 0∧0 = 0∧0 = 0∧[(-1)bso_11] ≥ 0)
1464_0_PLUS_LE(x0[0], x1[0]) → COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])
- (x1[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])), ≥)∧[(3)bni_12 + (-1)Bound*bni_12] + [(2)bni_12]x0[0] + [bni_12]x1[0] ≥ 0∧[2 + (-1)bso_13] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(COND_1464_0_PLUS_LE(x₁, x₂, x₃)) = [-1] + [-1]x₃ + [2]x₂
POL(1464_0_PLUS_LE(x₁, x₂)) = [1] + [2]x₁ + [-1]x₂
POL(-(x₁, x₂)) = x₁ + [-1]x₂
POL(1) = [1]
POL(&&(x₁, x₂)) = [-1]
POL(<=(x₁, x₂)) = [-1]
POL(0) = 0
POL(>(x₁, x₂)) = [-1]

The following pairs are in P_>:

1464_0_PLUS_LE(x0[0], x1[0]) → COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])

The following pairs are in P_bound:

1464_0_PLUS_LE(x0[0], x1[0]) → COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])

The following pairs are in P_≥:

COND_1464_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1464_0_PLUS_LE(-(x0[1], 1), x1[1])

There are no usable rules.

(16) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_1464_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1464_0_PLUS_LE(x0[1] - 1, x1[1])

The set Q consists of the following terms:
1493_1_plus_InvokeMethod(1481_0_plus_Return, 0)
1493_1_plus_InvokeMethod(1774_0_plus_Return(x0), x1)
Cond_1493_1_plus_InvokeMethod(TRUE, 1774_0_plus_Return(x0), x1)
1493_1_plus_InvokeMethod(1517_0_plus_Return(x0, x1), x1)
Cond_1493_1_plus_InvokeMethod2(TRUE, 1774_0_plus_Return(x0), 0)
1502_1_plus_InvokeMethod(1774_0_plus_Return(x0), x1)
1502_1_plus_InvokeMethod(1481_0_plus_Return, x0)

(17) IDependencyGraphProof (EQUIVALENT transformation)

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

(18) TRUE

(19) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

The ITRS R consists of the following rules:
1493_1_plus_InvokeMethod(1481_0_plus_Return, 0) → 1517_0_plus_Return(x1, x2)
1502_1_plus_InvokeMethod(1481_0_plus_Return, 0) → 1481_0_plus_Return
1493_1_plus_InvokeMethod(1774_0_plus_Return(x2), x1) → Cond_1493_1_plus_InvokeMethod(x2 > 0, 1774_0_plus_Return(x2), x1)
Cond_1493_1_plus_InvokeMethod(TRUE, 1774_0_plus_Return(x2), x1) → 1774_0_plus_Return(1 + x2)
1493_1_plus_InvokeMethod(1517_0_plus_Return(x0, x1), x1) → 1774_0_plus_Return(2)
1493_1_plus_InvokeMethod(1774_0_plus_Return(x0), 0) → Cond_1493_1_plus_InvokeMethod2(x0 > 0, 1774_0_plus_Return(x0), 0)
Cond_1493_1_plus_InvokeMethod2(TRUE, 1774_0_plus_Return(x0), 0) → 1774_0_plus_Return(1 + x0)
1493_1_plus_InvokeMethod(1481_0_plus_Return, 0) → 1774_0_plus_Return(2)
1502_1_plus_InvokeMethod(1774_0_plus_Return(x0), x2) → Cond_1493_1_plus_InvokeMethod(x0 > 0, 1774_0_plus_Return(x0), x2)
1502_1_plus_InvokeMethod(1481_0_plus_Return, x2) → 1774_0_plus_Return(2)

The integer pair graph contains the following rules and edges:
(0): 1464_0_PLUS_LE(x0[0], x1[0]) → COND_1464_0_PLUS_LE(x1[0] <= 0 && x0[0] > 0, x0[0], x1[0])
(1): COND_1464_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1464_0_PLUS_LE(x0[1] - 1, x1[1])
(3): COND_1464_0_PLUS_LE1(TRUE, x0[3], x1[3]) → 1464_0_PLUS_LE(x0[3], x1[3] - 1)

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

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

(0) -> (1), if (x1[0] <= 0 && x0[0] > 0 ∧x0[0] →^* x0[1]∧x1[0] →^* x1[1])

(20) IDependencyGraphProof (EQUIVALENT transformation)

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

(21) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

The ITRS R consists of the following rules:
1493_1_plus_InvokeMethod(1481_0_plus_Return, 0) → 1517_0_plus_Return(x1, x2)
1502_1_plus_InvokeMethod(1481_0_plus_Return, 0) → 1481_0_plus_Return
1493_1_plus_InvokeMethod(1774_0_plus_Return(x2), x1) → Cond_1493_1_plus_InvokeMethod(x2 > 0, 1774_0_plus_Return(x2), x1)
Cond_1493_1_plus_InvokeMethod(TRUE, 1774_0_plus_Return(x2), x1) → 1774_0_plus_Return(1 + x2)
1493_1_plus_InvokeMethod(1517_0_plus_Return(x0, x1), x1) → 1774_0_plus_Return(2)
1493_1_plus_InvokeMethod(1774_0_plus_Return(x0), 0) → Cond_1493_1_plus_InvokeMethod2(x0 > 0, 1774_0_plus_Return(x0), 0)
Cond_1493_1_plus_InvokeMethod2(TRUE, 1774_0_plus_Return(x0), 0) → 1774_0_plus_Return(1 + x0)
1493_1_plus_InvokeMethod(1481_0_plus_Return, 0) → 1774_0_plus_Return(2)
1502_1_plus_InvokeMethod(1774_0_plus_Return(x0), x2) → Cond_1493_1_plus_InvokeMethod(x0 > 0, 1774_0_plus_Return(x0), x2)
1502_1_plus_InvokeMethod(1481_0_plus_Return, x2) → 1774_0_plus_Return(2)

The integer pair graph contains the following rules and edges:
(1): COND_1464_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1464_0_PLUS_LE(x0[1] - 1, x1[1])
(0): 1464_0_PLUS_LE(x0[0], x1[0]) → COND_1464_0_PLUS_LE(x1[0] <= 0 && x0[0] > 0, x0[0], x1[0])

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

(0) -> (1), if (x1[0] <= 0 && x0[0] > 0 ∧x0[0] →^* x0[1]∧x1[0] →^* x1[1])

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

(23) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

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

(0) -> (1), if (x1[0] <= 0 && x0[0] > 0 ∧x0[0] →^* x0[1]∧x1[0] →^* x1[1])

(24) 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.IdpCand1ShapeHeuristic@8c1bb13 Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair COND_1464_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1464_0_PLUS_LE(-(x0[1], 1), x1[1]) the following chains were created:

We consider the chain COND_1464_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1464_0_PLUS_LE(-(x0[1], 1), x1[1]) which results in the following constraint:
(1)    (COND_1464_0_PLUS_LE(TRUE, x0[1], x1[1])≥NonInfC∧COND_1464_0_PLUS_LE(TRUE, x0[1], x1[1])≥1464_0_PLUS_LE(-(x0[1], 1), x1[1])∧(U^Increasing(1464_0_PLUS_LE(-(x0[1], 1), x1[1])), ≥))

We simplified constraint (1) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(2)    ((U^Increasing(1464_0_PLUS_LE(-(x0[1], 1), x1[1])), ≥)∧[bni_8] = 0∧[1 + (-1)bso_9] ≥ 0)

We simplified constraint (2) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(3)    ((U^Increasing(1464_0_PLUS_LE(-(x0[1], 1), x1[1])), ≥)∧[bni_8] = 0∧[1 + (-1)bso_9] ≥ 0)

We simplified constraint (3) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(4)    ((U^Increasing(1464_0_PLUS_LE(-(x0[1], 1), x1[1])), ≥)∧[bni_8] = 0∧[1 + (-1)bso_9] ≥ 0)

We simplified constraint (4) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(5)    ((U^Increasing(1464_0_PLUS_LE(-(x0[1], 1), x1[1])), ≥)∧[bni_8] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_9] ≥ 0)

For Pair 1464_0_PLUS_LE(x0[0], x1[0]) → COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0]) the following chains were created:

We consider the chain 1464_0_PLUS_LE(x0[0], x1[0]) → COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0]), COND_1464_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1464_0_PLUS_LE(-(x0[1], 1), x1[1]) which results in the following constraint:
(6)    (&&(<=(x1[0], 0), >(x0[0], 0))=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1] ⇒ 1464_0_PLUS_LE(x0[0], x1[0])≥NonInfC∧1464_0_PLUS_LE(x0[0], x1[0])≥COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])∧(U^Increasing(COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])), ≥))

We simplified constraint (6) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
(7)    (<=(x1[0], 0)=TRUE∧>(x0[0], 0)=TRUE ⇒ 1464_0_PLUS_LE(x0[0], x1[0])≥NonInfC∧1464_0_PLUS_LE(x0[0], x1[0])≥COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])∧(U^Increasing(COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    ([-1]x1[0] ≥ 0∧x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])), ≥)∧[(-1)bni_10 + (-1)Bound*bni_10] + [bni_10]x0[0] + [(-1)bni_10]x1[0] ≥ 0∧[(-1)bso_11] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    ([-1]x1[0] ≥ 0∧x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])), ≥)∧[(-1)bni_10 + (-1)Bound*bni_10] + [bni_10]x0[0] + [(-1)bni_10]x1[0] ≥ 0∧[(-1)bso_11] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    ([-1]x1[0] ≥ 0∧x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])), ≥)∧[(-1)bni_10 + (-1)Bound*bni_10] + [bni_10]x0[0] + [(-1)bni_10]x1[0] ≥ 0∧[(-1)bso_11] ≥ 0)

We simplified constraint (10) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(11)    (x1[0] ≥ 0∧x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])), ≥)∧[(-1)bni_10 + (-1)Bound*bni_10] + [bni_10]x0[0] + [bni_10]x1[0] ≥ 0∧[(-1)bso_11] ≥ 0)

We simplified constraint (11) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(12)    (x1[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_10] + [bni_10]x0[0] + [bni_10]x1[0] ≥ 0∧[(-1)bso_11] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

COND_1464_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1464_0_PLUS_LE(-(x0[1], 1), x1[1])
- ((U^Increasing(1464_0_PLUS_LE(-(x0[1], 1), x1[1])), ≥)∧[bni_8] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_9] ≥ 0)
1464_0_PLUS_LE(x0[0], x1[0]) → COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])
- (x1[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_10] + [bni_10]x0[0] + [bni_10]x1[0] ≥ 0∧[(-1)bso_11] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(COND_1464_0_PLUS_LE(x₁, x₂, x₃)) = [-1] + [-1]x₃ + x₂
POL(1464_0_PLUS_LE(x₁, x₂)) = [-1] + x₁ + [-1]x₂
POL(-(x₁, x₂)) = x₁ + [-1]x₂
POL(1) = [1]
POL(&&(x₁, x₂)) = [1]
POL(<=(x₁, x₂)) = [-1]
POL(0) = 0
POL(>(x₁, x₂)) = [-1]

The following pairs are in P_>:

COND_1464_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1464_0_PLUS_LE(-(x0[1], 1), x1[1])

The following pairs are in P_bound:

1464_0_PLUS_LE(x0[0], x1[0]) → COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])

The following pairs are in P_≥:

1464_0_PLUS_LE(x0[0], x1[0]) → COND_1464_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])

There are no usable rules.

(25) Complex Obligation (AND)

(26) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 1464_0_PLUS_LE(x0[0], x1[0]) → COND_1464_0_PLUS_LE(x1[0] <= 0 && x0[0] > 0, x0[0], x1[0])

The set Q consists of the following terms:
1493_1_plus_InvokeMethod(1481_0_plus_Return, 0)
1493_1_plus_InvokeMethod(1774_0_plus_Return(x0), x1)
Cond_1493_1_plus_InvokeMethod(TRUE, 1774_0_plus_Return(x0), x1)
1493_1_plus_InvokeMethod(1517_0_plus_Return(x0, x1), x1)
Cond_1493_1_plus_InvokeMethod2(TRUE, 1774_0_plus_Return(x0), 0)
1502_1_plus_InvokeMethod(1774_0_plus_Return(x0), x1)
1502_1_plus_InvokeMethod(1481_0_plus_Return, x0)

(27) IDependencyGraphProof (EQUIVALENT transformation)

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

(28) TRUE

(29) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

(30) IDependencyGraphProof (EQUIVALENT transformation)

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

(31) TRUE

(32) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: TimesPlusUserDef.times(II)I
SCC calls the following helper methods: TimesPlusUserDef.times(II)I, TimesPlusUserDef.plus(II)I
Performed SCC analyses: UsedFieldsAnalysis

(33) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 12 rules for P and 105 rules for R.

P rules:
259_0_times_NE(EOS(STATIC_259), i18, i41, i41) → 266_0_times_NE(EOS(STATIC_266), i18, i41, i41)
266_0_times_NE(EOS(STATIC_266), i18, i41, i41) → 270_0_times_Load(EOS(STATIC_270), i18, i41) | >(i41, 0)
270_0_times_Load(EOS(STATIC_270), i18, i41) → 284_0_times_LE(EOS(STATIC_284), i18, i41, i41)
284_0_times_LE(EOS(STATIC_284), i18, i41, i41) → 299_0_times_Load(EOS(STATIC_299), i18, i41) | >(i41, 0)
299_0_times_Load(EOS(STATIC_299), i18, i41) → 309_0_times_Load(EOS(STATIC_309), i18, i41, i18)
309_0_times_Load(EOS(STATIC_309), i18, i41, i18) → 327_0_times_ConstantStackPush(EOS(STATIC_327), i18, i18, i41)
327_0_times_ConstantStackPush(EOS(STATIC_327), i18, i18, i41) → 337_0_times_IntArithmetic(EOS(STATIC_337), i18, i18, i41, 1)
337_0_times_IntArithmetic(EOS(STATIC_337), i18, i18, i41, matching1) → 347_0_times_InvokeMethod(EOS(STATIC_347), i18, i18, -(i41, 1)) | &&(>(i41, 0), =(matching1, 1))
347_0_times_InvokeMethod(EOS(STATIC_347), i18, i18, i50) → 357_1_times_InvokeMethod(357_0_times_Load(EOS(STATIC_357), i18, i50), i18, i18, i50)
357_0_times_Load(EOS(STATIC_357), i18, i50) → 365_0_times_Load(EOS(STATIC_365), i18, i50)
365_0_times_Load(EOS(STATIC_365), i18, i50) → 249_0_times_Load(EOS(STATIC_249), i18, i50)
249_0_times_Load(EOS(STATIC_249), i18, i37) → 259_0_times_NE(EOS(STATIC_259), i18, i37, i37)
R rules:
1460_0_plus_Load(EOS(STATIC_1460), i638, i637) → 1463_0_plus_Load(EOS(STATIC_1463), i638, i637)
1496_0_plus_Load(EOS(STATIC_1496), i669) → 1463_0_plus_Load(EOS(STATIC_1463), i669, i679)
1507_0_plus_Load(EOS(STATIC_1507), i673) → 1463_0_plus_Load(EOS(STATIC_1463), i682, i673)
259_0_times_NE(EOS(STATIC_259), i18, matching1, matching2) → 267_0_times_NE(EOS(STATIC_267), i18, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
267_0_times_NE(EOS(STATIC_267), i18, matching1, matching2) → 272_0_times_ConstantStackPush(EOS(STATIC_272), i18, 0) | &&(=(matching1, 0), =(matching2, 0))
272_0_times_ConstantStackPush(EOS(STATIC_272), i18, matching1) → 286_0_times_Return(EOS(STATIC_286), i18, 0, 0) | =(matching1, 0)
357_1_times_InvokeMethod(286_0_times_Return(EOS(STATIC_286), i56, matching1, matching2), i56, i56, matching3) → 384_0_times_Return(EOS(STATIC_384), i56, i56, 0, i56, 0, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
357_1_times_InvokeMethod(1498_0_times_Return(EOS(STATIC_1498), matching1), matching2, matching3, i688) → 1512_0_times_Return(EOS(STATIC_1512), 0, 0, i688, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
357_1_times_InvokeMethod(1764_0_times_Return(EOS(STATIC_1764), i953), i1015, i1015, i1016) → 1792_0_times_Return(EOS(STATIC_1792), i1015, i1015, i1016, i953)
357_1_times_InvokeMethod(1829_0_times_Return(EOS(STATIC_1829), i1065), matching1, matching2, i1097) → 1845_0_times_Return(EOS(STATIC_1845), 0, 0, i1097, i1065) | &&(=(matching1, 0), =(matching2, 0))
384_0_times_Return(EOS(STATIC_384), i56, i56, matching1, i56, matching2, matching3) → 386_0_times_Load(EOS(STATIC_386), i56, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
386_0_times_Load(EOS(STATIC_386), i56, matching1) → 583_0_times_Load(EOS(STATIC_583), i56, 0) | =(matching1, 0)
557_0_times_Return(EOS(STATIC_557), i87, i87, i89, i88) → 850_0_times_Return(EOS(STATIC_850), i87, i87, i89, i88)
583_0_times_Load(EOS(STATIC_583), i87, i88) → 867_0_times_Load(EOS(STATIC_867), i87, i88)
850_0_times_Return(EOS(STATIC_850), i216, i216, i218, i217) → 1258_0_times_Return(EOS(STATIC_1258), i216, i216, i218, i217)
867_0_times_Load(EOS(STATIC_867), i216, i217) → 1279_0_times_Load(EOS(STATIC_1279), i216, i217)
1258_0_times_Return(EOS(STATIC_1258), i472, i472, i474, i473) → 1434_0_times_Return(EOS(STATIC_1434), i472, i472, i474, i473)
1279_0_times_Load(EOS(STATIC_1279), i472, i473) → 1453_0_times_Load(EOS(STATIC_1453), i472, i473)
1434_0_times_Return(EOS(STATIC_1434), i637, i637, i639, i638) → 1453_0_times_Load(EOS(STATIC_1453), i637, i638)
1453_0_times_Load(EOS(STATIC_1453), i637, i638) → 1456_0_times_InvokeMethod(EOS(STATIC_1456), i638, i637)
1456_0_times_InvokeMethod(EOS(STATIC_1456), i638, i637) → 1459_1_times_InvokeMethod(1459_0_plus_Load(EOS(STATIC_1459), i638, i637), i638, i637)
1459_0_plus_Load(EOS(STATIC_1459), i638, i637) → 1460_0_plus_Load(EOS(STATIC_1460), i638, i637)
1459_1_times_InvokeMethod(1481_0_plus_Return(EOS(STATIC_1481), matching1), i680, i681) → 1494_0_plus_Return(EOS(STATIC_1494), i680, i681, 0) | =(matching1, 0)
1459_1_times_InvokeMethod(1517_0_plus_Return(EOS(STATIC_1517), i700, i701, matching1), i700, i701) → 1528_0_plus_Return(EOS(STATIC_1528), i700, i701, i700, i701, 1) | =(matching1, 1)
1459_1_times_InvokeMethod(1527_0_plus_Return(EOS(STATIC_1527), matching1), i707, i708) → 1542_0_plus_Return(EOS(STATIC_1542), i707, i708, 1) | =(matching1, 1)
1459_1_times_InvokeMethod(1774_0_plus_Return(EOS(STATIC_1774), i1026, i1027, i1006), i1026, i1027) → 1809_0_plus_Return(EOS(STATIC_1809), i1026, i1027, i1026, i1027, i1006)
1459_1_times_InvokeMethod(1834_0_plus_Return(EOS(STATIC_1834), i1104, i1105, i1091), i1104, i1105) → 1854_0_plus_Return(EOS(STATIC_1854), i1104, i1105, i1104, i1105, i1091)
1459_1_times_InvokeMethod(1837_0_plus_Return(EOS(STATIC_1837), i1092), i1110, i1111) → 1859_0_plus_Return(EOS(STATIC_1859), i1110, i1111, i1092)
1494_0_plus_Return(EOS(STATIC_1494), i680, i681, matching1) → 1498_0_times_Return(EOS(STATIC_1498), 0) | =(matching1, 0)
1512_0_times_Return(EOS(STATIC_1512), matching1, matching2, i688, matching3) → 1434_0_times_Return(EOS(STATIC_1434), 0, 0, i688, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
1528_0_plus_Return(EOS(STATIC_1528), i700, i701, i700, i701, matching1) → 1569_0_plus_Return(EOS(STATIC_1569), i700, i701, i700, i701, 1) | =(matching1, 1)
1542_0_plus_Return(EOS(STATIC_1542), i707, i708, matching1) → 1613_0_plus_Return(EOS(STATIC_1613), i707, i708, 1) | =(matching1, 1)
1569_0_plus_Return(EOS(STATIC_1569), i735, i734, i735, i734, i736) → 1601_0_plus_Return(EOS(STATIC_1601), i735, i734, i735, i734, i736)
1601_0_plus_Return(EOS(STATIC_1601), i772, i771, i772, i771, i773) → 1666_0_plus_Return(EOS(STATIC_1666), i772, i771, i772, i771, i773)
1613_0_plus_Return(EOS(STATIC_1613), i790, i788, i789) → 1681_0_plus_Return(EOS(STATIC_1681), i790, i788, i789)
1666_0_plus_Return(EOS(STATIC_1666), i853, i852, i853, i852, i854) → 1738_0_plus_Return(EOS(STATIC_1738), i853, i852, i853, i852, i854)
1681_0_plus_Return(EOS(STATIC_1681), i879, i877, i878) → 1753_0_plus_Return(EOS(STATIC_1753), i879, i877, i878)
1738_0_plus_Return(EOS(STATIC_1738), i952, i951, i952, i951, i953) → 1764_0_times_Return(EOS(STATIC_1764), i953)
1753_0_plus_Return(EOS(STATIC_1753), i979, i977, i978) → 1819_0_plus_Return(EOS(STATIC_1819), i979, i977, i978)
1792_0_times_Return(EOS(STATIC_1792), i1015, i1015, i1016, i953) → 1434_0_times_Return(EOS(STATIC_1434), i1015, i1015, i1016, i953)
1809_0_plus_Return(EOS(STATIC_1809), i1026, i1027, i1026, i1027, i1006) → 1738_0_plus_Return(EOS(STATIC_1738), i1026, i1027, i1026, i1027, i1006)
1819_0_plus_Return(EOS(STATIC_1819), i1066, i1064, i1065) → 1829_0_times_Return(EOS(STATIC_1829), i1065)
1845_0_times_Return(EOS(STATIC_1845), matching1, matching2, i1097, i1065) → 1434_0_times_Return(EOS(STATIC_1434), 0, 0, i1097, i1065) | &&(=(matching1, 0), =(matching2, 0))
1854_0_plus_Return(EOS(STATIC_1854), i1104, i1105, i1104, i1105, i1091) → 1738_0_plus_Return(EOS(STATIC_1738), i1104, i1105, i1104, i1105, i1091)
1859_0_plus_Return(EOS(STATIC_1859), i1110, i1111, i1092) → 1819_0_plus_Return(EOS(STATIC_1819), i1110, i1111, i1092)
1463_0_plus_Load(EOS(STATIC_1463), i669, i670) → 1464_0_plus_LE(EOS(STATIC_1464), i669, i670, i670)
1464_0_plus_LE(EOS(STATIC_1464), i669, i673, i673) → 1466_0_plus_LE(EOS(STATIC_1466), i669, i673, i673)
1464_0_plus_LE(EOS(STATIC_1464), i669, i674, i674) → 1467_0_plus_LE(EOS(STATIC_1467), i669, i674, i674)
1466_0_plus_LE(EOS(STATIC_1466), i669, i673, i673) → 1469_0_plus_Load(EOS(STATIC_1469), i669, i673) | <=(i673, 0)
1467_0_plus_LE(EOS(STATIC_1467), i669, i674, i674) → 1470_0_plus_ConstantStackPush(EOS(STATIC_1470), i669, i674) | >(i674, 0)
1469_0_plus_Load(EOS(STATIC_1469), i669, i673) → 1471_0_plus_LE(EOS(STATIC_1471), i669, i673, i669)
1470_0_plus_ConstantStackPush(EOS(STATIC_1470), i669, i674) → 1473_0_plus_Load(EOS(STATIC_1473), i669, i674, 1)
1471_0_plus_LE(EOS(STATIC_1471), i677, i673, i677) → 1474_0_plus_LE(EOS(STATIC_1474), i677, i673, i677)
1471_0_plus_LE(EOS(STATIC_1471), i678, i673, i678) → 1475_0_plus_LE(EOS(STATIC_1475), i678, i673, i678)
1473_0_plus_Load(EOS(STATIC_1473), i669, i674, matching1) → 1476_0_plus_Load(EOS(STATIC_1476), i669, i674, 1, i669) | =(matching1, 1)
1474_0_plus_LE(EOS(STATIC_1474), i677, i673, i677) → 1477_0_plus_ConstantStackPush(EOS(STATIC_1477)) | <=(i677, 0)
1475_0_plus_LE(EOS(STATIC_1475), i678, i673, i678) → 1479_0_plus_ConstantStackPush(EOS(STATIC_1479), i678, i673) | >(i678, 0)
1476_0_plus_Load(EOS(STATIC_1476), i669, i674, matching1, i669) → 1480_0_plus_ConstantStackPush(EOS(STATIC_1480), i669, i674, 1, i669, i674) | =(matching1, 1)
1477_0_plus_ConstantStackPush(EOS(STATIC_1477)) → 1481_0_plus_Return(EOS(STATIC_1481), 0)
1479_0_plus_ConstantStackPush(EOS(STATIC_1479), i678, i673) → 1483_0_plus_Load(EOS(STATIC_1483), i678, i673, 1)
1480_0_plus_ConstantStackPush(EOS(STATIC_1480), i669, i674, matching1, i669, i674) → 1484_0_plus_IntArithmetic(EOS(STATIC_1484), i669, i674, 1, i669, i674, 1) | =(matching1, 1)
1483_0_plus_Load(EOS(STATIC_1483), i678, i673, matching1) → 1487_0_plus_ConstantStackPush(EOS(STATIC_1487), i673, 1, i678) | =(matching1, 1)
1484_0_plus_IntArithmetic(EOS(STATIC_1484), i669, i674, matching1, i669, i674, matching2) → 1488_0_plus_InvokeMethod(EOS(STATIC_1488), i669, i674, 1, i669) | &&(&&(>(i674, 0), =(matching1, 1)), =(matching2, 1))
1487_0_plus_ConstantStackPush(EOS(STATIC_1487), i673, matching1, i678) → 1491_0_plus_IntArithmetic(EOS(STATIC_1491), i673, 1, i678, 1) | =(matching1, 1)
1488_0_plus_InvokeMethod(EOS(STATIC_1488), i669, i674, matching1, i669) → 1493_1_plus_InvokeMethod(1493_0_plus_Load(EOS(STATIC_1493), i669), i669, i674, 1, i669) | =(matching1, 1)
1491_0_plus_IntArithmetic(EOS(STATIC_1491), i673, matching1, i678, matching2) → 1495_0_plus_Load(EOS(STATIC_1495), i673, 1) | &&(&&(>(i678, 0), =(matching1, 1)), =(matching2, 1))
1493_0_plus_Load(EOS(STATIC_1493), i669) → 1496_0_plus_Load(EOS(STATIC_1496), i669)
1493_1_plus_InvokeMethod(1481_0_plus_Return(EOS(STATIC_1481), matching1), i684, i674, matching2, i684) → 1509_0_plus_Return(EOS(STATIC_1509), i684, i674, 1, i684, 0, 0) | &&(=(matching1, 0), =(matching2, 1))
1493_1_plus_InvokeMethod(1517_0_plus_Return(EOS(STATIC_1517), i703, i704, matching1), i703, i674, matching2, i703) → 1529_0_plus_Return(EOS(STATIC_1529), i703, i674, 1, i703, i703, 1) | &&(=(matching1, 1), =(matching2, 1))
1493_1_plus_InvokeMethod(1527_0_plus_Return(EOS(STATIC_1527), matching1), i709, i674, matching2, i709) → 1543_0_plus_Return(EOS(STATIC_1543), i709, i674, 1, i709, 0, 1) | &&(=(matching1, 1), =(matching2, 1))
1493_1_plus_InvokeMethod(1774_0_plus_Return(EOS(STATIC_1774), i1029, i1030, i1006), i1029, i674, matching1, i1029) → 1811_0_plus_Return(EOS(STATIC_1811), i1029, i674, 1, i1029, i1029, i1006) | =(matching1, 1)
1493_1_plus_InvokeMethod(1834_0_plus_Return(EOS(STATIC_1834), i1107, i1108, i1091), i1107, i674, matching1, i1107) → 1856_0_plus_Return(EOS(STATIC_1856), i1107, i674, 1, i1107, i1107, i1091) | =(matching1, 1)
1493_1_plus_InvokeMethod(1837_0_plus_Return(EOS(STATIC_1837), i1092), i1113, i674, matching1, i1113) → 1861_0_plus_Return(EOS(STATIC_1861), i1113, i674, 1, i1113, 0, i1092) | =(matching1, 1)
1495_0_plus_Load(EOS(STATIC_1495), i673, matching1) → 1499_0_plus_InvokeMethod(EOS(STATIC_1499), 1, i673) | =(matching1, 1)
1499_0_plus_InvokeMethod(EOS(STATIC_1499), matching1, i673) → 1502_1_plus_InvokeMethod(1502_0_plus_Load(EOS(STATIC_1502), i673), 1, i673) | =(matching1, 1)
1502_0_plus_Load(EOS(STATIC_1502), i673) → 1507_0_plus_Load(EOS(STATIC_1507), i673)
1502_1_plus_InvokeMethod(1481_0_plus_Return(EOS(STATIC_1481), matching1), matching2, i699) → 1518_0_plus_Return(EOS(STATIC_1518), 1, 0, i699, 0) | &&(=(matching1, 0), =(matching2, 1))
1502_1_plus_InvokeMethod(1527_0_plus_Return(EOS(STATIC_1527), matching1), matching2, i712) → 1544_0_plus_Return(EOS(STATIC_1544), 1, i712, 1) | &&(=(matching1, 1), =(matching2, 1))
1502_1_plus_InvokeMethod(1837_0_plus_Return(EOS(STATIC_1837), i1092), matching1, i1116) → 1863_0_plus_Return(EOS(STATIC_1863), 1, i1116, i1092) | =(matching1, 1)
1509_0_plus_Return(EOS(STATIC_1509), i684, i674, matching1, i684, matching2, matching3) → 1513_0_plus_IntArithmetic(EOS(STATIC_1513), i684, i674, 1, 0) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
1513_0_plus_IntArithmetic(EOS(STATIC_1513), i684, i674, matching1, matching2) → 1517_0_plus_Return(EOS(STATIC_1517), i684, i674, 1) | &&(=(matching1, 1), =(matching2, 0))
1518_0_plus_Return(EOS(STATIC_1518), matching1, matching2, i699, matching3) → 1521_0_plus_IntArithmetic(EOS(STATIC_1521), 1, 0) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
1521_0_plus_IntArithmetic(EOS(STATIC_1521), matching1, matching2) → 1527_0_plus_Return(EOS(STATIC_1527), 1) | &&(=(matching1, 1), =(matching2, 0))
1529_0_plus_Return(EOS(STATIC_1529), i703, i674, matching1, i703, i703, matching2) → 1575_0_plus_Return(EOS(STATIC_1575), i703, i674, 1, i703, i703, 1) | &&(=(matching1, 1), =(matching2, 1))
1543_0_plus_Return(EOS(STATIC_1543), i709, i674, matching1, i709, matching2, matching3) → 1617_0_plus_Return(EOS(STATIC_1617), i709, i674, 1, i709, 0, 1) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 1))
1544_0_plus_Return(EOS(STATIC_1544), matching1, i712, matching2) → 1621_0_plus_Return(EOS(STATIC_1621), 1, i712, 1) | &&(=(matching1, 1), =(matching2, 1))
1575_0_plus_Return(EOS(STATIC_1575), i739, i674, matching1, i739, i739, i741) → 1607_0_plus_Return(EOS(STATIC_1607), i739, i674, 1, i739, i739, i741) | =(matching1, 1)
1607_0_plus_Return(EOS(STATIC_1607), i779, i674, matching1, i779, i779, i781) → 1671_0_plus_Return(EOS(STATIC_1671), i779, i674, 1, i779, i779, i781) | =(matching1, 1)
1617_0_plus_Return(EOS(STATIC_1617), i792, i674, matching1, i792, matching2, i793) → 1685_0_plus_Return(EOS(STATIC_1685), i792, i674, 1, i792, 0, i793) | &&(=(matching1, 1), =(matching2, 0))
1621_0_plus_Return(EOS(STATIC_1621), matching1, i797, i798) → 1692_0_plus_Return(EOS(STATIC_1692), 1, i797, i798) | =(matching1, 1)
1671_0_plus_Return(EOS(STATIC_1671), i860, i674, matching1, i860, i860, i862) → 1743_0_plus_Return(EOS(STATIC_1743), i860, i674, 1, i860, i860, i862) | =(matching1, 1)
1685_0_plus_Return(EOS(STATIC_1685), i884, i674, matching1, i884, matching2, i885) → 1757_0_plus_Return(EOS(STATIC_1757), i884, i674, 1, i884, 0, i885) | &&(=(matching1, 1), =(matching2, 0))
1692_0_plus_Return(EOS(STATIC_1692), matching1, i892, i893) → 1763_0_plus_Return(EOS(STATIC_1763), 1, i892, i893) | =(matching1, 1)
1743_0_plus_Return(EOS(STATIC_1743), i960, i674, matching1, i960, i960, i962) → 1767_0_plus_IntArithmetic(EOS(STATIC_1767), i960, i674, 1, i962) | =(matching1, 1)
1757_0_plus_Return(EOS(STATIC_1757), i984, i674, matching1, i984, matching2, i985) → 1823_0_plus_Return(EOS(STATIC_1823), i984, i674, 1, i984, 0, i985) | &&(=(matching1, 1), =(matching2, 0))
1763_0_plus_Return(EOS(STATIC_1763), matching1, i992, i993) → 1827_0_plus_Return(EOS(STATIC_1827), 1, i992, i993) | =(matching1, 1)
1767_0_plus_IntArithmetic(EOS(STATIC_1767), i960, i674, matching1, i962) → 1774_0_plus_Return(EOS(STATIC_1774), i960, i674, +(1, i962)) | &&(>(i962, 0), =(matching1, 1))
1811_0_plus_Return(EOS(STATIC_1811), i1029, i674, matching1, i1029, i1029, i1006) → 1743_0_plus_Return(EOS(STATIC_1743), i1029, i674, 1, i1029, i1029, i1006) | =(matching1, 1)
1823_0_plus_Return(EOS(STATIC_1823), i1071, i674, matching1, i1071, matching2, i1072) → 1830_0_plus_IntArithmetic(EOS(STATIC_1830), i1071, i674, 1, i1072) | &&(=(matching1, 1), =(matching2, 0))
1827_0_plus_Return(EOS(STATIC_1827), matching1, i1079, i1080) → 1831_0_plus_IntArithmetic(EOS(STATIC_1831), 1, i1080) | =(matching1, 1)
1830_0_plus_IntArithmetic(EOS(STATIC_1830), i1071, i674, matching1, i1072) → 1834_0_plus_Return(EOS(STATIC_1834), i1071, i674, +(1, i1072)) | &&(>(i1072, 0), =(matching1, 1))
1831_0_plus_IntArithmetic(EOS(STATIC_1831), matching1, i1080) → 1837_0_plus_Return(EOS(STATIC_1837), +(1, i1080)) | &&(>(i1080, 0), =(matching1, 1))
1856_0_plus_Return(EOS(STATIC_1856), i1107, i674, matching1, i1107, i1107, i1091) → 1743_0_plus_Return(EOS(STATIC_1743), i1107, i674, 1, i1107, i1107, i1091) | =(matching1, 1)
1861_0_plus_Return(EOS(STATIC_1861), i1113, i674, matching1, i1113, matching2, i1092) → 1823_0_plus_Return(EOS(STATIC_1823), i1113, i674, 1, i1113, 0, i1092) | &&(=(matching1, 1), =(matching2, 0))
1863_0_plus_Return(EOS(STATIC_1863), matching1, i1116, i1092) → 1827_0_plus_Return(EOS(STATIC_1827), 1, i1116, i1092) | =(matching1, 1)

Combined rules. Obtained 1 conditional rules for P and 23 conditional rules for R.

P rules:
259_0_times_NE(EOS(STATIC_259), x0, x1, x1) → 357_1_times_InvokeMethod(259_0_times_NE(EOS(STATIC_259), x0, -(x1, 1), -(x1, 1)), x0, x0, -(x1, 1)) | >(x1, 0)
R rules:
259_0_times_NE(EOS(STATIC_259), x0, 0, 0) → 286_0_times_Return(EOS(STATIC_286), x0, 0, 0)
357_1_times_InvokeMethod(286_0_times_Return(EOS(STATIC_286), x0, 0, 0), x0, x0, 0) → 1459_1_times_InvokeMethod(1464_0_plus_LE(EOS(STATIC_1464), 0, x0, x0), 0, x0)
357_1_times_InvokeMethod(1498_0_times_Return(EOS(STATIC_1498), 0), 0, 0, x3) → 1459_1_times_InvokeMethod(1464_0_plus_LE(EOS(STATIC_1464), 0, 0, 0), 0, 0)
357_1_times_InvokeMethod(1764_0_times_Return(EOS(STATIC_1764), x0), x1, x1, x2) → 1459_1_times_InvokeMethod(1464_0_plus_LE(EOS(STATIC_1464), x0, x1, x1), x0, x1)
357_1_times_InvokeMethod(1829_0_times_Return(EOS(STATIC_1829), x0), 0, 0, x3) → 1459_1_times_InvokeMethod(1464_0_plus_LE(EOS(STATIC_1464), x0, 0, 0), x0, 0)
1459_1_times_InvokeMethod(1481_0_plus_Return(EOS(STATIC_1481), 0), x1, x2) → 1498_0_times_Return(EOS(STATIC_1498), 0)
1459_1_times_InvokeMethod(1774_0_plus_Return(EOS(STATIC_1774), x0, x1, x2), x0, x1) → 1764_0_times_Return(EOS(STATIC_1764), x2)
1459_1_times_InvokeMethod(1834_0_plus_Return(EOS(STATIC_1834), x0, x1, x2), x0, x1) → 1764_0_times_Return(EOS(STATIC_1764), x2)
1459_1_times_InvokeMethod(1517_0_plus_Return(EOS(STATIC_1517), x0, x1, 1), x0, x1) → 1764_0_times_Return(EOS(STATIC_1764), 1)
1459_1_times_InvokeMethod(1837_0_plus_Return(EOS(STATIC_1837), x0), x1, x2) → 1829_0_times_Return(EOS(STATIC_1829), x0)
1459_1_times_InvokeMethod(1527_0_plus_Return(EOS(STATIC_1527), 1), x1, x2) → 1829_0_times_Return(EOS(STATIC_1829), 1)
1464_0_plus_LE(EOS(STATIC_1464), x0, x1, x1) → 1481_0_plus_Return(EOS(STATIC_1481), 0) | &&(<=(x1, 0), <=(x0, 0))
1464_0_plus_LE(EOS(STATIC_1464), x0, x1, x1) → 1493_1_plus_InvokeMethod(1464_0_plus_LE(EOS(STATIC_1464), x0, x2, x2), x0, x1, 1, x0) | >(x1, 0)
1464_0_plus_LE(EOS(STATIC_1464), x0, x1, x1) → 1502_1_plus_InvokeMethod(1464_0_plus_LE(EOS(STATIC_1464), x2, x1, x1), 1, x1) | &&(<=(x1, 0), >(x0, 0))
1493_1_plus_InvokeMethod(1481_0_plus_Return(EOS(STATIC_1481), 0), x1, x2, 1, x1) → 1517_0_plus_Return(EOS(STATIC_1517), x1, x2, 1)
1502_1_plus_InvokeMethod(1481_0_plus_Return(EOS(STATIC_1481), 0), 1, x2) → 1527_0_plus_Return(EOS(STATIC_1527), 1)
1493_1_plus_InvokeMethod(1774_0_plus_Return(EOS(STATIC_1774), x0, x1, x2), x0, x3, 1, x0) → 1774_0_plus_Return(EOS(STATIC_1774), x0, x3, +(1, x2)) | >(x2, 0)
1493_1_plus_InvokeMethod(1834_0_plus_Return(EOS(STATIC_1834), x0, x1, x2), x0, x3, 1, x0) → 1774_0_plus_Return(EOS(STATIC_1774), x0, x3, +(1, x2)) | >(x2, 0)
1493_1_plus_InvokeMethod(1517_0_plus_Return(EOS(STATIC_1517), x0, x1, 1), x0, x3, 1, x0) → 1774_0_plus_Return(EOS(STATIC_1774), x0, x3, 2)
1493_1_plus_InvokeMethod(1837_0_plus_Return(EOS(STATIC_1837), x0), x1, x2, 1, x1) → 1834_0_plus_Return(EOS(STATIC_1834), x1, x2, +(1, x0)) | >(x0, 0)
1493_1_plus_InvokeMethod(1527_0_plus_Return(EOS(STATIC_1527), 1), x1, x2, 1, x1) → 1834_0_plus_Return(EOS(STATIC_1834), x1, x2, 2)
1502_1_plus_InvokeMethod(1837_0_plus_Return(EOS(STATIC_1837), x0), 1, x2) → 1837_0_plus_Return(EOS(STATIC_1837), +(1, x0)) | >(x0, 0)
1502_1_plus_InvokeMethod(1527_0_plus_Return(EOS(STATIC_1527), 1), 1, x2) → 1837_0_plus_Return(EOS(STATIC_1837), 2)

Filtered ground terms:

259_0_times_NE(x1, x2, x3, x4) → 259_0_times_NE(x2, x3, x4)
Cond_259_0_times_NE(x1, x2, x3, x4, x5) → Cond_259_0_times_NE(x1, x3, x4, x5)
1837_0_plus_Return(x1, x2) → 1837_0_plus_Return(x2)
1502_1_plus_InvokeMethod(x1, x2, x3) → 1502_1_plus_InvokeMethod(x1, x3)
1527_0_plus_Return(x1, x2) → 1527_0_plus_Return
Cond_1502_1_plus_InvokeMethod(x1, x2, x3, x4) → Cond_1502_1_plus_InvokeMethod(x1, x2, x4)
1834_0_plus_Return(x1, x2, x3, x4) → 1834_0_plus_Return(x2, x3, x4)
1493_1_plus_InvokeMethod(x1, x2, x3, x4, x5) → 1493_1_plus_InvokeMethod(x1, x2, x3, x5)
Cond_1493_1_plus_InvokeMethod2(x1, x2, x3, x4, x5, x6) → Cond_1493_1_plus_InvokeMethod2(x1, x2, x3, x4, x6)
1774_0_plus_Return(x1, x2, x3, x4) → 1774_0_plus_Return(x2, x3, x4)
1517_0_plus_Return(x1, x2, x3, x4) → 1517_0_plus_Return(x2, x3)
Cond_1493_1_plus_InvokeMethod1(x1, x2, x3, x4, x5, x6) → Cond_1493_1_plus_InvokeMethod1(x1, x2, x3, x4, x6)
Cond_1493_1_plus_InvokeMethod(x1, x2, x3, x4, x5, x6) → Cond_1493_1_plus_InvokeMethod(x1, x2, x3, x4, x6)
1481_0_plus_Return(x1, x2) → 1481_0_plus_Return
1464_0_plus_LE(x1, x2, x3, x4) → 1464_0_plus_LE(x2, x3, x4)
Cond_1464_0_plus_LE2(x1, x2, x3, x4, x5, x6) → Cond_1464_0_plus_LE2(x1, x3, x4, x5, x6)
Cond_1464_0_plus_LE1(x1, x2, x3, x4, x5, x6) → Cond_1464_0_plus_LE1(x1, x3, x4, x5, x6)
Cond_1464_0_plus_LE(x1, x2, x3, x4, x5) → Cond_1464_0_plus_LE(x1, x3, x4, x5)
1829_0_times_Return(x1, x2) → 1829_0_times_Return(x2)
1764_0_times_Return(x1, x2) → 1764_0_times_Return(x2)
1498_0_times_Return(x1, x2) → 1498_0_times_Return
286_0_times_Return(x1, x2, x3, x4) → 286_0_times_Return(x2)

Filtered duplicate args:

259_0_times_NE(x1, x2, x3) → 259_0_times_NE(x1, x3)
Cond_259_0_times_NE(x1, x2, x3, x4) → Cond_259_0_times_NE(x1, x2, x4)
357_1_times_InvokeMethod(x1, x2, x3, x4) → 357_1_times_InvokeMethod(x1, x3, x4)
1464_0_plus_LE(x1, x2, x3) → 1464_0_plus_LE(x1, x3)
Cond_1464_0_plus_LE(x1, x2, x3, x4) → Cond_1464_0_plus_LE(x1, x2, x4)
Cond_1464_0_plus_LE1(x1, x2, x3, x4, x5) → Cond_1464_0_plus_LE1(x1, x2, x4, x5)
1493_1_plus_InvokeMethod(x1, x2, x3, x4) → 1493_1_plus_InvokeMethod(x1, x3, x4)
Cond_1464_0_plus_LE2(x1, x2, x3, x4, x5) → Cond_1464_0_plus_LE2(x1, x2, x4, x5)
Cond_1493_1_plus_InvokeMethod(x1, x2, x3, x4, x5) → Cond_1493_1_plus_InvokeMethod(x1, x2, x4)
Cond_1493_1_plus_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_1493_1_plus_InvokeMethod1(x1, x2, x4)
Cond_1493_1_plus_InvokeMethod2(x1, x2, x3, x4, x5) → Cond_1493_1_plus_InvokeMethod2(x1, x2, x4, x5)

Filtered unneeded arguments:

1459_1_times_InvokeMethod(x1, x2, x3) → 1459_1_times_InvokeMethod(x1)
Cond_1464_0_plus_LE(x1, x2, x3) → Cond_1464_0_plus_LE(x1)
Cond_1464_0_plus_LE1(x1, x2, x3, x4) → Cond_1464_0_plus_LE1(x1, x2, x4)
1493_1_plus_InvokeMethod(x1, x2, x3) → 1493_1_plus_InvokeMethod(x1)
Cond_1464_0_plus_LE2(x1, x2, x3, x4) → Cond_1464_0_plus_LE2(x1, x3, x4)
1502_1_plus_InvokeMethod(x1, x2) → 1502_1_plus_InvokeMethod(x1)
Cond_1493_1_plus_InvokeMethod(x1, x2, x3) → Cond_1493_1_plus_InvokeMethod(x1, x2)
Cond_1493_1_plus_InvokeMethod1(x1, x2, x3) → Cond_1493_1_plus_InvokeMethod1(x1, x2)
Cond_1493_1_plus_InvokeMethod2(x1, x2, x3, x4) → Cond_1493_1_plus_InvokeMethod2(x1, x2)
Cond_1502_1_plus_InvokeMethod(x1, x2, x3) → Cond_1502_1_plus_InvokeMethod(x1, x2)
1774_0_plus_Return(x1, x2, x3) → 1774_0_plus_Return(x3)
1834_0_plus_Return(x1, x2, x3) → 1834_0_plus_Return(x3)

Combined rules. Obtained 1 conditional rules for P and 23 conditional rules for R.

P rules:
259_0_times_NE(x0, x1) → 357_1_times_InvokeMethod(259_0_times_NE(x0, -(x1, 1)), x0, -(x1, 1)) | >(x1, 0)
R rules:
259_0_times_NE(x0, 0) → 286_0_times_Return(x0)
357_1_times_InvokeMethod(286_0_times_Return(x0), x0, 0) → 1459_1_times_InvokeMethod(1464_0_plus_LE(0, x0))
357_1_times_InvokeMethod(1498_0_times_Return, 0, x3) → 1459_1_times_InvokeMethod(1464_0_plus_LE(0, 0))
357_1_times_InvokeMethod(1764_0_times_Return(x0), x1, x2) → 1459_1_times_InvokeMethod(1464_0_plus_LE(x0, x1))
357_1_times_InvokeMethod(1829_0_times_Return(x0), 0, x3) → 1459_1_times_InvokeMethod(1464_0_plus_LE(x0, 0))
1459_1_times_InvokeMethod(1481_0_plus_Return) → 1498_0_times_Return
1459_1_times_InvokeMethod(1774_0_plus_Return(x2)) → 1764_0_times_Return(x2)
1459_1_times_InvokeMethod(1834_0_plus_Return(x2)) → 1764_0_times_Return(x2)
1459_1_times_InvokeMethod(1517_0_plus_Return(x0, x1)) → 1764_0_times_Return(1)
1459_1_times_InvokeMethod(1837_0_plus_Return(x0)) → 1829_0_times_Return(x0)
1459_1_times_InvokeMethod(1527_0_plus_Return) → 1829_0_times_Return(1)
1464_0_plus_LE(x0, x1) → 1481_0_plus_Return | &&(<=(x1, 0), <=(x0, 0))
1464_0_plus_LE(x0, x1) → 1493_1_plus_InvokeMethod(1464_0_plus_LE(x0, x2)) | >(x1, 0)
1464_0_plus_LE(x0, x1) → 1502_1_plus_InvokeMethod(1464_0_plus_LE(x2, x1)) | &&(<=(x1, 0), >(x0, 0))
1493_1_plus_InvokeMethod(1481_0_plus_Return) → 1517_0_plus_Return(x1, x2)
1502_1_plus_InvokeMethod(1481_0_plus_Return) → 1527_0_plus_Return
1493_1_plus_InvokeMethod(1774_0_plus_Return(x2)) → 1774_0_plus_Return(+(1, x2)) | >(x2, 0)
1493_1_plus_InvokeMethod(1834_0_plus_Return(x2)) → 1774_0_plus_Return(+(1, x2)) | >(x2, 0)
1493_1_plus_InvokeMethod(1517_0_plus_Return(x0, x1)) → 1774_0_plus_Return(2)
1493_1_plus_InvokeMethod(1837_0_plus_Return(x0)) → 1834_0_plus_Return(+(1, x0)) | >(x0, 0)
1493_1_plus_InvokeMethod(1527_0_plus_Return) → 1834_0_plus_Return(2)
1502_1_plus_InvokeMethod(1837_0_plus_Return(x0)) → 1837_0_plus_Return(+(1, x0)) | >(x0, 0)
1502_1_plus_InvokeMethod(1527_0_plus_Return) → 1837_0_plus_Return(2)

Performed bisimulation on rules. Used the following equivalence classes: {[Cond_1493_1_plus_InvokeMethod_2, Cond_1493_1_plus_InvokeMethod1_2, Cond_1493_1_plus_InvokeMethod2_2, Cond_1502_1_plus_InvokeMethod_2]=Cond_1493_1_plus_InvokeMethod_2, [1774_0_plus_Return_1, 1834_0_plus_Return_1, 1837_0_plus_Return_1]=1774_0_plus_Return_1, [1764_0_times_Return_1, 1829_0_times_Return_1]=1764_0_times_Return_1, [1498_0_times_Return, 1481_0_plus_Return, 1527_0_plus_Return]=1498_0_times_Return}

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

P rules:
259_0_TIMES_NE(x0, x1) → COND_259_0_TIMES_NE(>(x1, 0), x0, x1)
COND_259_0_TIMES_NE(TRUE, x0, x1) → 259_0_TIMES_NE(x0, -(x1, 1))
R rules:
259_0_times_NE(x0, 0) → 286_0_times_Return(x0)
357_1_times_InvokeMethod(286_0_times_Return(x0), x0, 0) → 1459_1_times_InvokeMethod(1464_0_plus_LE(0, x0))
357_1_times_InvokeMethod(1498_0_times_Return, 0, x3) → 1459_1_times_InvokeMethod(1464_0_plus_LE(0, 0))
357_1_times_InvokeMethod(1764_0_times_Return(x0), x1, x2) → 1459_1_times_InvokeMethod(1464_0_plus_LE(x0, x1))
357_1_times_InvokeMethod(1764_0_times_Return(x0), 0, x3) → 1459_1_times_InvokeMethod(1464_0_plus_LE(x0, 0))
1459_1_times_InvokeMethod(1498_0_times_Return) → 1498_0_times_Return
1459_1_times_InvokeMethod(1774_0_plus_Return(x2)) → 1764_0_times_Return(x2)
1459_1_times_InvokeMethod(1517_0_plus_Return(x0, x1)) → 1764_0_times_Return(1)
1459_1_times_InvokeMethod(1498_0_times_Return) → 1764_0_times_Return(1)
1464_0_plus_LE(x0, x1) → Cond_1464_0_plus_LE(&&(<=(x1, 0), <=(x0, 0)), x0, x1)
Cond_1464_0_plus_LE(TRUE, x0, x1) → 1498_0_times_Return
1464_0_plus_LE(x0, x1) → Cond_1464_0_plus_LE1(>(x1, 0), x0, x1, x2)
Cond_1464_0_plus_LE1(TRUE, x0, x1, x2) → 1493_1_plus_InvokeMethod(1464_0_plus_LE(x0, x2))
1464_0_plus_LE(x0, x1) → Cond_1464_0_plus_LE2(&&(<=(x1, 0), >(x0, 0)), x0, x1, x2)
Cond_1464_0_plus_LE2(TRUE, x0, x1, x2) → 1502_1_plus_InvokeMethod(1464_0_plus_LE(x2, x1))
1493_1_plus_InvokeMethod(1498_0_times_Return) → 1517_0_plus_Return(x1, x2)
1502_1_plus_InvokeMethod(1498_0_times_Return) → 1498_0_times_Return
1493_1_plus_InvokeMethod(1774_0_plus_Return(x2)) → Cond_1493_1_plus_InvokeMethod(>(x2, 0), 1774_0_plus_Return(x2))
Cond_1493_1_plus_InvokeMethod(TRUE, 1774_0_plus_Return(x2)) → 1774_0_plus_Return(+(1, x2))
1493_1_plus_InvokeMethod(1517_0_plus_Return(x0, x1)) → 1774_0_plus_Return(2)
1493_1_plus_InvokeMethod(1498_0_times_Return) → 1774_0_plus_Return(2)
1502_1_plus_InvokeMethod(1774_0_plus_Return(x0)) → Cond_1493_1_plus_InvokeMethod(>(x0, 0), 1774_0_plus_Return(x0))
1502_1_plus_InvokeMethod(1498_0_times_Return) → 1774_0_plus_Return(2)

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

The ITRS R consists of the following rules:
259_0_times_NE(x0, 0) → 286_0_times_Return(x0)
357_1_times_InvokeMethod(286_0_times_Return(x0), x0, 0) → 1459_1_times_InvokeMethod(1464_0_plus_LE(0, x0))
357_1_times_InvokeMethod(1498_0_times_Return, 0, x3) → 1459_1_times_InvokeMethod(1464_0_plus_LE(0, 0))
357_1_times_InvokeMethod(1764_0_times_Return(x0), x1, x2) → 1459_1_times_InvokeMethod(1464_0_plus_LE(x0, x1))
357_1_times_InvokeMethod(1764_0_times_Return(x0), 0, x3) → 1459_1_times_InvokeMethod(1464_0_plus_LE(x0, 0))
1459_1_times_InvokeMethod(1498_0_times_Return) → 1498_0_times_Return
1459_1_times_InvokeMethod(1774_0_plus_Return(x2)) → 1764_0_times_Return(x2)
1459_1_times_InvokeMethod(1517_0_plus_Return(x0, x1)) → 1764_0_times_Return(1)
1459_1_times_InvokeMethod(1498_0_times_Return) → 1764_0_times_Return(1)
1464_0_plus_LE(x0, x1) → Cond_1464_0_plus_LE(x1 <= 0 && x0 <= 0, x0, x1)
Cond_1464_0_plus_LE(TRUE, x0, x1) → 1498_0_times_Return
1464_0_plus_LE(x0, x1) → Cond_1464_0_plus_LE1(x1 > 0, x0, x1, x2)
Cond_1464_0_plus_LE1(TRUE, x0, x1, x2) → 1493_1_plus_InvokeMethod(1464_0_plus_LE(x0, x2))
1464_0_plus_LE(x0, x1) → Cond_1464_0_plus_LE2(x1 <= 0 && x0 > 0, x0, x1, x2)
Cond_1464_0_plus_LE2(TRUE, x0, x1, x2) → 1502_1_plus_InvokeMethod(1464_0_plus_LE(x2, x1))
1493_1_plus_InvokeMethod(1498_0_times_Return) → 1517_0_plus_Return(x1, x2)
1502_1_plus_InvokeMethod(1498_0_times_Return) → 1498_0_times_Return
1493_1_plus_InvokeMethod(1774_0_plus_Return(x2)) → Cond_1493_1_plus_InvokeMethod(x2 > 0, 1774_0_plus_Return(x2))
Cond_1493_1_plus_InvokeMethod(TRUE, 1774_0_plus_Return(x2)) → 1774_0_plus_Return(1 + x2)
1493_1_plus_InvokeMethod(1517_0_plus_Return(x0, x1)) → 1774_0_plus_Return(2)
1493_1_plus_InvokeMethod(1498_0_times_Return) → 1774_0_plus_Return(2)
1502_1_plus_InvokeMethod(1774_0_plus_Return(x0)) → Cond_1493_1_plus_InvokeMethod(x0 > 0, 1774_0_plus_Return(x0))
1502_1_plus_InvokeMethod(1498_0_times_Return) → 1774_0_plus_Return(2)

The integer pair graph contains the following rules and edges:
(0): 259_0_TIMES_NE(x0[0], x1[0]) → COND_259_0_TIMES_NE(x1[0] > 0, x0[0], x1[0])
(1): COND_259_0_TIMES_NE(TRUE, x0[1], x1[1]) → 259_0_TIMES_NE(x0[1], x1[1] - 1)

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

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

The set Q consists of the following terms:
259_0_times_NE(x0, 0)
357_1_times_InvokeMethod(286_0_times_Return(x0), x0, 0)
357_1_times_InvokeMethod(1498_0_times_Return, 0, x0)
357_1_times_InvokeMethod(1764_0_times_Return(x0), x1, x2)
1459_1_times_InvokeMethod(1498_0_times_Return)
1459_1_times_InvokeMethod(1774_0_plus_Return(x0))
1459_1_times_InvokeMethod(1517_0_plus_Return(x0, x1))
1464_0_plus_LE(x0, x1)
Cond_1464_0_plus_LE(TRUE, x0, x1)
Cond_1464_0_plus_LE1(TRUE, x0, x1, x2)
Cond_1464_0_plus_LE2(TRUE, x0, x1, x2)
1493_1_plus_InvokeMethod(1498_0_times_Return)
1502_1_plus_InvokeMethod(1498_0_times_Return)
1493_1_plus_InvokeMethod(1774_0_plus_Return(x0))
Cond_1493_1_plus_InvokeMethod(TRUE, 1774_0_plus_Return(x0))
1493_1_plus_InvokeMethod(1517_0_plus_Return(x0, x1))
1502_1_plus_InvokeMethod(1774_0_plus_Return(x0))

(35) 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.IdpCand1ShapeHeuristic@8c1bb13 Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

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 259_0_TIMES_NE(x0, x1) → COND_259_0_TIMES_NE(>(x1, 0), x0, x1) the following chains were created:

We consider the chain 259_0_TIMES_NE(x0[0], x1[0]) → COND_259_0_TIMES_NE(>(x1[0], 0), x0[0], x1[0]), COND_259_0_TIMES_NE(TRUE, x0[1], x1[1]) → 259_0_TIMES_NE(x0[1], -(x1[1], 1)) which results in the following constraint:
(1)    (>(x1[0], 0)=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1] ⇒ 259_0_TIMES_NE(x0[0], x1[0])≥NonInfC∧259_0_TIMES_NE(x0[0], x1[0])≥COND_259_0_TIMES_NE(>(x1[0], 0), x0[0], x1[0])∧(U^Increasing(COND_259_0_TIMES_NE(>(x1[0], 0), x0[0], x1[0])), ≥))

We simplified constraint (1) using rule (IV) which results in the following new constraint:
(2)    (>(x1[0], 0)=TRUE ⇒ 259_0_TIMES_NE(x0[0], x1[0])≥NonInfC∧259_0_TIMES_NE(x0[0], x1[0])≥COND_259_0_TIMES_NE(>(x1[0], 0), x0[0], x1[0])∧(U^Increasing(COND_259_0_TIMES_NE(>(x1[0], 0), x0[0], x1[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x1[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_259_0_TIMES_NE(>(x1[0], 0), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_29] + [(2)bni_29]x1[0] ≥ 0∧[(-1)bso_30] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x1[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_259_0_TIMES_NE(>(x1[0], 0), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_29] + [(2)bni_29]x1[0] ≥ 0∧[(-1)bso_30] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x1[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_259_0_TIMES_NE(>(x1[0], 0), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_29] + [(2)bni_29]x1[0] ≥ 0∧[(-1)bso_30] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x1[0] ≥ 0 ⇒ (U^Increasing(COND_259_0_TIMES_NE(>(x1[0], 0), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_29 + (2)bni_29] + [(2)bni_29]x1[0] ≥ 0∧[(-1)bso_30] ≥ 0)

For Pair COND_259_0_TIMES_NE(TRUE, x0, x1) → 259_0_TIMES_NE(x0, -(x1, 1)) the following chains were created:

We consider the chain COND_259_0_TIMES_NE(TRUE, x0[1], x1[1]) → 259_0_TIMES_NE(x0[1], -(x1[1], 1)) which results in the following constraint:
(7)    (COND_259_0_TIMES_NE(TRUE, x0[1], x1[1])≥NonInfC∧COND_259_0_TIMES_NE(TRUE, x0[1], x1[1])≥259_0_TIMES_NE(x0[1], -(x1[1], 1))∧(U^Increasing(259_0_TIMES_NE(x0[1], -(x1[1], 1))), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    ((U^Increasing(259_0_TIMES_NE(x0[1], -(x1[1], 1))), ≥)∧[bni_31] = 0∧[2 + (-1)bso_32] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    ((U^Increasing(259_0_TIMES_NE(x0[1], -(x1[1], 1))), ≥)∧[bni_31] = 0∧[2 + (-1)bso_32] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    ((U^Increasing(259_0_TIMES_NE(x0[1], -(x1[1], 1))), ≥)∧[bni_31] = 0∧[2 + (-1)bso_32] ≥ 0)

We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(11)    ((U^Increasing(259_0_TIMES_NE(x0[1], -(x1[1], 1))), ≥)∧[bni_31] = 0∧0 = 0∧[2 + (-1)bso_32] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

259_0_TIMES_NE(x0, x1) → COND_259_0_TIMES_NE(>(x1, 0), x0, x1)
- (x1[0] ≥ 0 ⇒ (U^Increasing(COND_259_0_TIMES_NE(>(x1[0], 0), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_29 + (2)bni_29] + [(2)bni_29]x1[0] ≥ 0∧[(-1)bso_30] ≥ 0)
COND_259_0_TIMES_NE(TRUE, x0, x1) → 259_0_TIMES_NE(x0, -(x1, 1))
- ((U^Increasing(259_0_TIMES_NE(x0[1], -(x1[1], 1))), ≥)∧[bni_31] = 0∧0 = 0∧[2 + (-1)bso_32] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(259_0_times_NE(x₁, x₂)) = [-1]
POL(0) = 0
POL(286_0_times_Return(x₁)) = [-1]
POL(357_1_times_InvokeMethod(x₁, x₂, x₃)) = [-1]
POL(1459_1_times_InvokeMethod(x₁)) = [-1]
POL(1464_0_plus_LE(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁
POL(1498_0_times_Return) = [-1]
POL(1764_0_times_Return(x₁)) = [-1]
POL(1774_0_plus_Return(x₁)) = x₁
POL(1517_0_plus_Return(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁
POL(1) = [1]
POL(Cond_1464_0_plus_LE(x₁, x₂, x₃)) = [-1] + [-1]x₃ + [-1]x₂
POL(&&(x₁, x₂)) = [-1]
POL(<=(x₁, x₂)) = [-1]
POL(Cond_1464_0_plus_LE1(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + [-1]x₂
POL(>(x₁, x₂)) = [-1]
POL(1493_1_plus_InvokeMethod(x₁)) = [-1] + [-1]x₁
POL(Cond_1464_0_plus_LE2(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + [-1]x₂
POL(1502_1_plus_InvokeMethod(x₁)) = [-1] + [-1]x₁
POL(Cond_1493_1_plus_InvokeMethod(x₁, x₂)) = [-1] + [-1]x₂
POL(+(x₁, x₂)) = x₁ + x₂
POL(2) = [2]
POL(259_0_TIMES_NE(x₁, x₂)) = [2]x₂
POL(COND_259_0_TIMES_NE(x₁, x₂, x₃)) = [2]x₃
POL(-(x₁, x₂)) = x₁ + [-1]x₂

The following pairs are in P_>:

COND_259_0_TIMES_NE(TRUE, x0[1], x1[1]) → 259_0_TIMES_NE(x0[1], -(x1[1], 1))

The following pairs are in P_bound:

259_0_TIMES_NE(x0[0], x1[0]) → COND_259_0_TIMES_NE(>(x1[0], 0), x0[0], x1[0])

The following pairs are in P_≥:

259_0_TIMES_NE(x0[0], x1[0]) → COND_259_0_TIMES_NE(>(x1[0], 0), x0[0], x1[0])

There are no usable rules.

(36) Complex Obligation (AND)

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

The ITRS R consists of the following rules:
259_0_times_NE(x0, 0) → 286_0_times_Return(x0)
357_1_times_InvokeMethod(286_0_times_Return(x0), x0, 0) → 1459_1_times_InvokeMethod(1464_0_plus_LE(0, x0))
357_1_times_InvokeMethod(1498_0_times_Return, 0, x3) → 1459_1_times_InvokeMethod(1464_0_plus_LE(0, 0))
357_1_times_InvokeMethod(1764_0_times_Return(x0), x1, x2) → 1459_1_times_InvokeMethod(1464_0_plus_LE(x0, x1))
357_1_times_InvokeMethod(1764_0_times_Return(x0), 0, x3) → 1459_1_times_InvokeMethod(1464_0_plus_LE(x0, 0))
1459_1_times_InvokeMethod(1498_0_times_Return) → 1498_0_times_Return
1459_1_times_InvokeMethod(1774_0_plus_Return(x2)) → 1764_0_times_Return(x2)
1459_1_times_InvokeMethod(1517_0_plus_Return(x0, x1)) → 1764_0_times_Return(1)
1459_1_times_InvokeMethod(1498_0_times_Return) → 1764_0_times_Return(1)
1464_0_plus_LE(x0, x1) → Cond_1464_0_plus_LE(x1 <= 0 && x0 <= 0, x0, x1)
Cond_1464_0_plus_LE(TRUE, x0, x1) → 1498_0_times_Return
1464_0_plus_LE(x0, x1) → Cond_1464_0_plus_LE1(x1 > 0, x0, x1, x2)
Cond_1464_0_plus_LE1(TRUE, x0, x1, x2) → 1493_1_plus_InvokeMethod(1464_0_plus_LE(x0, x2))
1464_0_plus_LE(x0, x1) → Cond_1464_0_plus_LE2(x1 <= 0 && x0 > 0, x0, x1, x2)
Cond_1464_0_plus_LE2(TRUE, x0, x1, x2) → 1502_1_plus_InvokeMethod(1464_0_plus_LE(x2, x1))
1493_1_plus_InvokeMethod(1498_0_times_Return) → 1517_0_plus_Return(x1, x2)
1502_1_plus_InvokeMethod(1498_0_times_Return) → 1498_0_times_Return
1493_1_plus_InvokeMethod(1774_0_plus_Return(x2)) → Cond_1493_1_plus_InvokeMethod(x2 > 0, 1774_0_plus_Return(x2))
Cond_1493_1_plus_InvokeMethod(TRUE, 1774_0_plus_Return(x2)) → 1774_0_plus_Return(1 + x2)
1493_1_plus_InvokeMethod(1517_0_plus_Return(x0, x1)) → 1774_0_plus_Return(2)
1493_1_plus_InvokeMethod(1498_0_times_Return) → 1774_0_plus_Return(2)
1502_1_plus_InvokeMethod(1774_0_plus_Return(x0)) → Cond_1493_1_plus_InvokeMethod(x0 > 0, 1774_0_plus_Return(x0))
1502_1_plus_InvokeMethod(1498_0_times_Return) → 1774_0_plus_Return(2)

The integer pair graph contains the following rules and edges:
(0): 259_0_TIMES_NE(x0[0], x1[0]) → COND_259_0_TIMES_NE(x1[0] > 0, x0[0], x1[0])

The set Q consists of the following terms:
259_0_times_NE(x0, 0)
357_1_times_InvokeMethod(286_0_times_Return(x0), x0, 0)
357_1_times_InvokeMethod(1498_0_times_Return, 0, x0)
357_1_times_InvokeMethod(1764_0_times_Return(x0), x1, x2)
1459_1_times_InvokeMethod(1498_0_times_Return)
1459_1_times_InvokeMethod(1774_0_plus_Return(x0))
1459_1_times_InvokeMethod(1517_0_plus_Return(x0, x1))
1464_0_plus_LE(x0, x1)
Cond_1464_0_plus_LE(TRUE, x0, x1)
Cond_1464_0_plus_LE1(TRUE, x0, x1, x2)
Cond_1464_0_plus_LE2(TRUE, x0, x1, x2)
1493_1_plus_InvokeMethod(1498_0_times_Return)
1502_1_plus_InvokeMethod(1498_0_times_Return)
1493_1_plus_InvokeMethod(1774_0_plus_Return(x0))
Cond_1493_1_plus_InvokeMethod(TRUE, 1774_0_plus_Return(x0))
1493_1_plus_InvokeMethod(1517_0_plus_Return(x0, x1))
1502_1_plus_InvokeMethod(1774_0_plus_Return(x0))

(38) IDependencyGraphProof (EQUIVALENT transformation)

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

(39) TRUE

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

The ITRS R consists of the following rules:
259_0_times_NE(x0, 0) → 286_0_times_Return(x0)
357_1_times_InvokeMethod(286_0_times_Return(x0), x0, 0) → 1459_1_times_InvokeMethod(1464_0_plus_LE(0, x0))
357_1_times_InvokeMethod(1498_0_times_Return, 0, x3) → 1459_1_times_InvokeMethod(1464_0_plus_LE(0, 0))
357_1_times_InvokeMethod(1764_0_times_Return(x0), x1, x2) → 1459_1_times_InvokeMethod(1464_0_plus_LE(x0, x1))
357_1_times_InvokeMethod(1764_0_times_Return(x0), 0, x3) → 1459_1_times_InvokeMethod(1464_0_plus_LE(x0, 0))
1459_1_times_InvokeMethod(1498_0_times_Return) → 1498_0_times_Return
1459_1_times_InvokeMethod(1774_0_plus_Return(x2)) → 1764_0_times_Return(x2)
1459_1_times_InvokeMethod(1517_0_plus_Return(x0, x1)) → 1764_0_times_Return(1)
1459_1_times_InvokeMethod(1498_0_times_Return) → 1764_0_times_Return(1)
1464_0_plus_LE(x0, x1) → Cond_1464_0_plus_LE(x1 <= 0 && x0 <= 0, x0, x1)
Cond_1464_0_plus_LE(TRUE, x0, x1) → 1498_0_times_Return
1464_0_plus_LE(x0, x1) → Cond_1464_0_plus_LE1(x1 > 0, x0, x1, x2)
Cond_1464_0_plus_LE1(TRUE, x0, x1, x2) → 1493_1_plus_InvokeMethod(1464_0_plus_LE(x0, x2))
1464_0_plus_LE(x0, x1) → Cond_1464_0_plus_LE2(x1 <= 0 && x0 > 0, x0, x1, x2)
Cond_1464_0_plus_LE2(TRUE, x0, x1, x2) → 1502_1_plus_InvokeMethod(1464_0_plus_LE(x2, x1))
1493_1_plus_InvokeMethod(1498_0_times_Return) → 1517_0_plus_Return(x1, x2)
1502_1_plus_InvokeMethod(1498_0_times_Return) → 1498_0_times_Return
1493_1_plus_InvokeMethod(1774_0_plus_Return(x2)) → Cond_1493_1_plus_InvokeMethod(x2 > 0, 1774_0_plus_Return(x2))
Cond_1493_1_plus_InvokeMethod(TRUE, 1774_0_plus_Return(x2)) → 1774_0_plus_Return(1 + x2)
1493_1_plus_InvokeMethod(1517_0_plus_Return(x0, x1)) → 1774_0_plus_Return(2)
1493_1_plus_InvokeMethod(1498_0_times_Return) → 1774_0_plus_Return(2)
1502_1_plus_InvokeMethod(1774_0_plus_Return(x0)) → Cond_1493_1_plus_InvokeMethod(x0 > 0, 1774_0_plus_Return(x0))
1502_1_plus_InvokeMethod(1498_0_times_Return) → 1774_0_plus_Return(2)

The integer pair graph contains the following rules and edges:
(1): COND_259_0_TIMES_NE(TRUE, x0[1], x1[1]) → 259_0_TIMES_NE(x0[1], x1[1] - 1)

The set Q consists of the following terms:
259_0_times_NE(x0, 0)
357_1_times_InvokeMethod(286_0_times_Return(x0), x0, 0)
357_1_times_InvokeMethod(1498_0_times_Return, 0, x0)
357_1_times_InvokeMethod(1764_0_times_Return(x0), x1, x2)
1459_1_times_InvokeMethod(1498_0_times_Return)
1459_1_times_InvokeMethod(1774_0_plus_Return(x0))
1459_1_times_InvokeMethod(1517_0_plus_Return(x0, x1))
1464_0_plus_LE(x0, x1)
Cond_1464_0_plus_LE(TRUE, x0, x1)
Cond_1464_0_plus_LE1(TRUE, x0, x1, x2)
Cond_1464_0_plus_LE2(TRUE, x0, x1, x2)
1493_1_plus_InvokeMethod(1498_0_times_Return)
1502_1_plus_InvokeMethod(1498_0_times_Return)
1493_1_plus_InvokeMethod(1774_0_plus_Return(x0))
Cond_1493_1_plus_InvokeMethod(TRUE, 1774_0_plus_Return(x0))
1493_1_plus_InvokeMethod(1517_0_plus_Return(x0, x1))
1502_1_plus_InvokeMethod(1774_0_plus_Return(x0))

(41) IDependencyGraphProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIDPv1Proof (SOUND transformation)

(7) Obligation:

(8) IDPNonInfProof (SOUND transformation)

(9) Complex Obligation (AND)

(10) Obligation:

(11) IDependencyGraphProof (EQUIVALENT transformation)

(12) Obligation:

(13) UsableRulesProof (EQUIVALENT transformation)

(14) Obligation:

(15) IDPNonInfProof (SOUND transformation)

(16) Obligation:

(17) IDependencyGraphProof (EQUIVALENT transformation)

(18) TRUE

(19) Obligation:

(20) IDependencyGraphProof (EQUIVALENT transformation)

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) IDPNonInfProof (SOUND transformation)

(25) Complex Obligation (AND)

(26) Obligation:

(27) IDependencyGraphProof (EQUIVALENT transformation)

(28) TRUE

(29) Obligation:

(30) IDependencyGraphProof (EQUIVALENT transformation)

(31) TRUE

(32) Obligation:

(33) SCCToIDPv1Proof (SOUND transformation)

(34) Obligation:

(35) IDPNonInfProof (SOUND transformation)

(36) Complex Obligation (AND)

(37) Obligation:

(38) IDependencyGraphProof (EQUIVALENT transformation)

(39) TRUE

(40) Obligation:

(41) IDependencyGraphProof (EQUIVALENT transformation)

(42) TRUE