Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 1537 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 6 ms)
↳4 AND
    ↳5 JBCTerminationSCC
        ↳6 SCCToIntTRSProof (⇒, 69 ms)
        ↳7 intTRS
        ↳8 PolynomialOrderProcessor (⇔, 0 ms)
        ↳9 YES
    ↳10 JBCTerminationSCC
        ↳11 SCCToIntTRSProof (⇒, 878 ms)
        ↳12 intTRS
        ↳13 TerminationGraphProcessor (⇒, 206 ms)
        ↳14 intTRS
        ↳15 PolynomialOrderProcessor (⇒, 0 ms)
        ↳16 intTRS
        ↳17 TerminationGraphProcessor (⇒, 110 ms)
        ↳18 AND
            ↳19 intTRS
                ↳20 PolynomialOrderProcessor (⇔, 0 ms)
                ↳21 YES
            ↳22 intTRS
                ↳23 PolynomialOrderProcessor (⇔, 0 ms)
                ↳24 YES
            ↳25 intTRS
                ↳26 PolynomialOrderProcessor (⇔, 0 ms)
                ↳27 YES

(0) Obligation:

JBC Problem based on JBC Program:
public class Binomial {
    
    public static int fact(int n) {
	if (n <= 0) return 1;
	else return n * fact(n - 1);
    }

    public static int binomialCoefficient(int n, int k) {
	return fact(n) / (fact(k) * fact(n - k));
    }

