(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_20 (Apple Inc.) Main-Class: BTreeR
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: UsedFieldsAnalysis

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 29 rules for P and 53 rules for R.


P rules:
935_0_height_FieldAccess(EOS(STATIC_935), java.lang.Object(BTreeR(EOC, o336, o337)), java.lang.Object(BTreeR(EOC, o336, o337))) → 938_0_height_FieldAccess(EOS(STATIC_938), java.lang.Object(BTreeR(EOC, o336, o337)), java.lang.Object(BTreeR(EOC, o336, o337)))
938_0_height_FieldAccess(EOS(STATIC_938), java.lang.Object(BTreeR(EOC, o336, o337)), java.lang.Object(BTreeR(EOC, o336, o337))) → 939_0_height_NONNULL(EOS(STATIC_939), java.lang.Object(BTreeR(EOC, o336, o337)), o336)
939_0_height_NONNULL(EOS(STATIC_939), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337)), java.lang.Object(o339sub)) → 941_0_height_NONNULL(EOS(STATIC_941), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337)), java.lang.Object(o339sub))
939_0_height_NONNULL(EOS(STATIC_939), java.lang.Object(BTreeR(EOC, NULL, o337)), NULL) → 942_0_height_NONNULL(EOS(STATIC_942), java.lang.Object(BTreeR(EOC, NULL, o337)), NULL)
941_0_height_NONNULL(EOS(STATIC_941), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337)), java.lang.Object(o339sub)) → 943_0_height_Load(EOS(STATIC_943), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337)))
943_0_height_Load(EOS(STATIC_943), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337))) → 946_0_height_FieldAccess(EOS(STATIC_946), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337)), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337)))
946_0_height_FieldAccess(EOS(STATIC_946), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337)), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337))) → 948_0_height_NONNULL(EOS(STATIC_948), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337)), java.lang.Object(o339sub))
948_0_height_NONNULL(EOS(STATIC_948), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337)), java.lang.Object(o339sub)) → 951_0_height_ConstantStackPush(EOS(STATIC_951), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337)))
951_0_height_ConstantStackPush(EOS(STATIC_951), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337))) → 955_0_height_Load(EOS(STATIC_955), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337)))
955_0_height_Load(EOS(STATIC_955), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337))) → 959_0_height_FieldAccess(EOS(STATIC_959), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337)))
959_0_height_FieldAccess(EOS(STATIC_959), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337))) → 962_0_height_InvokeMethod(EOS(STATIC_962), java.lang.Object(o339sub))
962_0_height_InvokeMethod(EOS(STATIC_962), java.lang.Object(o339sub)) → 965_1_height_InvokeMethod(965_0_height_Load(EOS(STATIC_965), java.lang.Object(o339sub)), java.lang.Object(o339sub))
965_0_height_Load(EOS(STATIC_965), java.lang.Object(o339sub)) → 971_0_height_Load(EOS(STATIC_971), java.lang.Object(o339sub))
971_0_height_Load(EOS(STATIC_971), java.lang.Object(o339sub)) → 934_0_height_Load(EOS(STATIC_934), java.lang.Object(o339sub))
934_0_height_Load(EOS(STATIC_934), java.lang.Object(o330sub)) → 935_0_height_FieldAccess(EOS(STATIC_935), java.lang.Object(o330sub), java.lang.Object(o330sub))
942_0_height_NONNULL(EOS(STATIC_942), java.lang.Object(BTreeR(EOC, NULL, o337)), NULL) → 944_0_height_Load(EOS(STATIC_944), java.lang.Object(BTreeR(EOC, NULL, o337)))
944_0_height_Load(EOS(STATIC_944), java.lang.Object(BTreeR(EOC, NULL, o337))) → 947_0_height_FieldAccess(EOS(STATIC_947), java.lang.Object(BTreeR(EOC, NULL, o337)), java.lang.Object(BTreeR(EOC, NULL, o337)))
947_0_height_FieldAccess(EOS(STATIC_947), java.lang.Object(BTreeR(EOC, NULL, o337)), java.lang.Object(BTreeR(EOC, NULL, o337))) → 950_0_height_NONNULL(EOS(STATIC_950), java.lang.Object(BTreeR(EOC, NULL, o337)), o337)
950_0_height_NONNULL(EOS(STATIC_950), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))), java.lang.Object(o341sub)) → 953_0_height_NONNULL(EOS(STATIC_953), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))), java.lang.Object(o341sub))
953_0_height_NONNULL(EOS(STATIC_953), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))), java.lang.Object(o341sub)) → 957_0_height_Load(EOS(STATIC_957), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))))
957_0_height_Load(EOS(STATIC_957), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub)))) → 960_0_height_FieldAccess(EOS(STATIC_960), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))))
960_0_height_FieldAccess(EOS(STATIC_960), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub)))) → 963_0_height_NONNULL(EOS(STATIC_963), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))), NULL)
963_0_height_NONNULL(EOS(STATIC_963), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))), NULL) → 967_0_height_ConstantStackPush(EOS(STATIC_967), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))))
967_0_height_ConstantStackPush(EOS(STATIC_967), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub)))) → 972_0_height_Load(EOS(STATIC_972), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))))
972_0_height_Load(EOS(STATIC_972), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub)))) → 977_0_height_FieldAccess(EOS(STATIC_977), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))))
977_0_height_FieldAccess(EOS(STATIC_977), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub)))) → 983_0_height_InvokeMethod(EOS(STATIC_983), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))), java.lang.Object(o341sub))
983_0_height_InvokeMethod(EOS(STATIC_983), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))), java.lang.Object(o341sub)) → 985_1_height_InvokeMethod(985_0_height_Load(EOS(STATIC_985), java.lang.Object(o341sub)), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))), java.lang.Object(o341sub))
985_0_height_Load(EOS(STATIC_985), java.lang.Object(o341sub)) → 987_0_height_Load(EOS(STATIC_987), java.lang.Object(o341sub))
987_0_height_Load(EOS(STATIC_987), java.lang.Object(o341sub)) → 934_0_height_Load(EOS(STATIC_934), java.lang.Object(o341sub))
R rules:
950_0_height_NONNULL(EOS(STATIC_950), java.lang.Object(BTreeR(EOC, NULL, NULL)), NULL) → 954_0_height_NONNULL(EOS(STATIC_954), java.lang.Object(BTreeR(EOC, NULL, NULL)), NULL)
954_0_height_NONNULL(EOS(STATIC_954), java.lang.Object(BTreeR(EOC, NULL, NULL)), NULL) → 958_0_height_ConstantStackPush(EOS(STATIC_958), java.lang.Object(BTreeR(EOC, NULL, NULL)))
958_0_height_ConstantStackPush(EOS(STATIC_958), java.lang.Object(BTreeR(EOC, NULL, NULL))) → 961_0_height_Return(EOS(STATIC_961), java.lang.Object(BTreeR(EOC, NULL, NULL)))
965_1_height_InvokeMethod(961_0_height_Return(EOS(STATIC_961), java.lang.Object(BTreeR(EOC, NULL, NULL))), java.lang.Object(BTreeR(EOC, NULL, NULL))) → 984_0_height_Return(EOS(STATIC_984), java.lang.Object(BTreeR(EOC, NULL, NULL)), java.lang.Object(BTreeR(EOC, NULL, NULL)))
965_1_height_InvokeMethod(988_0_height_Return(EOS(STATIC_988)), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), o395))) → 1018_0_height_Return(EOS(STATIC_1018), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), o395)))
965_1_height_InvokeMethod(1029_0_height_Return(EOS(STATIC_1029), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL))))) → 1090_0_height_Return(EOS(STATIC_1090), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))))
965_1_height_InvokeMethod(1681_0_height_Return(EOS(STATIC_1681)), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1934, o1935)), o1936)), o1937))) → 1736_0_height_Return(EOS(STATIC_1736), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1934, o1935)), o1936)), o1937)))
965_1_height_InvokeMethod(1684_0_height_Return(EOS(STATIC_1684), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1954, o1955)), o1956))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1954, o1955)), o1956))))) → 1750_0_height_Return(EOS(STATIC_1750), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1954, o1955)), o1956)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1954, o1955)), o1956)))))
965_1_height_InvokeMethod(1686_0_height_Return(EOS(STATIC_1686)), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1996, o1997)))), o1998))) → 1781_0_height_Return(EOS(STATIC_1781), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1996, o1997)))), o1998)))
965_1_height_InvokeMethod(1690_0_height_Return(EOS(STATIC_1690), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2015, o2016))))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2015, o2016))))))) → 1795_0_height_Return(EOS(STATIC_1795), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2015, o2016)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2015, o2016)))))))
984_0_height_Return(EOS(STATIC_984), java.lang.Object(BTreeR(EOC, NULL, NULL)), java.lang.Object(BTreeR(EOC, NULL, NULL))) → 986_0_height_IntArithmetic(EOS(STATIC_986))
985_1_height_InvokeMethod(961_0_height_Return(EOS(STATIC_961), java.lang.Object(BTreeR(EOC, NULL, NULL))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))), java.lang.Object(BTreeR(EOC, NULL, NULL))) → 1012_0_height_Return(EOS(STATIC_1012), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))), java.lang.Object(BTreeR(EOC, NULL, NULL)), java.lang.Object(BTreeR(EOC, NULL, NULL)))
985_1_height_InvokeMethod(988_0_height_Return(EOS(STATIC_988)), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), o368)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), o368))) → 1014_0_height_Return(EOS(STATIC_1014), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), o368)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), o368)))
985_1_height_InvokeMethod(1029_0_height_Return(EOS(STATIC_1029), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL))))) → 1091_0_height_Return(EOS(STATIC_1091), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))))
985_1_height_InvokeMethod(1681_0_height_Return(EOS(STATIC_1681)), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1943, o1944)), o1945)), o1946)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1943, o1944)), o1945)), o1946))) → 1744_0_height_Return(EOS(STATIC_1744), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1943, o1944)), o1945)), o1946)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1943, o1944)), o1945)), o1946)))
985_1_height_InvokeMethod(1684_0_height_Return(EOS(STATIC_1684), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1961, o1962)), o1963))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1961, o1962)), o1963)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1961, o1962)), o1963))))) → 1761_0_height_Return(EOS(STATIC_1761), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1961, o1962)), o1963)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1961, o1962)), o1963)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1961, o1962)), o1963)))))
985_1_height_InvokeMethod(1686_0_height_Return(EOS(STATIC_1686)), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2004, o2005)))), o2006)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2004, o2005)))), o2006))) → 1788_0_height_Return(EOS(STATIC_1788), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2004, o2005)))), o2006)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2004, o2005)))), o2006)))
985_1_height_InvokeMethod(1690_0_height_Return(EOS(STATIC_1690), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2021, o2022))))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2021, o2022)))))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2021, o2022))))))) → 1800_0_height_Return(EOS(STATIC_1800), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2021, o2022)))))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2021, o2022)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2021, o2022)))))))
986_0_height_IntArithmetic(EOS(STATIC_986)) → 988_0_height_Return(EOS(STATIC_988))
1012_0_height_Return(EOS(STATIC_1012), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))), java.lang.Object(BTreeR(EOC, NULL, NULL)), java.lang.Object(BTreeR(EOC, NULL, NULL))) → 1019_0_height_IntArithmetic(EOS(STATIC_1019), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))))
1014_0_height_Return(EOS(STATIC_1014), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), o368)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), o368))) → 1138_0_height_Return(EOS(STATIC_1138), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), o368)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), o368)))
1018_0_height_Return(EOS(STATIC_1018), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), o395))) → 1132_0_height_Return(EOS(STATIC_1132), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), o395)))
1019_0_height_IntArithmetic(EOS(STATIC_1019), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL))))) → 1029_0_height_Return(EOS(STATIC_1029), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))))
1090_0_height_Return(EOS(STATIC_1090), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL))))) → 1102_0_height_Return(EOS(STATIC_1102), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))))
1091_0_height_Return(EOS(STATIC_1091), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL))))) → 1111_0_height_Return(EOS(STATIC_1111), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))))
1102_0_height_Return(EOS(STATIC_1102), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o478, o479)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o478, o479))))) → 1293_0_height_Return(EOS(STATIC_1293), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o478, o479)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o478, o479)))))
1111_0_height_Return(EOS(STATIC_1111), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o493, o494)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o493, o494)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o493, o494))))) → 1308_0_height_Return(EOS(STATIC_1308), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o493, o494)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o493, o494)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o493, o494)))))
1132_0_height_Return(EOS(STATIC_1132), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o539, o540)), o541))) → 1269_0_height_Return(EOS(STATIC_1269), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o539, o540)), o541)))
1138_0_height_Return(EOS(STATIC_1138), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o562, o563)), o564)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o562, o563)), o564))) → 1279_0_height_Return(EOS(STATIC_1279), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o562, o563)), o564)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o562, o563)), o564)))
1269_0_height_Return(EOS(STATIC_1269), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o825, o826)), o827))) → 1418_0_height_Return(EOS(STATIC_1418), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o825, o826)), o827)))
1279_0_height_Return(EOS(STATIC_1279), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o865, o866)), o867)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o865, o866)), o867))) → 1436_0_height_Return(EOS(STATIC_1436), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o865, o866)), o867)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o865, o866)), o867)))
1293_0_height_Return(EOS(STATIC_1293), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o892, o893)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o892, o893))))) → 1449_0_height_Return(EOS(STATIC_1449), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o892, o893)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o892, o893)))))
1308_0_height_Return(EOS(STATIC_1308), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o920, o921)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o920, o921)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o920, o921))))) → 1459_0_height_Return(EOS(STATIC_1459), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o920, o921)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o920, o921)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o920, o921)))))
1418_0_height_Return(EOS(STATIC_1418), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1244, o1245)), o1246))) → 1587_0_height_Return(EOS(STATIC_1587), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1244, o1245)), o1246)))
1436_0_height_Return(EOS(STATIC_1436), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1286, o1287)), o1288)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1286, o1287)), o1288))) → 1598_0_height_Return(EOS(STATIC_1598), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1286, o1287)), o1288)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1286, o1287)), o1288)))
1449_0_height_Return(EOS(STATIC_1449), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1314, o1315)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1314, o1315))))) → 1618_0_height_Return(EOS(STATIC_1618), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1314, o1315)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1314, o1315)))))
1459_0_height_Return(EOS(STATIC_1459), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1342, o1343)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1342, o1343)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1342, o1343))))) → 1636_0_height_Return(EOS(STATIC_1636), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1342, o1343)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1342, o1343)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1342, o1343)))))
1587_0_height_Return(EOS(STATIC_1587), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1659, o1660)), o1661))) → 1669_0_height_IntArithmetic(EOS(STATIC_1669))
1598_0_height_Return(EOS(STATIC_1598), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1699, o1700)), o1701)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1699, o1700)), o1701))) → 1670_0_height_IntArithmetic(EOS(STATIC_1670), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1699, o1700)), o1701)))))
1618_0_height_Return(EOS(STATIC_1618), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1727, o1728)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1727, o1728))))) → 1672_0_height_IntArithmetic(EOS(STATIC_1672))
1636_0_height_Return(EOS(STATIC_1636), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1754, o1755)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1754, o1755)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1754, o1755))))) → 1674_0_height_IntArithmetic(EOS(STATIC_1674), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1754, o1755)))))))
1669_0_height_IntArithmetic(EOS(STATIC_1669)) → 1681_0_height_Return(EOS(STATIC_1681))
1670_0_height_IntArithmetic(EOS(STATIC_1670), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1699, o1700)), o1701))))) → 1684_0_height_Return(EOS(STATIC_1684), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1699, o1700)), o1701)))))
1672_0_height_IntArithmetic(EOS(STATIC_1672)) → 1686_0_height_Return(EOS(STATIC_1686))
1674_0_height_IntArithmetic(EOS(STATIC_1674), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1754, o1755))))))) → 1690_0_height_Return(EOS(STATIC_1690), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1754, o1755)))))))
1736_0_height_Return(EOS(STATIC_1736), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1934, o1935)), o1936)), o1937))) → 1587_0_height_Return(EOS(STATIC_1587), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1934, o1935)), o1936)), o1937)))
1744_0_height_Return(EOS(STATIC_1744), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1943, o1944)), o1945)), o1946)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1943, o1944)), o1945)), o1946))) → 1598_0_height_Return(EOS(STATIC_1598), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1943, o1944)), o1945)), o1946)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1943, o1944)), o1945)), o1946)))
1750_0_height_Return(EOS(STATIC_1750), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1954, o1955)), o1956)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1954, o1955)), o1956))))) → 1618_0_height_Return(EOS(STATIC_1618), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1954, o1955)), o1956)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1954, o1955)), o1956)))))
1761_0_height_Return(EOS(STATIC_1761), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1961, o1962)), o1963)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1961, o1962)), o1963)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1961, o1962)), o1963))))) → 1636_0_height_Return(EOS(STATIC_1636), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1961, o1962)), o1963)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1961, o1962)), o1963)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1961, o1962)), o1963)))))
1781_0_height_Return(EOS(STATIC_1781), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1996, o1997)))), o1998))) → 1587_0_height_Return(EOS(STATIC_1587), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1996, o1997)))), o1998)))
1788_0_height_Return(EOS(STATIC_1788), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2004, o2005)))), o2006)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2004, o2005)))), o2006))) → 1598_0_height_Return(EOS(STATIC_1598), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2004, o2005)))), o2006)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2004, o2005)))), o2006)))
1795_0_height_Return(EOS(STATIC_1795), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2015, o2016)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2015, o2016))))))) → 1618_0_height_Return(EOS(STATIC_1618), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2015, o2016)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2015, o2016)))))))
1800_0_height_Return(EOS(STATIC_1800), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2021, o2022)))))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2021, o2022)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2021, o2022))))))) → 1636_0_height_Return(EOS(STATIC_1636), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2021, o2022)))))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2021, o2022)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2021, o2022)))))))

