Termination proof of /tmp/tmpKEAA36/TaylorSeriesRec.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 1007 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIntTRSProof (⇒, 21 ms)

        ↳7 intTRS

        ↳8 LinearRankingProcessor (⇔, 0 ms)

        ↳9 YES

    ↳10 JBCTerminationSCC

        ↳11 SCCToIntTRSProof (⇒, 28 ms)

        ↳12 intTRS

        ↳13 PolynomialOrderProcessor (⇔, 0 ms)

        ↳14 YES

    ↳15 JBCTerminationSCC

        ↳16 SCCToIntTRSProof (⇒, 30 ms)

        ↳17 intTRS

        ↳18 PolynomialOrderProcessor (⇔, 0 ms)

        ↳19 YES

    ↳20 JBCTerminationSCC

        ↳21 SCCToIntTRSProof (⇒, 136 ms)

        ↳22 intTRS

        ↳23 PolynomialOrderProcessor (⇔, 0 ms)

        ↳24 YES

    ↳25 JBCTerminationSCC

        ↳26 SCCToIntTRSProof (⇒, 132 ms)

        ↳27 intTRS

        ↳28 PolynomialOrderProcessor (⇔, 0 ms)

        ↳29 YES

    ↳30 JBCTerminationSCC

        ↳31 SCCToIntTRSProof (⇒, 557 ms)

        ↳32 intTRS

        ↳33 TerminationGraphProcessor (⇒, 172 ms)

        ↳34 intTRS

        ↳35 PolynomialOrderProcessor (⇒, 43 ms)

        ↳36 intTRS

        ↳37 TerminationGraphProcessor (⇒, 0 ms)

        ↳38 intTRS

        ↳39 PolynomialOrderProcessor (⇔, 0 ms)

        ↳40 YES

(0) Obligation:

JBC Problem based on JBC Program:

public class TaylorSeriesRec {
    
    public static int power(int a, int b) {
	if (b <= 0) return 1;
	else return a * power(a, b-1);
    }

    public static int fact(int n) {
	if (n <= 0) return 1;
	else return n * fact(n-1);
    }

    public static int sin(int x, int n) {
	if (n <= 0) return x;
	else return power(-1, n) * power(x, 2*n+1) / fact(2*n+1) + sin(x, n-1);
    }

    public static int cos(int x, int n) {
	if (n <= 0) return 1;
	else return power(-1, n) * power(x, 2*n) / fact(2*n) + cos(x, n-1);
    }

    public static int exp(int x, int n) {
	if (n <= 0) return 1;
	else return power(x, n) / fact(n) + exp(x, n-1);
    }

    public static void main(String args[]) {
	for (int i = 0; i < args.length; i++)
	    if (i % 2 == 0) sin(args.length, i);
	    else if (i % 3 == 0) cos(args.length, i);
	    else if (i % 5 == 0) exp(args.length, i);
	    else for (int j = 0; j < 100; j++);
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

TaylorSeriesRec.sin(II)I: Graph of 48 nodes with 0 SCCs.

TaylorSeriesRec.power(II)I: Graph of 22 nodes with 0 SCCs.

TaylorSeriesRec.cos(II)I: Graph of 44 nodes with 0 SCCs.

TaylorSeriesRec.exp(II)I: Graph of 33 nodes with 0 SCCs.

TaylorSeriesRec.fact(I)I: Graph of 22 nodes with 0 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 6 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: TaylorSeriesRec.fact(I)I
SCC calls the following helper methods: TaylorSeriesRec.fact(I)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 11 IRules

P rules:
f1897_0_fact_GT(EOS, i324, i324, i324) → f1905_0_fact_GT(EOS, i324, i324, i324)
f1905_0_fact_GT(EOS, i324, i324, i324) → f1926_0_fact_Load(EOS, i324, i324) | >(i324, 0)
f1926_0_fact_Load(EOS, i324, i324) → f1938_0_fact_Load(EOS, i324, i324, i324)
f1938_0_fact_Load(EOS, i324, i324, i324) → f1945_0_fact_ConstantStackPush(EOS, i324, i324, i324)
f1945_0_fact_ConstantStackPush(EOS, i324, i324, i324) → f1975_0_fact_IntArithmetic(EOS, i324, i324, i324, 1)
f1975_0_fact_IntArithmetic(EOS, i324, i324, i324, matching1) → f1981_0_fact_InvokeMethod(EOS, i324, i324, -(i324, 1)) | &&(>(i324, 0), =(matching1, 1))
f1981_0_fact_InvokeMethod(EOS, i324, i324, i338) → f1984_0_fact_Load(EOS, i338, i338)
f1981_0_fact_InvokeMethod(EOS, i324, i324, i338) → f1984_1_fact_Load(EOS, i324, i324, i338, i338)
f1984_0_fact_Load(EOS, i338, i338) → f1992_0_fact_Load(EOS, i338, i338)
f1992_0_fact_Load(EOS, i338, i338) → f1885_0_fact_Load(EOS, i338, i338)
f1885_0_fact_Load(EOS, i320, i320) → f1897_0_fact_GT(EOS, i320, i320, i320)

Combined rules. Obtained 2 IRules

P rules:
f1897_0_fact_GT(EOS, x0, x0, x0) → f1984_1_fact_Load(EOS, x0, x0, -(x0, 1), -(x0, 1)) | >(x0, 0)
f1897_0_fact_GT(EOS, x0, x0, x0) → f1897_0_fact_GT(EOS, -(x0, 1), -(x0, 1), -(x0, 1)) | >(x0, 0)

Filtered ground terms:

f1897_0_fact_GT(x1, x2, x3, x4) → f1897_0_fact_GT(x2, x3, x4)
Cond_f1897_0_fact_GT(x1, x2, x3, x4, x5) → Cond_f1897_0_fact_GT(x1, x3, x4, x5)
f1984_1_fact_Load(x1, x2, x3, x4, x5) → f1984_1_fact_Load(x2, x3, x4, x5)
Cond_f1897_0_fact_GT1(x1, x2, x3, x4, x5) → Cond_f1897_0_fact_GT1(x1, x3, x4, x5)

Filtered duplicate terms:

f1897_0_fact_GT(x1, x2, x3) → f1897_0_fact_GT(x3)
Cond_f1897_0_fact_GT(x1, x2, x3, x4) → Cond_f1897_0_fact_GT(x1, x4)
f1984_1_fact_Load(x1, x2, x3, x4) → f1984_1_fact_Load(x4)
Cond_f1897_0_fact_GT1(x1, x2, x3, x4) → Cond_f1897_0_fact_GT1(x1, x4)

Filtered unneeded terms:

Cond_f1897_0_fact_GT(x1, x2) → Cond_f1897_0_fact_GT(x1)

Prepared 2 rules for path length conversion:

P rules:
f1897_0_fact_GT(x0) → f1984_1_fact_Load(-(x0, 1)) | >(x0, 0)
f1897_0_fact_GT(x0) → f1897_0_fact_GT(-(x0, 1)) | >(x0, 0)

Finished conversion. Obtained 1 rules.

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

(7) Obligation:

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

(8) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:

[f1897_0_fact_GT(x)] = 1·x₁

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

Therefore the following rule(s) have been dropped:

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

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: TaylorSeriesRec.power(II)I
SCC calls the following helper methods: TaylorSeriesRec.power(II)I
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 12 IRules

P rules:
f999_0_power_GT(EOS, i100, i100, i100) → f1007_0_power_GT(EOS, i100, i100, i100)
f1007_0_power_GT(EOS, i100, i100, i100) → f1018_0_power_Load(EOS, i100, i100) | >(i100, 0)
f1018_0_power_Load(EOS, i100, i100) → f1031_0_power_Load(EOS, i100, i100)
f1031_0_power_Load(EOS, i100, i100) → f1045_0_power_Load(EOS, i100, i100)
f1045_0_power_Load(EOS, i100, i100) → f1112_0_power_ConstantStackPush(EOS, i100, i100)
f1112_0_power_ConstantStackPush(EOS, i100, i100) → f1123_0_power_IntArithmetic(EOS, i100, i100, 1)
f1123_0_power_IntArithmetic(EOS, i100, i100, matching1) → f1128_0_power_InvokeMethod(EOS, i100, -(i100, 1)) | &&(>(i100, 0), =(matching1, 1))
f1128_0_power_InvokeMethod(EOS, i100, i117) → f1133_0_power_Load(EOS, i117, i117)
f1128_0_power_InvokeMethod(EOS, i100, i117) → f1133_1_power_Load(EOS, i100, i117, i117)
f1133_0_power_Load(EOS, i117, i117) → f1139_0_power_Load(EOS, i117, i117)
f1139_0_power_Load(EOS, i117, i117) → f987_0_power_Load(EOS, i117, i117)
f987_0_power_Load(EOS, i98, i98) → f999_0_power_GT(EOS, i98, i98, i98)

Combined rules. Obtained 2 IRules

P rules:
f999_0_power_GT(EOS, x0, x0, x0) → f1133_1_power_Load(EOS, x0, -(x0, 1), -(x0, 1)) | >(x0, 0)
f999_0_power_GT(EOS, x0, x0, x0) → f999_0_power_GT(EOS, -(x0, 1), -(x0, 1), -(x0, 1)) | >(x0, 0)

Filtered ground terms:

f999_0_power_GT(x1, x2, x3, x4) → f999_0_power_GT(x2, x3, x4)
Cond_f999_0_power_GT(x1, x2, x3, x4, x5) → Cond_f999_0_power_GT(x1, x3, x4, x5)
f1133_1_power_Load(x1, x2, x3, x4) → f1133_1_power_Load(x2, x3, x4)
Cond_f999_0_power_GT1(x1, x2, x3, x4, x5) → Cond_f999_0_power_GT1(x1, x3, x4, x5)

Filtered duplicate terms:

f999_0_power_GT(x1, x2, x3) → f999_0_power_GT(x3)
Cond_f999_0_power_GT(x1, x2, x3, x4) → Cond_f999_0_power_GT(x1, x4)
f1133_1_power_Load(x1, x2, x3) → f1133_1_power_Load(x3)
Cond_f999_0_power_GT1(x1, x2, x3, x4) → Cond_f999_0_power_GT1(x1, x4)

Filtered unneeded terms:

Cond_f999_0_power_GT(x1, x2) → Cond_f999_0_power_GT(x1)

Prepared 2 rules for path length conversion:

P rules:
f999_0_power_GT(x0) → f1133_1_power_Load(-(x0, 1)) | >(x0, 0)
f999_0_power_GT(x0) → f999_0_power_GT(-(x0, 1)) | >(x0, 0)

Finished conversion. Obtained 1 rules.

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

(12) Obligation:

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

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f999_0_power_GT(x2)] = x2

Therefore the following rule(s) have been dropped:

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

(14) YES

(15) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: TaylorSeriesRec.exp(II)I
SCC calls the following helper methods: TaylorSeriesRec.fact(I)I, TaylorSeriesRec.exp(II)I, TaylorSeriesRec.power(II)I
Performed SCC analyses:

Used field analysis yielded the following read fields:
Marker field analysis yielded the following relations that could be markers:

(16) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 25 IRules

P rules:
f2794_0_power_Return(EOS, i586, i586, i586) → f2801_0_exp_Load(EOS, i586, i586)
f2801_0_exp_Load(EOS, i586, i586) → f2808_0_exp_InvokeMethod(EOS, i586, i586, i586)
f2808_0_exp_InvokeMethod(EOS, i586, i586, i586) → f2818_0_fact_Load(EOS, i586, i586)
f2808_0_exp_InvokeMethod(EOS, i586, i586, i586) → f2818_1_fact_Load(EOS, i586, i586, i586, i586)
f2818_0_fact_Load(EOS, i586, i586) → f2825_0_fact_Load(EOS, i586, i586)
f2896_0_fact_Return(EOS, i612, i612, i612) → f2911_0_exp_IntArithmetic(EOS, i612, i612)
f2911_0_exp_IntArithmetic(EOS, i612, i612) → f2918_0_exp_Load(EOS, i612, i612)
f2918_0_exp_Load(EOS, i612, i612) → f2925_0_exp_Load(EOS, i612, i612)
f2925_0_exp_Load(EOS, i612, i612) → f2940_0_exp_ConstantStackPush(EOS, i612, i612)
f2940_0_exp_ConstantStackPush(EOS, i612, i612) → f2947_0_exp_IntArithmetic(EOS, i612, i612, 1)
f2947_0_exp_IntArithmetic(EOS, i612, i612, matching1) → f2961_0_exp_InvokeMethod(EOS, i612, -(i612, 1)) | &&(>(i612, 0), =(matching1, 1))
f2961_0_exp_InvokeMethod(EOS, i612, i638) → f2974_0_exp_Load(EOS, i638, i638)
f2961_0_exp_InvokeMethod(EOS, i612, i638) → f2974_1_exp_Load(EOS, i612, i638, i638)
f2974_0_exp_Load(EOS, i638, i638) → f2983_0_exp_Load(EOS, i638, i638)
f2983_0_exp_Load(EOS, i638, i638) → f2640_0_exp_Load(EOS, i638, i638)
f2640_0_exp_Load(EOS, i538, i538) → f2649_0_exp_GT(EOS, i538, i538, i538)
f2649_0_exp_GT(EOS, i542, i542, i542) → f2658_0_exp_GT(EOS, i542, i542, i542)
f2658_0_exp_GT(EOS, i542, i542, i542) → f2673_0_exp_Load(EOS, i542, i542) | >(i542, 0)
f2673_0_exp_Load(EOS, i542, i542) → f2690_0_exp_Load(EOS, i542, i542)
f2690_0_exp_Load(EOS, i542, i542) → f2703_0_exp_InvokeMethod(EOS, i542, i542, i542)
f2703_0_exp_InvokeMethod(EOS, i542, i542, i542) → f2736_0_power_Load(EOS, i542, i542)
f2703_0_exp_InvokeMethod(EOS, i542, i542, i542) → f2736_1_power_Load(EOS, i542, i542, i542, i542)
f2736_0_power_Load(EOS, i542, i542) → f2748_0_power_Load(EOS, i542, i542)
f2818_1_fact_Load(EOS, i612, i612, i612, i612) → f2896_0_fact_Return(EOS, i612, i612, i612)
f2736_1_power_Load(EOS, i586, i586, i586, i586) → f2794_0_power_Return(EOS, i586, i586, i586)

Combined rules. Obtained 4 IRules

P rules:
f2794_0_power_Return(EOS, x0, x0, x0) → f2825_0_fact_Load(EOS, x0, x0)
f2794_0_power_Return(EOS, x0, x0, x0) → f2974_1_exp_Load(EOS, x0, -(x0, 1), -(x0, 1)) | >(x0, 0)
f2794_0_power_Return(EOS, x0, x0, x0) → f2748_0_power_Load(EOS, -(x0, 1), -(x0, 1)) | >(x0, 1)
f2794_0_power_Return(EOS, x0, x0, x0) → f2794_0_power_Return(EOS, -(x0, 1), -(x0, 1), -(x0, 1)) | >(x0, 1)

Filtered ground terms:

f2794_0_power_Return(x1, x2, x3, x4) → f2794_0_power_Return(x2, x3, x4)
f2825_0_fact_Load(x1, x2, x3) → f2825_0_fact_Load(x2, x3)
Cond_f2794_0_power_Return(x1, x2, x3, x4, x5) → Cond_f2794_0_power_Return(x1, x3, x4, x5)
f2974_1_exp_Load(x1, x2, x3, x4) → f2974_1_exp_Load(x2, x3, x4)
Cond_f2794_0_power_Return1(x1, x2, x3, x4, x5) → Cond_f2794_0_power_Return1(x1, x3, x4, x5)
f2748_0_power_Load(x1, x2, x3) → f2748_0_power_Load(x2, x3)
Cond_f2794_0_power_Return2(x1, x2, x3, x4, x5) → Cond_f2794_0_power_Return2(x1, x3, x4, x5)

Filtered duplicate terms:

f2794_0_power_Return(x1, x2, x3) → f2794_0_power_Return(x3)
f2825_0_fact_Load(x1, x2) → f2825_0_fact_Load(x2)
Cond_f2794_0_power_Return(x1, x2, x3, x4) → Cond_f2794_0_power_Return(x1, x4)
f2974_1_exp_Load(x1, x2, x3) → f2974_1_exp_Load(x3)
Cond_f2794_0_power_Return1(x1, x2, x3, x4) → Cond_f2794_0_power_Return1(x1, x4)
f2748_0_power_Load(x1, x2) → f2748_0_power_Load(x2)
Cond_f2794_0_power_Return2(x1, x2, x3, x4) → Cond_f2794_0_power_Return2(x1, x4)

Filtered unneeded terms:

Cond_f2794_0_power_Return(x1, x2) → Cond_f2794_0_power_Return(x1)
Cond_f2794_0_power_Return1(x1, x2) → Cond_f2794_0_power_Return1(x1)

Prepared 4 rules for path length conversion:

P rules:
f2794_0_power_Return(x0) → f2825_0_fact_Load(x0)
f2794_0_power_Return(x0) → f2974_1_exp_Load(-(x0, 1)) | >(x0, 0)
f2794_0_power_Return(x0) → f2748_0_power_Load(-(x0, 1)) | >(x0, 1)
f2794_0_power_Return(x0) → f2794_0_power_Return(-(x0, 1)) | >(x0, 1)

Finished conversion. Obtained 1 rules.

P rules:
f2794_0_power_Return(x3) → f2794_0_power_Return(-(x3, 1)) | >(x3, 1)

(17) Obligation:

Rules:
f2794_0_power_Return(x3) → f2794_0_power_Return(-(x3, 1)) | >(x3, 1)

(18) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f2794_0_power_Return(x2)] = x2

