Termination proof of /tmp/tmpcQwmjO/BTreeR.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 940 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 1440 ms)

        ↳7 IDP

        ↳8 IDPtoQDPProof (⇒, 20 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 (⇒, 170 ms)

        ↳18 IDP

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

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

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

Filtered ground terms:

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

Filtered duplicate args:

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

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

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

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

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

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

(7) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:
none

The ITRS R consists of the following rules:
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, NULL))) → 961_0_height_Return
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))) → 961_0_height_Return
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3))) → 961_0_height_Return
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2))) → 961_0_height_Return
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0))) → 961_0_height_Return
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3))))) → 1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)), x3)))))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2))))) → 1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))), x2)))))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0))))) → 1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(NULL, NULL)), x0)))))
965_1_height_InvokeMethod(1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))) → 961_0_height_Return
965_1_height_InvokeMethod(1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))) → 961_0_height_Return
965_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))) → 961_0_height_Return
985_1_height_InvokeMethod(1684_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2))))))) → 1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(java.lang.Object(BTreeR(x0, x1)), x2)))))))
985_1_height_InvokeMethod(1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))), java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1))))))))) → 1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(x0, x1)))))))))
985_1_height_InvokeMethod(961_0_height_Return, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL))))))) → 1690_0_height_Return(java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, java.lang.Object(BTreeR(NULL, NULL)))))))

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

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

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

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

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

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

(8) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(9) Obligation:

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

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

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

We have to consider all minimal (P,Q,R)-chains.

(10) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(11) Obligation:

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

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

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

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

We have to consider all minimal (P,Q,R)-chains.

(12) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

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

(13) Obligation:

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

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

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

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

(15) YES

(16) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: BTreeR.<init>(I)V
SCC calls the following helper methods: BTreeR.<init>(I)V
Performed SCC analyses: UsedFieldsAnalysis

(17) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 30 rules for P and 8 rules for R.

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

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

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

Filtered ground terms:

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

Filtered unneeded arguments:

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

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

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

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

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

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

(18) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

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

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

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

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

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

(1) -> (5), if (397_0_<init>_InvokeMethod(x0[1] - 1) →^* 426_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:
634_1_<init>_InvokeMethod(426_0_<init>_Return, x0)

(19) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@5d8409fb Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 397_0_<INIT>_INVOKEMETHOD(x0) → COND_397_0_<INIT>_INVOKEMETHOD(>(x0, 1), x0) the following chains were created:

We consider the chain 397_0_<INIT>_INVOKEMETHOD(x0[0]) → COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0]), COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0[1]) → 476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(-(x0[1], 1)), x0[1], -(x0[1], 1)) which results in the following constraint:
(1)    (>(x0[0], 1)=TRUE∧x0[0]=x0[1] ⇒ 397_0_<INIT>_INVOKEMETHOD(x0[0])≥NonInfC∧397_0_<INIT>_INVOKEMETHOD(x0[0])≥COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])∧(U^Increasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥))

We simplified constraint (1) using rule (IV) which results in the following new constraint:
(2)    (>(x0[0], 1)=TRUE ⇒ 397_0_<INIT>_INVOKEMETHOD(x0[0])≥NonInfC∧397_0_<INIT>_INVOKEMETHOD(x0[0])≥COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])∧(U^Increasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x0[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥)∧[bni_16 + (-1)Bound*bni_16] + [(2)bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x0[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥)∧[bni_16 + (-1)Bound*bni_16] + [(2)bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x0[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥)∧[bni_16 + (-1)Bound*bni_16] + [(2)bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x0[0] ≥ 0 ⇒ (U^Increasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥)∧[(5)bni_16 + (-1)Bound*bni_16] + [(2)bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)
We consider the chain 397_0_<INIT>_INVOKEMETHOD(x0[0]) → COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0]), COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0[2]) → 397_0_<INIT>_INVOKEMETHOD(-(x0[2], 1)) which results in the following constraint:
(7)    (>(x0[0], 1)=TRUE∧x0[0]=x0[2] ⇒ 397_0_<INIT>_INVOKEMETHOD(x0[0])≥NonInfC∧397_0_<INIT>_INVOKEMETHOD(x0[0])≥COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])∧(U^Increasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥))

We simplified constraint (7) using rule (IV) which results in the following new constraint:
(8)    (>(x0[0], 1)=TRUE ⇒ 397_0_<INIT>_INVOKEMETHOD(x0[0])≥NonInfC∧397_0_<INIT>_INVOKEMETHOD(x0[0])≥COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])∧(U^Increasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥))

