Termination proof of /tmp/tmpA9Nno1/CyclicAnalysisRec.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 560 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 210 ms)

        ↳7 IDP

        ↳8 IDPtoQDPProof (⇒, 0 ms)

        ↳9 QDP

        ↳10 UsableRulesProof (⇔, 0 ms)

        ↳11 QDP

        ↳12 QReductionProof (⇔, 0 ms)

        ↳13 QDP

        ↳14 QDPSizeChangeProof (⇔, 0 ms)

        ↳15 YES

    ↳16 JBCTerminationSCC

        ↳17 SCCToIDPv1Proof (⇒, 90 ms)

        ↳18 IDP

        ↳19 IDPNonInfProof (⇒, 90 ms)

        ↳20 AND

            ↳21 IDP

                ↳22 IDependencyGraphProof (⇔, 0 ms)

                ↳23 TRUE

            ↳24 IDP

                ↳25 IDependencyGraphProof (⇔, 0 ms)

                ↳26 TRUE

(0) Obligation:

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

package CyclicAnalysisRec;

public class CyclicAnalysisRec {
	CyclicAnalysisRec field;

	public static void main(String[] args) {
		Random.args = args;
		CyclicAnalysisRec t = new CyclicAnalysisRec();
		t.field = new CyclicAnalysisRec();
		t.field.appendNewCyclicList(Random.random());
		t.appendNewList(Random.random());
		t.length();
	}

	public int length() {
		if (this.field == null) return 1;
		else return 1 + this.field.length();
	}

	public void appendNewCyclicList(int i) {
		CyclicAnalysisRec last = this.appendNewList(i);
		last.field = this;
	}

	/**
 	 * @param i number of elements to append
 	 * @return the last list element appended
 	 */
	private CyclicAnalysisRec appendNewList(int i) {
		this.field = new CyclicAnalysisRec();
		if (i <= 1) {
			return this.field;
		} else {
			return this.field.appendNewList(i-1);
		}
	}
}