Therefore the following rule(s) have been dropped:

f2794_0_power_Return(x0) → f2794_0_power_Return(-(x0, 1)) | >(x0, 1)

(19) YES

(20) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: TaylorSeriesRec.cos(II)I
SCC calls the following helper methods: TaylorSeriesRec.power(II)I, TaylorSeriesRec.fact(I)I, TaylorSeriesRec.cos(II)I
Performed SCC analyses:

Used field analysis yielded the following read fields:
Marker field analysis yielded the following relations that could be markers:

(21) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 37 IRules

P rules:
f2642_0_power_Return(EOS, i523, i523, i523) → f2651_0_cos_Load(EOS, i523, i523)
f2651_0_cos_Load(EOS, i523, i523) → f2659_0_cos_ConstantStackPush(EOS, i523, i523)
f2659_0_cos_ConstantStackPush(EOS, i523, i523) → f2667_0_cos_Load(EOS, i523, i523, 2)
f2667_0_cos_Load(EOS, i523, i523, matching1) → f2674_0_cos_IntArithmetic(EOS, i523, i523, 2, i523) | =(matching1, 2)
f2674_0_cos_IntArithmetic(EOS, i523, i523, matching1, i523) → f2682_0_cos_InvokeMethod(EOS, i523, i523, *(2, i523)) | &&(>=(i523, 1), =(matching1, 2))
f2682_0_cos_InvokeMethod(EOS, i523, i523, i545) → f2691_0_power_Load(EOS, i545, i545)
f2682_0_cos_InvokeMethod(EOS, i523, i523, i545) → f2691_1_power_Load(EOS, i523, i523, i545, i545)
f2691_0_power_Load(EOS, i545, i545) → f2698_0_power_Load(EOS, i545, i545)
f2749_0_power_Return(EOS, i523, i523, i562) → f2766_0_cos_IntArithmetic(EOS, i523, i523)
f2766_0_cos_IntArithmetic(EOS, i523, i523) → f2784_0_cos_ConstantStackPush(EOS, i523, i523)
f2784_0_cos_ConstantStackPush(EOS, i523, i523) → f2790_0_cos_Load(EOS, i523, i523, 2)
f2790_0_cos_Load(EOS, i523, i523, matching1) → f2796_0_cos_IntArithmetic(EOS, i523, i523, 2, i523) | =(matching1, 2)
f2796_0_cos_IntArithmetic(EOS, i523, i523, matching1, i523) → f2803_0_cos_InvokeMethod(EOS, i523, i523, *(2, i523)) | &&(>=(i523, 1), =(matching1, 2))
f2803_0_cos_InvokeMethod(EOS, i523, i523, i591) → f2809_0_fact_Load(EOS, i591, i591)
f2803_0_cos_InvokeMethod(EOS, i523, i523, i591) → f2809_1_fact_Load(EOS, i523, i523, i591, i591)
f2809_0_fact_Load(EOS, i591, i591) → f2820_0_fact_Load(EOS, i591, i591)
f2893_0_fact_Return(EOS, i523, i523, i603) → f2898_0_cos_IntArithmetic(EOS, i523, i523)
f2898_0_cos_IntArithmetic(EOS, i523, i523) → f2913_0_cos_Load(EOS, i523, i523)
f2913_0_cos_Load(EOS, i523, i523) → f2920_0_cos_Load(EOS, i523, i523)
f2920_0_cos_Load(EOS, i523, i523) → f2926_0_cos_ConstantStackPush(EOS, i523, i523)
f2926_0_cos_ConstantStackPush(EOS, i523, i523) → f2942_0_cos_IntArithmetic(EOS, i523, i523, 1)
f2942_0_cos_IntArithmetic(EOS, i523, i523, matching1) → f2949_0_cos_InvokeMethod(EOS, i523, -(i523, 1)) | &&(>(i523, 0), =(matching1, 1))
f2949_0_cos_InvokeMethod(EOS, i523, i626) → f2962_0_cos_Load(EOS, i626, i626)
f2949_0_cos_InvokeMethod(EOS, i523, i626) → f2962_1_cos_Load(EOS, i523, i626, i626)
f2962_0_cos_Load(EOS, i626, i626) → f2976_0_cos_Load(EOS, i626, i626)
f2976_0_cos_Load(EOS, i626, i626) → f2520_0_cos_Load(EOS, i626, i626)
f2520_0_cos_Load(EOS, i495, i495) → f2537_0_cos_GT(EOS, i495, i495, i495)
f2537_0_cos_GT(EOS, i505, i505, i505) → f2543_0_cos_GT(EOS, i505, i505, i505)
f2543_0_cos_GT(EOS, i505, i505, i505) → f2551_0_cos_ConstantStackPush(EOS, i505, i505) | >(i505, 0)
f2551_0_cos_ConstantStackPush(EOS, i505, i505) → f2561_0_cos_Load(EOS, i505, i505)
f2561_0_cos_Load(EOS, i505, i505) → f2570_0_cos_InvokeMethod(EOS, i505, i505, i505)
f2570_0_cos_InvokeMethod(EOS, i505, i505, i505) → f2587_0_power_Load(EOS, i505, i505)
f2570_0_cos_InvokeMethod(EOS, i505, i505, i505) → f2587_1_power_Load(EOS, i505, i505, i505, i505)
f2587_0_power_Load(EOS, i505, i505) → f2590_0_power_Load(EOS, i505, i505)
f2691_1_power_Load(EOS, i523, i523, i562, i562) → f2749_0_power_Return(EOS, i523, i523, i562)
f2809_1_fact_Load(EOS, i523, i523, i603, i603) → f2893_0_fact_Return(EOS, i523, i523, i603)
f2587_1_power_Load(EOS, i523, i523, i523, i523) → f2642_0_power_Return(EOS, i523, i523, i523)

