Termination proof of /tmp/tmpkvRwuo/TerminatorRec01.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 184 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 JBCTerminationSCC

↳5 SCCToIDPv1Proof (⇒, 179 ms)

↳6 IDP

↳7 IDPNonInfProof (⇒, 361 ms)

↳8 IDP

↳9 IDependencyGraphProof (⇔, 0 ms)

↳10 IDP

↳11 UsableRulesProof (⇔, 8 ms)

↳12 IDP

↳13 IDPNonInfProof (⇒, 0 ms)

↳14 IDP

↳15 IDependencyGraphProof (⇔, 0 ms)

↳16 TRUE

(0) Obligation:

JBC Problem based on JBC Program:

public class TerminatorRec01 {
	static int z = 0;

	public static void main(String[] args) {
		z = args.length;
		f(z);
	}

	public static void f(int x) {
		int y = 0;
		if (x > 0) {
			y = 2;
			while (y > 0) {
				z = z - 1;
				f(x - y);
				y = y - 1;
			}
		}
	}
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

TerminatorRec01.f(I)V: Graph of 37 nodes with 1 SCC.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 1 SCCs.

(4) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: TerminatorRec01.f(I)V
SCC calls the following helper methods: TerminatorRec01.f(I)V
Performed SCC analyses:

Used field analysis yielded the following read fields:
Marker field analysis yielded the following relations that could be markers:

(5) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 33 rules for P and 37 rules for R.

P rules:
f424_0_f_Store(EOS(STATIC_424), i94, i94, matching1) → f425_0_f_Load(EOS(STATIC_425), i94, i94) | =(matching1, 0)
f425_0_f_Load(EOS(STATIC_425), i94, i94) → f428_0_f_LE(EOS(STATIC_428), i94, i94, i94)
f428_0_f_LE(EOS(STATIC_428), i98, i98, i98) → f432_0_f_LE(EOS(STATIC_432), i98, i98, i98)
f432_0_f_LE(EOS(STATIC_432), i98, i98, i98) → f435_0_f_ConstantStackPush(EOS(STATIC_435), i98, i98) | >(i98, 0)
f435_0_f_ConstantStackPush(EOS(STATIC_435), i98, i98) → f439_0_f_Store(EOS(STATIC_439), i98, i98, 2)
f439_0_f_Store(EOS(STATIC_439), i98, i98, matching1) → f451_0_f_Load(EOS(STATIC_451), i98, i98, 2) | =(matching1, 2)
f451_0_f_Load(EOS(STATIC_451), i98, i98, matching1) → f515_0_f_Load(EOS(STATIC_515), i98, i98, 2) | =(matching1, 2)
f515_0_f_Load(EOS(STATIC_515), i98, i98, i122) → f574_0_f_Load(EOS(STATIC_574), i98, i98, i122)
f574_0_f_Load(EOS(STATIC_574), i98, i98, i141) → f578_0_f_LE(EOS(STATIC_578), i98, i98, i141, i141)
f578_0_f_LE(EOS(STATIC_578), i98, i98, i150, i150) → f582_0_f_LE(EOS(STATIC_582), i98, i98, i150, i150)
f582_0_f_LE(EOS(STATIC_582), i98, i98, i150, i150) → f586_0_f_FieldAccess(EOS(STATIC_586), i98, i98, i150) | >(i150, 0)
f586_0_f_FieldAccess(EOS(STATIC_586), i98, i98, i150) → f590_0_f_ConstantStackPush(EOS(STATIC_590), i98, i98, i150)
f590_0_f_ConstantStackPush(EOS(STATIC_590), i98, i98, i150) → f602_0_f_IntArithmetic(EOS(STATIC_602), i98, i98, i150)
f602_0_f_IntArithmetic(EOS(STATIC_602), i98, i98, i150) → f616_0_f_FieldAccess(EOS(STATIC_616), i98, i98, i150)
f616_0_f_FieldAccess(EOS(STATIC_616), i98, i98, i150) → f620_0_f_Load(EOS(STATIC_620), i98, i98, i150)
f620_0_f_Load(EOS(STATIC_620), i98, i98, i150) → f623_0_f_Load(EOS(STATIC_623), i98, i98, i150, i98)
f623_0_f_Load(EOS(STATIC_623), i98, i98, i150, i98) → f625_0_f_IntArithmetic(EOS(STATIC_625), i98, i98, i150, i98, i150)
f625_0_f_IntArithmetic(EOS(STATIC_625), i98, i98, i150, i98, i150) → f626_0_f_InvokeMethod(EOS(STATIC_626), i98, i98, i150, -(i98, i150)) | &&(>(i98, 0), >(i150, 0))
f626_0_f_InvokeMethod(EOS(STATIC_626), i98, i98, i150, i165) → f629_1_f_InvokeMethod(f629_0_f_ConstantStackPush(EOS(STATIC_629), i165, i165), i98, i98, i150, i165)
f629_0_f_ConstantStackPush(EOS(STATIC_629), i165, i165) → f631_0_f_ConstantStackPush(EOS(STATIC_631), i165, i165)
f631_0_f_ConstantStackPush(EOS(STATIC_631), i165, i165) → f422_0_f_ConstantStackPush(EOS(STATIC_422), i165, i165)
f422_0_f_ConstantStackPush(EOS(STATIC_422), i94, i94) → f424_0_f_Store(EOS(STATIC_424), i94, i94, 0)
f656_0_f_Return(EOS(STATIC_656), i98, i98, i150, i177) → f667_0_f_Return(EOS(STATIC_667), i98, i98, i150, i177)
f667_0_f_Return(EOS(STATIC_667), i98, i98, i150, i185) → f670_0_f_Load(EOS(STATIC_670), i98, i98, i150)
f670_0_f_Load(EOS(STATIC_670), i98, i98, i150) → f672_0_f_ConstantStackPush(EOS(STATIC_672), i98, i98, i150)
f672_0_f_ConstantStackPush(EOS(STATIC_672), i98, i98, i150) → f673_0_f_IntArithmetic(EOS(STATIC_673), i98, i98, i150, 1)
f673_0_f_IntArithmetic(EOS(STATIC_673), i98, i98, i150, matching1) → f675_0_f_Store(EOS(STATIC_675), i98, i98, -(i150, 1)) | &&(>(i150, 0), =(matching1, 1))
f675_0_f_Store(EOS(STATIC_675), i98, i98, i189) → f677_0_f_JMP(EOS(STATIC_677), i98, i98, i189)
f677_0_f_JMP(EOS(STATIC_677), i98, i98, i189) → f683_0_f_Load(EOS(STATIC_683), i98, i98, i189)
f683_0_f_Load(EOS(STATIC_683), i98, i98, i189) → f574_0_f_Load(EOS(STATIC_574), i98, i98, i189)
f666_0_f_Return(EOS(STATIC_666), i98, i98, i150, i181) → f667_0_f_Return(EOS(STATIC_667), i98, i98, i150, i181)
f629_1_f_InvokeMethod(f434_0_f_Return(EOS(STATIC_434), i177), i98, i98, i150, i177) → f656_0_f_Return(EOS(STATIC_656), i98, i98, i150, i177)
f629_1_f_InvokeMethod(f584_0_f_Return(EOS(STATIC_584), i181), i98, i98, i150, i181) → f666_0_f_Return(EOS(STATIC_666), i98, i98, i150, i181)
R rules:
f422_0_f_ConstantStackPush(EOS(STATIC_422), i94, i94) → f424_0_f_Store(EOS(STATIC_424), i94, i94, 0)
f424_0_f_Store(EOS(STATIC_424), i94, i94, matching1) → f425_0_f_Load(EOS(STATIC_425), i94, i94) | =(matching1, 0)
f425_0_f_Load(EOS(STATIC_425), i94, i94) → f428_0_f_LE(EOS(STATIC_428), i94, i94, i94)
f428_0_f_LE(EOS(STATIC_428), i97, i97, i97) → f431_0_f_LE(EOS(STATIC_431), i97, i97, i97)
f428_0_f_LE(EOS(STATIC_428), i98, i98, i98) → f432_0_f_LE(EOS(STATIC_432), i98, i98, i98)
f431_0_f_LE(EOS(STATIC_431), i97, i97, i97) → f434_0_f_Return(EOS(STATIC_434), i97) | <=(i97, 0)
f432_0_f_LE(EOS(STATIC_432), i98, i98, i98) → f435_0_f_ConstantStackPush(EOS(STATIC_435), i98, i98) | >(i98, 0)
f435_0_f_ConstantStackPush(EOS(STATIC_435), i98, i98) → f439_0_f_Store(EOS(STATIC_439), i98, i98, 2)
f439_0_f_Store(EOS(STATIC_439), i98, i98, matching1) → f451_0_f_Load(EOS(STATIC_451), i98, i98, 2) | =(matching1, 2)
f451_0_f_Load(EOS(STATIC_451), i98, i98, matching1) → f515_0_f_Load(EOS(STATIC_515), i98, i98, 2) | =(matching1, 2)
f515_0_f_Load(EOS(STATIC_515), i98, i98, i122) → f574_0_f_Load(EOS(STATIC_574), i98, i98, i122)
f574_0_f_Load(EOS(STATIC_574), i98, i98, i141) → f578_0_f_LE(EOS(STATIC_578), i98, i98, i141, i141)
f578_0_f_LE(EOS(STATIC_578), i98, i98, matching1, matching2) → f581_0_f_LE(EOS(STATIC_581), i98, i98, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
f578_0_f_LE(EOS(STATIC_578), i98, i98, i150, i150) → f582_0_f_LE(EOS(STATIC_582), i98, i98, i150, i150)
f581_0_f_LE(EOS(STATIC_581), i98, i98, matching1, matching2) → f584_0_f_Return(EOS(STATIC_584), i98) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
f582_0_f_LE(EOS(STATIC_582), i98, i98, i150, i150) → f586_0_f_FieldAccess(EOS(STATIC_586), i98, i98, i150) | >(i150, 0)
f586_0_f_FieldAccess(EOS(STATIC_586), i98, i98, i150) → f590_0_f_ConstantStackPush(EOS(STATIC_590), i98, i98, i150)
f590_0_f_ConstantStackPush(EOS(STATIC_590), i98, i98, i150) → f602_0_f_IntArithmetic(EOS(STATIC_602), i98, i98, i150)
f602_0_f_IntArithmetic(EOS(STATIC_602), i98, i98, i150) → f616_0_f_FieldAccess(EOS(STATIC_616), i98, i98, i150)
f616_0_f_FieldAccess(EOS(STATIC_616), i98, i98, i150) → f620_0_f_Load(EOS(STATIC_620), i98, i98, i150)
f620_0_f_Load(EOS(STATIC_620), i98, i98, i150) → f623_0_f_Load(EOS(STATIC_623), i98, i98, i150, i98)
f623_0_f_Load(EOS(STATIC_623), i98, i98, i150, i98) → f625_0_f_IntArithmetic(EOS(STATIC_625), i98, i98, i150, i98, i150)
f625_0_f_IntArithmetic(EOS(STATIC_625), i98, i98, i150, i98, i150) → f626_0_f_InvokeMethod(EOS(STATIC_626), i98, i98, i150, -(i98, i150)) | &&(>(i98, 0), >(i150, 0))
f626_0_f_InvokeMethod(EOS(STATIC_626), i98, i98, i150, i165) → f629_1_f_InvokeMethod(f629_0_f_ConstantStackPush(EOS(STATIC_629), i165, i165), i98, i98, i150, i165)
f629_0_f_ConstantStackPush(EOS(STATIC_629), i165, i165) → f631_0_f_ConstantStackPush(EOS(STATIC_631), i165, i165)
f656_0_f_Return(EOS(STATIC_656), i98, i98, i150, i177) → f667_0_f_Return(EOS(STATIC_667), i98, i98, i150, i177)
f666_0_f_Return(EOS(STATIC_666), i98, i98, i150, i181) → f667_0_f_Return(EOS(STATIC_667), i98, i98, i150, i181)
f667_0_f_Return(EOS(STATIC_667), i98, i98, i150, i185) → f670_0_f_Load(EOS(STATIC_670), i98, i98, i150)
f670_0_f_Load(EOS(STATIC_670), i98, i98, i150) → f672_0_f_ConstantStackPush(EOS(STATIC_672), i98, i98, i150)
f672_0_f_ConstantStackPush(EOS(STATIC_672), i98, i98, i150) → f673_0_f_IntArithmetic(EOS(STATIC_673), i98, i98, i150, 1)
f673_0_f_IntArithmetic(EOS(STATIC_673), i98, i98, i150, matching1) → f675_0_f_Store(EOS(STATIC_675), i98, i98, -(i150, 1)) | &&(>(i150, 0), =(matching1, 1))
f675_0_f_Store(EOS(STATIC_675), i98, i98, i189) → f677_0_f_JMP(EOS(STATIC_677), i98, i98, i189)
f677_0_f_JMP(EOS(STATIC_677), i98, i98, i189) → f683_0_f_Load(EOS(STATIC_683), i98, i98, i189)
f683_0_f_Load(EOS(STATIC_683), i98, i98, i189) → f574_0_f_Load(EOS(STATIC_574), i98, i98, i189)
f631_0_f_ConstantStackPush(EOS(STATIC_631), i165, i165) → f422_0_f_ConstantStackPush(EOS(STATIC_422), i165, i165)
f629_1_f_InvokeMethod(f434_0_f_Return(EOS(STATIC_434), i177), i98, i98, i150, i177) → f656_0_f_Return(EOS(STATIC_656), i98, i98, i150, i177)
f629_1_f_InvokeMethod(f584_0_f_Return(EOS(STATIC_584), i181), i98, i98, i150, i181) → f666_0_f_Return(EOS(STATIC_666), i98, i98, i150, i181)

Combined rules. Obtained 3 conditional rules for P and 6 conditional rules for R.

P rules:
f424_0_f_Store(EOS(STATIC_424), x0, x0, 0) → f629_1_f_InvokeMethod(f424_0_f_Store(EOS(STATIC_424), -(x0, 2), -(x0, 2), 0), x0, x0, 2, -(x0, 2)) | >(x0, 0)
f629_1_f_InvokeMethod(f434_0_f_Return(EOS(STATIC_434), x0), x1, x1, x2, x0) → f629_1_f_InvokeMethod(f424_0_f_Store(EOS(STATIC_424), -(x1, -(x2, 1)), -(x1, -(x2, 1)), 0), x1, x1, -(x2, 1), -(x1, -(x2, 1))) | &&(>(x2, 1), >(x1, 0))
f629_1_f_InvokeMethod(f584_0_f_Return(EOS(STATIC_584), x0), x1, x1, x2, x0) → f629_1_f_InvokeMethod(f424_0_f_Store(EOS(STATIC_424), -(x1, -(x2, 1)), -(x1, -(x2, 1)), 0), x1, x1, -(x2, 1), -(x1, -(x2, 1))) | &&(>(x2, 1), >(x1, 0))
R rules:
f424_0_f_Store(EOS(STATIC_424), x0, x0, 0) → f434_0_f_Return(EOS(STATIC_434), x0) | <=(x0, 0)
f424_0_f_Store(EOS(STATIC_424), x0, x0, 0) → f578_0_f_LE(EOS(STATIC_578), x0, x0, 2, 2) | >(x0, 0)
f578_0_f_LE(EOS(STATIC_578), x0, x0, 0, 0) → f584_0_f_Return(EOS(STATIC_584), x0)
f578_0_f_LE(EOS(STATIC_578), x0, x0, x1, x1) → f629_1_f_InvokeMethod(f424_0_f_Store(EOS(STATIC_424), -(x0, x1), -(x0, x1), 0), x0, x0, x1, -(x0, x1)) | &&(>(x1, 0), >(x0, 0))
f629_1_f_InvokeMethod(f434_0_f_Return(EOS(STATIC_434), x0), x1, x1, x2, x0) → f578_0_f_LE(EOS(STATIC_578), x1, x1, -(x2, 1), -(x2, 1)) | >(x2, 0)
f629_1_f_InvokeMethod(f584_0_f_Return(EOS(STATIC_584), x0), x1, x1, x2, x0) → f578_0_f_LE(EOS(STATIC_578), x1, x1, -(x2, 1), -(x2, 1)) | >(x2, 0)

Filtered ground terms:

f424_0_f_Store(x1, x2, x3, x4) → f424_0_f_Store(x2, x3)
Cond_f424_0_f_Store(x1, x2, x3, x4, x5) → Cond_f424_0_f_Store(x1, x3, x4)
f434_0_f_Return(x1, x2) → f434_0_f_Return(x2)
f584_0_f_Return(x1, x2) → f584_0_f_Return(x2)
Cond_f424_0_f_Store1(x1, x2, x3, x4, x5) → Cond_f424_0_f_Store1(x1, x3, x4)
f578_0_f_LE(x1, x2, x3, x4, x5) → f578_0_f_LE(x2, x3, x4, x5)
Cond_f578_0_f_LE(x1, x2, x3, x4, x5, x6) → Cond_f578_0_f_LE(x1, x3, x4, x5, x6)

Filtered unneeded arguments:

f629_1_f_InvokeMethod(x1, x2, x3, x4, x5) → f629_1_f_InvokeMethod(x1, x2, x3, x4)
Cond_f629_1_f_InvokeMethod(x1, x2, x3, x4, x5, x6) → Cond_f629_1_f_InvokeMethod(x1, x3, x4, x5)
Cond_f629_1_f_InvokeMethod1(x1, x2, x3, x4, x5, x6) → Cond_f629_1_f_InvokeMethod1(x1, x3, x4, x5)

Filtered duplicate args:

f424_0_f_Store(x1, x2) → f424_0_f_Store(x2)
Cond_f424_0_f_Store(x1, x2, x3) → Cond_f424_0_f_Store(x1, x3)
f629_1_f_InvokeMethod(x1, x2, x3, x4) → f629_1_f_InvokeMethod(x1, x3, x4)
Cond_f629_1_f_InvokeMethod(x1, x2, x3, x4) → Cond_f629_1_f_InvokeMethod(x1, x3, x4)
Cond_f629_1_f_InvokeMethod1(x1, x2, x3, x4) → Cond_f629_1_f_InvokeMethod1(x1, x3, x4)
Cond_f424_0_f_Store1(x1, x2, x3) → Cond_f424_0_f_Store1(x1, x3)
f578_0_f_LE(x1, x2, x3, x4) → f578_0_f_LE(x2, x4)
Cond_f578_0_f_LE(x1, x2, x3, x4, x5) → Cond_f578_0_f_LE(x1, x3, x5)

Combined rules. Obtained 6 conditional rules for P and 5 conditional rules for R.

P rules:
F424_0_F_STORE(x0) → F629_1_F_INVOKEMETHOD(f424_0_f_Store(-(x0, 2)), x0, 2) | >(x0, 0)
F424_0_F_STORE(x0) → F424_0_F_STORE(-(x0, 2)) | >(x0, 0)
F629_1_F_INVOKEMETHOD(f434_0_f_Return(x0), x1, x2) → F629_1_F_INVOKEMETHOD(f424_0_f_Store(-(x1, -(x2, 1))), x1, -(x2, 1)) | &&(>(x1, 0), >(x2, 1))
F629_1_F_INVOKEMETHOD(f434_0_f_Return(x0), x1, x2) → F424_0_F_STORE(-(x1, -(x2, 1))) | &&(>(x1, 0), >(x2, 1))
F629_1_F_INVOKEMETHOD(f584_0_f_Return(x0), x1, x2) → F629_1_F_INVOKEMETHOD(f424_0_f_Store(-(x1, -(x2, 1))), x1, -(x2, 1)) | &&(>(x1, 0), >(x2, 1))
F629_1_F_INVOKEMETHOD(f584_0_f_Return(x0), x1, x2) → F424_0_F_STORE(-(x1, -(x2, 1))) | &&(>(x1, 0), >(x2, 1))
R rules:
f578_0_f_LE(x0, 0) → f584_0_f_Return(x0)
f629_1_f_InvokeMethod(f434_0_f_Return(x0), x1, x2) → f578_0_f_LE(x1, -(x2, 1)) | >(x2, 0)
f629_1_f_InvokeMethod(f584_0_f_Return(x0), x1, x2) → f578_0_f_LE(x1, -(x2, 1)) | >(x2, 0)
f578_0_f_LE(x0, x1) → f629_1_f_InvokeMethod(f434_0_f_Return(-(x0, x1)), x0, x1) | &&(&&(>(x1, 0), <=(-(x0, x1), 0)), >(x0, 0))
f578_0_f_LE(x0, x1) → f629_1_f_InvokeMethod(f578_0_f_LE(-(x0, x1), 2), x0, x1) | &&(&&(>(x1, 0), >(-(x0, x1), 0)), >(x0, 0))

Finished conversion. Obtained 12 rules for P and 9 rules for R. System has predefined symbols.

P rules:
F424_0_F_STORE'(x0) → COND_F424_0_F_STORE(>(x0, 0), x0)
COND_F424_0_F_STORE(TRUE, x0) → F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x0, 2)), x0, 2)
F424_0_F_STORE'(x0) → COND_F424_0_F_STORE1(>(x0, 0), x0)
COND_F424_0_F_STORE1(TRUE, x0) → F424_0_F_STORE'(-(x0, 2))
F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0), x1, x2) → COND_F629_1_F_INVOKEMETHOD(&&(>(x1, 0), >(x2, 1)), f434_0_f_Return(x0), x1, x2)
COND_F629_1_F_INVOKEMETHOD(TRUE, f434_0_f_Return(x0), x1, x2) → F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1, -(x2, 1))), x1, -(x2, 1))
F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0), x1, x2) → COND_F629_1_F_INVOKEMETHOD1(&&(>(x1, 0), >(x2, 1)), f434_0_f_Return(x0), x1, x2)
COND_F629_1_F_INVOKEMETHOD1(TRUE, f434_0_f_Return(x0), x1, x2) → F424_0_F_STORE'(-(x1, -(x2, 1)))
F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0), x1, x2) → COND_F629_1_F_INVOKEMETHOD2(&&(>(x1, 0), >(x2, 1)), f584_0_f_Return(x0), x1, x2)
COND_F629_1_F_INVOKEMETHOD2(TRUE, f584_0_f_Return(x0), x1, x2) → F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1, -(x2, 1))), x1, -(x2, 1))
F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0), x1, x2) → COND_F629_1_F_INVOKEMETHOD3(&&(>(x1, 0), >(x2, 1)), f584_0_f_Return(x0), x1, x2)
COND_F629_1_F_INVOKEMETHOD3(TRUE, f584_0_f_Return(x0), x1, x2) → F424_0_F_STORE'(-(x1, -(x2, 1)))
R rules:
f578_0_f_LE(x0, 0) → f584_0_f_Return(x0)
f629_1_f_InvokeMethod(f434_0_f_Return(x0), x1, x2) → Cond_f629_1_f_InvokeMethod(>(x2, 0), f434_0_f_Return(x0), x1, x2)
Cond_f629_1_f_InvokeMethod(TRUE, f434_0_f_Return(x0), x1, x2) → f578_0_f_LE(x1, -(x2, 1))
f629_1_f_InvokeMethod(f584_0_f_Return(x0), x1, x2) → Cond_f629_1_f_InvokeMethod1(>(x2, 0), f584_0_f_Return(x0), x1, x2)
Cond_f629_1_f_InvokeMethod1(TRUE, f584_0_f_Return(x0), x1, x2) → f578_0_f_LE(x1, -(x2, 1))
f578_0_f_LE(x0, x1) → Cond_f578_0_f_LE(&&(&&(>(x1, 0), <=(-(x0, x1), 0)), >(x0, 0)), x0, x1)
Cond_f578_0_f_LE(TRUE, x0, x1) → f629_1_f_InvokeMethod(f434_0_f_Return(-(x0, x1)), x0, x1)
f578_0_f_LE(x0, x1) → Cond_f578_0_f_LE1(&&(&&(>(x1, 0), >(-(x0, x1), 0)), >(x0, 0)), x0, x1)
Cond_f578_0_f_LE1(TRUE, x0, x1) → f629_1_f_InvokeMethod(f578_0_f_LE(-(x0, x1), 2), x0, x1)

