Termination of the given JBC could be proven:

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

(0) Obligation:

JBC Problem based on JBC Program:
public class BTreeR {
    private BTreeR left, right;

    public BTreeR(int height) {
	if (height > 1) {
	    this.left = new BTreeR(height - 1);
	    this.right = new BTreeR(height - 1);
	}
    }

    public int height() {
	if (left == null && right == null) return 1;
	else if (left == null) return 1 + right.height();
	else return 1 + left.height();
    }

    public static void main(String[] args) {
	Random.args = args;
	BTreeR bt = new BTreeR(Random.random()*Random.random()+10);
	bt.height();
    }
}


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

  public static int random() {
      if (index >= args.length)
	  return 0;

      String string = args[index];
      index++;
      return string.length();
  }
}


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

BTreeR.<init>(I)V: Graph of 37 nodes with 0 SCCs.

BTreeR.height()I: Graph of 80 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: BTreeR.height()I
SCC calls the following helper methods: BTreeR.height()I
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
    • BTreeR: [left, right]
  • Marker field analysis yielded the following relations that could be markers:

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 31 IRules

P rules:
f1203_0_height_FieldAccess(EOS, java.lang.Object(BTreeR(EOC, o585, o586)), java.lang.Object(BTreeR(EOC, o585, o586)), java.lang.Object(BTreeR(EOC, o585, o586))) → f1204_0_height_FieldAccess(EOS, java.lang.Object(BTreeR(EOC, o585, o586)), java.lang.Object(BTreeR(EOC, o585, o586)), java.lang.Object(BTreeR(EOC, o585, o586)))
f1204_0_height_FieldAccess(EOS, java.lang.Object(BTreeR(EOC, o585, o586)), java.lang.Object(BTreeR(EOC, o585, o586)), java.lang.Object(BTreeR(EOC, o585, o586))) → f1205_0_height_NONNULL(EOS, java.lang.Object(BTreeR(EOC, o585, o586)), java.lang.Object(BTreeR(EOC, o585, o586)), o585)
f1205_0_height_NONNULL(EOS, java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(o588sub)) → f1206_0_height_NONNULL(EOS, java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(o588sub))
f1205_0_height_NONNULL(EOS, java.lang.Object(BTreeR(EOC, NULL, o586)), java.lang.Object(BTreeR(EOC, NULL, o586)), NULL) → f1207_0_height_NONNULL(EOS, java.lang.Object(BTreeR(EOC, NULL, o586)), java.lang.Object(BTreeR(EOC, NULL, o586)), NULL)
f1206_0_height_NONNULL(EOS, java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(o588sub)) → f1208_0_height_Load(EOS, java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)))
f1208_0_height_Load(EOS, java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586))) → f1210_0_height_FieldAccess(EOS, java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)))
f1210_0_height_FieldAccess(EOS, java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586))) → f1212_0_height_NONNULL(EOS, java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(o588sub))
f1212_0_height_NONNULL(EOS, java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(o588sub)) → f1214_0_height_ConstantStackPush(EOS, java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)))
f1214_0_height_ConstantStackPush(EOS, java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586))) → f1218_0_height_Load(EOS, java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)))
f1218_0_height_Load(EOS, java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586))) → f1222_0_height_FieldAccess(EOS, java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)))
f1222_0_height_FieldAccess(EOS, java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586))) → f1227_0_height_InvokeMethod(EOS, java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(o588sub))
f1227_0_height_InvokeMethod(EOS, java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(o588sub)) → f1231_0_height_Load(EOS, java.lang.Object(o588sub), java.lang.Object(o588sub))
f1227_0_height_InvokeMethod(EOS, java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(o588sub)) → f1231_1_height_Load(EOS, java.lang.Object(BTreeR(EOC, java.lang.Object(o588sub), o586)), java.lang.Object(o588sub), java.lang.Object(o588sub))
f1231_0_height_Load(EOS, java.lang.Object(o588sub), java.lang.Object(o588sub)) → f1248_0_height_Load(EOS, java.lang.Object(o588sub), java.lang.Object(o588sub))
f1248_0_height_Load(EOS, java.lang.Object(o588sub), java.lang.Object(o588sub)) → f1200_0_height_Load(EOS, java.lang.Object(o588sub), java.lang.Object(o588sub))
f1200_0_height_Load(EOS, java.lang.Object(o580sub), java.lang.Object(o580sub)) → f1203_0_height_FieldAccess(EOS, java.lang.Object(o580sub), java.lang.Object(o580sub), java.lang.Object(o580sub))
f1207_0_height_NONNULL(EOS, java.lang.Object(BTreeR(EOC, NULL, o586)), java.lang.Object(BTreeR(EOC, NULL, o586)), NULL) → f1209_0_height_Load(EOS, java.lang.Object(BTreeR(EOC, NULL, o586)), java.lang.Object(BTreeR(EOC, NULL, o586)))
f1209_0_height_Load(EOS, java.lang.Object(BTreeR(EOC, NULL, o586)), java.lang.Object(BTreeR(EOC, NULL, o586))) → f1211_0_height_FieldAccess(EOS, java.lang.Object(BTreeR(EOC, NULL, o586)), java.lang.Object(BTreeR(EOC, NULL, o586)), java.lang.Object(BTreeR(EOC, NULL, o586)))
f1211_0_height_FieldAccess(EOS, java.lang.Object(BTreeR(EOC, NULL, o586)), java.lang.Object(BTreeR(EOC, NULL, o586)), java.lang.Object(BTreeR(EOC, NULL, o586))) → f1213_0_height_NONNULL(EOS, java.lang.Object(BTreeR(EOC, NULL, o586)), java.lang.Object(BTreeR(EOC, NULL, o586)), o586)
f1213_0_height_NONNULL(EOS, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(o590sub)) → f1216_0_height_NONNULL(EOS, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(o590sub))
f1216_0_height_NONNULL(EOS, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(o590sub)) → f1220_0_height_Load(EOS, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))))
f1220_0_height_Load(EOS, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub)))) → f1225_0_height_FieldAccess(EOS, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))))
f1225_0_height_FieldAccess(EOS, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub)))) → f1229_0_height_NONNULL(EOS, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), NULL)
f1229_0_height_NONNULL(EOS, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), NULL) → f1234_0_height_ConstantStackPush(EOS, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))))
f1234_0_height_ConstantStackPush(EOS, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub)))) → f1252_0_height_Load(EOS, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))))
f1252_0_height_Load(EOS, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub)))) → f1253_0_height_FieldAccess(EOS, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))))
f1253_0_height_FieldAccess(EOS, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub)))) → f1259_0_height_InvokeMethod(EOS, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(o590sub))
f1259_0_height_InvokeMethod(EOS, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(o590sub)) → f1261_0_height_Load(EOS, java.lang.Object(o590sub), java.lang.Object(o590sub))
f1259_0_height_InvokeMethod(EOS, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(o590sub)) → f1261_1_height_Load(EOS, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o590sub))), java.lang.Object(o590sub), java.lang.Object(o590sub))
f1261_0_height_Load(EOS, java.lang.Object(o590sub), java.lang.Object(o590sub)) → f1263_0_height_Load(EOS, java.lang.Object(o590sub), java.lang.Object(o590sub))
f1263_0_height_Load(EOS, java.lang.Object(o590sub), java.lang.Object(o590sub)) → f1200_0_height_Load(EOS, java.lang.Object(o590sub), java.lang.Object(o590sub))

