Termination proof of /tmp/tmph3P7y9/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 (⇒, 100 ms)

        ↳7 IDP

        ↳8 IDPtoQDPProof (⇒, 30 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 (⇒, 180 ms)

        ↳18 IDP

        ↳19 IDPNonInfProof (⇒, 70 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:
1370_0_length_FieldAccess(EOS(STATIC_1370), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o827)), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o827))) → 1372_0_length_FieldAccess(EOS(STATIC_1372), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o827)), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o827)))
1372_0_length_FieldAccess(EOS(STATIC_1372), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o827)), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o827))) → 1374_0_length_NONNULL(EOS(STATIC_1374), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o827)), o827)
1374_0_length_NONNULL(EOS(STATIC_1374), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o829sub))), java.lang.Object(o829sub)) → 1376_0_length_NONNULL(EOS(STATIC_1376), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o829sub))), java.lang.Object(o829sub))
1376_0_length_NONNULL(EOS(STATIC_1376), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o829sub))), java.lang.Object(o829sub)) → 1378_0_length_ConstantStackPush(EOS(STATIC_1378), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o829sub))))
1378_0_length_ConstantStackPush(EOS(STATIC_1378), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o829sub)))) → 1382_0_length_Load(EOS(STATIC_1382), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o829sub))))
1382_0_length_Load(EOS(STATIC_1382), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o829sub)))) → 1385_0_length_FieldAccess(EOS(STATIC_1385), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o829sub))))
1385_0_length_FieldAccess(EOS(STATIC_1385), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(o829sub)))) → 1388_0_length_InvokeMethod(EOS(STATIC_1388), java.lang.Object(o829sub))
1388_0_length_InvokeMethod(EOS(STATIC_1388), java.lang.Object(o829sub)) → 1392_1_length_InvokeMethod(1392_0_length_Load(EOS(STATIC_1392), java.lang.Object(o829sub)), java.lang.Object(o829sub))
1392_0_length_Load(EOS(STATIC_1392), java.lang.Object(o829sub)) → 1396_0_length_Load(EOS(STATIC_1396), java.lang.Object(o829sub))
1396_0_length_Load(EOS(STATIC_1396), java.lang.Object(o829sub)) → 1369_0_length_Load(EOS(STATIC_1369), java.lang.Object(o829sub))
1369_0_length_Load(EOS(STATIC_1369), java.lang.Object(o822sub)) → 1370_0_length_FieldAccess(EOS(STATIC_1370), java.lang.Object(o822sub), java.lang.Object(o822sub))
R rules:
1374_0_length_NONNULL(EOS(STATIC_1374), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL)), NULL) → 1377_0_length_NONNULL(EOS(STATIC_1377), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL)), NULL)
1377_0_length_NONNULL(EOS(STATIC_1377), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL)), NULL) → 1380_0_length_ConstantStackPush(EOS(STATIC_1380), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL)))
1380_0_length_ConstantStackPush(EOS(STATIC_1380), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL))) → 1383_0_length_Return(EOS(STATIC_1383), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL)))
1392_1_length_InvokeMethod(1383_0_length_Return(EOS(STATIC_1383), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL))), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL))) → 1403_0_length_Return(EOS(STATIC_1403), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL)), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL)))
1392_1_length_InvokeMethod(1406_0_length_Return(EOS(STATIC_1406)), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL))))) → 1423_0_length_Return(EOS(STATIC_1423), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL)))))
1392_1_length_InvokeMethod(1570_0_length_Return(EOS(STATIC_1570)), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o1082))))))) → 1589_0_length_Return(EOS(STATIC_1589), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o1082)))))))
1403_0_length_Return(EOS(STATIC_1403), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL)), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL))) → 1404_0_length_IntArithmetic(EOS(STATIC_1404))
1404_0_length_IntArithmetic(EOS(STATIC_1404)) → 1406_0_length_Return(EOS(STATIC_1406))
1423_0_length_Return(EOS(STATIC_1423), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL))))) → 1450_0_length_Return(EOS(STATIC_1450), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL)))))
1450_0_length_Return(EOS(STATIC_1450), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o869))))) → 1492_0_length_Return(EOS(STATIC_1492), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o869)))))
1492_0_length_Return(EOS(STATIC_1492), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o918))))) → 1523_0_length_Return(EOS(STATIC_1523), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o918)))))
1523_0_length_Return(EOS(STATIC_1523), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o979))))) → 1561_0_length_Return(EOS(STATIC_1561), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o979)))))
1561_0_length_Return(EOS(STATIC_1561), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o1039))))) → 1565_0_length_IntArithmetic(EOS(STATIC_1565))
1565_0_length_IntArithmetic(EOS(STATIC_1565)) → 1570_0_length_Return(EOS(STATIC_1570))
1589_0_length_Return(EOS(STATIC_1589), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, o1082))))))) → 1561_0_length_Return(EOS(STATIC_1561), 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:
1370_0_length_FieldAccess(EOS(STATIC_1370), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(x0))), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(x0)))) → 1392_1_length_InvokeMethod(1370_0_length_FieldAccess(EOS(STATIC_1370), java.lang.Object(x0), java.lang.Object(x0)), java.lang.Object(x0))
R rules:
1392_1_length_InvokeMethod(1383_0_length_Return(EOS(STATIC_1383), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL))), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL))) → 1406_0_length_Return(EOS(STATIC_1406))
1392_1_length_InvokeMethod(1570_0_length_Return(EOS(STATIC_1570)), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, x0))))))) → 1570_0_length_Return(EOS(STATIC_1570))
1392_1_length_InvokeMethod(1406_0_length_Return(EOS(STATIC_1406)), java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(EOC, NULL))))) → 1570_0_length_Return(EOS(STATIC_1570))