(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:
f578_0_f_LE(x0, 0) → f584_0_f_Return(x0)
f629_1_f_InvokeMethod(f434_0_f_Return(x0), x1, x2) → Cond_f629_1_f_InvokeMethod(x2 > 0, f434_0_f_Return(x0), x1, x2)
Cond_f629_1_f_InvokeMethod(TRUE, f434_0_f_Return(x0), x1, x2) → f578_0_f_LE(x1, x2 - 1)
f629_1_f_InvokeMethod(f584_0_f_Return(x0), x1, x2) → Cond_f629_1_f_InvokeMethod1(x2 > 0, f584_0_f_Return(x0), x1, x2)
Cond_f629_1_f_InvokeMethod1(TRUE, f584_0_f_Return(x0), x1, x2) → f578_0_f_LE(x1, x2 - 1)
f578_0_f_LE(x0, x1) → Cond_f578_0_f_LE(x1 > 0 && x0 - x1 <= 0 && x0 > 0, x0, x1)
Cond_f578_0_f_LE(TRUE, x0, x1) → f629_1_f_InvokeMethod(f434_0_f_Return(x0 - x1), x0, x1)
f578_0_f_LE(x0, x1) → Cond_f578_0_f_LE1(x1 > 0 && x0 - x1 > 0 && x0 > 0, x0, x1)
Cond_f578_0_f_LE1(TRUE, x0, x1) → f629_1_f_InvokeMethod(f578_0_f_LE(x0 - x1, 2), x0, x1)

The integer pair graph contains the following rules and edges:
(0): F424_0_F_STORE'(x0[0]) → COND_F424_0_F_STORE(x0[0] > 0, x0[0])
(1): COND_F424_0_F_STORE(TRUE, x0[1]) → F629_1_F_INVOKEMETHOD'(f424_0_f_Store(x0[1] - 2), x0[1], 2)
(2): F424_0_F_STORE'(x0[2]) → COND_F424_0_F_STORE1(x0[2] > 0, x0[2])
(3): COND_F424_0_F_STORE1(TRUE, x0[3]) → F424_0_F_STORE'(x0[3] - 2)
(4): F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0[4]), x1[4], x2[4]) → COND_F629_1_F_INVOKEMETHOD(x1[4] > 0 && x2[4] > 1, f434_0_f_Return(x0[4]), x1[4], x2[4])
(5): COND_F629_1_F_INVOKEMETHOD(TRUE, f434_0_f_Return(x0[5]), x1[5], x2[5]) → F629_1_F_INVOKEMETHOD'(f424_0_f_Store(x1[5] - x2[5] - 1), x1[5], x2[5] - 1)
(6): F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0[6]), x1[6], x2[6]) → COND_F629_1_F_INVOKEMETHOD1(x1[6] > 0 && x2[6] > 1, f434_0_f_Return(x0[6]), x1[6], x2[6])
(7): COND_F629_1_F_INVOKEMETHOD1(TRUE, f434_0_f_Return(x0[7]), x1[7], x2[7]) → F424_0_F_STORE'(x1[7] - x2[7] - 1)
(8): F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0[8]), x1[8], x2[8]) → COND_F629_1_F_INVOKEMETHOD2(x1[8] > 0 && x2[8] > 1, f584_0_f_Return(x0[8]), x1[8], x2[8])
(9): COND_F629_1_F_INVOKEMETHOD2(TRUE, f584_0_f_Return(x0[9]), x1[9], x2[9]) → F629_1_F_INVOKEMETHOD'(f424_0_f_Store(x1[9] - x2[9] - 1), x1[9], x2[9] - 1)
(10): F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0[10]), x1[10], x2[10]) → COND_F629_1_F_INVOKEMETHOD3(x1[10] > 0 && x2[10] > 1, f584_0_f_Return(x0[10]), x1[10], x2[10])
(11): COND_F629_1_F_INVOKEMETHOD3(TRUE, f584_0_f_Return(x0[11]), x1[11], x2[11]) → F424_0_F_STORE'(x1[11] - x2[11] - 1)

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

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

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

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

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

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

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

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

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