Combined rules. Obtained 4 IRules

P rules:
f1203_0_height_FieldAccess(EOS, java.lang.Object(BTreeR(EOC, java.lang.Object(x0), x1)), java.lang.Object(BTreeR(EOC, java.lang.Object(x0), x1)), java.lang.Object(BTreeR(EOC, java.lang.Object(x0), x1))) → f1231_1_height_Load(EOS, java.lang.Object(BTreeR(EOC, java.lang.Object(x0), x1)), java.lang.Object(x0), java.lang.Object(x0))
f1203_0_height_FieldAccess(EOS, java.lang.Object(BTreeR(EOC, java.lang.Object(x0), x1)), java.lang.Object(BTreeR(EOC, java.lang.Object(x0), x1)), java.lang.Object(BTreeR(EOC, java.lang.Object(x0), x1))) → f1203_0_height_FieldAccess(EOS, java.lang.Object(x0), java.lang.Object(x0), java.lang.Object(x0))
f1203_0_height_FieldAccess(EOS, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(x0))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(x0))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(x0)))) → f1261_1_height_Load(EOS, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(x0))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(x0))), java.lang.Object(x0), java.lang.Object(x0))
f1203_0_height_FieldAccess(EOS, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(x0))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(x0))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(x0)))) → f1203_0_height_FieldAccess(EOS, java.lang.Object(x0), java.lang.Object(x0), java.lang.Object(x0))

