Termination proof of /tmp/tmpmpI5

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 990 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 1400 ms)

        ↳7 IDP

        ↳8 IDPtoQDPProof (⇒, 40 ms)

        ↳9 QDP

        ↳10 UsableRulesProof (⇔, 0 ms)

        ↳11 QDP

        ↳12 QReductionProof (⇔, 0 ms)

        ↳13 QDP

        ↳14 QDPSizeChangeProof (⇔, 0 ms)

        ↳15 YES

    ↳16 JBCTerminationSCC

        ↳17 SCCToIDPv1Proof (⇒, 180 ms)

        ↳18 IDP

        ↳19 IDPNonInfProof (⇒, 350 ms)

        ↳20 AND

            ↳21 IDP

                ↳22 IDependencyGraphProof (⇔, 0 ms)

                ↳23 TRUE

            ↳24 IDP

                ↳25 IDependencyGraphProof (⇔, 0 ms)

                ↳26 TRUE

(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:
927_0_height_FieldAccess(EOS(STATIC_927), java.lang.Object(BTreeR(EOC, o336, o337)), java.lang.Object(BTreeR(EOC, o336, o337))) → 928_0_height_FieldAccess(EOS(STATIC_928), java.lang.Object(BTreeR(EOC, o336, o337)), java.lang.Object(BTreeR(EOC, o336, o337)))
928_0_height_FieldAccess(EOS(STATIC_928), java.lang.Object(BTreeR(EOC, o336, o337)), java.lang.Object(BTreeR(EOC, o336, o337))) → 930_0_height_NONNULL(EOS(STATIC_930), java.lang.Object(BTreeR(EOC, o336, o337)), o336)
930_0_height_NONNULL(EOS(STATIC_930), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337)), java.lang.Object(o339sub)) → 931_0_height_NONNULL(EOS(STATIC_931), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337)), java.lang.Object(o339sub))
930_0_height_NONNULL(EOS(STATIC_930), java.lang.Object(BTreeR(EOC, NULL, o337)), NULL) → 932_0_height_NONNULL(EOS(STATIC_932), java.lang.Object(BTreeR(EOC, NULL, o337)), NULL)
931_0_height_NONNULL(EOS(STATIC_931), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337)), java.lang.Object(o339sub)) → 933_0_height_Load(EOS(STATIC_933), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337)))
933_0_height_Load(EOS(STATIC_933), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337))) → 936_0_height_FieldAccess(EOS(STATIC_936), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337)), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337)))
936_0_height_FieldAccess(EOS(STATIC_936), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337)), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337))) → 939_0_height_NONNULL(EOS(STATIC_939), 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, java.lang.Object(o339sub), o337)), java.lang.Object(o339sub)) → 941_0_height_ConstantStackPush(EOS(STATIC_941), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337)))
941_0_height_ConstantStackPush(EOS(STATIC_941), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337))) → 945_0_height_Load(EOS(STATIC_945), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337)))
945_0_height_Load(EOS(STATIC_945), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337))) → 949_0_height_FieldAccess(EOS(STATIC_949), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337)))
949_0_height_FieldAccess(EOS(STATIC_949), java.lang.Object(BTreeR(EOC, java.lang.Object(o339sub), o337))) → 953_0_height_InvokeMethod(EOS(STATIC_953), java.lang.Object(o339sub))
953_0_height_InvokeMethod(EOS(STATIC_953), java.lang.Object(o339sub)) → 957_1_height_InvokeMethod(957_0_height_Load(EOS(STATIC_957), java.lang.Object(o339sub)), java.lang.Object(o339sub))
957_0_height_Load(EOS(STATIC_957), java.lang.Object(o339sub)) → 963_0_height_Load(EOS(STATIC_963), java.lang.Object(o339sub))
963_0_height_Load(EOS(STATIC_963), java.lang.Object(o339sub)) → 925_0_height_Load(EOS(STATIC_925), java.lang.Object(o339sub))
925_0_height_Load(EOS(STATIC_925), java.lang.Object(o330sub)) → 927_0_height_FieldAccess(EOS(STATIC_927), java.lang.Object(o330sub), java.lang.Object(o330sub))
932_0_height_NONNULL(EOS(STATIC_932), java.lang.Object(BTreeR(EOC, NULL, o337)), NULL) → 935_0_height_Load(EOS(STATIC_935), java.lang.Object(BTreeR(EOC, NULL, o337)))
935_0_height_Load(EOS(STATIC_935), java.lang.Object(BTreeR(EOC, NULL, o337))) → 937_0_height_FieldAccess(EOS(STATIC_937), java.lang.Object(BTreeR(EOC, NULL, o337)), java.lang.Object(BTreeR(EOC, NULL, o337)))
937_0_height_FieldAccess(EOS(STATIC_937), java.lang.Object(BTreeR(EOC, NULL, o337)), java.lang.Object(BTreeR(EOC, NULL, o337))) → 940_0_height_NONNULL(EOS(STATIC_940), java.lang.Object(BTreeR(EOC, NULL, o337)), o337)
940_0_height_NONNULL(EOS(STATIC_940), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))), java.lang.Object(o341sub)) → 942_0_height_NONNULL(EOS(STATIC_942), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))), java.lang.Object(o341sub))
942_0_height_NONNULL(EOS(STATIC_942), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))), java.lang.Object(o341sub)) → 946_0_height_Load(EOS(STATIC_946), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))))
946_0_height_Load(EOS(STATIC_946), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub)))) → 951_0_height_FieldAccess(EOS(STATIC_951), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))))
951_0_height_FieldAccess(EOS(STATIC_951), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub)))) → 954_0_height_NONNULL(EOS(STATIC_954), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))), NULL)
954_0_height_NONNULL(EOS(STATIC_954), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))), NULL) → 958_0_height_ConstantStackPush(EOS(STATIC_958), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))))
958_0_height_ConstantStackPush(EOS(STATIC_958), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub)))) → 964_0_height_Load(EOS(STATIC_964), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))))
964_0_height_Load(EOS(STATIC_964), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub)))) → 969_0_height_FieldAccess(EOS(STATIC_969), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))))
969_0_height_FieldAccess(EOS(STATIC_969), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub)))) → 973_0_height_InvokeMethod(EOS(STATIC_973), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))), java.lang.Object(o341sub))
973_0_height_InvokeMethod(EOS(STATIC_973), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))), java.lang.Object(o341sub)) → 975_1_height_InvokeMethod(975_0_height_Load(EOS(STATIC_975), java.lang.Object(o341sub)), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(o341sub))), java.lang.Object(o341sub))
975_0_height_Load(EOS(STATIC_975), java.lang.Object(o341sub)) → 977_0_height_Load(EOS(STATIC_977), java.lang.Object(o341sub))
977_0_height_Load(EOS(STATIC_977), java.lang.Object(o341sub)) → 925_0_height_Load(EOS(STATIC_925), java.lang.Object(o341sub))
R rules:
940_0_height_NONNULL(EOS(STATIC_940), java.lang.Object(BTreeR(EOC, NULL, NULL)), NULL) → 943_0_height_NONNULL(EOS(STATIC_943), java.lang.Object(BTreeR(EOC, NULL, NULL)), NULL)
943_0_height_NONNULL(EOS(STATIC_943), java.lang.Object(BTreeR(EOC, NULL, NULL)), NULL) → 947_0_height_ConstantStackPush(EOS(STATIC_947), java.lang.Object(BTreeR(EOC, NULL, NULL)))
947_0_height_ConstantStackPush(EOS(STATIC_947), java.lang.Object(BTreeR(EOC, NULL, NULL))) → 952_0_height_Return(EOS(STATIC_952), java.lang.Object(BTreeR(EOC, NULL, NULL)))
957_1_height_InvokeMethod(952_0_height_Return(EOS(STATIC_952), java.lang.Object(BTreeR(EOC, NULL, NULL))), java.lang.Object(BTreeR(EOC, NULL, NULL))) → 974_0_height_Return(EOS(STATIC_974), java.lang.Object(BTreeR(EOC, NULL, NULL)), java.lang.Object(BTreeR(EOC, NULL, NULL)))
957_1_height_InvokeMethod(979_0_height_Return(EOS(STATIC_979)), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), o395))) → 1017_0_height_Return(EOS(STATIC_1017), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), o395)))
957_1_height_InvokeMethod(1028_0_height_Return(EOS(STATIC_1028), 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))))) → 1088_0_height_Return(EOS(STATIC_1088), 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)))))
957_1_height_InvokeMethod(1676_0_height_Return(EOS(STATIC_1676)), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1935, o1936)), o1937)), o1938))) → 1744_0_height_Return(EOS(STATIC_1744), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1935, o1936)), o1937)), o1938)))
957_1_height_InvokeMethod(1679_0_height_Return(EOS(STATIC_1679), 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, 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)))))
957_1_height_InvokeMethod(1683_0_height_Return(EOS(STATIC_1683)), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1998, o1999)))), o2000))) → 1787_0_height_Return(EOS(STATIC_1787), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1998, o1999)))), o2000)))
957_1_height_InvokeMethod(1687_0_height_Return(EOS(STATIC_1687), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2017, o2018))))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2017, o2018))))))) → 1799_0_height_Return(EOS(STATIC_1799), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2017, o2018)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2017, o2018)))))))
974_0_height_Return(EOS(STATIC_974), java.lang.Object(BTreeR(EOC, NULL, NULL)), java.lang.Object(BTreeR(EOC, NULL, NULL))) → 976_0_height_IntArithmetic(EOS(STATIC_976))
975_1_height_InvokeMethod(952_0_height_Return(EOS(STATIC_952), 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)))
975_1_height_InvokeMethod(979_0_height_Return(EOS(STATIC_979)), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), o366)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), o366))) → 1013_0_height_Return(EOS(STATIC_1013), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), o366)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), o366)))
975_1_height_InvokeMethod(1028_0_height_Return(EOS(STATIC_1028), 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))))) → 1089_0_height_Return(EOS(STATIC_1089), 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)))))
975_1_height_InvokeMethod(1676_0_height_Return(EOS(STATIC_1676)), 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))) → 1749_0_height_Return(EOS(STATIC_1749), 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)))
975_1_height_InvokeMethod(1679_0_height_Return(EOS(STATIC_1679), 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))))) → 1773_0_height_Return(EOS(STATIC_1773), 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)))))
975_1_height_InvokeMethod(1683_0_height_Return(EOS(STATIC_1683)), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2005, o2006)))), o2007)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2005, o2006)))), o2007))) → 1793_0_height_Return(EOS(STATIC_1793), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2005, o2006)))), o2007)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2005, o2006)))), o2007)))
975_1_height_InvokeMethod(1687_0_height_Return(EOS(STATIC_1687), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2023, o2024))))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2023, o2024)))))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2023, o2024))))))) → 1804_0_height_Return(EOS(STATIC_1804), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2023, o2024)))))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2023, o2024)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2023, o2024)))))))
976_0_height_IntArithmetic(EOS(STATIC_976)) → 979_0_height_Return(EOS(STATIC_979))
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))) → 1018_0_height_IntArithmetic(EOS(STATIC_1018), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))))
1013_0_height_Return(EOS(STATIC_1013), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), o366)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), o366))) → 1136_0_height_Return(EOS(STATIC_1136), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), o366)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), o366)))
1017_0_height_Return(EOS(STATIC_1017), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), o395))) → 1130_0_height_Return(EOS(STATIC_1130), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), o395)))
1018_0_height_IntArithmetic(EOS(STATIC_1018), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL))))) → 1028_0_height_Return(EOS(STATIC_1028), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))))
1088_0_height_Return(EOS(STATIC_1088), 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)))))
1089_0_height_Return(EOS(STATIC_1089), 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))))) → 1110_0_height_Return(EOS(STATIC_1110), 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))))) → 1279_0_height_Return(EOS(STATIC_1279), 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)))))
1110_0_height_Return(EOS(STATIC_1110), 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))))) → 1294_0_height_Return(EOS(STATIC_1294), 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)))))
1130_0_height_Return(EOS(STATIC_1130), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o539, o540)), o541))) → 1252_0_height_Return(EOS(STATIC_1252), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o539, o540)), o541)))
1136_0_height_Return(EOS(STATIC_1136), 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))) → 1265_0_height_Return(EOS(STATIC_1265), 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)))
1252_0_height_Return(EOS(STATIC_1252), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o825, o826)), o827))) → 1407_0_height_Return(EOS(STATIC_1407), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o825, o826)), o827)))
1265_0_height_Return(EOS(STATIC_1265), 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))) → 1415_0_height_Return(EOS(STATIC_1415), 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)))
1279_0_height_Return(EOS(STATIC_1279), 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))))) → 1434_0_height_Return(EOS(STATIC_1434), 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)))))
1294_0_height_Return(EOS(STATIC_1294), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o919, o920)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o919, o920)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o919, o920))))) → 1451_0_height_Return(EOS(STATIC_1451), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o919, o920)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o919, o920)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o919, o920)))))
1407_0_height_Return(EOS(STATIC_1407), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1244, o1245)), o1246))) → 1579_0_height_Return(EOS(STATIC_1579), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1244, o1245)), o1246)))
1415_0_height_Return(EOS(STATIC_1415), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1284, o1285)), o1286)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1284, o1285)), o1286))) → 1593_0_height_Return(EOS(STATIC_1593), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1284, o1285)), o1286)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1284, o1285)), o1286)))
1434_0_height_Return(EOS(STATIC_1434), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1312, o1313)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1312, o1313))))) → 1606_0_height_Return(EOS(STATIC_1606), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1312, o1313)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1312, o1313)))))
1451_0_height_Return(EOS(STATIC_1451), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1341, o1342)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1341, o1342)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1341, o1342))))) → 1628_0_height_Return(EOS(STATIC_1628), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1341, o1342)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1341, o1342)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1341, o1342)))))
1579_0_height_Return(EOS(STATIC_1579), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1659, o1660)), o1661))) → 1660_0_height_IntArithmetic(EOS(STATIC_1660))
1593_0_height_Return(EOS(STATIC_1593), 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))) → 1662_0_height_IntArithmetic(EOS(STATIC_1662), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1699, o1700)), o1701)))))
1606_0_height_Return(EOS(STATIC_1606), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1726, o1727)))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1726, o1727))))) → 1665_0_height_IntArithmetic(EOS(STATIC_1665))
1628_0_height_Return(EOS(STATIC_1628), 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))))) → 1668_0_height_IntArithmetic(EOS(STATIC_1668), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1754, o1755)))))))
1660_0_height_IntArithmetic(EOS(STATIC_1660)) → 1676_0_height_Return(EOS(STATIC_1676))
1662_0_height_IntArithmetic(EOS(STATIC_1662), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1699, o1700)), o1701))))) → 1679_0_height_Return(EOS(STATIC_1679), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1699, o1700)), o1701)))))
1665_0_height_IntArithmetic(EOS(STATIC_1665)) → 1683_0_height_Return(EOS(STATIC_1683))
1668_0_height_IntArithmetic(EOS(STATIC_1668), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1754, o1755))))))) → 1687_0_height_Return(EOS(STATIC_1687), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1754, o1755)))))))
1744_0_height_Return(EOS(STATIC_1744), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1935, o1936)), o1937)), o1938))) → 1579_0_height_Return(EOS(STATIC_1579), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, o1935, o1936)), o1937)), o1938)))
1749_0_height_Return(EOS(STATIC_1749), 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))) → 1593_0_height_Return(EOS(STATIC_1593), 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)))
1761_0_height_Return(EOS(STATIC_1761), 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))))) → 1606_0_height_Return(EOS(STATIC_1606), 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)))))
1773_0_height_Return(EOS(STATIC_1773), 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))))) → 1628_0_height_Return(EOS(STATIC_1628), 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)))))
1787_0_height_Return(EOS(STATIC_1787), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1998, o1999)))), o2000))) → 1579_0_height_Return(EOS(STATIC_1579), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o1998, o1999)))), o2000)))
1793_0_height_Return(EOS(STATIC_1793), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2005, o2006)))), o2007)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2005, o2006)))), o2007))) → 1593_0_height_Return(EOS(STATIC_1593), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2005, o2006)))), o2007)))), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2005, o2006)))), o2007)))
1799_0_height_Return(EOS(STATIC_1799), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2017, o2018)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2017, o2018))))))) → 1606_0_height_Return(EOS(STATIC_1606), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2017, o2018)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2017, o2018)))))))
1804_0_height_Return(EOS(STATIC_1804), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2023, o2024)))))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2023, o2024)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2023, o2024))))))) → 1628_0_height_Return(EOS(STATIC_1628), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2023, o2024)))))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2023, o2024)))))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, o2023, o2024)))))))

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