We simplified constraint (8) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(9)    (x0[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥)∧[bni_16 + (-1)Bound*bni_16] + [(2)bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)

We simplified constraint (9) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(10)    (x0[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥)∧[bni_16 + (-1)Bound*bni_16] + [(2)bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)

We simplified constraint (10) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(11)    (x0[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥)∧[bni_16 + (-1)Bound*bni_16] + [(2)bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)

We simplified constraint (11) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(12)    (x0[0] ≥ 0 ⇒ (U^Increasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥)∧[(5)bni_16 + (-1)Bound*bni_16] + [(2)bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)

For Pair COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0) → 476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(-(x0, 1)), x0, -(x0, 1)) the following chains were created:

We consider the chain COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0[1]) → 476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(-(x0[1], 1)), x0[1], -(x0[1], 1)) which results in the following constraint:
(13)    (COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0[1])≥NonInfC∧COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0[1])≥476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(-(x0[1], 1)), x0[1], -(x0[1], 1))∧(U^Increasing(476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(-(x0[1], 1)), x0[1], -(x0[1], 1))), ≥))

We simplified constraint (13) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(14)    ((U^Increasing(476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(-(x0[1], 1)), x0[1], -(x0[1], 1))), ≥)∧[bni_18] = 0∧[(-1)bso_19] ≥ 0)

We simplified constraint (14) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(15)    ((U^Increasing(476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(-(x0[1], 1)), x0[1], -(x0[1], 1))), ≥)∧[bni_18] = 0∧[(-1)bso_19] ≥ 0)

We simplified constraint (15) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(16)    ((U^Increasing(476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(-(x0[1], 1)), x0[1], -(x0[1], 1))), ≥)∧[bni_18] = 0∧[(-1)bso_19] ≥ 0)

We simplified constraint (16) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(17)    ((U^Increasing(476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(-(x0[1], 1)), x0[1], -(x0[1], 1))), ≥)∧[bni_18] = 0∧0 = 0∧[(-1)bso_19] ≥ 0)

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

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

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

We simplified constraint (19) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(20)    ((U^Increasing(397_0_<INIT>_INVOKEMETHOD(-(x0[2], 1))), ≥)∧[bni_20] = 0∧[2 + (-1)bso_21] ≥ 0)

We simplified constraint (20) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(21)    ((U^Increasing(397_0_<INIT>_INVOKEMETHOD(-(x0[2], 1))), ≥)∧[bni_20] = 0∧[2 + (-1)bso_21] ≥ 0)

We simplified constraint (21) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(22)    ((U^Increasing(397_0_<INIT>_INVOKEMETHOD(-(x0[2], 1))), ≥)∧[bni_20] = 0∧0 = 0∧[2 + (-1)bso_21] ≥ 0)

For Pair 476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0, 1) → COND_476_1_<INIT>_INVOKEMETHOD(>(x0, 0), 426_0_<init>_Return, x0, 1) the following chains were created:

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

We simplified constraint (23) using rule (IV) which results in the following new constraint:
(24)    (>(x0[3], 0)=TRUE ⇒ 476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0[3], 1)≥NonInfC∧476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0[3], 1)≥COND_476_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 426_0_<init>_Return, x0[3], 1)∧(U^Increasing(COND_476_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 426_0_<init>_Return, x0[3], 1)), ≥))

We simplified constraint (24) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(25)    (x0[3] + [-1] ≥ 0 ⇒ (U^Increasing(COND_476_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 426_0_<init>_Return, x0[3], 1)), ≥)∧[bni_22 + (-1)Bound*bni_22] + [(2)bni_22]x0[3] ≥ 0∧[(-1)bso_23] ≥ 0)

We simplified constraint (25) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(26)    (x0[3] + [-1] ≥ 0 ⇒ (U^Increasing(COND_476_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 426_0_<init>_Return, x0[3], 1)), ≥)∧[bni_22 + (-1)Bound*bni_22] + [(2)bni_22]x0[3] ≥ 0∧[(-1)bso_23] ≥ 0)

We simplified constraint (26) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(27)    (x0[3] + [-1] ≥ 0 ⇒ (U^Increasing(COND_476_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 426_0_<init>_Return, x0[3], 1)), ≥)∧[bni_22 + (-1)Bound*bni_22] + [(2)bni_22]x0[3] ≥ 0∧[(-1)bso_23] ≥ 0)

We simplified constraint (27) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(28)    (x0[3] ≥ 0 ⇒ (U^Increasing(COND_476_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 426_0_<init>_Return, x0[3], 1)), ≥)∧[(3)bni_22 + (-1)Bound*bni_22] + [(2)bni_22]x0[3] ≥ 0∧[(-1)bso_23] ≥ 0)