package CyclicAnalysisRec;

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

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

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
CyclicAnalysisRec.CyclicAnalysisRec.main([Ljava/lang/String;)V: Graph of 318 nodes with 0 SCCs.

CyclicAnalysisRec.CyclicAnalysisRec.appendNewList(I)LCyclicAnalysisRec/CyclicAnalysisRec;: Graph of 33 nodes with 0 SCCs.

CyclicAnalysisRec.CyclicAnalysisRec.length()I: Graph of 28 nodes with 0 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 2 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: CyclicAnalysisRec.CyclicAnalysisRec.length()I
SCC calls the following helper methods: CyclicAnalysisRec.CyclicAnalysisRec.length()I
Performed SCC analyses: UsedFieldsAnalysis

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 11 rules for P and 15 rules for R.

P rules:
1340_0_length_FieldAccess(EOS(STATIC_1340), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o825)), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o825))) → 1342_0_length_FieldAccess(EOS(STATIC_1342), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o825)), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o825)))
1342_0_length_FieldAccess(EOS(STATIC_1342), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o825)), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o825))) → 1344_0_length_NONNULL(EOS(STATIC_1344), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o825)), o825)
1344_0_length_NONNULL(EOS(STATIC_1344), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o827sub))), java.lang.Object(o827sub)) → 1345_0_length_NONNULL(EOS(STATIC_1345), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o827sub))), java.lang.Object(o827sub))
1345_0_length_NONNULL(EOS(STATIC_1345), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o827sub))), java.lang.Object(o827sub)) → 1348_0_length_ConstantStackPush(EOS(STATIC_1348), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o827sub))))
1348_0_length_ConstantStackPush(EOS(STATIC_1348), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o827sub)))) → 1351_0_length_Load(EOS(STATIC_1351), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o827sub))))
1351_0_length_Load(EOS(STATIC_1351), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o827sub)))) → 1354_0_length_FieldAccess(EOS(STATIC_1354), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o827sub))))
1354_0_length_FieldAccess(EOS(STATIC_1354), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o827sub)))) → 1357_0_length_InvokeMethod(EOS(STATIC_1357), java.lang.Object(o827sub))
1357_0_length_InvokeMethod(EOS(STATIC_1357), java.lang.Object(o827sub)) → 1362_1_length_InvokeMethod(1362_0_length_Load(EOS(STATIC_1362), java.lang.Object(o827sub)), java.lang.Object(o827sub))
1362_0_length_Load(EOS(STATIC_1362), java.lang.Object(o827sub)) → 1366_0_length_Load(EOS(STATIC_1366), java.lang.Object(o827sub))
1366_0_length_Load(EOS(STATIC_1366), java.lang.Object(o827sub)) → 1338_0_length_Load(EOS(STATIC_1338), java.lang.Object(o827sub))
1338_0_length_Load(EOS(STATIC_1338), java.lang.Object(o820sub)) → 1340_0_length_FieldAccess(EOS(STATIC_1340), java.lang.Object(o820sub), java.lang.Object(o820sub))
R rules:
1344_0_length_NONNULL(EOS(STATIC_1344), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL)), NULL) → 1346_0_length_NONNULL(EOS(STATIC_1346), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL)), NULL)
1346_0_length_NONNULL(EOS(STATIC_1346), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL)), NULL) → 1349_0_length_ConstantStackPush(EOS(STATIC_1349), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL)))
1349_0_length_ConstantStackPush(EOS(STATIC_1349), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL))) → 1353_0_length_Return(EOS(STATIC_1353), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL)))
1362_1_length_InvokeMethod(1353_0_length_Return(EOS(STATIC_1353), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL))), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL))) → 1373_0_length_Return(EOS(STATIC_1373), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL)), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL)))
1362_1_length_InvokeMethod(1376_0_length_Return(EOS(STATIC_1376)), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL))))) → 1393_0_length_Return(EOS(STATIC_1393), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL)))))
1362_1_length_InvokeMethod(1538_0_length_Return(EOS(STATIC_1538)), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o1082))))))) → 1555_0_length_Return(EOS(STATIC_1555), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o1082)))))))
1373_0_length_Return(EOS(STATIC_1373), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL)), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL))) → 1374_0_length_IntArithmetic(EOS(STATIC_1374))
1374_0_length_IntArithmetic(EOS(STATIC_1374)) → 1376_0_length_Return(EOS(STATIC_1376))
1393_0_length_Return(EOS(STATIC_1393), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL))))) → 1428_0_length_Return(EOS(STATIC_1428), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL)))))
1428_0_length_Return(EOS(STATIC_1428), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o868))))) → 1466_0_length_Return(EOS(STATIC_1466), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o868)))))
1466_0_length_Return(EOS(STATIC_1466), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o917))))) → 1507_0_length_Return(EOS(STATIC_1507), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o917)))))
1507_0_length_Return(EOS(STATIC_1507), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o978))))) → 1532_0_length_Return(EOS(STATIC_1532), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o978)))))
1532_0_length_Return(EOS(STATIC_1532), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o1038))))) → 1535_0_length_IntArithmetic(EOS(STATIC_1535))
1535_0_length_IntArithmetic(EOS(STATIC_1535)) → 1538_0_length_Return(EOS(STATIC_1538))
1555_0_length_Return(EOS(STATIC_1555), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o1082))))))) → 1532_0_length_Return(EOS(STATIC_1532), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o1082)))))))

Combined rules. Obtained 1 conditional rules for P and 3 conditional rules for R.

P rules:
1340_0_length_FieldAccess(EOS(STATIC_1340), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(x0))), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(x0)))) → 1362_1_length_InvokeMethod(1340_0_length_FieldAccess(EOS(STATIC_1340), java.lang.Object(x0), java.lang.Object(x0)), java.lang.Object(x0))
R rules:
1362_1_length_InvokeMethod(1353_0_length_Return(EOS(STATIC_1353), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL))), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL))) → 1376_0_length_Return(EOS(STATIC_1376))
1362_1_length_InvokeMethod(1538_0_length_Return(EOS(STATIC_1538)), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, x0))))))) → 1538_0_length_Return(EOS(STATIC_1538))
1362_1_length_InvokeMethod(1376_0_length_Return(EOS(STATIC_1376)), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL))))) → 1538_0_length_Return(EOS(STATIC_1538))

Filtered ground terms:

1340_0_length_FieldAccess(x1, x2, x3) → 1340_0_length_FieldAccess(x2, x3)
CyclicAnalysisRec.CyclicAnalysisRec(x1, x2) → CyclicAnalysisRec.CyclicAnalysisRec(x2)
1538_0_length_Return(x1) → 1538_0_length_Return
1376_0_length_Return(x1) → 1376_0_length_Return
1353_0_length_Return(x1, x2) → 1353_0_length_Return

