Termination proof of /tmp/tmp3cPHID/LinkedList.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 1720 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIntTRSProof (⇒, 2 ms)

        ↳7 intTRS

        ↳8 PolynomialOrderProcessor (⇔, 7 ms)

        ↳9 YES

    ↳10 JBCTerminationSCC

        ↳11 SCCToIntTRSProof (⇒, 21 ms)

        ↳12 intTRS

        ↳13 PolynomialOrderProcessor (⇔, 8 ms)

        ↳14 YES

    ↳15 JBCTerminationSCC

        ↳16 SCCToIntTRSProof (⇒, 854 ms)

        ↳17 intTRS

        ↳18 PolynomialOrderProcessor (⇔, 0 ms)

        ↳19 YES

(0) Obligation:

JBC Problem based on JBC Program:

public class Entry
{
    private String item;
    private int count;

    public Entry(String itemData, int countData)
    {
        item = itemData;
        count = countData;
    }

    public String toString( )
    {
        return (item + " " + count);
    }

    public boolean equals(Object otherObject)
    {
        if (otherObject == null)
            return false;
        else if (getClass( ) != otherObject.getClass( ))
            return false;
        else
        {
            Entry otherEntry = (Entry)otherObject;
            return (item.equals(otherEntry.item) 
                      && (count == otherEntry.count));
        }
    }

   // <There should be other constructors and methods, including accessor and 
   //                       mutator methods, but we do not use them in this demonstration.>
}



public class LinkedList<T>

{

    private class Node<T>

    {

        private T data;

        private Node<T> link;



        public Node( )

        {

             data = null;

             link = null;

        }



        public Node(T newData, Node<T> linkValue)

        {

            data = newData;

            link = linkValue;

        }

     }//End of Node<T> inner class



    private Node<T> head;



    public LinkedList( )

    {

        head = null;

    }



    /**

     Adds a node at the start of the list with the specified data.

     The added node will be the first node in the list.

    */

    public void addToStart(T itemData)

    {

        this.head = new Node<T>(itemData, this.head);

    }



    /**

     Removes the head node and returns true if the list contains at least

     one node. Returns false if the list is empty.

    */

    public boolean deleteHeadNode( )

    {

        if (head != null)

        {

            head = head.link;

            return true;

        }

        else

            return false;

    }



    /**

     Returns the number of nodes in the list.

    */

    public int size( )

    {

        int count = 0;

        Node<T> position = head;

        while (position != null)

        {

            count++;

            position = position.link;

        }

        return count;

    }



    public boolean contains(T item)

    {

        return (find(item) != null);

    }



    /**

     Finds the first node containing the target item, and returns a

     reference to that node. If target is not in the list, null is returned.

    */

    private Node<T> find(T target)

    {

        Node<T> position = head;

        T itemAtPosition;

        while (position != null)

        {

            itemAtPosition = position.data;

            if (itemAtPosition.equals(target))

                return position;

            position = position.link;

        }

        return null; //target was not found

    }



    /**

     Finds the first node containing the target and returns a reference

      to the data in that node. If target is not in the list, null is returned.

    */

    public T findData(T target)

    {

        return find(target).data;

    }



    public void outputList( )

    {

        Node<T> position = head;

        while (position != null)

        {

            //System.out.println(position.data);

            position = position.link;

        }

    }



    public boolean isEmpty( )

    {

        return (head == null);

    }



    public void clear( )

    {

        head = null;

    }



   /*

    For two lists to be equal they must contain the same data items in

    the same order. The equals method of T is used to compare data items.

   */

   public boolean equals(Object otherObject)

    {

        if (!(otherObject instanceof LinkedList))

            return false;

        else

        {

            LinkedList<T> otherList = (LinkedList<T>)otherObject;

            if (size( ) != otherList.size( ))

                return false;

            Node<T> position = head;

            Node<T> otherPosition = otherList.head;

            while (position != null)

            {

                if (!(position.data.equals(otherPosition.data)))

                    return false;

                position = position.link;

                otherPosition = otherPosition.link;

            }

            return true; //no mismatch was not found

        }

    }



