Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 1174 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 JBCTerminationSCC
↳5 SCCToIntTRSProof (⇒, 354 ms)
↳6 intTRS
↳7 PolynomialOrderProcessor (⇒, 27 ms)
↳8 intTRS
↳9 PolynomialOrderProcessor (⇒, 19 ms)
↳10 intTRS
↳11 TerminationGraphProcessor (⇒, 12 ms)
↳12 intTRS
↳13 PolynomialOrderProcessor (⇒, 35 ms)
↳14 intTRS
↳15 TerminationGraphProcessor (⇒, 0 ms)
↳16 intTRS
↳17 PolynomialOrderProcessor (⇒, 26 ms)
↳18 intTRS
↳19 TerminationGraphProcessor (⇒, 0 ms)
↳20 intTRS
↳21 PolynomialOrderProcessor (⇔, 0 ms)
↳22 YES

(0) Obligation:

JBC Problem based on JBC Program:
public class Iterations {
    public static void main(String args[]) {
        for (int i = 0; i < args.length; i++) {
	    int a = 2*i;
            for (int j = 0; j < a; j++)
		for (int k = i+j; k >= 0; k--) {
		    int b = 2*i+3*j+4*k;
		    for (int l = 0; l < b; l++)
			for (int m = 1000*i+100*j+10*k+l; m >= 0; m--);
		}
	}
    }
}


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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


(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 1 SCCs.

(4) Obligation:

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

(5) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 90 IRules

P rules:
f322_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i27) → f324_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i27, java.lang.Object(ARRAY(i6)))
f324_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i27, java.lang.Object(ARRAY(i6))) → f326_0_main_GE(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i27, i6) | >=(i6, 0)
f326_0_main_GE(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i27, i6) → f329_0_main_GE(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i27, i6)
f329_0_main_GE(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i27, i6) → f333_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27) | <(i27, i6)
f333_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27) → f337_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, 2)
f337_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, matching1) → f338_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, 2, i27) | =(matching1, 2)
f338_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, matching1, i27) → f341_0_main_Store(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, *(2, i27)) | =(matching1, 2)
f341_0_main_Store(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i29) → f342_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i29)
f342_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i29) → f344_0_main_Store(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i29, 0)
f344_0_main_Store(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i29, matching1) → f346_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i29, 0) | =(matching1, 0)
f346_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i29, matching1) → f712_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i29, 0) | =(matching1, 0)
f712_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i69) → f1000_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i69)
f1000_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i113) → f1273_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i113)
f1273_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i158) → f1508_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i158)
f1508_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206) → f1510_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i206)
f1510_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i206) → f1512_0_main_GE(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i206, i68)
f1512_0_main_GE(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i206, i68) → f1513_0_main_GE(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i206, i68)
f1512_0_main_GE(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i206, i68) → f1514_0_main_GE(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i206, i68)
f1513_0_main_GE(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i206, i68) → f1515_0_main_Inc(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27) | >=(i206, i68)
f1515_0_main_Inc(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27) → f1518_0_main_JMP(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), +(i27, 1)) | >=(i27, 0)
f1518_0_main_JMP(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i208) → f1522_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i208)
f1522_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i208) → f318_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i208)
f318_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27) → f322_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i27)
f1514_0_main_GE(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i206, i68) → f1517_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206) | <(i206, i68)
f1517_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206) → f1520_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i27)
f1520_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i27) → f1524_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i27, i206)
f1524_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i27, i206) → f1679_0_main_Store(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, +(i27, i206)) | &&(>=(i27, 0), >=(i206, 0))
f1679_0_main_Store(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i241) → f1681_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i241)
f1681_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i241) → f1726_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i241)
f1726_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i250) → f1729_0_main_LT(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i250, i250)
f1729_0_main_LT(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i254, i254) → f1731_0_main_LT(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i254, i254)
f1729_0_main_LT(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i255) → f1732_0_main_LT(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i255)
f1731_0_main_LT(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i254, i254) → f1733_0_main_Inc(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206) | <(i254, 0)
f1733_0_main_Inc(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206) → f1736_0_main_JMP(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, +(i206, 1)) | >=(i206, 0)
f1736_0_main_JMP(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i256) → f1742_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i256)
f1742_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i256) → f1508_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i256)
f1732_0_main_LT(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i255) → f1735_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255) | >=(i255, 0)
f1735_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255) → f1738_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, 2)
f1738_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, matching1) → f1743_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, 2, i27) | =(matching1, 2)
f1743_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, matching1, i27) → f2015_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, *(2, i27)) | =(matching1, 2)
f2015_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i297) → f2016_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i297, 3)
f2016_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i297, matching1) → f2018_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i297, 3, i206) | =(matching1, 3)
f2018_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i297, matching1, i206) → f2019_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i297, *(3, i206)) | =(matching1, 3)
f2019_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i297, i298) → f2021_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, +(i297, i298)) | &&(>=(i297, 0), >=(i298, 0))
f2021_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i299) → f2023_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i299, 4)
f2023_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i299, matching1) → f2025_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i299, 4, i255) | =(matching1, 4)
f2025_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i299, matching1, i255) → f2026_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i299, *(4, i255)) | =(matching1, 4)
f2026_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i299, i300) → f2028_0_main_Store(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, +(i299, i300)) | &&(>=(i299, 0), >=(i300, 0))
f2028_0_main_Store(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i301) → f2030_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i301)
f2030_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i301) → f2031_0_main_Store(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i301, 0)
f2031_0_main_Store(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i301, matching1) → f2033_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i301, 0) | =(matching1, 0)
f2033_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i301, matching1) → f2458_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i301, 0) | =(matching1, 0)
f2458_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i354) → f2775_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i354)
f2775_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i409) → f3039_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i409)
f3039_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i462) → f3263_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i462)
f3263_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515) → f3267_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i515)
f3267_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i515) → f3268_0_main_GE(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i515, i353)
f3268_0_main_GE(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i515, i353) → f3270_0_main_GE(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i515, i353)
f3268_0_main_GE(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i515, i353) → f3271_0_main_GE(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i515, i353)
f3270_0_main_GE(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i515, i353) → f3272_0_main_Inc(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255) | >=(i515, i353)
f3272_0_main_Inc(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255) → f3275_0_main_JMP(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, +(i255, -1)) | >=(i255, 0)
f3275_0_main_JMP(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i517) → f3280_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i517)
f3280_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i517) → f1726_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i517)
f3271_0_main_GE(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i515, i353) → f3273_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515) | <(i515, i353)
f3273_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515) → f3276_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, 1000)
f3276_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, matching1) → f3281_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, 1000, i27) | =(matching1, 1000)
f3281_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, matching1, i27) → f3506_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, *(1000, i27)) | =(matching1, 1000)
f3506_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i553) → f3508_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i553, 100)
f3508_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i553, matching1) → f3509_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i553, 100, i206) | =(matching1, 100)
f3509_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i553, matching1, i206) → f3511_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i553, *(100, i206)) | =(matching1, 100)
f3511_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i553, i554) → f3512_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, +(i553, i554)) | &&(>=(i553, 0), >=(i554, 0))
f3512_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i555) → f3514_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i555, 10)
f3514_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i555, matching1) → f3515_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i555, 10, i255) | =(matching1, 10)
f3515_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i555, matching1, i255) → f3517_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i555, *(10, i255)) | =(matching1, 10)
f3517_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i555, i556) → f3518_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, +(i555, i556)) | &&(>=(i555, 0), >=(i556, 0))
f3518_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i557) → f3520_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i557, i515)
f3520_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i557, i515) → f3521_0_main_Store(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, +(i557, i515)) | &&(>=(i557, 0), >=(i515, 0))
f3521_0_main_Store(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i558) → f3523_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i558)
f3523_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i558) → f3537_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i558)
f3537_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i560) → f3539_0_main_LT(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i560, i560)
f3539_0_main_LT(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i564, i564) → f3541_0_main_LT(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i564, i564)
f3539_0_main_LT(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i565, i565) → f3542_0_main_LT(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i565, i565)
f3541_0_main_LT(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i564, i564) → f3543_0_main_Inc(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515) | <(i564, 0)
f3543_0_main_Inc(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515) → f3547_0_main_JMP(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, +(i515, 1)) | >=(i515, 0)
f3547_0_main_JMP(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i566) → f3552_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i566)
f3552_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i566) → f3263_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i566)
f3542_0_main_LT(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i565, i565) → f3545_0_main_Inc(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i565) | >=(i565, 0)
f3545_0_main_Inc(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i565) → f3548_0_main_JMP(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, +(i565, -1)) | >=(i565, 0)
f3548_0_main_JMP(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i567) → f3556_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i567)
f3556_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i567) → f3537_0_main_Load(EOS, java.lang.Object(ARRAY(i6)), java.lang.Object(ARRAY(i6)), i27, i68, i206, i255, i353, i515, i567)