Filtered duplicate args:

1340_0_length_FieldAccess(x1, x2) → 1340_0_length_FieldAccess(x2)

Combined rules. Obtained 1 conditional rules for P and 3 conditional rules for R.

P rules:
1340_0_length_FieldAccess(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(x0)))) → 1362_1_length_InvokeMethod(1340_0_length_FieldAccess(java.lang.Object(x0)), java.lang.Object(x0))
R rules:
1362_1_length_InvokeMethod(1353_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL))) → 1376_0_length_Return
1362_1_length_InvokeMethod(1538_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(x0))))))) → 1538_0_length_Return
1362_1_length_InvokeMethod(1376_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL))))) → 1538_0_length_Return

Performed bisimulation on rules. Used the following equivalence classes: {[1353_0_length_Return, 1376_0_length_Return, 1538_0_length_Return]=1353_0_length_Return}

Finished conversion. Obtained 1 rules for P and 3 rules for R. System has no predefined symbols.

P rules:
1340_0_LENGTH_FIELDACCESS(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(x0)))) → 1340_0_LENGTH_FIELDACCESS(java.lang.Object(x0))
R rules:
1362_1_length_InvokeMethod(1353_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL))) → 1353_0_length_Return
1362_1_length_InvokeMethod(1353_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(x0))))))) → 1353_0_length_Return
1362_1_length_InvokeMethod(1353_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL))))) → 1353_0_length_Return

(7) 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:
1362_1_length_InvokeMethod(1353_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL))) → 1353_0_length_Return
1362_1_length_InvokeMethod(1353_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(x0))))))) → 1353_0_length_Return
1362_1_length_InvokeMethod(1353_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL))))) → 1353_0_length_Return

The integer pair graph contains the following rules and edges:
(0): 1340_0_LENGTH_FIELDACCESS(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(x0[0])))) → 1340_0_LENGTH_FIELDACCESS(java.lang.Object(x0[0]))

(0) -> (0), if (java.lang.Object(x0[0]) →^* java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(x0[0]'))))

The set Q consists of the following terms:
1362_1_length_InvokeMethod(1353_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL)))
1362_1_length_InvokeMethod(1353_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(x0)))))))
1362_1_length_InvokeMethod(1353_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL)))))

(8) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

1340_0_LENGTH_FIELDACCESS(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(x0[0])))) → 1340_0_LENGTH_FIELDACCESS(java.lang.Object(x0[0]))

The TRS R consists of the following rules:

1362_1_length_InvokeMethod(1353_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL))) → 1353_0_length_Return
1362_1_length_InvokeMethod(1353_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(x0))))))) → 1353_0_length_Return
1362_1_length_InvokeMethod(1353_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL))))) → 1353_0_length_Return

The set Q consists of the following terms:

1362_1_length_InvokeMethod(1353_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL)))
1362_1_length_InvokeMethod(1353_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(x0)))))))
1362_1_length_InvokeMethod(1353_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL)))))

We have to consider all minimal (P,Q,R)-chains.

(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:

Q DP problem:
The TRS P consists of the following rules:

1340_0_LENGTH_FIELDACCESS(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(x0[0])))) → 1340_0_LENGTH_FIELDACCESS(java.lang.Object(x0[0]))

R is empty.
The set Q consists of the following terms:

1362_1_length_InvokeMethod(1353_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL)))
1362_1_length_InvokeMethod(1353_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(x0)))))))
1362_1_length_InvokeMethod(1353_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL)))))

We have to consider all minimal (P,Q,R)-chains.

(12) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

1362_1_length_InvokeMethod(1353_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL)))
1362_1_length_InvokeMethod(1353_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(x0)))))))
1362_1_length_InvokeMethod(1353_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL)))))

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

1340_0_LENGTH_FIELDACCESS(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(x0[0])))) → 1340_0_LENGTH_FIELDACCESS(java.lang.Object(x0[0]))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

1340_0_LENGTH_FIELDACCESS(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(x0[0])))) → 1340_0_LENGTH_FIELDACCESS(java.lang.Object(x0[0]))
The graph contains the following edges 1 > 1

(15) YES

(16) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: CyclicAnalysisRec.CyclicAnalysisRec.appendNewList(I)LCyclicAnalysisRec/CyclicAnalysisRec;
SCC calls the following helper methods: CyclicAnalysisRec.CyclicAnalysisRec.appendNewList(I)LCyclicAnalysisRec/CyclicAnalysisRec;
Performed SCC analyses: UsedFieldsAnalysis

