Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 773 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 AND
    ↳5 JBCTerminationSCC
        ↳6 SCCToIntTRSProof (⇒, 42 ms)
        ↳7 intTRS
        ↳8 PolynomialOrderProcessor (⇔, 0 ms)
        ↳9 YES
    ↳10 JBCTerminationSCC
        ↳11 SCCToIntTRSProof (⇒, 43 ms)
        ↳12 intTRS
        ↳13 PolynomialOrderProcessor (⇔, 0 ms)
        ↳14 YES
    ↳15 JBCTerminationSCC
        ↳16 SCCToIntTRSProof (⇒, 64 ms)
        ↳17 intTRS
        ↳18 PolynomialOrderProcessor (⇔, 0 ms)
        ↳19 YES

(0) Obligation:

JBC Problem based on JBC Program:
package CyclicAnalysis;

public class CyclicAnalysis {
	CyclicAnalysis field;

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

	public int length() {
		int length = 1;
		CyclicAnalysis cur = this.field;
		while (cur != null) {
			cur = cur.field;
			length++;
		}
		return length;
	}

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

	/**
 	 * @param i number of elements to append
 	 * @return the last list element appended
 	 */
	private CyclicAnalysis appendNewList(int i) {
		this.field = new CyclicAnalysis();
		CyclicAnalysis cur = this.field;
		while (i > 1) {
			i--;
			cur = cur.field = new CyclicAnalysis();
		}
		return cur;
	}
}


