Termination proof of /tmp/tmpwldsgx/KnapsackDP.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 8130 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIntTRSProof (⇒, 161 ms)

        ↳7 intTRS

        ↳8 PolynomialOrderProcessor (⇒, 0 ms)

        ↳9 intTRS

        ↳10 LinearRankingProcessor (⇔, 12 ms)

        ↳11 YES

    ↳12 JBCTerminationSCC

        ↳13 SCCToIntTRSProof (⇒, 41 ms)

        ↳14 intTRS

        ↳15 PolynomialOrderProcessor (⇒, 0 ms)

        ↳16 intTRS

        ↳17 TerminationGraphProcessor (⇒, 10 ms)

        ↳18 intTRS

        ↳19 PolynomialOrderProcessor (⇔, 0 ms)

        ↳20 YES

    ↳21 JBCTerminationSCC

        ↳22 SCCToIntTRSProof (⇒, 449 ms)

        ↳23 intTRS

        ↳24 PolynomialOrderProcessor (⇒, 0 ms)

        ↳25 intTRS

        ↳26 PolynomialOrderProcessor (⇔, 0 ms)

        ↳27 YES

    ↳28 JBCTerminationSCC

        ↳29 SCCToIntTRSProof (⇒, 136 ms)

        ↳30 intTRS

        ↳31 TerminationGraphProcessor (⇒, 17 ms)

        ↳32 AND

            ↳33 intTRS

                ↳34 PolynomialOrderProcessor (⇔, 0 ms)

                ↳35 YES

            ↳36 intTRS

                ↳37 PolynomialOrderProcessor (⇔, 0 ms)

                ↳38 YES

(0) Obligation:

JBC Problem based on JBC Program:

class KnapsackDP
{
    static int nbObjects;
    static int [] weight={2,3,5,2,4,6,3,1};
    static int [] utility={5,8,14,6,13,17,10,4};
    static int weightmax=12;
    static int [] [] array;

    // Display the table
    static void consoleDisplay()
    {
	int i,j;
	for(i=0;i<nbObjects;i++) 
	    {
		for(j=0;j<=weightmax;j++)
		    {
			//System.out.print(array[i][j]+"\t");
		    }
		//System.out.println("");
	    }
    }

    // LateX
    static void Display()
    {
	int i,j;
	for(i=0;i<nbObjects;i++) 
	    {
		for(j=0;j<=weightmax;j++)
		    {
			if (j!=weightmax) {} //System.out.print(array[i][j]+" & ");
			else {} //System.out.print(array[i][j]+" ");
		    }
		//System.out.println("\\\\");
	    }
}

    // Extract the solution from the table
    static void InterpretArray()
    {
	int i,u,w;
	u=0;
	w=weightmax;
	
	for(i=nbObjects-1;i>=1;i--)
	    {
		if (array[i][w]!=array[i-1][w])
		    {
			//System.out.print((i+1)+" ");
			w=w-weight[i];
			u=u+utility[i];
		    }
	    }

	if (array[0][w]!=0);	
	{
	    //System.out.println("1");
	    w=w-weight[0];
	    u=u+utility[0];
	}
	
	//System.out.println("Cross check:"+u+" remaining weight "+w);
}

    static int max(int a, int b)
    {
	//if (a>b) return a; else return b;
	return ( (a>b) ? (a) : (b) );
    }

    static void SolveDP()
    {
	int i,j;
	array=new int[nbObjects][weightmax+1];
	
	// initialize the first row	
	for(j=0;j<=weightmax;j++)
	    if (j<weight[0]) array[0][j]=0; 
	    else array[0][j]=utility[0];			
	// for all other rows
	for(i=1;i<nbObjects;i++)
	    {
		for(j=0;j<=weightmax;j++)
		    if (j-weight[i]<0) array[i][j]=array[i-1][j];
		    else
			array[i][j]=max( array[i-1][j],
					 array[i-1][j-weight[i]]+utility[i]);	
	    }
    }