Filtered ground terms:


f1203_0_height_FieldAccess(x1, x2, x3, x4) → f1203_0_height_FieldAccess(x2, x3, x4)
f1231_1_height_Load(x1, x2, x3, x4) → f1231_1_height_Load(x2, x3, x4)
f1261_1_height_Load(x1, x2, x3, x4, x5) → f1261_1_height_Load(x2, x3, x4, x5)
BTreeR(x1, x2, x3) → BTreeR(x2, x3)

Filtered duplicate terms:


f1203_0_height_FieldAccess(x1, x2, x3) → f1203_0_height_FieldAccess(x3)
f1231_1_height_Load(x1, x2, x3) → f1231_1_height_Load(x1)
f1261_1_height_Load(x1, x2, x3, x4) → f1261_1_height_Load(x2)

Prepared 4 rules for path length conversion:

P rules:
f1203_0_height_FieldAccess(java.lang.Object(BTreeR(java.lang.Object(x0), x1))) → f1231_1_height_Load(java.lang.Object(BTreeR(java.lang.Object(x0), x1)))
f1203_0_height_FieldAccess(java.lang.Object(BTreeR(java.lang.Object(x0), x1))) → f1203_0_height_FieldAccess(java.lang.Object(x0))
f1203_0_height_FieldAccess(java.lang.Object(BTreeR(NULL, java.lang.Object(x0)))) → f1261_1_height_Load(java.lang.Object(BTreeR(NULL, java.lang.Object(x0))))
f1203_0_height_FieldAccess(java.lang.Object(BTreeR(NULL, java.lang.Object(x0)))) → f1203_0_height_FieldAccess(java.lang.Object(x0))

Finished conversion. Obtained 2 rules.

P rules:
f1203_0_height_FieldAccess(v7) → f1203_0_height_FieldAccess(v8) | &&(&&(>(+(v8, 1), 1), <=(+(v8, 2), v7)), >(+(v7, 1), 3))
f1203_0_height_FieldAccess(v9) → f1203_0_height_FieldAccess(v10) | &&(&&(>=(v9, +(v10, 2)), >(+(v9, 1), 3)), >(+(v10, 1), 1))

(7) Obligation:

Rules:
f1203_0_height_FieldAccess(v7) → f1203_0_height_FieldAccess(v8) | &&(&&(>(+(v8, 1), 1), <=(+(v8, 2), v7)), >(+(v7, 1), 3))
f1203_0_height_FieldAccess(v9) → f1203_0_height_FieldAccess(v10) | &&(&&(>=(v9, +(v10, 2)), >(+(v9, 1), 3)), >(+(v10, 1), 1))

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f1203_0_height_FieldAccess(x5)] = x5

Therefore the following rule(s) have been dropped:


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

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: BTreeR.<init>(I)V
SCC calls the following helper methods: BTreeR.<init>(I)V
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 32 IRules

