Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 6551 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 AND
    ↳5 JBCTerminationSCC
        ↳6 SCCToIntTRSProof (⇒, 67 ms)
        ↳7 intTRS
        ↳8 PolynomialOrderProcessor (⇒, 0 ms)
        ↳9 intTRS
        ↳10 LinearRankingProcessor (⇔, 0 ms)
        ↳11 YES
    ↳12 JBCTerminationSCC
        ↳13 SCCToIntTRSProof (⇒, 274 ms)
        ↳14 intTRS
        ↳15 PolynomialOrderProcessor (⇒, 14 ms)
        ↳16 intTRS
        ↳17 TerminationGraphProcessor (⇒, 0 ms)
        ↳18 intTRS
        ↳19 PolynomialOrderProcessor (⇔, 0 ms)
        ↳20 YES

(0) Obligation:

JBC Problem based on JBC Program:
public class Parts {

    public static int parts(int p, int q) {
	if (p <= 0) return 1;
	else if (q <= 0) return 0;
	else if (q > p) return parts(p, p);
	else return parts(p-q, q) + parts(p, q-1);
    }

    public static void main(String args[]) {
	for (int p = 0; p <= args.length; p++)
	    for (int q = 0; q <= args.length; q++)
		parts(p, q);
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

Parts.parts(II)I: Graph of 101 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: Parts.parts(II)I
SCC calls the following helper methods: Parts.parts(II)I
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 63 IRules

P rules:
f1775_0_parts_GT(EOS, i185, i180, i185, i180, i185) → f1781_0_parts_GT(EOS, i185, i180, i185, i180, i185)
f1781_0_parts_GT(EOS, i185, i180, i185, i180, i185) → f1795_0_parts_Load(EOS, i185, i180, i185, i180) | >(i185, 0)
f1795_0_parts_Load(EOS, i185, i180, i185, i180) → f1807_0_parts_GT(EOS, i185, i180, i185, i180, i180)
f1807_0_parts_GT(EOS, i185, i191, i185, i191, i191) → f1812_0_parts_GT(EOS, i185, i191, i185, i191, i191)
f1812_0_parts_GT(EOS, i185, i191, i185, i191, i191) → f1837_0_parts_Load(EOS, i185, i191, i185, i191) | >(i191, 0)
f1837_0_parts_Load(EOS, i185, i191, i185, i191) → f11861_0_parts_Load(EOS, i185, i191, i185, i191, i191)
f11861_0_parts_Load(EOS, i185, i191, i185, i191, i191) → f11865_0_parts_LE(EOS, i185, i191, i185, i191, i191, i185)
f11865_0_parts_LE(EOS, i185, i191, i185, i191, i191, i185) → f11873_0_parts_LE(EOS, i185, i191, i185, i191, i191, i185)
f11865_0_parts_LE(EOS, i185, i191, i185, i191, i191, i185) → f11874_0_parts_LE(EOS, i185, i191, i185, i191, i191, i185)
f11873_0_parts_LE(EOS, i185, i191, i185, i191, i191, i185) → f11881_0_parts_Load(EOS, i185, i191, i185, i191) | <=(i191, i185)
f11881_0_parts_Load(EOS, i185, i191, i185, i191) → f12065_0_parts_Load(EOS, i185, i191, i185, i191, i185)
f12065_0_parts_Load(EOS, i185, i191, i185, i191, i185) → f12067_0_parts_IntArithmetic(EOS, i185, i191, i185, i191, i185, i191)
f12067_0_parts_IntArithmetic(EOS, i185, i191, i185, i191, i185, i191) → f12070_0_parts_Load(EOS, i185, i191, i185, i191, -(i185, i191)) | &&(>(i185, 0), >(i191, 0))
f12070_0_parts_Load(EOS, i185, i191, i185, i191, i342) → f12073_0_parts_InvokeMethod(EOS, i185, i191, i185, i191, i342, i191)
f12073_0_parts_InvokeMethod(EOS, i185, i191, i185, i191, i342, i191) → f12076_0_parts_Load(EOS, i342, i191, i342, i191)
f12073_0_parts_InvokeMethod(EOS, i185, i191, i185, i191, i342, i191) → f12076_1_parts_Load(EOS, i185, i191, i185, i191, i342, i191, i342, i191)
f12076_0_parts_Load(EOS, i342, i191, i342, i191) → f12077_0_parts_Load(EOS, i342, i191, i342, i191)
f12077_0_parts_Load(EOS, i342, i191, i342, i191) → f1767_0_parts_Load(EOS, i342, i191, i342, i191)
f1767_0_parts_Load(EOS, i179, i180, i179, i180) → f1775_0_parts_GT(EOS, i179, i180, i179, i180, i179)
f12096_0_parts_Return(EOS, i185, i355, i185, i355, i357, i355, i357, i355) → f12099_0_parts_Load(EOS, i185, i355, i185, i355)
f12099_0_parts_Load(EOS, i185, i355, i185, i355) → f12127_0_parts_Load(EOS, i185, i355, i185, i355)
f12127_0_parts_Load(EOS, i185, i374, i185, i374) → f15989_0_parts_Load(EOS, i185, i374, i185, i374)
f15989_0_parts_Load(EOS, i185, i564, i185, i564) → f16031_0_parts_Load(EOS, i185, i564, i185, i564)
f16031_0_parts_Load(EOS, i185, i626, i185, i626) → f19134_0_parts_Load(EOS, i185, i626, i185, i626)
f19134_0_parts_Load(EOS, i185, i928, i185, i928) → f19172_0_parts_Load(EOS, i185, i928, i185, i928)
f19172_0_parts_Load(EOS, i185, i992, i185, i992) → f19655_0_parts_Load(EOS, i185, i992, i185, i992)
f19655_0_parts_Load(EOS, i185, i1260, i185, i1260) → f19657_0_parts_Load(EOS, i185, i1260, i1260, i185)
f19657_0_parts_Load(EOS, i185, i1260, i1260, i185) → f19659_0_parts_ConstantStackPush(EOS, i185, i1260, i185, i1260)
f19659_0_parts_ConstantStackPush(EOS, i185, i1260, i185, i1260) → f19662_0_parts_IntArithmetic(EOS, i185, i1260, i185, i1260, 1)
f19662_0_parts_IntArithmetic(EOS, i185, i1260, i185, i1260, matching1) → f19663_0_parts_InvokeMethod(EOS, i185, i1260, i185, -(i1260, 1)) | &&(>(i1260, 0), =(matching1, 1))
f19663_0_parts_InvokeMethod(EOS, i185, i1260, i185, i1362) → f19664_0_parts_Load(EOS, i185, i1362, i185, i1362)
f19663_0_parts_InvokeMethod(EOS, i185, i1260, i185, i1362) → f19664_1_parts_Load(EOS, i185, i1260, i185, i1362, i185, i1362)
f19664_0_parts_Load(EOS, i185, i1362, i185, i1362) → f19665_0_parts_Load(EOS, i185, i1362, i185, i1362)
f19665_0_parts_Load(EOS, i185, i1362, i185, i1362) → f1767_0_parts_Load(EOS, i185, i1362, i185, i1362)
f12120_0_parts_Return(EOS, i185, i374, i185, i374, i376, i374, i376, i374) → f16023_0_parts_Return(EOS, i185, i374, i185, i374, i376, i374, i376, i374)
f16023_0_parts_Return(EOS, i185, i626, i185, i626, i625, i626, i625, i626) → f19165_0_parts_Return(EOS, i185, i626, i185, i626, i625, i626, i625, i626)
f19165_0_parts_Return(EOS, i185, i992, i185, i992, i991, i992, i991, i992) → f19172_0_parts_Load(EOS, i185, i992, i185, i992)
f15886_0_parts_Return(EOS, i185, i400, i185, i400, i402, i400, i402, i400) → f12120_0_parts_Return(EOS, i185, i400, i185, i400, i402, i400, i402, i400)
f16022_0_parts_Return(EOS, i185, i604, i185, i604, i606, i604, i606, i604) → f16023_0_parts_Return(EOS, i185, i604, i185, i604, i606, i604, i606, i604)
f18153_0_parts_Return(EOS, i185, i661, i185, i661, i663, i661, i663, i661) → f16023_0_parts_Return(EOS, i185, i661, i185, i661, i663, i661, i663, i661)
f19164_0_parts_Return(EOS, i185, i970, i185, i970, i972, i970, i972, i970) → f19165_0_parts_Return(EOS, i185, i970, i185, i970, i972, i970, i972, i970)
f19618_0_parts_Return(EOS, i185, i1027, i185, i1027, i1029, i1027, i1029, i1027) → f19165_0_parts_Return(EOS, i185, i1027, i185, i1027, i1029, i1027, i1029, i1027)
f19661_0_parts_Return(EOS, i185, i1297, i185, i1297, i1299, i1297, i1299, i1297) → f19165_0_parts_Return(EOS, i185, i1297, i185, i1297, i1299, i1297, i1299, i1297)
f19686_0_parts_Return(EOS, i185, i1482, i185, i1482, i1484, i1482) → f19649_0_parts_Return(EOS, i185, i1482, i185, i1482, i1484, i1482)
f19649_0_parts_Return(EOS, i185, i1260, i185, i1260, i1261, i1260) → f19655_0_parts_Load(EOS, i185, i1260, i185, i1260)
f19696_0_parts_Return(EOS, i185, i1670, i185, i1670, i1672, i1670) → f19649_0_parts_Return(EOS, i185, i1670, i185, i1670, i1672, i1670)
f11874_0_parts_LE(EOS, i185, i191, i185, i191, i191, i185) → f12061_0_parts_Load(EOS, i185, i191, i185, i191) | >(i191, i185)
f12061_0_parts_Load(EOS, i185, i191, i185, i191) → f12066_0_parts_Load(EOS, i185, i191, i185, i191, i185)
f12066_0_parts_Load(EOS, i185, i191, i185, i191, i185) → f12068_0_parts_InvokeMethod(EOS, i185, i191, i185, i191, i185, i185)
f12068_0_parts_InvokeMethod(EOS, i185, i191, i185, i191, i185, i185) → f12071_0_parts_Load(EOS, i185, i185, i185, i185)
f12068_0_parts_InvokeMethod(EOS, i185, i191, i185, i191, i185, i185) → f12071_1_parts_Load(EOS, i185, i191, i185, i191, i185, i185, i185, i185)
f12071_0_parts_Load(EOS, i185, i185, i185, i185) → f12074_0_parts_Load(EOS, i185, i185, i185, i185)
f12074_0_parts_Load(EOS, i185, i185, i185, i185) → f1767_0_parts_Load(EOS, i185, i185, i185, i185)
f12076_1_parts_Load(EOS, i185, i355, i185, i355, i357, i355, i357, i355) → f12096_0_parts_Return(EOS, i185, i355, i185, i355, i357, i355, i357, i355)
f12076_1_parts_Load(EOS, i185, i374, i185, i374, i376, i374, i376, i374) → f12120_0_parts_Return(EOS, i185, i374, i185, i374, i376, i374, i376, i374)
f12076_1_parts_Load(EOS, i185, i400, i185, i400, i402, i400, i402, i400) → f15886_0_parts_Return(EOS, i185, i400, i185, i400, i402, i400, i402, i400)
f12076_1_parts_Load(EOS, i185, i604, i185, i604, i606, i604, i606, i604) → f16022_0_parts_Return(EOS, i185, i604, i185, i604, i606, i604, i606, i604)
f12076_1_parts_Load(EOS, i185, i661, i185, i661, i663, i661, i663, i661) → f18153_0_parts_Return(EOS, i185, i661, i185, i661, i663, i661, i663, i661)
f12076_1_parts_Load(EOS, i185, i970, i185, i970, i972, i970, i972, i970) → f19164_0_parts_Return(EOS, i185, i970, i185, i970, i972, i970, i972, i970)
f12076_1_parts_Load(EOS, i185, i1027, i185, i1027, i1029, i1027, i1029, i1027) → f19618_0_parts_Return(EOS, i185, i1027, i185, i1027, i1029, i1027, i1029, i1027)
f12076_1_parts_Load(EOS, i185, i1297, i185, i1297, i1299, i1297, i1299, i1297) → f19661_0_parts_Return(EOS, i185, i1297, i185, i1297, i1299, i1297, i1299, i1297)
f12076_1_parts_Load(EOS, i185, i1482, i185, i1482, i1484, i1482, i1484, i1482) → f19686_0_parts_Return(EOS, i185, i1482, i185, i1482, i1484, i1482)
f12076_1_parts_Load(EOS, i185, i1670, i185, i1670, i1672, i1670, i1672, i1670) → f19696_0_parts_Return(EOS, i185, i1670, i185, i1670, i1672, i1670)

Combined rules. Obtained 5 IRules

P rules:
f1775_0_parts_GT(EOS, x0, x1, x0, x1, x0) → f1775_0_parts_GT(EOS, -(x0, x1), x1, -(x0, x1), x1, -(x0, x1)) | &&(&&(>(x1, 0), <=(x1, x0)), >(x0, 0))
f1775_0_parts_GT(EOS, x0, x1, x0, x1, x0) → f12071_1_parts_Load(EOS, x0, x1, x0, x1, x0, x0, x0, x0) | &&(&&(>(x1, x0), >(x0, 0)), >(x1, 0))
f1775_0_parts_GT(EOS, x0, x1, x0, x1, x0) → f1775_0_parts_GT(EOS, x0, x0, x0, x0, x0) | &&(&&(>(x1, x0), >(x0, 0)), >(x1, 0))
f1775_0_parts_GT(EOS, x0, x1, x0, x1, x0) → f19664_1_parts_Load(EOS, x0, x1, x0, -(x1, 1), x0, -(x1, 1)) | &&(&&(>(x1, 0), <=(x1, x0)), >(x0, 0))
f1775_0_parts_GT(EOS, x0, x1, x0, x1, x0) → f1775_0_parts_GT(EOS, x0, -(x1, 1), x0, -(x1, 1), x0) | &&(&&(>(x1, 0), <=(x1, x0)), >(x0, 0))

Filtered ground terms:


f1775_0_parts_GT(x1, x2, x3, x4, x5, x6) → f1775_0_parts_GT(x2, x3, x4, x5, x6)
Cond_f1775_0_parts_GT(x1, x2, x3, x4, x5, x6, x7) → Cond_f1775_0_parts_GT(x1, x3, x4, x5, x6, x7)
Cond_f1775_0_parts_GT1(x1, x2, x3, x4, x5, x6, x7) → Cond_f1775_0_parts_GT1(x1, x3, x4, x5, x6, x7)
f12071_1_parts_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → f12071_1_parts_Load(x2, x3, x4, x5, x6, x7, x8, x9)
Cond_f1775_0_parts_GT2(x1, x2, x3, x4, x5, x6, x7) → Cond_f1775_0_parts_GT2(x1, x3, x4, x5, x6, x7)
Cond_f1775_0_parts_GT3(x1, x2, x3, x4, x5, x6, x7) → Cond_f1775_0_parts_GT3(x1, x3, x4, x5, x6, x7)
f19664_1_parts_Load(x1, x2, x3, x4, x5, x6, x7) → f19664_1_parts_Load(x2, x3, x4, x5, x6, x7)
Cond_f1775_0_parts_GT4(x1, x2, x3, x4, x5, x6, x7) → Cond_f1775_0_parts_GT4(x1, x3, x4, x5, x6, x7)

Filtered duplicate terms:


f1775_0_parts_GT(x1, x2, x3, x4, x5) → f1775_0_parts_GT(x4, x5)
Cond_f1775_0_parts_GT(x1, x2, x3, x4, x5, x6) → Cond_f1775_0_parts_GT(x1, x5, x6)
Cond_f1775_0_parts_GT1(x1, x2, x3, x4, x5, x6) → Cond_f1775_0_parts_GT1(x1, x5, x6)
f12071_1_parts_Load(x1, x2, x3, x4, x5, x6, x7, x8) → f12071_1_parts_Load(x4, x8)
Cond_f1775_0_parts_GT2(x1, x2, x3, x4, x5, x6) → Cond_f1775_0_parts_GT2(x1, x5, x6)
Cond_f1775_0_parts_GT3(x1, x2, x3, x4, x5, x6) → Cond_f1775_0_parts_GT3(x1, x5, x6)
f19664_1_parts_Load(x1, x2, x3, x4, x5, x6) → f19664_1_parts_Load(x5, x6)
Cond_f1775_0_parts_GT4(x1, x2, x3, x4, x5, x6) → Cond_f1775_0_parts_GT4(x1, x5, x6)

Filtered unneeded terms:


Cond_f1775_0_parts_GT1(x1, x2, x3) → Cond_f1775_0_parts_GT1(x1)
Cond_f1775_0_parts_GT2(x1, x2, x3) → Cond_f1775_0_parts_GT2(x1, x3)
Cond_f1775_0_parts_GT3(x1, x2, x3) → Cond_f1775_0_parts_GT3(x1)

Prepared 5 rules for path length conversion:

P rules:
f1775_0_parts_GT(x1, x0) → f1775_0_parts_GT(x1, -(x0, x1)) | &&(&&(>(x1, 0), <=(x1, x0)), >(x0, 0))
f1775_0_parts_GT(x1, x0) → f12071_1_parts_Load(x1, x0) | &&(&&(>(x1, x0), >(x0, 0)), >(x1, 0))
f1775_0_parts_GT(x1, x0) → f1775_0_parts_GT(x0, x0) | &&(&&(>(x1, x0), >(x0, 0)), >(x1, 0))
f1775_0_parts_GT(x1, x0) → f19664_1_parts_Load(x0, -(x1, 1)) | &&(&&(>(x1, 0), <=(x1, x0)), >(x0, 0))
f1775_0_parts_GT(x1, x0) → f1775_0_parts_GT(-(x1, 1), x0) | &&(&&(>(x1, 0), <=(x1, x0)), >(x0, 0))

Finished conversion. Obtained 3 rules.

P rules:
f1775_0_parts_GT(x0, x1) → f1775_0_parts_GT(x0, -(x1, x0)) | &&(&&(>=(x1, x0), >(x0, 0)), >(x1, 0))
f1775_0_parts_GT(x4, x5) → f1775_0_parts_GT(x5, x5) | &&(&&(>(x5, 0), >(x4, 0)), <(x5, x4))
f1775_0_parts_GT(x8, x9) → f1775_0_parts_GT(-(x8, 1), x9) | &&(&&(>=(x9, x8), >(x8, 0)), >(x9, 0))

(7) Obligation:

Rules:
f1775_0_parts_GT(x0, x1) → f1775_0_parts_GT(x0, -(x1, x0)) | &&(&&(>=(x1, x0), >(x0, 0)), >(x1, 0))
f1775_0_parts_GT(x4, x5) → f1775_0_parts_GT(x5, x5) | &&(&&(>(x5, 0), >(x4, 0)), <(x5, x4))
f1775_0_parts_GT(x8, x9) → f1775_0_parts_GT(-(x8, 1), x9) | &&(&&(>=(x9, x8), >(x8, 0)), >(x9, 0))

(8) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:


[f1775_0_parts_GT(x7, x9)] = x7

Therefore the following rule(s) have been dropped:


f1775_0_parts_GT(x2, x3) → f1775_0_parts_GT(x3, x3) | &&(&&(>(x3, 0), >(x2, 0)), <(x3, x2))
f1775_0_parts_GT(x4, x5) → f1775_0_parts_GT(-(x4, 1), x5) | &&(&&(>=(x5, x4), >(x4, 0)), >(x5, 0))

(9) Obligation:

Rules:
f1775_0_parts_GT(x0, x1) → f1775_0_parts_GT(x0, -(x1, x0)) | &&(&&(>=(x1, x0), >(x0, 0)), >(x1, 0))

(10) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:


[f1775_0_parts_GT(x)] = 1·x2

where x = (x1, ... ,xn).



Therefore the following rule(s) have been dropped:


f1775_0_parts_GT(x0, x1) → f1775_0_parts_GT(x0, -(x1, x0)) | &&(&&(>=(x1, x0), >(x0, 0)), >(x1, 0))

(11) YES

(12) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Parts.main([Ljava/lang/String;)V
SCC calls the following helper methods: Parts.parts(II)I
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
  • Marker field analysis yielded the following relations that could be markers:

(13) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 65 IRules

P rules:
f564_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i33, i33) → f566_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i33, i33, java.lang.Object(ARRAY(i1)))
f566_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i33, i33, java.lang.Object(ARRAY(i1))) → f569_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i33, i33, i1) | >=(i1, 0)
f569_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i33, i33, i1) → f572_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i33, i33, i1)
f572_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i33, i33, i1) → f576_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i33) | <=(i33, i1)
f576_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i33) → f580_0_main_Store(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i33, 0)
f580_0_main_Store(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i33, matching1) → f583_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i33, 0) | =(matching1, 0)
f583_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i33, matching1) → f697_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i33, 0) | =(matching1, 0)
f697_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i40, i41) → f1082_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i40, i41)
f1082_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i76, i77) → f1357_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i76, i77)
f1357_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i125, i126) → f1364_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i125, i126, i126)
f1364_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i125, i126, i126) → f1366_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i125, i126, i126, java.lang.Object(ARRAY(i1)))
f1366_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i125, i126, i126, java.lang.Object(ARRAY(i1))) → f1372_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i125, i126, i126, i1) | >=(i1, 0)
f1372_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i125, i126, i126, i1) → f1376_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i125, i126, i126, i1)
f1372_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i125, i126, i126, i1) → f1377_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i125, i126, i126, i1)
f1376_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i125, i126, i126, i1) → f1381_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i125) | >(i126, i1)
f1381_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i125) → f1389_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), +(i125, 1)) | >=(i125, 0)
f1389_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i130) → f1399_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i130)
f1399_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i130) → f560_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i130)
f560_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i33) → f564_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i33, i33)
f1377_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i125, i126, i126, i1) → f1385_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i125, i126) | <=(i126, i1)
f1385_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i125, i126) → f1392_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i125, i126, i125)
f1392_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i125, i126, i125) → f1402_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i125, i126, i125, i126)
f1402_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i125, i126, i125, i126) → f1684_0_parts_Load(EOS, i125, i126, i125, i126)
f1402_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i125, i126, i125, i126) → f1684_1_parts_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i125, i126, i125, i126, i125, i126)
f1684_0_parts_Load(EOS, i125, i126, i125, i126) → f1689_0_parts_Load(EOS, i125, i126, i125, i126)
f1835_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), matching1, i197, matching2, i197, matching3, i197) → f1750_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), 0, i197, 0, i197, 0, i197) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f1750_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), matching1, i169, matching2, i169, matching3, i169) → f1755_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), 0, i169) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f1755_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), matching1, i169) → f1769_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), 0, i169) | =(matching1, 0)
f1769_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), matching1, i169) → f1777_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), 0, +(i169, 1)) | &&(>=(i169, 0), =(matching1, 0))
f1777_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), matching1, i183) → f1793_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), 0, i183) | =(matching1, 0)
f1793_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), matching1, i183) → f1357_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), 0, i183) | =(matching1, 0)
f11879_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i284, matching1, i284, matching2, i284, matching3, matching4) → f1752_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i284, 0, i284, 0, i284, 0, 0) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
f1752_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i172, matching1, i172, matching2, i172, matching3, matching4) → f1759_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i172, 0, 0) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
f1759_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i172, matching1, matching2) → f1772_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i172, 0) | &&(=(matching1, 0), =(matching2, 0))
f1772_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i172, matching1) → f1784_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i172, 1) | =(matching1, 0)
f1784_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i172, matching1) → f1802_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i172, 1) | =(matching1, 1)
f1802_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i172, matching1) → f1357_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i172, 1) | =(matching1, 1)
f12107_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i364, i366, i364, i366, i364, i366) → f16003_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i364, i366, i364, i366, i364, i366)
f16003_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i592, i593, i592, i593, i592, i593) → f19146_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i592, i593, i592, i593, i592, i593)
f19146_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i958, i959, i958, i959, i958, i959) → f19150_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i958, i959)
f19150_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i958, i959) → f19641_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i958, i959)
f19641_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1197, i1198) → f19642_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1197, i1198)
f19642_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1197, i1198) → f19643_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1197, +(i1198, 1)) | >(i1198, 0)
f19643_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1197, i1228) → f19645_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1197, i1228)
f19645_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1197, i1228) → f1357_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1197, i1228)
f12139_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i388, i390, i388, i390, i388, i390) → f12107_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i388, i390, i388, i390, i388, i390)
f16002_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i584, i586, i584, i586, i584, i586) → f16003_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i584, i586, i584, i586, i584, i586)
f16042_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i646, i648, i646, i648, i646, i648) → f16003_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i646, i648, i646, i648, i646, i648)
f19145_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i950, i952, i950, i952, i950, i952) → f19146_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i950, i952, i950, i952, i950, i952)
f19180_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1012, i1014, i1012, i1014, i1012, i1014) → f19146_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1012, i1014, i1012, i1014, i1012, i1014)
f19658_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1282, i1284, i1282, i1284, i1282, i1284) → f19146_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1282, i1284, i1282, i1284, i1282, i1284)
f19683_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1467, i1469, i1467, i1469) → f19640_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1467, i1469, i1467, i1469)
f19640_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1197, i1198, i1197, i1198) → f19641_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1197, i1198)
f19694_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1655, i1657, i1655, i1657) → f19640_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1655, i1657, i1655, i1657)
f1684_1_parts_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), matching1, i197, matching2, i197, matching3, i197) → f1835_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), 0, i197, 0, i197, 0, i197) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f1684_1_parts_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i284, matching1, i284, matching2, i284, matching3) → f11879_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i284, 0, i284, 0, i284, 0, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f1684_1_parts_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i364, i366, i364, i366, i364, i366) → f12107_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i364, i366, i364, i366, i364, i366)
f1684_1_parts_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i388, i390, i388, i390, i388, i390) → f12139_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i388, i390, i388, i390, i388, i390)
f1684_1_parts_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i584, i586, i584, i586, i584, i586) → f16002_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i584, i586, i584, i586, i584, i586)
f1684_1_parts_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i646, i648, i646, i648, i646, i648) → f16042_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i646, i648, i646, i648, i646, i648)
f1684_1_parts_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i950, i952, i950, i952, i950, i952) → f19145_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i950, i952, i950, i952, i950, i952)
f1684_1_parts_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1012, i1014, i1012, i1014, i1012, i1014) → f19180_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1012, i1014, i1012, i1014, i1012, i1014)
f1684_1_parts_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1282, i1284, i1282, i1284, i1282, i1284) → f19658_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1282, i1284, i1282, i1284, i1282, i1284)
f1684_1_parts_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1467, i1469, i1467, i1469, i1467, i1469) → f19683_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1467, i1469, i1467, i1469)
f1684_1_parts_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1655, i1657, i1655, i1657, i1655, i1657) → f19694_0_parts_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1655, i1657, i1655, i1657)