    public static void main(String[] args)
    {
	//System.out.println("Solving knapsack using the dynamic programming paradigm.");
	nbObjects = args.length;
	SolveDP();
	Display();
	//System.out.println("Reading solution:");
	InterpretArray();
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
KnapsackDP.main([Ljava/lang/String;)V: Graph of 1214 nodes with 4 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 4 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: KnapsackDP.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:

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 48 IRules

P rules:
f26860_0_InterpretArray_ConstantStackPush(EOS, java.lang.Object(ARRAY(i7514)), i13892, i13894, i13892) → f26861_0_InterpretArray_LT(EOS, java.lang.Object(ARRAY(i7514)), i13892, i13894, i13892, 1)
f26861_0_InterpretArray_LT(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13894, i13902, matching1) → f26863_0_InterpretArray_LT(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13894, i13902, 1) | =(matching1, 1)
f26863_0_InterpretArray_LT(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13894, i13902, matching1) → f26865_0_InterpretArray_FieldAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13894) | &&(>=(i13902, 1), =(matching1, 1))
f26865_0_InterpretArray_FieldAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13894) → f26867_0_InterpretArray_Load(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13894, java.lang.Object(ARRAY(i7514)))
f26867_0_InterpretArray_Load(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13894, java.lang.Object(ARRAY(i7514))) → f26869_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13894, java.lang.Object(ARRAY(i7514)), i13902)
f26869_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13894, java.lang.Object(ARRAY(i7514)), i13902) → f26872_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13894, java.lang.Object(ARRAY(i7514)), i13902)
f26872_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13894, java.lang.Object(ARRAY(i7514)), i13902) → f26876_0_InterpretArray_Load(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13894, o31512) | <(i13902, i7514)
f26876_0_InterpretArray_Load(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13894, o31512) → f26879_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13894, o31512, i13894)
f26879_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13894, java.lang.Object(o31535put), i13894) → f26883_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13894, java.lang.Object(o31535put), i13894)
f26883_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13894, java.lang.Object(ARRAY(i13923)), i13894) → f26889_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13894, java.lang.Object(ARRAY(i13923)), i13894) | >=(i13923, 0)
f26889_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, java.lang.Object(ARRAY(i13923)), i13927) → f26896_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, java.lang.Object(ARRAY(i13923)), i13927)
f26896_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, java.lang.Object(ARRAY(i13923)), i13927) → f26903_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, java.lang.Object(ARRAY(i13923)), i13927)
f26903_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, java.lang.Object(ARRAY(i13923)), i13927) → f26910_0_InterpretArray_FieldAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949) | <(i13927, i13923)
f26910_0_InterpretArray_FieldAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949) → f26919_0_InterpretArray_Load(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949, java.lang.Object(ARRAY(i7514)))
f26919_0_InterpretArray_Load(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949, java.lang.Object(ARRAY(i7514))) → f26927_0_InterpretArray_ConstantStackPush(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949, java.lang.Object(ARRAY(i7514)), i13902)
f26927_0_InterpretArray_ConstantStackPush(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949, java.lang.Object(ARRAY(i7514)), i13902) → f26934_0_InterpretArray_IntArithmetic(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949, java.lang.Object(ARRAY(i7514)), i13902, 1)
f26934_0_InterpretArray_IntArithmetic(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949, java.lang.Object(ARRAY(i7514)), i13902, matching1) → f26942_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949, java.lang.Object(ARRAY(i7514)), -(i13902, 1)) | &&(>(i13902, 0), =(matching1, 1))
f26942_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949, java.lang.Object(ARRAY(i7514)), i14073) → f26949_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949, java.lang.Object(ARRAY(i7514)), i14073)
f26949_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949, java.lang.Object(ARRAY(i7514)), i14073) → f26957_0_InterpretArray_Load(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949, o32120) | <(i14073, i7514)
f26957_0_InterpretArray_Load(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949, o32120) → f26966_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949, o32120, i13927)
f26966_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949, java.lang.Object(o32290put), i13927) → f26973_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949, java.lang.Object(o32290put), i13927)
f26973_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949, java.lang.Object(ARRAY(i14257)), i13927) → f26982_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949, java.lang.Object(ARRAY(i14257)), i13927) | >=(i14257, 0)
f26982_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949, java.lang.Object(ARRAY(i14257)), i13927) → f26993_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949, java.lang.Object(ARRAY(i14257)), i13927)
f26993_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949, java.lang.Object(ARRAY(i14257)), i13927) → f27004_0_InterpretArray_EQ(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949, i14398) | <(i13927, i14257)
f27004_0_InterpretArray_EQ(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i14398, i14398) → f27014_0_InterpretArray_EQ(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i14398, i14398)
f27004_0_InterpretArray_EQ(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949, i14398) → f27015_0_InterpretArray_EQ(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949, i14398)
f27014_0_InterpretArray_EQ(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i14398, i14398) → f27026_0_InterpretArray_Inc(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927)
f27026_0_InterpretArray_Inc(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927) → f27038_0_InterpretArray_JMP(EOS, java.lang.Object(ARRAY(i7514)), +(i13902, -1), i13927) | >(i13902, 0)
f27038_0_InterpretArray_JMP(EOS, java.lang.Object(ARRAY(i7514)), i14696, i13927) → f27051_0_InterpretArray_Load(EOS, java.lang.Object(ARRAY(i7514)), i14696, i13927)
f27051_0_InterpretArray_Load(EOS, java.lang.Object(ARRAY(i7514)), i14696, i13927) → f26859_0_InterpretArray_Load(EOS, java.lang.Object(ARRAY(i7514)), i14696, i13927)
f26859_0_InterpretArray_Load(EOS, java.lang.Object(ARRAY(i7514)), i13892, i13894) → f26860_0_InterpretArray_ConstantStackPush(EOS, java.lang.Object(ARRAY(i7514)), i13892, i13894, i13892)
f27015_0_InterpretArray_EQ(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, i13949, i14398) → f27027_0_InterpretArray_Load(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927) | !(=(i13949, i14398))
f27027_0_InterpretArray_Load(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927) → f27039_0_InterpretArray_FieldAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927)
f27039_0_InterpretArray_FieldAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927) → f27052_0_InterpretArray_Load(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, java.lang.Object(ARRAY(8)))
f27052_0_InterpretArray_Load(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, java.lang.Object(ARRAY(matching1))) → f27064_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i13902, i13927, java.lang.Object(ARRAY(8)), i13902) | =(matching1, 8)
f27064_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i15118, i13927, java.lang.Object(ARRAY(matching1)), i15118) → f27075_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i15118, i13927, java.lang.Object(ARRAY(8)), i15118) | =(matching1, 8)
f27075_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i15118, i13927, java.lang.Object(ARRAY(matching1)), i15118) → f27087_0_InterpretArray_IntArithmetic(EOS, java.lang.Object(ARRAY(i7514)), i15118, i13927, i15261) | &&(<(i15118, 8), =(matching1, 8))
f27087_0_InterpretArray_IntArithmetic(EOS, java.lang.Object(ARRAY(i7514)), i15118, i13927, i15261) → f27099_0_InterpretArray_Store(EOS, java.lang.Object(ARRAY(i7514)), i15118, -(i13927, i15261)) | >=(i13927, 0)
f27099_0_InterpretArray_Store(EOS, java.lang.Object(ARRAY(i7514)), i15118, i15394) → f27110_0_InterpretArray_Load(EOS, java.lang.Object(ARRAY(i7514)), i15118, i15394)
f27110_0_InterpretArray_Load(EOS, java.lang.Object(ARRAY(i7514)), i15118, i15394) → f27122_0_InterpretArray_FieldAccess(EOS, java.lang.Object(ARRAY(i7514)), i15118, i15394)
f27122_0_InterpretArray_FieldAccess(EOS, java.lang.Object(ARRAY(i7514)), i15118, i15394) → f27132_0_InterpretArray_Load(EOS, java.lang.Object(ARRAY(i7514)), i15118, i15394, java.lang.Object(ARRAY(8)))
f27132_0_InterpretArray_Load(EOS, java.lang.Object(ARRAY(i7514)), i15118, i15394, java.lang.Object(ARRAY(matching1))) → f27142_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i15118, i15394, java.lang.Object(ARRAY(8)), i15118) | =(matching1, 8)
f27142_0_InterpretArray_ArrayAccess(EOS, java.lang.Object(ARRAY(i7514)), i15118, i15394, java.lang.Object(ARRAY(matching1)), i15118) → f27151_0_InterpretArray_IntArithmetic(EOS, java.lang.Object(ARRAY(i7514)), i15118, i15394) | &&(<(i15118, 8), =(matching1, 8))
f27151_0_InterpretArray_IntArithmetic(EOS, java.lang.Object(ARRAY(i7514)), i15118, i15394) → f27159_0_InterpretArray_Store(EOS, java.lang.Object(ARRAY(i7514)), i15118, i15394)
f27159_0_InterpretArray_Store(EOS, java.lang.Object(ARRAY(i7514)), i15118, i15394) → f27167_0_InterpretArray_Inc(EOS, java.lang.Object(ARRAY(i7514)), i15118, i15394)
f27167_0_InterpretArray_Inc(EOS, java.lang.Object(ARRAY(i7514)), i15118, i15394) → f27175_0_InterpretArray_JMP(EOS, java.lang.Object(ARRAY(i7514)), +(i15118, -1), i15394) | >(i15118, 0)
f27175_0_InterpretArray_JMP(EOS, java.lang.Object(ARRAY(i7514)), i16275, i15394) → f27181_0_InterpretArray_Load(EOS, java.lang.Object(ARRAY(i7514)), i16275, i15394)
f27181_0_InterpretArray_Load(EOS, java.lang.Object(ARRAY(i7514)), i16275, i15394) → f26859_0_InterpretArray_Load(EOS, java.lang.Object(ARRAY(i7514)), i16275, i15394)

Combined rules. Obtained 2 IRules

P rules:
f26860_0_InterpretArray_ConstantStackPush(EOS, java.lang.Object(ARRAY(x0)), x1, x2, x1) → f26860_0_InterpretArray_ConstantStackPush(EOS, java.lang.Object(ARRAY(x0)), -(x1, 1), x2, -(x1, 1)) | &&(&&(>(+(x1, 1), 1), <(-(x1, 1), x0)), <(x1, x0))
f26860_0_InterpretArray_ConstantStackPush(EOS, java.lang.Object(ARRAY(x0)), x1, x2, x1) → f26860_0_InterpretArray_ConstantStackPush(EOS, java.lang.Object(ARRAY(x0)), -(x1, 1), -(x2, x3), -(x1, 1)) | &&(&&(&&(&&(>(+(x2, 1), 0), >(+(x1, 1), 1)), <(x1, x0)), <(x1, 8)), <(-(x1, 1), x0))

Filtered ground terms:

f26860_0_InterpretArray_ConstantStackPush(x1, x2, x3, x4, x5) → f26860_0_InterpretArray_ConstantStackPush(x2, x3, x4, x5)
Cond_f26860_0_InterpretArray_ConstantStackPush(x1, x2, x3, x4, x5, x6) → Cond_f26860_0_InterpretArray_ConstantStackPush(x1, x3, x4, x5, x6)
Cond_f26860_0_InterpretArray_ConstantStackPush1(x1, x2, x3, x4, x5, x6, x7) → Cond_f26860_0_InterpretArray_ConstantStackPush1(x1, x3, x4, x5, x6, x7)

Filtered duplicate terms:

f26860_0_InterpretArray_ConstantStackPush(x1, x2, x3, x4) → f26860_0_InterpretArray_ConstantStackPush(x1, x3, x4)
Cond_f26860_0_InterpretArray_ConstantStackPush(x1, x2, x3, x4, x5) → Cond_f26860_0_InterpretArray_ConstantStackPush(x1, x2, x4, x5)
Cond_f26860_0_InterpretArray_ConstantStackPush1(x1, x2, x3, x4, x5, x6) → Cond_f26860_0_InterpretArray_ConstantStackPush1(x1, x2, x4, x5, x6)

Prepared 2 rules for path length conversion:

P rules:
f26860_0_InterpretArray_ConstantStackPush(java.lang.Object(ARRAY(x0)), x2, x1, x0) → f26860_0_InterpretArray_ConstantStackPush(java.lang.Object(ARRAY(x0)), x2, -(x1, 1), x0) | &&(&&(>(+(x1, 1), 1), <(-(x1, 1), x0)), <(x1, x0))
f26860_0_InterpretArray_ConstantStackPush(java.lang.Object(ARRAY(x0)), x2, x1, x0) → f26860_0_InterpretArray_ConstantStackPush(java.lang.Object(ARRAY(x0)), -(x2, x3), -(x1, 1), x0) | &&(&&(&&(&&(>(+(x2, 1), 0), >(+(x1, 1), 1)), <(x1, x0)), <(x1, 8)), <(-(x1, 1), x0))

Finished conversion. Obtained 2 rules.

P rules:
f26860_0_InterpretArray_ConstantStackPush(v11, x1, x2, x0) → f26860_0_InterpretArray_ConstantStackPush(v12, x1, -(x2, 1), x0) | &&(&&(&&(&&(&&(>(x2, 0), <(x2, x0)), <(-(x2, 1), x0)), >(+(v12, 1), 1)), <=(v12, v11)), >(+(v11, 1), 1))
f26860_0_InterpretArray_ConstantStackPush(v13, x4, x5, x3) → f26860_0_InterpretArray_ConstantStackPush(v14, -(x4, x6), -(x5, 1), x3) | &&(&&(&&(&&(&&(&&(&&(>(x5, 0), <(x5, x3)), <(x5, 8)), <(-(x5, 1), x3)), >(x4, -1)), >(+(v14, 1), 1)), <=(v14, v13)), >(+(v13, 1), 1))