Combined rules. Obtained 8 IRules

P rules:
f1512_0_main_GE(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x3, x3, x2) → f1512_0_main_GE(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), +(x1, 1), *(2, +(x1, 1)), 0, 0, *(2, +(x1, 1))) | &&(&&(&&(>=(x3, x2), >(+(x1, 1), 0)), >(+(x0, 1), 0)), <(+(x1, 1), x0))
f1512_0_main_GE(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x3, x3, x2) → f1729_0_main_LT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x3, +(x1, x3), +(x1, x3)) | &&(&&(>(+(x3, 1), 0), >(+(x1, 1), 0)), <(x3, x2))
f1729_0_main_LT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, x4) → f1512_0_main_GE(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, +(x3, 1), +(x3, 1), x2) | &&(>(+(x3, 1), 0), <(x4, 0))
f1729_0_main_LT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, x4) → f3268_0_main_GE(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, +(+(*(2, x1), *(3, x3)), *(4, x4)), 0, 0, +(+(*(2, x1), *(3, x3)), *(4, x4))) | &&(&&(&&(&&(>(+(x4, 1), 0), >=(*(4, x4), 0)), >=(*(3, x3), 0)), >=(+(*(2, x1), *(3, x3)), 0)), >=(*(2, x1), 0))
f3268_0_main_GE(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, x5, x6, x6, x5) → f1729_0_main_LT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x3, -(x4, 1), -(x4, 1)) | &&(>(+(x4, 1), 0), >=(x6, x5))
f3268_0_main_GE(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, x5, x6, x6, x5) → f3539_0_main_LT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, x5, x6, +(+(+(*(1000, x1), *(100, x3)), *(10, x4)), x6), +(+(+(*(1000, x1), *(100, x3)), *(10, x4)), x6)) | &&(&&(&&(&&(&&(&&(>(+(x6, 1), 0), <(x6, x5)), >=(*(1000, x1), 0)), >=(+(*(1000, x1), *(100, x3)), 0)), >=(+(+(*(1000, x1), *(100, x3)), *(10, x4)), 0)), >=(*(10, x4), 0)), >=(*(100, x3), 0))
f3539_0_main_LT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, x5, x6, x7, x7) → f3268_0_main_GE(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, x5, +(x6, 1), +(x6, 1), x5) | &&(>(+(x6, 1), 0), <(x7, 0))
f3539_0_main_LT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, x5, x6, x7, x7) → f3539_0_main_LT(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, x5, x6, -(x7, 1), -(x7, 1)) | >(+(x7, 1), 0)