Filtered ground terms:

1370_0_length_FieldAccess(x1, x2, x3) → 1370_0_length_FieldAccess(x2, x3)
CyclicAnalysisRec.CyclicAnalysisRec(x1, x2) → CyclicAnalysisRec.CyclicAnalysisRec(x2)
1570_0_length_Return(x1) → 1570_0_length_Return
1406_0_length_Return(x1) → 1406_0_length_Return
1383_0_length_Return(x1, x2) → 1383_0_length_Return

Filtered duplicate args:

1370_0_length_FieldAccess(x1, x2) → 1370_0_length_FieldAccess(x2)

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

P rules:
1370_0_length_FieldAccess(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(x0)))) → 1392_1_length_InvokeMethod(1370_0_length_FieldAccess(java.lang.Object(x0)), java.lang.Object(x0))
R rules:
1392_1_length_InvokeMethod(1383_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL))) → 1406_0_length_Return
1392_1_length_InvokeMethod(1570_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(x0))))))) → 1570_0_length_Return
1392_1_length_InvokeMethod(1406_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL))))) → 1570_0_length_Return

Performed bisimulation on rules. Used the following equivalence classes: {[1383_0_length_Return, 1406_0_length_Return, 1570_0_length_Return]=1383_0_length_Return}

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

P rules:
1370_0_LENGTH_FIELDACCESS(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(x0)))) → 1370_0_LENGTH_FIELDACCESS(java.lang.Object(x0))
R rules:
1392_1_length_InvokeMethod(1383_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL))) → 1383_0_length_Return
1392_1_length_InvokeMethod(1383_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(x0))))))) → 1383_0_length_Return
1392_1_length_InvokeMethod(1383_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL))))) → 1383_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:
1392_1_length_InvokeMethod(1383_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL))) → 1383_0_length_Return
1392_1_length_InvokeMethod(1383_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(x0))))))) → 1383_0_length_Return
1392_1_length_InvokeMethod(1383_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL))))) → 1383_0_length_Return

The integer pair graph contains the following rules and edges:
(0): 1370_0_LENGTH_FIELDACCESS(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(x0[0])))) → 1370_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:
1392_1_length_InvokeMethod(1383_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL)))
1392_1_length_InvokeMethod(1383_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(x0)))))))
1392_1_length_InvokeMethod(1383_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:

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

The TRS R consists of the following rules:

1392_1_length_InvokeMethod(1383_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL))) → 1383_0_length_Return
1392_1_length_InvokeMethod(1383_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(x0))))))) → 1383_0_length_Return
1392_1_length_InvokeMethod(1383_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL))))) → 1383_0_length_Return

The set Q consists of the following terms:

1392_1_length_InvokeMethod(1383_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL)))
1392_1_length_InvokeMethod(1383_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(x0)))))))
1392_1_length_InvokeMethod(1383_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:

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

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

1392_1_length_InvokeMethod(1383_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL)))
1392_1_length_InvokeMethod(1383_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(x0)))))))
1392_1_length_InvokeMethod(1383_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].