(17) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 20 rules for P and 11 rules for R.

P rules:
725_0_appendNewList_New(EOS(STATIC_725), i139) → 736_0_appendNewList_Duplicate(EOS(STATIC_736), i139)
736_0_appendNewList_Duplicate(EOS(STATIC_736), i139) → 748_0_appendNewList_InvokeMethod(EOS(STATIC_748), i139)
748_0_appendNewList_InvokeMethod(EOS(STATIC_748), i139) → 757_0_<init>_Load(EOS(STATIC_757), i139)
757_0_<init>_Load(EOS(STATIC_757), i139) → 778_0_<init>_InvokeMethod(EOS(STATIC_778), i139)
778_0_<init>_InvokeMethod(EOS(STATIC_778), i139) → 796_0_<init>_Return(EOS(STATIC_796), i139)
796_0_<init>_Return(EOS(STATIC_796), i139) → 814_0_appendNewList_FieldAccess(EOS(STATIC_814), i139)
814_0_appendNewList_FieldAccess(EOS(STATIC_814), i139) → 823_0_appendNewList_Load(EOS(STATIC_823), i139)
823_0_appendNewList_Load(EOS(STATIC_823), i139) → 836_0_appendNewList_ConstantStackPush(EOS(STATIC_836), i139, i139)
836_0_appendNewList_ConstantStackPush(EOS(STATIC_836), i139, i139) → 844_0_appendNewList_GT(EOS(STATIC_844), i139, i139, 1)
844_0_appendNewList_GT(EOS(STATIC_844), i179, i179, matching1) → 856_0_appendNewList_GT(EOS(STATIC_856), i179, i179, 1) | =(matching1, 1)
856_0_appendNewList_GT(EOS(STATIC_856), i179, i179, matching1) → 870_0_appendNewList_Load(EOS(STATIC_870), i179) | &&(>(i179, 1), =(matching1, 1))
870_0_appendNewList_Load(EOS(STATIC_870), i179) → 884_0_appendNewList_FieldAccess(EOS(STATIC_884), i179)
884_0_appendNewList_FieldAccess(EOS(STATIC_884), i179) → 894_0_appendNewList_Load(EOS(STATIC_894), i179)
894_0_appendNewList_Load(EOS(STATIC_894), i179) → 908_0_appendNewList_ConstantStackPush(EOS(STATIC_908), i179)
908_0_appendNewList_ConstantStackPush(EOS(STATIC_908), i179) → 925_0_appendNewList_IntArithmetic(EOS(STATIC_925), i179, 1)
925_0_appendNewList_IntArithmetic(EOS(STATIC_925), i179, matching1) → 942_0_appendNewList_InvokeMethod(EOS(STATIC_942), -(i179, 1)) | &&(>(i179, 0), =(matching1, 1))
942_0_appendNewList_InvokeMethod(EOS(STATIC_942), i205) → 956_1_appendNewList_InvokeMethod(956_0_appendNewList_Load(EOS(STATIC_956), i205), i205)
956_0_appendNewList_Load(EOS(STATIC_956), i205) → 981_0_appendNewList_Load(EOS(STATIC_981), i205)
981_0_appendNewList_Load(EOS(STATIC_981), i205) → 716_0_appendNewList_Load(EOS(STATIC_716), i205)
716_0_appendNewList_Load(EOS(STATIC_716), i139) → 725_0_appendNewList_New(EOS(STATIC_725), i139)
R rules:
844_0_appendNewList_GT(EOS(STATIC_844), i178, i178, matching1) → 855_0_appendNewList_GT(EOS(STATIC_855), i178, i178, 1) | =(matching1, 1)
855_0_appendNewList_GT(EOS(STATIC_855), i178, i178, matching1) → 869_0_appendNewList_Load(EOS(STATIC_869), i178) | &&(<=(i178, 1), =(matching1, 1))
869_0_appendNewList_Load(EOS(STATIC_869), i178) → 883_0_appendNewList_FieldAccess(EOS(STATIC_883), i178)
883_0_appendNewList_FieldAccess(EOS(STATIC_883), i178) → 893_0_appendNewList_Return(EOS(STATIC_893), i178)
956_1_appendNewList_InvokeMethod(893_0_appendNewList_Return(EOS(STATIC_893), matching1), matching2) → 1023_0_appendNewList_Return(EOS(STATIC_1023), 1, 1) | &&(=(matching1, 1), =(matching2, 1))
956_1_appendNewList_InvokeMethod(1036_0_appendNewList_Return(EOS(STATIC_1036)), i242) → 1091_0_appendNewList_Return(EOS(STATIC_1091), i242)
956_1_appendNewList_InvokeMethod(1213_0_appendNewList_Return(EOS(STATIC_1213)), i303) → 1291_0_appendNewList_Return(EOS(STATIC_1291), i303)
1023_0_appendNewList_Return(EOS(STATIC_1023), matching1, matching2) → 1036_0_appendNewList_Return(EOS(STATIC_1036)) | &&(=(matching1, 1), =(matching2, 1))
1091_0_appendNewList_Return(EOS(STATIC_1091), i242) → 1199_0_appendNewList_Return(EOS(STATIC_1199), i242)
1199_0_appendNewList_Return(EOS(STATIC_1199), i282) → 1213_0_appendNewList_Return(EOS(STATIC_1213))
1291_0_appendNewList_Return(EOS(STATIC_1291), i303) → 1199_0_appendNewList_Return(EOS(STATIC_1199), i303)