Combined rules. Obtained 2 conditional rules for P and 14 conditional rules for R.


P rules:
935_0_height_FieldAccess(EOS(STATIC_935), java.lang.Object(BTreeR(EOC, java.lang.Object(x0), x1)), java.lang.Object(BTreeR(EOC, java.lang.Object(x0), x1))) → 965_1_height_InvokeMethod(935_0_height_FieldAccess(EOS(STATIC_935), java.lang.Object(x0), java.lang.Object(x0)), java.lang.Object(x0))
935_0_height_FieldAccess(EOS(STATIC_935), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(x0))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(x0)))) → 985_1_height_InvokeMethod(935_0_height_FieldAccess(EOS(STATIC_935), java.lang.Object(x0), java.lang.Object(x0)), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(x0))), java.lang.Object(x0))
R rules:
965_1_height_InvokeMethod(961_0_height_Return(EOS(STATIC_961), java.lang.Object(BTreeR(EOC, NULL, NULL))), java.lang.Object(BTreeR(EOC, NULL, NULL))) → 988_0_height_Return(EOS(STATIC_988))
985_1_height_InvokeMethod(961_0_height_Return(EOS(STATIC_961), java.lang.Object(BTreeR(EOC, NULL, NULL))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))), java.lang.Object(BTreeR(EOC, NULL, NULL))) → 1029_0_height_Return(EOS(STATIC_1029), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))))
965_1_height_InvokeMethod(1681_0_height_Return(EOS(STATIC_1681)), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, x0, x1)), x2)), x3))) → 1681_0_height_Return(EOS(STATIC_1681))
965_1_height_InvokeMethod(1686_0_height_Return(EOS(STATIC_1686)), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, x0, x1)))), x2))) → 1681_0_height_Return(EOS(STATIC_1681))
965_1_height_InvokeMethod(988_0_height_Return(EOS(STATIC_988)), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), x0))) → 1681_0_height_Return(EOS(STATIC_1681))
985_1_height_InvokeMethod(1681_0_height_Return(EOS(STATIC_1681)), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, x0, x1)), x2)), x3)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, x0, x1)), x2)), x3))) → 1684_0_height_Return(EOS(STATIC_1684), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, x0, x1)), x2)), x3)))))
985_1_height_InvokeMethod(1686_0_height_Return(EOS(STATIC_1686)), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, x0, x1)))), x2)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, x0, x1)))), x2))) → 1684_0_height_Return(EOS(STATIC_1684), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, x0, x1)))), x2)))))
985_1_height_InvokeMethod(988_0_height_Return(EOS(STATIC_988)), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), x0)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), x0))) → 1684_0_height_Return(EOS(STATIC_1684), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), x0)))))
965_1_height_InvokeMethod(1684_0_height_Return(EOS(STATIC_1684), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, x0, x1)), x2))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, x0, x1)), x2))))) → 1686_0_height_Return(EOS(STATIC_1686))
965_1_height_InvokeMethod(1690_0_height_Return(EOS(STATIC_1690), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, x0, x1))))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, x0, x1))))))) → 1686_0_height_Return(EOS(STATIC_1686))
965_1_height_InvokeMethod(1029_0_height_Return(EOS(STATIC_1029), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL))))) → 1686_0_height_Return(EOS(STATIC_1686))
985_1_height_InvokeMethod(1684_0_height_Return(EOS(STATIC_1684), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, x0, x1)), x2))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, x0, x1)), x2)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, x0, x1)), x2))))) → 1690_0_height_Return(EOS(STATIC_1690), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, x0, x1)), x2)))))))
985_1_height_InvokeMethod(1690_0_height_Return(EOS(STATIC_1690), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, x0, x1))))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, x0, x1)))))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, x0, x1))))))) → 1690_0_height_Return(EOS(STATIC_1690), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, x0, x1)))))))))
985_1_height_InvokeMethod(1029_0_height_Return(EOS(STATIC_1029), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL))))) → 1690_0_height_Return(EOS(STATIC_1690), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))))))