P rules:
f532_0__init__InvokeMethod(EOS, i69, i69) → f536_0__init__Load(EOS, i69, i69)
f536_0__init__Load(EOS, i69, i69) → f540_0__init__ConstantStackPush(EOS, i69, i69, i69)
f540_0__init__ConstantStackPush(EOS, i69, i69, i69) → f548_0__init__LE(EOS, i69, i69, i69, 1)
f548_0__init__LE(EOS, i73, i73, i73, matching1) → f554_0__init__LE(EOS, i73, i73, i73, 1) | =(matching1, 1)
f554_0__init__LE(EOS, i73, i73, i73, matching1) → f563_0__init__Load(EOS, i73, i73) | &&(>(i73, 1), =(matching1, 1))
f563_0__init__Load(EOS, i73, i73) → f570_0__init__New(EOS, i73, i73)
f570_0__init__New(EOS, i73, i73) → f598_0__init__Duplicate(EOS, i73, i73)
f598_0__init__Duplicate(EOS, i73, i73) → f601_0__init__Load(EOS, i73, i73)
f601_0__init__Load(EOS, i73, i73) → f604_0__init__ConstantStackPush(EOS, i73, i73, i73)
f604_0__init__ConstantStackPush(EOS, i73, i73, i73) → f607_0__init__IntArithmetic(EOS, i73, i73, i73, 1)
f607_0__init__IntArithmetic(EOS, i73, i73, i73, matching1) → f609_0__init__InvokeMethod(EOS, i73, i73, -(i73, 1)) | &&(>(i73, 0), =(matching1, 1))
f609_0__init__InvokeMethod(EOS, i73, i73, i88) → f610_0__init__Load(EOS, i88, i88)
f609_0__init__InvokeMethod(EOS, i73, i73, i88) → f610_1__init__Load(EOS, i73, i73, i88, i88)
f610_0__init__Load(EOS, i88, i88) → f612_0__init__Load(EOS, i88, i88)
f612_0__init__Load(EOS, i88, i88) → f527_0__init__Load(EOS, i88, i88)
f527_0__init__Load(EOS, i69, i69) → f532_0__init__InvokeMethod(EOS, i69, i69)
f630_0__init__Return(EOS, i73, i73, matching1) → f757_0__init__Return(EOS, i73, i73, 1) | =(matching1, 1)
f757_0__init__Return(EOS, i73, i73, i151) → f762_0__init__FieldAccess(EOS, i73, i73)
f762_0__init__FieldAccess(EOS, i73, i73) → f766_0__init__Load(EOS, i73, i73)
f766_0__init__Load(EOS, i73, i73) → f770_0__init__New(EOS, i73, i73)
f770_0__init__New(EOS, i73, i73) → f772_0__init__Duplicate(EOS, i73, i73)
f772_0__init__Duplicate(EOS, i73, i73) → f774_0__init__Load(EOS, i73, i73)
f774_0__init__Load(EOS, i73, i73) → f778_0__init__ConstantStackPush(EOS, i73, i73)
f778_0__init__ConstantStackPush(EOS, i73, i73) → f780_0__init__IntArithmetic(EOS, i73, i73, 1)
f780_0__init__IntArithmetic(EOS, i73, i73, matching1) → f783_0__init__InvokeMethod(EOS, i73, -(i73, 1)) | &&(>(i73, 0), =(matching1, 1))
f783_0__init__InvokeMethod(EOS, i73, i158) → f786_0__init__Load(EOS, i158, i158)
f783_0__init__InvokeMethod(EOS, i73, i158) → f786_1__init__Load(EOS, i73, i158, i158)
f786_0__init__Load(EOS, i158, i158) → f791_0__init__Load(EOS, i158, i158)
f791_0__init__Load(EOS, i158, i158) → f527_0__init__Load(EOS, i158, i158)
f1050_0__init__Return(EOS, i73, i73, i265) → f757_0__init__Return(EOS, i73, i73, i265)
f610_1__init__Load(EOS, i73, i73, matching1, matching2) → f630_0__init__Return(EOS, i73, i73, 1) | &&(=(matching1, 1), =(matching2, 1))
f610_1__init__Load(EOS, i73, i73, i265, i265) → f1050_0__init__Return(EOS, i73, i73, i265)

Combined rules. Obtained 5 IRules

P rules:
f783_0__init__InvokeMethod(EOS, i73, i158) → f786_1__init__Load(EOS, i73, i158, i158)
f532_0__init__InvokeMethod(EOS, x0, x0) → f532_0__init__InvokeMethod(EOS, -(x0, 1), -(x0, 1)) | >(x0, 1)
f783_0__init__InvokeMethod(EOS, x0, x1) → f532_0__init__InvokeMethod(EOS, x1, x1)
f532_0__init__InvokeMethod(EOS, 2, 2) → f783_0__init__InvokeMethod(EOS, 2, 1)
f532_0__init__InvokeMethod(EOS, x0, x0) → f783_0__init__InvokeMethod(EOS, x0, -(x0, 1)) | >(x0, 1)