   public static void main(String[] args)

    {

        LinkedList<Entry> list = new LinkedList<Entry>( );



	for (int i = 1; i < args.length; i++) {

	    Entry entry = new Entry(args[i], i++);

	    list.addToStart(entry);

	    entry = new Entry(args[i], i++);

	    list.addToStart(entry);

	    entry = new Entry(args[i], i++);

	    list.addToStart(entry);

	}



	list.size(); // remove it!

        //System.out.println("List has " + list.size( ) 

	//                  + " nodes.");

        list.outputList( );

        //System.out.println("End of list.");

    }

}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
LinkedList.main([Ljava/lang/String;)V: Graph of 316 nodes with 3 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 3 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: LinkedList.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses:

Used field analysis yielded the following read fields:
- LinkedList$Node: [link]
Marker field analysis yielded the following relations that could be markers:

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 20 IRules

P rules:
f3012_0_outputList_NULL(EOS, java.lang.Object(o2480sub), java.lang.Object(o2480sub)) → f3014_0_outputList_NULL(EOS, java.lang.Object(o2480sub), java.lang.Object(o2480sub))
f3014_0_outputList_NULL(EOS, java.lang.Object(o2480sub), java.lang.Object(o2480sub)) → f3017_0_outputList_Load(EOS, java.lang.Object(o2480sub))
f3017_0_outputList_Load(EOS, java.lang.Object(o2480sub)) → f3020_0_outputList_InvokeMethod(EOS, java.lang.Object(o2480sub))
f3020_0_outputList_InvokeMethod(EOS, java.lang.Object(o2480sub)) → f3023_0_access$000_Load(EOS, java.lang.Object(o2480sub), java.lang.Object(o2480sub))
f3023_0_access$000_Load(EOS, java.lang.Object(o2480sub), java.lang.Object(o2480sub)) → f3027_0_access$000_FieldAccess(EOS, java.lang.Object(o2480sub), java.lang.Object(o2480sub))
f3027_0_access$000_FieldAccess(EOS, java.lang.Object(o2480sub), java.lang.Object(o2480sub)) → f3029_0_access$000_FieldAccess(EOS, java.lang.Object(o2480sub), java.lang.Object(o2480sub))
f3027_0_access$000_FieldAccess(EOS, java.lang.Object(o2497sub), java.lang.Object(o2497sub)) → f3030_0_access$000_FieldAccess(EOS, java.lang.Object(o2497sub), java.lang.Object(o2497sub))
f3029_0_access$000_FieldAccess(EOS, java.lang.Object(LinkedList$Node(EOC, o2501)), java.lang.Object(LinkedList$Node(EOC, o2501))) → f3032_0_access$000_FieldAccess(EOS, java.lang.Object(LinkedList$Node(EOC, o2501)), java.lang.Object(LinkedList$Node(EOC, o2501)))
f3032_0_access$000_FieldAccess(EOS, java.lang.Object(LinkedList$Node(EOC, o2501)), java.lang.Object(LinkedList$Node(EOC, o2501))) → f3035_0_access$000_Return(EOS, java.lang.Object(LinkedList$Node(EOC, o2501)), o2501)
f3035_0_access$000_Return(EOS, java.lang.Object(LinkedList$Node(EOC, o2501)), o2501) → f3038_0_outputList_Store(EOS, o2501)
f3038_0_outputList_Store(EOS, o2501) → f3041_0_outputList_JMP(EOS, o2501)
f3041_0_outputList_JMP(EOS, o2501) → f3045_0_outputList_Load(EOS, o2501)
f3045_0_outputList_Load(EOS, o2501) → f3010_0_outputList_Load(EOS, o2501)
f3010_0_outputList_Load(EOS, o2461) → f3012_0_outputList_NULL(EOS, o2461, o2461)
f3030_0_access$000_FieldAccess(EOS, java.lang.Object(LinkedList$Node(EOC, o2505)), java.lang.Object(LinkedList$Node(EOC, o2505))) → f3033_0_access$000_FieldAccess(EOS, java.lang.Object(LinkedList$Node(EOC, o2505)), java.lang.Object(LinkedList$Node(EOC, o2505)))
f3033_0_access$000_FieldAccess(EOS, java.lang.Object(LinkedList$Node(EOC, o2505)), java.lang.Object(LinkedList$Node(EOC, o2505))) → f3036_0_access$000_Return(EOS, java.lang.Object(LinkedList$Node(EOC, o2505)), o2505)
f3036_0_access$000_Return(EOS, java.lang.Object(LinkedList$Node(EOC, o2505)), o2505) → f3039_0_outputList_Store(EOS, o2505)
f3039_0_outputList_Store(EOS, o2505) → f3042_0_outputList_JMP(EOS, o2505)
f3042_0_outputList_JMP(EOS, o2505) → f3046_0_outputList_Load(EOS, o2505)
f3046_0_outputList_Load(EOS, o2505) → f3010_0_outputList_Load(EOS, o2505)

Combined rules. Obtained 1 IRules

P rules:
f3012_0_outputList_NULL(EOS, java.lang.Object(LinkedList$Node(EOC, x0)), java.lang.Object(LinkedList$Node(EOC, x0))) → f3012_0_outputList_NULL(EOS, x0, x0)

Filtered ground terms:

f3012_0_outputList_NULL(x1, x2, x3) → f3012_0_outputList_NULL(x2, x3)
LinkedList$Node(x1, x2) → LinkedList$Node(x2)

Filtered duplicate terms:

f3012_0_outputList_NULL(x1, x2) → f3012_0_outputList_NULL(x2)

Prepared 1 rules for path length conversion:

P rules:
f3012_0_outputList_NULL(java.lang.Object(LinkedList$Node(x0))) → f3012_0_outputList_NULL(x0)

Finished conversion. Obtained 1 rules.

P rules:
f3012_0_outputList_NULL(v2) → f3012_0_outputList_NULL(v3) | &&(&&(>(+(v3, 1), 0), <=(+(v3, 1), v2)), >(+(v2, 1), 1))

(7) Obligation:

Rules:
f3012_0_outputList_NULL(v2) → f3012_0_outputList_NULL(v3) | &&(&&(>(+(v3, 1), 0), <=(+(v3, 1), v2)), >(+(v2, 1), 1))

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f3012_0_outputList_NULL(x3)] = x3