Combined rules. Obtained 5 IRules

P rules:
f2642_0_power_Return(EOS, x0, x0, x0) → f2698_0_power_Load(EOS, *(2, x0), *(2, x0)) | >(+(x0, 1), 1)
f2642_0_power_Return(EOS, x0, x0, x0) → f2820_0_fact_Load(EOS, *(2, x0), *(2, x0)) | >(+(x0, 1), 1)
f2642_0_power_Return(EOS, x0, x0, x0) → f2962_1_cos_Load(EOS, x0, -(x0, 1), -(x0, 1)) | >(+(x0, 1), 1)
f2642_0_power_Return(EOS, x0, x0, x0) → f2590_0_power_Load(EOS, -(x0, 1), -(x0, 1)) | >(x0, 1)
f2642_0_power_Return(EOS, x0, x0, x0) → f2642_0_power_Return(EOS, -(x0, 1), -(x0, 1), -(x0, 1)) | >(x0, 1)

Filtered ground terms:

f2642_0_power_Return(x1, x2, x3, x4) → f2642_0_power_Return(x2, x3, x4)
Cond_f2642_0_power_Return(x1, x2, x3, x4, x5) → Cond_f2642_0_power_Return(x1, x3, x4, x5)
f2698_0_power_Load(x1, x2, x3) → f2698_0_power_Load(x2, x3)
Cond_f2642_0_power_Return1(x1, x2, x3, x4, x5) → Cond_f2642_0_power_Return1(x1, x3, x4, x5)
f2820_0_fact_Load(x1, x2, x3) → f2820_0_fact_Load(x2, x3)
Cond_f2642_0_power_Return2(x1, x2, x3, x4, x5) → Cond_f2642_0_power_Return2(x1, x3, x4, x5)
f2962_1_cos_Load(x1, x2, x3, x4) → f2962_1_cos_Load(x2, x3, x4)
Cond_f2642_0_power_Return3(x1, x2, x3, x4, x5) → Cond_f2642_0_power_Return3(x1, x3, x4, x5)
f2590_0_power_Load(x1, x2, x3) → f2590_0_power_Load(x2, x3)
Cond_f2642_0_power_Return4(x1, x2, x3, x4, x5) → Cond_f2642_0_power_Return4(x1, x3, x4, x5)

Filtered duplicate terms:

f2642_0_power_Return(x1, x2, x3) → f2642_0_power_Return(x3)
Cond_f2642_0_power_Return(x1, x2, x3, x4) → Cond_f2642_0_power_Return(x1, x4)
f2698_0_power_Load(x1, x2) → f2698_0_power_Load(x2)
Cond_f2642_0_power_Return1(x1, x2, x3, x4) → Cond_f2642_0_power_Return1(x1, x4)
f2820_0_fact_Load(x1, x2) → f2820_0_fact_Load(x2)
Cond_f2642_0_power_Return2(x1, x2, x3, x4) → Cond_f2642_0_power_Return2(x1, x4)
f2962_1_cos_Load(x1, x2, x3) → f2962_1_cos_Load(x3)
Cond_f2642_0_power_Return3(x1, x2, x3, x4) → Cond_f2642_0_power_Return3(x1, x4)
f2590_0_power_Load(x1, x2) → f2590_0_power_Load(x2)
Cond_f2642_0_power_Return4(x1, x2, x3, x4) → Cond_f2642_0_power_Return4(x1, x4)

Filtered unneeded terms:

Cond_f2642_0_power_Return(x1, x2) → Cond_f2642_0_power_Return(x1)
Cond_f2642_0_power_Return1(x1, x2) → Cond_f2642_0_power_Return1(x1)
Cond_f2642_0_power_Return2(x1, x2) → Cond_f2642_0_power_Return2(x1)
Cond_f2642_0_power_Return3(x1, x2) → Cond_f2642_0_power_Return3(x1)

Prepared 5 rules for path length conversion:

P rules:
f2642_0_power_Return(x0) → f2698_0_power_Load(*(2, x0)) | >(+(x0, 1), 1)
f2642_0_power_Return(x0) → f2820_0_fact_Load(*(2, x0)) | >(+(x0, 1), 1)
f2642_0_power_Return(x0) → f2962_1_cos_Load(-(x0, 1)) | >(+(x0, 1), 1)
f2642_0_power_Return(x0) → f2590_0_power_Load(-(x0, 1)) | >(x0, 1)
f2642_0_power_Return(x0) → f2642_0_power_Return(-(x0, 1)) | >(x0, 1)

Finished conversion. Obtained 1 rules.

P rules:
f2642_0_power_Return(x4) → f2642_0_power_Return(-(x4, 1)) | >(x4, 1)

(22) Obligation:

Rules:
f2642_0_power_Return(x4) → f2642_0_power_Return(-(x4, 1)) | >(x4, 1)

(23) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f2642_0_power_Return(x2)] = x2

Therefore the following rule(s) have been dropped:

f2642_0_power_Return(x0) → f2642_0_power_Return(-(x0, 1)) | >(x0, 1)

(24) YES

(25) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: TaylorSeriesRec.sin(II)I
SCC calls the following helper methods: TaylorSeriesRec.power(II)I, TaylorSeriesRec.fact(I)I, TaylorSeriesRec.sin(II)I
Performed SCC analyses:

Used field analysis yielded the following read fields:
Marker field analysis yielded the following relations that could be markers:

(26) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 41 IRules

P rules:
f2436_0_sin_GT(EOS, i481, i481, i481) → f2452_0_sin_GT(EOS, i481, i481, i481)
f2452_0_sin_GT(EOS, i481, i481, i481) → f2474_0_sin_ConstantStackPush(EOS, i481, i481) | >(i481, 0)
f2474_0_sin_ConstantStackPush(EOS, i481, i481) → f2486_0_sin_Load(EOS, i481, i481)
f2486_0_sin_Load(EOS, i481, i481) → f2494_0_sin_InvokeMethod(EOS, i481, i481, i481)
f2494_0_sin_InvokeMethod(EOS, i481, i481, i481) → f2508_0_power_Load(EOS, i481, i481)
f2494_0_sin_InvokeMethod(EOS, i481, i481, i481) → f2508_1_power_Load(EOS, i481, i481, i481, i481)
f2508_0_power_Load(EOS, i481, i481) → f2514_0_power_Load(EOS, i481, i481)
f2544_0_power_Return(EOS, i503, i503, i503) → f2548_0_sin_Load(EOS, i503, i503)
f2548_0_sin_Load(EOS, i503, i503) → f2553_0_sin_ConstantStackPush(EOS, i503, i503)
f2553_0_sin_ConstantStackPush(EOS, i503, i503) → f2557_0_sin_Load(EOS, i503, i503, 2)
f2557_0_sin_Load(EOS, i503, i503, matching1) → f2562_0_sin_IntArithmetic(EOS, i503, i503, 2, i503) | =(matching1, 2)
f2562_0_sin_IntArithmetic(EOS, i503, i503, matching1, i503) → f2567_0_sin_ConstantStackPush(EOS, i503, i503, *(2, i503)) | &&(>=(i503, 1), =(matching1, 2))
f2567_0_sin_ConstantStackPush(EOS, i503, i503, i506) → f2572_0_sin_IntArithmetic(EOS, i503, i503, i506, 1)
f2572_0_sin_IntArithmetic(EOS, i503, i503, i506, matching1) → f2583_0_sin_InvokeMethod(EOS, i503, i503, +(i506, 1)) | &&(>(i506, 0), =(matching1, 1))
f2583_0_sin_InvokeMethod(EOS, i503, i503, i515) → f2588_0_power_Load(EOS, i515, i515)
f2583_0_sin_InvokeMethod(EOS, i503, i503, i515) → f2588_1_power_Load(EOS, i503, i503, i515, i515)
f2588_0_power_Load(EOS, i515, i515) → f2592_0_power_Load(EOS, i515, i515)
f2643_0_power_Return(EOS, i503, i503, i535) → f2653_0_sin_IntArithmetic(EOS, i503, i503)
f2653_0_sin_IntArithmetic(EOS, i503, i503) → f2661_0_sin_ConstantStackPush(EOS, i503, i503)
f2661_0_sin_ConstantStackPush(EOS, i503, i503) → f2669_0_sin_Load(EOS, i503, i503, 2)
f2669_0_sin_Load(EOS, i503, i503, matching1) → f2676_0_sin_IntArithmetic(EOS, i503, i503, 2, i503) | =(matching1, 2)
f2676_0_sin_IntArithmetic(EOS, i503, i503, matching1, i503) → f2684_0_sin_ConstantStackPush(EOS, i503, i503, *(2, i503)) | &&(>=(i503, 1), =(matching1, 2))
f2684_0_sin_ConstantStackPush(EOS, i503, i503, i546) → f2693_0_sin_IntArithmetic(EOS, i503, i503, i546, 1)
f2693_0_sin_IntArithmetic(EOS, i503, i503, i546, matching1) → f2700_0_sin_InvokeMethod(EOS, i503, i503, +(i546, 1)) | &&(>(i546, 0), =(matching1, 1))
f2700_0_sin_InvokeMethod(EOS, i503, i503, i548) → f2705_0_fact_Load(EOS, i548, i548)
f2700_0_sin_InvokeMethod(EOS, i503, i503, i548) → f2705_1_fact_Load(EOS, i503, i503, i548, i548)
f2705_0_fact_Load(EOS, i548, i548) → f2730_0_fact_Load(EOS, i548, i548)
f2785_0_fact_Return(EOS, i503, i503, i575) → f2791_0_sin_IntArithmetic(EOS, i503, i503)
f2791_0_sin_IntArithmetic(EOS, i503, i503) → f2798_0_sin_Load(EOS, i503, i503)
f2798_0_sin_Load(EOS, i503, i503) → f2805_0_sin_Load(EOS, i503, i503)
f2805_0_sin_Load(EOS, i503, i503) → f2811_0_sin_ConstantStackPush(EOS, i503, i503)
f2811_0_sin_ConstantStackPush(EOS, i503, i503) → f2821_0_sin_IntArithmetic(EOS, i503, i503, 1)
f2821_0_sin_IntArithmetic(EOS, i503, i503, matching1) → f2827_0_sin_InvokeMethod(EOS, i503, -(i503, 1)) | &&(>(i503, 0), =(matching1, 1))
f2827_0_sin_InvokeMethod(EOS, i503, i595) → f2849_0_sin_Load(EOS, i595, i595)
f2827_0_sin_InvokeMethod(EOS, i503, i595) → f2849_1_sin_Load(EOS, i503, i595, i595)
f2849_0_sin_Load(EOS, i595, i595) → f2886_0_sin_Load(EOS, i595, i595)
f2886_0_sin_Load(EOS, i595, i595) → f2418_0_sin_Load(EOS, i595, i595)
f2418_0_sin_Load(EOS, i467, i467) → f2436_0_sin_GT(EOS, i467, i467, i467)
f2508_1_power_Load(EOS, i503, i503, i503, i503) → f2544_0_power_Return(EOS, i503, i503, i503)
f2588_1_power_Load(EOS, i503, i503, i535, i535) → f2643_0_power_Return(EOS, i503, i503, i535)
f2705_1_fact_Load(EOS, i503, i503, i575, i575) → f2785_0_fact_Return(EOS, i503, i503, i575)

