Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 383 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 AND
    ↳5 JBCTerminationSCC
        ↳6 SCCToIntTRSProof (⇒, 157 ms)
        ↳7 intTRS
        ↳8 PolynomialOrderProcessor (⇒, 0 ms)
        ↳9 intTRS
        ↳10 PolynomialOrderProcessor (⇔, 0 ms)
        ↳11 YES
    ↳12 JBCTerminationSCC
        ↳13 SCCToIntTRSProof (⇒, 0 ms)
        ↳14 intTRS
        ↳15 PolynomialOrderProcessor (⇔, 0 ms)
        ↳16 YES

(0) Obligation:

JBC Problem based on JBC Program:
public class AppE {
	AppE next;

	public static void main(String[] args) {
		Random.args = args;
		AppE list = createList();
		list.appE(Random.random());
	}

	public void appE(int i) {
		if (next == null) {
			if (i <= 0) {
				return;
			} else {
				next = new AppE();
			}
			i--;
	 	}
		next.appE(i);
	}

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

	public AppE() {
		this.next = null;
	}

	public AppE(AppE n) {
		this.next = n;
	}
}

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

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


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

AppE.createList()LAppE;: Graph of 91 nodes with 1 SCC.

AppE.appE(I)V: Graph of 56 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: AppE.appE(I)V
SCC calls the following helper methods: AppE.appE(I)V
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
    • AppE: [next]
  • Marker field analysis yielded the following relations that could be markers:

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 36 IRules

