Termination of the given JBC could be proven:

(0) Obligation:

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

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

	public static boolean eq(int x, int y) {
		if (x > 0 && y > 0) {
			return eq(x-1, y-1);
		} else {
			return (x == 0 && y == 0);
		}
	}
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

EqUserDefRec.eq(II)Z: Graph of 45 nodes with 0 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 1 SCCs.

(4) Obligation:

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

(5) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 15 rules for P and 30 rules for R.

P rules:
253_0_eq_LE(EOS(STATIC_253), i42, i37, i42) → 260_0_eq_LE(EOS(STATIC_260), i42, i37, i42)
260_0_eq_LE(EOS(STATIC_260), i42, i37, i42) → 270_0_eq_Load(EOS(STATIC_270), i42, i37) | >(i42, 0)
270_0_eq_Load(EOS(STATIC_270), i42, i37) → 284_0_eq_LE(EOS(STATIC_284), i42, i37, i37)
284_0_eq_LE(EOS(STATIC_284), i42, i46, i46) → 293_0_eq_LE(EOS(STATIC_293), i42, i46, i46)
293_0_eq_LE(EOS(STATIC_293), i42, i46, i46) → 306_0_eq_Load(EOS(STATIC_306), i42, i46) | >(i46, 0)
306_0_eq_Load(EOS(STATIC_306), i42, i46) → 320_0_eq_ConstantStackPush(EOS(STATIC_320), i42, i46, i42)
320_0_eq_ConstantStackPush(EOS(STATIC_320), i42, i46, i42) → 337_0_eq_IntArithmetic(EOS(STATIC_337), i42, i46, i42, 1)
337_0_eq_IntArithmetic(EOS(STATIC_337), i42, i46, i42, matching1) → 355_0_eq_Load(EOS(STATIC_355), i42, i46, -(i42, 1)) | &&(>(i42, 0), =(matching1, 1))
355_0_eq_Load(EOS(STATIC_355), i42, i46, i53) → 374_0_eq_ConstantStackPush(EOS(STATIC_374), i42, i46, i53, i46)
374_0_eq_ConstantStackPush(EOS(STATIC_374), i42, i46, i53, i46) → 407_0_eq_IntArithmetic(EOS(STATIC_407), i42, i46, i53, i46, 1)
407_0_eq_IntArithmetic(EOS(STATIC_407), i42, i46, i53, i46, matching1) → 440_0_eq_InvokeMethod(EOS(STATIC_440), i42, i46, i53, -(i46, 1)) | &&(>(i46, 0), =(matching1, 1))
440_0_eq_InvokeMethod(EOS(STATIC_440), i42, i46, i53, i65) → 459_1_eq_InvokeMethod(459_0_eq_Load(EOS(STATIC_459), i53, i65), i42, i46, i53, i65)
459_0_eq_Load(EOS(STATIC_459), i53, i65) → 463_0_eq_Load(EOS(STATIC_463), i53, i65)
463_0_eq_Load(EOS(STATIC_463), i53, i65) → 244_0_eq_Load(EOS(STATIC_244), i53, i65)
244_0_eq_Load(EOS(STATIC_244), i13, i37) → 253_0_eq_LE(EOS(STATIC_253), i13, i37, i13)
R rules:
253_0_eq_LE(EOS(STATIC_253), matching1, i37, matching2) → 259_0_eq_LE(EOS(STATIC_259), 0, i37, 0) | &&(=(matching1, 0), =(matching2, 0))
259_0_eq_LE(EOS(STATIC_259), matching1, i37, matching2) → 268_0_eq_Load(EOS(STATIC_268), 0, i37) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
268_0_eq_Load(EOS(STATIC_268), matching1, i37) → 281_0_eq_NE(EOS(STATIC_281), i37, 0) | =(matching1, 0)
281_0_eq_NE(EOS(STATIC_281), i37, matching1) → 289_0_eq_Load(EOS(STATIC_289), i37) | =(matching1, 0)
284_0_eq_LE(EOS(STATIC_284), i42, matching1, matching2) → 291_0_eq_LE(EOS(STATIC_291), i42, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
289_0_eq_Load(EOS(STATIC_289), i37) → 302_0_eq_NE(EOS(STATIC_302), i37)
291_0_eq_LE(EOS(STATIC_291), i42, matching1, matching2) → 304_0_eq_Load(EOS(STATIC_304), i42, 0) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
302_0_eq_NE(EOS(STATIC_302), i48) → 315_0_eq_NE(EOS(STATIC_315), i48)
302_0_eq_NE(EOS(STATIC_302), matching1) → 316_0_eq_NE(EOS(STATIC_316), 0) | =(matching1, 0)
304_0_eq_Load(EOS(STATIC_304), i42, matching1) → 319_0_eq_NE(EOS(STATIC_319), 0, i42) | =(matching1, 0)
315_0_eq_NE(EOS(STATIC_315), i48) → 329_0_eq_ConstantStackPush(EOS(STATIC_329)) | >(i48, 0)
316_0_eq_NE(EOS(STATIC_316), matching1) → 332_0_eq_ConstantStackPush(EOS(STATIC_332)) | =(matching1, 0)
319_0_eq_NE(EOS(STATIC_319), matching1, i42) → 334_0_eq_ConstantStackPush(EOS(STATIC_334)) | &&(>(i42, 0), =(matching1, 0))
329_0_eq_ConstantStackPush(EOS(STATIC_329)) → 347_0_eq_Return(EOS(STATIC_347), 0)
332_0_eq_ConstantStackPush(EOS(STATIC_332)) → 350_0_eq_JMP(EOS(STATIC_350), 1)
334_0_eq_ConstantStackPush(EOS(STATIC_334)) → 352_0_eq_Return(EOS(STATIC_352), 0)
350_0_eq_JMP(EOS(STATIC_350), matching1) → 369_0_eq_Return(EOS(STATIC_369), 1) | =(matching1, 1)
459_1_eq_InvokeMethod(347_0_eq_Return(EOS(STATIC_347), matching1), i42, i46, matching2, i77) → 479_0_eq_Return(EOS(STATIC_479), i42, i46, 0, i77, 0) | &&(=(matching1, 0), =(matching2, 0))
459_1_eq_InvokeMethod(352_0_eq_Return(EOS(STATIC_352), matching1), i42, i46, i79, matching2) → 483_0_eq_Return(EOS(STATIC_483), i42, i46, i79, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
459_1_eq_InvokeMethod(369_0_eq_Return(EOS(STATIC_369), matching1), i42, i46, matching2, matching3) → 492_0_eq_Return(EOS(STATIC_492), i42, i46, 0, 0, 1) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
459_1_eq_InvokeMethod(496_0_eq_Return(EOS(STATIC_496), i94, i95, i83), i42, i46, i94, i95) → 506_0_eq_Return(EOS(STATIC_506), i42, i46, i94, i95, i94, i95, i83)
459_1_eq_InvokeMethod(512_0_eq_Return(EOS(STATIC_512), i102, i103, i83), i42, i46, i102, i103) → 527_0_eq_Return(EOS(STATIC_527), i42, i46, i102, i103, i102, i103, i83)
479_0_eq_Return(EOS(STATIC_479), i42, i46, matching1, i77, matching2) → 484_0_eq_Return(EOS(STATIC_484), i42, i46, 0, i77, 0) | &&(=(matching1, 0), =(matching2, 0))
483_0_eq_Return(EOS(STATIC_483), i42, i46, i79, matching1, matching2) → 484_0_eq_Return(EOS(STATIC_484), i42, i46, i79, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
484_0_eq_Return(EOS(STATIC_484), i42, i46, i82, i81, matching1) → 493_0_eq_Return(EOS(STATIC_493), i42, i46, i82, i81, 0) | =(matching1, 0)
492_0_eq_Return(EOS(STATIC_492), i42, i46, matching1, matching2, matching3) → 493_0_eq_Return(EOS(STATIC_493), i42, i46, 0, 0, 1) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 1))
493_0_eq_Return(EOS(STATIC_493), i42, i46, i85, i84, i83) → 496_0_eq_Return(EOS(STATIC_496), i42, i46, i83)
496_0_eq_Return(EOS(STATIC_496), i42, i46, i83) → 512_0_eq_Return(EOS(STATIC_512), i42, i46, i83)
506_0_eq_Return(EOS(STATIC_506), i42, i46, i94, i95, i94, i95, i83) → 512_0_eq_Return(EOS(STATIC_512), i42, i46, i83)
527_0_eq_Return(EOS(STATIC_527), i42, i46, i102, i103, i102, i103, i83) → 506_0_eq_Return(EOS(STATIC_506), i42, i46, i102, i103, i102, i103, i83)

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

P rules:
253_0_eq_LE(EOS(STATIC_253), x0, x1, x0) → 459_1_eq_InvokeMethod(253_0_eq_LE(EOS(STATIC_253), -(x0, 1), -(x1, 1), -(x0, 1)), x0, x1, -(x0, 1), -(x1, 1)) | &&(>(x1, 0), >(x0, 0))
R rules:
253_0_eq_LE(EOS(STATIC_253), 0, x1, 0) → 347_0_eq_Return(EOS(STATIC_347), 0) | >(x1, 0)
253_0_eq_LE(EOS(STATIC_253), 0, 0, 0) → 369_0_eq_Return(EOS(STATIC_369), 1)
459_1_eq_InvokeMethod(496_0_eq_Return(EOS(STATIC_496), x0, x1, x2), x3, x4, x0, x1) → 512_0_eq_Return(EOS(STATIC_512), x3, x4, x2)
459_1_eq_InvokeMethod(512_0_eq_Return(EOS(STATIC_512), x0, x1, x2), x3, x4, x0, x1) → 512_0_eq_Return(EOS(STATIC_512), x3, x4, x2)
459_1_eq_InvokeMethod(369_0_eq_Return(EOS(STATIC_369), 1), x1, x2, 0, 0) → 512_0_eq_Return(EOS(STATIC_512), x1, x2, 1)
459_1_eq_InvokeMethod(347_0_eq_Return(EOS(STATIC_347), 0), x1, x2, 0, x4) → 512_0_eq_Return(EOS(STATIC_512), x1, x2, 0)
459_1_eq_InvokeMethod(352_0_eq_Return(EOS(STATIC_352), 0), x1, x2, x3, 0) → 512_0_eq_Return(EOS(STATIC_512), x1, x2, 0)

Filtered ground terms:

253_0_eq_LE(x1, x2, x3, x4) → 253_0_eq_LE(x2, x3, x4)
Cond_253_0_eq_LE(x1, x2, x3, x4, x5) → Cond_253_0_eq_LE(x1, x3, x4, x5)
512_0_eq_Return(x1, x2, x3, x4) → 512_0_eq_Return(x2, x3, x4)
352_0_eq_Return(x1, x2) → 352_0_eq_Return
347_0_eq_Return(x1, x2) → 347_0_eq_Return
369_0_eq_Return(x1, x2) → 369_0_eq_Return
496_0_eq_Return(x1, x2, x3, x4) → 496_0_eq_Return(x2, x3, x4)

Filtered duplicate args:

253_0_eq_LE(x1, x2, x3) → 253_0_eq_LE(x2, x3)
Cond_253_0_eq_LE(x1, x2, x3, x4) → Cond_253_0_eq_LE(x1, x3, x4)

Filtered unneeded arguments:

459_1_eq_InvokeMethod(x1, x2, x3, x4, x5) → 459_1_eq_InvokeMethod(x1, x4, x5)

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

P rules:
253_0_eq_LE(x1, x0) → 459_1_eq_InvokeMethod(253_0_eq_LE(-(x1, 1), -(x0, 1)), -(x0, 1), -(x1, 1)) | &&(>(x1, 0), >(x0, 0))
R rules:
253_0_eq_LE(x1, 0) → 347_0_eq_Return | >(x1, 0)
253_0_eq_LE(0, 0) → 369_0_eq_Return
459_1_eq_InvokeMethod(496_0_eq_Return(x0, x1, x2), x0, x1) → 512_0_eq_Return(x3, x4, x2)
459_1_eq_InvokeMethod(512_0_eq_Return(x0, x1, x2), x0, x1) → 512_0_eq_Return(x3, x4, x2)
459_1_eq_InvokeMethod(369_0_eq_Return, 0, 0) → 512_0_eq_Return(x1, x2, 1)
459_1_eq_InvokeMethod(347_0_eq_Return, 0, x4) → 512_0_eq_Return(x1, x2, 0)
459_1_eq_InvokeMethod(352_0_eq_Return, x3, 0) → 512_0_eq_Return(x1, x2, 0)

Performed bisimulation on rules. Used the following equivalence classes: {[347_0_eq_Return, 369_0_eq_Return, 352_0_eq_Return]=347_0_eq_Return}

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

P rules:
253_0_EQ_LE(x1, x0) → COND_253_0_EQ_LE(&&(>(x1, 0), >(x0, 0)), x1, x0)
COND_253_0_EQ_LE(TRUE, x1, x0) → 253_0_EQ_LE(-(x1, 1), -(x0, 1))
R rules:
253_0_eq_LE(x1, 0) → Cond_253_0_eq_LE(>(x1, 0), x1, 0)
Cond_253_0_eq_LE(TRUE, x1, 0) → 347_0_eq_Return
253_0_eq_LE(0, 0) → 347_0_eq_Return
459_1_eq_InvokeMethod(496_0_eq_Return(x0, x1, x2), x0, x1) → 512_0_eq_Return(x3, x4, x2)
459_1_eq_InvokeMethod(512_0_eq_Return(x0, x1, x2), x0, x1) → 512_0_eq_Return(x3, x4, x2)
459_1_eq_InvokeMethod(347_0_eq_Return, 0, 0) → 512_0_eq_Return(x1, x2, 1)
459_1_eq_InvokeMethod(347_0_eq_Return, 0, x4) → 512_0_eq_Return(x1, x2, 0)
459_1_eq_InvokeMethod(347_0_eq_Return, x3, 0) → 512_0_eq_Return(x1, x2, 0)

(6) Obligation:

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

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

The following domains are used:

Integer, Boolean

The ITRS R consists of the following rules:
253_0_eq_LE(x1, 0) → Cond_253_0_eq_LE(x1 > 0, x1, 0)
Cond_253_0_eq_LE(TRUE, x1, 0) → 347_0_eq_Return
253_0_eq_LE(0, 0) → 347_0_eq_Return
459_1_eq_InvokeMethod(496_0_eq_Return(x0, x1, x2), x0, x1) → 512_0_eq_Return(x3, x4, x2)
459_1_eq_InvokeMethod(512_0_eq_Return(x0, x1, x2), x0, x1) → 512_0_eq_Return(x3, x4, x2)
459_1_eq_InvokeMethod(347_0_eq_Return, 0, 0) → 512_0_eq_Return(x1, x2, 1)
459_1_eq_InvokeMethod(347_0_eq_Return, 0, x4) → 512_0_eq_Return(x1, x2, 0)
459_1_eq_InvokeMethod(347_0_eq_Return, x3, 0) → 512_0_eq_Return(x1, x2, 0)

The integer pair graph contains the following rules and edges:
(0): 253_0_EQ_LE(x1[0], x0[0]) → COND_253_0_EQ_LE(x1[0] > 0 && x0[0] > 0, x1[0], x0[0])
(1): COND_253_0_EQ_LE(TRUE, x1[1], x0[1]) → 253_0_EQ_LE(x1[1] - 1, x0[1] - 1)

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

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

The set Q consists of the following terms:
253_0_eq_LE(x0, 0)
Cond_253_0_eq_LE(TRUE, x0, 0)
459_1_eq_InvokeMethod(496_0_eq_Return(x0, x1, x2), x0, x1)
459_1_eq_InvokeMethod(512_0_eq_Return(x0, x1, x2), x0, x1)
459_1_eq_InvokeMethod(347_0_eq_Return, 0, x0)
459_1_eq_InvokeMethod(347_0_eq_Return, x0, 0)

(7) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@5954100e 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 253_0_EQ_LE(x1, x0) → COND_253_0_EQ_LE(&&(>(x1, 0), >(x0, 0)), x1, x0) the following chains were created:

• We consider the chain 253_0_EQ_LE(x1[0], x0[0]) → COND_253_0_EQ_LE(&&(>(x1[0], 0), >(x0[0], 0)), x1[0], x0[0]), COND_253_0_EQ_LE(TRUE, x1[1], x0[1]) → 253_0_EQ_LE(-(x1[1], 1), -(x0[1], 1)) which results in the following constraint:
  

  (1)    (&&(>(x1[0], 0), >(x0[0], 0))=TRUE∧x1[0]=x1[1]∧x0[0]=x0[1] ⇒ 253_0_EQ_LE(x1[0], x0[0])≥NonInfC∧253_0_EQ_LE(x1[0], x0[0])≥COND_253_0_EQ_LE(&&(>(x1[0], 0), >(x0[0], 0)), x1[0], x0[0])∧(U^Increasing(COND_253_0_EQ_LE(&&(>(x1[0], 0), >(x0[0], 0)), x1[0], x0[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 ⇒ 253_0_EQ_LE(x1[0], x0[0])≥NonInfC∧253_0_EQ_LE(x1[0], x0[0])≥COND_253_0_EQ_LE(&&(>(x1[0], 0), >(x0[0], 0)), x1[0], x0[0])∧(U^Increasing(COND_253_0_EQ_LE(&&(>(x1[0], 0), >(x0[0], 0)), x1[0], x0[0])), ≥))

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

  (3)    (x1[0] + [-1] ≥ 0∧x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_253_0_EQ_LE(&&(>(x1[0], 0), >(x0[0], 0)), x1[0], x0[0])), ≥)∧[bni_17 + (-1)Bound*bni_17] + [(2)bni_17]x0[0] + [(2)bni_17]x1[0] ≥ 0∧[(-1)bso_18] ≥ 0)

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

  (4)    (x1[0] + [-1] ≥ 0∧x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_253_0_EQ_LE(&&(>(x1[0], 0), >(x0[0], 0)), x1[0], x0[0])), ≥)∧[bni_17 + (-1)Bound*bni_17] + [(2)bni_17]x0[0] + [(2)bni_17]x1[0] ≥ 0∧[(-1)bso_18] ≥ 0)

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

  (5)    (x1[0] + [-1] ≥ 0∧x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_253_0_EQ_LE(&&(>(x1[0], 0), >(x0[0], 0)), x1[0], x0[0])), ≥)∧[bni_17 + (-1)Bound*bni_17] + [(2)bni_17]x0[0] + [(2)bni_17]x1[0] ≥ 0∧[(-1)bso_18] ≥ 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_253_0_EQ_LE(&&(>(x1[0], 0), >(x0[0], 0)), x1[0], x0[0])), ≥)∧[(3)bni_17 + (-1)Bound*bni_17] + [(2)bni_17]x0[0] + [(2)bni_17]x1[0] ≥ 0∧[(-1)bso_18] ≥ 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_253_0_EQ_LE(&&(>(x1[0], 0), >(x0[0], 0)), x1[0], x0[0])), ≥)∧[(5)bni_17 + (-1)Bound*bni_17] + [(2)bni_17]x0[0] + [(2)bni_17]x1[0] ≥ 0∧[(-1)bso_18] ≥ 0)

  
  
  