P rules:
927_0_height_FieldAccess(EOS(STATIC_927), java.lang.Object(BTreeR(EOC, java.lang.Object(x0), x1)), java.lang.Object(BTreeR(EOC, java.lang.Object(x0), x1))) → 957_1_height_InvokeMethod(927_0_height_FieldAccess(EOS(STATIC_927), java.lang.Object(x0), java.lang.Object(x0)), java.lang.Object(x0))
927_0_height_FieldAccess(EOS(STATIC_927), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(x0))), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(x0)))) → 975_1_height_InvokeMethod(927_0_height_FieldAccess(EOS(STATIC_927), java.lang.Object(x0), java.lang.Object(x0)), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(x0))), java.lang.Object(x0))
R rules:
957_1_height_InvokeMethod(952_0_height_Return(EOS(STATIC_952), java.lang.Object(BTreeR(EOC, NULL, NULL))), java.lang.Object(BTreeR(EOC, NULL, NULL))) → 979_0_height_Return(EOS(STATIC_979))
975_1_height_InvokeMethod(952_0_height_Return(EOS(STATIC_952), 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))) → 1028_0_height_Return(EOS(STATIC_1028), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, NULL, NULL)))))
957_1_height_InvokeMethod(1676_0_height_Return(EOS(STATIC_1676)), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, x0, x1)), x2)), x3))) → 1676_0_height_Return(EOS(STATIC_1676))
957_1_height_InvokeMethod(1683_0_height_Return(EOS(STATIC_1683)), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, x0, x1)))), x2))) → 1676_0_height_Return(EOS(STATIC_1676))
957_1_height_InvokeMethod(979_0_height_Return(EOS(STATIC_979)), java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), x0))) → 1676_0_height_Return(EOS(STATIC_1676))
975_1_height_InvokeMethod(1676_0_height_Return(EOS(STATIC_1676)), 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))) → 1679_0_height_Return(EOS(STATIC_1679), 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)))))
975_1_height_InvokeMethod(1683_0_height_Return(EOS(STATIC_1683)), 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))) → 1679_0_height_Return(EOS(STATIC_1679), 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)))))
975_1_height_InvokeMethod(979_0_height_Return(EOS(STATIC_979)), 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))) → 1679_0_height_Return(EOS(STATIC_1679), java.lang.Object(BTreeR(EOC, NULL, java.lang.Object(BTreeR(EOC, java.lang.Object(BTreeR(EOC, NULL, NULL)), x0)))))
957_1_height_InvokeMethod(1679_0_height_Return(EOS(STATIC_1679), 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))))) → 1683_0_height_Return(EOS(STATIC_1683))
957_1_height_InvokeMethod(1687_0_height_Return(EOS(STATIC_1687), 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))))))) → 1683_0_height_Return(EOS(STATIC_1683))
957_1_height_InvokeMethod(1028_0_height_Return(EOS(STATIC_1028), 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))))) → 1683_0_height_Return(EOS(STATIC_1683))
975_1_height_InvokeMethod(1679_0_height_Return(EOS(STATIC_1679), 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))))) → 1687_0_height_Return(EOS(STATIC_1687), 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)))))))
975_1_height_InvokeMethod(1687_0_height_Return(EOS(STATIC_1687), 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))))))) → 1687_0_height_Return(EOS(STATIC_1687), 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)))))))))
975_1_height_InvokeMethod(1028_0_height_Return(EOS(STATIC_1028), 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))))) → 1687_0_height_Return(EOS(STATIC_1687), 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)
927_0_height_FieldAccess(x1, x2, x3) → 927_0_height_FieldAccess(x2, x3)
1687_0_height_Return(x1, x2) → 1687_0_height_Return(x2)
1028_0_height_Return(x1, x2) → 1028_0_height_Return
1679_0_height_Return(x1, x2) → 1679_0_height_Return(x2)
1683_0_height_Return(x1) → 1683_0_height_Return
979_0_height_Return(x1) → 979_0_height_Return
1676_0_height_Return(x1) → 1676_0_height_Return
952_0_height_Return(x1, x2) → 952_0_height_Return