1392_1_length_InvokeMethod(1383_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(NULL)))
1392_1_length_InvokeMethod(1383_0_length_Return, java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(x0)))))))
1392_1_length_InvokeMethod(1383_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:

1370_0_LENGTH_FIELDACCESS(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(x0[0])))) → 1370_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:

1370_0_LENGTH_FIELDACCESS(java.lang.Object(CyclicAnalysisRec.CyclicAnalysisRec(java.lang.Object(x0[0])))) → 1370_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:
716_0_appendNewList_New(EOS(STATIC_716), i139) → 726_0_appendNewList_Duplicate(EOS(STATIC_726), i139)
726_0_appendNewList_Duplicate(EOS(STATIC_726), i139) → 736_0_appendNewList_InvokeMethod(EOS(STATIC_736), i139)
736_0_appendNewList_InvokeMethod(EOS(STATIC_736), i139) → 749_0_<init>_Load(EOS(STATIC_749), i139)
749_0_<init>_Load(EOS(STATIC_749), i139) → 765_0_<init>_InvokeMethod(EOS(STATIC_765), i139)
765_0_<init>_InvokeMethod(EOS(STATIC_765), i139) → 781_0_<init>_Return(EOS(STATIC_781), i139)
781_0_<init>_Return(EOS(STATIC_781), i139) → 802_0_appendNewList_FieldAccess(EOS(STATIC_802), i139)
802_0_appendNewList_FieldAccess(EOS(STATIC_802), i139) → 812_0_appendNewList_Load(EOS(STATIC_812), i139)
812_0_appendNewList_Load(EOS(STATIC_812), i139) → 825_0_appendNewList_ConstantStackPush(EOS(STATIC_825), i139, i139)
825_0_appendNewList_ConstantStackPush(EOS(STATIC_825), i139, i139) → 833_0_appendNewList_GT(EOS(STATIC_833), i139, i139, 1)
833_0_appendNewList_GT(EOS(STATIC_833), i178, i178, matching1) → 842_0_appendNewList_GT(EOS(STATIC_842), i178, i178, 1) | =(matching1, 1)
842_0_appendNewList_GT(EOS(STATIC_842), i178, i178, matching1) → 858_0_appendNewList_Load(EOS(STATIC_858), i178) | &&(>(i178, 1), =(matching1, 1))
858_0_appendNewList_Load(EOS(STATIC_858), i178) → 873_0_appendNewList_FieldAccess(EOS(STATIC_873), i178)
873_0_appendNewList_FieldAccess(EOS(STATIC_873), i178) → 882_0_appendNewList_Load(EOS(STATIC_882), i178)
882_0_appendNewList_Load(EOS(STATIC_882), i178) → 899_0_appendNewList_ConstantStackPush(EOS(STATIC_899), i178)
899_0_appendNewList_ConstantStackPush(EOS(STATIC_899), i178) → 918_0_appendNewList_IntArithmetic(EOS(STATIC_918), i178, 1)
918_0_appendNewList_IntArithmetic(EOS(STATIC_918), i178, matching1) → 942_0_appendNewList_InvokeMethod(EOS(STATIC_942), -(i178, 1)) | &&(>(i178, 0), =(matching1, 1))
942_0_appendNewList_InvokeMethod(EOS(STATIC_942), i205) → 960_1_appendNewList_InvokeMethod(960_0_appendNewList_Load(EOS(STATIC_960), i205), i205)
960_0_appendNewList_Load(EOS(STATIC_960), i205) → 988_0_appendNewList_Load(EOS(STATIC_988), i205)
988_0_appendNewList_Load(EOS(STATIC_988), i205) → 707_0_appendNewList_Load(EOS(STATIC_707), i205)
707_0_appendNewList_Load(EOS(STATIC_707), i139) → 716_0_appendNewList_New(EOS(STATIC_716), i139)
R rules:
833_0_appendNewList_GT(EOS(STATIC_833), i177, i177, matching1) → 841_0_appendNewList_GT(EOS(STATIC_841), i177, i177, 1) | =(matching1, 1)
841_0_appendNewList_GT(EOS(STATIC_841), i177, i177, matching1) → 857_0_appendNewList_Load(EOS(STATIC_857), i177) | &&(<=(i177, 1), =(matching1, 1))
857_0_appendNewList_Load(EOS(STATIC_857), i177) → 872_0_appendNewList_FieldAccess(EOS(STATIC_872), i177)
872_0_appendNewList_FieldAccess(EOS(STATIC_872), i177) → 881_0_appendNewList_Return(EOS(STATIC_881), i177)
960_1_appendNewList_InvokeMethod(881_0_appendNewList_Return(EOS(STATIC_881), matching1), matching2) → 1030_0_appendNewList_Return(EOS(STATIC_1030), 1, 1) | &&(=(matching1, 1), =(matching2, 1))
960_1_appendNewList_InvokeMethod(1042_0_appendNewList_Return(EOS(STATIC_1042)), i242) → 1098_0_appendNewList_Return(EOS(STATIC_1098), i242)
960_1_appendNewList_InvokeMethod(1236_0_appendNewList_Return(EOS(STATIC_1236)), i305) → 1322_0_appendNewList_Return(EOS(STATIC_1322), i305)
1030_0_appendNewList_Return(EOS(STATIC_1030), matching1, matching2) → 1042_0_appendNewList_Return(EOS(STATIC_1042)) | &&(=(matching1, 1), =(matching2, 1))
1098_0_appendNewList_Return(EOS(STATIC_1098), i242) → 1220_0_appendNewList_Return(EOS(STATIC_1220), i242)
1220_0_appendNewList_Return(EOS(STATIC_1220), i282) → 1236_0_appendNewList_Return(EOS(STATIC_1236))
1322_0_appendNewList_Return(EOS(STATIC_1322), i305) → 1220_0_appendNewList_Return(EOS(STATIC_1220), i305)

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