P rules:
f593_0_appE_FieldAccess(EOS, java.lang.Object(AppE(EOC, o110)), i83, java.lang.Object(AppE(EOC, o110)), i83, java.lang.Object(AppE(EOC, o110))) → f594_0_appE_FieldAccess(EOS, java.lang.Object(AppE(EOC, o110)), i83, java.lang.Object(AppE(EOC, o110)), i83, java.lang.Object(AppE(EOC, o110)))
f594_0_appE_FieldAccess(EOS, java.lang.Object(AppE(EOC, o110)), i83, java.lang.Object(AppE(EOC, o110)), i83, java.lang.Object(AppE(EOC, o110))) → f600_0_appE_NONNULL(EOS, java.lang.Object(AppE(EOC, o110)), i83, java.lang.Object(AppE(EOC, o110)), i83, o110)
f600_0_appE_NONNULL(EOS, java.lang.Object(AppE(EOC, java.lang.Object(o113sub))), i83, java.lang.Object(AppE(EOC, java.lang.Object(o113sub))), i83, java.lang.Object(o113sub)) → f604_0_appE_NONNULL(EOS, java.lang.Object(AppE(EOC, java.lang.Object(o113sub))), i83, java.lang.Object(AppE(EOC, java.lang.Object(o113sub))), i83, java.lang.Object(o113sub))
f600_0_appE_NONNULL(EOS, java.lang.Object(AppE(EOC, NULL)), i83, java.lang.Object(AppE(EOC, NULL)), i83, NULL) → f605_0_appE_NONNULL(EOS, java.lang.Object(AppE(EOC, NULL)), i83, java.lang.Object(AppE(EOC, NULL)), i83, NULL)
f604_0_appE_NONNULL(EOS, java.lang.Object(AppE(EOC, java.lang.Object(o113sub))), i83, java.lang.Object(AppE(EOC, java.lang.Object(o113sub))), i83, java.lang.Object(o113sub)) → f609_0_appE_Load(EOS, java.lang.Object(AppE(EOC, java.lang.Object(o113sub))), i83, java.lang.Object(AppE(EOC, java.lang.Object(o113sub))), i83)
f609_0_appE_Load(EOS, java.lang.Object(AppE(EOC, java.lang.Object(o113sub))), i83, java.lang.Object(AppE(EOC, java.lang.Object(o113sub))), i83) → f616_0_appE_FieldAccess(EOS, java.lang.Object(AppE(EOC, java.lang.Object(o113sub))), i83, i83, java.lang.Object(AppE(EOC, java.lang.Object(o113sub))))
f616_0_appE_FieldAccess(EOS, java.lang.Object(AppE(EOC, java.lang.Object(o113sub))), i83, i83, java.lang.Object(AppE(EOC, java.lang.Object(o113sub)))) → f627_0_appE_Load(EOS, java.lang.Object(AppE(EOC, java.lang.Object(o113sub))), i83, i83, java.lang.Object(o113sub))
f627_0_appE_Load(EOS, java.lang.Object(AppE(EOC, java.lang.Object(o113sub))), i83, i83, java.lang.Object(o113sub)) → f638_0_appE_InvokeMethod(EOS, java.lang.Object(AppE(EOC, java.lang.Object(o113sub))), i83, java.lang.Object(o113sub), i83)
f638_0_appE_InvokeMethod(EOS, java.lang.Object(AppE(EOC, java.lang.Object(o113sub))), i83, java.lang.Object(o113sub), i83) → f651_0_appE_Load(EOS, java.lang.Object(o113sub), i83, java.lang.Object(o113sub), i83)
f638_0_appE_InvokeMethod(EOS, java.lang.Object(AppE(EOC, java.lang.Object(o113sub))), i83, java.lang.Object(o113sub), i83) → f651_1_appE_Load(EOS, java.lang.Object(AppE(EOC, java.lang.Object(o113sub))), i83, java.lang.Object(o113sub), i83, java.lang.Object(o113sub), i83)
f651_0_appE_Load(EOS, java.lang.Object(o113sub), i83, java.lang.Object(o113sub), i83) → f665_0_appE_Load(EOS, java.lang.Object(o113sub), i83, java.lang.Object(o113sub), i83)
f665_0_appE_Load(EOS, java.lang.Object(o113sub), i83, java.lang.Object(o113sub), i83) → f587_0_appE_Load(EOS, java.lang.Object(o113sub), i83, java.lang.Object(o113sub), i83)
f587_0_appE_Load(EOS, java.lang.Object(o100sub), i83, java.lang.Object(o100sub), i83) → f593_0_appE_FieldAccess(EOS, java.lang.Object(o100sub), i83, java.lang.Object(o100sub), i83, java.lang.Object(o100sub))
f605_0_appE_NONNULL(EOS, java.lang.Object(AppE(EOC, NULL)), i83, java.lang.Object(AppE(EOC, NULL)), i83, NULL) → f614_0_appE_Load(EOS, java.lang.Object(AppE(EOC, NULL)), i83, java.lang.Object(AppE(EOC, NULL)), i83)
f614_0_appE_Load(EOS, java.lang.Object(AppE(EOC, NULL)), i83, java.lang.Object(AppE(EOC, NULL)), i83) → f622_0_appE_GT(EOS, java.lang.Object(AppE(EOC, NULL)), i83, java.lang.Object(AppE(EOC, NULL)), i83, i83)
f622_0_appE_GT(EOS, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), i93, i93) → f633_0_appE_GT(EOS, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), i93, i93)
f633_0_appE_GT(EOS, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), i93, i93) → f646_0_appE_Load(EOS, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), i93) | >(i93, 0)
f646_0_appE_Load(EOS, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), i93) → f657_0_appE_New(EOS, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)))
f657_0_appE_New(EOS, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL))) → f685_0_appE_Duplicate(EOS, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)))
f685_0_appE_Duplicate(EOS, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL))) → f690_0_appE_InvokeMethod(EOS, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)))
f690_0_appE_InvokeMethod(EOS, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL))) → f708_0__init__Load(EOS, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)))
f708_0__init__Load(EOS, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL))) → f722_0__init__InvokeMethod(EOS, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)))
f722_0__init__InvokeMethod(EOS, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL))) → f730_0__init__Load(EOS, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)))
f730_0__init__Load(EOS, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL))) → f767_0__init__ConstantStackPush(EOS, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)))
f767_0__init__ConstantStackPush(EOS, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL))) → f776_0__init__FieldAccess(EOS, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), NULL)
f776_0__init__FieldAccess(EOS, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), NULL) → f791_0__init__Return(EOS, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)))
f791_0__init__Return(EOS, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL))) → f800_0_appE_FieldAccess(EOS, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL)))
f800_0_appE_FieldAccess(EOS, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), i93, java.lang.Object(AppE(EOC, NULL)), java.lang.Object(AppE(EOC, NULL))) → f847_0_appE_Inc(EOS, java.lang.Object(AppE(EOC, java.lang.Object(AppE(EOC, NULL)))), i93, java.lang.Object(AppE(EOC, java.lang.Object(AppE(EOC, NULL)))), i93)
f847_0_appE_Inc(EOS, java.lang.Object(AppE(EOC, java.lang.Object(AppE(EOC, NULL)))), i93, java.lang.Object(AppE(EOC, java.lang.Object(AppE(EOC, NULL)))), i93) → f875_0_appE_Load(EOS, java.lang.Object(AppE(EOC, java.lang.Object(AppE(EOC, NULL)))), i93, java.lang.Object(AppE(EOC, java.lang.Object(AppE(EOC, NULL)))), +(i93, -1)) | >(i93, 0)
f875_0_appE_Load(EOS, java.lang.Object(AppE(EOC, java.lang.Object(AppE(EOC, NULL)))), i93, java.lang.Object(AppE(EOC, java.lang.Object(AppE(EOC, NULL)))), i132) → f889_0_appE_FieldAccess(EOS, java.lang.Object(AppE(EOC, java.lang.Object(AppE(EOC, NULL)))), i93, i132, java.lang.Object(AppE(EOC, java.lang.Object(AppE(EOC, NULL)))))
f889_0_appE_FieldAccess(EOS, java.lang.Object(AppE(EOC, java.lang.Object(AppE(EOC, NULL)))), i93, i132, java.lang.Object(AppE(EOC, java.lang.Object(AppE(EOC, NULL))))) → f899_0_appE_Load(EOS, java.lang.Object(AppE(EOC, java.lang.Object(AppE(EOC, NULL)))), i93, i132, java.lang.Object(AppE(EOC, NULL)))
f899_0_appE_Load(EOS, java.lang.Object(AppE(EOC, java.lang.Object(AppE(EOC, NULL)))), i93, i132, java.lang.Object(AppE(EOC, NULL))) → f940_0_appE_InvokeMethod(EOS, java.lang.Object(AppE(EOC, java.lang.Object(AppE(EOC, NULL)))), i93, java.lang.Object(AppE(EOC, NULL)), i132)
f940_0_appE_InvokeMethod(EOS, java.lang.Object(AppE(EOC, java.lang.Object(AppE(EOC, NULL)))), i93, java.lang.Object(AppE(EOC, NULL)), i132) → f957_0_appE_Load(EOS, java.lang.Object(AppE(EOC, NULL)), i132, java.lang.Object(AppE(EOC, NULL)), i132)
f940_0_appE_InvokeMethod(EOS, java.lang.Object(AppE(EOC, java.lang.Object(AppE(EOC, NULL)))), i93, java.lang.Object(AppE(EOC, NULL)), i132) → f957_1_appE_Load(EOS, java.lang.Object(AppE(EOC, java.lang.Object(AppE(EOC, NULL)))), i93, java.lang.Object(AppE(EOC, NULL)), i132, java.lang.Object(AppE(EOC, NULL)), i132)
f957_0_appE_Load(EOS, java.lang.Object(AppE(EOC, NULL)), i132, java.lang.Object(AppE(EOC, NULL)), i132) → f964_0_appE_Load(EOS, java.lang.Object(AppE(EOC, NULL)), i132, java.lang.Object(AppE(EOC, NULL)), i132)
f964_0_appE_Load(EOS, java.lang.Object(AppE(EOC, NULL)), i132, java.lang.Object(AppE(EOC, NULL)), i132) → f587_0_appE_Load(EOS, java.lang.Object(AppE(EOC, NULL)), i132, java.lang.Object(AppE(EOC, NULL)), i132)