For Pair COND_476_1_<INIT>_INVOKEMETHOD(TRUE, 426_0_<init>_Return, x0, 1) → 397_0_<INIT>_INVOKEMETHOD(-(x0, 1)) the following chains were created:

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

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

We simplified constraint (30) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(31)    ((U^Increasing(397_0_<INIT>_INVOKEMETHOD(-(x0[4], 1))), ≥)∧[bni_24] = 0∧[2 + (-1)bso_25] ≥ 0)

We simplified constraint (31) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(32)    ((U^Increasing(397_0_<INIT>_INVOKEMETHOD(-(x0[4], 1))), ≥)∧[bni_24] = 0∧[2 + (-1)bso_25] ≥ 0)

We simplified constraint (32) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(33)    ((U^Increasing(397_0_<INIT>_INVOKEMETHOD(-(x0[4], 1))), ≥)∧[bni_24] = 0∧0 = 0∧[2 + (-1)bso_25] ≥ 0)

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

We consider the chain 476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0[5], x1[5]) → COND_476_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 426_0_<init>_Return, x0[5], x1[5]), COND_476_1_<INIT>_INVOKEMETHOD1(TRUE, 426_0_<init>_Return, x0[6], x1[6]) → 397_0_<INIT>_INVOKEMETHOD(-(x0[6], 1)) which results in the following constraint:
(34)    (>(x0[5], 0)=TRUE∧x0[5]=x0[6]∧x1[5]=x1[6] ⇒ 476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0[5], x1[5])≥NonInfC∧476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0[5], x1[5])≥COND_476_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 426_0_<init>_Return, x0[5], x1[5])∧(U^Increasing(COND_476_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 426_0_<init>_Return, x0[5], x1[5])), ≥))

We simplified constraint (34) using rule (IV) which results in the following new constraint:
(35)    (>(x0[5], 0)=TRUE ⇒ 476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0[5], x1[5])≥NonInfC∧476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0[5], x1[5])≥COND_476_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 426_0_<init>_Return, x0[5], x1[5])∧(U^Increasing(COND_476_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 426_0_<init>_Return, x0[5], x1[5])), ≥))