Filtered duplicate args:

927_0_height_FieldAccess(x1, x2) → 927_0_height_FieldAccess(x2)
975_1_height_InvokeMethod(x1, x2, x3) → 975_1_height_InvokeMethod(x1, x2)

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

P rules:
927_0_height_FieldAccess(java.lang.Object(BTreeR(java.lang.Object(x0), x1))) → 957_1_height_InvokeMethod(927_0_height_FieldAccess(java.lang.Object(x0)), java.lang.Object(x0))
927_0_height_FieldAccess(java.lang.Object(BTreeR(NULL, java.lang.Object(x0)))) → 975_1_height_InvokeMethod(927_0_height_FieldAccess(java.lang.Object(x0)), java.lang.Object(BTreeR(NULL, java.lang.Object(x0))))
R rules:
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, NULL))) → 979_0_height_Return
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))) → 1028_0_height_Return
957_1_height_InvokeMethod(1676_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3))) → 1676_0_height_Return
957_1_height_InvokeMethod(1683_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2))) → 1676_0_height_Return
957_1_height_InvokeMethod(979_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0))) → 1676_0_height_Return
975_1_height_InvokeMethod(1676_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3))))) → 1679_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3)))))
975_1_height_InvokeMethod(1683_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2))))) → 1679_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2)))))
975_1_height_InvokeMethod(979_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0))))) → 1679_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0)))))
957_1_height_InvokeMethod(1679_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))))) → 1683_0_height_Return
957_1_height_InvokeMethod(1687_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))))))) → 1683_0_height_Return
957_1_height_InvokeMethod(1028_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))) → 1683_0_height_Return
975_1_height_InvokeMethod(1679_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))))))) → 1687_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)))))))
975_1_height_InvokeMethod(1687_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))))))))) → 1687_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))))))))
975_1_height_InvokeMethod(1028_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))))) → 1687_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: {[952_0_height_Return, 979_0_height_Return, 1028_0_height_Return, 1676_0_height_Return, 1683_0_height_Return]=952_0_height_Return}

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