Combined rules. Obtained 4 IRules

P rules:
f593_0_appE_FieldAccess(EOS, java.lang.Object(AppE(EOC, java.lang.Object(x0))), x1, java.lang.Object(AppE(EOC, java.lang.Object(x0))), x1, java.lang.Object(AppE(EOC, java.lang.Object(x0)))) → f651_1_appE_Load(EOS, java.lang.Object(AppE(EOC, java.lang.Object(x0))), x1, java.lang.Object(x0), x1, java.lang.Object(x0), x1)
f593_0_appE_FieldAccess(EOS, java.lang.Object(AppE(EOC, java.lang.Object(x0))), x1, java.lang.Object(AppE(EOC, java.lang.Object(x0))), x1, java.lang.Object(AppE(EOC, java.lang.Object(x0)))) → f593_0_appE_FieldAccess(EOS, java.lang.Object(x0), x1, java.lang.Object(x0), x1, java.lang.Object(x0))
f593_0_appE_FieldAccess(EOS, java.lang.Object(AppE(EOC, NULL)), x0, java.lang.Object(AppE(EOC, NULL)), x0, java.lang.Object(AppE(EOC, NULL))) → f957_1_appE_Load(EOS, java.lang.Object(AppE(EOC, java.lang.Object(AppE(EOC, NULL)))), x0, java.lang.Object(AppE(EOC, NULL)), -(x0, 1), java.lang.Object(AppE(EOC, NULL)), -(x0, 1)) | >(x0, 0)
f593_0_appE_FieldAccess(EOS, java.lang.Object(AppE(EOC, NULL)), x0, java.lang.Object(AppE(EOC, NULL)), x0, java.lang.Object(AppE(EOC, NULL))) → f593_0_appE_FieldAccess(EOS, java.lang.Object(AppE(EOC, NULL)), -(x0, 1), java.lang.Object(AppE(EOC, NULL)), -(x0, 1), java.lang.Object(AppE(EOC, NULL))) | >(x0, 0)

