Termination proof of /tmp/tmpR4wJ9c/LogRecursive.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 367 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 JBCTerminationSCC

↳5 SCCToIDPv1Proof (⇒, 0 ms)

↳6 IDP

↳7 IDPNonInfProof (⇒, 201 ms)

↳8 IDP

↳9 IDependencyGraphProof (⇔, 0 ms)

↳10 TRUE

(0) Obligation:

JBC Problem based on JBC Program:

public class LogRecursive {
  public static void main(String[] args) {
    Random.args = args;
    log(Random.random(), Random.random());
  }

  public static int log(int x, int y) {
    if (x >= y && y > 1) {
      return 1 + log(x/y, y);
    }
    return 0;
  }
}


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

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

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

LogRecursive.log(II)I: Graph of 37 nodes with 0 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 1 SCCs.

(4) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: LogRecursive.log(II)I
SCC calls the following helper methods: LogRecursive.log(II)I
Performed SCC analyses:

Used field analysis yielded the following read fields:
Marker field analysis yielded the following relations that could be markers:

(5) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 16 rules for P and 34 rules for R.

P rules:
f504_0_log_Load(EOS(STATIC_504), i78, i79, i78, i79, i78) → f507_0_log_LT(EOS(STATIC_507), i78, i79, i78, i79, i78, i79)
f507_0_log_LT(EOS(STATIC_507), i78, i79, i78, i79, i78, i79) → f510_0_log_LT(EOS(STATIC_510), i78, i79, i78, i79, i78, i79)
f510_0_log_LT(EOS(STATIC_510), i78, i79, i78, i79, i78, i79) → f514_0_log_Load(EOS(STATIC_514), i78, i79, i78, i79) | >=(i78, i79)
f514_0_log_Load(EOS(STATIC_514), i78, i79, i78, i79) → f520_0_log_ConstantStackPush(EOS(STATIC_520), i78, i79, i78, i79, i79)
f520_0_log_ConstantStackPush(EOS(STATIC_520), i78, i79, i78, i79, i79) → f525_0_log_LE(EOS(STATIC_525), i78, i79, i78, i79, i79, 1)
f525_0_log_LE(EOS(STATIC_525), i78, i107, i78, i107, i107, matching1) → f589_0_log_LE(EOS(STATIC_589), i78, i107, i78, i107, i107, 1) | =(matching1, 1)
f589_0_log_LE(EOS(STATIC_589), i78, i107, i78, i107, i107, matching1) → f599_0_log_ConstantStackPush(EOS(STATIC_599), i78, i107, i78, i107) | &&(>(i107, 1), =(matching1, 1))
f599_0_log_ConstantStackPush(EOS(STATIC_599), i78, i107, i78, i107) → f608_0_log_Load(EOS(STATIC_608), i78, i107, i78, i107)
f608_0_log_Load(EOS(STATIC_608), i78, i107, i78, i107) → f611_0_log_Load(EOS(STATIC_611), i78, i107, i107, i78)
f611_0_log_Load(EOS(STATIC_611), i78, i107, i107, i78) → f654_0_log_IntArithmetic(EOS(STATIC_654), i78, i107, i107, i78, i107)
f654_0_log_IntArithmetic(EOS(STATIC_654), i78, i107, i107, i78, i107) → f661_0_log_Load(EOS(STATIC_661), i78, i107, i107, /(i78, i107)) | >(i107, 1)
f661_0_log_Load(EOS(STATIC_661), i78, i107, i107, i134) → f663_0_log_InvokeMethod(EOS(STATIC_663), i78, i107, i134, i107)
f663_0_log_InvokeMethod(EOS(STATIC_663), i78, i107, i134, i107) → f664_1_log_InvokeMethod(f664_0_log_Load(EOS(STATIC_664), i134, i107, i134, i107), i78, i107, i134, i107)
f664_0_log_Load(EOS(STATIC_664), i134, i107, i134, i107) → f666_0_log_Load(EOS(STATIC_666), i134, i107, i134, i107)
f666_0_log_Load(EOS(STATIC_666), i134, i107, i134, i107) → f502_0_log_Load(EOS(STATIC_502), i134, i107, i134, i107)
f502_0_log_Load(EOS(STATIC_502), i78, i79, i78, i79) → f504_0_log_Load(EOS(STATIC_504), i78, i79, i78, i79, i78)
R rules:
f502_0_log_Load(EOS(STATIC_502), i78, i79, i78, i79) → f504_0_log_Load(EOS(STATIC_504), i78, i79, i78, i79, i78)
f504_0_log_Load(EOS(STATIC_504), i78, i79, i78, i79, i78) → f507_0_log_LT(EOS(STATIC_507), i78, i79, i78, i79, i78, i79)
f507_0_log_LT(EOS(STATIC_507), i78, i79, i78, i79, i78, i79) → f509_0_log_LT(EOS(STATIC_509), i78, i79, i78, i79, i78, i79)
f507_0_log_LT(EOS(STATIC_507), i78, i79, i78, i79, i78, i79) → f510_0_log_LT(EOS(STATIC_510), i78, i79, i78, i79, i78, i79)
f509_0_log_LT(EOS(STATIC_509), i78, i79, i78, i79, i78, i79) → f513_0_log_ConstantStackPush(EOS(STATIC_513), i78, i79) | <(i78, i79)
f510_0_log_LT(EOS(STATIC_510), i78, i79, i78, i79, i78, i79) → f514_0_log_Load(EOS(STATIC_514), i78, i79, i78, i79) | >=(i78, i79)
f513_0_log_ConstantStackPush(EOS(STATIC_513), i78, i79) → f518_0_log_Return(EOS(STATIC_518), i78, i79)
f514_0_log_Load(EOS(STATIC_514), i78, i79, i78, i79) → f520_0_log_ConstantStackPush(EOS(STATIC_520), i78, i79, i78, i79, i79)
f520_0_log_ConstantStackPush(EOS(STATIC_520), i78, i79, i78, i79, i79) → f525_0_log_LE(EOS(STATIC_525), i78, i79, i78, i79, i79, 1)
f525_0_log_LE(EOS(STATIC_525), i78, i106, i78, i106, i106, matching1) → f588_0_log_LE(EOS(STATIC_588), i78, i106, i78, i106, i106, 1) | =(matching1, 1)
f525_0_log_LE(EOS(STATIC_525), i78, i107, i78, i107, i107, matching1) → f589_0_log_LE(EOS(STATIC_589), i78, i107, i78, i107, i107, 1) | =(matching1, 1)
f588_0_log_LE(EOS(STATIC_588), i78, i106, i78, i106, i106, matching1) → f593_0_log_ConstantStackPush(EOS(STATIC_593), i78, i106) | &&(<=(i106, 1), =(matching1, 1))
f589_0_log_LE(EOS(STATIC_589), i78, i107, i78, i107, i107, matching1) → f599_0_log_ConstantStackPush(EOS(STATIC_599), i78, i107, i78, i107) | &&(>(i107, 1), =(matching1, 1))
f593_0_log_ConstantStackPush(EOS(STATIC_593), i78, i106) → f605_0_log_Return(EOS(STATIC_605), i78, i106)
f599_0_log_ConstantStackPush(EOS(STATIC_599), i78, i107, i78, i107) → f608_0_log_Load(EOS(STATIC_608), i78, i107, i78, i107)
f608_0_log_Load(EOS(STATIC_608), i78, i107, i78, i107) → f611_0_log_Load(EOS(STATIC_611), i78, i107, i107, i78)
f611_0_log_Load(EOS(STATIC_611), i78, i107, i107, i78) → f654_0_log_IntArithmetic(EOS(STATIC_654), i78, i107, i107, i78, i107)
f654_0_log_IntArithmetic(EOS(STATIC_654), i78, i107, i107, i78, i107) → f661_0_log_Load(EOS(STATIC_661), i78, i107, i107, /(i78, i107)) | >(i107, 1)
f661_0_log_Load(EOS(STATIC_661), i78, i107, i107, i134) → f663_0_log_InvokeMethod(EOS(STATIC_663), i78, i107, i134, i107)
f663_0_log_InvokeMethod(EOS(STATIC_663), i78, i107, i134, i107) → f664_1_log_InvokeMethod(f664_0_log_Load(EOS(STATIC_664), i134, i107, i134, i107), i78, i107, i134, i107)
f664_0_log_Load(EOS(STATIC_664), i134, i107, i134, i107) → f666_0_log_Load(EOS(STATIC_666), i134, i107, i134, i107)
f688_0_log_Return(EOS(STATIC_688), i78, i142, i144, i142) → f691_0_log_IntArithmetic(EOS(STATIC_691), i78, i142)
f691_0_log_IntArithmetic(EOS(STATIC_691), i78, i142) → f693_0_log_Return(EOS(STATIC_693), i78, i142)
f735_0_log_Return(EOS(STATIC_735), i78, i187, i189, i187) → f798_0_log_Return(EOS(STATIC_798), i78, i187, i189, i187)
f798_0_log_Return(EOS(STATIC_798), i78, i240, i241, i240) → f880_0_log_Return(EOS(STATIC_880), i78, i240, i241, i240)
f880_0_log_Return(EOS(STATIC_880), i78, i304, i305, i304) → f950_0_log_Return(EOS(STATIC_950), i78, i304, i305, i304)
f950_0_log_Return(EOS(STATIC_950), i78, i377, i378, i377) → f1013_0_log_Return(EOS(STATIC_1013), i78, i377, i378, i377)
f1013_0_log_Return(EOS(STATIC_1013), i78, i450, i451, i450) → f1016_0_log_IntArithmetic(EOS(STATIC_1016), i78, i450)
f1016_0_log_IntArithmetic(EOS(STATIC_1016), i78, i450) → f1019_0_log_Return(EOS(STATIC_1019), i78, i450)
f1060_0_log_Return(EOS(STATIC_1060), i78, i510, i512, i510) → f1013_0_log_Return(EOS(STATIC_1013), i78, i510, i512, i510)
f666_0_log_Load(EOS(STATIC_666), i134, i107, i134, i107) → f502_0_log_Load(EOS(STATIC_502), i134, i107, i134, i107)
f664_1_log_InvokeMethod(f518_0_log_Return(EOS(STATIC_518), i144, i142), i78, i142, i144, i142) → f688_0_log_Return(EOS(STATIC_688), i78, i142, i144, i142)
f664_1_log_InvokeMethod(f693_0_log_Return(EOS(STATIC_693), i189, i187), i78, i187, i189, i187) → f735_0_log_Return(EOS(STATIC_735), i78, i187, i189, i187)
f664_1_log_InvokeMethod(f1019_0_log_Return(EOS(STATIC_1019), i512, i510), i78, i510, i512, i510) → f1060_0_log_Return(EOS(STATIC_1060), i78, i510, i512, i510)