Combined rules. Obtained 1 conditional rules for P and 3 conditional rules for R.

P rules:
725_0_appendNewList_New(EOS(STATIC_725), x0) → 956_1_appendNewList_InvokeMethod(725_0_appendNewList_New(EOS(STATIC_725), -(x0, 1)), -(x0, 1)) | >(x0, 1)
R rules:
956_1_appendNewList_InvokeMethod(893_0_appendNewList_Return(EOS(STATIC_893), 1), 1) → 1036_0_appendNewList_Return(EOS(STATIC_1036))
956_1_appendNewList_InvokeMethod(1036_0_appendNewList_Return(EOS(STATIC_1036)), x0) → 1213_0_appendNewList_Return(EOS(STATIC_1213))
956_1_appendNewList_InvokeMethod(1213_0_appendNewList_Return(EOS(STATIC_1213)), x0) → 1213_0_appendNewList_Return(EOS(STATIC_1213))

Filtered ground terms:

725_0_appendNewList_New(x1, x2) → 725_0_appendNewList_New(x2)
Cond_725_0_appendNewList_New(x1, x2, x3) → Cond_725_0_appendNewList_New(x1, x3)
1213_0_appendNewList_Return(x1) → 1213_0_appendNewList_Return
1036_0_appendNewList_Return(x1) → 1036_0_appendNewList_Return
893_0_appendNewList_Return(x1, x2) → 893_0_appendNewList_Return

Combined rules. Obtained 1 conditional rules for P and 3 conditional rules for R.

P rules:
725_0_appendNewList_New(x0) → 956_1_appendNewList_InvokeMethod(725_0_appendNewList_New(-(x0, 1)), -(x0, 1)) | >(x0, 1)
R rules:
956_1_appendNewList_InvokeMethod(893_0_appendNewList_Return, 1) → 1036_0_appendNewList_Return
956_1_appendNewList_InvokeMethod(1036_0_appendNewList_Return, x0) → 1213_0_appendNewList_Return
956_1_appendNewList_InvokeMethod(1213_0_appendNewList_Return, x0) → 1213_0_appendNewList_Return

Performed bisimulation on rules. Used the following equivalence classes: {[893_0_appendNewList_Return, 1036_0_appendNewList_Return, 1213_0_appendNewList_Return]=893_0_appendNewList_Return}

Finished conversion. Obtained 2 rules for P and 2 rules for R. System has predefined symbols.

P rules:
725_0_APPENDNEWLIST_NEW(x0) → COND_725_0_APPENDNEWLIST_NEW(>(x0, 1), x0)
COND_725_0_APPENDNEWLIST_NEW(TRUE, x0) → 725_0_APPENDNEWLIST_NEW(-(x0, 1))
R rules:
956_1_appendNewList_InvokeMethod(893_0_appendNewList_Return, 1) → 893_0_appendNewList_Return
956_1_appendNewList_InvokeMethod(893_0_appendNewList_Return, x0) → 893_0_appendNewList_Return

(18) 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:
956_1_appendNewList_InvokeMethod(893_0_appendNewList_Return, 1) → 893_0_appendNewList_Return
956_1_appendNewList_InvokeMethod(893_0_appendNewList_Return, x0) → 893_0_appendNewList_Return