Filtered ground terms:


f593_0_appE_FieldAccess(x1, x2, x3, x4, x5, x6) → f593_0_appE_FieldAccess(x2, x3, x4, x5, x6)
f651_1_appE_Load(x1, x2, x3, x4, x5, x6, x7) → f651_1_appE_Load(x2, x3, x4, x5, x6, x7)
Cond_f593_0_appE_FieldAccess(x1, x2, x3, x4, x5, x6, x7) → Cond_f593_0_appE_FieldAccess(x1, x4, x6)
f957_1_appE_Load(x1, x2, x3, x4, x5, x6, x7) → f957_1_appE_Load(x3, x5, x7)
Cond_f593_0_appE_FieldAccess1(x1, x2, x3, x4, x5, x6, x7) → Cond_f593_0_appE_FieldAccess1(x1, x4, x6)
AppE(x1, x2) → AppE(x2)

Filtered duplicate terms:


f593_0_appE_FieldAccess(x1, x2, x3, x4, x5) → f593_0_appE_FieldAccess(x4, x5)
f651_1_appE_Load(x1, x2, x3, x4, x5, x6) → f651_1_appE_Load(x1, x6)
Cond_f593_0_appE_FieldAccess(x1, x2, x3) → Cond_f593_0_appE_FieldAccess(x1, x3)
f957_1_appE_Load(x1, x2, x3) → f957_1_appE_Load(x3)
Cond_f593_0_appE_FieldAccess1(x1, x2, x3) → Cond_f593_0_appE_FieldAccess1(x1, x3)

Filtered unneeded terms:


Cond_f593_0_appE_FieldAccess(x1, x2) → Cond_f593_0_appE_FieldAccess(x1)

Prepared 4 rules for path length conversion:

P rules:
f593_0_appE_FieldAccess(x1, java.lang.Object(AppE(java.lang.Object(x0)))) → f651_1_appE_Load(java.lang.Object(AppE(java.lang.Object(x0))), x1)
f593_0_appE_FieldAccess(x1, java.lang.Object(AppE(java.lang.Object(x0)))) → f593_0_appE_FieldAccess(x1, java.lang.Object(x0))
f593_0_appE_FieldAccess(x0, java.lang.Object(AppE(NULL))) → f957_1_appE_Load(-(x0, 1)) | >(x0, 0)
f593_0_appE_FieldAccess(x0, java.lang.Object(AppE(NULL))) → f593_0_appE_FieldAccess(-(x0, 1), java.lang.Object(AppE(NULL))) | >(x0, 0)

Finished conversion. Obtained 2 rules.

P rules:
f593_0_appE_FieldAccess(x2, v8) → f593_0_appE_FieldAccess(x2, v9) | &&(&&(>(+(v9, 1), 1), <=(+(v9, 2), v8)), >(+(v8, 1), 3))
f593_0_appE_FieldAccess(x5, v10) → f593_0_appE_FieldAccess(-(x5, 1), v11) | &&(&&(&&(>(x5, 0), >(+(v11, 1), 2)), <=(v11, v10)), >(+(v10, 1), 2))

(7) Obligation:

Rules:
f593_0_appE_FieldAccess(x2, v8) → f593_0_appE_FieldAccess(x2, v9) | &&(&&(>(+(v9, 1), 1), <=(+(v9, 2), v8)), >(+(v8, 1), 3))
f593_0_appE_FieldAccess(x5, v10) → f593_0_appE_FieldAccess(-(x5, 1), v11) | &&(&&(&&(>(x5, 0), >(+(v11, 1), 2)), <=(v11, v10)), >(+(v10, 1), 2))