Filtered ground terms:


f783_0__init__InvokeMethod(x1, x2, x3) → f783_0__init__InvokeMethod(x2, x3)
f786_1__init__Load(x1, x2, x3, x4) → f786_1__init__Load(x2, x3, x4)
f532_0__init__InvokeMethod(x1, x2, x3) → f532_0__init__InvokeMethod(x2, x3)
Cond_f532_0__init__InvokeMethod(x1, x2, x3, x4) → Cond_f532_0__init__InvokeMethod(x1, x3, x4)
Cond_f532_0__init__InvokeMethod1(x1, x2, x3, x4) → Cond_f532_0__init__InvokeMethod1(x1, x3, x4)

Filtered duplicate terms:


f786_1__init__Load(x1, x2, x3) → f786_1__init__Load(x1, x3)
f532_0__init__InvokeMethod(x1, x2) → f532_0__init__InvokeMethod(x2)
Cond_f532_0__init__InvokeMethod(x1, x2, x3) → Cond_f532_0__init__InvokeMethod(x1, x3)
Cond_f532_0__init__InvokeMethod1(x1, x2, x3) → Cond_f532_0__init__InvokeMethod1(x1, x3)

Filtered unneeded terms:


f783_0__init__InvokeMethod(x1, x2) → f783_0__init__InvokeMethod(x2)

Prepared 5 rules for path length conversion:

P rules:
f783_0__init__InvokeMethod(i158) → f786_1__init__Load(i73, i158)
f532_0__init__InvokeMethod(x0) → f532_0__init__InvokeMethod(-(x0, 1)) | >(x0, 1)
f783_0__init__InvokeMethod(x1) → f532_0__init__InvokeMethod(x1)
f532_0__init__InvokeMethod(2) → f783_0__init__InvokeMethod(1)
f532_0__init__InvokeMethod(x0) → f783_0__init__InvokeMethod(-(x0, 1)) | >(x0, 1)

Finished conversion. Obtained 4 rules.

P rules:
f532_0__init__InvokeMethod(x2) → f532_0__init__InvokeMethod(-(x2, 1)) | >(x2, 1)
f783_0__init__InvokeMethod(x3) → f532_0__init__InvokeMethod(x3)
f532_0__init__InvokeMethod(c2) → f783_0__init__InvokeMethod(1) | =(2, c2)
f532_0__init__InvokeMethod(x4) → f783_0__init__InvokeMethod(-(x4, 1)) | >(x4, 1)

(12) Obligation:

Rules:
f532_0__init__InvokeMethod(x2) → f532_0__init__InvokeMethod(-(x2, 1)) | >(x2, 1)
f783_0__init__InvokeMethod(x3) → f532_0__init__InvokeMethod(x3)
f532_0__init__InvokeMethod(c2) → f783_0__init__InvokeMethod(1) | =(2, c2)
f532_0__init__InvokeMethod(x4) → f783_0__init__InvokeMethod(-(x4, 1)) | >(x4, 1)

(13) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:


[f532_0__init__InvokeMethod(x5)] = -1 + x5
[f783_0__init__InvokeMethod(x8)] = -1 + x8

Therefore the following rule(s) have been dropped:


f532_0__init__InvokeMethod(x0) → f532_0__init__InvokeMethod(-(x0, 1)) | >(x0, 1)
f532_0__init__InvokeMethod(x2) → f783_0__init__InvokeMethod(1) | =(2, x2)
f532_0__init__InvokeMethod(x3) → f783_0__init__InvokeMethod(-(x3, 1)) | >(x3, 1)

(14) Obligation:

Rules:
f783_0__init__InvokeMethod(x1) → f532_0__init__InvokeMethod(x1) | TRUE

(15) TerminationGraphProcessor (EQUIVALENT transformation)

Constructed the termination graph and obtained no non-trivial SCC(s).


(16) YES