(5) -> (4), if (f424_0_f_Store(x1[5] - x2[5] - 1) →^* f434_0_f_Return(x0[4])∧x1[5] →^* x1[4]∧x2[5] - 1 →^* x2[4])

(5) -> (6), if (f424_0_f_Store(x1[5] - x2[5] - 1) →^* f434_0_f_Return(x0[6])∧x1[5] →^* x1[6]∧x2[5] - 1 →^* x2[6])

(5) -> (8), if (f424_0_f_Store(x1[5] - x2[5] - 1) →^* f584_0_f_Return(x0[8])∧x1[5] →^* x1[8]∧x2[5] - 1 →^* x2[8])

(5) -> (10), if (f424_0_f_Store(x1[5] - x2[5] - 1) →^* f584_0_f_Return(x0[10])∧x1[5] →^* x1[10]∧x2[5] - 1 →^* x2[10])

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

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

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

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

(9) -> (4), if (f424_0_f_Store(x1[9] - x2[9] - 1) →^* f434_0_f_Return(x0[4])∧x1[9] →^* x1[4]∧x2[9] - 1 →^* x2[4])

(9) -> (6), if (f424_0_f_Store(x1[9] - x2[9] - 1) →^* f434_0_f_Return(x0[6])∧x1[9] →^* x1[6]∧x2[9] - 1 →^* x2[6])

(9) -> (8), if (f424_0_f_Store(x1[9] - x2[9] - 1) →^* f584_0_f_Return(x0[8])∧x1[9] →^* x1[8]∧x2[9] - 1 →^* x2[8])

(9) -> (10), if (f424_0_f_Store(x1[9] - x2[9] - 1) →^* f584_0_f_Return(x0[10])∧x1[9] →^* x1[10]∧x2[9] - 1 →^* x2[10])

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

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

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

The set Q consists of the following terms:
f629_1_f_InvokeMethod(f434_0_f_Return(x0), x1, x2)
Cond_f629_1_f_InvokeMethod(TRUE, f434_0_f_Return(x0), x1, x2)
f629_1_f_InvokeMethod(f584_0_f_Return(x0), x1, x2)
Cond_f629_1_f_InvokeMethod1(TRUE, f584_0_f_Return(x0), x1, x2)
f578_0_f_LE(x0, x1)
Cond_f578_0_f_LE(TRUE, x0, x1)
Cond_f578_0_f_LE1(TRUE, x0, x1)

(7) IDPNonInfProof (SOUND transformation)

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

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

For Pair F424_0_F_STORE'(x0) → COND_F424_0_F_STORE(>(x0, 0), x0) the following chains were created:

We consider the chain F424_0_F_STORE'(x0[0]) → COND_F424_0_F_STORE(>(x0[0], 0), x0[0]), COND_F424_0_F_STORE(TRUE, x0[1]) → F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x0[1], 2)), x0[1], 2) which results in the following constraint:
(1)    (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ F424_0_F_STORE'(x0[0])≥NonInfC∧F424_0_F_STORE'(x0[0])≥COND_F424_0_F_STORE(>(x0[0], 0), x0[0])∧(U^Increasing(COND_F424_0_F_STORE(>(x0[0], 0), x0[0])), ≥))

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

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

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

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

We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(6)    (0 ≥ 0 ⇒ (U^Increasing(COND_F424_0_F_STORE(>(x0[0], 0), x0[0])), ≥)∧[bni_64] ≥ 0∧[(-1)bni_64 + (-1)Bound*bni_64] ≥ 0∧[1] ≥ 0∧[(-1)bso_65] ≥ 0)

For Pair COND_F424_0_F_STORE(TRUE, x0) → F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x0, 2)), x0, 2) the following chains were created:

We consider the chain F424_0_F_STORE'(x0[0]) → COND_F424_0_F_STORE(>(x0[0], 0), x0[0]), COND_F424_0_F_STORE(TRUE, x0[1]) → F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x0[1], 2)), x0[1], 2) which results in the following constraint:
(7)    (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ COND_F424_0_F_STORE(TRUE, x0[1])≥NonInfC∧COND_F424_0_F_STORE(TRUE, x0[1])≥F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x0[1], 2)), x0[1], 2)∧(U^Increasing(F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x0[1], 2)), x0[1], 2)), ≥))

We simplified constraint (7) using rule (III) which results in the following new constraint:
(8)    (>(x0[0], 0)=TRUE ⇒ COND_F424_0_F_STORE(TRUE, x0[0])≥NonInfC∧COND_F424_0_F_STORE(TRUE, x0[0])≥F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x0[0], 2)), x0[0], 2)∧(U^Increasing(F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x0[1], 2)), x0[1], 2)), ≥))

We simplified constraint (8) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(9)    (0 ≥ 0 ⇒ (U^Increasing(F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x0[1], 2)), x0[1], 2)), ≥)∧[(-1)bni_66 + (-1)Bound*bni_66] ≥ 0∧[1 + (-1)bso_67] ≥ 0)

We simplified constraint (9) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(10)    (0 ≥ 0 ⇒ (U^Increasing(F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x0[1], 2)), x0[1], 2)), ≥)∧[(-1)bni_66 + (-1)Bound*bni_66] ≥ 0∧[1 + (-1)bso_67] ≥ 0)

We simplified constraint (10) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(11)    (0 ≥ 0 ⇒ (U^Increasing(F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x0[1], 2)), x0[1], 2)), ≥)∧[(-1)bni_66 + (-1)Bound*bni_66] ≥ 0∧[1 + (-1)bso_67] ≥ 0)

We simplified constraint (11) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(12)    (0 ≥ 0 ⇒ (U^Increasing(F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x0[1], 2)), x0[1], 2)), ≥)∧0 ≥ 0∧[(-1)bni_66 + (-1)Bound*bni_66] ≥ 0∧0 ≥ 0∧[1 + (-1)bso_67] ≥ 0)

For Pair F424_0_F_STORE'(x0) → COND_F424_0_F_STORE1(>(x0, 0), x0) the following chains were created:

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

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

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

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

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

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

For Pair COND_F424_0_F_STORE1(TRUE, x0) → F424_0_F_STORE'(-(x0, 2)) the following chains were created:

We consider the chain F424_0_F_STORE'(x0[2]) → COND_F424_0_F_STORE1(>(x0[2], 0), x0[2]), COND_F424_0_F_STORE1(TRUE, x0[3]) → F424_0_F_STORE'(-(x0[3], 2)), F424_0_F_STORE'(x0[0]) → COND_F424_0_F_STORE(>(x0[0], 0), x0[0]) which results in the following constraint:
(19)    (>(x0[2], 0)=TRUE∧x0[2]=x0[3]∧-(x0[3], 2)=x0[0] ⇒ COND_F424_0_F_STORE1(TRUE, x0[3])≥NonInfC∧COND_F424_0_F_STORE1(TRUE, x0[3])≥F424_0_F_STORE'(-(x0[3], 2))∧(U^Increasing(F424_0_F_STORE'(-(x0[3], 2))), ≥))

We simplified constraint (19) using rules (III), (IV) which results in the following new constraint:
(20)    (>(x0[2], 0)=TRUE ⇒ COND_F424_0_F_STORE1(TRUE, x0[2])≥NonInfC∧COND_F424_0_F_STORE1(TRUE, x0[2])≥F424_0_F_STORE'(-(x0[2], 2))∧(U^Increasing(F424_0_F_STORE'(-(x0[3], 2))), ≥))

We simplified constraint (20) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(21)    (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x0[3], 2))), ≥)∧[(-1)bni_70 + (-1)Bound*bni_70] ≥ 0∧[(-1)bso_71] ≥ 0)

We simplified constraint (21) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(22)    (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x0[3], 2))), ≥)∧[(-1)bni_70 + (-1)Bound*bni_70] ≥ 0∧[(-1)bso_71] ≥ 0)

We simplified constraint (22) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(23)    (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x0[3], 2))), ≥)∧[(-1)bni_70 + (-1)Bound*bni_70] ≥ 0∧[(-1)bso_71] ≥ 0)

