Termination of the given JBC could be proven:

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

(0) Obligation:

JBC Problem based on JBC Program:
package SharingAnalysisRec;

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

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


package SharingAnalysisRec;

public class SharingAnalysisRec {
	int val;
	SharingAnalysisRec field;

	public static void main(String[] args) {
		Random.args = args;
		SharingAnalysisRec t1 = new SharingAnalysisRec();
		SharingAnalysisRec t2 = t1.appendNewList(1);
		SharingAnalysisRec t3 = t2.appendNewList(Random.random());
		t2.field = null;
		copy(t1, t3);
	}

	public static void copy(SharingAnalysisRec source, SharingAnalysisRec target) {
		if (source == null) {
			return;
		} else {
			SharingAnalysisRec newEle = new SharingAnalysisRec();
			newEle.val = source.val;
			target.field = newEle;
			copy(source.field, newEle);
		}
	}

	/**
 	 * @param i number of elements to append
 	 * @return the last list element appended
 	 */
	private SharingAnalysisRec appendNewList(int i) {
		this.field = new SharingAnalysisRec();
		this.val = Random.random();
		if (i <= 1) {
			return this.field;
		} else {
			return this.field.appendNewList(i-1);
		}
	}
}


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

SharingAnalysisRec.SharingAnalysisRec.appendNewList(I)LSharingAnalysisRec/SharingAnalysisRec;: Graph of 113 nodes with 0 SCCs.

SharingAnalysisRec.SharingAnalysisRec.copy(LSharingAnalysisRec/SharingAnalysisRec;LSharingAnalysisRec/SharingAnalysisRec;)V: Graph of 35 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: SharingAnalysisRec.SharingAnalysisRec.copy(LSharingAnalysisRec/SharingAnalysisRec;LSharingAnalysisRec/SharingAnalysisRec;)V
SCC calls the following helper methods: SharingAnalysisRec.SharingAnalysisRec.copy(LSharingAnalysisRec/SharingAnalysisRec;LSharingAnalysisRec/SharingAnalysisRec;)V
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
    • SharingAnalysisRec.SharingAnalysisRec: [val, 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 25 IRules

P rules:
f2540_0_copy_NONNULL(EOS, java.lang.Object(o882sub), java.lang.Object(o882sub), java.lang.Object(o882sub)) → f2542_0_copy_NONNULL(EOS, java.lang.Object(o882sub), java.lang.Object(o882sub), java.lang.Object(o882sub))
f2542_0_copy_NONNULL(EOS, java.lang.Object(o882sub), java.lang.Object(o882sub), java.lang.Object(o882sub)) → f2545_0_copy_New(EOS, java.lang.Object(o882sub), java.lang.Object(o882sub))
f2545_0_copy_New(EOS, java.lang.Object(o882sub), java.lang.Object(o882sub)) → f2547_0_copy_Duplicate(EOS, java.lang.Object(o882sub), java.lang.Object(o882sub))
f2547_0_copy_Duplicate(EOS, java.lang.Object(o882sub), java.lang.Object(o882sub)) → f2550_0_copy_InvokeMethod(EOS, java.lang.Object(o882sub), java.lang.Object(o882sub))
f2550_0_copy_InvokeMethod(EOS, java.lang.Object(o882sub), java.lang.Object(o882sub)) → f2556_0__init__Load(EOS, java.lang.Object(o882sub), java.lang.Object(o882sub))
f2556_0__init__Load(EOS, java.lang.Object(o882sub), java.lang.Object(o882sub)) → f2558_0__init__InvokeMethod(EOS, java.lang.Object(o882sub), java.lang.Object(o882sub))
f2558_0__init__InvokeMethod(EOS, java.lang.Object(o882sub), java.lang.Object(o882sub)) → f2559_0__init__Return(EOS, java.lang.Object(o882sub), java.lang.Object(o882sub))
f2559_0__init__Return(EOS, java.lang.Object(o882sub), java.lang.Object(o882sub)) → f2560_0_copy_Store(EOS, java.lang.Object(o882sub), java.lang.Object(o882sub))
f2560_0_copy_Store(EOS, java.lang.Object(o882sub), java.lang.Object(o882sub)) → f2561_0_copy_Load(EOS, java.lang.Object(o882sub), java.lang.Object(o882sub))
f2561_0_copy_Load(EOS, java.lang.Object(o882sub), java.lang.Object(o882sub)) → f2563_0_copy_Load(EOS, java.lang.Object(o882sub), java.lang.Object(o882sub))
f2563_0_copy_Load(EOS, java.lang.Object(o882sub), java.lang.Object(o882sub)) → f2564_0_copy_FieldAccess(EOS, java.lang.Object(o882sub), java.lang.Object(o882sub), java.lang.Object(o882sub))
f2564_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)), java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)), java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893))) → f2565_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)), java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)), java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)))
f2565_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)), java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)), java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893))) → f2566_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)), java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)))
f2566_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)), java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893))) → f2567_0_copy_Load(EOS, java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)), java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)))
f2567_0_copy_Load(EOS, java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)), java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893))) → f2568_0_copy_Load(EOS, java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)), java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)))
f2568_0_copy_Load(EOS, java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)), java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893))) → f2569_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)), java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)))
f2569_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)), java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893))) → f2570_0_copy_Load(EOS, java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)), java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)))
f2570_0_copy_Load(EOS, java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)), java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893))) → f2571_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)), java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)))
f2571_0_copy_FieldAccess(EOS, java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)), java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893))) → f2572_0_copy_Load(EOS, java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)), o893)
f2572_0_copy_Load(EOS, java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)), o893) → f2573_0_copy_InvokeMethod(EOS, java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)), o893)
f2573_0_copy_InvokeMethod(EOS, java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)), o893) → f2574_0_copy_Load(EOS, o893, o893)
f2573_0_copy_InvokeMethod(EOS, java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)), o893) → f2574_1_copy_Load(EOS, java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, i775, o893)), o893, o893)
f2574_0_copy_Load(EOS, o893, o893) → f2575_0_copy_Load(EOS, o893, o893)
f2575_0_copy_Load(EOS, o893, o893) → f2539_0_copy_Load(EOS, o893, o893)
f2539_0_copy_Load(EOS, o879, o879) → f2540_0_copy_NONNULL(EOS, o879, o879, o879)