(7) Obligation:

Rules:
f26860_0_InterpretArray_ConstantStackPush(v11, x1, x2, x0) → f26860_0_InterpretArray_ConstantStackPush(v12, x1, -(x2, 1), x0) | &&(&&(&&(&&(&&(>(x2, 0), <(x2, x0)), <(-(x2, 1), x0)), >(+(v12, 1), 1)), <=(v12, v11)), >(+(v11, 1), 1))
f26860_0_InterpretArray_ConstantStackPush(v13, x4, x5, x3) → f26860_0_InterpretArray_ConstantStackPush(v14, -(x4, x6), -(x5, 1), x3) | &&(&&(&&(&&(&&(&&(&&(>(x5, 0), <(x5, x3)), <(x5, 8)), <(-(x5, 1), x3)), >(x4, -1)), >(+(v14, 1), 1)), <=(v14, v13)), >(+(v13, 1), 1))

(8) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:

[f26860_0_InterpretArray_ConstantStackPush(x12, x14, x16, x18)] = x16

Therefore the following rule(s) have been dropped:

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

(9) Obligation:

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

(10) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:

[f26860_0_InterpretArray_ConstantStackPush(x)] = 1·x₃

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

Therefore the following rule(s) have been dropped:

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

(11) YES

(12) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: KnapsackDP.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:

(13) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 31 IRules

P rules:
f26275_0_Display_FieldAccess(EOS, java.lang.Object(ARRAY(i7514)), i10772, i10772) → f26288_0_Display_GE(EOS, java.lang.Object(ARRAY(i7514)), i10772, i10772, i7514)
f26288_0_Display_GE(EOS, java.lang.Object(ARRAY(i7514)), i10772, i10772, i7514) → f26301_0_Display_GE(EOS, java.lang.Object(ARRAY(i7514)), i10772, i10772, i7514)
f26301_0_Display_GE(EOS, java.lang.Object(ARRAY(i7514)), i10772, i10772, i7514) → f26315_0_Display_ConstantStackPush(EOS, java.lang.Object(ARRAY(i7514)), i10772) | <(i10772, i7514)
f26315_0_Display_ConstantStackPush(EOS, java.lang.Object(ARRAY(i7514)), i10772) → f26328_0_Display_Store(EOS, java.lang.Object(ARRAY(i7514)), i10772, 0)
f26328_0_Display_Store(EOS, java.lang.Object(ARRAY(i7514)), i10772, matching1) → f26342_0_Display_Load(EOS, java.lang.Object(ARRAY(i7514)), i10772, 0) | =(matching1, 0)
f26342_0_Display_Load(EOS, java.lang.Object(ARRAY(i7514)), i10772, matching1) → f26434_0_Display_Load(EOS, java.lang.Object(ARRAY(i7514)), i10772, 0) | =(matching1, 0)
f26434_0_Display_Load(EOS, java.lang.Object(ARRAY(i7514)), i10772, i11298) → f26508_0_Display_Load(EOS, java.lang.Object(ARRAY(i7514)), i10772, i11298)
f26508_0_Display_Load(EOS, java.lang.Object(ARRAY(i7514)), i10772, i11471) → f26590_0_Display_Load(EOS, java.lang.Object(ARRAY(i7514)), i10772, i11471)
f26590_0_Display_Load(EOS, java.lang.Object(ARRAY(i7514)), i10772, i11635) → f26670_0_Display_Load(EOS, java.lang.Object(ARRAY(i7514)), i10772, i11635)
f26670_0_Display_Load(EOS, java.lang.Object(ARRAY(i7514)), i10772, i11979) → f26683_0_Display_FieldAccess(EOS, java.lang.Object(ARRAY(i7514)), i10772, i11979, i11979)
f26683_0_Display_FieldAccess(EOS, java.lang.Object(ARRAY(i7514)), i10772, i11979, i11979) → f26697_0_Display_GT(EOS, java.lang.Object(ARRAY(i7514)), i10772, i11979, i11979, 12)
f26697_0_Display_GT(EOS, java.lang.Object(ARRAY(i7514)), i10772, i12235, i12235, matching1) → f26709_0_Display_GT(EOS, java.lang.Object(ARRAY(i7514)), i10772, i12235, i12235, 12) | =(matching1, 12)
f26697_0_Display_GT(EOS, java.lang.Object(ARRAY(i7514)), i10772, i12236, i12236, matching1) → f26710_0_Display_GT(EOS, java.lang.Object(ARRAY(i7514)), i10772, i12236, i12236, 12) | =(matching1, 12)
f26709_0_Display_GT(EOS, java.lang.Object(ARRAY(i7514)), i10772, i12235, i12235, matching1) → f26723_0_Display_Load(EOS, java.lang.Object(ARRAY(i7514)), i10772, i12235) | &&(<=(i12235, 12), =(matching1, 12))
f26723_0_Display_Load(EOS, java.lang.Object(ARRAY(i7514)), i10772, i12235) → f26737_0_Display_FieldAccess(EOS, java.lang.Object(ARRAY(i7514)), i10772, i12235, i12235)
f26737_0_Display_FieldAccess(EOS, java.lang.Object(ARRAY(i7514)), i10772, i12235, i12235) → f26750_0_Display_EQ(EOS, java.lang.Object(ARRAY(i7514)), i10772, i12235, i12235, 12)
f26750_0_Display_EQ(EOS, java.lang.Object(ARRAY(i7514)), i10772, i12684, i12684, matching1) → f26763_0_Display_EQ(EOS, java.lang.Object(ARRAY(i7514)), i10772, i12684, i12684, 12) | =(matching1, 12)
f26750_0_Display_EQ(EOS, java.lang.Object(ARRAY(i7514)), i10772, matching1, matching2, matching3) → f26764_0_Display_EQ(EOS, java.lang.Object(ARRAY(i7514)), i10772, 12, 12, 12) | &&(&&(&&(=(i12235, 12), =(matching1, 12)), =(matching2, 12)), =(matching3, 12))
f26763_0_Display_EQ(EOS, java.lang.Object(ARRAY(i7514)), i10772, i12684, i12684, matching1) → f26776_0_Display_Inc(EOS, java.lang.Object(ARRAY(i7514)), i10772, i12684) | &&(<(i12684, 12), =(matching1, 12))
f26776_0_Display_Inc(EOS, java.lang.Object(ARRAY(i7514)), i10772, i12684) → f26787_0_Display_JMP(EOS, java.lang.Object(ARRAY(i7514)), i10772, +(i12684, 1)) | >=(i12684, 0)
f26787_0_Display_JMP(EOS, java.lang.Object(ARRAY(i7514)), i10772, i12964) → f26799_0_Display_Load(EOS, java.lang.Object(ARRAY(i7514)), i10772, i12964)
f26799_0_Display_Load(EOS, java.lang.Object(ARRAY(i7514)), i10772, i12964) → f26670_0_Display_Load(EOS, java.lang.Object(ARRAY(i7514)), i10772, i12964)
f26764_0_Display_EQ(EOS, java.lang.Object(ARRAY(i7514)), i10772, matching1, matching2, matching3) → f26777_0_Display_Inc(EOS, java.lang.Object(ARRAY(i7514)), i10772, 12) | &&(&&(=(matching1, 12), =(matching2, 12)), =(matching3, 12))
f26777_0_Display_Inc(EOS, java.lang.Object(ARRAY(i7514)), i10772, matching1) → f26788_0_Display_JMP(EOS, java.lang.Object(ARRAY(i7514)), i10772, 13) | =(matching1, 12)
f26788_0_Display_JMP(EOS, java.lang.Object(ARRAY(i7514)), i10772, matching1) → f26800_0_Display_Load(EOS, java.lang.Object(ARRAY(i7514)), i10772, 13) | =(matching1, 13)
f26800_0_Display_Load(EOS, java.lang.Object(ARRAY(i7514)), i10772, matching1) → f26670_0_Display_Load(EOS, java.lang.Object(ARRAY(i7514)), i10772, 13) | =(matching1, 13)
f26710_0_Display_GT(EOS, java.lang.Object(ARRAY(i7514)), i10772, i12236, i12236, matching1) → f26724_0_Display_Inc(EOS, java.lang.Object(ARRAY(i7514)), i10772) | &&(>(i12236, 12), =(matching1, 12))
f26724_0_Display_Inc(EOS, java.lang.Object(ARRAY(i7514)), i10772) → f26738_0_Display_JMP(EOS, java.lang.Object(ARRAY(i7514)), +(i10772, 1)) | >=(i10772, 0)
f26738_0_Display_JMP(EOS, java.lang.Object(ARRAY(i7514)), i12465) → f26751_0_Display_Load(EOS, java.lang.Object(ARRAY(i7514)), i12465)
f26751_0_Display_Load(EOS, java.lang.Object(ARRAY(i7514)), i12465) → f26260_0_Display_Load(EOS, java.lang.Object(ARRAY(i7514)), i12465)
f26260_0_Display_Load(EOS, java.lang.Object(ARRAY(i7514)), i10772) → f26275_0_Display_FieldAccess(EOS, java.lang.Object(ARRAY(i7514)), i10772, i10772)