Combined rules. Obtained 5 IRules

P rules:
f2785_0_fact_Return(EOS, x0, x0, x1) → f2849_1_sin_Load(EOS, x0, -(x0, 1), -(x0, 1)) | >(x0, 0)
f2785_0_fact_Return(EOS, x0, x0, x1) → f2514_0_power_Load(EOS, -(x0, 1), -(x0, 1)) | >(x0, 1)
f2785_0_fact_Return(EOS, x0, x0, x1) → f2592_0_power_Load(EOS, +(*(2, -(x0, 1)), 1), +(*(2, -(x0, 1)), 1)) | &&(>(+(x0, 1), 2), >(*(2, -(x0, 1)), 0))
f2785_0_fact_Return(EOS, x0, x0, x1) → f2730_0_fact_Load(EOS, +(*(2, -(x0, 1)), 1), +(*(2, -(x0, 1)), 1)) | &&(>(+(x0, 1), 2), >(*(2, -(x0, 1)), 0))
f2785_0_fact_Return(EOS, x0, x0, x1) → f2785_0_fact_Return(EOS, -(x0, 1), -(x0, 1), +(*(2, -(x0, 1)), 1)) | &&(>(+(x0, 1), 2), >(*(2, -(x0, 1)), 0))

Filtered ground terms:

f2785_0_fact_Return(x1, x2, x3, x4) → f2785_0_fact_Return(x2, x3, x4)
Cond_f2785_0_fact_Return(x1, x2, x3, x4, x5) → Cond_f2785_0_fact_Return(x1, x3, x4, x5)
f2849_1_sin_Load(x1, x2, x3, x4) → f2849_1_sin_Load(x2, x3, x4)
Cond_f2785_0_fact_Return1(x1, x2, x3, x4, x5) → Cond_f2785_0_fact_Return1(x1, x3, x4, x5)
f2514_0_power_Load(x1, x2, x3) → f2514_0_power_Load(x2, x3)
Cond_f2785_0_fact_Return2(x1, x2, x3, x4, x5) → Cond_f2785_0_fact_Return2(x1, x3, x4, x5)
f2592_0_power_Load(x1, x2, x3) → f2592_0_power_Load(x2, x3)
Cond_f2785_0_fact_Return3(x1, x2, x3, x4, x5) → Cond_f2785_0_fact_Return3(x1, x3, x4, x5)
f2730_0_fact_Load(x1, x2, x3) → f2730_0_fact_Load(x2, x3)
Cond_f2785_0_fact_Return4(x1, x2, x3, x4, x5) → Cond_f2785_0_fact_Return4(x1, x3, x4, x5)

Filtered duplicate terms:

f2785_0_fact_Return(x1, x2, x3) → f2785_0_fact_Return(x2, x3)
Cond_f2785_0_fact_Return(x1, x2, x3, x4) → Cond_f2785_0_fact_Return(x1, x3, x4)
f2849_1_sin_Load(x1, x2, x3) → f2849_1_sin_Load(x3)
Cond_f2785_0_fact_Return1(x1, x2, x3, x4) → Cond_f2785_0_fact_Return1(x1, x3, x4)
f2514_0_power_Load(x1, x2) → f2514_0_power_Load(x2)
Cond_f2785_0_fact_Return2(x1, x2, x3, x4) → Cond_f2785_0_fact_Return2(x1, x3, x4)
f2592_0_power_Load(x1, x2) → f2592_0_power_Load(x2)
Cond_f2785_0_fact_Return3(x1, x2, x3, x4) → Cond_f2785_0_fact_Return3(x1, x3, x4)
f2730_0_fact_Load(x1, x2) → f2730_0_fact_Load(x2)
Cond_f2785_0_fact_Return4(x1, x2, x3, x4) → Cond_f2785_0_fact_Return4(x1, x3, x4)

Filtered unneeded terms:

Cond_f2785_0_fact_Return(x1, x2, x3) → Cond_f2785_0_fact_Return(x1)
Cond_f2785_0_fact_Return1(x1, x2, x3) → Cond_f2785_0_fact_Return1(x1)
Cond_f2785_0_fact_Return2(x1, x2, x3) → Cond_f2785_0_fact_Return2(x1)
Cond_f2785_0_fact_Return3(x1, x2, x3) → Cond_f2785_0_fact_Return3(x1)
Cond_f2785_0_fact_Return4(x1, x2, x3) → Cond_f2785_0_fact_Return4(x1, x2)
f2785_0_fact_Return(x1, x2) → f2785_0_fact_Return(x1)

Prepared 5 rules for path length conversion:

P rules:
f2785_0_fact_Return(x0) → f2849_1_sin_Load(-(x0, 1)) | >(x0, 0)
f2785_0_fact_Return(x0) → f2514_0_power_Load(-(x0, 1)) | >(x0, 1)
f2785_0_fact_Return(x0) → f2592_0_power_Load(+(*(2, -(x0, 1)), 1)) | &&(>(+(x0, 1), 2), >(*(2, -(x0, 1)), 0))
f2785_0_fact_Return(x0) → f2730_0_fact_Load(+(*(2, -(x0, 1)), 1)) | &&(>(+(x0, 1), 2), >(*(2, -(x0, 1)), 0))
f2785_0_fact_Return(x0) → f2785_0_fact_Return(-(x0, 1)) | &&(>(+(x0, 1), 2), >(*(2, -(x0, 1)), 0))

Finished conversion. Obtained 1 rules.

P rules:
f2785_0_fact_Return(x4) → f2785_0_fact_Return(-(x4, 1)) | &&(>(*(2, x4), 2), >(x4, 1))

(27) Obligation:

Rules:
f2785_0_fact_Return(x4) → f2785_0_fact_Return(-(x4, 1)) | &&(>(*(2, x4), 2), >(x4, 1))

(28) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f2785_0_fact_Return(x2)] = x2

Therefore the following rule(s) have been dropped:

f2785_0_fact_Return(x0) → f2785_0_fact_Return(-(x0, 1)) | &&(>(*(2, x0), 2), >(x0, 1))

(29) YES