P rules:
716_0_appendNewList_New(EOS(STATIC_716), x0) → 960_1_appendNewList_InvokeMethod(716_0_appendNewList_New(EOS(STATIC_716), -(x0, 1)), -(x0, 1)) | >(x0, 1)
R rules:
960_1_appendNewList_InvokeMethod(881_0_appendNewList_Return(EOS(STATIC_881), 1), 1) → 1042_0_appendNewList_Return(EOS(STATIC_1042))
960_1_appendNewList_InvokeMethod(1042_0_appendNewList_Return(EOS(STATIC_1042)), x0) → 1236_0_appendNewList_Return(EOS(STATIC_1236))
960_1_appendNewList_InvokeMethod(1236_0_appendNewList_Return(EOS(STATIC_1236)), x0) → 1236_0_appendNewList_Return(EOS(STATIC_1236))

Filtered ground terms:

716_0_appendNewList_New(x1, x2) → 716_0_appendNewList_New(x2)
Cond_716_0_appendNewList_New(x1, x2, x3) → Cond_716_0_appendNewList_New(x1, x3)
1236_0_appendNewList_Return(x1) → 1236_0_appendNewList_Return
1042_0_appendNewList_Return(x1) → 1042_0_appendNewList_Return
881_0_appendNewList_Return(x1, x2) → 881_0_appendNewList_Return

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

P rules:
716_0_appendNewList_New(x0) → 960_1_appendNewList_InvokeMethod(716_0_appendNewList_New(-(x0, 1)), -(x0, 1)) | >(x0, 1)
R rules:
960_1_appendNewList_InvokeMethod(881_0_appendNewList_Return, 1) → 1042_0_appendNewList_Return
960_1_appendNewList_InvokeMethod(1042_0_appendNewList_Return, x0) → 1236_0_appendNewList_Return
960_1_appendNewList_InvokeMethod(1236_0_appendNewList_Return, x0) → 1236_0_appendNewList_Return

Performed bisimulation on rules. Used the following equivalence classes: {[881_0_appendNewList_Return, 1042_0_appendNewList_Return, 1236_0_appendNewList_Return]=881_0_appendNewList_Return}

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

P rules:
716_0_APPENDNEWLIST_NEW(x0) → COND_716_0_APPENDNEWLIST_NEW(>(x0, 1), x0)
COND_716_0_APPENDNEWLIST_NEW(TRUE, x0) → 716_0_APPENDNEWLIST_NEW(-(x0, 1))
R rules:
960_1_appendNewList_InvokeMethod(881_0_appendNewList_Return, 1) → 881_0_appendNewList_Return
960_1_appendNewList_InvokeMethod(881_0_appendNewList_Return, x0) → 881_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:
960_1_appendNewList_InvokeMethod(881_0_appendNewList_Return, 1) → 881_0_appendNewList_Return
960_1_appendNewList_InvokeMethod(881_0_appendNewList_Return, x0) → 881_0_appendNewList_Return