Combined rules. Obtained 3 IRules

P rules:
f26697_0_Display_GT(EOS, java.lang.Object(ARRAY(x0)), x1, x2, x2, 12) → f26697_0_Display_GT(EOS, java.lang.Object(ARRAY(x0)), x1, +(x2, 1), +(x2, 1), 12) | &&(<(x2, 12), >(+(x2, 1), 0))
f26697_0_Display_GT(EOS, java.lang.Object(ARRAY(x0)), x1, 12, 12, 12) → f26697_0_Display_GT(EOS, java.lang.Object(ARRAY(x0)), x1, 13, 13, 12)
f26697_0_Display_GT(EOS, java.lang.Object(ARRAY(x0)), x1, x2, x2, 12) → f26697_0_Display_GT(EOS, java.lang.Object(ARRAY(x0)), +(x1, 1), 0, 0, 12) | &&(&&(>(x2, 12), <(+(x1, 1), x0)), >(+(x1, 1), 0))

Filtered ground terms:

f26697_0_Display_GT(x1, x2, x3, x4, x5, x6) → f26697_0_Display_GT(x2, x3, x4, x5)
Cond_f26697_0_Display_GT(x1, x2, x3, x4, x5, x6, x7) → Cond_f26697_0_Display_GT(x1, x3, x4, x5, x6)
Cond_f26697_0_Display_GT1(x1, x2, x3, x4, x5, x6, x7) → Cond_f26697_0_Display_GT1(x1, x3, x4, x5, x6)

Filtered duplicate terms:

f26697_0_Display_GT(x1, x2, x3, x4) → f26697_0_Display_GT(x1, x2, x4)
Cond_f26697_0_Display_GT(x1, x2, x3, x4, x5) → Cond_f26697_0_Display_GT(x1, x2, x3, x5)
Cond_f26697_0_Display_GT1(x1, x2, x3, x4, x5) → Cond_f26697_0_Display_GT1(x1, x2, x3, x5)

Filtered unneeded terms:

Cond_f26697_0_Display_GT1(x1, x2, x3, x4) → Cond_f26697_0_Display_GT1(x1, x2, x3)

Prepared 3 rules for path length conversion:

P rules:
f26697_0_Display_GT(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f26697_0_Display_GT(java.lang.Object(ARRAY(x0)), x1, +(x2, 1), x0) | &&(<(x2, 12), >(+(x2, 1), 0))
f26697_0_Display_GT(java.lang.Object(ARRAY(x0)), x1, 12, x0) → f26697_0_Display_GT(java.lang.Object(ARRAY(x0)), x1, 13, x0)
f26697_0_Display_GT(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f26697_0_Display_GT(java.lang.Object(ARRAY(x0)), +(x1, 1), 0, x0) | &&(&&(>(x2, 12), <(+(x1, 1), x0)), >(+(x1, 1), 0))

Finished conversion. Obtained 3 rules.

P rules:
f26697_0_Display_GT(v12, x1, x2, x0) → f26697_0_Display_GT(v13, x1, +(x2, 1), x0) | &&(&&(&&(&&(>(x2, -1), <(x2, 12)), >(+(v13, 1), 1)), <=(v13, v12)), >(+(v12, 1), 1))
f26697_0_Display_GT(v14, x4, c12, x3) → f26697_0_Display_GT(v15, x4, 13, x3) | &&(&&(&&(>(+(v15, 1), 1), <=(v15, v14)), >(+(v14, 1), 1)), =(12, c12))
f26697_0_Display_GT(v16, x6, x7, x5) → f26697_0_Display_GT(v17, +(x6, 1), 0, x5) | &&(&&(&&(&&(&&(>(x7, 12), >(x6, -1)), <(+(x6, 1), x5)), >(+(v17, 1), 1)), <=(v17, v16)), >(+(v16, 1), 1))

(14) Obligation:

Rules:
f26697_0_Display_GT(v12, x1, x2, x0) → f26697_0_Display_GT(v13, x1, +(x2, 1), x0) | &&(&&(&&(&&(>(x2, -1), <(x2, 12)), >(+(v13, 1), 1)), <=(v13, v12)), >(+(v12, 1), 1))
f26697_0_Display_GT(v14, x4, c12, x3) → f26697_0_Display_GT(v15, x4, 13, x3) | &&(&&(&&(>(+(v15, 1), 1), <=(v15, v14)), >(+(v14, 1), 1)), =(12, c12))
f26697_0_Display_GT(v16, x6, x7, x5) → f26697_0_Display_GT(v17, +(x6, 1), 0, x5) | &&(&&(&&(&&(&&(>(x7, 12), >(x6, -1)), <(+(x6, 1), x5)), >(+(v17, 1), 1)), <=(v17, v16)), >(+(v16, 1), 1))

(15) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:

[f26697_0_Display_GT(x16, x18, x20, x22)] = -1 - x18 + x22

Therefore the following rule(s) have been dropped:

f26697_0_Display_GT(x10, x11, x12, x13) → f26697_0_Display_GT(x14, +(x11, 1), 0, x13) | &&(&&(&&(&&(&&(>(x12, 12), >(x11, -1)), <(+(x11, 1), x13)), >(+(x14, 1), 1)), <=(x14, x10)), >(+(x10, 1), 1))

(16) Obligation:

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

(17) TerminationGraphProcessor (SOUND transformation)

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

(18) Obligation:

Rules:
f26697_0_Display_GT(x0, x1, x2, x3) → f26697_0_Display_GT(x4, x1, +(x2, 1), x3) | &&(&&(&&(&&(>(x2, -1), <(x2, 12)), >(+(x4, 1), 1)), <=(x4, x0)), >(+(x0, 1), 1))

(19) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f26697_0_Display_GT(x6, x8, x10, x12)] = 11 - x10

Therefore the following rule(s) have been dropped:

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

(20) YES

(21) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: KnapsackDP.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:

(22) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 107 IRules

P rules:
f24523_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i948)), i7182, i7182) → f24524_0_SolveDP_GE(EOS, java.lang.Object(ARRAY(i948)), i7182, i7182, i948)
f24524_0_SolveDP_GE(EOS, java.lang.Object(ARRAY(i948)), i7182, i7182, i948) → f24526_0_SolveDP_GE(EOS, java.lang.Object(ARRAY(i948)), i7182, i7182, i948)
f24526_0_SolveDP_GE(EOS, java.lang.Object(ARRAY(i948)), i7182, i7182, i948) → f24528_0_SolveDP_ConstantStackPush(EOS, java.lang.Object(ARRAY(i948)), i7182) | <(i7182, i948)
f24528_0_SolveDP_ConstantStackPush(EOS, java.lang.Object(ARRAY(i948)), i7182) → f24530_0_SolveDP_Store(EOS, java.lang.Object(ARRAY(i948)), i7182, 0)
f24530_0_SolveDP_Store(EOS, java.lang.Object(ARRAY(i948)), i7182, matching1) → f24532_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i7182, 0) | =(matching1, 0)
f24532_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i7182, matching1) → f24758_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i7182, 0) | =(matching1, 0)
f24758_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i7486, i7487) → f24998_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i7486, i7487)
f24998_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i7799, i7800) → f25379_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i7799, i7800)
f25379_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i8502, i8503) → f25767_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i8502, i8503)
f25767_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9363, i9364) → f25769_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i948)), i9363, i9364, i9364)
f25769_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i948)), i9363, i9364, i9364) → f25772_0_SolveDP_GT(EOS, java.lang.Object(ARRAY(i948)), i9363, i9364, i9364, 12)
f25772_0_SolveDP_GT(EOS, java.lang.Object(ARRAY(i948)), i9363, i9370, i9370, matching1) → f25775_0_SolveDP_GT(EOS, java.lang.Object(ARRAY(i948)), i9363, i9370, i9370, 12) | =(matching1, 12)
f25772_0_SolveDP_GT(EOS, java.lang.Object(ARRAY(i948)), i9363, i9371, i9371, matching1) → f25776_0_SolveDP_GT(EOS, java.lang.Object(ARRAY(i948)), i9363, i9371, i9371, 12) | =(matching1, 12)
f25775_0_SolveDP_GT(EOS, java.lang.Object(ARRAY(i948)), i9363, i9370, i9370, matching1) → f25779_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9363, i9370) | &&(<=(i9370, 12), =(matching1, 12))
f25779_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9363, i9370) → f25783_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i948)), i9363, i9370, i9370)
f25783_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i948)), i9363, i9370, i9370) → f25786_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9363, i9370, i9370, java.lang.Object(ARRAY(8)))
f25786_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9363, i9370, i9370, java.lang.Object(ARRAY(matching1))) → f25790_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9363, i9370, i9370, java.lang.Object(ARRAY(8)), i9363) | =(matching1, 8)
f25790_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, i9370, java.lang.Object(ARRAY(matching1)), i9413) → f25793_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, i9370, java.lang.Object(ARRAY(8)), i9413) | =(matching1, 8)
f25793_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, i9370, java.lang.Object(ARRAY(matching1)), i9413) → f25797_0_SolveDP_IntArithmetic(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, i9370, i9415) | &&(<(i9413, 8), =(matching1, 8))
f25797_0_SolveDP_IntArithmetic(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, i9370, i9415) → f25801_0_SolveDP_GE(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, -(i9370, i9415)) | >=(i9370, 0)
f25801_0_SolveDP_GE(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, i9419) → f25804_0_SolveDP_GE(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, i9419)
f25801_0_SolveDP_GE(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, i9420) → f25805_0_SolveDP_GE(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, i9420)
f25804_0_SolveDP_GE(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, i9419) → f25809_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370) | <(i9419, 0)
f25809_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370) → f25815_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(ARRAY(i948)))
f25815_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(ARRAY(i948))) → f25819_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(ARRAY(i948)), i9413)
f25819_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(ARRAY(i948)), i9413) → f25824_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(ARRAY(i948)), i9413)
f25824_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(ARRAY(i948)), i9413) → f25831_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19938) | <(i9413, i948)
f25831_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19938) → f25838_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19938, i9370)
f25838_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19938, i9370) → f25844_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19938, i9370, java.lang.Object(ARRAY(i948)))
f25844_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19938, i9370, java.lang.Object(ARRAY(i948))) → f25852_0_SolveDP_ConstantStackPush(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19938, i9370, java.lang.Object(ARRAY(i948)), i9413)
f25852_0_SolveDP_ConstantStackPush(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19938, i9370, java.lang.Object(ARRAY(i948)), i9413) → f25859_0_SolveDP_IntArithmetic(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19938, i9370, java.lang.Object(ARRAY(i948)), i9413, 1)
f25859_0_SolveDP_IntArithmetic(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19938, i9370, java.lang.Object(ARRAY(i948)), i9413, matching1) → f25868_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19938, i9370, java.lang.Object(ARRAY(i948)), -(i9413, 1)) | &&(>(i9413, 0), =(matching1, 1))
f25868_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19938, i9370, java.lang.Object(ARRAY(i948)), i9461) → f25878_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19938, i9370, java.lang.Object(ARRAY(i948)), i9461)
f25878_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19938, i9370, java.lang.Object(ARRAY(i948)), i9461) → f25887_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19938, i9370, o20015) | <(i9461, i948)
f25887_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19938, i9370, o20015) → f25899_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19938, i9370, o20015, i9370)
f25899_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19938, i9370, java.lang.Object(o20094put), i9370) → f25911_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19938, i9370, java.lang.Object(o20094put), i9370)
f25911_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19938, i9370, java.lang.Object(ARRAY(i9527)), i9370) → f25927_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19938, i9370, java.lang.Object(ARRAY(i9527)), i9370) | >=(i9527, 0)
f25927_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19938, i9370, java.lang.Object(ARRAY(i9527)), i9370) → f25941_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19938, i9370, java.lang.Object(ARRAY(i9527)), i9370)
f25941_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19938, i9370, java.lang.Object(ARRAY(i9527)), i9370) → f25958_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19938, i9370) | <(i9370, i9527)
f25958_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(o20323put), i9370) → f25976_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(o20323put), i9370)
f25976_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(ARRAY(i9630)), i9370) → f25991_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(ARRAY(i9630)), i9370) | >=(i9630, 0)
f25991_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(ARRAY(i9630)), i9370) → f26008_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(ARRAY(i9630)), i9370)
f26008_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(ARRAY(i9630)), i9370) → f26027_0_SolveDP_JMP(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370) | <(i9370, i9630)
f26027_0_SolveDP_JMP(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370) → f26045_0_SolveDP_Inc(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370)
f26045_0_SolveDP_Inc(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370) → f26465_0_SolveDP_Inc(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370)
f26465_0_SolveDP_Inc(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370) → f26474_0_SolveDP_JMP(EOS, java.lang.Object(ARRAY(i948)), i9413, +(i9370, 1)) | >=(i9370, 0)
f26474_0_SolveDP_JMP(EOS, java.lang.Object(ARRAY(i948)), i9413, i11396) → f26483_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i11396)
f26483_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i11396) → f25767_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i11396)
f25805_0_SolveDP_GE(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, i9420) → f25810_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370) | >=(i9420, 0)
f25810_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370) → f25816_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(ARRAY(i948)))
f25816_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(ARRAY(i948))) → f25820_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(ARRAY(i948)), i9413)
f25820_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(ARRAY(i948)), i9413) → f25826_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(ARRAY(i948)), i9413)
f25826_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(ARRAY(i948)), i9413) → f25833_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940) | <(i9413, i948)
f25833_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940) → f25839_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370)
f25839_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370) → f25846_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, java.lang.Object(ARRAY(i948)))
f25846_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, java.lang.Object(ARRAY(i948))) → f25854_0_SolveDP_ConstantStackPush(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, java.lang.Object(ARRAY(i948)), i9413)
f25854_0_SolveDP_ConstantStackPush(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, java.lang.Object(ARRAY(i948)), i9413) → f25860_0_SolveDP_IntArithmetic(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, java.lang.Object(ARRAY(i948)), i9413, 1)
f25860_0_SolveDP_IntArithmetic(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, java.lang.Object(ARRAY(i948)), i9413, matching1) → f25870_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, java.lang.Object(ARRAY(i948)), -(i9413, 1)) | &&(>(i9413, 0), =(matching1, 1))
f25870_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, java.lang.Object(ARRAY(i948)), i9466) → f25881_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, java.lang.Object(ARRAY(i948)), i9466)
f25881_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, java.lang.Object(ARRAY(i948)), i9466) → f25889_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, o20017) | <(i9466, i948)
f25889_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, o20017) → f25901_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, o20017, i9370)
f25901_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, java.lang.Object(o20113put), i9370) → f25915_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, java.lang.Object(o20113put), i9370)
f25915_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, java.lang.Object(ARRAY(i9528)), i9370) → f25930_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, java.lang.Object(ARRAY(i9528)), i9370) | >=(i9528, 0)
f25930_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, java.lang.Object(ARRAY(i9528)), i9370) → f25945_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, java.lang.Object(ARRAY(i9528)), i9370)
f25945_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, java.lang.Object(ARRAY(i9528)), i9370) → f25962_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578) | <(i9370, i9528)
f25962_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578) → f25980_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, java.lang.Object(ARRAY(i948)))
f25980_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, java.lang.Object(ARRAY(i948))) → f25996_0_SolveDP_ConstantStackPush(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, java.lang.Object(ARRAY(i948)), i9413)
f25996_0_SolveDP_ConstantStackPush(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, java.lang.Object(ARRAY(i948)), i9413) → f26014_0_SolveDP_IntArithmetic(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, java.lang.Object(ARRAY(i948)), i9413, 1)
f26014_0_SolveDP_IntArithmetic(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, java.lang.Object(ARRAY(i948)), i9413, matching1) → f26032_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, java.lang.Object(ARRAY(i948)), -(i9413, 1)) | &&(>(i9413, 0), =(matching1, 1))
f26032_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, java.lang.Object(ARRAY(i948)), i9748) → f26050_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, java.lang.Object(ARRAY(i948)), i9748)
f26050_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, java.lang.Object(ARRAY(i948)), i9748) → f26069_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, o20920) | <(i9748, i948)
f26069_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, o20920) → f26089_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, o20920, i9370)
f26089_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, o20920, i9370) → f26107_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, o20920, i9370, java.lang.Object(ARRAY(8)))
f26107_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, o20920, i9370, java.lang.Object(ARRAY(matching1))) → f26128_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, o20920, i9370, java.lang.Object(ARRAY(8)), i9413) | =(matching1, 8)
f26128_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, o20920, i9370, java.lang.Object(ARRAY(matching1)), i9413) → f26149_0_SolveDP_IntArithmetic(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, o20920, i9370, i10173) | &&(<(i9413, 8), =(matching1, 8))
f26149_0_SolveDP_IntArithmetic(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, o20920, i9370, i10173) → f26170_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, o20920, -(i9370, i10173)) | >=(i9370, 0)
f26170_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, java.lang.Object(o22209put), i10283) → f26193_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, java.lang.Object(o22209put), i10283)
f26193_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, java.lang.Object(ARRAY(i10523)), i10283) → f26217_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, java.lang.Object(ARRAY(i10523)), i10283) | >=(i10523, 0)
f26217_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, java.lang.Object(ARRAY(i10523)), i10660) → f26241_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, java.lang.Object(ARRAY(i10523)), i10660)
f26241_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, java.lang.Object(ARRAY(i10523)), i10660) → f26268_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, java.lang.Object(ARRAY(i10523)), i10660)
f26268_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, java.lang.Object(ARRAY(i10523)), i10660) → f26281_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i10848) | <(i10660, i10523)
f26281_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i10848) → f26294_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i10848, java.lang.Object(ARRAY(8)))
f26294_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i10848, java.lang.Object(ARRAY(matching1))) → f26308_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i10848, java.lang.Object(ARRAY(8)), i9413) | =(matching1, 8)
f26308_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i10848, java.lang.Object(ARRAY(matching1)), i9413) → f26321_0_SolveDP_IntArithmetic(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i10848, i11001) | &&(<(i9413, 8), =(matching1, 8))
f26321_0_SolveDP_IntArithmetic(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i10848, i11001) → f26335_0_SolveDP_InvokeMethod(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, +(i10848, i11001))
f26335_0_SolveDP_InvokeMethod(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i11052) → f26349_0_max_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i11052, i9578, i11052)
f26349_0_max_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i11052, i9578, i11052) → f26373_0_max_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i11052, i9578, i11052, i9578)
f26373_0_max_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i11052, i9578, i11052, i9578) → f26385_0_max_LE(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i11052, i9578, i11052, i9578, i11052)
f26385_0_max_LE(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i11052, i9578, i11052, i9578, i11052) → f26394_0_max_LE(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i11052, i9578, i11052, i9578, i11052)
f26385_0_max_LE(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i11052, i9578, i11052, i9578, i11052) → f26395_0_max_LE(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i11052, i9578, i11052, i9578, i11052)
f26394_0_max_LE(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i11052, i9578, i11052, i9578, i11052) → f26406_0_max_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i11052, i11052) | <=(i9578, i11052)
f26406_0_max_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i11052, i11052) → f26417_0_max_Return(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i11052, i11052)
f26417_0_max_Return(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i11052, i11052) → f26426_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i11052)
f26426_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(o25069put), i9370, i11052) → f26437_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(o25069put), i9370, i11052)
f26437_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(ARRAY(i11329)), i9370, i11052) → f26446_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(ARRAY(i11329)), i9370, i11052) | >=(i11329, 0)
f26446_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(ARRAY(i11329)), i9370, i11052) → f26455_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(ARRAY(i11329)), i9370, i11052)
f26455_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, java.lang.Object(ARRAY(i11329)), i9370, i11052) → f26465_0_SolveDP_Inc(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370) | <(i9370, i11329)
f26395_0_max_LE(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i11052, i9578, i11052, i9578, i11052) → f26407_0_max_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i11052, i9578) | >(i9578, i11052)
f26407_0_max_Load(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i11052, i9578) → f26418_0_max_JMP(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i11052, i9578)
f26418_0_max_JMP(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i11052, i9578) → f26427_0_max_Return(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i11052, i9578)
f26427_0_max_Return(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578, i11052, i9578) → f26439_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578)
f26439_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578) → f26426_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i948)), i9413, i9370, o19940, i9370, i9578)
f25776_0_SolveDP_GT(EOS, java.lang.Object(ARRAY(i948)), i9363, i9371, i9371, matching1) → f25780_0_SolveDP_Inc(EOS, java.lang.Object(ARRAY(i948)), i9363) | &&(>(i9371, 12), =(matching1, 12))
f25780_0_SolveDP_Inc(EOS, java.lang.Object(ARRAY(i948)), i9363) → f25784_0_SolveDP_JMP(EOS, java.lang.Object(ARRAY(i948)), +(i9363, 1)) | >(i9363, 0)
f25784_0_SolveDP_JMP(EOS, java.lang.Object(ARRAY(i948)), i9372) → f25787_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9372)
f25787_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9372) → f24522_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i9372)
f24522_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i948)), i7182) → f24523_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i948)), i7182, i7182)

