Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_20 (Apple Inc.) Main-Class: Test10

public class Test10 {
    public static void main(String[] args) {
	rec(args.length);
    }

    private static void rec(long l) {
	if (l > 0) {
	    for (int i = (int) l ; i < 100; i++)
		test(i);

	    rec (l - 1);
	}
    }

    private static void test(int i) {
	descend(i);
	descend(i);
	descend(i);
	descend(i);
	descend(i);
	descend(i);
	descend(i);
	descend(i);
    }

    private static void descend(int i) {
	if (i > 0)
	    descend(i - 1);
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

Test10.rec(J)V: Graph of 75 nodes with 1 SCC.

Test10.descend(I)V: Graph of 17 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: Test10.descend(I)V
SCC calls the following helper methods: Test10.descend(I)V
Performed SCC analyses: UsedFieldsAnalysis

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 9 rules for P and 7 rules for R.

P rules:
227_0_descend_LE(EOS(STATIC_227), i46, i46) → 231_0_descend_LE(EOS(STATIC_231), i46, i46)
231_0_descend_LE(EOS(STATIC_231), i46, i46) → 235_0_descend_Load(EOS(STATIC_235), i46) | >(i46, 0)
235_0_descend_Load(EOS(STATIC_235), i46) → 239_0_descend_ConstantStackPush(EOS(STATIC_239), i46)
239_0_descend_ConstantStackPush(EOS(STATIC_239), i46) → 244_0_descend_IntArithmetic(EOS(STATIC_244), i46, 1)
244_0_descend_IntArithmetic(EOS(STATIC_244), i46, matching1) → 248_0_descend_InvokeMethod(EOS(STATIC_248), -(i46, 1)) | &&(>(i46, 0), =(matching1, 1))
248_0_descend_InvokeMethod(EOS(STATIC_248), i48) → 250_1_descend_InvokeMethod(250_0_descend_Load(EOS(STATIC_250), i48), i48)
250_0_descend_Load(EOS(STATIC_250), i48) → 253_0_descend_Load(EOS(STATIC_253), i48)
253_0_descend_Load(EOS(STATIC_253), i48) → 224_0_descend_Load(EOS(STATIC_224), i48)
224_0_descend_Load(EOS(STATIC_224), i42) → 227_0_descend_LE(EOS(STATIC_227), i42, i42)
R rules:
227_0_descend_LE(EOS(STATIC_227), matching1, matching2) → 229_0_descend_LE(EOS(STATIC_229), 0, 0) | &&(=(matching1, 0), =(matching2, 0))
229_0_descend_LE(EOS(STATIC_229), matching1, matching2) → 233_0_descend_Return(EOS(STATIC_233)) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
250_1_descend_InvokeMethod(233_0_descend_Return(EOS(STATIC_233)), matching1) → 263_0_descend_Return(EOS(STATIC_263), 0) | =(matching1, 0)
250_1_descend_InvokeMethod(289_0_descend_Return(EOS(STATIC_289)), i63) → 310_0_descend_Return(EOS(STATIC_310), i63)
263_0_descend_Return(EOS(STATIC_263), matching1) → 284_0_descend_Return(EOS(STATIC_284), 0) | =(matching1, 0)
284_0_descend_Return(EOS(STATIC_284), i57) → 289_0_descend_Return(EOS(STATIC_289))
310_0_descend_Return(EOS(STATIC_310), i63) → 284_0_descend_Return(EOS(STATIC_284), i63)

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

P rules:
227_0_descend_LE(EOS(STATIC_227), x0, x0) → 250_1_descend_InvokeMethod(227_0_descend_LE(EOS(STATIC_227), -(x0, 1), -(x0, 1)), -(x0, 1)) | >(x0, 0)
R rules:
227_0_descend_LE(EOS(STATIC_227), 0, 0) → 233_0_descend_Return(EOS(STATIC_233))
250_1_descend_InvokeMethod(233_0_descend_Return(EOS(STATIC_233)), 0) → 289_0_descend_Return(EOS(STATIC_289))
250_1_descend_InvokeMethod(289_0_descend_Return(EOS(STATIC_289)), x0) → 289_0_descend_Return(EOS(STATIC_289))

Filtered ground terms:

227_0_descend_LE(x1, x2, x3) → 227_0_descend_LE(x2, x3)
Cond_227_0_descend_LE(x1, x2, x3, x4) → Cond_227_0_descend_LE(x1, x3, x4)
289_0_descend_Return(x1) → 289_0_descend_Return
233_0_descend_Return(x1) → 233_0_descend_Return

Filtered duplicate args:

227_0_descend_LE(x1, x2) → 227_0_descend_LE(x2)
Cond_227_0_descend_LE(x1, x2, x3) → Cond_227_0_descend_LE(x1, x3)

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

P rules:
227_0_descend_LE(x0) → 250_1_descend_InvokeMethod(227_0_descend_LE(-(x0, 1)), -(x0, 1)) | >(x0, 0)
R rules:
227_0_descend_LE(0) → 233_0_descend_Return
250_1_descend_InvokeMethod(233_0_descend_Return, 0) → 289_0_descend_Return
250_1_descend_InvokeMethod(289_0_descend_Return, x0) → 289_0_descend_Return

Performed bisimulation on rules. Used the following equivalence classes: {[233_0_descend_Return, 289_0_descend_Return]=233_0_descend_Return}

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

P rules:
227_0_DESCEND_LE(x0) → COND_227_0_DESCEND_LE(>(x0, 0), x0)
COND_227_0_DESCEND_LE(TRUE, x0) → 227_0_DESCEND_LE(-(x0, 1))
R rules:
227_0_descend_LE(0) → 233_0_descend_Return
250_1_descend_InvokeMethod(233_0_descend_Return, 0) → 233_0_descend_Return
250_1_descend_InvokeMethod(233_0_descend_Return, x0) → 233_0_descend_Return

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

Integer

The ITRS R consists of the following rules:
227_0_descend_LE(0) → 233_0_descend_Return
250_1_descend_InvokeMethod(233_0_descend_Return, 0) → 233_0_descend_Return
250_1_descend_InvokeMethod(233_0_descend_Return, x0) → 233_0_descend_Return

The integer pair graph contains the following rules and edges:
(0): 227_0_DESCEND_LE(x0[0]) → COND_227_0_DESCEND_LE(x0[0] > 0, x0[0])
(1): COND_227_0_DESCEND_LE(TRUE, x0[1]) → 227_0_DESCEND_LE(x0[1] - 1)

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

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

The set Q consists of the following terms:
227_0_descend_LE(0)
250_1_descend_InvokeMethod(233_0_descend_Return, x0)

(8) 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@550571f6 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 227_0_DESCEND_LE(x0) → COND_227_0_DESCEND_LE(>(x0, 0), x0) the following chains were created:

• We consider the chain 227_0_DESCEND_LE(x0[0]) → COND_227_0_DESCEND_LE(>(x0[0], 0), x0[0]), COND_227_0_DESCEND_LE(TRUE, x0[1]) → 227_0_DESCEND_LE(-(x0[1], 1)) which results in the following constraint:
  

  (1)    (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 227_0_DESCEND_LE(x0[0])≥NonInfC∧227_0_DESCEND_LE(x0[0])≥COND_227_0_DESCEND_LE(>(x0[0], 0), x0[0])∧(U^Increasing(COND_227_0_DESCEND_LE(>(x0[0], 0), x0[0])), ≥))

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

  (2)    (>(x0[0], 0)=TRUE ⇒ 227_0_DESCEND_LE(x0[0])≥NonInfC∧227_0_DESCEND_LE(x0[0])≥COND_227_0_DESCEND_LE(>(x0[0], 0), x0[0])∧(U^Increasing(COND_227_0_DESCEND_LE(>(x0[0], 0), x0[0])), ≥))

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

  (3)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_227_0_DESCEND_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_11] + [(2)bni_11]x0[0] ≥ 0∧[(-1)bso_12] ≥ 0)

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

  (4)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_227_0_DESCEND_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_11] + [(2)bni_11]x0[0] ≥ 0∧[(-1)bso_12] ≥ 0)

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

  (5)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_227_0_DESCEND_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_11] + [(2)bni_11]x0[0] ≥ 0∧[(-1)bso_12] ≥ 0)

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

  (6)    (x0[0] ≥ 0 ⇒ (U^Increasing(COND_227_0_DESCEND_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_11 + (2)bni_11] + [(2)bni_11]x0[0] ≥ 0∧[(-1)bso_12] ≥ 0)

  
  
  

For Pair COND_227_0_DESCEND_LE(TRUE, x0) → 227_0_DESCEND_LE(-(x0, 1)) the following chains were created:

• We consider the chain COND_227_0_DESCEND_LE(TRUE, x0[1]) → 227_0_DESCEND_LE(-(x0[1], 1)) which results in the following constraint:
  

  (7)    (COND_227_0_DESCEND_LE(TRUE, x0[1])≥NonInfC∧COND_227_0_DESCEND_LE(TRUE, x0[1])≥227_0_DESCEND_LE(-(x0[1], 1))∧(U^Increasing(227_0_DESCEND_LE(-(x0[1], 1))), ≥))

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

  (8)    ((U^Increasing(227_0_DESCEND_LE(-(x0[1], 1))), ≥)∧[bni_13] = 0∧[2 + (-1)bso_14] ≥ 0)

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

  (9)    ((U^Increasing(227_0_DESCEND_LE(-(x0[1], 1))), ≥)∧[bni_13] = 0∧[2 + (-1)bso_14] ≥ 0)

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

  (10)    ((U^Increasing(227_0_DESCEND_LE(-(x0[1], 1))), ≥)∧[bni_13] = 0∧[2 + (-1)bso_14] ≥ 0)

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

  (11)    ((U^Increasing(227_0_DESCEND_LE(-(x0[1], 1))), ≥)∧[bni_13] = 0∧0 = 0∧[2 + (-1)bso_14] ≥ 0)

  
  
  

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

• 227_0_DESCEND_LE(x0) → COND_227_0_DESCEND_LE(>(x0, 0), x0)
  
  • (x0[0] ≥ 0 ⇒ (U^Increasing(COND_227_0_DESCEND_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_11 + (2)bni_11] + [(2)bni_11]x0[0] ≥ 0∧[(-1)bso_12] ≥ 0)
    
  
  
• COND_227_0_DESCEND_LE(TRUE, x0) → 227_0_DESCEND_LE(-(x0, 1))
  
  • ((U^Increasing(227_0_DESCEND_LE(-(x0[1], 1))), ≥)∧[bni_13] = 0∧0 = 0∧[2 + (-1)bso_14] ≥ 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(227_0_descend_LE(x₁)) = [-1]   
POL(0) = 0   
POL(233_0_descend_Return) = [-1]   
POL(250_1_descend_InvokeMethod(x₁, x₂)) = [-1]   
POL(227_0_DESCEND_LE(x₁)) = [2]x₁   
POL(COND_227_0_DESCEND_LE(x₁, x₂)) = [2]x₂   
POL(>(x₁, x₂)) = [-1]   
POL(-(x₁, x₂)) = x₁ + [-1]x₂   
POL(1) = [1]   

The following pairs are in P_>:

COND_227_0_DESCEND_LE(TRUE, x0[1]) → 227_0_DESCEND_LE(-(x0[1], 1))

The following pairs are in P_bound:

227_0_DESCEND_LE(x0[0]) → COND_227_0_DESCEND_LE(>(x0[0], 0), x0[0])

The following pairs are in P_≥:

227_0_DESCEND_LE(x0[0]) → COND_227_0_DESCEND_LE(>(x0[0], 0), x0[0])

There are no usable rules.

(9) Complex Obligation (AND)

(10) 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:
227_0_descend_LE(0) → 233_0_descend_Return
250_1_descend_InvokeMethod(233_0_descend_Return, 0) → 233_0_descend_Return
250_1_descend_InvokeMethod(233_0_descend_Return, x0) → 233_0_descend_Return

The integer pair graph contains the following rules and edges:
(0): 227_0_DESCEND_LE(x0[0]) → COND_227_0_DESCEND_LE(x0[0] > 0, x0[0])


The set Q consists of the following terms:
227_0_descend_LE(0)
250_1_descend_InvokeMethod(233_0_descend_Return, x0)

(11) IDependencyGraphProof (EQUIVALENT transformation)

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

(12) TRUE

(13) 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:
227_0_descend_LE(0) → 233_0_descend_Return
250_1_descend_InvokeMethod(233_0_descend_Return, 0) → 233_0_descend_Return
250_1_descend_InvokeMethod(233_0_descend_Return, x0) → 233_0_descend_Return

The integer pair graph contains the following rules and edges:
(1): COND_227_0_DESCEND_LE(TRUE, x0[1]) → 227_0_DESCEND_LE(x0[1] - 1)


The set Q consists of the following terms:
227_0_descend_LE(0)
250_1_descend_InvokeMethod(233_0_descend_Return, x0)

(14) IDependencyGraphProof (EQUIVALENT transformation)

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

(15) TRUE

(16) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test10.rec(J)V
SCC calls the following helper methods: Test10.descend(I)V, Test10.rec(J)V
Performed SCC analyses: UsedFieldsAnalysis

(17) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 59 rules for P and 40 rules for R.

P rules:
63_0_rec_ConstantStackPush(EOS(STATIC_63), i3, i3) → 65_0_rec_Cmp(EOS(STATIC_65), i3, i3, 0)
65_0_rec_Cmp(EOS(STATIC_65), i6, i6, matching1) → 68_0_rec_Cmp(EOS(STATIC_68), i6, i6, 0) | =(matching1, 0)
68_0_rec_Cmp(EOS(STATIC_68), i6, i6, matching1) → 72_0_rec_LE(EOS(STATIC_72), i6, 1) | &&(>(i6, 0), =(matching1, 0))
72_0_rec_LE(EOS(STATIC_72), i6, matching1) → 76_0_rec_Load(EOS(STATIC_76), i6) | &&(>(1, 0), =(matching1, 1))
76_0_rec_Load(EOS(STATIC_76), i6) → 81_0_rec_TypeCast(EOS(STATIC_81), i6, i6)
81_0_rec_TypeCast(EOS(STATIC_81), i6, i6) → 92_0_rec_Store(EOS(STATIC_92), i6, i10) | =(i10, i6)
92_0_rec_Store(EOS(STATIC_92), i6, i10) → 94_0_rec_Load(EOS(STATIC_94), i6, i10)
94_0_rec_Load(EOS(STATIC_94), i6, i10) → 96_0_rec_ConstantStackPush(EOS(STATIC_96), i6, i10, i10)
96_0_rec_ConstantStackPush(EOS(STATIC_96), i6, i10, i10) → 99_0_rec_GE(EOS(STATIC_99), i6, i10, i10, 100)
99_0_rec_GE(EOS(STATIC_99), i6, i14, i14, matching1) → 102_0_rec_GE(EOS(STATIC_102), i6, i14, i14, 100) | =(matching1, 100)
99_0_rec_GE(EOS(STATIC_99), i6, i15, i15, matching1) → 103_0_rec_GE(EOS(STATIC_103), i6, i15, i15, 100) | =(matching1, 100)
102_0_rec_GE(EOS(STATIC_102), i6, i14, i14, matching1) → 105_0_rec_Load(EOS(STATIC_105), i6, i14) | &&(<(i14, 100), =(matching1, 100))
105_0_rec_Load(EOS(STATIC_105), i6, i14) → 109_0_rec_InvokeMethod(EOS(STATIC_109), i6, i14, i14)
109_0_rec_InvokeMethod(EOS(STATIC_109), i6, i14, i14) → 113_0_test_Load(EOS(STATIC_113), i6, i14, i14, i14)
113_0_test_Load(EOS(STATIC_113), i6, i14, i14, i14) → 120_0_test_InvokeMethod(EOS(STATIC_120), i6, i14, i14, i14, i14)
120_0_test_InvokeMethod(EOS(STATIC_120), i6, i14, i14, i14, i14) → 123_1_test_InvokeMethod(123_0_descend_Load(EOS(STATIC_123), i14), i6, i14, i14, i14, i14)
123_1_test_InvokeMethod(289_0_descend_Return(EOS(STATIC_289)), i6, i60, i60, i60, i60) → 307_0_descend_Return(EOS(STATIC_307), i6, i60, i60, i60, i60)
307_0_descend_Return(EOS(STATIC_307), i6, i60, i60, i60, i60) → 278_0_descend_Return(EOS(STATIC_278), i6, i60, i60, i60, i60)
278_0_descend_Return(EOS(STATIC_278), i6, i53, i53, i53, i53) → 287_0_test_Load(EOS(STATIC_287), i6, i53, i53, i53)
287_0_test_Load(EOS(STATIC_287), i6, i53, i53, i53) → 291_0_test_InvokeMethod(EOS(STATIC_291), i6, i53, i53, i53, i53)
291_0_test_InvokeMethod(EOS(STATIC_291), i6, i53, i53, i53, i53) → 295_1_test_InvokeMethod(295_0_descend_Load(EOS(STATIC_295), i53), i6, i53, i53, i53, i53)
295_1_test_InvokeMethod(289_0_descend_Return(EOS(STATIC_289)), i6, i69, i69, i69, i69) → 319_0_descend_Return(EOS(STATIC_319), i6, i69, i69, i69, i69)
319_0_descend_Return(EOS(STATIC_319), i6, i69, i69, i69, i69) → 320_0_test_Load(EOS(STATIC_320), i6, i69, i69, i69)
320_0_test_Load(EOS(STATIC_320), i6, i69, i69, i69) → 322_0_test_InvokeMethod(EOS(STATIC_322), i6, i69, i69, i69, i69)
322_0_test_InvokeMethod(EOS(STATIC_322), i6, i69, i69, i69, i69) → 324_1_test_InvokeMethod(324_0_descend_Load(EOS(STATIC_324), i69), i6, i69, i69, i69, i69)
324_1_test_InvokeMethod(289_0_descend_Return(EOS(STATIC_289)), i6, i73, i73, i73, i73) → 335_0_descend_Return(EOS(STATIC_335), i6, i73, i73, i73, i73)
335_0_descend_Return(EOS(STATIC_335), i6, i73, i73, i73, i73) → 337_0_test_Load(EOS(STATIC_337), i6, i73, i73, i73)
337_0_test_Load(EOS(STATIC_337), i6, i73, i73, i73) → 339_0_test_InvokeMethod(EOS(STATIC_339), i6, i73, i73, i73, i73)
339_0_test_InvokeMethod(EOS(STATIC_339), i6, i73, i73, i73, i73) → 341_1_test_InvokeMethod(341_0_descend_Load(EOS(STATIC_341), i73), i6, i73, i73, i73, i73)
341_1_test_InvokeMethod(289_0_descend_Return(EOS(STATIC_289)), i6, i75, i75, i75, i75) → 352_0_descend_Return(EOS(STATIC_352), i6, i75, i75, i75, i75)
352_0_descend_Return(EOS(STATIC_352), i6, i75, i75, i75, i75) → 353_0_test_Load(EOS(STATIC_353), i6, i75, i75, i75)
353_0_test_Load(EOS(STATIC_353), i6, i75, i75, i75) → 356_0_test_InvokeMethod(EOS(STATIC_356), i6, i75, i75, i75, i75)
356_0_test_InvokeMethod(EOS(STATIC_356), i6, i75, i75, i75, i75) → 358_1_test_InvokeMethod(358_0_descend_Load(EOS(STATIC_358), i75), i6, i75, i75, i75, i75)
358_1_test_InvokeMethod(289_0_descend_Return(EOS(STATIC_289)), i6, i79, i79, i79, i79) → 369_0_descend_Return(EOS(STATIC_369), i6, i79, i79, i79, i79)
369_0_descend_Return(EOS(STATIC_369), i6, i79, i79, i79, i79) → 371_0_test_Load(EOS(STATIC_371), i6, i79, i79, i79)
371_0_test_Load(EOS(STATIC_371), i6, i79, i79, i79) → 373_0_test_InvokeMethod(EOS(STATIC_373), i6, i79, i79, i79, i79)
373_0_test_InvokeMethod(EOS(STATIC_373), i6, i79, i79, i79, i79) → 375_1_test_InvokeMethod(375_0_descend_Load(EOS(STATIC_375), i79), i6, i79, i79, i79, i79)
375_1_test_InvokeMethod(289_0_descend_Return(EOS(STATIC_289)), i6, i82, i82, i82, i82) → 389_0_descend_Return(EOS(STATIC_389), i6, i82, i82, i82, i82)
389_0_descend_Return(EOS(STATIC_389), i6, i82, i82, i82, i82) → 391_0_test_Load(EOS(STATIC_391), i6, i82, i82, i82)
391_0_test_Load(EOS(STATIC_391), i6, i82, i82, i82) → 393_0_test_InvokeMethod(EOS(STATIC_393), i6, i82, i82, i82, i82)
393_0_test_InvokeMethod(EOS(STATIC_393), i6, i82, i82, i82, i82) → 395_1_test_InvokeMethod(395_0_descend_Load(EOS(STATIC_395), i82), i6, i82, i82, i82, i82)
395_1_test_InvokeMethod(289_0_descend_Return(EOS(STATIC_289)), i6, i86, i86, i86, i86) → 405_0_descend_Return(EOS(STATIC_405), i6, i86, i86, i86, i86)
405_0_descend_Return(EOS(STATIC_405), i6, i86, i86, i86, i86) → 407_0_test_Load(EOS(STATIC_407), i6, i86, i86, i86)
407_0_test_Load(EOS(STATIC_407), i6, i86, i86, i86) → 409_0_test_InvokeMethod(EOS(STATIC_409), i6, i86, i86, i86)
409_0_test_InvokeMethod(EOS(STATIC_409), i6, i86, i86, i86) → 410_1_test_InvokeMethod(410_0_descend_Load(EOS(STATIC_410), i86), i6, i86, i86, i86)
410_1_test_InvokeMethod(289_0_descend_Return(EOS(STATIC_289)), i6, i90, i90, i90) → 421_0_descend_Return(EOS(STATIC_421), i6, i90, i90, i90)
421_0_descend_Return(EOS(STATIC_421), i6, i90, i90, i90) → 423_0_test_Return(EOS(STATIC_423), i6, i90, i90)
423_0_test_Return(EOS(STATIC_423), i6, i90, i90) → 425_0_rec_Inc(EOS(STATIC_425), i6, i90)
425_0_rec_Inc(EOS(STATIC_425), i6, i90) → 427_0_rec_JMP(EOS(STATIC_427), i6, +(i90, 1)) | >(i90, 0)
427_0_rec_JMP(EOS(STATIC_427), i6, i92) → 430_0_rec_Load(EOS(STATIC_430), i6, i92)
430_0_rec_Load(EOS(STATIC_430), i6, i92) → 94_0_rec_Load(EOS(STATIC_94), i6, i92)
103_0_rec_GE(EOS(STATIC_103), i6, i15, i15, matching1) → 107_0_rec_Load(EOS(STATIC_107), i6) | &&(>=(i15, 100), =(matching1, 100))
107_0_rec_Load(EOS(STATIC_107), i6) → 111_0_rec_ConstantStackPush(EOS(STATIC_111), i6)
111_0_rec_ConstantStackPush(EOS(STATIC_111), i6) → 114_0_rec_IntArithmetic(EOS(STATIC_114), i6, 1)
114_0_rec_IntArithmetic(EOS(STATIC_114), i6, matching1) → 117_0_rec_InvokeMethod(EOS(STATIC_117), -(i6, 1)) | &&(>(i6, 0), =(matching1, 1))
117_0_rec_InvokeMethod(EOS(STATIC_117), i17) → 121_1_rec_InvokeMethod(121_0_rec_Load(EOS(STATIC_121), i17), i17)
121_0_rec_Load(EOS(STATIC_121), i17) → 126_0_rec_Load(EOS(STATIC_126), i17)
126_0_rec_Load(EOS(STATIC_126), i17) → 61_0_rec_Load(EOS(STATIC_61), i17)
61_0_rec_Load(EOS(STATIC_61), i3) → 63_0_rec_ConstantStackPush(EOS(STATIC_63), i3, i3)
R rules:
123_0_descend_Load(EOS(STATIC_123), i14) → 129_0_descend_Load(EOS(STATIC_129), i14)
129_0_descend_Load(EOS(STATIC_129), i14) → 224_0_descend_Load(EOS(STATIC_224), i14)
295_0_descend_Load(EOS(STATIC_295), i53) → 304_0_descend_Load(EOS(STATIC_304), i53)
304_0_descend_Load(EOS(STATIC_304), i53) → 224_0_descend_Load(EOS(STATIC_224), i53)
324_0_descend_Load(EOS(STATIC_324), i69) → 326_0_descend_Load(EOS(STATIC_326), i69)
326_0_descend_Load(EOS(STATIC_326), i69) → 224_0_descend_Load(EOS(STATIC_224), i69)
341_0_descend_Load(EOS(STATIC_341), i73) → 343_0_descend_Load(EOS(STATIC_343), i73)
343_0_descend_Load(EOS(STATIC_343), i73) → 224_0_descend_Load(EOS(STATIC_224), i73)
358_0_descend_Load(EOS(STATIC_358), i75) → 360_0_descend_Load(EOS(STATIC_360), i75)
360_0_descend_Load(EOS(STATIC_360), i75) → 224_0_descend_Load(EOS(STATIC_224), i75)
375_0_descend_Load(EOS(STATIC_375), i79) → 377_0_descend_Load(EOS(STATIC_377), i79)
377_0_descend_Load(EOS(STATIC_377), i79) → 224_0_descend_Load(EOS(STATIC_224), i79)
395_0_descend_Load(EOS(STATIC_395), i82) → 398_0_descend_Load(EOS(STATIC_398), i82)
398_0_descend_Load(EOS(STATIC_398), i82) → 224_0_descend_Load(EOS(STATIC_224), i82)
410_0_descend_Load(EOS(STATIC_410), i86) → 412_0_descend_Load(EOS(STATIC_412), i86)
412_0_descend_Load(EOS(STATIC_412), i86) → 224_0_descend_Load(EOS(STATIC_224), i86)
253_0_descend_Load(EOS(STATIC_253), i48) → 224_0_descend_Load(EOS(STATIC_224), i48)
224_0_descend_Load(EOS(STATIC_224), i42) → 227_0_descend_LE(EOS(STATIC_227), i42, i42)
227_0_descend_LE(EOS(STATIC_227), matching1, matching2) → 229_0_descend_LE(EOS(STATIC_229), 0, 0) | &&(=(matching1, 0), =(matching2, 0))
227_0_descend_LE(EOS(STATIC_227), i46, i46) → 231_0_descend_LE(EOS(STATIC_231), i46, i46)
229_0_descend_LE(EOS(STATIC_229), matching1, matching2) → 233_0_descend_Return(EOS(STATIC_233)) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
231_0_descend_LE(EOS(STATIC_231), i46, i46) → 235_0_descend_Load(EOS(STATIC_235), i46) | >(i46, 0)
235_0_descend_Load(EOS(STATIC_235), i46) → 239_0_descend_ConstantStackPush(EOS(STATIC_239), i46)
239_0_descend_ConstantStackPush(EOS(STATIC_239), i46) → 244_0_descend_IntArithmetic(EOS(STATIC_244), i46, 1)
244_0_descend_IntArithmetic(EOS(STATIC_244), i46, matching1) → 248_0_descend_InvokeMethod(EOS(STATIC_248), -(i46, 1)) | &&(>(i46, 0), =(matching1, 1))
248_0_descend_InvokeMethod(EOS(STATIC_248), i48) → 250_1_descend_InvokeMethod(250_0_descend_Load(EOS(STATIC_250), i48), i48)
250_0_descend_Load(EOS(STATIC_250), i48) → 253_0_descend_Load(EOS(STATIC_253), i48)
250_1_descend_InvokeMethod(233_0_descend_Return(EOS(STATIC_233)), matching1) → 263_0_descend_Return(EOS(STATIC_263), 0) | =(matching1, 0)
250_1_descend_InvokeMethod(289_0_descend_Return(EOS(STATIC_289)), i63) → 310_0_descend_Return(EOS(STATIC_310), i63)
263_0_descend_Return(EOS(STATIC_263), matching1) → 284_0_descend_Return(EOS(STATIC_284), 0) | =(matching1, 0)
284_0_descend_Return(EOS(STATIC_284), i57) → 289_0_descend_Return(EOS(STATIC_289))
310_0_descend_Return(EOS(STATIC_310), i63) → 284_0_descend_Return(EOS(STATIC_284), i63)
65_0_rec_Cmp(EOS(STATIC_65), matching1, matching2, matching3) → 67_0_rec_Cmp(EOS(STATIC_67), 0, 0, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
67_0_rec_Cmp(EOS(STATIC_67), matching1, matching2, matching3) → 69_0_rec_LE(EOS(STATIC_69), 0, 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
69_0_rec_LE(EOS(STATIC_69), matching1, matching2) → 74_0_rec_Return(EOS(STATIC_74)) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
121_1_rec_InvokeMethod(74_0_rec_Return(EOS(STATIC_74)), matching1) → 140_0_rec_Return(EOS(STATIC_140), 0) | =(matching1, 0)
121_1_rec_InvokeMethod(191_0_rec_Return(EOS(STATIC_191)), i37) → 219_0_rec_Return(EOS(STATIC_219), i37)
140_0_rec_Return(EOS(STATIC_140), matching1) → 183_0_rec_Return(EOS(STATIC_183), 0) | =(matching1, 0)
183_0_rec_Return(EOS(STATIC_183), i31) → 191_0_rec_Return(EOS(STATIC_191))
219_0_rec_Return(EOS(STATIC_219), i37) → 183_0_rec_Return(EOS(STATIC_183), i37)

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

P rules:
99_0_rec_GE(EOS(STATIC_99), x0, x1, x1, 100) → 123_1_test_InvokeMethod(123_0_descend_Load(EOS(STATIC_123), x1), x0, x1, x1, x1, x1) | <(x1, 100)
123_1_test_InvokeMethod(289_0_descend_Return(EOS(STATIC_289)), x0, x1, x1, x1, x1) → 295_1_test_InvokeMethod(295_0_descend_Load(EOS(STATIC_295), x1), x0, x1, x1, x1, x1)
295_1_test_InvokeMethod(289_0_descend_Return(EOS(STATIC_289)), x0, x1, x1, x1, x1) → 324_1_test_InvokeMethod(324_0_descend_Load(EOS(STATIC_324), x1), x0, x1, x1, x1, x1)
324_1_test_InvokeMethod(289_0_descend_Return(EOS(STATIC_289)), x0, x1, x1, x1, x1) → 341_1_test_InvokeMethod(341_0_descend_Load(EOS(STATIC_341), x1), x0, x1, x1, x1, x1)
341_1_test_InvokeMethod(289_0_descend_Return(EOS(STATIC_289)), x0, x1, x1, x1, x1) → 358_1_test_InvokeMethod(358_0_descend_Load(EOS(STATIC_358), x1), x0, x1, x1, x1, x1)
358_1_test_InvokeMethod(289_0_descend_Return(EOS(STATIC_289)), x0, x1, x1, x1, x1) → 375_1_test_InvokeMethod(375_0_descend_Load(EOS(STATIC_375), x1), x0, x1, x1, x1, x1)
375_1_test_InvokeMethod(289_0_descend_Return(EOS(STATIC_289)), x0, x1, x1, x1, x1) → 395_1_test_InvokeMethod(395_0_descend_Load(EOS(STATIC_395), x1), x0, x1, x1, x1, x1)
395_1_test_InvokeMethod(289_0_descend_Return(EOS(STATIC_289)), x0, x1, x1, x1, x1) → 410_1_test_InvokeMethod(410_0_descend_Load(EOS(STATIC_410), x1), x0, x1, x1, x1)
410_1_test_InvokeMethod(289_0_descend_Return(EOS(STATIC_289)), x0, x1, x1, x1) → 99_0_rec_GE(EOS(STATIC_99), x0, +(x1, 1), +(x1, 1), 100) | >(x1, 0)
99_0_rec_GE(EOS(STATIC_99), x0, x1, x1, 100) → 121_1_rec_InvokeMethod(99_0_rec_GE(EOS(STATIC_99), -(x0, 1), -(x0, 1), -(x0, 1), 100), -(x0, 1)) | &&(>(+(x1, 1), 100), >(x0, 1))
R rules:
123_0_descend_Load(EOS(STATIC_123), x0) → 227_0_descend_LE(EOS(STATIC_227), x0, x0)
295_0_descend_Load(EOS(STATIC_295), x0) → 227_0_descend_LE(EOS(STATIC_227), x0, x0)
324_0_descend_Load(EOS(STATIC_324), x0) → 227_0_descend_LE(EOS(STATIC_227), x0, x0)
341_0_descend_Load(EOS(STATIC_341), x0) → 227_0_descend_LE(EOS(STATIC_227), x0, x0)
358_0_descend_Load(EOS(STATIC_358), x0) → 227_0_descend_LE(EOS(STATIC_227), x0, x0)
375_0_descend_Load(EOS(STATIC_375), x0) → 227_0_descend_LE(EOS(STATIC_227), x0, x0)
395_0_descend_Load(EOS(STATIC_395), x0) → 227_0_descend_LE(EOS(STATIC_227), x0, x0)
410_0_descend_Load(EOS(STATIC_410), x0) → 227_0_descend_LE(EOS(STATIC_227), x0, x0)
227_0_descend_LE(EOS(STATIC_227), 0, 0) → 233_0_descend_Return(EOS(STATIC_233))
227_0_descend_LE(EOS(STATIC_227), x0, x0) → 250_1_descend_InvokeMethod(227_0_descend_LE(EOS(STATIC_227), -(x0, 1), -(x0, 1)), -(x0, 1)) | >(x0, 0)
250_1_descend_InvokeMethod(233_0_descend_Return(EOS(STATIC_233)), 0) → 289_0_descend_Return(EOS(STATIC_289))
250_1_descend_InvokeMethod(289_0_descend_Return(EOS(STATIC_289)), x0) → 289_0_descend_Return(EOS(STATIC_289))
121_1_rec_InvokeMethod(74_0_rec_Return(EOS(STATIC_74)), 0) → 191_0_rec_Return(EOS(STATIC_191))
121_1_rec_InvokeMethod(191_0_rec_Return(EOS(STATIC_191)), x0) → 191_0_rec_Return(EOS(STATIC_191))

Filtered ground terms:

99_0_rec_GE(x1, x2, x3, x4, x5) → 99_0_rec_GE(x2, x3, x4)
Cond_99_0_rec_GE1(x1, x2, x3, x4, x5, x6) → Cond_99_0_rec_GE1(x1, x3, x4, x5)
Cond_410_1_test_InvokeMethod(x1, x2, x3, x4, x5, x6) → Cond_410_1_test_InvokeMethod(x1, x3, x4, x5, x6)
289_0_descend_Return(x1) → 289_0_descend_Return
410_0_descend_Load(x1, x2) → 410_0_descend_Load(x2)
395_0_descend_Load(x1, x2) → 395_0_descend_Load(x2)
375_0_descend_Load(x1, x2) → 375_0_descend_Load(x2)
358_0_descend_Load(x1, x2) → 358_0_descend_Load(x2)
341_0_descend_Load(x1, x2) → 341_0_descend_Load(x2)
324_0_descend_Load(x1, x2) → 324_0_descend_Load(x2)
295_0_descend_Load(x1, x2) → 295_0_descend_Load(x2)
123_0_descend_Load(x1, x2) → 123_0_descend_Load(x2)
Cond_99_0_rec_GE(x1, x2, x3, x4, x5, x6) → Cond_99_0_rec_GE(x1, x3, x4, x5)
191_0_rec_Return(x1) → 191_0_rec_Return
74_0_rec_Return(x1) → 74_0_rec_Return
233_0_descend_Return(x1) → 233_0_descend_Return
227_0_descend_LE(x1, x2, x3) → 227_0_descend_LE(x2, x3)
Cond_227_0_descend_LE(x1, x2, x3, x4) → Cond_227_0_descend_LE(x1, x3, x4)

Filtered duplicate args:

99_0_rec_GE(x1, x2, x3) → 99_0_rec_GE(x1, x3)
Cond_99_0_rec_GE(x1, x2, x3, x4) → Cond_99_0_rec_GE(x1, x2, x4)
123_1_test_InvokeMethod(x1, x2, x3, x4, x5, x6) → 123_1_test_InvokeMethod(x1, x2, x6)
295_1_test_InvokeMethod(x1, x2, x3, x4, x5, x6) → 295_1_test_InvokeMethod(x1, x2, x6)
324_1_test_InvokeMethod(x1, x2, x3, x4, x5, x6) → 324_1_test_InvokeMethod(x1, x2, x6)
341_1_test_InvokeMethod(x1, x2, x3, x4, x5, x6) → 341_1_test_InvokeMethod(x1, x2, x6)
358_1_test_InvokeMethod(x1, x2, x3, x4, x5, x6) → 358_1_test_InvokeMethod(x1, x2, x6)
375_1_test_InvokeMethod(x1, x2, x3, x4, x5, x6) → 375_1_test_InvokeMethod(x1, x2, x6)
395_1_test_InvokeMethod(x1, x2, x3, x4, x5, x6) → 395_1_test_InvokeMethod(x1, x2, x6)
410_1_test_InvokeMethod(x1, x2, x3, x4, x5) → 410_1_test_InvokeMethod(x1, x2, x5)
Cond_410_1_test_InvokeMethod(x1, x2, x3, x4, x5) → Cond_410_1_test_InvokeMethod(x1, x2, x5)
Cond_99_0_rec_GE1(x1, x2, x3, x4) → Cond_99_0_rec_GE1(x1, x2, x4)
227_0_descend_LE(x1, x2) → 227_0_descend_LE(x2)
Cond_227_0_descend_LE(x1, x2, x3) → Cond_227_0_descend_LE(x1, x3)

Filtered unneeded arguments:

Cond_99_0_rec_GE1(x1, x2, x3) → Cond_99_0_rec_GE1(x1, x2)

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

P rules:
99_0_rec_GE(x0, x1) → 123_1_test_InvokeMethod(123_0_descend_Load(x1), x0, x1) | <(x1, 100)
123_1_test_InvokeMethod(289_0_descend_Return, x0, x1) → 295_1_test_InvokeMethod(295_0_descend_Load(x1), x0, x1)
295_1_test_InvokeMethod(289_0_descend_Return, x0, x1) → 324_1_test_InvokeMethod(324_0_descend_Load(x1), x0, x1)
324_1_test_InvokeMethod(289_0_descend_Return, x0, x1) → 341_1_test_InvokeMethod(341_0_descend_Load(x1), x0, x1)
341_1_test_InvokeMethod(289_0_descend_Return, x0, x1) → 358_1_test_InvokeMethod(358_0_descend_Load(x1), x0, x1)
358_1_test_InvokeMethod(289_0_descend_Return, x0, x1) → 375_1_test_InvokeMethod(375_0_descend_Load(x1), x0, x1)
375_1_test_InvokeMethod(289_0_descend_Return, x0, x1) → 395_1_test_InvokeMethod(395_0_descend_Load(x1), x0, x1)
395_1_test_InvokeMethod(289_0_descend_Return, x0, x1) → 410_1_test_InvokeMethod(410_0_descend_Load(x1), x0, x1)
410_1_test_InvokeMethod(289_0_descend_Return, x0, x1) → 99_0_rec_GE(x0, +(x1, 1)) | >(x1, 0)
99_0_rec_GE(x0, x1) → 121_1_rec_InvokeMethod(99_0_rec_GE(-(x0, 1), -(x0, 1)), -(x0, 1)) | &&(>(x1, 99), >(x0, 1))
R rules:
123_0_descend_Load(x0) → 227_0_descend_LE(x0)
295_0_descend_Load(x0) → 227_0_descend_LE(x0)
324_0_descend_Load(x0) → 227_0_descend_LE(x0)
341_0_descend_Load(x0) → 227_0_descend_LE(x0)
358_0_descend_Load(x0) → 227_0_descend_LE(x0)
375_0_descend_Load(x0) → 227_0_descend_LE(x0)
395_0_descend_Load(x0) → 227_0_descend_LE(x0)
410_0_descend_Load(x0) → 227_0_descend_LE(x0)
227_0_descend_LE(0) → 233_0_descend_Return
227_0_descend_LE(x0) → 250_1_descend_InvokeMethod(227_0_descend_LE(-(x0, 1)), -(x0, 1)) | >(x0, 0)
250_1_descend_InvokeMethod(233_0_descend_Return, 0) → 289_0_descend_Return
250_1_descend_InvokeMethod(289_0_descend_Return, x0) → 289_0_descend_Return
121_1_rec_InvokeMethod(74_0_rec_Return, 0) → 191_0_rec_Return
121_1_rec_InvokeMethod(191_0_rec_Return, x0) → 191_0_rec_Return

Performed bisimulation on rules. Used the following equivalence classes: {[123_0_descend_Load_1, 295_0_descend_Load_1, 324_0_descend_Load_1, 341_0_descend_Load_1, 358_0_descend_Load_1, 375_0_descend_Load_1, 395_0_descend_Load_1, 410_0_descend_Load_1]=123_0_descend_Load_1, [233_0_descend_Return, 289_0_descend_Return, 74_0_rec_Return, 191_0_rec_Return]=233_0_descend_Return}

Finished conversion. Obtained 13 rules for P and 8 rules for R. System has predefined symbols.

P rules:
99_0_REC_GE(x0, x1) → COND_99_0_REC_GE(<(x1, 100), x0, x1)
COND_99_0_REC_GE(TRUE, x0, x1) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1), x0, x1)
123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0, x1) → 295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1), x0, x1)
295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0, x1) → 324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1), x0, x1)
324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0, x1) → 341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1), x0, x1)
341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0, x1) → 358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1), x0, x1)
358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0, x1) → 375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1), x0, x1)
375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0, x1) → 395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1), x0, x1)
395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0, x1) → 410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1), x0, x1)
410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0, x1) → COND_410_1_TEST_INVOKEMETHOD(>(x1, 0), 233_0_descend_Return, x0, x1)
COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0, x1) → 99_0_REC_GE(x0, +(x1, 1))
99_0_REC_GE(x0, x1) → COND_99_0_REC_GE1(&&(>(x1, 99), >(x0, 1)), x0, x1)
COND_99_0_REC_GE1(TRUE, x0, x1) → 99_0_REC_GE(-(x0, 1), -(x0, 1))
R rules:
123_0_descend_Load(x0) → 227_0_descend_LE(x0)
227_0_descend_LE(0) → 233_0_descend_Return
227_0_descend_LE(x0) → Cond_227_0_descend_LE(>(x0, 0), x0)
Cond_227_0_descend_LE(TRUE, x0) → 250_1_descend_InvokeMethod(227_0_descend_LE(-(x0, 1)), -(x0, 1))
250_1_descend_InvokeMethod(233_0_descend_Return, 0) → 233_0_descend_Return
250_1_descend_InvokeMethod(233_0_descend_Return, x0) → 233_0_descend_Return
121_1_rec_InvokeMethod(233_0_descend_Return, 0) → 233_0_descend_Return
121_1_rec_InvokeMethod(233_0_descend_Return, x0) → 233_0_descend_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, Boolean

