Termination proof of /tmp/tmp4ymzNI/AProVERec01.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 230 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 350 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 (⇒, 730 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))) → 586_0_add_FieldAccess(EOS(STATIC_586), java.lang.Object(List(EOC, o75)), i76, java.lang.Object(List(EOC, o75)))
586_0_add_FieldAccess(EOS(STATIC_586), java.lang.Object(List(EOC, o75)), i76, java.lang.Object(List(EOC, o75))) → 588_0_add_NONNULL(EOS(STATIC_588), java.lang.Object(List(EOC, o75)), i76, o75)
588_0_add_NONNULL(EOS(STATIC_588), 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) → 597_0_add_FieldAccess(EOS(STATIC_597), i76, java.lang.Object(List(EOC, java.lang.Object(o78sub))))
597_0_add_FieldAccess(EOS(STATIC_597), 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)) → 605_0_add_InvokeMethod(EOS(STATIC_605), java.lang.Object(o78sub), i76)
605_0_add_InvokeMethod(EOS(STATIC_605), 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) → 612_0_add_Load(EOS(STATIC_612), java.lang.Object(o78sub), i76)
612_0_add_Load(EOS(STATIC_612), java.lang.Object(o78sub), i76) → 581_0_add_Load(EOS(STATIC_581), java.lang.Object(o78sub), i76)
581_0_add_Load(EOS(STATIC_581), java.lang.Object(o70sub), i76) → 583_0_add_FieldAccess(EOS(STATIC_583), java.lang.Object(o70sub), i76, java.lang.Object(o70sub))
R rules:
588_0_add_NONNULL(EOS(STATIC_588), 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) → 599_0_add_New(EOS(STATIC_599), i76, java.lang.Object(List(EOC, NULL)))
599_0_add_New(EOS(STATIC_599), i76, java.lang.Object(List(EOC, NULL))) → 603_0_add_Duplicate(EOS(STATIC_603), i76, java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)))
603_0_add_Duplicate(EOS(STATIC_603), 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(646_0_add_Return(EOS(STATIC_646)), java.lang.Object(o78sub), i89) → 667_0_add_Return(EOS(STATIC_667), java.lang.Object(List(EOC, java.lang.Object(List(EOC, NULL)))), i89)
608_1_add_InvokeMethod(770_0_add_Return(EOS(STATIC_770)), java.lang.Object(o78sub), i157) → 831_0_add_Return(EOS(STATIC_831), java.lang.Object(List(EOC, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o157)))))), i157)
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) → 614_0_add_InvokeMethod(EOS(STATIC_614), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL)
614_0_add_InvokeMethod(EOS(STATIC_614), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL) → 616_0_<init>_Load(EOS(STATIC_616), 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)
616_0_<init>_Load(EOS(STATIC_616), 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) → 619_0_<init>_InvokeMethod(EOS(STATIC_619), 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)))
619_0_<init>_InvokeMethod(EOS(STATIC_619), 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>_Load(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)
620_0_<init>_Load(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) → 622_0_<init>_ConstantStackPush(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, java.lang.Object(List(EOC, NULL)))
622_0_<init>_ConstantStackPush(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, java.lang.Object(List(EOC, NULL))) → 624_0_<init>_FieldAccess(EOS(STATIC_624), 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)
624_0_<init>_FieldAccess(EOS(STATIC_624), 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) → 625_0_<init>_Load(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) | =(matching1, 0)
625_0_<init>_Load(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) → 627_0_<init>_ConstantStackPush(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, java.lang.Object(List(EOC, NULL)))
627_0_<init>_ConstantStackPush(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, java.lang.Object(List(EOC, NULL))) → 629_0_<init>_FieldAccess(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)), NULL)
629_0_<init>_FieldAccess(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)), NULL) → 630_0_<init>_Load(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)
630_0_<init>_Load(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) → 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, java.lang.Object(List(EOC, 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, java.lang.Object(List(EOC, NULL))) → 634_0_<init>_FieldAccess(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)), NULL, java.lang.Object(List(EOC, NULL)), i76)
634_0_<init>_FieldAccess(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)), NULL, java.lang.Object(List(EOC, NULL)), i76) → 636_0_<init>_Load(EOS(STATIC_636), 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)
636_0_<init>_Load(EOS(STATIC_636), 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, NULL, java.lang.Object(List(EOC, 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, NULL, java.lang.Object(List(EOC, NULL))) → 639_0_<init>_FieldAccess(EOS(STATIC_639), 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>_FieldAccess(EOS(STATIC_639), 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>_Return(EOS(STATIC_641), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL)
641_0_<init>_Return(EOS(STATIC_641), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), i76, NULL) → 642_0_add_FieldAccess(EOS(STATIC_642), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)))
642_0_add_FieldAccess(EOS(STATIC_642), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL))) → 645_0_add_JMP(EOS(STATIC_645))
645_0_add_JMP(EOS(STATIC_645)) → 646_0_add_Return(EOS(STATIC_646))
667_0_add_Return(EOS(STATIC_667), java.lang.Object(List(EOC, java.lang.Object(List(EOC, NULL)))), i89) → 757_0_add_Return(EOS(STATIC_757), java.lang.Object(List(EOC, java.lang.Object(List(EOC, NULL)))), i89)
757_0_add_Return(EOS(STATIC_757), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o157)))), i143) → 770_0_add_Return(EOS(STATIC_770))
831_0_add_Return(EOS(STATIC_831), java.lang.Object(List(EOC, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o157)))))), i157) → 757_0_add_Return(EOS(STATIC_757), java.lang.Object(List(EOC, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o157)))))), i157)

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(646_0_add_Return(EOS(STATIC_646)), java.lang.Object(x0), x1) → 770_0_add_Return(EOS(STATIC_770))
608_1_add_InvokeMethod(770_0_add_Return(EOS(STATIC_770)), java.lang.Object(x0), x1) → 770_0_add_Return(EOS(STATIC_770))