Filtered ground terms:



BTreeR(x1, x2, x3) → BTreeR(x2, x3)
935_0_height_FieldAccess(x1, x2, x3) → 935_0_height_FieldAccess(x2, x3)
1690_0_height_Return(x1, x2) → 1690_0_height_Return(x2)
1029_0_height_Return(x1, x2) → 1029_0_height_Return
1684_0_height_Return(x1, x2) → 1684_0_height_Return(x2)
1686_0_height_Return(x1) → 1686_0_height_Return
988_0_height_Return(x1) → 988_0_height_Return
1681_0_height_Return(x1) → 1681_0_height_Return
961_0_height_Return(x1, x2) → 961_0_height_Return

Filtered duplicate args:



935_0_height_FieldAccess(x1, x2) → 935_0_height_FieldAccess(x2)
985_1_height_InvokeMethod(x1, x2, x3) → 985_1_height_InvokeMethod(x1, x2)

Combined rules. Obtained 2 conditional rules for P and 14 conditional rules for R.


P rules:
935_0_height_FieldAccess(java.lang.Object(BTreeR(java.lang.Object(x0), x1))) → 965_1_height_InvokeMethod(935_0_height_FieldAccess(java.lang.Object(x0)), java.lang.Object(x0))
935_0_height_FieldAccess(java.lang.Object(BTreeR(NULL, java.lang.Object(x0)))) → 985_1_height_InvokeMethod(935_0_height_FieldAccess(java.lang.Object(x0)), java.lang.Object(BTreeR(NULL, java.lang.Object(x0))))
R rules:
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, NULL))) → 988_0_height_Return
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))) → 1029_0_height_Return
965_1_height_InvokeMethod(1681_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3))) → 1681_0_height_Return
965_1_height_InvokeMethod(1686_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2))) → 1681_0_height_Return
965_1_height_InvokeMethod(988_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0))) → 1681_0_height_Return
985_1_height_InvokeMethod(1681_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3))))) → 1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3)))))
985_1_height_InvokeMethod(1686_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2))))) → 1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2)))))
985_1_height_InvokeMethod(988_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0))))) → 1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0)))))
965_1_height_InvokeMethod(1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))) → 1686_0_height_Return
965_1_height_InvokeMethod(1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))) → 1686_0_height_Return
965_1_height_InvokeMethod(1029_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))) → 1686_0_height_Return
985_1_height_InvokeMethod(1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))))) → 1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)))))))
985_1_height_InvokeMethod(1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))))) → 1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))))))))
985_1_height_InvokeMethod(1029_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))))) → 1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL)))))))

Performed bisimulation on rules. Used the following equivalence classes: {[961_0_height_Return, 988_0_height_Return, 1029_0_height_Return, 1681_0_height_Return, 1686_0_height_Return]=961_0_height_Return}


Finished conversion. Obtained 2 rules for P and 14 rules for R. System has no predefined symbols.


P rules:
935_0_HEIGHT_FIELDACCESS(java.lang.Object(BTreeR(java.lang.Object(x0), x1))) → 935_0_HEIGHT_FIELDACCESS(java.lang.Object(x0))
935_0_HEIGHT_FIELDACCESS(java.lang.Object(BTreeR(NULL, java.lang.Object(x0)))) → 935_0_HEIGHT_FIELDACCESS(java.lang.Object(x0))
R rules:
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, NULL))) → 961_0_height_Return
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))) → 961_0_height_Return
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3))) → 961_0_height_Return
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2))) → 961_0_height_Return
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0))) → 961_0_height_Return
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3))))) → 1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3)))))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2))))) → 1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2)))))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0))))) → 1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0)))))
965_1_height_InvokeMethod(1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))) → 961_0_height_Return
965_1_height_InvokeMethod(1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))) → 961_0_height_Return
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))) → 961_0_height_Return
985_1_height_InvokeMethod(1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))))) → 1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)))))))
985_1_height_InvokeMethod(1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))))) → 1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))))))))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))))) → 1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL)))))))