The ITRS R consists of the following rules:
123_0_descend_Load(x0) → 227_0_descend_LE(x0)
227_0_descend_LE(0) → 233_0_descend_Return
227_0_descend_LE(x0) → Cond_227_0_descend_LE(x0 > 0, x0)
Cond_227_0_descend_LE(TRUE, x0) → 250_1_descend_InvokeMethod(227_0_descend_LE(x0 - 1), x0 - 1)
250_1_descend_InvokeMethod(233_0_descend_Return, 0) → 233_0_descend_Return
250_1_descend_InvokeMethod(233_0_descend_Return, x0) → 233_0_descend_Return
121_1_rec_InvokeMethod(233_0_descend_Return, 0) → 233_0_descend_Return
121_1_rec_InvokeMethod(233_0_descend_Return, x0) → 233_0_descend_Return

The integer pair graph contains the following rules and edges:
(0): 99_0_REC_GE(x0[0], x1[0]) → COND_99_0_REC_GE(x1[0] < 100, x0[0], x1[0])
(1): COND_99_0_REC_GE(TRUE, x0[1], x1[1]) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])
(2): 123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2]) → 295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])
(3): 295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3]) → 324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])
(4): 324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4]) → 341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])
(5): 341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5]) → 358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])
(6): 358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6]) → 375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])
(7): 375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7]) → 395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])
(8): 395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8]) → 410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])
(9): 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9]) → COND_410_1_TEST_INVOKEMETHOD(x1[9] > 0, 233_0_descend_Return, x0[9], x1[9])
(10): COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10]) → 99_0_REC_GE(x0[10], x1[10] + 1)
(11): 99_0_REC_GE(x0[11], x1[11]) → COND_99_0_REC_GE1(x1[11] > 99 && x0[11] > 1, x0[11], x1[11])
(12): COND_99_0_REC_GE1(TRUE, x0[12], x1[12]) → 99_0_REC_GE(x0[12] - 1, x0[12] - 1)

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