    public static void main(String args[]) {
	for (int n = 0; n <= args.length; n++)
	    for (int k = 0; k <= args.length; k++)
		if (k <= n) binomialCoefficient(n, k);
		else binomialCoefficient(k, n);
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

Binomial.fact(I)I: Graph of 22 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: Binomial.fact(I)I
SCC calls the following helper methods: Binomial.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:
f1710_0_fact_GT(EOS, i211, i211, i211) → f1714_0_fact_GT(EOS, i211, i211, i211)
f1714_0_fact_GT(EOS, i211, i211, i211) → f1719_0_fact_Load(EOS, i211, i211) | >(i211, 0)
f1719_0_fact_Load(EOS, i211, i211) → f1724_0_fact_Load(EOS, i211, i211, i211)
f1724_0_fact_Load(EOS, i211, i211, i211) → f1729_0_fact_ConstantStackPush(EOS, i211, i211, i211)
f1729_0_fact_ConstantStackPush(EOS, i211, i211, i211) → f1837_0_fact_IntArithmetic(EOS, i211, i211, i211, 1)
f1837_0_fact_IntArithmetic(EOS, i211, i211, i211, matching1) → f1841_0_fact_InvokeMethod(EOS, i211, i211, -(i211, 1)) | &&(>(i211, 0), =(matching1, 1))
f1841_0_fact_InvokeMethod(EOS, i211, i211, i250) → f1844_0_fact_Load(EOS, i250, i250)
f1841_0_fact_InvokeMethod(EOS, i211, i211, i250) → f1844_1_fact_Load(EOS, i211, i211, i250, i250)
f1844_0_fact_Load(EOS, i250, i250) → f1847_0_fact_Load(EOS, i250, i250)
f1847_0_fact_Load(EOS, i250, i250) → f1708_0_fact_Load(EOS, i250, i250)
f1708_0_fact_Load(EOS, i205, i205) → f1710_0_fact_GT(EOS, i205, i205, i205)

Combined rules. Obtained 2 IRules

P rules:
f1710_0_fact_GT(EOS, x0, x0, x0) → f1844_1_fact_Load(EOS, x0, x0, -(x0, 1), -(x0, 1)) | >(x0, 0)
f1710_0_fact_GT(EOS, x0, x0, x0) → f1710_0_fact_GT(EOS, -(x0, 1), -(x0, 1), -(x0, 1)) | >(x0, 0)

Filtered ground terms:


f1710_0_fact_GT(x1, x2, x3, x4) → f1710_0_fact_GT(x2, x3, x4)
Cond_f1710_0_fact_GT(x1, x2, x3, x4, x5) → Cond_f1710_0_fact_GT(x1, x3, x4, x5)
f1844_1_fact_Load(x1, x2, x3, x4, x5) → f1844_1_fact_Load(x2, x3, x4, x5)
Cond_f1710_0_fact_GT1(x1, x2, x3, x4, x5) → Cond_f1710_0_fact_GT1(x1, x3, x4, x5)

Filtered duplicate terms:


f1710_0_fact_GT(x1, x2, x3) → f1710_0_fact_GT(x3)
Cond_f1710_0_fact_GT(x1, x2, x3, x4) → Cond_f1710_0_fact_GT(x1, x4)
f1844_1_fact_Load(x1, x2, x3, x4) → f1844_1_fact_Load(x4)
Cond_f1710_0_fact_GT1(x1, x2, x3, x4) → Cond_f1710_0_fact_GT1(x1, x4)

Filtered unneeded terms:


Cond_f1710_0_fact_GT(x1, x2) → Cond_f1710_0_fact_GT(x1)

Prepared 2 rules for path length conversion:

P rules:
f1710_0_fact_GT(x0) → f1844_1_fact_Load(-(x0, 1)) | >(x0, 0)
f1710_0_fact_GT(x0) → f1710_0_fact_GT(-(x0, 1)) | >(x0, 0)

Finished conversion. Obtained 1 rules.

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

(7) Obligation:

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

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f1710_0_fact_GT(x2)] = x2

Therefore the following rule(s) have been dropped:


f1710_0_fact_GT(x0) → f1710_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: Binomial.main([Ljava/lang/String;)V
SCC calls the following helper methods: Binomial.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:

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 206 IRules

P rules:
f2769_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i628, i628) → f2771_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i628, i628, java.lang.Object(ARRAY(i1)))
f2771_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i628, i628, java.lang.Object(ARRAY(i1))) → f2774_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i628, i628, i1) | >=(i1, 0)
f2774_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i628, i628, i1) → f2776_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i628, i628, i1)
f2776_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i628, i628, i1) → f2780_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i628) | <=(i628, i1)
f2780_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i628) → f2784_0_main_Store(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i628, 0)
f2784_0_main_Store(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i628, matching1) → f2785_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i628, 0) | =(matching1, 0)
f2785_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i628, matching1) → f3126_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i628, 0) | =(matching1, 0)
f3126_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i700, i701) → f4127_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i700, i701)
f4127_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1050, i1051) → f5131_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1050, i1051)
f5131_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1427, i1428) → f6014_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1427, i1428)
f6014_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810) → f6025_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810)
f6025_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810) → f6026_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810, java.lang.Object(ARRAY(i1)))
f6026_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810, java.lang.Object(ARRAY(i1))) → f6028_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810, i1) | >=(i1, 0)
f6028_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810, i1) → f6030_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810, i1)
f6028_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810, i1) → f6031_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810, i1)
f6030_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810, i1) → f6032_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809) | >(i1810, i1)
f6032_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809) → f6037_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), +(i1809, 1))
f6037_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1814) → f6042_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1814)
f6042_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1814) → f2766_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1814)
f2766_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i628) → f2769_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i628, i628)
f6031_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810, i1) → f6035_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810) | <=(i1810, i1)
f6035_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810) → f6039_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810)
f6039_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810) → f6044_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810, i1809)
f6044_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810, i1809) → f6211_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810, i1809)
f6044_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810, i1809) → f6212_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810, i1809)
f6211_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810, i1809) → f6213_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810) | >(i1810, i1809)
f6213_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810) → f6216_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810)
f6216_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810) → f6219_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810, i1809)
f6219_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810, i1809) → f6222_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810, i1809, i1810, i1809)
f6222_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810, i1809, i1810, i1809) → f6225_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810, i1809, i1810, i1809, i1810)
f6225_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810, i1809, i1810, i1809, i1810) → f6229_0_fact_Load(EOS, i1810, i1810)
f6225_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810, i1809, i1810, i1809, i1810) → f6229_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810, i1809, i1810, i1809, i1810, i1810)
f6229_0_fact_Load(EOS, i1810, i1810) → f6232_0_fact_Load(EOS, i1810, i1810)
f6255_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, matching1, matching2, i1809, matching3, i1809, matching4, matching5) → f6260_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, 0, 0, i1809, 0, i1809) | &&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 0))
f6260_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, matching1, matching2, i1809, matching3, i1809) → f6270_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, 0, 0, i1809, 0, i1809, i1809) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f6270_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, matching1, matching2, i1809, matching3, i1809, i1809) → f6281_0_fact_Load(EOS, i1809, i1809) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f6270_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, matching1, matching2, i1809, matching3, i1809, i1809) → f6281_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, 0, 0, i1809, 0, i1809, i1809, i1809) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f6281_0_fact_Load(EOS, i1809, i1809) → f6288_0_fact_Load(EOS, i1809, i1809)
f6335_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, matching1, matching2, i1879, matching3, i1879, i1879, i1879) → f6345_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, 0, 0, i1879, 0, i1879) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f6345_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, matching1, matching2, i1879, matching3, i1879) → f6378_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, 0, 0, i1879, i1879, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f6378_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, matching1, matching2, i1879, i1879, matching3) → f6409_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, 0, 0, i1879, 0, i1879) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f6409_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, matching1, matching2, i1879, matching3, i1879) → f6448_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, 0, 0, i1879, -(0, i1879)) | &&(&&(&&(<=(i1879, 0), =(matching1, 0)), =(matching2, 0)), =(matching3, 0))
f6448_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, matching1, matching2, i1879, i1945) → f6488_0_fact_Load(EOS, i1945, i1945) | &&(=(matching1, 0), =(matching2, 0))
f6448_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, matching1, matching2, i1879, i1945) → f6488_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, 0, 0, i1879, i1945, i1945) | &&(=(matching1, 0), =(matching2, 0))
f6488_0_fact_Load(EOS, i1945, i1945) → f6500_0_fact_Load(EOS, i1945, i1945)
f6589_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, matching1, matching2, i1879, matching3, matching4) → f6608_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, 0, 0, i1879) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
f6608_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, matching1, matching2, i1879) → f6612_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, 0, 0, i1879) | &&(=(matching1, 0), =(matching2, 0))
f6612_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, matching1, matching2, i1879) → f6667_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, 0, 0, i1879) | &&(=(matching1, 0), =(matching2, 0))
f6667_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, matching1, matching2, i1879) → f6726_0_binomialCoefficient_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, 0, 0, i1879) | &&(=(matching1, 0), =(matching2, 0))
f6726_0_binomialCoefficient_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, matching1, matching2, i1879) → f6775_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, 0) | &&(=(matching1, 0), =(matching2, 0))
f6775_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, matching1) → f6798_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, 0) | =(matching1, 0)
f6798_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, matching1) → f6843_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, 0) | =(matching1, 0)
f6843_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2020, matching1) → f6864_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2020, 1) | =(matching1, 0)
f6864_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2020, matching1) → f6879_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2020, 1) | =(matching1, 1)
f6879_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2020, matching1) → f6014_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2020, 1) | =(matching1, 1)
f6590_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, matching1, matching2, i1879, i1992) → f6612_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, 0, 0, i1879) | &&(=(matching1, 0), =(matching2, 0))
f6336_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, matching1, matching2, i1883, matching3, i1883, i1883) → f6348_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, 0, 0, i1883, 0, i1883) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f6348_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, matching1, matching2, i1883, matching3, i1883) → f6380_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, 0, 0, i1883, i1883, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f6380_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, matching1, matching2, i1883, i1883, matching3) → f6411_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, 0, 0, i1883, 0, i1883) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f6411_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, matching1, matching2, i1883, matching3, i1883) → f6452_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, 0, 0, i1883, -(0, i1883)) | &&(&&(&&(>(i1883, 0), =(matching1, 0)), =(matching2, 0)), =(matching3, 0))
f6452_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, matching1, matching2, i1883, i1946) → f6489_0_fact_Load(EOS, i1946, i1946) | &&(=(matching1, 0), =(matching2, 0))
f6452_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, matching1, matching2, i1883, i1946) → f6489_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, 0, 0, i1883, i1946, i1946) | &&(=(matching1, 0), =(matching2, 0))
f6489_0_fact_Load(EOS, i1946, i1946) → f6502_0_fact_Load(EOS, i1946, i1946)
f6591_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, matching1, matching2, i1883, i1996, i1996) → f6614_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, 0, 0, i1883) | &&(=(matching1, 0), =(matching2, 0))
f6614_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, matching1, matching2, i1883) → f6670_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, 0, 0, i1883) | &&(=(matching1, 0), =(matching2, 0))
f6670_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, matching1, matching2, i1883) → f6728_0_binomialCoefficient_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, 0, 0, i1883) | &&(=(matching1, 0), =(matching2, 0))
f6728_0_binomialCoefficient_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, matching1, matching2, i1883) → f6778_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, 0) | &&(=(matching1, 0), =(matching2, 0))
f6778_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, matching1) → f6801_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, 0) | =(matching1, 0)
f6801_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, matching1) → f6855_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, 0) | =(matching1, 0)
f6855_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2040, matching1) → f6870_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2040, 1) | =(matching1, 0)
f6870_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2040, matching1) → f6887_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2040, 1) | =(matching1, 1)
f6887_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2040, matching1) → f6014_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2040, 1) | =(matching1, 1)
f6256_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1863, i1863, i1809, i1863, i1809, i1863) → f6262_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1863, i1863, i1809, i1863, i1809)
f6262_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1863, i1863, i1809, i1863, i1809) → f6273_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1863, i1863, i1809, i1863, i1809, i1809)
f6273_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1863, i1863, i1809, i1863, i1809, i1809) → f6283_0_fact_Load(EOS, i1809, i1809)
f6273_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1863, i1863, i1809, i1863, i1809, i1809) → f6283_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1863, i1863, i1809, i1863, i1809, i1809, i1809)
f6283_0_fact_Load(EOS, i1809, i1809) → f6290_0_fact_Load(EOS, i1809, i1809)
f6337_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863, i1863, i1887, i1863, i1887, i1887, i1887) → f6351_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863, i1863, i1887, i1863, i1887)
f6351_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863, i1863, i1887, i1863, i1887) → f6384_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863, i1863, i1887, i1887, i1863)
f6384_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863, i1863, i1887, i1887, i1863) → f6414_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863, i1863, i1887, i1863, i1887)
f6414_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863, i1863, i1887, i1863, i1887) → f6454_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863, i1863, i1887, -(i1863, i1887)) | &&(>(i1863, 0), <=(i1887, 0))
f6454_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863, i1863, i1887, i1947) → f6491_0_fact_Load(EOS, i1947, i1947)
f6454_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863, i1863, i1887, i1947) → f6491_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863, i1863, i1887, i1947, i1947)
f6491_0_fact_Load(EOS, i1947, i1947) → f6504_0_fact_Load(EOS, i1947, i1947)
f6595_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863, i1863, i1887, i2008) → f6617_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863, i1863, i1887)
f6617_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863, i1863, i1887) → f6673_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863, i1863, i1887)
f6673_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863, i1863, i1887) → f6733_0_binomialCoefficient_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863, i1863, i1887)
f6733_0_binomialCoefficient_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863, i1863, i1887) → f6781_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863)
f6781_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863) → f6805_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863)
f6805_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863) → f6849_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863)
f6849_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899) → f6867_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, +(i1899, 1)) | >(i1899, 0)
f6867_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i2232) → f6883_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i2232)
f6883_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i2232) → f6014_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i2232)
f6339_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891, i1863, i1891, i1891) → f6354_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891, i1863, i1891)
f6354_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891, i1863, i1891) → f6385_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891, i1891, i1863)
f6385_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891, i1891, i1863) → f6418_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891, i1863, i1891)
f6418_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891, i1863, i1891) → f6460_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891, -(i1863, i1891)) | &&(>(i1863, 0), >(i1891, 0))
f6460_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891, i1948) → f6492_0_fact_Load(EOS, i1948, i1948)
f6460_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891, i1948) → f6492_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891, i1948, i1948)
f6492_0_fact_Load(EOS, i1948, i1948) → f6505_0_fact_Load(EOS, i1948, i1948)
f6596_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891, i2012, i2012) → f6621_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891)
f6621_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891) → f6629_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891)
f6629_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891) → f6682_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891)
f6682_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891) → f6739_0_binomialCoefficient_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891)
f6739_0_binomialCoefficient_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891) → f6785_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863)
f6785_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863) → f6809_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863)
f6809_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863) → f6862_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863)
f6862_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907) → f6875_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, +(i1907, 1)) | >(i1907, 0)
f6875_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i2234) → f6892_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i2234)
f6892_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i2234) → f6014_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i2234)
f6597_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891, i2016) → f6629_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891)
f6212_0_main_GT(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1810, i1809) → f6215_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810) | <=(i1810, i1809)
f6215_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810) → f6218_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1809)
f6218_0_main_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1809) → f6221_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1809, i1810)
f6221_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1809, i1810) → f6224_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1809, i1810, i1809, i1810)
f6224_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1809, i1810, i1809, i1810) → f6228_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1809, i1810, i1809, i1810, i1809)
f6228_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1809, i1810, i1809, i1810, i1809) → f6231_0_fact_Load(EOS, i1809, i1809)
f6228_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1809, i1810, i1809, i1810, i1809) → f6231_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1810, i1809, i1810, i1809, i1810, i1809, i1809)
f6231_0_fact_Load(EOS, i1809, i1809) → f6234_0_fact_Load(EOS, i1809, i1809)
f6257_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1810, i1867, i1810, i1867, i1810, i1867, i1867) → f6265_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1810, i1867, i1810, i1867, i1810)
f6265_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1810, i1867, i1810, i1867, i1810) → f6275_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1810, i1867, i1810, i1867, i1810, i1810)
f6275_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1810, i1867, i1810, i1867, i1810, i1810) → f6285_0_fact_Load(EOS, i1810, i1810)
f6275_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1810, i1867, i1810, i1867, i1810, i1810) → f6285_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1810, i1867, i1810, i1867, i1810, i1810, i1810)
f6285_0_fact_Load(EOS, i1810, i1810) → f6292_0_fact_Load(EOS, i1810, i1810)
f6340_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, matching1, i1867, matching2, i1867, matching3, matching4, matching5) → f6360_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, 0, i1867, 0, i1867, 0) | &&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 0))
f6360_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, matching1, i1867, matching2, i1867, matching3) → f6389_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, 0, i1867, 0, 0, i1867) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f6389_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, matching1, i1867, matching2, matching3, i1867) → f6423_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, 0, i1867, 0, i1867, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f6423_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, matching1, i1867, matching2, i1867, matching3) → f6465_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), -(i1867, 0), 0, -(i1867, 0), 0, -(i1867, 0)) | &&(&&(&&(<=(i1867, 0), =(matching1, 0)), =(matching2, 0)), =(matching3, 0))
f6465_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, matching1, i1867, matching2, i1867) → f6494_0_fact_Load(EOS, i1867, i1867) | &&(=(matching1, 0), =(matching2, 0))
f6465_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, matching1, i1867, matching2, i1867) → f6494_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, 0, i1867, 0, i1867, i1867) | &&(=(matching1, 0), =(matching2, 0))
f6494_0_fact_Load(EOS, i1867, i1867) → f6507_0_fact_Load(EOS, i1867, i1867)
f6598_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2020, matching1, i2020, matching2, i2020, i2020) → f6633_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2020, 0, i2020, 0) | &&(=(matching1, 0), =(matching2, 0))
f6633_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2020, matching1, i2020, matching2) → f6686_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2020, 0, i2020, 0) | &&(=(matching1, 0), =(matching2, 0))
f6686_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2020, matching1, i2020, matching2) → f6744_0_binomialCoefficient_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2020, 0, i2020, 0) | &&(=(matching1, 0), =(matching2, 0))
f6744_0_binomialCoefficient_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2020, matching1, i2020, matching2) → f6787_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2020, 0) | &&(=(matching1, 0), =(matching2, 0))
f6787_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2020, matching1) → f6811_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2020, 0) | =(matching1, 0)
f6811_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2020, matching1) → f6843_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2020, 0) | =(matching1, 0)
f6341_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899, i1867, i1899, i1867, i1899, i1899) → f6365_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899, i1867, i1899, i1867, i1899)
f6365_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899, i1867, i1899, i1867, i1899) → f6395_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899, i1867, i1899, i1899, i1867)
f6395_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899, i1867, i1899, i1899, i1867) → f6429_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899, i1867, i1899, i1867, i1899)
f6429_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899, i1867, i1899, i1867, i1899) → f6470_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899, i1867, i1899, -(i1867, i1899)) | &&(<=(i1867, 0), >(i1899, 0))
f6470_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899, i1867, i1899, i1959) → f6495_0_fact_Load(EOS, i1959, i1959)
f6470_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899, i1867, i1899, i1959) → f6495_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899, i1867, i1899, i1959, i1959)
f6495_0_fact_Load(EOS, i1959, i1959) → f6509_0_fact_Load(EOS, i1959, i1959)
f6601_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899, i1867, i1899, i2028, i2028) → f6639_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899, i1867, i1899)
f6639_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899, i1867, i1899) → f6694_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899, i1867, i1899)
f6694_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899, i1867, i1899) → f6752_0_binomialCoefficient_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899, i1867, i1899)
f6752_0_binomialCoefficient_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899, i1867, i1899) → f6789_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899)
f6789_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899) → f6813_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899)
f6813_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899) → f6849_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899)
f6258_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1810, i1871, i1810, i1871, i1810, i1871) → f6269_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1810, i1871, i1810, i1871, i1810)
f6269_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1810, i1871, i1810, i1871, i1810) → f6280_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1810, i1871, i1810, i1871, i1810, i1810)
f6280_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1810, i1871, i1810, i1871, i1810, i1810) → f6287_0_fact_Load(EOS, i1810, i1810)
f6280_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1810, i1871, i1810, i1871, i1810, i1810) → f6287_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1810, i1871, i1810, i1871, i1810, i1810, i1810)
f6287_0_fact_Load(EOS, i1810, i1810) → f6294_0_fact_Load(EOS, i1810, i1810)
f6343_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, matching1, i1871, matching2, i1871, matching3, matching4, matching5) → f6370_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, 0, i1871, 0, i1871, 0) | &&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 0))
f6370_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, matching1, i1871, matching2, i1871, matching3) → f6400_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, 0, i1871, 0, 0, i1871) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f6400_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, matching1, i1871, matching2, matching3, i1871) → f6436_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, 0, i1871, 0, i1871, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f6436_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, matching1, i1871, matching2, i1871, matching3) → f6475_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), -(i1871, 0), 0, -(i1871, 0), 0, -(i1871, 0)) | &&(&&(&&(>(i1871, 0), =(matching1, 0)), =(matching2, 0)), =(matching3, 0))
f6475_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, matching1, i1871, matching2, i1871) → f6496_0_fact_Load(EOS, i1871, i1871) | &&(=(matching1, 0), =(matching2, 0))
f6475_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, matching1, i1871, matching2, i1871) → f6496_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, 0, i1871, 0, i1871, i1871) | &&(=(matching1, 0), =(matching2, 0))
f6496_0_fact_Load(EOS, i1871, i1871) → f6510_0_fact_Load(EOS, i1871, i1871)
f6604_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2040, matching1, i2040, matching2, i2040) → f6647_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2040, 0, i2040, 0) | &&(=(matching1, 0), =(matching2, 0))
f6647_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2040, matching1, i2040, matching2) → f6702_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2040, 0, i2040, 0) | &&(=(matching1, 0), =(matching2, 0))
f6702_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2040, matching1, i2040, matching2) → f6762_0_binomialCoefficient_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2040, 0, i2040, 0) | &&(=(matching1, 0), =(matching2, 0))
f6762_0_binomialCoefficient_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2040, matching1, i2040, matching2) → f6792_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2040, 0) | &&(=(matching1, 0), =(matching2, 0))
f6792_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2040, matching1) → f6818_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2040, 0) | =(matching1, 0)
f6818_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2040, matching1) → f6855_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2040, 0) | =(matching1, 0)
f6344_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907, i1871, i1907, i1907) → f6377_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907, i1871, i1907)
f6377_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907, i1871, i1907) → f6407_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907, i1907, i1871)
f6407_0_binomialCoefficient_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907, i1907, i1871) → f6445_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907, i1871, i1907)
f6445_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907, i1871, i1907) → f6486_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907, -(i1871, i1907)) | &&(>(i1871, 0), >(i1907, 0))
f6486_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907, i1964) → f6498_0_fact_Load(EOS, i1964, i1964)
f6486_0_binomialCoefficient_InvokeMethod(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907, i1964) → f6498_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907, i1964, i1964)
f6498_0_fact_Load(EOS, i1964, i1964) → f6512_0_fact_Load(EOS, i1964, i1964)
f6605_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907, i2044, i2044) → f6655_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907)
f6655_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907) → f6664_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907)
f6664_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907) → f6724_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907)
f6724_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907) → f6773_0_binomialCoefficient_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907)
f6773_0_binomialCoefficient_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907) → f6797_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907)
f6797_0_main_StackPop(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907) → f6823_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907)
f6823_0_main_JMP(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907) → f6862_0_main_Inc(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907)
f6606_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907, i2048) → f6664_0_binomialCoefficient_IntArithmetic(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907)
f6229_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, matching1, matching2, i1809, matching3, i1809, matching4, matching5) → f6255_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, 0, 0, i1809, 0, i1809, 0, 0) | &&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 0))
f6229_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1863, i1863, i1809, i1863, i1809, i1863, i1863) → f6256_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1809, i1863, i1863, i1809, i1863, i1809, i1863)
f6281_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, matching1, matching2, i1879, matching3, i1879, i1879, i1879) → f6335_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, 0, 0, i1879, 0, i1879, i1879, i1879) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f6281_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, matching1, matching2, i1883, matching3, i1883, i1883, i1883) → f6336_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, 0, 0, i1883, 0, i1883, i1883) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f6488_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, matching1, matching2, i1879, matching3, matching4) → f6589_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, 0, 0, i1879, 0, 0) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
f6488_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, matching1, matching2, i1879, i1992, i1992) → f6590_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1879, 0, 0, i1879, i1992) | &&(=(matching1, 0), =(matching2, 0))
f6489_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, matching1, matching2, i1883, i1996, i1996) → f6591_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1883, 0, 0, i1883, i1996, i1996) | &&(=(matching1, 0), =(matching2, 0))
f6283_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863, i1863, i1887, i1863, i1887, i1887, i1887) → f6337_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863, i1863, i1887, i1863, i1887, i1887, i1887)
f6283_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891, i1863, i1891, i1891, i1891) → f6339_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891, i1863, i1891, i1891)
f6491_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863, i1863, i1887, i2008, i2008) → f6595_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1887, i1863, i1863, i1887, i2008)
f6492_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891, i2012, i2012) → f6596_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891, i2012, i2012)
f6492_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891, i2016, i2016) → f6597_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1891, i1863, i1863, i1891, i2016)
f6231_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1810, i1867, i1810, i1867, i1810, i1867, i1867) → f6257_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1810, i1867, i1810, i1867, i1810, i1867, i1867)
f6231_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1810, i1871, i1810, i1871, i1810, i1871, i1871) → f6258_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1810, i1871, i1810, i1871, i1810, i1871)
f6285_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, matching1, i1867, matching2, i1867, matching3, matching4, matching5) → f6340_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, 0, i1867, 0, i1867, 0, 0, 0) | &&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 0))
f6285_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899, i1867, i1899, i1867, i1899, i1899, i1899) → f6341_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899, i1867, i1899, i1867, i1899, i1899)
f6494_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2020, matching1, i2020, matching2, i2020, i2020) → f6598_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2020, 0, i2020, 0, i2020, i2020) | &&(=(matching1, 0), =(matching2, 0))
f6495_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899, i1867, i1899, i2028, i2028) → f6601_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1867, i1899, i1867, i1899, i2028, i2028)
f6287_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, matching1, i1871, matching2, i1871, matching3, matching4, matching5) → f6343_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, 0, i1871, 0, i1871, 0, 0, 0) | &&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 0))
f6287_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907, i1871, i1907, i1907, i1907) → f6344_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907, i1871, i1907, i1907)
f6496_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2040, matching1, i2040, matching2, i2040, i2040) → f6604_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i2040, 0, i2040, 0, i2040) | &&(=(matching1, 0), =(matching2, 0))
f6498_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907, i2044, i2044) → f6605_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907, i2044, i2044)
f6498_1_fact_Load(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907, i2048, i2048) → f6606_0_fact_Return(EOS, java.lang.Object(ARRAY(i1)), java.lang.Object(ARRAY(i1)), i1871, i1907, i1871, i1907, i2048)