(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:
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, NULL))) → 961_0_height_Return
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))) → 961_0_height_Return
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3))) → 961_0_height_Return
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2))) → 961_0_height_Return
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0))) → 961_0_height_Return
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3))))) → 1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3)))))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2))))) → 1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2)))))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0))))) → 1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0)))))
965_1_height_InvokeMethod(1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))) → 961_0_height_Return
965_1_height_InvokeMethod(1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))) → 961_0_height_Return
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))) → 961_0_height_Return
985_1_height_InvokeMethod(1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))))) → 1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)))))))
985_1_height_InvokeMethod(1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))))) → 1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))))))))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))))) → 1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL)))))))

The integer pair graph contains the following rules and edges:
(0): 935_0_HEIGHT_FIELDACCESS(java.lang.Object(BTreeR(java.lang.Object(x0[0]), x1[0]))) → 935_0_HEIGHT_FIELDACCESS(java.lang.Object(x0[0]))
(1): 935_0_HEIGHT_FIELDACCESS(java.lang.Object(BTreeR(NULL, java.lang.Object(x0[1])))) → 935_0_HEIGHT_FIELDACCESS(java.lang.Object(x0[1]))

(0) -> (0), if (java.lang.Object(x0[0]) →* java.lang.Object(BTreeR(java.lang.Object(x0[0]'), x1[0]')))


(0) -> (1), if (java.lang.Object(x0[0]) →* java.lang.Object(BTreeR(NULL, java.lang.Object(x0[1]))))


(1) -> (0), if (java.lang.Object(x0[1]) →* java.lang.Object(BTreeR(java.lang.Object(x0[0]), x1[0])))


(1) -> (1), if (java.lang.Object(x0[1]) →* java.lang.Object(BTreeR(NULL, java.lang.Object(x0[1]'))))



The set Q consists of the following terms:
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, NULL)))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL)))))
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3)))
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2)))
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0)))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3)))))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2)))))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0)))))
965_1_height_InvokeMethod(1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)))))
965_1_height_InvokeMethod(1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))))))
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL)))))
985_1_height_InvokeMethod(1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)))))))
985_1_height_InvokeMethod(1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))))))))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL)))))))

(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:

935_0_HEIGHT_FIELDACCESS(java.lang.Object(BTreeR(java.lang.Object(x0[0]), x1[0]))) → 935_0_HEIGHT_FIELDACCESS(java.lang.Object(x0[0]))
935_0_HEIGHT_FIELDACCESS(java.lang.Object(BTreeR(NULL, java.lang.Object(x0[1])))) → 935_0_HEIGHT_FIELDACCESS(java.lang.Object(x0[1]))

The TRS R consists of the following rules:

965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, NULL))) → 961_0_height_Return
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))) → 961_0_height_Return
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3))) → 961_0_height_Return
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2))) → 961_0_height_Return
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0))) → 961_0_height_Return
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3))))) → 1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3)))))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2))))) → 1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2)))))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0))))) → 1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0)))))
965_1_height_InvokeMethod(1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))) → 961_0_height_Return
965_1_height_InvokeMethod(1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))) → 961_0_height_Return
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))) → 961_0_height_Return
985_1_height_InvokeMethod(1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))))) → 1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)))))))
985_1_height_InvokeMethod(1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))))) → 1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))))))))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))))) → 1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL)))))))

The set Q consists of the following terms:

965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, NULL)))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL)))))
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3)))
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2)))
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0)))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3)))))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2)))))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0)))))
965_1_height_InvokeMethod(1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)))))
965_1_height_InvokeMethod(1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))))))
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL)))))
985_1_height_InvokeMethod(1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)))))))
985_1_height_InvokeMethod(1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))))))))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL)))))))

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:

935_0_HEIGHT_FIELDACCESS(java.lang.Object(BTreeR(java.lang.Object(x0[0]), x1[0]))) → 935_0_HEIGHT_FIELDACCESS(java.lang.Object(x0[0]))
935_0_HEIGHT_FIELDACCESS(java.lang.Object(BTreeR(NULL, java.lang.Object(x0[1])))) → 935_0_HEIGHT_FIELDACCESS(java.lang.Object(x0[1]))

R is empty.
The set Q consists of the following terms:

965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, NULL)))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL)))))
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3)))
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2)))
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0)))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3)))))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2)))))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0)))))
965_1_height_InvokeMethod(1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)))))
965_1_height_InvokeMethod(1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))))))
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL)))))
985_1_height_InvokeMethod(1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)))))))
985_1_height_InvokeMethod(1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))))))))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL)))))))

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].

965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, NULL)))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL)))))
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3)))
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2)))
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0)))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3)))))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2)))))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0)))))
965_1_height_InvokeMethod(1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)))))
965_1_height_InvokeMethod(1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))))))
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL)))))
985_1_height_InvokeMethod(1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)))))))
985_1_height_InvokeMethod(1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))))))))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL)))))))

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

935_0_HEIGHT_FIELDACCESS(java.lang.Object(BTreeR(java.lang.Object(x0[0]), x1[0]))) → 935_0_HEIGHT_FIELDACCESS(java.lang.Object(x0[0]))
935_0_HEIGHT_FIELDACCESS(java.lang.Object(BTreeR(NULL, java.lang.Object(x0[1])))) → 935_0_HEIGHT_FIELDACCESS(java.lang.Object(x0[1]))

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:

  • 935_0_HEIGHT_FIELDACCESS(java.lang.Object(BTreeR(java.lang.Object(x0[0]), x1[0]))) → 935_0_HEIGHT_FIELDACCESS(java.lang.Object(x0[0]))
    The graph contains the following edges 1 > 1

  • 935_0_HEIGHT_FIELDACCESS(java.lang.Object(BTreeR(NULL, java.lang.Object(x0[1])))) → 935_0_HEIGHT_FIELDACCESS(java.lang.Object(x0[1]))
    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: BTreeR.<init>(I)V
SCC calls the following helper methods: BTreeR.<init>(I)V
Performed SCC analyses: UsedFieldsAnalysis

(17) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 30 rules for P and 8 rules for R.