(1) -> (2), if (123_0_descend_Load(x1[1]) →^* 233_0_descend_Return∧x0[1] →^* x0[2]∧x1[1] →^* x1[2])

(2) -> (3), if (123_0_descend_Load(x1[2]) →^* 233_0_descend_Return∧x0[2] →^* x0[3]∧x1[2] →^* x1[3])

(3) -> (4), if (123_0_descend_Load(x1[3]) →^* 233_0_descend_Return∧x0[3] →^* x0[4]∧x1[3] →^* x1[4])

(4) -> (5), if (123_0_descend_Load(x1[4]) →^* 233_0_descend_Return∧x0[4] →^* x0[5]∧x1[4] →^* x1[5])

(5) -> (6), if (123_0_descend_Load(x1[5]) →^* 233_0_descend_Return∧x0[5] →^* x0[6]∧x1[5] →^* x1[6])

(6) -> (7), if (123_0_descend_Load(x1[6]) →^* 233_0_descend_Return∧x0[6] →^* x0[7]∧x1[6] →^* x1[7])

(7) -> (8), if (123_0_descend_Load(x1[7]) →^* 233_0_descend_Return∧x0[7] →^* x0[8]∧x1[7] →^* x1[8])

(8) -> (9), if (123_0_descend_Load(x1[8]) →^* 233_0_descend_Return∧x0[8] →^* x0[9]∧x1[8] →^* x1[9])

(9) -> (10), if (x1[9] > 0 ∧x0[9] →^* x0[10]∧x1[9] →^* x1[10])

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

(10) -> (11), if (x0[10] →^* x0[11]∧x1[10] + 1 →^* x1[11])

(11) -> (12), if (x1[11] > 99 && x0[11] > 1 ∧x0[11] →^* x0[12]∧x1[11] →^* x1[12])

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

(12) -> (11), if (x0[12] - 1 →^* x0[11]∧x0[12] - 1 →^* x1[11])

The set Q consists of the following terms:
123_0_descend_Load(x0)
227_0_descend_LE(x0)
Cond_227_0_descend_LE(TRUE, x0)
250_1_descend_InvokeMethod(233_0_descend_Return, x0)
121_1_rec_InvokeMethod(233_0_descend_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@550571f6 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 99_0_REC_GE(x0, x1) → COND_99_0_REC_GE(<(x1, 100), x0, x1) the following chains were created:

• We consider the chain 99_0_REC_GE(x0[0], x1[0]) → COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0]), COND_99_0_REC_GE(TRUE, x0[1], x1[1]) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1]) which results in the following constraint:
  

  (1)    (<(x1[0], 100)=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1] ⇒ 99_0_REC_GE(x0[0], x1[0])≥NonInfC∧99_0_REC_GE(x0[0], x1[0])≥COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])∧(U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥))

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

  (2)    (<(x1[0], 100)=TRUE ⇒ 99_0_REC_GE(x0[0], x1[0])≥NonInfC∧99_0_REC_GE(x0[0], x1[0])≥COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])∧(U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥))

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

  (3)    ([99] + [-1]x1[0] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_39 + (-1)Bound*bni_39] + [bni_39]x0[0] ≥ 0∧[(-1)bso_40] ≥ 0)

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

  (4)    ([99] + [-1]x1[0] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_39 + (-1)Bound*bni_39] + [bni_39]x0[0] ≥ 0∧[(-1)bso_40] ≥ 0)

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

  (5)    ([99] + [-1]x1[0] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_39 + (-1)Bound*bni_39] + [bni_39]x0[0] ≥ 0∧[(-1)bso_40] ≥ 0)

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

  (6)    ([99] + [-1]x1[0] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[bni_39] = 0∧[(-1)bni_39 + (-1)Bound*bni_39] ≥ 0∧0 = 0∧[(-1)bso_40] ≥ 0)

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

  (7)    ([99] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[bni_39] = 0∧[(-1)bni_39 + (-1)Bound*bni_39] ≥ 0∧0 = 0∧[(-1)bso_40] ≥ 0)

  
  

  (8)    ([99] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[bni_39] = 0∧[(-1)bni_39 + (-1)Bound*bni_39] ≥ 0∧0 = 0∧[(-1)bso_40] ≥ 0)

  
  
  

For Pair COND_99_0_REC_GE(TRUE, x0, x1) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1), x0, x1) the following chains were created:

• We consider the chain COND_99_0_REC_GE(TRUE, x0[1], x1[1]) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1]) which results in the following constraint:
  

  (9)    (COND_99_0_REC_GE(TRUE, x0[1], x1[1])≥NonInfC∧COND_99_0_REC_GE(TRUE, x0[1], x1[1])≥123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])∧(U^Increasing(123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])), ≥))

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

  (10)    ((U^Increasing(123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_41] = 0∧[(-1)bso_42] ≥ 0)

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

  (11)    ((U^Increasing(123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_41] = 0∧[(-1)bso_42] ≥ 0)

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

  (12)    ((U^Increasing(123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_41] = 0∧[(-1)bso_42] ≥ 0)

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

  (13)    ((U^Increasing(123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_41] = 0∧0 = 0∧0 = 0∧[(-1)bso_42] ≥ 0)

  
  
  

For Pair 123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0, x1) → 295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1), x0, x1) the following chains were created:

• We consider the chain 123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2]) → 295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2]) which results in the following constraint:
  

  (14)    (123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2])≥NonInfC∧123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2])≥295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])∧(U^Increasing(295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])), ≥))

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

  (15)    ((U^Increasing(295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])), ≥)∧[bni_43] = 0∧[(-1)bso_44] ≥ 0)

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

  (16)    ((U^Increasing(295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])), ≥)∧[bni_43] = 0∧[(-1)bso_44] ≥ 0)

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

  (17)    ((U^Increasing(295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])), ≥)∧[bni_43] = 0∧[(-1)bso_44] ≥ 0)

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

  (18)    ((U^Increasing(295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])), ≥)∧[bni_43] = 0∧0 = 0∧0 = 0∧[(-1)bso_44] ≥ 0)

  
  
  