We simplified constraint (35) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(36)    (x0[5] + [-1] ≥ 0 ⇒ (U^Increasing(COND_476_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 426_0_<init>_Return, x0[5], x1[5])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [(2)bni_26]x0[5] ≥ 0∧[1 + (-1)bso_27] ≥ 0)

We simplified constraint (36) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(37)    (x0[5] + [-1] ≥ 0 ⇒ (U^Increasing(COND_476_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 426_0_<init>_Return, x0[5], x1[5])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [(2)bni_26]x0[5] ≥ 0∧[1 + (-1)bso_27] ≥ 0)

We simplified constraint (37) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(38)    (x0[5] + [-1] ≥ 0 ⇒ (U^Increasing(COND_476_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 426_0_<init>_Return, x0[5], x1[5])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [(2)bni_26]x0[5] ≥ 0∧[1 + (-1)bso_27] ≥ 0)

We simplified constraint (38) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(39)    (x0[5] + [-1] ≥ 0 ⇒ (U^Increasing(COND_476_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 426_0_<init>_Return, x0[5], x1[5])), ≥)∧0 = 0∧[bni_26 + (-1)Bound*bni_26] + [(2)bni_26]x0[5] ≥ 0∧0 = 0∧[1 + (-1)bso_27] ≥ 0)

We simplified constraint (39) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(40)    (x0[5] ≥ 0 ⇒ (U^Increasing(COND_476_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 426_0_<init>_Return, x0[5], x1[5])), ≥)∧0 = 0∧[(3)bni_26 + (-1)Bound*bni_26] + [(2)bni_26]x0[5] ≥ 0∧0 = 0∧[1 + (-1)bso_27] ≥ 0)

For Pair COND_476_1_<INIT>_INVOKEMETHOD1(TRUE, 426_0_<init>_Return, x0, x1) → 397_0_<INIT>_INVOKEMETHOD(-(x0, 1)) the following chains were created:

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

We simplified constraint (41) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(42)    ((U^Increasing(397_0_<INIT>_INVOKEMETHOD(-(x0[6], 1))), ≥)∧[bni_28] = 0∧[1 + (-1)bso_29] ≥ 0)

We simplified constraint (42) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(43)    ((U^Increasing(397_0_<INIT>_INVOKEMETHOD(-(x0[6], 1))), ≥)∧[bni_28] = 0∧[1 + (-1)bso_29] ≥ 0)

We simplified constraint (43) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(44)    ((U^Increasing(397_0_<INIT>_INVOKEMETHOD(-(x0[6], 1))), ≥)∧[bni_28] = 0∧[1 + (-1)bso_29] ≥ 0)

We simplified constraint (44) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(45)    ((U^Increasing(397_0_<INIT>_INVOKEMETHOD(-(x0[6], 1))), ≥)∧[bni_28] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_29] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

397_0_<INIT>_INVOKEMETHOD(x0) → COND_397_0_<INIT>_INVOKEMETHOD(>(x0, 1), x0)
- (x0[0] ≥ 0 ⇒ (U^Increasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥)∧[(5)bni_16 + (-1)Bound*bni_16] + [(2)bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)
- (x0[0] ≥ 0 ⇒ (U^Increasing(COND_397_0_<INIT>_INVOKEMETHOD(>(x0[0], 1), x0[0])), ≥)∧[(5)bni_16 + (-1)Bound*bni_16] + [(2)bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)
COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0) → 476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(-(x0, 1)), x0, -(x0, 1))
- ((U^Increasing(476_1_<INIT>_INVOKEMETHOD(397_0_<init>_InvokeMethod(-(x0[1], 1)), x0[1], -(x0[1], 1))), ≥)∧[bni_18] = 0∧0 = 0∧[(-1)bso_19] ≥ 0)
COND_397_0_<INIT>_INVOKEMETHOD(TRUE, x0) → 397_0_<INIT>_INVOKEMETHOD(-(x0, 1))
- ((U^Increasing(397_0_<INIT>_INVOKEMETHOD(-(x0[2], 1))), ≥)∧[bni_20] = 0∧0 = 0∧[2 + (-1)bso_21] ≥ 0)
476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0, 1) → COND_476_1_<INIT>_INVOKEMETHOD(>(x0, 0), 426_0_<init>_Return, x0, 1)
- (x0[3] ≥ 0 ⇒ (U^Increasing(COND_476_1_<INIT>_INVOKEMETHOD(>(x0[3], 0), 426_0_<init>_Return, x0[3], 1)), ≥)∧[(3)bni_22 + (-1)Bound*bni_22] + [(2)bni_22]x0[3] ≥ 0∧[(-1)bso_23] ≥ 0)
COND_476_1_<INIT>_INVOKEMETHOD(TRUE, 426_0_<init>_Return, x0, 1) → 397_0_<INIT>_INVOKEMETHOD(-(x0, 1))
- ((U^Increasing(397_0_<INIT>_INVOKEMETHOD(-(x0[4], 1))), ≥)∧[bni_24] = 0∧0 = 0∧[2 + (-1)bso_25] ≥ 0)
476_1_<INIT>_INVOKEMETHOD(426_0_<init>_Return, x0, x1) → COND_476_1_<INIT>_INVOKEMETHOD1(>(x0, 0), 426_0_<init>_Return, x0, x1)
- (x0[5] ≥ 0 ⇒ (U^Increasing(COND_476_1_<INIT>_INVOKEMETHOD1(>(x0[5], 0), 426_0_<init>_Return, x0[5], x1[5])), ≥)∧0 = 0∧[(3)bni_26 + (-1)Bound*bni_26] + [(2)bni_26]x0[5] ≥ 0∧0 = 0∧[1 + (-1)bso_27] ≥ 0)
COND_476_1_<INIT>_INVOKEMETHOD1(TRUE, 426_0_<init>_Return, x0, x1) → 397_0_<INIT>_INVOKEMETHOD(-(x0, 1))
- ((U^Increasing(397_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(634_1_<init>_InvokeMethod(x₁, x₂)) = [-1]
POL(426_0_<init>_Return) = 0
POL(1) = [1]
POL(397_0_<INIT>_INVOKEMETHOD(x₁)) = [1] + [2]x₁
POL(COND_397_0_<INIT>_INVOKEMETHOD(x₁, x₂)) = [1] + [2]x₂
POL(>(x₁, x₂)) = [-1]
POL(476_1_<INIT>_INVOKEMETHOD(x₁, x₂, x₃)) = [1] + [2]x₂
POL(397_0_<init>_InvokeMethod(x₁)) = x₁
POL(-(x₁, x₂)) = x₁ + [-1]x₂
POL(COND_476_1_<INIT>_INVOKEMETHOD(x₁, x₂, x₃, x₄)) = [1] + [2]x₃
POL(0) = 0
POL(COND_476_1_<INIT>_INVOKEMETHOD1(x₁, x₂, x₃, x₄)) = [2]x₃

The following pairs are in P_>:

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

The following pairs are in P_bound:

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

The following pairs are in P_≥:

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

There are no usable rules.

(20) Complex Obligation (AND)

(21) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

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

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

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

(22) IDependencyGraphProof (EQUIVALENT transformation)

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

(23) TRUE

(24) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

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

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

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

(25) IDependencyGraphProof (EQUIVALENT transformation)

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

(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