P rules:
397_0_<init>_InvokeMethod(EOS(STATIC_397), i57) → 402_0_<init>_Load(EOS(STATIC_402), i57)
402_0_<init>_Load(EOS(STATIC_402), i57) → 406_0_<init>_ConstantStackPush(EOS(STATIC_406), i57, i57)
406_0_<init>_ConstantStackPush(EOS(STATIC_406), i57, i57) → 415_0_<init>_LE(EOS(STATIC_415), i57, i57, 1)
415_0_<init>_LE(EOS(STATIC_415), i64, i64, matching1) → 421_0_<init>_LE(EOS(STATIC_421), i64, i64, 1) | =(matching1, 1)
421_0_<init>_LE(EOS(STATIC_421), i64, i64, matching1) → 428_0_<init>_Load(EOS(STATIC_428), i64) | &&(>(i64, 1), =(matching1, 1))
428_0_<init>_Load(EOS(STATIC_428), i64) → 435_0_<init>_New(EOS(STATIC_435), i64)
435_0_<init>_New(EOS(STATIC_435), i64) → 450_0_<init>_Duplicate(EOS(STATIC_450), i64)
450_0_<init>_Duplicate(EOS(STATIC_450), i64) → 458_0_<init>_Load(EOS(STATIC_458), i64)
458_0_<init>_Load(EOS(STATIC_458), i64) → 462_0_<init>_ConstantStackPush(EOS(STATIC_462), i64, i64)
462_0_<init>_ConstantStackPush(EOS(STATIC_462), i64, i64) → 468_0_<init>_IntArithmetic(EOS(STATIC_468), i64, i64, 1)
468_0_<init>_IntArithmetic(EOS(STATIC_468), i64, i64, matching1) → 472_0_<init>_InvokeMethod(EOS(STATIC_472), i64, -(i64, 1)) | &&(>(i64, 0), =(matching1, 1))
472_0_<init>_InvokeMethod(EOS(STATIC_472), i64, i66) → 476_1_<init>_InvokeMethod(476_0_<init>_Load(EOS(STATIC_476), i66), i64, i66)
476_0_<init>_Load(EOS(STATIC_476), i66) → 479_0_<init>_Load(EOS(STATIC_479), i66)
476_1_<init>_InvokeMethod(426_0_<init>_Return(EOS(STATIC_426)), i64, matching1) → 493_0_<init>_Return(EOS(STATIC_493), i64, 1) | =(matching1, 1)
476_1_<init>_InvokeMethod(767_0_<init>_Return(EOS(STATIC_767)), i64, i133) → 853_0_<init>_Return(EOS(STATIC_853), i64, i133)
479_0_<init>_Load(EOS(STATIC_479), i66) → 392_0_<init>_Load(EOS(STATIC_392), i66)
392_0_<init>_Load(EOS(STATIC_392), i57) → 397_0_<init>_InvokeMethod(EOS(STATIC_397), i57)
493_0_<init>_Return(EOS(STATIC_493), i64, matching1) → 568_0_<init>_Return(EOS(STATIC_568), i64, 1) | =(matching1, 1)
568_0_<init>_Return(EOS(STATIC_568), i64, i92) → 578_0_<init>_FieldAccess(EOS(STATIC_578), i64)
578_0_<init>_FieldAccess(EOS(STATIC_578), i64) → 587_0_<init>_Load(EOS(STATIC_587), i64)
587_0_<init>_Load(EOS(STATIC_587), i64) → 595_0_<init>_New(EOS(STATIC_595), i64)
595_0_<init>_New(EOS(STATIC_595), i64) → 604_0_<init>_Duplicate(EOS(STATIC_604), i64)
604_0_<init>_Duplicate(EOS(STATIC_604), i64) → 613_0_<init>_Load(EOS(STATIC_613), i64)
613_0_<init>_Load(EOS(STATIC_613), i64) → 616_0_<init>_ConstantStackPush(EOS(STATIC_616), i64)
616_0_<init>_ConstantStackPush(EOS(STATIC_616), i64) → 627_0_<init>_IntArithmetic(EOS(STATIC_627), i64, 1)
627_0_<init>_IntArithmetic(EOS(STATIC_627), i64, matching1) → 630_0_<init>_InvokeMethod(EOS(STATIC_630), -(i64, 1)) | &&(>(i64, 0), =(matching1, 1))
630_0_<init>_InvokeMethod(EOS(STATIC_630), i99) → 634_1_<init>_InvokeMethod(634_0_<init>_Load(EOS(STATIC_634), i99), i99)
634_0_<init>_Load(EOS(STATIC_634), i99) → 638_0_<init>_Load(EOS(STATIC_638), i99)
638_0_<init>_Load(EOS(STATIC_638), i99) → 392_0_<init>_Load(EOS(STATIC_392), i99)
853_0_<init>_Return(EOS(STATIC_853), i64, i133) → 568_0_<init>_Return(EOS(STATIC_568), i64, i133)
R rules:
415_0_<init>_LE(EOS(STATIC_415), i63, i63, matching1) → 420_0_<init>_LE(EOS(STATIC_420), i63, i63, 1) | =(matching1, 1)
420_0_<init>_LE(EOS(STATIC_420), i63, i63, matching1) → 426_0_<init>_Return(EOS(STATIC_426)) | &&(<=(i63, 1), =(matching1, 1))
634_1_<init>_InvokeMethod(426_0_<init>_Return(EOS(STATIC_426)), matching1) → 653_0_<init>_Return(EOS(STATIC_653), 1) | =(matching1, 1)
634_1_<init>_InvokeMethod(767_0_<init>_Return(EOS(STATIC_767)), i137) → 859_0_<init>_Return(EOS(STATIC_859), i137)
653_0_<init>_Return(EOS(STATIC_653), matching1) → 745_0_<init>_Return(EOS(STATIC_745), 1) | =(matching1, 1)
745_0_<init>_Return(EOS(STATIC_745), i126) → 753_0_<init>_FieldAccess(EOS(STATIC_753))
753_0_<init>_FieldAccess(EOS(STATIC_753)) → 767_0_<init>_Return(EOS(STATIC_767))
859_0_<init>_Return(EOS(STATIC_859), i137) → 745_0_<init>_Return(EOS(STATIC_745), i137)

Combined rules. Obtained 3 conditional rules for P and 2 conditional rules for R.


P rules:
397_0_<init>_InvokeMethod(EOS(STATIC_397), x0) → 476_1_<init>_InvokeMethod(397_0_<init>_InvokeMethod(EOS(STATIC_397), -(x0, 1)), x0, -(x0, 1)) | >(x0, 1)
476_1_<init>_InvokeMethod(426_0_<init>_Return(EOS(STATIC_426)), x0, 1) → 634_1_<init>_InvokeMethod(397_0_<init>_InvokeMethod(EOS(STATIC_397), -(x0, 1)), -(x0, 1)) | >(x0, 0)
476_1_<init>_InvokeMethod(767_0_<init>_Return(EOS(STATIC_767)), x0, x1) → 634_1_<init>_InvokeMethod(397_0_<init>_InvokeMethod(EOS(STATIC_397), -(x0, 1)), -(x0, 1)) | >(x0, 0)
R rules:
634_1_<init>_InvokeMethod(426_0_<init>_Return(EOS(STATIC_426)), 1) → 767_0_<init>_Return(EOS(STATIC_767))
634_1_<init>_InvokeMethod(767_0_<init>_Return(EOS(STATIC_767)), x0) → 767_0_<init>_Return(EOS(STATIC_767))

Filtered ground terms:



397_0_<init>_InvokeMethod(x1, x2) → 397_0_<init>_InvokeMethod(x2)
Cond_476_1_<init>_InvokeMethod1(x1, x2, x3, x4) → Cond_476_1_<init>_InvokeMethod1(x1, x3, x4)
767_0_<init>_Return(x1) → 767_0_<init>_Return
Cond_476_1_<init>_InvokeMethod(x1, x2, x3, x4) → Cond_476_1_<init>_InvokeMethod(x1, x3)
426_0_<init>_Return(x1) → 426_0_<init>_Return
Cond_397_0_<init>_InvokeMethod(x1, x2, x3) → Cond_397_0_<init>_InvokeMethod(x1, x3)

Filtered unneeded arguments:



Cond_476_1_<init>_InvokeMethod1(x1, x2, x3) → Cond_476_1_<init>_InvokeMethod1(x1, x2)

Combined rules. Obtained 3 conditional rules for P and 2 conditional rules for R.


P rules:
397_0_<init>_InvokeMethod(x0) → 476_1_<init>_InvokeMethod(397_0_<init>_InvokeMethod(-(x0, 1)), x0, -(x0, 1)) | >(x0, 1)
476_1_<init>_InvokeMethod(426_0_<init>_Return, x0, 1) → 634_1_<init>_InvokeMethod(397_0_<init>_InvokeMethod(-(x0, 1)), -(x0, 1)) | >(x0, 0)
476_1_<init>_InvokeMethod(767_0_<init>_Return, x0, x1) → 634_1_<init>_InvokeMethod(397_0_<init>_InvokeMethod(-(x0, 1)), -(x0, 1)) | >(x0, 0)
R rules:
634_1_<init>_InvokeMethod(426_0_<init>_Return, 1) → 767_0_<init>_Return
634_1_<init>_InvokeMethod(767_0_<init>_Return, x0) → 767_0_<init>_Return

Performed bisimulation on rules. Used the following equivalence classes: {[426_0__Return, 767_0__Return]=426_0__Return}


Finished conversion. Obtained 7 rules for P and 2 rules for R. System has predefined symbols.


P rules:
397_0_<INIT>_INVOKEMETHOD(x0) → COND_397_0_<INIT>_INVOKEMETHOD(>(x0, 1), x0)
COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0) → 476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(-(x0, 1)), x0, -(x0, 1))
COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0) → 397_0_<INIT>_INVOKEMETHOD(-(x0, 1))
476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0, 1) → COND_476_1_<INIT>_INVOKEMETHOD(>(x0, 0), 426_0_<init>_Return, x0, 1)
COND_476_1_<INIT>_INVOKEMETHOD(TRUE, 426_0_<init>_Return, x0, 1) → 397_0_<INIT>_INVOKEMETHOD(-(x0, 1))
476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0, x1) → COND_476_1_<INIT>_INVOKEMETHOD1(>(x0, 0), 426_0_<init>_Return, x0, x1)
COND_476_1_<INIT>_INVOKEMETHOD1(TRUE, 426_0_<init>_Return, x0, x1) → 397_0_<INIT>_INVOKEMETHOD(-(x0, 1))
R rules:
634_1_<init>_InvokeMethod(426_0_<init>_Return, 1) → 426_0_<init>_Return
634_1_<init>_InvokeMethod(426_0_<init>_Return, x0) → 426_0_<init>_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:

Integer


The ITRS R consists of the following rules:
634_1_<init>_InvokeMethod(426_0_<init>_Return, 1) → 426_0_<init>_Return
634_1_<init>_InvokeMethod(426_0_<init>_Return, x0) → 426_0_<init>_Return

The integer pair graph contains the following rules and edges:
(0): 397_0_<INIT>_INVOKEMETHOD(x0[0]) → COND_397_0_<INIT>_INVOKEMETHOD(x0[0] > 1, x0[0])
(1): COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0[1]) → 476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(x0[1] - 1), x0[1], x0[1] - 1)
(2): COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0[2]) → 397_0_<INIT>_INVOKEMETHOD(x0[2] - 1)
(3): 476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0[3], 1) → COND_476_1_<INIT>_INVOKEMETHOD(x0[3] > 0, 426_0_<init>_Return, x0[3], 1)
(4): COND_476_1_<INIT>_INVOKEMETHOD(TRUE, 426_0_<init>_Return, x0[4], 1) → 397_0_<INIT>_INVOKEMETHOD(x0[4] - 1)
(5): 476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0[5], x1[5]) → COND_476_1_<INIT>_INVOKEMETHOD1(x0[5] > 0, 426_0_<init>_Return, x0[5], x1[5])
(6): COND_476_1_<INIT>_INVOKEMETHOD1(TRUE, 426_0_<init>_Return, x0[6], x1[6]) → 397_0_<INIT>_INVOKEMETHOD(x0[6] - 1)

(0) -> (1), if (x0[0] > 1x0[0]* x0[1])


(0) -> (2), if (x0[0] > 1x0[0]* x0[2])


(1) -> (3), if (397_0_<init>_InvokeMethod(x0[1] - 1) →* 426_0_<init>_Returnx0[1]* x0[3]x0[1] - 1* 1)


(1) -> (5), if (397_0_<init>_InvokeMethod(x0[1] - 1) →* 426_0_<init>_Returnx0[1]* x0[5]x0[1] - 1* x1[5])


(2) -> (0), if (x0[2] - 1* x0[0])


(3) -> (4), if (x0[3] > 0x0[3]* x0[4])


(4) -> (0), if (x0[4] - 1* x0[0])


(5) -> (6), if (x0[5] > 0x0[5]* x0[6]x1[5]* x1[6])


(6) -> (0), if (x0[6] - 1* x0[0])



The set Q consists of the following terms:
634_1_<init>_InvokeMethod(426_0_<init>_Return, x0)

(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.IdpCand1ShapeHeuristic@5d8409fb Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

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 397_0_<INIT>_INVOKEMETHOD(x0) → COND_397_0_<INIT>_INVOKEMETHOD(>(x0, 1), x0) the following chains were created:
  • We consider the chain 397_0_<INIT>_INVOKEMETHOD(x0[0]) → COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0]), COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0[1]) → 476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(-(x0[1], 1)), x0[1], -(x0[1], 1)) which results in the following constraint:

    (1)    (>(x0[0], 1)=TRUEx0[0]=x0[1]397_0_<INIT>_INVOKEMETHOD(x0[0])≥NonInfC∧397_0_<INIT>_INVOKEMETHOD(x0[0])≥COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])∧(UIncreasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥))



    We simplified constraint (1) using rule (IV) which results in the following new constraint:

    (2)    (>(x0[0], 1)=TRUE397_0_<INIT>_INVOKEMETHOD(x0[0])≥NonInfC∧397_0_<INIT>_INVOKEMETHOD(x0[0])≥COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])∧(UIncreasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥))



    We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (3)    (x0[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥)∧[bni_16 + (-1)Bound*bni_16] + [(2)bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)



    We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (4)    (x0[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥)∧[bni_16 + (-1)Bound*bni_16] + [(2)bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)



    We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (5)    (x0[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥)∧[bni_16 + (-1)Bound*bni_16] + [(2)bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)



    We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (6)    (x0[0] ≥ 0 ⇒ (UIncreasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥)∧[(5)bni_16 + (-1)Bound*bni_16] + [(2)bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)



  • We consider the chain 397_0_<INIT>_INVOKEMETHOD(x0[0]) → COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0]), COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0[2]) → 397_0_<INIT>_INVOKEMETHOD(-(x0[2], 1)) which results in the following constraint:

    (7)    (>(x0[0], 1)=TRUEx0[0]=x0[2]397_0_<INIT>_INVOKEMETHOD(x0[0])≥NonInfC∧397_0_<INIT>_INVOKEMETHOD(x0[0])≥COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])∧(UIncreasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥))



    We simplified constraint (7) using rule (IV) which results in the following new constraint:

    (8)    (>(x0[0], 1)=TRUE397_0_<INIT>_INVOKEMETHOD(x0[0])≥NonInfC∧397_0_<INIT>_INVOKEMETHOD(x0[0])≥COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])∧(UIncreasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥))



    We simplified constraint (8) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (9)    (x0[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥)∧[bni_16 + (-1)Bound*bni_16] + [(2)bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)



    We simplified constraint (9) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (10)    (x0[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥)∧[bni_16 + (-1)Bound*bni_16] + [(2)bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)



    We simplified constraint (10) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (11)    (x0[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥)∧[bni_16 + (-1)Bound*bni_16] + [(2)bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)



    We simplified constraint (11) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (12)    (x0[0] ≥ 0 ⇒ (UIncreasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥)∧[(5)bni_16 + (-1)Bound*bni_16] + [(2)bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)







For Pair COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0) → 476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(-(x0, 1)), x0, -(x0, 1)) the following chains were created:
  • We consider the chain COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0[1]) → 476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(-(x0[1], 1)), x0[1], -(x0[1], 1)) which results in the following constraint:

    (13)    (COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0[1])≥NonInfC∧COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0[1])≥476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(-(x0[1], 1)), x0[1], -(x0[1], 1))∧(UIncreasing(476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(-(x0[1], 1)), x0[1], -(x0[1], 1))), ≥))



    We simplified constraint (13) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (14)    ((UIncreasing(476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(-(x0[1], 1)), x0[1], -(x0[1], 1))), ≥)∧[bni_18] = 0∧[(-1)bso_19] ≥ 0)



    We simplified constraint (14) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (15)    ((UIncreasing(476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(-(x0[1], 1)), x0[1], -(x0[1], 1))), ≥)∧[bni_18] = 0∧[(-1)bso_19] ≥ 0)



    We simplified constraint (15) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (16)    ((UIncreasing(476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(-(x0[1], 1)), x0[1], -(x0[1], 1))), ≥)∧[bni_18] = 0∧[(-1)bso_19] ≥ 0)



    We simplified constraint (16) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (17)    ((UIncreasing(476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(-(x0[1], 1)), x0[1], -(x0[1], 1))), ≥)∧[bni_18] = 0∧0 = 0∧[(-1)bso_19] ≥ 0)







For Pair COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0) → 397_0_<INIT>_INVOKEMETHOD(-(x0, 1)) the following chains were created:
  • We consider the chain COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0[2]) → 397_0_<INIT>_INVOKEMETHOD(-(x0[2], 1)) which results in the following constraint:

    (18)    (COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0[2])≥NonInfC∧COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0[2])≥397_0_<INIT>_INVOKEMETHOD(-(x0[2], 1))∧(UIncreasing(397_0_<INIT>_INVOKEMETHOD(-(x0[2], 1))), ≥))



    We simplified constraint (18) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (19)    ((UIncreasing(397_0_<INIT>_INVOKEMETHOD(-(x0[2], 1))), ≥)∧[bni_20] = 0∧[2 + (-1)bso_21] ≥ 0)



    We simplified constraint (19) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (20)    ((UIncreasing(397_0_<INIT>_INVOKEMETHOD(-(x0[2], 1))), ≥)∧[bni_20] = 0∧[2 + (-1)bso_21] ≥ 0)



    We simplified constraint (20) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (21)    ((UIncreasing(397_0_<INIT>_INVOKEMETHOD(-(x0[2], 1))), ≥)∧[bni_20] = 0∧[2 + (-1)bso_21] ≥ 0)



    We simplified constraint (21) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (22)    ((UIncreasing(397_0_<INIT>_INVOKEMETHOD(-(x0[2], 1))), ≥)∧[bni_20] = 0∧0 = 0∧[2 + (-1)bso_21] ≥ 0)