For Pair 295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0, x1) → 324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1), x0, x1) the following chains were created:

• We consider the chain 295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3]) → 324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3]) which results in the following constraint:
  

  (19)    (295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3])≥NonInfC∧295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3])≥324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])∧(U^Increasing(324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])), ≥))

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

  (20)    ((U^Increasing(324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])), ≥)∧[bni_45] = 0∧[(-1)bso_46] ≥ 0)

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

  (21)    ((U^Increasing(324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])), ≥)∧[bni_45] = 0∧[(-1)bso_46] ≥ 0)

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

  (22)    ((U^Increasing(324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])), ≥)∧[bni_45] = 0∧[(-1)bso_46] ≥ 0)

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

  (23)    ((U^Increasing(324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])), ≥)∧[bni_45] = 0∧0 = 0∧0 = 0∧[(-1)bso_46] ≥ 0)

  
  
  

For Pair 324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0, x1) → 341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1), x0, x1) the following chains were created:

• We consider the chain 324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4]) → 341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4]) which results in the following constraint:
  

  (24)    (324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4])≥NonInfC∧324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4])≥341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])∧(U^Increasing(341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])), ≥))

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

  (25)    ((U^Increasing(341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])), ≥)∧[bni_47] = 0∧[(-1)bso_48] ≥ 0)

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

  (26)    ((U^Increasing(341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])), ≥)∧[bni_47] = 0∧[(-1)bso_48] ≥ 0)

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

  (27)    ((U^Increasing(341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])), ≥)∧[bni_47] = 0∧[(-1)bso_48] ≥ 0)

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

  (28)    ((U^Increasing(341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])), ≥)∧[bni_47] = 0∧0 = 0∧0 = 0∧[(-1)bso_48] ≥ 0)

  
  
  

For Pair 341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0, x1) → 358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1), x0, x1) the following chains were created:

• We consider the chain 341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5]) → 358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5]) which results in the following constraint:
  

  (29)    (341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5])≥NonInfC∧341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5])≥358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])∧(U^Increasing(358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])), ≥))

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

  (30)    ((U^Increasing(358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])), ≥)∧[bni_49] = 0∧[(-1)bso_50] ≥ 0)

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

  (31)    ((U^Increasing(358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])), ≥)∧[bni_49] = 0∧[(-1)bso_50] ≥ 0)

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

  (32)    ((U^Increasing(358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])), ≥)∧[bni_49] = 0∧[(-1)bso_50] ≥ 0)

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

  (33)    ((U^Increasing(358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])), ≥)∧[bni_49] = 0∧0 = 0∧0 = 0∧[(-1)bso_50] ≥ 0)

  
  
  

For Pair 358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0, x1) → 375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1), x0, x1) the following chains were created:

• We consider the chain 358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6]) → 375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6]) which results in the following constraint:
  

  (34)    (358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6])≥NonInfC∧358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6])≥375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])∧(U^Increasing(375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])), ≥))

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

  (35)    ((U^Increasing(375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])), ≥)∧[bni_51] = 0∧[(-1)bso_52] ≥ 0)

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

  (36)    ((U^Increasing(375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])), ≥)∧[bni_51] = 0∧[(-1)bso_52] ≥ 0)

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

  (37)    ((U^Increasing(375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])), ≥)∧[bni_51] = 0∧[(-1)bso_52] ≥ 0)

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

  (38)    ((U^Increasing(375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])), ≥)∧[bni_51] = 0∧0 = 0∧0 = 0∧[(-1)bso_52] ≥ 0)

  
  
  

For Pair 375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0, x1) → 395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1), x0, x1) the following chains were created:

• We consider the chain 375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7]) → 395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7]) which results in the following constraint:
  

  (39)    (375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7])≥NonInfC∧375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7])≥395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])∧(U^Increasing(395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])), ≥))

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

  (40)    ((U^Increasing(395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])), ≥)∧[bni_53] = 0∧[(-1)bso_54] ≥ 0)

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

  (41)    ((U^Increasing(395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])), ≥)∧[bni_53] = 0∧[(-1)bso_54] ≥ 0)

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

  (42)    ((U^Increasing(395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])), ≥)∧[bni_53] = 0∧[(-1)bso_54] ≥ 0)

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

  (43)    ((U^Increasing(395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])), ≥)∧[bni_53] = 0∧0 = 0∧0 = 0∧[(-1)bso_54] ≥ 0)

  
  
  

For Pair 395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0, x1) → 410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1), x0, x1) the following chains were created:

• We consider the chain 395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8]) → 410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8]) which results in the following constraint:
  

  (44)    (395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8])≥NonInfC∧395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8])≥410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])∧(U^Increasing(410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])), ≥))

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

  (45)    ((U^Increasing(410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])), ≥)∧[bni_55] = 0∧[(-1)bso_56] ≥ 0)

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

  (46)    ((U^Increasing(410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])), ≥)∧[bni_55] = 0∧[(-1)bso_56] ≥ 0)

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

  (47)    ((U^Increasing(410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])), ≥)∧[bni_55] = 0∧[(-1)bso_56] ≥ 0)

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

  (48)    ((U^Increasing(410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])), ≥)∧[bni_55] = 0∧0 = 0∧0 = 0∧[(-1)bso_56] ≥ 0)

  
  
  

For Pair 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0, x1) → COND_410_1_TEST_INVOKEMETHOD(>(x1, 0), 233_0_descend_Return, x0, x1) the following chains were created:

• We consider the chain 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9]) → COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9]), COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10]) → 99_0_REC_GE(x0[10], +(x1[10], 1)) which results in the following constraint:
  

  (49)    (>(x1[9], 0)=TRUE∧x0[9]=x0[10]∧x1[9]=x1[10] ⇒ 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9])≥NonInfC∧410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9])≥COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])∧(U^Increasing(COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])), ≥))

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

  (50)    (>(x1[9], 0)=TRUE ⇒ 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9])≥NonInfC∧410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9])≥COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])∧(U^Increasing(COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])), ≥))

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

  (51)    (x1[9] + [-1] ≥ 0 ⇒ (U^Increasing(COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])), ≥)∧[(-1)bni_57 + (-1)Bound*bni_57] + [bni_57]x0[9] ≥ 0∧[(-1)bso_58] ≥ 0)

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

  (52)    (x1[9] + [-1] ≥ 0 ⇒ (U^Increasing(COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])), ≥)∧[(-1)bni_57 + (-1)Bound*bni_57] + [bni_57]x0[9] ≥ 0∧[(-1)bso_58] ≥ 0)

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

  (53)    (x1[9] + [-1] ≥ 0 ⇒ (U^Increasing(COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])), ≥)∧[(-1)bni_57 + (-1)Bound*bni_57] + [bni_57]x0[9] ≥ 0∧[(-1)bso_58] ≥ 0)

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

  (54)    (x1[9] + [-1] ≥ 0 ⇒ (U^Increasing(COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])), ≥)∧[bni_57] = 0∧[(-1)bni_57 + (-1)Bound*bni_57] ≥ 0∧0 = 0∧[(-1)bso_58] ≥ 0)

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

  (55)    (x1[9] ≥ 0 ⇒ (U^Increasing(COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])), ≥)∧[bni_57] = 0∧[(-1)bni_57 + (-1)Bound*bni_57] ≥ 0∧0 = 0∧[(-1)bso_58] ≥ 0)

  
  
  

For Pair COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0, x1) → 99_0_REC_GE(x0, +(x1, 1)) the following chains were created:

• We consider the chain COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10]) → 99_0_REC_GE(x0[10], +(x1[10], 1)) which results in the following constraint:
  

  (56)    (COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10])≥NonInfC∧COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10])≥99_0_REC_GE(x0[10], +(x1[10], 1))∧(U^Increasing(99_0_REC_GE(x0[10], +(x1[10], 1))), ≥))

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

  (57)    ((U^Increasing(99_0_REC_GE(x0[10], +(x1[10], 1))), ≥)∧[bni_59] = 0∧[(-1)bso_60] ≥ 0)

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

  (58)    ((U^Increasing(99_0_REC_GE(x0[10], +(x1[10], 1))), ≥)∧[bni_59] = 0∧[(-1)bso_60] ≥ 0)

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

  (59)    ((U^Increasing(99_0_REC_GE(x0[10], +(x1[10], 1))), ≥)∧[bni_59] = 0∧[(-1)bso_60] ≥ 0)

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

  (60)    ((U^Increasing(99_0_REC_GE(x0[10], +(x1[10], 1))), ≥)∧[bni_59] = 0∧0 = 0∧0 = 0∧[(-1)bso_60] ≥ 0)

  
  
  

For Pair 99_0_REC_GE(x0, x1) → COND_99_0_REC_GE1(&&(>(x1, 99), >(x0, 1)), x0, x1) the following chains were created:

• We consider the chain 99_0_REC_GE(x0[11], x1[11]) → COND_99_0_REC_GE1(&&(>(x1[11], 99), >(x0[11], 1)), x0[11], x1[11]), COND_99_0_REC_GE1(TRUE, x0[12], x1[12]) → 99_0_REC_GE(-(x0[12], 1), -(x0[12], 1)) which results in the following constraint:
  

  (61)    (&&(>(x1[11], 99), >(x0[11], 1))=TRUE∧x0[11]=x0[12]∧x1[11]=x1[12] ⇒ 99_0_REC_GE(x0[11], x1[11])≥NonInfC∧99_0_REC_GE(x0[11], x1[11])≥COND_99_0_REC_GE1(&&(>(x1[11], 99), >(x0[11], 1)), x0[11], x1[11])∧(U^Increasing(COND_99_0_REC_GE1(&&(>(x1[11], 99), >(x0[11], 1)), x0[11], x1[11])), ≥))

  
  
  We simplified constraint (61) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (62)    (>(x1[11], 99)=TRUE∧>(x0[11], 1)=TRUE ⇒ 99_0_REC_GE(x0[11], x1[11])≥NonInfC∧99_0_REC_GE(x0[11], x1[11])≥COND_99_0_REC_GE1(&&(>(x1[11], 99), >(x0[11], 1)), x0[11], x1[11])∧(U^Increasing(COND_99_0_REC_GE1(&&(>(x1[11], 99), >(x0[11], 1)), x0[11], x1[11])), ≥))

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

  (63)    (x1[11] + [-100] ≥ 0∧x0[11] + [-2] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE1(&&(>(x1[11], 99), >(x0[11], 1)), x0[11], x1[11])), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [bni_61]x0[11] ≥ 0∧[(-1)bso_62] ≥ 0)

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

  (64)    (x1[11] + [-100] ≥ 0∧x0[11] + [-2] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE1(&&(>(x1[11], 99), >(x0[11], 1)), x0[11], x1[11])), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [bni_61]x0[11] ≥ 0∧[(-1)bso_62] ≥ 0)

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

  (65)    (x1[11] + [-100] ≥ 0∧x0[11] + [-2] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE1(&&(>(x1[11], 99), >(x0[11], 1)), x0[11], x1[11])), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [bni_61]x0[11] ≥ 0∧[(-1)bso_62] ≥ 0)

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

  (66)    (x1[11] ≥ 0∧x0[11] + [-2] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE1(&&(>(x1[11], 99), >(x0[11], 1)), x0[11], x1[11])), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [bni_61]x0[11] ≥ 0∧[(-1)bso_62] ≥ 0)

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

  (67)    (x1[11] ≥ 0∧x0[11] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE1(&&(>(x1[11], 99), >(x0[11], 1)), x0[11], x1[11])), ≥)∧[bni_61 + (-1)Bound*bni_61] + [bni_61]x0[11] ≥ 0∧[(-1)bso_62] ≥ 0)

  
  
  

For Pair COND_99_0_REC_GE1(TRUE, x0, x1) → 99_0_REC_GE(-(x0, 1), -(x0, 1)) the following chains were created:

• We consider the chain COND_99_0_REC_GE1(TRUE, x0[12], x1[12]) → 99_0_REC_GE(-(x0[12], 1), -(x0[12], 1)) which results in the following constraint:
  

  (68)    (COND_99_0_REC_GE1(TRUE, x0[12], x1[12])≥NonInfC∧COND_99_0_REC_GE1(TRUE, x0[12], x1[12])≥99_0_REC_GE(-(x0[12], 1), -(x0[12], 1))∧(U^Increasing(99_0_REC_GE(-(x0[12], 1), -(x0[12], 1))), ≥))

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

  (69)    ((U^Increasing(99_0_REC_GE(-(x0[12], 1), -(x0[12], 1))), ≥)∧[bni_63] = 0∧[1 + (-1)bso_64] ≥ 0)

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

  (70)    ((U^Increasing(99_0_REC_GE(-(x0[12], 1), -(x0[12], 1))), ≥)∧[bni_63] = 0∧[1 + (-1)bso_64] ≥ 0)

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

  (71)    ((U^Increasing(99_0_REC_GE(-(x0[12], 1), -(x0[12], 1))), ≥)∧[bni_63] = 0∧[1 + (-1)bso_64] ≥ 0)

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

  (72)    ((U^Increasing(99_0_REC_GE(-(x0[12], 1), -(x0[12], 1))), ≥)∧[bni_63] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_64] ≥ 0)

  
  
  

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

• 99_0_REC_GE(x0, x1) → COND_99_0_REC_GE(<(x1, 100), x0, x1)
  
  • ([99] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[bni_39] = 0∧[(-1)bni_39 + (-1)Bound*bni_39] ≥ 0∧0 = 0∧[(-1)bso_40] ≥ 0)
    
  • ([99] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[bni_39] = 0∧[(-1)bni_39 + (-1)Bound*bni_39] ≥ 0∧0 = 0∧[(-1)bso_40] ≥ 0)
    
  
  
• COND_99_0_REC_GE(TRUE, x0, x1) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1), x0, x1)
  
  • ((U^Increasing(123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_41] = 0∧0 = 0∧0 = 0∧[(-1)bso_42] ≥ 0)
    
  
  
• 123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0, x1) → 295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1), x0, x1)
  
  • ((U^Increasing(295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])), ≥)∧[bni_43] = 0∧0 = 0∧0 = 0∧[(-1)bso_44] ≥ 0)
    
  
  
• 295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0, x1) → 324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1), x0, x1)
  
  • ((U^Increasing(324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])), ≥)∧[bni_45] = 0∧0 = 0∧0 = 0∧[(-1)bso_46] ≥ 0)
    
  
  
• 324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0, x1) → 341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1), x0, x1)
  
  • ((U^Increasing(341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])), ≥)∧[bni_47] = 0∧0 = 0∧0 = 0∧[(-1)bso_48] ≥ 0)
    
  
  
• 341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0, x1) → 358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1), x0, x1)
  
  • ((U^Increasing(358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])), ≥)∧[bni_49] = 0∧0 = 0∧0 = 0∧[(-1)bso_50] ≥ 0)
    
  
  
• 358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0, x1) → 375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1), x0, x1)
  
  • ((U^Increasing(375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])), ≥)∧[bni_51] = 0∧0 = 0∧0 = 0∧[(-1)bso_52] ≥ 0)
    
  
  
• 375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0, x1) → 395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1), x0, x1)
  
  • ((U^Increasing(395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])), ≥)∧[bni_53] = 0∧0 = 0∧0 = 0∧[(-1)bso_54] ≥ 0)
    
  
  
• 395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0, x1) → 410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1), x0, x1)
  
  • ((U^Increasing(410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])), ≥)∧[bni_55] = 0∧0 = 0∧0 = 0∧[(-1)bso_56] ≥ 0)
    
  
  
• 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0, x1) → COND_410_1_TEST_INVOKEMETHOD(>(x1, 0), 233_0_descend_Return, x0, x1)
  
  • (x1[9] ≥ 0 ⇒ (U^Increasing(COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])), ≥)∧[bni_57] = 0∧[(-1)bni_57 + (-1)Bound*bni_57] ≥ 0∧0 = 0∧[(-1)bso_58] ≥ 0)
    
  
  
• COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0, x1) → 99_0_REC_GE(x0, +(x1, 1))
  
  • ((U^Increasing(99_0_REC_GE(x0[10], +(x1[10], 1))), ≥)∧[bni_59] = 0∧0 = 0∧0 = 0∧[(-1)bso_60] ≥ 0)
    
  
  
• 99_0_REC_GE(x0, x1) → COND_99_0_REC_GE1(&&(>(x1, 99), >(x0, 1)), x0, x1)
  
  • (x1[11] ≥ 0∧x0[11] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE1(&&(>(x1[11], 99), >(x0[11], 1)), x0[11], x1[11])), ≥)∧[bni_61 + (-1)Bound*bni_61] + [bni_61]x0[11] ≥ 0∧[(-1)bso_62] ≥ 0)
    
  
  
• COND_99_0_REC_GE1(TRUE, x0, x1) → 99_0_REC_GE(-(x0, 1), -(x0, 1))
  
  • ((U^Increasing(99_0_REC_GE(-(x0[12], 1), -(x0[12], 1))), ≥)∧[bni_63] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_64] ≥ 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(123_0_descend_Load(x₁)) = [-1] + [-1]x₁   
POL(227_0_descend_LE(x₁)) = [-1] + x₁   
POL(0) = 0   
POL(233_0_descend_Return) = [-1]   
POL(Cond_227_0_descend_LE(x₁, x₂)) = x₂   
POL(>(x₁, x₂)) = [-1]   
POL(250_1_descend_InvokeMethod(x₁, x₂)) = [-1] + [2]x₂ + x₁   
POL(-(x₁, x₂)) = x₁ + [-1]x₂   
POL(1) = [1]   
POL(121_1_rec_InvokeMethod(x₁, x₂)) = [-1]   
POL(99_0_REC_GE(x₁, x₂)) = [-1] + x₁   
POL(COND_99_0_REC_GE(x₁, x₂, x₃)) = [-1] + x₂   
POL(<(x₁, x₂)) = [-1]   
POL(100) = [100]   
POL(123_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + x₂   
POL(295_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + x₂   
POL(324_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + x₂   
POL(341_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + x₂   
POL(358_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + x₂   
POL(375_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + x₂   
POL(395_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + x₂   
POL(410_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + x₂   
POL(COND_410_1_TEST_INVOKEMETHOD(x₁, x₂, x₃, x₄)) = [-1] + x₃   
POL(+(x₁, x₂)) = x₁ + x₂   
POL(COND_99_0_REC_GE1(x₁, x₂, x₃)) = [-1] + x₂   
POL(&&(x₁, x₂)) = [-1]   
POL(99) = [99]   

The following pairs are in P_>:

COND_99_0_REC_GE1(TRUE, x0[12], x1[12]) → 99_0_REC_GE(-(x0[12], 1), -(x0[12], 1))

The following pairs are in P_bound:

99_0_REC_GE(x0[11], x1[11]) → COND_99_0_REC_GE1(&&(>(x1[11], 99), >(x0[11], 1)), x0[11], x1[11])

The following pairs are in P_≥:

99_0_REC_GE(x0[0], x1[0]) → COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])
COND_99_0_REC_GE(TRUE, x0[1], x1[1]) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])
123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2]) → 295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])
295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3]) → 324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])
324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4]) → 341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])
341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5]) → 358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])
358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6]) → 375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])
375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7]) → 395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])
395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8]) → 410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])
410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9]) → COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])
COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10]) → 99_0_REC_GE(x0[10], +(x1[10], 1))
99_0_REC_GE(x0[11], x1[11]) → COND_99_0_REC_GE1(&&(>(x1[11], 99), >(x0[11], 1)), x0[11], x1[11])

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

227_0_descend_LE(0)¹ → 233_0_descend_Return¹
Cond_227_0_descend_LE(>(x0, 0), x0)¹ → 227_0_descend_LE(x0)¹

(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, Boolean

The ITRS R consists of the following rules:
123_0_descend_Load(x0) → 227_0_descend_LE(x0)
227_0_descend_LE(0) → 233_0_descend_Return
227_0_descend_LE(x0) → Cond_227_0_descend_LE(x0 > 0, x0)
Cond_227_0_descend_LE(TRUE, x0) → 250_1_descend_InvokeMethod(227_0_descend_LE(x0 - 1), x0 - 1)
250_1_descend_InvokeMethod(233_0_descend_Return, 0) → 233_0_descend_Return
250_1_descend_InvokeMethod(233_0_descend_Return, x0) → 233_0_descend_Return
121_1_rec_InvokeMethod(233_0_descend_Return, 0) → 233_0_descend_Return
121_1_rec_InvokeMethod(233_0_descend_Return, x0) → 233_0_descend_Return

The integer pair graph contains the following rules and edges:
(0): 99_0_REC_GE(x0[0], x1[0]) → COND_99_0_REC_GE(x1[0] < 100, x0[0], x1[0])
(1): COND_99_0_REC_GE(TRUE, x0[1], x1[1]) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])
(2): 123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2]) → 295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])
(3): 295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3]) → 324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])
(4): 324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4]) → 341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])
(5): 341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5]) → 358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])
(6): 358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6]) → 375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])
(7): 375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7]) → 395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])
(8): 395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8]) → 410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])
(9): 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9]) → COND_410_1_TEST_INVOKEMETHOD(x1[9] > 0, 233_0_descend_Return, x0[9], x1[9])
(10): COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10]) → 99_0_REC_GE(x0[10], x1[10] + 1)
(11): 99_0_REC_GE(x0[11], x1[11]) → COND_99_0_REC_GE1(x1[11] > 99 && x0[11] > 1, x0[11], x1[11])

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

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

(1) -> (2), if (123_0_descend_Load(x1[1]) →^* 233_0_descend_Return∧x0[1] →^* x0[2]∧x1[1] →^* x1[2])

(2) -> (3), if (123_0_descend_Load(x1[2]) →^* 233_0_descend_Return∧x0[2] →^* x0[3]∧x1[2] →^* x1[3])

(3) -> (4), if (123_0_descend_Load(x1[3]) →^* 233_0_descend_Return∧x0[3] →^* x0[4]∧x1[3] →^* x1[4])

(4) -> (5), if (123_0_descend_Load(x1[4]) →^* 233_0_descend_Return∧x0[4] →^* x0[5]∧x1[4] →^* x1[5])

(5) -> (6), if (123_0_descend_Load(x1[5]) →^* 233_0_descend_Return∧x0[5] →^* x0[6]∧x1[5] →^* x1[6])

(6) -> (7), if (123_0_descend_Load(x1[6]) →^* 233_0_descend_Return∧x0[6] →^* x0[7]∧x1[6] →^* x1[7])

(7) -> (8), if (123_0_descend_Load(x1[7]) →^* 233_0_descend_Return∧x0[7] →^* x0[8]∧x1[7] →^* x1[8])

(8) -> (9), if (123_0_descend_Load(x1[8]) →^* 233_0_descend_Return∧x0[8] →^* x0[9]∧x1[8] →^* x1[9])

(9) -> (10), if (x1[9] > 0 ∧x0[9] →^* x0[10]∧x1[9] →^* x1[10])

(10) -> (11), if (x0[10] →^* x0[11]∧x1[10] + 1 →^* x1[11])

The set Q consists of the following terms:
123_0_descend_Load(x0)
227_0_descend_LE(x0)
Cond_227_0_descend_LE(TRUE, x0)
250_1_descend_InvokeMethod(233_0_descend_Return, x0)
121_1_rec_InvokeMethod(233_0_descend_Return, x0)

(22) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(23) 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:
123_0_descend_Load(x0) → 227_0_descend_LE(x0)
227_0_descend_LE(0) → 233_0_descend_Return
227_0_descend_LE(x0) → Cond_227_0_descend_LE(x0 > 0, x0)
Cond_227_0_descend_LE(TRUE, x0) → 250_1_descend_InvokeMethod(227_0_descend_LE(x0 - 1), x0 - 1)
250_1_descend_InvokeMethod(233_0_descend_Return, 0) → 233_0_descend_Return
250_1_descend_InvokeMethod(233_0_descend_Return, x0) → 233_0_descend_Return
121_1_rec_InvokeMethod(233_0_descend_Return, 0) → 233_0_descend_Return
121_1_rec_InvokeMethod(233_0_descend_Return, x0) → 233_0_descend_Return

The integer pair graph contains the following rules and edges:
(10): COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10]) → 99_0_REC_GE(x0[10], x1[10] + 1)
(9): 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9]) → COND_410_1_TEST_INVOKEMETHOD(x1[9] > 0, 233_0_descend_Return, x0[9], x1[9])
(8): 395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8]) → 410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])
(7): 375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7]) → 395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])
(6): 358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6]) → 375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])
(5): 341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5]) → 358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])
(4): 324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4]) → 341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])
(3): 295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3]) → 324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])
(2): 123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2]) → 295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])
(1): COND_99_0_REC_GE(TRUE, x0[1], x1[1]) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])
(0): 99_0_REC_GE(x0[0], x1[0]) → COND_99_0_REC_GE(x1[0] < 100, x0[0], x1[0])

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

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

(1) -> (2), if (123_0_descend_Load(x1[1]) →^* 233_0_descend_Return∧x0[1] →^* x0[2]∧x1[1] →^* x1[2])

(2) -> (3), if (123_0_descend_Load(x1[2]) →^* 233_0_descend_Return∧x0[2] →^* x0[3]∧x1[2] →^* x1[3])

(3) -> (4), if (123_0_descend_Load(x1[3]) →^* 233_0_descend_Return∧x0[3] →^* x0[4]∧x1[3] →^* x1[4])

(4) -> (5), if (123_0_descend_Load(x1[4]) →^* 233_0_descend_Return∧x0[4] →^* x0[5]∧x1[4] →^* x1[5])

(5) -> (6), if (123_0_descend_Load(x1[5]) →^* 233_0_descend_Return∧x0[5] →^* x0[6]∧x1[5] →^* x1[6])

(6) -> (7), if (123_0_descend_Load(x1[6]) →^* 233_0_descend_Return∧x0[6] →^* x0[7]∧x1[6] →^* x1[7])

(7) -> (8), if (123_0_descend_Load(x1[7]) →^* 233_0_descend_Return∧x0[7] →^* x0[8]∧x1[7] →^* x1[8])

(8) -> (9), if (123_0_descend_Load(x1[8]) →^* 233_0_descend_Return∧x0[8] →^* x0[9]∧x1[8] →^* x1[9])

(9) -> (10), if (x1[9] > 0 ∧x0[9] →^* x0[10]∧x1[9] →^* x1[10])

The set Q consists of the following terms:
123_0_descend_Load(x0)
227_0_descend_LE(x0)
Cond_227_0_descend_LE(TRUE, x0)
250_1_descend_InvokeMethod(233_0_descend_Return, x0)
121_1_rec_InvokeMethod(233_0_descend_Return, x0)

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

(25) 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:
123_0_descend_Load(x0) → 227_0_descend_LE(x0)
227_0_descend_LE(0) → 233_0_descend_Return
227_0_descend_LE(x0) → Cond_227_0_descend_LE(x0 > 0, x0)
Cond_227_0_descend_LE(TRUE, x0) → 250_1_descend_InvokeMethod(227_0_descend_LE(x0 - 1), x0 - 1)
250_1_descend_InvokeMethod(233_0_descend_Return, 0) → 233_0_descend_Return
250_1_descend_InvokeMethod(233_0_descend_Return, x0) → 233_0_descend_Return

The integer pair graph contains the following rules and edges:
(10): COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10]) → 99_0_REC_GE(x0[10], x1[10] + 1)
(9): 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9]) → COND_410_1_TEST_INVOKEMETHOD(x1[9] > 0, 233_0_descend_Return, x0[9], x1[9])
(8): 395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8]) → 410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])
(7): 375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7]) → 395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])
(6): 358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6]) → 375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])
(5): 341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5]) → 358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])
(4): 324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4]) → 341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])
(3): 295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3]) → 324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])
(2): 123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2]) → 295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])
(1): COND_99_0_REC_GE(TRUE, x0[1], x1[1]) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])
(0): 99_0_REC_GE(x0[0], x1[0]) → COND_99_0_REC_GE(x1[0] < 100, x0[0], x1[0])

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

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

(1) -> (2), if (123_0_descend_Load(x1[1]) →^* 233_0_descend_Return∧x0[1] →^* x0[2]∧x1[1] →^* x1[2])

(2) -> (3), if (123_0_descend_Load(x1[2]) →^* 233_0_descend_Return∧x0[2] →^* x0[3]∧x1[2] →^* x1[3])

(3) -> (4), if (123_0_descend_Load(x1[3]) →^* 233_0_descend_Return∧x0[3] →^* x0[4]∧x1[3] →^* x1[4])

(4) -> (5), if (123_0_descend_Load(x1[4]) →^* 233_0_descend_Return∧x0[4] →^* x0[5]∧x1[4] →^* x1[5])

(5) -> (6), if (123_0_descend_Load(x1[5]) →^* 233_0_descend_Return∧x0[5] →^* x0[6]∧x1[5] →^* x1[6])

(6) -> (7), if (123_0_descend_Load(x1[6]) →^* 233_0_descend_Return∧x0[6] →^* x0[7]∧x1[6] →^* x1[7])

(7) -> (8), if (123_0_descend_Load(x1[7]) →^* 233_0_descend_Return∧x0[7] →^* x0[8]∧x1[7] →^* x1[8])

(8) -> (9), if (123_0_descend_Load(x1[8]) →^* 233_0_descend_Return∧x0[8] →^* x0[9]∧x1[8] →^* x1[9])

(9) -> (10), if (x1[9] > 0 ∧x0[9] →^* x0[10]∧x1[9] →^* x1[10])

The set Q consists of the following terms:
123_0_descend_Load(x0)
227_0_descend_LE(x0)
Cond_227_0_descend_LE(TRUE, x0)
250_1_descend_InvokeMethod(233_0_descend_Return, x0)
121_1_rec_InvokeMethod(233_0_descend_Return, x0)

(26) 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@550571f6 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 COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10]) → 99_0_REC_GE(x0[10], +(x1[10], 1)) the following chains were created:

• We consider the chain COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10]) → 99_0_REC_GE(x0[10], +(x1[10], 1)) which results in the following constraint:
  

  (1)    (COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10])≥NonInfC∧COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10])≥99_0_REC_GE(x0[10], +(x1[10], 1))∧(U^Increasing(99_0_REC_GE(x0[10], +(x1[10], 1))), ≥))

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

  (2)    ((U^Increasing(99_0_REC_GE(x0[10], +(x1[10], 1))), ≥)∧[bni_21] = 0∧[1 + (-1)bso_22] ≥ 0)

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

  (3)    ((U^Increasing(99_0_REC_GE(x0[10], +(x1[10], 1))), ≥)∧[bni_21] = 0∧[1 + (-1)bso_22] ≥ 0)

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

  (4)    ((U^Increasing(99_0_REC_GE(x0[10], +(x1[10], 1))), ≥)∧[bni_21] = 0∧[1 + (-1)bso_22] ≥ 0)

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

  (5)    ((U^Increasing(99_0_REC_GE(x0[10], +(x1[10], 1))), ≥)∧[bni_21] = 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)

  
  
  

For Pair 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9]) → COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9]) the following chains were created:

• We consider the chain 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9]) → COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9]), COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10]) → 99_0_REC_GE(x0[10], +(x1[10], 1)) which results in the following constraint:
  

  (6)    (>(x1[9], 0)=TRUE∧x0[9]=x0[10]∧x1[9]=x1[10] ⇒ 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9])≥NonInfC∧410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9])≥COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])∧(U^Increasing(COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])), ≥))

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

  (7)    (>(x1[9], 0)=TRUE ⇒ 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9])≥NonInfC∧410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9])≥COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])∧(U^Increasing(COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])), ≥))

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

  (8)    (x1[9] + [-1] ≥ 0 ⇒ (U^Increasing(COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [(-1)bni_23]x1[9] ≥ 0∧[(-1)bso_24] ≥ 0)

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

  (9)    (x1[9] + [-1] ≥ 0 ⇒ (U^Increasing(COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [(-1)bni_23]x1[9] ≥ 0∧[(-1)bso_24] ≥ 0)

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

  (10)    (x1[9] + [-1] ≥ 0 ⇒ (U^Increasing(COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [(-1)bni_23]x1[9] ≥ 0∧[(-1)bso_24] ≥ 0)

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

  (11)    (x1[9] ≥ 0 ⇒ (U^Increasing(COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])), ≥)∧[(-2)bni_23 + (-1)Bound*bni_23] + [(-1)bni_23]x1[9] ≥ 0∧[(-1)bso_24] ≥ 0)

  
  
  

For Pair 395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8]) → 410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8]) the following chains were created:

• We consider the chain 395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8]) → 410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8]) which results in the following constraint:
  

  (12)    (395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8])≥NonInfC∧395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8])≥410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])∧(U^Increasing(410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])), ≥))

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

  (13)    ((U^Increasing(410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])), ≥)∧[bni_25] = 0∧[(-1)bso_26] ≥ 0)

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

  (14)    ((U^Increasing(410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])), ≥)∧[bni_25] = 0∧[(-1)bso_26] ≥ 0)

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

  (15)    ((U^Increasing(410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])), ≥)∧[bni_25] = 0∧[(-1)bso_26] ≥ 0)

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

  (16)    ((U^Increasing(410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])), ≥)∧[bni_25] = 0∧0 = 0∧[(-1)bso_26] ≥ 0)

  
  
  

For Pair 375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7]) → 395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7]) the following chains were created:

• We consider the chain 375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7]) → 395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7]) which results in the following constraint:
  

  (17)    (375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7])≥NonInfC∧375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7])≥395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])∧(U^Increasing(395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])), ≥))

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

  (18)    ((U^Increasing(395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])), ≥)∧[bni_27] = 0∧[(-1)bso_28] ≥ 0)

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

  (19)    ((U^Increasing(395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])), ≥)∧[bni_27] = 0∧[(-1)bso_28] ≥ 0)

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

  (20)    ((U^Increasing(395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])), ≥)∧[bni_27] = 0∧[(-1)bso_28] ≥ 0)

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

  (21)    ((U^Increasing(395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])), ≥)∧[bni_27] = 0∧0 = 0∧[(-1)bso_28] ≥ 0)

  
  
  

For Pair 358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6]) → 375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6]) the following chains were created:

• We consider the chain 358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6]) → 375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6]) which results in the following constraint:
  

  (22)    (358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6])≥NonInfC∧358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6])≥375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])∧(U^Increasing(375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])), ≥))

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

  (23)    ((U^Increasing(375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])), ≥)∧[bni_29] = 0∧[(-1)bso_30] ≥ 0)

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

  (24)    ((U^Increasing(375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])), ≥)∧[bni_29] = 0∧[(-1)bso_30] ≥ 0)

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

  (25)    ((U^Increasing(375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])), ≥)∧[bni_29] = 0∧[(-1)bso_30] ≥ 0)

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

  (26)    ((U^Increasing(375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])), ≥)∧[bni_29] = 0∧0 = 0∧[(-1)bso_30] ≥ 0)

  
  
  

For Pair 341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5]) → 358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5]) the following chains were created:

• We consider the chain 341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5]) → 358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5]) which results in the following constraint:
  

  (27)    (341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5])≥NonInfC∧341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5])≥358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])∧(U^Increasing(358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])), ≥))

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

  (28)    ((U^Increasing(358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])), ≥)∧[bni_31] = 0∧[(-1)bso_32] ≥ 0)

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

  (29)    ((U^Increasing(358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])), ≥)∧[bni_31] = 0∧[(-1)bso_32] ≥ 0)

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

  (30)    ((U^Increasing(358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])), ≥)∧[bni_31] = 0∧[(-1)bso_32] ≥ 0)

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

  (31)    ((U^Increasing(358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])), ≥)∧[bni_31] = 0∧0 = 0∧[(-1)bso_32] ≥ 0)

  
  
  

For Pair 324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4]) → 341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4]) the following chains were created:

• We consider the chain 324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4]) → 341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4]) which results in the following constraint:
  

  (32)    (324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4])≥NonInfC∧324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4])≥341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])∧(U^Increasing(341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])), ≥))

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

  (33)    ((U^Increasing(341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])), ≥)∧[bni_33] = 0∧[(-1)bso_34] ≥ 0)

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

  (34)    ((U^Increasing(341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])), ≥)∧[bni_33] = 0∧[(-1)bso_34] ≥ 0)

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

  (35)    ((U^Increasing(341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])), ≥)∧[bni_33] = 0∧[(-1)bso_34] ≥ 0)

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

  (36)    ((U^Increasing(341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])), ≥)∧[bni_33] = 0∧0 = 0∧[(-1)bso_34] ≥ 0)

  
  
  

For Pair 295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3]) → 324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3]) the following chains were created:

• We consider the chain 295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3]) → 324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3]) which results in the following constraint:
  

  (37)    (295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3])≥NonInfC∧295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3])≥324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])∧(U^Increasing(324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])), ≥))

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

  (38)    ((U^Increasing(324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])), ≥)∧[bni_35] = 0∧[(-1)bso_36] ≥ 0)

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

  (39)    ((U^Increasing(324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])), ≥)∧[bni_35] = 0∧[(-1)bso_36] ≥ 0)

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

  (40)    ((U^Increasing(324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])), ≥)∧[bni_35] = 0∧[(-1)bso_36] ≥ 0)

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

  (41)    ((U^Increasing(324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])), ≥)∧[bni_35] = 0∧0 = 0∧[(-1)bso_36] ≥ 0)

  
  
  

For Pair 123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2]) → 295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2]) the following chains were created:

• We consider the chain 123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2]) → 295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2]) which results in the following constraint:
  

  (42)    (123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2])≥NonInfC∧123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2])≥295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])∧(U^Increasing(295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])), ≥))

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

  (43)    ((U^Increasing(295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])), ≥)∧[bni_37] = 0∧[(-1)bso_38] ≥ 0)

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

  (44)    ((U^Increasing(295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])), ≥)∧[bni_37] = 0∧[(-1)bso_38] ≥ 0)

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

  (45)    ((U^Increasing(295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])), ≥)∧[bni_37] = 0∧[(-1)bso_38] ≥ 0)

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

  (46)    ((U^Increasing(295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])), ≥)∧[bni_37] = 0∧0 = 0∧[(-1)bso_38] ≥ 0)

  
  
  

For Pair COND_99_0_REC_GE(TRUE, x0[1], x1[1]) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1]) the following chains were created:

• We consider the chain COND_99_0_REC_GE(TRUE, x0[1], x1[1]) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1]) which results in the following constraint:
  

  (47)    (COND_99_0_REC_GE(TRUE, x0[1], x1[1])≥NonInfC∧COND_99_0_REC_GE(TRUE, x0[1], x1[1])≥123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])∧(U^Increasing(123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])), ≥))

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

  (48)    ((U^Increasing(123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_39] = 0∧[(-1)bso_40] ≥ 0)

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

  (49)    ((U^Increasing(123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_39] = 0∧[(-1)bso_40] ≥ 0)

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

  (50)    ((U^Increasing(123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_39] = 0∧[(-1)bso_40] ≥ 0)

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

  (51)    ((U^Increasing(123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_39] = 0∧0 = 0∧[(-1)bso_40] ≥ 0)

  
  
  

For Pair 99_0_REC_GE(x0[0], x1[0]) → COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0]) the following chains were created:

• We consider the chain 99_0_REC_GE(x0[0], x1[0]) → COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0]), COND_99_0_REC_GE(TRUE, x0[1], x1[1]) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1]) which results in the following constraint:
  

  (52)    (<(x1[0], 100)=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1] ⇒ 99_0_REC_GE(x0[0], x1[0])≥NonInfC∧99_0_REC_GE(x0[0], x1[0])≥COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])∧(U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥))

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

  (53)    (<(x1[0], 100)=TRUE ⇒ 99_0_REC_GE(x0[0], x1[0])≥NonInfC∧99_0_REC_GE(x0[0], x1[0])≥COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])∧(U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥))

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

  (54)    ([99] + [-1]x1[0] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [(-1)bni_41]x1[0] ≥ 0∧[(-1)bso_42] ≥ 0)

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

  (55)    ([99] + [-1]x1[0] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [(-1)bni_41]x1[0] ≥ 0∧[(-1)bso_42] ≥ 0)

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

  (56)    ([99] + [-1]x1[0] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [(-1)bni_41]x1[0] ≥ 0∧[(-1)bso_42] ≥ 0)

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

  (57)    ([99] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [bni_41]x1[0] ≥ 0∧[(-1)bso_42] ≥ 0)

  
  

  (58)    ([99] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [(-1)bni_41]x1[0] ≥ 0∧[(-1)bso_42] ≥ 0)

  
  
  

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

• COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10]) → 99_0_REC_GE(x0[10], +(x1[10], 1))
  
  • ((U^Increasing(99_0_REC_GE(x0[10], +(x1[10], 1))), ≥)∧[bni_21] = 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)
    
  
  
• 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9]) → COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])
  
  • (x1[9] ≥ 0 ⇒ (U^Increasing(COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])), ≥)∧[(-2)bni_23 + (-1)Bound*bni_23] + [(-1)bni_23]x1[9] ≥ 0∧[(-1)bso_24] ≥ 0)
    
  
  
• 395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8]) → 410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])
  
  • ((U^Increasing(410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])), ≥)∧[bni_25] = 0∧0 = 0∧[(-1)bso_26] ≥ 0)
    
  
  
• 375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7]) → 395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])
  
  • ((U^Increasing(395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])), ≥)∧[bni_27] = 0∧0 = 0∧[(-1)bso_28] ≥ 0)
    
  
  
• 358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6]) → 375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])
  
  • ((U^Increasing(375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])), ≥)∧[bni_29] = 0∧0 = 0∧[(-1)bso_30] ≥ 0)
    
  
  
• 341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5]) → 358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])
  
  • ((U^Increasing(358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])), ≥)∧[bni_31] = 0∧0 = 0∧[(-1)bso_32] ≥ 0)
    
  
  
• 324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4]) → 341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])
  
  • ((U^Increasing(341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])), ≥)∧[bni_33] = 0∧0 = 0∧[(-1)bso_34] ≥ 0)
    
  
  
• 295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3]) → 324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])
  
  • ((U^Increasing(324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])), ≥)∧[bni_35] = 0∧0 = 0∧[(-1)bso_36] ≥ 0)
    
  
  
• 123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2]) → 295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])
  
  • ((U^Increasing(295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])), ≥)∧[bni_37] = 0∧0 = 0∧[(-1)bso_38] ≥ 0)
    
  
  
• COND_99_0_REC_GE(TRUE, x0[1], x1[1]) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])
  
  • ((U^Increasing(123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_39] = 0∧0 = 0∧[(-1)bso_40] ≥ 0)
    
  
  
• 99_0_REC_GE(x0[0], x1[0]) → COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])
  
  • ([99] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [bni_41]x1[0] ≥ 0∧[(-1)bso_42] ≥ 0)
    
  • ([99] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [(-1)bni_41]x1[0] ≥ 0∧[(-1)bso_42] ≥ 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(123_0_descend_Load(x₁)) = [-1] + [-1]x₁   
POL(227_0_descend_LE(x₁)) = [-1] + [-1]x₁   
POL(0) = 0   
POL(233_0_descend_Return) = [2]   
POL(Cond_227_0_descend_LE(x₁, x₂)) = [-1] + [-1]x₂   
POL(>(x₁, x₂)) = [-1]   
POL(250_1_descend_InvokeMethod(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁   
POL(-(x₁, x₂)) = x₁ + [-1]x₂   
POL(1) = [1]   
POL(COND_410_1_TEST_INVOKEMETHOD(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₄   
POL(99_0_REC_GE(x₁, x₂)) = [-1] + [-1]x₂   
POL(+(x₁, x₂)) = x₁ + x₂   
POL(410_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(395_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(375_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(358_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(341_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(324_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(295_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(123_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(COND_99_0_REC_GE(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(<(x₁, x₂)) = [-1]   
POL(100) = [100]   

The following pairs are in P_>:

COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10]) → 99_0_REC_GE(x0[10], +(x1[10], 1))

The following pairs are in P_bound:

99_0_REC_GE(x0[0], x1[0]) → COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])

The following pairs are in P_≥:

410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9]) → COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])
395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8]) → 410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])
375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7]) → 395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])
358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6]) → 375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])
341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5]) → 358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])
324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4]) → 341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])
295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3]) → 324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])
123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2]) → 295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])
COND_99_0_REC_GE(TRUE, x0[1], x1[1]) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])
99_0_REC_GE(x0[0], x1[0]) → COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])

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

123_0_descend_Load(x0)¹ ↔ 227_0_descend_LE(x0)¹
233_0_descend_Return¹ → 227_0_descend_LE(0)¹
227_0_descend_LE(x0)¹ ↔ Cond_227_0_descend_LE(>(x0, 0), x0)¹
233_0_descend_Return¹ → 250_1_descend_InvokeMethod(233_0_descend_Return, 0)¹

(27) Complex Obligation (AND)

(28) 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:
123_0_descend_Load(x0) → 227_0_descend_LE(x0)
227_0_descend_LE(0) → 233_0_descend_Return
227_0_descend_LE(x0) → Cond_227_0_descend_LE(x0 > 0, x0)
Cond_227_0_descend_LE(TRUE, x0) → 250_1_descend_InvokeMethod(227_0_descend_LE(x0 - 1), x0 - 1)
250_1_descend_InvokeMethod(233_0_descend_Return, 0) → 233_0_descend_Return
250_1_descend_InvokeMethod(233_0_descend_Return, x0) → 233_0_descend_Return

The integer pair graph contains the following rules and edges:
(9): 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9]) → COND_410_1_TEST_INVOKEMETHOD(x1[9] > 0, 233_0_descend_Return, x0[9], x1[9])
(8): 395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8]) → 410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])
(7): 375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7]) → 395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])
(6): 358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6]) → 375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])
(5): 341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5]) → 358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])
(4): 324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4]) → 341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])
(3): 295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3]) → 324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])
(2): 123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2]) → 295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])
(1): COND_99_0_REC_GE(TRUE, x0[1], x1[1]) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])
(0): 99_0_REC_GE(x0[0], x1[0]) → COND_99_0_REC_GE(x1[0] < 100, x0[0], x1[0])

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

(1) -> (2), if (123_0_descend_Load(x1[1]) →^* 233_0_descend_Return∧x0[1] →^* x0[2]∧x1[1] →^* x1[2])

(2) -> (3), if (123_0_descend_Load(x1[2]) →^* 233_0_descend_Return∧x0[2] →^* x0[3]∧x1[2] →^* x1[3])

(3) -> (4), if (123_0_descend_Load(x1[3]) →^* 233_0_descend_Return∧x0[3] →^* x0[4]∧x1[3] →^* x1[4])

(4) -> (5), if (123_0_descend_Load(x1[4]) →^* 233_0_descend_Return∧x0[4] →^* x0[5]∧x1[4] →^* x1[5])

(5) -> (6), if (123_0_descend_Load(x1[5]) →^* 233_0_descend_Return∧x0[5] →^* x0[6]∧x1[5] →^* x1[6])

(6) -> (7), if (123_0_descend_Load(x1[6]) →^* 233_0_descend_Return∧x0[6] →^* x0[7]∧x1[6] →^* x1[7])

(7) -> (8), if (123_0_descend_Load(x1[7]) →^* 233_0_descend_Return∧x0[7] →^* x0[8]∧x1[7] →^* x1[8])

(8) -> (9), if (123_0_descend_Load(x1[8]) →^* 233_0_descend_Return∧x0[8] →^* x0[9]∧x1[8] →^* x1[9])

The set Q consists of the following terms:
123_0_descend_Load(x0)
227_0_descend_LE(x0)
Cond_227_0_descend_LE(TRUE, x0)
250_1_descend_InvokeMethod(233_0_descend_Return, x0)
121_1_rec_InvokeMethod(233_0_descend_Return, x0)

(29) IDependencyGraphProof (EQUIVALENT transformation)

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

(30) TRUE

(31) 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:
123_0_descend_Load(x0) → 227_0_descend_LE(x0)
227_0_descend_LE(0) → 233_0_descend_Return
227_0_descend_LE(x0) → Cond_227_0_descend_LE(x0 > 0, x0)
Cond_227_0_descend_LE(TRUE, x0) → 250_1_descend_InvokeMethod(227_0_descend_LE(x0 - 1), x0 - 1)
250_1_descend_InvokeMethod(233_0_descend_Return, 0) → 233_0_descend_Return
250_1_descend_InvokeMethod(233_0_descend_Return, x0) → 233_0_descend_Return

The integer pair graph contains the following rules and edges:
(10): COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10]) → 99_0_REC_GE(x0[10], x1[10] + 1)
(9): 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9]) → COND_410_1_TEST_INVOKEMETHOD(x1[9] > 0, 233_0_descend_Return, x0[9], x1[9])
(8): 395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8]) → 410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])
(7): 375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7]) → 395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])
(6): 358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6]) → 375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])
(5): 341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5]) → 358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])
(4): 324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4]) → 341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])
(3): 295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3]) → 324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])
(2): 123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2]) → 295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])
(1): COND_99_0_REC_GE(TRUE, x0[1], x1[1]) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])

(1) -> (2), if (123_0_descend_Load(x1[1]) →^* 233_0_descend_Return∧x0[1] →^* x0[2]∧x1[1] →^* x1[2])