Combined rules. Obtained 1 conditional rules for P and 6 conditional rules for R.

P rules:
f504_0_log_Load(EOS(STATIC_504), x0, x1, x0, x1, x0) → f664_1_log_InvokeMethod(f504_0_log_Load(EOS(STATIC_504), /(x0, x1), x1, /(x0, x1), x1, /(x0, x1)), x0, x1, /(x0, x1), x1) | &&(>(x1, 1), <=(x1, x0))
R rules:
f504_0_log_Load(EOS(STATIC_504), x0, x1, x0, x1, x0) → f518_0_log_Return(EOS(STATIC_518), x0, x1) | >(x1, x0)
f504_0_log_Load(EOS(STATIC_504), x0, x1, x0, x1, x0) → f605_0_log_Return(EOS(STATIC_605), x0, x1) | &&(<=(x1, 1), <=(x1, x0))
f504_0_log_Load(EOS(STATIC_504), x0, x1, x0, x1, x0) → f664_1_log_InvokeMethod(f504_0_log_Load(EOS(STATIC_504), /(x0, x1), x1, /(x0, x1), x1, /(x0, x1)), x0, x1, /(x0, x1), x1) | &&(>(x1, 1), <=(x1, x0))
f664_1_log_InvokeMethod(f518_0_log_Return(EOS(STATIC_518), x0, x1), x2, x1, x0, x1) → f693_0_log_Return(EOS(STATIC_693), x2, x1)
f664_1_log_InvokeMethod(f693_0_log_Return(EOS(STATIC_693), x0, x1), x2, x1, x0, x1) → f1019_0_log_Return(EOS(STATIC_1019), x2, x1)
f664_1_log_InvokeMethod(f1019_0_log_Return(EOS(STATIC_1019), x0, x1), x2, x1, x0, x1) → f1019_0_log_Return(EOS(STATIC_1019), x2, x1)