Combined rules. Obtained 21 IRules

P rules:
f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x2, x0) → f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), +(x1, 1), 0, 0, x0) | &&(&&(>(x2, x0), <=(+(x1, 1), x0)), >(+(x0, 1), 0))
f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x2, x0) → f6232_0_fact_Load(EOS, x2, x2) | &&(<=(x2, x0), >(x2, x1))
f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x2, x0) → f6234_0_fact_Load(EOS, x1, x1) | &&(<=(x2, x0), <=(x2, x1))
f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, 0, 0, x0) → f6288_0_fact_Load(EOS, x1, x1) | &&(>(+(x0, 1), 0), <(x1, 0))
f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x2, x0) → f6290_0_fact_Load(EOS, x1, x1) | &&(<=(x2, x0), >(x2, x1))
f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, 0, 0, x0) → f6500_0_fact_Load(EOS, -(0, x1), -(0, x1)) | &&(>(+(x0, 1), 0), <(x1, 0))
f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, 0, 0, x0) → f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, 1, 1, x0) | &&(<(x1, 0), >(+(x0, 1), 0))
f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x2, x0) → f6504_0_fact_Load(EOS, -(x2, x1), -(x2, x1)) | &&(&&(&&(>(x2, x1), >(x2, 0)), <=(x1, 0)), <=(x2, x0))
f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x2, x0) → f6505_0_fact_Load(EOS, -(x2, x1), -(x2, x1)) | &&(&&(&&(>(x2, x1), >(x2, 0)), >(x1, 0)), <=(x2, x0))
f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x2, x0) → f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, +(x2, 1), +(x2, 1), x0) | &&(&&(&&(&&(>(x2, x1), >(x2, 0)), <=(x2, x0)), >(+(x0, 1), 0)), <=(x1, 0))
f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x2, x0) → f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, +(x2, 1), +(x2, 1), x0) | &&(&&(&&(&&(>(x2, x1), >(x2, 0)), <=(x2, x0)), >(+(x0, 1), 0)), >(x1, 0))
f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x2, x0) → f6292_0_fact_Load(EOS, x2, x2) | &&(<=(x2, x0), <=(x2, x1))
f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x2, x0) → f6294_0_fact_Load(EOS, x2, x2) | &&(<=(x2, x0), <=(x2, x1))
f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), 0, 0, 0, x0) → f6507_0_fact_Load(EOS, 0, 0) | >(+(x0, 1), 0)
f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x2, x0) → f6509_0_fact_Load(EOS, -(x1, x2), -(x1, x2)) | &&(&&(&&(>(x2, 0), <=(x2, x1)), <=(x1, 0)), <=(x2, x0))
f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), 0, 0, 0, x0) → f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), 0, 1, 1, x0) | >(+(x0, 1), 0)
f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x2, x0) → f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, +(x2, 1), +(x2, 1), x0) | &&(&&(&&(&&(>(x2, 0), <=(x2, x1)), <=(x2, x0)), >(+(x0, 1), 0)), <=(x1, 0))
f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), arith, 0, 0, x0) → f6510_0_fact_Load(EOS, arith, arith) | &&(>(arith, 0), >(+(x0, 1), 0))
f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x2, x0) → f6512_0_fact_Load(EOS, -(x1, x2), -(x1, x2)) | &&(&&(&&(>(x2, 0), <=(x2, x1)), >(x1, 0)), <=(x2, x0))
f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), arith, 0, 0, x0) → f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), arith, 1, 1, x0) | &&(>(+(x0, 1), 0), >(arith, 0))
f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x2, x0) → f6028_0_main_GT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, +(x2, 1), +(x2, 1), x0) | &&(&&(&&(&&(>(x2, 0), <=(x2, x1)), <=(x2, x0)), >(+(x0, 1), 0)), >(x1, 0))