(30) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: TaylorSeriesRec.main([Ljava/lang/String;)V
SCC calls the following helper methods: TaylorSeriesRec.exp(II)I, TaylorSeriesRec.cos(II)I, TaylorSeriesRec.sin(II)I, TaylorSeriesRec.power(II)I, TaylorSeriesRec.fact(I)I
Performed SCC analyses:

Used field analysis yielded the following read fields:
Marker field analysis yielded the following relations that could be markers:

(31) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 92 IRules

P rules:
f3228_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i728) → f3230_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i728, java.lang.Object(ARRAY(i9)))
f3230_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i728, java.lang.Object(ARRAY(i9))) → f3232_0_main_GE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i728, i9) | >=(i9, 0)
f3232_0_main_GE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i728, i9) → f3235_0_main_GE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i728, i9)
f3235_0_main_GE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i728, i9) → f3239_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728) | <(i728, i9)
f3239_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728) → f3242_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i728)
f3242_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i728) → f3245_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i728, 2)
f3245_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i728, matching1) → f3248_0_main_NE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, %(i728, 2)) | =(matching1, 2)
f3248_0_main_NE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, matching1) → f3250_0_main_NE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, 1) | =(matching1, 1)
f3248_0_main_NE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, matching1) → f3251_0_main_NE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, 0) | =(matching1, 0)
f3250_0_main_NE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, matching1) → f3253_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728) | &&(>(1, 0), =(matching1, 1))
f3253_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728) → f3257_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i728)
f3257_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i728) → f3261_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i728, 3)
f3261_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i728, matching1) → f3265_0_main_NE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, %(i728, 3)) | =(matching1, 3)
f3265_0_main_NE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i763) → f3268_0_main_NE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i763)
f3265_0_main_NE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, matching1) → f3269_0_main_NE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, 0) | =(matching1, 0)
f3268_0_main_NE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i763) → f3272_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728) | >(i763, 0)
f3272_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728) → f3277_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i728)
f3277_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i728) → f3281_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i728, 5)
f3281_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i728, matching1) → f3301_0_main_NE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, %(i728, 5)) | =(matching1, 5)
f3301_0_main_NE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i779) → f3307_0_main_NE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i779)
f3301_0_main_NE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, matching1) → f3308_0_main_NE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, 0) | =(matching1, 0)
f3307_0_main_NE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i779) → f3316_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728) | >(i779, 0)
f3316_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728) → f3326_0_main_Store(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, 0)
f3326_0_main_Store(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, matching1) → f3334_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, 0) | =(matching1, 0)
f3334_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, matching1) → f3416_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, 0) | =(matching1, 0)
f3416_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i808) → f3499_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i808)
f3499_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i841) → f3529_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i841)
f3529_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i850) → f3549_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i850)
f3549_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i853) → f3552_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i853, i853)
f3552_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i853, i853) → f3555_0_main_GE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i853, i853, 100)
f3555_0_main_GE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i857, i857, matching1) → f3557_0_main_GE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i857, i857, 100) | =(matching1, 100)
f3555_0_main_GE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i858, i858, matching1) → f3558_0_main_GE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i858, i858, 100) | =(matching1, 100)
f3557_0_main_GE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i857, i857, matching1) → f3560_0_main_Inc(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i857) | &&(<(i857, 100), =(matching1, 100))
f3560_0_main_Inc(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i857) → f3570_0_main_JMP(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, +(i857, 1)) | >=(i857, 0)
f3570_0_main_JMP(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i863) → f3577_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i863)
f3577_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i863) → f3549_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i863)
f3558_0_main_GE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i858, i858, matching1) → f3566_0_main_Inc(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728) | &&(>=(i858, 100), =(matching1, 100))
f3566_0_main_Inc(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728) → f3572_0_main_JMP(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), +(i728, 1)) | >=(i728, 0)
f3572_0_main_JMP(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i864) → f3582_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i864)
f3582_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i864) → f3161_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i864)
f3161_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728) → f3228_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i728)
f3308_0_main_NE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, matching1) → f3318_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728) | =(matching1, 0)
f3318_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728) → f3328_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, java.lang.Object(ARRAY(i9)))
f3328_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, java.lang.Object(ARRAY(i9))) → f3336_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i9) | >=(i9, 0)
f3336_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i9) → f3361_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i9, i728)
f3361_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i9, i728) → f3375_0_exp_Load(EOS, i9, i728, i9, i728)
f3361_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i9, i728) → f3375_1_exp_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i9, i728, i9, i728)
f3375_0_exp_Load(EOS, i9, i728, i9, i728) → f3384_0_exp_Load(EOS, i9, i728, i9, i728)
f3450_0_exp_Return(EOS, java.lang.Object(ARRAY(i818)), java.lang.Object(ARRAY(i818)), matching1, i818, matching2, i818, matching3) → f3463_0_main_StackPop(EOS, java.lang.Object(ARRAY(i818)), java.lang.Object(ARRAY(i818)), 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f3463_0_main_StackPop(EOS, java.lang.Object(ARRAY(i818)), java.lang.Object(ARRAY(i818)), matching1) → f3470_0_main_JMP(EOS, java.lang.Object(ARRAY(i818)), java.lang.Object(ARRAY(i818)), 0) | =(matching1, 0)
f3470_0_main_JMP(EOS, java.lang.Object(ARRAY(i818)), java.lang.Object(ARRAY(i818)), matching1) → f3479_0_main_Inc(EOS, java.lang.Object(ARRAY(i818)), java.lang.Object(ARRAY(i818)), 0) | =(matching1, 0)
f3479_0_main_Inc(EOS, java.lang.Object(ARRAY(i818)), java.lang.Object(ARRAY(i818)), matching1) → f3566_0_main_Inc(EOS, java.lang.Object(ARRAY(i818)), java.lang.Object(ARRAY(i818)), 0) | =(matching1, 0)
f3451_0_exp_Return(EOS, java.lang.Object(ARRAY(i826)), java.lang.Object(ARRAY(i826)), i824, i826, i824) → f3466_0_main_StackPop(EOS, java.lang.Object(ARRAY(i826)), java.lang.Object(ARRAY(i826)), i824)
f3466_0_main_StackPop(EOS, java.lang.Object(ARRAY(i826)), java.lang.Object(ARRAY(i826)), i824) → f3472_0_main_JMP(EOS, java.lang.Object(ARRAY(i826)), java.lang.Object(ARRAY(i826)), i824)
f3472_0_main_JMP(EOS, java.lang.Object(ARRAY(i826)), java.lang.Object(ARRAY(i826)), i824) → f3486_0_main_Inc(EOS, java.lang.Object(ARRAY(i826)), java.lang.Object(ARRAY(i826)), i824)
f3486_0_main_Inc(EOS, java.lang.Object(ARRAY(i826)), java.lang.Object(ARRAY(i826)), i824) → f3566_0_main_Inc(EOS, java.lang.Object(ARRAY(i826)), java.lang.Object(ARRAY(i826)), i824)
f3269_0_main_NE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, matching1) → f3274_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728) | =(matching1, 0)
f3274_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728) → f3279_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, java.lang.Object(ARRAY(i9)))
f3279_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, java.lang.Object(ARRAY(i9))) → f3283_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i9) | >=(i9, 0)
f3283_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i9) → f3303_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i9, i728)
f3303_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i9, i728) → f3310_0_cos_Load(EOS, i9, i728, i9, i728)
f3303_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i9, i728) → f3310_1_cos_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i9, i728, i9, i728)
f3310_0_cos_Load(EOS, i9, i728, i9, i728) → f3320_0_cos_Load(EOS, i9, i728, i9, i728)
f3362_0_cos_Return(EOS, java.lang.Object(ARRAY(i786)), java.lang.Object(ARRAY(i786)), matching1, i786, matching2, i786, matching3) → f3377_0_main_StackPop(EOS, java.lang.Object(ARRAY(i786)), java.lang.Object(ARRAY(i786)), 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f3377_0_main_StackPop(EOS, java.lang.Object(ARRAY(i786)), java.lang.Object(ARRAY(i786)), matching1) → f3385_0_main_JMP(EOS, java.lang.Object(ARRAY(i786)), java.lang.Object(ARRAY(i786)), 0) | =(matching1, 0)
f3385_0_main_JMP(EOS, java.lang.Object(ARRAY(i786)), java.lang.Object(ARRAY(i786)), matching1) → f3394_0_main_Inc(EOS, java.lang.Object(ARRAY(i786)), java.lang.Object(ARRAY(i786)), 0) | =(matching1, 0)
f3394_0_main_Inc(EOS, java.lang.Object(ARRAY(i786)), java.lang.Object(ARRAY(i786)), matching1) → f3479_0_main_Inc(EOS, java.lang.Object(ARRAY(i786)), java.lang.Object(ARRAY(i786)), 0) | =(matching1, 0)
f3364_0_cos_Return(EOS, java.lang.Object(ARRAY(i794)), java.lang.Object(ARRAY(i794)), i792, i794, i792) → f3380_0_main_StackPop(EOS, java.lang.Object(ARRAY(i794)), java.lang.Object(ARRAY(i794)), i792)
f3380_0_main_StackPop(EOS, java.lang.Object(ARRAY(i794)), java.lang.Object(ARRAY(i794)), i792) → f3388_0_main_JMP(EOS, java.lang.Object(ARRAY(i794)), java.lang.Object(ARRAY(i794)), i792)
f3388_0_main_JMP(EOS, java.lang.Object(ARRAY(i794)), java.lang.Object(ARRAY(i794)), i792) → f3402_0_main_Inc(EOS, java.lang.Object(ARRAY(i794)), java.lang.Object(ARRAY(i794)), i792)
f3402_0_main_Inc(EOS, java.lang.Object(ARRAY(i794)), java.lang.Object(ARRAY(i794)), i792) → f3486_0_main_Inc(EOS, java.lang.Object(ARRAY(i794)), java.lang.Object(ARRAY(i794)), i792)
f3251_0_main_NE(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, matching1) → f3255_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728) | =(matching1, 0)
f3255_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728) → f3259_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, java.lang.Object(ARRAY(i9)))
f3259_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, java.lang.Object(ARRAY(i9))) → f3262_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i9) | >=(i9, 0)
f3262_0_main_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i9) → f3266_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i9, i728)
f3266_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i9, i728) → f3271_0_sin_Load(EOS, i9, i728, i9, i728)
f3266_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i9, i728) → f3271_1_sin_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i728, i9, i728, i9, i728)
f3271_0_sin_Load(EOS, i9, i728, i9, i728) → f3276_0_sin_Load(EOS, i9, i728, i9, i728)
f3304_0_sin_Return(EOS, java.lang.Object(ARRAY(i768)), java.lang.Object(ARRAY(i768)), matching1, i768, matching2, i768, matching3, i768) → f3312_0_main_StackPop(EOS, java.lang.Object(ARRAY(i768)), java.lang.Object(ARRAY(i768)), 0, i768) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f3312_0_main_StackPop(EOS, java.lang.Object(ARRAY(i768)), java.lang.Object(ARRAY(i768)), matching1, i768) → f3321_0_main_JMP(EOS, java.lang.Object(ARRAY(i768)), java.lang.Object(ARRAY(i768)), 0) | =(matching1, 0)
f3321_0_main_JMP(EOS, java.lang.Object(ARRAY(i768)), java.lang.Object(ARRAY(i768)), matching1) → f3330_0_main_Inc(EOS, java.lang.Object(ARRAY(i768)), java.lang.Object(ARRAY(i768)), 0) | =(matching1, 0)
f3330_0_main_Inc(EOS, java.lang.Object(ARRAY(i768)), java.lang.Object(ARRAY(i768)), matching1) → f3394_0_main_Inc(EOS, java.lang.Object(ARRAY(i768)), java.lang.Object(ARRAY(i768)), 0) | =(matching1, 0)
f3305_0_sin_Return(EOS, java.lang.Object(ARRAY(i775)), java.lang.Object(ARRAY(i775)), i773, i775, i773, i771) → f3314_0_main_StackPop(EOS, java.lang.Object(ARRAY(i775)), java.lang.Object(ARRAY(i775)), i773, i771)
f3314_0_main_StackPop(EOS, java.lang.Object(ARRAY(i775)), java.lang.Object(ARRAY(i775)), i773, i771) → f3324_0_main_JMP(EOS, java.lang.Object(ARRAY(i775)), java.lang.Object(ARRAY(i775)), i773)
f3324_0_main_JMP(EOS, java.lang.Object(ARRAY(i775)), java.lang.Object(ARRAY(i775)), i773) → f3332_0_main_Inc(EOS, java.lang.Object(ARRAY(i775)), java.lang.Object(ARRAY(i775)), i773)
f3332_0_main_Inc(EOS, java.lang.Object(ARRAY(i775)), java.lang.Object(ARRAY(i775)), i773) → f3402_0_main_Inc(EOS, java.lang.Object(ARRAY(i775)), java.lang.Object(ARRAY(i775)), i773)
f3375_1_exp_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), matching1, i818, matching2, i818, matching3) → f3450_0_exp_Return(EOS, java.lang.Object(ARRAY(i818)), java.lang.Object(ARRAY(i818)), 0, i818, 0, i818, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f3375_1_exp_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i824, i826, i824, i826, i824) → f3451_0_exp_Return(EOS, java.lang.Object(ARRAY(i826)), java.lang.Object(ARRAY(i826)), i824, i826, i824)
f3310_1_cos_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), matching1, i786, matching2, i786, matching3) → f3362_0_cos_Return(EOS, java.lang.Object(ARRAY(i786)), java.lang.Object(ARRAY(i786)), 0, i786, 0, i786, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f3310_1_cos_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i792, i794, i792, i794, i792) → f3364_0_cos_Return(EOS, java.lang.Object(ARRAY(i794)), java.lang.Object(ARRAY(i794)), i792, i794, i792)
f3271_1_sin_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), matching1, i768, matching2, i768, matching3) → f3304_0_sin_Return(EOS, java.lang.Object(ARRAY(i768)), java.lang.Object(ARRAY(i768)), 0, i768, 0, i768, 0, i768) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f3271_1_sin_Load(EOS, java.lang.Object(ARRAY(i9)), java.lang.Object(ARRAY(i9)), i773, i775, i773, i775, i773) → f3305_0_sin_Return(EOS, java.lang.Object(ARRAY(i775)), java.lang.Object(ARRAY(i775)), i773, i775, i773, i771)