(2) -> (3), if (123_0_descend_Load(x1[2]) →^* 233_0_descend_Return∧x0[2] →^* x0[3]∧x1[2] →^* x1[3])

(3) -> (4), if (123_0_descend_Load(x1[3]) →^* 233_0_descend_Return∧x0[3] →^* x0[4]∧x1[3] →^* x1[4])

(4) -> (5), if (123_0_descend_Load(x1[4]) →^* 233_0_descend_Return∧x0[4] →^* x0[5]∧x1[4] →^* x1[5])

(5) -> (6), if (123_0_descend_Load(x1[5]) →^* 233_0_descend_Return∧x0[5] →^* x0[6]∧x1[5] →^* x1[6])

(6) -> (7), if (123_0_descend_Load(x1[6]) →^* 233_0_descend_Return∧x0[6] →^* x0[7]∧x1[6] →^* x1[7])

(7) -> (8), if (123_0_descend_Load(x1[7]) →^* 233_0_descend_Return∧x0[7] →^* x0[8]∧x1[7] →^* x1[8])

(8) -> (9), if (123_0_descend_Load(x1[8]) →^* 233_0_descend_Return∧x0[8] →^* x0[9]∧x1[8] →^* x1[9])

(9) -> (10), if (x1[9] > 0 ∧x0[9] →^* x0[10]∧x1[9] →^* x1[10])

The set Q consists of the following terms:
123_0_descend_Load(x0)
227_0_descend_LE(x0)
Cond_227_0_descend_LE(TRUE, x0)
250_1_descend_InvokeMethod(233_0_descend_Return, x0)
121_1_rec_InvokeMethod(233_0_descend_Return, x0)

(32) IDependencyGraphProof (EQUIVALENT transformation)

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

(33) TRUE

(34) 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:
123_0_descend_Load(x0) → 227_0_descend_LE(x0)
227_0_descend_LE(0) → 233_0_descend_Return
227_0_descend_LE(x0) → Cond_227_0_descend_LE(x0 > 0, x0)
Cond_227_0_descend_LE(TRUE, x0) → 250_1_descend_InvokeMethod(227_0_descend_LE(x0 - 1), x0 - 1)
250_1_descend_InvokeMethod(233_0_descend_Return, 0) → 233_0_descend_Return
250_1_descend_InvokeMethod(233_0_descend_Return, x0) → 233_0_descend_Return
121_1_rec_InvokeMethod(233_0_descend_Return, 0) → 233_0_descend_Return
121_1_rec_InvokeMethod(233_0_descend_Return, x0) → 233_0_descend_Return

The integer pair graph contains the following rules and edges:
(0): 99_0_REC_GE(x0[0], x1[0]) → COND_99_0_REC_GE(x1[0] < 100, x0[0], x1[0])
(1): COND_99_0_REC_GE(TRUE, x0[1], x1[1]) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])
(2): 123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2]) → 295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])
(3): 295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3]) → 324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])
(4): 324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4]) → 341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])
(5): 341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5]) → 358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])
(6): 358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6]) → 375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])
(7): 375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7]) → 395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])
(8): 395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8]) → 410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])
(9): 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9]) → COND_410_1_TEST_INVOKEMETHOD(x1[9] > 0, 233_0_descend_Return, x0[9], x1[9])
(10): COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10]) → 99_0_REC_GE(x0[10], x1[10] + 1)
(12): COND_99_0_REC_GE1(TRUE, x0[12], x1[12]) → 99_0_REC_GE(x0[12] - 1, x0[12] - 1)

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

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

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

(1) -> (2), if (123_0_descend_Load(x1[1]) →^* 233_0_descend_Return∧x0[1] →^* x0[2]∧x1[1] →^* x1[2])

(2) -> (3), if (123_0_descend_Load(x1[2]) →^* 233_0_descend_Return∧x0[2] →^* x0[3]∧x1[2] →^* x1[3])

(3) -> (4), if (123_0_descend_Load(x1[3]) →^* 233_0_descend_Return∧x0[3] →^* x0[4]∧x1[3] →^* x1[4])

(4) -> (5), if (123_0_descend_Load(x1[4]) →^* 233_0_descend_Return∧x0[4] →^* x0[5]∧x1[4] →^* x1[5])

(5) -> (6), if (123_0_descend_Load(x1[5]) →^* 233_0_descend_Return∧x0[5] →^* x0[6]∧x1[5] →^* x1[6])

(6) -> (7), if (123_0_descend_Load(x1[6]) →^* 233_0_descend_Return∧x0[6] →^* x0[7]∧x1[6] →^* x1[7])

(7) -> (8), if (123_0_descend_Load(x1[7]) →^* 233_0_descend_Return∧x0[7] →^* x0[8]∧x1[7] →^* x1[8])

(8) -> (9), if (123_0_descend_Load(x1[8]) →^* 233_0_descend_Return∧x0[8] →^* x0[9]∧x1[8] →^* x1[9])

(9) -> (10), if (x1[9] > 0 ∧x0[9] →^* x0[10]∧x1[9] →^* x1[10])

The set Q consists of the following terms:
123_0_descend_Load(x0)
227_0_descend_LE(x0)
Cond_227_0_descend_LE(TRUE, x0)
250_1_descend_InvokeMethod(233_0_descend_Return, x0)
121_1_rec_InvokeMethod(233_0_descend_Return, x0)

(35) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(36) 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:
123_0_descend_Load(x0) → 227_0_descend_LE(x0)
227_0_descend_LE(0) → 233_0_descend_Return
227_0_descend_LE(x0) → Cond_227_0_descend_LE(x0 > 0, x0)
Cond_227_0_descend_LE(TRUE, x0) → 250_1_descend_InvokeMethod(227_0_descend_LE(x0 - 1), x0 - 1)
250_1_descend_InvokeMethod(233_0_descend_Return, 0) → 233_0_descend_Return
250_1_descend_InvokeMethod(233_0_descend_Return, x0) → 233_0_descend_Return
121_1_rec_InvokeMethod(233_0_descend_Return, 0) → 233_0_descend_Return
121_1_rec_InvokeMethod(233_0_descend_Return, x0) → 233_0_descend_Return

The integer pair graph contains the following rules and edges:
(10): COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10]) → 99_0_REC_GE(x0[10], x1[10] + 1)
(9): 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9]) → COND_410_1_TEST_INVOKEMETHOD(x1[9] > 0, 233_0_descend_Return, x0[9], x1[9])
(8): 395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8]) → 410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])
(7): 375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7]) → 395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])
(6): 358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6]) → 375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])
(5): 341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5]) → 358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])
(4): 324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4]) → 341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])
(3): 295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3]) → 324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])
(2): 123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2]) → 295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])
(1): COND_99_0_REC_GE(TRUE, x0[1], x1[1]) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])
(0): 99_0_REC_GE(x0[0], x1[0]) → COND_99_0_REC_GE(x1[0] < 100, x0[0], x1[0])

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

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

(1) -> (2), if (123_0_descend_Load(x1[1]) →^* 233_0_descend_Return∧x0[1] →^* x0[2]∧x1[1] →^* x1[2])

(2) -> (3), if (123_0_descend_Load(x1[2]) →^* 233_0_descend_Return∧x0[2] →^* x0[3]∧x1[2] →^* x1[3])

(3) -> (4), if (123_0_descend_Load(x1[3]) →^* 233_0_descend_Return∧x0[3] →^* x0[4]∧x1[3] →^* x1[4])

(4) -> (5), if (123_0_descend_Load(x1[4]) →^* 233_0_descend_Return∧x0[4] →^* x0[5]∧x1[4] →^* x1[5])

(5) -> (6), if (123_0_descend_Load(x1[5]) →^* 233_0_descend_Return∧x0[5] →^* x0[6]∧x1[5] →^* x1[6])

(6) -> (7), if (123_0_descend_Load(x1[6]) →^* 233_0_descend_Return∧x0[6] →^* x0[7]∧x1[6] →^* x1[7])

(7) -> (8), if (123_0_descend_Load(x1[7]) →^* 233_0_descend_Return∧x0[7] →^* x0[8]∧x1[7] →^* x1[8])

(8) -> (9), if (123_0_descend_Load(x1[8]) →^* 233_0_descend_Return∧x0[8] →^* x0[9]∧x1[8] →^* x1[9])

(9) -> (10), if (x1[9] > 0 ∧x0[9] →^* x0[10]∧x1[9] →^* x1[10])

The set Q consists of the following terms:
123_0_descend_Load(x0)
227_0_descend_LE(x0)
Cond_227_0_descend_LE(TRUE, x0)
250_1_descend_InvokeMethod(233_0_descend_Return, x0)
121_1_rec_InvokeMethod(233_0_descend_Return, x0)

(37) 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.

(38) 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:
123_0_descend_Load(x0) → 227_0_descend_LE(x0)
227_0_descend_LE(0) → 233_0_descend_Return
227_0_descend_LE(x0) → Cond_227_0_descend_LE(x0 > 0, x0)
Cond_227_0_descend_LE(TRUE, x0) → 250_1_descend_InvokeMethod(227_0_descend_LE(x0 - 1), x0 - 1)
250_1_descend_InvokeMethod(233_0_descend_Return, 0) → 233_0_descend_Return
250_1_descend_InvokeMethod(233_0_descend_Return, x0) → 233_0_descend_Return

The integer pair graph contains the following rules and edges:
(10): COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10]) → 99_0_REC_GE(x0[10], x1[10] + 1)
(9): 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9]) → COND_410_1_TEST_INVOKEMETHOD(x1[9] > 0, 233_0_descend_Return, x0[9], x1[9])
(8): 395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8]) → 410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])
(7): 375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7]) → 395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])
(6): 358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6]) → 375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])
(5): 341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5]) → 358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])
(4): 324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4]) → 341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])
(3): 295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3]) → 324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])
(2): 123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2]) → 295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])
(1): COND_99_0_REC_GE(TRUE, x0[1], x1[1]) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])
(0): 99_0_REC_GE(x0[0], x1[0]) → COND_99_0_REC_GE(x1[0] < 100, x0[0], x1[0])

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

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

(1) -> (2), if (123_0_descend_Load(x1[1]) →^* 233_0_descend_Return∧x0[1] →^* x0[2]∧x1[1] →^* x1[2])

(2) -> (3), if (123_0_descend_Load(x1[2]) →^* 233_0_descend_Return∧x0[2] →^* x0[3]∧x1[2] →^* x1[3])

(3) -> (4), if (123_0_descend_Load(x1[3]) →^* 233_0_descend_Return∧x0[3] →^* x0[4]∧x1[3] →^* x1[4])

(4) -> (5), if (123_0_descend_Load(x1[4]) →^* 233_0_descend_Return∧x0[4] →^* x0[5]∧x1[4] →^* x1[5])

(5) -> (6), if (123_0_descend_Load(x1[5]) →^* 233_0_descend_Return∧x0[5] →^* x0[6]∧x1[5] →^* x1[6])

(6) -> (7), if (123_0_descend_Load(x1[6]) →^* 233_0_descend_Return∧x0[6] →^* x0[7]∧x1[6] →^* x1[7])

(7) -> (8), if (123_0_descend_Load(x1[7]) →^* 233_0_descend_Return∧x0[7] →^* x0[8]∧x1[7] →^* x1[8])

(8) -> (9), if (123_0_descend_Load(x1[8]) →^* 233_0_descend_Return∧x0[8] →^* x0[9]∧x1[8] →^* x1[9])

(9) -> (10), if (x1[9] > 0 ∧x0[9] →^* x0[10]∧x1[9] →^* x1[10])

The set Q consists of the following terms:
123_0_descend_Load(x0)
227_0_descend_LE(x0)
Cond_227_0_descend_LE(TRUE, x0)
250_1_descend_InvokeMethod(233_0_descend_Return, x0)
121_1_rec_InvokeMethod(233_0_descend_Return, x0)

(39) 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@550571f6 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 COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10]) → 99_0_REC_GE(x0[10], +(x1[10], 1)) the following chains were created:

• We consider the chain COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10]) → 99_0_REC_GE(x0[10], +(x1[10], 1)) which results in the following constraint:
  

  (1)    (COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10])≥NonInfC∧COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10])≥99_0_REC_GE(x0[10], +(x1[10], 1))∧(U^Increasing(99_0_REC_GE(x0[10], +(x1[10], 1))), ≥))

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

  (2)    ((U^Increasing(99_0_REC_GE(x0[10], +(x1[10], 1))), ≥)∧[bni_22] = 0∧[1 + (-1)bso_23] ≥ 0)

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

  (3)    ((U^Increasing(99_0_REC_GE(x0[10], +(x1[10], 1))), ≥)∧[bni_22] = 0∧[1 + (-1)bso_23] ≥ 0)

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

  (4)    ((U^Increasing(99_0_REC_GE(x0[10], +(x1[10], 1))), ≥)∧[bni_22] = 0∧[1 + (-1)bso_23] ≥ 0)

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

  (5)    ((U^Increasing(99_0_REC_GE(x0[10], +(x1[10], 1))), ≥)∧[bni_22] = 0∧0 = 0∧[1 + (-1)bso_23] ≥ 0)

  
  
  

For Pair 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9]) → COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9]) the following chains were created:

• We consider the chain 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9]) → COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9]), COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10]) → 99_0_REC_GE(x0[10], +(x1[10], 1)) which results in the following constraint:
  

  (6)    (>(x1[9], 0)=TRUE∧x0[9]=x0[10]∧x1[9]=x1[10] ⇒ 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9])≥NonInfC∧410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9])≥COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])∧(U^Increasing(COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])), ≥))

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

  (7)    (>(x1[9], 0)=TRUE ⇒ 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9])≥NonInfC∧410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9])≥COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])∧(U^Increasing(COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])), ≥))

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

  (8)    (x1[9] + [-1] ≥ 0 ⇒ (U^Increasing(COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]x1[9] ≥ 0∧[(-1)bso_25] ≥ 0)

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

  (9)    (x1[9] + [-1] ≥ 0 ⇒ (U^Increasing(COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]x1[9] ≥ 0∧[(-1)bso_25] ≥ 0)

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

  (10)    (x1[9] + [-1] ≥ 0 ⇒ (U^Increasing(COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]x1[9] ≥ 0∧[(-1)bso_25] ≥ 0)

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

  (11)    (x1[9] ≥ 0 ⇒ (U^Increasing(COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])), ≥)∧[(-2)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]x1[9] ≥ 0∧[(-1)bso_25] ≥ 0)

  
  
  

For Pair 395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8]) → 410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8]) the following chains were created:

• We consider the chain 395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8]) → 410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8]) which results in the following constraint:
  

  (12)    (395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8])≥NonInfC∧395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8])≥410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])∧(U^Increasing(410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])), ≥))

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

  (13)    ((U^Increasing(410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])), ≥)∧[bni_26] = 0∧[(-1)bso_27] ≥ 0)

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

  (14)    ((U^Increasing(410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])), ≥)∧[bni_26] = 0∧[(-1)bso_27] ≥ 0)

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

  (15)    ((U^Increasing(410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])), ≥)∧[bni_26] = 0∧[(-1)bso_27] ≥ 0)

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

  (16)    ((U^Increasing(410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])), ≥)∧[bni_26] = 0∧0 = 0∧[(-1)bso_27] ≥ 0)

  
  
  

For Pair 375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7]) → 395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7]) the following chains were created:

• We consider the chain 375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7]) → 395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7]) which results in the following constraint:
  

  (17)    (375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7])≥NonInfC∧375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7])≥395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])∧(U^Increasing(395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])), ≥))

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

  (18)    ((U^Increasing(395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])), ≥)∧[bni_28] = 0∧[(-1)bso_29] ≥ 0)

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

  (19)    ((U^Increasing(395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])), ≥)∧[bni_28] = 0∧[(-1)bso_29] ≥ 0)

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

  (20)    ((U^Increasing(395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])), ≥)∧[bni_28] = 0∧[(-1)bso_29] ≥ 0)

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

  (21)    ((U^Increasing(395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])), ≥)∧[bni_28] = 0∧0 = 0∧[(-1)bso_29] ≥ 0)

  
  
  

For Pair 358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6]) → 375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6]) the following chains were created:

• We consider the chain 358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6]) → 375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6]) which results in the following constraint:
  

  (22)    (358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6])≥NonInfC∧358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6])≥375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])∧(U^Increasing(375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])), ≥))

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

  (23)    ((U^Increasing(375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])), ≥)∧[bni_30] = 0∧[(-1)bso_31] ≥ 0)

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

  (24)    ((U^Increasing(375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])), ≥)∧[bni_30] = 0∧[(-1)bso_31] ≥ 0)

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

  (25)    ((U^Increasing(375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])), ≥)∧[bni_30] = 0∧[(-1)bso_31] ≥ 0)

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

  (26)    ((U^Increasing(375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])), ≥)∧[bni_30] = 0∧0 = 0∧[(-1)bso_31] ≥ 0)

  
  
  