For Pair COND_253_0_EQ_LE(TRUE, x1, x0) → 253_0_EQ_LE(-(x1, 1), -(x0, 1)) the following chains were created:

• We consider the chain COND_253_0_EQ_LE(TRUE, x1[1], x0[1]) → 253_0_EQ_LE(-(x1[1], 1), -(x0[1], 1)) which results in the following constraint:
  

  (8)    (COND_253_0_EQ_LE(TRUE, x1[1], x0[1])≥NonInfC∧COND_253_0_EQ_LE(TRUE, x1[1], x0[1])≥253_0_EQ_LE(-(x1[1], 1), -(x0[1], 1))∧(U^Increasing(253_0_EQ_LE(-(x1[1], 1), -(x0[1], 1))), ≥))

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

  (9)    ((U^Increasing(253_0_EQ_LE(-(x1[1], 1), -(x0[1], 1))), ≥)∧[bni_19] = 0∧[4 + (-1)bso_20] ≥ 0)

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

  (10)    ((U^Increasing(253_0_EQ_LE(-(x1[1], 1), -(x0[1], 1))), ≥)∧[bni_19] = 0∧[4 + (-1)bso_20] ≥ 0)

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

  (11)    ((U^Increasing(253_0_EQ_LE(-(x1[1], 1), -(x0[1], 1))), ≥)∧[bni_19] = 0∧[4 + (-1)bso_20] ≥ 0)

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

  (12)    ((U^Increasing(253_0_EQ_LE(-(x1[1], 1), -(x0[1], 1))), ≥)∧[bni_19] = 0∧0 = 0∧0 = 0∧[4 + (-1)bso_20] ≥ 0)

  
  
  

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