The integer pair graph contains the following rules and edges:
(0): 716_0_APPENDNEWLIST_NEW(x0[0]) → COND_716_0_APPENDNEWLIST_NEW(x0[0] > 1, x0[0])
(1): COND_716_0_APPENDNEWLIST_NEW(TRUE, x0[1]) → 716_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:
960_1_appendNewList_InvokeMethod(881_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@65a8e0bd 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 716_0_APPENDNEWLIST_NEW(x0) → COND_716_0_APPENDNEWLIST_NEW(>(x0, 1), x0) the following chains were created:

We consider the chain 716_0_APPENDNEWLIST_NEW(x0[0]) → COND_716_0_APPENDNEWLIST_NEW(>(x0[0], 1), x0[0]), COND_716_0_APPENDNEWLIST_NEW(TRUE, x0[1]) → 716_0_APPENDNEWLIST_NEW(-(x0[1], 1)) which results in the following constraint:
(1)    (>(x0[0], 1)=TRUE∧x0[0]=x0[1] ⇒ 716_0_APPENDNEWLIST_NEW(x0[0])≥NonInfC∧716_0_APPENDNEWLIST_NEW(x0[0])≥COND_716_0_APPENDNEWLIST_NEW(>(x0[0], 1), x0[0])∧(U^Increasing(COND_716_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 ⇒ 716_0_APPENDNEWLIST_NEW(x0[0])≥NonInfC∧716_0_APPENDNEWLIST_NEW(x0[0])≥COND_716_0_APPENDNEWLIST_NEW(>(x0[0], 1), x0[0])∧(U^Increasing(COND_716_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_716_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_716_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_716_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_716_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_716_0_APPENDNEWLIST_NEW(TRUE, x0) → 716_0_APPENDNEWLIST_NEW(-(x0, 1)) the following chains were created:

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

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    ((U^Increasing(716_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(716_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(716_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(716_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.

716_0_APPENDNEWLIST_NEW(x0) → COND_716_0_APPENDNEWLIST_NEW(>(x0, 1), x0)
- (x0[0] ≥ 0 ⇒ (U^Increasing(COND_716_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_716_0_APPENDNEWLIST_NEW(TRUE, x0) → 716_0_APPENDNEWLIST_NEW(-(x0, 1))
- ((U^Increasing(716_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(960_1_appendNewList_InvokeMethod(x₁, x₂)) = [-1]
POL(881_0_appendNewList_Return) = [-1]
POL(1) = [1]
POL(716_0_APPENDNEWLIST_NEW(x₁)) = [2]x₁
POL(COND_716_0_APPENDNEWLIST_NEW(x₁, x₂)) = [2]x₂
POL(>(x₁, x₂)) = [-1]
POL(-(x₁, x₂)) = x₁ + [-1]x₂

The following pairs are in P_>:

COND_716_0_APPENDNEWLIST_NEW(TRUE, x0[1]) → 716_0_APPENDNEWLIST_NEW(-(x0[1], 1))

The following pairs are in P_bound:

716_0_APPENDNEWLIST_NEW(x0[0]) → COND_716_0_APPENDNEWLIST_NEW(>(x0[0], 1), x0[0])

The following pairs are in P_≥:

716_0_APPENDNEWLIST_NEW(x0[0]) → COND_716_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:
960_1_appendNewList_InvokeMethod(881_0_appendNewList_Return, 1) → 881_0_appendNewList_Return
960_1_appendNewList_InvokeMethod(881_0_appendNewList_Return, x0) → 881_0_appendNewList_Return

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

The set Q consists of the following terms:
960_1_appendNewList_InvokeMethod(881_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:
960_1_appendNewList_InvokeMethod(881_0_appendNewList_Return, 1) → 881_0_appendNewList_Return
960_1_appendNewList_InvokeMethod(881_0_appendNewList_Return, x0) → 881_0_appendNewList_Return

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

The set Q consists of the following terms:
960_1_appendNewList_InvokeMethod(881_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