package CyclicAnalysis;

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

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


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
CyclicAnalysis.CyclicAnalysis.main([Ljava/lang/String;)V: Graph of 307 nodes with 3 SCCs.


(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 3 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: CyclicAnalysis.CyclicAnalysis.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
    • CyclicAnalysis.CyclicAnalysis: [field]
  • Marker field analysis yielded the following relations that could be markers:

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 18 IRules

P rules:
f1851_0_length_NULL(EOS, java.lang.Object(o566sub), java.lang.Object(o566sub)) → f1853_0_length_NULL(EOS, java.lang.Object(o566sub), java.lang.Object(o566sub))
f1853_0_length_NULL(EOS, java.lang.Object(o566sub), java.lang.Object(o566sub)) → f1857_0_length_Load(EOS, java.lang.Object(o566sub))
f1857_0_length_Load(EOS, java.lang.Object(o566sub)) → f1860_0_length_FieldAccess(EOS, java.lang.Object(o566sub))
f1860_0_length_FieldAccess(EOS, java.lang.Object(o566sub)) → f1871_0_length_FieldAccess(EOS, java.lang.Object(o566sub))
f1860_0_length_FieldAccess(EOS, java.lang.Object(o569sub)) → f1872_0_length_FieldAccess(EOS, java.lang.Object(o569sub))
f1871_0_length_FieldAccess(EOS, java.lang.Object(CyclicAnalysis.CyclicAnalysis(EOC, o571))) → f1876_0_length_FieldAccess(EOS, java.lang.Object(CyclicAnalysis.CyclicAnalysis(EOC, o571)))
f1876_0_length_FieldAccess(EOS, java.lang.Object(CyclicAnalysis.CyclicAnalysis(EOC, o571))) → f1881_0_length_Store(EOS, o571)
f1881_0_length_Store(EOS, o571) → f1887_0_length_Inc(EOS, o571)
f1887_0_length_Inc(EOS, o571) → f1891_0_length_JMP(EOS, o571)
f1891_0_length_JMP(EOS, o571) → f1901_0_length_Load(EOS, o571)
f1901_0_length_Load(EOS, o571) → f1847_0_length_Load(EOS, o571)
f1847_0_length_Load(EOS, o556) → f1851_0_length_NULL(EOS, o556, o556)
f1872_0_length_FieldAccess(EOS, java.lang.Object(CyclicAnalysis.CyclicAnalysis(EOC, o573))) → f1878_0_length_FieldAccess(EOS, java.lang.Object(CyclicAnalysis.CyclicAnalysis(EOC, o573)))
f1878_0_length_FieldAccess(EOS, java.lang.Object(CyclicAnalysis.CyclicAnalysis(EOC, o573))) → f1884_0_length_Store(EOS, o573)
f1884_0_length_Store(EOS, o573) → f1889_0_length_Inc(EOS, o573)
f1889_0_length_Inc(EOS, o573) → f1894_0_length_JMP(EOS, o573)
f1894_0_length_JMP(EOS, o573) → f1909_0_length_Load(EOS, o573)
f1909_0_length_Load(EOS, o573) → f1847_0_length_Load(EOS, o573)

Combined rules. Obtained 1 IRules

P rules:
f1851_0_length_NULL(EOS, java.lang.Object(CyclicAnalysis.CyclicAnalysis(EOC, x0)), java.lang.Object(CyclicAnalysis.CyclicAnalysis(EOC, x0))) → f1851_0_length_NULL(EOS, x0, x0)

Filtered ground terms:


f1851_0_length_NULL(x1, x2, x3) → f1851_0_length_NULL(x2, x3)
CyclicAnalysis.CyclicAnalysis(x1, x2) → CyclicAnalysis.CyclicAnalysis(x2)

Filtered duplicate terms:


f1851_0_length_NULL(x1, x2) → f1851_0_length_NULL(x2)

Prepared 1 rules for path length conversion:

P rules:
f1851_0_length_NULL(java.lang.Object(CyclicAnalysis.CyclicAnalysis(x0))) → f1851_0_length_NULL(x0)

Finished conversion. Obtained 1 rules.

P rules:
f1851_0_length_NULL(v2) → f1851_0_length_NULL(v3) | &&(&&(>(+(v3, 1), 0), <=(+(v3, 1), v2)), >(+(v2, 1), 1))

(7) Obligation:

Rules:
f1851_0_length_NULL(v2) → f1851_0_length_NULL(v3) | &&(&&(>(+(v3, 1), 0), <=(+(v3, 1), v2)), >(+(v2, 1), 1))

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f1851_0_length_NULL(x3)] = x3

Therefore the following rule(s) have been dropped:


f1851_0_length_NULL(x0) → f1851_0_length_NULL(x1) | &&(&&(>(+(x1, 1), 0), <=(+(x1, 1), x0)), >(+(x0, 1), 1))

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: CyclicAnalysis.CyclicAnalysis.main([Ljava/lang/String;)V
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:

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 23 IRules

P rules:
f1315_0_appendNewList_ConstantStackPush(EOS, i140, i140, o357[CyclicAnalysis.field]o355) → f1320_0_appendNewList_LE(EOS, i140, i140, 1, o357[CyclicAnalysis.field]o355)
f1320_0_appendNewList_LE(EOS, i153, i153, matching1, o357[CyclicAnalysis.field]o355) → f1324_0_appendNewList_LE(EOS, i153, i153, 1, o357[CyclicAnalysis.field]o355) | =(matching1, 1)
f1324_0_appendNewList_LE(EOS, i153, i153, matching1, o357[CyclicAnalysis.field]o355) → f1329_0_appendNewList_Inc(EOS, i153, o357[CyclicAnalysis.field]o355) | &&(>(i153, 1), =(matching1, 1))
f1329_0_appendNewList_Inc(EOS, i153, o357[CyclicAnalysis.field]o355) → f1334_0_appendNewList_Load(EOS, +(i153, -1), o357[CyclicAnalysis.field]o355) | >(i153, 0)
f1334_0_appendNewList_Load(EOS, i154, o357[CyclicAnalysis.field]o355) → f1339_0_appendNewList_New(EOS, i154, o357[CyclicAnalysis.field]o355)
f1339_0_appendNewList_New(EOS, i154, o357[CyclicAnalysis.field]o355) → f1344_0_appendNewList_Duplicate(EOS, i154, o357[CyclicAnalysis.field]o355)
f1344_0_appendNewList_Duplicate(EOS, i154, o357[CyclicAnalysis.field]o355) → f1350_0_appendNewList_InvokeMethod(EOS, i154, o357[CyclicAnalysis.field]o355)
f1350_0_appendNewList_InvokeMethod(EOS, i154, o357[CyclicAnalysis.field]o355) → f1354_0__init__Load(EOS, i154, o357[CyclicAnalysis.field]o355)
f1354_0__init__Load(EOS, i154, o357[CyclicAnalysis.field]o355) → f1358_0__init__InvokeMethod(EOS, i154, o357[CyclicAnalysis.field]o355)
f1358_0__init__InvokeMethod(EOS, i154, o357[CyclicAnalysis.field]o355) → f1364_0__init__Return(EOS, i154, o357[CyclicAnalysis.field]o355)
f1364_0__init__Return(EOS, i154, o357[CyclicAnalysis.field]o355) → f1368_0_appendNewList_Duplicate(EOS, i154, o357[CyclicAnalysis.field]o355)
f1368_0_appendNewList_Duplicate(EOS, i154, o357[CyclicAnalysis.field]o355) → f1375_0_appendNewList_FieldAccess(EOS, i154, o357[CyclicAnalysis.field]o355)
f1375_0_appendNewList_FieldAccess(EOS, i154, o357[CyclicAnalysis.field]o355) → f1385_0_appendNewList_FieldAccess(EOS, i154, o357[CyclicAnalysis.field]o355) | >(o357[CyclicAnalysis.field]o355, 0)
f1375_0_appendNewList_FieldAccess(EOS, i154, o357[CyclicAnalysis.field]o355) → f1386_0_appendNewList_FieldAccess(EOS, i154)
f1385_0_appendNewList_FieldAccess(EOS, i154, o357[CyclicAnalysis.field]o355) → f1394_0_appendNewList_Store(EOS, i154, o357[CyclicAnalysis.field]o377) | =(o357[CyclicAnalysis.field]o377, +(o357[CyclicAnalysis.field]o355, 1))
f1394_0_appendNewList_Store(EOS, i154, o357[CyclicAnalysis.field]o377) → f1400_0_appendNewList_JMP(EOS, i154, o357[CyclicAnalysis.field]o377)
f1400_0_appendNewList_JMP(EOS, i154, o357[CyclicAnalysis.field]o377) → f1413_0_appendNewList_Load(EOS, i154, o357[CyclicAnalysis.field]o377)
f1413_0_appendNewList_Load(EOS, i154, o357[CyclicAnalysis.field]o377) → f1311_0_appendNewList_Load(EOS, i154, o357[CyclicAnalysis.field]o377)
f1311_0_appendNewList_Load(EOS, i140, o357[CyclicAnalysis.field]o355) → f1315_0_appendNewList_ConstantStackPush(EOS, i140, i140, o357[CyclicAnalysis.field]o355)
f1386_0_appendNewList_FieldAccess(EOS, i154) → f1398_0_appendNewList_Store(EOS, i154)
f1398_0_appendNewList_Store(EOS, i154) → f1403_0_appendNewList_JMP(EOS, i154)
f1403_0_appendNewList_JMP(EOS, i154) → f1414_0_appendNewList_Load(EOS, i154)
f1414_0_appendNewList_Load(EOS, i154) → f1311_0_appendNewList_Load(EOS, i154, o397[CyclicAnalysis.field]o377) | =(o397[CyclicAnalysis.field]o377, 1)

Combined rules. Obtained 2 IRules

P rules:
f1315_0_appendNewList_ConstantStackPush(EOS, x0, x0, x1) → f1315_0_appendNewList_ConstantStackPush(EOS, -(x0, 1), -(x0, 1), +(x1, 1)) | &&(>(x0, 1), >(x1, 0))
f1315_0_appendNewList_ConstantStackPush(EOS, x0, x0, x1) → f1315_0_appendNewList_ConstantStackPush(EOS, -(x0, 1), -(x0, 1), 1) | >(x0, 1)

Filtered ground terms:


f1315_0_appendNewList_ConstantStackPush(x1, x2, x3, x4) → f1315_0_appendNewList_ConstantStackPush(x2, x3, x4)
Cond_f1315_0_appendNewList_ConstantStackPush(x1, x2, x3, x4, x5) → Cond_f1315_0_appendNewList_ConstantStackPush(x1, x3, x4, x5)
Cond_f1315_0_appendNewList_ConstantStackPush1(x1, x2, x3, x4, x5) → Cond_f1315_0_appendNewList_ConstantStackPush1(x1, x3, x4, x5)

Filtered duplicate terms:


f1315_0_appendNewList_ConstantStackPush(x1, x2, x3) → f1315_0_appendNewList_ConstantStackPush(x2, x3)
Cond_f1315_0_appendNewList_ConstantStackPush(x1, x2, x3, x4) → Cond_f1315_0_appendNewList_ConstantStackPush(x1, x3, x4)
Cond_f1315_0_appendNewList_ConstantStackPush1(x1, x2, x3, x4) → Cond_f1315_0_appendNewList_ConstantStackPush1(x1, x3, x4)

Filtered unneeded terms:


Cond_f1315_0_appendNewList_ConstantStackPush1(x1, x2, x3) → Cond_f1315_0_appendNewList_ConstantStackPush1(x1, x2)

Prepared 2 rules for path length conversion:

P rules:
f1315_0_appendNewList_ConstantStackPush(x0, x1) → f1315_0_appendNewList_ConstantStackPush(-(x0, 1), +(x1, 1)) | &&(>(x0, 1), >(x1, 0))
f1315_0_appendNewList_ConstantStackPush(x0, x1) → f1315_0_appendNewList_ConstantStackPush(-(x0, 1), 1) | >(x0, 1)

Finished conversion. Obtained 2 rules.

P rules:
f1315_0_appendNewList_ConstantStackPush(x0, x1) → f1315_0_appendNewList_ConstantStackPush(-(x0, 1), +(x1, 1)) | &&(>(x0, 1), >(x1, 0))
f1315_0_appendNewList_ConstantStackPush(x2, x3) → f1315_0_appendNewList_ConstantStackPush(-(x2, 1), 1) | >(x2, 1)

(12) Obligation:

Rules:
f1315_0_appendNewList_ConstantStackPush(x0, x1) → f1315_0_appendNewList_ConstantStackPush(-(x0, 1), +(x1, 1)) | &&(>(x0, 1), >(x1, 0))
f1315_0_appendNewList_ConstantStackPush(x2, x3) → f1315_0_appendNewList_ConstantStackPush(-(x2, 1), 1) | >(x2, 1)

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f1315_0_appendNewList_ConstantStackPush(x5, x7)] = x5

Therefore the following rule(s) have been dropped:


f1315_0_appendNewList_ConstantStackPush(x0, x1) → f1315_0_appendNewList_ConstantStackPush(-(x0, 1), +(x1, 1)) | &&(>(x0, 1), >(x1, 0))
f1315_0_appendNewList_ConstantStackPush(x2, x3) → f1315_0_appendNewList_ConstantStackPush(-(x2, 1), 1) | >(x2, 1)

(14) YES

(15) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: CyclicAnalysis.CyclicAnalysis.main([Ljava/lang/String;)V
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:

(16) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 23 IRules

P rules:
f367_0_appendNewList_ConstantStackPush(EOS, i34, i34, o60[CyclicAnalysis.field]o58) → f371_0_appendNewList_LE(EOS, i34, i34, 1, o60[CyclicAnalysis.field]o58)
f371_0_appendNewList_LE(EOS, i48, i48, matching1, o60[CyclicAnalysis.field]o58) → f375_0_appendNewList_LE(EOS, i48, i48, 1, o60[CyclicAnalysis.field]o58) | =(matching1, 1)
f375_0_appendNewList_LE(EOS, i48, i48, matching1, o60[CyclicAnalysis.field]o58) → f380_0_appendNewList_Inc(EOS, i48, o60[CyclicAnalysis.field]o58) | &&(>(i48, 1), =(matching1, 1))
f380_0_appendNewList_Inc(EOS, i48, o60[CyclicAnalysis.field]o58) → f384_0_appendNewList_Load(EOS, +(i48, -1), o60[CyclicAnalysis.field]o58) | >(i48, 0)
f384_0_appendNewList_Load(EOS, i49, o60[CyclicAnalysis.field]o58) → f387_0_appendNewList_New(EOS, i49, o60[CyclicAnalysis.field]o58)
f387_0_appendNewList_New(EOS, i49, o60[CyclicAnalysis.field]o58) → f392_0_appendNewList_Duplicate(EOS, i49, o60[CyclicAnalysis.field]o58)
f392_0_appendNewList_Duplicate(EOS, i49, o60[CyclicAnalysis.field]o58) → f397_0_appendNewList_InvokeMethod(EOS, i49, o60[CyclicAnalysis.field]o58)
f397_0_appendNewList_InvokeMethod(EOS, i49, o60[CyclicAnalysis.field]o58) → f404_0__init__Load(EOS, i49, o60[CyclicAnalysis.field]o58)
f404_0__init__Load(EOS, i49, o60[CyclicAnalysis.field]o58) → f467_0__init__InvokeMethod(EOS, i49, o60[CyclicAnalysis.field]o58)
f467_0__init__InvokeMethod(EOS, i49, o60[CyclicAnalysis.field]o58) → f475_0__init__Return(EOS, i49, o60[CyclicAnalysis.field]o58)
f475_0__init__Return(EOS, i49, o60[CyclicAnalysis.field]o58) → f485_0_appendNewList_Duplicate(EOS, i49, o60[CyclicAnalysis.field]o58)
f485_0_appendNewList_Duplicate(EOS, i49, o60[CyclicAnalysis.field]o58) → f491_0_appendNewList_FieldAccess(EOS, i49, o60[CyclicAnalysis.field]o58)
f491_0_appendNewList_FieldAccess(EOS, i49, o60[CyclicAnalysis.field]o58) → f513_0_appendNewList_FieldAccess(EOS, i49, o60[CyclicAnalysis.field]o58) | >(o60[CyclicAnalysis.field]o58, 0)
f491_0_appendNewList_FieldAccess(EOS, i49, o60[CyclicAnalysis.field]o58) → f514_0_appendNewList_FieldAccess(EOS, i49)
f513_0_appendNewList_FieldAccess(EOS, i49, o60[CyclicAnalysis.field]o58) → f524_0_appendNewList_Store(EOS, i49, o60[CyclicAnalysis.field]o76) | =(o60[CyclicAnalysis.field]o76, +(o60[CyclicAnalysis.field]o58, 1))
f524_0_appendNewList_Store(EOS, i49, o60[CyclicAnalysis.field]o76) → f553_0_appendNewList_JMP(EOS, i49, o60[CyclicAnalysis.field]o76)
f553_0_appendNewList_JMP(EOS, i49, o60[CyclicAnalysis.field]o76) → f586_0_appendNewList_Load(EOS, i49, o60[CyclicAnalysis.field]o76)
f586_0_appendNewList_Load(EOS, i49, o60[CyclicAnalysis.field]o76) → f362_0_appendNewList_Load(EOS, i49, o60[CyclicAnalysis.field]o76)
f362_0_appendNewList_Load(EOS, i34, o60[CyclicAnalysis.field]o58) → f367_0_appendNewList_ConstantStackPush(EOS, i34, i34, o60[CyclicAnalysis.field]o58)
f514_0_appendNewList_FieldAccess(EOS, i49) → f531_0_appendNewList_Store(EOS, i49)
f531_0_appendNewList_Store(EOS, i49) → f557_0_appendNewList_JMP(EOS, i49)
f557_0_appendNewList_JMP(EOS, i49) → f601_0_appendNewList_Load(EOS, i49)
f601_0_appendNewList_Load(EOS, i49) → f362_0_appendNewList_Load(EOS, i49, o106[CyclicAnalysis.field]o76) | =(o106[CyclicAnalysis.field]o76, 1)

Combined rules. Obtained 2 IRules

P rules:
f367_0_appendNewList_ConstantStackPush(EOS, x0, x0, x1) → f367_0_appendNewList_ConstantStackPush(EOS, -(x0, 1), -(x0, 1), +(x1, 1)) | &&(>(x0, 1), >(x1, 0))
f367_0_appendNewList_ConstantStackPush(EOS, x0, x0, x1) → f367_0_appendNewList_ConstantStackPush(EOS, -(x0, 1), -(x0, 1), 1) | >(x0, 1)

Filtered ground terms:


f367_0_appendNewList_ConstantStackPush(x1, x2, x3, x4) → f367_0_appendNewList_ConstantStackPush(x2, x3, x4)
Cond_f367_0_appendNewList_ConstantStackPush(x1, x2, x3, x4, x5) → Cond_f367_0_appendNewList_ConstantStackPush(x1, x3, x4, x5)
Cond_f367_0_appendNewList_ConstantStackPush1(x1, x2, x3, x4, x5) → Cond_f367_0_appendNewList_ConstantStackPush1(x1, x3, x4, x5)

Filtered duplicate terms:


f367_0_appendNewList_ConstantStackPush(x1, x2, x3) → f367_0_appendNewList_ConstantStackPush(x2, x3)
Cond_f367_0_appendNewList_ConstantStackPush(x1, x2, x3, x4) → Cond_f367_0_appendNewList_ConstantStackPush(x1, x3, x4)
Cond_f367_0_appendNewList_ConstantStackPush1(x1, x2, x3, x4) → Cond_f367_0_appendNewList_ConstantStackPush1(x1, x3, x4)

Filtered unneeded terms:


Cond_f367_0_appendNewList_ConstantStackPush1(x1, x2, x3) → Cond_f367_0_appendNewList_ConstantStackPush1(x1, x2)

Prepared 2 rules for path length conversion:

P rules:
f367_0_appendNewList_ConstantStackPush(x0, x1) → f367_0_appendNewList_ConstantStackPush(-(x0, 1), +(x1, 1)) | &&(>(x0, 1), >(x1, 0))
f367_0_appendNewList_ConstantStackPush(x0, x1) → f367_0_appendNewList_ConstantStackPush(-(x0, 1), 1) | >(x0, 1)

Finished conversion. Obtained 2 rules.

P rules:
f367_0_appendNewList_ConstantStackPush(x0, x1) → f367_0_appendNewList_ConstantStackPush(-(x0, 1), +(x1, 1)) | &&(>(x0, 1), >(x1, 0))
f367_0_appendNewList_ConstantStackPush(x2, x3) → f367_0_appendNewList_ConstantStackPush(-(x2, 1), 1) | >(x2, 1)

(17) Obligation:

Rules:
f367_0_appendNewList_ConstantStackPush(x0, x1) → f367_0_appendNewList_ConstantStackPush(-(x0, 1), +(x1, 1)) | &&(>(x0, 1), >(x1, 0))
f367_0_appendNewList_ConstantStackPush(x2, x3) → f367_0_appendNewList_ConstantStackPush(-(x2, 1), 1) | >(x2, 1)

(18) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f367_0_appendNewList_ConstantStackPush(x5, x7)] = x5

Therefore the following rule(s) have been dropped:


f367_0_appendNewList_ConstantStackPush(x0, x1) → f367_0_appendNewList_ConstantStackPush(-(x0, 1), +(x1, 1)) | &&(>(x0, 1), >(x1, 0))
f367_0_appendNewList_ConstantStackPush(x2, x3) → f367_0_appendNewList_ConstantStackPush(-(x2, 1), 1) | >(x2, 1)

(19) YES