Termination proof of /tmp/tmpxtfuuQ/TimesPlusUserDef.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 620 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 10 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 490 ms)

        ↳7 IDP

        ↳8 IDPNonInfProof (⇒, 270 ms)

        ↳9 AND

            ↳10 IDP

                ↳11 IDependencyGraphProof (⇔, 0 ms)

                ↳12 IDP

                ↳13 UsableRulesProof (⇔, 0 ms)

                ↳14 IDP

                ↳15 IDPNonInfProof (⇒, 90 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 (⇒, 90 ms)

                ↳25 AND

                    ↳26 IDP

                        ↳27 IDependencyGraphProof (⇔, 0 ms)

                        ↳28 TRUE

                    ↳29 IDP

                        ↳30 IDependencyGraphProof (⇔, 0 ms)

                        ↳31 TRUE

    ↳32 JBCTerminationSCC

        ↳33 SCCToIDPv1Proof (⇒, 870 ms)

        ↳34 IDP

        ↳35 IDPNonInfProof (⇒, 110 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:
1429_0_plus_LE(EOS(STATIC_1429), i664, i668, i668) → 1430_0_plus_LE(EOS(STATIC_1430), i664, i668, i668)
1429_0_plus_LE(EOS(STATIC_1429), i664, i669, i669) → 1431_0_plus_LE(EOS(STATIC_1431), i664, i669, i669)
1430_0_plus_LE(EOS(STATIC_1430), i664, i668, i668) → 1433_0_plus_Load(EOS(STATIC_1433), i664, i668) | <=(i668, 0)
1433_0_plus_Load(EOS(STATIC_1433), i664, i668) → 1435_0_plus_LE(EOS(STATIC_1435), i664, i668, i664)
1435_0_plus_LE(EOS(STATIC_1435), i674, i668, i674) → 1440_0_plus_LE(EOS(STATIC_1440), i674, i668, i674)
1440_0_plus_LE(EOS(STATIC_1440), i674, i668, i674) → 1444_0_plus_ConstantStackPush(EOS(STATIC_1444), i674, i668) | >(i674, 0)
1444_0_plus_ConstantStackPush(EOS(STATIC_1444), i674, i668) → 1449_0_plus_Load(EOS(STATIC_1449), i674, i668, 1)
1449_0_plus_Load(EOS(STATIC_1449), i674, i668, matching1) → 1453_0_plus_ConstantStackPush(EOS(STATIC_1453), i668, 1, i674) | =(matching1, 1)
1453_0_plus_ConstantStackPush(EOS(STATIC_1453), i668, matching1, i674) → 1457_0_plus_IntArithmetic(EOS(STATIC_1457), i668, 1, i674, 1) | =(matching1, 1)
1457_0_plus_IntArithmetic(EOS(STATIC_1457), i668, matching1, i674, matching2) → 1461_0_plus_Load(EOS(STATIC_1461), i668, 1, -(i674, 1)) | &&(&&(>(i674, 0), =(matching1, 1)), =(matching2, 1))
1461_0_plus_Load(EOS(STATIC_1461), i668, matching1, i678) → 1467_0_plus_InvokeMethod(EOS(STATIC_1467), 1, i678, i668) | =(matching1, 1)
1467_0_plus_InvokeMethod(EOS(STATIC_1467), matching1, i678, i668) → 1469_1_plus_InvokeMethod(1469_0_plus_Load(EOS(STATIC_1469), i678, i668), 1, i678, i668) | =(matching1, 1)
1469_0_plus_Load(EOS(STATIC_1469), i678, i668) → 1475_0_plus_Load(EOS(STATIC_1475), i678, i668)
1475_0_plus_Load(EOS(STATIC_1475), i678, i668) → 1427_0_plus_Load(EOS(STATIC_1427), i678, i668)
1427_0_plus_Load(EOS(STATIC_1427), i664, i665) → 1429_0_plus_LE(EOS(STATIC_1429), i664, i665, i665)
1431_0_plus_LE(EOS(STATIC_1431), i664, i669, i669) → 1434_0_plus_ConstantStackPush(EOS(STATIC_1434), i664, i669) | >(i669, 0)
1434_0_plus_ConstantStackPush(EOS(STATIC_1434), i664, i669) → 1438_0_plus_Load(EOS(STATIC_1438), i664, i669, 1)
1438_0_plus_Load(EOS(STATIC_1438), i664, i669, matching1) → 1442_0_plus_Load(EOS(STATIC_1442), i664, i669, 1, i664) | =(matching1, 1)
1442_0_plus_Load(EOS(STATIC_1442), i664, i669, matching1, i664) → 1445_0_plus_ConstantStackPush(EOS(STATIC_1445), i664, i669, 1, i664, i669) | =(matching1, 1)
1445_0_plus_ConstantStackPush(EOS(STATIC_1445), i664, i669, matching1, i664, i669) → 1450_0_plus_IntArithmetic(EOS(STATIC_1450), i664, i669, 1, i664, i669, 1) | =(matching1, 1)
1450_0_plus_IntArithmetic(EOS(STATIC_1450), i664, i669, matching1, i664, i669, matching2) → 1454_0_plus_InvokeMethod(EOS(STATIC_1454), i664, i669, 1, i664, -(i669, 1)) | &&(&&(>(i669, 0), =(matching1, 1)), =(matching2, 1))
1454_0_plus_InvokeMethod(EOS(STATIC_1454), i664, i669, matching1, i664, i675) → 1459_1_plus_InvokeMethod(1459_0_plus_Load(EOS(STATIC_1459), i664, i675), i664, i669, 1, i664, i675) | =(matching1, 1)
1459_0_plus_Load(EOS(STATIC_1459), i664, i675) → 1463_0_plus_Load(EOS(STATIC_1463), i664, i675)
1463_0_plus_Load(EOS(STATIC_1463), i664, i675) → 1427_0_plus_Load(EOS(STATIC_1427), i664, i675)
R rules:
1435_0_plus_LE(EOS(STATIC_1435), i673, i668, i673) → 1439_0_plus_LE(EOS(STATIC_1439), i673, i668, i673)
1439_0_plus_LE(EOS(STATIC_1439), i673, i668, i673) → 1443_0_plus_ConstantStackPush(EOS(STATIC_1443)) | <=(i673, 0)
1443_0_plus_ConstantStackPush(EOS(STATIC_1443)) → 1447_0_plus_Return(EOS(STATIC_1447), 0)
1459_1_plus_InvokeMethod(1447_0_plus_Return(EOS(STATIC_1447), matching1), i682, i669, matching2, i682, matching3) → 1477_0_plus_Return(EOS(STATIC_1477), i682, i669, 1, i682, 0, 0) | &&(&&(=(matching1, 0), =(matching2, 1)), =(matching3, 0))
1459_1_plus_InvokeMethod(1485_0_plus_Return(EOS(STATIC_1485), i700, i701, matching1), i700, i669, matching2, i700, i701) → 1497_0_plus_Return(EOS(STATIC_1497), i700, i669, 1, i700, i701, i700, i701, 1) | &&(=(matching1, 1), =(matching2, 1))
1459_1_plus_InvokeMethod(1494_0_plus_Return(EOS(STATIC_1494), matching1), i706, i669, matching2, i706, matching3) → 1512_0_plus_Return(EOS(STATIC_1512), i706, i669, 1, i706, 0, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 0))
1459_1_plus_InvokeMethod(1749_0_plus_Return(EOS(STATIC_1749), i1028, i1029, i1004), i1028, i669, matching1, i1028, i1029) → 1786_0_plus_Return(EOS(STATIC_1786), i1028, i669, 1, i1028, i1029, i1028, i1029, i1004) | =(matching1, 1)
1459_1_plus_InvokeMethod(1813_0_plus_Return(EOS(STATIC_1813), i1106, i1107, i1090), i1106, i669, matching1, i1106, i1107) → 1837_0_plus_Return(EOS(STATIC_1837), i1106, i669, 1, i1106, i1107, i1106, i1107, i1090) | =(matching1, 1)
1459_1_plus_InvokeMethod(1815_0_plus_Return(EOS(STATIC_1815), i1091), i1112, i669, matching1, i1112, matching2) → 1841_0_plus_Return(EOS(STATIC_1841), i1112, i669, 1, i1112, 0, i1091) | &&(=(matching1, 1), =(matching2, 0))
1469_1_plus_InvokeMethod(1447_0_plus_Return(EOS(STATIC_1447), matching1), matching2, matching3, i695) → 1486_0_plus_Return(EOS(STATIC_1486), 1, 0, i695, 0) | &&(&&(=(matching1, 0), =(matching2, 1)), =(matching3, 0))
1469_1_plus_InvokeMethod(1494_0_plus_Return(EOS(STATIC_1494), matching1), matching2, i708, i709) → 1514_0_plus_Return(EOS(STATIC_1514), 1, i708, i709, 1) | &&(=(matching1, 1), =(matching2, 1))
1469_1_plus_InvokeMethod(1815_0_plus_Return(EOS(STATIC_1815), i1091), matching1, i1114, i1115) → 1843_0_plus_Return(EOS(STATIC_1843), 1, i1114, i1115, i1091) | =(matching1, 1)
1477_0_plus_Return(EOS(STATIC_1477), i682, i669, matching1, i682, matching2, matching3) → 1482_0_plus_IntArithmetic(EOS(STATIC_1482), i682, i669, 1, 0) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
1482_0_plus_IntArithmetic(EOS(STATIC_1482), i682, i669, matching1, matching2) → 1485_0_plus_Return(EOS(STATIC_1485), i682, i669, 1) | &&(=(matching1, 1), =(matching2, 0))
1486_0_plus_Return(EOS(STATIC_1486), matching1, matching2, i695, matching3) → 1489_0_plus_IntArithmetic(EOS(STATIC_1489), 1, 0) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
1489_0_plus_IntArithmetic(EOS(STATIC_1489), matching1, matching2) → 1494_0_plus_Return(EOS(STATIC_1494), 1) | &&(=(matching1, 1), =(matching2, 0))
1497_0_plus_Return(EOS(STATIC_1497), i700, i669, matching1, i700, i701, i700, i701, matching2) → 1542_0_plus_Return(EOS(STATIC_1542), i700, i669, 1, i700, i701, i700, i701, 1) | &&(=(matching1, 1), =(matching2, 1))
1512_0_plus_Return(EOS(STATIC_1512), i706, i669, matching1, i706, matching2, matching3) → 1587_0_plus_Return(EOS(STATIC_1587), i706, i669, 1, i706, 0, 1) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 1))
1514_0_plus_Return(EOS(STATIC_1514), matching1, i708, i709, matching2) → 1591_0_plus_Return(EOS(STATIC_1591), 1, i708, i709, 1) | &&(=(matching1, 1), =(matching2, 1))
1542_0_plus_Return(EOS(STATIC_1542), i736, i669, matching1, i736, i737, i736, i737, i738) → 1577_0_plus_Return(EOS(STATIC_1577), i736, i669, 1, i736, i737, i736, i737, i738) | =(matching1, 1)
1577_0_plus_Return(EOS(STATIC_1577), i776, i669, matching1, i776, i777, i776, i777, i778) → 1646_0_plus_Return(EOS(STATIC_1646), i776, i669, 1, i776, i777, i776, i777, i778) | =(matching1, 1)
1587_0_plus_Return(EOS(STATIC_1587), i790, i669, matching1, i790, matching2, i791) → 1661_0_plus_Return(EOS(STATIC_1661), i790, i669, 1, i790, 0, i791) | &&(=(matching1, 1), =(matching2, 0))
1591_0_plus_Return(EOS(STATIC_1591), matching1, i797, i795, i796) → 1666_0_plus_Return(EOS(STATIC_1666), 1, i797, i795, i796) | =(matching1, 1)
1646_0_plus_Return(EOS(STATIC_1646), i859, i669, matching1, i859, i860, i859, i860, i861) → 1719_0_plus_Return(EOS(STATIC_1719), i859, i669, 1, i859, i860, i859, i860, i861) | =(matching1, 1)
1661_0_plus_Return(EOS(STATIC_1661), i884, i669, matching1, i884, matching2, i885) → 1733_0_plus_Return(EOS(STATIC_1733), i884, i669, 1, i884, 0, i885) | &&(=(matching1, 1), =(matching2, 0))
1666_0_plus_Return(EOS(STATIC_1666), matching1, i894, i892, i893) → 1739_0_plus_Return(EOS(STATIC_1739), 1, i894, i892, i893) | =(matching1, 1)
1719_0_plus_Return(EOS(STATIC_1719), i959, i669, matching1, i959, i960, i959, i960, i961) → 1742_0_plus_IntArithmetic(EOS(STATIC_1742), i959, i669, 1, i961) | =(matching1, 1)
1733_0_plus_Return(EOS(STATIC_1733), i983, i669, matching1, i983, matching2, i984) → 1800_0_plus_Return(EOS(STATIC_1800), i983, i669, 1, i983, 0, i984) | &&(=(matching1, 1), =(matching2, 0))
1739_0_plus_Return(EOS(STATIC_1739), matching1, i993, i991, i992) → 1806_0_plus_Return(EOS(STATIC_1806), 1, i993, i991, i992) | =(matching1, 1)
1742_0_plus_IntArithmetic(EOS(STATIC_1742), i959, i669, matching1, i961) → 1749_0_plus_Return(EOS(STATIC_1749), i959, i669, +(1, i961)) | &&(>(i961, 0), =(matching1, 1))
1786_0_plus_Return(EOS(STATIC_1786), i1028, i669, matching1, i1028, i1029, i1028, i1029, i1004) → 1719_0_plus_Return(EOS(STATIC_1719), i1028, i669, 1, i1028, i1029, i1028, i1029, i1004) | =(matching1, 1)
1800_0_plus_Return(EOS(STATIC_1800), i1069, i669, matching1, i1069, matching2, i1070) → 1809_0_plus_IntArithmetic(EOS(STATIC_1809), i1069, i669, 1, i1070) | &&(=(matching1, 1), =(matching2, 0))
1806_0_plus_Return(EOS(STATIC_1806), matching1, i1079, i1077, i1078) → 1811_0_plus_IntArithmetic(EOS(STATIC_1811), 1, i1078) | =(matching1, 1)
1809_0_plus_IntArithmetic(EOS(STATIC_1809), i1069, i669, matching1, i1070) → 1813_0_plus_Return(EOS(STATIC_1813), i1069, i669, +(1, i1070)) | &&(>(i1070, 0), =(matching1, 1))
1811_0_plus_IntArithmetic(EOS(STATIC_1811), matching1, i1078) → 1815_0_plus_Return(EOS(STATIC_1815), +(1, i1078)) | &&(>(i1078, 0), =(matching1, 1))
1837_0_plus_Return(EOS(STATIC_1837), i1106, i669, matching1, i1106, i1107, i1106, i1107, i1090) → 1719_0_plus_Return(EOS(STATIC_1719), i1106, i669, 1, i1106, i1107, i1106, i1107, i1090) | =(matching1, 1)
1841_0_plus_Return(EOS(STATIC_1841), i1112, i669, matching1, i1112, matching2, i1091) → 1800_0_plus_Return(EOS(STATIC_1800), i1112, i669, 1, i1112, 0, i1091) | &&(=(matching1, 1), =(matching2, 0))
1843_0_plus_Return(EOS(STATIC_1843), matching1, i1114, i1115, i1091) → 1806_0_plus_Return(EOS(STATIC_1806), 1, i1114, i1115, i1091) | =(matching1, 1)

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

