Termination proof of /tmp/tmpWChP2n/Fibonacci.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 160 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 JBCTerminationSCC

↳5 SCCToIDPv1Proof (⇒, 270 ms)

↳6 IDP

↳7 IDPNonInfProof (⇒, 420 ms)

↳8 AND

    ↳9 IDP

        ↳10 IDependencyGraphProof (⇔, 0 ms)

        ↳11 TRUE

    ↳12 IDP

        ↳13 IDependencyGraphProof (⇔, 0 ms)

        ↳14 TRUE

(0) Obligation:

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

public class Fibonacci {
	public static void main(String[] args) {
		fib(args.length);
	}

	public static int fib(int x) {
		if (x == 0) {
			return 0;
		} else if (x == 1) {
			return 1;
		} else {
			return fib(x-1) + fib(x-2);
		}
	}
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

Fibonacci.fib(I)I: Graph of 49 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: Fibonacci.fib(I)I
SCC calls the following helper methods: Fibonacci.fib(I)I
Performed SCC analyses: UsedFieldsAnalysis

(5) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 30 rules for P and 20 rules for R.

P rules:
64_0_fib_NE(EOS(STATIC_64), i4, i4) → 67_0_fib_NE(EOS(STATIC_67), i4, i4)
67_0_fib_NE(EOS(STATIC_67), i4, i4) → 69_0_fib_Load(EOS(STATIC_69), i4) | >(i4, 0)
69_0_fib_Load(EOS(STATIC_69), i4) → 74_0_fib_ConstantStackPush(EOS(STATIC_74), i4, i4)
74_0_fib_ConstantStackPush(EOS(STATIC_74), i4, i4) → 79_0_fib_NE(EOS(STATIC_79), i4, i4, 1)
79_0_fib_NE(EOS(STATIC_79), i7, i7, matching1) → 86_0_fib_NE(EOS(STATIC_86), i7, i7, 1) | =(matching1, 1)
86_0_fib_NE(EOS(STATIC_86), i7, i7, matching1) → 94_0_fib_Load(EOS(STATIC_94), i7) | &&(!(=(i7, 1)), =(matching1, 1))
94_0_fib_Load(EOS(STATIC_94), i7) → 99_0_fib_ConstantStackPush(EOS(STATIC_99), i7, i7)
99_0_fib_ConstantStackPush(EOS(STATIC_99), i7, i7) → 106_0_fib_IntArithmetic(EOS(STATIC_106), i7, i7, 1)
106_0_fib_IntArithmetic(EOS(STATIC_106), i7, i7, matching1) → 115_0_fib_InvokeMethod(EOS(STATIC_115), i7, -(i7, 1)) | &&(>(i7, 0), =(matching1, 1))
115_0_fib_InvokeMethod(EOS(STATIC_115), i7, i11) → 120_1_fib_InvokeMethod(120_0_fib_Load(EOS(STATIC_120), i11), i7, i11)
120_0_fib_Load(EOS(STATIC_120), i11) → 127_0_fib_Load(EOS(STATIC_127), i11)
120_1_fib_InvokeMethod(98_0_fib_Return(EOS(STATIC_98), matching1, matching2), i7, matching3) → 145_0_fib_Return(EOS(STATIC_145), i7, 1, 1, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
120_1_fib_InvokeMethod(570_0_fib_Return(EOS(STATIC_570), i161), i7, i179) → 600_0_fib_Return(EOS(STATIC_600), i7, i179, i161)
120_1_fib_InvokeMethod(617_0_fib_Return(EOS(STATIC_617), i202), i7, i207) → 633_0_fib_Return(EOS(STATIC_633), i7, i207, i202)
127_0_fib_Load(EOS(STATIC_127), i11) → 61_0_fib_Load(EOS(STATIC_61), i11)
61_0_fib_Load(EOS(STATIC_61), i1) → 64_0_fib_NE(EOS(STATIC_64), i1, i1)
145_0_fib_Return(EOS(STATIC_145), i7, matching1, matching2, matching3) → 147_0_fib_Load(EOS(STATIC_147), i7, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
147_0_fib_Load(EOS(STATIC_147), i7, matching1) → 256_0_fib_Load(EOS(STATIC_256), i7, 1) | =(matching1, 1)
256_0_fib_Load(EOS(STATIC_256), i7, i40) → 345_0_fib_Load(EOS(STATIC_345), i7, i40)
345_0_fib_Load(EOS(STATIC_345), i7, i79) → 444_0_fib_Load(EOS(STATIC_444), i7, i79)
444_0_fib_Load(EOS(STATIC_444), i7, i119) → 539_0_fib_Load(EOS(STATIC_539), i7, i119)
539_0_fib_Load(EOS(STATIC_539), i7, i161) → 545_0_fib_ConstantStackPush(EOS(STATIC_545), i161, i7)
545_0_fib_ConstantStackPush(EOS(STATIC_545), i161, i7) → 548_0_fib_IntArithmetic(EOS(STATIC_548), i161, i7, 2)
548_0_fib_IntArithmetic(EOS(STATIC_548), i161, i7, matching1) → 550_0_fib_InvokeMethod(EOS(STATIC_550), i161, -(i7, 2)) | &&(>(i7, 0), =(matching1, 2))
550_0_fib_InvokeMethod(EOS(STATIC_550), i161, i172) → 552_1_fib_InvokeMethod(552_0_fib_Load(EOS(STATIC_552), i172), i161, i172)
552_0_fib_Load(EOS(STATIC_552), i172) → 554_0_fib_Load(EOS(STATIC_554), i172)
554_0_fib_Load(EOS(STATIC_554), i172) → 61_0_fib_Load(EOS(STATIC_61), i172)
600_0_fib_Return(EOS(STATIC_600), i7, i179, i161) → 523_0_fib_Return(EOS(STATIC_523), i7, i179, i161)
523_0_fib_Return(EOS(STATIC_523), i7, i162, i161) → 539_0_fib_Load(EOS(STATIC_539), i7, i161)
633_0_fib_Return(EOS(STATIC_633), i7, i207, i202) → 523_0_fib_Return(EOS(STATIC_523), i7, i207, i202)
R rules:
64_0_fib_NE(EOS(STATIC_64), matching1, matching2) → 68_0_fib_NE(EOS(STATIC_68), 0, 0) | &&(=(matching1, 0), =(matching2, 0))
68_0_fib_NE(EOS(STATIC_68), matching1, matching2) → 70_0_fib_ConstantStackPush(EOS(STATIC_70), 0) | &&(=(matching1, 0), =(matching2, 0))
70_0_fib_ConstantStackPush(EOS(STATIC_70), matching1) → 76_0_fib_Return(EOS(STATIC_76), 0, 0) | =(matching1, 0)
79_0_fib_NE(EOS(STATIC_79), matching1, matching2, matching3) → 84_0_fib_NE(EOS(STATIC_84), 1, 1, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
84_0_fib_NE(EOS(STATIC_84), matching1, matching2, matching3) → 92_0_fib_ConstantStackPush(EOS(STATIC_92), 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
92_0_fib_ConstantStackPush(EOS(STATIC_92), matching1) → 98_0_fib_Return(EOS(STATIC_98), 1, 1) | =(matching1, 1)
234_0_fib_Return(EOS(STATIC_234), i7, i41, i40) → 331_0_fib_Return(EOS(STATIC_331), i7, i41, i40)
331_0_fib_Return(EOS(STATIC_331), i7, i80, i79) → 427_0_fib_Return(EOS(STATIC_427), i7, i80, i79)
427_0_fib_Return(EOS(STATIC_427), i7, i120, i119) → 523_0_fib_Return(EOS(STATIC_523), i7, i120, i119)
552_1_fib_InvokeMethod(76_0_fib_Return(EOS(STATIC_76), matching1, matching2), i161, matching3) → 562_0_fib_Return(EOS(STATIC_562), i161, 0, 0, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
552_1_fib_InvokeMethod(98_0_fib_Return(EOS(STATIC_98), matching1, matching2), i161, matching3) → 563_0_fib_Return(EOS(STATIC_563), i161, 1, 1, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
552_1_fib_InvokeMethod(570_0_fib_Return(EOS(STATIC_570), i182), i161, i183) → 601_0_fib_Return(EOS(STATIC_601), i161, i183, i182)
552_1_fib_InvokeMethod(617_0_fib_Return(EOS(STATIC_617), i202), i161, i209) → 636_0_fib_Return(EOS(STATIC_636), i161, i209, i202)
562_0_fib_Return(EOS(STATIC_562), i161, matching1, matching2, matching3) → 565_0_fib_IntArithmetic(EOS(STATIC_565), i161, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
563_0_fib_Return(EOS(STATIC_563), i161, matching1, matching2, matching3) → 568_0_fib_IntArithmetic(EOS(STATIC_568), i161, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
565_0_fib_IntArithmetic(EOS(STATIC_565), i161, matching1) → 570_0_fib_Return(EOS(STATIC_570), +(i161, 0)) | &&(>(i161, 0), =(matching1, 0))
568_0_fib_IntArithmetic(EOS(STATIC_568), i161, matching1) → 613_0_fib_IntArithmetic(EOS(STATIC_613), i161, 1) | =(matching1, 1)
601_0_fib_Return(EOS(STATIC_601), i161, i183, i182) → 613_0_fib_IntArithmetic(EOS(STATIC_613), i161, i182)
613_0_fib_IntArithmetic(EOS(STATIC_613), i161, i182) → 617_0_fib_Return(EOS(STATIC_617), +(i161, i182)) | &&(>(i161, 0), >(i182, 0))
636_0_fib_Return(EOS(STATIC_636), i161, i209, i202) → 601_0_fib_Return(EOS(STATIC_601), i161, i209, i202)

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

P rules:
64_0_fib_NE(EOS(STATIC_64), x0, x0) → 120_1_fib_InvokeMethod(64_0_fib_NE(EOS(STATIC_64), -(x0, 1), -(x0, 1)), x0, -(x0, 1)) | &&(>(x0, 0), !(=(x0, 1)))
120_1_fib_InvokeMethod(98_0_fib_Return(EOS(STATIC_98), 1, 1), x2, 1) → 552_1_fib_InvokeMethod(64_0_fib_NE(EOS(STATIC_64), -(x2, 2), -(x2, 2)), 1, -(x2, 2)) | >(x2, 0)
120_1_fib_InvokeMethod(570_0_fib_Return(EOS(STATIC_570), x0), x1, x2) → 552_1_fib_InvokeMethod(64_0_fib_NE(EOS(STATIC_64), -(x1, 2), -(x1, 2)), x0, -(x1, 2)) | >(x1, 0)
120_1_fib_InvokeMethod(617_0_fib_Return(EOS(STATIC_617), x0), x1, x2) → 552_1_fib_InvokeMethod(64_0_fib_NE(EOS(STATIC_64), -(x1, 2), -(x1, 2)), x0, -(x1, 2)) | >(x1, 0)
R rules:
64_0_fib_NE(EOS(STATIC_64), 0, 0) → 76_0_fib_Return(EOS(STATIC_76), 0, 0)
552_1_fib_InvokeMethod(76_0_fib_Return(EOS(STATIC_76), 0, 0), arith[1], 0) → 570_0_fib_Return(EOS(STATIC_570), arith[1]) | >(arith[1], 0)
552_1_fib_InvokeMethod(570_0_fib_Return(EOS(STATIC_570), x0), x1, x2) → 617_0_fib_Return(EOS(STATIC_617), +(x1, x0)) | &&(>(x1, 0), >(x0, 0))
552_1_fib_InvokeMethod(617_0_fib_Return(EOS(STATIC_617), x0), x1, x2) → 617_0_fib_Return(EOS(STATIC_617), +(x1, x0)) | &&(>(x1, 0), >(x0, 0))
552_1_fib_InvokeMethod(98_0_fib_Return(EOS(STATIC_98), 1, 1), x2, 1) → 617_0_fib_Return(EOS(STATIC_617), +(x2, 1)) | >(x2, 0)

Filtered ground terms:

64_0_fib_NE(x1, x2, x3) → 64_0_fib_NE(x2, x3)
617_0_fib_Return(x1, x2) → 617_0_fib_Return(x2)
570_0_fib_Return(x1, x2) → 570_0_fib_Return(x2)
Cond_120_1_fib_InvokeMethod(x1, x2, x3, x4) → Cond_120_1_fib_InvokeMethod(x1, x3)
98_0_fib_Return(x1, x2, x3) → 98_0_fib_Return
Cond_64_0_fib_NE(x1, x2, x3, x4) → Cond_64_0_fib_NE(x1, x3, x4)
Cond_552_1_fib_InvokeMethod3(x1, x2, x3, x4) → Cond_552_1_fib_InvokeMethod3(x1, x3)
Cond_552_1_fib_InvokeMethod(x1, x2, x3, x4) → Cond_552_1_fib_InvokeMethod(x1, x3)
76_0_fib_Return(x1, x2, x3) → 76_0_fib_Return

Filtered duplicate args:

64_0_fib_NE(x1, x2) → 64_0_fib_NE(x2)
Cond_64_0_fib_NE(x1, x2, x3) → Cond_64_0_fib_NE(x1, x3)

Filtered unneeded arguments:

Cond_120_1_fib_InvokeMethod1(x1, x2, x3, x4) → Cond_120_1_fib_InvokeMethod1(x1, x2, x3)
Cond_120_1_fib_InvokeMethod2(x1, x2, x3, x4) → Cond_120_1_fib_InvokeMethod2(x1, x2, x3)
Cond_552_1_fib_InvokeMethod1(x1, x2, x3, x4) → Cond_552_1_fib_InvokeMethod1(x1, x2, x3)
Cond_552_1_fib_InvokeMethod2(x1, x2, x3, x4) → Cond_552_1_fib_InvokeMethod2(x1, x2, x3)

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

P rules:
64_0_fib_NE(x0) → 120_1_fib_InvokeMethod(64_0_fib_NE(-(x0, 1)), x0, -(x0, 1)) | &&(>(x0, 0), !(=(x0, 1)))
120_1_fib_InvokeMethod(98_0_fib_Return, x2, 1) → 552_1_fib_InvokeMethod(64_0_fib_NE(-(x2, 2)), 1, -(x2, 2)) | >(x2, 0)
120_1_fib_InvokeMethod(570_0_fib_Return(x0), x1, x2) → 552_1_fib_InvokeMethod(64_0_fib_NE(-(x1, 2)), x0, -(x1, 2)) | >(x1, 0)
120_1_fib_InvokeMethod(617_0_fib_Return(x0), x1, x2) → 552_1_fib_InvokeMethod(64_0_fib_NE(-(x1, 2)), x0, -(x1, 2)) | >(x1, 0)
R rules:
64_0_fib_NE(0) → 76_0_fib_Return
552_1_fib_InvokeMethod(76_0_fib_Return, arith[1], 0) → 570_0_fib_Return(arith[1]) | >(arith[1], 0)
552_1_fib_InvokeMethod(570_0_fib_Return(x0), x1, x2) → 617_0_fib_Return(+(x1, x0)) | &&(>(x1, 0), >(x0, 0))
552_1_fib_InvokeMethod(617_0_fib_Return(x0), x1, x2) → 617_0_fib_Return(+(x1, x0)) | &&(>(x1, 0), >(x0, 0))
552_1_fib_InvokeMethod(98_0_fib_Return, x2, 1) → 617_0_fib_Return(+(x2, 1)) | >(x2, 0)

Performed bisimulation on rules. Used the following equivalence classes: {[76_0_fib_Return, 98_0_fib_Return]=76_0_fib_Return}

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

P rules:
64_0_FIB_NE(x0) → COND_64_0_FIB_NE(&&(>(x0, 0), !(=(x0, 1))), x0)
COND_64_0_FIB_NE(TRUE, x0) → 120_1_FIB_INVOKEMETHOD(64_0_fib_NE(-(x0, 1)), x0, -(x0, 1))
COND_64_0_FIB_NE(TRUE, x0) → 64_0_FIB_NE(-(x0, 1))
120_1_FIB_INVOKEMETHOD(76_0_fib_Return, x2, 1) → COND_120_1_FIB_INVOKEMETHOD(>(x2, 0), 76_0_fib_Return, x2, 1)
COND_120_1_FIB_INVOKEMETHOD(TRUE, 76_0_fib_Return, x2, 1) → 64_0_FIB_NE(-(x2, 2))
120_1_FIB_INVOKEMETHOD(570_0_fib_Return(x0), x1, x2) → COND_120_1_FIB_INVOKEMETHOD1(>(x1, 0), 570_0_fib_Return(x0), x1, x2)
COND_120_1_FIB_INVOKEMETHOD1(TRUE, 570_0_fib_Return(x0), x1, x2) → 64_0_FIB_NE(-(x1, 2))
120_1_FIB_INVOKEMETHOD(617_0_fib_Return(x0), x1, x2) → COND_120_1_FIB_INVOKEMETHOD2(>(x1, 0), 617_0_fib_Return(x0), x1, x2)
COND_120_1_FIB_INVOKEMETHOD2(TRUE, 617_0_fib_Return(x0), x1, x2) → 64_0_FIB_NE(-(x1, 2))
R rules:
64_0_fib_NE(0) → 76_0_fib_Return
552_1_fib_InvokeMethod(76_0_fib_Return, arith[1], 0) → Cond_552_1_fib_InvokeMethod(>(arith[1], 0), 76_0_fib_Return, arith[1], 0)
Cond_552_1_fib_InvokeMethod(TRUE, 76_0_fib_Return, arith[1], 0) → 570_0_fib_Return(arith[1])
552_1_fib_InvokeMethod(570_0_fib_Return(x0), x1, x2) → Cond_552_1_fib_InvokeMethod1(&&(>(x1, 0), >(x0, 0)), 570_0_fib_Return(x0), x1, x2)
Cond_552_1_fib_InvokeMethod1(TRUE, 570_0_fib_Return(x0), x1, x2) → 617_0_fib_Return(+(x1, x0))
552_1_fib_InvokeMethod(617_0_fib_Return(x0), x1, x2) → Cond_552_1_fib_InvokeMethod2(&&(>(x1, 0), >(x0, 0)), 617_0_fib_Return(x0), x1, x2)
Cond_552_1_fib_InvokeMethod2(TRUE, 617_0_fib_Return(x0), x1, x2) → 617_0_fib_Return(+(x1, x0))
552_1_fib_InvokeMethod(76_0_fib_Return, x2, 1) → Cond_552_1_fib_InvokeMethod3(>(x2, 0), 76_0_fib_Return, x2, 1)
Cond_552_1_fib_InvokeMethod3(TRUE, 76_0_fib_Return, x2, 1) → 617_0_fib_Return(+(x2, 1))

(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:
64_0_fib_NE(0) → 76_0_fib_Return
552_1_fib_InvokeMethod(76_0_fib_Return, arith[1], 0) → Cond_552_1_fib_InvokeMethod(arith[1] > 0, 76_0_fib_Return, arith[1], 0)
Cond_552_1_fib_InvokeMethod(TRUE, 76_0_fib_Return, arith[1], 0) → 570_0_fib_Return(arith[1])
552_1_fib_InvokeMethod(570_0_fib_Return(x0), x1, x2) → Cond_552_1_fib_InvokeMethod1(x1 > 0 && x0 > 0, 570_0_fib_Return(x0), x1, x2)
Cond_552_1_fib_InvokeMethod1(TRUE, 570_0_fib_Return(x0), x1, x2) → 617_0_fib_Return(x1 + x0)
552_1_fib_InvokeMethod(617_0_fib_Return(x0), x1, x2) → Cond_552_1_fib_InvokeMethod2(x1 > 0 && x0 > 0, 617_0_fib_Return(x0), x1, x2)
Cond_552_1_fib_InvokeMethod2(TRUE, 617_0_fib_Return(x0), x1, x2) → 617_0_fib_Return(x1 + x0)
552_1_fib_InvokeMethod(76_0_fib_Return, x2, 1) → Cond_552_1_fib_InvokeMethod3(x2 > 0, 76_0_fib_Return, x2, 1)
Cond_552_1_fib_InvokeMethod3(TRUE, 76_0_fib_Return, x2, 1) → 617_0_fib_Return(x2 + 1)

The integer pair graph contains the following rules and edges:
(0): 64_0_FIB_NE(x0[0]) → COND_64_0_FIB_NE(x0[0] > 0 && !(x0[0] = 1), x0[0])
(1): COND_64_0_FIB_NE(TRUE, x0[1]) → 120_1_FIB_INVOKEMETHOD(64_0_fib_NE(x0[1] - 1), x0[1], x0[1] - 1)
(2): COND_64_0_FIB_NE(TRUE, x0[2]) → 64_0_FIB_NE(x0[2] - 1)
(3): 120_1_FIB_INVOKEMETHOD(76_0_fib_Return, x2[3], 1) → COND_120_1_FIB_INVOKEMETHOD(x2[3] > 0, 76_0_fib_Return, x2[3], 1)
(4): COND_120_1_FIB_INVOKEMETHOD(TRUE, 76_0_fib_Return, x2[4], 1) → 64_0_FIB_NE(x2[4] - 2)
(5): 120_1_FIB_INVOKEMETHOD(570_0_fib_Return(x0[5]), x1[5], x2[5]) → COND_120_1_FIB_INVOKEMETHOD1(x1[5] > 0, 570_0_fib_Return(x0[5]), x1[5], x2[5])
(6): COND_120_1_FIB_INVOKEMETHOD1(TRUE, 570_0_fib_Return(x0[6]), x1[6], x2[6]) → 64_0_FIB_NE(x1[6] - 2)
(7): 120_1_FIB_INVOKEMETHOD(617_0_fib_Return(x0[7]), x1[7], x2[7]) → COND_120_1_FIB_INVOKEMETHOD2(x1[7] > 0, 617_0_fib_Return(x0[7]), x1[7], x2[7])
(8): COND_120_1_FIB_INVOKEMETHOD2(TRUE, 617_0_fib_Return(x0[8]), x1[8], x2[8]) → 64_0_FIB_NE(x1[8] - 2)

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

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

(1) -> (3), if (64_0_fib_NE(x0[1] - 1) →^* 76_0_fib_Return∧x0[1] →^* x2[3]∧x0[1] - 1 →^* 1)

(1) -> (5), if (64_0_fib_NE(x0[1] - 1) →^* 570_0_fib_Return(x0[5])∧x0[1] →^* x1[5]∧x0[1] - 1 →^* x2[5])

(1) -> (7), if (64_0_fib_NE(x0[1] - 1) →^* 617_0_fib_Return(x0[7])∧x0[1] →^* x1[7]∧x0[1] - 1 →^* x2[7])

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

(3) -> (4), if (x2[3] > 0 ∧x2[3] →^* x2[4])

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

(5) -> (6), if (x1[5] > 0 ∧570_0_fib_Return(x0[5]) →^* 570_0_fib_Return(x0[6])∧x1[5] →^* x1[6]∧x2[5] →^* x2[6])

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

(7) -> (8), if (x1[7] > 0 ∧617_0_fib_Return(x0[7]) →^* 617_0_fib_Return(x0[8])∧x1[7] →^* x1[8]∧x2[7] →^* x2[8])

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

The set Q consists of the following terms:
64_0_fib_NE(0)
552_1_fib_InvokeMethod(76_0_fib_Return, x0, 0)
Cond_552_1_fib_InvokeMethod(TRUE, 76_0_fib_Return, x0, 0)
552_1_fib_InvokeMethod(570_0_fib_Return(x0), x1, x2)
Cond_552_1_fib_InvokeMethod1(TRUE, 570_0_fib_Return(x0), x1, x2)
552_1_fib_InvokeMethod(617_0_fib_Return(x0), x1, x2)
Cond_552_1_fib_InvokeMethod2(TRUE, 617_0_fib_Return(x0), x1, x2)
552_1_fib_InvokeMethod(76_0_fib_Return, x0, 1)
Cond_552_1_fib_InvokeMethod3(TRUE, 76_0_fib_Return, x0, 1)

(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@5540b40 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 64_0_FIB_NE(x0) → COND_64_0_FIB_NE(&&(>(x0, 0), !(=(x0, 1))), x0) the following chains were created:

We consider the chain 64_0_FIB_NE(x0[0]) → COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0]), COND_64_0_FIB_NE(TRUE, x0[1]) → 120_1_FIB_INVOKEMETHOD(64_0_fib_NE(-(x0[1], 1)), x0[1], -(x0[1], 1)) which results in the following constraint:
(1)    (&&(>(x0[0], 0), !(=(x0[0], 1)))=TRUE∧x0[0]=x0[1] ⇒ 64_0_FIB_NE(x0[0])≥NonInfC∧64_0_FIB_NE(x0[0])≥COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])∧(U^Increasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥))

We simplified constraint (1) using rules (IV), (IDP_BOOLEAN) which results in the following new constraints:
(2)    (>(x0[0], 0)=TRUE∧<(x0[0], 1)=TRUE ⇒ 64_0_FIB_NE(x0[0])≥NonInfC∧64_0_FIB_NE(x0[0])≥COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])∧(U^Increasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥))

(3)    (>(x0[0], 0)=TRUE∧>(x0[0], 1)=TRUE ⇒ 64_0_FIB_NE(x0[0])≥NonInfC∧64_0_FIB_NE(x0[0])≥COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])∧(U^Increasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(4)    (x0[0] + [-1] ≥ 0∧[-1]x0[0] ≥ 0 ⇒ (U^Increasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[1 + (-1)bso_31] ≥ 0)

We simplified constraint (3) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(5)    (x0[0] + [-1] ≥ 0∧x0[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[1 + (-1)bso_31] ≥ 0)

We simplified constraint (4) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(6)    (x0[0] + [-1] ≥ 0∧[-1]x0[0] ≥ 0 ⇒ (U^Increasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[1 + (-1)bso_31] ≥ 0)

We simplified constraint (5) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(7)    (x0[0] + [-1] ≥ 0∧x0[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[1 + (-1)bso_31] ≥ 0)

We simplified constraint (6) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(8)    (x0[0] + [-1] ≥ 0∧[-1]x0[0] ≥ 0 ⇒ (U^Increasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[1 + (-1)bso_31] ≥ 0)

We simplified constraint (7) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(9)    (x0[0] + [-1] ≥ 0∧x0[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[1 + (-1)bso_31] ≥ 0)

We solved constraint (8) using rule (IDP_SMT_SPLIT).We simplified constraint (9) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(10)    (x0[0] ≥ 0∧[-1] + x0[0] ≥ 0 ⇒ (U^Increasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)Bound*bni_30 + bni_30] + [bni_30]x0[0] ≥ 0∧[1 + (-1)bso_31] ≥ 0)

We simplified constraint (10) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(11)    ([1] + x0[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)Bound*bni_30 + (2)bni_30] + [bni_30]x0[0] ≥ 0∧[1 + (-1)bso_31] ≥ 0)
We consider the chain 64_0_FIB_NE(x0[0]) → COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0]), COND_64_0_FIB_NE(TRUE, x0[2]) → 64_0_FIB_NE(-(x0[2], 1)) which results in the following constraint:
(12)    (&&(>(x0[0], 0), !(=(x0[0], 1)))=TRUE∧x0[0]=x0[2] ⇒ 64_0_FIB_NE(x0[0])≥NonInfC∧64_0_FIB_NE(x0[0])≥COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])∧(U^Increasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥))

We simplified constraint (12) using rules (IV), (IDP_BOOLEAN) which results in the following new constraints:
(13)    (>(x0[0], 0)=TRUE∧<(x0[0], 1)=TRUE ⇒ 64_0_FIB_NE(x0[0])≥NonInfC∧64_0_FIB_NE(x0[0])≥COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])∧(U^Increasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥))

(14)    (>(x0[0], 0)=TRUE∧>(x0[0], 1)=TRUE ⇒ 64_0_FIB_NE(x0[0])≥NonInfC∧64_0_FIB_NE(x0[0])≥COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])∧(U^Increasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥))

We simplified constraint (13) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(15)    (x0[0] + [-1] ≥ 0∧[-1]x0[0] ≥ 0 ⇒ (U^Increasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[1 + (-1)bso_31] ≥ 0)

We simplified constraint (14) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(16)    (x0[0] + [-1] ≥ 0∧x0[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[1 + (-1)bso_31] ≥ 0)

We simplified constraint (15) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(17)    (x0[0] + [-1] ≥ 0∧[-1]x0[0] ≥ 0 ⇒ (U^Increasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[1 + (-1)bso_31] ≥ 0)

We simplified constraint (16) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(18)    (x0[0] + [-1] ≥ 0∧x0[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[1 + (-1)bso_31] ≥ 0)

We simplified constraint (17) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(19)    (x0[0] + [-1] ≥ 0∧[-1]x0[0] ≥ 0 ⇒ (U^Increasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[1 + (-1)bso_31] ≥ 0)

We simplified constraint (18) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(20)    (x0[0] + [-1] ≥ 0∧x0[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[1 + (-1)bso_31] ≥ 0)

We solved constraint (19) using rule (IDP_SMT_SPLIT).We simplified constraint (20) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(21)    (x0[0] ≥ 0∧[-1] + x0[0] ≥ 0 ⇒ (U^Increasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)Bound*bni_30 + bni_30] + [bni_30]x0[0] ≥ 0∧[1 + (-1)bso_31] ≥ 0)

We simplified constraint (21) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(22)    ([1] + x0[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)Bound*bni_30 + (2)bni_30] + [bni_30]x0[0] ≥ 0∧[1 + (-1)bso_31] ≥ 0)

For Pair COND_64_0_FIB_NE(TRUE, x0) → 120_1_FIB_INVOKEMETHOD(64_0_fib_NE(-(x0, 1)), x0, -(x0, 1)) the following chains were created:

We consider the chain COND_64_0_FIB_NE(TRUE, x0[1]) → 120_1_FIB_INVOKEMETHOD(64_0_fib_NE(-(x0[1], 1)), x0[1], -(x0[1], 1)) which results in the following constraint:
(23)    (COND_64_0_FIB_NE(TRUE, x0[1])≥NonInfC∧COND_64_0_FIB_NE(TRUE, x0[1])≥120_1_FIB_INVOKEMETHOD(64_0_fib_NE(-(x0[1], 1)), x0[1], -(x0[1], 1))∧(U^Increasing(120_1_FIB_INVOKEMETHOD(64_0_fib_NE(-(x0[1], 1)), x0[1], -(x0[1], 1))), ≥))

We simplified constraint (23) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(24)    ((U^Increasing(120_1_FIB_INVOKEMETHOD(64_0_fib_NE(-(x0[1], 1)), x0[1], -(x0[1], 1))), ≥)∧[bni_32] = 0∧[(-1)bso_33] ≥ 0)

We simplified constraint (24) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(25)    ((U^Increasing(120_1_FIB_INVOKEMETHOD(64_0_fib_NE(-(x0[1], 1)), x0[1], -(x0[1], 1))), ≥)∧[bni_32] = 0∧[(-1)bso_33] ≥ 0)

We simplified constraint (25) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(26)    ((U^Increasing(120_1_FIB_INVOKEMETHOD(64_0_fib_NE(-(x0[1], 1)), x0[1], -(x0[1], 1))), ≥)∧[bni_32] = 0∧[(-1)bso_33] ≥ 0)

We simplified constraint (26) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(27)    ((U^Increasing(120_1_FIB_INVOKEMETHOD(64_0_fib_NE(-(x0[1], 1)), x0[1], -(x0[1], 1))), ≥)∧[bni_32] = 0∧0 = 0∧[(-1)bso_33] ≥ 0)

For Pair COND_64_0_FIB_NE(TRUE, x0) → 64_0_FIB_NE(-(x0, 1)) the following chains were created:

We consider the chain COND_64_0_FIB_NE(TRUE, x0[2]) → 64_0_FIB_NE(-(x0[2], 1)) which results in the following constraint:
(28)    (COND_64_0_FIB_NE(TRUE, x0[2])≥NonInfC∧COND_64_0_FIB_NE(TRUE, x0[2])≥64_0_FIB_NE(-(x0[2], 1))∧(U^Increasing(64_0_FIB_NE(-(x0[2], 1))), ≥))

We simplified constraint (28) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(29)    ((U^Increasing(64_0_FIB_NE(-(x0[2], 1))), ≥)∧[bni_34] = 0∧[(-1)bso_35] ≥ 0)

We simplified constraint (29) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(30)    ((U^Increasing(64_0_FIB_NE(-(x0[2], 1))), ≥)∧[bni_34] = 0∧[(-1)bso_35] ≥ 0)

We simplified constraint (30) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(31)    ((U^Increasing(64_0_FIB_NE(-(x0[2], 1))), ≥)∧[bni_34] = 0∧[(-1)bso_35] ≥ 0)

We simplified constraint (31) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(32)    ((U^Increasing(64_0_FIB_NE(-(x0[2], 1))), ≥)∧[bni_34] = 0∧0 = 0∧[(-1)bso_35] ≥ 0)

For Pair 120_1_FIB_INVOKEMETHOD(76_0_fib_Return, x2, 1) → COND_120_1_FIB_INVOKEMETHOD(>(x2, 0), 76_0_fib_Return, x2, 1) the following chains were created:

We consider the chain 120_1_FIB_INVOKEMETHOD(76_0_fib_Return, x2[3], 1) → COND_120_1_FIB_INVOKEMETHOD(>(x2[3], 0), 76_0_fib_Return, x2[3], 1), COND_120_1_FIB_INVOKEMETHOD(TRUE, 76_0_fib_Return, x2[4], 1) → 64_0_FIB_NE(-(x2[4], 2)) which results in the following constraint:
(33)    (>(x2[3], 0)=TRUE∧x2[3]=x2[4] ⇒ 120_1_FIB_INVOKEMETHOD(76_0_fib_Return, x2[3], 1)≥NonInfC∧120_1_FIB_INVOKEMETHOD(76_0_fib_Return, x2[3], 1)≥COND_120_1_FIB_INVOKEMETHOD(>(x2[3], 0), 76_0_fib_Return, x2[3], 1)∧(U^Increasing(COND_120_1_FIB_INVOKEMETHOD(>(x2[3], 0), 76_0_fib_Return, x2[3], 1)), ≥))

We simplified constraint (33) using rule (IV) which results in the following new constraint:
(34)    (>(x2[3], 0)=TRUE ⇒ 120_1_FIB_INVOKEMETHOD(76_0_fib_Return, x2[3], 1)≥NonInfC∧120_1_FIB_INVOKEMETHOD(76_0_fib_Return, x2[3], 1)≥COND_120_1_FIB_INVOKEMETHOD(>(x2[3], 0), 76_0_fib_Return, x2[3], 1)∧(U^Increasing(COND_120_1_FIB_INVOKEMETHOD(>(x2[3], 0), 76_0_fib_Return, x2[3], 1)), ≥))

We simplified constraint (34) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(35)    (x2[3] + [-1] ≥ 0 ⇒ (U^Increasing(COND_120_1_FIB_INVOKEMETHOD(>(x2[3], 0), 76_0_fib_Return, x2[3], 1)), ≥)∧[(-1)bni_36 + (-1)Bound*bni_36] + [bni_36]x2[3] ≥ 0∧[(-1)bso_37] ≥ 0)

We simplified constraint (35) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(36)    (x2[3] + [-1] ≥ 0 ⇒ (U^Increasing(COND_120_1_FIB_INVOKEMETHOD(>(x2[3], 0), 76_0_fib_Return, x2[3], 1)), ≥)∧[(-1)bni_36 + (-1)Bound*bni_36] + [bni_36]x2[3] ≥ 0∧[(-1)bso_37] ≥ 0)

We simplified constraint (36) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(37)    (x2[3] + [-1] ≥ 0 ⇒ (U^Increasing(COND_120_1_FIB_INVOKEMETHOD(>(x2[3], 0), 76_0_fib_Return, x2[3], 1)), ≥)∧[(-1)bni_36 + (-1)Bound*bni_36] + [bni_36]x2[3] ≥ 0∧[(-1)bso_37] ≥ 0)

We simplified constraint (37) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(38)    (x2[3] ≥ 0 ⇒ (U^Increasing(COND_120_1_FIB_INVOKEMETHOD(>(x2[3], 0), 76_0_fib_Return, x2[3], 1)), ≥)∧[(-1)Bound*bni_36] + [bni_36]x2[3] ≥ 0∧[(-1)bso_37] ≥ 0)

For Pair COND_120_1_FIB_INVOKEMETHOD(TRUE, 76_0_fib_Return, x2, 1) → 64_0_FIB_NE(-(x2, 2)) the following chains were created:

We consider the chain COND_120_1_FIB_INVOKEMETHOD(TRUE, 76_0_fib_Return, x2[4], 1) → 64_0_FIB_NE(-(x2[4], 2)) which results in the following constraint:
(39)    (COND_120_1_FIB_INVOKEMETHOD(TRUE, 76_0_fib_Return, x2[4], 1)≥NonInfC∧COND_120_1_FIB_INVOKEMETHOD(TRUE, 76_0_fib_Return, x2[4], 1)≥64_0_FIB_NE(-(x2[4], 2))∧(U^Increasing(64_0_FIB_NE(-(x2[4], 2))), ≥))

We simplified constraint (39) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(40)    ((U^Increasing(64_0_FIB_NE(-(x2[4], 2))), ≥)∧[bni_38] = 0∧[1 + (-1)bso_39] ≥ 0)

We simplified constraint (40) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(41)    ((U^Increasing(64_0_FIB_NE(-(x2[4], 2))), ≥)∧[bni_38] = 0∧[1 + (-1)bso_39] ≥ 0)

We simplified constraint (41) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(42)    ((U^Increasing(64_0_FIB_NE(-(x2[4], 2))), ≥)∧[bni_38] = 0∧[1 + (-1)bso_39] ≥ 0)

We simplified constraint (42) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(43)    ((U^Increasing(64_0_FIB_NE(-(x2[4], 2))), ≥)∧[bni_38] = 0∧0 = 0∧[1 + (-1)bso_39] ≥ 0)

For Pair 120_1_FIB_INVOKEMETHOD(570_0_fib_Return(x0), x1, x2) → COND_120_1_FIB_INVOKEMETHOD1(>(x1, 0), 570_0_fib_Return(x0), x1, x2) the following chains were created:

We consider the chain 120_1_FIB_INVOKEMETHOD(570_0_fib_Return(x0[5]), x1[5], x2[5]) → COND_120_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 570_0_fib_Return(x0[5]), x1[5], x2[5]), COND_120_1_FIB_INVOKEMETHOD1(TRUE, 570_0_fib_Return(x0[6]), x1[6], x2[6]) → 64_0_FIB_NE(-(x1[6], 2)) which results in the following constraint:
(44)    (>(x1[5], 0)=TRUE∧570_0_fib_Return(x0[5])=570_0_fib_Return(x0[6])∧x1[5]=x1[6]∧x2[5]=x2[6] ⇒ 120_1_FIB_INVOKEMETHOD(570_0_fib_Return(x0[5]), x1[5], x2[5])≥NonInfC∧120_1_FIB_INVOKEMETHOD(570_0_fib_Return(x0[5]), x1[5], x2[5])≥COND_120_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 570_0_fib_Return(x0[5]), x1[5], x2[5])∧(U^Increasing(COND_120_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 570_0_fib_Return(x0[5]), x1[5], x2[5])), ≥))

We simplified constraint (44) using rules (I), (II), (IV) which results in the following new constraint:
(45)    (>(x1[5], 0)=TRUE ⇒ 120_1_FIB_INVOKEMETHOD(570_0_fib_Return(x0[5]), x1[5], x2[5])≥NonInfC∧120_1_FIB_INVOKEMETHOD(570_0_fib_Return(x0[5]), x1[5], x2[5])≥COND_120_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 570_0_fib_Return(x0[5]), x1[5], x2[5])∧(U^Increasing(COND_120_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 570_0_fib_Return(x0[5]), x1[5], x2[5])), ≥))

We simplified constraint (45) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(46)    (x1[5] + [-1] ≥ 0 ⇒ (U^Increasing(COND_120_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 570_0_fib_Return(x0[5]), x1[5], x2[5])), ≥)∧[(-1)bni_40 + (-1)Bound*bni_40] + [bni_40]x1[5] ≥ 0∧[(-1)bso_41] ≥ 0)

We simplified constraint (46) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(47)    (x1[5] + [-1] ≥ 0 ⇒ (U^Increasing(COND_120_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 570_0_fib_Return(x0[5]), x1[5], x2[5])), ≥)∧[(-1)bni_40 + (-1)Bound*bni_40] + [bni_40]x1[5] ≥ 0∧[(-1)bso_41] ≥ 0)

We simplified constraint (47) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(48)    (x1[5] + [-1] ≥ 0 ⇒ (U^Increasing(COND_120_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 570_0_fib_Return(x0[5]), x1[5], x2[5])), ≥)∧[(-1)bni_40 + (-1)Bound*bni_40] + [bni_40]x1[5] ≥ 0∧[(-1)bso_41] ≥ 0)

We simplified constraint (48) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(49)    (x1[5] + [-1] ≥ 0 ⇒ (U^Increasing(COND_120_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 570_0_fib_Return(x0[5]), x1[5], x2[5])), ≥)∧0 = 0∧0 = 0∧[(-1)bni_40 + (-1)Bound*bni_40] + [bni_40]x1[5] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_41] ≥ 0)

We simplified constraint (49) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(50)    (x1[5] ≥ 0 ⇒ (U^Increasing(COND_120_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 570_0_fib_Return(x0[5]), x1[5], x2[5])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_40] + [bni_40]x1[5] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_41] ≥ 0)

For Pair COND_120_1_FIB_INVOKEMETHOD1(TRUE, 570_0_fib_Return(x0), x1, x2) → 64_0_FIB_NE(-(x1, 2)) the following chains were created:

We consider the chain COND_120_1_FIB_INVOKEMETHOD1(TRUE, 570_0_fib_Return(x0[6]), x1[6], x2[6]) → 64_0_FIB_NE(-(x1[6], 2)) which results in the following constraint:
(51)    (COND_120_1_FIB_INVOKEMETHOD1(TRUE, 570_0_fib_Return(x0[6]), x1[6], x2[6])≥NonInfC∧COND_120_1_FIB_INVOKEMETHOD1(TRUE, 570_0_fib_Return(x0[6]), x1[6], x2[6])≥64_0_FIB_NE(-(x1[6], 2))∧(U^Increasing(64_0_FIB_NE(-(x1[6], 2))), ≥))

We simplified constraint (51) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(52)    ((U^Increasing(64_0_FIB_NE(-(x1[6], 2))), ≥)∧[bni_42] = 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (52) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(53)    ((U^Increasing(64_0_FIB_NE(-(x1[6], 2))), ≥)∧[bni_42] = 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (53) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(54)    ((U^Increasing(64_0_FIB_NE(-(x1[6], 2))), ≥)∧[bni_42] = 0∧[1 + (-1)bso_43] ≥ 0)

We simplified constraint (54) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(55)    ((U^Increasing(64_0_FIB_NE(-(x1[6], 2))), ≥)∧[bni_42] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_43] ≥ 0)

For Pair 120_1_FIB_INVOKEMETHOD(617_0_fib_Return(x0), x1, x2) → COND_120_1_FIB_INVOKEMETHOD2(>(x1, 0), 617_0_fib_Return(x0), x1, x2) the following chains were created:

We consider the chain 120_1_FIB_INVOKEMETHOD(617_0_fib_Return(x0[7]), x1[7], x2[7]) → COND_120_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 617_0_fib_Return(x0[7]), x1[7], x2[7]), COND_120_1_FIB_INVOKEMETHOD2(TRUE, 617_0_fib_Return(x0[8]), x1[8], x2[8]) → 64_0_FIB_NE(-(x1[8], 2)) which results in the following constraint:
(56)    (>(x1[7], 0)=TRUE∧617_0_fib_Return(x0[7])=617_0_fib_Return(x0[8])∧x1[7]=x1[8]∧x2[7]=x2[8] ⇒ 120_1_FIB_INVOKEMETHOD(617_0_fib_Return(x0[7]), x1[7], x2[7])≥NonInfC∧120_1_FIB_INVOKEMETHOD(617_0_fib_Return(x0[7]), x1[7], x2[7])≥COND_120_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 617_0_fib_Return(x0[7]), x1[7], x2[7])∧(U^Increasing(COND_120_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 617_0_fib_Return(x0[7]), x1[7], x2[7])), ≥))

We simplified constraint (56) using rules (I), (II), (IV) which results in the following new constraint:
(57)    (>(x1[7], 0)=TRUE ⇒ 120_1_FIB_INVOKEMETHOD(617_0_fib_Return(x0[7]), x1[7], x2[7])≥NonInfC∧120_1_FIB_INVOKEMETHOD(617_0_fib_Return(x0[7]), x1[7], x2[7])≥COND_120_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 617_0_fib_Return(x0[7]), x1[7], x2[7])∧(U^Increasing(COND_120_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 617_0_fib_Return(x0[7]), x1[7], x2[7])), ≥))

We simplified constraint (57) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(58)    (x1[7] + [-1] ≥ 0 ⇒ (U^Increasing(COND_120_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 617_0_fib_Return(x0[7]), x1[7], x2[7])), ≥)∧[(-1)bni_44 + (-1)Bound*bni_44] + [bni_44]x1[7] ≥ 0∧[(-1)bso_45] ≥ 0)

We simplified constraint (58) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(59)    (x1[7] + [-1] ≥ 0 ⇒ (U^Increasing(COND_120_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 617_0_fib_Return(x0[7]), x1[7], x2[7])), ≥)∧[(-1)bni_44 + (-1)Bound*bni_44] + [bni_44]x1[7] ≥ 0∧[(-1)bso_45] ≥ 0)

We simplified constraint (59) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(60)    (x1[7] + [-1] ≥ 0 ⇒ (U^Increasing(COND_120_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 617_0_fib_Return(x0[7]), x1[7], x2[7])), ≥)∧[(-1)bni_44 + (-1)Bound*bni_44] + [bni_44]x1[7] ≥ 0∧[(-1)bso_45] ≥ 0)

We simplified constraint (60) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(61)    (x1[7] + [-1] ≥ 0 ⇒ (U^Increasing(COND_120_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 617_0_fib_Return(x0[7]), x1[7], x2[7])), ≥)∧0 = 0∧0 = 0∧[(-1)bni_44 + (-1)Bound*bni_44] + [bni_44]x1[7] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_45] ≥ 0)

We simplified constraint (61) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(62)    (x1[7] ≥ 0 ⇒ (U^Increasing(COND_120_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 617_0_fib_Return(x0[7]), x1[7], x2[7])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_44] + [bni_44]x1[7] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_45] ≥ 0)

For Pair COND_120_1_FIB_INVOKEMETHOD2(TRUE, 617_0_fib_Return(x0), x1, x2) → 64_0_FIB_NE(-(x1, 2)) the following chains were created:

We consider the chain COND_120_1_FIB_INVOKEMETHOD2(TRUE, 617_0_fib_Return(x0[8]), x1[8], x2[8]) → 64_0_FIB_NE(-(x1[8], 2)) which results in the following constraint:
(63)    (COND_120_1_FIB_INVOKEMETHOD2(TRUE, 617_0_fib_Return(x0[8]), x1[8], x2[8])≥NonInfC∧COND_120_1_FIB_INVOKEMETHOD2(TRUE, 617_0_fib_Return(x0[8]), x1[8], x2[8])≥64_0_FIB_NE(-(x1[8], 2))∧(U^Increasing(64_0_FIB_NE(-(x1[8], 2))), ≥))

We simplified constraint (63) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(64)    ((U^Increasing(64_0_FIB_NE(-(x1[8], 2))), ≥)∧[bni_46] = 0∧[1 + (-1)bso_47] ≥ 0)

We simplified constraint (64) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(65)    ((U^Increasing(64_0_FIB_NE(-(x1[8], 2))), ≥)∧[bni_46] = 0∧[1 + (-1)bso_47] ≥ 0)

We simplified constraint (65) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(66)    ((U^Increasing(64_0_FIB_NE(-(x1[8], 2))), ≥)∧[bni_46] = 0∧[1 + (-1)bso_47] ≥ 0)

We simplified constraint (66) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(67)    ((U^Increasing(64_0_FIB_NE(-(x1[8], 2))), ≥)∧[bni_46] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

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

64_0_FIB_NE(x0) → COND_64_0_FIB_NE(&&(>(x0, 0), !(=(x0, 1))), x0)
- ([1] + x0[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)Bound*bni_30 + (2)bni_30] + [bni_30]x0[0] ≥ 0∧[1 + (-1)bso_31] ≥ 0)
- ([1] + x0[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)Bound*bni_30 + (2)bni_30] + [bni_30]x0[0] ≥ 0∧[1 + (-1)bso_31] ≥ 0)
COND_64_0_FIB_NE(TRUE, x0) → 120_1_FIB_INVOKEMETHOD(64_0_fib_NE(-(x0, 1)), x0, -(x0, 1))
- ((U^Increasing(120_1_FIB_INVOKEMETHOD(64_0_fib_NE(-(x0[1], 1)), x0[1], -(x0[1], 1))), ≥)∧[bni_32] = 0∧0 = 0∧[(-1)bso_33] ≥ 0)
COND_64_0_FIB_NE(TRUE, x0) → 64_0_FIB_NE(-(x0, 1))
- ((U^Increasing(64_0_FIB_NE(-(x0[2], 1))), ≥)∧[bni_34] = 0∧0 = 0∧[(-1)bso_35] ≥ 0)
120_1_FIB_INVOKEMETHOD(76_0_fib_Return, x2, 1) → COND_120_1_FIB_INVOKEMETHOD(>(x2, 0), 76_0_fib_Return, x2, 1)
- (x2[3] ≥ 0 ⇒ (U^Increasing(COND_120_1_FIB_INVOKEMETHOD(>(x2[3], 0), 76_0_fib_Return, x2[3], 1)), ≥)∧[(-1)Bound*bni_36] + [bni_36]x2[3] ≥ 0∧[(-1)bso_37] ≥ 0)
COND_120_1_FIB_INVOKEMETHOD(TRUE, 76_0_fib_Return, x2, 1) → 64_0_FIB_NE(-(x2, 2))
- ((U^Increasing(64_0_FIB_NE(-(x2[4], 2))), ≥)∧[bni_38] = 0∧0 = 0∧[1 + (-1)bso_39] ≥ 0)
120_1_FIB_INVOKEMETHOD(570_0_fib_Return(x0), x1, x2) → COND_120_1_FIB_INVOKEMETHOD1(>(x1, 0), 570_0_fib_Return(x0), x1, x2)
- (x1[5] ≥ 0 ⇒ (U^Increasing(COND_120_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 570_0_fib_Return(x0[5]), x1[5], x2[5])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_40] + [bni_40]x1[5] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_41] ≥ 0)
COND_120_1_FIB_INVOKEMETHOD1(TRUE, 570_0_fib_Return(x0), x1, x2) → 64_0_FIB_NE(-(x1, 2))
- ((U^Increasing(64_0_FIB_NE(-(x1[6], 2))), ≥)∧[bni_42] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_43] ≥ 0)
120_1_FIB_INVOKEMETHOD(617_0_fib_Return(x0), x1, x2) → COND_120_1_FIB_INVOKEMETHOD2(>(x1, 0), 617_0_fib_Return(x0), x1, x2)
- (x1[7] ≥ 0 ⇒ (U^Increasing(COND_120_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 617_0_fib_Return(x0[7]), x1[7], x2[7])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_44] + [bni_44]x1[7] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_45] ≥ 0)
COND_120_1_FIB_INVOKEMETHOD2(TRUE, 617_0_fib_Return(x0), x1, x2) → 64_0_FIB_NE(-(x1, 2))
- ((U^Increasing(64_0_FIB_NE(-(x1[8], 2))), ≥)∧[bni_46] = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 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(64_0_fib_NE(x₁)) = [-1] + [-1]x₁
POL(0) = 0
POL(76_0_fib_Return) = [-1]
POL(552_1_fib_InvokeMethod(x₁, x₂, x₃)) = [-1] + [-1]x₂ + [-1]x₁
POL(Cond_552_1_fib_InvokeMethod(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃
POL(>(x₁, x₂)) = [-1]
POL(570_0_fib_Return(x₁)) = x₁
POL(Cond_552_1_fib_InvokeMethod1(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + [-1]x₂
POL(&&(x₁, x₂)) = [-1]
POL(617_0_fib_Return(x₁)) = x₁
POL(+(x₁, x₂)) = x₁ + x₂
POL(Cond_552_1_fib_InvokeMethod2(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + [-1]x₂
POL(1) = [1]
POL(Cond_552_1_fib_InvokeMethod3(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃
POL(64_0_FIB_NE(x₁)) = x₁
POL(COND_64_0_FIB_NE(x₁, x₂)) = [-1] + x₂
POL(!(x₁)) = [-1]
POL(=(x₁, x₂)) = [-1]
POL(120_1_FIB_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + x₂
POL(-(x₁, x₂)) = x₁ + [-1]x₂
POL(COND_120_1_FIB_INVOKEMETHOD(x₁, x₂, x₃, x₄)) = [-1] + x₃
POL(2) = [2]
POL(COND_120_1_FIB_INVOKEMETHOD1(x₁, x₂, x₃, x₄)) = [-1] + x₃
POL(COND_120_1_FIB_INVOKEMETHOD2(x₁, x₂, x₃, x₄)) = [-1] + x₃

The following pairs are in P_>:

64_0_FIB_NE(x0[0]) → COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])
COND_120_1_FIB_INVOKEMETHOD(TRUE, 76_0_fib_Return, x2[4], 1) → 64_0_FIB_NE(-(x2[4], 2))
COND_120_1_FIB_INVOKEMETHOD1(TRUE, 570_0_fib_Return(x0[6]), x1[6], x2[6]) → 64_0_FIB_NE(-(x1[6], 2))
COND_120_1_FIB_INVOKEMETHOD2(TRUE, 617_0_fib_Return(x0[8]), x1[8], x2[8]) → 64_0_FIB_NE(-(x1[8], 2))

The following pairs are in P_bound:

64_0_FIB_NE(x0[0]) → COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])
120_1_FIB_INVOKEMETHOD(76_0_fib_Return, x2[3], 1) → COND_120_1_FIB_INVOKEMETHOD(>(x2[3], 0), 76_0_fib_Return, x2[3], 1)
120_1_FIB_INVOKEMETHOD(570_0_fib_Return(x0[5]), x1[5], x2[5]) → COND_120_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 570_0_fib_Return(x0[5]), x1[5], x2[5])
120_1_FIB_INVOKEMETHOD(617_0_fib_Return(x0[7]), x1[7], x2[7]) → COND_120_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 617_0_fib_Return(x0[7]), x1[7], x2[7])

The following pairs are in P_≥:

COND_64_0_FIB_NE(TRUE, x0[1]) → 120_1_FIB_INVOKEMETHOD(64_0_fib_NE(-(x0[1], 1)), x0[1], -(x0[1], 1))
COND_64_0_FIB_NE(TRUE, x0[2]) → 64_0_FIB_NE(-(x0[2], 1))
120_1_FIB_INVOKEMETHOD(76_0_fib_Return, x2[3], 1) → COND_120_1_FIB_INVOKEMETHOD(>(x2[3], 0), 76_0_fib_Return, x2[3], 1)
120_1_FIB_INVOKEMETHOD(570_0_fib_Return(x0[5]), x1[5], x2[5]) → COND_120_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 570_0_fib_Return(x0[5]), x1[5], x2[5])
120_1_FIB_INVOKEMETHOD(617_0_fib_Return(x0[7]), x1[7], x2[7]) → COND_120_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 617_0_fib_Return(x0[7]), x1[7], x2[7])

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

64_0_fib_NE(0)¹ → 76_0_fib_Return¹

(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:
64_0_fib_NE(0) → 76_0_fib_Return
552_1_fib_InvokeMethod(76_0_fib_Return, arith[1], 0) → Cond_552_1_fib_InvokeMethod(arith[1] > 0, 76_0_fib_Return, arith[1], 0)
Cond_552_1_fib_InvokeMethod(TRUE, 76_0_fib_Return, arith[1], 0) → 570_0_fib_Return(arith[1])
552_1_fib_InvokeMethod(570_0_fib_Return(x0), x1, x2) → Cond_552_1_fib_InvokeMethod1(x1 > 0 && x0 > 0, 570_0_fib_Return(x0), x1, x2)
Cond_552_1_fib_InvokeMethod1(TRUE, 570_0_fib_Return(x0), x1, x2) → 617_0_fib_Return(x1 + x0)
552_1_fib_InvokeMethod(617_0_fib_Return(x0), x1, x2) → Cond_552_1_fib_InvokeMethod2(x1 > 0 && x0 > 0, 617_0_fib_Return(x0), x1, x2)
Cond_552_1_fib_InvokeMethod2(TRUE, 617_0_fib_Return(x0), x1, x2) → 617_0_fib_Return(x1 + x0)
552_1_fib_InvokeMethod(76_0_fib_Return, x2, 1) → Cond_552_1_fib_InvokeMethod3(x2 > 0, 76_0_fib_Return, x2, 1)
Cond_552_1_fib_InvokeMethod3(TRUE, 76_0_fib_Return, x2, 1) → 617_0_fib_Return(x2 + 1)

The integer pair graph contains the following rules and edges:
(1): COND_64_0_FIB_NE(TRUE, x0[1]) → 120_1_FIB_INVOKEMETHOD(64_0_fib_NE(x0[1] - 1), x0[1], x0[1] - 1)
(2): COND_64_0_FIB_NE(TRUE, x0[2]) → 64_0_FIB_NE(x0[2] - 1)
(3): 120_1_FIB_INVOKEMETHOD(76_0_fib_Return, x2[3], 1) → COND_120_1_FIB_INVOKEMETHOD(x2[3] > 0, 76_0_fib_Return, x2[3], 1)
(5): 120_1_FIB_INVOKEMETHOD(570_0_fib_Return(x0[5]), x1[5], x2[5]) → COND_120_1_FIB_INVOKEMETHOD1(x1[5] > 0, 570_0_fib_Return(x0[5]), x1[5], x2[5])
(7): 120_1_FIB_INVOKEMETHOD(617_0_fib_Return(x0[7]), x1[7], x2[7]) → COND_120_1_FIB_INVOKEMETHOD2(x1[7] > 0, 617_0_fib_Return(x0[7]), x1[7], x2[7])

(1) -> (3), if (64_0_fib_NE(x0[1] - 1) →^* 76_0_fib_Return∧x0[1] →^* x2[3]∧x0[1] - 1 →^* 1)

(1) -> (5), if (64_0_fib_NE(x0[1] - 1) →^* 570_0_fib_Return(x0[5])∧x0[1] →^* x1[5]∧x0[1] - 1 →^* x2[5])

(1) -> (7), if (64_0_fib_NE(x0[1] - 1) →^* 617_0_fib_Return(x0[7])∧x0[1] →^* x1[7]∧x0[1] - 1 →^* x2[7])

(10) IDependencyGraphProof (EQUIVALENT transformation)

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

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

The ITRS R consists of the following rules:
64_0_fib_NE(0) → 76_0_fib_Return
552_1_fib_InvokeMethod(76_0_fib_Return, arith[1], 0) → Cond_552_1_fib_InvokeMethod(arith[1] > 0, 76_0_fib_Return, arith[1], 0)
Cond_552_1_fib_InvokeMethod(TRUE, 76_0_fib_Return, arith[1], 0) → 570_0_fib_Return(arith[1])
552_1_fib_InvokeMethod(570_0_fib_Return(x0), x1, x2) → Cond_552_1_fib_InvokeMethod1(x1 > 0 && x0 > 0, 570_0_fib_Return(x0), x1, x2)
Cond_552_1_fib_InvokeMethod1(TRUE, 570_0_fib_Return(x0), x1, x2) → 617_0_fib_Return(x1 + x0)
552_1_fib_InvokeMethod(617_0_fib_Return(x0), x1, x2) → Cond_552_1_fib_InvokeMethod2(x1 > 0 && x0 > 0, 617_0_fib_Return(x0), x1, x2)
Cond_552_1_fib_InvokeMethod2(TRUE, 617_0_fib_Return(x0), x1, x2) → 617_0_fib_Return(x1 + x0)
552_1_fib_InvokeMethod(76_0_fib_Return, x2, 1) → Cond_552_1_fib_InvokeMethod3(x2 > 0, 76_0_fib_Return, x2, 1)
Cond_552_1_fib_InvokeMethod3(TRUE, 76_0_fib_Return, x2, 1) → 617_0_fib_Return(x2 + 1)

The integer pair graph contains the following rules and edges:
(1): COND_64_0_FIB_NE(TRUE, x0[1]) → 120_1_FIB_INVOKEMETHOD(64_0_fib_NE(x0[1] - 1), x0[1], x0[1] - 1)
(2): COND_64_0_FIB_NE(TRUE, x0[2]) → 64_0_FIB_NE(x0[2] - 1)
(4): COND_120_1_FIB_INVOKEMETHOD(TRUE, 76_0_fib_Return, x2[4], 1) → 64_0_FIB_NE(x2[4] - 2)
(6): COND_120_1_FIB_INVOKEMETHOD1(TRUE, 570_0_fib_Return(x0[6]), x1[6], x2[6]) → 64_0_FIB_NE(x1[6] - 2)
(8): COND_120_1_FIB_INVOKEMETHOD2(TRUE, 617_0_fib_Return(x0[8]), x1[8], x2[8]) → 64_0_FIB_NE(x1[8] - 2)

The set Q consists of the following terms:
64_0_fib_NE(0)
552_1_fib_InvokeMethod(76_0_fib_Return, x0, 0)
Cond_552_1_fib_InvokeMethod(TRUE, 76_0_fib_Return, x0, 0)
552_1_fib_InvokeMethod(570_0_fib_Return(x0), x1, x2)
Cond_552_1_fib_InvokeMethod1(TRUE, 570_0_fib_Return(x0), x1, x2)
552_1_fib_InvokeMethod(617_0_fib_Return(x0), x1, x2)
Cond_552_1_fib_InvokeMethod2(TRUE, 617_0_fib_Return(x0), x1, x2)
552_1_fib_InvokeMethod(76_0_fib_Return, x0, 1)
Cond_552_1_fib_InvokeMethod3(TRUE, 76_0_fib_Return, x0, 1)

(13) IDependencyGraphProof (EQUIVALENT transformation)

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

(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) Complex Obligation (AND)

(9) Obligation:

(10) IDependencyGraphProof (EQUIVALENT transformation)

(11) TRUE

(12) Obligation:

(13) IDependencyGraphProof (EQUIVALENT transformation)

(14) TRUE