Termination proof of /tmp/tmp_5OIri/AProVERec01.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 270 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 520 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 (⇒, 650 ms)

        ↳18 IDP

        ↳19 IDPNonInfProof (⇒, 120 ms)

        ↳20 IDP

        ↳21 IDependencyGraphProof (⇔, 0 ms)

        ↳22 TRUE

(0) Obligation:

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

public class AProVERec01 {
	public static void main(String[] args){
		List a = new List(args[0].length(), null);
		rec(args[1].length(), a);
	}

	public static void rec(int y, List res){
		int x = 3 * y;
		if(x < 100000){
			rec(x+1, res);
		}
		x = x*2;
		res.add(x);
	}
}

class List {
	int val = 0;
	List next = null;
	
	List (int v,List n){
		val = v;
		next = n;
	}

	public void add(int newVal){
		if (next == null) {
			next = new List(newVal, null);
		} else {
			next.add(newVal);
		}
	}
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

AProVERec01.rec(ILList;)V: Graph of 49 nodes with 0 SCCs.

List.add(I)V: Graph of 42 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: List.add(I)V
SCC calls the following helper methods: List.add(I)V
Performed SCC analyses: UsedFieldsAnalysis

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 11 rules for P and 30 rules for R.

P rules:
583_0_add_FieldAccess(EOS(STATIC_583), java.lang.Object(List(EOC, o75)), i76, java.lang.Object(List(EOC, o75))) → 584_0_add_FieldAccess(EOS(STATIC_584), java.lang.Object(List(EOC, o75)), i76, java.lang.Object(List(EOC, o75)))
584_0_add_FieldAccess(EOS(STATIC_584), java.lang.Object(List(EOC, o75)), i76, java.lang.Object(List(EOC, o75))) → 587_0_add_NONNULL(EOS(STATIC_587), java.lang.Object(List(EOC, o75)), i76, o75)
587_0_add_NONNULL(EOS(STATIC_587), java.lang.Object(List(EOC, java.lang.Object(o78sub))), i76, java.lang.Object(o78sub)) → 590_0_add_NONNULL(EOS(STATIC_590), java.lang.Object(List(EOC, java.lang.Object(o78sub))), i76, java.lang.Object(o78sub))
590_0_add_NONNULL(EOS(STATIC_590), java.lang.Object(List(EOC, java.lang.Object(o78sub))), i76, java.lang.Object(o78sub)) → 593_0_add_Load(EOS(STATIC_593), java.lang.Object(List(EOC, java.lang.Object(o78sub))), i76)
593_0_add_Load(EOS(STATIC_593), java.lang.Object(List(EOC, java.lang.Object(o78sub))), i76) → 596_0_add_FieldAccess(EOS(STATIC_596), i76, java.lang.Object(List(EOC, java.lang.Object(o78sub))))
596_0_add_FieldAccess(EOS(STATIC_596), i76, java.lang.Object(List(EOC, java.lang.Object(o78sub)))) → 601_0_add_Load(EOS(STATIC_601), i76, java.lang.Object(o78sub))
601_0_add_Load(EOS(STATIC_601), i76, java.lang.Object(o78sub)) → 604_0_add_InvokeMethod(EOS(STATIC_604), java.lang.Object(o78sub), i76)
604_0_add_InvokeMethod(EOS(STATIC_604), java.lang.Object(o78sub), i76) → 608_1_add_InvokeMethod(608_0_add_Load(EOS(STATIC_608), java.lang.Object(o78sub), i76), java.lang.Object(o78sub), i76)
608_0_add_Load(EOS(STATIC_608), java.lang.Object(o78sub), i76) → 611_0_add_Load(EOS(STATIC_611), java.lang.Object(o78sub), i76)
611_0_add_Load(EOS(STATIC_611), java.lang.Object(o78sub), i76) → 580_0_add_Load(EOS(STATIC_580), java.lang.Object(o78sub), i76)
580_0_add_Load(EOS(STATIC_580), java.lang.Object(o70sub), i76) → 583_0_add_FieldAccess(EOS(STATIC_583), java.lang.Object(o70sub), i76, java.lang.Object(o70sub))
R rules:
587_0_add_NONNULL(EOS(STATIC_587), java.lang.Object(List(EOC, NULL)), i76, NULL) → 591_0_add_NONNULL(EOS(STATIC_591), java.lang.Object(List(EOC, NULL)), i76, NULL)
591_0_add_NONNULL(EOS(STATIC_591), java.lang.Object(List(EOC, NULL)), i76, NULL) → 595_0_add_Load(EOS(STATIC_595), java.lang.Object(List(EOC, NULL)), i76)
595_0_add_Load(EOS(STATIC_595), java.lang.Object(List(EOC, NULL)), i76) → 598_0_add_New(EOS(STATIC_598), i76, java.lang.Object(List(EOC, NULL)))
598_0_add_New(EOS(STATIC_598), i76, java.lang.Object(List(EOC, NULL))) → 602_0_add_Duplicate(EOS(STATIC_602), i76, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)))
602_0_add_Duplicate(EOS(STATIC_602), i76, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL))) → 606_0_add_Load(EOS(STATIC_606), i76, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)))
606_0_add_Load(EOS(STATIC_606), i76, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL))) → 610_0_add_ConstantStackPush(EOS(STATIC_610), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76)
608_1_add_InvokeMethod(648_0_add_Return(EOS(STATIC_648)), java.lang.Object(o78sub), i89) → 670_0_add_Return(EOS(STATIC_670), java.lang.Object(List(EOC, java.lang.Object(List(EOC, NULL)))), i89)
608_1_add_InvokeMethod(752_0_add_Return(EOS(STATIC_752)), java.lang.Object(o78sub), i156) → 814_0_add_Return(EOS(STATIC_814), java.lang.Object(List(EOC, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o157)))))), i156)
610_0_add_ConstantStackPush(EOS(STATIC_610), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76) → 613_0_add_InvokeMethod(EOS(STATIC_613), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL)
613_0_add_InvokeMethod(EOS(STATIC_613), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL) → 615_0_<init>_Load(EOS(STATIC_615), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), i76, NULL)
615_0_<init>_Load(EOS(STATIC_615), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), i76, NULL) → 620_0_<init>_InvokeMethod(EOS(STATIC_620), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)))
620_0_<init>_InvokeMethod(EOS(STATIC_620), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL))) → 622_0_<init>_Load(EOS(STATIC_622), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), i76, NULL)
622_0_<init>_Load(EOS(STATIC_622), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), i76, NULL) → 623_0_<init>_ConstantStackPush(EOS(STATIC_623), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)))
623_0_<init>_ConstantStackPush(EOS(STATIC_623), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL))) → 625_0_<init>_FieldAccess(EOS(STATIC_625), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), 0)
625_0_<init>_FieldAccess(EOS(STATIC_625), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), matching1) → 627_0_<init>_Load(EOS(STATIC_627), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), i76, NULL) | =(matching1, 0)
627_0_<init>_Load(EOS(STATIC_627), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), i76, NULL) → 629_0_<init>_ConstantStackPush(EOS(STATIC_629), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)))
629_0_<init>_ConstantStackPush(EOS(STATIC_629), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL))) → 630_0_<init>_FieldAccess(EOS(STATIC_630), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), NULL)
630_0_<init>_FieldAccess(EOS(STATIC_630), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), NULL) → 632_0_<init>_Load(EOS(STATIC_632), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), i76, NULL)
632_0_<init>_Load(EOS(STATIC_632), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), i76, NULL) → 634_0_<init>_Load(EOS(STATIC_634), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)))
634_0_<init>_Load(EOS(STATIC_634), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL))) → 635_0_<init>_FieldAccess(EOS(STATIC_635), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), NULL, java.lang.Object(List(EOC, NULL)), i76)
635_0_<init>_FieldAccess(EOS(STATIC_635), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), NULL, java.lang.Object(List(EOC, NULL)), i76) → 637_0_<init>_Load(EOS(STATIC_637), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), NULL)
637_0_<init>_Load(EOS(STATIC_637), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), NULL) → 639_0_<init>_Load(EOS(STATIC_639), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, NULL, java.lang.Object(List(EOC, NULL)))
639_0_<init>_Load(EOS(STATIC_639), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, NULL, java.lang.Object(List(EOC, NULL))) → 641_0_<init>_FieldAccess(EOS(STATIC_641), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), NULL)
641_0_<init>_FieldAccess(EOS(STATIC_641), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL, java.lang.Object(List(EOC, NULL)), NULL) → 642_0_<init>_Return(EOS(STATIC_642), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL)
642_0_<init>_Return(EOS(STATIC_642), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL) → 644_0_add_FieldAccess(EOS(STATIC_644), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)))
644_0_add_FieldAccess(EOS(STATIC_644), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL))) → 646_0_add_JMP(EOS(STATIC_646))
646_0_add_JMP(EOS(STATIC_646)) → 648_0_add_Return(EOS(STATIC_648))
670_0_add_Return(EOS(STATIC_670), java.lang.Object(List(EOC, java.lang.Object(List(EOC, NULL)))), i89) → 740_0_add_Return(EOS(STATIC_740), java.lang.Object(List(EOC, java.lang.Object(List(EOC, NULL)))), i89)
740_0_add_Return(EOS(STATIC_740), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o157)))), i143) → 752_0_add_Return(EOS(STATIC_752))
814_0_add_Return(EOS(STATIC_814), java.lang.Object(List(EOC, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o157)))))), i156) → 740_0_add_Return(EOS(STATIC_740), java.lang.Object(List(EOC, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o157)))))), i156)

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