Therefore the following rule(s) have been dropped:

f3012_0_outputList_NULL(x0) → f3012_0_outputList_NULL(x1) | &&(&&(>(+(x1, 1), 0), <=(+(x1, 1), x0)), >(+(x0, 1), 1))

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: LinkedList.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses:

Used field analysis yielded the following read fields:
- LinkedList$Node: [link]
Marker field analysis yielded the following relations that could be markers:

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 21 IRules

P rules:
f2929_0_size_NULL(EOS, java.lang.Object(o2339sub), java.lang.Object(o2339sub)) → f2932_0_size_NULL(EOS, java.lang.Object(o2339sub), java.lang.Object(o2339sub))
f2932_0_size_NULL(EOS, java.lang.Object(o2339sub), java.lang.Object(o2339sub)) → f2936_0_size_Inc(EOS, java.lang.Object(o2339sub))
f2936_0_size_Inc(EOS, java.lang.Object(o2339sub)) → f2939_0_size_Load(EOS, java.lang.Object(o2339sub))
f2939_0_size_Load(EOS, java.lang.Object(o2339sub)) → f2943_0_size_InvokeMethod(EOS, java.lang.Object(o2339sub))
f2943_0_size_InvokeMethod(EOS, java.lang.Object(o2339sub)) → f2947_0_access$000_Load(EOS, java.lang.Object(o2339sub), java.lang.Object(o2339sub))
f2947_0_access$000_Load(EOS, java.lang.Object(o2339sub), java.lang.Object(o2339sub)) → f2954_0_access$000_FieldAccess(EOS, java.lang.Object(o2339sub), java.lang.Object(o2339sub))
f2954_0_access$000_FieldAccess(EOS, java.lang.Object(o2339sub), java.lang.Object(o2339sub)) → f2957_0_access$000_FieldAccess(EOS, java.lang.Object(o2339sub), java.lang.Object(o2339sub))
f2954_0_access$000_FieldAccess(EOS, java.lang.Object(o2353sub), java.lang.Object(o2353sub)) → f2958_0_access$000_FieldAccess(EOS, java.lang.Object(o2353sub), java.lang.Object(o2353sub))
f2957_0_access$000_FieldAccess(EOS, java.lang.Object(LinkedList$Node(EOC, o2361)), java.lang.Object(LinkedList$Node(EOC, o2361))) → f2961_0_access$000_FieldAccess(EOS, java.lang.Object(LinkedList$Node(EOC, o2361)), java.lang.Object(LinkedList$Node(EOC, o2361)))
f2961_0_access$000_FieldAccess(EOS, java.lang.Object(LinkedList$Node(EOC, o2361)), java.lang.Object(LinkedList$Node(EOC, o2361))) → f2966_0_access$000_Return(EOS, java.lang.Object(LinkedList$Node(EOC, o2361)), o2361)
f2966_0_access$000_Return(EOS, java.lang.Object(LinkedList$Node(EOC, o2361)), o2361) → f2971_0_size_Store(EOS, o2361)
f2971_0_size_Store(EOS, o2361) → f2976_0_size_JMP(EOS, o2361)
f2976_0_size_JMP(EOS, o2361) → f2981_0_size_Load(EOS, o2361)
f2981_0_size_Load(EOS, o2361) → f2927_0_size_Load(EOS, o2361)
f2927_0_size_Load(EOS, o2326) → f2929_0_size_NULL(EOS, o2326, o2326)
f2958_0_access$000_FieldAccess(EOS, java.lang.Object(LinkedList$Node(EOC, o2365)), java.lang.Object(LinkedList$Node(EOC, o2365))) → f2962_0_access$000_FieldAccess(EOS, java.lang.Object(LinkedList$Node(EOC, o2365)), java.lang.Object(LinkedList$Node(EOC, o2365)))
f2962_0_access$000_FieldAccess(EOS, java.lang.Object(LinkedList$Node(EOC, o2365)), java.lang.Object(LinkedList$Node(EOC, o2365))) → f2967_0_access$000_Return(EOS, java.lang.Object(LinkedList$Node(EOC, o2365)), o2365)
f2967_0_access$000_Return(EOS, java.lang.Object(LinkedList$Node(EOC, o2365)), o2365) → f2972_0_size_Store(EOS, o2365)
f2972_0_size_Store(EOS, o2365) → f2977_0_size_JMP(EOS, o2365)
f2977_0_size_JMP(EOS, o2365) → f2982_0_size_Load(EOS, o2365)
f2982_0_size_Load(EOS, o2365) → f2927_0_size_Load(EOS, o2365)