Filtered ground terms:

583_0_add_FieldAccess(x1, x2, x3, x4) → 583_0_add_FieldAccess(x2, x3, x4)
List(x1, x2) → List(x2)
770_0_add_Return(x1) → 770_0_add_Return
646_0_add_Return(x1) → 646_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(646_0_add_Return) → 770_0_add_Return
608_1_add_InvokeMethod(770_0_add_Return) → 770_0_add_Return

Performed bisimulation on rules. Used the following equivalence classes: {[646_0_add_Return, 770_0_add_Return]=646_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(646_0_add_Return) → 646_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(646_0_add_Return) → 646_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(646_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(646_0_add_Return) → 646_0_add_Return

The set Q consists of the following terms:

608_1_add_InvokeMethod(646_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(646_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(646_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) → 288_0_rec_IntArithmetic(EOS(STATIC_288), java.lang.Object(List(EOC)), 3, i38) | =(matching1, 3)
288_0_rec_IntArithmetic(EOS(STATIC_288), java.lang.Object(List(EOC)), matching1, i38) → 295_0_rec_Store(EOS(STATIC_295), java.lang.Object(List(EOC)), *(3, i38)) | =(matching1, 3)
295_0_rec_Store(EOS(STATIC_295), java.lang.Object(List(EOC)), i42) → 302_0_rec_Load(EOS(STATIC_302), java.lang.Object(List(EOC)), i42)
302_0_rec_Load(EOS(STATIC_302), java.lang.Object(List(EOC)), i42) → 309_0_rec_ConstantStackPush(EOS(STATIC_309), java.lang.Object(List(EOC)), i42, i42)
309_0_rec_ConstantStackPush(EOS(STATIC_309), java.lang.Object(List(EOC)), i42, i42) → 322_0_rec_GE(EOS(STATIC_322), java.lang.Object(List(EOC)), i42, i42, 100000)
322_0_rec_GE(EOS(STATIC_322), java.lang.Object(List(EOC)), i47, i47, matching1) → 333_0_rec_GE(EOS(STATIC_333), java.lang.Object(List(EOC)), i47, i47, 100000) | =(matching1, 100000)
333_0_rec_GE(EOS(STATIC_333), java.lang.Object(List(EOC)), i47, i47, matching1) → 342_0_rec_Load(EOS(STATIC_342), java.lang.Object(List(EOC)), i47) | &&(<(i47, 100000), =(matching1, 100000))
342_0_rec_Load(EOS(STATIC_342), java.lang.Object(List(EOC)), i47) → 353_0_rec_ConstantStackPush(EOS(STATIC_353), java.lang.Object(List(EOC)), i47, i47)
353_0_rec_ConstantStackPush(EOS(STATIC_353), java.lang.Object(List(EOC)), i47, i47) → 363_0_rec_IntArithmetic(EOS(STATIC_363), java.lang.Object(List(EOC)), i47, i47, 1)
363_0_rec_IntArithmetic(EOS(STATIC_363), java.lang.Object(List(EOC)), i47, i47, matching1) → 373_0_rec_Load(EOS(STATIC_373), java.lang.Object(List(EOC)), i47, +(i47, 1)) | &&(>=(i47, 0), =(matching1, 1))
373_0_rec_Load(EOS(STATIC_373), java.lang.Object(List(EOC)), i47, i53) → 382_0_rec_InvokeMethod(EOS(STATIC_382), java.lang.Object(List(EOC)), i47, i53, java.lang.Object(List(EOC)))
382_0_rec_InvokeMethod(EOS(STATIC_382), java.lang.Object(List(EOC)), i47, i53, java.lang.Object(List(EOC))) → 391_1_rec_InvokeMethod(391_0_rec_ConstantStackPush(EOS(STATIC_391), i53, java.lang.Object(List(EOC))), java.lang.Object(List(EOC)), i47, i53, java.lang.Object(List(EOC)))
391_0_rec_ConstantStackPush(EOS(STATIC_391), i53, java.lang.Object(List(EOC))) → 401_0_rec_ConstantStackPush(EOS(STATIC_401), i53, java.lang.Object(List(EOC)))
401_0_rec_ConstantStackPush(EOS(STATIC_401), i53, java.lang.Object(List(EOC))) → 283_0_rec_ConstantStackPush(EOS(STATIC_283), i53, java.lang.Object(List(EOC)))
283_0_rec_ConstantStackPush(EOS(STATIC_283), i38, java.lang.Object(List(EOC))) → 286_0_rec_Load(EOS(STATIC_286), i38, java.lang.Object(List(EOC)), 3)
R rules:
417_0_add_Load(EOS(STATIC_417), java.lang.Object(List(EOC))) → 581_0_add_Load(EOS(STATIC_581), java.lang.Object(List(EOC)), i55)
851_0_add_Load(EOS(STATIC_851), java.lang.Object(List(EOC))) → 581_0_add_Load(EOS(STATIC_581), java.lang.Object(List(EOC)), i183)
612_0_add_Load(EOS(STATIC_612), java.lang.Object(o78sub), i76) → 581_0_add_Load(EOS(STATIC_581), java.lang.Object(o78sub), i76)
322_0_rec_GE(EOS(STATIC_322), java.lang.Object(List(EOC)), i48, i48, matching1) → 334_0_rec_GE(EOS(STATIC_334), java.lang.Object(List(EOC)), i48, i48, 100000) | =(matching1, 100000)
334_0_rec_GE(EOS(STATIC_334), java.lang.Object(List(EOC)), i48, i48, matching1) → 345_0_rec_Load(EOS(STATIC_345), java.lang.Object(List(EOC)), i48) | &&(>=(i48, 100000), =(matching1, 100000))
345_0_rec_Load(EOS(STATIC_345), java.lang.Object(List(EOC)), i48) → 355_0_rec_ConstantStackPush(EOS(STATIC_355), java.lang.Object(List(EOC)), i48)
355_0_rec_ConstantStackPush(EOS(STATIC_355), java.lang.Object(List(EOC)), i48) → 365_0_rec_IntArithmetic(EOS(STATIC_365), java.lang.Object(List(EOC)), i48)
365_0_rec_IntArithmetic(EOS(STATIC_365), java.lang.Object(List(EOC)), i48) → 375_0_rec_Store(EOS(STATIC_375), java.lang.Object(List(EOC))) | >(i48, 1)
375_0_rec_Store(EOS(STATIC_375), java.lang.Object(List(EOC))) → 384_0_rec_Load(EOS(STATIC_384), java.lang.Object(List(EOC)))
384_0_rec_Load(EOS(STATIC_384), java.lang.Object(List(EOC))) → 393_0_rec_Load(EOS(STATIC_393), java.lang.Object(List(EOC)))
391_1_rec_InvokeMethod(766_0_rec_Return(EOS(STATIC_766)), java.lang.Object(List(EOC)), i47, i153, java.lang.Object(List(EOC))) → 817_0_rec_Return(EOS(STATIC_817), java.lang.Object(List(EOC)), i47, i153, java.lang.Object(List(EOC)))
391_1_rec_InvokeMethod(875_0_rec_Return(EOS(STATIC_875)), java.lang.Object(List(EOC)), i47, i199, java.lang.Object(List(EOC))) → 891_0_rec_Return(EOS(STATIC_891), java.lang.Object(List(EOC)), i47, i199, java.lang.Object(List(EOC)))
393_0_rec_Load(EOS(STATIC_393), java.lang.Object(List(EOC))) → 403_0_rec_InvokeMethod(EOS(STATIC_403), java.lang.Object(List(EOC)))
403_0_rec_InvokeMethod(EOS(STATIC_403), java.lang.Object(List(EOC))) → 409_1_rec_InvokeMethod(409_0_add_Load(EOS(STATIC_409), java.lang.Object(List(EOC))), java.lang.Object(List(EOC)))
409_0_add_Load(EOS(STATIC_409), java.lang.Object(List(EOC))) → 417_0_add_Load(EOS(STATIC_417), java.lang.Object(List(EOC)))
409_1_rec_InvokeMethod(646_0_add_Return(EOS(STATIC_646)), java.lang.Object(List(EOC))) → 662_0_add_Return(EOS(STATIC_662), java.lang.Object(List(EOC)))
409_1_rec_InvokeMethod(770_0_add_Return(EOS(STATIC_770)), java.lang.Object(List(EOC))) → 824_0_add_Return(EOS(STATIC_824), java.lang.Object(List(EOC)))
662_0_add_Return(EOS(STATIC_662), java.lang.Object(List(EOC))) → 663_0_add_Return(EOS(STATIC_663), java.lang.Object(List(EOC)))
663_0_add_Return(EOS(STATIC_663), java.lang.Object(List(EOC))) → 745_0_add_Return(EOS(STATIC_745), java.lang.Object(List(EOC)))
712_0_rec_Return(EOS(STATIC_712), java.lang.Object(List(EOC)), i47, i115, java.lang.Object(List(EOC))) → 735_0_rec_Return(EOS(STATIC_735), java.lang.Object(List(EOC)), i47, i115, java.lang.Object(List(EOC)))
735_0_rec_Return(EOS(STATIC_735), java.lang.Object(List(EOC)), i47, i128, java.lang.Object(List(EOC))) → 818_0_rec_Return(EOS(STATIC_818), java.lang.Object(List(EOC)), i47, i128, java.lang.Object(List(EOC)))
745_0_add_Return(EOS(STATIC_745), java.lang.Object(List(EOC))) → 766_0_rec_Return(EOS(STATIC_766))
766_0_rec_Return(EOS(STATIC_766)) → 875_0_rec_Return(EOS(STATIC_875))
817_0_rec_Return(EOS(STATIC_817), java.lang.Object(List(EOC)), i47, i153, java.lang.Object(List(EOC))) → 818_0_rec_Return(EOS(STATIC_818), java.lang.Object(List(EOC)), i47, i153, java.lang.Object(List(EOC)))
818_0_rec_Return(EOS(STATIC_818), java.lang.Object(List(EOC)), i47, i169, java.lang.Object(List(EOC))) → 834_0_rec_Load(EOS(STATIC_834), java.lang.Object(List(EOC)), i47)
824_0_add_Return(EOS(STATIC_824), java.lang.Object(List(EOC))) → 745_0_add_Return(EOS(STATIC_745), java.lang.Object(List(EOC)))
834_0_rec_Load(EOS(STATIC_834), java.lang.Object(List(EOC)), i47) → 838_0_rec_ConstantStackPush(EOS(STATIC_838), java.lang.Object(List(EOC)), i47)
838_0_rec_ConstantStackPush(EOS(STATIC_838), java.lang.Object(List(EOC)), i47) → 840_0_rec_IntArithmetic(EOS(STATIC_840), java.lang.Object(List(EOC)), i47)
840_0_rec_IntArithmetic(EOS(STATIC_840), java.lang.Object(List(EOC)), i47) → 842_0_rec_Store(EOS(STATIC_842), java.lang.Object(List(EOC)))
842_0_rec_Store(EOS(STATIC_842), java.lang.Object(List(EOC))) → 844_0_rec_Load(EOS(STATIC_844), java.lang.Object(List(EOC)))
844_0_rec_Load(EOS(STATIC_844), java.lang.Object(List(EOC))) → 846_0_rec_Load(EOS(STATIC_846), java.lang.Object(List(EOC)))
846_0_rec_Load(EOS(STATIC_846), java.lang.Object(List(EOC))) → 847_0_rec_InvokeMethod(EOS(STATIC_847), java.lang.Object(List(EOC)))
847_0_rec_InvokeMethod(EOS(STATIC_847), java.lang.Object(List(EOC))) → 849_1_rec_InvokeMethod(849_0_add_Load(EOS(STATIC_849), java.lang.Object(List(EOC))), java.lang.Object(List(EOC)))
849_0_add_Load(EOS(STATIC_849), java.lang.Object(List(EOC))) → 851_0_add_Load(EOS(STATIC_851), java.lang.Object(List(EOC)))
849_1_rec_InvokeMethod(646_0_add_Return(EOS(STATIC_646)), java.lang.Object(List(EOC))) → 860_0_add_Return(EOS(STATIC_860), java.lang.Object(List(EOC)))
849_1_rec_InvokeMethod(770_0_add_Return(EOS(STATIC_770)), java.lang.Object(List(EOC))) → 867_0_add_Return(EOS(STATIC_867), java.lang.Object(List(EOC)))
860_0_add_Return(EOS(STATIC_860), java.lang.Object(List(EOC))) → 868_0_add_Return(EOS(STATIC_868), java.lang.Object(List(EOC)))
867_0_add_Return(EOS(STATIC_867), java.lang.Object(List(EOC))) → 868_0_add_Return(EOS(STATIC_868), java.lang.Object(List(EOC)))
868_0_add_Return(EOS(STATIC_868), java.lang.Object(List(EOC))) → 875_0_rec_Return(EOS(STATIC_875))
891_0_rec_Return(EOS(STATIC_891), java.lang.Object(List(EOC)), i47, i199, java.lang.Object(List(EOC))) → 818_0_rec_Return(EOS(STATIC_818), java.lang.Object(List(EOC)), i47, i199, java.lang.Object(List(EOC)))
581_0_add_Load(EOS(STATIC_581), 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))) → 586_0_add_FieldAccess(EOS(STATIC_586), java.lang.Object(List(EOC)), i76, java.lang.Object(List(EOC)))
586_0_add_FieldAccess(EOS(STATIC_586), java.lang.Object(List(EOC)), i76, java.lang.Object(List(EOC))) → 588_0_add_NONNULL(EOS(STATIC_588), java.lang.Object(List(EOC)), i76, o75)
588_0_add_NONNULL(EOS(STATIC_588), 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))
588_0_add_NONNULL(EOS(STATIC_588), 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) → 597_0_add_FieldAccess(EOS(STATIC_597), i76, java.lang.Object(List(EOC)))
595_0_add_Load(EOS(STATIC_595), java.lang.Object(List(EOC)), i76) → 599_0_add_New(EOS(STATIC_599), i76, java.lang.Object(List(EOC)))
597_0_add_FieldAccess(EOS(STATIC_597), i76, java.lang.Object(List(EOC))) → 601_0_add_Load(EOS(STATIC_601), i76, java.lang.Object(o78sub))
599_0_add_New(EOS(STATIC_599), i76, java.lang.Object(List(EOC))) → 603_0_add_Duplicate(EOS(STATIC_603), i76, java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
601_0_add_Load(EOS(STATIC_601), i76, java.lang.Object(o78sub)) → 605_0_add_InvokeMethod(EOS(STATIC_605), java.lang.Object(o78sub), i76)
603_0_add_Duplicate(EOS(STATIC_603), 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)))
605_0_add_InvokeMethod(EOS(STATIC_605), 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) → 612_0_add_Load(EOS(STATIC_612), java.lang.Object(o78sub), i76)
608_1_add_InvokeMethod(646_0_add_Return(EOS(STATIC_646)), java.lang.Object(o78sub), i89) → 667_0_add_Return(EOS(STATIC_667), java.lang.Object(List(EOC)), i89)
608_1_add_InvokeMethod(770_0_add_Return(EOS(STATIC_770)), java.lang.Object(o78sub), i157) → 831_0_add_Return(EOS(STATIC_831), java.lang.Object(List(EOC)), i157)
610_0_add_ConstantStackPush(EOS(STATIC_610), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76) → 614_0_add_InvokeMethod(EOS(STATIC_614), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL)
614_0_add_InvokeMethod(EOS(STATIC_614), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL) → 616_0_<init>_Load(EOS(STATIC_616), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), i76, NULL)
616_0_<init>_Load(EOS(STATIC_616), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), i76, NULL) → 619_0_<init>_InvokeMethod(EOS(STATIC_619), 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)))
619_0_<init>_InvokeMethod(EOS(STATIC_619), 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>_Load(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)
620_0_<init>_Load(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) → 622_0_<init>_ConstantStackPush(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, java.lang.Object(List(EOC)))
622_0_<init>_ConstantStackPush(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, java.lang.Object(List(EOC))) → 624_0_<init>_FieldAccess(EOS(STATIC_624), 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)
624_0_<init>_FieldAccess(EOS(STATIC_624), 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) → 625_0_<init>_Load(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) | =(matching1, 0)
625_0_<init>_Load(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) → 627_0_<init>_ConstantStackPush(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, java.lang.Object(List(EOC)))
627_0_<init>_ConstantStackPush(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, java.lang.Object(List(EOC))) → 629_0_<init>_FieldAccess(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)), NULL)
629_0_<init>_FieldAccess(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)), NULL) → 630_0_<init>_Load(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)
630_0_<init>_Load(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) → 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, java.lang.Object(List(EOC)))
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, java.lang.Object(List(EOC))) → 634_0_<init>_FieldAccess(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)), NULL, java.lang.Object(List(EOC)), i76)
634_0_<init>_FieldAccess(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)), NULL, java.lang.Object(List(EOC)), i76) → 636_0_<init>_Load(EOS(STATIC_636), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL, java.lang.Object(List(EOC)), NULL)
636_0_<init>_Load(EOS(STATIC_636), 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, NULL, java.lang.Object(List(EOC)))
637_0_<init>_Load(EOS(STATIC_637), 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>_FieldAccess(EOS(STATIC_639), 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>_FieldAccess(EOS(STATIC_639), 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>_Return(EOS(STATIC_641), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL)
641_0_<init>_Return(EOS(STATIC_641), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)), i76, NULL) → 642_0_add_FieldAccess(EOS(STATIC_642), java.lang.Object(List(EOC)), java.lang.Object(List(EOC)))
642_0_add_FieldAccess(EOS(STATIC_642), java.lang.Object(List(EOC)), java.lang.Object(List(EOC))) → 645_0_add_JMP(EOS(STATIC_645))
645_0_add_JMP(EOS(STATIC_645)) → 646_0_add_Return(EOS(STATIC_646))
667_0_add_Return(EOS(STATIC_667), java.lang.Object(List(EOC)), i89) → 757_0_add_Return(EOS(STATIC_757), java.lang.Object(List(EOC)), i89)
757_0_add_Return(EOS(STATIC_757), java.lang.Object(List(EOC)), i143) → 770_0_add_Return(EOS(STATIC_770))
831_0_add_Return(EOS(STATIC_831), java.lang.Object(List(EOC)), i157) → 757_0_add_Return(EOS(STATIC_757), java.lang.Object(List(EOC)), i157)

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) → 391_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:
391_1_rec_InvokeMethod(766_0_rec_Return(EOS(STATIC_766)), java.lang.Object(List(EOC)), x0, x1, java.lang.Object(List(EOC))) → 849_1_rec_InvokeMethod(588_0_add_NONNULL(EOS(STATIC_588), java.lang.Object(List(EOC)), x2, x3), java.lang.Object(List(EOC)))
391_1_rec_InvokeMethod(875_0_rec_Return(EOS(STATIC_875)), java.lang.Object(List(EOC)), x0, x1, java.lang.Object(List(EOC))) → 849_1_rec_InvokeMethod(588_0_add_NONNULL(EOS(STATIC_588), java.lang.Object(List(EOC)), x2, x3), java.lang.Object(List(EOC)))
588_0_add_NONNULL(EOS(STATIC_588), java.lang.Object(List(EOC)), x0, java.lang.Object(x1)) → 608_1_add_InvokeMethod(588_0_add_NONNULL(EOS(STATIC_588), java.lang.Object(List(EOC)), x0, x2), java.lang.Object(List(EOC)), x0)
588_0_add_NONNULL(EOS(STATIC_588), java.lang.Object(List(EOC)), x0, NULL) → 646_0_add_Return(EOS(STATIC_646))
608_1_add_InvokeMethod(646_0_add_Return(EOS(STATIC_646)), java.lang.Object(x0), x1) → 770_0_add_Return(EOS(STATIC_770))
608_1_add_InvokeMethod(770_0_add_Return(EOS(STATIC_770)), java.lang.Object(x0), x1) → 770_0_add_Return(EOS(STATIC_770))
849_1_rec_InvokeMethod(646_0_add_Return(EOS(STATIC_646)), java.lang.Object(List(EOC))) → 875_0_rec_Return(EOS(STATIC_875))
849_1_rec_InvokeMethod(770_0_add_Return(EOS(STATIC_770)), java.lang.Object(List(EOC))) → 875_0_rec_Return(EOS(STATIC_875))