We simplified constraint (23) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(24)    (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x0[3], 2))), ≥)∧0 ≥ 0∧[(-1)bni_70 + (-1)Bound*bni_70] ≥ 0∧0 ≥ 0∧[(-1)bso_71] ≥ 0)
We consider the chain F424_0_F_STORE'(x0[2]) → COND_F424_0_F_STORE1(>(x0[2], 0), x0[2]), COND_F424_0_F_STORE1(TRUE, x0[3]) → F424_0_F_STORE'(-(x0[3], 2)), F424_0_F_STORE'(x0[2]) → COND_F424_0_F_STORE1(>(x0[2], 0), x0[2]) which results in the following constraint:
(25)    (>(x0[2], 0)=TRUE∧x0[2]=x0[3]∧-(x0[3], 2)=x0[2]1 ⇒ COND_F424_0_F_STORE1(TRUE, x0[3])≥NonInfC∧COND_F424_0_F_STORE1(TRUE, x0[3])≥F424_0_F_STORE'(-(x0[3], 2))∧(U^Increasing(F424_0_F_STORE'(-(x0[3], 2))), ≥))

We simplified constraint (25) using rules (III), (IV) which results in the following new constraint:
(26)    (>(x0[2], 0)=TRUE ⇒ COND_F424_0_F_STORE1(TRUE, x0[2])≥NonInfC∧COND_F424_0_F_STORE1(TRUE, x0[2])≥F424_0_F_STORE'(-(x0[2], 2))∧(U^Increasing(F424_0_F_STORE'(-(x0[3], 2))), ≥))

We simplified constraint (26) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(27)    (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x0[3], 2))), ≥)∧[(-1)bni_70 + (-1)Bound*bni_70] ≥ 0∧[(-1)bso_71] ≥ 0)

We simplified constraint (27) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(28)    (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x0[3], 2))), ≥)∧[(-1)bni_70 + (-1)Bound*bni_70] ≥ 0∧[(-1)bso_71] ≥ 0)

We simplified constraint (28) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(29)    (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x0[3], 2))), ≥)∧[(-1)bni_70 + (-1)Bound*bni_70] ≥ 0∧[(-1)bso_71] ≥ 0)

We simplified constraint (29) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(30)    (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x0[3], 2))), ≥)∧0 ≥ 0∧[(-1)bni_70 + (-1)Bound*bni_70] ≥ 0∧0 ≥ 0∧[(-1)bso_71] ≥ 0)

For Pair F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0), x1, x2) → COND_F629_1_F_INVOKEMETHOD(&&(>(x1, 0), >(x2, 1)), f434_0_f_Return(x0), x1, x2) the following chains were created:

We consider the chain F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0[4]), x1[4], x2[4]) → COND_F629_1_F_INVOKEMETHOD(&&(>(x1[4], 0), >(x2[4], 1)), f434_0_f_Return(x0[4]), x1[4], x2[4]), COND_F629_1_F_INVOKEMETHOD(TRUE, f434_0_f_Return(x0[5]), x1[5], x2[5]) → F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[5], -(x2[5], 1))), x1[5], -(x2[5], 1)) which results in the following constraint:
(31)    (&&(>(x1[4], 0), >(x2[4], 1))=TRUE∧f434_0_f_Return(x0[4])=f434_0_f_Return(x0[5])∧x1[4]=x1[5]∧x2[4]=x2[5] ⇒ F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0[4]), x1[4], x2[4])≥NonInfC∧F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0[4]), x1[4], x2[4])≥COND_F629_1_F_INVOKEMETHOD(&&(>(x1[4], 0), >(x2[4], 1)), f434_0_f_Return(x0[4]), x1[4], x2[4])∧(U^Increasing(COND_F629_1_F_INVOKEMETHOD(&&(>(x1[4], 0), >(x2[4], 1)), f434_0_f_Return(x0[4]), x1[4], x2[4])), ≥))

We simplified constraint (31) using rules (I), (II), (IV) which results in the following new constraint:
(32)    (&&(>(x1[4], 0), >(x2[4], 1))=TRUE ⇒ F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0[4]), x1[4], x2[4])≥NonInfC∧F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0[4]), x1[4], x2[4])≥COND_F629_1_F_INVOKEMETHOD(&&(>(x1[4], 0), >(x2[4], 1)), f434_0_f_Return(x0[4]), x1[4], x2[4])∧(U^Increasing(COND_F629_1_F_INVOKEMETHOD(&&(>(x1[4], 0), >(x2[4], 1)), f434_0_f_Return(x0[4]), x1[4], x2[4])), ≥))

We simplified constraint (32) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(33)    (0 ≥ 0 ⇒ (U^Increasing(COND_F629_1_F_INVOKEMETHOD(&&(>(x1[4], 0), >(x2[4], 1)), f434_0_f_Return(x0[4]), x1[4], x2[4])), ≥)∧[(-1)bni_72 + (-1)Bound*bni_72] + [bni_72]x2[4] ≥ 0∧[(-1)bso_73] ≥ 0)

We simplified constraint (33) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(34)    (0 ≥ 0 ⇒ (U^Increasing(COND_F629_1_F_INVOKEMETHOD(&&(>(x1[4], 0), >(x2[4], 1)), f434_0_f_Return(x0[4]), x1[4], x2[4])), ≥)∧[(-1)bni_72 + (-1)Bound*bni_72] + [bni_72]x2[4] ≥ 0∧[(-1)bso_73] ≥ 0)

We simplified constraint (34) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(35)    (0 ≥ 0 ⇒ (U^Increasing(COND_F629_1_F_INVOKEMETHOD(&&(>(x1[4], 0), >(x2[4], 1)), f434_0_f_Return(x0[4]), x1[4], x2[4])), ≥)∧[(-1)bni_72 + (-1)Bound*bni_72] + [bni_72]x2[4] ≥ 0∧[(-1)bso_73] ≥ 0)

We simplified constraint (35) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(36)    (0 ≥ 0 ⇒ (U^Increasing(COND_F629_1_F_INVOKEMETHOD(&&(>(x1[4], 0), >(x2[4], 1)), f434_0_f_Return(x0[4]), x1[4], x2[4])), ≥)∧[bni_72] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_72 + (-1)Bound*bni_72] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_73] ≥ 0)

For Pair COND_F629_1_F_INVOKEMETHOD(TRUE, f434_0_f_Return(x0), x1, x2) → F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1, -(x2, 1))), x1, -(x2, 1)) the following chains were created:

We consider the chain F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0[4]), x1[4], x2[4]) → COND_F629_1_F_INVOKEMETHOD(&&(>(x1[4], 0), >(x2[4], 1)), f434_0_f_Return(x0[4]), x1[4], x2[4]), COND_F629_1_F_INVOKEMETHOD(TRUE, f434_0_f_Return(x0[5]), x1[5], x2[5]) → F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[5], -(x2[5], 1))), x1[5], -(x2[5], 1)) which results in the following constraint:
(37)    (&&(>(x1[4], 0), >(x2[4], 1))=TRUE∧f434_0_f_Return(x0[4])=f434_0_f_Return(x0[5])∧x1[4]=x1[5]∧x2[4]=x2[5] ⇒ COND_F629_1_F_INVOKEMETHOD(TRUE, f434_0_f_Return(x0[5]), x1[5], x2[5])≥NonInfC∧COND_F629_1_F_INVOKEMETHOD(TRUE, f434_0_f_Return(x0[5]), x1[5], x2[5])≥F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[5], -(x2[5], 1))), x1[5], -(x2[5], 1))∧(U^Increasing(F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[5], -(x2[5], 1))), x1[5], -(x2[5], 1))), ≥))

We simplified constraint (37) using rules (I), (II), (III) which results in the following new constraint:
(38)    (&&(>(x1[4], 0), >(x2[4], 1))=TRUE ⇒ COND_F629_1_F_INVOKEMETHOD(TRUE, f434_0_f_Return(x0[4]), x1[4], x2[4])≥NonInfC∧COND_F629_1_F_INVOKEMETHOD(TRUE, f434_0_f_Return(x0[4]), x1[4], x2[4])≥F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[4], -(x2[4], 1))), x1[4], -(x2[4], 1))∧(U^Increasing(F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[5], -(x2[5], 1))), x1[5], -(x2[5], 1))), ≥))

We simplified constraint (38) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(39)    (0 ≥ 0 ⇒ (U^Increasing(F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[5], -(x2[5], 1))), x1[5], -(x2[5], 1))), ≥)∧[(-1)bni_74 + (-1)Bound*bni_74] + [bni_74]x2[4] ≥ 0∧[1 + (-1)bso_75] + x2[4] ≥ 0)

We simplified constraint (39) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(40)    (0 ≥ 0 ⇒ (U^Increasing(F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[5], -(x2[5], 1))), x1[5], -(x2[5], 1))), ≥)∧[(-1)bni_74 + (-1)Bound*bni_74] + [bni_74]x2[4] ≥ 0∧[1 + (-1)bso_75] + x2[4] ≥ 0)

We simplified constraint (40) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(41)    (0 ≥ 0 ⇒ (U^Increasing(F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[5], -(x2[5], 1))), x1[5], -(x2[5], 1))), ≥)∧[(-1)bni_74 + (-1)Bound*bni_74] + [bni_74]x2[4] ≥ 0∧[1 + (-1)bso_75] + x2[4] ≥ 0)

We simplified constraint (41) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(42)    (0 ≥ 0 ⇒ (U^Increasing(F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[5], -(x2[5], 1))), x1[5], -(x2[5], 1))), ≥)∧[bni_74] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_74 + (-1)Bound*bni_74] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_75] ≥ 0)

For Pair F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0), x1, x2) → COND_F629_1_F_INVOKEMETHOD1(&&(>(x1, 0), >(x2, 1)), f434_0_f_Return(x0), x1, x2) the following chains were created:

We consider the chain F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0[6]), x1[6], x2[6]) → COND_F629_1_F_INVOKEMETHOD1(&&(>(x1[6], 0), >(x2[6], 1)), f434_0_f_Return(x0[6]), x1[6], x2[6]), COND_F629_1_F_INVOKEMETHOD1(TRUE, f434_0_f_Return(x0[7]), x1[7], x2[7]) → F424_0_F_STORE'(-(x1[7], -(x2[7], 1))) which results in the following constraint:
(43)    (&&(>(x1[6], 0), >(x2[6], 1))=TRUE∧f434_0_f_Return(x0[6])=f434_0_f_Return(x0[7])∧x1[6]=x1[7]∧x2[6]=x2[7] ⇒ F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0[6]), x1[6], x2[6])≥NonInfC∧F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0[6]), x1[6], x2[6])≥COND_F629_1_F_INVOKEMETHOD1(&&(>(x1[6], 0), >(x2[6], 1)), f434_0_f_Return(x0[6]), x1[6], x2[6])∧(U^Increasing(COND_F629_1_F_INVOKEMETHOD1(&&(>(x1[6], 0), >(x2[6], 1)), f434_0_f_Return(x0[6]), x1[6], x2[6])), ≥))

We simplified constraint (43) using rules (I), (II), (IV) which results in the following new constraint:
(44)    (&&(>(x1[6], 0), >(x2[6], 1))=TRUE ⇒ F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0[6]), x1[6], x2[6])≥NonInfC∧F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0[6]), x1[6], x2[6])≥COND_F629_1_F_INVOKEMETHOD1(&&(>(x1[6], 0), >(x2[6], 1)), f434_0_f_Return(x0[6]), x1[6], x2[6])∧(U^Increasing(COND_F629_1_F_INVOKEMETHOD1(&&(>(x1[6], 0), >(x2[6], 1)), f434_0_f_Return(x0[6]), x1[6], x2[6])), ≥))

We simplified constraint (44) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(45)    (0 ≥ 0 ⇒ (U^Increasing(COND_F629_1_F_INVOKEMETHOD1(&&(>(x1[6], 0), >(x2[6], 1)), f434_0_f_Return(x0[6]), x1[6], x2[6])), ≥)∧[(-1)bni_76 + (-1)Bound*bni_76] + [bni_76]x2[6] ≥ 0∧[(-1)bso_77] ≥ 0)