Combined rules. Obtained 1 IRules

P rules:
f2929_0_size_NULL(EOS, java.lang.Object(LinkedList$Node(EOC, x0)), java.lang.Object(LinkedList$Node(EOC, x0))) → f2929_0_size_NULL(EOS, x0, x0)

Filtered ground terms:

f2929_0_size_NULL(x1, x2, x3) → f2929_0_size_NULL(x2, x3)
LinkedList$Node(x1, x2) → LinkedList$Node(x2)

Filtered duplicate terms:

f2929_0_size_NULL(x1, x2) → f2929_0_size_NULL(x2)

Prepared 1 rules for path length conversion:

P rules:
f2929_0_size_NULL(java.lang.Object(LinkedList$Node(x0))) → f2929_0_size_NULL(x0)

Finished conversion. Obtained 1 rules.

P rules:
f2929_0_size_NULL(v2) → f2929_0_size_NULL(v3) | &&(&&(>(+(v3, 1), 0), <=(+(v3, 1), v2)), >(+(v2, 1), 1))

(12) Obligation:

Rules:
f2929_0_size_NULL(v2) → f2929_0_size_NULL(v3) | &&(&&(>(+(v3, 1), 0), <=(+(v3, 1), v2)), >(+(v2, 1), 1))

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f2929_0_size_NULL(x3)] = x3