P rules:
583_0_add_FieldAccess(EOS(STATIC_583), java.lang.Object(List(EOC, java.lang.Object(x0))), x1, java.lang.Object(List(EOC, java.lang.Object(x0)))) → 608_1_add_InvokeMethod(583_0_add_FieldAccess(EOS(STATIC_583), java.lang.Object(x0), x1, java.lang.Object(x0)), java.lang.Object(x0), x1)
R rules:
608_1_add_InvokeMethod(648_0_add_Return(EOS(STATIC_648)), java.lang.Object(x0), x1) → 752_0_add_Return(EOS(STATIC_752))
608_1_add_InvokeMethod(752_0_add_Return(EOS(STATIC_752)), java.lang.Object(x0), x1) → 752_0_add_Return(EOS(STATIC_752))

Filtered ground terms:

583_0_add_FieldAccess(x1, x2, x3, x4) → 583_0_add_FieldAccess(x2, x3, x4)
List(x1, x2) → List(x2)
752_0_add_Return(x1) → 752_0_add_Return
648_0_add_Return(x1) → 648_0_add_Return

Filtered duplicate args:

583_0_add_FieldAccess(x1, x2, x3) → 583_0_add_FieldAccess(x2, x3)

Filtered unneeded arguments:

583_0_add_FieldAccess(x1, x2) → 583_0_add_FieldAccess(x2)
608_1_add_InvokeMethod(x1, x2, x3) → 608_1_add_InvokeMethod(x1)

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

P rules:
583_0_add_FieldAccess(java.lang.Object(List(java.lang.Object(x0)))) → 608_1_add_InvokeMethod(583_0_add_FieldAccess(java.lang.Object(x0)))
R rules:
608_1_add_InvokeMethod(648_0_add_Return) → 752_0_add_Return
608_1_add_InvokeMethod(752_0_add_Return) → 752_0_add_Return

Performed bisimulation on rules. Used the following equivalence classes: {[648_0_add_Return, 752_0_add_Return]=648_0_add_Return}

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

P rules:
583_0_ADD_FIELDACCESS(java.lang.Object(List(java.lang.Object(x0)))) → 583_0_ADD_FIELDACCESS(java.lang.Object(x0))
R rules:
608_1_add_InvokeMethod(648_0_add_Return) → 648_0_add_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:
608_1_add_InvokeMethod(648_0_add_Return) → 648_0_add_Return

The integer pair graph contains the following rules and edges:
(0): 583_0_ADD_FIELDACCESS(java.lang.Object(List(java.lang.Object(x0[0])))) → 583_0_ADD_FIELDACCESS(java.lang.Object(x0[0]))

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

The set Q consists of the following terms:
608_1_add_InvokeMethod(648_0_add_Return)

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

583_0_ADD_FIELDACCESS(java.lang.Object(List(java.lang.Object(x0[0])))) → 583_0_ADD_FIELDACCESS(java.lang.Object(x0[0]))

The TRS R consists of the following rules:

608_1_add_InvokeMethod(648_0_add_Return) → 648_0_add_Return

The set Q consists of the following terms:

608_1_add_InvokeMethod(648_0_add_Return)

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:

583_0_ADD_FIELDACCESS(java.lang.Object(List(java.lang.Object(x0[0])))) → 583_0_ADD_FIELDACCESS(java.lang.Object(x0[0]))

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

608_1_add_InvokeMethod(648_0_add_Return)

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].

608_1_add_InvokeMethod(648_0_add_Return)

(13) Obligation:

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