• 253_0_EQ_LE(x1, x0) → COND_253_0_EQ_LE(&&(>(x1, 0), >(x0, 0)), x1, x0)
  
  • (x1[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(COND_253_0_EQ_LE(&&(>(x1[0], 0), >(x0[0], 0)), x1[0], x0[0])), ≥)∧[(5)bni_17 + (-1)Bound*bni_17] + [(2)bni_17]x0[0] + [(2)bni_17]x1[0] ≥ 0∧[(-1)bso_18] ≥ 0)
    
  
  
• COND_253_0_EQ_LE(TRUE, x1, x0) → 253_0_EQ_LE(-(x1, 1), -(x0, 1))
  
  • ((U^Increasing(253_0_EQ_LE(-(x1[1], 1), -(x0[1], 1))), ≥)∧[bni_19] = 0∧0 = 0∧0 = 0∧[4 + (-1)bso_20] ≥ 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(253_0_eq_LE(x₁, x₂)) = [-1] + [-1]x₁   
POL(0) = 0   
POL(Cond_253_0_eq_LE(x₁, x₂, x₃)) = [-1] + [-1]x₂   
POL(>(x₁, x₂)) = [-1]   
POL(347_0_eq_Return) = [-1]   
POL(459_1_eq_InvokeMethod(x₁, x₂, x₃)) = [-1]   
POL(496_0_eq_Return(x₁, x₂, x₃)) = [-1]   
POL(512_0_eq_Return(x₁, x₂, x₃)) = [-1]   
POL(1) = [1]   
POL(253_0_EQ_LE(x₁, x₂)) = [1] + [2]x₂ + [2]x₁   
POL(COND_253_0_EQ_LE(x₁, x₂, x₃)) = [1] + [2]x₃ + [2]x₂   
POL(&&(x₁, x₂)) = [-1]   
POL(-(x₁, x₂)) = x₁ + [-1]x₂   

The following pairs are in P_>:

COND_253_0_EQ_LE(TRUE, x1[1], x0[1]) → 253_0_EQ_LE(-(x1[1], 1), -(x0[1], 1))

The following pairs are in P_bound:

253_0_EQ_LE(x1[0], x0[0]) → COND_253_0_EQ_LE(&&(>(x1[0], 0), >(x0[0], 0)), x1[0], x0[0])

The following pairs are in P_≥:

253_0_EQ_LE(x1[0], x0[0]) → COND_253_0_EQ_LE(&&(>(x1[0], 0), >(x0[0], 0)), x1[0], x0[0])

There are no usable rules.

(8) Complex Obligation (AND)

(9) 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:
253_0_eq_LE(x1, 0) → Cond_253_0_eq_LE(x1 > 0, x1, 0)
Cond_253_0_eq_LE(TRUE, x1, 0) → 347_0_eq_Return
253_0_eq_LE(0, 0) → 347_0_eq_Return
459_1_eq_InvokeMethod(496_0_eq_Return(x0, x1, x2), x0, x1) → 512_0_eq_Return(x3, x4, x2)
459_1_eq_InvokeMethod(512_0_eq_Return(x0, x1, x2), x0, x1) → 512_0_eq_Return(x3, x4, x2)
459_1_eq_InvokeMethod(347_0_eq_Return, 0, 0) → 512_0_eq_Return(x1, x2, 1)
459_1_eq_InvokeMethod(347_0_eq_Return, 0, x4) → 512_0_eq_Return(x1, x2, 0)
459_1_eq_InvokeMethod(347_0_eq_Return, x3, 0) → 512_0_eq_Return(x1, x2, 0)

The integer pair graph contains the following rules and edges:
(0): 253_0_EQ_LE(x1[0], x0[0]) → COND_253_0_EQ_LE(x1[0] > 0 && x0[0] > 0, x1[0], x0[0])


The set Q consists of the following terms:
253_0_eq_LE(x0, 0)
Cond_253_0_eq_LE(TRUE, x0, 0)
459_1_eq_InvokeMethod(496_0_eq_Return(x0, x1, x2), x0, x1)
459_1_eq_InvokeMethod(512_0_eq_Return(x0, x1, x2), x0, x1)
459_1_eq_InvokeMethod(347_0_eq_Return, 0, x0)
459_1_eq_InvokeMethod(347_0_eq_Return, x0, 0)

(10) IDependencyGraphProof (EQUIVALENT transformation)

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

(11) TRUE

(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

The ITRS R consists of the following rules:
253_0_eq_LE(x1, 0) → Cond_253_0_eq_LE(x1 > 0, x1, 0)
Cond_253_0_eq_LE(TRUE, x1, 0) → 347_0_eq_Return
253_0_eq_LE(0, 0) → 347_0_eq_Return
459_1_eq_InvokeMethod(496_0_eq_Return(x0, x1, x2), x0, x1) → 512_0_eq_Return(x3, x4, x2)
459_1_eq_InvokeMethod(512_0_eq_Return(x0, x1, x2), x0, x1) → 512_0_eq_Return(x3, x4, x2)
459_1_eq_InvokeMethod(347_0_eq_Return, 0, 0) → 512_0_eq_Return(x1, x2, 1)
459_1_eq_InvokeMethod(347_0_eq_Return, 0, x4) → 512_0_eq_Return(x1, x2, 0)
459_1_eq_InvokeMethod(347_0_eq_Return, x3, 0) → 512_0_eq_Return(x1, x2, 0)

The integer pair graph contains the following rules and edges:
(1): COND_253_0_EQ_LE(TRUE, x1[1], x0[1]) → 253_0_EQ_LE(x1[1] - 1, x0[1] - 1)


The set Q consists of the following terms:
253_0_eq_LE(x0, 0)
Cond_253_0_eq_LE(TRUE, x0, 0)
459_1_eq_InvokeMethod(496_0_eq_Return(x0, x1, x2), x0, x1)
459_1_eq_InvokeMethod(512_0_eq_Return(x0, x1, x2), x0, x1)
459_1_eq_InvokeMethod(347_0_eq_Return, 0, x0)
459_1_eq_InvokeMethod(347_0_eq_Return, x0, 0)

(13) IDependencyGraphProof (EQUIVALENT transformation)

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

(14) TRUE