Therefore the following rule(s) have been dropped:

f2929_0_size_NULL(x0) → f2929_0_size_NULL(x1) | &&(&&(>(+(x1, 1), 0), <=(+(x1, 1), x0)), >(+(x0, 1), 1))

(14) YES

(15) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: LinkedList.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses:

Used field analysis yielded the following read fields:
- LinkedList: [head]
Marker field analysis yielded the following relations that could be markers:

(16) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 140 IRules

P rules:
f2588_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i89, i89) → f2589_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i89, i89, java.lang.Object(ARRAY(i16)))
f2589_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i89, i89, java.lang.Object(ARRAY(i16))) → f2590_0_main_GE(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i89, i89, i16) | >=(i16, 0)
f2590_0_main_GE(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i89, i89, i16) → f2592_0_main_GE(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i89, i89, i16)
f2592_0_main_GE(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i89, i89, i16) → f2594_0_main_New(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i89) | <(i89, i16)
f2594_0_main_New(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i89) → f2596_0_main_Duplicate(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i89)
f2596_0_main_Duplicate(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i89) → f2598_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i89)
f2598_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i89) → f2599_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i89, java.lang.Object(ARRAY(i16)))
f2599_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i89, java.lang.Object(ARRAY(i16))) → f2601_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i89, java.lang.Object(ARRAY(i16)), i89)
f2601_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i89, java.lang.Object(ARRAY(i16)), i89) → f2603_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i89, java.lang.Object(ARRAY(i16)), i89)
f2603_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i89, java.lang.Object(ARRAY(i16)), i89) → f2606_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i89) | <(i89, i16)
f2606_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i89) → f2609_0_main_Inc(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i89, i89)
f2609_0_main_Inc(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i89, i89) → f2611_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), +(i89, 1), i89) | >(i89, 0)
f2611_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, i89) → f2615_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, i89, i89)
f2615_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, i89, i89) → f2626_0__init__InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, i89, i89)
f2626_0__init__InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, i89, i89) → f2630_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, i89, i89)
f2630_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, i89, i89) → f2634_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, i89, i89)
f2634_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, i89, i89) → f2637_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, i89, i89)
f2637_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, i89, i89) → f2640_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, i89, i89)
f2640_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, i89, i89) → f2644_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, i89, i89)
f2644_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, i89, i89) → f2647_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, i89, i89)
f2647_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, i89, i89) → f2654_0__init__Return(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, i89)
f2654_0__init__Return(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, i89) → f2658_0_main_Store(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2658_0_main_Store(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2661_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2661_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2665_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2665_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2668_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2668_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2672_0_addToStart_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2672_0_addToStart_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2679_0_addToStart_New(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2679_0_addToStart_New(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2683_0_addToStart_Duplicate(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2683_0_addToStart_Duplicate(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2687_0_addToStart_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2687_0_addToStart_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2690_0_addToStart_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2690_0_addToStart_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2694_0_addToStart_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2694_0_addToStart_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2698_0_addToStart_FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2698_0_addToStart_FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2703_0_addToStart_InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2703_0_addToStart_InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2708_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2708_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2728_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2728_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2750_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2750_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2757_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2757_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2762_0__init__InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2762_0__init__InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2767_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2767_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2773_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2773_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2778_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2778_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2785_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2785_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2788_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2788_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2794_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2794_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2804_0__init__Return(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2804_0__init__Return(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2816_0_addToStart_FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2816_0_addToStart_FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2835_0_addToStart_Return(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2835_0_addToStart_Return(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2845_0_main_New(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2845_0_main_New(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2855_0_main_Duplicate(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2855_0_main_Duplicate(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2874_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91)
f2874_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2879_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, java.lang.Object(ARRAY(i16)))
f2879_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, java.lang.Object(ARRAY(i16))) → f2882_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, java.lang.Object(ARRAY(i16)), i91)
f2882_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, java.lang.Object(ARRAY(i16)), i91) → f2885_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, java.lang.Object(ARRAY(i16)), i91)
f2885_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, java.lang.Object(ARRAY(i16)), i91) → f2889_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) | <(i91, i16)
f2889_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91) → f2893_0_main_Inc(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, i91)
f2893_0_main_Inc(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i91, i91) → f2896_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), +(i91, 1), i91) | >(i91, 0)
f2896_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, i91) → f2899_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, i91, i91)
f2899_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, i91, i91) → f2905_0__init__InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, i91, i91)
f2905_0__init__InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, i91, i91) → f2910_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, i91, i91)
f2910_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, i91, i91) → f2915_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, i91, i91)
f2915_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, i91, i91) → f2919_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, i91, i91)
f2919_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, i91, i91) → f2924_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, i91, i91)
f2924_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, i91, i91) → f2928_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, i91, i91)
f2928_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, i91, i91) → f2930_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, i91, i91)
f2930_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, i91, i91) → f2934_0__init__Return(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, i91)
f2934_0__init__Return(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, i91) → f2938_0_main_Store(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f2938_0_main_Store(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f2941_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f2941_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f2945_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f2945_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f2949_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f2949_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f2952_0_addToStart_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f2952_0_addToStart_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f2959_0_addToStart_New(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f2959_0_addToStart_New(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f2964_0_addToStart_Duplicate(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f2964_0_addToStart_Duplicate(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f2969_0_addToStart_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f2969_0_addToStart_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f2974_0_addToStart_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f2974_0_addToStart_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f2979_0_addToStart_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f2979_0_addToStart_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f2985_0_addToStart_FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f2985_0_addToStart_FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f2989_0_addToStart_InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f2989_0_addToStart_InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f2993_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f2993_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f2998_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f2998_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f3000_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f3000_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f3002_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f3002_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f3004_0__init__InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f3004_0__init__InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f3006_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f3006_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f3008_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f3008_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f3011_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f3011_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f3013_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f3013_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f3016_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f3016_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f3019_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f3019_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f3022_0__init__Return(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f3022_0__init__Return(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f3025_0_addToStart_FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f3025_0_addToStart_FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f3026_0_addToStart_Return(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f3026_0_addToStart_Return(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f3028_0_main_New(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f3028_0_main_New(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f3031_0_main_Duplicate(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f3031_0_main_Duplicate(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f3034_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103)
f3034_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f3037_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, java.lang.Object(ARRAY(i16)))
f3037_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, java.lang.Object(ARRAY(i16))) → f3040_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, java.lang.Object(ARRAY(i16)), i103)
f3040_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, java.lang.Object(ARRAY(i16)), i103) → f3043_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, java.lang.Object(ARRAY(i16)), i103)
f3043_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, java.lang.Object(ARRAY(i16)), i103) → f3047_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) | <(i103, i16)
f3047_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103) → f3049_0_main_Inc(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, i103)
f3049_0_main_Inc(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i103, i103) → f3050_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), +(i103, 1), i103) | >(i103, 0)
f3050_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109, i103) → f3052_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109, i103, i103)
f3052_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109, i103, i103) → f3056_0__init__InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109, i103, i103)
f3056_0__init__InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109, i103, i103) → f3063_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109, i103, i103)
f3063_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109, i103, i103) → f3069_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109, i103, i103)
f3069_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109, i103, i103) → f3072_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109, i103, i103)
f3072_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109, i103, i103) → f3074_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109, i103, i103)
f3074_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109, i103, i103) → f3076_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109, i103, i103)
f3076_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109, i103, i103) → f3078_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109, i103, i103)
f3078_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109, i103, i103) → f3086_0__init__Return(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109, i103)
f3086_0__init__Return(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109, i103) → f3090_0_main_Store(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3090_0_main_Store(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3091_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3091_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3093_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3093_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3098_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3098_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3103_0_addToStart_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3103_0_addToStart_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3106_0_addToStart_New(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3106_0_addToStart_New(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3108_0_addToStart_Duplicate(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3108_0_addToStart_Duplicate(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3110_0_addToStart_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3110_0_addToStart_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3112_0_addToStart_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3112_0_addToStart_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3114_0_addToStart_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3114_0_addToStart_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3116_0_addToStart_FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3116_0_addToStart_FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3118_0_addToStart_InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3118_0_addToStart_InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3120_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3120_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3123_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3123_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3124_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3124_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3125_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3125_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3126_0__init__InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3126_0__init__InvokeMethod(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3127_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3127_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3128_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3128_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3129_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3129_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3133_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3133_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3136_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3136_0__init__Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3140_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3140_0__init__FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3148_0__init__Return(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3148_0__init__Return(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3153_0_addToStart_FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3153_0_addToStart_FieldAccess(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3184_0_addToStart_Return(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3184_0_addToStart_Return(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3186_0_main_Inc(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109)
f3186_0_main_Inc(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i109) → f3188_0_main_JMP(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), +(i109, 1)) | >(i109, 0)
f3188_0_main_JMP(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i111) → f3202_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i111)
f3202_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i111) → f2579_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i111)
f2579_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i89) → f2588_0_main_Load(EOS, java.lang.Object(ARRAY(i16)), java.lang.Object(ARRAY(i16)), i89, i89)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:

f2588_0_main_Load(x1, x2, x3, x4, x5) → f2588_0_main_Load(x2, x3, x4, x5)
Cond_f2588_0_main_Load(x1, x2, x3, x4, x5, x6) → Cond_f2588_0_main_Load(x1, x3, x4, x5, x6)

Filtered duplicate terms:

f2588_0_main_Load(x1, x2, x3, x4) → f2588_0_main_Load(x2, x4)
Cond_f2588_0_main_Load(x1, x2, x3, x4, x5) → Cond_f2588_0_main_Load(x1, x3, x5)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

P rules:
f2588_0_main_Load(v5, x1, x0) → f2588_0_main_Load(v6, +(x1, 4), x0) | &&(&&(&&(&&(&&(&&(>(x1, 0), <(+(x1, 2), x0)), <(+(x1, 1), x0)), >(x0, -1)), >(+(v6, 1), 1)), <=(v6, v5)), >(+(v5, 1), 1))

(17) Obligation:

Rules:
f2588_0_main_Load(v5, x1, x0) → f2588_0_main_Load(v6, +(x1, 4), x0) | &&(&&(&&(&&(&&(&&(>(x1, 0), <(+(x1, 2), x0)), <(+(x1, 1), x0)), >(x0, -1)), >(+(v6, 1), 1)), <=(v6, v5)), >(+(v5, 1), 1))

(18) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f2588_0_main_Load(x5, x7, x9)] = -x7 + x9

Therefore the following rule(s) have been dropped:

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

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIntTRSProof (SOUND transformation)

(7) Obligation:

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

(9) YES

(10) Obligation:

(11) SCCToIntTRSProof (SOUND transformation)

(12) Obligation:

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

(14) YES

(15) Obligation:

(16) SCCToIntTRSProof (SOUND transformation)

(17) Obligation:

(18) PolynomialOrderProcessor (EQUIVALENT transformation)

(19) YES