Filtered ground terms:


f1512_0_main_GE(x1, x2, x3, x4, x5, x6, x7, x8) → f1512_0_main_GE(x2, x3, x4, x5, x6, x7, x8)
Cond_f1512_0_main_GE(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f1512_0_main_GE(x1, x3, x4, x5, x6, x7, x8, x9)
Cond_f1512_0_main_GE1(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f1512_0_main_GE1(x1, x3, x4, x5, x6, x7, x8, x9)
f1729_0_main_LT(x1, x2, x3, x4, x5, x6, x7, x8) → f1729_0_main_LT(x2, x3, x4, x5, x6, x7, x8)
Cond_f1729_0_main_LT(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f1729_0_main_LT(x1, x3, x4, x5, x6, x7, x8, x9)
Cond_f1729_0_main_LT1(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f1729_0_main_LT1(x1, x3, x4, x5, x6, x7, x8, x9)
f3268_0_main_GE(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) → f3268_0_main_GE(x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
Cond_f3268_0_main_GE(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) → Cond_f3268_0_main_GE(x1, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
Cond_f3268_0_main_GE1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) → Cond_f3268_0_main_GE1(x1, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
f3539_0_main_LT(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) → f3539_0_main_LT(x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
Cond_f3539_0_main_LT(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) → Cond_f3539_0_main_LT(x1, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
Cond_f3539_0_main_LT1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) → Cond_f3539_0_main_LT1(x1, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)

Filtered duplicate terms:


f1512_0_main_GE(x1, x2, x3, x4, x5, x6, x7) → f1512_0_main_GE(x2, x3, x6, x7)
Cond_f1512_0_main_GE(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1512_0_main_GE(x1, x3, x4, x7, x8)
Cond_f1512_0_main_GE1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1512_0_main_GE1(x1, x3, x4, x7, x8)
f1729_0_main_LT(x1, x2, x3, x4, x5, x6, x7) → f1729_0_main_LT(x2, x3, x4, x5, x7)
Cond_f1729_0_main_LT(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1729_0_main_LT(x1, x3, x4, x5, x6, x8)
Cond_f1729_0_main_LT1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1729_0_main_LT1(x1, x3, x4, x5, x6, x8)
f3268_0_main_GE(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → f3268_0_main_GE(x2, x3, x4, x5, x6, x9, x10)
Cond_f3268_0_main_GE(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) → Cond_f3268_0_main_GE(x1, x3, x4, x5, x6, x7, x10, x11)
Cond_f3268_0_main_GE1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) → Cond_f3268_0_main_GE1(x1, x3, x4, x5, x6, x7, x10, x11)
f3539_0_main_LT(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → f3539_0_main_LT(x2, x3, x4, x5, x6, x7, x8, x10)
Cond_f3539_0_main_LT(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) → Cond_f3539_0_main_LT(x1, x3, x4, x5, x6, x7, x8, x9, x11)
Cond_f3539_0_main_LT1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) → Cond_f3539_0_main_LT1(x1, x3, x4, x5, x6, x7, x8, x9, x11)

Filtered unneeded terms:


Cond_f1512_0_main_GE(x1, x2, x3, x4, x5) → Cond_f1512_0_main_GE(x1, x2, x3)
Cond_f1729_0_main_LT(x1, x2, x3, x4, x5, x6) → Cond_f1729_0_main_LT(x1, x2, x3, x4, x5)
Cond_f3268_0_main_GE(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f3268_0_main_GE(x1, x2, x3, x4, x5, x6)
Cond_f3539_0_main_LT(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f3539_0_main_LT(x1, x2, x3, x4, x5, x6, x7, x8)

Prepared 8 rules for path length conversion:

P rules:
f1512_0_main_GE(java.lang.Object(ARRAY(x0)), x1, x3, x2, x0) → f1512_0_main_GE(java.lang.Object(ARRAY(x0)), +(x1, 1), 0, *(2, +(x1, 1)), x0) | &&(&&(&&(>=(x3, x2), >(+(x1, 1), 0)), >(+(x0, 1), 0)), <(+(x1, 1), x0))
f1512_0_main_GE(java.lang.Object(ARRAY(x0)), x1, x3, x2, x0) → f1729_0_main_LT(java.lang.Object(ARRAY(x0)), x1, x2, x3, +(x1, x3), x0) | &&(&&(>(+(x3, 1), 0), >(+(x1, 1), 0)), <(x3, x2))
f1729_0_main_LT(java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, x0) → f1512_0_main_GE(java.lang.Object(ARRAY(x0)), x1, +(x3, 1), x2, x0) | &&(>(+(x3, 1), 0), <(x4, 0))
f1729_0_main_LT(java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, x0) → f3268_0_main_GE(java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, 0, +(+(*(2, x1), *(3, x3)), *(4, x4)), x0) | &&(&&(&&(&&(>(+(x4, 1), 0), >=(*(4, x4), 0)), >=(*(3, x3), 0)), >=(+(*(2, x1), *(3, x3)), 0)), >=(*(2, x1), 0))
f3268_0_main_GE(java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, x6, x5, x0) → f1729_0_main_LT(java.lang.Object(ARRAY(x0)), x1, x2, x3, -(x4, 1), x0) | &&(>(+(x4, 1), 0), >=(x6, x5))
f3268_0_main_GE(java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, x6, x5, x0) → f3539_0_main_LT(java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, x5, x6, +(+(+(*(1000, x1), *(100, x3)), *(10, x4)), x6), x0) | &&(&&(&&(&&(&&(&&(>(+(x6, 1), 0), <(x6, x5)), >=(*(1000, x1), 0)), >=(+(*(1000, x1), *(100, x3)), 0)), >=(+(+(*(1000, x1), *(100, x3)), *(10, x4)), 0)), >=(*(10, x4), 0)), >=(*(100, x3), 0))
f3539_0_main_LT(java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, x5, x6, x7, x0) → f3268_0_main_GE(java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, +(x6, 1), x5, x0) | &&(>(+(x6, 1), 0), <(x7, 0))
f3539_0_main_LT(java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, x5, x6, x7, x0) → f3539_0_main_LT(java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, x5, x6, -(x7, 1), x0) | >(+(x7, 1), 0)

Finished conversion. Obtained 8 rules.

P rules:
f1512_0_main_GE(v76, x1, x2, x3, x0) → f1512_0_main_GE(v77, +(x1, 1), 0, +(*(2, x1), 2), x0) | &&(&&(&&(&&(&&(&&(<=(x3, x2), >(x1, -1)), <(+(x1, 1), x0)), >(x0, -1)), >(+(v77, 1), 1)), <=(v77, v76)), >(+(v76, 1), 1))
f1512_0_main_GE(v78, x5, x6, x7, x4) → f1729_0_main_LT(v79, x5, x7, x6, +(x5, x6), x4) | &&(&&(&&(&&(&&(>(x7, x6), >(x6, -1)), >(x5, -1)), >(+(v79, 1), 1)), <=(v79, v78)), >(+(v78, 1), 1))
f1729_0_main_LT(v80, x9, x10, x11, x12, x8) → f1512_0_main_GE(v81, x9, +(x11, 1), x10, x8) | &&(&&(&&(&&(<(x12, 0), >(x11, -1)), >(+(v81, 1), 1)), <=(v81, v80)), >(+(v80, 1), 1))
f1729_0_main_LT(v82, x14, x15, x16, x17, x13) → f3268_0_main_GE(v83, x14, x15, x16, x17, 0, +(+(*(2, x14), *(3, x16)), *(4, x17)), x13) | &&(&&(&&(&&(&&(&&(&&(>(x17, -1), >(+(v83, 1), 1)), <=(v83, v82)), >(+(v82, 1), 1)), >=(*(4, x17), 0)), >=(*(3, x16), 0)), >=(+(*(2, x14), *(3, x16)), 0)), >=(*(2, x14), 0))
f3268_0_main_GE(v84, x19, x20, x21, x22, x23, x24, x18) → f1729_0_main_LT(v85, x19, x20, x21, -(x22, 1), x18) | &&(&&(&&(&&(<=(x24, x23), >(x22, -1)), >(+(v85, 1), 1)), <=(v85, v84)), >(+(v84, 1), 1))
f3268_0_main_GE(v86, x26, x27, x28, x29, x30, x31, x25) → f3539_0_main_LT(v87, x26, x27, x28, x29, x31, x30, +(+(+(*(1000, x26), *(100, x28)), *(10, x29)), x30), x25) | &&(&&(&&(&&(&&(&&(&&(&&(&&(>(x31, x30), >(x30, -1)), >(+(v87, 1), 1)), <=(v87, v86)), >(+(v86, 1), 1)), >=(*(1000, x26), 0)), >=(+(*(1000, x26), *(100, x28)), 0)), >=(+(+(*(1000, x26), *(100, x28)), *(10, x29)), 0)), >=(*(10, x29), 0)), >=(*(100, x28), 0))
f3539_0_main_LT(v88, x33, x34, x35, x36, x37, x38, x39, x32) → f3268_0_main_GE(v89, x33, x34, x35, x36, +(x38, 1), x37, x32) | &&(&&(&&(&&(<(x39, 0), >(x38, -1)), >(+(v89, 1), 1)), <=(v89, v88)), >(+(v88, 1), 1))
f3539_0_main_LT(v90, x41, x42, x43, x44, x45, x46, x47, x40) → f3539_0_main_LT(v91, x41, x42, x43, x44, x45, x46, -(x47, 1), x40) | &&(&&(&&(>(x47, -1), >(+(v91, 1), 1)), <=(v91, v90)), >(+(v90, 1), 1))

(6) Obligation:

Rules:
f1512_0_main_GE(v76, x1, x2, x3, x0) → f1512_0_main_GE(v77, +(x1, 1), 0, +(*(2, x1), 2), x0) | &&(&&(&&(&&(&&(&&(<=(x3, x2), >(x1, -1)), <(+(x1, 1), x0)), >(x0, -1)), >(+(v77, 1), 1)), <=(v77, v76)), >(+(v76, 1), 1))
f1512_0_main_GE(v78, x5, x6, x7, x4) → f1729_0_main_LT(v79, x5, x7, x6, +(x5, x6), x4) | &&(&&(&&(&&(&&(>(x7, x6), >(x6, -1)), >(x5, -1)), >(+(v79, 1), 1)), <=(v79, v78)), >(+(v78, 1), 1))
f1729_0_main_LT(v80, x9, x10, x11, x12, x8) → f1512_0_main_GE(v81, x9, +(x11, 1), x10, x8) | &&(&&(&&(&&(<(x12, 0), >(x11, -1)), >(+(v81, 1), 1)), <=(v81, v80)), >(+(v80, 1), 1))
f1729_0_main_LT(v82, x14, x15, x16, x17, x13) → f3268_0_main_GE(v83, x14, x15, x16, x17, 0, +(+(*(2, x14), *(3, x16)), *(4, x17)), x13) | &&(&&(&&(&&(&&(&&(&&(>(x17, -1), >(+(v83, 1), 1)), <=(v83, v82)), >(+(v82, 1), 1)), >=(*(4, x17), 0)), >=(*(3, x16), 0)), >=(+(*(2, x14), *(3, x16)), 0)), >=(*(2, x14), 0))
f3268_0_main_GE(v84, x19, x20, x21, x22, x23, x24, x18) → f1729_0_main_LT(v85, x19, x20, x21, -(x22, 1), x18) | &&(&&(&&(&&(<=(x24, x23), >(x22, -1)), >(+(v85, 1), 1)), <=(v85, v84)), >(+(v84, 1), 1))
f3268_0_main_GE(v86, x26, x27, x28, x29, x30, x31, x25) → f3539_0_main_LT(v87, x26, x27, x28, x29, x31, x30, +(+(+(*(1000, x26), *(100, x28)), *(10, x29)), x30), x25) | &&(&&(&&(&&(&&(&&(&&(&&(&&(>(x31, x30), >(x30, -1)), >(+(v87, 1), 1)), <=(v87, v86)), >(+(v86, 1), 1)), >=(*(1000, x26), 0)), >=(+(*(1000, x26), *(100, x28)), 0)), >=(+(+(*(1000, x26), *(100, x28)), *(10, x29)), 0)), >=(*(10, x29), 0)), >=(*(100, x28), 0))
f3539_0_main_LT(v88, x33, x34, x35, x36, x37, x38, x39, x32) → f3268_0_main_GE(v89, x33, x34, x35, x36, +(x38, 1), x37, x32) | &&(&&(&&(&&(<(x39, 0), >(x38, -1)), >(+(v89, 1), 1)), <=(v89, v88)), >(+(v88, 1), 1))
f3539_0_main_LT(v90, x41, x42, x43, x44, x45, x46, x47, x40) → f3539_0_main_LT(v91, x41, x42, x43, x44, x45, x46, -(x47, 1), x40) | &&(&&(&&(>(x47, -1), >(+(v91, 1), 1)), <=(v91, v90)), >(+(v90, 1), 1))

(7) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:


[f1512_0_main_GE(x65, x67, x69, x71, x73)] = -1 - x67 + x73
[f1729_0_main_LT(x76, x78, x80, x82, x84, x86)] = -1 - x78 + x86
[f3268_0_main_GE(x89, x91, x93, x95, x97, x99, x101, x103)] = -1 + x103 - x91
[f3539_0_main_LT(x106, x108, x110, x112, x114, x116, x118, x120, x122)] = -1 - x108 + x122

Therefore the following rule(s) have been dropped:


f1512_0_main_GE(x0, x1, x2, x3, x4) → f1512_0_main_GE(x5, +(x1, 1), 0, +(*(2, x1), 2), x4) | &&(&&(&&(&&(&&(&&(<=(x3, x2), >(x1, -1)), <(+(x1, 1), x4)), >(x4, -1)), >(+(x5, 1), 1)), <=(x5, x0)), >(+(x0, 1), 1))

(8) Obligation:

Rules:
f1512_0_main_GE(x6, x7, x8, x9, x10) → f1729_0_main_LT(x11, x7, x9, x8, +(x7, x8), x10) | &&(&&(&&(&&(&&(>(x9, x8), >(x8, -1)), >(x7, -1)), >(+(x11, 1), 1)), <=(x11, x6)), >(+(x6, 1), 1))
f1729_0_main_LT(x12, x13, x14, x15, x16, x17) → f1512_0_main_GE(x18, x13, +(x15, 1), x14, x17) | &&(&&(&&(&&(<(x16, 0), >(x15, -1)), >(+(x18, 1), 1)), <=(x18, x12)), >(+(x12, 1), 1))
f1729_0_main_LT(x19, x20, x21, x22, x23, x24) → f3268_0_main_GE(x25, x20, x21, x22, x23, 0, +(+(*(2, x20), *(3, x22)), *(4, x23)), x24) | &&(&&(&&(&&(&&(&&(&&(>(x23, -1), >(+(x25, 1), 1)), <=(x25, x19)), >(+(x19, 1), 1)), >=(*(4, x23), 0)), >=(*(3, x22), 0)), >=(+(*(2, x20), *(3, x22)), 0)), >=(*(2, x20), 0))
f3268_0_main_GE(x26, x27, x28, x29, x30, x31, x32, x33) → f1729_0_main_LT(x34, x27, x28, x29, -(x30, 1), x33) | &&(&&(&&(&&(<=(x32, x31), >(x30, -1)), >(+(x34, 1), 1)), <=(x34, x26)), >(+(x26, 1), 1))
f3268_0_main_GE(x35, x36, x37, x38, x39, x40, x41, x42) → f3539_0_main_LT(x43, x36, x37, x38, x39, x41, x40, +(+(+(*(1000, x36), *(100, x38)), *(10, x39)), x40), x42) | &&(&&(&&(&&(&&(&&(&&(&&(&&(>(x41, x40), >(x40, -1)), >(+(x43, 1), 1)), <=(x43, x35)), >(+(x35, 1), 1)), >=(*(1000, x36), 0)), >=(+(*(1000, x36), *(100, x38)), 0)), >=(+(+(*(1000, x36), *(100, x38)), *(10, x39)), 0)), >=(*(10, x39), 0)), >=(*(100, x38), 0))
f3539_0_main_LT(x44, x45, x46, x47, x48, x49, x50, x51, x52) → f3268_0_main_GE(x53, x45, x46, x47, x48, +(x50, 1), x49, x52) | &&(&&(&&(&&(<(x51, 0), >(x50, -1)), >(+(x53, 1), 1)), <=(x53, x44)), >(+(x44, 1), 1))
f3539_0_main_LT(x54, x55, x56, x57, x58, x59, x60, x61, x62) → f3539_0_main_LT(x63, x55, x56, x57, x58, x59, x60, -(x61, 1), x62) | &&(&&(&&(>(x61, -1), >(+(x63, 1), 1)), <=(x63, x54)), >(+(x54, 1), 1))

(9) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:


[f1512_0_main_GE(x59, x61, x63, x65, x67)] = x61 - x63 + x65
[f1729_0_main_LT(x70, x72, x74, x76, x78, x80)] = -1 + x72 + x74 - x76
[f3268_0_main_GE(x83, x85, x87, x89, x91, x93, x95, x97)] = -1 + x85 + x87 - x89
[f3539_0_main_LT(x100, x102, x104, x106, x108, x110, x112, x114, x116)] = -1 + x102 + x104 - x106

Therefore the following rule(s) have been dropped:


f1512_0_main_GE(x0, x1, x2, x3, x4) → f1729_0_main_LT(x5, x1, x3, x2, +(x1, x2), x4) | &&(&&(&&(&&(&&(>(x3, x2), >(x2, -1)), >(x1, -1)), >(+(x5, 1), 1)), <=(x5, x0)), >(+(x0, 1), 1))

(10) Obligation:

Rules:
f1729_0_main_LT(x6, x7, x8, x9, x10, x11) → f1512_0_main_GE(x12, x7, +(x9, 1), x8, x11) | &&(&&(&&(&&(<(x10, 0), >(x9, -1)), >(+(x12, 1), 1)), <=(x12, x6)), >(+(x6, 1), 1))
f1729_0_main_LT(x13, x14, x15, x16, x17, x18) → f3268_0_main_GE(x19, x14, x15, x16, x17, 0, +(+(*(2, x14), *(3, x16)), *(4, x17)), x18) | &&(&&(&&(&&(&&(&&(&&(>(x17, -1), >(+(x19, 1), 1)), <=(x19, x13)), >(+(x13, 1), 1)), >=(*(4, x17), 0)), >=(*(3, x16), 0)), >=(+(*(2, x14), *(3, x16)), 0)), >=(*(2, x14), 0))
f3268_0_main_GE(x20, x21, x22, x23, x24, x25, x26, x27) → f1729_0_main_LT(x28, x21, x22, x23, -(x24, 1), x27) | &&(&&(&&(&&(<=(x26, x25), >(x24, -1)), >(+(x28, 1), 1)), <=(x28, x20)), >(+(x20, 1), 1))
f3268_0_main_GE(x29, x30, x31, x32, x33, x34, x35, x36) → f3539_0_main_LT(x37, x30, x31, x32, x33, x35, x34, +(+(+(*(1000, x30), *(100, x32)), *(10, x33)), x34), x36) | &&(&&(&&(&&(&&(&&(&&(&&(&&(>(x35, x34), >(x34, -1)), >(+(x37, 1), 1)), <=(x37, x29)), >(+(x29, 1), 1)), >=(*(1000, x30), 0)), >=(+(*(1000, x30), *(100, x32)), 0)), >=(+(+(*(1000, x30), *(100, x32)), *(10, x33)), 0)), >=(*(10, x33), 0)), >=(*(100, x32), 0))
f3539_0_main_LT(x38, x39, x40, x41, x42, x43, x44, x45, x46) → f3268_0_main_GE(x47, x39, x40, x41, x42, +(x44, 1), x43, x46) | &&(&&(&&(&&(<(x45, 0), >(x44, -1)), >(+(x47, 1), 1)), <=(x47, x38)), >(+(x38, 1), 1))
f3539_0_main_LT(x48, x49, x50, x51, x52, x53, x54, x55, x56) → f3539_0_main_LT(x57, x49, x50, x51, x52, x53, x54, -(x55, 1), x56) | &&(&&(&&(>(x55, -1), >(+(x57, 1), 1)), <=(x57, x48)), >(+(x48, 1), 1))

(11) TerminationGraphProcessor (SOUND transformation)

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


(12) Obligation:

Rules:
f1729_0_main_LT(x7, x8, x9, x10, x11, x12) → f3268_0_main_GE(x13, x8, x9, x10, x11, 0, +(+(*(2, x8), *(3, x10)), *(4, x11)), x12) | &&(&&(&&(&&(&&(&&(&&(>(x11, -1), >(+(x13, 1), 1)), <=(x13, x7)), >(+(x7, 1), 1)), >=(*(4, x11), 0)), >=(*(3, x10), 0)), >=(+(*(2, x8), *(3, x10)), 0)), >=(*(2, x8), 0))
f3268_0_main_GE(x14, x15, x16, x17, x18, x19, x20, x21) → f1729_0_main_LT(x22, x15, x16, x17, -(x18, 1), x21) | &&(&&(&&(&&(<=(x20, x19), >(x18, -1)), >(+(x22, 1), 1)), <=(x22, x14)), >(+(x14, 1), 1))
f3539_0_main_LT(x32, x33, x34, x35, x36, x37, x38, x39, x40) → f3268_0_main_GE(x41, x33, x34, x35, x36, +(x38, 1), x37, x40) | &&(&&(&&(&&(<(x39, 0), >(x38, -1)), >(+(x41, 1), 1)), <=(x41, x32)), >(+(x32, 1), 1))
f3539_0_main_LT(x42, x43, x44, x45, x46, x47, x48, x49, x50) → f3539_0_main_LT(x51, x43, x44, x45, x46, x47, x48, -(x49, 1), x50) | &&(&&(&&(>(x49, -1), >(+(x51, 1), 1)), <=(x51, x42)), >(+(x42, 1), 1))
f3268_0_main_GE(x23, x24, x25, x26, x27, x28, x29, x30) → f3539_0_main_LT(x31, x24, x25, x26, x27, x29, x28, +(+(+(*(1000, x24), *(100, x26)), *(10, x27)), x28), x30) | &&(&&(&&(&&(&&(&&(&&(&&(&&(>(x29, x28), >(x28, -1)), >(+(x31, 1), 1)), <=(x31, x23)), >(+(x23, 1), 1)), >=(*(1000, x24), 0)), >=(+(*(1000, x24), *(100, x26)), 0)), >=(+(+(*(1000, x24), *(100, x26)), *(10, x27)), 0)), >=(*(10, x27), 0)), >=(*(100, x26), 0))

(13) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:


[f1729_0_main_LT(x46, x48, x50, x52, x54, x56)] = 9·x48 + x52 + x54
[f3268_0_main_GE(x59, x61, x63, x65, x67, x69, x71, x73)] = -1 + 9·x61 + x65 + x67
[f3539_0_main_LT(x76, x78, x80, x82, x84, x86, x88, x90, x92)] = -1 + 9·x78 + x82 + x84

Therefore the following rule(s) have been dropped:


f1729_0_main_LT(x0, x1, x2, x3, x4, x5) → f3268_0_main_GE(x6, x1, x2, x3, x4, 0, +(+(*(2, x1), *(3, x3)), *(4, x4)), x5) | &&(&&(&&(&&(&&(&&(&&(>(x4, -1), >(+(x6, 1), 1)), <=(x6, x0)), >(+(x0, 1), 1)), >=(*(4, x4), 0)), >=(*(3, x3), 0)), >=(+(*(2, x1), *(3, x3)), 0)), >=(*(2, x1), 0))

(14) Obligation:

Rules:
f3268_0_main_GE(x7, x8, x9, x10, x11, x12, x13, x14) → f1729_0_main_LT(x15, x8, x9, x10, -(x11, 1), x14) | &&(&&(&&(&&(<=(x13, x12), >(x11, -1)), >(+(x15, 1), 1)), <=(x15, x7)), >(+(x7, 1), 1))
f3539_0_main_LT(x16, x17, x18, x19, x20, x21, x22, x23, x24) → f3268_0_main_GE(x25, x17, x18, x19, x20, +(x22, 1), x21, x24) | &&(&&(&&(&&(<(x23, 0), >(x22, -1)), >(+(x25, 1), 1)), <=(x25, x16)), >(+(x16, 1), 1))
f3539_0_main_LT(x26, x27, x28, x29, x30, x31, x32, x33, x34) → f3539_0_main_LT(x35, x27, x28, x29, x30, x31, x32, -(x33, 1), x34) | &&(&&(&&(>(x33, -1), >(+(x35, 1), 1)), <=(x35, x26)), >(+(x26, 1), 1))
f3268_0_main_GE(x36, x37, x38, x39, x40, x41, x42, x43) → f3539_0_main_LT(x44, x37, x38, x39, x40, x42, x41, +(+(+(*(1000, x37), *(100, x39)), *(10, x40)), x41), x43) | &&(&&(&&(&&(&&(&&(&&(&&(&&(>(x42, x41), >(x41, -1)), >(+(x44, 1), 1)), <=(x44, x36)), >(+(x36, 1), 1)), >=(*(1000, x37), 0)), >=(+(*(1000, x37), *(100, x39)), 0)), >=(+(+(*(1000, x37), *(100, x39)), *(10, x40)), 0)), >=(*(10, x40), 0)), >=(*(100, x39), 0))

(15) TerminationGraphProcessor (SOUND transformation)

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


(16) Obligation:

Rules:
f3539_0_main_LT(x9, x10, x11, x12, x13, x14, x15, x16, x17) → f3268_0_main_GE(x18, x10, x11, x12, x13, +(x15, 1), x14, x17) | &&(&&(&&(&&(<(x16, 0), >(x15, -1)), >(+(x18, 1), 1)), <=(x18, x9)), >(+(x9, 1), 1))
f3539_0_main_LT(x19, x20, x21, x22, x23, x24, x25, x26, x27) → f3539_0_main_LT(x28, x20, x21, x22, x23, x24, x25, -(x26, 1), x27) | &&(&&(&&(>(x26, -1), >(+(x28, 1), 1)), <=(x28, x19)), >(+(x19, 1), 1))
f3268_0_main_GE(x29, x30, x31, x32, x33, x34, x35, x36) → f3539_0_main_LT(x37, x30, x31, x32, x33, x35, x34, +(+(+(*(1000, x30), *(100, x32)), *(10, x33)), x34), x36) | &&(&&(&&(&&(&&(&&(&&(&&(&&(>(x35, x34), >(x34, -1)), >(+(x37, 1), 1)), <=(x37, x29)), >(+(x29, 1), 1)), >=(*(1000, x30), 0)), >=(+(*(1000, x30), *(100, x32)), 0)), >=(+(+(*(1000, x30), *(100, x32)), *(10, x33)), 0)), >=(*(10, x33), 0)), >=(*(100, x32), 0))

(17) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:


[f3539_0_main_LT(x30, x32, x34, x36, x38, x40, x42, x44, x46)] = -1 + 10·x32 + x36 + x38 + x40 - x42
[f3268_0_main_GE(x49, x51, x53, x55, x57, x59, x61, x63)] = 10·x51 + x55 + x57 - x59 + x61

Therefore the following rule(s) have been dropped:


f3268_0_main_GE(x20, x21, x22, x23, x24, x25, x26, x27) → f3539_0_main_LT(x28, x21, x22, x23, x24, x26, x25, +(+(+(*(1000, x21), *(100, x23)), *(10, x24)), x25), x27) | &&(&&(&&(&&(&&(&&(&&(&&(&&(>(x26, x25), >(x25, -1)), >(+(x28, 1), 1)), <=(x28, x20)), >(+(x20, 1), 1)), >=(*(1000, x21), 0)), >=(+(*(1000, x21), *(100, x23)), 0)), >=(+(+(*(1000, x21), *(100, x23)), *(10, x24)), 0)), >=(*(10, x24), 0)), >=(*(100, x23), 0))

(18) Obligation:

Rules:
f3539_0_main_LT(x0, x1, x2, x3, x4, x5, x6, x7, x8) → f3268_0_main_GE(x9, x1, x2, x3, x4, +(x6, 1), x5, x8) | &&(&&(&&(&&(<(x7, 0), >(x6, -1)), >(+(x9, 1), 1)), <=(x9, x0)), >(+(x0, 1), 1))
f3539_0_main_LT(x10, x11, x12, x13, x14, x15, x16, x17, x18) → f3539_0_main_LT(x19, x11, x12, x13, x14, x15, x16, -(x17, 1), x18) | &&(&&(&&(>(x17, -1), >(+(x19, 1), 1)), <=(x19, x10)), >(+(x10, 1), 1))

(19) TerminationGraphProcessor (SOUND transformation)

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


(20) Obligation:

Rules:
f3539_0_main_LT(x10, x11, x12, x13, x14, x15, x16, x17, x18) → f3539_0_main_LT(x19, x11, x12, x13, x14, x15, x16, -(x17, 1), x18) | &&(&&(&&(>(x17, -1), >(+(x19, 1), 1)), <=(x19, x10)), >(+(x10, 1), 1))

(21) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f3539_0_main_LT(x11, x13, x15, x17, x19, x21, x23, x25, x27)] = x25

Therefore the following rule(s) have been dropped:


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

(22) YES