Filtered ground terms:

391_1_rec_InvokeMethod(x1, x2, x3, x4, x5) → 391_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)
875_0_rec_Return(x1) → 875_0_rec_Return
849_1_rec_InvokeMethod(x1, x2) → 849_1_rec_InvokeMethod(x1)
770_0_add_Return(x1) → 770_0_add_Return
646_0_add_Return(x1) → 646_0_add_Return
588_0_add_NONNULL(x1, x2, x3, x4) → 588_0_add_NONNULL(x3, x4)
766_0_rec_Return(x1) → 766_0_rec_Return

Filtered unneeded arguments:

391_1_rec_InvokeMethod(x1, x2, x3) → 391_1_rec_InvokeMethod(x1)
588_0_add_NONNULL(x1, x2) → 588_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) → 391_1_rec_InvokeMethod(286_0_rec_Load(+(*(3, x0), 1))) | &&(>(100000, *(3, x0)), <=(0, *(3, x0)))
R rules:
391_1_rec_InvokeMethod(766_0_rec_Return) → 849_1_rec_InvokeMethod(588_0_add_NONNULL(x3))
391_1_rec_InvokeMethod(875_0_rec_Return) → 849_1_rec_InvokeMethod(588_0_add_NONNULL(x3))
588_0_add_NONNULL(java.lang.Object(x1)) → 608_1_add_InvokeMethod(588_0_add_NONNULL(x2), java.lang.Object(List))
588_0_add_NONNULL(NULL) → 646_0_add_Return
608_1_add_InvokeMethod(646_0_add_Return, java.lang.Object(x0)) → 770_0_add_Return
608_1_add_InvokeMethod(770_0_add_Return, java.lang.Object(x0)) → 770_0_add_Return
849_1_rec_InvokeMethod(646_0_add_Return) → 875_0_rec_Return
849_1_rec_InvokeMethod(770_0_add_Return) → 875_0_rec_Return