Combined rules. Obtained 3 IRules

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

Filtered ground terms:

f25772_0_SolveDP_GT(x1, x2, x3, x4, x5, x6) → f25772_0_SolveDP_GT(x2, x3, x4, x5)
Cond_f25772_0_SolveDP_GT(x1, x2, x3, x4, x5, x6, x7) → Cond_f25772_0_SolveDP_GT(x1, x3, x4, x5, x6)
Cond_f25772_0_SolveDP_GT1(x1, x2, x3, x4, x5, x6, x7) → Cond_f25772_0_SolveDP_GT1(x1, x3, x4, x5, x6)
Cond_f25772_0_SolveDP_GT2(x1, x2, x3, x4, x5, x6, x7) → Cond_f25772_0_SolveDP_GT2(x1, x3, x4, x5, x6)

Filtered duplicate terms:

f25772_0_SolveDP_GT(x1, x2, x3, x4) → f25772_0_SolveDP_GT(x1, x2, x4)
Cond_f25772_0_SolveDP_GT(x1, x2, x3, x4, x5) → Cond_f25772_0_SolveDP_GT(x1, x2, x3, x5)
Cond_f25772_0_SolveDP_GT1(x1, x2, x3, x4, x5) → Cond_f25772_0_SolveDP_GT1(x1, x2, x3, x5)
Cond_f25772_0_SolveDP_GT2(x1, x2, x3, x4, x5) → Cond_f25772_0_SolveDP_GT2(x1, x2, x3, x5)

Filtered unneeded terms:

Cond_f25772_0_SolveDP_GT2(x1, x2, x3, x4) → Cond_f25772_0_SolveDP_GT2(x1, x2, x3)

Prepared 3 rules for path length conversion:

P rules:
f25772_0_SolveDP_GT(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f25772_0_SolveDP_GT(java.lang.Object(ARRAY(x0)), x1, +(x2, 1), x0) | &&(&&(&&(&&(&&(>(+(x2, 1), 0), <=(x2, 12)), >(x1, 0)), <(x1, x0)), <(-(x1, 1), x0)), <(x1, 8))
f25772_0_SolveDP_GT(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f25772_0_SolveDP_GT(java.lang.Object(ARRAY(x0)), x1, +(x2, 1), x0) | &&(&&(&&(&&(&&(>(+(x2, 1), 0), <=(x2, 12)), >(x1, 0)), <(x1, x0)), <(x1, 8)), <(-(x1, 1), x0))
f25772_0_SolveDP_GT(java.lang.Object(ARRAY(x0)), x1, x2, x0) → f25772_0_SolveDP_GT(java.lang.Object(ARRAY(x0)), +(x1, 1), 0, x0) | &&(&&(>(x2, 12), <(+(x1, 1), x0)), >(x1, 0))

Finished conversion. Obtained 3 rules.

P rules:
f25772_0_SolveDP_GT(v13, x1, x2, x0) → f25772_0_SolveDP_GT(v14, x1, +(x2, 1), x0) | &&(&&(&&(&&(&&(&&(&&(&&(>(x2, -1), <=(x2, 12)), >(x1, 0)), <(x1, x0)), <(x1, 8)), <(-(x1, 1), x0)), >(+(v14, 1), 1)), <=(v14, v13)), >(+(v13, 1), 1))
f25772_0_SolveDP_GT(v15, x4, x5, x3) → f25772_0_SolveDP_GT(v16, x4, +(x5, 1), x3) | &&(&&(&&(&&(&&(&&(&&(&&(>(x5, -1), <=(x5, 12)), >(x4, 0)), <(x4, x3)), <(x4, 8)), <(-(x4, 1), x3)), >(+(v16, 1), 1)), <=(v16, v15)), >(+(v15, 1), 1))
f25772_0_SolveDP_GT(v17, x7, x8, x6) → f25772_0_SolveDP_GT(v18, +(x7, 1), 0, x6) | &&(&&(&&(&&(&&(>(x8, 12), >(x7, 0)), <(+(x7, 1), x6)), >(+(v18, 1), 1)), <=(v18, v17)), >(+(v17, 1), 1))

(23) Obligation:

Rules:
f25772_0_SolveDP_GT(v13, x1, x2, x0) → f25772_0_SolveDP_GT(v14, x1, +(x2, 1), x0) | &&(&&(&&(&&(&&(&&(&&(&&(>(x2, -1), <=(x2, 12)), >(x1, 0)), <(x1, x0)), <(x1, 8)), <(-(x1, 1), x0)), >(+(v14, 1), 1)), <=(v14, v13)), >(+(v13, 1), 1))
f25772_0_SolveDP_GT(v15, x4, x5, x3) → f25772_0_SolveDP_GT(v16, x4, +(x5, 1), x3) | &&(&&(&&(&&(&&(&&(&&(&&(>(x5, -1), <=(x5, 12)), >(x4, 0)), <(x4, x3)), <(x4, 8)), <(-(x4, 1), x3)), >(+(v16, 1), 1)), <=(v16, v15)), >(+(v15, 1), 1))
f25772_0_SolveDP_GT(v17, x7, x8, x6) → f25772_0_SolveDP_GT(v18, +(x7, 1), 0, x6) | &&(&&(&&(&&(&&(>(x8, 12), >(x7, 0)), <(+(x7, 1), x6)), >(+(v18, 1), 1)), <=(v18, v17)), >(+(v17, 1), 1))

(24) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:

[f25772_0_SolveDP_GT(x16, x18, x20, x22)] = -2 - x18 + x22

Therefore the following rule(s) have been dropped:

f25772_0_SolveDP_GT(x10, x11, x12, x13) → f25772_0_SolveDP_GT(x14, +(x11, 1), 0, x13) | &&(&&(&&(&&(&&(>(x12, 12), >(x11, 0)), <(+(x11, 1), x13)), >(+(x14, 1), 1)), <=(x14, x10)), >(+(x10, 1), 1))

(25) Obligation:

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

(26) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f25772_0_SolveDP_GT(x11, x13, x15, x17)] = 12 - x15

Therefore the following rule(s) have been dropped:

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

(27) YES

(28) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: KnapsackDP.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:

(29) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 41 IRules

P rules:
f1390_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i101)), i102, i102) → f1393_0_SolveDP_GT(EOS, java.lang.Object(ARRAY(i101)), i102, i102, 12)
f1393_0_SolveDP_GT(EOS, java.lang.Object(ARRAY(i101)), i108, i108, matching1) → f1396_0_SolveDP_GT(EOS, java.lang.Object(ARRAY(i101)), i108, i108, 12) | =(matching1, 12)
f1396_0_SolveDP_GT(EOS, java.lang.Object(ARRAY(i101)), i108, i108, matching1) → f1398_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i101)), i108) | &&(<=(i108, 12), =(matching1, 12))
f1398_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i101)), i108) → f1402_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i101)), i108, i108)
f1402_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i101)), i108, i108) → f1406_0_SolveDP_ConstantStackPush(EOS, java.lang.Object(ARRAY(i101)), i108, i108, java.lang.Object(ARRAY(8)))
f1406_0_SolveDP_ConstantStackPush(EOS, java.lang.Object(ARRAY(i101)), i108, i108, java.lang.Object(ARRAY(matching1))) → f1410_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i101)), i108, i108, java.lang.Object(ARRAY(8)), 0) | =(matching1, 8)
f1410_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i101)), i108, i108, java.lang.Object(ARRAY(matching1)), matching2) → f1416_0_SolveDP_GE(EOS, java.lang.Object(ARRAY(i101)), i108, i108, 2) | &&(&&(<(0, 8), =(matching1, 8)), =(matching2, 0))
f1416_0_SolveDP_GE(EOS, java.lang.Object(ARRAY(i101)), i114, i114, matching1) → f1422_0_SolveDP_GE(EOS, java.lang.Object(ARRAY(i101)), i114, i114, 2) | =(matching1, 2)
f1416_0_SolveDP_GE(EOS, java.lang.Object(ARRAY(i101)), i115, i115, matching1) → f1424_0_SolveDP_GE(EOS, java.lang.Object(ARRAY(i101)), i115, i115, 2) | =(matching1, 2)
f1422_0_SolveDP_GE(EOS, java.lang.Object(ARRAY(i101)), i114, i114, matching1) → f1429_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i101)), i114) | &&(<(i114, 2), =(matching1, 2))
f1429_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i101)), i114) → f1438_0_SolveDP_ConstantStackPush(EOS, java.lang.Object(ARRAY(i101)), i114, java.lang.Object(ARRAY(i101)))
f1438_0_SolveDP_ConstantStackPush(EOS, java.lang.Object(ARRAY(i101)), i114, java.lang.Object(ARRAY(i101))) → f1447_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i101)), i114, java.lang.Object(ARRAY(i101)), 0)
f1447_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i123)), i114, java.lang.Object(ARRAY(i123)), matching1) → f1457_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i123)), i114, java.lang.Object(ARRAY(i123)), 0) | =(matching1, 0)
f1457_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i123)), i114, java.lang.Object(ARRAY(i123)), matching1) → f1467_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i123)), i114, o153) | &&(<(0, i123), =(matching1, 0))
f1467_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i123)), i114, o153) → f1477_0_SolveDP_ConstantStackPush(EOS, java.lang.Object(ARRAY(i123)), i114, o153, i114)
f1477_0_SolveDP_ConstantStackPush(EOS, java.lang.Object(ARRAY(i123)), i114, o153, i114) → f1487_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i123)), i114, o153, i114, 0)
f1487_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i123)), i114, java.lang.Object(o161put), i114, matching1) → f1504_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i123)), i114, java.lang.Object(o161put), i114, 0) | =(matching1, 0)
f1504_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i123)), i114, java.lang.Object(ARRAY(i127)), i114, matching1) → f1515_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i123)), i114, java.lang.Object(ARRAY(i127)), i114, 0) | &&(>=(i127, 0), =(matching1, 0))
f1515_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i123)), i114, java.lang.Object(ARRAY(i127)), i114, matching1) → f1529_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i123)), i114, java.lang.Object(ARRAY(i127)), i114, 0) | =(matching1, 0)
f1529_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i123)), i114, java.lang.Object(ARRAY(i127)), i114, matching1) → f1551_0_SolveDP_JMP(EOS, java.lang.Object(ARRAY(i123)), i114) | &&(<(i114, i127), =(matching1, 0))
f1551_0_SolveDP_JMP(EOS, java.lang.Object(ARRAY(i123)), i114) → f1566_0_SolveDP_Inc(EOS, java.lang.Object(ARRAY(i123)), i114)
f1566_0_SolveDP_Inc(EOS, java.lang.Object(ARRAY(i123)), i114) → f1582_0_SolveDP_JMP(EOS, java.lang.Object(ARRAY(i123)), +(i114, 1)) | >=(i114, 0)
f1582_0_SolveDP_JMP(EOS, java.lang.Object(ARRAY(i123)), i129) → f1613_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i123)), i129)
f1613_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i123)), i129) → f1384_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i123)), i129)
f1384_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i101)), i102) → f1390_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i101)), i102, i102)
f1424_0_SolveDP_GE(EOS, java.lang.Object(ARRAY(i101)), i115, i115, matching1) → f1432_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i101)), i115) | &&(>=(i115, 2), =(matching1, 2))
f1432_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i101)), i115) → f1440_0_SolveDP_ConstantStackPush(EOS, java.lang.Object(ARRAY(i101)), i115, java.lang.Object(ARRAY(i101)))
f1440_0_SolveDP_ConstantStackPush(EOS, java.lang.Object(ARRAY(i101)), i115, java.lang.Object(ARRAY(i101))) → f1450_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i101)), i115, java.lang.Object(ARRAY(i101)), 0)
f1450_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i124)), i115, java.lang.Object(ARRAY(i124)), matching1) → f1460_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i124)), i115, java.lang.Object(ARRAY(i124)), 0) | =(matching1, 0)
f1460_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i124)), i115, java.lang.Object(ARRAY(i124)), matching1) → f1471_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i124)), i115, o155) | &&(<(0, i124), =(matching1, 0))
f1471_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i124)), i115, o155) → f1480_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i124)), i115, o155, i115)
f1480_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(i124)), i115, o155, i115) → f1495_0_SolveDP_ConstantStackPush(EOS, java.lang.Object(ARRAY(i124)), i115, o155, i115, java.lang.Object(ARRAY(8)))
f1495_0_SolveDP_ConstantStackPush(EOS, java.lang.Object(ARRAY(i124)), i115, o155, i115, java.lang.Object(ARRAY(matching1))) → f1509_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i124)), i115, o155, i115, java.lang.Object(ARRAY(8)), 0) | =(matching1, 8)
f1509_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i124)), i115, o155, i115, java.lang.Object(ARRAY(matching1)), matching2) → f1519_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i124)), i115, o155, i115) | &&(&&(<(0, 8), =(matching1, 8)), =(matching2, 0))
f1519_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i124)), i115, java.lang.Object(o166put), i115) → f1541_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i124)), i115, java.lang.Object(o166put), i115)
f1541_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i124)), i115, java.lang.Object(ARRAY(i128)), i115) → f1557_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i124)), i115, java.lang.Object(ARRAY(i128)), i115) | >=(i128, 0)
f1557_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i124)), i115, java.lang.Object(ARRAY(i128)), i115) → f1570_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i124)), i115, java.lang.Object(ARRAY(i128)), i115)
f1570_0_SolveDP_ArrayAccess(EOS, java.lang.Object(ARRAY(i124)), i115, java.lang.Object(ARRAY(i128)), i115) → f1592_0_SolveDP_Inc(EOS, java.lang.Object(ARRAY(i124)), i115) | <(i115, i128)
f1592_0_SolveDP_Inc(EOS, java.lang.Object(ARRAY(i124)), i115) → f1616_0_SolveDP_JMP(EOS, java.lang.Object(ARRAY(i124)), +(i115, 1)) | >(i115, 0)
f1616_0_SolveDP_JMP(EOS, java.lang.Object(ARRAY(i124)), i133) → f1903_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i124)), i133)
f1903_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i124)), i133) → f1384_0_SolveDP_Load(EOS, java.lang.Object(ARRAY(i124)), i133)

