Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 298 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 JBCTerminationSCC
↳5 SCCToIntTRSProof (⇒, 70 ms)
↳6 intTRS
↳7 PolynomialOrderProcessor (⇒, 4 ms)
↳8 intTRS
↳9 TerminationGraphProcessor (⇔, 0 ms)
↳10 YES

(0) Obligation:

JBC Problem based on JBC Program:
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:
  • Used field analysis yielded the following read fields:
  • Marker field analysis yielded the following relations that could be markers:

(5) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 32 IRules

P rules:
f66_0_fib_NE(EOS, i4, i4, i4) → f67_0_fib_NE(EOS, i4, i4, i4)
f67_0_fib_NE(EOS, i4, i4, i4) → f71_0_fib_Load(EOS, i4, i4) | >(i4, 0)
f71_0_fib_Load(EOS, i4, i4) → f75_0_fib_ConstantStackPush(EOS, i4, i4, i4)
f75_0_fib_ConstantStackPush(EOS, i4, i4, i4) → f79_0_fib_NE(EOS, i4, i4, i4, 1)
f79_0_fib_NE(EOS, i7, i7, i7, matching1) → f85_0_fib_NE(EOS, i7, i7, i7, 1) | =(matching1, 1)
f85_0_fib_NE(EOS, i7, i7, i7, matching1) → f110_0_fib_Load(EOS, i7, i7) | &&(>(i7, 1), =(matching1, 1))
f110_0_fib_Load(EOS, i7, i7) → f117_0_fib_ConstantStackPush(EOS, i7, i7, i7)
f117_0_fib_ConstantStackPush(EOS, i7, i7, i7) → f122_0_fib_IntArithmetic(EOS, i7, i7, i7, 1)
f122_0_fib_IntArithmetic(EOS, i7, i7, i7, matching1) → f136_0_fib_InvokeMethod(EOS, i7, i7, -(i7, 1)) | &&(>(i7, 0), =(matching1, 1))
f136_0_fib_InvokeMethod(EOS, i7, i7, i14) → f139_0_fib_Load(EOS, i14, i14)
f136_0_fib_InvokeMethod(EOS, i7, i7, i14) → f139_1_fib_Load(EOS, i7, i7, i14, i14)
f139_0_fib_Load(EOS, i14, i14) → f148_0_fib_Load(EOS, i14, i14)
f148_0_fib_Load(EOS, i14, i14) → f63_0_fib_Load(EOS, i14, i14)
f63_0_fib_Load(EOS, i1, i1) → f66_0_fib_NE(EOS, i1, i1, i1)
f183_0_fib_Return(EOS, i7, i7, matching1, matching2, matching3) → f184_0_fib_Load(EOS, i7, i7, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
f184_0_fib_Load(EOS, i7, i7, matching1) → f416_0_fib_Load(EOS, i7, i7, 1) | =(matching1, 1)
f416_0_fib_Load(EOS, i7, i7, i66) → f593_0_fib_Load(EOS, i7, i7, i66)
f593_0_fib_Load(EOS, i7, i7, i130) → f792_0_fib_Load(EOS, i7, i7, i130)
f792_0_fib_Load(EOS, i7, i7, i199) → f924_0_fib_Load(EOS, i7, i7, i199)
f924_0_fib_Load(EOS, i7, i7, i263) → f927_0_fib_ConstantStackPush(EOS, i7, i263, i7)
f927_0_fib_ConstantStackPush(EOS, i7, i263, i7) → f929_0_fib_IntArithmetic(EOS, i7, i263, i7, 2)
f929_0_fib_IntArithmetic(EOS, i7, i263, i7, matching1) → f930_0_fib_InvokeMethod(EOS, i7, i263, -(i7, 2)) | &&(>(i7, 0), =(matching1, 2))
f930_0_fib_InvokeMethod(EOS, i7, i263, i274) → f932_0_fib_Load(EOS, i274, i274)
f930_0_fib_InvokeMethod(EOS, i7, i263, i274) → f932_1_fib_Load(EOS, i7, i263, i274, i274)
f932_0_fib_Load(EOS, i274, i274) → f934_0_fib_Load(EOS, i274, i274)
f934_0_fib_Load(EOS, i274, i274) → f63_0_fib_Load(EOS, i274, i274)
f1005_0_fib_Return(EOS, i7, i7, i290, i287) → f910_0_fib_Return(EOS, i7, i7, i290, i287)
f910_0_fib_Return(EOS, i7, i7, i264, i263) → f924_0_fib_Load(EOS, i7, i7, i263)
f1050_0_fib_Return(EOS, i7, i7, i334, i332) → f910_0_fib_Return(EOS, i7, i7, i334, i332)
f139_1_fib_Load(EOS, i7, i7, matching1, matching2) → f183_0_fib_Return(EOS, i7, i7, 1, 1, 1) | &&(=(matching1, 1), =(matching2, 1))
f139_1_fib_Load(EOS, i7, i7, i290, i290) → f1005_0_fib_Return(EOS, i7, i7, i290, i287)
f139_1_fib_Load(EOS, i7, i7, i334, i334) → f1050_0_fib_Return(EOS, i7, i7, i334, i332)

Combined rules. Obtained 5 IRules

P rules:
f930_0_fib_InvokeMethod(EOS, i7, i263, i274) → f932_1_fib_Load(EOS, i7, i263, i274, i274)
f66_0_fib_NE(EOS, x0, x0, x0) → f66_0_fib_NE(EOS, -(x0, 1), -(x0, 1), -(x0, 1)) | >(x0, 1)
f930_0_fib_InvokeMethod(EOS, x0, x1, x2) → f66_0_fib_NE(EOS, x2, x2, x2)
f66_0_fib_NE(EOS, 2, 2, 2) → f930_0_fib_InvokeMethod(EOS, 2, 1, 0)
f66_0_fib_NE(EOS, x0, x0, x0) → f930_0_fib_InvokeMethod(EOS, x0, x1, -(x0, 2)) | >(x0, 1)

Filtered ground terms:


f930_0_fib_InvokeMethod(x1, x2, x3, x4) → f930_0_fib_InvokeMethod(x2, x3, x4)
f932_1_fib_Load(x1, x2, x3, x4, x5) → f932_1_fib_Load(x2, x3, x4, x5)
f66_0_fib_NE(x1, x2, x3, x4) → f66_0_fib_NE(x2, x3, x4)
Cond_f66_0_fib_NE(x1, x2, x3, x4, x5) → Cond_f66_0_fib_NE(x1, x3, x4, x5)
Cond_f66_0_fib_NE1(x1, x2, x3, x4, x5, x6) → Cond_f66_0_fib_NE1(x1, x3, x4, x5, x6)

Filtered duplicate terms:


f932_1_fib_Load(x1, x2, x3, x4) → f932_1_fib_Load(x1, x2, x4)
f66_0_fib_NE(x1, x2, x3) → f66_0_fib_NE(x3)
Cond_f66_0_fib_NE(x1, x2, x3, x4) → Cond_f66_0_fib_NE(x1, x4)
Cond_f66_0_fib_NE1(x1, x2, x3, x4, x5) → Cond_f66_0_fib_NE1(x1, x4, x5)

Filtered unneeded terms:


Cond_f66_0_fib_NE1(x1, x2, x3) → Cond_f66_0_fib_NE1(x1, x2)
f930_0_fib_InvokeMethod(x1, x2, x3) → f930_0_fib_InvokeMethod(x3)

Prepared 5 rules for path length conversion:

P rules:
f930_0_fib_InvokeMethod(i274) → f932_1_fib_Load(i7, i263, i274)
f66_0_fib_NE(x0) → f66_0_fib_NE(-(x0, 1)) | >(x0, 1)
f930_0_fib_InvokeMethod(x2) → f66_0_fib_NE(x2)
f66_0_fib_NE(2) → f930_0_fib_InvokeMethod(0)
f66_0_fib_NE(x0) → f930_0_fib_InvokeMethod(-(x0, 2)) | >(x0, 1)

Finished conversion. Obtained 4 rules.

P rules:
f66_0_fib_NE(x3) → f66_0_fib_NE(-(x3, 1)) | >(x3, 1)
f930_0_fib_InvokeMethod(x4) → f66_0_fib_NE(x4)
f66_0_fib_NE(c2) → f930_0_fib_InvokeMethod(0) | =(2, c2)
f66_0_fib_NE(x5) → f930_0_fib_InvokeMethod(-(x5, 2)) | >(x5, 1)

(6) Obligation:

Rules:
f66_0_fib_NE(x3) → f66_0_fib_NE(-(x3, 1)) | >(x3, 1)
f930_0_fib_InvokeMethod(x4) → f66_0_fib_NE(x4)
f66_0_fib_NE(c2) → f930_0_fib_InvokeMethod(0) | =(2, c2)
f66_0_fib_NE(x5) → f930_0_fib_InvokeMethod(-(x5, 2)) | >(x5, 1)

(7) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:


[f66_0_fib_NE(x5)] = -1 + x5
[f930_0_fib_InvokeMethod(x8)] = -1 + x8

Therefore the following rule(s) have been dropped:


f66_0_fib_NE(x0) → f66_0_fib_NE(-(x0, 1)) | >(x0, 1)
f66_0_fib_NE(x2) → f930_0_fib_InvokeMethod(0) | =(2, x2)
f66_0_fib_NE(x3) → f930_0_fib_InvokeMethod(-(x3, 2)) | >(x3, 1)

(8) Obligation:

Rules:
f930_0_fib_InvokeMethod(x1) → f66_0_fib_NE(x1) | TRUE

(9) TerminationGraphProcessor (EQUIVALENT transformation)

Constructed the termination graph and obtained no non-trivial SCC(s).


(10) YES