We simplified constraint (45) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(46)    (0 ≥ 0 ⇒ (U^Increasing(COND_F629_1_F_INVOKEMETHOD1(&&(>(x1[6], 0), >(x2[6], 1)), f434_0_f_Return(x0[6]), x1[6], x2[6])), ≥)∧[(-1)bni_76 + (-1)Bound*bni_76] + [bni_76]x2[6] ≥ 0∧[(-1)bso_77] ≥ 0)

We simplified constraint (46) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(47)    (0 ≥ 0 ⇒ (U^Increasing(COND_F629_1_F_INVOKEMETHOD1(&&(>(x1[6], 0), >(x2[6], 1)), f434_0_f_Return(x0[6]), x1[6], x2[6])), ≥)∧[(-1)bni_76 + (-1)Bound*bni_76] + [bni_76]x2[6] ≥ 0∧[(-1)bso_77] ≥ 0)

We simplified constraint (47) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(48)    (0 ≥ 0 ⇒ (U^Increasing(COND_F629_1_F_INVOKEMETHOD1(&&(>(x1[6], 0), >(x2[6], 1)), f434_0_f_Return(x0[6]), x1[6], x2[6])), ≥)∧[bni_76] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_76 + (-1)Bound*bni_76] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_77] ≥ 0)

For Pair COND_F629_1_F_INVOKEMETHOD1(TRUE, f434_0_f_Return(x0), x1, x2) → F424_0_F_STORE'(-(x1, -(x2, 1))) the following chains were created:

We consider the chain F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0[6]), x1[6], x2[6]) → COND_F629_1_F_INVOKEMETHOD1(&&(>(x1[6], 0), >(x2[6], 1)), f434_0_f_Return(x0[6]), x1[6], x2[6]), COND_F629_1_F_INVOKEMETHOD1(TRUE, f434_0_f_Return(x0[7]), x1[7], x2[7]) → F424_0_F_STORE'(-(x1[7], -(x2[7], 1))), F424_0_F_STORE'(x0[0]) → COND_F424_0_F_STORE(>(x0[0], 0), x0[0]) which results in the following constraint:
(49)    (&&(>(x1[6], 0), >(x2[6], 1))=TRUE∧f434_0_f_Return(x0[6])=f434_0_f_Return(x0[7])∧x1[6]=x1[7]∧x2[6]=x2[7]∧-(x1[7], -(x2[7], 1))=x0[0] ⇒ COND_F629_1_F_INVOKEMETHOD1(TRUE, f434_0_f_Return(x0[7]), x1[7], x2[7])≥NonInfC∧COND_F629_1_F_INVOKEMETHOD1(TRUE, f434_0_f_Return(x0[7]), x1[7], x2[7])≥F424_0_F_STORE'(-(x1[7], -(x2[7], 1)))∧(U^Increasing(F424_0_F_STORE'(-(x1[7], -(x2[7], 1)))), ≥))

We simplified constraint (49) using rules (I), (II), (III), (IV) which results in the following new constraint:
(50)    (&&(>(x1[6], 0), >(x2[6], 1))=TRUE ⇒ COND_F629_1_F_INVOKEMETHOD1(TRUE, f434_0_f_Return(x0[6]), x1[6], x2[6])≥NonInfC∧COND_F629_1_F_INVOKEMETHOD1(TRUE, f434_0_f_Return(x0[6]), x1[6], x2[6])≥F424_0_F_STORE'(-(x1[6], -(x2[6], 1)))∧(U^Increasing(F424_0_F_STORE'(-(x1[7], -(x2[7], 1)))), ≥))

We simplified constraint (50) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(51)    (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x1[7], -(x2[7], 1)))), ≥)∧[(-1)bni_78 + (-1)Bound*bni_78] + [bni_78]x2[6] ≥ 0∧[(-1)bso_79] + x2[6] ≥ 0)

We simplified constraint (51) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(52)    (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x1[7], -(x2[7], 1)))), ≥)∧[(-1)bni_78 + (-1)Bound*bni_78] + [bni_78]x2[6] ≥ 0∧[(-1)bso_79] + x2[6] ≥ 0)

We simplified constraint (52) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(53)    (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x1[7], -(x2[7], 1)))), ≥)∧[(-1)bni_78 + (-1)Bound*bni_78] + [bni_78]x2[6] ≥ 0∧[(-1)bso_79] + x2[6] ≥ 0)

We simplified constraint (53) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(54)    (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x1[7], -(x2[7], 1)))), ≥)∧[bni_78] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_78 + (-1)Bound*bni_78] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_79] ≥ 0)
We consider the chain F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0[6]), x1[6], x2[6]) → COND_F629_1_F_INVOKEMETHOD1(&&(>(x1[6], 0), >(x2[6], 1)), f434_0_f_Return(x0[6]), x1[6], x2[6]), COND_F629_1_F_INVOKEMETHOD1(TRUE, f434_0_f_Return(x0[7]), x1[7], x2[7]) → F424_0_F_STORE'(-(x1[7], -(x2[7], 1))), F424_0_F_STORE'(x0[2]) → COND_F424_0_F_STORE1(>(x0[2], 0), x0[2]) which results in the following constraint:
(55)    (&&(>(x1[6], 0), >(x2[6], 1))=TRUE∧f434_0_f_Return(x0[6])=f434_0_f_Return(x0[7])∧x1[6]=x1[7]∧x2[6]=x2[7]∧-(x1[7], -(x2[7], 1))=x0[2] ⇒ COND_F629_1_F_INVOKEMETHOD1(TRUE, f434_0_f_Return(x0[7]), x1[7], x2[7])≥NonInfC∧COND_F629_1_F_INVOKEMETHOD1(TRUE, f434_0_f_Return(x0[7]), x1[7], x2[7])≥F424_0_F_STORE'(-(x1[7], -(x2[7], 1)))∧(U^Increasing(F424_0_F_STORE'(-(x1[7], -(x2[7], 1)))), ≥))

We simplified constraint (55) using rules (I), (II), (III), (IV) which results in the following new constraint:
(56)    (&&(>(x1[6], 0), >(x2[6], 1))=TRUE ⇒ COND_F629_1_F_INVOKEMETHOD1(TRUE, f434_0_f_Return(x0[6]), x1[6], x2[6])≥NonInfC∧COND_F629_1_F_INVOKEMETHOD1(TRUE, f434_0_f_Return(x0[6]), x1[6], x2[6])≥F424_0_F_STORE'(-(x1[6], -(x2[6], 1)))∧(U^Increasing(F424_0_F_STORE'(-(x1[7], -(x2[7], 1)))), ≥))

We simplified constraint (56) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(57)    (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x1[7], -(x2[7], 1)))), ≥)∧[(-1)bni_78 + (-1)Bound*bni_78] + [bni_78]x2[6] ≥ 0∧[(-1)bso_79] + x2[6] ≥ 0)

We simplified constraint (57) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(58)    (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x1[7], -(x2[7], 1)))), ≥)∧[(-1)bni_78 + (-1)Bound*bni_78] + [bni_78]x2[6] ≥ 0∧[(-1)bso_79] + x2[6] ≥ 0)

We simplified constraint (58) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(59)    (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x1[7], -(x2[7], 1)))), ≥)∧[(-1)bni_78 + (-1)Bound*bni_78] + [bni_78]x2[6] ≥ 0∧[(-1)bso_79] + x2[6] ≥ 0)

We simplified constraint (59) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(60)    (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x1[7], -(x2[7], 1)))), ≥)∧[bni_78] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_78 + (-1)Bound*bni_78] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_79] ≥ 0)

For Pair F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0), x1, x2) → COND_F629_1_F_INVOKEMETHOD2(&&(>(x1, 0), >(x2, 1)), f584_0_f_Return(x0), x1, x2) the following chains were created:

We consider the chain F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0[8]), x1[8], x2[8]) → COND_F629_1_F_INVOKEMETHOD2(&&(>(x1[8], 0), >(x2[8], 1)), f584_0_f_Return(x0[8]), x1[8], x2[8]), COND_F629_1_F_INVOKEMETHOD2(TRUE, f584_0_f_Return(x0[9]), x1[9], x2[9]) → F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[9], -(x2[9], 1))), x1[9], -(x2[9], 1)) which results in the following constraint:
(61)    (&&(>(x1[8], 0), >(x2[8], 1))=TRUE∧f584_0_f_Return(x0[8])=f584_0_f_Return(x0[9])∧x1[8]=x1[9]∧x2[8]=x2[9] ⇒ F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0[8]), x1[8], x2[8])≥NonInfC∧F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0[8]), x1[8], x2[8])≥COND_F629_1_F_INVOKEMETHOD2(&&(>(x1[8], 0), >(x2[8], 1)), f584_0_f_Return(x0[8]), x1[8], x2[8])∧(U^Increasing(COND_F629_1_F_INVOKEMETHOD2(&&(>(x1[8], 0), >(x2[8], 1)), f584_0_f_Return(x0[8]), x1[8], x2[8])), ≥))

We simplified constraint (61) using rules (I), (II), (IV) which results in the following new constraint:
(62)    (&&(>(x1[8], 0), >(x2[8], 1))=TRUE ⇒ F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0[8]), x1[8], x2[8])≥NonInfC∧F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0[8]), x1[8], x2[8])≥COND_F629_1_F_INVOKEMETHOD2(&&(>(x1[8], 0), >(x2[8], 1)), f584_0_f_Return(x0[8]), x1[8], x2[8])∧(U^Increasing(COND_F629_1_F_INVOKEMETHOD2(&&(>(x1[8], 0), >(x2[8], 1)), f584_0_f_Return(x0[8]), x1[8], x2[8])), ≥))

We simplified constraint (62) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(63)    (0 ≥ 0 ⇒ (U^Increasing(COND_F629_1_F_INVOKEMETHOD2(&&(>(x1[8], 0), >(x2[8], 1)), f584_0_f_Return(x0[8]), x1[8], x2[8])), ≥)∧[(-1)bni_80 + (-1)Bound*bni_80] + [bni_80]x2[8] ≥ 0∧[(-1)bso_81] ≥ 0)

We simplified constraint (63) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(64)    (0 ≥ 0 ⇒ (U^Increasing(COND_F629_1_F_INVOKEMETHOD2(&&(>(x1[8], 0), >(x2[8], 1)), f584_0_f_Return(x0[8]), x1[8], x2[8])), ≥)∧[(-1)bni_80 + (-1)Bound*bni_80] + [bni_80]x2[8] ≥ 0∧[(-1)bso_81] ≥ 0)

We simplified constraint (64) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(65)    (0 ≥ 0 ⇒ (U^Increasing(COND_F629_1_F_INVOKEMETHOD2(&&(>(x1[8], 0), >(x2[8], 1)), f584_0_f_Return(x0[8]), x1[8], x2[8])), ≥)∧[(-1)bni_80 + (-1)Bound*bni_80] + [bni_80]x2[8] ≥ 0∧[(-1)bso_81] ≥ 0)

We simplified constraint (65) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(66)    (0 ≥ 0 ⇒ (U^Increasing(COND_F629_1_F_INVOKEMETHOD2(&&(>(x1[8], 0), >(x2[8], 1)), f584_0_f_Return(x0[8]), x1[8], x2[8])), ≥)∧[bni_80] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_80 + (-1)Bound*bni_80] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_81] ≥ 0)

For Pair COND_F629_1_F_INVOKEMETHOD2(TRUE, f584_0_f_Return(x0), x1, x2) → F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1, -(x2, 1))), x1, -(x2, 1)) the following chains were created:

We consider the chain F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0[8]), x1[8], x2[8]) → COND_F629_1_F_INVOKEMETHOD2(&&(>(x1[8], 0), >(x2[8], 1)), f584_0_f_Return(x0[8]), x1[8], x2[8]), COND_F629_1_F_INVOKEMETHOD2(TRUE, f584_0_f_Return(x0[9]), x1[9], x2[9]) → F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[9], -(x2[9], 1))), x1[9], -(x2[9], 1)) which results in the following constraint:
(67)    (&&(>(x1[8], 0), >(x2[8], 1))=TRUE∧f584_0_f_Return(x0[8])=f584_0_f_Return(x0[9])∧x1[8]=x1[9]∧x2[8]=x2[9] ⇒ COND_F629_1_F_INVOKEMETHOD2(TRUE, f584_0_f_Return(x0[9]), x1[9], x2[9])≥NonInfC∧COND_F629_1_F_INVOKEMETHOD2(TRUE, f584_0_f_Return(x0[9]), x1[9], x2[9])≥F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[9], -(x2[9], 1))), x1[9], -(x2[9], 1))∧(U^Increasing(F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[9], -(x2[9], 1))), x1[9], -(x2[9], 1))), ≥))

We simplified constraint (67) using rules (I), (II), (III) which results in the following new constraint:
(68)    (&&(>(x1[8], 0), >(x2[8], 1))=TRUE ⇒ COND_F629_1_F_INVOKEMETHOD2(TRUE, f584_0_f_Return(x0[8]), x1[8], x2[8])≥NonInfC∧COND_F629_1_F_INVOKEMETHOD2(TRUE, f584_0_f_Return(x0[8]), x1[8], x2[8])≥F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[8], -(x2[8], 1))), x1[8], -(x2[8], 1))∧(U^Increasing(F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[9], -(x2[9], 1))), x1[9], -(x2[9], 1))), ≥))

We simplified constraint (68) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(69)    (0 ≥ 0 ⇒ (U^Increasing(F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[9], -(x2[9], 1))), x1[9], -(x2[9], 1))), ≥)∧[(-1)bni_82 + (-1)Bound*bni_82] + [bni_82]x2[8] ≥ 0∧[1 + (-1)bso_83] + x2[8] ≥ 0)

We simplified constraint (69) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(70)    (0 ≥ 0 ⇒ (U^Increasing(F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[9], -(x2[9], 1))), x1[9], -(x2[9], 1))), ≥)∧[(-1)bni_82 + (-1)Bound*bni_82] + [bni_82]x2[8] ≥ 0∧[1 + (-1)bso_83] + x2[8] ≥ 0)

We simplified constraint (70) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(71)    (0 ≥ 0 ⇒ (U^Increasing(F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[9], -(x2[9], 1))), x1[9], -(x2[9], 1))), ≥)∧[(-1)bni_82 + (-1)Bound*bni_82] + [bni_82]x2[8] ≥ 0∧[1 + (-1)bso_83] + x2[8] ≥ 0)

We simplified constraint (71) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(72)    (0 ≥ 0 ⇒ (U^Increasing(F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[9], -(x2[9], 1))), x1[9], -(x2[9], 1))), ≥)∧[bni_82] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_82 + (-1)Bound*bni_82] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_83] ≥ 0)

For Pair F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0), x1, x2) → COND_F629_1_F_INVOKEMETHOD3(&&(>(x1, 0), >(x2, 1)), f584_0_f_Return(x0), x1, x2) the following chains were created:

We consider the chain F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0[10]), x1[10], x2[10]) → COND_F629_1_F_INVOKEMETHOD3(&&(>(x1[10], 0), >(x2[10], 1)), f584_0_f_Return(x0[10]), x1[10], x2[10]), COND_F629_1_F_INVOKEMETHOD3(TRUE, f584_0_f_Return(x0[11]), x1[11], x2[11]) → F424_0_F_STORE'(-(x1[11], -(x2[11], 1))) which results in the following constraint:
(73)    (&&(>(x1[10], 0), >(x2[10], 1))=TRUE∧f584_0_f_Return(x0[10])=f584_0_f_Return(x0[11])∧x1[10]=x1[11]∧x2[10]=x2[11] ⇒ F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0[10]), x1[10], x2[10])≥NonInfC∧F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0[10]), x1[10], x2[10])≥COND_F629_1_F_INVOKEMETHOD3(&&(>(x1[10], 0), >(x2[10], 1)), f584_0_f_Return(x0[10]), x1[10], x2[10])∧(U^Increasing(COND_F629_1_F_INVOKEMETHOD3(&&(>(x1[10], 0), >(x2[10], 1)), f584_0_f_Return(x0[10]), x1[10], x2[10])), ≥))

We simplified constraint (73) using rules (I), (II), (IV) which results in the following new constraint:
(74)    (&&(>(x1[10], 0), >(x2[10], 1))=TRUE ⇒ F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0[10]), x1[10], x2[10])≥NonInfC∧F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0[10]), x1[10], x2[10])≥COND_F629_1_F_INVOKEMETHOD3(&&(>(x1[10], 0), >(x2[10], 1)), f584_0_f_Return(x0[10]), x1[10], x2[10])∧(U^Increasing(COND_F629_1_F_INVOKEMETHOD3(&&(>(x1[10], 0), >(x2[10], 1)), f584_0_f_Return(x0[10]), x1[10], x2[10])), ≥))

We simplified constraint (74) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(75)    (0 ≥ 0 ⇒ (U^Increasing(COND_F629_1_F_INVOKEMETHOD3(&&(>(x1[10], 0), >(x2[10], 1)), f584_0_f_Return(x0[10]), x1[10], x2[10])), ≥)∧[(-1)bni_84 + (-1)Bound*bni_84] + [bni_84]x2[10] ≥ 0∧[(-1)bso_85] ≥ 0)

We simplified constraint (75) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(76)    (0 ≥ 0 ⇒ (U^Increasing(COND_F629_1_F_INVOKEMETHOD3(&&(>(x1[10], 0), >(x2[10], 1)), f584_0_f_Return(x0[10]), x1[10], x2[10])), ≥)∧[(-1)bni_84 + (-1)Bound*bni_84] + [bni_84]x2[10] ≥ 0∧[(-1)bso_85] ≥ 0)

We simplified constraint (76) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(77)    (0 ≥ 0 ⇒ (U^Increasing(COND_F629_1_F_INVOKEMETHOD3(&&(>(x1[10], 0), >(x2[10], 1)), f584_0_f_Return(x0[10]), x1[10], x2[10])), ≥)∧[(-1)bni_84 + (-1)Bound*bni_84] + [bni_84]x2[10] ≥ 0∧[(-1)bso_85] ≥ 0)

We simplified constraint (77) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(78)    (0 ≥ 0 ⇒ (U^Increasing(COND_F629_1_F_INVOKEMETHOD3(&&(>(x1[10], 0), >(x2[10], 1)), f584_0_f_Return(x0[10]), x1[10], x2[10])), ≥)∧[bni_84] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_84 + (-1)Bound*bni_84] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_85] ≥ 0)

For Pair COND_F629_1_F_INVOKEMETHOD3(TRUE, f584_0_f_Return(x0), x1, x2) → F424_0_F_STORE'(-(x1, -(x2, 1))) the following chains were created:

We consider the chain F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0[10]), x1[10], x2[10]) → COND_F629_1_F_INVOKEMETHOD3(&&(>(x1[10], 0), >(x2[10], 1)), f584_0_f_Return(x0[10]), x1[10], x2[10]), COND_F629_1_F_INVOKEMETHOD3(TRUE, f584_0_f_Return(x0[11]), x1[11], x2[11]) → F424_0_F_STORE'(-(x1[11], -(x2[11], 1))), F424_0_F_STORE'(x0[0]) → COND_F424_0_F_STORE(>(x0[0], 0), x0[0]) which results in the following constraint:
(79)    (&&(>(x1[10], 0), >(x2[10], 1))=TRUE∧f584_0_f_Return(x0[10])=f584_0_f_Return(x0[11])∧x1[10]=x1[11]∧x2[10]=x2[11]∧-(x1[11], -(x2[11], 1))=x0[0] ⇒ COND_F629_1_F_INVOKEMETHOD3(TRUE, f584_0_f_Return(x0[11]), x1[11], x2[11])≥NonInfC∧COND_F629_1_F_INVOKEMETHOD3(TRUE, f584_0_f_Return(x0[11]), x1[11], x2[11])≥F424_0_F_STORE'(-(x1[11], -(x2[11], 1)))∧(U^Increasing(F424_0_F_STORE'(-(x1[11], -(x2[11], 1)))), ≥))

We simplified constraint (79) using rules (I), (II), (III), (IV) which results in the following new constraint:
(80)    (&&(>(x1[10], 0), >(x2[10], 1))=TRUE ⇒ COND_F629_1_F_INVOKEMETHOD3(TRUE, f584_0_f_Return(x0[10]), x1[10], x2[10])≥NonInfC∧COND_F629_1_F_INVOKEMETHOD3(TRUE, f584_0_f_Return(x0[10]), x1[10], x2[10])≥F424_0_F_STORE'(-(x1[10], -(x2[10], 1)))∧(U^Increasing(F424_0_F_STORE'(-(x1[11], -(x2[11], 1)))), ≥))

We simplified constraint (80) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(81)    (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x1[11], -(x2[11], 1)))), ≥)∧[(-1)bni_86 + (-1)Bound*bni_86] + [bni_86]x2[10] ≥ 0∧[(-1)bso_87] + x2[10] ≥ 0)

We simplified constraint (81) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(82)    (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x1[11], -(x2[11], 1)))), ≥)∧[(-1)bni_86 + (-1)Bound*bni_86] + [bni_86]x2[10] ≥ 0∧[(-1)bso_87] + x2[10] ≥ 0)

We simplified constraint (82) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(83)    (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x1[11], -(x2[11], 1)))), ≥)∧[(-1)bni_86 + (-1)Bound*bni_86] + [bni_86]x2[10] ≥ 0∧[(-1)bso_87] + x2[10] ≥ 0)

We simplified constraint (83) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(84)    (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x1[11], -(x2[11], 1)))), ≥)∧[bni_86] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_86 + (-1)Bound*bni_86] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_87] ≥ 0)
We consider the chain F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0[10]), x1[10], x2[10]) → COND_F629_1_F_INVOKEMETHOD3(&&(>(x1[10], 0), >(x2[10], 1)), f584_0_f_Return(x0[10]), x1[10], x2[10]), COND_F629_1_F_INVOKEMETHOD3(TRUE, f584_0_f_Return(x0[11]), x1[11], x2[11]) → F424_0_F_STORE'(-(x1[11], -(x2[11], 1))), F424_0_F_STORE'(x0[2]) → COND_F424_0_F_STORE1(>(x0[2], 0), x0[2]) which results in the following constraint:
(85)    (&&(>(x1[10], 0), >(x2[10], 1))=TRUE∧f584_0_f_Return(x0[10])=f584_0_f_Return(x0[11])∧x1[10]=x1[11]∧x2[10]=x2[11]∧-(x1[11], -(x2[11], 1))=x0[2] ⇒ COND_F629_1_F_INVOKEMETHOD3(TRUE, f584_0_f_Return(x0[11]), x1[11], x2[11])≥NonInfC∧COND_F629_1_F_INVOKEMETHOD3(TRUE, f584_0_f_Return(x0[11]), x1[11], x2[11])≥F424_0_F_STORE'(-(x1[11], -(x2[11], 1)))∧(U^Increasing(F424_0_F_STORE'(-(x1[11], -(x2[11], 1)))), ≥))

We simplified constraint (85) using rules (I), (II), (III), (IV) which results in the following new constraint:
(86)    (&&(>(x1[10], 0), >(x2[10], 1))=TRUE ⇒ COND_F629_1_F_INVOKEMETHOD3(TRUE, f584_0_f_Return(x0[10]), x1[10], x2[10])≥NonInfC∧COND_F629_1_F_INVOKEMETHOD3(TRUE, f584_0_f_Return(x0[10]), x1[10], x2[10])≥F424_0_F_STORE'(-(x1[10], -(x2[10], 1)))∧(U^Increasing(F424_0_F_STORE'(-(x1[11], -(x2[11], 1)))), ≥))

We simplified constraint (86) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(87)    (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x1[11], -(x2[11], 1)))), ≥)∧[(-1)bni_86 + (-1)Bound*bni_86] + [bni_86]x2[10] ≥ 0∧[(-1)bso_87] + x2[10] ≥ 0)

