Termination proof of /tmp/tmpZguCrr/Flatten.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBC2FIG (⇐)

↳2 FIGraph

↳3 FIGtoITRSProof (⇐)

↳4 AND

    ↳5 ITRS

        ↳6 DuplicateArgsRemoverProof (⇔)

        ↳7 ITRS

        ↳8 ITRStoIDPProof (⇔)

        ↳9 IDP

        ↳10 UsableRulesProof (⇔)

        ↳11 IDP

        ↳12 IDPNonInfProof (⇐)

        ↳13 AND

            ↳14 IDP

                ↳15 IDPNonInfProof (⇐)

                ↳16 IDP

                ↳17 IDependencyGraphProof (⇔)

                ↳18 TRUE

            ↳19 IDP

                ↳20 IDependencyGraphProof (⇔)

                ↳21 TRUE

    ↳22 ITRS

        ↳23 GroundTermsRemoverProof (⇔)

        ↳24 ITRS

        ↳25 DuplicateArgsRemoverProof (⇔)

        ↳26 ITRS

        ↳27 ITRSFilterProcessorProof (⇐)

        ↳28 ITRS

        ↳29 ITRSFSMergerProof (⇐)

        ↳30 ITRS

        ↳31 ITRStoIDPProof (⇔)

        ↳32 IDP

        ↳33 UsableRulesProof (⇔)

        ↳34 IDP

        ↳35 ItpfGraphProof (⇔)

        ↳36 IDP

        ↳37 IDPNonInfProof (⇐)

        ↳38 AND

            ↳39 IDP

                ↳40 IDependencyGraphProof (⇔)

                ↳41 TRUE

            ↳42 IDP

                ↳43 IDependencyGraphProof (⇔)

                ↳44 IDP

                ↳45 IDPNonInfProof (⇐)

                ↳46 AND

                    ↳47 IDP

                        ↳48 IDependencyGraphProof (⇔)

                        ↳49 TRUE

                    ↳50 IDP

                        ↳51 IDependencyGraphProof (⇔)

                        ↳52 TRUE

(0) Obligation:

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

public class Flatten {
  public static IntList flatten(TreeList list) {
    TreeList cur = list;
    IntList result = null;
    while (cur != null) {
      Tree tree = cur.value;
      if (tree != null) {
        IntList oldIntList = result;
        result = new IntList();
        result.value = tree.value;
        result.next = oldIntList;
        TreeList oldCur = cur;
        cur = new TreeList();
        cur.value = tree.left;
        cur.next = oldCur;
        oldCur.value = tree.right;
      } else cur = cur.next;
    }
    if (cur != list) {}
    return result;
  }
  public static void main(String[] args) {
    Random.args = args;
    int listLength = Random.random();
    TreeList list = null;
    for (int i = listLength; i > 0; i--) {
      Tree tree = Tree.createTree();
      list = new TreeList(tree, list);
    }

    flatten(list);
  }

}


public class IntList {
  int value;
  IntList next;

  public IntList(int value, IntList next) {
    this.value = value;
    this.next = next;
  }

  public IntList() {
  }

  public static IntList createList() {
    IntList result = null;
    int length = Random.random();
    while (length > 0) {
      result = new IntList(Random.random(), result);
      length--;
    }
    return result;
  }
}


public class Random {
  static String[] args;
  static int index = 0;

  public static int random() {
    String string = args[index];
    index++;
    return string.length();
  }
}


public class Tree {
  Tree left;
  Tree right;
  int value;

  public Tree(Tree l, Tree r) {
    this.left = l;
    this.right = r;
  }

  public Tree() {
  }

  public static Tree createNode() {
    Tree result = new Tree();
    result.value = Random.random();
    return result;
  }

  public static Tree createTree() {
    int counter = Random.random();
    if (counter == 0) {
      return null;
    }
    Tree result = createNode();
    Tree t = result;

    while (counter > 0) {
      int branch = Random.random();
      if (branch > 0) {
        if (t.left == null) {
          t.left = createNode();
          t = result;
        } else {
          t = t.left;
        }
      } else {
        if (t.right == null) {
          t.right = createNode();
          t = result;
        } else {
          t = t.right;
        }
      }
      counter--;
    }

    return result;
  }
  public static void main(String[] args) {
    Random.args = args;
    createTree();
  }
}


public class TreeList {
  Tree value;
  TreeList next;

  public TreeList(Tree value, TreeList next) {
    this.value = value;
    this.next = next;
  }