(8) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:


[f593_0_appE_FieldAccess(x7, x9)] = -1 + x7

Therefore the following rule(s) have been dropped:


f593_0_appE_FieldAccess(x3, x4) → f593_0_appE_FieldAccess(-(x3, 1), x5) | &&(&&(&&(>(x3, 0), >(+(x5, 1), 2)), <=(x5, x4)), >(+(x4, 1), 2))

(9) Obligation:

Rules:
f593_0_appE_FieldAccess(x0, x1) → f593_0_appE_FieldAccess(x0, x2) | &&(&&(>(+(x2, 1), 1), <=(+(x2, 2), x1)), >(+(x1, 1), 3))

(10) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f593_0_appE_FieldAccess(x4, x6)] = x6

Therefore the following rule(s) have been dropped:


f593_0_appE_FieldAccess(x0, x1) → f593_0_appE_FieldAccess(x0, x2) | &&(&&(>(+(x2, 1), 1), <=(+(x2, 2), x1)), >(+(x1, 1), 3))

(11) YES

(12) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: AppE.createList()LAppE;
SCC calls the following helper methods:
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
  • Marker field analysis yielded the following relations that could be markers:

(13) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 17 IRules

P rules:
f362_0_createList_LE(EOS, i42, i42) → f371_0_createList_LE(EOS, i42, i42)
f371_0_createList_LE(EOS, i42, i42) → f392_0_createList_New(EOS, i42) | >(i42, 0)
f392_0_createList_New(EOS, i42) → f412_0_createList_Duplicate(EOS, i42)
f412_0_createList_Duplicate(EOS, i42) → f420_0_createList_Load(EOS, i42)
f420_0_createList_Load(EOS, i42) → f438_0_createList_InvokeMethod(EOS, i42)
f438_0_createList_InvokeMethod(EOS, i42) → f442_0__init__Load(EOS, i42)
f442_0__init__Load(EOS, i42) → f446_0__init__InvokeMethod(EOS, i42)
f446_0__init__InvokeMethod(EOS, i42) → f457_0__init__Load(EOS, i42)
f457_0__init__Load(EOS, i42) → f461_0__init__Load(EOS, i42)
f461_0__init__Load(EOS, i42) → f462_0__init__FieldAccess(EOS, i42)
f462_0__init__FieldAccess(EOS, i42) → f465_0__init__Return(EOS, i42)
f465_0__init__Return(EOS, i42) → f467_0_createList_Store(EOS, i42)
f467_0_createList_Store(EOS, i42) → f471_0_createList_Inc(EOS, i42)
f471_0_createList_Inc(EOS, i42) → f475_0_createList_JMP(EOS, +(i42, -1)) | >(i42, 0)
f475_0_createList_JMP(EOS, i69) → f482_0_createList_Load(EOS, i69)
f482_0_createList_Load(EOS, i69) → f351_0_createList_Load(EOS, i69)
f351_0_createList_Load(EOS, i38) → f362_0_createList_LE(EOS, i38, i38)

Combined rules. Obtained 1 IRules

P rules:
f362_0_createList_LE(EOS, x0, x0) → f362_0_createList_LE(EOS, -(x0, 1), -(x0, 1)) | >(x0, 0)

Filtered ground terms:


f362_0_createList_LE(x1, x2, x3) → f362_0_createList_LE(x2, x3)
Cond_f362_0_createList_LE(x1, x2, x3, x4) → Cond_f362_0_createList_LE(x1, x3, x4)

Filtered duplicate terms:


f362_0_createList_LE(x1, x2) → f362_0_createList_LE(x2)
Cond_f362_0_createList_LE(x1, x2, x3) → Cond_f362_0_createList_LE(x1, x3)

Prepared 1 rules for path length conversion:

P rules:
f362_0_createList_LE(x0) → f362_0_createList_LE(-(x0, 1)) | >(x0, 0)

Finished conversion. Obtained 1 rules.

P rules:
f362_0_createList_LE(x0) → f362_0_createList_LE(-(x0, 1)) | >(x0, 0)

(14) Obligation:

Rules:
f362_0_createList_LE(x0) → f362_0_createList_LE(-(x0, 1)) | >(x0, 0)

(15) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f362_0_createList_LE(x2)] = x2

Therefore the following rule(s) have been dropped:


f362_0_createList_LE(x0) → f362_0_createList_LE(-(x0, 1)) | >(x0, 0)

(16) YES