P rules:
1429_0_plus_LE(EOS(STATIC_1429), x0, x1, x1) → 1469_1_plus_InvokeMethod(1429_0_plus_LE(EOS(STATIC_1429), -(x0, 1), x1, x1), 1, -(x0, 1), x1) | &&(<=(x1, 0), >(x0, 0))
1429_0_plus_LE(EOS(STATIC_1429), x0, x1, x1) → 1459_1_plus_InvokeMethod(1429_0_plus_LE(EOS(STATIC_1429), x0, -(x1, 1), -(x1, 1)), x0, x1, 1, x0, -(x1, 1)) | >(x1, 0)
R rules:
1459_1_plus_InvokeMethod(1447_0_plus_Return(EOS(STATIC_1447), 0), x1, x2, 1, x1, 0) → 1485_0_plus_Return(EOS(STATIC_1485), x1, x2, 1)
1469_1_plus_InvokeMethod(1447_0_plus_Return(EOS(STATIC_1447), 0), 1, 0, x3) → 1494_0_plus_Return(EOS(STATIC_1494), 1)
1459_1_plus_InvokeMethod(1749_0_plus_Return(EOS(STATIC_1749), x0, x1, x2), x0, x3, 1, x0, x1) → 1749_0_plus_Return(EOS(STATIC_1749), x0, x3, +(1, x2)) | >(x2, 0)
1459_1_plus_InvokeMethod(1813_0_plus_Return(EOS(STATIC_1813), x0, x1, x2), x0, x3, 1, x0, x1) → 1749_0_plus_Return(EOS(STATIC_1749), x0, x3, +(1, x2)) | >(x2, 0)
1459_1_plus_InvokeMethod(1485_0_plus_Return(EOS(STATIC_1485), x0, x1, 1), x0, x3, 1, x0, x1) → 1749_0_plus_Return(EOS(STATIC_1749), x0, x3, 2)
1459_1_plus_InvokeMethod(1815_0_plus_Return(EOS(STATIC_1815), x0), x1, x2, 1, x1, 0) → 1813_0_plus_Return(EOS(STATIC_1813), x1, x2, +(1, x0)) | >(x0, 0)
1459_1_plus_InvokeMethod(1494_0_plus_Return(EOS(STATIC_1494), 1), x1, x2, 1, x1, 0) → 1813_0_plus_Return(EOS(STATIC_1813), x1, x2, 2)
1469_1_plus_InvokeMethod(1815_0_plus_Return(EOS(STATIC_1815), x0), 1, x2, x3) → 1815_0_plus_Return(EOS(STATIC_1815), +(1, x0)) | >(x0, 0)
1469_1_plus_InvokeMethod(1494_0_plus_Return(EOS(STATIC_1494), 1), 1, x2, x3) → 1815_0_plus_Return(EOS(STATIC_1815), 2)

Filtered ground terms:

1459_1_plus_InvokeMethod(x1, x2, x3, x4, x5, x6) → 1459_1_plus_InvokeMethod(x1, x2, x3, x5, x6)
1429_0_plus_LE(x1, x2, x3, x4) → 1429_0_plus_LE(x2, x3, x4)
Cond_1429_0_plus_LE1(x1, x2, x3, x4, x5) → Cond_1429_0_plus_LE1(x1, x3, x4, x5)
1469_1_plus_InvokeMethod(x1, x2, x3, x4) → 1469_1_plus_InvokeMethod(x1, x3, x4)
Cond_1429_0_plus_LE(x1, x2, x3, x4, x5) → Cond_1429_0_plus_LE(x1, x3, x4, x5)
1815_0_plus_Return(x1, x2) → 1815_0_plus_Return(x2)
1494_0_plus_Return(x1, x2) → 1494_0_plus_Return
Cond_1469_1_plus_InvokeMethod(x1, x2, x3, x4, x5) → Cond_1469_1_plus_InvokeMethod(x1, x2, x4, x5)
1813_0_plus_Return(x1, x2, x3, x4) → 1813_0_plus_Return(x2, x3, x4)
Cond_1459_1_plus_InvokeMethod2(x1, x2, x3, x4, x5, x6, x7) → Cond_1459_1_plus_InvokeMethod2(x1, x2, x3, x4, x6)
1749_0_plus_Return(x1, x2, x3, x4) → 1749_0_plus_Return(x2, x3, x4)
1485_0_plus_Return(x1, x2, x3, x4) → 1485_0_plus_Return(x2, x3)
Cond_1459_1_plus_InvokeMethod1(x1, x2, x3, x4, x5, x6, x7) → Cond_1459_1_plus_InvokeMethod1(x1, x2, x3, x4, x6, x7)
Cond_1459_1_plus_InvokeMethod(x1, x2, x3, x4, x5, x6, x7) → Cond_1459_1_plus_InvokeMethod(x1, x2, x3, x4, x6, x7)
1447_0_plus_Return(x1, x2) → 1447_0_plus_Return

Filtered duplicate args:

1429_0_plus_LE(x1, x2, x3) → 1429_0_plus_LE(x1, x3)
Cond_1429_0_plus_LE(x1, x2, x3, x4) → Cond_1429_0_plus_LE(x1, x2, x4)
Cond_1429_0_plus_LE1(x1, x2, x3, x4) → Cond_1429_0_plus_LE1(x1, x2, x4)
1459_1_plus_InvokeMethod(x1, x2, x3, x4, x5) → 1459_1_plus_InvokeMethod(x1, x3, x4, x5)
Cond_1459_1_plus_InvokeMethod(x1, x2, x3, x4, x5, x6) → Cond_1459_1_plus_InvokeMethod(x1, x2, x4)
Cond_1459_1_plus_InvokeMethod1(x1, x2, x3, x4, x5, x6) → Cond_1459_1_plus_InvokeMethod1(x1, x2, x4)
Cond_1459_1_plus_InvokeMethod2(x1, x2, x3, x4, x5) → Cond_1459_1_plus_InvokeMethod2(x1, x2, x4, x5)

Filtered unneeded arguments:

1469_1_plus_InvokeMethod(x1, x2, x3) → 1469_1_plus_InvokeMethod(x1, x2)
1459_1_plus_InvokeMethod(x1, x2, x3, x4) → 1459_1_plus_InvokeMethod(x1, x4)
Cond_1459_1_plus_InvokeMethod(x1, x2, x3) → Cond_1459_1_plus_InvokeMethod(x1, x2)
Cond_1459_1_plus_InvokeMethod1(x1, x2, x3) → Cond_1459_1_plus_InvokeMethod1(x1, x2)
Cond_1459_1_plus_InvokeMethod2(x1, x2, x3, x4) → Cond_1459_1_plus_InvokeMethod2(x1, x2)
Cond_1469_1_plus_InvokeMethod(x1, x2, x3, x4) → Cond_1469_1_plus_InvokeMethod(x1, x2)
1749_0_plus_Return(x1, x2, x3) → 1749_0_plus_Return(x3)
1813_0_plus_Return(x1, x2, x3) → 1813_0_plus_Return(x3)

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

P rules:
1429_0_plus_LE(x0, x1) → 1469_1_plus_InvokeMethod(1429_0_plus_LE(-(x0, 1), x1), -(x0, 1)) | &&(<=(x1, 0), >(x0, 0))
1429_0_plus_LE(x0, x1) → 1459_1_plus_InvokeMethod(1429_0_plus_LE(x0, -(x1, 1)), -(x1, 1)) | >(x1, 0)
R rules:
1459_1_plus_InvokeMethod(1447_0_plus_Return, 0) → 1485_0_plus_Return(x1, x2)
1469_1_plus_InvokeMethod(1447_0_plus_Return, 0) → 1494_0_plus_Return
1459_1_plus_InvokeMethod(1749_0_plus_Return(x2), x1) → 1749_0_plus_Return(+(1, x2)) | >(x2, 0)
1459_1_plus_InvokeMethod(1813_0_plus_Return(x2), x1) → 1749_0_plus_Return(+(1, x2)) | >(x2, 0)
1459_1_plus_InvokeMethod(1485_0_plus_Return(x0, x1), x1) → 1749_0_plus_Return(2)
1459_1_plus_InvokeMethod(1815_0_plus_Return(x0), 0) → 1813_0_plus_Return(+(1, x0)) | >(x0, 0)
1459_1_plus_InvokeMethod(1494_0_plus_Return, 0) → 1813_0_plus_Return(2)
1469_1_plus_InvokeMethod(1815_0_plus_Return(x0), x2) → 1815_0_plus_Return(+(1, x0)) | >(x0, 0)
1469_1_plus_InvokeMethod(1494_0_plus_Return, x2) → 1815_0_plus_Return(2)

Performed bisimulation on rules. Used the following equivalence classes: {[1447_0_plus_Return, 1494_0_plus_Return]=1447_0_plus_Return, [1749_0_plus_Return_1, 1813_0_plus_Return_1, 1815_0_plus_Return_1]=1749_0_plus_Return_1, [Cond_1459_1_plus_InvokeMethod_3, Cond_1459_1_plus_InvokeMethod1_3, Cond_1469_1_plus_InvokeMethod_3]=Cond_1459_1_plus_InvokeMethod_3}

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

P rules:
1429_0_PLUS_LE(x0, x1) → COND_1429_0_PLUS_LE(&&(<=(x1, 0), >(x0, 0)), x0, x1)
COND_1429_0_PLUS_LE(TRUE, x0, x1) → 1429_0_PLUS_LE(-(x0, 1), x1)
1429_0_PLUS_LE(x0, x1) → COND_1429_0_PLUS_LE1(>(x1, 0), x0, x1)
COND_1429_0_PLUS_LE1(TRUE, x0, x1) → 1429_0_PLUS_LE(x0, -(x1, 1))
R rules:
1459_1_plus_InvokeMethod(1447_0_plus_Return, 0) → 1485_0_plus_Return(x1, x2)
1469_1_plus_InvokeMethod(1447_0_plus_Return, 0) → 1447_0_plus_Return
1459_1_plus_InvokeMethod(1749_0_plus_Return(x2), x1) → Cond_1459_1_plus_InvokeMethod(>(x2, 0), 1749_0_plus_Return(x2), x1)
Cond_1459_1_plus_InvokeMethod(TRUE, 1749_0_plus_Return(x2), x1) → 1749_0_plus_Return(+(1, x2))
1459_1_plus_InvokeMethod(1485_0_plus_Return(x0, x1), x1) → 1749_0_plus_Return(2)
1459_1_plus_InvokeMethod(1749_0_plus_Return(x0), 0) → Cond_1459_1_plus_InvokeMethod2(>(x0, 0), 1749_0_plus_Return(x0), 0)
Cond_1459_1_plus_InvokeMethod2(TRUE, 1749_0_plus_Return(x0), 0) → 1749_0_plus_Return(+(1, x0))
1459_1_plus_InvokeMethod(1447_0_plus_Return, 0) → 1749_0_plus_Return(2)
1469_1_plus_InvokeMethod(1749_0_plus_Return(x0), x2) → Cond_1459_1_plus_InvokeMethod(>(x0, 0), 1749_0_plus_Return(x0), x2)
1469_1_plus_InvokeMethod(1447_0_plus_Return, x2) → 1749_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:
1459_1_plus_InvokeMethod(1447_0_plus_Return, 0) → 1485_0_plus_Return(x1, x2)
1469_1_plus_InvokeMethod(1447_0_plus_Return, 0) → 1447_0_plus_Return
1459_1_plus_InvokeMethod(1749_0_plus_Return(x2), x1) → Cond_1459_1_plus_InvokeMethod(x2 > 0, 1749_0_plus_Return(x2), x1)
Cond_1459_1_plus_InvokeMethod(TRUE, 1749_0_plus_Return(x2), x1) → 1749_0_plus_Return(1 + x2)
1459_1_plus_InvokeMethod(1485_0_plus_Return(x0, x1), x1) → 1749_0_plus_Return(2)
1459_1_plus_InvokeMethod(1749_0_plus_Return(x0), 0) → Cond_1459_1_plus_InvokeMethod2(x0 > 0, 1749_0_plus_Return(x0), 0)
Cond_1459_1_plus_InvokeMethod2(TRUE, 1749_0_plus_Return(x0), 0) → 1749_0_plus_Return(1 + x0)
1459_1_plus_InvokeMethod(1447_0_plus_Return, 0) → 1749_0_plus_Return(2)
1469_1_plus_InvokeMethod(1749_0_plus_Return(x0), x2) → Cond_1459_1_plus_InvokeMethod(x0 > 0, 1749_0_plus_Return(x0), x2)
1469_1_plus_InvokeMethod(1447_0_plus_Return, x2) → 1749_0_plus_Return(2)