For Pair 476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0, 1) → COND_476_1_<INIT>_INVOKEMETHOD(>(x0, 0), 426_0_<init>_Return, x0, 1) the following chains were created:
  • We consider the chain 476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0[3], 1) → COND_476_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 426_0_<init>_Return, x0[3], 1), COND_476_1_<INIT>_INVOKEMETHOD(TRUE, 426_0_<init>_Return, x0[4], 1) → 397_0_<INIT>_INVOKEMETHOD(-(x0[4], 1)) which results in the following constraint:

    (23)    (>(x0[3], 0)=TRUEx0[3]=x0[4]476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0[3], 1)≥NonInfC∧476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0[3], 1)≥COND_476_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 426_0_<init>_Return, x0[3], 1)∧(UIncreasing(COND_476_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 426_0_<init>_Return, x0[3], 1)), ≥))



    We simplified constraint (23) using rule (IV) which results in the following new constraint:

    (24)    (>(x0[3], 0)=TRUE476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0[3], 1)≥NonInfC∧476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0[3], 1)≥COND_476_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 426_0_<init>_Return, x0[3], 1)∧(UIncreasing(COND_476_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 426_0_<init>_Return, x0[3], 1)), ≥))



    We simplified constraint (24) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (25)    (x0[3] + [-1] ≥ 0 ⇒ (UIncreasing(COND_476_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 426_0_<init>_Return, x0[3], 1)), ≥)∧[bni_22 + (-1)Bound*bni_22] + [(2)bni_22]x0[3] ≥ 0∧[(-1)bso_23] ≥ 0)



    We simplified constraint (25) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (26)    (x0[3] + [-1] ≥ 0 ⇒ (UIncreasing(COND_476_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 426_0_<init>_Return, x0[3], 1)), ≥)∧[bni_22 + (-1)Bound*bni_22] + [(2)bni_22]x0[3] ≥ 0∧[(-1)bso_23] ≥ 0)



    We simplified constraint (26) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (27)    (x0[3] + [-1] ≥ 0 ⇒ (UIncreasing(COND_476_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 426_0_<init>_Return, x0[3], 1)), ≥)∧[bni_22 + (-1)Bound*bni_22] + [(2)bni_22]x0[3] ≥ 0∧[(-1)bso_23] ≥ 0)



    We simplified constraint (27) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (28)    (x0[3] ≥ 0 ⇒ (UIncreasing(COND_476_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 426_0_<init>_Return, x0[3], 1)), ≥)∧[(3)bni_22 + (-1)Bound*bni_22] + [(2)bni_22]x0[3] ≥ 0∧[(-1)bso_23] ≥ 0)







For Pair COND_476_1_<INIT>_INVOKEMETHOD(TRUE, 426_0_<init>_Return, x0, 1) → 397_0_<INIT>_INVOKEMETHOD(-(x0, 1)) the following chains were created:
  • We consider the chain COND_476_1_<INIT>_INVOKEMETHOD(TRUE, 426_0_<init>_Return, x0[4], 1) → 397_0_<INIT>_INVOKEMETHOD(-(x0[4], 1)) which results in the following constraint:

    (29)    (COND_476_1_<INIT>_INVOKEMETHOD(TRUE, 426_0_<init>_Return, x0[4], 1)≥NonInfC∧COND_476_1_<INIT>_INVOKEMETHOD(TRUE, 426_0_<init>_Return, x0[4], 1)≥397_0_<INIT>_INVOKEMETHOD(-(x0[4], 1))∧(UIncreasing(397_0_<INIT>_INVOKEMETHOD(-(x0[4], 1))), ≥))



    We simplified constraint (29) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (30)    ((UIncreasing(397_0_<INIT>_INVOKEMETHOD(-(x0[4], 1))), ≥)∧[bni_24] = 0∧[2 + (-1)bso_25] ≥ 0)



    We simplified constraint (30) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (31)    ((UIncreasing(397_0_<INIT>_INVOKEMETHOD(-(x0[4], 1))), ≥)∧[bni_24] = 0∧[2 + (-1)bso_25] ≥ 0)



    We simplified constraint (31) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (32)    ((UIncreasing(397_0_<INIT>_INVOKEMETHOD(-(x0[4], 1))), ≥)∧[bni_24] = 0∧[2 + (-1)bso_25] ≥ 0)



    We simplified constraint (32) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (33)    ((UIncreasing(397_0_<INIT>_INVOKEMETHOD(-(x0[4], 1))), ≥)∧[bni_24] = 0∧0 = 0∧[2 + (-1)bso_25] ≥ 0)







For Pair 476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0, x1) → COND_476_1_<INIT>_INVOKEMETHOD1(>(x0, 0), 426_0_<init>_Return, x0, x1) the following chains were created:
  • We consider the chain 476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0[5], x1[5]) → COND_476_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 426_0_<init>_Return, x0[5], x1[5]), COND_476_1_<INIT>_INVOKEMETHOD1(TRUE, 426_0_<init>_Return, x0[6], x1[6]) → 397_0_<INIT>_INVOKEMETHOD(-(x0[6], 1)) which results in the following constraint:

    (34)    (>(x0[5], 0)=TRUEx0[5]=x0[6]x1[5]=x1[6]476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0[5], x1[5])≥NonInfC∧476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0[5], x1[5])≥COND_476_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 426_0_<init>_Return, x0[5], x1[5])∧(UIncreasing(COND_476_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 426_0_<init>_Return, x0[5], x1[5])), ≥))



    We simplified constraint (34) using rule (IV) which results in the following new constraint:

    (35)    (>(x0[5], 0)=TRUE476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0[5], x1[5])≥NonInfC∧476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0[5], x1[5])≥COND_476_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 426_0_<init>_Return, x0[5], x1[5])∧(UIncreasing(COND_476_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 426_0_<init>_Return, x0[5], x1[5])), ≥))



    We simplified constraint (35) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (36)    (x0[5] + [-1] ≥ 0 ⇒ (UIncreasing(COND_476_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 426_0_<init>_Return, x0[5], x1[5])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [(2)bni_26]x0[5] ≥ 0∧[1 + (-1)bso_27] ≥ 0)



    We simplified constraint (36) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (37)    (x0[5] + [-1] ≥ 0 ⇒ (UIncreasing(COND_476_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 426_0_<init>_Return, x0[5], x1[5])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [(2)bni_26]x0[5] ≥ 0∧[1 + (-1)bso_27] ≥ 0)



    We simplified constraint (37) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (38)    (x0[5] + [-1] ≥ 0 ⇒ (UIncreasing(COND_476_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 426_0_<init>_Return, x0[5], x1[5])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [(2)bni_26]x0[5] ≥ 0∧[1 + (-1)bso_27] ≥ 0)



    We simplified constraint (38) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (39)    (x0[5] + [-1] ≥ 0 ⇒ (UIncreasing(COND_476_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 426_0_<init>_Return, x0[5], x1[5])), ≥)∧0 = 0∧[bni_26 + (-1)Bound*bni_26] + [(2)bni_26]x0[5] ≥ 0∧0 = 0∧[1 + (-1)bso_27] ≥ 0)



    We simplified constraint (39) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (40)    (x0[5] ≥ 0 ⇒ (UIncreasing(COND_476_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 426_0_<init>_Return, x0[5], x1[5])), ≥)∧0 = 0∧[(3)bni_26 + (-1)Bound*bni_26] + [(2)bni_26]x0[5] ≥ 0∧0 = 0∧[1 + (-1)bso_27] ≥ 0)







For Pair COND_476_1_<INIT>_INVOKEMETHOD1(TRUE, 426_0_<init>_Return, x0, x1) → 397_0_<INIT>_INVOKEMETHOD(-(x0, 1)) the following chains were created:
  • We consider the chain COND_476_1_<INIT>_INVOKEMETHOD1(TRUE, 426_0_<init>_Return, x0[6], x1[6]) → 397_0_<INIT>_INVOKEMETHOD(-(x0[6], 1)) which results in the following constraint:

    (41)    (COND_476_1_<INIT>_INVOKEMETHOD1(TRUE, 426_0_<init>_Return, x0[6], x1[6])≥NonInfC∧COND_476_1_<INIT>_INVOKEMETHOD1(TRUE, 426_0_<init>_Return, x0[6], x1[6])≥397_0_<INIT>_INVOKEMETHOD(-(x0[6], 1))∧(UIncreasing(397_0_<INIT>_INVOKEMETHOD(-(x0[6], 1))), ≥))



    We simplified constraint (41) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (42)    ((UIncreasing(397_0_<INIT>_INVOKEMETHOD(-(x0[6], 1))), ≥)∧[bni_28] = 0∧[1 + (-1)bso_29] ≥ 0)



    We simplified constraint (42) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (43)    ((UIncreasing(397_0_<INIT>_INVOKEMETHOD(-(x0[6], 1))), ≥)∧[bni_28] = 0∧[1 + (-1)bso_29] ≥ 0)



    We simplified constraint (43) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (44)    ((UIncreasing(397_0_<INIT>_INVOKEMETHOD(-(x0[6], 1))), ≥)∧[bni_28] = 0∧[1 + (-1)bso_29] ≥ 0)



    We simplified constraint (44) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (45)    ((UIncreasing(397_0_<INIT>_INVOKEMETHOD(-(x0[6], 1))), ≥)∧[bni_28] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_29] ≥ 0)