P rules:
927_0_HEIGHT_FIELDACCESS(java.lang.Object(BTreeR(java.lang.Object(x0), x1))) → 927_0_HEIGHT_FIELDACCESS(java.lang.Object(x0))
927_0_HEIGHT_FIELDACCESS(java.lang.Object(BTreeR(NULL, java.lang.Object(x0)))) → 927_0_HEIGHT_FIELDACCESS(java.lang.Object(x0))
R rules:
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, NULL))) → 952_0_height_Return
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))) → 952_0_height_Return
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3))) → 952_0_height_Return
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2))) → 952_0_height_Return
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0))) → 952_0_height_Return
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3))))) → 1679_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3)))))
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2))))) → 1679_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2)))))
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0))))) → 1679_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0)))))
957_1_height_InvokeMethod(1679_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))))) → 952_0_height_Return
957_1_height_InvokeMethod(1687_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))))))) → 952_0_height_Return
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))) → 952_0_height_Return
975_1_height_InvokeMethod(1679_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))))))) → 1687_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)))))))
975_1_height_InvokeMethod(1687_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))))))))) → 1687_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))))))))
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))))) → 1687_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:
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, NULL))) → 952_0_height_Return
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))) → 952_0_height_Return
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3))) → 952_0_height_Return
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2))) → 952_0_height_Return
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0))) → 952_0_height_Return
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3))))) → 1679_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3)))))
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2))))) → 1679_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2)))))
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0))))) → 1679_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0)))))
957_1_height_InvokeMethod(1679_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))))) → 952_0_height_Return
957_1_height_InvokeMethod(1687_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))))))) → 952_0_height_Return
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))) → 952_0_height_Return
975_1_height_InvokeMethod(1679_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))))))) → 1687_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)))))))
975_1_height_InvokeMethod(1687_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))))))))) → 1687_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))))))))
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))))) → 1687_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): 927_0_HEIGHT_FIELDACCESS(java.lang.Object(BTreeR(java.lang.Object(x0[0]), x1[0]))) → 927_0_HEIGHT_FIELDACCESS(java.lang.Object(x0[0]))
(1): 927_0_HEIGHT_FIELDACCESS(java.lang.Object(BTreeR(NULL, java.lang.Object(x0[1])))) → 927_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:
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, NULL)))
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL)))))
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3)))
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2)))
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0)))
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3)))))
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2)))))
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0)))))
957_1_height_InvokeMethod(1679_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)))))
957_1_height_InvokeMethod(1687_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)))))))
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL)))))
975_1_height_InvokeMethod(1679_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)))))))
975_1_height_InvokeMethod(1687_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)))))))))
975_1_height_InvokeMethod(952_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:

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

The TRS R consists of the following rules:

957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, NULL))) → 952_0_height_Return
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))) → 952_0_height_Return
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3))) → 952_0_height_Return
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2))) → 952_0_height_Return
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0))) → 952_0_height_Return
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3))))) → 1679_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3)))))
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2))))) → 1679_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2)))))
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0))))) → 1679_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0)))))
957_1_height_InvokeMethod(1679_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))))) → 952_0_height_Return
957_1_height_InvokeMethod(1687_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))))))) → 952_0_height_Return
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))) → 952_0_height_Return
975_1_height_InvokeMethod(1679_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))))))) → 1687_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)))))))
975_1_height_InvokeMethod(1687_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))))))))) → 1687_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))))))))
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))))) → 1687_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:

957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, NULL)))
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL)))))
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3)))
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2)))
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0)))
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3)))))
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2)))))
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0)))))
957_1_height_InvokeMethod(1679_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)))))
957_1_height_InvokeMethod(1687_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)))))))
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL)))))
975_1_height_InvokeMethod(1679_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)))))))
975_1_height_InvokeMethod(1687_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)))))))))
975_1_height_InvokeMethod(952_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:

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

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

957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, NULL)))
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL)))))
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3)))
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2)))
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0)))
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3)))))
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2)))))
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0)))))
957_1_height_InvokeMethod(1679_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)))))
957_1_height_InvokeMethod(1687_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)))))))
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL)))))
975_1_height_InvokeMethod(1679_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)))))))
975_1_height_InvokeMethod(1687_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)))))))))
975_1_height_InvokeMethod(952_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].