Filtered ground terms:

f504_0_log_Load(x1, x2, x3, x4, x5, x6) → f504_0_log_Load(x2, x3, x4, x5, x6)
Cond_f504_0_log_Load(x1, x2, x3, x4, x5, x6, x7) → Cond_f504_0_log_Load(x1, x3, x4, x5, x6, x7)
f518_0_log_Return(x1, x2, x3) → f518_0_log_Return(x2, x3)
Cond_f504_0_log_Load1(x1, x2, x3, x4, x5, x6, x7) → Cond_f504_0_log_Load1(x1, x3, x4, x5, x6, x7)
f605_0_log_Return(x1, x2, x3) → f605_0_log_Return(x2, x3)
Cond_f504_0_log_Load2(x1, x2, x3, x4, x5, x6, x7) → Cond_f504_0_log_Load2(x1, x3, x4, x5, x6, x7)
f693_0_log_Return(x1, x2, x3) → f693_0_log_Return(x2, x3)
f1019_0_log_Return(x1, x2, x3) → f1019_0_log_Return(x2, x3)

Filtered unneeded arguments:

f664_1_log_InvokeMethod(x1, x2, x3, x4, x5) → f664_1_log_InvokeMethod(x1, x3, x5)

Filtered duplicate args:

f504_0_log_Load(x1, x2, x3, x4, x5) → f504_0_log_Load(x4, x5)
Cond_f504_0_log_Load(x1, x2, x3, x4, x5, x6) → Cond_f504_0_log_Load(x1, x5, x6)
f664_1_log_InvokeMethod(x1, x2, x3) → f664_1_log_InvokeMethod(x1)
Cond_f504_0_log_Load1(x1, x2, x3, x4, x5, x6) → Cond_f504_0_log_Load1(x1, x5, x6)
Cond_f504_0_log_Load2(x1, x2, x3, x4, x5, x6) → Cond_f504_0_log_Load2(x1, x5, x6)