Combined rules. Obtained 10 IRules

P rules:
f3228_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x1) → f3555_0_main_GE(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, 0, 0, 100) | &&(&&(&&(&&(<(x1, x0), >(%(x1, 5), 0)), >(%(x1, 3), 0)), >(+(x0, 1), 0)), =(%(x1, 2), 1))
f3555_0_main_GE(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x2, 100) → f3555_0_main_GE(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, +(x2, 1), +(x2, 1), 100) | &&(<(x2, 100), >(+(x2, 1), 0))
f3555_0_main_GE(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x2, 100) → f3228_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), +(x1, 1), +(x1, 1)) | &&(>(+(x1, 1), 0), >(+(x2, 1), 100))
f3228_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x1) → f3384_0_exp_Load(EOS, x0, x1, x0, x1) | &&(&&(&&(&&(<(x1, x0), =(%(x1, 5), 0)), >(%(x1, 3), 0)), =(%(x1, 2), 1)), >(+(x0, 1), 0))
f3228_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x1) → f3320_0_cos_Load(EOS, x0, x1, x0, x1) | &&(&&(&&(<(x1, x0), =(%(x1, 3), 0)), =(%(x1, 2), 1)), >(+(x0, 1), 0))
f3228_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x1) → f3276_0_sin_Load(EOS, x0, x1, x0, x1) | &&(&&(<(x1, x0), =(%(x1, 2), 0)), >(+(x0, 1), 0))
f3228_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x1) → f3228_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), +(x1, 1), +(x1, 1)) | &&(&&(&&(&&(&&(>(+(x1, 1), 0), <(x1, x0)), =(%(x1, 5), 0)), >(%(x1, 3), 0)), =(%(x1, 2), 1)), >(+(x0, 1), 0))
f3228_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x1) → f3228_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), +(x1, 1), +(x1, 1)) | &&(&&(&&(&&(>(+(x1, 1), 0), <(x1, x0)), =(%(x1, 3), 0)), =(%(x1, 2), 1)), >(+(x0, 1), 0))
f3228_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), 0, 0) → f3228_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), 1, 1) | >(x0, 0)
f3228_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x1) → f3228_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), +(x1, 1), +(x1, 1)) | &&(&&(&&(>(+(x1, 1), 0), <(x1, x0)), =(%(x1, 2), 0)), >(+(x0, 1), 0))

Filtered ground terms:

f3228_0_main_Load(x1, x2, x3, x4, x5) → f3228_0_main_Load(x2, x3, x4, x5)
Cond_f3228_0_main_Load(x1, x2, x3, x4, x5, x6) → Cond_f3228_0_main_Load(x1, x3, x4, x5, x6)
f3555_0_main_GE(x1, x2, x3, x4, x5, x6, x7) → f3555_0_main_GE(x2, x3, x4, x5, x6)
Cond_f3555_0_main_GE(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f3555_0_main_GE(x1, x3, x4, x5, x6, x7)
Cond_f3555_0_main_GE1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f3555_0_main_GE1(x1, x3, x4, x5, x6, x7)
Cond_f3228_0_main_Load1(x1, x2, x3, x4, x5, x6) → Cond_f3228_0_main_Load1(x1, x3, x4, x5, x6)
f3384_0_exp_Load(x1, x2, x3, x4, x5) → f3384_0_exp_Load(x2, x3, x4, x5)
Cond_f3228_0_main_Load2(x1, x2, x3, x4, x5, x6) → Cond_f3228_0_main_Load2(x1, x3, x4, x5, x6)
f3320_0_cos_Load(x1, x2, x3, x4, x5) → f3320_0_cos_Load(x2, x3, x4, x5)
Cond_f3228_0_main_Load3(x1, x2, x3, x4, x5, x6) → Cond_f3228_0_main_Load3(x1, x3, x4, x5, x6)
f3276_0_sin_Load(x1, x2, x3, x4, x5) → f3276_0_sin_Load(x2, x3, x4, x5)
Cond_f3228_0_main_Load4(x1, x2, x3, x4, x5, x6) → Cond_f3228_0_main_Load4(x1, x3, x4, x5, x6)
Cond_f3228_0_main_Load5(x1, x2, x3, x4, x5, x6) → Cond_f3228_0_main_Load5(x1, x3, x4, x5, x6)
Cond_f3228_0_main_Load6(x1, x2, x3, x4, x5, x6) → Cond_f3228_0_main_Load6(x1, x3, x4)
Cond_f3228_0_main_Load7(x1, x2, x3, x4, x5, x6) → Cond_f3228_0_main_Load7(x1, x3, x4, x5, x6)

Filtered duplicate terms:

f3228_0_main_Load(x1, x2, x3, x4) → f3228_0_main_Load(x2, x4)
Cond_f3228_0_main_Load(x1, x2, x3, x4, x5) → Cond_f3228_0_main_Load(x1, x3, x5)
f3555_0_main_GE(x1, x2, x3, x4, x5) → f3555_0_main_GE(x2, x3, x5)
Cond_f3555_0_main_GE(x1, x2, x3, x4, x5, x6) → Cond_f3555_0_main_GE(x1, x3, x4, x6)
Cond_f3555_0_main_GE1(x1, x2, x3, x4, x5, x6) → Cond_f3555_0_main_GE1(x1, x3, x4, x6)
Cond_f3228_0_main_Load1(x1, x2, x3, x4, x5) → Cond_f3228_0_main_Load1(x1, x3, x5)
f3384_0_exp_Load(x1, x2, x3, x4) → f3384_0_exp_Load(x3, x4)
Cond_f3228_0_main_Load2(x1, x2, x3, x4, x5) → Cond_f3228_0_main_Load2(x1, x3, x5)
f3320_0_cos_Load(x1, x2, x3, x4) → f3320_0_cos_Load(x3, x4)
Cond_f3228_0_main_Load3(x1, x2, x3, x4, x5) → Cond_f3228_0_main_Load3(x1, x3, x5)
f3276_0_sin_Load(x1, x2, x3, x4) → f3276_0_sin_Load(x3, x4)
Cond_f3228_0_main_Load4(x1, x2, x3, x4, x5) → Cond_f3228_0_main_Load4(x1, x3, x5)
Cond_f3228_0_main_Load5(x1, x2, x3, x4, x5) → Cond_f3228_0_main_Load5(x1, x3, x5)
Cond_f3228_0_main_Load6(x1, x2, x3) → Cond_f3228_0_main_Load6(x1, x3)
Cond_f3228_0_main_Load7(x1, x2, x3, x4, x5) → Cond_f3228_0_main_Load7(x1, x3, x5)

Filtered unneeded terms:

Cond_f3555_0_main_GE1(x1, x2, x3, x4) → Cond_f3555_0_main_GE1(x1, x2, x3)
Cond_f3228_0_main_Load1(x1, x2, x3) → Cond_f3228_0_main_Load1(x1)
Cond_f3228_0_main_Load2(x1, x2, x3) → Cond_f3228_0_main_Load2(x1)
Cond_f3228_0_main_Load3(x1, x2, x3) → Cond_f3228_0_main_Load3(x1)

Prepared 10 rules for path length conversion:

P rules:
f3228_0_main_Load(java.lang.Object(ARRAY(x0)), x1, x0) → f3555_0_main_GE(java.lang.Object(ARRAY(x0)), x1, 0, x0) | &&(&&(&&(&&(<(x1, x0), >(%(x1, 5), 0)), >(%(x1, 3), 0)), >(+(x0, 1), 0)), =(%(x1, 2), 1))
f3555_0_main_GE(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f3555_0_main_GE(java.lang.Object(ARRAY(x0)), x1, +(x2, 1), x0) | &&(<(x2, 100), >(+(x2, 1), 0))
f3555_0_main_GE(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f3228_0_main_Load(java.lang.Object(ARRAY(x0)), +(x1, 1), x0) | &&(>(+(x1, 1), 0), >(+(x2, 1), 100))
f3228_0_main_Load(java.lang.Object(ARRAY(x0)), x1, x0) → f3384_0_exp_Load(x0, x1) | &&(&&(&&(&&(<(x1, x0), =(%(x1, 5), 0)), >(%(x1, 3), 0)), =(%(x1, 2), 1)), >(+(x0, 1), 0))
f3228_0_main_Load(java.lang.Object(ARRAY(x0)), x1, x0) → f3320_0_cos_Load(x0, x1) | &&(&&(&&(<(x1, x0), =(%(x1, 3), 0)), =(%(x1, 2), 1)), >(+(x0, 1), 0))
f3228_0_main_Load(java.lang.Object(ARRAY(x0)), x1, x0) → f3276_0_sin_Load(x0, x1) | &&(&&(<(x1, x0), =(%(x1, 2), 0)), >(+(x0, 1), 0))
f3228_0_main_Load(java.lang.Object(ARRAY(x0)), x1, x0) → f3228_0_main_Load(java.lang.Object(ARRAY(x0)), +(x1, 1), x0) | &&(&&(&&(&&(&&(>(+(x1, 1), 0), <(x1, x0)), =(%(x1, 5), 0)), >(%(x1, 3), 0)), =(%(x1, 2), 1)), >(+(x0, 1), 0))
f3228_0_main_Load(java.lang.Object(ARRAY(x0)), x1, x0) → f3228_0_main_Load(java.lang.Object(ARRAY(x0)), +(x1, 1), x0) | &&(&&(&&(&&(>(+(x1, 1), 0), <(x1, x0)), =(%(x1, 3), 0)), =(%(x1, 2), 1)), >(+(x0, 1), 0))
f3228_0_main_Load(java.lang.Object(ARRAY(x0)), 0, x0) → f3228_0_main_Load(java.lang.Object(ARRAY(x0)), 1, x0) | >(x0, 0)
f3228_0_main_Load(java.lang.Object(ARRAY(x0)), x1, x0) → f3228_0_main_Load(java.lang.Object(ARRAY(x0)), +(x1, 1), x0) | &&(&&(&&(>(+(x1, 1), 0), <(x1, x0)), =(%(x1, 2), 0)), >(+(x0, 1), 0))

Finished conversion. Obtained 11 rules.

P rules:
f3228_0_main_Load(v28, x1, x0) → f3228_0_main_Load'(v28, x1, x0) | &&(&&(&&(&&(&&(&&(&&(<(x1, x0), >(-(x1, *(5, div)), 0)), >(-(x1, *(3, div1)), 0)), =(-(x1, *(2, div2)), 1)), >(x0, -1)), >(+(v29, 1), 1)), <=(v29, v28)), >(+(v28, 1), 1))
f3228_0_main_Load'(v28, x1, x0) → f3555_0_main_GE(v29, x1, 0, x0) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(<(x1, x0), >(-(x1, *(5, div)), 0)), <(-(x1, *(5, div)), 5)), >(-(x1, *(3, div1)), 0)), <(-(x1, *(3, div1)), 3)), >=(-(x1, *(2, div2)), 0)), =(-(x1, *(2, div2)), 1)), <(-(x1, *(2, div2)), 2)), >(x0, -1)), >(+(v29, 1), 1)), <=(v29, v28)), >(+(v28, 1), 1))
f3555_0_main_GE(v30, x3, x4, x2) → f3555_0_main_GE(v31, x3, +(x4, 1), x2) | &&(&&(&&(&&(>(x4, -1), <(x4, 100)), >(+(v31, 1), 1)), <=(v31, v30)), >(+(v30, 1), 1))
f3555_0_main_GE(v32, x6, x7, x5) → f3228_0_main_Load(v33, +(x6, 1), x5) | &&(&&(&&(&&(>(x7, 99), >(x6, -1)), >(+(v33, 1), 1)), <=(v33, v32)), >(+(v32, 1), 1))
f3228_0_main_Load(v34, x15, x14) → f3228_0_main_Load'(v34, x15, x14) | &&(&&(&&(&&(&&(&&(&&(&&(>(x15, -1), <(x15, x14)), =(-(x15, *(5, div)), 0)), >(-(x15, *(3, div1)), 0)), =(-(x15, *(2, div2)), 1)), >(x14, -1)), >(+(v35, 1), 1)), <=(v35, v34)), >(+(v34, 1), 1))
f3228_0_main_Load'(v34, x15, x14) → f3228_0_main_Load(v35, +(x15, 1), x14) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(x15, -1), <(x15, x14)), >=(-(x15, *(5, div)), 0)), =(-(x15, *(5, div)), 0)), <(-(x15, *(5, div)), 5)), >(-(x15, *(3, div1)), 0)), <(-(x15, *(3, div1)), 3)), >=(-(x15, *(2, div2)), 0)), =(-(x15, *(2, div2)), 1)), <(-(x15, *(2, div2)), 2)), >(x14, -1)), >(+(v35, 1), 1)), <=(v35, v34)), >(+(v34, 1), 1))
f3228_0_main_Load(v36, x17, x16) → f3228_0_main_Load'(v36, x17, x16) | &&(&&(&&(&&(&&(&&(&&(>(x17, -1), <(x17, x16)), =(-(x17, *(3, div)), 0)), =(-(x17, *(2, div1)), 1)), >(x16, -1)), >(+(v37, 1), 1)), <=(v37, v36)), >(+(v36, 1), 1))
f3228_0_main_Load'(v36, x17, x16) → f3228_0_main_Load(v37, +(x17, 1), x16) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(x17, -1), <(x17, x16)), >=(-(x17, *(3, div)), 0)), =(-(x17, *(3, div)), 0)), <(-(x17, *(3, div)), 3)), >=(-(x17, *(2, div1)), 0)), =(-(x17, *(2, div1)), 1)), <(-(x17, *(2, div1)), 2)), >(x16, -1)), >(+(v37, 1), 1)), <=(v37, v36)), >(+(v36, 1), 1))
f3228_0_main_Load(v38, c0, x18) → f3228_0_main_Load(v39, 1, x18) | &&(&&(&&(&&(>(x18, 0), >(+(v39, 1), 1)), <=(v39, v38)), >(+(v38, 1), 1)), =(0, c0))
f3228_0_main_Load(v40, x20, x19) → f3228_0_main_Load'(v40, x20, x19) | &&(&&(&&(&&(&&(&&(>(x20, -1), <(x20, x19)), =(-(x20, *(2, div)), 0)), >(x19, -1)), >(+(v41, 1), 1)), <=(v41, v40)), >(+(v40, 1), 1))
f3228_0_main_Load'(v40, x20, x19) → f3228_0_main_Load(v41, +(x20, 1), x19) | &&(&&(&&(&&(&&(&&(&&(&&(>(x20, -1), <(x20, x19)), >=(-(x20, *(2, div)), 0)), =(-(x20, *(2, div)), 0)), <(-(x20, *(2, div)), 2)), >(x19, -1)), >(+(v41, 1), 1)), <=(v41, v40)), >(+(v40, 1), 1))

(32) Obligation:

Rules:
f3228_0_main_Load(v28, x1, x0) → f3228_0_main_Load'(v28, x1, x0) | &&(&&(&&(&&(&&(&&(&&(<(x1, x0), >(-(x1, *(5, div)), 0)), >(-(x1, *(3, div1)), 0)), =(-(x1, *(2, div2)), 1)), >(x0, -1)), >(+(v29, 1), 1)), <=(v29, v28)), >(+(v28, 1), 1))
f3228_0_main_Load'(v28, x1, x0) → f3555_0_main_GE(v29, x1, 0, x0) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(<(x1, x0), >(-(x1, *(5, div)), 0)), <(-(x1, *(5, div)), 5)), >(-(x1, *(3, div1)), 0)), <(-(x1, *(3, div1)), 3)), >=(-(x1, *(2, div2)), 0)), =(-(x1, *(2, div2)), 1)), <(-(x1, *(2, div2)), 2)), >(x0, -1)), >(+(v29, 1), 1)), <=(v29, v28)), >(+(v28, 1), 1))
f3555_0_main_GE(v30, x3, x4, x2) → f3555_0_main_GE(v31, x3, +(x4, 1), x2) | &&(&&(&&(&&(>(x4, -1), <(x4, 100)), >(+(v31, 1), 1)), <=(v31, v30)), >(+(v30, 1), 1))
f3555_0_main_GE(v32, x6, x7, x5) → f3228_0_main_Load(v33, +(x6, 1), x5) | &&(&&(&&(&&(>(x7, 99), >(x6, -1)), >(+(v33, 1), 1)), <=(v33, v32)), >(+(v32, 1), 1))
f3228_0_main_Load(v34, x15, x14) → f3228_0_main_Load'(v34, x15, x14) | &&(&&(&&(&&(&&(&&(&&(&&(>(x15, -1), <(x15, x14)), =(-(x15, *(5, div)), 0)), >(-(x15, *(3, div1)), 0)), =(-(x15, *(2, div2)), 1)), >(x14, -1)), >(+(v35, 1), 1)), <=(v35, v34)), >(+(v34, 1), 1))
f3228_0_main_Load'(v34, x15, x14) → f3228_0_main_Load(v35, +(x15, 1), x14) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(x15, -1), <(x15, x14)), >=(-(x15, *(5, div)), 0)), =(-(x15, *(5, div)), 0)), <(-(x15, *(5, div)), 5)), >(-(x15, *(3, div1)), 0)), <(-(x15, *(3, div1)), 3)), >=(-(x15, *(2, div2)), 0)), =(-(x15, *(2, div2)), 1)), <(-(x15, *(2, div2)), 2)), >(x14, -1)), >(+(v35, 1), 1)), <=(v35, v34)), >(+(v34, 1), 1))
f3228_0_main_Load(v36, x17, x16) → f3228_0_main_Load'(v36, x17, x16) | &&(&&(&&(&&(&&(&&(&&(>(x17, -1), <(x17, x16)), =(-(x17, *(3, div)), 0)), =(-(x17, *(2, div1)), 1)), >(x16, -1)), >(+(v37, 1), 1)), <=(v37, v36)), >(+(v36, 1), 1))
f3228_0_main_Load'(v36, x17, x16) → f3228_0_main_Load(v37, +(x17, 1), x16) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(x17, -1), <(x17, x16)), >=(-(x17, *(3, div)), 0)), =(-(x17, *(3, div)), 0)), <(-(x17, *(3, div)), 3)), >=(-(x17, *(2, div1)), 0)), =(-(x17, *(2, div1)), 1)), <(-(x17, *(2, div1)), 2)), >(x16, -1)), >(+(v37, 1), 1)), <=(v37, v36)), >(+(v36, 1), 1))
f3228_0_main_Load(v38, c0, x18) → f3228_0_main_Load(v39, 1, x18) | &&(&&(&&(&&(>(x18, 0), >(+(v39, 1), 1)), <=(v39, v38)), >(+(v38, 1), 1)), =(0, c0))
f3228_0_main_Load(v40, x20, x19) → f3228_0_main_Load'(v40, x20, x19) | &&(&&(&&(&&(&&(&&(>(x20, -1), <(x20, x19)), =(-(x20, *(2, div)), 0)), >(x19, -1)), >(+(v41, 1), 1)), <=(v41, v40)), >(+(v40, 1), 1))
f3228_0_main_Load'(v40, x20, x19) → f3228_0_main_Load(v41, +(x20, 1), x19) | &&(&&(&&(&&(&&(&&(&&(&&(>(x20, -1), <(x20, x19)), >=(-(x20, *(2, div)), 0)), =(-(x20, *(2, div)), 0)), <(-(x20, *(2, div)), 2)), >(x19, -1)), >(+(v41, 1), 1)), <=(v41, v40)), >(+(v40, 1), 1))

(33) TerminationGraphProcessor (SOUND transformation)

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

(34) Obligation:

Rules:
f3228_0_main_Load(x0, x1, x2) → f3228_0_main_Load'(x0, x1, x2) | &&(&&(&&(&&(&&(&&(&&(<(x1, x2), >(-(x1, *(5, x3)), 0)), >(-(x1, *(3, x4)), 0)), =(-(x1, *(2, x5)), 1)), >(x2, -1)), >(+(x6, 1), 1)), <=(x6, x0)), >(+(x0, 1), 1))
f3555_0_main_GE(x19, x20, x21, x22) → f3228_0_main_Load(x23, +(x20, 1), x22) | &&(&&(&&(&&(>(x21, 99), >(x20, -1)), >(+(x23, 1), 1)), <=(x23, x19)), >(+(x19, 1), 1))
f3555_0_main_GE(x14, x15, x16, x17) → f3555_0_main_GE(x18, x15, +(x16, 1), x17) | &&(&&(&&(&&(>(x16, -1), <(x16, 100)), >(+(x18, 1), 1)), <=(x18, x14)), >(+(x14, 1), 1))
f3228_0_main_Load'(x7, x8, x9) → f3555_0_main_GE(x10, x8, 0, x9) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(<(x8, x9), >(-(x8, *(5, x11)), 0)), <(-(x8, *(5, x11)), 5)), >(-(x8, *(3, x12)), 0)), <(-(x8, *(3, x12)), 3)), >=(-(x8, *(2, x13)), 0)), =(-(x8, *(2, x13)), 1)), <(-(x8, *(2, x13)), 2)), >(x9, -1)), >(+(x10, 1), 1)), <=(x10, x7)), >(+(x7, 1), 1))
f3228_0_main_Load'(x59, x60, x61) → f3228_0_main_Load(x62, +(x60, 1), x61) | &&(&&(&&(&&(&&(&&(&&(&&(>(x60, -1), <(x60, x61)), >=(-(x60, *(2, x63)), 0)), =(-(x60, *(2, x63)), 0)), <(-(x60, *(2, x63)), 2)), >(x61, -1)), >(+(x62, 1), 1)), <=(x62, x59)), >(+(x59, 1), 1))
f3228_0_main_Load(x54, x55, x56) → f3228_0_main_Load'(x54, x55, x56) | &&(&&(&&(&&(&&(&&(>(x55, -1), <(x55, x56)), =(-(x55, *(2, x57)), 0)), >(x56, -1)), >(+(x58, 1), 1)), <=(x58, x54)), >(+(x54, 1), 1))
f3228_0_main_Load'(x31, x32, x33) → f3228_0_main_Load(x34, +(x32, 1), x33) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(x32, -1), <(x32, x33)), >=(-(x32, *(5, x35)), 0)), =(-(x32, *(5, x35)), 0)), <(-(x32, *(5, x35)), 5)), >(-(x32, *(3, x36)), 0)), <(-(x32, *(3, x36)), 3)), >=(-(x32, *(2, x37)), 0)), =(-(x32, *(2, x37)), 1)), <(-(x32, *(2, x37)), 2)), >(x33, -1)), >(+(x34, 1), 1)), <=(x34, x31)), >(+(x31, 1), 1))
f3228_0_main_Load(x24, x25, x26) → f3228_0_main_Load'(x24, x25, x26) | &&(&&(&&(&&(&&(&&(&&(&&(>(x25, -1), <(x25, x26)), =(-(x25, *(5, x27)), 0)), >(-(x25, *(3, x28)), 0)), =(-(x25, *(2, x29)), 1)), >(x26, -1)), >(+(x30, 1), 1)), <=(x30, x24)), >(+(x24, 1), 1))
f3228_0_main_Load'(x44, x45, x46) → f3228_0_main_Load(x47, +(x45, 1), x46) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(x45, -1), <(x45, x46)), >=(-(x45, *(3, x48)), 0)), =(-(x45, *(3, x48)), 0)), <(-(x45, *(3, x48)), 3)), >=(-(x45, *(2, x49)), 0)), =(-(x45, *(2, x49)), 1)), <(-(x45, *(2, x49)), 2)), >(x46, -1)), >(+(x47, 1), 1)), <=(x47, x44)), >(+(x44, 1), 1))
f3228_0_main_Load(x38, x39, x40) → f3228_0_main_Load'(x38, x39, x40) | &&(&&(&&(&&(&&(&&(&&(>(x39, -1), <(x39, x40)), =(-(x39, *(3, x41)), 0)), =(-(x39, *(2, x42)), 1)), >(x40, -1)), >(+(x43, 1), 1)), <=(x43, x38)), >(+(x38, 1), 1))

(35) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:

[f3228_0_main_Load(x61, x63, x65)] = 1 - 2·x63 + 2·x65
[f3228_0_main_Load'(x68, x70, x72)] = -2·x70 + 2·x72
[f3555_0_main_GE(x75, x77, x79, x81)] = -1 - 2·x77 + 2·x81

Therefore the following rule(s) have been dropped:

f3228_0_main_Load(x0, x1, x2) → f3228_0_main_Load'(x0, x1, x2) | &&(&&(&&(&&(&&(&&(&&(<(x1, x2), >(-(x1, *(5, x3)), 0)), >(-(x1, *(3, x4)), 0)), =(-(x1, *(2, x5)), 1)), >(x2, -1)), >(+(x6, 1), 1)), <=(x6, x0)), >(+(x0, 1), 1))
f3228_0_main_Load'(x17, x18, x19) → f3555_0_main_GE(x20, x18, 0, x19) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(<(x18, x19), >(-(x18, *(5, x21)), 0)), <(-(x18, *(5, x21)), 5)), >(-(x18, *(3, x22)), 0)), <(-(x18, *(3, x22)), 3)), >=(-(x18, *(2, x23)), 0)), =(-(x18, *(2, x23)), 1)), <(-(x18, *(2, x23)), 2)), >(x19, -1)), >(+(x20, 1), 1)), <=(x20, x17)), >(+(x17, 1), 1))
f3228_0_main_Load'(x24, x25, x26) → f3228_0_main_Load(x27, +(x25, 1), x26) | &&(&&(&&(&&(&&(&&(&&(&&(>(x25, -1), <(x25, x26)), >=(-(x25, *(2, x28)), 0)), =(-(x25, *(2, x28)), 0)), <(-(x25, *(2, x28)), 2)), >(x26, -1)), >(+(x27, 1), 1)), <=(x27, x24)), >(+(x24, 1), 1))
f3228_0_main_Load(x29, x30, x31) → f3228_0_main_Load'(x29, x30, x31) | &&(&&(&&(&&(&&(&&(>(x30, -1), <(x30, x31)), =(-(x30, *(2, x32)), 0)), >(x31, -1)), >(+(x33, 1), 1)), <=(x33, x29)), >(+(x29, 1), 1))
f3228_0_main_Load'(x34, x35, x36) → f3228_0_main_Load(x37, +(x35, 1), x36) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(x35, -1), <(x35, x36)), >=(-(x35, *(5, x38)), 0)), =(-(x35, *(5, x38)), 0)), <(-(x35, *(5, x38)), 5)), >(-(x35, *(3, x39)), 0)), <(-(x35, *(3, x39)), 3)), >=(-(x35, *(2, x40)), 0)), =(-(x35, *(2, x40)), 1)), <(-(x35, *(2, x40)), 2)), >(x36, -1)), >(+(x37, 1), 1)), <=(x37, x34)), >(+(x34, 1), 1))
f3228_0_main_Load(x41, x42, x43) → f3228_0_main_Load'(x41, x42, x43) | &&(&&(&&(&&(&&(&&(&&(&&(>(x42, -1), <(x42, x43)), =(-(x42, *(5, x44)), 0)), >(-(x42, *(3, x45)), 0)), =(-(x42, *(2, x46)), 1)), >(x43, -1)), >(+(x47, 1), 1)), <=(x47, x41)), >(+(x41, 1), 1))
f3228_0_main_Load'(x48, x49, x50) → f3228_0_main_Load(x51, +(x49, 1), x50) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(x49, -1), <(x49, x50)), >=(-(x49, *(3, x52)), 0)), =(-(x49, *(3, x52)), 0)), <(-(x49, *(3, x52)), 3)), >=(-(x49, *(2, x53)), 0)), =(-(x49, *(2, x53)), 1)), <(-(x49, *(2, x53)), 2)), >(x50, -1)), >(+(x51, 1), 1)), <=(x51, x48)), >(+(x48, 1), 1))
f3228_0_main_Load(x54, x55, x56) → f3228_0_main_Load'(x54, x55, x56) | &&(&&(&&(&&(&&(&&(&&(>(x55, -1), <(x55, x56)), =(-(x55, *(3, x57)), 0)), =(-(x55, *(2, x58)), 1)), >(x56, -1)), >(+(x59, 1), 1)), <=(x59, x54)), >(+(x54, 1), 1))

(36) Obligation:

Rules:
f3555_0_main_GE(x7, x8, x9, x10) → f3228_0_main_Load(x11, +(x8, 1), x10) | &&(&&(&&(&&(>(x9, 99), >(x8, -1)), >(+(x11, 1), 1)), <=(x11, x7)), >(+(x7, 1), 1))
f3555_0_main_GE(x12, x13, x14, x15) → f3555_0_main_GE(x16, x13, +(x14, 1), x15) | &&(&&(&&(&&(>(x14, -1), <(x14, 100)), >(+(x16, 1), 1)), <=(x16, x12)), >(+(x12, 1), 1))

(37) TerminationGraphProcessor (SOUND transformation)

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

(38) Obligation:

Rules:
f3555_0_main_GE(x5, x6, x7, x8) → f3555_0_main_GE(x9, x6, +(x7, 1), x8) | &&(&&(&&(&&(>(x7, -1), <(x7, 100)), >(+(x9, 1), 1)), <=(x9, x5)), >(+(x5, 1), 1))

(39) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f3555_0_main_GE(x6, x8, x10, x12)] = 99 - x10

Therefore the following rule(s) have been dropped:

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

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIntTRSProof (SOUND transformation)

(7) Obligation:

(8) LinearRankingProcessor (EQUIVALENT transformation)

(9) YES

(10) Obligation:

(11) SCCToIntTRSProof (SOUND transformation)

(12) Obligation:

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

(14) YES

(15) Obligation:

(16) SCCToIntTRSProof (SOUND transformation)

(17) Obligation:

(18) PolynomialOrderProcessor (EQUIVALENT transformation)

(19) YES

(20) Obligation:

(21) SCCToIntTRSProof (SOUND transformation)

(22) Obligation:

(23) PolynomialOrderProcessor (EQUIVALENT transformation)

(24) YES

(25) Obligation:

(26) SCCToIntTRSProof (SOUND transformation)

(27) Obligation:

(28) PolynomialOrderProcessor (EQUIVALENT transformation)

(29) YES

(30) Obligation:

(31) SCCToIntTRSProof (SOUND transformation)

(32) Obligation:

(33) TerminationGraphProcessor (SOUND transformation)

(34) Obligation:

(35) PolynomialOrderProcessor (SOUND transformation)

(36) Obligation:

(37) TerminationGraphProcessor (SOUND transformation)

(38) Obligation:

(39) PolynomialOrderProcessor (EQUIVALENT transformation)

(40) YES