The integer pair graph contains the following rules and edges:
(0): 1429_0_PLUS_LE(x0[0], x1[0]) → COND_1429_0_PLUS_LE(x1[0] <= 0 && x0[0] > 0, x0[0], x1[0])
(1): COND_1429_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1429_0_PLUS_LE(x0[1] - 1, x1[1])
(2): 1429_0_PLUS_LE(x0[2], x1[2]) → COND_1429_0_PLUS_LE1(x1[2] > 0, x0[2], x1[2])
(3): COND_1429_0_PLUS_LE1(TRUE, x0[3], x1[3]) → 1429_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:
1459_1_plus_InvokeMethod(1447_0_plus_Return, 0)
1459_1_plus_InvokeMethod(1749_0_plus_Return(x0), x1)
Cond_1459_1_plus_InvokeMethod(TRUE, 1749_0_plus_Return(x0), x1)
1459_1_plus_InvokeMethod(1485_0_plus_Return(x0, x1), x1)
Cond_1459_1_plus_InvokeMethod2(TRUE, 1749_0_plus_Return(x0), 0)
1469_1_plus_InvokeMethod(1749_0_plus_Return(x0), x1)
1469_1_plus_InvokeMethod(1447_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@4725d9b 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 1429_0_PLUS_LE(x0, x1) → COND_1429_0_PLUS_LE(&&(<=(x1, 0), >(x0, 0)), x0, x1) the following chains were created:

We consider the chain 1429_0_PLUS_LE(x0[0], x1[0]) → COND_1429_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0]), COND_1429_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1429_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] ⇒ 1429_0_PLUS_LE(x0[0], x1[0])≥NonInfC∧1429_0_PLUS_LE(x0[0], x1[0])≥COND_1429_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])∧(U^Increasing(COND_1429_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 ⇒ 1429_0_PLUS_LE(x0[0], x1[0])≥NonInfC∧1429_0_PLUS_LE(x0[0], x1[0])≥COND_1429_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])∧(U^Increasing(COND_1429_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_1429_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_1429_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_1429_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_1429_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_1429_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_1429_0_PLUS_LE(TRUE, x0, x1) → 1429_0_PLUS_LE(-(x0, 1), x1) the following chains were created:

We consider the chain COND_1429_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1429_0_PLUS_LE(-(x0[1], 1), x1[1]) which results in the following constraint:
(8)    (COND_1429_0_PLUS_LE(TRUE, x0[1], x1[1])≥NonInfC∧COND_1429_0_PLUS_LE(TRUE, x0[1], x1[1])≥1429_0_PLUS_LE(-(x0[1], 1), x1[1])∧(U^Increasing(1429_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(1429_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(1429_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(1429_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(1429_0_PLUS_LE(-(x0[1], 1), x1[1])), ≥)∧[bni_25] = 0∧0 = 0∧0 = 0∧[(-1)bso_26] ≥ 0)

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

We consider the chain 1429_0_PLUS_LE(x0[2], x1[2]) → COND_1429_0_PLUS_LE1(>(x1[2], 0), x0[2], x1[2]), COND_1429_0_PLUS_LE1(TRUE, x0[3], x1[3]) → 1429_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] ⇒ 1429_0_PLUS_LE(x0[2], x1[2])≥NonInfC∧1429_0_PLUS_LE(x0[2], x1[2])≥COND_1429_0_PLUS_LE1(>(x1[2], 0), x0[2], x1[2])∧(U^Increasing(COND_1429_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 ⇒ 1429_0_PLUS_LE(x0[2], x1[2])≥NonInfC∧1429_0_PLUS_LE(x0[2], x1[2])≥COND_1429_0_PLUS_LE1(>(x1[2], 0), x0[2], x1[2])∧(U^Increasing(COND_1429_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_1429_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_1429_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_1429_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_1429_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_1429_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_1429_0_PLUS_LE1(TRUE, x0, x1) → 1429_0_PLUS_LE(x0, -(x1, 1)) the following chains were created:

We consider the chain COND_1429_0_PLUS_LE1(TRUE, x0[3], x1[3]) → 1429_0_PLUS_LE(x0[3], -(x1[3], 1)) which results in the following constraint:
(20)    (COND_1429_0_PLUS_LE1(TRUE, x0[3], x1[3])≥NonInfC∧COND_1429_0_PLUS_LE1(TRUE, x0[3], x1[3])≥1429_0_PLUS_LE(x0[3], -(x1[3], 1))∧(U^Increasing(1429_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(1429_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(1429_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(1429_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(1429_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.

1429_0_PLUS_LE(x0, x1) → COND_1429_0_PLUS_LE(&&(<=(x1, 0), >(x0, 0)), x0, x1)
- (x1[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(COND_1429_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_1429_0_PLUS_LE(TRUE, x0, x1) → 1429_0_PLUS_LE(-(x0, 1), x1)
- ((U^Increasing(1429_0_PLUS_LE(-(x0[1], 1), x1[1])), ≥)∧[bni_25] = 0∧0 = 0∧0 = 0∧[(-1)bso_26] ≥ 0)
1429_0_PLUS_LE(x0, x1) → COND_1429_0_PLUS_LE1(>(x1, 0), x0, x1)
- (x1[2] ≥ 0 ⇒ (U^Increasing(COND_1429_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_1429_0_PLUS_LE1(TRUE, x0, x1) → 1429_0_PLUS_LE(x0, -(x1, 1))
- ((U^Increasing(1429_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(1459_1_plus_InvokeMethod(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁
POL(1447_0_plus_Return) = [-1]
POL(0) = 0
POL(1485_0_plus_Return(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁
POL(1469_1_plus_InvokeMethod(x₁, x₂)) = [-1] + [-1]x₁
POL(1749_0_plus_Return(x₁)) = x₁
POL(Cond_1459_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_1459_1_plus_InvokeMethod2(x₁, x₂, x₃)) = [-1] + [-1]x₂
POL(1429_0_PLUS_LE(x₁, x₂)) = [-1] + x₂
POL(COND_1429_0_PLUS_LE(x₁, x₂, x₃)) = [-1] + x₃
POL(&&(x₁, x₂)) = [-1]
POL(<=(x₁, x₂)) = [-1]
POL(-(x₁, x₂)) = x₁ + [-1]x₂
POL(COND_1429_0_PLUS_LE1(x₁, x₂, x₃)) = [-1] + x₃

The following pairs are in P_>:

COND_1429_0_PLUS_LE1(TRUE, x0[3], x1[3]) → 1429_0_PLUS_LE(x0[3], -(x1[3], 1))

The following pairs are in P_bound:

1429_0_PLUS_LE(x0[2], x1[2]) → COND_1429_0_PLUS_LE1(>(x1[2], 0), x0[2], x1[2])

The following pairs are in P_≥:

1429_0_PLUS_LE(x0[0], x1[0]) → COND_1429_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])
COND_1429_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1429_0_PLUS_LE(-(x0[1], 1), x1[1])
1429_0_PLUS_LE(x0[2], x1[2]) → COND_1429_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:
1459_1_plus_InvokeMethod(1447_0_plus_Return, 0) → 1485_0_plus_Return(x1, x2)
1469_1_plus_InvokeMethod(1447_0_plus_Return, 0) → 1447_0_plus_Return
1459_1_plus_InvokeMethod(1749_0_plus_Return(x2), x1) → Cond_1459_1_plus_InvokeMethod(x2 > 0, 1749_0_plus_Return(x2), x1)
Cond_1459_1_plus_InvokeMethod(TRUE, 1749_0_plus_Return(x2), x1) → 1749_0_plus_Return(1 + x2)
1459_1_plus_InvokeMethod(1485_0_plus_Return(x0, x1), x1) → 1749_0_plus_Return(2)
1459_1_plus_InvokeMethod(1749_0_plus_Return(x0), 0) → Cond_1459_1_plus_InvokeMethod2(x0 > 0, 1749_0_plus_Return(x0), 0)
Cond_1459_1_plus_InvokeMethod2(TRUE, 1749_0_plus_Return(x0), 0) → 1749_0_plus_Return(1 + x0)
1459_1_plus_InvokeMethod(1447_0_plus_Return, 0) → 1749_0_plus_Return(2)
1469_1_plus_InvokeMethod(1749_0_plus_Return(x0), x2) → Cond_1459_1_plus_InvokeMethod(x0 > 0, 1749_0_plus_Return(x0), x2)
1469_1_plus_InvokeMethod(1447_0_plus_Return, x2) → 1749_0_plus_Return(2)

The integer pair graph contains the following rules and edges:
(1): COND_1429_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1429_0_PLUS_LE(x0[1] - 1, x1[1])
(0): 1429_0_PLUS_LE(x0[0], x1[0]) → COND_1429_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_1429_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1429_0_PLUS_LE(x0[1] - 1, x1[1])
(0): 1429_0_PLUS_LE(x0[0], x1[0]) → COND_1429_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@4725d9b 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_1429_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1429_0_PLUS_LE(-(x0[1], 1), x1[1]) the following chains were created:

We consider the chain COND_1429_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1429_0_PLUS_LE(-(x0[1], 1), x1[1]) which results in the following constraint:
(1)    (COND_1429_0_PLUS_LE(TRUE, x0[1], x1[1])≥NonInfC∧COND_1429_0_PLUS_LE(TRUE, x0[1], x1[1])≥1429_0_PLUS_LE(-(x0[1], 1), x1[1])∧(U^Increasing(1429_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(1429_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(1429_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(1429_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(1429_0_PLUS_LE(-(x0[1], 1), x1[1])), ≥)∧[bni_10] = 0∧0 = 0∧0 = 0∧[(-1)bso_11] ≥ 0)

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

We consider the chain 1429_0_PLUS_LE(x0[0], x1[0]) → COND_1429_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0]), COND_1429_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1429_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] ⇒ 1429_0_PLUS_LE(x0[0], x1[0])≥NonInfC∧1429_0_PLUS_LE(x0[0], x1[0])≥COND_1429_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])∧(U^Increasing(COND_1429_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 ⇒ 1429_0_PLUS_LE(x0[0], x1[0])≥NonInfC∧1429_0_PLUS_LE(x0[0], x1[0])≥COND_1429_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])∧(U^Increasing(COND_1429_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_1429_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_1429_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_1429_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_1429_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_1429_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_1429_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1429_0_PLUS_LE(-(x0[1], 1), x1[1])
- ((U^Increasing(1429_0_PLUS_LE(-(x0[1], 1), x1[1])), ≥)∧[bni_10] = 0∧0 = 0∧0 = 0∧[(-1)bso_11] ≥ 0)
1429_0_PLUS_LE(x0[0], x1[0]) → COND_1429_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])
- (x1[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(COND_1429_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_1429_0_PLUS_LE(x₁, x₂, x₃)) = [-1] + [-1]x₃ + [2]x₂
POL(1429_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_>:

1429_0_PLUS_LE(x0[0], x1[0]) → COND_1429_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])

The following pairs are in P_bound:

1429_0_PLUS_LE(x0[0], x1[0]) → COND_1429_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])

The following pairs are in P_≥:

COND_1429_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1429_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_1429_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1429_0_PLUS_LE(x0[1] - 1, x1[1])

The set Q consists of the following terms:
1459_1_plus_InvokeMethod(1447_0_plus_Return, 0)
1459_1_plus_InvokeMethod(1749_0_plus_Return(x0), x1)
Cond_1459_1_plus_InvokeMethod(TRUE, 1749_0_plus_Return(x0), x1)
1459_1_plus_InvokeMethod(1485_0_plus_Return(x0, x1), x1)
Cond_1459_1_plus_InvokeMethod2(TRUE, 1749_0_plus_Return(x0), 0)
1469_1_plus_InvokeMethod(1749_0_plus_Return(x0), x1)
1469_1_plus_InvokeMethod(1447_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:
1459_1_plus_InvokeMethod(1447_0_plus_Return, 0) → 1485_0_plus_Return(x1, x2)
1469_1_plus_InvokeMethod(1447_0_plus_Return, 0) → 1447_0_plus_Return
1459_1_plus_InvokeMethod(1749_0_plus_Return(x2), x1) → Cond_1459_1_plus_InvokeMethod(x2 > 0, 1749_0_plus_Return(x2), x1)
Cond_1459_1_plus_InvokeMethod(TRUE, 1749_0_plus_Return(x2), x1) → 1749_0_plus_Return(1 + x2)
1459_1_plus_InvokeMethod(1485_0_plus_Return(x0, x1), x1) → 1749_0_plus_Return(2)
1459_1_plus_InvokeMethod(1749_0_plus_Return(x0), 0) → Cond_1459_1_plus_InvokeMethod2(x0 > 0, 1749_0_plus_Return(x0), 0)
Cond_1459_1_plus_InvokeMethod2(TRUE, 1749_0_plus_Return(x0), 0) → 1749_0_plus_Return(1 + x0)
1459_1_plus_InvokeMethod(1447_0_plus_Return, 0) → 1749_0_plus_Return(2)
1469_1_plus_InvokeMethod(1749_0_plus_Return(x0), x2) → Cond_1459_1_plus_InvokeMethod(x0 > 0, 1749_0_plus_Return(x0), x2)
1469_1_plus_InvokeMethod(1447_0_plus_Return, x2) → 1749_0_plus_Return(2)

The integer pair graph contains the following rules and edges:
(0): 1429_0_PLUS_LE(x0[0], x1[0]) → COND_1429_0_PLUS_LE(x1[0] <= 0 && x0[0] > 0, x0[0], x1[0])
(1): COND_1429_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1429_0_PLUS_LE(x0[1] - 1, x1[1])
(3): COND_1429_0_PLUS_LE1(TRUE, x0[3], x1[3]) → 1429_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:
1459_1_plus_InvokeMethod(1447_0_plus_Return, 0) → 1485_0_plus_Return(x1, x2)
1469_1_plus_InvokeMethod(1447_0_plus_Return, 0) → 1447_0_plus_Return
1459_1_plus_InvokeMethod(1749_0_plus_Return(x2), x1) → Cond_1459_1_plus_InvokeMethod(x2 > 0, 1749_0_plus_Return(x2), x1)
Cond_1459_1_plus_InvokeMethod(TRUE, 1749_0_plus_Return(x2), x1) → 1749_0_plus_Return(1 + x2)
1459_1_plus_InvokeMethod(1485_0_plus_Return(x0, x1), x1) → 1749_0_plus_Return(2)
1459_1_plus_InvokeMethod(1749_0_plus_Return(x0), 0) → Cond_1459_1_plus_InvokeMethod2(x0 > 0, 1749_0_plus_Return(x0), 0)
Cond_1459_1_plus_InvokeMethod2(TRUE, 1749_0_plus_Return(x0), 0) → 1749_0_plus_Return(1 + x0)
1459_1_plus_InvokeMethod(1447_0_plus_Return, 0) → 1749_0_plus_Return(2)
1469_1_plus_InvokeMethod(1749_0_plus_Return(x0), x2) → Cond_1459_1_plus_InvokeMethod(x0 > 0, 1749_0_plus_Return(x0), x2)
1469_1_plus_InvokeMethod(1447_0_plus_Return, x2) → 1749_0_plus_Return(2)

The integer pair graph contains the following rules and edges:
(1): COND_1429_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1429_0_PLUS_LE(x0[1] - 1, x1[1])
(0): 1429_0_PLUS_LE(x0[0], x1[0]) → COND_1429_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@4725d9b 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_1429_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1429_0_PLUS_LE(-(x0[1], 1), x1[1]) the following chains were created:

We consider the chain COND_1429_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1429_0_PLUS_LE(-(x0[1], 1), x1[1]) which results in the following constraint:
(1)    (COND_1429_0_PLUS_LE(TRUE, x0[1], x1[1])≥NonInfC∧COND_1429_0_PLUS_LE(TRUE, x0[1], x1[1])≥1429_0_PLUS_LE(-(x0[1], 1), x1[1])∧(U^Increasing(1429_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(1429_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(1429_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(1429_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(1429_0_PLUS_LE(-(x0[1], 1), x1[1])), ≥)∧[bni_8] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_9] ≥ 0)

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

We consider the chain 1429_0_PLUS_LE(x0[0], x1[0]) → COND_1429_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0]), COND_1429_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1429_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] ⇒ 1429_0_PLUS_LE(x0[0], x1[0])≥NonInfC∧1429_0_PLUS_LE(x0[0], x1[0])≥COND_1429_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])∧(U^Increasing(COND_1429_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 ⇒ 1429_0_PLUS_LE(x0[0], x1[0])≥NonInfC∧1429_0_PLUS_LE(x0[0], x1[0])≥COND_1429_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])∧(U^Increasing(COND_1429_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_1429_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_1429_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_1429_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_1429_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_1429_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_1429_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1429_0_PLUS_LE(-(x0[1], 1), x1[1])
- ((U^Increasing(1429_0_PLUS_LE(-(x0[1], 1), x1[1])), ≥)∧[bni_8] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_9] ≥ 0)
1429_0_PLUS_LE(x0[0], x1[0]) → COND_1429_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])
- (x1[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(COND_1429_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_1429_0_PLUS_LE(x₁, x₂, x₃)) = [-1] + [-1]x₃ + x₂
POL(1429_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_1429_0_PLUS_LE(TRUE, x0[1], x1[1]) → 1429_0_PLUS_LE(-(x0[1], 1), x1[1])

The following pairs are in P_bound:

1429_0_PLUS_LE(x0[0], x1[0]) → COND_1429_0_PLUS_LE(&&(<=(x1[0], 0), >(x0[0], 0)), x0[0], x1[0])

The following pairs are in P_≥:

1429_0_PLUS_LE(x0[0], x1[0]) → COND_1429_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): 1429_0_PLUS_LE(x0[0], x1[0]) → COND_1429_0_PLUS_LE(x1[0] <= 0 && x0[0] > 0, x0[0], x1[0])

The set Q consists of the following terms:
1459_1_plus_InvokeMethod(1447_0_plus_Return, 0)
1459_1_plus_InvokeMethod(1749_0_plus_Return(x0), x1)
Cond_1459_1_plus_InvokeMethod(TRUE, 1749_0_plus_Return(x0), x1)
1459_1_plus_InvokeMethod(1485_0_plus_Return(x0, x1), x1)
Cond_1459_1_plus_InvokeMethod2(TRUE, 1749_0_plus_Return(x0), 0)
1469_1_plus_InvokeMethod(1749_0_plus_Return(x0), x1)
1469_1_plus_InvokeMethod(1447_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:
270_0_times_NE(EOS(STATIC_270), i18, i43, i43) → 277_0_times_NE(EOS(STATIC_277), i18, i43, i43)
277_0_times_NE(EOS(STATIC_277), i18, i43, i43) → 288_0_times_Load(EOS(STATIC_288), i18, i43) | >(i43, 0)
288_0_times_Load(EOS(STATIC_288), i18, i43) → 300_0_times_LE(EOS(STATIC_300), i18, i43, i43)
300_0_times_LE(EOS(STATIC_300), i18, i43, i43) → 314_0_times_Load(EOS(STATIC_314), i18, i43) | >(i43, 0)
314_0_times_Load(EOS(STATIC_314), i18, i43) → 326_0_times_Load(EOS(STATIC_326), i18, i43, i18)
326_0_times_Load(EOS(STATIC_326), i18, i43, i18) → 345_0_times_ConstantStackPush(EOS(STATIC_345), i18, i18, i43)
345_0_times_ConstantStackPush(EOS(STATIC_345), i18, i18, i43) → 354_0_times_IntArithmetic(EOS(STATIC_354), i18, i18, i43, 1)
354_0_times_IntArithmetic(EOS(STATIC_354), i18, i18, i43, matching1) → 364_0_times_InvokeMethod(EOS(STATIC_364), i18, i18, -(i43, 1)) | &&(>(i43, 0), =(matching1, 1))
364_0_times_InvokeMethod(EOS(STATIC_364), i18, i18, i53) → 373_1_times_InvokeMethod(373_0_times_Load(EOS(STATIC_373), i18, i53), i18, i18, i53)
373_0_times_Load(EOS(STATIC_373), i18, i53) → 382_0_times_Load(EOS(STATIC_382), i18, i53)
382_0_times_Load(EOS(STATIC_382), i18, i53) → 258_0_times_Load(EOS(STATIC_258), i18, i53)
258_0_times_Load(EOS(STATIC_258), i18, i37) → 270_0_times_NE(EOS(STATIC_270), i18, i37, i37)
R rules:
1425_0_plus_Load(EOS(STATIC_1425), i635, i634) → 1427_0_plus_Load(EOS(STATIC_1427), i635, i634)
1463_0_plus_Load(EOS(STATIC_1463), i664) → 1427_0_plus_Load(EOS(STATIC_1427), i664, i675)
1475_0_plus_Load(EOS(STATIC_1475), i668) → 1427_0_plus_Load(EOS(STATIC_1427), i678, i668)
270_0_times_NE(EOS(STATIC_270), i18, matching1, matching2) → 279_0_times_NE(EOS(STATIC_279), i18, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
279_0_times_NE(EOS(STATIC_279), i18, matching1, matching2) → 290_0_times_ConstantStackPush(EOS(STATIC_290), i18, 0) | &&(=(matching1, 0), =(matching2, 0))
290_0_times_ConstantStackPush(EOS(STATIC_290), i18, matching1) → 302_0_times_Return(EOS(STATIC_302), i18, 0, 0) | =(matching1, 0)
373_1_times_InvokeMethod(302_0_times_Return(EOS(STATIC_302), i57, matching1, matching2), i57, i57, matching3) → 400_0_times_Return(EOS(STATIC_400), i57, i57, 0, i57, 0, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
373_1_times_InvokeMethod(1465_0_times_Return(EOS(STATIC_1465), matching1), matching2, matching3, i685) → 1481_0_times_Return(EOS(STATIC_1481), 0, 0, i685, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
373_1_times_InvokeMethod(1740_0_times_Return(EOS(STATIC_1740), i953), i1013, i1013, i1014) → 1767_0_times_Return(EOS(STATIC_1767), i1013, i1013, i1014, i953)
373_1_times_InvokeMethod(1808_0_times_Return(EOS(STATIC_1808), i1063), matching1, matching2, i1096) → 1824_0_times_Return(EOS(STATIC_1824), 0, 0, i1096, i1063) | &&(=(matching1, 0), =(matching2, 0))
400_0_times_Return(EOS(STATIC_400), i57, i57, matching1, i57, matching2, matching3) → 402_0_times_Load(EOS(STATIC_402), i57, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
402_0_times_Load(EOS(STATIC_402), i57, matching1) → 571_0_times_Load(EOS(STATIC_571), i57, 0) | =(matching1, 0)
552_0_times_Return(EOS(STATIC_552), i87, i87, i89, i88) → 830_0_times_Return(EOS(STATIC_830), i87, i87, i89, i88)
571_0_times_Load(EOS(STATIC_571), i87, i88) → 843_0_times_Load(EOS(STATIC_843), i87, i88)
830_0_times_Return(EOS(STATIC_830), i216, i216, i218, i217) → 1226_0_times_Return(EOS(STATIC_1226), i216, i216, i218, i217)
843_0_times_Load(EOS(STATIC_843), i216, i217) → 1249_0_times_Load(EOS(STATIC_1249), i216, i217)
1226_0_times_Return(EOS(STATIC_1226), i470, i470, i472, i471) → 1399_0_times_Return(EOS(STATIC_1399), i470, i470, i472, i471)
1249_0_times_Load(EOS(STATIC_1249), i470, i471) → 1417_0_times_Load(EOS(STATIC_1417), i470, i471)
1399_0_times_Return(EOS(STATIC_1399), i634, i634, i636, i635) → 1417_0_times_Load(EOS(STATIC_1417), i634, i635)
1417_0_times_Load(EOS(STATIC_1417), i634, i635) → 1421_0_times_InvokeMethod(EOS(STATIC_1421), i635, i634)
1421_0_times_InvokeMethod(EOS(STATIC_1421), i635, i634) → 1423_1_times_InvokeMethod(1423_0_plus_Load(EOS(STATIC_1423), i635, i634), i635, i634)
1423_0_plus_Load(EOS(STATIC_1423), i635, i634) → 1425_0_plus_Load(EOS(STATIC_1425), i635, i634)
1423_1_times_InvokeMethod(1447_0_plus_Return(EOS(STATIC_1447), matching1), i676, i677) → 1460_0_plus_Return(EOS(STATIC_1460), i676, i677, 0) | =(matching1, 0)
1423_1_times_InvokeMethod(1485_0_plus_Return(EOS(STATIC_1485), i697, i698, matching1), i697, i698) → 1496_0_plus_Return(EOS(STATIC_1496), i697, i698, i697, i698, 1) | =(matching1, 1)
1423_1_times_InvokeMethod(1494_0_plus_Return(EOS(STATIC_1494), matching1), i703, i704) → 1511_0_plus_Return(EOS(STATIC_1511), i703, i704, 1) | =(matching1, 1)
1423_1_times_InvokeMethod(1749_0_plus_Return(EOS(STATIC_1749), i1025, i1026, i1004), i1025, i1026) → 1784_0_plus_Return(EOS(STATIC_1784), i1025, i1026, i1025, i1026, i1004)
1423_1_times_InvokeMethod(1813_0_plus_Return(EOS(STATIC_1813), i1103, i1104, i1090), i1103, i1104) → 1835_0_plus_Return(EOS(STATIC_1835), i1103, i1104, i1103, i1104, i1090)
1423_1_times_InvokeMethod(1815_0_plus_Return(EOS(STATIC_1815), i1091), i1110, i1111) → 1840_0_plus_Return(EOS(STATIC_1840), i1110, i1111, i1091)
1460_0_plus_Return(EOS(STATIC_1460), i676, i677, matching1) → 1465_0_times_Return(EOS(STATIC_1465), 0) | =(matching1, 0)
1481_0_times_Return(EOS(STATIC_1481), matching1, matching2, i685, matching3) → 1399_0_times_Return(EOS(STATIC_1399), 0, 0, i685, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
1496_0_plus_Return(EOS(STATIC_1496), i697, i698, i697, i698, matching1) → 1538_0_plus_Return(EOS(STATIC_1538), i697, i698, i697, i698, 1) | =(matching1, 1)
1511_0_plus_Return(EOS(STATIC_1511), i703, i704, matching1) → 1583_0_plus_Return(EOS(STATIC_1583), i703, i704, 1) | =(matching1, 1)
1538_0_plus_Return(EOS(STATIC_1538), i731, i730, i731, i730, i732) → 1572_0_plus_Return(EOS(STATIC_1572), i731, i730, i731, i730, i732)
1572_0_plus_Return(EOS(STATIC_1572), i770, i769, i770, i769, i771) → 1641_0_plus_Return(EOS(STATIC_1641), i770, i769, i770, i769, i771)
1583_0_plus_Return(EOS(STATIC_1583), i788, i786, i787) → 1657_0_plus_Return(EOS(STATIC_1657), i788, i786, i787)
1641_0_plus_Return(EOS(STATIC_1641), i852, i851, i852, i851, i853) → 1713_0_plus_Return(EOS(STATIC_1713), i852, i851, i852, i851, i853)
1657_0_plus_Return(EOS(STATIC_1657), i879, i877, i878) → 1729_0_plus_Return(EOS(STATIC_1729), i879, i877, i878)
1713_0_plus_Return(EOS(STATIC_1713), i952, i951, i952, i951, i953) → 1740_0_times_Return(EOS(STATIC_1740), i953)
1729_0_plus_Return(EOS(STATIC_1729), i978, i976, i977) → 1796_0_plus_Return(EOS(STATIC_1796), i978, i976, i977)
1767_0_times_Return(EOS(STATIC_1767), i1013, i1013, i1014, i953) → 1399_0_times_Return(EOS(STATIC_1399), i1013, i1013, i1014, i953)
1784_0_plus_Return(EOS(STATIC_1784), i1025, i1026, i1025, i1026, i1004) → 1713_0_plus_Return(EOS(STATIC_1713), i1025, i1026, i1025, i1026, i1004)
1796_0_plus_Return(EOS(STATIC_1796), i1064, i1062, i1063) → 1808_0_times_Return(EOS(STATIC_1808), i1063)
1824_0_times_Return(EOS(STATIC_1824), matching1, matching2, i1096, i1063) → 1399_0_times_Return(EOS(STATIC_1399), 0, 0, i1096, i1063) | &&(=(matching1, 0), =(matching2, 0))
1835_0_plus_Return(EOS(STATIC_1835), i1103, i1104, i1103, i1104, i1090) → 1713_0_plus_Return(EOS(STATIC_1713), i1103, i1104, i1103, i1104, i1090)
1840_0_plus_Return(EOS(STATIC_1840), i1110, i1111, i1091) → 1796_0_plus_Return(EOS(STATIC_1796), i1110, i1111, i1091)
1427_0_plus_Load(EOS(STATIC_1427), i664, i665) → 1429_0_plus_LE(EOS(STATIC_1429), i664, i665, i665)
1429_0_plus_LE(EOS(STATIC_1429), i664, i668, i668) → 1430_0_plus_LE(EOS(STATIC_1430), i664, i668, i668)
1429_0_plus_LE(EOS(STATIC_1429), i664, i669, i669) → 1431_0_plus_LE(EOS(STATIC_1431), i664, i669, i669)
1430_0_plus_LE(EOS(STATIC_1430), i664, i668, i668) → 1433_0_plus_Load(EOS(STATIC_1433), i664, i668) | <=(i668, 0)
1431_0_plus_LE(EOS(STATIC_1431), i664, i669, i669) → 1434_0_plus_ConstantStackPush(EOS(STATIC_1434), i664, i669) | >(i669, 0)
1433_0_plus_Load(EOS(STATIC_1433), i664, i668) → 1435_0_plus_LE(EOS(STATIC_1435), i664, i668, i664)
1434_0_plus_ConstantStackPush(EOS(STATIC_1434), i664, i669) → 1438_0_plus_Load(EOS(STATIC_1438), i664, i669, 1)
1435_0_plus_LE(EOS(STATIC_1435), i673, i668, i673) → 1439_0_plus_LE(EOS(STATIC_1439), i673, i668, i673)
1435_0_plus_LE(EOS(STATIC_1435), i674, i668, i674) → 1440_0_plus_LE(EOS(STATIC_1440), i674, i668, i674)
1438_0_plus_Load(EOS(STATIC_1438), i664, i669, matching1) → 1442_0_plus_Load(EOS(STATIC_1442), i664, i669, 1, i664) | =(matching1, 1)
1439_0_plus_LE(EOS(STATIC_1439), i673, i668, i673) → 1443_0_plus_ConstantStackPush(EOS(STATIC_1443)) | <=(i673, 0)
1440_0_plus_LE(EOS(STATIC_1440), i674, i668, i674) → 1444_0_plus_ConstantStackPush(EOS(STATIC_1444), i674, i668) | >(i674, 0)
1442_0_plus_Load(EOS(STATIC_1442), i664, i669, matching1, i664) → 1445_0_plus_ConstantStackPush(EOS(STATIC_1445), i664, i669, 1, i664, i669) | =(matching1, 1)
1443_0_plus_ConstantStackPush(EOS(STATIC_1443)) → 1447_0_plus_Return(EOS(STATIC_1447), 0)
1444_0_plus_ConstantStackPush(EOS(STATIC_1444), i674, i668) → 1449_0_plus_Load(EOS(STATIC_1449), i674, i668, 1)
1445_0_plus_ConstantStackPush(EOS(STATIC_1445), i664, i669, matching1, i664, i669) → 1450_0_plus_IntArithmetic(EOS(STATIC_1450), i664, i669, 1, i664, i669, 1) | =(matching1, 1)
1449_0_plus_Load(EOS(STATIC_1449), i674, i668, matching1) → 1453_0_plus_ConstantStackPush(EOS(STATIC_1453), i668, 1, i674) | =(matching1, 1)
1450_0_plus_IntArithmetic(EOS(STATIC_1450), i664, i669, matching1, i664, i669, matching2) → 1454_0_plus_InvokeMethod(EOS(STATIC_1454), i664, i669, 1, i664) | &&(&&(>(i669, 0), =(matching1, 1)), =(matching2, 1))
1453_0_plus_ConstantStackPush(EOS(STATIC_1453), i668, matching1, i674) → 1457_0_plus_IntArithmetic(EOS(STATIC_1457), i668, 1, i674, 1) | =(matching1, 1)
1454_0_plus_InvokeMethod(EOS(STATIC_1454), i664, i669, matching1, i664) → 1459_1_plus_InvokeMethod(1459_0_plus_Load(EOS(STATIC_1459), i664), i664, i669, 1, i664) | =(matching1, 1)
1457_0_plus_IntArithmetic(EOS(STATIC_1457), i668, matching1, i674, matching2) → 1461_0_plus_Load(EOS(STATIC_1461), i668, 1) | &&(&&(>(i674, 0), =(matching1, 1)), =(matching2, 1))
1459_0_plus_Load(EOS(STATIC_1459), i664) → 1463_0_plus_Load(EOS(STATIC_1463), i664)
1459_1_plus_InvokeMethod(1447_0_plus_Return(EOS(STATIC_1447), matching1), i682, i669, matching2, i682) → 1477_0_plus_Return(EOS(STATIC_1477), i682, i669, 1, i682, 0, 0) | &&(=(matching1, 0), =(matching2, 1))
1459_1_plus_InvokeMethod(1485_0_plus_Return(EOS(STATIC_1485), i700, i701, matching1), i700, i669, matching2, i700) → 1497_0_plus_Return(EOS(STATIC_1497), i700, i669, 1, i700, i700, 1) | &&(=(matching1, 1), =(matching2, 1))
1459_1_plus_InvokeMethod(1494_0_plus_Return(EOS(STATIC_1494), matching1), i706, i669, matching2, i706) → 1512_0_plus_Return(EOS(STATIC_1512), i706, i669, 1, i706, 0, 1) | &&(=(matching1, 1), =(matching2, 1))
1459_1_plus_InvokeMethod(1749_0_plus_Return(EOS(STATIC_1749), i1028, i1029, i1004), i1028, i669, matching1, i1028) → 1786_0_plus_Return(EOS(STATIC_1786), i1028, i669, 1, i1028, i1028, i1004) | =(matching1, 1)
1459_1_plus_InvokeMethod(1813_0_plus_Return(EOS(STATIC_1813), i1106, i1107, i1090), i1106, i669, matching1, i1106) → 1837_0_plus_Return(EOS(STATIC_1837), i1106, i669, 1, i1106, i1106, i1090) | =(matching1, 1)
1459_1_plus_InvokeMethod(1815_0_plus_Return(EOS(STATIC_1815), i1091), i1112, i669, matching1, i1112) → 1841_0_plus_Return(EOS(STATIC_1841), i1112, i669, 1, i1112, 0, i1091) | =(matching1, 1)
1461_0_plus_Load(EOS(STATIC_1461), i668, matching1) → 1467_0_plus_InvokeMethod(EOS(STATIC_1467), 1, i668) | =(matching1, 1)
1467_0_plus_InvokeMethod(EOS(STATIC_1467), matching1, i668) → 1469_1_plus_InvokeMethod(1469_0_plus_Load(EOS(STATIC_1469), i668), 1, i668) | =(matching1, 1)
1469_0_plus_Load(EOS(STATIC_1469), i668) → 1475_0_plus_Load(EOS(STATIC_1475), i668)
1469_1_plus_InvokeMethod(1447_0_plus_Return(EOS(STATIC_1447), matching1), matching2, i695) → 1486_0_plus_Return(EOS(STATIC_1486), 1, 0, i695, 0) | &&(=(matching1, 0), =(matching2, 1))
1469_1_plus_InvokeMethod(1494_0_plus_Return(EOS(STATIC_1494), matching1), matching2, i709) → 1514_0_plus_Return(EOS(STATIC_1514), 1, i709, 1) | &&(=(matching1, 1), =(matching2, 1))
1469_1_plus_InvokeMethod(1815_0_plus_Return(EOS(STATIC_1815), i1091), matching1, i1115) → 1843_0_plus_Return(EOS(STATIC_1843), 1, i1115, i1091) | =(matching1, 1)
1477_0_plus_Return(EOS(STATIC_1477), i682, i669, matching1, i682, matching2, matching3) → 1482_0_plus_IntArithmetic(EOS(STATIC_1482), i682, i669, 1, 0) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
1482_0_plus_IntArithmetic(EOS(STATIC_1482), i682, i669, matching1, matching2) → 1485_0_plus_Return(EOS(STATIC_1485), i682, i669, 1) | &&(=(matching1, 1), =(matching2, 0))
1486_0_plus_Return(EOS(STATIC_1486), matching1, matching2, i695, matching3) → 1489_0_plus_IntArithmetic(EOS(STATIC_1489), 1, 0) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
1489_0_plus_IntArithmetic(EOS(STATIC_1489), matching1, matching2) → 1494_0_plus_Return(EOS(STATIC_1494), 1) | &&(=(matching1, 1), =(matching2, 0))
1497_0_plus_Return(EOS(STATIC_1497), i700, i669, matching1, i700, i700, matching2) → 1542_0_plus_Return(EOS(STATIC_1542), i700, i669, 1, i700, i700, 1) | &&(=(matching1, 1), =(matching2, 1))
1512_0_plus_Return(EOS(STATIC_1512), i706, i669, matching1, i706, matching2, matching3) → 1587_0_plus_Return(EOS(STATIC_1587), i706, i669, 1, i706, 0, 1) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 1))
1514_0_plus_Return(EOS(STATIC_1514), matching1, i709, matching2) → 1591_0_plus_Return(EOS(STATIC_1591), 1, i709, 1) | &&(=(matching1, 1), =(matching2, 1))
1542_0_plus_Return(EOS(STATIC_1542), i736, i669, matching1, i736, i736, i738) → 1577_0_plus_Return(EOS(STATIC_1577), i736, i669, 1, i736, i736, i738) | =(matching1, 1)
1577_0_plus_Return(EOS(STATIC_1577), i776, i669, matching1, i776, i776, i778) → 1646_0_plus_Return(EOS(STATIC_1646), i776, i669, 1, i776, i776, i778) | =(matching1, 1)
1587_0_plus_Return(EOS(STATIC_1587), i790, i669, matching1, i790, matching2, i791) → 1661_0_plus_Return(EOS(STATIC_1661), i790, i669, 1, i790, 0, i791) | &&(=(matching1, 1), =(matching2, 0))
1591_0_plus_Return(EOS(STATIC_1591), matching1, i795, i796) → 1666_0_plus_Return(EOS(STATIC_1666), 1, i795, i796) | =(matching1, 1)
1646_0_plus_Return(EOS(STATIC_1646), i859, i669, matching1, i859, i859, i861) → 1719_0_plus_Return(EOS(STATIC_1719), i859, i669, 1, i859, i859, i861) | =(matching1, 1)
1661_0_plus_Return(EOS(STATIC_1661), i884, i669, matching1, i884, matching2, i885) → 1733_0_plus_Return(EOS(STATIC_1733), i884, i669, 1, i884, 0, i885) | &&(=(matching1, 1), =(matching2, 0))
1666_0_plus_Return(EOS(STATIC_1666), matching1, i892, i893) → 1739_0_plus_Return(EOS(STATIC_1739), 1, i892, i893) | =(matching1, 1)
1719_0_plus_Return(EOS(STATIC_1719), i959, i669, matching1, i959, i959, i961) → 1742_0_plus_IntArithmetic(EOS(STATIC_1742), i959, i669, 1, i961) | =(matching1, 1)
1733_0_plus_Return(EOS(STATIC_1733), i983, i669, matching1, i983, matching2, i984) → 1800_0_plus_Return(EOS(STATIC_1800), i983, i669, 1, i983, 0, i984) | &&(=(matching1, 1), =(matching2, 0))
1739_0_plus_Return(EOS(STATIC_1739), matching1, i991, i992) → 1806_0_plus_Return(EOS(STATIC_1806), 1, i991, i992) | =(matching1, 1)
1742_0_plus_IntArithmetic(EOS(STATIC_1742), i959, i669, matching1, i961) → 1749_0_plus_Return(EOS(STATIC_1749), i959, i669, +(1, i961)) | &&(>(i961, 0), =(matching1, 1))
1786_0_plus_Return(EOS(STATIC_1786), i1028, i669, matching1, i1028, i1028, i1004) → 1719_0_plus_Return(EOS(STATIC_1719), i1028, i669, 1, i1028, i1028, i1004) | =(matching1, 1)
1800_0_plus_Return(EOS(STATIC_1800), i1069, i669, matching1, i1069, matching2, i1070) → 1809_0_plus_IntArithmetic(EOS(STATIC_1809), i1069, i669, 1, i1070) | &&(=(matching1, 1), =(matching2, 0))
1806_0_plus_Return(EOS(STATIC_1806), matching1, i1077, i1078) → 1811_0_plus_IntArithmetic(EOS(STATIC_1811), 1, i1078) | =(matching1, 1)
1809_0_plus_IntArithmetic(EOS(STATIC_1809), i1069, i669, matching1, i1070) → 1813_0_plus_Return(EOS(STATIC_1813), i1069, i669, +(1, i1070)) | &&(>(i1070, 0), =(matching1, 1))
1811_0_plus_IntArithmetic(EOS(STATIC_1811), matching1, i1078) → 1815_0_plus_Return(EOS(STATIC_1815), +(1, i1078)) | &&(>(i1078, 0), =(matching1, 1))
1837_0_plus_Return(EOS(STATIC_1837), i1106, i669, matching1, i1106, i1106, i1090) → 1719_0_plus_Return(EOS(STATIC_1719), i1106, i669, 1, i1106, i1106, i1090) | =(matching1, 1)
1841_0_plus_Return(EOS(STATIC_1841), i1112, i669, matching1, i1112, matching2, i1091) → 1800_0_plus_Return(EOS(STATIC_1800), i1112, i669, 1, i1112, 0, i1091) | &&(=(matching1, 1), =(matching2, 0))
1843_0_plus_Return(EOS(STATIC_1843), matching1, i1115, i1091) → 1806_0_plus_Return(EOS(STATIC_1806), 1, i1115, i1091) | =(matching1, 1)

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

P rules:
270_0_times_NE(EOS(STATIC_270), x0, x1, x1) → 373_1_times_InvokeMethod(270_0_times_NE(EOS(STATIC_270), x0, -(x1, 1), -(x1, 1)), x0, x0, -(x1, 1)) | >(x1, 0)
R rules:
270_0_times_NE(EOS(STATIC_270), x0, 0, 0) → 302_0_times_Return(EOS(STATIC_302), x0, 0, 0)
373_1_times_InvokeMethod(302_0_times_Return(EOS(STATIC_302), x0, 0, 0), x0, x0, 0) → 1423_1_times_InvokeMethod(1429_0_plus_LE(EOS(STATIC_1429), 0, x0, x0), 0, x0)
373_1_times_InvokeMethod(1465_0_times_Return(EOS(STATIC_1465), 0), 0, 0, x3) → 1423_1_times_InvokeMethod(1429_0_plus_LE(EOS(STATIC_1429), 0, 0, 0), 0, 0)
373_1_times_InvokeMethod(1740_0_times_Return(EOS(STATIC_1740), x0), x1, x1, x2) → 1423_1_times_InvokeMethod(1429_0_plus_LE(EOS(STATIC_1429), x0, x1, x1), x0, x1)
373_1_times_InvokeMethod(1808_0_times_Return(EOS(STATIC_1808), x0), 0, 0, x3) → 1423_1_times_InvokeMethod(1429_0_plus_LE(EOS(STATIC_1429), x0, 0, 0), x0, 0)
1423_1_times_InvokeMethod(1447_0_plus_Return(EOS(STATIC_1447), 0), x1, x2) → 1465_0_times_Return(EOS(STATIC_1465), 0)
1423_1_times_InvokeMethod(1749_0_plus_Return(EOS(STATIC_1749), x0, x1, x2), x0, x1) → 1740_0_times_Return(EOS(STATIC_1740), x2)
1423_1_times_InvokeMethod(1813_0_plus_Return(EOS(STATIC_1813), x0, x1, x2), x0, x1) → 1740_0_times_Return(EOS(STATIC_1740), x2)
1423_1_times_InvokeMethod(1485_0_plus_Return(EOS(STATIC_1485), x0, x1, 1), x0, x1) → 1740_0_times_Return(EOS(STATIC_1740), 1)
1423_1_times_InvokeMethod(1815_0_plus_Return(EOS(STATIC_1815), x0), x1, x2) → 1808_0_times_Return(EOS(STATIC_1808), x0)
1423_1_times_InvokeMethod(1494_0_plus_Return(EOS(STATIC_1494), 1), x1, x2) → 1808_0_times_Return(EOS(STATIC_1808), 1)
1429_0_plus_LE(EOS(STATIC_1429), x0, x1, x1) → 1447_0_plus_Return(EOS(STATIC_1447), 0) | &&(<=(x1, 0), <=(x0, 0))
1429_0_plus_LE(EOS(STATIC_1429), x0, x1, x1) → 1459_1_plus_InvokeMethod(1429_0_plus_LE(EOS(STATIC_1429), x0, x2, x2), x0, x1, 1, x0) | >(x1, 0)
1429_0_plus_LE(EOS(STATIC_1429), x0, x1, x1) → 1469_1_plus_InvokeMethod(1429_0_plus_LE(EOS(STATIC_1429), x2, x1, x1), 1, x1) | &&(<=(x1, 0), >(x0, 0))
1459_1_plus_InvokeMethod(1447_0_plus_Return(EOS(STATIC_1447), 0), x1, x2, 1, x1) → 1485_0_plus_Return(EOS(STATIC_1485), x1, x2, 1)
1469_1_plus_InvokeMethod(1447_0_plus_Return(EOS(STATIC_1447), 0), 1, x2) → 1494_0_plus_Return(EOS(STATIC_1494), 1)
1459_1_plus_InvokeMethod(1749_0_plus_Return(EOS(STATIC_1749), x0, x1, x2), x0, x3, 1, x0) → 1749_0_plus_Return(EOS(STATIC_1749), x0, x3, +(1, x2)) | >(x2, 0)
1459_1_plus_InvokeMethod(1813_0_plus_Return(EOS(STATIC_1813), x0, x1, x2), x0, x3, 1, x0) → 1749_0_plus_Return(EOS(STATIC_1749), x0, x3, +(1, x2)) | >(x2, 0)
1459_1_plus_InvokeMethod(1485_0_plus_Return(EOS(STATIC_1485), x0, x1, 1), x0, x3, 1, x0) → 1749_0_plus_Return(EOS(STATIC_1749), x0, x3, 2)
1459_1_plus_InvokeMethod(1815_0_plus_Return(EOS(STATIC_1815), x0), x1, x2, 1, x1) → 1813_0_plus_Return(EOS(STATIC_1813), x1, x2, +(1, x0)) | >(x0, 0)
1459_1_plus_InvokeMethod(1494_0_plus_Return(EOS(STATIC_1494), 1), x1, x2, 1, x1) → 1813_0_plus_Return(EOS(STATIC_1813), x1, x2, 2)
1469_1_plus_InvokeMethod(1815_0_plus_Return(EOS(STATIC_1815), x0), 1, x2) → 1815_0_plus_Return(EOS(STATIC_1815), +(1, x0)) | >(x0, 0)
1469_1_plus_InvokeMethod(1494_0_plus_Return(EOS(STATIC_1494), 1), 1, x2) → 1815_0_plus_Return(EOS(STATIC_1815), 2)

Filtered ground terms:

270_0_times_NE(x1, x2, x3, x4) → 270_0_times_NE(x2, x3, x4)
Cond_270_0_times_NE(x1, x2, x3, x4, x5) → Cond_270_0_times_NE(x1, x3, x4, x5)
1815_0_plus_Return(x1, x2) → 1815_0_plus_Return(x2)
1469_1_plus_InvokeMethod(x1, x2, x3) → 1469_1_plus_InvokeMethod(x1, x3)
1494_0_plus_Return(x1, x2) → 1494_0_plus_Return
Cond_1469_1_plus_InvokeMethod(x1, x2, x3, x4) → Cond_1469_1_plus_InvokeMethod(x1, x2, x4)
1813_0_plus_Return(x1, x2, x3, x4) → 1813_0_plus_Return(x2, x3, x4)
1459_1_plus_InvokeMethod(x1, x2, x3, x4, x5) → 1459_1_plus_InvokeMethod(x1, x2, x3, x5)
Cond_1459_1_plus_InvokeMethod2(x1, x2, x3, x4, x5, x6) → Cond_1459_1_plus_InvokeMethod2(x1, x2, x3, x4, x6)
1749_0_plus_Return(x1, x2, x3, x4) → 1749_0_plus_Return(x2, x3, x4)
1485_0_plus_Return(x1, x2, x3, x4) → 1485_0_plus_Return(x2, x3)
Cond_1459_1_plus_InvokeMethod1(x1, x2, x3, x4, x5, x6) → Cond_1459_1_plus_InvokeMethod1(x1, x2, x3, x4, x6)
Cond_1459_1_plus_InvokeMethod(x1, x2, x3, x4, x5, x6) → Cond_1459_1_plus_InvokeMethod(x1, x2, x3, x4, x6)
1447_0_plus_Return(x1, x2) → 1447_0_plus_Return
1429_0_plus_LE(x1, x2, x3, x4) → 1429_0_plus_LE(x2, x3, x4)
Cond_1429_0_plus_LE2(x1, x2, x3, x4, x5, x6) → Cond_1429_0_plus_LE2(x1, x3, x4, x5, x6)
Cond_1429_0_plus_LE1(x1, x2, x3, x4, x5, x6) → Cond_1429_0_plus_LE1(x1, x3, x4, x5, x6)
Cond_1429_0_plus_LE(x1, x2, x3, x4, x5) → Cond_1429_0_plus_LE(x1, x3, x4, x5)
1808_0_times_Return(x1, x2) → 1808_0_times_Return(x2)
1740_0_times_Return(x1, x2) → 1740_0_times_Return(x2)
1465_0_times_Return(x1, x2) → 1465_0_times_Return
302_0_times_Return(x1, x2, x3, x4) → 302_0_times_Return(x2)

Filtered duplicate args:

270_0_times_NE(x1, x2, x3) → 270_0_times_NE(x1, x3)
Cond_270_0_times_NE(x1, x2, x3, x4) → Cond_270_0_times_NE(x1, x2, x4)
373_1_times_InvokeMethod(x1, x2, x3, x4) → 373_1_times_InvokeMethod(x1, x3, x4)
1429_0_plus_LE(x1, x2, x3) → 1429_0_plus_LE(x1, x3)
Cond_1429_0_plus_LE(x1, x2, x3, x4) → Cond_1429_0_plus_LE(x1, x2, x4)
Cond_1429_0_plus_LE1(x1, x2, x3, x4, x5) → Cond_1429_0_plus_LE1(x1, x2, x4, x5)
1459_1_plus_InvokeMethod(x1, x2, x3, x4) → 1459_1_plus_InvokeMethod(x1, x3, x4)
Cond_1429_0_plus_LE2(x1, x2, x3, x4, x5) → Cond_1429_0_plus_LE2(x1, x2, x4, x5)
Cond_1459_1_plus_InvokeMethod(x1, x2, x3, x4, x5) → Cond_1459_1_plus_InvokeMethod(x1, x2, x4)
Cond_1459_1_plus_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_1459_1_plus_InvokeMethod1(x1, x2, x4)
Cond_1459_1_plus_InvokeMethod2(x1, x2, x3, x4, x5) → Cond_1459_1_plus_InvokeMethod2(x1, x2, x4, x5)

Filtered unneeded arguments:

1423_1_times_InvokeMethod(x1, x2, x3) → 1423_1_times_InvokeMethod(x1)
Cond_1429_0_plus_LE(x1, x2, x3) → Cond_1429_0_plus_LE(x1)
Cond_1429_0_plus_LE1(x1, x2, x3, x4) → Cond_1429_0_plus_LE1(x1, x2, x4)
1459_1_plus_InvokeMethod(x1, x2, x3) → 1459_1_plus_InvokeMethod(x1)
Cond_1429_0_plus_LE2(x1, x2, x3, x4) → Cond_1429_0_plus_LE2(x1, x3, x4)
1469_1_plus_InvokeMethod(x1, x2) → 1469_1_plus_InvokeMethod(x1)
Cond_1459_1_plus_InvokeMethod(x1, x2, x3) → Cond_1459_1_plus_InvokeMethod(x1, x2)
Cond_1459_1_plus_InvokeMethod1(x1, x2, x3) → Cond_1459_1_plus_InvokeMethod1(x1, x2)
Cond_1459_1_plus_InvokeMethod2(x1, x2, x3, x4) → Cond_1459_1_plus_InvokeMethod2(x1, x2)
Cond_1469_1_plus_InvokeMethod(x1, x2, x3) → Cond_1469_1_plus_InvokeMethod(x1, x2)
1749_0_plus_Return(x1, x2, x3) → 1749_0_plus_Return(x3)
1813_0_plus_Return(x1, x2, x3) → 1813_0_plus_Return(x3)

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

P rules:
270_0_times_NE(x0, x1) → 373_1_times_InvokeMethod(270_0_times_NE(x0, -(x1, 1)), x0, -(x1, 1)) | >(x1, 0)
R rules:
270_0_times_NE(x0, 0) → 302_0_times_Return(x0)
373_1_times_InvokeMethod(302_0_times_Return(x0), x0, 0) → 1423_1_times_InvokeMethod(1429_0_plus_LE(0, x0))
373_1_times_InvokeMethod(1465_0_times_Return, 0, x3) → 1423_1_times_InvokeMethod(1429_0_plus_LE(0, 0))
373_1_times_InvokeMethod(1740_0_times_Return(x0), x1, x2) → 1423_1_times_InvokeMethod(1429_0_plus_LE(x0, x1))
373_1_times_InvokeMethod(1808_0_times_Return(x0), 0, x3) → 1423_1_times_InvokeMethod(1429_0_plus_LE(x0, 0))
1423_1_times_InvokeMethod(1447_0_plus_Return) → 1465_0_times_Return
1423_1_times_InvokeMethod(1749_0_plus_Return(x2)) → 1740_0_times_Return(x2)
1423_1_times_InvokeMethod(1813_0_plus_Return(x2)) → 1740_0_times_Return(x2)
1423_1_times_InvokeMethod(1485_0_plus_Return(x0, x1)) → 1740_0_times_Return(1)
1423_1_times_InvokeMethod(1815_0_plus_Return(x0)) → 1808_0_times_Return(x0)
1423_1_times_InvokeMethod(1494_0_plus_Return) → 1808_0_times_Return(1)
1429_0_plus_LE(x0, x1) → 1447_0_plus_Return | &&(<=(x1, 0), <=(x0, 0))
1429_0_plus_LE(x0, x1) → 1459_1_plus_InvokeMethod(1429_0_plus_LE(x0, x2)) | >(x1, 0)
1429_0_plus_LE(x0, x1) → 1469_1_plus_InvokeMethod(1429_0_plus_LE(x2, x1)) | &&(<=(x1, 0), >(x0, 0))
1459_1_plus_InvokeMethod(1447_0_plus_Return) → 1485_0_plus_Return(x1, x2)
1469_1_plus_InvokeMethod(1447_0_plus_Return) → 1494_0_plus_Return
1459_1_plus_InvokeMethod(1749_0_plus_Return(x2)) → 1749_0_plus_Return(+(1, x2)) | >(x2, 0)
1459_1_plus_InvokeMethod(1813_0_plus_Return(x2)) → 1749_0_plus_Return(+(1, x2)) | >(x2, 0)
1459_1_plus_InvokeMethod(1485_0_plus_Return(x0, x1)) → 1749_0_plus_Return(2)
1459_1_plus_InvokeMethod(1815_0_plus_Return(x0)) → 1813_0_plus_Return(+(1, x0)) | >(x0, 0)
1459_1_plus_InvokeMethod(1494_0_plus_Return) → 1813_0_plus_Return(2)
1469_1_plus_InvokeMethod(1815_0_plus_Return(x0)) → 1815_0_plus_Return(+(1, x0)) | >(x0, 0)
1469_1_plus_InvokeMethod(1494_0_plus_Return) → 1815_0_plus_Return(2)

Performed bisimulation on rules. Used the following equivalence classes: {[Cond_1459_1_plus_InvokeMethod_2, Cond_1459_1_plus_InvokeMethod1_2, Cond_1459_1_plus_InvokeMethod2_2, Cond_1469_1_plus_InvokeMethod_2]=Cond_1459_1_plus_InvokeMethod_2, [1749_0_plus_Return_1, 1813_0_plus_Return_1, 1815_0_plus_Return_1]=1749_0_plus_Return_1, [1740_0_times_Return_1, 1808_0_times_Return_1]=1740_0_times_Return_1, [1465_0_times_Return, 1447_0_plus_Return, 1494_0_plus_Return]=1465_0_times_Return}

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

P rules:
270_0_TIMES_NE(x0, x1) → COND_270_0_TIMES_NE(>(x1, 0), x0, x1)
COND_270_0_TIMES_NE(TRUE, x0, x1) → 270_0_TIMES_NE(x0, -(x1, 1))
R rules:
270_0_times_NE(x0, 0) → 302_0_times_Return(x0)
373_1_times_InvokeMethod(302_0_times_Return(x0), x0, 0) → 1423_1_times_InvokeMethod(1429_0_plus_LE(0, x0))
373_1_times_InvokeMethod(1465_0_times_Return, 0, x3) → 1423_1_times_InvokeMethod(1429_0_plus_LE(0, 0))
373_1_times_InvokeMethod(1740_0_times_Return(x0), x1, x2) → 1423_1_times_InvokeMethod(1429_0_plus_LE(x0, x1))
373_1_times_InvokeMethod(1740_0_times_Return(x0), 0, x3) → 1423_1_times_InvokeMethod(1429_0_plus_LE(x0, 0))
1423_1_times_InvokeMethod(1465_0_times_Return) → 1465_0_times_Return
1423_1_times_InvokeMethod(1749_0_plus_Return(x2)) → 1740_0_times_Return(x2)
1423_1_times_InvokeMethod(1485_0_plus_Return(x0, x1)) → 1740_0_times_Return(1)
1423_1_times_InvokeMethod(1465_0_times_Return) → 1740_0_times_Return(1)
1429_0_plus_LE(x0, x1) → Cond_1429_0_plus_LE(&&(<=(x1, 0), <=(x0, 0)), x0, x1)
Cond_1429_0_plus_LE(TRUE, x0, x1) → 1465_0_times_Return
1429_0_plus_LE(x0, x1) → Cond_1429_0_plus_LE1(>(x1, 0), x0, x1, x2)
Cond_1429_0_plus_LE1(TRUE, x0, x1, x2) → 1459_1_plus_InvokeMethod(1429_0_plus_LE(x0, x2))
1429_0_plus_LE(x0, x1) → Cond_1429_0_plus_LE2(&&(<=(x1, 0), >(x0, 0)), x0, x1, x2)
Cond_1429_0_plus_LE2(TRUE, x0, x1, x2) → 1469_1_plus_InvokeMethod(1429_0_plus_LE(x2, x1))
1459_1_plus_InvokeMethod(1465_0_times_Return) → 1485_0_plus_Return(x1, x2)
1469_1_plus_InvokeMethod(1465_0_times_Return) → 1465_0_times_Return
1459_1_plus_InvokeMethod(1749_0_plus_Return(x2)) → Cond_1459_1_plus_InvokeMethod(>(x2, 0), 1749_0_plus_Return(x2))
Cond_1459_1_plus_InvokeMethod(TRUE, 1749_0_plus_Return(x2)) → 1749_0_plus_Return(+(1, x2))
1459_1_plus_InvokeMethod(1485_0_plus_Return(x0, x1)) → 1749_0_plus_Return(2)
1459_1_plus_InvokeMethod(1465_0_times_Return) → 1749_0_plus_Return(2)
1469_1_plus_InvokeMethod(1749_0_plus_Return(x0)) → Cond_1459_1_plus_InvokeMethod(>(x0, 0), 1749_0_plus_Return(x0))
1469_1_plus_InvokeMethod(1465_0_times_Return) → 1749_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:
270_0_times_NE(x0, 0) → 302_0_times_Return(x0)
373_1_times_InvokeMethod(302_0_times_Return(x0), x0, 0) → 1423_1_times_InvokeMethod(1429_0_plus_LE(0, x0))
373_1_times_InvokeMethod(1465_0_times_Return, 0, x3) → 1423_1_times_InvokeMethod(1429_0_plus_LE(0, 0))
373_1_times_InvokeMethod(1740_0_times_Return(x0), x1, x2) → 1423_1_times_InvokeMethod(1429_0_plus_LE(x0, x1))
373_1_times_InvokeMethod(1740_0_times_Return(x0), 0, x3) → 1423_1_times_InvokeMethod(1429_0_plus_LE(x0, 0))
1423_1_times_InvokeMethod(1465_0_times_Return) → 1465_0_times_Return
1423_1_times_InvokeMethod(1749_0_plus_Return(x2)) → 1740_0_times_Return(x2)
1423_1_times_InvokeMethod(1485_0_plus_Return(x0, x1)) → 1740_0_times_Return(1)
1423_1_times_InvokeMethod(1465_0_times_Return) → 1740_0_times_Return(1)
1429_0_plus_LE(x0, x1) → Cond_1429_0_plus_LE(x1 <= 0 && x0 <= 0, x0, x1)
Cond_1429_0_plus_LE(TRUE, x0, x1) → 1465_0_times_Return
1429_0_plus_LE(x0, x1) → Cond_1429_0_plus_LE1(x1 > 0, x0, x1, x2)
Cond_1429_0_plus_LE1(TRUE, x0, x1, x2) → 1459_1_plus_InvokeMethod(1429_0_plus_LE(x0, x2))
1429_0_plus_LE(x0, x1) → Cond_1429_0_plus_LE2(x1 <= 0 && x0 > 0, x0, x1, x2)
Cond_1429_0_plus_LE2(TRUE, x0, x1, x2) → 1469_1_plus_InvokeMethod(1429_0_plus_LE(x2, x1))
1459_1_plus_InvokeMethod(1465_0_times_Return) → 1485_0_plus_Return(x1, x2)
1469_1_plus_InvokeMethod(1465_0_times_Return) → 1465_0_times_Return
1459_1_plus_InvokeMethod(1749_0_plus_Return(x2)) → Cond_1459_1_plus_InvokeMethod(x2 > 0, 1749_0_plus_Return(x2))
Cond_1459_1_plus_InvokeMethod(TRUE, 1749_0_plus_Return(x2)) → 1749_0_plus_Return(1 + x2)
1459_1_plus_InvokeMethod(1485_0_plus_Return(x0, x1)) → 1749_0_plus_Return(2)
1459_1_plus_InvokeMethod(1465_0_times_Return) → 1749_0_plus_Return(2)
1469_1_plus_InvokeMethod(1749_0_plus_Return(x0)) → Cond_1459_1_plus_InvokeMethod(x0 > 0, 1749_0_plus_Return(x0))
1469_1_plus_InvokeMethod(1465_0_times_Return) → 1749_0_plus_Return(2)

The integer pair graph contains the following rules and edges:
(0): 270_0_TIMES_NE(x0[0], x1[0]) → COND_270_0_TIMES_NE(x1[0] > 0, x0[0], x1[0])
(1): COND_270_0_TIMES_NE(TRUE, x0[1], x1[1]) → 270_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:
270_0_times_NE(x0, 0)
373_1_times_InvokeMethod(302_0_times_Return(x0), x0, 0)
373_1_times_InvokeMethod(1465_0_times_Return, 0, x0)
373_1_times_InvokeMethod(1740_0_times_Return(x0), x1, x2)
1423_1_times_InvokeMethod(1465_0_times_Return)
1423_1_times_InvokeMethod(1749_0_plus_Return(x0))
1423_1_times_InvokeMethod(1485_0_plus_Return(x0, x1))
1429_0_plus_LE(x0, x1)
Cond_1429_0_plus_LE(TRUE, x0, x1)
Cond_1429_0_plus_LE1(TRUE, x0, x1, x2)
Cond_1429_0_plus_LE2(TRUE, x0, x1, x2)
1459_1_plus_InvokeMethod(1465_0_times_Return)
1469_1_plus_InvokeMethod(1465_0_times_Return)
1459_1_plus_InvokeMethod(1749_0_plus_Return(x0))
Cond_1459_1_plus_InvokeMethod(TRUE, 1749_0_plus_Return(x0))
1459_1_plus_InvokeMethod(1485_0_plus_Return(x0, x1))
1469_1_plus_InvokeMethod(1749_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@4725d9b 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 270_0_TIMES_NE(x0, x1) → COND_270_0_TIMES_NE(>(x1, 0), x0, x1) the following chains were created:

We consider the chain 270_0_TIMES_NE(x0[0], x1[0]) → COND_270_0_TIMES_NE(>(x1[0], 0), x0[0], x1[0]), COND_270_0_TIMES_NE(TRUE, x0[1], x1[1]) → 270_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] ⇒ 270_0_TIMES_NE(x0[0], x1[0])≥NonInfC∧270_0_TIMES_NE(x0[0], x1[0])≥COND_270_0_TIMES_NE(>(x1[0], 0), x0[0], x1[0])∧(U^Increasing(COND_270_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 ⇒ 270_0_TIMES_NE(x0[0], x1[0])≥NonInfC∧270_0_TIMES_NE(x0[0], x1[0])≥COND_270_0_TIMES_NE(>(x1[0], 0), x0[0], x1[0])∧(U^Increasing(COND_270_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_270_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_270_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_270_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_270_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_270_0_TIMES_NE(TRUE, x0, x1) → 270_0_TIMES_NE(x0, -(x1, 1)) the following chains were created:

We consider the chain COND_270_0_TIMES_NE(TRUE, x0[1], x1[1]) → 270_0_TIMES_NE(x0[1], -(x1[1], 1)) which results in the following constraint:
(7)    (COND_270_0_TIMES_NE(TRUE, x0[1], x1[1])≥NonInfC∧COND_270_0_TIMES_NE(TRUE, x0[1], x1[1])≥270_0_TIMES_NE(x0[1], -(x1[1], 1))∧(U^Increasing(270_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(270_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(270_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(270_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(270_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.

270_0_TIMES_NE(x0, x1) → COND_270_0_TIMES_NE(>(x1, 0), x0, x1)
- (x1[0] ≥ 0 ⇒ (U^Increasing(COND_270_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_270_0_TIMES_NE(TRUE, x0, x1) → 270_0_TIMES_NE(x0, -(x1, 1))
- ((U^Increasing(270_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(270_0_times_NE(x₁, x₂)) = [-1]
POL(0) = 0
POL(302_0_times_Return(x₁)) = [-1]
POL(373_1_times_InvokeMethod(x₁, x₂, x₃)) = [-1]
POL(1423_1_times_InvokeMethod(x₁)) = [-1]
POL(1429_0_plus_LE(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁
POL(1465_0_times_Return) = [-1]
POL(1740_0_times_Return(x₁)) = [-1]
POL(1749_0_plus_Return(x₁)) = x₁
POL(1485_0_plus_Return(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁
POL(1) = [1]
POL(Cond_1429_0_plus_LE(x₁, x₂, x₃)) = [-1] + [-1]x₃ + [-1]x₂
POL(&&(x₁, x₂)) = [-1]
POL(<=(x₁, x₂)) = [-1]
POL(Cond_1429_0_plus_LE1(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + [-1]x₂
POL(>(x₁, x₂)) = [-1]
POL(1459_1_plus_InvokeMethod(x₁)) = [-1] + [-1]x₁
POL(Cond_1429_0_plus_LE2(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + [-1]x₂
POL(1469_1_plus_InvokeMethod(x₁)) = [-1] + [-1]x₁
POL(Cond_1459_1_plus_InvokeMethod(x₁, x₂)) = [-1] + [-1]x₂
POL(+(x₁, x₂)) = x₁ + x₂
POL(2) = [2]
POL(270_0_TIMES_NE(x₁, x₂)) = [2]x₂
POL(COND_270_0_TIMES_NE(x₁, x₂, x₃)) = [2]x₃
POL(-(x₁, x₂)) = x₁ + [-1]x₂

The following pairs are in P_>:

COND_270_0_TIMES_NE(TRUE, x0[1], x1[1]) → 270_0_TIMES_NE(x0[1], -(x1[1], 1))

The following pairs are in P_bound:

270_0_TIMES_NE(x0[0], x1[0]) → COND_270_0_TIMES_NE(>(x1[0], 0), x0[0], x1[0])

The following pairs are in P_≥:

270_0_TIMES_NE(x0[0], x1[0]) → COND_270_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:
270_0_times_NE(x0, 0) → 302_0_times_Return(x0)
373_1_times_InvokeMethod(302_0_times_Return(x0), x0, 0) → 1423_1_times_InvokeMethod(1429_0_plus_LE(0, x0))
373_1_times_InvokeMethod(1465_0_times_Return, 0, x3) → 1423_1_times_InvokeMethod(1429_0_plus_LE(0, 0))
373_1_times_InvokeMethod(1740_0_times_Return(x0), x1, x2) → 1423_1_times_InvokeMethod(1429_0_plus_LE(x0, x1))
373_1_times_InvokeMethod(1740_0_times_Return(x0), 0, x3) → 1423_1_times_InvokeMethod(1429_0_plus_LE(x0, 0))
1423_1_times_InvokeMethod(1465_0_times_Return) → 1465_0_times_Return
1423_1_times_InvokeMethod(1749_0_plus_Return(x2)) → 1740_0_times_Return(x2)
1423_1_times_InvokeMethod(1485_0_plus_Return(x0, x1)) → 1740_0_times_Return(1)
1423_1_times_InvokeMethod(1465_0_times_Return) → 1740_0_times_Return(1)
1429_0_plus_LE(x0, x1) → Cond_1429_0_plus_LE(x1 <= 0 && x0 <= 0, x0, x1)
Cond_1429_0_plus_LE(TRUE, x0, x1) → 1465_0_times_Return
1429_0_plus_LE(x0, x1) → Cond_1429_0_plus_LE1(x1 > 0, x0, x1, x2)
Cond_1429_0_plus_LE1(TRUE, x0, x1, x2) → 1459_1_plus_InvokeMethod(1429_0_plus_LE(x0, x2))
1429_0_plus_LE(x0, x1) → Cond_1429_0_plus_LE2(x1 <= 0 && x0 > 0, x0, x1, x2)
Cond_1429_0_plus_LE2(TRUE, x0, x1, x2) → 1469_1_plus_InvokeMethod(1429_0_plus_LE(x2, x1))
1459_1_plus_InvokeMethod(1465_0_times_Return) → 1485_0_plus_Return(x1, x2)
1469_1_plus_InvokeMethod(1465_0_times_Return) → 1465_0_times_Return
1459_1_plus_InvokeMethod(1749_0_plus_Return(x2)) → Cond_1459_1_plus_InvokeMethod(x2 > 0, 1749_0_plus_Return(x2))
Cond_1459_1_plus_InvokeMethod(TRUE, 1749_0_plus_Return(x2)) → 1749_0_plus_Return(1 + x2)
1459_1_plus_InvokeMethod(1485_0_plus_Return(x0, x1)) → 1749_0_plus_Return(2)
1459_1_plus_InvokeMethod(1465_0_times_Return) → 1749_0_plus_Return(2)
1469_1_plus_InvokeMethod(1749_0_plus_Return(x0)) → Cond_1459_1_plus_InvokeMethod(x0 > 0, 1749_0_plus_Return(x0))
1469_1_plus_InvokeMethod(1465_0_times_Return) → 1749_0_plus_Return(2)

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

The set Q consists of the following terms:
270_0_times_NE(x0, 0)
373_1_times_InvokeMethod(302_0_times_Return(x0), x0, 0)
373_1_times_InvokeMethod(1465_0_times_Return, 0, x0)
373_1_times_InvokeMethod(1740_0_times_Return(x0), x1, x2)
1423_1_times_InvokeMethod(1465_0_times_Return)
1423_1_times_InvokeMethod(1749_0_plus_Return(x0))
1423_1_times_InvokeMethod(1485_0_plus_Return(x0, x1))
1429_0_plus_LE(x0, x1)
Cond_1429_0_plus_LE(TRUE, x0, x1)
Cond_1429_0_plus_LE1(TRUE, x0, x1, x2)
Cond_1429_0_plus_LE2(TRUE, x0, x1, x2)
1459_1_plus_InvokeMethod(1465_0_times_Return)
1469_1_plus_InvokeMethod(1465_0_times_Return)
1459_1_plus_InvokeMethod(1749_0_plus_Return(x0))
Cond_1459_1_plus_InvokeMethod(TRUE, 1749_0_plus_Return(x0))
1459_1_plus_InvokeMethod(1485_0_plus_Return(x0, x1))
1469_1_plus_InvokeMethod(1749_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:
270_0_times_NE(x0, 0) → 302_0_times_Return(x0)
373_1_times_InvokeMethod(302_0_times_Return(x0), x0, 0) → 1423_1_times_InvokeMethod(1429_0_plus_LE(0, x0))
373_1_times_InvokeMethod(1465_0_times_Return, 0, x3) → 1423_1_times_InvokeMethod(1429_0_plus_LE(0, 0))
373_1_times_InvokeMethod(1740_0_times_Return(x0), x1, x2) → 1423_1_times_InvokeMethod(1429_0_plus_LE(x0, x1))
373_1_times_InvokeMethod(1740_0_times_Return(x0), 0, x3) → 1423_1_times_InvokeMethod(1429_0_plus_LE(x0, 0))
1423_1_times_InvokeMethod(1465_0_times_Return) → 1465_0_times_Return
1423_1_times_InvokeMethod(1749_0_plus_Return(x2)) → 1740_0_times_Return(x2)
1423_1_times_InvokeMethod(1485_0_plus_Return(x0, x1)) → 1740_0_times_Return(1)
1423_1_times_InvokeMethod(1465_0_times_Return) → 1740_0_times_Return(1)
1429_0_plus_LE(x0, x1) → Cond_1429_0_plus_LE(x1 <= 0 && x0 <= 0, x0, x1)
Cond_1429_0_plus_LE(TRUE, x0, x1) → 1465_0_times_Return
1429_0_plus_LE(x0, x1) → Cond_1429_0_plus_LE1(x1 > 0, x0, x1, x2)
Cond_1429_0_plus_LE1(TRUE, x0, x1, x2) → 1459_1_plus_InvokeMethod(1429_0_plus_LE(x0, x2))
1429_0_plus_LE(x0, x1) → Cond_1429_0_plus_LE2(x1 <= 0 && x0 > 0, x0, x1, x2)
Cond_1429_0_plus_LE2(TRUE, x0, x1, x2) → 1469_1_plus_InvokeMethod(1429_0_plus_LE(x2, x1))
1459_1_plus_InvokeMethod(1465_0_times_Return) → 1485_0_plus_Return(x1, x2)
1469_1_plus_InvokeMethod(1465_0_times_Return) → 1465_0_times_Return
1459_1_plus_InvokeMethod(1749_0_plus_Return(x2)) → Cond_1459_1_plus_InvokeMethod(x2 > 0, 1749_0_plus_Return(x2))
Cond_1459_1_plus_InvokeMethod(TRUE, 1749_0_plus_Return(x2)) → 1749_0_plus_Return(1 + x2)
1459_1_plus_InvokeMethod(1485_0_plus_Return(x0, x1)) → 1749_0_plus_Return(2)
1459_1_plus_InvokeMethod(1465_0_times_Return) → 1749_0_plus_Return(2)
1469_1_plus_InvokeMethod(1749_0_plus_Return(x0)) → Cond_1459_1_plus_InvokeMethod(x0 > 0, 1749_0_plus_Return(x0))
1469_1_plus_InvokeMethod(1465_0_times_Return) → 1749_0_plus_Return(2)

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

The set Q consists of the following terms:
270_0_times_NE(x0, 0)
373_1_times_InvokeMethod(302_0_times_Return(x0), x0, 0)
373_1_times_InvokeMethod(1465_0_times_Return, 0, x0)
373_1_times_InvokeMethod(1740_0_times_Return(x0), x1, x2)
1423_1_times_InvokeMethod(1465_0_times_Return)
1423_1_times_InvokeMethod(1749_0_plus_Return(x0))
1423_1_times_InvokeMethod(1485_0_plus_Return(x0, x1))
1429_0_plus_LE(x0, x1)
Cond_1429_0_plus_LE(TRUE, x0, x1)
Cond_1429_0_plus_LE1(TRUE, x0, x1, x2)
Cond_1429_0_plus_LE2(TRUE, x0, x1, x2)
1459_1_plus_InvokeMethod(1465_0_times_Return)
1469_1_plus_InvokeMethod(1465_0_times_Return)
1459_1_plus_InvokeMethod(1749_0_plus_Return(x0))
Cond_1459_1_plus_InvokeMethod(TRUE, 1749_0_plus_Return(x0))
1459_1_plus_InvokeMethod(1485_0_plus_Return(x0, x1))
1469_1_plus_InvokeMethod(1749_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