Filtered unneeded arguments:

Cond_f504_0_log_Load1(x1, x2, x3) → Cond_f504_0_log_Load1(x1)

Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.

P rules:
F504_0_LOG_LOAD(x1, x0) → F504_0_LOG_LOAD(x1, /(x0, x1)) | &&(<=(x1, x0), >(x1, 1))
R rules:

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

P rules:
F504_0_LOG_LOAD'(x1, x0) → COND_F504_0_LOG_LOAD(&&(<=(x1, x0), >(x1, 1)), x1, x0)
COND_F504_0_LOG_LOAD(TRUE, x1, x0) → F504_0_LOG_LOAD'(x1, /(x0, x1))
R rules:

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

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): F504_0_LOG_LOAD'(x1[0], x0[0]) → COND_F504_0_LOG_LOAD(x1[0] <= x0[0] && x1[0] > 1, x1[0], x0[0])
(1): COND_F504_0_LOG_LOAD(TRUE, x1[1], x0[1]) → F504_0_LOG_LOAD'(x1[1], x0[1] / x1[1])

(0) -> (1), if (x1[0] <= x0[0] && x1[0] > 1 ∧x1[0] →^* x1[1]∧x0[0] →^* x0[1])

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

The set Q is empty.

(7) 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.IdpDefaultShapeHeuristic@1604f448 Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 1 Max Right Steps: 1

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 F504_0_LOG_LOAD'(x1, x0) → COND_F504_0_LOG_LOAD(&&(<=(x1, x0), >(x1, 1)), x1, x0) the following chains were created:

We consider the chain F504_0_LOG_LOAD'(x1[0], x0[0]) → COND_F504_0_LOG_LOAD(&&(<=(x1[0], x0[0]), >(x1[0], 1)), x1[0], x0[0]), COND_F504_0_LOG_LOAD(TRUE, x1[1], x0[1]) → F504_0_LOG_LOAD'(x1[1], /(x0[1], x1[1])) which results in the following constraint:
(1)    (&&(<=(x1[0], x0[0]), >(x1[0], 1))=TRUE∧x1[0]=x1[1]∧x0[0]=x0[1] ⇒ F504_0_LOG_LOAD'(x1[0], x0[0])≥NonInfC∧F504_0_LOG_LOAD'(x1[0], x0[0])≥COND_F504_0_LOG_LOAD(&&(<=(x1[0], x0[0]), >(x1[0], 1)), x1[0], x0[0])∧(U^Increasing(COND_F504_0_LOG_LOAD(&&(<=(x1[0], x0[0]), >(x1[0], 1)), x1[0], x0[0])), ≥))

We simplified constraint (1) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
(2)    (<=(x1[0], x0[0])=TRUE∧>(x1[0], 1)=TRUE ⇒ F504_0_LOG_LOAD'(x1[0], x0[0])≥NonInfC∧F504_0_LOG_LOAD'(x1[0], x0[0])≥COND_F504_0_LOG_LOAD(&&(<=(x1[0], x0[0]), >(x1[0], 1)), x1[0], x0[0])∧(U^Increasing(COND_F504_0_LOG_LOAD(&&(<=(x1[0], x0[0]), >(x1[0], 1)), x1[0], x0[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x0[0] + [-1]x1[0] ≥ 0∧x1[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_F504_0_LOG_LOAD(&&(<=(x1[0], x0[0]), >(x1[0], 1)), x1[0], x0[0])), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]x0[0] + [(-1)bni_13]x1[0] ≥ 0∧[1 + (-1)bso_14] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x0[0] + [-1]x1[0] ≥ 0∧x1[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_F504_0_LOG_LOAD(&&(<=(x1[0], x0[0]), >(x1[0], 1)), x1[0], x0[0])), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]x0[0] + [(-1)bni_13]x1[0] ≥ 0∧[1 + (-1)bso_14] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x0[0] + [-1]x1[0] ≥ 0∧x1[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_F504_0_LOG_LOAD(&&(<=(x1[0], x0[0]), >(x1[0], 1)), x1[0], x0[0])), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]x0[0] + [(-1)bni_13]x1[0] ≥ 0∧[1 + (-1)bso_14] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x0[0] ≥ 0∧x1[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_F504_0_LOG_LOAD(&&(<=(x1[0], x0[0]), >(x1[0], 1)), x1[0], x0[0])), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]x0[0] ≥ 0∧[1 + (-1)bso_14] ≥ 0)

We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(7)    (x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_F504_0_LOG_LOAD(&&(<=(x1[0], x0[0]), >(x1[0], 1)), x1[0], x0[0])), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]x0[0] ≥ 0∧[1 + (-1)bso_14] ≥ 0)

For Pair COND_F504_0_LOG_LOAD(TRUE, x1, x0) → F504_0_LOG_LOAD'(x1, /(x0, x1)) the following chains were created:

We consider the chain F504_0_LOG_LOAD'(x1[0], x0[0]) → COND_F504_0_LOG_LOAD(&&(<=(x1[0], x0[0]), >(x1[0], 1)), x1[0], x0[0]), COND_F504_0_LOG_LOAD(TRUE, x1[1], x0[1]) → F504_0_LOG_LOAD'(x1[1], /(x0[1], x1[1])), F504_0_LOG_LOAD'(x1[0], x0[0]) → COND_F504_0_LOG_LOAD(&&(<=(x1[0], x0[0]), >(x1[0], 1)), x1[0], x0[0]) which results in the following constraint:
(8)    (&&(<=(x1[0], x0[0]), >(x1[0], 1))=TRUE∧x1[0]=x1[1]∧x0[0]=x0[1]∧x1[1]=x1[0]1∧/(x0[1], x1[1])=x0[0]1 ⇒ COND_F504_0_LOG_LOAD(TRUE, x1[1], x0[1])≥NonInfC∧COND_F504_0_LOG_LOAD(TRUE, x1[1], x0[1])≥F504_0_LOG_LOAD'(x1[1], /(x0[1], x1[1]))∧(U^Increasing(F504_0_LOG_LOAD'(x1[1], /(x0[1], x1[1]))), ≥))

We simplified constraint (8) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(9)    (<=(x1[0], x0[0])=TRUE∧>(x1[0], 1)=TRUE ⇒ COND_F504_0_LOG_LOAD(TRUE, x1[0], x0[0])≥NonInfC∧COND_F504_0_LOG_LOAD(TRUE, x1[0], x0[0])≥F504_0_LOG_LOAD'(x1[0], /(x0[0], x1[0]))∧(U^Increasing(F504_0_LOG_LOAD'(x1[1], /(x0[1], x1[1]))), ≥))