The integer pair graph contains the following rules and edges:
(0): 725_0_APPENDNEWLIST_NEW(x0[0]) → COND_725_0_APPENDNEWLIST_NEW(x0[0] > 1, x0[0])
(1): COND_725_0_APPENDNEWLIST_NEW(TRUE, x0[1]) → 725_0_APPENDNEWLIST_NEW(x0[1] - 1)

(0) -> (1), if (x0[0] > 1 ∧x0[0] →^* x0[1])

(1) -> (0), if (x0[1] - 1 →^* x0[0])

The set Q consists of the following terms:
956_1_appendNewList_InvokeMethod(893_0_appendNewList_Return, x0)

(19) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@6df0a29b Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 725_0_APPENDNEWLIST_NEW(x0) → COND_725_0_APPENDNEWLIST_NEW(>(x0, 1), x0) the following chains were created:

We consider the chain 725_0_APPENDNEWLIST_NEW(x0[0]) → COND_725_0_APPENDNEWLIST_NEW(>(x0[0], 1), x0[0]), COND_725_0_APPENDNEWLIST_NEW(TRUE, x0[1]) → 725_0_APPENDNEWLIST_NEW(-(x0[1], 1)) which results in the following constraint:
(1)    (>(x0[0], 1)=TRUE∧x0[0]=x0[1] ⇒ 725_0_APPENDNEWLIST_NEW(x0[0])≥NonInfC∧725_0_APPENDNEWLIST_NEW(x0[0])≥COND_725_0_APPENDNEWLIST_NEW(>(x0[0], 1), x0[0])∧(U^Increasing(COND_725_0_APPENDNEWLIST_NEW(>(x0[0], 1), x0[0])), ≥))