Combined rules. Obtained 5 IRules

P rules:
f1372_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x2, x0) → f1372_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), +(x1, 1), 0, 0, x0) | &&(&&(&&(>(x2, x0), >(+(x1, 1), 0)), <=(+(x1, 1), x0)), >(+(x0, 1), 0))
f1372_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x2, x0) → f1689_0_parts_Load(EOS, x1, x2, x1, x2) | <=(x2, x0)
f1372_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x2, x0) → f1372_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, +(x2, 1), +(x2, 1), x0) | &&(&&(>(x2, 0), >(+(x0, 1), 0)), <=(x2, x0))
f1372_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), 0, x2, x2, x0) → f1372_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), 0, +(x2, 1), +(x2, 1), x0) | &&(&&(>(+(x2, 1), 0), >(+(x0, 1), 0)), <=(x2, x0))
f1372_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, 0, 0, x0) → f1372_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, 1, 1, x0) | >(+(x0, 1), 0)

Filtered ground terms:


f1372_0_main_GT(x1, x2, x3, x4, x5, x6, x7) → f1372_0_main_GT(x2, x3, x4, x5, x6, x7)
Cond_f1372_0_main_GT(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1372_0_main_GT(x1, x3, x4, x5, x6, x7, x8)
Cond_f1372_0_main_GT1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1372_0_main_GT1(x1, x3, x4, x5, x6, x7, x8)
f1689_0_parts_Load(x1, x2, x3, x4, x5) → f1689_0_parts_Load(x2, x3, x4, x5)
Cond_f1372_0_main_GT2(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1372_0_main_GT2(x1, x3, x4, x5, x6, x7, x8)
Cond_f1372_0_main_GT3(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1372_0_main_GT3(x1, x3, x4, x6, x7, x8)
Cond_f1372_0_main_GT4(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1372_0_main_GT4(x1, x3, x4, x5, x8)

Filtered duplicate terms:


f1372_0_main_GT(x1, x2, x3, x4, x5, x6) → f1372_0_main_GT(x2, x3, x5)
Cond_f1372_0_main_GT(x1, x2, x3, x4, x5, x6, x7) → Cond_f1372_0_main_GT(x1, x3, x4, x6)
Cond_f1372_0_main_GT1(x1, x2, x3, x4, x5, x6, x7) → Cond_f1372_0_main_GT1(x1, x3, x4, x6)
f1689_0_parts_Load(x1, x2, x3, x4) → f1689_0_parts_Load(x3, x4)
Cond_f1372_0_main_GT2(x1, x2, x3, x4, x5, x6, x7) → Cond_f1372_0_main_GT2(x1, x3, x4, x6)
Cond_f1372_0_main_GT3(x1, x2, x3, x4, x5, x6) → Cond_f1372_0_main_GT3(x1, x3, x5)
Cond_f1372_0_main_GT4(x1, x2, x3, x4, x5) → Cond_f1372_0_main_GT4(x1, x3, x4)

Filtered unneeded terms:


Cond_f1372_0_main_GT(x1, x2, x3, x4) → Cond_f1372_0_main_GT(x1, x2, x3)
Cond_f1372_0_main_GT1(x1, x2, x3, x4) → Cond_f1372_0_main_GT1(x1)

Prepared 5 rules for path length conversion:

P rules:
f1372_0_main_GT(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f1372_0_main_GT(java.lang.Object(ARRAY(x0)), +(x1, 1), 0, x0) | &&(&&(&&(>(x2, x0), >(+(x1, 1), 0)), <=(+(x1, 1), x0)), >(+(x0, 1), 0))
f1372_0_main_GT(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f1689_0_parts_Load(x1, x2) | <=(x2, x0)
f1372_0_main_GT(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f1372_0_main_GT(java.lang.Object(ARRAY(x0)), x1, +(x2, 1), x0) | &&(&&(>(x2, 0), >(+(x0, 1), 0)), <=(x2, x0))
f1372_0_main_GT(java.lang.Object(ARRAY(x0)), 0, x2, x0) → f1372_0_main_GT(java.lang.Object(ARRAY(x0)), 0, +(x2, 1), x0) | &&(&&(>(+(x2, 1), 0), >(+(x0, 1), 0)), <=(x2, x0))
f1372_0_main_GT(java.lang.Object(ARRAY(x0)), x1, 0, x0) → f1372_0_main_GT(java.lang.Object(ARRAY(x0)), x1, 1, x0) | >(+(x0, 1), 0)

Finished conversion. Obtained 4 rules.

P rules:
f1372_0_main_GT(v17, x1, x2, x0) → f1372_0_main_GT(v18, +(x1, 1), 0, x0) | &&(&&(&&(&&(&&(&&(>(x2, x0), >(x1, -1)), <=(+(x1, 1), x0)), >(x0, -1)), >(+(v18, 1), 1)), <=(v18, v17)), >(+(v17, 1), 1))
f1372_0_main_GT(v19, x7, x8, x6) → f1372_0_main_GT(v20, x7, +(x8, 1), x6) | &&(&&(&&(&&(&&(>(x8, 0), <=(x8, x6)), >(x6, -1)), >(+(v20, 1), 1)), <=(v20, v19)), >(+(v19, 1), 1))
f1372_0_main_GT(v21, c0, x10, x9) → f1372_0_main_GT(v22, 0, +(x10, 1), x9) | &&(&&(&&(&&(&&(&&(>=(x9, x10), >(x9, -1)), >(x10, -1)), >(+(v22, 1), 1)), <=(v22, v21)), >(+(v21, 1), 1)), =(0, c0))
f1372_0_main_GT(v23, x12, c0, x11) → f1372_0_main_GT(v24, x12, 1, x11) | &&(&&(&&(&&(>(x11, -1), >(+(v24, 1), 1)), <=(v24, v23)), >(+(v23, 1), 1)), =(0, c0))

(14) Obligation:

Rules:
f1372_0_main_GT(v17, x1, x2, x0) → f1372_0_main_GT(v18, +(x1, 1), 0, x0) | &&(&&(&&(&&(&&(&&(>(x2, x0), >(x1, -1)), <=(+(x1, 1), x0)), >(x0, -1)), >(+(v18, 1), 1)), <=(v18, v17)), >(+(v17, 1), 1))
f1372_0_main_GT(v19, x7, x8, x6) → f1372_0_main_GT(v20, x7, +(x8, 1), x6) | &&(&&(&&(&&(&&(>(x8, 0), <=(x8, x6)), >(x6, -1)), >(+(v20, 1), 1)), <=(v20, v19)), >(+(v19, 1), 1))
f1372_0_main_GT(v21, c0, x10, x9) → f1372_0_main_GT(v22, 0, +(x10, 1), x9) | &&(&&(&&(&&(&&(&&(>=(x9, x10), >(x9, -1)), >(x10, -1)), >(+(v22, 1), 1)), <=(v22, v21)), >(+(v21, 1), 1)), =(0, c0))
f1372_0_main_GT(v23, x12, c0, x11) → f1372_0_main_GT(v24, x12, 1, x11) | &&(&&(&&(&&(>(x11, -1), >(+(v24, 1), 1)), <=(v24, v23)), >(+(v23, 1), 1)), =(0, c0))

(15) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:


[f1372_0_main_GT(x21, x23, x25, x27)] = -1 - x23 + x27

Therefore the following rule(s) have been dropped:


f1372_0_main_GT(x0, x1, x2, x3) → f1372_0_main_GT(x4, +(x1, 1), 0, x3) | &&(&&(&&(&&(&&(&&(>(x2, x3), >(x1, -1)), <=(+(x1, 1), x3)), >(x3, -1)), >(+(x4, 1), 1)), <=(x4, x0)), >(+(x0, 1), 1))

(16) Obligation:

Rules:
f1372_0_main_GT(x5, x6, x7, x8) → f1372_0_main_GT(x9, x6, +(x7, 1), x8) | &&(&&(&&(&&(&&(>(x7, 0), <=(x7, x8)), >(x8, -1)), >(+(x9, 1), 1)), <=(x9, x5)), >(+(x5, 1), 1))
f1372_0_main_GT(x10, x11, x12, x13) → f1372_0_main_GT(x14, 0, +(x12, 1), x13) | &&(&&(&&(&&(&&(&&(>=(x13, x12), >(x13, -1)), >(x12, -1)), >(+(x14, 1), 1)), <=(x14, x10)), >(+(x10, 1), 1)), =(0, x11))
f1372_0_main_GT(x15, x16, x17, x18) → f1372_0_main_GT(x19, x16, 1, x18) | &&(&&(&&(&&(>(x18, -1), >(+(x19, 1), 1)), <=(x19, x15)), >(+(x15, 1), 1)), =(0, x17))

(17) TerminationGraphProcessor (SOUND transformation)

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


(18) Obligation:

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

(19) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f1372_0_main_GT(x11, x13, x15, x17)] = -x15 + x17

Therefore the following rule(s) have been dropped:


f1372_0_main_GT(x0, x1, x2, x3) → f1372_0_main_GT(x4, x1, +(x2, 1), x3) | &&(&&(&&(&&(&&(>(x2, 0), <=(x2, x3)), >(x3, -1)), >(+(x4, 1), 1)), <=(x4, x0)), >(+(x0, 1), 1))
f1372_0_main_GT(x5, x6, x7, x8) → f1372_0_main_GT(x9, 0, +(x7, 1), x8) | &&(&&(&&(&&(&&(&&(>=(x8, x7), >(x8, -1)), >(x7, -1)), >(+(x9, 1), 1)), <=(x9, x5)), >(+(x5, 1), 1)), =(0, x6))

(20) YES