We simplified constraint (9) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(10)    (x0[0] + [-1]x1[0] ≥ 0∧x1[0] + [-2] ≥ 0 ⇒ (U^Increasing(F504_0_LOG_LOAD'(x1[1], /(x0[1], x1[1]))), ≥)∧[(-2)bni_15 + (-1)Bound*bni_15] + [bni_15]x0[0] + [(-1)bni_15]x1[0] ≥ 0∧[-1 + (-1)bso_19] + x0[0] + [-1]max{x0[0], [-1]x0[0]} + min{max{x1[0], [-1]x1[0]} + [-1], max{x0[0], [-1]x0[0]}} ≥ 0)

We simplified constraint (10) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(11)    (x0[0] + [-1]x1[0] ≥ 0∧x1[0] + [-2] ≥ 0 ⇒ (U^Increasing(F504_0_LOG_LOAD'(x1[1], /(x0[1], x1[1]))), ≥)∧[(-2)bni_15 + (-1)Bound*bni_15] + [bni_15]x0[0] + [(-1)bni_15]x1[0] ≥ 0∧[-1 + (-1)bso_19] + x0[0] + [-1]max{x0[0], [-1]x0[0]} + min{max{x1[0], [-1]x1[0]} + [-1], max{x0[0], [-1]x0[0]}} ≥ 0)

We simplified constraint (11) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(12)    (x0[0] + [-1]x1[0] ≥ 0∧x1[0] + [-2] ≥ 0∧[2]x0[0] ≥ 0∧[2]x1[0] ≥ 0 ⇒ (U^Increasing(F504_0_LOG_LOAD'(x1[1], /(x0[1], x1[1]))), ≥)∧[(-2)bni_15 + (-1)Bound*bni_15] + [bni_15]x0[0] + [(-1)bni_15]x1[0] ≥ 0∧[-2 + (-1)bso_19] + x1[0] ≥ 0)

We simplified constraint (12) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(13)    (x0[0] ≥ 0∧x1[0] + [-2] ≥ 0∧[2]x1[0] + [2]x0[0] ≥ 0∧[2]x1[0] ≥ 0 ⇒ (U^Increasing(F504_0_LOG_LOAD'(x1[1], /(x0[1], x1[1]))), ≥)∧[(-2)bni_15 + (-1)Bound*bni_15] + [bni_15]x0[0] ≥ 0∧[-2 + (-1)bso_19] + x1[0] ≥ 0)

We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(14)    (x0[0] ≥ 0∧x1[0] ≥ 0∧[4] + [2]x1[0] + [2]x0[0] ≥ 0∧[4] + [2]x1[0] ≥ 0 ⇒ (U^Increasing(F504_0_LOG_LOAD'(x1[1], /(x0[1], x1[1]))), ≥)∧[(-1)Bound*bni_15 + (-2)bni_15] + [bni_15]x0[0] ≥ 0∧[(-1)bso_19] + x1[0] ≥ 0)

We simplified constraint (14) using rule (IDP_POLY_GCD) which results in the following new constraint:
(15)    (x0[0] ≥ 0∧x1[0] ≥ 0∧[2] + x1[0] + x0[0] ≥ 0∧[2] + x1[0] ≥ 0 ⇒ (U^Increasing(F504_0_LOG_LOAD'(x1[1], /(x0[1], x1[1]))), ≥)∧[(-1)Bound*bni_15 + (-2)bni_15] + [bni_15]x0[0] ≥ 0∧[(-1)bso_19] + x1[0] ≥ 0)

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

F504_0_LOG_LOAD'(x1, x0) → COND_F504_0_LOG_LOAD(&&(<=(x1, x0), >(x1, 1)), x1, x0)
- (x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_F504_0_LOG_LOAD(&&(<=(x1[0], x0[0]), >(x1[0], 1)), x1[0], x0[0])), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]x0[0] ≥ 0∧[1 + (-1)bso_14] ≥ 0)
COND_F504_0_LOG_LOAD(TRUE, x1, x0) → F504_0_LOG_LOAD'(x1, /(x0, x1))
- (x0[0] ≥ 0∧x1[0] ≥ 0∧[2] + x1[0] + x0[0] ≥ 0∧[2] + x1[0] ≥ 0 ⇒ (U^Increasing(F504_0_LOG_LOAD'(x1[1], /(x0[1], x1[1]))), ≥)∧[(-1)Bound*bni_15 + (-2)bni_15] + [bni_15]x0[0] ≥ 0∧[(-1)bso_19] + x1[0] ≥ 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) = [2]
POL(FALSE) = [2]
POL(F504_0_LOG_LOAD'(x₁, x₂)) = [-1] + x₂ + [-1]x₁
POL(COND_F504_0_LOG_LOAD(x₁, x₂, x₃)) = x₃ + [-1]x₂ + [-1]x₁
POL(&&(x₁, x₂)) = [2]
POL(<=(x₁, x₂)) = [-1]
POL(>(x₁, x₂)) = [-1]
POL(1) = [1]

Polynomial Interpretations with Context Sensitive Arithemetic Replacement
POL(Term^CSAR-Mode @ Context)

POL(/(x₁, x1[0])¹ @ {F504_0_LOG_LOAD'_2/1}) = max{x₁, [-1]x₁} + [-1]min{max{x₂, [-1]x₂} + [-1], max{x₁, [-1]x₁}}

The following pairs are in P_>:

F504_0_LOG_LOAD'(x1[0], x0[0]) → COND_F504_0_LOG_LOAD(&&(<=(x1[0], x0[0]), >(x1[0], 1)), x1[0], x0[0])

The following pairs are in P_bound:

F504_0_LOG_LOAD'(x1[0], x0[0]) → COND_F504_0_LOG_LOAD(&&(<=(x1[0], x0[0]), >(x1[0], 1)), x1[0], x0[0])
COND_F504_0_LOG_LOAD(TRUE, x1[1], x0[1]) → F504_0_LOG_LOAD'(x1[1], /(x0[1], x1[1]))

The following pairs are in P_≥:

COND_F504_0_LOG_LOAD(TRUE, x1[1], x0[1]) → F504_0_LOG_LOAD'(x1[1], /(x0[1], x1[1]))

At least the following rules have been oriented under context sensitive arithmetic replacement:

TRUE¹ → &&(TRUE, TRUE)¹
&&(TRUE, FALSE)¹ ↔ FALSE¹
&&(FALSE, TRUE)¹ ↔ FALSE¹
&&(FALSE, FALSE)¹ ↔ FALSE¹
/¹ →

(8) Obligation: