(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_Returnx0[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] > 0x2[3]* x2[4])


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


(5) -> (6), if (x1[5] > 0570_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] > 0617_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)))=TRUEx0[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])∧(UIncreasing(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)=TRUE64_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])∧(UIncreasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥))


    (3)    (>(x0[0], 0)=TRUE>(x0[0], 1)=TRUE64_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])∧(UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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)))=TRUEx0[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])∧(UIncreasing(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)=TRUE64_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])∧(UIncreasing(COND_64_0_FIB_NE(&&(>(x0[0], 0), !(=(x0[0], 1))), x0[0])), ≥))


    (14)    (>(x0[0], 0)=TRUE>(x0[0], 1)=TRUE64_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])∧(UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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))∧(UIncreasing(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)    ((UIncreasing(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)    ((UIncreasing(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)    ((UIncreasing(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)    ((UIncreasing(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))∧(UIncreasing(64_0_FIB_NE(-(x0[2], 1))), ≥))



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

    (29)    ((UIncreasing(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)    ((UIncreasing(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)    ((UIncreasing(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)    ((UIncreasing(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)=TRUEx2[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)∧(UIncreasing(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)=TRUE120_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)∧(UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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))∧(UIncreasing(64_0_FIB_NE(-(x2[4], 2))), ≥))



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

    (40)    ((UIncreasing(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)    ((UIncreasing(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)    ((UIncreasing(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)    ((UIncreasing(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)=TRUE570_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])∧(UIncreasing(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)=TRUE120_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])∧(UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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))∧(UIncreasing(64_0_FIB_NE(-(x1[6], 2))), ≥))



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

    (52)    ((UIncreasing(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)    ((UIncreasing(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)    ((UIncreasing(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)    ((UIncreasing(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)=TRUE617_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])∧(UIncreasing(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)=TRUE120_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])∧(UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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))∧(UIncreasing(64_0_FIB_NE(-(x1[8], 2))), ≥))



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

    (64)    ((UIncreasing(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)    ((UIncreasing(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)    ((UIncreasing(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)    ((UIncreasing(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 ⇒ (UIncreasing(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 ⇒ (UIncreasing(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))
    • ((UIncreasing(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))
    • ((UIncreasing(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 ⇒ (UIncreasing(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))
    • ((UIncreasing(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 ⇒ (UIncreasing(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))
    • ((UIncreasing(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 ⇒ (UIncreasing(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))
    • ((UIncreasing(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 Pbound 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 Pbound.
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(x1)) = [-1] + [-1]x1   
POL(0) = 0   
POL(76_0_fib_Return) = [-1]   
POL(552_1_fib_InvokeMethod(x1, x2, x3)) = [-1] + [-1]x2 + [-1]x1   
POL(Cond_552_1_fib_InvokeMethod(x1, x2, x3, x4)) = [-1] + [-1]x3   
POL(>(x1, x2)) = [-1]   
POL(570_0_fib_Return(x1)) = x1   
POL(Cond_552_1_fib_InvokeMethod1(x1, x2, x3, x4)) = [-1] + [-1]x3 + [-1]x2   
POL(&&(x1, x2)) = [-1]   
POL(617_0_fib_Return(x1)) = x1   
POL(+(x1, x2)) = x1 + x2   
POL(Cond_552_1_fib_InvokeMethod2(x1, x2, x3, x4)) = [-1] + [-1]x3 + [-1]x2   
POL(1) = [1]   
POL(Cond_552_1_fib_InvokeMethod3(x1, x2, x3, x4)) = [-1] + [-1]x3   
POL(64_0_FIB_NE(x1)) = x1   
POL(COND_64_0_FIB_NE(x1, x2)) = [-1] + x2   
POL(!(x1)) = [-1]   
POL(=(x1, x2)) = [-1]   
POL(120_1_FIB_INVOKEMETHOD(x1, x2, x3)) = [-1] + x2   
POL(-(x1, x2)) = x1 + [-1]x2   
POL(COND_120_1_FIB_INVOKEMETHOD(x1, x2, x3, x4)) = [-1] + x3   
POL(2) = [2]   
POL(COND_120_1_FIB_INVOKEMETHOD1(x1, x2, x3, x4)) = [-1] + x3   
POL(COND_120_1_FIB_INVOKEMETHOD2(x1, x2, x3, x4)) = [-1] + x3   

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 Pbound:

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)176_0_fib_Return1

(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_Returnx0[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])



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)

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

(14) TRUE