  public TreeList() {
  }
}

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 882 nodes with 2 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:
Load10574(o18579, o18579, java.lang.Object(TreeList(java.lang.Object(Tree(i3261, o22248, o22249)), o19096))) → JMP11347(o18579new, o18579new, java.lang.Object(TreeList(o22248, java.lang.Object(TreeList(o22249, o19096)))))
Load10574(java.lang.Object(TreeList(java.lang.Object(Tree(i3262, o22264, o22265)), o19117)), java.lang.Object(TreeList(java.lang.Object(Tree(i3262, o22264, o22265)), o19117)), java.lang.Object(TreeList(java.lang.Object(Tree(i3262, o22264, o22265)), o19117))) → JMP11347(java.lang.Object(TreeList(o22265, o19117)), java.lang.Object(TreeList(o22265, o19117)), java.lang.Object(TreeList(o22264, java.lang.Object(TreeList(o22265, o19117)))))
Load10574(java.lang.Object(TreeList(NULL, o19117)), java.lang.Object(TreeList(NULL, o19117)), java.lang.Object(TreeList(NULL, o19117))) → JMP11347(java.lang.Object(TreeList(NULL, o19117)), java.lang.Object(TreeList(NULL, o19117)), o19117)
JMP11347(o18579, o18579, o19096) → Load10574(o18579, o18579, o19096)
Load10574(o18579, o18579, java.lang.Object(TreeList(NULL, o19096))) → Load10574(o18579, o18579, o19096)
The set Q consists of the following terms:
Load10574(x0, x0, java.lang.Object(TreeList(java.lang.Object(Tree(x1, x2, x3)), x4)))
JMP11347(x0, x0, x1)
Load10574(x0, x0, java.lang.Object(TreeList(NULL, x1)))

(6) DuplicateArgsRemoverProof (EQUIVALENT transformation)

Some arguments are removed because they only appear as duplicates.
We removed arguments according to the following replacements:

Load10574(x1, x2, x3) → Load10574(x2, x3)
JMP11347(x1, x2, x3) → JMP11347(x2, x3)

(7) 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:
Load10574(o18579, java.lang.Object(TreeList(java.lang.Object(Tree(i3261, o22248, o22249)), o19096))) → JMP11347(o18579new, java.lang.Object(TreeList(o22248, java.lang.Object(TreeList(o22249, o19096)))))
Load10574(java.lang.Object(TreeList(java.lang.Object(Tree(i3262, o22264, o22265)), o19117)), java.lang.Object(TreeList(java.lang.Object(Tree(i3262, o22264, o22265)), o19117))) → JMP11347(java.lang.Object(TreeList(o22265, o19117)), java.lang.Object(TreeList(o22264, java.lang.Object(TreeList(o22265, o19117)))))
Load10574(java.lang.Object(TreeList(NULL, o19117)), java.lang.Object(TreeList(NULL, o19117))) → JMP11347(java.lang.Object(TreeList(NULL, o19117)), o19117)
JMP11347(o18579, o19096) → Load10574(o18579, o19096)
Load10574(o18579, java.lang.Object(TreeList(NULL, o19096))) → Load10574(o18579, o19096)
The set Q consists of the following terms:
Load10574(x0, java.lang.Object(TreeList(java.lang.Object(Tree(x1, x2, x3)), x4)))
JMP11347(x0, x1)
Load10574(x0, java.lang.Object(TreeList(NULL, x1)))

(8) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(9) 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:
none

The ITRS R consists of the following rules:
Load10574(o18579, java.lang.Object(TreeList(java.lang.Object(Tree(i3261, o22248, o22249)), o19096))) → JMP11347(o18579new, java.lang.Object(TreeList(o22248, java.lang.Object(TreeList(o22249, o19096)))))
Load10574(java.lang.Object(TreeList(java.lang.Object(Tree(i3262, o22264, o22265)), o19117)), java.lang.Object(TreeList(java.lang.Object(Tree(i3262, o22264, o22265)), o19117))) → JMP11347(java.lang.Object(TreeList(o22265, o19117)), java.lang.Object(TreeList(o22264, java.lang.Object(TreeList(o22265, o19117)))))
Load10574(java.lang.Object(TreeList(NULL, o19117)), java.lang.Object(TreeList(NULL, o19117))) → JMP11347(java.lang.Object(TreeList(NULL, o19117)), o19117)
JMP11347(o18579, o19096) → Load10574(o18579, o19096)
Load10574(o18579, java.lang.Object(TreeList(NULL, o19096))) → Load10574(o18579, o19096)