583_0_ADD_FIELDACCESS(java.lang.Object(List(java.lang.Object(x0[0])))) → 583_0_ADD_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:

583_0_ADD_FIELDACCESS(java.lang.Object(List(java.lang.Object(x0[0])))) → 583_0_ADD_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: AProVERec01.rec(ILList;)V
SCC calls the following helper methods: AProVERec01.rec(ILList;)V, List.add(I)V
Performed SCC analyses: UsedFieldsAnalysis

(17) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 15 rules for P and 80 rules for R.

P rules:
286_0_rec_Load(EOS(STATIC_286), i38, java.lang.Object(List(EOC)), matching1) → 289_0_rec_IntArithmetic(EOS(STATIC_289), java.lang.Object(List(EOC)), 3, i38) | =(matching1, 3)
289_0_rec_IntArithmetic(EOS(STATIC_289), java.lang.Object(List(EOC)), matching1, i38) → 297_0_rec_Store(EOS(STATIC_297), java.lang.Object(List(EOC)), *(3, i38)) | =(matching1, 3)
297_0_rec_Store(EOS(STATIC_297), java.lang.Object(List(EOC)), i42) → 304_0_rec_Load(EOS(STATIC_304), java.lang.Object(List(EOC)), i42)
304_0_rec_Load(EOS(STATIC_304), java.lang.Object(List(EOC)), i42) → 312_0_rec_ConstantStackPush(EOS(STATIC_312), java.lang.Object(List(EOC)), i42, i42)
312_0_rec_ConstantStackPush(EOS(STATIC_312), java.lang.Object(List(EOC)), i42, i42) → 325_0_rec_GE(EOS(STATIC_325), java.lang.Object(List(EOC)), i42, i42, 100000)
325_0_rec_GE(EOS(STATIC_325), java.lang.Object(List(EOC)), i48, i48, matching1) → 336_0_rec_GE(EOS(STATIC_336), java.lang.Object(List(EOC)), i48, i48, 100000) | =(matching1, 100000)
336_0_rec_GE(EOS(STATIC_336), java.lang.Object(List(EOC)), i48, i48, matching1) → 346_0_rec_Load(EOS(STATIC_346), java.lang.Object(List(EOC)), i48) | &&(<(i48, 100000), =(matching1, 100000))
346_0_rec_Load(EOS(STATIC_346), java.lang.Object(List(EOC)), i48) → 357_0_rec_ConstantStackPush(EOS(STATIC_357), java.lang.Object(List(EOC)), i48, i48)
357_0_rec_ConstantStackPush(EOS(STATIC_357), java.lang.Object(List(EOC)), i48, i48) → 367_0_rec_IntArithmetic(EOS(STATIC_367), java.lang.Object(List(EOC)), i48, i48, 1)
367_0_rec_IntArithmetic(EOS(STATIC_367), java.lang.Object(List(EOC)), i48, i48, matching1) → 377_0_rec_Load(EOS(STATIC_377), java.lang.Object(List(EOC)), i48, +(i48, 1)) | &&(>=(i48, 0), =(matching1, 1))
377_0_rec_Load(EOS(STATIC_377), java.lang.Object(List(EOC)), i48, i54) → 386_0_rec_InvokeMethod(EOS(STATIC_386), java.lang.Object(List(EOC)), i48, i54, java.lang.Object(List(EOC)))
386_0_rec_InvokeMethod(EOS(STATIC_386), java.lang.Object(List(EOC)), i48, i54, java.lang.Object(List(EOC))) → 395_1_rec_InvokeMethod(395_0_rec_ConstantStackPush(EOS(STATIC_395), i54, java.lang.Object(List(EOC))), java.lang.Object(List(EOC)), i48, i54, java.lang.Object(List(EOC)))
395_0_rec_ConstantStackPush(EOS(STATIC_395), i54, java.lang.Object(List(EOC))) → 406_0_rec_ConstantStackPush(EOS(STATIC_406), i54, java.lang.Object(List(EOC)))
406_0_rec_ConstantStackPush(EOS(STATIC_406), i54, java.lang.Object(List(EOC))) → 282_0_rec_ConstantStackPush(EOS(STATIC_282), i54, java.lang.Object(List(EOC)))
282_0_rec_ConstantStackPush(EOS(STATIC_282), i38, java.lang.Object(List(EOC))) → 286_0_rec_Load(EOS(STATIC_286), i38, java.lang.Object(List(EOC)), 3)
R rules:
422_0_add_Load(EOS(STATIC_422), java.lang.Object(List(EOC))) → 580_0_add_Load(EOS(STATIC_580), java.lang.Object(List(EOC)), i55)
836_0_add_Load(EOS(STATIC_836), java.lang.Object(List(EOC))) → 580_0_add_Load(EOS(STATIC_580), java.lang.Object(List(EOC)), i181)
611_0_add_Load(EOS(STATIC_611), java.lang.Object(o78sub), i76) → 580_0_add_Load(EOS(STATIC_580), java.lang.Object(o78sub), i76)
325_0_rec_GE(EOS(STATIC_325), java.lang.Object(List(EOC)), i49, i49, matching1) → 337_0_rec_GE(EOS(STATIC_337), java.lang.Object(List(EOC)), i49, i49, 100000) | =(matching1, 100000)
337_0_rec_GE(EOS(STATIC_337), java.lang.Object(List(EOC)), i49, i49, matching1) → 348_0_rec_Load(EOS(STATIC_348), java.lang.Object(List(EOC)), i49) | &&(>=(i49, 100000), =(matching1, 100000))
348_0_rec_Load(EOS(STATIC_348), java.lang.Object(List(EOC)), i49) → 359_0_rec_ConstantStackPush(EOS(STATIC_359), java.lang.Object(List(EOC)), i49)
359_0_rec_ConstantStackPush(EOS(STATIC_359), java.lang.Object(List(EOC)), i49) → 369_0_rec_IntArithmetic(EOS(STATIC_369), java.lang.Object(List(EOC)), i49)
369_0_rec_IntArithmetic(EOS(STATIC_369), java.lang.Object(List(EOC)), i49) → 379_0_rec_Store(EOS(STATIC_379), java.lang.Object(List(EOC))) | >(i49, 1)
379_0_rec_Store(EOS(STATIC_379), java.lang.Object(List(EOC))) → 388_0_rec_Load(EOS(STATIC_388), java.lang.Object(List(EOC)))
388_0_rec_Load(EOS(STATIC_388), java.lang.Object(List(EOC))) → 397_0_rec_Load(EOS(STATIC_397), java.lang.Object(List(EOC)))
395_1_rec_InvokeMethod(749_0_rec_Return(EOS(STATIC_749)), java.lang.Object(List(EOC)), i48, i152, java.lang.Object(List(EOC))) → 800_0_rec_Return(EOS(STATIC_800), java.lang.Object(List(EOC)), i48, i152, java.lang.Object(List(EOC)))
395_1_rec_InvokeMethod(862_0_rec_Return(EOS(STATIC_862)), java.lang.Object(List(EOC)), i48, i198, java.lang.Object(List(EOC))) → 878_0_rec_Return(EOS(STATIC_878), java.lang.Object(List(EOC)), i48, i198, java.lang.Object(List(EOC)))
397_0_rec_Load(EOS(STATIC_397), java.lang.Object(List(EOC))) → 408_0_rec_InvokeMethod(EOS(STATIC_408), java.lang.Object(List(EOC)))
408_0_rec_InvokeMethod(EOS(STATIC_408), java.lang.Object(List(EOC))) → 414_1_rec_InvokeMethod(414_0_add_Load(EOS(STATIC_414), java.lang.Object(List(EOC))), java.lang.Object(List(EOC)))
414_0_add_Load(EOS(STATIC_414), java.lang.Object(List(EOC))) → 422_0_add_Load(EOS(STATIC_422), java.lang.Object(List(EOC)))
414_1_rec_InvokeMethod(648_0_add_Return(EOS(STATIC_648)), java.lang.Object(List(EOC))) → 665_0_add_Return(EOS(STATIC_665), java.lang.Object(List(EOC)))
414_1_rec_InvokeMethod(752_0_add_Return(EOS(STATIC_752)), java.lang.Object(List(EOC))) → 807_0_add_Return(EOS(STATIC_807), java.lang.Object(List(EOC)))
665_0_add_Return(EOS(STATIC_665), java.lang.Object(List(EOC))) → 666_0_add_Return(EOS(STATIC_666), java.lang.Object(List(EOC)))
666_0_add_Return(EOS(STATIC_666), java.lang.Object(List(EOC))) → 731_0_add_Return(EOS(STATIC_731), java.lang.Object(List(EOC)))
705_0_rec_Return(EOS(STATIC_705), java.lang.Object(List(EOC)), i48, i115, java.lang.Object(List(EOC))) → 722_0_rec_Return(EOS(STATIC_722), java.lang.Object(List(EOC)), i48, i115, java.lang.Object(List(EOC)))
722_0_rec_Return(EOS(STATIC_722), java.lang.Object(List(EOC)), i48, i127, java.lang.Object(List(EOC))) → 801_0_rec_Return(EOS(STATIC_801), java.lang.Object(List(EOC)), i48, i127, java.lang.Object(List(EOC)))
731_0_add_Return(EOS(STATIC_731), java.lang.Object(List(EOC))) → 749_0_rec_Return(EOS(STATIC_749))
749_0_rec_Return(EOS(STATIC_749)) → 862_0_rec_Return(EOS(STATIC_862))
800_0_rec_Return(EOS(STATIC_800), java.lang.Object(List(EOC)), i48, i152, java.lang.Object(List(EOC))) → 801_0_rec_Return(EOS(STATIC_801), java.lang.Object(List(EOC)), i48, i152, java.lang.Object(List(EOC)))
801_0_rec_Return(EOS(STATIC_801), java.lang.Object(List(EOC)), i48, i166, java.lang.Object(List(EOC))) → 818_0_rec_Load(EOS(STATIC_818), java.lang.Object(List(EOC)), i48)
807_0_add_Return(EOS(STATIC_807), java.lang.Object(List(EOC))) → 731_0_add_Return(EOS(STATIC_731), java.lang.Object(List(EOC)))
818_0_rec_Load(EOS(STATIC_818), java.lang.Object(List(EOC)), i48) → 821_0_rec_ConstantStackPush(EOS(STATIC_821), java.lang.Object(List(EOC)), i48)
821_0_rec_ConstantStackPush(EOS(STATIC_821), java.lang.Object(List(EOC)), i48) → 823_0_rec_IntArithmetic(EOS(STATIC_823), java.lang.Object(List(EOC)), i48)
823_0_rec_IntArithmetic(EOS(STATIC_823), java.lang.Object(List(EOC)), i48) → 826_0_rec_Store(EOS(STATIC_826), java.lang.Object(List(EOC)))
826_0_rec_Store(EOS(STATIC_826), java.lang.Object(List(EOC))) → 828_0_rec_Load(EOS(STATIC_828), java.lang.Object(List(EOC)))
828_0_rec_Load(EOS(STATIC_828), java.lang.Object(List(EOC))) → 830_0_rec_Load(EOS(STATIC_830), java.lang.Object(List(EOC)))
830_0_rec_Load(EOS(STATIC_830), java.lang.Object(List(EOC))) → 832_0_rec_InvokeMethod(EOS(STATIC_832), java.lang.Object(List(EOC)))
832_0_rec_InvokeMethod(EOS(STATIC_832), java.lang.Object(List(EOC))) → 834_1_rec_InvokeMethod(834_0_add_Load(EOS(STATIC_834), java.lang.Object(List(EOC))), java.lang.Object(List(EOC)))
834_0_add_Load(EOS(STATIC_834), java.lang.Object(List(EOC))) → 836_0_add_Load(EOS(STATIC_836), java.lang.Object(List(EOC)))
834_1_rec_InvokeMethod(648_0_add_Return(EOS(STATIC_648)), java.lang.Object(List(EOC))) → 846_0_add_Return(EOS(STATIC_846), java.lang.Object(List(EOC)))
834_1_rec_InvokeMethod(752_0_add_Return(EOS(STATIC_752)), java.lang.Object(List(EOC))) → 854_0_add_Return(EOS(STATIC_854), java.lang.Object(List(EOC)))
846_0_add_Return(EOS(STATIC_846), java.lang.Object(List(EOC))) → 855_0_add_Return(EOS(STATIC_855), java.lang.Object(List(EOC)))
854_0_add_Return(EOS(STATIC_854), java.lang.Object(List(EOC))) → 855_0_add_Return(EOS(STATIC_855), java.lang.Object(List(EOC)))
855_0_add_Return(EOS(STATIC_855), java.lang.Object(List(EOC))) → 862_0_rec_Return(EOS(STATIC_862))
878_0_rec_Return(EOS(STATIC_878), java.lang.Object(List(EOC)), i48, i198, java.lang.Object(List(EOC))) → 801_0_rec_Return(EOS(STATIC_801), java.lang.Object(List(EOC)), i48, i198, java.lang.Object(List(EOC)))
580_0_add_Load(EOS(STATIC_580), java.lang.Object(o70sub), i76) → 583_0_add_FieldAccess(EOS(STATIC_583), java.lang.Object(o70sub), i76, java.lang.Object(o70sub))
583_0_add_FieldAccess(EOS(STATIC_583), java.lang.Object(List(EOC)), i76, java.lang.Object(List(EOC))) → 584_0_add_FieldAccess(EOS(STATIC_584), java.lang.Object(List(EOC)), i76, java.lang.Object(List(EOC)))
584_0_add_FieldAccess(EOS(STATIC_584), java.lang.Object(List(EOC)), i76, java.lang.Object(List(EOC))) → 587_0_add_NONNULL(EOS(STATIC_587), java.lang.Object(List(EOC)), i76, o75)
587_0_add_NONNULL(EOS(STATIC_587), java.lang.Object(List(EOC)), i76, java.lang.Object(o78sub)) → 590_0_add_NONNULL(EOS(STATIC_590), java.lang.Object(List(EOC)), i76, java.lang.Object(o78sub))
587_0_add_NONNULL(EOS(STATIC_587), java.lang.Object(List(EOC)), i76, NULL) → 591_0_add_NONNULL(EOS(STATIC_591), java.lang.Object(List(EOC)), i76, NULL)
590_0_add_NONNULL(EOS(STATIC_590), java.lang.Object(List(EOC)), i76, java.lang.Object(o78sub)) → 593_0_add_Load(EOS(STATIC_593), java.lang.Object(List(EOC)), i76)
591_0_add_NONNULL(EOS(STATIC_591), java.lang.Object(List(EOC)), i76, NULL) → 595_0_add_Load(EOS(STATIC_595), java.lang.Object(List(EOC)), i76)
593_0_add_Load(EOS(STATIC_593), java.lang.Object(List(EOC)), i76) → 596_0_add_FieldAccess(EOS(STATIC_596), i76, java.lang.Object(List(EOC)))
595_0_add_Load(EOS(STATIC_595), java.lang.Object(List(EOC)), i76) → 598_0_add_New(EOS(STATIC_598), i76, java.lang.Object(List(EOC)))
596_0_add_FieldAccess(EOS(STATIC_596), i76, java.lang.Object(List(EOC))) → 601_0_add_Load(EOS(STATIC_601), i76, java.lang.Object(o78sub))
598_0_add_New(EOS(STATIC_598), i76, java.lang.Object(List(EOC))) → 602_0_add_Duplicate(EOS(STATIC_602), i76, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
601_0_add_Load(EOS(STATIC_601), i76, java.lang.Object(o78sub)) → 604_0_add_InvokeMethod(EOS(STATIC_604), java.lang.Object(o78sub), i76)
602_0_add_Duplicate(EOS(STATIC_602), i76, java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 606_0_add_Load(EOS(STATIC_606), i76, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
604_0_add_InvokeMethod(EOS(STATIC_604), java.lang.Object(o78sub), i76) → 608_1_add_InvokeMethod(608_0_add_Load(EOS(STATIC_608), java.lang.Object(o78sub), i76), java.lang.Object(o78sub), i76)
606_0_add_Load(EOS(STATIC_606), i76, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 610_0_add_ConstantStackPush(EOS(STATIC_610), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76)
608_0_add_Load(EOS(STATIC_608), java.lang.Object(o78sub), i76) → 611_0_add_Load(EOS(STATIC_611), java.lang.Object(o78sub), i76)
608_1_add_InvokeMethod(648_0_add_Return(EOS(STATIC_648)), java.lang.Object(o78sub), i89) → 670_0_add_Return(EOS(STATIC_670), java.lang.Object(List(EOC)), i89)
608_1_add_InvokeMethod(752_0_add_Return(EOS(STATIC_752)), java.lang.Object(o78sub), i156) → 814_0_add_Return(EOS(STATIC_814), java.lang.Object(List(EOC)), i156)
610_0_add_ConstantStackPush(EOS(STATIC_610), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76) → 613_0_add_InvokeMethod(EOS(STATIC_613), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL)
613_0_add_InvokeMethod(EOS(STATIC_613), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL) → 615_0_<init>_Load(EOS(STATIC_615), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), i76, NULL)
615_0_<init>_Load(EOS(STATIC_615), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), i76, NULL) → 620_0_<init>_InvokeMethod(EOS(STATIC_620), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)))
620_0_<init>_InvokeMethod(EOS(STATIC_620), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC))) → 622_0_<init>_Load(EOS(STATIC_622), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), i76, NULL)
622_0_<init>_Load(EOS(STATIC_622), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), i76, NULL) → 623_0_<init>_ConstantStackPush(EOS(STATIC_623), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)))
623_0_<init>_ConstantStackPush(EOS(STATIC_623), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC))) → 625_0_<init>_FieldAccess(EOS(STATIC_625), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), 0)
625_0_<init>_FieldAccess(EOS(STATIC_625), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), matching1) → 627_0_<init>_Load(EOS(STATIC_627), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), i76, NULL) | =(matching1, 0)
627_0_<init>_Load(EOS(STATIC_627), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), i76, NULL) → 629_0_<init>_ConstantStackPush(EOS(STATIC_629), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)))
629_0_<init>_ConstantStackPush(EOS(STATIC_629), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC))) → 630_0_<init>_FieldAccess(EOS(STATIC_630), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), NULL)
630_0_<init>_FieldAccess(EOS(STATIC_630), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), NULL) → 632_0_<init>_Load(EOS(STATIC_632), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), i76, NULL)
632_0_<init>_Load(EOS(STATIC_632), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), i76, NULL) → 634_0_<init>_Load(EOS(STATIC_634), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)))
634_0_<init>_Load(EOS(STATIC_634), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC))) → 635_0_<init>_FieldAccess(EOS(STATIC_635), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), NULL, java.lang.Object(List(EOC)), i76)
635_0_<init>_FieldAccess(EOS(STATIC_635), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), NULL, java.lang.Object(List(EOC)), i76) → 637_0_<init>_Load(EOS(STATIC_637), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), NULL)
637_0_<init>_Load(EOS(STATIC_637), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), NULL) → 639_0_<init>_Load(EOS(STATIC_639), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, NULL, java.lang.Object(List(EOC)))
639_0_<init>_Load(EOS(STATIC_639), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, NULL, java.lang.Object(List(EOC))) → 641_0_<init>_FieldAccess(EOS(STATIC_641), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), NULL)
641_0_<init>_FieldAccess(EOS(STATIC_641), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), NULL) → 642_0_<init>_Return(EOS(STATIC_642), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL)
642_0_<init>_Return(EOS(STATIC_642), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL) → 644_0_add_FieldAccess(EOS(STATIC_644), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
644_0_add_FieldAccess(EOS(STATIC_644), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 646_0_add_JMP(EOS(STATIC_646))
646_0_add_JMP(EOS(STATIC_646)) → 648_0_add_Return(EOS(STATIC_648))
670_0_add_Return(EOS(STATIC_670), java.lang.Object(List(EOC)), i89) → 740_0_add_Return(EOS(STATIC_740), java.lang.Object(List(EOC)), i89)
740_0_add_Return(EOS(STATIC_740), java.lang.Object(List(EOC)), i143) → 752_0_add_Return(EOS(STATIC_752))
814_0_add_Return(EOS(STATIC_814), java.lang.Object(List(EOC)), i156) → 740_0_add_Return(EOS(STATIC_740), java.lang.Object(List(EOC)), i156)

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

P rules:
286_0_rec_Load(EOS(STATIC_286), x0, java.lang.Object(List(EOC)), 3) → 395_1_rec_InvokeMethod(286_0_rec_Load(EOS(STATIC_286), +(*(3, x0), 1), java.lang.Object(List(EOC)), 3), java.lang.Object(List(EOC)), *(3, x0), +(*(3, x0), 1), java.lang.Object(List(EOC))) | &&(>(100000, *(3, x0)), <=(0, *(3, x0)))
R rules:
395_1_rec_InvokeMethod(749_0_rec_Return(EOS(STATIC_749)), java.lang.Object(List(EOC)), x0, x1, java.lang.Object(List(EOC))) → 834_1_rec_InvokeMethod(587_0_add_NONNULL(EOS(STATIC_587), java.lang.Object(List(EOC)), x2, x3), java.lang.Object(List(EOC)))
395_1_rec_InvokeMethod(862_0_rec_Return(EOS(STATIC_862)), java.lang.Object(List(EOC)), x0, x1, java.lang.Object(List(EOC))) → 834_1_rec_InvokeMethod(587_0_add_NONNULL(EOS(STATIC_587), java.lang.Object(List(EOC)), x2, x3), java.lang.Object(List(EOC)))
587_0_add_NONNULL(EOS(STATIC_587), java.lang.Object(List(EOC)), x0, java.lang.Object(x1)) → 608_1_add_InvokeMethod(587_0_add_NONNULL(EOS(STATIC_587), java.lang.Object(List(EOC)), x0, x2), java.lang.Object(List(EOC)), x0)
587_0_add_NONNULL(EOS(STATIC_587), java.lang.Object(List(EOC)), x0, NULL) → 648_0_add_Return(EOS(STATIC_648))
608_1_add_InvokeMethod(648_0_add_Return(EOS(STATIC_648)), java.lang.Object(x0), x1) → 752_0_add_Return(EOS(STATIC_752))
608_1_add_InvokeMethod(752_0_add_Return(EOS(STATIC_752)), java.lang.Object(x0), x1) → 752_0_add_Return(EOS(STATIC_752))
834_1_rec_InvokeMethod(648_0_add_Return(EOS(STATIC_648)), java.lang.Object(List(EOC))) → 862_0_rec_Return(EOS(STATIC_862))
834_1_rec_InvokeMethod(752_0_add_Return(EOS(STATIC_752)), java.lang.Object(List(EOC))) → 862_0_rec_Return(EOS(STATIC_862))

Filtered ground terms:

395_1_rec_InvokeMethod(x1, x2, x3, x4, x5) → 395_1_rec_InvokeMethod(x1, x3, x4)
List(x1) → List
286_0_rec_Load(x1, x2, x3, x4) → 286_0_rec_Load(x2)
Cond_286_0_rec_Load(x1, x2, x3, x4, x5) → Cond_286_0_rec_Load(x1, x3)
862_0_rec_Return(x1) → 862_0_rec_Return
834_1_rec_InvokeMethod(x1, x2) → 834_1_rec_InvokeMethod(x1)
752_0_add_Return(x1) → 752_0_add_Return
648_0_add_Return(x1) → 648_0_add_Return
587_0_add_NONNULL(x1, x2, x3, x4) → 587_0_add_NONNULL(x3, x4)
749_0_rec_Return(x1) → 749_0_rec_Return

Filtered unneeded arguments:

395_1_rec_InvokeMethod(x1, x2, x3) → 395_1_rec_InvokeMethod(x1)
587_0_add_NONNULL(x1, x2) → 587_0_add_NONNULL(x2)
608_1_add_InvokeMethod(x1, x2, x3) → 608_1_add_InvokeMethod(x1, x2)

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

P rules:
286_0_rec_Load(x0) → 395_1_rec_InvokeMethod(286_0_rec_Load(+(*(3, x0), 1))) | &&(>(100000, *(3, x0)), <=(0, *(3, x0)))
R rules:
395_1_rec_InvokeMethod(749_0_rec_Return) → 834_1_rec_InvokeMethod(587_0_add_NONNULL(x3))
395_1_rec_InvokeMethod(862_0_rec_Return) → 834_1_rec_InvokeMethod(587_0_add_NONNULL(x3))
587_0_add_NONNULL(java.lang.Object(x1)) → 608_1_add_InvokeMethod(587_0_add_NONNULL(x2), java.lang.Object(List))
587_0_add_NONNULL(NULL) → 648_0_add_Return
608_1_add_InvokeMethod(648_0_add_Return, java.lang.Object(x0)) → 752_0_add_Return
608_1_add_InvokeMethod(752_0_add_Return, java.lang.Object(x0)) → 752_0_add_Return
834_1_rec_InvokeMethod(648_0_add_Return) → 862_0_rec_Return
834_1_rec_InvokeMethod(752_0_add_Return) → 862_0_rec_Return

Performed bisimulation on rules. Used the following equivalence classes: {[749_0_rec_Return, 862_0_rec_Return, List, 648_0_add_Return, 752_0_add_Return]=749_0_rec_Return}

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

P rules:
286_0_REC_LOAD(x0) → COND_286_0_REC_LOAD(&&(>(100000, *(3, x0)), <=(0, *(3, x0))), x0)
COND_286_0_REC_LOAD(TRUE, x0) → 286_0_REC_LOAD(+(*(3, x0), 1))
R rules:
395_1_rec_InvokeMethod(749_0_rec_Return) → 834_1_rec_InvokeMethod(587_0_add_NONNULL(x3))
587_0_add_NONNULL(java.lang.Object(x1)) → 608_1_add_InvokeMethod(587_0_add_NONNULL(x2), java.lang.Object(749_0_rec_Return))
587_0_add_NONNULL(NULL) → 749_0_rec_Return
608_1_add_InvokeMethod(749_0_rec_Return, java.lang.Object(x0)) → 749_0_rec_Return
834_1_rec_InvokeMethod(749_0_rec_Return) → 749_0_rec_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:

Boolean, Integer

The ITRS R consists of the following rules:
395_1_rec_InvokeMethod(749_0_rec_Return) → 834_1_rec_InvokeMethod(587_0_add_NONNULL(x3))
587_0_add_NONNULL(java.lang.Object(x1)) → 608_1_add_InvokeMethod(587_0_add_NONNULL(x2), java.lang.Object(749_0_rec_Return))
587_0_add_NONNULL(NULL) → 749_0_rec_Return
608_1_add_InvokeMethod(749_0_rec_Return, java.lang.Object(x0)) → 749_0_rec_Return
834_1_rec_InvokeMethod(749_0_rec_Return) → 749_0_rec_Return

The integer pair graph contains the following rules and edges:
(0): 286_0_REC_LOAD(x0[0]) → COND_286_0_REC_LOAD(100000 > 3 * x0[0] && 0 <= 3 * x0[0], x0[0])
(1): COND_286_0_REC_LOAD(TRUE, x0[1]) → 286_0_REC_LOAD(3 * x0[1] + 1)

(0) -> (1), if (100000 > 3 * x0[0] && 0 <= 3 * x0[0] ∧x0[0] →^* x0[1])

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

The set Q consists of the following terms:
395_1_rec_InvokeMethod(749_0_rec_Return)
587_0_add_NONNULL(java.lang.Object(x0))
587_0_add_NONNULL(NULL)
608_1_add_InvokeMethod(749_0_rec_Return, java.lang.Object(x0))
834_1_rec_InvokeMethod(749_0_rec_Return)

(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.IdpDefaultShapeHeuristic@224a9dcd Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 1 Max Right Steps: 1

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 286_0_REC_LOAD(x0) → COND_286_0_REC_LOAD(&&(>(100000, *(3, x0)), <=(0, *(3, x0))), x0) the following chains were created:

We consider the chain 286_0_REC_LOAD(x0[0]) → COND_286_0_REC_LOAD(&&(>(100000, *(3, x0[0])), <=(0, *(3, x0[0]))), x0[0]), COND_286_0_REC_LOAD(TRUE, x0[1]) → 286_0_REC_LOAD(+(*(3, x0[1]), 1)) which results in the following constraint:
(1)    (&&(>(100000, *(3, x0[0])), <=(0, *(3, x0[0])))=TRUE∧x0[0]=x0[1] ⇒ 286_0_REC_LOAD(x0[0])≥NonInfC∧286_0_REC_LOAD(x0[0])≥COND_286_0_REC_LOAD(&&(>(100000, *(3, x0[0])), <=(0, *(3, x0[0]))), x0[0])∧(U^Increasing(COND_286_0_REC_LOAD(&&(>(100000, *(3, x0[0])), <=(0, *(3, x0[0]))), x0[0])), ≥))

We simplified constraint (1) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
(2)    (>(100000, *(3, x0[0]))=TRUE∧<=(0, *(3, x0[0]))=TRUE ⇒ 286_0_REC_LOAD(x0[0])≥NonInfC∧286_0_REC_LOAD(x0[0])≥COND_286_0_REC_LOAD(&&(>(100000, *(3, x0[0])), <=(0, *(3, x0[0]))), x0[0])∧(U^Increasing(COND_286_0_REC_LOAD(&&(>(100000, *(3, x0[0])), <=(0, *(3, x0[0]))), x0[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    ([99999] + [-3]x0[0] ≥ 0∧[3]x0[0] ≥ 0 ⇒ (U^Increasing(COND_286_0_REC_LOAD(&&(>(100000, *(3, x0[0])), <=(0, *(3, x0[0]))), x0[0])), ≥)∧[(-1)Bound*bni_24] + [(-1)bni_24]x0[0] ≥ 0∧[(-1)bso_25] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    ([99999] + [-3]x0[0] ≥ 0∧[3]x0[0] ≥ 0 ⇒ (U^Increasing(COND_286_0_REC_LOAD(&&(>(100000, *(3, x0[0])), <=(0, *(3, x0[0]))), x0[0])), ≥)∧[(-1)Bound*bni_24] + [(-1)bni_24]x0[0] ≥ 0∧[(-1)bso_25] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    ([99999] + [-3]x0[0] ≥ 0∧[3]x0[0] ≥ 0 ⇒ (U^Increasing(COND_286_0_REC_LOAD(&&(>(100000, *(3, x0[0])), <=(0, *(3, x0[0]))), x0[0])), ≥)∧[(-1)Bound*bni_24] + [(-1)bni_24]x0[0] ≥ 0∧[(-1)bso_25] ≥ 0)

We simplified constraint (5) using rule (IDP_POLY_GCD) which results in the following new constraint:
(6)    ([33333] + [-1]x0[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(COND_286_0_REC_LOAD(&&(>(100000, *(3, x0[0])), <=(0, *(3, x0[0]))), x0[0])), ≥)∧[(-1)Bound*bni_24] + [(-1)bni_24]x0[0] ≥ 0∧[(-1)bso_25] ≥ 0)

For Pair COND_286_0_REC_LOAD(TRUE, x0) → 286_0_REC_LOAD(+(*(3, x0), 1)) the following chains were created:

We consider the chain 286_0_REC_LOAD(x0[0]) → COND_286_0_REC_LOAD(&&(>(100000, *(3, x0[0])), <=(0, *(3, x0[0]))), x0[0]), COND_286_0_REC_LOAD(TRUE, x0[1]) → 286_0_REC_LOAD(+(*(3, x0[1]), 1)), 286_0_REC_LOAD(x0[0]) → COND_286_0_REC_LOAD(&&(>(100000, *(3, x0[0])), <=(0, *(3, x0[0]))), x0[0]) which results in the following constraint:
(7)    (&&(>(100000, *(3, x0[0])), <=(0, *(3, x0[0])))=TRUE∧x0[0]=x0[1]∧+(*(3, x0[1]), 1)=x0[0]1 ⇒ COND_286_0_REC_LOAD(TRUE, x0[1])≥NonInfC∧COND_286_0_REC_LOAD(TRUE, x0[1])≥286_0_REC_LOAD(+(*(3, x0[1]), 1))∧(U^Increasing(286_0_REC_LOAD(+(*(3, x0[1]), 1))), ≥))

We simplified constraint (7) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(8)    (>(100000, *(3, x0[0]))=TRUE∧<=(0, *(3, x0[0]))=TRUE ⇒ COND_286_0_REC_LOAD(TRUE, x0[0])≥NonInfC∧COND_286_0_REC_LOAD(TRUE, x0[0])≥286_0_REC_LOAD(+(*(3, x0[0]), 1))∧(U^Increasing(286_0_REC_LOAD(+(*(3, x0[1]), 1))), ≥))

We simplified constraint (8) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(9)    ([99999] + [-3]x0[0] ≥ 0∧[3]x0[0] ≥ 0 ⇒ (U^Increasing(286_0_REC_LOAD(+(*(3, x0[1]), 1))), ≥)∧[(-1)Bound*bni_26] + [(-1)bni_26]x0[0] ≥ 0∧[1 + (-1)bso_27] + [2]x0[0] ≥ 0)

We simplified constraint (9) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(10)    ([99999] + [-3]x0[0] ≥ 0∧[3]x0[0] ≥ 0 ⇒ (U^Increasing(286_0_REC_LOAD(+(*(3, x0[1]), 1))), ≥)∧[(-1)Bound*bni_26] + [(-1)bni_26]x0[0] ≥ 0∧[1 + (-1)bso_27] + [2]x0[0] ≥ 0)

We simplified constraint (10) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(11)    ([99999] + [-3]x0[0] ≥ 0∧[3]x0[0] ≥ 0 ⇒ (U^Increasing(286_0_REC_LOAD(+(*(3, x0[1]), 1))), ≥)∧[(-1)Bound*bni_26] + [(-1)bni_26]x0[0] ≥ 0∧[1 + (-1)bso_27] + [2]x0[0] ≥ 0)

We simplified constraint (11) using rule (IDP_POLY_GCD) which results in the following new constraint:
(12)    ([33333] + [-1]x0[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(286_0_REC_LOAD(+(*(3, x0[1]), 1))), ≥)∧[(-1)Bound*bni_26] + [(-1)bni_26]x0[0] ≥ 0∧[1 + (-1)bso_27] + [2]x0[0] ≥ 0)

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

286_0_REC_LOAD(x0) → COND_286_0_REC_LOAD(&&(>(100000, *(3, x0)), <=(0, *(3, x0))), x0)
- ([33333] + [-1]x0[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(COND_286_0_REC_LOAD(&&(>(100000, *(3, x0[0])), <=(0, *(3, x0[0]))), x0[0])), ≥)∧[(-1)Bound*bni_24] + [(-1)bni_24]x0[0] ≥ 0∧[(-1)bso_25] ≥ 0)
COND_286_0_REC_LOAD(TRUE, x0) → 286_0_REC_LOAD(+(*(3, x0), 1))
- ([33333] + [-1]x0[0] ≥ 0∧x0[0] ≥ 0 ⇒ (U^Increasing(286_0_REC_LOAD(+(*(3, x0[1]), 1))), ≥)∧[(-1)Bound*bni_26] + [(-1)bni_26]x0[0] ≥ 0∧[1 + (-1)bso_27] + [2]x0[0] ≥ 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(395_1_rec_InvokeMethod(x₁)) = [-1] + [-1]x₁
POL(749_0_rec_Return) = [-1]
POL(834_1_rec_InvokeMethod(x₁)) = [-1] + [-1]x₁
POL(587_0_add_NONNULL(x₁)) = [-1] + [-1]x₁
POL(java.lang.Object(x₁)) = [-1] + [-1]x₁
POL(608_1_add_InvokeMethod(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁
POL(NULL) = [-1]
POL(286_0_REC_LOAD(x₁)) = [-1]x₁
POL(COND_286_0_REC_LOAD(x₁, x₂)) = [-1]x₂ + x₁
POL(&&(x₁, x₂)) = 0
POL(>(x₁, x₂)) = [-1]
POL(100000) = [100000]
POL(*(x₁, x₂)) = x₁·x₂
POL(3) = [3]
POL(<=(x₁, x₂)) = [-1]
POL(0) = 0
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]

The following pairs are in P_>:

COND_286_0_REC_LOAD(TRUE, x0[1]) → 286_0_REC_LOAD(+(*(3, x0[1]), 1))

The following pairs are in P_bound:

286_0_REC_LOAD(x0[0]) → COND_286_0_REC_LOAD(&&(>(100000, *(3, x0[0])), <=(0, *(3, x0[0]))), x0[0])
COND_286_0_REC_LOAD(TRUE, x0[1]) → 286_0_REC_LOAD(+(*(3, x0[1]), 1))

The following pairs are in P_≥:

286_0_REC_LOAD(x0[0]) → COND_286_0_REC_LOAD(&&(>(100000, *(3, x0[0])), <=(0, *(3, x0[0]))), x0[0])

At least the following rules have been oriented under context sensitive arithmetic replacement:

&&(TRUE, TRUE)¹ → TRUE¹
&&(TRUE, FALSE)¹ → FALSE¹
&&(FALSE, TRUE)¹ ↔ FALSE¹
&&(FALSE, FALSE)¹ ↔ FALSE¹

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

Boolean, Integer

The ITRS R consists of the following rules:
395_1_rec_InvokeMethod(749_0_rec_Return) → 834_1_rec_InvokeMethod(587_0_add_NONNULL(x3))
587_0_add_NONNULL(java.lang.Object(x1)) → 608_1_add_InvokeMethod(587_0_add_NONNULL(x2), java.lang.Object(749_0_rec_Return))
587_0_add_NONNULL(NULL) → 749_0_rec_Return
608_1_add_InvokeMethod(749_0_rec_Return, java.lang.Object(x0)) → 749_0_rec_Return
834_1_rec_InvokeMethod(749_0_rec_Return) → 749_0_rec_Return

The integer pair graph contains the following rules and edges:
(0): 286_0_REC_LOAD(x0[0]) → COND_286_0_REC_LOAD(100000 > 3 * x0[0] && 0 <= 3 * x0[0], x0[0])

The set Q consists of the following terms:
395_1_rec_InvokeMethod(749_0_rec_Return)
587_0_add_NONNULL(java.lang.Object(x0))
587_0_add_NONNULL(NULL)
608_1_add_InvokeMethod(749_0_rec_Return, java.lang.Object(x0))
834_1_rec_InvokeMethod(749_0_rec_Return)

(21) 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) Obligation:

(21) IDependencyGraphProof (EQUIVALENT transformation)

(22) TRUE