For Pair 341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5]) → 358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5]) the following chains were created:

• We consider the chain 341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5]) → 358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5]) which results in the following constraint:
  

  (27)    (341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5])≥NonInfC∧341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5])≥358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])∧(U^Increasing(358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])), ≥))

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

  (28)    ((U^Increasing(358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])), ≥)∧[bni_32] = 0∧[(-1)bso_33] ≥ 0)

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

  (29)    ((U^Increasing(358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])), ≥)∧[bni_32] = 0∧[(-1)bso_33] ≥ 0)

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

  (30)    ((U^Increasing(358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])), ≥)∧[bni_32] = 0∧[(-1)bso_33] ≥ 0)

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

  (31)    ((U^Increasing(358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])), ≥)∧[bni_32] = 0∧0 = 0∧[(-1)bso_33] ≥ 0)

  
  
  

For Pair 324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4]) → 341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4]) the following chains were created:

• We consider the chain 324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4]) → 341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4]) which results in the following constraint:
  

  (32)    (324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4])≥NonInfC∧324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4])≥341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])∧(U^Increasing(341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])), ≥))

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

  (33)    ((U^Increasing(341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])), ≥)∧[bni_34] = 0∧[(-1)bso_35] ≥ 0)

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

  (34)    ((U^Increasing(341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])), ≥)∧[bni_34] = 0∧[(-1)bso_35] ≥ 0)

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

  (35)    ((U^Increasing(341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])), ≥)∧[bni_34] = 0∧[(-1)bso_35] ≥ 0)

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

  (36)    ((U^Increasing(341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])), ≥)∧[bni_34] = 0∧0 = 0∧[(-1)bso_35] ≥ 0)

  
  
  

For Pair 295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3]) → 324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3]) the following chains were created:

• We consider the chain 295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3]) → 324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3]) which results in the following constraint:
  

  (37)    (295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3])≥NonInfC∧295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3])≥324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])∧(U^Increasing(324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])), ≥))

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

  (38)    ((U^Increasing(324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])), ≥)∧[bni_36] = 0∧[(-1)bso_37] ≥ 0)

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

  (39)    ((U^Increasing(324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])), ≥)∧[bni_36] = 0∧[(-1)bso_37] ≥ 0)

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

  (40)    ((U^Increasing(324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])), ≥)∧[bni_36] = 0∧[(-1)bso_37] ≥ 0)

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

  (41)    ((U^Increasing(324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])), ≥)∧[bni_36] = 0∧0 = 0∧[(-1)bso_37] ≥ 0)

  
  
  

For Pair 123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2]) → 295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2]) the following chains were created:

• We consider the chain 123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2]) → 295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2]) which results in the following constraint:
  

  (42)    (123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2])≥NonInfC∧123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2])≥295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])∧(U^Increasing(295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])), ≥))

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

  (43)    ((U^Increasing(295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])), ≥)∧[bni_38] = 0∧[(-1)bso_39] ≥ 0)

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

  (44)    ((U^Increasing(295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])), ≥)∧[bni_38] = 0∧[(-1)bso_39] ≥ 0)

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

  (45)    ((U^Increasing(295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])), ≥)∧[bni_38] = 0∧[(-1)bso_39] ≥ 0)

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

  (46)    ((U^Increasing(295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])), ≥)∧[bni_38] = 0∧0 = 0∧[(-1)bso_39] ≥ 0)

  
  
  

For Pair COND_99_0_REC_GE(TRUE, x0[1], x1[1]) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1]) the following chains were created:

• We consider the chain COND_99_0_REC_GE(TRUE, x0[1], x1[1]) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1]) which results in the following constraint:
  

  (47)    (COND_99_0_REC_GE(TRUE, x0[1], x1[1])≥NonInfC∧COND_99_0_REC_GE(TRUE, x0[1], x1[1])≥123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])∧(U^Increasing(123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])), ≥))

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

  (48)    ((U^Increasing(123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_40] = 0∧[(-1)bso_41] ≥ 0)

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

  (49)    ((U^Increasing(123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_40] = 0∧[(-1)bso_41] ≥ 0)

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

  (50)    ((U^Increasing(123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_40] = 0∧[(-1)bso_41] ≥ 0)

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

  (51)    ((U^Increasing(123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_40] = 0∧0 = 0∧[(-1)bso_41] ≥ 0)

  
  
  

For Pair 99_0_REC_GE(x0[0], x1[0]) → COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0]) the following chains were created:

• We consider the chain 99_0_REC_GE(x0[0], x1[0]) → COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0]), COND_99_0_REC_GE(TRUE, x0[1], x1[1]) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1]) which results in the following constraint:
  

  (52)    (<(x1[0], 100)=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1] ⇒ 99_0_REC_GE(x0[0], x1[0])≥NonInfC∧99_0_REC_GE(x0[0], x1[0])≥COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])∧(U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥))

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

  (53)    (<(x1[0], 100)=TRUE ⇒ 99_0_REC_GE(x0[0], x1[0])≥NonInfC∧99_0_REC_GE(x0[0], x1[0])≥COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])∧(U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥))

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

  (54)    ([99] + [-1]x1[0] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [(-1)bni_42]x1[0] ≥ 0∧[(-1)bso_43] ≥ 0)

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

  (55)    ([99] + [-1]x1[0] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [(-1)bni_42]x1[0] ≥ 0∧[(-1)bso_43] ≥ 0)

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

  (56)    ([99] + [-1]x1[0] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [(-1)bni_42]x1[0] ≥ 0∧[(-1)bso_43] ≥ 0)

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

  (57)    ([99] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]x1[0] ≥ 0∧[(-1)bso_43] ≥ 0)

  
  

  (58)    ([99] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [(-1)bni_42]x1[0] ≥ 0∧[(-1)bso_43] ≥ 0)

  
  
  

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

• COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10]) → 99_0_REC_GE(x0[10], +(x1[10], 1))
  
  • ((U^Increasing(99_0_REC_GE(x0[10], +(x1[10], 1))), ≥)∧[bni_22] = 0∧0 = 0∧[1 + (-1)bso_23] ≥ 0)
    
  
  
• 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9]) → COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])
  
  • (x1[9] ≥ 0 ⇒ (U^Increasing(COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])), ≥)∧[(-2)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]x1[9] ≥ 0∧[(-1)bso_25] ≥ 0)
    
  
  
• 395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8]) → 410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])
  
  • ((U^Increasing(410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])), ≥)∧[bni_26] = 0∧0 = 0∧[(-1)bso_27] ≥ 0)
    
  
  
• 375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7]) → 395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])
  
  • ((U^Increasing(395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])), ≥)∧[bni_28] = 0∧0 = 0∧[(-1)bso_29] ≥ 0)
    
  
  
• 358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6]) → 375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])
  
  • ((U^Increasing(375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])), ≥)∧[bni_30] = 0∧0 = 0∧[(-1)bso_31] ≥ 0)
    
  
  
• 341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5]) → 358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])
  
  • ((U^Increasing(358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])), ≥)∧[bni_32] = 0∧0 = 0∧[(-1)bso_33] ≥ 0)
    
  
  
• 324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4]) → 341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])
  
  • ((U^Increasing(341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])), ≥)∧[bni_34] = 0∧0 = 0∧[(-1)bso_35] ≥ 0)
    
  
  
• 295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3]) → 324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])
  
  • ((U^Increasing(324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])), ≥)∧[bni_36] = 0∧0 = 0∧[(-1)bso_37] ≥ 0)
    
  
  
• 123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2]) → 295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])
  
  • ((U^Increasing(295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])), ≥)∧[bni_38] = 0∧0 = 0∧[(-1)bso_39] ≥ 0)
    
  
  
• COND_99_0_REC_GE(TRUE, x0[1], x1[1]) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])
  
  • ((U^Increasing(123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_40] = 0∧0 = 0∧[(-1)bso_41] ≥ 0)
    
  
  
• 99_0_REC_GE(x0[0], x1[0]) → COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])
  
  • ([99] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]x1[0] ≥ 0∧[(-1)bso_43] ≥ 0)
    
  • ([99] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [(-1)bni_42]x1[0] ≥ 0∧[(-1)bso_43] ≥ 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(123_0_descend_Load(x₁)) = [-1]   
POL(227_0_descend_LE(x₁)) = x₁   
POL(0) = 0   
POL(233_0_descend_Return) = [-1]   
POL(Cond_227_0_descend_LE(x₁, x₂)) = [1] + [-1]x₂   
POL(>(x₁, x₂)) = [-1]   
POL(250_1_descend_InvokeMethod(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁   
POL(-(x₁, x₂)) = x₁ + [-1]x₂   
POL(1) = [1]   
POL(COND_410_1_TEST_INVOKEMETHOD(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₄   
POL(99_0_REC_GE(x₁, x₂)) = [-1] + [-1]x₂   
POL(+(x₁, x₂)) = x₁ + x₂   
POL(410_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(395_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(375_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(358_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(341_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(324_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(295_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(123_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(COND_99_0_REC_GE(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(<(x₁, x₂)) = 0   
POL(100) = [100]   

The following pairs are in P_>:

COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10]) → 99_0_REC_GE(x0[10], +(x1[10], 1))

The following pairs are in P_bound:

99_0_REC_GE(x0[0], x1[0]) → COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])

The following pairs are in P_≥:

410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9]) → COND_410_1_TEST_INVOKEMETHOD(>(x1[9], 0), 233_0_descend_Return, x0[9], x1[9])
395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8]) → 410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])
375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7]) → 395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])
358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6]) → 375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])
341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5]) → 358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])
324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4]) → 341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])
295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3]) → 324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])
123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2]) → 295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])
COND_99_0_REC_GE(TRUE, x0[1], x1[1]) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])
99_0_REC_GE(x0[0], x1[0]) → COND_99_0_REC_GE(<(x1[0], 100), x0[0], x1[0])

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

227_0_descend_LE(0)¹ → 233_0_descend_Return¹
250_1_descend_InvokeMethod(233_0_descend_Return, 0)¹ → 233_0_descend_Return¹

(40) Complex Obligation (AND)

(41) 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:
123_0_descend_Load(x0) → 227_0_descend_LE(x0)
227_0_descend_LE(0) → 233_0_descend_Return
227_0_descend_LE(x0) → Cond_227_0_descend_LE(x0 > 0, x0)
Cond_227_0_descend_LE(TRUE, x0) → 250_1_descend_InvokeMethod(227_0_descend_LE(x0 - 1), x0 - 1)
250_1_descend_InvokeMethod(233_0_descend_Return, 0) → 233_0_descend_Return
250_1_descend_InvokeMethod(233_0_descend_Return, x0) → 233_0_descend_Return

The integer pair graph contains the following rules and edges:
(9): 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9]) → COND_410_1_TEST_INVOKEMETHOD(x1[9] > 0, 233_0_descend_Return, x0[9], x1[9])
(8): 395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8]) → 410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])
(7): 375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7]) → 395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])
(6): 358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6]) → 375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])
(5): 341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5]) → 358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])
(4): 324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4]) → 341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])
(3): 295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3]) → 324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])
(2): 123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2]) → 295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])
(1): COND_99_0_REC_GE(TRUE, x0[1], x1[1]) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])
(0): 99_0_REC_GE(x0[0], x1[0]) → COND_99_0_REC_GE(x1[0] < 100, x0[0], x1[0])

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

(1) -> (2), if (123_0_descend_Load(x1[1]) →^* 233_0_descend_Return∧x0[1] →^* x0[2]∧x1[1] →^* x1[2])

(2) -> (3), if (123_0_descend_Load(x1[2]) →^* 233_0_descend_Return∧x0[2] →^* x0[3]∧x1[2] →^* x1[3])

(3) -> (4), if (123_0_descend_Load(x1[3]) →^* 233_0_descend_Return∧x0[3] →^* x0[4]∧x1[3] →^* x1[4])

(4) -> (5), if (123_0_descend_Load(x1[4]) →^* 233_0_descend_Return∧x0[4] →^* x0[5]∧x1[4] →^* x1[5])

(5) -> (6), if (123_0_descend_Load(x1[5]) →^* 233_0_descend_Return∧x0[5] →^* x0[6]∧x1[5] →^* x1[6])

(6) -> (7), if (123_0_descend_Load(x1[6]) →^* 233_0_descend_Return∧x0[6] →^* x0[7]∧x1[6] →^* x1[7])

(7) -> (8), if (123_0_descend_Load(x1[7]) →^* 233_0_descend_Return∧x0[7] →^* x0[8]∧x1[7] →^* x1[8])

(8) -> (9), if (123_0_descend_Load(x1[8]) →^* 233_0_descend_Return∧x0[8] →^* x0[9]∧x1[8] →^* x1[9])

The set Q consists of the following terms:
123_0_descend_Load(x0)
227_0_descend_LE(x0)
Cond_227_0_descend_LE(TRUE, x0)
250_1_descend_InvokeMethod(233_0_descend_Return, x0)
121_1_rec_InvokeMethod(233_0_descend_Return, x0)

(42) IDependencyGraphProof (EQUIVALENT transformation)

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

(43) TRUE

(44) 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:
123_0_descend_Load(x0) → 227_0_descend_LE(x0)
227_0_descend_LE(0) → 233_0_descend_Return
227_0_descend_LE(x0) → Cond_227_0_descend_LE(x0 > 0, x0)
Cond_227_0_descend_LE(TRUE, x0) → 250_1_descend_InvokeMethod(227_0_descend_LE(x0 - 1), x0 - 1)
250_1_descend_InvokeMethod(233_0_descend_Return, 0) → 233_0_descend_Return
250_1_descend_InvokeMethod(233_0_descend_Return, x0) → 233_0_descend_Return

The integer pair graph contains the following rules and edges:
(10): COND_410_1_TEST_INVOKEMETHOD(TRUE, 233_0_descend_Return, x0[10], x1[10]) → 99_0_REC_GE(x0[10], x1[10] + 1)
(9): 410_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[9], x1[9]) → COND_410_1_TEST_INVOKEMETHOD(x1[9] > 0, 233_0_descend_Return, x0[9], x1[9])
(8): 395_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[8], x1[8]) → 410_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[8]), x0[8], x1[8])
(7): 375_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[7], x1[7]) → 395_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[7]), x0[7], x1[7])
(6): 358_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[6], x1[6]) → 375_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[6]), x0[6], x1[6])
(5): 341_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[5], x1[5]) → 358_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[5]), x0[5], x1[5])
(4): 324_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[4], x1[4]) → 341_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[4]), x0[4], x1[4])
(3): 295_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[3], x1[3]) → 324_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[3]), x0[3], x1[3])
(2): 123_1_TEST_INVOKEMETHOD(233_0_descend_Return, x0[2], x1[2]) → 295_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[2]), x0[2], x1[2])
(1): COND_99_0_REC_GE(TRUE, x0[1], x1[1]) → 123_1_TEST_INVOKEMETHOD(123_0_descend_Load(x1[1]), x0[1], x1[1])

(1) -> (2), if (123_0_descend_Load(x1[1]) →^* 233_0_descend_Return∧x0[1] →^* x0[2]∧x1[1] →^* x1[2])

(2) -> (3), if (123_0_descend_Load(x1[2]) →^* 233_0_descend_Return∧x0[2] →^* x0[3]∧x1[2] →^* x1[3])

(3) -> (4), if (123_0_descend_Load(x1[3]) →^* 233_0_descend_Return∧x0[3] →^* x0[4]∧x1[3] →^* x1[4])

(4) -> (5), if (123_0_descend_Load(x1[4]) →^* 233_0_descend_Return∧x0[4] →^* x0[5]∧x1[4] →^* x1[5])

(5) -> (6), if (123_0_descend_Load(x1[5]) →^* 233_0_descend_Return∧x0[5] →^* x0[6]∧x1[5] →^* x1[6])

(6) -> (7), if (123_0_descend_Load(x1[6]) →^* 233_0_descend_Return∧x0[6] →^* x0[7]∧x1[6] →^* x1[7])

(7) -> (8), if (123_0_descend_Load(x1[7]) →^* 233_0_descend_Return∧x0[7] →^* x0[8]∧x1[7] →^* x1[8])

(8) -> (9), if (123_0_descend_Load(x1[8]) →^* 233_0_descend_Return∧x0[8] →^* x0[9]∧x1[8] →^* x1[9])

(9) -> (10), if (x1[9] > 0 ∧x0[9] →^* x0[10]∧x1[9] →^* x1[10])

The set Q consists of the following terms:
123_0_descend_Load(x0)
227_0_descend_LE(x0)
Cond_227_0_descend_LE(TRUE, x0)
250_1_descend_InvokeMethod(233_0_descend_Return, x0)
121_1_rec_InvokeMethod(233_0_descend_Return, x0)

(45) IDependencyGraphProof (EQUIVALENT transformation)

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

(46) TRUE