Termination proof of /tmp/tmp5wFHvW/Fibonacci.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 150 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 JBCTerminationSCC

↳5 SCCToIDPv1Proof (⇒, 260 ms)

↳6 IDP

↳7 IDPNonInfProof (⇒, 400 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:
62_0_fib_NE(EOS(STATIC_62), i4, i4) → 64_0_fib_NE(EOS(STATIC_64), i4, i4)
64_0_fib_NE(EOS(STATIC_64), i4, i4) → 67_0_fib_Load(EOS(STATIC_67), i4) | >(i4, 0)
67_0_fib_Load(EOS(STATIC_67), i4) → 71_0_fib_ConstantStackPush(EOS(STATIC_71), i4, i4)
71_0_fib_ConstantStackPush(EOS(STATIC_71), i4, i4) → 76_0_fib_NE(EOS(STATIC_76), i4, i4, 1)
76_0_fib_NE(EOS(STATIC_76), i7, i7, matching1) → 82_0_fib_NE(EOS(STATIC_82), i7, i7, 1) | =(matching1, 1)
82_0_fib_NE(EOS(STATIC_82), i7, i7, matching1) → 91_0_fib_Load(EOS(STATIC_91), i7) | &&(!(=(i7, 1)), =(matching1, 1))
91_0_fib_Load(EOS(STATIC_91), i7) → 97_0_fib_ConstantStackPush(EOS(STATIC_97), i7, i7)
97_0_fib_ConstantStackPush(EOS(STATIC_97), i7, i7) → 102_0_fib_IntArithmetic(EOS(STATIC_102), i7, i7, 1)
102_0_fib_IntArithmetic(EOS(STATIC_102), i7, i7, matching1) → 112_0_fib_InvokeMethod(EOS(STATIC_112), i7, -(i7, 1)) | &&(>(i7, 0), =(matching1, 1))
112_0_fib_InvokeMethod(EOS(STATIC_112), i7, i10) → 117_1_fib_InvokeMethod(117_0_fib_Load(EOS(STATIC_117), i10), i7, i10)
117_0_fib_Load(EOS(STATIC_117), i10) → 124_0_fib_Load(EOS(STATIC_124), i10)
117_1_fib_InvokeMethod(95_0_fib_Return(EOS(STATIC_95), matching1, matching2), i7, matching3) → 140_0_fib_Return(EOS(STATIC_140), i7, 1, 1, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
117_1_fib_InvokeMethod(564_0_fib_Return(EOS(STATIC_564), i160), i7, i178) → 593_0_fib_Return(EOS(STATIC_593), i7, i178, i160)
117_1_fib_InvokeMethod(611_0_fib_Return(EOS(STATIC_611), i201), i7, i206) → 628_0_fib_Return(EOS(STATIC_628), i7, i206, i201)
124_0_fib_Load(EOS(STATIC_124), i10) → 59_0_fib_Load(EOS(STATIC_59), i10)
59_0_fib_Load(EOS(STATIC_59), i1) → 62_0_fib_NE(EOS(STATIC_62), i1, i1)
140_0_fib_Return(EOS(STATIC_140), i7, matching1, matching2, matching3) → 142_0_fib_Load(EOS(STATIC_142), i7, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
142_0_fib_Load(EOS(STATIC_142), i7, matching1) → 253_0_fib_Load(EOS(STATIC_253), i7, 1) | =(matching1, 1)
253_0_fib_Load(EOS(STATIC_253), i7, i39) → 340_0_fib_Load(EOS(STATIC_340), i7, i39)
340_0_fib_Load(EOS(STATIC_340), i7, i78) → 439_0_fib_Load(EOS(STATIC_439), i7, i78)
439_0_fib_Load(EOS(STATIC_439), i7, i118) → 533_0_fib_Load(EOS(STATIC_533), i7, i118)
533_0_fib_Load(EOS(STATIC_533), i7, i160) → 538_0_fib_ConstantStackPush(EOS(STATIC_538), i160, i7)
538_0_fib_ConstantStackPush(EOS(STATIC_538), i160, i7) → 542_0_fib_IntArithmetic(EOS(STATIC_542), i160, i7, 2)
542_0_fib_IntArithmetic(EOS(STATIC_542), i160, i7, matching1) → 544_0_fib_InvokeMethod(EOS(STATIC_544), i160, -(i7, 2)) | &&(>(i7, 0), =(matching1, 2))
544_0_fib_InvokeMethod(EOS(STATIC_544), i160, i171) → 545_1_fib_InvokeMethod(545_0_fib_Load(EOS(STATIC_545), i171), i160, i171)
545_0_fib_Load(EOS(STATIC_545), i171) → 547_0_fib_Load(EOS(STATIC_547), i171)
547_0_fib_Load(EOS(STATIC_547), i171) → 59_0_fib_Load(EOS(STATIC_59), i171)
593_0_fib_Return(EOS(STATIC_593), i7, i178, i160) → 518_0_fib_Return(EOS(STATIC_518), i7, i178, i160)
518_0_fib_Return(EOS(STATIC_518), i7, i161, i160) → 533_0_fib_Load(EOS(STATIC_533), i7, i160)
628_0_fib_Return(EOS(STATIC_628), i7, i206, i201) → 518_0_fib_Return(EOS(STATIC_518), i7, i206, i201)
R rules:
62_0_fib_NE(EOS(STATIC_62), matching1, matching2) → 65_0_fib_NE(EOS(STATIC_65), 0, 0) | &&(=(matching1, 0), =(matching2, 0))
65_0_fib_NE(EOS(STATIC_65), matching1, matching2) → 69_0_fib_ConstantStackPush(EOS(STATIC_69), 0) | &&(=(matching1, 0), =(matching2, 0))
69_0_fib_ConstantStackPush(EOS(STATIC_69), matching1) → 72_0_fib_Return(EOS(STATIC_72), 0, 0) | =(matching1, 0)
76_0_fib_NE(EOS(STATIC_76), matching1, matching2, matching3) → 81_0_fib_NE(EOS(STATIC_81), 1, 1, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
81_0_fib_NE(EOS(STATIC_81), matching1, matching2, matching3) → 89_0_fib_ConstantStackPush(EOS(STATIC_89), 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
89_0_fib_ConstantStackPush(EOS(STATIC_89), matching1) → 95_0_fib_Return(EOS(STATIC_95), 1, 1) | =(matching1, 1)
231_0_fib_Return(EOS(STATIC_231), i7, i40, i39) → 325_0_fib_Return(EOS(STATIC_325), i7, i40, i39)
325_0_fib_Return(EOS(STATIC_325), i7, i79, i78) → 423_0_fib_Return(EOS(STATIC_423), i7, i79, i78)
423_0_fib_Return(EOS(STATIC_423), i7, i119, i118) → 518_0_fib_Return(EOS(STATIC_518), i7, i119, i118)
545_1_fib_InvokeMethod(72_0_fib_Return(EOS(STATIC_72), matching1, matching2), i160, matching3) → 556_0_fib_Return(EOS(STATIC_556), i160, 0, 0, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
545_1_fib_InvokeMethod(95_0_fib_Return(EOS(STATIC_95), matching1, matching2), i160, matching3) → 557_0_fib_Return(EOS(STATIC_557), i160, 1, 1, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
545_1_fib_InvokeMethod(564_0_fib_Return(EOS(STATIC_564), i181), i160, i182) → 595_0_fib_Return(EOS(STATIC_595), i160, i182, i181)
545_1_fib_InvokeMethod(611_0_fib_Return(EOS(STATIC_611), i201), i160, i208) → 631_0_fib_Return(EOS(STATIC_631), i160, i208, i201)
556_0_fib_Return(EOS(STATIC_556), i160, matching1, matching2, matching3) → 559_0_fib_IntArithmetic(EOS(STATIC_559), i160, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
557_0_fib_Return(EOS(STATIC_557), i160, matching1, matching2, matching3) → 561_0_fib_IntArithmetic(EOS(STATIC_561), i160, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
559_0_fib_IntArithmetic(EOS(STATIC_559), i160, matching1) → 564_0_fib_Return(EOS(STATIC_564), +(i160, 0)) | &&(>(i160, 0), =(matching1, 0))
561_0_fib_IntArithmetic(EOS(STATIC_561), i160, matching1) → 607_0_fib_IntArithmetic(EOS(STATIC_607), i160, 1) | =(matching1, 1)
595_0_fib_Return(EOS(STATIC_595), i160, i182, i181) → 607_0_fib_IntArithmetic(EOS(STATIC_607), i160, i181)
607_0_fib_IntArithmetic(EOS(STATIC_607), i160, i181) → 611_0_fib_Return(EOS(STATIC_611), +(i160, i181)) | &&(>(i160, 0), >(i181, 0))
631_0_fib_Return(EOS(STATIC_631), i160, i208, i201) → 595_0_fib_Return(EOS(STATIC_595), i160, i208, i201)

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

P rules:
62_0_fib_NE(EOS(STATIC_62), x0, x0) → 117_1_fib_InvokeMethod(62_0_fib_NE(EOS(STATIC_62), -(x0, 1), -(x0, 1)), x0, -(x0, 1)) | &&(>(x0, 0), !(=(x0, 1)))
117_1_fib_InvokeMethod(95_0_fib_Return(EOS(STATIC_95), 1, 1), x2, 1) → 545_1_fib_InvokeMethod(62_0_fib_NE(EOS(STATIC_62), -(x2, 2), -(x2, 2)), 1, -(x2, 2)) | >(x2, 0)
117_1_fib_InvokeMethod(564_0_fib_Return(EOS(STATIC_564), x0), x1, x2) → 545_1_fib_InvokeMethod(62_0_fib_NE(EOS(STATIC_62), -(x1, 2), -(x1, 2)), x0, -(x1, 2)) | >(x1, 0)
117_1_fib_InvokeMethod(611_0_fib_Return(EOS(STATIC_611), x0), x1, x2) → 545_1_fib_InvokeMethod(62_0_fib_NE(EOS(STATIC_62), -(x1, 2), -(x1, 2)), x0, -(x1, 2)) | >(x1, 0)
R rules:
62_0_fib_NE(EOS(STATIC_62), 0, 0) → 72_0_fib_Return(EOS(STATIC_72), 0, 0)
545_1_fib_InvokeMethod(72_0_fib_Return(EOS(STATIC_72), 0, 0), arith[1], 0) → 564_0_fib_Return(EOS(STATIC_564), arith[1]) | >(arith[1], 0)
545_1_fib_InvokeMethod(564_0_fib_Return(EOS(STATIC_564), x0), x1, x2) → 611_0_fib_Return(EOS(STATIC_611), +(x1, x0)) | &&(>(x1, 0), >(x0, 0))
545_1_fib_InvokeMethod(611_0_fib_Return(EOS(STATIC_611), x0), x1, x2) → 611_0_fib_Return(EOS(STATIC_611), +(x1, x0)) | &&(>(x1, 0), >(x0, 0))
545_1_fib_InvokeMethod(95_0_fib_Return(EOS(STATIC_95), 1, 1), x2, 1) → 611_0_fib_Return(EOS(STATIC_611), +(x2, 1)) | >(x2, 0)

Filtered ground terms:

62_0_fib_NE(x1, x2, x3) → 62_0_fib_NE(x2, x3)
611_0_fib_Return(x1, x2) → 611_0_fib_Return(x2)
564_0_fib_Return(x1, x2) → 564_0_fib_Return(x2)
Cond_117_1_fib_InvokeMethod(x1, x2, x3, x4) → Cond_117_1_fib_InvokeMethod(x1, x3)
95_0_fib_Return(x1, x2, x3) → 95_0_fib_Return
Cond_62_0_fib_NE(x1, x2, x3, x4) → Cond_62_0_fib_NE(x1, x3, x4)
Cond_545_1_fib_InvokeMethod3(x1, x2, x3, x4) → Cond_545_1_fib_InvokeMethod3(x1, x3)
Cond_545_1_fib_InvokeMethod(x1, x2, x3, x4) → Cond_545_1_fib_InvokeMethod(x1, x3)
72_0_fib_Return(x1, x2, x3) → 72_0_fib_Return

Filtered duplicate args:

62_0_fib_NE(x1, x2) → 62_0_fib_NE(x2)
Cond_62_0_fib_NE(x1, x2, x3) → Cond_62_0_fib_NE(x1, x3)

Filtered unneeded arguments:

Cond_117_1_fib_InvokeMethod1(x1, x2, x3, x4) → Cond_117_1_fib_InvokeMethod1(x1, x2, x3)
Cond_117_1_fib_InvokeMethod2(x1, x2, x3, x4) → Cond_117_1_fib_InvokeMethod2(x1, x2, x3)
Cond_545_1_fib_InvokeMethod1(x1, x2, x3, x4) → Cond_545_1_fib_InvokeMethod1(x1, x2, x3)
Cond_545_1_fib_InvokeMethod2(x1, x2, x3, x4) → Cond_545_1_fib_InvokeMethod2(x1, x2, x3)

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

P rules:
62_0_fib_NE(x0) → 117_1_fib_InvokeMethod(62_0_fib_NE(-(x0, 1)), x0, -(x0, 1)) | &&(>(x0, 0), !(=(x0, 1)))
117_1_fib_InvokeMethod(95_0_fib_Return, x2, 1) → 545_1_fib_InvokeMethod(62_0_fib_NE(-(x2, 2)), 1, -(x2, 2)) | >(x2, 0)
117_1_fib_InvokeMethod(564_0_fib_Return(x0), x1, x2) → 545_1_fib_InvokeMethod(62_0_fib_NE(-(x1, 2)), x0, -(x1, 2)) | >(x1, 0)
117_1_fib_InvokeMethod(611_0_fib_Return(x0), x1, x2) → 545_1_fib_InvokeMethod(62_0_fib_NE(-(x1, 2)), x0, -(x1, 2)) | >(x1, 0)
R rules:
62_0_fib_NE(0) → 72_0_fib_Return
545_1_fib_InvokeMethod(72_0_fib_Return, arith[1], 0) → 564_0_fib_Return(arith[1]) | >(arith[1], 0)
545_1_fib_InvokeMethod(564_0_fib_Return(x0), x1, x2) → 611_0_fib_Return(+(x1, x0)) | &&(>(x1, 0), >(x0, 0))
545_1_fib_InvokeMethod(611_0_fib_Return(x0), x1, x2) → 611_0_fib_Return(+(x1, x0)) | &&(>(x1, 0), >(x0, 0))
545_1_fib_InvokeMethod(95_0_fib_Return, x2, 1) → 611_0_fib_Return(+(x2, 1)) | >(x2, 0)

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

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

P rules:
62_0_FIB_NE(x0) → COND_62_0_FIB_NE(&&(>(x0, 0), !(=(x0, 1))), x0)
COND_62_0_FIB_NE(TRUE, x0) → 117_1_FIB_INVOKEMETHOD(62_0_fib_NE(-(x0, 1)), x0, -(x0, 1))
COND_62_0_FIB_NE(TRUE, x0) → 62_0_FIB_NE(-(x0, 1))
117_1_FIB_INVOKEMETHOD(72_0_fib_Return, x2, 1) → COND_117_1_FIB_INVOKEMETHOD(>(x2, 0), 72_0_fib_Return, x2, 1)
COND_117_1_FIB_INVOKEMETHOD(TRUE, 72_0_fib_Return, x2, 1) → 62_0_FIB_NE(-(x2, 2))
117_1_FIB_INVOKEMETHOD(564_0_fib_Return(x0), x1, x2) → COND_117_1_FIB_INVOKEMETHOD1(>(x1, 0), 564_0_fib_Return(x0), x1, x2)
COND_117_1_FIB_INVOKEMETHOD1(TRUE, 564_0_fib_Return(x0), x1, x2) → 62_0_FIB_NE(-(x1, 2))
117_1_FIB_INVOKEMETHOD(611_0_fib_Return(x0), x1, x2) → COND_117_1_FIB_INVOKEMETHOD2(>(x1, 0), 611_0_fib_Return(x0), x1, x2)
COND_117_1_FIB_INVOKEMETHOD2(TRUE, 611_0_fib_Return(x0), x1, x2) → 62_0_FIB_NE(-(x1, 2))
R rules:
62_0_fib_NE(0) → 72_0_fib_Return
545_1_fib_InvokeMethod(72_0_fib_Return, arith[1], 0) → Cond_545_1_fib_InvokeMethod(>(arith[1], 0), 72_0_fib_Return, arith[1], 0)
Cond_545_1_fib_InvokeMethod(TRUE, 72_0_fib_Return, arith[1], 0) → 564_0_fib_Return(arith[1])
545_1_fib_InvokeMethod(564_0_fib_Return(x0), x1, x2) → Cond_545_1_fib_InvokeMethod1(&&(>(x1, 0), >(x0, 0)), 564_0_fib_Return(x0), x1, x2)
Cond_545_1_fib_InvokeMethod1(TRUE, 564_0_fib_Return(x0), x1, x2) → 611_0_fib_Return(+(x1, x0))
545_1_fib_InvokeMethod(611_0_fib_Return(x0), x1, x2) → Cond_545_1_fib_InvokeMethod2(&&(>(x1, 0), >(x0, 0)), 611_0_fib_Return(x0), x1, x2)
Cond_545_1_fib_InvokeMethod2(TRUE, 611_0_fib_Return(x0), x1, x2) → 611_0_fib_Return(+(x1, x0))
545_1_fib_InvokeMethod(72_0_fib_Return, x2, 1) → Cond_545_1_fib_InvokeMethod3(>(x2, 0), 72_0_fib_Return, x2, 1)
Cond_545_1_fib_InvokeMethod3(TRUE, 72_0_fib_Return, x2, 1) → 611_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:
62_0_fib_NE(0) → 72_0_fib_Return
545_1_fib_InvokeMethod(72_0_fib_Return, arith[1], 0) → Cond_545_1_fib_InvokeMethod(arith[1] > 0, 72_0_fib_Return, arith[1], 0)
Cond_545_1_fib_InvokeMethod(TRUE, 72_0_fib_Return, arith[1], 0) → 564_0_fib_Return(arith[1])
545_1_fib_InvokeMethod(564_0_fib_Return(x0), x1, x2) → Cond_545_1_fib_InvokeMethod1(x1 > 0 && x0 > 0, 564_0_fib_Return(x0), x1, x2)
Cond_545_1_fib_InvokeMethod1(TRUE, 564_0_fib_Return(x0), x1, x2) → 611_0_fib_Return(x1 + x0)
545_1_fib_InvokeMethod(611_0_fib_Return(x0), x1, x2) → Cond_545_1_fib_InvokeMethod2(x1 > 0 && x0 > 0, 611_0_fib_Return(x0), x1, x2)
Cond_545_1_fib_InvokeMethod2(TRUE, 611_0_fib_Return(x0), x1, x2) → 611_0_fib_Return(x1 + x0)
545_1_fib_InvokeMethod(72_0_fib_Return, x2, 1) → Cond_545_1_fib_InvokeMethod3(x2 > 0, 72_0_fib_Return, x2, 1)
Cond_545_1_fib_InvokeMethod3(TRUE, 72_0_fib_Return, x2, 1) → 611_0_fib_Return(x2 + 1)

The integer pair graph contains the following rules and edges:
(0): 62_0_FIB_NE(x0[0]) → COND_62_0_FIB_NE(x0[0] > 0 && !(x0[0] = 1), x0[0])
(1): COND_62_0_FIB_NE(TRUE, x0[1]) → 117_1_FIB_INVOKEMETHOD(62_0_fib_NE(x0[1] - 1), x0[1], x0[1] - 1)
(2): COND_62_0_FIB_NE(TRUE, x0[2]) → 62_0_FIB_NE(x0[2] - 1)
(3): 117_1_FIB_INVOKEMETHOD(72_0_fib_Return, x2[3], 1) → COND_117_1_FIB_INVOKEMETHOD(x2[3] > 0, 72_0_fib_Return, x2[3], 1)
(4): COND_117_1_FIB_INVOKEMETHOD(TRUE, 72_0_fib_Return, x2[4], 1) → 62_0_FIB_NE(x2[4] - 2)
(5): 117_1_FIB_INVOKEMETHOD(564_0_fib_Return(x0[5]), x1[5], x2[5]) → COND_117_1_FIB_INVOKEMETHOD1(x1[5] > 0, 564_0_fib_Return(x0[5]), x1[5], x2[5])
(6): COND_117_1_FIB_INVOKEMETHOD1(TRUE, 564_0_fib_Return(x0[6]), x1[6], x2[6]) → 62_0_FIB_NE(x1[6] - 2)
(7): 117_1_FIB_INVOKEMETHOD(611_0_fib_Return(x0[7]), x1[7], x2[7]) → COND_117_1_FIB_INVOKEMETHOD2(x1[7] > 0, 611_0_fib_Return(x0[7]), x1[7], x2[7])
(8): COND_117_1_FIB_INVOKEMETHOD2(TRUE, 611_0_fib_Return(x0[8]), x1[8], x2[8]) → 62_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 (62_0_fib_NE(x0[1] - 1) →^* 72_0_fib_Return∧x0[1] →^* x2[3]∧x0[1] - 1 →^* 1)

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

(1) -> (7), if (62_0_fib_NE(x0[1] - 1) →^* 611_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 ∧564_0_fib_Return(x0[5]) →^* 564_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 ∧611_0_fib_Return(x0[7]) →^* 611_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:
62_0_fib_NE(0)
545_1_fib_InvokeMethod(72_0_fib_Return, x0, 0)
Cond_545_1_fib_InvokeMethod(TRUE, 72_0_fib_Return, x0, 0)
545_1_fib_InvokeMethod(564_0_fib_Return(x0), x1, x2)
Cond_545_1_fib_InvokeMethod1(TRUE, 564_0_fib_Return(x0), x1, x2)
545_1_fib_InvokeMethod(611_0_fib_Return(x0), x1, x2)
Cond_545_1_fib_InvokeMethod2(TRUE, 611_0_fib_Return(x0), x1, x2)
545_1_fib_InvokeMethod(72_0_fib_Return, x0, 1)
Cond_545_1_fib_InvokeMethod3(TRUE, 72_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@6d6e2026 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 62_0_FIB_NE(x0) → COND_62_0_FIB_NE(&&(>(x0, 0), !(=(x0, 1))), x0) the following chains were created:

We consider the chain 62_0_FIB_NE(x0[0]) → COND_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0]), COND_62_0_FIB_NE(TRUE, x0[1]) → 117_1_FIB_INVOKEMETHOD(62_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] ⇒ 62_0_FIB_NE(x0[0])≥NonInfC∧62_0_FIB_NE(x0[0])≥COND_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])∧(U^Increasing(COND_62_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 ⇒ 62_0_FIB_NE(x0[0])≥NonInfC∧62_0_FIB_NE(x0[0])≥COND_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])∧(U^Increasing(COND_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥))

(3)    (>(x0[0], 0)=TRUE∧>(x0[0], 1)=TRUE ⇒ 62_0_FIB_NE(x0[0])≥NonInfC∧62_0_FIB_NE(x0[0])≥COND_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])∧(U^Increasing(COND_62_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_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[(-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_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[(-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_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[(-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_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[(-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_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[(-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_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[(-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_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[(-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_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[bni_30 + (-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[(-1)bso_31] ≥ 0)
We consider the chain 62_0_FIB_NE(x0[0]) → COND_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0]), COND_62_0_FIB_NE(TRUE, x0[2]) → 62_0_FIB_NE(-(x0[2], 1)) which results in the following constraint:
(12)    (&&(>(x0[0], 0), !(=(x0[0], 1)))=TRUE∧x0[0]=x0[2] ⇒ 62_0_FIB_NE(x0[0])≥NonInfC∧62_0_FIB_NE(x0[0])≥COND_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])∧(U^Increasing(COND_62_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 ⇒ 62_0_FIB_NE(x0[0])≥NonInfC∧62_0_FIB_NE(x0[0])≥COND_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])∧(U^Increasing(COND_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥))

(14)    (>(x0[0], 0)=TRUE∧>(x0[0], 1)=TRUE ⇒ 62_0_FIB_NE(x0[0])≥NonInfC∧62_0_FIB_NE(x0[0])≥COND_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])∧(U^Increasing(COND_62_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_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[(-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_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[(-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_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[(-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_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[(-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_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[(-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_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[(-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_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[(-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[(-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_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[bni_30 + (-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[(-1)bso_31] ≥ 0)

For Pair COND_62_0_FIB_NE(TRUE, x0) → 117_1_FIB_INVOKEMETHOD(62_0_fib_NE(-(x0, 1)), x0, -(x0, 1)) the following chains were created:

We consider the chain COND_62_0_FIB_NE(TRUE, x0[1]) → 117_1_FIB_INVOKEMETHOD(62_0_fib_NE(-(x0[1], 1)), x0[1], -(x0[1], 1)) which results in the following constraint:
(23)    (COND_62_0_FIB_NE(TRUE, x0[1])≥NonInfC∧COND_62_0_FIB_NE(TRUE, x0[1])≥117_1_FIB_INVOKEMETHOD(62_0_fib_NE(-(x0[1], 1)), x0[1], -(x0[1], 1))∧(U^Increasing(117_1_FIB_INVOKEMETHOD(62_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(117_1_FIB_INVOKEMETHOD(62_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(117_1_FIB_INVOKEMETHOD(62_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(117_1_FIB_INVOKEMETHOD(62_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(117_1_FIB_INVOKEMETHOD(62_0_fib_NE(-(x0[1], 1)), x0[1], -(x0[1], 1))), ≥)∧[bni_32] = 0∧0 = 0∧[(-1)bso_33] ≥ 0)

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

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

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

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

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

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

For Pair 117_1_FIB_INVOKEMETHOD(72_0_fib_Return, x2, 1) → COND_117_1_FIB_INVOKEMETHOD(>(x2, 0), 72_0_fib_Return, x2, 1) the following chains were created:

We consider the chain 117_1_FIB_INVOKEMETHOD(72_0_fib_Return, x2[3], 1) → COND_117_1_FIB_INVOKEMETHOD(>(x2[3], 0), 72_0_fib_Return, x2[3], 1), COND_117_1_FIB_INVOKEMETHOD(TRUE, 72_0_fib_Return, x2[4], 1) → 62_0_FIB_NE(-(x2[4], 2)) which results in the following constraint:
(33)    (>(x2[3], 0)=TRUE∧x2[3]=x2[4] ⇒ 117_1_FIB_INVOKEMETHOD(72_0_fib_Return, x2[3], 1)≥NonInfC∧117_1_FIB_INVOKEMETHOD(72_0_fib_Return, x2[3], 1)≥COND_117_1_FIB_INVOKEMETHOD(>(x2[3], 0), 72_0_fib_Return, x2[3], 1)∧(U^Increasing(COND_117_1_FIB_INVOKEMETHOD(>(x2[3], 0), 72_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 ⇒ 117_1_FIB_INVOKEMETHOD(72_0_fib_Return, x2[3], 1)≥NonInfC∧117_1_FIB_INVOKEMETHOD(72_0_fib_Return, x2[3], 1)≥COND_117_1_FIB_INVOKEMETHOD(>(x2[3], 0), 72_0_fib_Return, x2[3], 1)∧(U^Increasing(COND_117_1_FIB_INVOKEMETHOD(>(x2[3], 0), 72_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_117_1_FIB_INVOKEMETHOD(>(x2[3], 0), 72_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_117_1_FIB_INVOKEMETHOD(>(x2[3], 0), 72_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_117_1_FIB_INVOKEMETHOD(>(x2[3], 0), 72_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_117_1_FIB_INVOKEMETHOD(>(x2[3], 0), 72_0_fib_Return, x2[3], 1)), ≥)∧[(-1)Bound*bni_36] + [bni_36]x2[3] ≥ 0∧[(-1)bso_37] ≥ 0)

For Pair COND_117_1_FIB_INVOKEMETHOD(TRUE, 72_0_fib_Return, x2, 1) → 62_0_FIB_NE(-(x2, 2)) the following chains were created:

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

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

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

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

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

For Pair 117_1_FIB_INVOKEMETHOD(564_0_fib_Return(x0), x1, x2) → COND_117_1_FIB_INVOKEMETHOD1(>(x1, 0), 564_0_fib_Return(x0), x1, x2) the following chains were created:

We consider the chain 117_1_FIB_INVOKEMETHOD(564_0_fib_Return(x0[5]), x1[5], x2[5]) → COND_117_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 564_0_fib_Return(x0[5]), x1[5], x2[5]), COND_117_1_FIB_INVOKEMETHOD1(TRUE, 564_0_fib_Return(x0[6]), x1[6], x2[6]) → 62_0_FIB_NE(-(x1[6], 2)) which results in the following constraint:
(44)    (>(x1[5], 0)=TRUE∧564_0_fib_Return(x0[5])=564_0_fib_Return(x0[6])∧x1[5]=x1[6]∧x2[5]=x2[6] ⇒ 117_1_FIB_INVOKEMETHOD(564_0_fib_Return(x0[5]), x1[5], x2[5])≥NonInfC∧117_1_FIB_INVOKEMETHOD(564_0_fib_Return(x0[5]), x1[5], x2[5])≥COND_117_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 564_0_fib_Return(x0[5]), x1[5], x2[5])∧(U^Increasing(COND_117_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 564_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 ⇒ 117_1_FIB_INVOKEMETHOD(564_0_fib_Return(x0[5]), x1[5], x2[5])≥NonInfC∧117_1_FIB_INVOKEMETHOD(564_0_fib_Return(x0[5]), x1[5], x2[5])≥COND_117_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 564_0_fib_Return(x0[5]), x1[5], x2[5])∧(U^Increasing(COND_117_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 564_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_117_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 564_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_117_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 564_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_117_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 564_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_117_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 564_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_117_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 564_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_117_1_FIB_INVOKEMETHOD1(TRUE, 564_0_fib_Return(x0), x1, x2) → 62_0_FIB_NE(-(x1, 2)) the following chains were created:

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

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

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

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

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

For Pair 117_1_FIB_INVOKEMETHOD(611_0_fib_Return(x0), x1, x2) → COND_117_1_FIB_INVOKEMETHOD2(>(x1, 0), 611_0_fib_Return(x0), x1, x2) the following chains were created:

We consider the chain 117_1_FIB_INVOKEMETHOD(611_0_fib_Return(x0[7]), x1[7], x2[7]) → COND_117_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 611_0_fib_Return(x0[7]), x1[7], x2[7]), COND_117_1_FIB_INVOKEMETHOD2(TRUE, 611_0_fib_Return(x0[8]), x1[8], x2[8]) → 62_0_FIB_NE(-(x1[8], 2)) which results in the following constraint:
(56)    (>(x1[7], 0)=TRUE∧611_0_fib_Return(x0[7])=611_0_fib_Return(x0[8])∧x1[7]=x1[8]∧x2[7]=x2[8] ⇒ 117_1_FIB_INVOKEMETHOD(611_0_fib_Return(x0[7]), x1[7], x2[7])≥NonInfC∧117_1_FIB_INVOKEMETHOD(611_0_fib_Return(x0[7]), x1[7], x2[7])≥COND_117_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 611_0_fib_Return(x0[7]), x1[7], x2[7])∧(U^Increasing(COND_117_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 611_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 ⇒ 117_1_FIB_INVOKEMETHOD(611_0_fib_Return(x0[7]), x1[7], x2[7])≥NonInfC∧117_1_FIB_INVOKEMETHOD(611_0_fib_Return(x0[7]), x1[7], x2[7])≥COND_117_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 611_0_fib_Return(x0[7]), x1[7], x2[7])∧(U^Increasing(COND_117_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 611_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_117_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 611_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_117_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 611_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_117_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 611_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_117_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 611_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_117_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 611_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_117_1_FIB_INVOKEMETHOD2(TRUE, 611_0_fib_Return(x0), x1, x2) → 62_0_FIB_NE(-(x1, 2)) the following chains were created:

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

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

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

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

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

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

62_0_FIB_NE(x0) → COND_62_0_FIB_NE(&&(>(x0, 0), !(=(x0, 1))), x0)
- ([1] + x0[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(COND_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[bni_30 + (-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[(-1)bso_31] ≥ 0)
- ([1] + x0[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(COND_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥)∧[bni_30 + (-1)Bound*bni_30] + [bni_30]x0[0] ≥ 0∧[(-1)bso_31] ≥ 0)
COND_62_0_FIB_NE(TRUE, x0) → 117_1_FIB_INVOKEMETHOD(62_0_fib_NE(-(x0, 1)), x0, -(x0, 1))
- ((U^Increasing(117_1_FIB_INVOKEMETHOD(62_0_fib_NE(-(x0[1], 1)), x0[1], -(x0[1], 1))), ≥)∧[bni_32] = 0∧0 = 0∧[(-1)bso_33] ≥ 0)
COND_62_0_FIB_NE(TRUE, x0) → 62_0_FIB_NE(-(x0, 1))
- ((U^Increasing(62_0_FIB_NE(-(x0[2], 1))), ≥)∧[bni_34] = 0∧0 = 0∧[1 + (-1)bso_35] ≥ 0)
117_1_FIB_INVOKEMETHOD(72_0_fib_Return, x2, 1) → COND_117_1_FIB_INVOKEMETHOD(>(x2, 0), 72_0_fib_Return, x2, 1)
- (x2[3] ≥ 0 ⇒ (U^Increasing(COND_117_1_FIB_INVOKEMETHOD(>(x2[3], 0), 72_0_fib_Return, x2[3], 1)), ≥)∧[(-1)Bound*bni_36] + [bni_36]x2[3] ≥ 0∧[(-1)bso_37] ≥ 0)
COND_117_1_FIB_INVOKEMETHOD(TRUE, 72_0_fib_Return, x2, 1) → 62_0_FIB_NE(-(x2, 2))
- ((U^Increasing(62_0_FIB_NE(-(x2[4], 2))), ≥)∧[bni_38] = 0∧0 = 0∧[2 + (-1)bso_39] ≥ 0)
117_1_FIB_INVOKEMETHOD(564_0_fib_Return(x0), x1, x2) → COND_117_1_FIB_INVOKEMETHOD1(>(x1, 0), 564_0_fib_Return(x0), x1, x2)
- (x1[5] ≥ 0 ⇒ (U^Increasing(COND_117_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 564_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_117_1_FIB_INVOKEMETHOD1(TRUE, 564_0_fib_Return(x0), x1, x2) → 62_0_FIB_NE(-(x1, 2))
- ((U^Increasing(62_0_FIB_NE(-(x1[6], 2))), ≥)∧[bni_42] = 0∧0 = 0∧0 = 0∧0 = 0∧[2 + (-1)bso_43] ≥ 0)
117_1_FIB_INVOKEMETHOD(611_0_fib_Return(x0), x1, x2) → COND_117_1_FIB_INVOKEMETHOD2(>(x1, 0), 611_0_fib_Return(x0), x1, x2)
- (x1[7] ≥ 0 ⇒ (U^Increasing(COND_117_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 611_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_117_1_FIB_INVOKEMETHOD2(TRUE, 611_0_fib_Return(x0), x1, x2) → 62_0_FIB_NE(-(x1, 2))
- ((U^Increasing(62_0_FIB_NE(-(x1[8], 2))), ≥)∧[bni_46] = 0∧0 = 0∧0 = 0∧0 = 0∧[2 + (-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(62_0_fib_NE(x₁)) = [-1] + [2]x₁
POL(0) = 0
POL(72_0_fib_Return) = [-1]
POL(545_1_fib_InvokeMethod(x₁, x₂, x₃)) = [-1] + [-1]x₂ + [-1]x₁
POL(Cond_545_1_fib_InvokeMethod(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃
POL(>(x₁, x₂)) = [-1]
POL(564_0_fib_Return(x₁)) = x₁
POL(Cond_545_1_fib_InvokeMethod1(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + [-1]x₂
POL(&&(x₁, x₂)) = [-1]
POL(611_0_fib_Return(x₁)) = x₁
POL(+(x₁, x₂)) = x₁ + x₂
POL(Cond_545_1_fib_InvokeMethod2(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + [-1]x₂
POL(1) = [1]
POL(Cond_545_1_fib_InvokeMethod3(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃
POL(62_0_FIB_NE(x₁)) = [-1] + x₁
POL(COND_62_0_FIB_NE(x₁, x₂)) = [-1] + x₂
POL(!(x₁)) = [-1]
POL(=(x₁, x₂)) = [-1]
POL(117_1_FIB_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + x₂
POL(-(x₁, x₂)) = x₁ + [-1]x₂
POL(COND_117_1_FIB_INVOKEMETHOD(x₁, x₂, x₃, x₄)) = [-1] + x₃
POL(2) = [2]
POL(COND_117_1_FIB_INVOKEMETHOD1(x₁, x₂, x₃, x₄)) = [-1] + x₃
POL(COND_117_1_FIB_INVOKEMETHOD2(x₁, x₂, x₃, x₄)) = [-1] + x₃

The following pairs are in P_>:

COND_62_0_FIB_NE(TRUE, x0[2]) → 62_0_FIB_NE(-(x0[2], 1))
COND_117_1_FIB_INVOKEMETHOD(TRUE, 72_0_fib_Return, x2[4], 1) → 62_0_FIB_NE(-(x2[4], 2))
COND_117_1_FIB_INVOKEMETHOD1(TRUE, 564_0_fib_Return(x0[6]), x1[6], x2[6]) → 62_0_FIB_NE(-(x1[6], 2))
COND_117_1_FIB_INVOKEMETHOD2(TRUE, 611_0_fib_Return(x0[8]), x1[8], x2[8]) → 62_0_FIB_NE(-(x1[8], 2))

The following pairs are in P_bound:

62_0_FIB_NE(x0[0]) → COND_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])
117_1_FIB_INVOKEMETHOD(72_0_fib_Return, x2[3], 1) → COND_117_1_FIB_INVOKEMETHOD(>(x2[3], 0), 72_0_fib_Return, x2[3], 1)
117_1_FIB_INVOKEMETHOD(564_0_fib_Return(x0[5]), x1[5], x2[5]) → COND_117_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 564_0_fib_Return(x0[5]), x1[5], x2[5])
117_1_FIB_INVOKEMETHOD(611_0_fib_Return(x0[7]), x1[7], x2[7]) → COND_117_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 611_0_fib_Return(x0[7]), x1[7], x2[7])

The following pairs are in P_≥:

62_0_FIB_NE(x0[0]) → COND_62_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])
COND_62_0_FIB_NE(TRUE, x0[1]) → 117_1_FIB_INVOKEMETHOD(62_0_fib_NE(-(x0[1], 1)), x0[1], -(x0[1], 1))
117_1_FIB_INVOKEMETHOD(72_0_fib_Return, x2[3], 1) → COND_117_1_FIB_INVOKEMETHOD(>(x2[3], 0), 72_0_fib_Return, x2[3], 1)
117_1_FIB_INVOKEMETHOD(564_0_fib_Return(x0[5]), x1[5], x2[5]) → COND_117_1_FIB_INVOKEMETHOD1(>(x1[5], 0), 564_0_fib_Return(x0[5]), x1[5], x2[5])
117_1_FIB_INVOKEMETHOD(611_0_fib_Return(x0[7]), x1[7], x2[7]) → COND_117_1_FIB_INVOKEMETHOD2(>(x1[7], 0), 611_0_fib_Return(x0[7]), x1[7], x2[7])

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

62_0_fib_NE(0)¹ ↔ 72_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:
62_0_fib_NE(0) → 72_0_fib_Return
545_1_fib_InvokeMethod(72_0_fib_Return, arith[1], 0) → Cond_545_1_fib_InvokeMethod(arith[1] > 0, 72_0_fib_Return, arith[1], 0)
Cond_545_1_fib_InvokeMethod(TRUE, 72_0_fib_Return, arith[1], 0) → 564_0_fib_Return(arith[1])
545_1_fib_InvokeMethod(564_0_fib_Return(x0), x1, x2) → Cond_545_1_fib_InvokeMethod1(x1 > 0 && x0 > 0, 564_0_fib_Return(x0), x1, x2)
Cond_545_1_fib_InvokeMethod1(TRUE, 564_0_fib_Return(x0), x1, x2) → 611_0_fib_Return(x1 + x0)
545_1_fib_InvokeMethod(611_0_fib_Return(x0), x1, x2) → Cond_545_1_fib_InvokeMethod2(x1 > 0 && x0 > 0, 611_0_fib_Return(x0), x1, x2)
Cond_545_1_fib_InvokeMethod2(TRUE, 611_0_fib_Return(x0), x1, x2) → 611_0_fib_Return(x1 + x0)
545_1_fib_InvokeMethod(72_0_fib_Return, x2, 1) → Cond_545_1_fib_InvokeMethod3(x2 > 0, 72_0_fib_Return, x2, 1)
Cond_545_1_fib_InvokeMethod3(TRUE, 72_0_fib_Return, x2, 1) → 611_0_fib_Return(x2 + 1)

The integer pair graph contains the following rules and edges:
(0): 62_0_FIB_NE(x0[0]) → COND_62_0_FIB_NE(x0[0] > 0 && !(x0[0] = 1), x0[0])
(1): COND_62_0_FIB_NE(TRUE, x0[1]) → 117_1_FIB_INVOKEMETHOD(62_0_fib_NE(x0[1] - 1), x0[1], x0[1] - 1)
(3): 117_1_FIB_INVOKEMETHOD(72_0_fib_Return, x2[3], 1) → COND_117_1_FIB_INVOKEMETHOD(x2[3] > 0, 72_0_fib_Return, x2[3], 1)
(5): 117_1_FIB_INVOKEMETHOD(564_0_fib_Return(x0[5]), x1[5], x2[5]) → COND_117_1_FIB_INVOKEMETHOD1(x1[5] > 0, 564_0_fib_Return(x0[5]), x1[5], x2[5])
(7): 117_1_FIB_INVOKEMETHOD(611_0_fib_Return(x0[7]), x1[7], x2[7]) → COND_117_1_FIB_INVOKEMETHOD2(x1[7] > 0, 611_0_fib_Return(x0[7]), x1[7], x2[7])

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

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

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

(1) -> (7), if (62_0_fib_NE(x0[1] - 1) →^* 611_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:
62_0_fib_NE(0) → 72_0_fib_Return
545_1_fib_InvokeMethod(72_0_fib_Return, arith[1], 0) → Cond_545_1_fib_InvokeMethod(arith[1] > 0, 72_0_fib_Return, arith[1], 0)
Cond_545_1_fib_InvokeMethod(TRUE, 72_0_fib_Return, arith[1], 0) → 564_0_fib_Return(arith[1])
545_1_fib_InvokeMethod(564_0_fib_Return(x0), x1, x2) → Cond_545_1_fib_InvokeMethod1(x1 > 0 && x0 > 0, 564_0_fib_Return(x0), x1, x2)
Cond_545_1_fib_InvokeMethod1(TRUE, 564_0_fib_Return(x0), x1, x2) → 611_0_fib_Return(x1 + x0)
545_1_fib_InvokeMethod(611_0_fib_Return(x0), x1, x2) → Cond_545_1_fib_InvokeMethod2(x1 > 0 && x0 > 0, 611_0_fib_Return(x0), x1, x2)
Cond_545_1_fib_InvokeMethod2(TRUE, 611_0_fib_Return(x0), x1, x2) → 611_0_fib_Return(x1 + x0)
545_1_fib_InvokeMethod(72_0_fib_Return, x2, 1) → Cond_545_1_fib_InvokeMethod3(x2 > 0, 72_0_fib_Return, x2, 1)
Cond_545_1_fib_InvokeMethod3(TRUE, 72_0_fib_Return, x2, 1) → 611_0_fib_Return(x2 + 1)

The integer pair graph contains the following rules and edges:
(1): COND_62_0_FIB_NE(TRUE, x0[1]) → 117_1_FIB_INVOKEMETHOD(62_0_fib_NE(x0[1] - 1), x0[1], x0[1] - 1)
(2): COND_62_0_FIB_NE(TRUE, x0[2]) → 62_0_FIB_NE(x0[2] - 1)
(4): COND_117_1_FIB_INVOKEMETHOD(TRUE, 72_0_fib_Return, x2[4], 1) → 62_0_FIB_NE(x2[4] - 2)
(6): COND_117_1_FIB_INVOKEMETHOD1(TRUE, 564_0_fib_Return(x0[6]), x1[6], x2[6]) → 62_0_FIB_NE(x1[6] - 2)
(8): COND_117_1_FIB_INVOKEMETHOD2(TRUE, 611_0_fib_Return(x0[8]), x1[8], x2[8]) → 62_0_FIB_NE(x1[8] - 2)

The set Q consists of the following terms:
62_0_fib_NE(0)
545_1_fib_InvokeMethod(72_0_fib_Return, x0, 0)
Cond_545_1_fib_InvokeMethod(TRUE, 72_0_fib_Return, x0, 0)
545_1_fib_InvokeMethod(564_0_fib_Return(x0), x1, x2)
Cond_545_1_fib_InvokeMethod1(TRUE, 564_0_fib_Return(x0), x1, x2)
545_1_fib_InvokeMethod(611_0_fib_Return(x0), x1, x2)
Cond_545_1_fib_InvokeMethod2(TRUE, 611_0_fib_Return(x0), x1, x2)
545_1_fib_InvokeMethod(72_0_fib_Return, x0, 1)
Cond_545_1_fib_InvokeMethod3(TRUE, 72_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