957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, NULL)))
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL)))))
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3)))
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2)))
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0)))
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3)))))
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2)))))
975_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0)))))
957_1_height_InvokeMethod(1679_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)))))
957_1_height_InvokeMethod(1687_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)))))))
957_1_height_InvokeMethod(952_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL)))))
975_1_height_InvokeMethod(1679_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)))))))
975_1_height_InvokeMethod(1687_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)))))))))
975_1_height_InvokeMethod(952_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:

927_0_HEIGHT_FIELDACCESS(java.lang.Object(BTreeR(java.lang.Object(x0[0]), x1[0]))) → 927_0_HEIGHT_FIELDACCESS(java.lang.Object(x0[0]))
927_0_HEIGHT_FIELDACCESS(java.lang.Object(BTreeR(NULL, java.lang.Object(x0[1])))) → 927_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:

927_0_HEIGHT_FIELDACCESS(java.lang.Object(BTreeR(java.lang.Object(x0[0]), x1[0]))) → 927_0_HEIGHT_FIELDACCESS(java.lang.Object(x0[0]))
The graph contains the following edges 1 > 1
927_0_HEIGHT_FIELDACCESS(java.lang.Object(BTreeR(NULL, java.lang.Object(x0[1])))) → 927_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:
401_0_<init>_InvokeMethod(EOS(STATIC_401), i58) → 406_0_<init>_Load(EOS(STATIC_406), i58)
406_0_<init>_Load(EOS(STATIC_406), i58) → 412_0_<init>_ConstantStackPush(EOS(STATIC_412), i58, i58)
412_0_<init>_ConstantStackPush(EOS(STATIC_412), i58, i58) → 423_0_<init>_LE(EOS(STATIC_423), i58, i58, 1)
423_0_<init>_LE(EOS(STATIC_423), i64, i64, matching1) → 430_0_<init>_LE(EOS(STATIC_430), i64, i64, 1) | =(matching1, 1)
430_0_<init>_LE(EOS(STATIC_430), i64, i64, matching1) → 438_0_<init>_Load(EOS(STATIC_438), i64) | &&(>(i64, 1), =(matching1, 1))
438_0_<init>_Load(EOS(STATIC_438), i64) → 447_0_<init>_New(EOS(STATIC_447), i64)
447_0_<init>_New(EOS(STATIC_447), i64) → 466_0_<init>_Duplicate(EOS(STATIC_466), i64)
466_0_<init>_Duplicate(EOS(STATIC_466), i64) → 474_0_<init>_Load(EOS(STATIC_474), i64)
474_0_<init>_Load(EOS(STATIC_474), i64) → 478_0_<init>_ConstantStackPush(EOS(STATIC_478), i64, i64)
478_0_<init>_ConstantStackPush(EOS(STATIC_478), i64, i64) → 484_0_<init>_IntArithmetic(EOS(STATIC_484), i64, i64, 1)
484_0_<init>_IntArithmetic(EOS(STATIC_484), i64, i64, matching1) → 488_0_<init>_InvokeMethod(EOS(STATIC_488), i64, -(i64, 1)) | &&(>(i64, 0), =(matching1, 1))
488_0_<init>_InvokeMethod(EOS(STATIC_488), i64, i66) → 492_1_<init>_InvokeMethod(492_0_<init>_Load(EOS(STATIC_492), i66), i64, i66)
492_0_<init>_Load(EOS(STATIC_492), i66) → 494_0_<init>_Load(EOS(STATIC_494), i66)
492_1_<init>_InvokeMethod(436_0_<init>_Return(EOS(STATIC_436)), i64, matching1) → 503_0_<init>_Return(EOS(STATIC_503), i64, 1) | =(matching1, 1)
492_1_<init>_InvokeMethod(757_0_<init>_Return(EOS(STATIC_757)), i64, i133) → 846_0_<init>_Return(EOS(STATIC_846), i64, i133)
494_0_<init>_Load(EOS(STATIC_494), i66) → 395_0_<init>_Load(EOS(STATIC_395), i66)
395_0_<init>_Load(EOS(STATIC_395), i58) → 401_0_<init>_InvokeMethod(EOS(STATIC_401), i58)
503_0_<init>_Return(EOS(STATIC_503), i64, matching1) → 575_0_<init>_Return(EOS(STATIC_575), i64, 1) | =(matching1, 1)
575_0_<init>_Return(EOS(STATIC_575), i64, i92) → 585_0_<init>_FieldAccess(EOS(STATIC_585), i64)
585_0_<init>_FieldAccess(EOS(STATIC_585), i64) → 594_0_<init>_Load(EOS(STATIC_594), i64)
594_0_<init>_Load(EOS(STATIC_594), i64) → 601_0_<init>_New(EOS(STATIC_601), i64)
601_0_<init>_New(EOS(STATIC_601), i64) → 610_0_<init>_Duplicate(EOS(STATIC_610), i64)
610_0_<init>_Duplicate(EOS(STATIC_610), i64) → 619_0_<init>_Load(EOS(STATIC_619), i64)
619_0_<init>_Load(EOS(STATIC_619), i64) → 622_0_<init>_ConstantStackPush(EOS(STATIC_622), i64)
622_0_<init>_ConstantStackPush(EOS(STATIC_622), i64) → 633_0_<init>_IntArithmetic(EOS(STATIC_633), i64, 1)
633_0_<init>_IntArithmetic(EOS(STATIC_633), i64, matching1) → 637_0_<init>_InvokeMethod(EOS(STATIC_637), -(i64, 1)) | &&(>(i64, 0), =(matching1, 1))
637_0_<init>_InvokeMethod(EOS(STATIC_637), i99) → 640_1_<init>_InvokeMethod(640_0_<init>_Load(EOS(STATIC_640), i99), i99)
640_0_<init>_Load(EOS(STATIC_640), i99) → 644_0_<init>_Load(EOS(STATIC_644), i99)
644_0_<init>_Load(EOS(STATIC_644), i99) → 395_0_<init>_Load(EOS(STATIC_395), i99)
846_0_<init>_Return(EOS(STATIC_846), i64, i133) → 575_0_<init>_Return(EOS(STATIC_575), i64, i133)
R rules:
423_0_<init>_LE(EOS(STATIC_423), i63, i63, matching1) → 429_0_<init>_LE(EOS(STATIC_429), i63, i63, 1) | =(matching1, 1)
429_0_<init>_LE(EOS(STATIC_429), i63, i63, matching1) → 436_0_<init>_Return(EOS(STATIC_436)) | &&(<=(i63, 1), =(matching1, 1))
640_1_<init>_InvokeMethod(436_0_<init>_Return(EOS(STATIC_436)), matching1) → 658_0_<init>_Return(EOS(STATIC_658), 1) | =(matching1, 1)
640_1_<init>_InvokeMethod(757_0_<init>_Return(EOS(STATIC_757)), i137) → 851_0_<init>_Return(EOS(STATIC_851), i137)
658_0_<init>_Return(EOS(STATIC_658), matching1) → 735_0_<init>_Return(EOS(STATIC_735), 1) | =(matching1, 1)
735_0_<init>_Return(EOS(STATIC_735), i126) → 743_0_<init>_FieldAccess(EOS(STATIC_743))
743_0_<init>_FieldAccess(EOS(STATIC_743)) → 757_0_<init>_Return(EOS(STATIC_757))
851_0_<init>_Return(EOS(STATIC_851), i137) → 735_0_<init>_Return(EOS(STATIC_735), i137)

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

P rules:
401_0_<init>_InvokeMethod(EOS(STATIC_401), x0) → 492_1_<init>_InvokeMethod(401_0_<init>_InvokeMethod(EOS(STATIC_401), -(x0, 1)), x0, -(x0, 1)) | >(x0, 1)
492_1_<init>_InvokeMethod(436_0_<init>_Return(EOS(STATIC_436)), x0, 1) → 640_1_<init>_InvokeMethod(401_0_<init>_InvokeMethod(EOS(STATIC_401), -(x0, 1)), -(x0, 1)) | >(x0, 0)
492_1_<init>_InvokeMethod(757_0_<init>_Return(EOS(STATIC_757)), x0, x1) → 640_1_<init>_InvokeMethod(401_0_<init>_InvokeMethod(EOS(STATIC_401), -(x0, 1)), -(x0, 1)) | >(x0, 0)
R rules:
640_1_<init>_InvokeMethod(436_0_<init>_Return(EOS(STATIC_436)), 1) → 757_0_<init>_Return(EOS(STATIC_757))
640_1_<init>_InvokeMethod(757_0_<init>_Return(EOS(STATIC_757)), x0) → 757_0_<init>_Return(EOS(STATIC_757))

Filtered ground terms:

401_0_<init>_InvokeMethod(x1, x2) → 401_0_<init>_InvokeMethod(x2)
Cond_492_1_<init>_InvokeMethod1(x1, x2, x3, x4) → Cond_492_1_<init>_InvokeMethod1(x1, x3, x4)
757_0_<init>_Return(x1) → 757_0_<init>_Return
Cond_492_1_<init>_InvokeMethod(x1, x2, x3, x4) → Cond_492_1_<init>_InvokeMethod(x1, x3)
436_0_<init>_Return(x1) → 436_0_<init>_Return
Cond_401_0_<init>_InvokeMethod(x1, x2, x3) → Cond_401_0_<init>_InvokeMethod(x1, x3)

Filtered unneeded arguments:

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

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

P rules:
401_0_<init>_InvokeMethod(x0) → 492_1_<init>_InvokeMethod(401_0_<init>_InvokeMethod(-(x0, 1)), x0, -(x0, 1)) | >(x0, 1)
492_1_<init>_InvokeMethod(436_0_<init>_Return, x0, 1) → 640_1_<init>_InvokeMethod(401_0_<init>_InvokeMethod(-(x0, 1)), -(x0, 1)) | >(x0, 0)
492_1_<init>_InvokeMethod(757_0_<init>_Return, x0, x1) → 640_1_<init>_InvokeMethod(401_0_<init>_InvokeMethod(-(x0, 1)), -(x0, 1)) | >(x0, 0)
R rules:
640_1_<init>_InvokeMethod(436_0_<init>_Return, 1) → 757_0_<init>_Return
640_1_<init>_InvokeMethod(757_0_<init>_Return, x0) → 757_0_<init>_Return

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

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

P rules:
401_0_<INIT>_INVOKEMETHOD(x0) → COND_401_0_<INIT>_INVOKEMETHOD(>(x0, 1), x0)
COND_401_0_<INIT>_INVOKEMETHOD(TRUE, x0) → 492_1_<INIT>_INVOKEMETHOD(401_0_<init>_InvokeMethod(-(x0, 1)), x0, -(x0, 1))
COND_401_0_<INIT>_INVOKEMETHOD(TRUE, x0) → 401_0_<INIT>_INVOKEMETHOD(-(x0, 1))
492_1_<INIT>_INVOKEMETHOD(436_0_<init>_Return, x0, 1) → COND_492_1_<INIT>_INVOKEMETHOD(>(x0, 0), 436_0_<init>_Return, x0, 1)
COND_492_1_<INIT>_INVOKEMETHOD(TRUE, 436_0_<init>_Return, x0, 1) → 401_0_<INIT>_INVOKEMETHOD(-(x0, 1))
492_1_<INIT>_INVOKEMETHOD(436_0_<init>_Return, x0, x1) → COND_492_1_<INIT>_INVOKEMETHOD1(>(x0, 0), 436_0_<init>_Return, x0, x1)
COND_492_1_<INIT>_INVOKEMETHOD1(TRUE, 436_0_<init>_Return, x0, x1) → 401_0_<INIT>_INVOKEMETHOD(-(x0, 1))
R rules:
640_1_<init>_InvokeMethod(436_0_<init>_Return, 1) → 436_0_<init>_Return
640_1_<init>_InvokeMethod(436_0_<init>_Return, x0) → 436_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:
640_1_<init>_InvokeMethod(436_0_<init>_Return, 1) → 436_0_<init>_Return
640_1_<init>_InvokeMethod(436_0_<init>_Return, x0) → 436_0_<init>_Return

The integer pair graph contains the following rules and edges:
(0): 401_0_<INIT>_INVOKEMETHOD(x0[0]) → COND_401_0_<INIT>_INVOKEMETHOD(x0[0] > 1, x0[0])
(1): COND_401_0_<INIT>_INVOKEMETHOD(TRUE, x0[1]) → 492_1_<INIT>_INVOKEMETHOD(401_0_<init>_InvokeMethod(x0[1] - 1), x0[1], x0[1] - 1)
(2): COND_401_0_<INIT>_INVOKEMETHOD(TRUE, x0[2]) → 401_0_<INIT>_INVOKEMETHOD(x0[2] - 1)
(3): 492_1_<INIT>_INVOKEMETHOD(436_0_<init>_Return, x0[3], 1) → COND_492_1_<INIT>_INVOKEMETHOD(x0[3] > 0, 436_0_<init>_Return, x0[3], 1)
(4): COND_492_1_<INIT>_INVOKEMETHOD(TRUE, 436_0_<init>_Return, x0[4], 1) → 401_0_<INIT>_INVOKEMETHOD(x0[4] - 1)
(5): 492_1_<INIT>_INVOKEMETHOD(436_0_<init>_Return, x0[5], x1[5]) → COND_492_1_<INIT>_INVOKEMETHOD1(x0[5] > 0, 436_0_<init>_Return, x0[5], x1[5])
(6): COND_492_1_<INIT>_INVOKEMETHOD1(TRUE, 436_0_<init>_Return, x0[6], x1[6]) → 401_0_<INIT>_INVOKEMETHOD(x0[6] - 1)

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

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

(1) -> (3), if (401_0_<init>_InvokeMethod(x0[1] - 1) →^* 436_0_<init>_Return∧x0[1] →^* x0[3]∧x0[1] - 1 →^* 1)

(1) -> (5), if (401_0_<init>_InvokeMethod(x0[1] - 1) →^* 436_0_<init>_Return∧x0[1] →^* x0[5]∧x0[1] - 1 →^* x1[5])

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

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

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

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

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

The set Q consists of the following terms:
640_1_<init>_InvokeMethod(436_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@387a2618 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 401_0_<INIT>_INVOKEMETHOD(x0) → COND_401_0_<INIT>_INVOKEMETHOD(>(x0, 1), x0) the following chains were created:

We consider the chain 401_0_<INIT>_INVOKEMETHOD(x0[0]) → COND_401_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0]), COND_401_0_<INIT>_INVOKEMETHOD(TRUE, x0[1]) → 492_1_<INIT>_INVOKEMETHOD(401_0_<init>_InvokeMethod(-(x0[1], 1)), x0[1], -(x0[1], 1)) which results in the following constraint:
(1)    (>(x0[0], 1)=TRUE∧x0[0]=x0[1] ⇒ 401_0_<INIT>_INVOKEMETHOD(x0[0])≥NonInfC∧401_0_<INIT>_INVOKEMETHOD(x0[0])≥COND_401_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])∧(U^Increasing(COND_401_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)=TRUE ⇒ 401_0_<INIT>_INVOKEMETHOD(x0[0])≥NonInfC∧401_0_<INIT>_INVOKEMETHOD(x0[0])≥COND_401_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])∧(U^Increasing(COND_401_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 ⇒ (U^Increasing(COND_401_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 ⇒ (U^Increasing(COND_401_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 ⇒ (U^Increasing(COND_401_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 ⇒ (U^Increasing(COND_401_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 401_0_<INIT>_INVOKEMETHOD(x0[0]) → COND_401_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0]), COND_401_0_<INIT>_INVOKEMETHOD(TRUE, x0[2]) → 401_0_<INIT>_INVOKEMETHOD(-(x0[2], 1)) which results in the following constraint:
(7)    (>(x0[0], 1)=TRUE∧x0[0]=x0[2] ⇒ 401_0_<INIT>_INVOKEMETHOD(x0[0])≥NonInfC∧401_0_<INIT>_INVOKEMETHOD(x0[0])≥COND_401_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])∧(U^Increasing(COND_401_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)=TRUE ⇒ 401_0_<INIT>_INVOKEMETHOD(x0[0])≥NonInfC∧401_0_<INIT>_INVOKEMETHOD(x0[0])≥COND_401_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])∧(U^Increasing(COND_401_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 ⇒ (U^Increasing(COND_401_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 ⇒ (U^Increasing(COND_401_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 ⇒ (U^Increasing(COND_401_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 ⇒ (U^Increasing(COND_401_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_401_0_<INIT>_INVOKEMETHOD(TRUE, x0) → 492_1_<INIT>_INVOKEMETHOD(401_0_<init>_InvokeMethod(-(x0, 1)), x0, -(x0, 1)) the following chains were created:

We consider the chain COND_401_0_<INIT>_INVOKEMETHOD(TRUE, x0[1]) → 492_1_<INIT>_INVOKEMETHOD(401_0_<init>_InvokeMethod(-(x0[1], 1)), x0[1], -(x0[1], 1)) which results in the following constraint:
(13)    (COND_401_0_<INIT>_INVOKEMETHOD(TRUE, x0[1])≥NonInfC∧COND_401_0_<INIT>_INVOKEMETHOD(TRUE, x0[1])≥492_1_<INIT>_INVOKEMETHOD(401_0_<init>_InvokeMethod(-(x0[1], 1)), x0[1], -(x0[1], 1))∧(U^Increasing(492_1_<INIT>_INVOKEMETHOD(401_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)    ((U^Increasing(492_1_<INIT>_INVOKEMETHOD(401_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)    ((U^Increasing(492_1_<INIT>_INVOKEMETHOD(401_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)    ((U^Increasing(492_1_<INIT>_INVOKEMETHOD(401_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)    ((U^Increasing(492_1_<INIT>_INVOKEMETHOD(401_0_<init>_InvokeMethod(-(x0[1], 1)), x0[1], -(x0[1], 1))), ≥)∧[bni_18] = 0∧0 = 0∧[(-1)bso_19] ≥ 0)

For Pair COND_401_0_<INIT>_INVOKEMETHOD(TRUE, x0) → 401_0_<INIT>_INVOKEMETHOD(-(x0, 1)) the following chains were created:

We consider the chain COND_401_0_<INIT>_INVOKEMETHOD(TRUE, x0[2]) → 401_0_<INIT>_INVOKEMETHOD(-(x0[2], 1)) which results in the following constraint:
(18)    (COND_401_0_<INIT>_INVOKEMETHOD(TRUE, x0[2])≥NonInfC∧COND_401_0_<INIT>_INVOKEMETHOD(TRUE, x0[2])≥401_0_<INIT>_INVOKEMETHOD(-(x0[2], 1))∧(U^Increasing(401_0_<INIT>_INVOKEMETHOD(-(x0[2], 1))), ≥))

We simplified constraint (18) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(19)    ((U^Increasing(401_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)    ((U^Increasing(401_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)    ((U^Increasing(401_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)    ((U^Increasing(401_0_<INIT>_INVOKEMETHOD(-(x0[2], 1))), ≥)∧[bni_20] = 0∧0 = 0∧[2 + (-1)bso_21] ≥ 0)

For Pair 492_1_<INIT>_INVOKEMETHOD(436_0_<init>_Return, x0, 1) → COND_492_1_<INIT>_INVOKEMETHOD(>(x0, 0), 436_0_<init>_Return, x0, 1) the following chains were created:

We consider the chain 492_1_<INIT>_INVOKEMETHOD(436_0_<init>_Return, x0[3], 1) → COND_492_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 436_0_<init>_Return, x0[3], 1), COND_492_1_<INIT>_INVOKEMETHOD(TRUE, 436_0_<init>_Return, x0[4], 1) → 401_0_<INIT>_INVOKEMETHOD(-(x0[4], 1)) which results in the following constraint:
(23)    (>(x0[3], 0)=TRUE∧x0[3]=x0[4] ⇒ 492_1_<INIT>_INVOKEMETHOD(436_0_<init>_Return, x0[3], 1)≥NonInfC∧492_1_<INIT>_INVOKEMETHOD(436_0_<init>_Return, x0[3], 1)≥COND_492_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 436_0_<init>_Return, x0[3], 1)∧(U^Increasing(COND_492_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 436_0_<init>_Return, x0[3], 1)), ≥))

We simplified constraint (23) using rule (IV) which results in the following new constraint:
(24)    (>(x0[3], 0)=TRUE ⇒ 492_1_<INIT>_INVOKEMETHOD(436_0_<init>_Return, x0[3], 1)≥NonInfC∧492_1_<INIT>_INVOKEMETHOD(436_0_<init>_Return, x0[3], 1)≥COND_492_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 436_0_<init>_Return, x0[3], 1)∧(U^Increasing(COND_492_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 436_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 ⇒ (U^Increasing(COND_492_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 436_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 ⇒ (U^Increasing(COND_492_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 436_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 ⇒ (U^Increasing(COND_492_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 436_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 ⇒ (U^Increasing(COND_492_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 436_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_492_1_<INIT>_INVOKEMETHOD(TRUE, 436_0_<init>_Return, x0, 1) → 401_0_<INIT>_INVOKEMETHOD(-(x0, 1)) the following chains were created:

We consider the chain COND_492_1_<INIT>_INVOKEMETHOD(TRUE, 436_0_<init>_Return, x0[4], 1) → 401_0_<INIT>_INVOKEMETHOD(-(x0[4], 1)) which results in the following constraint:
(29)    (COND_492_1_<INIT>_INVOKEMETHOD(TRUE, 436_0_<init>_Return, x0[4], 1)≥NonInfC∧COND_492_1_<INIT>_INVOKEMETHOD(TRUE, 436_0_<init>_Return, x0[4], 1)≥401_0_<INIT>_INVOKEMETHOD(-(x0[4], 1))∧(U^Increasing(401_0_<INIT>_INVOKEMETHOD(-(x0[4], 1))), ≥))

We simplified constraint (29) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(30)    ((U^Increasing(401_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)    ((U^Increasing(401_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)    ((U^Increasing(401_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)    ((U^Increasing(401_0_<INIT>_INVOKEMETHOD(-(x0[4], 1))), ≥)∧[bni_24] = 0∧0 = 0∧[2 + (-1)bso_25] ≥ 0)

For Pair 492_1_<INIT>_INVOKEMETHOD(436_0_<init>_Return, x0, x1) → COND_492_1_<INIT>_INVOKEMETHOD1(>(x0, 0), 436_0_<init>_Return, x0, x1) the following chains were created:

We consider the chain 492_1_<INIT>_INVOKEMETHOD(436_0_<init>_Return, x0[5], x1[5]) → COND_492_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 436_0_<init>_Return, x0[5], x1[5]), COND_492_1_<INIT>_INVOKEMETHOD1(TRUE, 436_0_<init>_Return, x0[6], x1[6]) → 401_0_<INIT>_INVOKEMETHOD(-(x0[6], 1)) which results in the following constraint:
(34)    (>(x0[5], 0)=TRUE∧x0[5]=x0[6]∧x1[5]=x1[6] ⇒ 492_1_<INIT>_INVOKEMETHOD(436_0_<init>_Return, x0[5], x1[5])≥NonInfC∧492_1_<INIT>_INVOKEMETHOD(436_0_<init>_Return, x0[5], x1[5])≥COND_492_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 436_0_<init>_Return, x0[5], x1[5])∧(U^Increasing(COND_492_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 436_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)=TRUE ⇒ 492_1_<INIT>_INVOKEMETHOD(436_0_<init>_Return, x0[5], x1[5])≥NonInfC∧492_1_<INIT>_INVOKEMETHOD(436_0_<init>_Return, x0[5], x1[5])≥COND_492_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 436_0_<init>_Return, x0[5], x1[5])∧(U^Increasing(COND_492_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 436_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 ⇒ (U^Increasing(COND_492_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 436_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 ⇒ (U^Increasing(COND_492_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 436_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 ⇒ (U^Increasing(COND_492_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 436_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 ⇒ (U^Increasing(COND_492_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 436_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 ⇒ (U^Increasing(COND_492_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 436_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_492_1_<INIT>_INVOKEMETHOD1(TRUE, 436_0_<init>_Return, x0, x1) → 401_0_<INIT>_INVOKEMETHOD(-(x0, 1)) the following chains were created:

We consider the chain COND_492_1_<INIT>_INVOKEMETHOD1(TRUE, 436_0_<init>_Return, x0[6], x1[6]) → 401_0_<INIT>_INVOKEMETHOD(-(x0[6], 1)) which results in the following constraint:
(41)    (COND_492_1_<INIT>_INVOKEMETHOD1(TRUE, 436_0_<init>_Return, x0[6], x1[6])≥NonInfC∧COND_492_1_<INIT>_INVOKEMETHOD1(TRUE, 436_0_<init>_Return, x0[6], x1[6])≥401_0_<INIT>_INVOKEMETHOD(-(x0[6], 1))∧(U^Increasing(401_0_<INIT>_INVOKEMETHOD(-(x0[6], 1))), ≥))

We simplified constraint (41) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(42)    ((U^Increasing(401_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)    ((U^Increasing(401_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)    ((U^Increasing(401_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)    ((U^Increasing(401_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.

401_0_<INIT>_INVOKEMETHOD(x0) → COND_401_0_<INIT>_INVOKEMETHOD(>(x0, 1), x0)
- (x0[0] ≥ 0 ⇒ (U^Increasing(COND_401_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 ⇒ (U^Increasing(COND_401_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_401_0_<INIT>_INVOKEMETHOD(TRUE, x0) → 492_1_<INIT>_INVOKEMETHOD(401_0_<init>_InvokeMethod(-(x0, 1)), x0, -(x0, 1))
- ((U^Increasing(492_1_<INIT>_INVOKEMETHOD(401_0_<init>_InvokeMethod(-(x0[1], 1)), x0[1], -(x0[1], 1))), ≥)∧[bni_18] = 0∧0 = 0∧[(-1)bso_19] ≥ 0)
COND_401_0_<INIT>_INVOKEMETHOD(TRUE, x0) → 401_0_<INIT>_INVOKEMETHOD(-(x0, 1))
- ((U^Increasing(401_0_<INIT>_INVOKEMETHOD(-(x0[2], 1))), ≥)∧[bni_20] = 0∧0 = 0∧[2 + (-1)bso_21] ≥ 0)
492_1_<INIT>_INVOKEMETHOD(436_0_<init>_Return, x0, 1) → COND_492_1_<INIT>_INVOKEMETHOD(>(x0, 0), 436_0_<init>_Return, x0, 1)
- (x0[3] ≥ 0 ⇒ (U^Increasing(COND_492_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 436_0_<init>_Return, x0[3], 1)), ≥)∧[(3)bni_22 + (-1)Bound*bni_22] + [(2)bni_22]x0[3] ≥ 0∧[(-1)bso_23] ≥ 0)
COND_492_1_<INIT>_INVOKEMETHOD(TRUE, 436_0_<init>_Return, x0, 1) → 401_0_<INIT>_INVOKEMETHOD(-(x0, 1))
- ((U^Increasing(401_0_<INIT>_INVOKEMETHOD(-(x0[4], 1))), ≥)∧[bni_24] = 0∧0 = 0∧[2 + (-1)bso_25] ≥ 0)
492_1_<INIT>_INVOKEMETHOD(436_0_<init>_Return, x0, x1) → COND_492_1_<INIT>_INVOKEMETHOD1(>(x0, 0), 436_0_<init>_Return, x0, x1)
- (x0[5] ≥ 0 ⇒ (U^Increasing(COND_492_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 436_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_492_1_<INIT>_INVOKEMETHOD1(TRUE, 436_0_<init>_Return, x0, x1) → 401_0_<INIT>_INVOKEMETHOD(-(x0, 1))
- ((U^Increasing(401_0_<INIT>_INVOKEMETHOD(-(x0[6], 1))), ≥)∧[bni_28] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_29] ≥ 0)

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

POL(TRUE) = 0
POL(FALSE) = 0
POL(640_1_<init>_InvokeMethod(x₁, x₂)) = [-1]
POL(436_0_<init>_Return) = 0
POL(1) = [1]
POL(401_0_<INIT>_INVOKEMETHOD(x₁)) = [1] + [2]x₁
POL(COND_401_0_<INIT>_INVOKEMETHOD(x₁, x₂)) = [1] + [2]x₂
POL(>(x₁, x₂)) = [-1]
POL(492_1_<INIT>_INVOKEMETHOD(x₁, x₂, x₃)) = [1] + [2]x₂
POL(401_0_<init>_InvokeMethod(x₁)) = x₁
POL(-(x₁, x₂)) = x₁ + [-1]x₂
POL(COND_492_1_<INIT>_INVOKEMETHOD(x₁, x₂, x₃, x₄)) = [1] + [2]x₃
POL(0) = 0
POL(COND_492_1_<INIT>_INVOKEMETHOD1(x₁, x₂, x₃, x₄)) = [2]x₃

The following pairs are in P_>:

COND_401_0_<INIT>_INVOKEMETHOD(TRUE, x0[2]) → 401_0_<INIT>_INVOKEMETHOD(-(x0[2], 1))
COND_492_1_<INIT>_INVOKEMETHOD(TRUE, 436_0_<init>_Return, x0[4], 1) → 401_0_<INIT>_INVOKEMETHOD(-(x0[4], 1))
492_1_<INIT>_INVOKEMETHOD(436_0_<init>_Return, x0[5], x1[5]) → COND_492_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 436_0_<init>_Return, x0[5], x1[5])
COND_492_1_<INIT>_INVOKEMETHOD1(TRUE, 436_0_<init>_Return, x0[6], x1[6]) → 401_0_<INIT>_INVOKEMETHOD(-(x0[6], 1))

The following pairs are in P_bound:

401_0_<INIT>_INVOKEMETHOD(x0[0]) → COND_401_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])
492_1_<INIT>_INVOKEMETHOD(436_0_<init>_Return, x0[3], 1) → COND_492_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 436_0_<init>_Return, x0[3], 1)
492_1_<INIT>_INVOKEMETHOD(436_0_<init>_Return, x0[5], x1[5]) → COND_492_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 436_0_<init>_Return, x0[5], x1[5])

The following pairs are in P_≥:

401_0_<INIT>_INVOKEMETHOD(x0[0]) → COND_401_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])
COND_401_0_<INIT>_INVOKEMETHOD(TRUE, x0[1]) → 492_1_<INIT>_INVOKEMETHOD(401_0_<init>_InvokeMethod(-(x0[1], 1)), x0[1], -(x0[1], 1))
492_1_<INIT>_INVOKEMETHOD(436_0_<init>_Return, x0[3], 1) → COND_492_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 436_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

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

(1) -> (3), if (401_0_<init>_InvokeMethod(x0[1] - 1) →^* 436_0_<init>_Return∧x0[1] →^* x0[3]∧x0[1] - 1 →^* 1)

The set Q consists of the following terms:
640_1_<init>_InvokeMethod(436_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:
640_1_<init>_InvokeMethod(436_0_<init>_Return, 1) → 436_0_<init>_Return
640_1_<init>_InvokeMethod(436_0_<init>_Return, x0) → 436_0_<init>_Return

The integer pair graph contains the following rules and edges:
(1): COND_401_0_<INIT>_INVOKEMETHOD(TRUE, x0[1]) → 492_1_<INIT>_INVOKEMETHOD(401_0_<init>_InvokeMethod(x0[1] - 1), x0[1], x0[1] - 1)
(2): COND_401_0_<INIT>_INVOKEMETHOD(TRUE, x0[2]) → 401_0_<INIT>_INVOKEMETHOD(x0[2] - 1)
(4): COND_492_1_<INIT>_INVOKEMETHOD(TRUE, 436_0_<init>_Return, x0[4], 1) → 401_0_<INIT>_INVOKEMETHOD(x0[4] - 1)
(6): COND_492_1_<INIT>_INVOKEMETHOD1(TRUE, 436_0_<init>_Return, x0[6], x1[6]) → 401_0_<INIT>_INVOKEMETHOD(x0[6] - 1)

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

(25) IDependencyGraphProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIDPv1Proof (SOUND transformation)

(7) Obligation:

(8) IDPtoQDPProof (SOUND transformation)

(9) Obligation:

(10) UsableRulesProof (EQUIVALENT transformation)

(11) Obligation:

(12) QReductionProof (EQUIVALENT transformation)

(13) Obligation:

(14) QDPSizeChangeProof (EQUIVALENT transformation)

(15) YES

(16) Obligation:

(17) SCCToIDPv1Proof (SOUND transformation)

(18) Obligation:

(19) IDPNonInfProof (SOUND transformation)

(20) Complex Obligation (AND)

(21) Obligation:

(22) IDependencyGraphProof (EQUIVALENT transformation)

(23) TRUE

(24) Obligation:

(25) IDependencyGraphProof (EQUIVALENT transformation)

(26) TRUE