Termination proof of /tmp/tmp_a1vjD/LinkedList.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBC2FIG (⇐)

↳2 FIGraph

↳3 FIGtoITRSProof (⇐)

↳4 AND

    ↳5 ITRS

        ↳6 ITRStoQTRSProof (⇔)

        ↳7 QTRS

        ↳8 RFCMatchBoundsTRSProof (⇔)

        ↳9 TRUE

    ↳10 ITRS

        ↳11 ITRStoIDPProof (⇔)

        ↳12 IDP

        ↳13 UsableRulesProof (⇔)

        ↳14 IDP

        ↳15 IDPNonInfProof (⇐)

        ↳16 AND

            ↳17 IDP

                ↳18 IDependencyGraphProof (⇔)

                ↳19 TRUE

            ↳20 IDP

                ↳21 IDependencyGraphProof (⇔)

                ↳22 TRUE

    ↳23 ITRS

        ↳24 GroundTermsRemoverProof (⇔)

        ↳25 ITRS

        ↳26 ITRSFilterProcessorProof (⇐)

        ↳27 ITRS

        ↳28 ITRStoIDPProof (⇔)

        ↳29 IDP

        ↳30 UsableRulesProof (⇔)

        ↳31 IDP

        ↳32 ItpfGraphProof (⇔)

        ↳33 IDP

        ↳34 IDPNonInfProof (⇐)

        ↳35 AND

            ↳36 IDP

                ↳37 IDependencyGraphProof (⇔)

                ↳38 TRUE

            ↳39 IDP

                ↳40 IDependencyGraphProof (⇔)

                ↳41 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: LinkedList

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) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 335 nodes with 3 SCCs.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph to ITRS rules

(4) Complex Obligation (AND)

(5) Obligation:

ITRS problem:

The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load5091(java.lang.Object(LinkedList$Node(o2896))) → Load5091(o2896)
The set Q consists of the following terms:
Load5091(java.lang.Object(LinkedList$Node(x0)))

(6) ITRStoQTRSProof (EQUIVALENT transformation)

Represented integers and predefined function symbols by Terms

(7) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

Load5091(java.lang.Object(LinkedList$Node(o2896))) → Load5091(o2896)

The set Q consists of the following terms:

Load5091(java.lang.Object(LinkedList$Node(x0)))

(8) RFCMatchBoundsTRSProof (EQUIVALENT transformation)

Termination of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 1. This implies Q-termination of R.
The following rules were used to construct the certificate:

Load5091(java.lang.Object(LinkedList$Node(o2896))) → Load5091(o2896)

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

18948, 18949

Node 18948 is start node and node 18949 is final node.

Those nodes are connect through the following edges:

18948 to 18949 labelled Load5091_1(0), Load5091_1(1)
18949 to 18949 labelled #_1(0)

(9) TRUE

(10) Obligation:

ITRS problem:

The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load4490(i16, java.lang.Object(LinkedList$Node(o2681))) → Return5054(i16 + 1, o2681)
Load4490(i16, java.lang.Object(LinkedList$Node(o2690))) → JMP5240(i16 + 1, o2690)
JMP5240(i17, o2681) → Load4490(i17, o2681)
Return5054(i17, o2681) → Load4490(i17, o2681)
Load4490(i16, java.lang.Object(LinkedList$Node(o2681))) → Load4490(i16 + 1, o2681)
The set Q consists of the following terms:
Load4490(x0, java.lang.Object(LinkedList$Node(x1)))
JMP5240(x0, x1)
Return5054(x0, x1)

(11) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(12) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

The ITRS R consists of the following rules:
Load4490(i16, java.lang.Object(LinkedList$Node(o2681))) → Return5054(i16 + 1, o2681)
Load4490(i16, java.lang.Object(LinkedList$Node(o2690))) → JMP5240(i16 + 1, o2690)
JMP5240(i17, o2681) → Load4490(i17, o2681)
Return5054(i17, o2681) → Load4490(i17, o2681)
Load4490(i16, java.lang.Object(LinkedList$Node(o2681))) → Load4490(i16 + 1, o2681)

The integer pair graph contains the following rules and edges:
(0): LOAD4490(i16[0], java.lang.Object(LinkedList$Node(o2681[0]))) → RETURN5054(i16[0] + 1, o2681[0])
(1): LOAD4490(i16[1], java.lang.Object(LinkedList$Node(o2690[1]))) → JMP5240'(i16[1] + 1, o2690[1])
(2): JMP5240'(i17[2], o2681[2]) → LOAD4490(i17[2], o2681[2])
(3): RETURN5054(i17[3], o2681[3]) → LOAD4490(i17[3], o2681[3])
(4): LOAD4490(i16[4], java.lang.Object(LinkedList$Node(o2681[4]))) → LOAD4490(i16[4] + 1, o2681[4])

(0) -> (3), if ((o2681[0] →^* o2681[3])∧(i16[0] + 1 →^* i17[3]))

(1) -> (2), if ((i16[1] + 1 →^* i17[2])∧(o2690[1] →^* o2681[2]))

(2) -> (0), if ((o2681[2] →^* java.lang.Object(LinkedList$Node(o2681[0])))∧(i17[2] →^* i16[0]))

(2) -> (1), if ((i17[2] →^* i16[1])∧(o2681[2] →^* java.lang.Object(LinkedList$Node(o2690[1]))))

(2) -> (4), if ((o2681[2] →^* java.lang.Object(LinkedList$Node(o2681[4])))∧(i17[2] →^* i16[4]))

(3) -> (0), if ((o2681[3] →^* java.lang.Object(LinkedList$Node(o2681[0])))∧(i17[3] →^* i16[0]))

(3) -> (1), if ((i17[3] →^* i16[1])∧(o2681[3] →^* java.lang.Object(LinkedList$Node(o2690[1]))))

(3) -> (4), if ((i17[3] →^* i16[4])∧(o2681[3] →^* java.lang.Object(LinkedList$Node(o2681[4]))))

(4) -> (0), if ((o2681[4] →^* java.lang.Object(LinkedList$Node(o2681[0])))∧(i16[4] + 1 →^* i16[0]))

(4) -> (1), if ((i16[4] + 1 →^* i16[1])∧(o2681[4] →^* java.lang.Object(LinkedList$Node(o2690[1]))))

(4) -> (4), if ((o2681[4] →^* java.lang.Object(LinkedList$Node(o2681[4]')))∧(i16[4] + 1 →^* i16[4]'))

The set Q consists of the following terms:
Load4490(x0, java.lang.Object(LinkedList$Node(x1)))
JMP5240(x0, x1)
Return5054(x0, x1)

(13) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(14) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD4490(i16[0], java.lang.Object(LinkedList$Node(o2681[0]))) → RETURN5054(i16[0] + 1, o2681[0])
(1): LOAD4490(i16[1], java.lang.Object(LinkedList$Node(o2690[1]))) → JMP5240'(i16[1] + 1, o2690[1])
(2): JMP5240'(i17[2], o2681[2]) → LOAD4490(i17[2], o2681[2])
(3): RETURN5054(i17[3], o2681[3]) → LOAD4490(i17[3], o2681[3])
(4): LOAD4490(i16[4], java.lang.Object(LinkedList$Node(o2681[4]))) → LOAD4490(i16[4] + 1, o2681[4])