Termination of the given JBC could be proven:

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

(0) Obligation:

JBC Problem based on JBC Program:
/**
 * The classical Ackermann function.
 *
 * All calls terminate.
 *
 * Julia + BinTerm prove that all calls terminate
 *
 * Note that we have to express the basic cases as m <= 0 and n <= 0
 * in order to prove termination.
 *
 * @author <A HREF="mailto:fausto.spoto@univr.it">Fausto Spoto</A>
 */

public class Ackermann {

    public static int ack(int m, int n) {
	if (m <= 0) return n + 1;
	else if (n <= 0) return ack(m - 1,1);
	else return ack(m - 1,ack(m,n - 1));
    }

    public static void main(String[] args) {
	ack(10,12);
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

Ackermann.ack(II)I: Graph of 55 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: Ackermann.ack(II)I
SCC calls the following helper methods: Ackermann.ack(II)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 41 IRules

P rules:
f362_0_ack_GT(EOS, i40, i38, i40, i38, i40) → f365_0_ack_GT(EOS, i40, i38, i40, i38, i40)
f365_0_ack_GT(EOS, i40, i38, i40, i38, i40) → f368_0_ack_Load(EOS, i40, i38, i40, i38) | >(i40, 0)
f368_0_ack_Load(EOS, i40, i38, i40, i38) → f372_0_ack_GT(EOS, i40, i38, i40, i38, i38)
f372_0_ack_GT(EOS, i40, i43, i40, i43, i43) → f376_0_ack_GT(EOS, i40, i43, i40, i43, i43)
f372_0_ack_GT(EOS, i40, i44, i40, i44, i44) → f377_0_ack_GT(EOS, i40, i44, i40, i44, i44)
f376_0_ack_GT(EOS, i40, i43, i40, i43, i43) → f380_0_ack_Load(EOS, i40, i43, i40, i43) | <=(i43, 0)
f380_0_ack_Load(EOS, i40, i43, i40, i43) → f387_0_ack_ConstantStackPush(EOS, i40, i43, i40, i43, i40)
f387_0_ack_ConstantStackPush(EOS, i40, i43, i40, i43, i40) → f407_0_ack_IntArithmetic(EOS, i40, i43, i40, i43, i40, 1)
f407_0_ack_IntArithmetic(EOS, i40, i43, i40, i43, i40, matching1) → f411_0_ack_ConstantStackPush(EOS, i40, i43, i40, i43, -(i40, 1)) | &&(>(i40, 0), =(matching1, 1))
f411_0_ack_ConstantStackPush(EOS, i40, i43, i40, i43, i48) → f414_0_ack_InvokeMethod(EOS, i40, i43, i40, i43, i48, 1)
f414_0_ack_InvokeMethod(EOS, i40, i43, i40, i43, i48, matching1) → f418_0_ack_Load(EOS, i48, 1, i48, 1) | =(matching1, 1)
f414_0_ack_InvokeMethod(EOS, i40, i43, i40, i43, i48, matching1) → f418_1_ack_Load(EOS, i40, i43, i40, i43, i48, 1, i48, 1) | =(matching1, 1)
f418_0_ack_Load(EOS, i48, matching1, i48, matching2) → f421_0_ack_Load(EOS, i48, 1, i48, 1) | &&(=(matching1, 1), =(matching2, 1))
f421_0_ack_Load(EOS, i48, matching1, i48, matching2) → f361_0_ack_Load(EOS, i48, 1, i48, 1) | &&(=(matching1, 1), =(matching2, 1))
f361_0_ack_Load(EOS, i37, i38, i37, i38) → f362_0_ack_GT(EOS, i37, i38, i37, i38, i37)
f377_0_ack_GT(EOS, i40, i44, i40, i44, i44) → f382_0_ack_Load(EOS, i40, i44, i40, i44) | >(i44, 0)
f382_0_ack_Load(EOS, i40, i44, i40, i44) → f388_0_ack_ConstantStackPush(EOS, i40, i44, i40, i44, i40)
f388_0_ack_ConstantStackPush(EOS, i40, i44, i40, i44, i40) → f410_0_ack_IntArithmetic(EOS, i40, i44, i40, i44, i40, 1)
f410_0_ack_IntArithmetic(EOS, i40, i44, i40, i44, i40, matching1) → f413_0_ack_Load(EOS, i40, i44, i40, i44, -(i40, 1)) | &&(>(i40, 0), =(matching1, 1))
f413_0_ack_Load(EOS, i40, i44, i40, i44, i49) → f416_0_ack_Load(EOS, i40, i44, i44, i49, i40)
f416_0_ack_Load(EOS, i40, i44, i44, i49, i40) → f419_0_ack_ConstantStackPush(EOS, i40, i44, i49, i40, i44)
f419_0_ack_ConstantStackPush(EOS, i40, i44, i49, i40, i44) → f423_0_ack_IntArithmetic(EOS, i40, i44, i49, i40, i44, 1)
f423_0_ack_IntArithmetic(EOS, i40, i44, i49, i40, i44, matching1) → f424_0_ack_InvokeMethod(EOS, i40, i44, i49, i40, -(i44, 1)) | &&(>(i44, 0), =(matching1, 1))
f424_0_ack_InvokeMethod(EOS, i40, i44, i49, i40, i50) → f434_0_ack_Load(EOS, i40, i50, i40, i50)
f424_0_ack_InvokeMethod(EOS, i40, i44, i49, i40, i50) → f434_1_ack_Load(EOS, i40, i44, i49, i40, i50, i40, i50)
f434_0_ack_Load(EOS, i40, i50, i40, i50) → f437_0_ack_Load(EOS, i40, i50, i40, i50)
f437_0_ack_Load(EOS, i40, i50, i40, i50) → f361_0_ack_Load(EOS, i40, i50, i40, i50)
f460_0_ack_Return(EOS, i65, i44, i49, i65, matching1, i65, matching2, i63) → f463_0_ack_InvokeMethod(EOS, i65, i44, i49, i63) | &&(=(matching1, 0), =(matching2, 0))
f463_0_ack_InvokeMethod(EOS, i65, i44, i49, i63) → f527_0_ack_InvokeMethod(EOS, i65, i44, i49, i63)
f527_0_ack_InvokeMethod(EOS, i102, i44, i49, i100) → f530_0_ack_Load(EOS, i49, i100, i49, i100)
f527_0_ack_InvokeMethod(EOS, i102, i44, i49, i100) → f530_1_ack_Load(EOS, i102, i44, i49, i100, i49, i100)
f530_0_ack_Load(EOS, i49, i100, i49, i100) → f547_0_ack_Load(EOS, i49, i100, i49, i100)
f547_0_ack_Load(EOS, i49, i100, i49, i100) → f361_0_ack_Load(EOS, i49, i100, i49, i100)
f553_0_ack_Return(EOS, i127, i44, i49, i127, matching1, i127, matching2, i125) → f460_0_ack_Return(EOS, i127, i44, i49, i127, 0, i127, 0, i125) | &&(=(matching1, 0), =(matching2, 0))
f623_0_ack_Return(EOS, i169, i44, i49, i169, i171, i167) → f519_0_ack_Return(EOS, i169, i44, i49, i169, i171, i167)
f519_0_ack_Return(EOS, i102, i44, i49, i102, i104, i100) → f527_0_ack_InvokeMethod(EOS, i102, i44, i49, i100)
f670_0_ack_Return(EOS, i198, i44, i49, i198, i200, i196) → f519_0_ack_Return(EOS, i198, i44, i49, i198, i200, i196)
f434_1_ack_Load(EOS, i65, i44, i49, i65, matching1, i65, matching2) → f460_0_ack_Return(EOS, i65, i44, i49, i65, 0, i65, 0, i63) | &&(=(matching1, 0), =(matching2, 0))
f434_1_ack_Load(EOS, i127, i44, i49, i127, matching1, i127, matching2) → f553_0_ack_Return(EOS, i127, i44, i49, i127, 0, i127, 0, i125) | &&(=(matching1, 0), =(matching2, 0))
f434_1_ack_Load(EOS, i169, i44, i49, i169, i171, i169, i171) → f623_0_ack_Return(EOS, i169, i44, i49, i169, i171, i167)
f434_1_ack_Load(EOS, i198, i44, i49, i198, i200, i198, i200) → f670_0_ack_Return(EOS, i198, i44, i49, i198, i200, i196)

Combined rules. Obtained 7 IRules

P rules:
f527_0_ack_InvokeMethod(EOS, i102, i44, i49, i100) → f530_1_ack_Load(EOS, i102, i44, i49, i100, i49, i100)
f362_0_ack_GT(EOS, x0, x1, x0, x1, x0) → f418_1_ack_Load(EOS, x0, x1, x0, x1, -(x0, 1), 1, -(x0, 1), 1) | &&(<=(x1, 0), >(x0, 0))
f362_0_ack_GT(EOS, x0, x1, x0, x1, x0) → f362_0_ack_GT(EOS, -(x0, 1), 1, -(x0, 1), 1, -(x0, 1)) | &&(<=(x1, 0), >(x0, 0))
f362_0_ack_GT(EOS, x0, x1, x0, x1, x0) → f362_0_ack_GT(EOS, x0, -(x1, 1), x0, -(x1, 1), x0) | &&(>(x1, 0), >(x0, 0))
f527_0_ack_InvokeMethod(EOS, x0, x1, x2, x3) → f362_0_ack_GT(EOS, x2, x3, x2, x3, x2)
f362_0_ack_GT(EOS, x0, 1, x0, 1, x0) → f527_0_ack_InvokeMethod(EOS, x0, 1, -(x0, 1), x2) | >(x0, 0)
f362_0_ack_GT(EOS, x0, x1, x0, x1, x0) → f527_0_ack_InvokeMethod(EOS, x0, x1, -(x0, 1), x2) | &&(>(x1, 0), >(x0, 0))

Filtered ground terms:


f527_0_ack_InvokeMethod(x1, x2, x3, x4, x5) → f527_0_ack_InvokeMethod(x2, x3, x4, x5)
f530_1_ack_Load(x1, x2, x3, x4, x5, x6, x7) → f530_1_ack_Load(x2, x3, x4, x5, x6, x7)
f362_0_ack_GT(x1, x2, x3, x4, x5, x6) → f362_0_ack_GT(x2, x3, x4, x5, x6)
Cond_f362_0_ack_GT(x1, x2, x3, x4, x5, x6, x7) → Cond_f362_0_ack_GT(x1, x3, x4, x5, x6, x7)
f418_1_ack_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → f418_1_ack_Load(x2, x3, x4, x5, x6, x8)
Cond_f362_0_ack_GT1(x1, x2, x3, x4, x5, x6, x7) → Cond_f362_0_ack_GT1(x1, x3, x4, x5, x6, x7)
Cond_f362_0_ack_GT2(x1, x2, x3, x4, x5, x6, x7) → Cond_f362_0_ack_GT2(x1, x3, x4, x5, x6, x7)
Cond_f362_0_ack_GT3(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f362_0_ack_GT3(x1, x3, x5, x7, x8)
Cond_f362_0_ack_GT4(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f362_0_ack_GT4(x1, x3, x4, x5, x6, x7, x8)

Filtered duplicate terms:


f530_1_ack_Load(x1, x2, x3, x4, x5, x6) → f530_1_ack_Load(x1, x2, x5, x6)
f362_0_ack_GT(x1, x2, x3, x4, x5) → f362_0_ack_GT(x4, x5)
Cond_f362_0_ack_GT(x1, x2, x3, x4, x5, x6) → Cond_f362_0_ack_GT(x1, x5, x6)
f418_1_ack_Load(x1, x2, x3, x4, x5, x6) → f418_1_ack_Load(x4, x6)
Cond_f362_0_ack_GT1(x1, x2, x3, x4, x5, x6) → Cond_f362_0_ack_GT1(x1, x5, x6)
Cond_f362_0_ack_GT2(x1, x2, x3, x4, x5, x6) → Cond_f362_0_ack_GT2(x1, x5, x6)
Cond_f362_0_ack_GT3(x1, x2, x3, x4, x5) → Cond_f362_0_ack_GT3(x1, x4, x5)
Cond_f362_0_ack_GT4(x1, x2, x3, x4, x5, x6, x7) → Cond_f362_0_ack_GT4(x1, x5, x6, x7)

Filtered unneeded terms:


Cond_f362_0_ack_GT(x1, x2, x3) → Cond_f362_0_ack_GT(x1)
Cond_f362_0_ack_GT1(x1, x2, x3) → Cond_f362_0_ack_GT1(x1, x3)
Cond_f362_0_ack_GT4(x1, x2, x3, x4) → Cond_f362_0_ack_GT4(x1, x3, x4)
f527_0_ack_InvokeMethod(x1, x2, x3, x4) → f527_0_ack_InvokeMethod(x3, x4)

Prepared 7 rules for path length conversion:

P rules:
f527_0_ack_InvokeMethod(i49, i100) → f530_1_ack_Load(i102, i44, i49, i100)
f362_0_ack_GT(x1, x0) → f418_1_ack_Load(x1, -(x0, 1)) | &&(<=(x1, 0), >(x0, 0))
f362_0_ack_GT(x1, x0) → f362_0_ack_GT(1, -(x0, 1)) | &&(<=(x1, 0), >(x0, 0))
f362_0_ack_GT(x1, x0) → f362_0_ack_GT(-(x1, 1), x0) | &&(>(x1, 0), >(x0, 0))
f527_0_ack_InvokeMethod(x2, x3) → f362_0_ack_GT(x3, x2)
f362_0_ack_GT(1, x0) → f527_0_ack_InvokeMethod(-(x0, 1), x2) | >(x0, 0)
f362_0_ack_GT(x1, x0) → f527_0_ack_InvokeMethod(-(x0, 1), x2) | &&(>(x1, 0), >(x0, 0))

Finished conversion. Obtained 5 rules.

P rules:
f362_0_ack_GT(x6, x7) → f362_0_ack_GT(1, -(x7, 1)) | &&(<=(x6, 0), >(x7, 0))
f362_0_ack_GT(x8, x9) → f362_0_ack_GT(-(x8, 1), x9) | &&(>(x8, 0), >(x9, 0))
f527_0_ack_InvokeMethod(x10, x11) → f362_0_ack_GT(x11, x10)
f362_0_ack_GT(c1, x12) → f527_0_ack_InvokeMethod(-(x12, 1), x13) | &&(>(x12, 0), =(1, c1))
f362_0_ack_GT(x14, x15) → f527_0_ack_InvokeMethod(-(x15, 1), x16) | &&(>(x14, 0), >(x15, 0))

(6) Obligation:

Rules:
f362_0_ack_GT(x6, x7) → f362_0_ack_GT(1, -(x7, 1)) | &&(<=(x6, 0), >(x7, 0))
f362_0_ack_GT(x8, x9) → f362_0_ack_GT(-(x8, 1), x9) | &&(>(x8, 0), >(x9, 0))
f527_0_ack_InvokeMethod(x10, x11) → f362_0_ack_GT(x11, x10)
f362_0_ack_GT(c1, x12) → f527_0_ack_InvokeMethod(-(x12, 1), x13) | &&(>(x12, 0), =(1, c1))
f362_0_ack_GT(x14, x15) → f527_0_ack_InvokeMethod(-(x15, 1), x16) | &&(>(x14, 0), >(x15, 0))

(7) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:


[f362_0_ack_GT(x13, x15)] = -1 + x15
[f527_0_ack_InvokeMethod(x18, x20)] = -1 + x18

Therefore the following rule(s) have been dropped:


f362_0_ack_GT(x0, x1) → f362_0_ack_GT(1, -(x1, 1)) | &&(<=(x0, 0), >(x1, 0))
f362_0_ack_GT(x6, x7) → f527_0_ack_InvokeMethod(-(x7, 1), x8) | &&(>(x7, 0), =(1, x6))
f362_0_ack_GT(x9, x10) → f527_0_ack_InvokeMethod(-(x10, 1), x11) | &&(>(x9, 0), >(x10, 0))

(8) Obligation:

Rules:
f362_0_ack_GT(x2, x3) → f362_0_ack_GT(-(x2, 1), x3) | &&(>(x2, 0), >(x3, 0))
f527_0_ack_InvokeMethod(x4, x5) → f362_0_ack_GT(x5, x4) | TRUE

(9) TerminationGraphProcessor (SOUND transformation)

Constructed the termination graph and obtained one non-trivial SCC.


(10) Obligation:

Rules:
f362_0_ack_GT(x0, x1) → f362_0_ack_GT(-(x0, 1), x1) | &&(>(x0, 0), >(x1, 0))

(11) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f362_0_ack_GT(x3, x5)] = x3

Therefore the following rule(s) have been dropped:


f362_0_ack_GT(x0, x1) → f362_0_ack_GT(-(x0, 1), x1) | &&(>(x0, 0), >(x1, 0))

(12) YES