Performed bisimulation on rules. Used the following equivalence classes: {[766_0_rec_Return, 875_0_rec_Return, List, 646_0_add_Return, 770_0_add_Return]=766_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:
391_1_rec_InvokeMethod(766_0_rec_Return) → 849_1_rec_InvokeMethod(588_0_add_NONNULL(x3))
588_0_add_NONNULL(java.lang.Object(x1)) → 608_1_add_InvokeMethod(588_0_add_NONNULL(x2), java.lang.Object(766_0_rec_Return))
588_0_add_NONNULL(NULL) → 766_0_rec_Return
608_1_add_InvokeMethod(766_0_rec_Return, java.lang.Object(x0)) → 766_0_rec_Return
849_1_rec_InvokeMethod(766_0_rec_Return) → 766_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:
391_1_rec_InvokeMethod(766_0_rec_Return) → 849_1_rec_InvokeMethod(588_0_add_NONNULL(x3))
588_0_add_NONNULL(java.lang.Object(x1)) → 608_1_add_InvokeMethod(588_0_add_NONNULL(x2), java.lang.Object(766_0_rec_Return))
588_0_add_NONNULL(NULL) → 766_0_rec_Return
608_1_add_InvokeMethod(766_0_rec_Return, java.lang.Object(x0)) → 766_0_rec_Return
849_1_rec_InvokeMethod(766_0_rec_Return) → 766_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:
391_1_rec_InvokeMethod(766_0_rec_Return)
588_0_add_NONNULL(java.lang.Object(x0))
588_0_add_NONNULL(NULL)
608_1_add_InvokeMethod(766_0_rec_Return, java.lang.Object(x0))
849_1_rec_InvokeMethod(766_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@43a63a1c 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(391_1_rec_InvokeMethod(x₁)) = [-1] + [-1]x₁
POL(766_0_rec_Return) = [-1]
POL(849_1_rec_InvokeMethod(x₁)) = [-1] + [-1]x₁
POL(588_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₂ + [-1]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:
391_1_rec_InvokeMethod(766_0_rec_Return) → 849_1_rec_InvokeMethod(588_0_add_NONNULL(x3))
588_0_add_NONNULL(java.lang.Object(x1)) → 608_1_add_InvokeMethod(588_0_add_NONNULL(x2), java.lang.Object(766_0_rec_Return))
588_0_add_NONNULL(NULL) → 766_0_rec_Return
608_1_add_InvokeMethod(766_0_rec_Return, java.lang.Object(x0)) → 766_0_rec_Return
849_1_rec_InvokeMethod(766_0_rec_Return) → 766_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:
391_1_rec_InvokeMethod(766_0_rec_Return)
588_0_add_NONNULL(java.lang.Object(x0))
588_0_add_NONNULL(NULL)
608_1_add_InvokeMethod(766_0_rec_Return, java.lang.Object(x0))
849_1_rec_InvokeMethod(766_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