The integer pair graph contains the following rules and edges:
(0): LOAD10574(o18579[0], java.lang.Object(TreeList(java.lang.Object(Tree(i3261[0], o22248[0], o22249[0])), o19096[0]))) → JMP11347'(o18579new[0], java.lang.Object(TreeList(o22248[0], java.lang.Object(TreeList(o22249[0], o19096[0])))))
(1): LOAD10574(java.lang.Object(TreeList(java.lang.Object(Tree(i3262[1], o22264[1], o22265[1])), o19117[1])), java.lang.Object(TreeList(java.lang.Object(Tree(i3262[1], o22264[1], o22265[1])), o19117[1]))) → JMP11347'(java.lang.Object(TreeList(o22265[1], o19117[1])), java.lang.Object(TreeList(o22264[1], java.lang.Object(TreeList(o22265[1], o19117[1])))))
(2): LOAD10574(java.lang.Object(TreeList(NULL, o19117[2])), java.lang.Object(TreeList(NULL, o19117[2]))) → JMP11347'(java.lang.Object(TreeList(NULL, o19117[2])), o19117[2])
(3): JMP11347'(o18579[3], o19096[3]) → LOAD10574(o18579[3], o19096[3])
(4): LOAD10574(o18579[4], java.lang.Object(TreeList(NULL, o19096[4]))) → LOAD10574(o18579[4], o19096[4])

(0) -> (3), if ((o18579new[0] →^* o18579[3])∧(java.lang.Object(TreeList(o22248[0], java.lang.Object(TreeList(o22249[0], o19096[0])))) →^* o19096[3]))

(1) -> (3), if ((java.lang.Object(TreeList(o22265[1], o19117[1])) →^* o18579[3])∧(java.lang.Object(TreeList(o22264[1], java.lang.Object(TreeList(o22265[1], o19117[1])))) →^* o19096[3]))

(2) -> (3), if ((o19117[2] →^* o19096[3])∧(java.lang.Object(TreeList(NULL, o19117[2])) →^* o18579[3]))

(3) -> (0), if ((o18579[3] →^* o18579[0])∧(o19096[3] →^* java.lang.Object(TreeList(java.lang.Object(Tree(i3261[0], o22248[0], o22249[0])), o19096[0]))))

(3) -> (1), if ((o19096[3] →^* java.lang.Object(TreeList(java.lang.Object(Tree(i3262[1], o22264[1], o22265[1])), o19117[1])))∧(o18579[3] →^* java.lang.Object(TreeList(java.lang.Object(Tree(i3262[1], o22264[1], o22265[1])), o19117[1]))))

(3) -> (2), if ((o18579[3] →^* java.lang.Object(TreeList(NULL, o19117[2])))∧(o19096[3] →^* java.lang.Object(TreeList(NULL, o19117[2]))))

(3) -> (4), if ((o19096[3] →^* java.lang.Object(TreeList(NULL, o19096[4])))∧(o18579[3] →^* o18579[4]))

(4) -> (0), if ((o18579[4] →^* o18579[0])∧(o19096[4] →^* java.lang.Object(TreeList(java.lang.Object(Tree(i3261[0], o22248[0], o22249[0])), o19096[0]))))

(4) -> (1), if ((o19096[4] →^* java.lang.Object(TreeList(java.lang.Object(Tree(i3262[1], o22264[1], o22265[1])), o19117[1])))∧(o18579[4] →^* java.lang.Object(TreeList(java.lang.Object(Tree(i3262[1], o22264[1], o22265[1])), o19117[1]))))

(4) -> (2), if ((o18579[4] →^* java.lang.Object(TreeList(NULL, o19117[2])))∧(o19096[4] →^* java.lang.Object(TreeList(NULL, o19117[2]))))

(4) -> (4), if ((o18579[4] →^* o18579[4]')∧(o19096[4] →^* java.lang.Object(TreeList(NULL, o19096[4]'))))

The set Q consists of the following terms:
Load10574(x0, java.lang.Object(TreeList(java.lang.Object(Tree(x1, x2, x3)), x4)))
JMP11347(x0, x1)
Load10574(x0, java.lang.Object(TreeList(NULL, x1)))

(10) 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.

(11) 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:
none

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD10574(o18579[0], java.lang.Object(TreeList(java.lang.Object(Tree(i3261[0], o22248[0], o22249[0])), o19096[0]))) → JMP11347'(o18579new[0], java.lang.Object(TreeList(o22248[0], java.lang.Object(TreeList(o22249[0], o19096[0])))))
(1): LOAD10574(java.lang.Object(TreeList(java.lang.Object(Tree(i3262[1], o22264[1], o22265[1])), o19117[1])), java.lang.Object(TreeList(java.lang.Object(Tree(i3262[1], o22264[1], o22265[1])), o19117[1]))) → JMP11347'(java.lang.Object(TreeList(o22265[1], o19117[1])), java.lang.Object(TreeList(o22264[1], java.lang.Object(TreeList(o22265[1], o19117[1])))))
(2): LOAD10574(java.lang.Object(TreeList(NULL, o19117[2])), java.lang.Object(TreeList(NULL, o19117[2]))) → JMP11347'(java.lang.Object(TreeList(NULL, o19117[2])), o19117[2])
(3): JMP11347'(o18579[3], o19096[3]) → LOAD10574(o18579[3], o19096[3])
(4): LOAD10574(o18579[4], java.lang.Object(TreeList(NULL, o19096[4]))) → LOAD10574(o18579[4], o19096[4])