Combined rules. Obtained 2 IRules

P rules:
f2540_0_copy_NONNULL(EOS, java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, x0, x1)), java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, x0, x1)), java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, x0, x1))) → f2574_1_copy_Load(EOS, java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, x0, x1)), x1, x1)
f2540_0_copy_NONNULL(EOS, java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, x0, x1)), java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, x0, x1)), java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(EOC, x0, x1))) → f2540_0_copy_NONNULL(EOS, x1, x1, x1)

Filtered ground terms:


f2540_0_copy_NONNULL(x1, x2, x3, x4) → f2540_0_copy_NONNULL(x2, x3, x4)
f2574_1_copy_Load(x1, x2, x3, x4) → f2574_1_copy_Load(x2, x3, x4)
SharingAnalysisRec.SharingAnalysisRec(x1, x2, x3) → SharingAnalysisRec.SharingAnalysisRec(x2, x3)

Filtered duplicate terms:


f2540_0_copy_NONNULL(x1, x2, x3) → f2540_0_copy_NONNULL(x3)
f2574_1_copy_Load(x1, x2, x3) → f2574_1_copy_Load(x1)

Filtered unneeded terms:


SharingAnalysisRec.SharingAnalysisRec(x1, x2) → SharingAnalysisRec.SharingAnalysisRec(x2)

Prepared 2 rules for path length conversion:

P rules:
f2540_0_copy_NONNULL(java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(x1))) → f2574_1_copy_Load(java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(x1)))
f2540_0_copy_NONNULL(java.lang.Object(SharingAnalysisRec.SharingAnalysisRec(x1))) → f2540_0_copy_NONNULL(x1)

Finished conversion. Obtained 1 rules.

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

(7) Obligation:

Rules:
f2540_0_copy_NONNULL(v3) → f2540_0_copy_NONNULL(v4) | &&(&&(>(+(v4, 1), 0), <=(+(v4, 1), v3)), >(+(v3, 1), 1))

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f2540_0_copy_NONNULL(x3)] = x3

Therefore the following rule(s) have been dropped:


f2540_0_copy_NONNULL(x0) → f2540_0_copy_NONNULL(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: SharingAnalysisRec.SharingAnalysisRec.appendNewList(I)LSharingAnalysisRec/SharingAnalysisRec;
SCC calls the following helper methods: SharingAnalysisRec.SharingAnalysisRec.appendNewList(I)LSharingAnalysisRec/SharingAnalysisRec;
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
    • java.lang.String: [count]
    • SharingAnalysisRec.SharingAnalysisRec: [field]
  • Marker field analysis yielded the following relations that could be markers:

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 41 IRules

P rules:
f1216_0_appendNewList_New(EOS, i176, i176) → f1218_0_appendNewList_Duplicate(EOS, i176, i176)
f1218_0_appendNewList_Duplicate(EOS, i176, i176) → f1220_0_appendNewList_InvokeMethod(EOS, i176, i176)
f1220_0_appendNewList_InvokeMethod(EOS, i176, i176) → f1224_0__init__Load(EOS, i176, i176)
f1224_0__init__Load(EOS, i176, i176) → f1230_0__init__InvokeMethod(EOS, i176, i176)
f1230_0__init__InvokeMethod(EOS, i176, i176) → f1236_0__init__Return(EOS, i176, i176)
f1236_0__init__Return(EOS, i176, i176) → f1238_0_appendNewList_FieldAccess(EOS, i176, i176)
f1238_0_appendNewList_FieldAccess(EOS, i176, i176) → f1243_0_appendNewList_Load(EOS, i176, i176)
f1243_0_appendNewList_Load(EOS, i176, i176) → f1246_0_appendNewList_InvokeMethod(EOS, i176, i176)
f1246_0_appendNewList_InvokeMethod(EOS, i176, i176) → f1249_0_random_FieldAccess(EOS, i176, i176)
f1249_0_random_FieldAccess(EOS, i176, i176) → f1254_0_random_FieldAccess(EOS, i176, i176, java.lang.Object(ARRAY(i126)))
f1254_0_random_FieldAccess(EOS, i176, i176, java.lang.Object(ARRAY(i126))) → f1259_0_random_ArrayAccess(EOS, i176, i176, java.lang.Object(ARRAY(i126)), i175)
f1259_0_random_ArrayAccess(EOS, i176, i176, java.lang.Object(ARRAY(i126)), i175) → f1265_0_random_ArrayAccess(EOS, i176, i176, java.lang.Object(ARRAY(i126)), i175)
f1265_0_random_ArrayAccess(EOS, i176, i176, java.lang.Object(ARRAY(i126)), i175) → f1269_0_random_Store(EOS, i176, i176, o234) | <(i175, i126)
f1269_0_random_Store(EOS, i176, i176, o234) → f1276_0_random_FieldAccess(EOS, i176, i176, o234)
f1276_0_random_FieldAccess(EOS, i176, i176, o234) → f1282_0_random_ConstantStackPush(EOS, i176, i176, o234, i175)
f1282_0_random_ConstantStackPush(EOS, i176, i176, o234, i175) → f1291_0_random_IntArithmetic(EOS, i176, i176, o234, i175, 1)
f1291_0_random_IntArithmetic(EOS, i176, i176, o234, i175, matching1) → f1295_0_random_FieldAccess(EOS, i176, i176, o234, +(i175, 1)) | &&(>=(i175, 0), =(matching1, 1))
f1295_0_random_FieldAccess(EOS, i176, i176, o234, i188) → f1297_0_random_Load(EOS, i176, i176, o234)
f1297_0_random_Load(EOS, i176, i176, o234) → f1308_0_random_InvokeMethod(EOS, i176, i176, o234)
f1308_0_random_InvokeMethod(EOS, i176, i176, java.lang.Object(o240sub)) → f1317_0_random_InvokeMethod(EOS, i176, i176, java.lang.Object(o240sub))
f1317_0_random_InvokeMethod(EOS, i176, i176, java.lang.Object(o240sub)) → f1324_0_length_Load(EOS, i176, i176, java.lang.Object(o240sub), java.lang.Object(o240sub))
f1324_0_length_Load(EOS, i176, i176, java.lang.Object(o240sub), java.lang.Object(o240sub)) → f1339_0_length_FieldAccess(EOS, i176, i176, java.lang.Object(o240sub), java.lang.Object(o240sub))
f1339_0_length_FieldAccess(EOS, i176, i176, java.lang.Object(java.lang.String(o249sub, i201)), java.lang.Object(java.lang.String(o249sub, i201))) → f1351_0_length_FieldAccess(EOS, i176, i176, java.lang.Object(java.lang.String(o249sub, i201)), java.lang.Object(java.lang.String(o249sub, i201)))
f1351_0_length_FieldAccess(EOS, i176, i176, java.lang.Object(java.lang.String(o249sub, i201)), java.lang.Object(java.lang.String(o249sub, i201))) → f1359_0_length_Return(EOS, i176, i176, java.lang.Object(java.lang.String(o249sub, i201)))
f1359_0_length_Return(EOS, i176, i176, java.lang.Object(java.lang.String(o249sub, i201))) → f1370_0_random_Return(EOS, i176, i176)
f1370_0_random_Return(EOS, i176, i176) → f1377_0_appendNewList_FieldAccess(EOS, i176, i176)
f1377_0_appendNewList_FieldAccess(EOS, i176, i176) → f1388_0_appendNewList_Load(EOS, i176, i176)
f1388_0_appendNewList_Load(EOS, i176, i176) → f1400_0_appendNewList_ConstantStackPush(EOS, i176, i176, i176)
f1400_0_appendNewList_ConstantStackPush(EOS, i176, i176, i176) → f1409_0_appendNewList_GT(EOS, i176, i176, i176, 1)
f1409_0_appendNewList_GT(EOS, i211, i211, i211, matching1) → f1423_0_appendNewList_GT(EOS, i211, i211, i211, 1) | =(matching1, 1)
f1423_0_appendNewList_GT(EOS, i211, i211, i211, matching1) → f1437_0_appendNewList_Load(EOS, i211, i211) | &&(>(i211, 1), =(matching1, 1))
f1437_0_appendNewList_Load(EOS, i211, i211) → f1443_0_appendNewList_FieldAccess(EOS, i211, i211)
f1443_0_appendNewList_FieldAccess(EOS, i211, i211) → f1450_0_appendNewList_Load(EOS, i211, i211)
f1450_0_appendNewList_Load(EOS, i211, i211) → f1454_0_appendNewList_ConstantStackPush(EOS, i211, i211)
f1454_0_appendNewList_ConstantStackPush(EOS, i211, i211) → f1489_0_appendNewList_IntArithmetic(EOS, i211, i211, 1)
f1489_0_appendNewList_IntArithmetic(EOS, i211, i211, matching1) → f1499_0_appendNewList_InvokeMethod(EOS, i211, -(i211, 1)) | &&(>(i211, 0), =(matching1, 1))
f1499_0_appendNewList_InvokeMethod(EOS, i211, i231) → f1513_0_appendNewList_Load(EOS, i231, i231)
f1499_0_appendNewList_InvokeMethod(EOS, i211, i231) → f1513_1_appendNewList_Load(EOS, i211, i231, i231)
f1513_0_appendNewList_Load(EOS, i231, i231) → f1526_0_appendNewList_Load(EOS, i231, i231)
f1526_0_appendNewList_Load(EOS, i231, i231) → f1210_0_appendNewList_Load(EOS, i231, i231)
f1210_0_appendNewList_Load(EOS, i176, i176) → f1216_0_appendNewList_New(EOS, i176, i176)

Combined rules. Obtained 2 IRules

P rules:
f1216_0_appendNewList_New(EOS, x0, x0) → f1513_1_appendNewList_Load(EOS, x0, -(x0, 1), -(x0, 1)) | >(x0, 1)
f1216_0_appendNewList_New(EOS, x0, x0) → f1216_0_appendNewList_New(EOS, -(x0, 1), -(x0, 1)) | >(x0, 1)

Filtered ground terms:


f1216_0_appendNewList_New(x1, x2, x3) → f1216_0_appendNewList_New(x2, x3)
Cond_f1216_0_appendNewList_New(x1, x2, x3, x4) → Cond_f1216_0_appendNewList_New(x1, x3, x4)
f1513_1_appendNewList_Load(x1, x2, x3, x4) → f1513_1_appendNewList_Load(x2, x3, x4)
Cond_f1216_0_appendNewList_New1(x1, x2, x3, x4) → Cond_f1216_0_appendNewList_New1(x1, x3, x4)

Filtered duplicate terms:


f1216_0_appendNewList_New(x1, x2) → f1216_0_appendNewList_New(x2)
Cond_f1216_0_appendNewList_New(x1, x2, x3) → Cond_f1216_0_appendNewList_New(x1, x3)
f1513_1_appendNewList_Load(x1, x2, x3) → f1513_1_appendNewList_Load(x3)
Cond_f1216_0_appendNewList_New1(x1, x2, x3) → Cond_f1216_0_appendNewList_New1(x1, x3)

Filtered unneeded terms:


Cond_f1216_0_appendNewList_New(x1, x2) → Cond_f1216_0_appendNewList_New(x1)

Prepared 2 rules for path length conversion:

P rules:
f1216_0_appendNewList_New(x0) → f1513_1_appendNewList_Load(-(x0, 1)) | >(x0, 1)
f1216_0_appendNewList_New(x0) → f1216_0_appendNewList_New(-(x0, 1)) | >(x0, 1)

Finished conversion. Obtained 1 rules.

P rules:
f1216_0_appendNewList_New(x1) → f1216_0_appendNewList_New(-(x1, 1)) | >(x1, 1)

(12) Obligation:

Rules:
f1216_0_appendNewList_New(x1) → f1216_0_appendNewList_New(-(x1, 1)) | >(x1, 1)

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f1216_0_appendNewList_New(x2)] = x2

Therefore the following rule(s) have been dropped:


f1216_0_appendNewList_New(x0) → f1216_0_appendNewList_New(-(x0, 1)) | >(x0, 1)

(14) YES