Combined rules. Obtained 2 IRules

P rules:
f1390_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(x0)), x1, x1) → f1390_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(x0)), +(x1, 1), +(x1, 1)) | &&(&&(&&(>(+(x1, 1), 0), <=(x1, 12)), >(x0, 0)), <(x1, 2))
f1390_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(x0)), x1, x1) → f1390_0_SolveDP_FieldAccess(EOS, java.lang.Object(ARRAY(x0)), +(x1, 1), +(x1, 1)) | &&(&&(>(+(x1, 1), 2), >(x0, 0)), <=(x1, 12))

Filtered ground terms:

f1390_0_SolveDP_FieldAccess(x1, x2, x3, x4) → f1390_0_SolveDP_FieldAccess(x2, x3, x4)
Cond_f1390_0_SolveDP_FieldAccess(x1, x2, x3, x4, x5) → Cond_f1390_0_SolveDP_FieldAccess(x1, x3, x4, x5)
Cond_f1390_0_SolveDP_FieldAccess1(x1, x2, x3, x4, x5) → Cond_f1390_0_SolveDP_FieldAccess1(x1, x3, x4, x5)

Filtered duplicate terms:

f1390_0_SolveDP_FieldAccess(x1, x2, x3) → f1390_0_SolveDP_FieldAccess(x1, x3)
Cond_f1390_0_SolveDP_FieldAccess(x1, x2, x3, x4) → Cond_f1390_0_SolveDP_FieldAccess(x1, x2, x4)
Cond_f1390_0_SolveDP_FieldAccess1(x1, x2, x3, x4) → Cond_f1390_0_SolveDP_FieldAccess1(x1, x2, x4)

Prepared 2 rules for path length conversion:

P rules:
f1390_0_SolveDP_FieldAccess(java.lang.Object(ARRAY(x0)), x1, x0) → f1390_0_SolveDP_FieldAccess(java.lang.Object(ARRAY(x0)), +(x1, 1), x0) | &&(&&(&&(>(+(x1, 1), 0), <=(x1, 12)), >(x0, 0)), <(x1, 2))
f1390_0_SolveDP_FieldAccess(java.lang.Object(ARRAY(x0)), x1, x0) → f1390_0_SolveDP_FieldAccess(java.lang.Object(ARRAY(x0)), +(x1, 1), x0) | &&(&&(>(+(x1, 1), 2), >(x0, 0)), <=(x1, 12))

Finished conversion. Obtained 2 rules.

P rules:
f1390_0_SolveDP_FieldAccess(v7, x1, x0) → f1390_0_SolveDP_FieldAccess(v8, +(x1, 1), x0) | &&(&&(&&(&&(&&(&&(>(x1, -1), <=(x1, 12)), <(x1, 2)), >(x0, 0)), >(+(v8, 1), 1)), <=(v8, v7)), >(+(v7, 1), 1))
f1390_0_SolveDP_FieldAccess(v9, x3, x2) → f1390_0_SolveDP_FieldAccess(v10, +(x3, 1), x2) | &&(&&(&&(&&(&&(>(x3, 1), <=(x3, 12)), >(x2, 0)), >=(v9, v10)), >(+(v9, 1), 1)), >(+(v10, 1), 1))

(30) Obligation:

Rules:
f1390_0_SolveDP_FieldAccess(v7, x1, x0) → f1390_0_SolveDP_FieldAccess(v8, +(x1, 1), x0) | &&(&&(&&(&&(&&(&&(>(x1, -1), <=(x1, 12)), <(x1, 2)), >(x0, 0)), >(+(v8, 1), 1)), <=(v8, v7)), >(+(v7, 1), 1))
f1390_0_SolveDP_FieldAccess(v9, x3, x2) → f1390_0_SolveDP_FieldAccess(v10, +(x3, 1), x2) | &&(&&(&&(&&(&&(>(x3, 1), <=(x3, 12)), >(x2, 0)), >=(v9, v10)), >(+(v9, 1), 1)), >(+(v10, 1), 1))

(31) TerminationGraphProcessor (SOUND transformation)

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

(32) Complex Obligation (AND)

(33) Obligation:

Rules:
f1390_0_SolveDP_FieldAccess(x0, x1, x2) → f1390_0_SolveDP_FieldAccess(x3, +(x1, 1), x2) | &&(&&(&&(&&(&&(&&(>(x1, -1), <=(x1, 12)), <(x1, 2)), >(x2, 0)), >(+(x3, 1), 1)), <=(x3, x0)), >(+(x0, 1), 1))

(34) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f1390_0_SolveDP_FieldAccess(x5, x7, x9)] = 1 - x7

Therefore the following rule(s) have been dropped:

f1390_0_SolveDP_FieldAccess(x0, x1, x2) → f1390_0_SolveDP_FieldAccess(x3, +(x1, 1), x2) | &&(&&(&&(&&(&&(&&(>(x1, -1), <=(x1, 12)), <(x1, 2)), >(x2, 0)), >(+(x3, 1), 1)), <=(x3, x0)), >(+(x0, 1), 1))

(35) YES

(36) Obligation:

Rules:
f1390_0_SolveDP_FieldAccess(x4, x5, x6) → f1390_0_SolveDP_FieldAccess(x7, +(x5, 1), x6) | &&(&&(&&(&&(&&(>(x5, 1), <=(x5, 12)), >(x6, 0)), >=(x4, x7)), >(+(x4, 1), 1)), >(+(x7, 1), 1))

(37) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f1390_0_SolveDP_FieldAccess(x5, x7, x9)] = 12 - x7

Therefore the following rule(s) have been dropped:

f1390_0_SolveDP_FieldAccess(x0, x1, x2) → f1390_0_SolveDP_FieldAccess(x3, +(x1, 1), x2) | &&(&&(&&(&&(&&(>(x1, 1), <=(x1, 12)), >(x2, 0)), >=(x0, x3)), >(+(x0, 1), 1)), >(+(x3, 1), 1))

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIntTRSProof (SOUND transformation)

(7) Obligation:

(8) PolynomialOrderProcessor (SOUND transformation)

(9) Obligation:

(10) LinearRankingProcessor (EQUIVALENT transformation)

(11) YES

(12) Obligation:

(13) SCCToIntTRSProof (SOUND transformation)

(14) Obligation:

(15) PolynomialOrderProcessor (SOUND transformation)

(16) Obligation:

(17) TerminationGraphProcessor (SOUND transformation)

(18) Obligation:

(19) PolynomialOrderProcessor (EQUIVALENT transformation)

(20) YES

(21) Obligation:

(22) SCCToIntTRSProof (SOUND transformation)

(23) Obligation:

(24) PolynomialOrderProcessor (SOUND transformation)

(25) Obligation:

(26) PolynomialOrderProcessor (EQUIVALENT transformation)

(27) YES

(28) Obligation:

(29) SCCToIntTRSProof (SOUND transformation)

(30) Obligation:

(31) TerminationGraphProcessor (SOUND transformation)

(32) Complex Obligation (AND)

(33) Obligation:

(34) PolynomialOrderProcessor (EQUIVALENT transformation)

(35) YES

(36) Obligation:

(37) PolynomialOrderProcessor (EQUIVALENT transformation)

(38) YES