We simplified constraint (1) using rule (IV) which results in the following new constraint:
(2)    (>(x0[0], 1)=TRUE ⇒ 725_0_APPENDNEWLIST_NEW(x0[0])≥NonInfC∧725_0_APPENDNEWLIST_NEW(x0[0])≥COND_725_0_APPENDNEWLIST_NEW(>(x0[0], 1), x0[0])∧(U^Increasing(COND_725_0_APPENDNEWLIST_NEW(>(x0[0], 1), x0[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x0[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_725_0_APPENDNEWLIST_NEW(>(x0[0], 1), x0[0])), ≥)∧[(-1)Bound*bni_10] + [(2)bni_10]x0[0] ≥ 0∧[(-1)bso_11] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x0[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_725_0_APPENDNEWLIST_NEW(>(x0[0], 1), x0[0])), ≥)∧[(-1)Bound*bni_10] + [(2)bni_10]x0[0] ≥ 0∧[(-1)bso_11] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x0[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_725_0_APPENDNEWLIST_NEW(>(x0[0], 1), x0[0])), ≥)∧[(-1)Bound*bni_10] + [(2)bni_10]x0[0] ≥ 0∧[(-1)bso_11] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x0[0] ≥ 0 ⇒ (U^Increasing(COND_725_0_APPENDNEWLIST_NEW(>(x0[0], 1), x0[0])), ≥)∧[(-1)Bound*bni_10 + (4)bni_10] + [(2)bni_10]x0[0] ≥ 0∧[(-1)bso_11] ≥ 0)

For Pair COND_725_0_APPENDNEWLIST_NEW(TRUE, x0) → 725_0_APPENDNEWLIST_NEW(-(x0, 1)) the following chains were created:

We consider the chain COND_725_0_APPENDNEWLIST_NEW(TRUE, x0[1]) → 725_0_APPENDNEWLIST_NEW(-(x0[1], 1)) which results in the following constraint:
(7)    (COND_725_0_APPENDNEWLIST_NEW(TRUE, x0[1])≥NonInfC∧COND_725_0_APPENDNEWLIST_NEW(TRUE, x0[1])≥725_0_APPENDNEWLIST_NEW(-(x0[1], 1))∧(U^Increasing(725_0_APPENDNEWLIST_NEW(-(x0[1], 1))), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    ((U^Increasing(725_0_APPENDNEWLIST_NEW(-(x0[1], 1))), ≥)∧[bni_12] = 0∧[2 + (-1)bso_13] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    ((U^Increasing(725_0_APPENDNEWLIST_NEW(-(x0[1], 1))), ≥)∧[bni_12] = 0∧[2 + (-1)bso_13] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    ((U^Increasing(725_0_APPENDNEWLIST_NEW(-(x0[1], 1))), ≥)∧[bni_12] = 0∧[2 + (-1)bso_13] ≥ 0)

We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(11)    ((U^Increasing(725_0_APPENDNEWLIST_NEW(-(x0[1], 1))), ≥)∧[bni_12] = 0∧0 = 0∧[2 + (-1)bso_13] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

725_0_APPENDNEWLIST_NEW(x0) → COND_725_0_APPENDNEWLIST_NEW(>(x0, 1), x0)
- (x0[0] ≥ 0 ⇒ (U^Increasing(COND_725_0_APPENDNEWLIST_NEW(>(x0[0], 1), x0[0])), ≥)∧[(-1)Bound*bni_10 + (4)bni_10] + [(2)bni_10]x0[0] ≥ 0∧[(-1)bso_11] ≥ 0)
COND_725_0_APPENDNEWLIST_NEW(TRUE, x0) → 725_0_APPENDNEWLIST_NEW(-(x0, 1))
- ((U^Increasing(725_0_APPENDNEWLIST_NEW(-(x0[1], 1))), ≥)∧[bni_12] = 0∧0 = 0∧[2 + (-1)bso_13] ≥ 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(956_1_appendNewList_InvokeMethod(x₁, x₂)) = [-1]
POL(893_0_appendNewList_Return) = [-1]
POL(1) = [1]
POL(725_0_APPENDNEWLIST_NEW(x₁)) = [2]x₁
POL(COND_725_0_APPENDNEWLIST_NEW(x₁, x₂)) = [2]x₂
POL(>(x₁, x₂)) = [-1]
POL(-(x₁, x₂)) = x₁ + [-1]x₂

The following pairs are in P_>:

COND_725_0_APPENDNEWLIST_NEW(TRUE, x0[1]) → 725_0_APPENDNEWLIST_NEW(-(x0[1], 1))

The following pairs are in P_bound:

725_0_APPENDNEWLIST_NEW(x0[0]) → COND_725_0_APPENDNEWLIST_NEW(>(x0[0], 1), x0[0])

The following pairs are in P_≥:

725_0_APPENDNEWLIST_NEW(x0[0]) → COND_725_0_APPENDNEWLIST_NEW(>(x0[0], 1), x0[0])

There are no usable rules.

(20) Complex Obligation (AND)

(21) 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:
956_1_appendNewList_InvokeMethod(893_0_appendNewList_Return, 1) → 893_0_appendNewList_Return
956_1_appendNewList_InvokeMethod(893_0_appendNewList_Return, x0) → 893_0_appendNewList_Return

The integer pair graph contains the following rules and edges:
(0): 725_0_APPENDNEWLIST_NEW(x0[0]) → COND_725_0_APPENDNEWLIST_NEW(x0[0] > 1, x0[0])

The set Q consists of the following terms:
956_1_appendNewList_InvokeMethod(893_0_appendNewList_Return, x0)

(22) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(23) TRUE

(24) 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:
956_1_appendNewList_InvokeMethod(893_0_appendNewList_Return, 1) → 893_0_appendNewList_Return
956_1_appendNewList_InvokeMethod(893_0_appendNewList_Return, x0) → 893_0_appendNewList_Return

The integer pair graph contains the following rules and edges:
(1): COND_725_0_APPENDNEWLIST_NEW(TRUE, x0[1]) → 725_0_APPENDNEWLIST_NEW(x0[1] - 1)

The set Q consists of the following terms:
956_1_appendNewList_InvokeMethod(893_0_appendNewList_Return, x0)

(25) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIDPv1Proof (SOUND transformation)

(7) Obligation:

(8) IDPtoQDPProof (SOUND transformation)

(9) Obligation:

(10) UsableRulesProof (EQUIVALENT transformation)

(11) Obligation:

(12) QReductionProof (EQUIVALENT transformation)

(13) Obligation:

(14) QDPSizeChangeProof (EQUIVALENT transformation)

(15) YES

(16) Obligation:

(17) SCCToIDPv1Proof (SOUND transformation)

(18) Obligation:

(19) IDPNonInfProof (SOUND transformation)

(20) Complex Obligation (AND)

(21) Obligation:

(22) IDependencyGraphProof (EQUIVALENT transformation)

(23) TRUE

(24) Obligation:

(25) IDependencyGraphProof (EQUIVALENT transformation)

(26) TRUE