Termination proof of /tmp/tmpeHFCoQ/Test2.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 3515 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 JBCTerminationSCC

↳5 SCCToIntTRSProof (⇒, 49 ms)

↳6 intTRS

↳7 LinearRankingProcessor (⇔, 0 ms)

↳8 YES

(0) Obligation:

JBC Problem based on JBC Program:

public class Test2 {
    public static void main(String[] args) {
	iter(args.length, args.length % 5, args.length % 4);
    }

    private static void iter(int x, int y, int z) {
	while (x + y + 3 * z >= 0) {
	    if (x > y)
		x--;
	    else if (y > z) {
		x++;
		y -= 2;
	    }
	    else if (y <= z) {
		x = add(x, 1);
		y = add(y, 1);
		z = z - 1;
	    }
	}
    }

    private static int add(int v, int w) {
	return v + w;
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Test2.main([Ljava/lang/String;)V: Graph of 106 nodes with 1 SCC.

(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: Test2.main([Ljava/lang/String;)V
SCC calls the following helper methods:
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 57 IRules

P rules:
f14208_0_iter_Load(EOS, i5500, i5501, i5502, i5500) → f14210_0_iter_IntArithmetic(EOS, i5500, i5501, i5502, i5500, i5501)
f14210_0_iter_IntArithmetic(EOS, i5500, i5501, i5502, i5500, i5501) → f14211_0_iter_ConstantStackPush(EOS, i5500, i5501, i5502, +(i5500, i5501))
f14211_0_iter_ConstantStackPush(EOS, i5500, i5501, i5502, i5508) → f14212_0_iter_Load(EOS, i5500, i5501, i5502, i5508, 3)
f14212_0_iter_Load(EOS, i5500, i5501, i5502, i5508, matching1) → f14213_0_iter_IntArithmetic(EOS, i5500, i5501, i5502, i5508, 3, i5502) | =(matching1, 3)
f14213_0_iter_IntArithmetic(EOS, i5500, i5501, i5502, i5508, matching1, i5502) → f14214_0_iter_IntArithmetic(EOS, i5500, i5501, i5502, i5508, *(3, i5502)) | =(matching1, 3)
f14214_0_iter_IntArithmetic(EOS, i5500, i5501, i5502, i5508, i5509) → f14216_0_iter_LT(EOS, i5500, i5501, i5502, +(i5508, i5509))
f14216_0_iter_LT(EOS, i5500, i5501, i5502, i5514) → f14218_0_iter_LT(EOS, i5500, i5501, i5502, i5514)
f14218_0_iter_LT(EOS, i5500, i5501, i5502, i5514) → f14223_0_iter_Load(EOS, i5500, i5501, i5502) | >=(i5514, 0)
f14223_0_iter_Load(EOS, i5500, i5501, i5502) → f14225_0_iter_Load(EOS, i5500, i5501, i5502, i5500)
f14225_0_iter_Load(EOS, i5500, i5501, i5502, i5500) → f14228_0_iter_LE(EOS, i5500, i5501, i5502, i5500, i5501)
f14228_0_iter_LE(EOS, i5500, i5501, i5502, i5500, i5501) → f14229_0_iter_LE(EOS, i5500, i5501, i5502, i5500, i5501)
f14228_0_iter_LE(EOS, i5500, i5501, i5502, i5500, i5501) → f14230_0_iter_LE(EOS, i5500, i5501, i5502, i5500, i5501)
f14229_0_iter_LE(EOS, i5500, i5501, i5502, i5500, i5501) → f14232_0_iter_Load(EOS, i5500, i5501, i5502) | <=(i5500, i5501)
f14232_0_iter_Load(EOS, i5500, i5501, i5502) → f14234_0_iter_Load(EOS, i5500, i5501, i5502, i5501)
f14234_0_iter_Load(EOS, i5500, i5501, i5502, i5501) → f14237_0_iter_LE(EOS, i5500, i5501, i5502, i5501, i5502)
f14237_0_iter_LE(EOS, i5500, i5501, i5502, i5501, i5502) → f14240_0_iter_LE(EOS, i5500, i5501, i5502, i5501, i5502)
f14237_0_iter_LE(EOS, i5500, i5501, i5502, i5501, i5502) → f14241_0_iter_LE(EOS, i5500, i5501, i5502, i5501, i5502)
f14240_0_iter_LE(EOS, i5500, i5501, i5502, i5501, i5502) → f14398_0_iter_Load(EOS, i5500, i5501, i5502) | <=(i5501, i5502)
f14398_0_iter_Load(EOS, i5500, i5501, i5502) → f14400_0_iter_Load(EOS, i5500, i5501, i5502, i5501)
f14400_0_iter_Load(EOS, i5500, i5501, i5502, i5501) → f14402_0_iter_GT(EOS, i5500, i5501, i5502, i5501, i5502)
f14402_0_iter_GT(EOS, i5500, i5501, i5502, i5501, i5502) → f14404_0_iter_GT(EOS, i5500, i5501, i5502, i5501, i5502)
f14402_0_iter_GT(EOS, i5500, i5501, i5502, i5501, i5502) → f14405_0_iter_GT(EOS, i5500, i5501, i5502, i5501, i5502)
f14404_0_iter_GT(EOS, i5500, i5501, i5502, i5501, i5502) → f14412_0_iter_Load(EOS, i5500, i5501, i5502) | >(i5501, i5502)
f14412_0_iter_Load(EOS, i5500, i5501, i5502) → f14206_0_iter_Load(EOS, i5500, i5501, i5502)
f14206_0_iter_Load(EOS, i5500, i5501, i5502) → f14208_0_iter_Load(EOS, i5500, i5501, i5502, i5500)
f14405_0_iter_GT(EOS, i5500, i5501, i5502, i5501, i5502) → f14413_0_iter_Load(EOS, i5500, i5501, i5502) | <=(i5501, i5502)
f14413_0_iter_Load(EOS, i5500, i5501, i5502) → f16735_0_iter_ConstantStackPush(EOS, i5501, i5502, i5500)
f16735_0_iter_ConstantStackPush(EOS, i5501, i5502, i5500) → f16736_0_iter_InvokeMethod(EOS, i5501, i5502, i5500, 1)
f16736_0_iter_InvokeMethod(EOS, i5501, i5502, i5500, matching1) → f16738_0_add_Load(EOS, i5501, i5502, i5500, 1, i5500, 1) | =(matching1, 1)
f16738_0_add_Load(EOS, i5501, i5502, i5500, matching1, i5500, matching2) → f16739_0_add_Load(EOS, i5501, i5502, i5500, 1, 1, i5500) | &&(=(matching1, 1), =(matching2, 1))
f16739_0_add_Load(EOS, i5501, i5502, i5500, matching1, matching2, i5500) → f16740_0_add_IntArithmetic(EOS, i5501, i5502, i5500, 1, i5500, 1) | &&(=(matching1, 1), =(matching2, 1))
f16740_0_add_IntArithmetic(EOS, i5501, i5502, i5500, matching1, i5500, matching2) → f16741_0_add_Return(EOS, i5501, i5502, i5500, 1, +(i5500, 1)) | &&(=(matching1, 1), =(matching2, 1))
f16741_0_add_Return(EOS, i5501, i5502, i5500, matching1, i6506) → f16743_0_iter_Store(EOS, i5501, i5502, i6506) | =(matching1, 1)
f16743_0_iter_Store(EOS, i5501, i5502, i6506) → f16744_0_iter_Load(EOS, i6506, i5501, i5502)
f16744_0_iter_Load(EOS, i6506, i5501, i5502) → f16745_0_iter_ConstantStackPush(EOS, i6506, i5502, i5501)
f16745_0_iter_ConstantStackPush(EOS, i6506, i5502, i5501) → f16746_0_iter_InvokeMethod(EOS, i6506, i5502, i5501, 1)
f16746_0_iter_InvokeMethod(EOS, i6506, i5502, i5501, matching1) → f16747_0_add_Load(EOS, i6506, i5502, i5501, 1, i5501, 1) | =(matching1, 1)
f16747_0_add_Load(EOS, i6506, i5502, i5501, matching1, i5501, matching2) → f16751_0_add_Load(EOS, i6506, i5502, i5501, 1, 1, i5501) | &&(=(matching1, 1), =(matching2, 1))
f16751_0_add_Load(EOS, i6506, i5502, i5501, matching1, matching2, i5501) → f16752_0_add_IntArithmetic(EOS, i6506, i5502, i5501, 1, i5501, 1) | &&(=(matching1, 1), =(matching2, 1))
f16752_0_add_IntArithmetic(EOS, i6506, i5502, i5501, matching1, i5501, matching2) → f16755_0_add_Return(EOS, i6506, i5502, i5501, 1, +(i5501, 1)) | &&(=(matching1, 1), =(matching2, 1))
f16755_0_add_Return(EOS, i6506, i5502, i5501, matching1, i6511) → f16756_0_iter_Store(EOS, i6506, i5502, i6511) | =(matching1, 1)
f16756_0_iter_Store(EOS, i6506, i5502, i6511) → f16757_0_iter_Load(EOS, i6506, i6511, i5502)
f16757_0_iter_Load(EOS, i6506, i6511, i5502) → f16758_0_iter_ConstantStackPush(EOS, i6506, i6511, i5502)
f16758_0_iter_ConstantStackPush(EOS, i6506, i6511, i5502) → f16760_0_iter_IntArithmetic(EOS, i6506, i6511, i5502, 1)
f16760_0_iter_IntArithmetic(EOS, i6506, i6511, i5502, matching1) → f16761_0_iter_Store(EOS, i6506, i6511, -(i5502, 1)) | =(matching1, 1)
f16761_0_iter_Store(EOS, i6506, i6511, i6514) → f16762_0_iter_JMP(EOS, i6506, i6511, i6514)
f16762_0_iter_JMP(EOS, i6506, i6511, i6514) → f16766_0_iter_Load(EOS, i6506, i6511, i6514)
f16766_0_iter_Load(EOS, i6506, i6511, i6514) → f14206_0_iter_Load(EOS, i6506, i6511, i6514)
f14241_0_iter_LE(EOS, i5500, i5501, i5502, i5501, i5502) → f14399_0_iter_Inc(EOS, i5500, i5501, i5502) | >(i5501, i5502)
f14399_0_iter_Inc(EOS, i5500, i5501, i5502) → f14401_0_iter_Inc(EOS, +(i5500, 1), i5501, i5502)
f14401_0_iter_Inc(EOS, i5702, i5501, i5502) → f14403_0_iter_JMP(EOS, i5702, +(i5501, -2), i5502)
f14403_0_iter_JMP(EOS, i5702, i5703, i5502) → f14408_0_iter_Load(EOS, i5702, i5703, i5502)
f14408_0_iter_Load(EOS, i5702, i5703, i5502) → f14206_0_iter_Load(EOS, i5702, i5703, i5502)
f14230_0_iter_LE(EOS, i5500, i5501, i5502, i5500, i5501) → f14233_0_iter_Inc(EOS, i5500, i5501, i5502) | >(i5500, i5501)
f14233_0_iter_Inc(EOS, i5500, i5501, i5502) → f14235_0_iter_JMP(EOS, +(i5500, -1), i5501, i5502)
f14235_0_iter_JMP(EOS, i5515, i5501, i5502) → f14239_0_iter_Load(EOS, i5515, i5501, i5502)
f14239_0_iter_Load(EOS, i5515, i5501, i5502) → f14206_0_iter_Load(EOS, i5515, i5501, i5502)

Combined rules. Obtained 3 IRules

P rules:
f14208_0_iter_Load(EOS, x0, x1, x2, x0) → f14208_0_iter_Load(EOS, +(x0, 1), +(x1, 1), -(x2, 1), +(x0, 1)) | &&(&&(>=(x2, x1), >=(+(+(x0, x1), *(3, x2)), 0)), >=(x1, x0))
f14208_0_iter_Load(EOS, x0, x1, x2, x0) → f14208_0_iter_Load(EOS, +(x0, 1), -(x1, 2), x2, +(x0, 1)) | &&(&&(<(x2, x1), >=(+(+(x0, x1), *(3, x2)), 0)), >=(x1, x0))
f14208_0_iter_Load(EOS, x0, x1, x2, x0) → f14208_0_iter_Load(EOS, -(x0, 1), x1, x2, -(x0, 1)) | &&(>=(+(+(x0, x1), *(3, x2)), 0), <(x1, x0))

Filtered ground terms:

f14208_0_iter_Load(x1, x2, x3, x4, x5) → f14208_0_iter_Load(x2, x3, x4, x5)
Cond_f14208_0_iter_Load(x1, x2, x3, x4, x5, x6) → Cond_f14208_0_iter_Load(x1, x3, x4, x5, x6)
Cond_f14208_0_iter_Load1(x1, x2, x3, x4, x5, x6) → Cond_f14208_0_iter_Load1(x1, x3, x4, x5, x6)
Cond_f14208_0_iter_Load2(x1, x2, x3, x4, x5, x6) → Cond_f14208_0_iter_Load2(x1, x3, x4, x5, x6)

Filtered duplicate terms:

f14208_0_iter_Load(x1, x2, x3, x4) → f14208_0_iter_Load(x2, x3, x4)
Cond_f14208_0_iter_Load(x1, x2, x3, x4, x5) → Cond_f14208_0_iter_Load(x1, x3, x4, x5)
Cond_f14208_0_iter_Load1(x1, x2, x3, x4, x5) → Cond_f14208_0_iter_Load1(x1, x3, x4, x5)
Cond_f14208_0_iter_Load2(x1, x2, x3, x4, x5) → Cond_f14208_0_iter_Load2(x1, x3, x4, x5)

Prepared 3 rules for path length conversion:

P rules:
f14208_0_iter_Load(x1, x2, x0) → f14208_0_iter_Load(+(x1, 1), -(x2, 1), +(x0, 1)) | &&(&&(>=(x2, x1), >=(+(+(x0, x1), *(3, x2)), 0)), >=(x1, x0))
f14208_0_iter_Load(x1, x2, x0) → f14208_0_iter_Load(-(x1, 2), x2, +(x0, 1)) | &&(&&(<(x2, x1), >=(+(+(x0, x1), *(3, x2)), 0)), >=(x1, x0))
f14208_0_iter_Load(x1, x2, x0) → f14208_0_iter_Load(x1, x2, -(x0, 1)) | &&(>=(+(+(x0, x1), *(3, x2)), 0), <(x1, x0))

Finished conversion. Obtained 3 rules.

P rules:
f14208_0_iter_Load(x0, x1, x2) → f14208_0_iter_Load(+(x0, 1), -(x1, 1), +(x2, 1)) | &&(&&(<=(x2, x0), >=(x1, x0)), >=(+(+(x2, x0), *(3, x1)), 0))
f14208_0_iter_Load(x3, x4, x5) → f14208_0_iter_Load(-(x3, 2), x4, +(x5, 1)) | &&(&&(<=(x5, x3), <(x4, x3)), >=(+(+(x5, x3), *(3, x4)), 0))
f14208_0_iter_Load(x6, x7, x8) → f14208_0_iter_Load(x6, x7, -(x8, 1)) | &&(>=(+(+(x8, x6), *(3, x7)), 0), >(x8, x6))

(6) Obligation:

Rules:
f14208_0_iter_Load(x0, x1, x2) → f14208_0_iter_Load(+(x0, 1), -(x1, 1), +(x2, 1)) | &&(&&(<=(x2, x0), >=(x1, x0)), >=(+(+(x2, x0), *(3, x1)), 0))
f14208_0_iter_Load(x3, x4, x5) → f14208_0_iter_Load(-(x3, 2), x4, +(x5, 1)) | &&(&&(<=(x5, x3), <(x4, x3)), >=(+(+(x5, x3), *(3, x4)), 0))
f14208_0_iter_Load(x6, x7, x8) → f14208_0_iter_Load(x6, x7, -(x8, 1)) | &&(>=(+(+(x8, x6), *(3, x7)), 0), >(x8, x6))

(7) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:

[f14208_0_iter_Load(x)] = 1·x₁ + 3·x₂ + 1·x₃

where x = (x₁, ... ,x_n).

Therefore the following rule(s) have been dropped:

f14208_0_iter_Load(x0, x1, x2) → f14208_0_iter_Load(+(x0, 1), -(x1, 1), +(x2, 1)) | &&(&&(<=(x2, x0), >=(x1, x0)), >=(+(+(x2, x0), *(3, x1)), 0))
f14208_0_iter_Load(x3, x4, x5) → f14208_0_iter_Load(-(x3, 2), x4, +(x5, 1)) | &&(&&(<=(x5, x3), <(x4, x3)), >=(+(+(x5, x3), *(3, x4)), 0))
f14208_0_iter_Load(x6, x7, x8) → f14208_0_iter_Load(x6, x7, -(x8, 1)) | &&(>=(+(+(x8, x6), *(3, x7)), 0), >(x8, x6))