To summarize, we get the following constraints P for the following pairs.
  • 397_0_<INIT>_INVOKEMETHOD(x0) → COND_397_0_<INIT>_INVOKEMETHOD(>(x0, 1), x0)
    • (x0[0] ≥ 0 ⇒ (UIncreasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥)∧[(5)bni_16 + (-1)Bound*bni_16] + [(2)bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)
    • (x0[0] ≥ 0 ⇒ (UIncreasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥)∧[(5)bni_16 + (-1)Bound*bni_16] + [(2)bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)

  • COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0) → 476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(-(x0, 1)), x0, -(x0, 1))
    • ((UIncreasing(476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(-(x0[1], 1)), x0[1], -(x0[1], 1))), ≥)∧[bni_18] = 0∧0 = 0∧[(-1)bso_19] ≥ 0)

  • COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0) → 397_0_<INIT>_INVOKEMETHOD(-(x0, 1))
    • ((UIncreasing(397_0_<INIT>_INVOKEMETHOD(-(x0[2], 1))), ≥)∧[bni_20] = 0∧0 = 0∧[2 + (-1)bso_21] ≥ 0)

  • 476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0, 1) → COND_476_1_<INIT>_INVOKEMETHOD(>(x0, 0), 426_0_<init>_Return, x0, 1)
    • (x0[3] ≥ 0 ⇒ (UIncreasing(COND_476_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 426_0_<init>_Return, x0[3], 1)), ≥)∧[(3)bni_22 + (-1)Bound*bni_22] + [(2)bni_22]x0[3] ≥ 0∧[(-1)bso_23] ≥ 0)

  • COND_476_1_<INIT>_INVOKEMETHOD(TRUE, 426_0_<init>_Return, x0, 1) → 397_0_<INIT>_INVOKEMETHOD(-(x0, 1))
    • ((UIncreasing(397_0_<INIT>_INVOKEMETHOD(-(x0[4], 1))), ≥)∧[bni_24] = 0∧0 = 0∧[2 + (-1)bso_25] ≥ 0)

  • 476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0, x1) → COND_476_1_<INIT>_INVOKEMETHOD1(>(x0, 0), 426_0_<init>_Return, x0, x1)
    • (x0[5] ≥ 0 ⇒ (UIncreasing(COND_476_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 426_0_<init>_Return, x0[5], x1[5])), ≥)∧0 = 0∧[(3)bni_26 + (-1)Bound*bni_26] + [(2)bni_26]x0[5] ≥ 0∧0 = 0∧[1 + (-1)bso_27] ≥ 0)

  • COND_476_1_<INIT>_INVOKEMETHOD1(TRUE, 426_0_<init>_Return, x0, x1) → 397_0_<INIT>_INVOKEMETHOD(-(x0, 1))
    • ((UIncreasing(397_0_<INIT>_INVOKEMETHOD(-(x0[6], 1))), ≥)∧[bni_28] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_29] ≥ 0)




The constraints for P> respective Pbound 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 Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(634_1_<init>_InvokeMethod(x1, x2)) = [-1]   
POL(426_0_<init>_Return) = 0   
POL(1) = [1]   
POL(397_0_<INIT>_INVOKEMETHOD(x1)) = [1] + [2]x1   
POL(COND_397_0_<INIT>_INVOKEMETHOD(x1, x2)) = [1] + [2]x2   
POL(>(x1, x2)) = [-1]   
POL(476_1_<INIT>_INVOKEMETHOD(x1, x2, x3)) = [1] + [2]x2   
POL(397_0_<init>_InvokeMethod(x1)) = x1   
POL(-(x1, x2)) = x1 + [-1]x2   
POL(COND_476_1_<INIT>_INVOKEMETHOD(x1, x2, x3, x4)) = [1] + [2]x3   
POL(0) = 0   
POL(COND_476_1_<INIT>_INVOKEMETHOD1(x1, x2, x3, x4)) = [2]x3   

The following pairs are in P>:

COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0[2]) → 397_0_<INIT>_INVOKEMETHOD(-(x0[2], 1))
COND_476_1_<INIT>_INVOKEMETHOD(TRUE, 426_0_<init>_Return, x0[4], 1) → 397_0_<INIT>_INVOKEMETHOD(-(x0[4], 1))
476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0[5], x1[5]) → COND_476_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 426_0_<init>_Return, x0[5], x1[5])
COND_476_1_<INIT>_INVOKEMETHOD1(TRUE, 426_0_<init>_Return, x0[6], x1[6]) → 397_0_<INIT>_INVOKEMETHOD(-(x0[6], 1))

The following pairs are in Pbound:

397_0_<INIT>_INVOKEMETHOD(x0[0]) → COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])
476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0[3], 1) → COND_476_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 426_0_<init>_Return, x0[3], 1)
476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0[5], x1[5]) → COND_476_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 426_0_<init>_Return, x0[5], x1[5])

The following pairs are in P:

397_0_<INIT>_INVOKEMETHOD(x0[0]) → COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])
COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0[1]) → 476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(-(x0[1], 1)), x0[1], -(x0[1], 1))
476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0[3], 1) → COND_476_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 426_0_<init>_Return, x0[3], 1)

There are no usable rules.

(20) Complex Obligation (AND)

(21) 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:

Integer


The ITRS R consists of the following rules:
634_1_<init>_InvokeMethod(426_0_<init>_Return, 1) → 426_0_<init>_Return
634_1_<init>_InvokeMethod(426_0_<init>_Return, x0) → 426_0_<init>_Return

The integer pair graph contains the following rules and edges:
(0): 397_0_<INIT>_INVOKEMETHOD(x0[0]) → COND_397_0_<INIT>_INVOKEMETHOD(x0[0] > 1, x0[0])
(1): COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0[1]) → 476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(x0[1] - 1), x0[1], x0[1] - 1)
(3): 476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0[3], 1) → COND_476_1_<INIT>_INVOKEMETHOD(x0[3] > 0, 426_0_<init>_Return, x0[3], 1)

(0) -> (1), if (x0[0] > 1x0[0]* x0[1])


(1) -> (3), if (397_0_<init>_InvokeMethod(x0[1] - 1) →* 426_0_<init>_Returnx0[1]* x0[3]x0[1] - 1* 1)



The set Q consists of the following terms:
634_1_<init>_InvokeMethod(426_0_<init>_Return, x0)

(22) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 less nodes.

(23) TRUE

(24) 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:

Integer


The ITRS R consists of the following rules:
634_1_<init>_InvokeMethod(426_0_<init>_Return, 1) → 426_0_<init>_Return
634_1_<init>_InvokeMethod(426_0_<init>_Return, x0) → 426_0_<init>_Return

The integer pair graph contains the following rules and edges:
(1): COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0[1]) → 476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(x0[1] - 1), x0[1], x0[1] - 1)
(2): COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0[2]) → 397_0_<INIT>_INVOKEMETHOD(x0[2] - 1)
(4): COND_476_1_<INIT>_INVOKEMETHOD(TRUE, 426_0_<init>_Return, x0[4], 1) → 397_0_<INIT>_INVOKEMETHOD(x0[4] - 1)
(6): COND_476_1_<INIT>_INVOKEMETHOD1(TRUE, 426_0_<init>_Return, x0[6], x1[6]) → 397_0_<INIT>_INVOKEMETHOD(x0[6] - 1)


The set Q consists of the following terms:
634_1_<init>_InvokeMethod(426_0_<init>_Return, x0)

(25) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 4 less nodes.

(26) TRUE