We simplified constraint (87) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(88)    (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x1[11], -(x2[11], 1)))), ≥)∧[(-1)bni_86 + (-1)Bound*bni_86] + [bni_86]x2[10] ≥ 0∧[(-1)bso_87] + x2[10] ≥ 0)

We simplified constraint (88) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(89)    (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x1[11], -(x2[11], 1)))), ≥)∧[(-1)bni_86 + (-1)Bound*bni_86] + [bni_86]x2[10] ≥ 0∧[(-1)bso_87] + x2[10] ≥ 0)

We simplified constraint (89) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(90)    (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x1[11], -(x2[11], 1)))), ≥)∧[bni_86] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_86 + (-1)Bound*bni_86] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_87] ≥ 0)

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

F424_0_F_STORE'(x0) → COND_F424_0_F_STORE(>(x0, 0), x0)
- (0 ≥ 0 ⇒ (U^Increasing(COND_F424_0_F_STORE(>(x0[0], 0), x0[0])), ≥)∧[bni_64] ≥ 0∧[(-1)bni_64 + (-1)Bound*bni_64] ≥ 0∧[1] ≥ 0∧[(-1)bso_65] ≥ 0)
COND_F424_0_F_STORE(TRUE, x0) → F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x0, 2)), x0, 2)
- (0 ≥ 0 ⇒ (U^Increasing(F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x0[1], 2)), x0[1], 2)), ≥)∧0 ≥ 0∧[(-1)bni_66 + (-1)Bound*bni_66] ≥ 0∧0 ≥ 0∧[1 + (-1)bso_67] ≥ 0)
F424_0_F_STORE'(x0) → COND_F424_0_F_STORE1(>(x0, 0), x0)
- (0 ≥ 0 ⇒ (U^Increasing(COND_F424_0_F_STORE1(>(x0[2], 0), x0[2])), ≥)∧[bni_68] ≥ 0∧[(-1)bni_68 + (-1)Bound*bni_68] ≥ 0∧[1] ≥ 0∧[(-1)bso_69] ≥ 0)
COND_F424_0_F_STORE1(TRUE, x0) → F424_0_F_STORE'(-(x0, 2))
- (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x0[3], 2))), ≥)∧0 ≥ 0∧[(-1)bni_70 + (-1)Bound*bni_70] ≥ 0∧0 ≥ 0∧[(-1)bso_71] ≥ 0)
- (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x0[3], 2))), ≥)∧0 ≥ 0∧[(-1)bni_70 + (-1)Bound*bni_70] ≥ 0∧0 ≥ 0∧[(-1)bso_71] ≥ 0)
F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0), x1, x2) → COND_F629_1_F_INVOKEMETHOD(&&(>(x1, 0), >(x2, 1)), f434_0_f_Return(x0), x1, x2)
- (0 ≥ 0 ⇒ (U^Increasing(COND_F629_1_F_INVOKEMETHOD(&&(>(x1[4], 0), >(x2[4], 1)), f434_0_f_Return(x0[4]), x1[4], x2[4])), ≥)∧[bni_72] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_72 + (-1)Bound*bni_72] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_73] ≥ 0)
COND_F629_1_F_INVOKEMETHOD(TRUE, f434_0_f_Return(x0), x1, x2) → F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1, -(x2, 1))), x1, -(x2, 1))
- (0 ≥ 0 ⇒ (U^Increasing(F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[5], -(x2[5], 1))), x1[5], -(x2[5], 1))), ≥)∧[bni_74] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_74 + (-1)Bound*bni_74] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_75] ≥ 0)
F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0), x1, x2) → COND_F629_1_F_INVOKEMETHOD1(&&(>(x1, 0), >(x2, 1)), f434_0_f_Return(x0), x1, x2)
- (0 ≥ 0 ⇒ (U^Increasing(COND_F629_1_F_INVOKEMETHOD1(&&(>(x1[6], 0), >(x2[6], 1)), f434_0_f_Return(x0[6]), x1[6], x2[6])), ≥)∧[bni_76] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_76 + (-1)Bound*bni_76] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_77] ≥ 0)
COND_F629_1_F_INVOKEMETHOD1(TRUE, f434_0_f_Return(x0), x1, x2) → F424_0_F_STORE'(-(x1, -(x2, 1)))
- (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x1[7], -(x2[7], 1)))), ≥)∧[bni_78] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_78 + (-1)Bound*bni_78] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_79] ≥ 0)
- (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x1[7], -(x2[7], 1)))), ≥)∧[bni_78] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_78 + (-1)Bound*bni_78] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_79] ≥ 0)
F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0), x1, x2) → COND_F629_1_F_INVOKEMETHOD2(&&(>(x1, 0), >(x2, 1)), f584_0_f_Return(x0), x1, x2)
- (0 ≥ 0 ⇒ (U^Increasing(COND_F629_1_F_INVOKEMETHOD2(&&(>(x1[8], 0), >(x2[8], 1)), f584_0_f_Return(x0[8]), x1[8], x2[8])), ≥)∧[bni_80] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_80 + (-1)Bound*bni_80] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_81] ≥ 0)
COND_F629_1_F_INVOKEMETHOD2(TRUE, f584_0_f_Return(x0), x1, x2) → F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1, -(x2, 1))), x1, -(x2, 1))
- (0 ≥ 0 ⇒ (U^Increasing(F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[9], -(x2[9], 1))), x1[9], -(x2[9], 1))), ≥)∧[bni_82] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_82 + (-1)Bound*bni_82] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_83] ≥ 0)
F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0), x1, x2) → COND_F629_1_F_INVOKEMETHOD3(&&(>(x1, 0), >(x2, 1)), f584_0_f_Return(x0), x1, x2)
- (0 ≥ 0 ⇒ (U^Increasing(COND_F629_1_F_INVOKEMETHOD3(&&(>(x1[10], 0), >(x2[10], 1)), f584_0_f_Return(x0[10]), x1[10], x2[10])), ≥)∧[bni_84] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_84 + (-1)Bound*bni_84] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_85] ≥ 0)
COND_F629_1_F_INVOKEMETHOD3(TRUE, f584_0_f_Return(x0), x1, x2) → F424_0_F_STORE'(-(x1, -(x2, 1)))
- (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x1[11], -(x2[11], 1)))), ≥)∧[bni_86] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_86 + (-1)Bound*bni_86] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_87] ≥ 0)
- (0 ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x1[11], -(x2[11], 1)))), ≥)∧[bni_86] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bni_86 + (-1)Bound*bni_86] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_87] ≥ 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 with natural coefficients for non-tuple symbols [NONINF][POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(f578_0_f_LE(x₁, x₂)) = 0
POL(0) = 0
POL(f584_0_f_Return(x₁)) = 0
POL(f629_1_f_InvokeMethod(x₁, x₂, x₃)) = 0
POL(f434_0_f_Return(x₁)) = 0
POL(Cond_f629_1_f_InvokeMethod(x₁, x₂, x₃, x₄)) = 0
POL(>(x₁, x₂)) = 0
POL(-(x₁, x₂)) = 0
POL(1) = 0
POL(Cond_f629_1_f_InvokeMethod1(x₁, x₂, x₃, x₄)) = 0
POL(Cond_f578_0_f_LE(x₁, x₂, x₃)) = 0
POL(&&(x₁, x₂)) = 0
POL(<=(x₁, x₂)) = 0
POL(Cond_f578_0_f_LE1(x₁, x₂, x₃)) = 0
POL(2) = 0
POL(F424_0_F_STORE'(x₁)) = [-1] + x₁
POL(COND_F424_0_F_STORE(x₁, x₂)) = [-1]
POL(F629_1_F_INVOKEMETHOD'(x₁, x₂, x₃)) = [-1] + x₃ + [-1]x₁
POL(f424_0_f_Store(x₁)) = [1]
POL(COND_F424_0_F_STORE1(x₁, x₂)) = [-1]
POL(COND_F629_1_F_INVOKEMETHOD(x₁, x₂, x₃, x₄)) = [-1] + x₄ + [-1]x₂ + [2]x₁
POL(COND_F629_1_F_INVOKEMETHOD1(x₁, x₂, x₃, x₄)) = [-1] + x₄ + [-1]x₂
POL(COND_F629_1_F_INVOKEMETHOD2(x₁, x₂, x₃, x₄)) = [-1] + x₄ + [-1]x₂ + x₁
POL(COND_F629_1_F_INVOKEMETHOD3(x₁, x₂, x₃, x₄)) = [-1] + x₄ + [-1]x₂ + [2]x₁

The following pairs are in P_>:

COND_F424_0_F_STORE(TRUE, x0[1]) → F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x0[1], 2)), x0[1], 2)
COND_F629_1_F_INVOKEMETHOD(TRUE, f434_0_f_Return(x0[5]), x1[5], x2[5]) → F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[5], -(x2[5], 1))), x1[5], -(x2[5], 1))
COND_F629_1_F_INVOKEMETHOD2(TRUE, f584_0_f_Return(x0[9]), x1[9], x2[9]) → F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[9], -(x2[9], 1))), x1[9], -(x2[9], 1))

The following pairs are in P_bound:

F424_0_F_STORE'(x0[0]) → COND_F424_0_F_STORE(>(x0[0], 0), x0[0])
COND_F424_0_F_STORE(TRUE, x0[1]) → F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x0[1], 2)), x0[1], 2)
F424_0_F_STORE'(x0[2]) → COND_F424_0_F_STORE1(>(x0[2], 0), x0[2])
COND_F424_0_F_STORE1(TRUE, x0[3]) → F424_0_F_STORE'(-(x0[3], 2))
F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0[4]), x1[4], x2[4]) → COND_F629_1_F_INVOKEMETHOD(&&(>(x1[4], 0), >(x2[4], 1)), f434_0_f_Return(x0[4]), x1[4], x2[4])
COND_F629_1_F_INVOKEMETHOD(TRUE, f434_0_f_Return(x0[5]), x1[5], x2[5]) → F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[5], -(x2[5], 1))), x1[5], -(x2[5], 1))
F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0[6]), x1[6], x2[6]) → COND_F629_1_F_INVOKEMETHOD1(&&(>(x1[6], 0), >(x2[6], 1)), f434_0_f_Return(x0[6]), x1[6], x2[6])
COND_F629_1_F_INVOKEMETHOD1(TRUE, f434_0_f_Return(x0[7]), x1[7], x2[7]) → F424_0_F_STORE'(-(x1[7], -(x2[7], 1)))
F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0[8]), x1[8], x2[8]) → COND_F629_1_F_INVOKEMETHOD2(&&(>(x1[8], 0), >(x2[8], 1)), f584_0_f_Return(x0[8]), x1[8], x2[8])
COND_F629_1_F_INVOKEMETHOD2(TRUE, f584_0_f_Return(x0[9]), x1[9], x2[9]) → F629_1_F_INVOKEMETHOD'(f424_0_f_Store(-(x1[9], -(x2[9], 1))), x1[9], -(x2[9], 1))
F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0[10]), x1[10], x2[10]) → COND_F629_1_F_INVOKEMETHOD3(&&(>(x1[10], 0), >(x2[10], 1)), f584_0_f_Return(x0[10]), x1[10], x2[10])
COND_F629_1_F_INVOKEMETHOD3(TRUE, f584_0_f_Return(x0[11]), x1[11], x2[11]) → F424_0_F_STORE'(-(x1[11], -(x2[11], 1)))

The following pairs are in P_≥:

F424_0_F_STORE'(x0[0]) → COND_F424_0_F_STORE(>(x0[0], 0), x0[0])
F424_0_F_STORE'(x0[2]) → COND_F424_0_F_STORE1(>(x0[2], 0), x0[2])
COND_F424_0_F_STORE1(TRUE, x0[3]) → F424_0_F_STORE'(-(x0[3], 2))
F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0[4]), x1[4], x2[4]) → COND_F629_1_F_INVOKEMETHOD(&&(>(x1[4], 0), >(x2[4], 1)), f434_0_f_Return(x0[4]), x1[4], x2[4])
F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0[6]), x1[6], x2[6]) → COND_F629_1_F_INVOKEMETHOD1(&&(>(x1[6], 0), >(x2[6], 1)), f434_0_f_Return(x0[6]), x1[6], x2[6])
COND_F629_1_F_INVOKEMETHOD1(TRUE, f434_0_f_Return(x0[7]), x1[7], x2[7]) → F424_0_F_STORE'(-(x1[7], -(x2[7], 1)))
F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0[8]), x1[8], x2[8]) → COND_F629_1_F_INVOKEMETHOD2(&&(>(x1[8], 0), >(x2[8], 1)), f584_0_f_Return(x0[8]), x1[8], x2[8])
F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0[10]), x1[10], x2[10]) → COND_F629_1_F_INVOKEMETHOD3(&&(>(x1[10], 0), >(x2[10], 1)), f584_0_f_Return(x0[10]), x1[10], x2[10])
COND_F629_1_F_INVOKEMETHOD3(TRUE, f584_0_f_Return(x0[11]), x1[11], x2[11]) → F424_0_F_STORE'(-(x1[11], -(x2[11], 1)))

At least the following rules have been oriented under context sensitive arithmetic replacement:

&&(TRUE, TRUE)¹ → TRUE¹
&&(TRUE, FALSE)¹ → FALSE¹
&&(FALSE, TRUE)¹ → FALSE¹
&&(FALSE, FALSE)¹ → FALSE¹

(8) Obligation:

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

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

The following domains are used:

Integer, Boolean

The ITRS R consists of the following rules:
f578_0_f_LE(x0, 0) → f584_0_f_Return(x0)
f629_1_f_InvokeMethod(f434_0_f_Return(x0), x1, x2) → Cond_f629_1_f_InvokeMethod(x2 > 0, f434_0_f_Return(x0), x1, x2)
Cond_f629_1_f_InvokeMethod(TRUE, f434_0_f_Return(x0), x1, x2) → f578_0_f_LE(x1, x2 - 1)
f629_1_f_InvokeMethod(f584_0_f_Return(x0), x1, x2) → Cond_f629_1_f_InvokeMethod1(x2 > 0, f584_0_f_Return(x0), x1, x2)
Cond_f629_1_f_InvokeMethod1(TRUE, f584_0_f_Return(x0), x1, x2) → f578_0_f_LE(x1, x2 - 1)
f578_0_f_LE(x0, x1) → Cond_f578_0_f_LE(x1 > 0 && x0 - x1 <= 0 && x0 > 0, x0, x1)
Cond_f578_0_f_LE(TRUE, x0, x1) → f629_1_f_InvokeMethod(f434_0_f_Return(x0 - x1), x0, x1)
f578_0_f_LE(x0, x1) → Cond_f578_0_f_LE1(x1 > 0 && x0 - x1 > 0 && x0 > 0, x0, x1)
Cond_f578_0_f_LE1(TRUE, x0, x1) → f629_1_f_InvokeMethod(f578_0_f_LE(x0 - x1, 2), x0, x1)

The integer pair graph contains the following rules and edges:
(0): F424_0_F_STORE'(x0[0]) → COND_F424_0_F_STORE(x0[0] > 0, x0[0])
(2): F424_0_F_STORE'(x0[2]) → COND_F424_0_F_STORE1(x0[2] > 0, x0[2])
(3): COND_F424_0_F_STORE1(TRUE, x0[3]) → F424_0_F_STORE'(x0[3] - 2)
(4): F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0[4]), x1[4], x2[4]) → COND_F629_1_F_INVOKEMETHOD(x1[4] > 0 && x2[4] > 1, f434_0_f_Return(x0[4]), x1[4], x2[4])
(6): F629_1_F_INVOKEMETHOD'(f434_0_f_Return(x0[6]), x1[6], x2[6]) → COND_F629_1_F_INVOKEMETHOD1(x1[6] > 0 && x2[6] > 1, f434_0_f_Return(x0[6]), x1[6], x2[6])
(7): COND_F629_1_F_INVOKEMETHOD1(TRUE, f434_0_f_Return(x0[7]), x1[7], x2[7]) → F424_0_F_STORE'(x1[7] - x2[7] - 1)
(8): F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0[8]), x1[8], x2[8]) → COND_F629_1_F_INVOKEMETHOD2(x1[8] > 0 && x2[8] > 1, f584_0_f_Return(x0[8]), x1[8], x2[8])
(10): F629_1_F_INVOKEMETHOD'(f584_0_f_Return(x0[10]), x1[10], x2[10]) → COND_F629_1_F_INVOKEMETHOD3(x1[10] > 0 && x2[10] > 1, f584_0_f_Return(x0[10]), x1[10], x2[10])
(11): COND_F629_1_F_INVOKEMETHOD3(TRUE, f584_0_f_Return(x0[11]), x1[11], x2[11]) → F424_0_F_STORE'(x1[11] - x2[11] - 1)

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

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

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

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

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

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

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

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

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

(9) IDependencyGraphProof (EQUIVALENT transformation)

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

(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

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

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

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

(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

R is empty.

The integer pair graph contains the following rules and edges:
(3): COND_F424_0_F_STORE1(TRUE, x0[3]) → F424_0_F_STORE'(x0[3] - 2)
(2): F424_0_F_STORE'(x0[2]) → COND_F424_0_F_STORE1(x0[2] > 0, x0[2])

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

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

(13) IDPNonInfProof (SOUND transformation)

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

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

For Pair COND_F424_0_F_STORE1(TRUE, x0[3]) → F424_0_F_STORE'(-(x0[3], 2)) the following chains were created:

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

We simplified constraint (1) using rules (III), (IV) which results in the following new constraint:
(2)    (>(x0[2], 0)=TRUE ⇒ COND_F424_0_F_STORE1(TRUE, x0[2])≥NonInfC∧COND_F424_0_F_STORE1(TRUE, x0[2])≥F424_0_F_STORE'(-(x0[2], 2))∧(U^Increasing(F424_0_F_STORE'(-(x0[3], 2))), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x0[3], 2))), ≥)∧[(2)bni_9 + (-1)Bound*bni_9] + [bni_9]x0[2] ≥ 0∧[2 + (-1)bso_10] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x0[3], 2))), ≥)∧[(2)bni_9 + (-1)Bound*bni_9] + [bni_9]x0[2] ≥ 0∧[2 + (-1)bso_10] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x0[3], 2))), ≥)∧[(2)bni_9 + (-1)Bound*bni_9] + [bni_9]x0[2] ≥ 0∧[2 + (-1)bso_10] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x0[2] ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x0[3], 2))), ≥)∧[(3)bni_9 + (-1)Bound*bni_9] + [bni_9]x0[2] ≥ 0∧[2 + (-1)bso_10] ≥ 0)

For Pair F424_0_F_STORE'(x0[2]) → COND_F424_0_F_STORE1(>(x0[2], 0), x0[2]) the following chains were created:

We consider the chain F424_0_F_STORE'(x0[2]) → COND_F424_0_F_STORE1(>(x0[2], 0), x0[2]), COND_F424_0_F_STORE1(TRUE, x0[3]) → F424_0_F_STORE'(-(x0[3], 2)) which results in the following constraint:
(7)    (>(x0[2], 0)=TRUE∧x0[2]=x0[3] ⇒ F424_0_F_STORE'(x0[2])≥NonInfC∧F424_0_F_STORE'(x0[2])≥COND_F424_0_F_STORE1(>(x0[2], 0), x0[2])∧(U^Increasing(COND_F424_0_F_STORE1(>(x0[2], 0), x0[2])), ≥))

We simplified constraint (7) using rule (IV) which results in the following new constraint:
(8)    (>(x0[2], 0)=TRUE ⇒ F424_0_F_STORE'(x0[2])≥NonInfC∧F424_0_F_STORE'(x0[2])≥COND_F424_0_F_STORE1(>(x0[2], 0), x0[2])∧(U^Increasing(COND_F424_0_F_STORE1(>(x0[2], 0), x0[2])), ≥))

We simplified constraint (8) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(9)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_F424_0_F_STORE1(>(x0[2], 0), x0[2])), ≥)∧[(2)bni_11 + (-1)Bound*bni_11] + [bni_11]x0[2] ≥ 0∧[(-1)bso_12] ≥ 0)

We simplified constraint (9) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(10)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_F424_0_F_STORE1(>(x0[2], 0), x0[2])), ≥)∧[(2)bni_11 + (-1)Bound*bni_11] + [bni_11]x0[2] ≥ 0∧[(-1)bso_12] ≥ 0)

We simplified constraint (10) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(11)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_F424_0_F_STORE1(>(x0[2], 0), x0[2])), ≥)∧[(2)bni_11 + (-1)Bound*bni_11] + [bni_11]x0[2] ≥ 0∧[(-1)bso_12] ≥ 0)

We simplified constraint (11) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(12)    (x0[2] ≥ 0 ⇒ (U^Increasing(COND_F424_0_F_STORE1(>(x0[2], 0), x0[2])), ≥)∧[(3)bni_11 + (-1)Bound*bni_11] + [bni_11]x0[2] ≥ 0∧[(-1)bso_12] ≥ 0)

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

COND_F424_0_F_STORE1(TRUE, x0[3]) → F424_0_F_STORE'(-(x0[3], 2))
- (x0[2] ≥ 0 ⇒ (U^Increasing(F424_0_F_STORE'(-(x0[3], 2))), ≥)∧[(3)bni_9 + (-1)Bound*bni_9] + [bni_9]x0[2] ≥ 0∧[2 + (-1)bso_10] ≥ 0)
F424_0_F_STORE'(x0[2]) → COND_F424_0_F_STORE1(>(x0[2], 0), x0[2])
- (x0[2] ≥ 0 ⇒ (U^Increasing(COND_F424_0_F_STORE1(>(x0[2], 0), x0[2])), ≥)∧[(3)bni_11 + (-1)Bound*bni_11] + [bni_11]x0[2] ≥ 0∧[(-1)bso_12] ≥ 0)

POL(TRUE) = [3]
POL(FALSE) = 0
POL(COND_F424_0_F_STORE1(x₁, x₂)) = [2] + x₂
POL(F424_0_F_STORE'(x₁)) = [2] + x₁
POL(-(x₁, x₂)) = x₁ + [-1]x₂
POL(2) = [2]
POL(>(x₁, x₂)) = [-1]
POL(0) = 0

The following pairs are in P_>:

COND_F424_0_F_STORE1(TRUE, x0[3]) → F424_0_F_STORE'(-(x0[3], 2))

The following pairs are in P_bound:

COND_F424_0_F_STORE1(TRUE, x0[3]) → F424_0_F_STORE'(-(x0[3], 2))
F424_0_F_STORE'(x0[2]) → COND_F424_0_F_STORE1(>(x0[2], 0), x0[2])

The following pairs are in P_≥:

F424_0_F_STORE'(x0[2]) → COND_F424_0_F_STORE1(>(x0[2], 0), x0[2])

There are no usable rules.

(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

R is empty.

The integer pair graph contains the following rules and edges:
(2): F424_0_F_STORE'(x0[2]) → COND_F424_0_F_STORE1(x0[2] > 0, x0[2])

The set Q consists of the following terms:
f629_1_f_InvokeMethod(f434_0_f_Return(x0), x1, x2)
Cond_f629_1_f_InvokeMethod(TRUE, f434_0_f_Return(x0), x1, x2)
f629_1_f_InvokeMethod(f584_0_f_Return(x0), x1, x2)
Cond_f629_1_f_InvokeMethod1(TRUE, f584_0_f_Return(x0), x1, x2)
f578_0_f_LE(x0, x1)
Cond_f578_0_f_LE(TRUE, x0, x1)
Cond_f578_0_f_LE1(TRUE, x0, x1)

(15) 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) Obligation:

(5) SCCToIDPv1Proof (SOUND transformation)

(6) Obligation:

(7) IDPNonInfProof (SOUND transformation)

(8) Obligation:

(9) IDependencyGraphProof (EQUIVALENT transformation)

(10) Obligation:

(11) UsableRulesProof (EQUIVALENT transformation)

(12) Obligation:

(13) IDPNonInfProof (SOUND transformation)

(14) Obligation:

(15) IDependencyGraphProof (EQUIVALENT transformation)

(16) TRUE