Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 209 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 AND
    ↳5 JBCTerminationSCC
        ↳6 SCCToIntTRSProof (⇒, 52 ms)
        ↳7 intTRS
        ↳8 PolynomialOrderProcessor (⇔, 0 ms)
        ↳9 YES
    ↳10 JBCTerminationSCC
        ↳11 SCCToIntTRSProof (⇒, 140 ms)
        ↳12 intTRS
        ↳13 PolynomialOrderProcessor (⇒, 0 ms)
        ↳14 intTRS
        ↳15 PolynomialOrderProcessor (⇔, 0 ms)
        ↳16 YES

(0) Obligation:

JBC Problem based on JBC Program:
public class Test10 {
    public static void main(String[] args) {
	rec(args.length);
    }

    private static void rec(long l) {
	if (l > 0) {
	    for (int i = (int) l ; i < 100; i++)
		test(i);

	    rec (l - 1);
	}
    }

    private static void test(int i) {
	descend(i);
	descend(i);
	descend(i);
	descend(i);
	descend(i);
	descend(i);
	descend(i);
	descend(i);
    }

    private static void descend(int i) {
	if (i > 0)
	    descend(i - 1);
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

Test10.rec(J)V: Graph of 75 nodes with 1 SCC.

Test10.descend(I)V: Graph of 17 nodes with 0 SCCs.


(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 2 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test10.descend(I)V
SCC calls the following helper methods: Test10.descend(I)V
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
  • Marker field analysis yielded the following relations that could be markers:

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 10 IRules

P rules:
f310_0_descend_LE(EOS, i66, i66, i66) → f320_0_descend_LE(EOS, i66, i66, i66)
f320_0_descend_LE(EOS, i66, i66, i66) → f324_0_descend_Load(EOS, i66, i66) | >(i66, 0)
f324_0_descend_Load(EOS, i66, i66) → f327_0_descend_ConstantStackPush(EOS, i66, i66)
f327_0_descend_ConstantStackPush(EOS, i66, i66) → f338_0_descend_IntArithmetic(EOS, i66, i66, 1)
f338_0_descend_IntArithmetic(EOS, i66, i66, matching1) → f342_0_descend_InvokeMethod(EOS, i66, -(i66, 1)) | &&(>(i66, 0), =(matching1, 1))
f342_0_descend_InvokeMethod(EOS, i66, i68) → f344_0_descend_Load(EOS, i68, i68)
f342_0_descend_InvokeMethod(EOS, i66, i68) → f344_1_descend_Load(EOS, i66, i68, i68)
f344_0_descend_Load(EOS, i68, i68) → f347_0_descend_Load(EOS, i68, i68)
f347_0_descend_Load(EOS, i68, i68) → f292_0_descend_Load(EOS, i68, i68)
f292_0_descend_Load(EOS, i55, i55) → f310_0_descend_LE(EOS, i55, i55, i55)

Combined rules. Obtained 2 IRules

P rules:
f310_0_descend_LE(EOS, x0, x0, x0) → f344_1_descend_Load(EOS, x0, -(x0, 1), -(x0, 1)) | >(x0, 0)
f310_0_descend_LE(EOS, x0, x0, x0) → f310_0_descend_LE(EOS, -(x0, 1), -(x0, 1), -(x0, 1)) | >(x0, 0)

Filtered ground terms:


f310_0_descend_LE(x1, x2, x3, x4) → f310_0_descend_LE(x2, x3, x4)
Cond_f310_0_descend_LE(x1, x2, x3, x4, x5) → Cond_f310_0_descend_LE(x1, x3, x4, x5)
f344_1_descend_Load(x1, x2, x3, x4) → f344_1_descend_Load(x2, x3, x4)
Cond_f310_0_descend_LE1(x1, x2, x3, x4, x5) → Cond_f310_0_descend_LE1(x1, x3, x4, x5)

Filtered duplicate terms:


f310_0_descend_LE(x1, x2, x3) → f310_0_descend_LE(x3)
Cond_f310_0_descend_LE(x1, x2, x3, x4) → Cond_f310_0_descend_LE(x1, x4)
f344_1_descend_Load(x1, x2, x3) → f344_1_descend_Load(x3)
Cond_f310_0_descend_LE1(x1, x2, x3, x4) → Cond_f310_0_descend_LE1(x1, x4)

Filtered unneeded terms:


Cond_f310_0_descend_LE(x1, x2) → Cond_f310_0_descend_LE(x1)

Prepared 2 rules for path length conversion:

P rules:
f310_0_descend_LE(x0) → f344_1_descend_Load(-(x0, 1)) | >(x0, 0)
f310_0_descend_LE(x0) → f310_0_descend_LE(-(x0, 1)) | >(x0, 0)

Finished conversion. Obtained 1 rules.

P rules:
f310_0_descend_LE(x1) → f310_0_descend_LE(-(x1, 1)) | >(x1, 0)

(7) Obligation:

Rules:
f310_0_descend_LE(x1) → f310_0_descend_LE(-(x1, 1)) | >(x1, 0)

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f310_0_descend_LE(x2)] = x2

Therefore the following rule(s) have been dropped:


f310_0_descend_LE(x0) → f310_0_descend_LE(-(x0, 1)) | >(x0, 0)

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test10.rec(J)V
SCC calls the following helper methods: Test10.descend(I)V, Test10.rec(J)V
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
  • Marker field analysis yielded the following relations that could be markers:

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 76 IRules

P rules:
f67_0_rec_ConstantStackPush(EOS, i2, i2, i2) → f70_0_rec_Cmp(EOS, i2, i2, i2, 0)
f70_0_rec_Cmp(EOS, i6, i6, i6, matching1) → f74_0_rec_Cmp(EOS, i6, i6, i6, 0) | =(matching1, 0)
f74_0_rec_Cmp(EOS, i6, i6, i6, matching1) → f81_0_rec_LE(EOS, i6, i6, 1) | &&(>(i6, 0), =(matching1, 0))
f81_0_rec_LE(EOS, i6, i6, matching1) → f85_0_rec_Load(EOS, i6, i6) | &&(>(1, 0), =(matching1, 1))
f85_0_rec_Load(EOS, i6, i6) → f89_0_rec_TypeCast(EOS, i6, i6, i6)
f89_0_rec_TypeCast(EOS, i6, i6, i6) → f117_0_rec_Store(EOS, i6, i6, i14) | =(i14, i6)
f117_0_rec_Store(EOS, i6, i6, i14) → f120_0_rec_Load(EOS, i6, i6, i14)
f120_0_rec_Load(EOS, i6, i6, i14) → f122_0_rec_ConstantStackPush(EOS, i6, i6, i14, i14)
f122_0_rec_ConstantStackPush(EOS, i6, i6, i14, i14) → f128_0_rec_GE(EOS, i6, i6, i14, i14, 100)
f128_0_rec_GE(EOS, i6, i6, i18, i18, matching1) → f130_0_rec_GE(EOS, i6, i6, i18, i18, 100) | =(matching1, 100)
f128_0_rec_GE(EOS, i6, i6, i19, i19, matching1) → f131_0_rec_GE(EOS, i6, i6, i19, i19, 100) | =(matching1, 100)
f130_0_rec_GE(EOS, i6, i6, i18, i18, matching1) → f134_0_rec_Load(EOS, i6, i6, i18) | &&(<(i18, 100), =(matching1, 100))
f134_0_rec_Load(EOS, i6, i6, i18) → f138_0_rec_InvokeMethod(EOS, i6, i6, i18, i18)
f138_0_rec_InvokeMethod(EOS, i6, i6, i18, i18) → f142_0_test_Load(EOS, i6, i6, i18, i18, i18)
f142_0_test_Load(EOS, i6, i6, i18, i18, i18) → f148_0_test_InvokeMethod(EOS, i6, i6, i18, i18, i18, i18)
f148_0_test_InvokeMethod(EOS, i6, i6, i18, i18, i18, i18) → f152_0_descend_Load(EOS, i18, i18)
f148_0_test_InvokeMethod(EOS, i6, i6, i18, i18, i18, i18) → f152_1_descend_Load(EOS, i6, i6, i18, i18, i18, i18, i18)
f152_0_descend_Load(EOS, i18, i18) → f157_0_descend_Load(EOS, i18, i18)
f438_0_descend_Return(EOS, i6, i6, i89, i89, i89, i89) → f387_0_descend_Return(EOS, i6, i6, i89, i89, i89, i89)
f387_0_descend_Return(EOS, i6, i6, i76, i76, i76, i76) → f399_0_test_Load(EOS, i6, i6, i76, i76, i76)
f399_0_test_Load(EOS, i6, i6, i76, i76, i76) → f405_0_test_InvokeMethod(EOS, i6, i6, i76, i76, i76, i76)
f405_0_test_InvokeMethod(EOS, i6, i6, i76, i76, i76, i76) → f408_0_descend_Load(EOS, i76, i76)
f405_0_test_InvokeMethod(EOS, i6, i6, i76, i76, i76, i76) → f408_1_descend_Load(EOS, i6, i6, i76, i76, i76, i76, i76)
f408_0_descend_Load(EOS, i76, i76) → f420_0_descend_Load(EOS, i76, i76)
f470_0_descend_Return(EOS, i6, i6, i104, i104, i104, i104) → f473_0_test_Load(EOS, i6, i6, i104, i104, i104)
f473_0_test_Load(EOS, i6, i6, i104, i104, i104) → f475_0_test_InvokeMethod(EOS, i6, i6, i104, i104, i104, i104)
f475_0_test_InvokeMethod(EOS, i6, i6, i104, i104, i104, i104) → f477_0_descend_Load(EOS, i104, i104)
f475_0_test_InvokeMethod(EOS, i6, i6, i104, i104, i104, i104) → f477_1_descend_Load(EOS, i6, i6, i104, i104, i104, i104, i104)
f477_0_descend_Load(EOS, i104, i104) → f479_0_descend_Load(EOS, i104, i104)
f508_0_descend_Return(EOS, i6, i6, i112, i112, i112, i112) → f510_0_test_Load(EOS, i6, i6, i112, i112, i112)
f510_0_test_Load(EOS, i6, i6, i112, i112, i112) → f513_0_test_InvokeMethod(EOS, i6, i6, i112, i112, i112, i112)
f513_0_test_InvokeMethod(EOS, i6, i6, i112, i112, i112, i112) → f515_0_descend_Load(EOS, i112, i112)
f513_0_test_InvokeMethod(EOS, i6, i6, i112, i112, i112, i112) → f515_1_descend_Load(EOS, i6, i6, i112, i112, i112, i112, i112)
f515_0_descend_Load(EOS, i112, i112) → f517_0_descend_Load(EOS, i112, i112)
f546_0_descend_Return(EOS, i6, i6, i121, i121, i121, i121) → f548_0_test_Load(EOS, i6, i6, i121, i121, i121)
f548_0_test_Load(EOS, i6, i6, i121, i121, i121) → f550_0_test_InvokeMethod(EOS, i6, i6, i121, i121, i121, i121)
f550_0_test_InvokeMethod(EOS, i6, i6, i121, i121, i121, i121) → f552_0_descend_Load(EOS, i121, i121)
f550_0_test_InvokeMethod(EOS, i6, i6, i121, i121, i121, i121) → f552_1_descend_Load(EOS, i6, i6, i121, i121, i121, i121, i121)
f552_0_descend_Load(EOS, i121, i121) → f555_0_descend_Load(EOS, i121, i121)
f584_0_descend_Return(EOS, i6, i6, i131, i131, i131, i131) → f587_0_test_Load(EOS, i6, i6, i131, i131, i131)
f587_0_test_Load(EOS, i6, i6, i131, i131, i131) → f589_0_test_InvokeMethod(EOS, i6, i6, i131, i131, i131, i131)
f589_0_test_InvokeMethod(EOS, i6, i6, i131, i131, i131, i131) → f591_0_descend_Load(EOS, i131, i131)
f589_0_test_InvokeMethod(EOS, i6, i6, i131, i131, i131, i131) → f591_1_descend_Load(EOS, i6, i6, i131, i131, i131, i131, i131)
f591_0_descend_Load(EOS, i131, i131) → f594_0_descend_Load(EOS, i131, i131)
f612_0_descend_Return(EOS, i6, i6, i139, i139, i139, i139) → f614_0_test_Load(EOS, i6, i6, i139, i139, i139)
f614_0_test_Load(EOS, i6, i6, i139, i139, i139) → f615_0_test_InvokeMethod(EOS, i6, i6, i139, i139, i139, i139)
f615_0_test_InvokeMethod(EOS, i6, i6, i139, i139, i139, i139) → f618_0_descend_Load(EOS, i139, i139)
f615_0_test_InvokeMethod(EOS, i6, i6, i139, i139, i139, i139) → f618_1_descend_Load(EOS, i6, i6, i139, i139, i139, i139, i139)
f618_0_descend_Load(EOS, i139, i139) → f620_0_descend_Load(EOS, i139, i139)
f639_0_descend_Return(EOS, i6, i6, i147, i147, i147, i147) → f641_0_test_Load(EOS, i6, i6, i147, i147, i147)
f641_0_test_Load(EOS, i6, i6, i147, i147, i147) → f643_0_test_InvokeMethod(EOS, i6, i6, i147, i147, i147)
f643_0_test_InvokeMethod(EOS, i6, i6, i147, i147, i147) → f644_0_descend_Load(EOS, i147, i147)
f643_0_test_InvokeMethod(EOS, i6, i6, i147, i147, i147) → f644_1_descend_Load(EOS, i6, i6, i147, i147, i147, i147)
f644_0_descend_Load(EOS, i147, i147) → f646_0_descend_Load(EOS, i147, i147)
f659_0_descend_Return(EOS, i6, i6, i152, i152, i152) → f660_0_test_Return(EOS, i6, i6, i152, i152)
f660_0_test_Return(EOS, i6, i6, i152, i152) → f662_0_rec_Inc(EOS, i6, i6, i152)
f662_0_rec_Inc(EOS, i6, i6, i152) → f664_0_rec_JMP(EOS, i6, i6, +(i152, 1)) | >(i152, 0)
f664_0_rec_JMP(EOS, i6, i6, i153) → f667_0_rec_Load(EOS, i6, i6, i153)
f667_0_rec_Load(EOS, i6, i6, i153) → f120_0_rec_Load(EOS, i6, i6, i153)
f131_0_rec_GE(EOS, i6, i6, i19, i19, matching1) → f136_0_rec_Load(EOS, i6, i6) | &&(>=(i19, 100), =(matching1, 100))
f136_0_rec_Load(EOS, i6, i6) → f140_0_rec_ConstantStackPush(EOS, i6, i6)
f140_0_rec_ConstantStackPush(EOS, i6, i6) → f144_0_rec_IntArithmetic(EOS, i6, i6, 1)
f144_0_rec_IntArithmetic(EOS, i6, i6, matching1) → f146_0_rec_InvokeMethod(EOS, i6, -(i6, 1)) | &&(>(i6, 0), =(matching1, 1))
f146_0_rec_InvokeMethod(EOS, i6, i22) → f150_0_rec_Load(EOS, i22, i22)
f146_0_rec_InvokeMethod(EOS, i6, i22) → f150_1_rec_Load(EOS, i6, i22, i22)
f150_0_rec_Load(EOS, i22, i22) → f154_0_rec_Load(EOS, i22, i22)
f154_0_rec_Load(EOS, i22, i22) → f64_0_rec_Load(EOS, i22, i22)
f64_0_rec_Load(EOS, i2, i2) → f67_0_rec_ConstantStackPush(EOS, i2, i2, i2)
f152_1_descend_Load(EOS, i6, i6, i89, i89, i89, i89, i89) → f438_0_descend_Return(EOS, i6, i6, i89, i89, i89, i89)
f408_1_descend_Load(EOS, i6, i6, i104, i104, i104, i104, i104) → f470_0_descend_Return(EOS, i6, i6, i104, i104, i104, i104)
f477_1_descend_Load(EOS, i6, i6, i112, i112, i112, i112, i112) → f508_0_descend_Return(EOS, i6, i6, i112, i112, i112, i112)
f515_1_descend_Load(EOS, i6, i6, i121, i121, i121, i121, i121) → f546_0_descend_Return(EOS, i6, i6, i121, i121, i121, i121)
f552_1_descend_Load(EOS, i6, i6, i131, i131, i131, i131, i131) → f584_0_descend_Return(EOS, i6, i6, i131, i131, i131, i131)
f591_1_descend_Load(EOS, i6, i6, i139, i139, i139, i139, i139) → f612_0_descend_Return(EOS, i6, i6, i139, i139, i139, i139)
f618_1_descend_Load(EOS, i6, i6, i147, i147, i147, i147, i147) → f639_0_descend_Return(EOS, i6, i6, i147, i147, i147, i147)
f644_1_descend_Load(EOS, i6, i6, i152, i152, i152, i152) → f659_0_descend_Return(EOS, i6, i6, i152, i152, i152)

Combined rules. Obtained 11 IRules

P rules:
f128_0_rec_GE(EOS, x0, x0, x1, x1, 100) → f157_0_descend_Load(EOS, x1, x1) | <(x1, 100)
f128_0_rec_GE(EOS, x0, x0, x1, x1, 100) → f150_1_rec_Load(EOS, x0, -(x0, 1), -(x0, 1)) | &&(>(x0, 0), >(+(x1, 1), 100))
f128_0_rec_GE(EOS, x0, x0, x1, x1, 100) → f128_0_rec_GE(EOS, -(x0, 1), -(x0, 1), -(x0, 1), -(x0, 1), 100) | &&(>(x0, 1), >(+(x1, 1), 100))
f128_0_rec_GE(EOS, x0, x0, x1, x1, 100) → f420_0_descend_Load(EOS, x1, x1) | <(x1, 100)
f128_0_rec_GE(EOS, x0, x0, x1, x1, 100) → f479_0_descend_Load(EOS, x1, x1) | <(x1, 100)
f128_0_rec_GE(EOS, x0, x0, x1, x1, 100) → f517_0_descend_Load(EOS, x1, x1) | <(x1, 100)
f128_0_rec_GE(EOS, x0, x0, x1, x1, 100) → f555_0_descend_Load(EOS, x1, x1) | <(x1, 100)
f128_0_rec_GE(EOS, x0, x0, x1, x1, 100) → f594_0_descend_Load(EOS, x1, x1) | <(x1, 100)
f128_0_rec_GE(EOS, x0, x0, x1, x1, 100) → f620_0_descend_Load(EOS, x1, x1) | <(x1, 100)
f128_0_rec_GE(EOS, x0, x0, x1, x1, 100) → f646_0_descend_Load(EOS, x1, x1) | <(x1, 100)
f128_0_rec_GE(EOS, x0, x0, x1, x1, 100) → f128_0_rec_GE(EOS, x0, x0, +(x1, 1), +(x1, 1), 100) | &&(<(x1, 100), >(x1, 0))

Filtered ground terms:


f128_0_rec_GE(x1, x2, x3, x4, x5, x6) → f128_0_rec_GE(x2, x3, x4, x5)
Cond_f128_0_rec_GE(x1, x2, x3, x4, x5, x6, x7) → Cond_f128_0_rec_GE(x1, x3, x4, x5, x6)
f157_0_descend_Load(x1, x2, x3) → f157_0_descend_Load(x2, x3)
Cond_f128_0_rec_GE1(x1, x2, x3, x4, x5, x6, x7) → Cond_f128_0_rec_GE1(x1, x3, x4, x5, x6)
f150_1_rec_Load(x1, x2, x3, x4) → f150_1_rec_Load(x2, x3, x4)
Cond_f128_0_rec_GE2(x1, x2, x3, x4, x5, x6, x7) → Cond_f128_0_rec_GE2(x1, x3, x4, x5, x6)
Cond_f128_0_rec_GE3(x1, x2, x3, x4, x5, x6, x7) → Cond_f128_0_rec_GE3(x1, x3, x4, x5, x6)
f420_0_descend_Load(x1, x2, x3) → f420_0_descend_Load(x2, x3)
Cond_f128_0_rec_GE4(x1, x2, x3, x4, x5, x6, x7) → Cond_f128_0_rec_GE4(x1, x3, x4, x5, x6)
f479_0_descend_Load(x1, x2, x3) → f479_0_descend_Load(x2, x3)
Cond_f128_0_rec_GE5(x1, x2, x3, x4, x5, x6, x7) → Cond_f128_0_rec_GE5(x1, x3, x4, x5, x6)
f517_0_descend_Load(x1, x2, x3) → f517_0_descend_Load(x2, x3)
Cond_f128_0_rec_GE6(x1, x2, x3, x4, x5, x6, x7) → Cond_f128_0_rec_GE6(x1, x3, x4, x5, x6)
f555_0_descend_Load(x1, x2, x3) → f555_0_descend_Load(x2, x3)
Cond_f128_0_rec_GE7(x1, x2, x3, x4, x5, x6, x7) → Cond_f128_0_rec_GE7(x1, x3, x4, x5, x6)
f594_0_descend_Load(x1, x2, x3) → f594_0_descend_Load(x2, x3)
Cond_f128_0_rec_GE8(x1, x2, x3, x4, x5, x6, x7) → Cond_f128_0_rec_GE8(x1, x3, x4, x5, x6)
f620_0_descend_Load(x1, x2, x3) → f620_0_descend_Load(x2, x3)
Cond_f128_0_rec_GE9(x1, x2, x3, x4, x5, x6, x7) → Cond_f128_0_rec_GE9(x1, x3, x4, x5, x6)
f646_0_descend_Load(x1, x2, x3) → f646_0_descend_Load(x2, x3)
Cond_f128_0_rec_GE10(x1, x2, x3, x4, x5, x6, x7) → Cond_f128_0_rec_GE10(x1, x3, x4, x5, x6)

Filtered duplicate terms:


f128_0_rec_GE(x1, x2, x3, x4) → f128_0_rec_GE(x2, x4)
Cond_f128_0_rec_GE(x1, x2, x3, x4, x5) → Cond_f128_0_rec_GE(x1, x3, x5)
f157_0_descend_Load(x1, x2) → f157_0_descend_Load(x2)
Cond_f128_0_rec_GE1(x1, x2, x3, x4, x5) → Cond_f128_0_rec_GE1(x1, x3, x5)
f150_1_rec_Load(x1, x2, x3) → f150_1_rec_Load(x3)
Cond_f128_0_rec_GE2(x1, x2, x3, x4, x5) → Cond_f128_0_rec_GE2(x1, x3, x5)
Cond_f128_0_rec_GE3(x1, x2, x3, x4, x5) → Cond_f128_0_rec_GE3(x1, x3, x5)
f420_0_descend_Load(x1, x2) → f420_0_descend_Load(x2)
Cond_f128_0_rec_GE4(x1, x2, x3, x4, x5) → Cond_f128_0_rec_GE4(x1, x3, x5)
f479_0_descend_Load(x1, x2) → f479_0_descend_Load(x2)
Cond_f128_0_rec_GE5(x1, x2, x3, x4, x5) → Cond_f128_0_rec_GE5(x1, x3, x5)
f517_0_descend_Load(x1, x2) → f517_0_descend_Load(x2)
Cond_f128_0_rec_GE6(x1, x2, x3, x4, x5) → Cond_f128_0_rec_GE6(x1, x3, x5)
f555_0_descend_Load(x1, x2) → f555_0_descend_Load(x2)
Cond_f128_0_rec_GE7(x1, x2, x3, x4, x5) → Cond_f128_0_rec_GE7(x1, x3, x5)
f594_0_descend_Load(x1, x2) → f594_0_descend_Load(x2)
Cond_f128_0_rec_GE8(x1, x2, x3, x4, x5) → Cond_f128_0_rec_GE8(x1, x3, x5)
f620_0_descend_Load(x1, x2) → f620_0_descend_Load(x2)
Cond_f128_0_rec_GE9(x1, x2, x3, x4, x5) → Cond_f128_0_rec_GE9(x1, x3, x5)
f646_0_descend_Load(x1, x2) → f646_0_descend_Load(x2)
Cond_f128_0_rec_GE10(x1, x2, x3, x4, x5) → Cond_f128_0_rec_GE10(x1, x3, x5)

Filtered unneeded terms:


Cond_f128_0_rec_GE(x1, x2, x3) → Cond_f128_0_rec_GE(x1)
Cond_f128_0_rec_GE1(x1, x2, x3) → Cond_f128_0_rec_GE1(x1)
Cond_f128_0_rec_GE2(x1, x2, x3) → Cond_f128_0_rec_GE2(x1, x2)
Cond_f128_0_rec_GE3(x1, x2, x3) → Cond_f128_0_rec_GE3(x1)
Cond_f128_0_rec_GE4(x1, x2, x3) → Cond_f128_0_rec_GE4(x1)
Cond_f128_0_rec_GE5(x1, x2, x3) → Cond_f128_0_rec_GE5(x1)
Cond_f128_0_rec_GE6(x1, x2, x3) → Cond_f128_0_rec_GE6(x1)
Cond_f128_0_rec_GE7(x1, x2, x3) → Cond_f128_0_rec_GE7(x1)
Cond_f128_0_rec_GE8(x1, x2, x3) → Cond_f128_0_rec_GE8(x1)
Cond_f128_0_rec_GE9(x1, x2, x3) → Cond_f128_0_rec_GE9(x1)

Prepared 11 rules for path length conversion:

P rules:
f128_0_rec_GE(x0, x1) → f157_0_descend_Load(x1) | <(x1, 100)
f128_0_rec_GE(x0, x1) → f150_1_rec_Load(-(x0, 1)) | &&(>(x0, 0), >(+(x1, 1), 100))
f128_0_rec_GE(x0, x1) → f128_0_rec_GE(-(x0, 1), -(x0, 1)) | &&(>(x0, 1), >(+(x1, 1), 100))
f128_0_rec_GE(x0, x1) → f420_0_descend_Load(x1) | <(x1, 100)
f128_0_rec_GE(x0, x1) → f479_0_descend_Load(x1) | <(x1, 100)
f128_0_rec_GE(x0, x1) → f517_0_descend_Load(x1) | <(x1, 100)
f128_0_rec_GE(x0, x1) → f555_0_descend_Load(x1) | <(x1, 100)
f128_0_rec_GE(x0, x1) → f594_0_descend_Load(x1) | <(x1, 100)
f128_0_rec_GE(x0, x1) → f620_0_descend_Load(x1) | <(x1, 100)
f128_0_rec_GE(x0, x1) → f646_0_descend_Load(x1) | <(x1, 100)
f128_0_rec_GE(x0, x1) → f128_0_rec_GE(x0, +(x1, 1)) | &&(<(x1, 100), >(x1, 0))

Finished conversion. Obtained 2 rules.

P rules:
f128_0_rec_GE(x4, x5) → f128_0_rec_GE(-(x4, 1), -(x4, 1)) | &&(>(x4, 1), >(x5, 99))
f128_0_rec_GE(x20, x21) → f128_0_rec_GE(x20, +(x21, 1)) | &&(<(x21, 100), >(x21, 0))

(12) Obligation:

Rules:
f128_0_rec_GE(x4, x5) → f128_0_rec_GE(-(x4, 1), -(x4, 1)) | &&(>(x4, 1), >(x5, 99))
f128_0_rec_GE(x20, x21) → f128_0_rec_GE(x20, +(x21, 1)) | &&(<(x21, 100), >(x21, 0))

(13) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:


[f128_0_rec_GE(x5, x7)] = -1 + x5

Therefore the following rule(s) have been dropped:


f128_0_rec_GE(x0, x1) → f128_0_rec_GE(-(x0, 1), -(x0, 1)) | &&(>(x0, 1), >(x1, 99))

(14) Obligation:

Rules:
f128_0_rec_GE(x2, x3) → f128_0_rec_GE(x2, +(x3, 1)) | &&(<(x3, 100), >(x3, 0))

(15) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f128_0_rec_GE(x3, x5)] = 99 - x5

Therefore the following rule(s) have been dropped:


f128_0_rec_GE(x0, x1) → f128_0_rec_GE(x0, +(x1, 1)) | &&(<(x1, 100), >(x1, 0))

(16) YES