Filtered ground terms:


f6028_0_main_GT(x1, x2, x3, x4, x5, x6, x7) → f6028_0_main_GT(x2, x3, x4, x5, x6, x7)
Cond_f6028_0_main_GT(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f6028_0_main_GT(x1, x3, x4, x5, x6, x7, x8)
Cond_f6028_0_main_GT1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f6028_0_main_GT1(x1, x3, x4, x5, x6, x7, x8)
f6232_0_fact_Load(x1, x2, x3) → f6232_0_fact_Load(x2, x3)
Cond_f6028_0_main_GT2(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f6028_0_main_GT2(x1, x3, x4, x5, x6, x7, x8)
f6234_0_fact_Load(x1, x2, x3) → f6234_0_fact_Load(x2, x3)
Cond_f6028_0_main_GT3(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f6028_0_main_GT3(x1, x3, x4, x5, x8)
f6288_0_fact_Load(x1, x2, x3) → f6288_0_fact_Load(x2, x3)
Cond_f6028_0_main_GT4(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f6028_0_main_GT4(x1, x3, x4, x5, x6, x7, x8)
f6290_0_fact_Load(x1, x2, x3) → f6290_0_fact_Load(x2, x3)
Cond_f6028_0_main_GT5(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f6028_0_main_GT5(x1, x3, x4, x5, x8)
f6500_0_fact_Load(x1, x2, x3) → f6500_0_fact_Load(x2, x3)
Cond_f6028_0_main_GT6(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f6028_0_main_GT6(x1, x3, x4, x5, x8)
Cond_f6028_0_main_GT7(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f6028_0_main_GT7(x1, x3, x4, x5, x6, x7, x8)
f6504_0_fact_Load(x1, x2, x3) → f6504_0_fact_Load(x2, x3)
Cond_f6028_0_main_GT8(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f6028_0_main_GT8(x1, x3, x4, x5, x6, x7, x8)
f6505_0_fact_Load(x1, x2, x3) → f6505_0_fact_Load(x2, x3)
Cond_f6028_0_main_GT9(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f6028_0_main_GT9(x1, x3, x4, x5, x6, x7, x8)
Cond_f6028_0_main_GT10(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f6028_0_main_GT10(x1, x3, x4, x5, x6, x7, x8)
Cond_f6028_0_main_GT11(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f6028_0_main_GT11(x1, x3, x4, x5, x6, x7, x8)
f6292_0_fact_Load(x1, x2, x3) → f6292_0_fact_Load(x2, x3)
Cond_f6028_0_main_GT12(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f6028_0_main_GT12(x1, x3, x4, x5, x6, x7, x8)
f6294_0_fact_Load(x1, x2, x3) → f6294_0_fact_Load(x2, x3)
Cond_f6028_0_main_GT13(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f6028_0_main_GT13(x1, x3, x4, x8)
f6507_0_fact_Load(x1, x2, x3) → f6507_0_fact_Load
Cond_f6028_0_main_GT14(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f6028_0_main_GT14(x1, x3, x4, x5, x6, x7, x8)
f6509_0_fact_Load(x1, x2, x3) → f6509_0_fact_Load(x2, x3)
Cond_f6028_0_main_GT15(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f6028_0_main_GT15(x1, x3, x4, x8)
Cond_f6028_0_main_GT16(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f6028_0_main_GT16(x1, x3, x4, x5, x6, x7, x8)
Cond_f6028_0_main_GT17(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f6028_0_main_GT17(x1, x3, x4, x5, x8)
f6510_0_fact_Load(x1, x2, x3) → f6510_0_fact_Load(x2, x3)
Cond_f6028_0_main_GT18(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f6028_0_main_GT18(x1, x3, x4, x5, x6, x7, x8)
f6512_0_fact_Load(x1, x2, x3) → f6512_0_fact_Load(x2, x3)
Cond_f6028_0_main_GT19(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f6028_0_main_GT19(x1, x3, x4, x5, x8)
Cond_f6028_0_main_GT20(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f6028_0_main_GT20(x1, x3, x4, x5, x6, x7, x8)

Filtered duplicate terms:


f6028_0_main_GT(x1, x2, x3, x4, x5, x6) → f6028_0_main_GT(x2, x3, x5)
Cond_f6028_0_main_GT(x1, x2, x3, x4, x5, x6, x7) → Cond_f6028_0_main_GT(x1, x3, x4, x6)
Cond_f6028_0_main_GT1(x1, x2, x3, x4, x5, x6, x7) → Cond_f6028_0_main_GT1(x1, x3, x4, x6)
f6232_0_fact_Load(x1, x2) → f6232_0_fact_Load(x2)
Cond_f6028_0_main_GT2(x1, x2, x3, x4, x5, x6, x7) → Cond_f6028_0_main_GT2(x1, x3, x4, x6)
f6234_0_fact_Load(x1, x2) → f6234_0_fact_Load(x2)
Cond_f6028_0_main_GT3(x1, x2, x3, x4, x5) → Cond_f6028_0_main_GT3(x1, x3, x4)
f6288_0_fact_Load(x1, x2) → f6288_0_fact_Load(x2)
Cond_f6028_0_main_GT4(x1, x2, x3, x4, x5, x6, x7) → Cond_f6028_0_main_GT4(x1, x3, x4, x6)
f6290_0_fact_Load(x1, x2) → f6290_0_fact_Load(x2)
Cond_f6028_0_main_GT5(x1, x2, x3, x4, x5) → Cond_f6028_0_main_GT5(x1, x3, x4)
f6500_0_fact_Load(x1, x2) → f6500_0_fact_Load(x2)
Cond_f6028_0_main_GT6(x1, x2, x3, x4, x5) → Cond_f6028_0_main_GT6(x1, x3, x4)
Cond_f6028_0_main_GT7(x1, x2, x3, x4, x5, x6, x7) → Cond_f6028_0_main_GT7(x1, x3, x4, x6)
f6504_0_fact_Load(x1, x2) → f6504_0_fact_Load(x2)
Cond_f6028_0_main_GT8(x1, x2, x3, x4, x5, x6, x7) → Cond_f6028_0_main_GT8(x1, x3, x4, x6)
f6505_0_fact_Load(x1, x2) → f6505_0_fact_Load(x2)
Cond_f6028_0_main_GT9(x1, x2, x3, x4, x5, x6, x7) → Cond_f6028_0_main_GT9(x1, x3, x4, x6)
Cond_f6028_0_main_GT10(x1, x2, x3, x4, x5, x6, x7) → Cond_f6028_0_main_GT10(x1, x3, x4, x6)
Cond_f6028_0_main_GT11(x1, x2, x3, x4, x5, x6, x7) → Cond_f6028_0_main_GT11(x1, x3, x4, x6)
f6292_0_fact_Load(x1, x2) → f6292_0_fact_Load(x2)
Cond_f6028_0_main_GT12(x1, x2, x3, x4, x5, x6, x7) → Cond_f6028_0_main_GT12(x1, x3, x4, x6)
f6294_0_fact_Load(x1, x2) → f6294_0_fact_Load(x2)
Cond_f6028_0_main_GT13(x1, x2, x3, x4) → Cond_f6028_0_main_GT13(x1, x3)
Cond_f6028_0_main_GT14(x1, x2, x3, x4, x5, x6, x7) → Cond_f6028_0_main_GT14(x1, x3, x4, x6)
f6509_0_fact_Load(x1, x2) → f6509_0_fact_Load(x2)
Cond_f6028_0_main_GT15(x1, x2, x3, x4) → Cond_f6028_0_main_GT15(x1, x3)
Cond_f6028_0_main_GT16(x1, x2, x3, x4, x5, x6, x7) → Cond_f6028_0_main_GT16(x1, x3, x4, x6)
Cond_f6028_0_main_GT17(x1, x2, x3, x4, x5) → Cond_f6028_0_main_GT17(x1, x3, x4)
f6510_0_fact_Load(x1, x2) → f6510_0_fact_Load(x2)
Cond_f6028_0_main_GT18(x1, x2, x3, x4, x5, x6, x7) → Cond_f6028_0_main_GT18(x1, x3, x4, x6)
f6512_0_fact_Load(x1, x2) → f6512_0_fact_Load(x2)
Cond_f6028_0_main_GT19(x1, x2, x3, x4, x5) → Cond_f6028_0_main_GT19(x1, x3, x4)
Cond_f6028_0_main_GT20(x1, x2, x3, x4, x5, x6, x7) → Cond_f6028_0_main_GT20(x1, x3, x4, x6)

Filtered unneeded terms:


Cond_f6028_0_main_GT(x1, x2, x3, x4) → Cond_f6028_0_main_GT(x1, x2, x3)
Cond_f6028_0_main_GT1(x1, x2, x3, x4) → Cond_f6028_0_main_GT1(x1)
Cond_f6028_0_main_GT2(x1, x2, x3, x4) → Cond_f6028_0_main_GT2(x1)
Cond_f6028_0_main_GT3(x1, x2, x3) → Cond_f6028_0_main_GT3(x1)
Cond_f6028_0_main_GT4(x1, x2, x3, x4) → Cond_f6028_0_main_GT4(x1)
Cond_f6028_0_main_GT5(x1, x2, x3) → Cond_f6028_0_main_GT5(x1)
Cond_f6028_0_main_GT7(x1, x2, x3, x4) → Cond_f6028_0_main_GT7(x1)
Cond_f6028_0_main_GT8(x1, x2, x3, x4) → Cond_f6028_0_main_GT8(x1)
Cond_f6028_0_main_GT11(x1, x2, x3, x4) → Cond_f6028_0_main_GT11(x1)
Cond_f6028_0_main_GT12(x1, x2, x3, x4) → Cond_f6028_0_main_GT12(x1)
Cond_f6028_0_main_GT13(x1, x2) → Cond_f6028_0_main_GT13(x1)
Cond_f6028_0_main_GT14(x1, x2, x3, x4) → Cond_f6028_0_main_GT14(x1)
Cond_f6028_0_main_GT17(x1, x2, x3) → Cond_f6028_0_main_GT17(x1)
Cond_f6028_0_main_GT18(x1, x2, x3, x4) → Cond_f6028_0_main_GT18(x1)

Prepared 21 rules for path length conversion:

P rules:
f6028_0_main_GT(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f6028_0_main_GT(java.lang.Object(ARRAY(x0)), +(x1, 1), 0, x0) | &&(&&(>(x2, x0), <=(+(x1, 1), x0)), >(+(x0, 1), 0))
f6028_0_main_GT(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f6232_0_fact_Load(x2) | &&(<=(x2, x0), >(x2, x1))
f6028_0_main_GT(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f6234_0_fact_Load(x1) | &&(<=(x2, x0), <=(x2, x1))
f6028_0_main_GT(java.lang.Object(ARRAY(x0)), x1, 0, x0) → f6288_0_fact_Load(x1) | &&(>(+(x0, 1), 0), <(x1, 0))
f6028_0_main_GT(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f6290_0_fact_Load(x1) | &&(<=(x2, x0), >(x2, x1))
f6028_0_main_GT(java.lang.Object(ARRAY(x0)), x1, 0, x0) → f6500_0_fact_Load(-(0, x1)) | &&(>(+(x0, 1), 0), <(x1, 0))
f6028_0_main_GT(java.lang.Object(ARRAY(x0)), x1, 0, x0) → f6028_0_main_GT(java.lang.Object(ARRAY(x0)), x1, 1, x0) | &&(<(x1, 0), >(+(x0, 1), 0))
f6028_0_main_GT(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f6504_0_fact_Load(-(x2, x1)) | &&(&&(&&(>(x2, x1), >(x2, 0)), <=(x1, 0)), <=(x2, x0))
f6028_0_main_GT(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f6505_0_fact_Load(-(x2, x1)) | &&(&&(&&(>(x2, x1), >(x2, 0)), >(x1, 0)), <=(x2, x0))
f6028_0_main_GT(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f6028_0_main_GT(java.lang.Object(ARRAY(x0)), x1, +(x2, 1), x0) | &&(&&(&&(&&(>(x2, x1), >(x2, 0)), <=(x2, x0)), >(+(x0, 1), 0)), <=(x1, 0))
f6028_0_main_GT(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f6028_0_main_GT(java.lang.Object(ARRAY(x0)), x1, +(x2, 1), x0) | &&(&&(&&(&&(>(x2, x1), >(x2, 0)), <=(x2, x0)), >(+(x0, 1), 0)), >(x1, 0))
f6028_0_main_GT(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f6292_0_fact_Load(x2) | &&(<=(x2, x0), <=(x2, x1))
f6028_0_main_GT(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f6294_0_fact_Load(x2) | &&(<=(x2, x0), <=(x2, x1))
f6028_0_main_GT(java.lang.Object(ARRAY(x0)), 0, 0, x0) → f6507_0_fact_Load | >(+(x0, 1), 0)
f6028_0_main_GT(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f6509_0_fact_Load(-(x1, x2)) | &&(&&(&&(>(x2, 0), <=(x2, x1)), <=(x1, 0)), <=(x2, x0))
f6028_0_main_GT(java.lang.Object(ARRAY(x0)), 0, 0, x0) → f6028_0_main_GT(java.lang.Object(ARRAY(x0)), 0, 1, x0) | >(+(x0, 1), 0)
f6028_0_main_GT(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f6028_0_main_GT(java.lang.Object(ARRAY(x0)), x1, +(x2, 1), x0) | &&(&&(&&(&&(>(x2, 0), <=(x2, x1)), <=(x2, x0)), >(+(x0, 1), 0)), <=(x1, 0))
f6028_0_main_GT(java.lang.Object(ARRAY(x0)), arith, 0, x0) → f6510_0_fact_Load(arith) | &&(>(arith, 0), >(+(x0, 1), 0))
f6028_0_main_GT(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f6512_0_fact_Load(-(x1, x2)) | &&(&&(&&(>(x2, 0), <=(x2, x1)), >(x1, 0)), <=(x2, x0))
f6028_0_main_GT(java.lang.Object(ARRAY(x0)), arith, 0, x0) → f6028_0_main_GT(java.lang.Object(ARRAY(x0)), arith, 1, x0) | &&(>(+(x0, 1), 0), >(arith, 0))
f6028_0_main_GT(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f6028_0_main_GT(java.lang.Object(ARRAY(x0)), x1, +(x2, 1), x0) | &&(&&(&&(&&(>(x2, 0), <=(x2, x1)), <=(x2, x0)), >(+(x0, 1), 0)), >(x1, 0))

Finished conversion. Obtained 8 rules.

P rules:
f6028_0_main_GT(v58, x1, x2, x0) → f6028_0_main_GT(v59, +(x1, 1), 0, x0) | &&(&&(&&(&&(&&(>(x2, x0), <=(+(x1, 1), x0)), >(x0, -1)), >(+(v59, 1), 1)), <=(v59, v58)), >(+(v58, 1), 1))
f6028_0_main_GT(v60, x17, c0, x16) → f6028_0_main_GT(v61, x17, 1, x16) | &&(&&(&&(&&(&&(<(x17, 0), >(x16, -1)), >(+(v61, 1), 1)), <=(v61, v60)), >(+(v60, 1), 1)), =(0, c0))
f6028_0_main_GT(v62, x25, x26, x24) → f6028_0_main_GT(v63, x25, +(x26, 1), x24) | &&(&&(&&(&&(&&(&&(&&(>(x26, x25), >(x26, 0)), <=(x26, x24)), <=(x25, 0)), >(x24, -1)), >(+(v63, 1), 1)), <=(v63, v62)), >(+(v62, 1), 1))
f6028_0_main_GT(v64, x28, x29, x27) → f6028_0_main_GT(v65, x28, +(x29, 1), x27) | &&(&&(&&(&&(&&(&&(&&(>(x29, x28), >(x29, 0)), <=(x29, x27)), >(x28, 0)), >(x27, -1)), >(+(v65, 1), 1)), <=(v65, v64)), >(+(v64, 1), 1))
f6028_0_main_GT(v66, c0, c01, x40) → f6028_0_main_GT(v67, 0, 1, x40) | &&(&&(&&(&&(&&(>(x40, -1), >(+(v67, 1), 1)), <=(v67, v66)), >(+(v66, 1), 1)), =(0, c0)), =(0, c01))
f6028_0_main_GT(v68, x42, x43, x41) → f6028_0_main_GT(v69, x42, +(x43, 1), x41) | &&(&&(&&(&&(&&(&&(&&(>(x43, 0), <=(x43, x42)), <=(x43, x41)), <=(x42, 0)), >(x41, -1)), >(+(v69, 1), 1)), <=(v69, v68)), >(+(v68, 1), 1))
f6028_0_main_GT(v70, x50, c0, x49) → f6028_0_main_GT(v71, x50, 1, x49) | &&(&&(&&(&&(&&(>(x50, 0), >(x49, -1)), >(+(v71, 1), 1)), <=(v71, v70)), >(+(v70, 1), 1)), =(0, c0))
f6028_0_main_GT(v72, x52, x53, x51) → f6028_0_main_GT(v73, x52, +(x53, 1), x51) | &&(&&(&&(&&(&&(&&(&&(>(x53, 0), <=(x53, x52)), <=(x53, x51)), >(x52, 0)), >(x51, -1)), >(+(v73, 1), 1)), <=(v73, v72)), >(+(v72, 1), 1))

(12) Obligation:

Rules:
f6028_0_main_GT(v58, x1, x2, x0) → f6028_0_main_GT(v59, +(x1, 1), 0, x0) | &&(&&(&&(&&(&&(>(x2, x0), <=(+(x1, 1), x0)), >(x0, -1)), >(+(v59, 1), 1)), <=(v59, v58)), >(+(v58, 1), 1))
f6028_0_main_GT(v60, x17, c0, x16) → f6028_0_main_GT(v61, x17, 1, x16) | &&(&&(&&(&&(&&(<(x17, 0), >(x16, -1)), >(+(v61, 1), 1)), <=(v61, v60)), >(+(v60, 1), 1)), =(0, c0))
f6028_0_main_GT(v62, x25, x26, x24) → f6028_0_main_GT(v63, x25, +(x26, 1), x24) | &&(&&(&&(&&(&&(&&(&&(>(x26, x25), >(x26, 0)), <=(x26, x24)), <=(x25, 0)), >(x24, -1)), >(+(v63, 1), 1)), <=(v63, v62)), >(+(v62, 1), 1))
f6028_0_main_GT(v64, x28, x29, x27) → f6028_0_main_GT(v65, x28, +(x29, 1), x27) | &&(&&(&&(&&(&&(&&(&&(>(x29, x28), >(x29, 0)), <=(x29, x27)), >(x28, 0)), >(x27, -1)), >(+(v65, 1), 1)), <=(v65, v64)), >(+(v64, 1), 1))
f6028_0_main_GT(v66, c0, c01, x40) → f6028_0_main_GT(v67, 0, 1, x40) | &&(&&(&&(&&(&&(>(x40, -1), >(+(v67, 1), 1)), <=(v67, v66)), >(+(v66, 1), 1)), =(0, c0)), =(0, c01))
f6028_0_main_GT(v68, x42, x43, x41) → f6028_0_main_GT(v69, x42, +(x43, 1), x41) | &&(&&(&&(&&(&&(&&(&&(>(x43, 0), <=(x43, x42)), <=(x43, x41)), <=(x42, 0)), >(x41, -1)), >(+(v69, 1), 1)), <=(v69, v68)), >(+(v68, 1), 1))
f6028_0_main_GT(v70, x50, c0, x49) → f6028_0_main_GT(v71, x50, 1, x49) | &&(&&(&&(&&(&&(>(x50, 0), >(x49, -1)), >(+(v71, 1), 1)), <=(v71, v70)), >(+(v70, 1), 1)), =(0, c0))
f6028_0_main_GT(v72, x52, x53, x51) → f6028_0_main_GT(v73, x52, +(x53, 1), x51) | &&(&&(&&(&&(&&(&&(&&(>(x53, 0), <=(x53, x52)), <=(x53, x51)), >(x52, 0)), >(x51, -1)), >(+(v73, 1), 1)), <=(v73, v72)), >(+(v72, 1), 1))

(13) TerminationGraphProcessor (SOUND transformation)

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


(14) Obligation:

Rules:
f6028_0_main_GT(x0, x1, x2, x3) → f6028_0_main_GT(x4, +(x1, 1), 0, x3) | &&(&&(&&(&&(&&(>(x2, x3), <=(+(x1, 1), x3)), >(x3, -1)), >(+(x4, 1), 1)), <=(x4, x0)), >(+(x0, 1), 1))
f6028_0_main_GT(x5, x6, x7, x8) → f6028_0_main_GT(x9, x6, 1, x8) | &&(&&(&&(&&(&&(<(x6, 0), >(x8, -1)), >(+(x9, 1), 1)), <=(x9, x5)), >(+(x5, 1), 1)), =(0, x7))
f6028_0_main_GT(x10, x11, x12, x13) → f6028_0_main_GT(x14, x11, +(x12, 1), x13) | &&(&&(&&(&&(&&(&&(&&(>(x12, x11), >(x12, 0)), <=(x12, x13)), <=(x11, 0)), >(x13, -1)), >(+(x14, 1), 1)), <=(x14, x10)), >(+(x10, 1), 1))
f6028_0_main_GT(x20, x21, x22, x23) → f6028_0_main_GT(x24, 0, 1, x23) | &&(&&(&&(&&(&&(>(x23, -1), >(+(x24, 1), 1)), <=(x24, x20)), >(+(x20, 1), 1)), =(0, x21)), =(0, x22))
f6028_0_main_GT(x15, x16, x17, x18) → f6028_0_main_GT(x19, x16, +(x17, 1), x18) | &&(&&(&&(&&(&&(&&(&&(>(x17, x16), >(x17, 0)), <=(x17, x18)), >(x16, 0)), >(x18, -1)), >(+(x19, 1), 1)), <=(x19, x15)), >(+(x15, 1), 1))
f6028_0_main_GT(x35, x36, x37, x38) → f6028_0_main_GT(x39, x36, +(x37, 1), x38) | &&(&&(&&(&&(&&(&&(&&(>(x37, 0), <=(x37, x36)), <=(x37, x38)), >(x36, 0)), >(x38, -1)), >(+(x39, 1), 1)), <=(x39, x35)), >(+(x35, 1), 1))
f6028_0_main_GT(x30, x31, x32, x33) → f6028_0_main_GT(x34, x31, 1, x33) | &&(&&(&&(&&(&&(>(x31, 0), >(x33, -1)), >(+(x34, 1), 1)), <=(x34, x30)), >(+(x30, 1), 1)), =(0, x32))

(15) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:


[f6028_0_main_GT(x36, x38, x40, x42)] = -1 - x38 + x42

Therefore the following rule(s) have been dropped:


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

(16) Obligation:

Rules:
f6028_0_main_GT(x5, x6, x7, x8) → f6028_0_main_GT(x9, x6, 1, x8) | &&(&&(&&(&&(&&(<(x6, 0), >(x8, -1)), >(+(x9, 1), 1)), <=(x9, x5)), >(+(x5, 1), 1)), =(0, x7))
f6028_0_main_GT(x10, x11, x12, x13) → f6028_0_main_GT(x14, x11, +(x12, 1), x13) | &&(&&(&&(&&(&&(&&(&&(>(x12, x11), >(x12, 0)), <=(x12, x13)), <=(x11, 0)), >(x13, -1)), >(+(x14, 1), 1)), <=(x14, x10)), >(+(x10, 1), 1))
f6028_0_main_GT(x15, x16, x17, x18) → f6028_0_main_GT(x19, 0, 1, x18) | &&(&&(&&(&&(&&(>(x18, -1), >(+(x19, 1), 1)), <=(x19, x15)), >(+(x15, 1), 1)), =(0, x16)), =(0, x17))
f6028_0_main_GT(x20, x21, x22, x23) → f6028_0_main_GT(x24, x21, +(x22, 1), x23) | &&(&&(&&(&&(&&(&&(&&(>(x22, x21), >(x22, 0)), <=(x22, x23)), >(x21, 0)), >(x23, -1)), >(+(x24, 1), 1)), <=(x24, x20)), >(+(x20, 1), 1))
f6028_0_main_GT(x25, x26, x27, x28) → f6028_0_main_GT(x29, x26, +(x27, 1), x28) | &&(&&(&&(&&(&&(&&(&&(>(x27, 0), <=(x27, x26)), <=(x27, x28)), >(x26, 0)), >(x28, -1)), >(+(x29, 1), 1)), <=(x29, x25)), >(+(x25, 1), 1))
f6028_0_main_GT(x30, x31, x32, x33) → f6028_0_main_GT(x34, x31, 1, x33) | &&(&&(&&(&&(&&(>(x31, 0), >(x33, -1)), >(+(x34, 1), 1)), <=(x34, x30)), >(+(x30, 1), 1)), =(0, x32))

(17) TerminationGraphProcessor (SOUND transformation)

Constructed the termination graph and obtained 3 non-trivial SCCs.


(18) Complex Obligation (AND)

(19) Obligation:

Rules:
f6028_0_main_GT(x20, x21, x22, x23) → f6028_0_main_GT(x24, x21, +(x22, 1), x23) | &&(&&(&&(&&(&&(&&(&&(>(x22, 0), <=(x22, x21)), <=(x22, x23)), >(x21, 0)), >(x23, -1)), >(+(x24, 1), 1)), <=(x24, x20)), >(+(x20, 1), 1))

(20) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f6028_0_main_GT(x6, x8, x10, x12)] = -x10 + x12

Therefore the following rule(s) have been dropped:


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

(21) YES

(22) Obligation:

Rules:
f6028_0_main_GT(x15, x16, x17, x18) → f6028_0_main_GT(x19, x16, +(x17, 1), x18) | &&(&&(&&(&&(&&(&&(&&(>(x17, x16), >(x17, 0)), <=(x17, x18)), >(x16, 0)), >(x18, -1)), >(+(x19, 1), 1)), <=(x19, x15)), >(+(x15, 1), 1))

(23) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f6028_0_main_GT(x6, x8, x10, x12)] = -x10 + x12

Therefore the following rule(s) have been dropped:


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

(24) YES

(25) Obligation:

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

(26) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f6028_0_main_GT(x6, x8, x10, x12)] = -x10 + x12

Therefore the following rule(s) have been dropped:


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

(27) YES