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:
210_0_descend_LE(EOS(STATIC_210), i42, i42) → 213_0_descend_LE(EOS(STATIC_213), i42, i42)
213_0_descend_LE(EOS(STATIC_213), i42, i42) → 217_0_descend_Load(EOS(STATIC_217), i42) | >(i42, 0)
217_0_descend_Load(EOS(STATIC_217), i42) → 221_0_descend_ConstantStackPush(EOS(STATIC_221), i42)
221_0_descend_ConstantStackPush(EOS(STATIC_221), i42) → 224_0_descend_IntArithmetic(EOS(STATIC_224), i42, 1)
224_0_descend_IntArithmetic(EOS(STATIC_224), i42, matching1) → 227_0_descend_InvokeMethod(EOS(STATIC_227), -(i42, 1)) | &&(>(i42, 0), =(matching1, 1))
227_0_descend_InvokeMethod(EOS(STATIC_227), i45) → 229_1_descend_InvokeMethod(229_0_descend_Load(EOS(STATIC_229), i45), i45)
229_0_descend_Load(EOS(STATIC_229), i45) → 231_0_descend_Load(EOS(STATIC_231), i45)
231_0_descend_Load(EOS(STATIC_231), i45) → 207_0_descend_Load(EOS(STATIC_207), i45)
207_0_descend_Load(EOS(STATIC_207), i40) → 210_0_descend_LE(EOS(STATIC_210), i40, i40)
R rules:
210_0_descend_LE(EOS(STATIC_210), matching1, matching2) → 212_0_descend_LE(EOS(STATIC_212), 0, 0) | &&(=(matching1, 0), =(matching2, 0))
212_0_descend_LE(EOS(STATIC_212), matching1, matching2) → 215_0_descend_Return(EOS(STATIC_215)) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
229_1_descend_InvokeMethod(215_0_descend_Return(EOS(STATIC_215)), matching1) → 238_0_descend_Return(EOS(STATIC_238), 0) | =(matching1, 0)
229_1_descend_InvokeMethod(264_0_descend_Return(EOS(STATIC_264)), i57) → 286_0_descend_Return(EOS(STATIC_286), i57)
238_0_descend_Return(EOS(STATIC_238), matching1) → 259_0_descend_Return(EOS(STATIC_259), 0) | =(matching1, 0)
259_0_descend_Return(EOS(STATIC_259), i53) → 264_0_descend_Return(EOS(STATIC_264))
286_0_descend_Return(EOS(STATIC_286), i57) → 259_0_descend_Return(EOS(STATIC_259), i57)

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

P rules:
210_0_descend_LE(EOS(STATIC_210), x0, x0) → 229_1_descend_InvokeMethod(210_0_descend_LE(EOS(STATIC_210), -(x0, 1), -(x0, 1)), -(x0, 1)) | >(x0, 0)
R rules:
210_0_descend_LE(EOS(STATIC_210), 0, 0) → 215_0_descend_Return(EOS(STATIC_215))
229_1_descend_InvokeMethod(215_0_descend_Return(EOS(STATIC_215)), 0) → 264_0_descend_Return(EOS(STATIC_264))
229_1_descend_InvokeMethod(264_0_descend_Return(EOS(STATIC_264)), x0) → 264_0_descend_Return(EOS(STATIC_264))

Filtered ground terms:

210_0_descend_LE(x1, x2, x3) → 210_0_descend_LE(x2, x3)
Cond_210_0_descend_LE(x1, x2, x3, x4) → Cond_210_0_descend_LE(x1, x3, x4)
264_0_descend_Return(x1) → 264_0_descend_Return
215_0_descend_Return(x1) → 215_0_descend_Return

Filtered duplicate args:

210_0_descend_LE(x1, x2) → 210_0_descend_LE(x2)
Cond_210_0_descend_LE(x1, x2, x3) → Cond_210_0_descend_LE(x1, x3)

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

P rules:
210_0_descend_LE(x0) → 229_1_descend_InvokeMethod(210_0_descend_LE(-(x0, 1)), -(x0, 1)) | >(x0, 0)
R rules:
210_0_descend_LE(0) → 215_0_descend_Return
229_1_descend_InvokeMethod(215_0_descend_Return, 0) → 264_0_descend_Return
229_1_descend_InvokeMethod(264_0_descend_Return, x0) → 264_0_descend_Return

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

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

P rules:
210_0_DESCEND_LE(x0) → COND_210_0_DESCEND_LE(>(x0, 0), x0)
COND_210_0_DESCEND_LE(TRUE, x0) → 210_0_DESCEND_LE(-(x0, 1))
R rules:
210_0_descend_LE(0) → 215_0_descend_Return
229_1_descend_InvokeMethod(215_0_descend_Return, 0) → 215_0_descend_Return
229_1_descend_InvokeMethod(215_0_descend_Return, x0) → 215_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:
210_0_descend_LE(0) → 215_0_descend_Return
229_1_descend_InvokeMethod(215_0_descend_Return, 0) → 215_0_descend_Return
229_1_descend_InvokeMethod(215_0_descend_Return, x0) → 215_0_descend_Return

The integer pair graph contains the following rules and edges:
(0): 210_0_DESCEND_LE(x0[0]) → COND_210_0_DESCEND_LE(x0[0] > 0, x0[0])
(1): COND_210_0_DESCEND_LE(TRUE, x0[1]) → 210_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:
210_0_descend_LE(0)
229_1_descend_InvokeMethod(215_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@74cc39fe 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 210_0_DESCEND_LE(x0) → COND_210_0_DESCEND_LE(>(x0, 0), x0) the following chains were created:

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

  (1)    (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 210_0_DESCEND_LE(x0[0])≥NonInfC∧210_0_DESCEND_LE(x0[0])≥COND_210_0_DESCEND_LE(>(x0[0], 0), x0[0])∧(U^Increasing(COND_210_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 ⇒ 210_0_DESCEND_LE(x0[0])≥NonInfC∧210_0_DESCEND_LE(x0[0])≥COND_210_0_DESCEND_LE(>(x0[0], 0), x0[0])∧(U^Increasing(COND_210_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_210_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_210_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_210_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_210_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_210_0_DESCEND_LE(TRUE, x0) → 210_0_DESCEND_LE(-(x0, 1)) the following chains were created:

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

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

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

  (8)    ((U^Increasing(210_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(210_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(210_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(210_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.

• 210_0_DESCEND_LE(x0) → COND_210_0_DESCEND_LE(>(x0, 0), x0)
  
  • (x0[0] ≥ 0 ⇒ (U^Increasing(COND_210_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_210_0_DESCEND_LE(TRUE, x0) → 210_0_DESCEND_LE(-(x0, 1))
  
  • ((U^Increasing(210_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(210_0_descend_LE(x₁)) = [-1]   
POL(0) = 0   
POL(215_0_descend_Return) = [-1]   
POL(229_1_descend_InvokeMethod(x₁, x₂)) = [-1]   
POL(210_0_DESCEND_LE(x₁)) = [2]x₁   
POL(COND_210_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_210_0_DESCEND_LE(TRUE, x0[1]) → 210_0_DESCEND_LE(-(x0[1], 1))

The following pairs are in P_bound:

210_0_DESCEND_LE(x0[0]) → COND_210_0_DESCEND_LE(>(x0[0], 0), x0[0])

The following pairs are in P_≥:

210_0_DESCEND_LE(x0[0]) → COND_210_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:
210_0_descend_LE(0) → 215_0_descend_Return
229_1_descend_InvokeMethod(215_0_descend_Return, 0) → 215_0_descend_Return
229_1_descend_InvokeMethod(215_0_descend_Return, x0) → 215_0_descend_Return

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


The set Q consists of the following terms:
210_0_descend_LE(0)
229_1_descend_InvokeMethod(215_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:
210_0_descend_LE(0) → 215_0_descend_Return
229_1_descend_InvokeMethod(215_0_descend_Return, 0) → 215_0_descend_Return
229_1_descend_InvokeMethod(215_0_descend_Return, x0) → 215_0_descend_Return

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


The set Q consists of the following terms:
210_0_descend_LE(0)
229_1_descend_InvokeMethod(215_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) → 75_0_rec_Load(EOS(STATIC_75), i6) | &&(>(1, 0), =(matching1, 1))
75_0_rec_Load(EOS(STATIC_75), i6) → 79_0_rec_TypeCast(EOS(STATIC_79), i6, i6)
79_0_rec_TypeCast(EOS(STATIC_79), i6, i6) → 87_0_rec_Store(EOS(STATIC_87), i6, i10) | =(i10, i6)
87_0_rec_Store(EOS(STATIC_87), i6, i10) → 90_0_rec_Load(EOS(STATIC_90), i6, i10)
90_0_rec_Load(EOS(STATIC_90), i6, i10) → 93_0_rec_ConstantStackPush(EOS(STATIC_93), i6, i10, i10)
93_0_rec_ConstantStackPush(EOS(STATIC_93), i6, i10, i10) → 96_0_rec_GE(EOS(STATIC_96), i6, i10, i10, 100)
96_0_rec_GE(EOS(STATIC_96), i6, i13, i13, matching1) → 98_0_rec_GE(EOS(STATIC_98), i6, i13, i13, 100) | =(matching1, 100)
96_0_rec_GE(EOS(STATIC_96), i6, i14, i14, matching1) → 99_0_rec_GE(EOS(STATIC_99), i6, i14, i14, 100) | =(matching1, 100)
98_0_rec_GE(EOS(STATIC_98), i6, i13, i13, matching1) → 101_0_rec_Load(EOS(STATIC_101), i6, i13) | &&(<(i13, 100), =(matching1, 100))
101_0_rec_Load(EOS(STATIC_101), i6, i13) → 103_0_rec_InvokeMethod(EOS(STATIC_103), i6, i13, i13)
103_0_rec_InvokeMethod(EOS(STATIC_103), i6, i13, i13) → 105_0_test_Load(EOS(STATIC_105), i6, i13, i13, i13)
105_0_test_Load(EOS(STATIC_105), i6, i13, i13, i13) → 109_0_test_InvokeMethod(EOS(STATIC_109), i6, i13, i13, i13, i13)
109_0_test_InvokeMethod(EOS(STATIC_109), i6, i13, i13, i13, i13) → 113_1_test_InvokeMethod(113_0_descend_Load(EOS(STATIC_113), i13), i6, i13, i13, i13, i13)
113_1_test_InvokeMethod(264_0_descend_Return(EOS(STATIC_264)), i6, i55, i55, i55, i55) → 283_0_descend_Return(EOS(STATIC_283), i6, i55, i55, i55, i55)
283_0_descend_Return(EOS(STATIC_283), i6, i55, i55, i55, i55) → 252_0_descend_Return(EOS(STATIC_252), i6, i55, i55, i55, i55)
252_0_descend_Return(EOS(STATIC_252), i6, i49, i49, i49, i49) → 261_0_test_Load(EOS(STATIC_261), i6, i49, i49, i49)
261_0_test_Load(EOS(STATIC_261), i6, i49, i49, i49) → 266_0_test_InvokeMethod(EOS(STATIC_266), i6, i49, i49, i49, i49)
266_0_test_InvokeMethod(EOS(STATIC_266), i6, i49, i49, i49, i49) → 270_1_test_InvokeMethod(270_0_descend_Load(EOS(STATIC_270), i49), i6, i49, i49, i49, i49)
270_1_test_InvokeMethod(264_0_descend_Return(EOS(STATIC_264)), i6, i64, i64, i64, i64) → 295_0_descend_Return(EOS(STATIC_295), i6, i64, i64, i64, i64)
295_0_descend_Return(EOS(STATIC_295), i6, i64, i64, i64, i64) → 297_0_test_Load(EOS(STATIC_297), i6, i64, i64, i64)
297_0_test_Load(EOS(STATIC_297), i6, i64, i64, i64) → 299_0_test_InvokeMethod(EOS(STATIC_299), i6, i64, i64, i64, i64)
299_0_test_InvokeMethod(EOS(STATIC_299), i6, i64, i64, i64, i64) → 301_1_test_InvokeMethod(301_0_descend_Load(EOS(STATIC_301), i64), i6, i64, i64, i64, i64)
301_1_test_InvokeMethod(264_0_descend_Return(EOS(STATIC_264)), i6, i68, i68, i68, i68) → 313_0_descend_Return(EOS(STATIC_313), i6, i68, i68, i68, i68)
313_0_descend_Return(EOS(STATIC_313), i6, i68, i68, i68, i68) → 315_0_test_Load(EOS(STATIC_315), i6, i68, i68, i68)
315_0_test_Load(EOS(STATIC_315), i6, i68, i68, i68) → 317_0_test_InvokeMethod(EOS(STATIC_317), i6, i68, i68, i68, i68)
317_0_test_InvokeMethod(EOS(STATIC_317), i6, i68, i68, i68, i68) → 319_1_test_InvokeMethod(319_0_descend_Load(EOS(STATIC_319), i68), i6, i68, i68, i68, i68)
319_1_test_InvokeMethod(264_0_descend_Return(EOS(STATIC_264)), i6, i73, i73, i73, i73) → 330_0_descend_Return(EOS(STATIC_330), i6, i73, i73, i73, i73)
330_0_descend_Return(EOS(STATIC_330), i6, i73, i73, i73, i73) → 332_0_test_Load(EOS(STATIC_332), i6, i73, i73, i73)
332_0_test_Load(EOS(STATIC_332), i6, i73, i73, i73) → 334_0_test_InvokeMethod(EOS(STATIC_334), i6, i73, i73, i73, i73)
334_0_test_InvokeMethod(EOS(STATIC_334), i6, i73, i73, i73, i73) → 336_1_test_InvokeMethod(336_0_descend_Load(EOS(STATIC_336), i73), i6, i73, i73, i73, i73)
336_1_test_InvokeMethod(264_0_descend_Return(EOS(STATIC_264)), i6, i76, i76, i76, i76) → 347_0_descend_Return(EOS(STATIC_347), i6, i76, i76, i76, i76)
347_0_descend_Return(EOS(STATIC_347), i6, i76, i76, i76, i76) → 349_0_test_Load(EOS(STATIC_349), i6, i76, i76, i76)
349_0_test_Load(EOS(STATIC_349), i6, i76, i76, i76) → 351_0_test_InvokeMethod(EOS(STATIC_351), i6, i76, i76, i76, i76)
351_0_test_InvokeMethod(EOS(STATIC_351), i6, i76, i76, i76, i76) → 353_1_test_InvokeMethod(353_0_descend_Load(EOS(STATIC_353), i76), i6, i76, i76, i76, i76)
353_1_test_InvokeMethod(264_0_descend_Return(EOS(STATIC_264)), i6, i79, i79, i79, i79) → 364_0_descend_Return(EOS(STATIC_364), i6, i79, i79, i79, i79)
364_0_descend_Return(EOS(STATIC_364), i6, i79, i79, i79, i79) → 365_0_test_Load(EOS(STATIC_365), i6, i79, i79, i79)
365_0_test_Load(EOS(STATIC_365), i6, i79, i79, i79) → 368_0_test_InvokeMethod(EOS(STATIC_368), i6, i79, i79, i79, i79)
368_0_test_InvokeMethod(EOS(STATIC_368), i6, i79, i79, i79, i79) → 370_1_test_InvokeMethod(370_0_descend_Load(EOS(STATIC_370), i79), i6, i79, i79, i79, i79)
370_1_test_InvokeMethod(264_0_descend_Return(EOS(STATIC_264)), i6, i83, i83, i83, i83) → 381_0_descend_Return(EOS(STATIC_381), i6, i83, i83, i83, i83)
381_0_descend_Return(EOS(STATIC_381), i6, i83, i83, i83, i83) → 383_0_test_Load(EOS(STATIC_383), i6, i83, i83, i83)
383_0_test_Load(EOS(STATIC_383), i6, i83, i83, i83) → 385_0_test_InvokeMethod(EOS(STATIC_385), i6, i83, i83, i83)
385_0_test_InvokeMethod(EOS(STATIC_385), i6, i83, i83, i83) → 387_1_test_InvokeMethod(387_0_descend_Load(EOS(STATIC_387), i83), i6, i83, i83, i83)
387_1_test_InvokeMethod(264_0_descend_Return(EOS(STATIC_264)), i6, i86, i86, i86) → 398_0_descend_Return(EOS(STATIC_398), i6, i86, i86, i86)
398_0_descend_Return(EOS(STATIC_398), i6, i86, i86, i86) → 400_0_test_Return(EOS(STATIC_400), i6, i86, i86)
400_0_test_Return(EOS(STATIC_400), i6, i86, i86) → 402_0_rec_Inc(EOS(STATIC_402), i6, i86)
402_0_rec_Inc(EOS(STATIC_402), i6, i86) → 404_0_rec_JMP(EOS(STATIC_404), i6, +(i86, 1)) | >(i86, 0)
404_0_rec_JMP(EOS(STATIC_404), i6, i87) → 407_0_rec_Load(EOS(STATIC_407), i6, i87)
407_0_rec_Load(EOS(STATIC_407), i6, i87) → 90_0_rec_Load(EOS(STATIC_90), i6, i87)
99_0_rec_GE(EOS(STATIC_99), i6, i14, i14, matching1) → 102_0_rec_Load(EOS(STATIC_102), i6) | &&(>=(i14, 100), =(matching1, 100))
102_0_rec_Load(EOS(STATIC_102), i6) → 104_0_rec_ConstantStackPush(EOS(STATIC_104), i6)
104_0_rec_ConstantStackPush(EOS(STATIC_104), i6) → 106_0_rec_IntArithmetic(EOS(STATIC_106), i6, 1)
106_0_rec_IntArithmetic(EOS(STATIC_106), i6, matching1) → 107_0_rec_InvokeMethod(EOS(STATIC_107), -(i6, 1)) | &&(>(i6, 0), =(matching1, 1))
107_0_rec_InvokeMethod(EOS(STATIC_107), i16) → 111_1_rec_InvokeMethod(111_0_rec_Load(EOS(STATIC_111), i16), i16)
111_0_rec_Load(EOS(STATIC_111), i16) → 115_0_rec_Load(EOS(STATIC_115), i16)
115_0_rec_Load(EOS(STATIC_115), i16) → 61_0_rec_Load(EOS(STATIC_61), i16)
61_0_rec_Load(EOS(STATIC_61), i3) → 63_0_rec_ConstantStackPush(EOS(STATIC_63), i3, i3)
R rules:
113_0_descend_Load(EOS(STATIC_113), i13) → 117_0_descend_Load(EOS(STATIC_117), i13)
117_0_descend_Load(EOS(STATIC_117), i13) → 207_0_descend_Load(EOS(STATIC_207), i13)
270_0_descend_Load(EOS(STATIC_270), i49) → 280_0_descend_Load(EOS(STATIC_280), i49)
280_0_descend_Load(EOS(STATIC_280), i49) → 207_0_descend_Load(EOS(STATIC_207), i49)
301_0_descend_Load(EOS(STATIC_301), i64) → 304_0_descend_Load(EOS(STATIC_304), i64)
304_0_descend_Load(EOS(STATIC_304), i64) → 207_0_descend_Load(EOS(STATIC_207), i64)
319_0_descend_Load(EOS(STATIC_319), i68) → 321_0_descend_Load(EOS(STATIC_321), i68)
321_0_descend_Load(EOS(STATIC_321), i68) → 207_0_descend_Load(EOS(STATIC_207), i68)
336_0_descend_Load(EOS(STATIC_336), i73) → 338_0_descend_Load(EOS(STATIC_338), i73)
338_0_descend_Load(EOS(STATIC_338), i73) → 207_0_descend_Load(EOS(STATIC_207), i73)
353_0_descend_Load(EOS(STATIC_353), i76) → 355_0_descend_Load(EOS(STATIC_355), i76)
355_0_descend_Load(EOS(STATIC_355), i76) → 207_0_descend_Load(EOS(STATIC_207), i76)
370_0_descend_Load(EOS(STATIC_370), i79) → 372_0_descend_Load(EOS(STATIC_372), i79)
372_0_descend_Load(EOS(STATIC_372), i79) → 207_0_descend_Load(EOS(STATIC_207), i79)
387_0_descend_Load(EOS(STATIC_387), i83) → 389_0_descend_Load(EOS(STATIC_389), i83)
389_0_descend_Load(EOS(STATIC_389), i83) → 207_0_descend_Load(EOS(STATIC_207), i83)
231_0_descend_Load(EOS(STATIC_231), i45) → 207_0_descend_Load(EOS(STATIC_207), i45)
207_0_descend_Load(EOS(STATIC_207), i40) → 210_0_descend_LE(EOS(STATIC_210), i40, i40)
210_0_descend_LE(EOS(STATIC_210), matching1, matching2) → 212_0_descend_LE(EOS(STATIC_212), 0, 0) | &&(=(matching1, 0), =(matching2, 0))
210_0_descend_LE(EOS(STATIC_210), i42, i42) → 213_0_descend_LE(EOS(STATIC_213), i42, i42)
212_0_descend_LE(EOS(STATIC_212), matching1, matching2) → 215_0_descend_Return(EOS(STATIC_215)) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
213_0_descend_LE(EOS(STATIC_213), i42, i42) → 217_0_descend_Load(EOS(STATIC_217), i42) | >(i42, 0)
217_0_descend_Load(EOS(STATIC_217), i42) → 221_0_descend_ConstantStackPush(EOS(STATIC_221), i42)
221_0_descend_ConstantStackPush(EOS(STATIC_221), i42) → 224_0_descend_IntArithmetic(EOS(STATIC_224), i42, 1)
224_0_descend_IntArithmetic(EOS(STATIC_224), i42, matching1) → 227_0_descend_InvokeMethod(EOS(STATIC_227), -(i42, 1)) | &&(>(i42, 0), =(matching1, 1))
227_0_descend_InvokeMethod(EOS(STATIC_227), i45) → 229_1_descend_InvokeMethod(229_0_descend_Load(EOS(STATIC_229), i45), i45)
229_0_descend_Load(EOS(STATIC_229), i45) → 231_0_descend_Load(EOS(STATIC_231), i45)
229_1_descend_InvokeMethod(215_0_descend_Return(EOS(STATIC_215)), matching1) → 238_0_descend_Return(EOS(STATIC_238), 0) | =(matching1, 0)
229_1_descend_InvokeMethod(264_0_descend_Return(EOS(STATIC_264)), i57) → 286_0_descend_Return(EOS(STATIC_286), i57)
238_0_descend_Return(EOS(STATIC_238), matching1) → 259_0_descend_Return(EOS(STATIC_259), 0) | =(matching1, 0)
259_0_descend_Return(EOS(STATIC_259), i53) → 264_0_descend_Return(EOS(STATIC_264))
286_0_descend_Return(EOS(STATIC_286), i57) → 259_0_descend_Return(EOS(STATIC_259), i57)
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) → 73_0_rec_Return(EOS(STATIC_73)) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
111_1_rec_InvokeMethod(73_0_rec_Return(EOS(STATIC_73)), matching1) → 125_0_rec_Return(EOS(STATIC_125), 0) | =(matching1, 0)
111_1_rec_InvokeMethod(181_0_rec_Return(EOS(STATIC_181)), i35) → 204_0_rec_Return(EOS(STATIC_204), i35)
125_0_rec_Return(EOS(STATIC_125), matching1) → 174_0_rec_Return(EOS(STATIC_174), 0) | =(matching1, 0)
174_0_rec_Return(EOS(STATIC_174), i29) → 181_0_rec_Return(EOS(STATIC_181))
204_0_rec_Return(EOS(STATIC_204), i35) → 174_0_rec_Return(EOS(STATIC_174), i35)

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

P rules:
96_0_rec_GE(EOS(STATIC_96), x0, x1, x1, 100) → 113_1_test_InvokeMethod(113_0_descend_Load(EOS(STATIC_113), x1), x0, x1, x1, x1, x1) | <(x1, 100)
113_1_test_InvokeMethod(264_0_descend_Return(EOS(STATIC_264)), x0, x1, x1, x1, x1) → 270_1_test_InvokeMethod(270_0_descend_Load(EOS(STATIC_270), x1), x0, x1, x1, x1, x1)
270_1_test_InvokeMethod(264_0_descend_Return(EOS(STATIC_264)), x0, x1, x1, x1, x1) → 301_1_test_InvokeMethod(301_0_descend_Load(EOS(STATIC_301), x1), x0, x1, x1, x1, x1)
301_1_test_InvokeMethod(264_0_descend_Return(EOS(STATIC_264)), x0, x1, x1, x1, x1) → 319_1_test_InvokeMethod(319_0_descend_Load(EOS(STATIC_319), x1), x0, x1, x1, x1, x1)
319_1_test_InvokeMethod(264_0_descend_Return(EOS(STATIC_264)), x0, x1, x1, x1, x1) → 336_1_test_InvokeMethod(336_0_descend_Load(EOS(STATIC_336), x1), x0, x1, x1, x1, x1)
336_1_test_InvokeMethod(264_0_descend_Return(EOS(STATIC_264)), x0, x1, x1, x1, x1) → 353_1_test_InvokeMethod(353_0_descend_Load(EOS(STATIC_353), x1), x0, x1, x1, x1, x1)
353_1_test_InvokeMethod(264_0_descend_Return(EOS(STATIC_264)), x0, x1, x1, x1, x1) → 370_1_test_InvokeMethod(370_0_descend_Load(EOS(STATIC_370), x1), x0, x1, x1, x1, x1)
370_1_test_InvokeMethod(264_0_descend_Return(EOS(STATIC_264)), x0, x1, x1, x1, x1) → 387_1_test_InvokeMethod(387_0_descend_Load(EOS(STATIC_387), x1), x0, x1, x1, x1)
387_1_test_InvokeMethod(264_0_descend_Return(EOS(STATIC_264)), x0, x1, x1, x1) → 96_0_rec_GE(EOS(STATIC_96), x0, +(x1, 1), +(x1, 1), 100) | >(x1, 0)
96_0_rec_GE(EOS(STATIC_96), x0, x1, x1, 100) → 111_1_rec_InvokeMethod(96_0_rec_GE(EOS(STATIC_96), -(x0, 1), -(x0, 1), -(x0, 1), 100), -(x0, 1)) | &&(>(+(x1, 1), 100), >(x0, 1))
R rules:
113_0_descend_Load(EOS(STATIC_113), x0) → 210_0_descend_LE(EOS(STATIC_210), x0, x0)
270_0_descend_Load(EOS(STATIC_270), x0) → 210_0_descend_LE(EOS(STATIC_210), x0, x0)
301_0_descend_Load(EOS(STATIC_301), x0) → 210_0_descend_LE(EOS(STATIC_210), x0, x0)
319_0_descend_Load(EOS(STATIC_319), x0) → 210_0_descend_LE(EOS(STATIC_210), x0, x0)
336_0_descend_Load(EOS(STATIC_336), x0) → 210_0_descend_LE(EOS(STATIC_210), x0, x0)
353_0_descend_Load(EOS(STATIC_353), x0) → 210_0_descend_LE(EOS(STATIC_210), x0, x0)
370_0_descend_Load(EOS(STATIC_370), x0) → 210_0_descend_LE(EOS(STATIC_210), x0, x0)
387_0_descend_Load(EOS(STATIC_387), x0) → 210_0_descend_LE(EOS(STATIC_210), x0, x0)
210_0_descend_LE(EOS(STATIC_210), 0, 0) → 215_0_descend_Return(EOS(STATIC_215))
210_0_descend_LE(EOS(STATIC_210), x0, x0) → 229_1_descend_InvokeMethod(210_0_descend_LE(EOS(STATIC_210), -(x0, 1), -(x0, 1)), -(x0, 1)) | >(x0, 0)
229_1_descend_InvokeMethod(215_0_descend_Return(EOS(STATIC_215)), 0) → 264_0_descend_Return(EOS(STATIC_264))
229_1_descend_InvokeMethod(264_0_descend_Return(EOS(STATIC_264)), x0) → 264_0_descend_Return(EOS(STATIC_264))
111_1_rec_InvokeMethod(73_0_rec_Return(EOS(STATIC_73)), 0) → 181_0_rec_Return(EOS(STATIC_181))
111_1_rec_InvokeMethod(181_0_rec_Return(EOS(STATIC_181)), x0) → 181_0_rec_Return(EOS(STATIC_181))

Filtered ground terms:

96_0_rec_GE(x1, x2, x3, x4, x5) → 96_0_rec_GE(x2, x3, x4)
Cond_96_0_rec_GE1(x1, x2, x3, x4, x5, x6) → Cond_96_0_rec_GE1(x1, x3, x4, x5)
Cond_387_1_test_InvokeMethod(x1, x2, x3, x4, x5, x6) → Cond_387_1_test_InvokeMethod(x1, x3, x4, x5, x6)
264_0_descend_Return(x1) → 264_0_descend_Return
387_0_descend_Load(x1, x2) → 387_0_descend_Load(x2)
370_0_descend_Load(x1, x2) → 370_0_descend_Load(x2)
353_0_descend_Load(x1, x2) → 353_0_descend_Load(x2)
336_0_descend_Load(x1, x2) → 336_0_descend_Load(x2)
319_0_descend_Load(x1, x2) → 319_0_descend_Load(x2)
301_0_descend_Load(x1, x2) → 301_0_descend_Load(x2)
270_0_descend_Load(x1, x2) → 270_0_descend_Load(x2)
113_0_descend_Load(x1, x2) → 113_0_descend_Load(x2)
Cond_96_0_rec_GE(x1, x2, x3, x4, x5, x6) → Cond_96_0_rec_GE(x1, x3, x4, x5)
181_0_rec_Return(x1) → 181_0_rec_Return
73_0_rec_Return(x1) → 73_0_rec_Return
215_0_descend_Return(x1) → 215_0_descend_Return
210_0_descend_LE(x1, x2, x3) → 210_0_descend_LE(x2, x3)
Cond_210_0_descend_LE(x1, x2, x3, x4) → Cond_210_0_descend_LE(x1, x3, x4)

Filtered duplicate args:

96_0_rec_GE(x1, x2, x3) → 96_0_rec_GE(x1, x3)
Cond_96_0_rec_GE(x1, x2, x3, x4) → Cond_96_0_rec_GE(x1, x2, x4)
113_1_test_InvokeMethod(x1, x2, x3, x4, x5, x6) → 113_1_test_InvokeMethod(x1, x2, x6)
270_1_test_InvokeMethod(x1, x2, x3, x4, x5, x6) → 270_1_test_InvokeMethod(x1, x2, x6)
301_1_test_InvokeMethod(x1, x2, x3, x4, x5, x6) → 301_1_test_InvokeMethod(x1, x2, x6)
319_1_test_InvokeMethod(x1, x2, x3, x4, x5, x6) → 319_1_test_InvokeMethod(x1, x2, x6)
336_1_test_InvokeMethod(x1, x2, x3, x4, x5, x6) → 336_1_test_InvokeMethod(x1, x2, x6)
353_1_test_InvokeMethod(x1, x2, x3, x4, x5, x6) → 353_1_test_InvokeMethod(x1, x2, x6)
370_1_test_InvokeMethod(x1, x2, x3, x4, x5, x6) → 370_1_test_InvokeMethod(x1, x2, x6)
387_1_test_InvokeMethod(x1, x2, x3, x4, x5) → 387_1_test_InvokeMethod(x1, x2, x5)
Cond_387_1_test_InvokeMethod(x1, x2, x3, x4, x5) → Cond_387_1_test_InvokeMethod(x1, x2, x5)
Cond_96_0_rec_GE1(x1, x2, x3, x4) → Cond_96_0_rec_GE1(x1, x2, x4)
210_0_descend_LE(x1, x2) → 210_0_descend_LE(x2)
Cond_210_0_descend_LE(x1, x2, x3) → Cond_210_0_descend_LE(x1, x3)

Filtered unneeded arguments:

Cond_96_0_rec_GE1(x1, x2, x3) → Cond_96_0_rec_GE1(x1, x2)

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

P rules:
96_0_rec_GE(x0, x1) → 113_1_test_InvokeMethod(113_0_descend_Load(x1), x0, x1) | <(x1, 100)
113_1_test_InvokeMethod(264_0_descend_Return, x0, x1) → 270_1_test_InvokeMethod(270_0_descend_Load(x1), x0, x1)
270_1_test_InvokeMethod(264_0_descend_Return, x0, x1) → 301_1_test_InvokeMethod(301_0_descend_Load(x1), x0, x1)
301_1_test_InvokeMethod(264_0_descend_Return, x0, x1) → 319_1_test_InvokeMethod(319_0_descend_Load(x1), x0, x1)
319_1_test_InvokeMethod(264_0_descend_Return, x0, x1) → 336_1_test_InvokeMethod(336_0_descend_Load(x1), x0, x1)
336_1_test_InvokeMethod(264_0_descend_Return, x0, x1) → 353_1_test_InvokeMethod(353_0_descend_Load(x1), x0, x1)
353_1_test_InvokeMethod(264_0_descend_Return, x0, x1) → 370_1_test_InvokeMethod(370_0_descend_Load(x1), x0, x1)
370_1_test_InvokeMethod(264_0_descend_Return, x0, x1) → 387_1_test_InvokeMethod(387_0_descend_Load(x1), x0, x1)
387_1_test_InvokeMethod(264_0_descend_Return, x0, x1) → 96_0_rec_GE(x0, +(x1, 1)) | >(x1, 0)
96_0_rec_GE(x0, x1) → 111_1_rec_InvokeMethod(96_0_rec_GE(-(x0, 1), -(x0, 1)), -(x0, 1)) | &&(>(x1, 99), >(x0, 1))
R rules:
113_0_descend_Load(x0) → 210_0_descend_LE(x0)
270_0_descend_Load(x0) → 210_0_descend_LE(x0)
301_0_descend_Load(x0) → 210_0_descend_LE(x0)
319_0_descend_Load(x0) → 210_0_descend_LE(x0)
336_0_descend_Load(x0) → 210_0_descend_LE(x0)
353_0_descend_Load(x0) → 210_0_descend_LE(x0)
370_0_descend_Load(x0) → 210_0_descend_LE(x0)
387_0_descend_Load(x0) → 210_0_descend_LE(x0)
210_0_descend_LE(0) → 215_0_descend_Return
210_0_descend_LE(x0) → 229_1_descend_InvokeMethod(210_0_descend_LE(-(x0, 1)), -(x0, 1)) | >(x0, 0)
229_1_descend_InvokeMethod(215_0_descend_Return, 0) → 264_0_descend_Return
229_1_descend_InvokeMethod(264_0_descend_Return, x0) → 264_0_descend_Return
111_1_rec_InvokeMethod(73_0_rec_Return, 0) → 181_0_rec_Return
111_1_rec_InvokeMethod(181_0_rec_Return, x0) → 181_0_rec_Return

Performed bisimulation on rules. Used the following equivalence classes: {[113_0_descend_Load_1, 270_0_descend_Load_1, 301_0_descend_Load_1, 319_0_descend_Load_1, 336_0_descend_Load_1, 353_0_descend_Load_1, 370_0_descend_Load_1, 387_0_descend_Load_1]=113_0_descend_Load_1, [215_0_descend_Return, 264_0_descend_Return, 73_0_rec_Return, 181_0_rec_Return]=215_0_descend_Return}

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

P rules:
96_0_REC_GE(x0, x1) → COND_96_0_REC_GE(<(x1, 100), x0, x1)
COND_96_0_REC_GE(TRUE, x0, x1) → 113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1), x0, x1)
113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0, x1) → 270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1), x0, x1)
270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0, x1) → 301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1), x0, x1)
301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0, x1) → 319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1), x0, x1)
319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0, x1) → 336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1), x0, x1)
336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0, x1) → 353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1), x0, x1)
353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0, x1) → 370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1), x0, x1)
370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0, x1) → 387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1), x0, x1)
387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0, x1) → COND_387_1_TEST_INVOKEMETHOD(>(x1, 0), 215_0_descend_Return, x0, x1)
COND_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0, x1) → 96_0_REC_GE(x0, +(x1, 1))
96_0_REC_GE(x0, x1) → COND_96_0_REC_GE1(&&(>(x1, 99), >(x0, 1)), x0, x1)
COND_96_0_REC_GE1(TRUE, x0, x1) → 96_0_REC_GE(-(x0, 1), -(x0, 1))
R rules:
113_0_descend_Load(x0) → 210_0_descend_LE(x0)
210_0_descend_LE(0) → 215_0_descend_Return
210_0_descend_LE(x0) → Cond_210_0_descend_LE(>(x0, 0), x0)
Cond_210_0_descend_LE(TRUE, x0) → 229_1_descend_InvokeMethod(210_0_descend_LE(-(x0, 1)), -(x0, 1))
229_1_descend_InvokeMethod(215_0_descend_Return, 0) → 215_0_descend_Return
229_1_descend_InvokeMethod(215_0_descend_Return, x0) → 215_0_descend_Return
111_1_rec_InvokeMethod(215_0_descend_Return, 0) → 215_0_descend_Return
111_1_rec_InvokeMethod(215_0_descend_Return, x0) → 215_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:
113_0_descend_Load(x0) → 210_0_descend_LE(x0)
210_0_descend_LE(0) → 215_0_descend_Return
210_0_descend_LE(x0) → Cond_210_0_descend_LE(x0 > 0, x0)
Cond_210_0_descend_LE(TRUE, x0) → 229_1_descend_InvokeMethod(210_0_descend_LE(x0 - 1), x0 - 1)
229_1_descend_InvokeMethod(215_0_descend_Return, 0) → 215_0_descend_Return
229_1_descend_InvokeMethod(215_0_descend_Return, x0) → 215_0_descend_Return
111_1_rec_InvokeMethod(215_0_descend_Return, 0) → 215_0_descend_Return
111_1_rec_InvokeMethod(215_0_descend_Return, x0) → 215_0_descend_Return

The integer pair graph contains the following rules and edges:
(0): 96_0_REC_GE(x0[0], x1[0]) → COND_96_0_REC_GE(x1[0] < 100, x0[0], x1[0])
(1): COND_96_0_REC_GE(TRUE, x0[1], x1[1]) → 113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[1]), x0[1], x1[1])
(2): 113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2]) → 270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2])
(3): 270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3]) → 301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3])
(4): 301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4]) → 319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4])
(5): 319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5]) → 336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5])
(6): 336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6]) → 353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6])
(7): 353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7]) → 370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7])
(8): 370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8]) → 387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8])
(9): 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9]) → COND_387_1_TEST_INVOKEMETHOD(x1[9] > 0, 215_0_descend_Return, x0[9], x1[9])
(10): COND_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0[10], x1[10]) → 96_0_REC_GE(x0[10], x1[10] + 1)
(11): 96_0_REC_GE(x0[11], x1[11]) → COND_96_0_REC_GE1(x1[11] > 99 && x0[11] > 1, x0[11], x1[11])
(12): COND_96_0_REC_GE1(TRUE, x0[12], x1[12]) → 96_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 (113_0_descend_Load(x1[1]) →^* 215_0_descend_Return∧x0[1] →^* x0[2]∧x1[1] →^* x1[2])

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

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

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

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

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

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

(8) -> (9), if (113_0_descend_Load(x1[8]) →^* 215_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:
113_0_descend_Load(x0)
210_0_descend_LE(x0)
Cond_210_0_descend_LE(TRUE, x0)
229_1_descend_InvokeMethod(215_0_descend_Return, x0)
111_1_rec_InvokeMethod(215_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@74cc39fe 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 96_0_REC_GE(x0, x1) → COND_96_0_REC_GE(<(x1, 100), x0, x1) the following chains were created:

• We consider the chain 96_0_REC_GE(x0[0], x1[0]) → COND_96_0_REC_GE(<(x1[0], 100), x0[0], x1[0]), COND_96_0_REC_GE(TRUE, x0[1], x1[1]) → 113_1_TEST_INVOKEMETHOD(113_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] ⇒ 96_0_REC_GE(x0[0], x1[0])≥NonInfC∧96_0_REC_GE(x0[0], x1[0])≥COND_96_0_REC_GE(<(x1[0], 100), x0[0], x1[0])∧(U^Increasing(COND_96_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 ⇒ 96_0_REC_GE(x0[0], x1[0])≥NonInfC∧96_0_REC_GE(x0[0], x1[0])≥COND_96_0_REC_GE(<(x1[0], 100), x0[0], x1[0])∧(U^Increasing(COND_96_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_96_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_96_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_96_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_96_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] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_96_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] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_96_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_96_0_REC_GE(TRUE, x0, x1) → 113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1), x0, x1) the following chains were created:

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

  (9)    (COND_96_0_REC_GE(TRUE, x0[1], x1[1])≥NonInfC∧COND_96_0_REC_GE(TRUE, x0[1], x1[1])≥113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[1]), x0[1], x1[1])∧(U^Increasing(113_1_TEST_INVOKEMETHOD(113_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(113_1_TEST_INVOKEMETHOD(113_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(113_1_TEST_INVOKEMETHOD(113_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(113_1_TEST_INVOKEMETHOD(113_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(113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_41] = 0∧0 = 0∧0 = 0∧[(-1)bso_42] ≥ 0)

  
  
  

For Pair 113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0, x1) → 270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1), x0, x1) the following chains were created:

• We consider the chain 113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2]) → 270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2]) which results in the following constraint:
  

  (14)    (113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2])≥NonInfC∧113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2])≥270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2])∧(U^Increasing(270_1_TEST_INVOKEMETHOD(113_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(270_1_TEST_INVOKEMETHOD(113_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(270_1_TEST_INVOKEMETHOD(113_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(270_1_TEST_INVOKEMETHOD(113_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(270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2])), ≥)∧[bni_43] = 0∧0 = 0∧0 = 0∧[(-1)bso_44] ≥ 0)

  
  
  

For Pair 270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0, x1) → 301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1), x0, x1) the following chains were created:

• We consider the chain 270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3]) → 301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3]) which results in the following constraint:
  

  (19)    (270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3])≥NonInfC∧270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3])≥301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3])∧(U^Increasing(301_1_TEST_INVOKEMETHOD(113_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(301_1_TEST_INVOKEMETHOD(113_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(301_1_TEST_INVOKEMETHOD(113_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(301_1_TEST_INVOKEMETHOD(113_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(301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3])), ≥)∧[bni_45] = 0∧0 = 0∧0 = 0∧[(-1)bso_46] ≥ 0)

  
  
  

For Pair 301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0, x1) → 319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1), x0, x1) the following chains were created:

• We consider the chain 301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4]) → 319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4]) which results in the following constraint:
  

  (24)    (301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4])≥NonInfC∧301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4])≥319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4])∧(U^Increasing(319_1_TEST_INVOKEMETHOD(113_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(319_1_TEST_INVOKEMETHOD(113_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(319_1_TEST_INVOKEMETHOD(113_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(319_1_TEST_INVOKEMETHOD(113_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(319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4])), ≥)∧[bni_47] = 0∧0 = 0∧0 = 0∧[(-1)bso_48] ≥ 0)

  
  
  

For Pair 319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0, x1) → 336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1), x0, x1) the following chains were created:

• We consider the chain 319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5]) → 336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5]) which results in the following constraint:
  

  (29)    (319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5])≥NonInfC∧319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5])≥336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5])∧(U^Increasing(336_1_TEST_INVOKEMETHOD(113_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(336_1_TEST_INVOKEMETHOD(113_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(336_1_TEST_INVOKEMETHOD(113_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(336_1_TEST_INVOKEMETHOD(113_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(336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5])), ≥)∧[bni_49] = 0∧0 = 0∧0 = 0∧[(-1)bso_50] ≥ 0)

  
  
  

For Pair 336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0, x1) → 353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1), x0, x1) the following chains were created:

• We consider the chain 336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6]) → 353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6]) which results in the following constraint:
  

  (34)    (336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6])≥NonInfC∧336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6])≥353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6])∧(U^Increasing(353_1_TEST_INVOKEMETHOD(113_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(353_1_TEST_INVOKEMETHOD(113_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(353_1_TEST_INVOKEMETHOD(113_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(353_1_TEST_INVOKEMETHOD(113_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(353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6])), ≥)∧[bni_51] = 0∧0 = 0∧0 = 0∧[(-1)bso_52] ≥ 0)

  
  
  

For Pair 353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0, x1) → 370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1), x0, x1) the following chains were created:

• We consider the chain 353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7]) → 370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7]) which results in the following constraint:
  

  (39)    (353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7])≥NonInfC∧353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7])≥370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7])∧(U^Increasing(370_1_TEST_INVOKEMETHOD(113_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(370_1_TEST_INVOKEMETHOD(113_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(370_1_TEST_INVOKEMETHOD(113_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(370_1_TEST_INVOKEMETHOD(113_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(370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7])), ≥)∧[bni_53] = 0∧0 = 0∧0 = 0∧[(-1)bso_54] ≥ 0)

  
  
  

For Pair 370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0, x1) → 387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1), x0, x1) the following chains were created:

• We consider the chain 370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8]) → 387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8]) which results in the following constraint:
  

  (44)    (370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8])≥NonInfC∧370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8])≥387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8])∧(U^Increasing(387_1_TEST_INVOKEMETHOD(113_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(387_1_TEST_INVOKEMETHOD(113_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(387_1_TEST_INVOKEMETHOD(113_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(387_1_TEST_INVOKEMETHOD(113_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(387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8])), ≥)∧[bni_55] = 0∧0 = 0∧0 = 0∧[(-1)bso_56] ≥ 0)

  
  
  

For Pair 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0, x1) → COND_387_1_TEST_INVOKEMETHOD(>(x1, 0), 215_0_descend_Return, x0, x1) the following chains were created:

• We consider the chain 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9]) → COND_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_0_descend_Return, x0[9], x1[9]), COND_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0[10], x1[10]) → 96_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] ⇒ 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9])≥NonInfC∧387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9])≥COND_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_0_descend_Return, x0[9], x1[9])∧(U^Increasing(COND_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_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 ⇒ 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9])≥NonInfC∧387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9])≥COND_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_0_descend_Return, x0[9], x1[9])∧(U^Increasing(COND_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_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_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_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_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_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_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_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_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_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_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_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_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0, x1) → 96_0_REC_GE(x0, +(x1, 1)) the following chains were created:

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

  (56)    (COND_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0[10], x1[10])≥NonInfC∧COND_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0[10], x1[10])≥96_0_REC_GE(x0[10], +(x1[10], 1))∧(U^Increasing(96_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(96_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(96_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(96_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(96_0_REC_GE(x0[10], +(x1[10], 1))), ≥)∧[bni_59] = 0∧0 = 0∧0 = 0∧[(-1)bso_60] ≥ 0)

  
  
  

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

• We consider the chain 96_0_REC_GE(x0[11], x1[11]) → COND_96_0_REC_GE1(&&(>(x1[11], 99), >(x0[11], 1)), x0[11], x1[11]), COND_96_0_REC_GE1(TRUE, x0[12], x1[12]) → 96_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] ⇒ 96_0_REC_GE(x0[11], x1[11])≥NonInfC∧96_0_REC_GE(x0[11], x1[11])≥COND_96_0_REC_GE1(&&(>(x1[11], 99), >(x0[11], 1)), x0[11], x1[11])∧(U^Increasing(COND_96_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 ⇒ 96_0_REC_GE(x0[11], x1[11])≥NonInfC∧96_0_REC_GE(x0[11], x1[11])≥COND_96_0_REC_GE1(&&(>(x1[11], 99), >(x0[11], 1)), x0[11], x1[11])∧(U^Increasing(COND_96_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_96_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_96_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_96_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_96_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_96_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_96_0_REC_GE1(TRUE, x0, x1) → 96_0_REC_GE(-(x0, 1), -(x0, 1)) the following chains were created:

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

  (68)    (COND_96_0_REC_GE1(TRUE, x0[12], x1[12])≥NonInfC∧COND_96_0_REC_GE1(TRUE, x0[12], x1[12])≥96_0_REC_GE(-(x0[12], 1), -(x0[12], 1))∧(U^Increasing(96_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(96_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(96_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(96_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(96_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.

• 96_0_REC_GE(x0, x1) → COND_96_0_REC_GE(<(x1, 100), x0, x1)
  
  • ([99] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_96_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] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_96_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_96_0_REC_GE(TRUE, x0, x1) → 113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1), x0, x1)
  
  • ((U^Increasing(113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_41] = 0∧0 = 0∧0 = 0∧[(-1)bso_42] ≥ 0)
    
  
  
• 113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0, x1) → 270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1), x0, x1)
  
  • ((U^Increasing(270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2])), ≥)∧[bni_43] = 0∧0 = 0∧0 = 0∧[(-1)bso_44] ≥ 0)
    
  
  
• 270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0, x1) → 301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1), x0, x1)
  
  • ((U^Increasing(301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3])), ≥)∧[bni_45] = 0∧0 = 0∧0 = 0∧[(-1)bso_46] ≥ 0)
    
  
  
• 301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0, x1) → 319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1), x0, x1)
  
  • ((U^Increasing(319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4])), ≥)∧[bni_47] = 0∧0 = 0∧0 = 0∧[(-1)bso_48] ≥ 0)
    
  
  
• 319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0, x1) → 336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1), x0, x1)
  
  • ((U^Increasing(336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5])), ≥)∧[bni_49] = 0∧0 = 0∧0 = 0∧[(-1)bso_50] ≥ 0)
    
  
  
• 336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0, x1) → 353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1), x0, x1)
  
  • ((U^Increasing(353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6])), ≥)∧[bni_51] = 0∧0 = 0∧0 = 0∧[(-1)bso_52] ≥ 0)
    
  
  
• 353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0, x1) → 370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1), x0, x1)
  
  • ((U^Increasing(370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7])), ≥)∧[bni_53] = 0∧0 = 0∧0 = 0∧[(-1)bso_54] ≥ 0)
    
  
  
• 370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0, x1) → 387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1), x0, x1)
  
  • ((U^Increasing(387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8])), ≥)∧[bni_55] = 0∧0 = 0∧0 = 0∧[(-1)bso_56] ≥ 0)
    
  
  
• 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0, x1) → COND_387_1_TEST_INVOKEMETHOD(>(x1, 0), 215_0_descend_Return, x0, x1)
  
  • (x1[9] ≥ 0 ⇒ (U^Increasing(COND_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_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_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0, x1) → 96_0_REC_GE(x0, +(x1, 1))
  
  • ((U^Increasing(96_0_REC_GE(x0[10], +(x1[10], 1))), ≥)∧[bni_59] = 0∧0 = 0∧0 = 0∧[(-1)bso_60] ≥ 0)
    
  
  
• 96_0_REC_GE(x0, x1) → COND_96_0_REC_GE1(&&(>(x1, 99), >(x0, 1)), x0, x1)
  
  • (x1[11] ≥ 0∧x0[11] ≥ 0 ⇒ (U^Increasing(COND_96_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_96_0_REC_GE1(TRUE, x0, x1) → 96_0_REC_GE(-(x0, 1), -(x0, 1))
  
  • ((U^Increasing(96_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(113_0_descend_Load(x₁)) = [-1]   
POL(210_0_descend_LE(x₁)) = [-1]   
POL(0) = 0   
POL(215_0_descend_Return) = [-1]   
POL(Cond_210_0_descend_LE(x₁, x₂)) = [-1]   
POL(>(x₁, x₂)) = [-1]   
POL(229_1_descend_InvokeMethod(x₁, x₂)) = [-1]   
POL(-(x₁, x₂)) = x₁ + [-1]x₂   
POL(1) = [1]   
POL(111_1_rec_InvokeMethod(x₁, x₂)) = [-1]   
POL(96_0_REC_GE(x₁, x₂)) = [-1] + x₁   
POL(COND_96_0_REC_GE(x₁, x₂, x₃)) = [-1] + x₂   
POL(<(x₁, x₂)) = [-1]   
POL(100) = [100]   
POL(113_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + x₂   
POL(270_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + x₂   
POL(301_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + x₂   
POL(319_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = x₁ + x₂   
POL(336_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + x₂   
POL(353_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + x₂   
POL(370_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + x₂   
POL(387_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + x₂   
POL(COND_387_1_TEST_INVOKEMETHOD(x₁, x₂, x₃, x₄)) = [-1] + x₃   
POL(+(x₁, x₂)) = x₁ + x₂   
POL(COND_96_0_REC_GE1(x₁, x₂, x₃)) = [-1] + x₂   
POL(&&(x₁, x₂)) = [-1]   
POL(99) = [99]   

The following pairs are in P_>:

COND_96_0_REC_GE1(TRUE, x0[12], x1[12]) → 96_0_REC_GE(-(x0[12], 1), -(x0[12], 1))

The following pairs are in P_bound:

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

The following pairs are in P_≥:

96_0_REC_GE(x0[0], x1[0]) → COND_96_0_REC_GE(<(x1[0], 100), x0[0], x1[0])
COND_96_0_REC_GE(TRUE, x0[1], x1[1]) → 113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[1]), x0[1], x1[1])
113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2]) → 270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2])
270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3]) → 301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3])
301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4]) → 319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4])
319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5]) → 336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5])
336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6]) → 353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6])
353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7]) → 370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7])
370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8]) → 387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8])
387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9]) → COND_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_0_descend_Return, x0[9], x1[9])
COND_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0[10], x1[10]) → 96_0_REC_GE(x0[10], +(x1[10], 1))
96_0_REC_GE(x0[11], x1[11]) → COND_96_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:

113_0_descend_Load(x0)¹ ↔ 210_0_descend_LE(x0)¹
210_0_descend_LE(0)¹ ↔ 215_0_descend_Return¹
210_0_descend_LE(x0)¹ ↔ Cond_210_0_descend_LE(>(x0, 0), x0)¹
Cond_210_0_descend_LE(TRUE, x0)¹ ↔ 229_1_descend_InvokeMethod(210_0_descend_LE(-(x0, 1)), -(x0, 1))¹
229_1_descend_InvokeMethod(215_0_descend_Return, 0)¹ ↔ 215_0_descend_Return¹
229_1_descend_InvokeMethod(215_0_descend_Return, x0)¹ ↔ 215_0_descend_Return¹

(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:
113_0_descend_Load(x0) → 210_0_descend_LE(x0)
210_0_descend_LE(0) → 215_0_descend_Return
210_0_descend_LE(x0) → Cond_210_0_descend_LE(x0 > 0, x0)
Cond_210_0_descend_LE(TRUE, x0) → 229_1_descend_InvokeMethod(210_0_descend_LE(x0 - 1), x0 - 1)
229_1_descend_InvokeMethod(215_0_descend_Return, 0) → 215_0_descend_Return
229_1_descend_InvokeMethod(215_0_descend_Return, x0) → 215_0_descend_Return
111_1_rec_InvokeMethod(215_0_descend_Return, 0) → 215_0_descend_Return
111_1_rec_InvokeMethod(215_0_descend_Return, x0) → 215_0_descend_Return

The integer pair graph contains the following rules and edges:
(0): 96_0_REC_GE(x0[0], x1[0]) → COND_96_0_REC_GE(x1[0] < 100, x0[0], x1[0])
(1): COND_96_0_REC_GE(TRUE, x0[1], x1[1]) → 113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[1]), x0[1], x1[1])
(2): 113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2]) → 270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2])
(3): 270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3]) → 301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3])
(4): 301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4]) → 319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4])
(5): 319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5]) → 336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5])
(6): 336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6]) → 353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6])
(7): 353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7]) → 370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7])
(8): 370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8]) → 387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8])
(9): 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9]) → COND_387_1_TEST_INVOKEMETHOD(x1[9] > 0, 215_0_descend_Return, x0[9], x1[9])
(10): COND_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0[10], x1[10]) → 96_0_REC_GE(x0[10], x1[10] + 1)
(11): 96_0_REC_GE(x0[11], x1[11]) → COND_96_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 (113_0_descend_Load(x1[1]) →^* 215_0_descend_Return∧x0[1] →^* x0[2]∧x1[1] →^* x1[2])

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

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

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

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

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

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

(8) -> (9), if (113_0_descend_Load(x1[8]) →^* 215_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:
113_0_descend_Load(x0)
210_0_descend_LE(x0)
Cond_210_0_descend_LE(TRUE, x0)
229_1_descend_InvokeMethod(215_0_descend_Return, x0)
111_1_rec_InvokeMethod(215_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:
113_0_descend_Load(x0) → 210_0_descend_LE(x0)
210_0_descend_LE(0) → 215_0_descend_Return
210_0_descend_LE(x0) → Cond_210_0_descend_LE(x0 > 0, x0)
Cond_210_0_descend_LE(TRUE, x0) → 229_1_descend_InvokeMethod(210_0_descend_LE(x0 - 1), x0 - 1)
229_1_descend_InvokeMethod(215_0_descend_Return, 0) → 215_0_descend_Return
229_1_descend_InvokeMethod(215_0_descend_Return, x0) → 215_0_descend_Return
111_1_rec_InvokeMethod(215_0_descend_Return, 0) → 215_0_descend_Return
111_1_rec_InvokeMethod(215_0_descend_Return, x0) → 215_0_descend_Return

The integer pair graph contains the following rules and edges:
(10): COND_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0[10], x1[10]) → 96_0_REC_GE(x0[10], x1[10] + 1)
(9): 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9]) → COND_387_1_TEST_INVOKEMETHOD(x1[9] > 0, 215_0_descend_Return, x0[9], x1[9])
(8): 370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8]) → 387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8])
(7): 353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7]) → 370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7])
(6): 336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6]) → 353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6])
(5): 319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5]) → 336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5])
(4): 301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4]) → 319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4])
(3): 270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3]) → 301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3])
(2): 113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2]) → 270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2])
(1): COND_96_0_REC_GE(TRUE, x0[1], x1[1]) → 113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[1]), x0[1], x1[1])
(0): 96_0_REC_GE(x0[0], x1[0]) → COND_96_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 (113_0_descend_Load(x1[1]) →^* 215_0_descend_Return∧x0[1] →^* x0[2]∧x1[1] →^* x1[2])

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

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

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

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

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

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

(8) -> (9), if (113_0_descend_Load(x1[8]) →^* 215_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:
113_0_descend_Load(x0)
210_0_descend_LE(x0)
Cond_210_0_descend_LE(TRUE, x0)
229_1_descend_InvokeMethod(215_0_descend_Return, x0)
111_1_rec_InvokeMethod(215_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:
113_0_descend_Load(x0) → 210_0_descend_LE(x0)
210_0_descend_LE(0) → 215_0_descend_Return
210_0_descend_LE(x0) → Cond_210_0_descend_LE(x0 > 0, x0)
Cond_210_0_descend_LE(TRUE, x0) → 229_1_descend_InvokeMethod(210_0_descend_LE(x0 - 1), x0 - 1)
229_1_descend_InvokeMethod(215_0_descend_Return, 0) → 215_0_descend_Return
229_1_descend_InvokeMethod(215_0_descend_Return, x0) → 215_0_descend_Return

The integer pair graph contains the following rules and edges:
(10): COND_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0[10], x1[10]) → 96_0_REC_GE(x0[10], x1[10] + 1)
(9): 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9]) → COND_387_1_TEST_INVOKEMETHOD(x1[9] > 0, 215_0_descend_Return, x0[9], x1[9])
(8): 370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8]) → 387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8])
(7): 353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7]) → 370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7])
(6): 336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6]) → 353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6])
(5): 319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5]) → 336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5])
(4): 301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4]) → 319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4])
(3): 270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3]) → 301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3])
(2): 113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2]) → 270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2])
(1): COND_96_0_REC_GE(TRUE, x0[1], x1[1]) → 113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[1]), x0[1], x1[1])
(0): 96_0_REC_GE(x0[0], x1[0]) → COND_96_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 (113_0_descend_Load(x1[1]) →^* 215_0_descend_Return∧x0[1] →^* x0[2]∧x1[1] →^* x1[2])

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

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

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

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

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

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

(8) -> (9), if (113_0_descend_Load(x1[8]) →^* 215_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:
113_0_descend_Load(x0)
210_0_descend_LE(x0)
Cond_210_0_descend_LE(TRUE, x0)
229_1_descend_InvokeMethod(215_0_descend_Return, x0)
111_1_rec_InvokeMethod(215_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@74cc39fe 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_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0[10], x1[10]) → 96_0_REC_GE(x0[10], +(x1[10], 1)) the following chains were created:

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

  (1)    (COND_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0[10], x1[10])≥NonInfC∧COND_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0[10], x1[10])≥96_0_REC_GE(x0[10], +(x1[10], 1))∧(U^Increasing(96_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(96_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(96_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(96_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(96_0_REC_GE(x0[10], +(x1[10], 1))), ≥)∧[bni_21] = 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)

  
  
  

For Pair 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9]) → COND_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_0_descend_Return, x0[9], x1[9]) the following chains were created:

• We consider the chain 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9]) → COND_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_0_descend_Return, x0[9], x1[9]), COND_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0[10], x1[10]) → 96_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] ⇒ 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9])≥NonInfC∧387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9])≥COND_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_0_descend_Return, x0[9], x1[9])∧(U^Increasing(COND_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_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 ⇒ 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9])≥NonInfC∧387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9])≥COND_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_0_descend_Return, x0[9], x1[9])∧(U^Increasing(COND_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_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_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_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_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_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_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_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_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_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 370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8]) → 387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8]) the following chains were created:

• We consider the chain 370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8]) → 387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8]) which results in the following constraint:
  

  (12)    (370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8])≥NonInfC∧370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8])≥387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8])∧(U^Increasing(387_1_TEST_INVOKEMETHOD(113_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(387_1_TEST_INVOKEMETHOD(113_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(387_1_TEST_INVOKEMETHOD(113_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(387_1_TEST_INVOKEMETHOD(113_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(387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8])), ≥)∧[bni_25] = 0∧0 = 0∧[(-1)bso_26] ≥ 0)

  
  
  

For Pair 353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7]) → 370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7]) the following chains were created:

• We consider the chain 353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7]) → 370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7]) which results in the following constraint:
  

  (17)    (353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7])≥NonInfC∧353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7])≥370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7])∧(U^Increasing(370_1_TEST_INVOKEMETHOD(113_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(370_1_TEST_INVOKEMETHOD(113_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(370_1_TEST_INVOKEMETHOD(113_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(370_1_TEST_INVOKEMETHOD(113_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(370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7])), ≥)∧[bni_27] = 0∧0 = 0∧[(-1)bso_28] ≥ 0)

  
  
  

For Pair 336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6]) → 353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6]) the following chains were created:

• We consider the chain 336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6]) → 353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6]) which results in the following constraint:
  

  (22)    (336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6])≥NonInfC∧336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6])≥353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6])∧(U^Increasing(353_1_TEST_INVOKEMETHOD(113_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(353_1_TEST_INVOKEMETHOD(113_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(353_1_TEST_INVOKEMETHOD(113_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(353_1_TEST_INVOKEMETHOD(113_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(353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6])), ≥)∧[bni_29] = 0∧0 = 0∧[(-1)bso_30] ≥ 0)

  
  
  

For Pair 319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5]) → 336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5]) the following chains were created:

• We consider the chain 319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5]) → 336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5]) which results in the following constraint:
  

  (27)    (319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5])≥NonInfC∧319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5])≥336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5])∧(U^Increasing(336_1_TEST_INVOKEMETHOD(113_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(336_1_TEST_INVOKEMETHOD(113_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(336_1_TEST_INVOKEMETHOD(113_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(336_1_TEST_INVOKEMETHOD(113_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(336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5])), ≥)∧[bni_31] = 0∧0 = 0∧[(-1)bso_32] ≥ 0)

  
  
  

For Pair 301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4]) → 319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4]) the following chains were created:

• We consider the chain 301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4]) → 319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4]) which results in the following constraint:
  

  (32)    (301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4])≥NonInfC∧301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4])≥319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4])∧(U^Increasing(319_1_TEST_INVOKEMETHOD(113_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(319_1_TEST_INVOKEMETHOD(113_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(319_1_TEST_INVOKEMETHOD(113_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(319_1_TEST_INVOKEMETHOD(113_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(319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4])), ≥)∧[bni_33] = 0∧0 = 0∧[(-1)bso_34] ≥ 0)

  
  
  

For Pair 270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3]) → 301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3]) the following chains were created:

• We consider the chain 270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3]) → 301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3]) which results in the following constraint:
  

  (37)    (270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3])≥NonInfC∧270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3])≥301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3])∧(U^Increasing(301_1_TEST_INVOKEMETHOD(113_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(301_1_TEST_INVOKEMETHOD(113_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(301_1_TEST_INVOKEMETHOD(113_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(301_1_TEST_INVOKEMETHOD(113_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(301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3])), ≥)∧[bni_35] = 0∧0 = 0∧[(-1)bso_36] ≥ 0)

  
  
  

For Pair 113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2]) → 270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2]) the following chains were created:

• We consider the chain 113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2]) → 270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2]) which results in the following constraint:
  

  (42)    (113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2])≥NonInfC∧113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2])≥270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2])∧(U^Increasing(270_1_TEST_INVOKEMETHOD(113_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(270_1_TEST_INVOKEMETHOD(113_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(270_1_TEST_INVOKEMETHOD(113_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(270_1_TEST_INVOKEMETHOD(113_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(270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2])), ≥)∧[bni_37] = 0∧0 = 0∧[(-1)bso_38] ≥ 0)

  
  
  

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

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

  (47)    (COND_96_0_REC_GE(TRUE, x0[1], x1[1])≥NonInfC∧COND_96_0_REC_GE(TRUE, x0[1], x1[1])≥113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[1]), x0[1], x1[1])∧(U^Increasing(113_1_TEST_INVOKEMETHOD(113_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(113_1_TEST_INVOKEMETHOD(113_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(113_1_TEST_INVOKEMETHOD(113_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(113_1_TEST_INVOKEMETHOD(113_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(113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_39] = 0∧0 = 0∧[(-1)bso_40] ≥ 0)

  
  
  

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

• We consider the chain 96_0_REC_GE(x0[0], x1[0]) → COND_96_0_REC_GE(<(x1[0], 100), x0[0], x1[0]), COND_96_0_REC_GE(TRUE, x0[1], x1[1]) → 113_1_TEST_INVOKEMETHOD(113_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] ⇒ 96_0_REC_GE(x0[0], x1[0])≥NonInfC∧96_0_REC_GE(x0[0], x1[0])≥COND_96_0_REC_GE(<(x1[0], 100), x0[0], x1[0])∧(U^Increasing(COND_96_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 ⇒ 96_0_REC_GE(x0[0], x1[0])≥NonInfC∧96_0_REC_GE(x0[0], x1[0])≥COND_96_0_REC_GE(<(x1[0], 100), x0[0], x1[0])∧(U^Increasing(COND_96_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_96_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_96_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_96_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_96_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_96_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_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0[10], x1[10]) → 96_0_REC_GE(x0[10], +(x1[10], 1))
  
  • ((U^Increasing(96_0_REC_GE(x0[10], +(x1[10], 1))), ≥)∧[bni_21] = 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)
    
  
  
• 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9]) → COND_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_0_descend_Return, x0[9], x1[9])
  
  • (x1[9] ≥ 0 ⇒ (U^Increasing(COND_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_0_descend_Return, x0[9], x1[9])), ≥)∧[(-2)bni_23 + (-1)Bound*bni_23] + [(-1)bni_23]x1[9] ≥ 0∧[(-1)bso_24] ≥ 0)
    
  
  
• 370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8]) → 387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8])
  
  • ((U^Increasing(387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8])), ≥)∧[bni_25] = 0∧0 = 0∧[(-1)bso_26] ≥ 0)
    
  
  
• 353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7]) → 370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7])
  
  • ((U^Increasing(370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7])), ≥)∧[bni_27] = 0∧0 = 0∧[(-1)bso_28] ≥ 0)
    
  
  
• 336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6]) → 353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6])
  
  • ((U^Increasing(353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6])), ≥)∧[bni_29] = 0∧0 = 0∧[(-1)bso_30] ≥ 0)
    
  
  
• 319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5]) → 336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5])
  
  • ((U^Increasing(336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5])), ≥)∧[bni_31] = 0∧0 = 0∧[(-1)bso_32] ≥ 0)
    
  
  
• 301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4]) → 319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4])
  
  • ((U^Increasing(319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4])), ≥)∧[bni_33] = 0∧0 = 0∧[(-1)bso_34] ≥ 0)
    
  
  
• 270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3]) → 301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3])
  
  • ((U^Increasing(301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3])), ≥)∧[bni_35] = 0∧0 = 0∧[(-1)bso_36] ≥ 0)
    
  
  
• 113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2]) → 270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2])
  
  • ((U^Increasing(270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2])), ≥)∧[bni_37] = 0∧0 = 0∧[(-1)bso_38] ≥ 0)
    
  
  
• COND_96_0_REC_GE(TRUE, x0[1], x1[1]) → 113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[1]), x0[1], x1[1])
  
  • ((U^Increasing(113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_39] = 0∧0 = 0∧[(-1)bso_40] ≥ 0)
    
  
  
• 96_0_REC_GE(x0[0], x1[0]) → COND_96_0_REC_GE(<(x1[0], 100), x0[0], x1[0])
  
  • ([99] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_96_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_96_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(113_0_descend_Load(x₁)) = [-1] + x₁   
POL(210_0_descend_LE(x₁)) = [1] + [-1]x₁   
POL(0) = 0   
POL(215_0_descend_Return) = [-1]   
POL(Cond_210_0_descend_LE(x₁, x₂)) = [-1] + [-1]x₂   
POL(>(x₁, x₂)) = [-1]   
POL(229_1_descend_InvokeMethod(x₁, x₂)) = [1] + [-1]x₂ + [-1]x₁   
POL(-(x₁, x₂)) = x₁ + [-1]x₂   
POL(1) = [1]   
POL(COND_387_1_TEST_INVOKEMETHOD(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₄   
POL(96_0_REC_GE(x₁, x₂)) = [-1] + [-1]x₂   
POL(+(x₁, x₂)) = x₁ + x₂   
POL(387_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(370_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(353_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(336_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(319_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(301_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(270_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(113_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(COND_96_0_REC_GE(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(<(x₁, x₂)) = [-1]   
POL(100) = [100]   

The following pairs are in P_>:

COND_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0[10], x1[10]) → 96_0_REC_GE(x0[10], +(x1[10], 1))

The following pairs are in P_bound:

96_0_REC_GE(x0[0], x1[0]) → COND_96_0_REC_GE(<(x1[0], 100), x0[0], x1[0])

The following pairs are in P_≥:

387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9]) → COND_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_0_descend_Return, x0[9], x1[9])
370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8]) → 387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8])
353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7]) → 370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7])
336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6]) → 353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6])
319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5]) → 336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5])
301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4]) → 319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4])
270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3]) → 301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3])
113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2]) → 270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2])
COND_96_0_REC_GE(TRUE, x0[1], x1[1]) → 113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[1]), x0[1], x1[1])
96_0_REC_GE(x0[0], x1[0]) → COND_96_0_REC_GE(<(x1[0], 100), x0[0], x1[0])

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

210_0_descend_LE(x0)¹ → Cond_210_0_descend_LE(>(x0, 0), x0)¹

(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:
113_0_descend_Load(x0) → 210_0_descend_LE(x0)
210_0_descend_LE(0) → 215_0_descend_Return
210_0_descend_LE(x0) → Cond_210_0_descend_LE(x0 > 0, x0)
Cond_210_0_descend_LE(TRUE, x0) → 229_1_descend_InvokeMethod(210_0_descend_LE(x0 - 1), x0 - 1)
229_1_descend_InvokeMethod(215_0_descend_Return, 0) → 215_0_descend_Return
229_1_descend_InvokeMethod(215_0_descend_Return, x0) → 215_0_descend_Return

The integer pair graph contains the following rules and edges:
(9): 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9]) → COND_387_1_TEST_INVOKEMETHOD(x1[9] > 0, 215_0_descend_Return, x0[9], x1[9])
(8): 370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8]) → 387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8])
(7): 353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7]) → 370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7])
(6): 336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6]) → 353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6])
(5): 319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5]) → 336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5])
(4): 301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4]) → 319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4])
(3): 270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3]) → 301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3])
(2): 113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2]) → 270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2])
(1): COND_96_0_REC_GE(TRUE, x0[1], x1[1]) → 113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[1]), x0[1], x1[1])
(0): 96_0_REC_GE(x0[0], x1[0]) → COND_96_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 (113_0_descend_Load(x1[1]) →^* 215_0_descend_Return∧x0[1] →^* x0[2]∧x1[1] →^* x1[2])

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

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

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

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

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

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

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

The set Q consists of the following terms:
113_0_descend_Load(x0)
210_0_descend_LE(x0)
Cond_210_0_descend_LE(TRUE, x0)
229_1_descend_InvokeMethod(215_0_descend_Return, x0)
111_1_rec_InvokeMethod(215_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:
113_0_descend_Load(x0) → 210_0_descend_LE(x0)
210_0_descend_LE(0) → 215_0_descend_Return
210_0_descend_LE(x0) → Cond_210_0_descend_LE(x0 > 0, x0)
Cond_210_0_descend_LE(TRUE, x0) → 229_1_descend_InvokeMethod(210_0_descend_LE(x0 - 1), x0 - 1)
229_1_descend_InvokeMethod(215_0_descend_Return, 0) → 215_0_descend_Return
229_1_descend_InvokeMethod(215_0_descend_Return, x0) → 215_0_descend_Return

The integer pair graph contains the following rules and edges:
(10): COND_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0[10], x1[10]) → 96_0_REC_GE(x0[10], x1[10] + 1)
(9): 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9]) → COND_387_1_TEST_INVOKEMETHOD(x1[9] > 0, 215_0_descend_Return, x0[9], x1[9])
(8): 370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8]) → 387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8])
(7): 353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7]) → 370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7])
(6): 336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6]) → 353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6])
(5): 319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5]) → 336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5])
(4): 301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4]) → 319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4])
(3): 270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3]) → 301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3])
(2): 113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2]) → 270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2])
(1): COND_96_0_REC_GE(TRUE, x0[1], x1[1]) → 113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[1]), x0[1], x1[1])

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

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

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

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

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

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

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

(8) -> (9), if (113_0_descend_Load(x1[8]) →^* 215_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:
113_0_descend_Load(x0)
210_0_descend_LE(x0)
Cond_210_0_descend_LE(TRUE, x0)
229_1_descend_InvokeMethod(215_0_descend_Return, x0)
111_1_rec_InvokeMethod(215_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:
113_0_descend_Load(x0) → 210_0_descend_LE(x0)
210_0_descend_LE(0) → 215_0_descend_Return
210_0_descend_LE(x0) → Cond_210_0_descend_LE(x0 > 0, x0)
Cond_210_0_descend_LE(TRUE, x0) → 229_1_descend_InvokeMethod(210_0_descend_LE(x0 - 1), x0 - 1)
229_1_descend_InvokeMethod(215_0_descend_Return, 0) → 215_0_descend_Return
229_1_descend_InvokeMethod(215_0_descend_Return, x0) → 215_0_descend_Return
111_1_rec_InvokeMethod(215_0_descend_Return, 0) → 215_0_descend_Return
111_1_rec_InvokeMethod(215_0_descend_Return, x0) → 215_0_descend_Return

The integer pair graph contains the following rules and edges:
(0): 96_0_REC_GE(x0[0], x1[0]) → COND_96_0_REC_GE(x1[0] < 100, x0[0], x1[0])
(1): COND_96_0_REC_GE(TRUE, x0[1], x1[1]) → 113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[1]), x0[1], x1[1])
(2): 113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2]) → 270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2])
(3): 270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3]) → 301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3])
(4): 301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4]) → 319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4])
(5): 319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5]) → 336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5])
(6): 336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6]) → 353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6])
(7): 353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7]) → 370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7])
(8): 370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8]) → 387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8])
(9): 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9]) → COND_387_1_TEST_INVOKEMETHOD(x1[9] > 0, 215_0_descend_Return, x0[9], x1[9])
(10): COND_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0[10], x1[10]) → 96_0_REC_GE(x0[10], x1[10] + 1)
(12): COND_96_0_REC_GE1(TRUE, x0[12], x1[12]) → 96_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 (113_0_descend_Load(x1[1]) →^* 215_0_descend_Return∧x0[1] →^* x0[2]∧x1[1] →^* x1[2])

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

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

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

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

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

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

(8) -> (9), if (113_0_descend_Load(x1[8]) →^* 215_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:
113_0_descend_Load(x0)
210_0_descend_LE(x0)
Cond_210_0_descend_LE(TRUE, x0)
229_1_descend_InvokeMethod(215_0_descend_Return, x0)
111_1_rec_InvokeMethod(215_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:
113_0_descend_Load(x0) → 210_0_descend_LE(x0)
210_0_descend_LE(0) → 215_0_descend_Return
210_0_descend_LE(x0) → Cond_210_0_descend_LE(x0 > 0, x0)
Cond_210_0_descend_LE(TRUE, x0) → 229_1_descend_InvokeMethod(210_0_descend_LE(x0 - 1), x0 - 1)
229_1_descend_InvokeMethod(215_0_descend_Return, 0) → 215_0_descend_Return
229_1_descend_InvokeMethod(215_0_descend_Return, x0) → 215_0_descend_Return
111_1_rec_InvokeMethod(215_0_descend_Return, 0) → 215_0_descend_Return
111_1_rec_InvokeMethod(215_0_descend_Return, x0) → 215_0_descend_Return

The integer pair graph contains the following rules and edges:
(10): COND_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0[10], x1[10]) → 96_0_REC_GE(x0[10], x1[10] + 1)
(9): 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9]) → COND_387_1_TEST_INVOKEMETHOD(x1[9] > 0, 215_0_descend_Return, x0[9], x1[9])
(8): 370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8]) → 387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8])
(7): 353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7]) → 370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7])
(6): 336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6]) → 353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6])
(5): 319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5]) → 336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5])
(4): 301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4]) → 319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4])
(3): 270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3]) → 301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3])
(2): 113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2]) → 270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2])
(1): COND_96_0_REC_GE(TRUE, x0[1], x1[1]) → 113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[1]), x0[1], x1[1])
(0): 96_0_REC_GE(x0[0], x1[0]) → COND_96_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 (113_0_descend_Load(x1[1]) →^* 215_0_descend_Return∧x0[1] →^* x0[2]∧x1[1] →^* x1[2])

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

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

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

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

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

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

(8) -> (9), if (113_0_descend_Load(x1[8]) →^* 215_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:
113_0_descend_Load(x0)
210_0_descend_LE(x0)
Cond_210_0_descend_LE(TRUE, x0)
229_1_descend_InvokeMethod(215_0_descend_Return, x0)
111_1_rec_InvokeMethod(215_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:
113_0_descend_Load(x0) → 210_0_descend_LE(x0)
210_0_descend_LE(0) → 215_0_descend_Return
210_0_descend_LE(x0) → Cond_210_0_descend_LE(x0 > 0, x0)
Cond_210_0_descend_LE(TRUE, x0) → 229_1_descend_InvokeMethod(210_0_descend_LE(x0 - 1), x0 - 1)
229_1_descend_InvokeMethod(215_0_descend_Return, 0) → 215_0_descend_Return
229_1_descend_InvokeMethod(215_0_descend_Return, x0) → 215_0_descend_Return

The integer pair graph contains the following rules and edges:
(10): COND_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0[10], x1[10]) → 96_0_REC_GE(x0[10], x1[10] + 1)
(9): 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9]) → COND_387_1_TEST_INVOKEMETHOD(x1[9] > 0, 215_0_descend_Return, x0[9], x1[9])
(8): 370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8]) → 387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8])
(7): 353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7]) → 370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7])
(6): 336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6]) → 353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6])
(5): 319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5]) → 336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5])
(4): 301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4]) → 319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4])
(3): 270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3]) → 301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3])
(2): 113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2]) → 270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2])
(1): COND_96_0_REC_GE(TRUE, x0[1], x1[1]) → 113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[1]), x0[1], x1[1])
(0): 96_0_REC_GE(x0[0], x1[0]) → COND_96_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 (113_0_descend_Load(x1[1]) →^* 215_0_descend_Return∧x0[1] →^* x0[2]∧x1[1] →^* x1[2])

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

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

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

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

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

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

(8) -> (9), if (113_0_descend_Load(x1[8]) →^* 215_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:
113_0_descend_Load(x0)
210_0_descend_LE(x0)
Cond_210_0_descend_LE(TRUE, x0)
229_1_descend_InvokeMethod(215_0_descend_Return, x0)
111_1_rec_InvokeMethod(215_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@74cc39fe 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_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0[10], x1[10]) → 96_0_REC_GE(x0[10], +(x1[10], 1)) the following chains were created:

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

  (1)    (COND_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0[10], x1[10])≥NonInfC∧COND_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0[10], x1[10])≥96_0_REC_GE(x0[10], +(x1[10], 1))∧(U^Increasing(96_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(96_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(96_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(96_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(96_0_REC_GE(x0[10], +(x1[10], 1))), ≥)∧[bni_22] = 0∧0 = 0∧[1 + (-1)bso_23] ≥ 0)

  
  
  

For Pair 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9]) → COND_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_0_descend_Return, x0[9], x1[9]) the following chains were created:

• We consider the chain 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9]) → COND_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_0_descend_Return, x0[9], x1[9]), COND_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0[10], x1[10]) → 96_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] ⇒ 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9])≥NonInfC∧387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9])≥COND_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_0_descend_Return, x0[9], x1[9])∧(U^Increasing(COND_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_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 ⇒ 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9])≥NonInfC∧387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9])≥COND_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_0_descend_Return, x0[9], x1[9])∧(U^Increasing(COND_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_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_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_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_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_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_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_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_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_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 370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8]) → 387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8]) the following chains were created:

• We consider the chain 370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8]) → 387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8]) which results in the following constraint:
  

  (12)    (370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8])≥NonInfC∧370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8])≥387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8])∧(U^Increasing(387_1_TEST_INVOKEMETHOD(113_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(387_1_TEST_INVOKEMETHOD(113_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(387_1_TEST_INVOKEMETHOD(113_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(387_1_TEST_INVOKEMETHOD(113_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(387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8])), ≥)∧[bni_26] = 0∧0 = 0∧[(-1)bso_27] ≥ 0)

  
  
  

For Pair 353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7]) → 370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7]) the following chains were created:

• We consider the chain 353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7]) → 370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7]) which results in the following constraint:
  

  (17)    (353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7])≥NonInfC∧353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7])≥370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7])∧(U^Increasing(370_1_TEST_INVOKEMETHOD(113_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(370_1_TEST_INVOKEMETHOD(113_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(370_1_TEST_INVOKEMETHOD(113_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(370_1_TEST_INVOKEMETHOD(113_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(370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7])), ≥)∧[bni_28] = 0∧0 = 0∧[(-1)bso_29] ≥ 0)

  
  
  

For Pair 336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6]) → 353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6]) the following chains were created:

• We consider the chain 336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6]) → 353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6]) which results in the following constraint:
  

  (22)    (336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6])≥NonInfC∧336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6])≥353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6])∧(U^Increasing(353_1_TEST_INVOKEMETHOD(113_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(353_1_TEST_INVOKEMETHOD(113_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(353_1_TEST_INVOKEMETHOD(113_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(353_1_TEST_INVOKEMETHOD(113_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(353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6])), ≥)∧[bni_30] = 0∧0 = 0∧[(-1)bso_31] ≥ 0)

  
  
  

For Pair 319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5]) → 336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5]) the following chains were created:

• We consider the chain 319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5]) → 336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5]) which results in the following constraint:
  

  (27)    (319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5])≥NonInfC∧319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5])≥336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5])∧(U^Increasing(336_1_TEST_INVOKEMETHOD(113_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(336_1_TEST_INVOKEMETHOD(113_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(336_1_TEST_INVOKEMETHOD(113_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(336_1_TEST_INVOKEMETHOD(113_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(336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5])), ≥)∧[bni_32] = 0∧0 = 0∧[(-1)bso_33] ≥ 0)

  
  
  

For Pair 301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4]) → 319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4]) the following chains were created:

• We consider the chain 301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4]) → 319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4]) which results in the following constraint:
  

  (32)    (301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4])≥NonInfC∧301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4])≥319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4])∧(U^Increasing(319_1_TEST_INVOKEMETHOD(113_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(319_1_TEST_INVOKEMETHOD(113_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(319_1_TEST_INVOKEMETHOD(113_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(319_1_TEST_INVOKEMETHOD(113_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(319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4])), ≥)∧[bni_34] = 0∧0 = 0∧[(-1)bso_35] ≥ 0)

  
  
  

For Pair 270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3]) → 301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3]) the following chains were created:

• We consider the chain 270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3]) → 301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3]) which results in the following constraint:
  

  (37)    (270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3])≥NonInfC∧270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3])≥301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3])∧(U^Increasing(301_1_TEST_INVOKEMETHOD(113_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(301_1_TEST_INVOKEMETHOD(113_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(301_1_TEST_INVOKEMETHOD(113_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(301_1_TEST_INVOKEMETHOD(113_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(301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3])), ≥)∧[bni_36] = 0∧0 = 0∧[(-1)bso_37] ≥ 0)

  
  
  

For Pair 113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2]) → 270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2]) the following chains were created:

• We consider the chain 113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2]) → 270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2]) which results in the following constraint:
  

  (42)    (113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2])≥NonInfC∧113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2])≥270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2])∧(U^Increasing(270_1_TEST_INVOKEMETHOD(113_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(270_1_TEST_INVOKEMETHOD(113_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(270_1_TEST_INVOKEMETHOD(113_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(270_1_TEST_INVOKEMETHOD(113_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(270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2])), ≥)∧[bni_38] = 0∧0 = 0∧[(-1)bso_39] ≥ 0)

  
  
  

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

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

  (47)    (COND_96_0_REC_GE(TRUE, x0[1], x1[1])≥NonInfC∧COND_96_0_REC_GE(TRUE, x0[1], x1[1])≥113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[1]), x0[1], x1[1])∧(U^Increasing(113_1_TEST_INVOKEMETHOD(113_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(113_1_TEST_INVOKEMETHOD(113_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(113_1_TEST_INVOKEMETHOD(113_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(113_1_TEST_INVOKEMETHOD(113_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(113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_40] = 0∧0 = 0∧[(-1)bso_41] ≥ 0)

  
  
  

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

• We consider the chain 96_0_REC_GE(x0[0], x1[0]) → COND_96_0_REC_GE(<(x1[0], 100), x0[0], x1[0]), COND_96_0_REC_GE(TRUE, x0[1], x1[1]) → 113_1_TEST_INVOKEMETHOD(113_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] ⇒ 96_0_REC_GE(x0[0], x1[0])≥NonInfC∧96_0_REC_GE(x0[0], x1[0])≥COND_96_0_REC_GE(<(x1[0], 100), x0[0], x1[0])∧(U^Increasing(COND_96_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 ⇒ 96_0_REC_GE(x0[0], x1[0])≥NonInfC∧96_0_REC_GE(x0[0], x1[0])≥COND_96_0_REC_GE(<(x1[0], 100), x0[0], x1[0])∧(U^Increasing(COND_96_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_96_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_96_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_96_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_96_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_96_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_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0[10], x1[10]) → 96_0_REC_GE(x0[10], +(x1[10], 1))
  
  • ((U^Increasing(96_0_REC_GE(x0[10], +(x1[10], 1))), ≥)∧[bni_22] = 0∧0 = 0∧[1 + (-1)bso_23] ≥ 0)
    
  
  
• 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9]) → COND_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_0_descend_Return, x0[9], x1[9])
  
  • (x1[9] ≥ 0 ⇒ (U^Increasing(COND_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_0_descend_Return, x0[9], x1[9])), ≥)∧[(-2)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]x1[9] ≥ 0∧[(-1)bso_25] ≥ 0)
    
  
  
• 370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8]) → 387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8])
  
  • ((U^Increasing(387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8])), ≥)∧[bni_26] = 0∧0 = 0∧[(-1)bso_27] ≥ 0)
    
  
  
• 353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7]) → 370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7])
  
  • ((U^Increasing(370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7])), ≥)∧[bni_28] = 0∧0 = 0∧[(-1)bso_29] ≥ 0)
    
  
  
• 336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6]) → 353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6])
  
  • ((U^Increasing(353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6])), ≥)∧[bni_30] = 0∧0 = 0∧[(-1)bso_31] ≥ 0)
    
  
  
• 319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5]) → 336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5])
  
  • ((U^Increasing(336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5])), ≥)∧[bni_32] = 0∧0 = 0∧[(-1)bso_33] ≥ 0)
    
  
  
• 301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4]) → 319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4])
  
  • ((U^Increasing(319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4])), ≥)∧[bni_34] = 0∧0 = 0∧[(-1)bso_35] ≥ 0)
    
  
  
• 270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3]) → 301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3])
  
  • ((U^Increasing(301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3])), ≥)∧[bni_36] = 0∧0 = 0∧[(-1)bso_37] ≥ 0)
    
  
  
• 113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2]) → 270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2])
  
  • ((U^Increasing(270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2])), ≥)∧[bni_38] = 0∧0 = 0∧[(-1)bso_39] ≥ 0)
    
  
  
• COND_96_0_REC_GE(TRUE, x0[1], x1[1]) → 113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[1]), x0[1], x1[1])
  
  • ((U^Increasing(113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_40] = 0∧0 = 0∧[(-1)bso_41] ≥ 0)
    
  
  
• 96_0_REC_GE(x0[0], x1[0]) → COND_96_0_REC_GE(<(x1[0], 100), x0[0], x1[0])
  
  • ([99] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_96_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_96_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(113_0_descend_Load(x₁)) = [-1] + [-1]x₁   
POL(210_0_descend_LE(x₁)) = [-1]   
POL(0) = 0   
POL(215_0_descend_Return) = [2]   
POL(Cond_210_0_descend_LE(x₁, x₂)) = [-1]x₂   
POL(>(x₁, x₂)) = [-1]   
POL(229_1_descend_InvokeMethod(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁   
POL(-(x₁, x₂)) = x₁ + [-1]x₂   
POL(1) = [1]   
POL(COND_387_1_TEST_INVOKEMETHOD(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₄   
POL(96_0_REC_GE(x₁, x₂)) = [-1] + [-1]x₂   
POL(+(x₁, x₂)) = x₁ + x₂   
POL(387_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(370_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(353_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(336_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(319_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(301_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(270_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(113_1_TEST_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(COND_96_0_REC_GE(x₁, x₂, x₃)) = [-1] + [-1]x₃   
POL(<(x₁, x₂)) = 0   
POL(100) = [100]   

The following pairs are in P_>:

COND_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0[10], x1[10]) → 96_0_REC_GE(x0[10], +(x1[10], 1))

The following pairs are in P_bound:

96_0_REC_GE(x0[0], x1[0]) → COND_96_0_REC_GE(<(x1[0], 100), x0[0], x1[0])

The following pairs are in P_≥:

387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9]) → COND_387_1_TEST_INVOKEMETHOD(>(x1[9], 0), 215_0_descend_Return, x0[9], x1[9])
370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8]) → 387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8])
353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7]) → 370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7])
336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6]) → 353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6])
319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5]) → 336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5])
301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4]) → 319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4])
270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3]) → 301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3])
113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2]) → 270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2])
COND_96_0_REC_GE(TRUE, x0[1], x1[1]) → 113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[1]), x0[1], x1[1])
96_0_REC_GE(x0[0], x1[0]) → COND_96_0_REC_GE(<(x1[0], 100), x0[0], x1[0])

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

215_0_descend_Return¹ → 210_0_descend_LE(0)¹

(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:
113_0_descend_Load(x0) → 210_0_descend_LE(x0)
210_0_descend_LE(0) → 215_0_descend_Return
210_0_descend_LE(x0) → Cond_210_0_descend_LE(x0 > 0, x0)
Cond_210_0_descend_LE(TRUE, x0) → 229_1_descend_InvokeMethod(210_0_descend_LE(x0 - 1), x0 - 1)
229_1_descend_InvokeMethod(215_0_descend_Return, 0) → 215_0_descend_Return
229_1_descend_InvokeMethod(215_0_descend_Return, x0) → 215_0_descend_Return

The integer pair graph contains the following rules and edges:
(9): 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9]) → COND_387_1_TEST_INVOKEMETHOD(x1[9] > 0, 215_0_descend_Return, x0[9], x1[9])
(8): 370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8]) → 387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8])
(7): 353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7]) → 370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7])
(6): 336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6]) → 353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6])
(5): 319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5]) → 336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5])
(4): 301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4]) → 319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4])
(3): 270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3]) → 301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3])
(2): 113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2]) → 270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2])
(1): COND_96_0_REC_GE(TRUE, x0[1], x1[1]) → 113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[1]), x0[1], x1[1])
(0): 96_0_REC_GE(x0[0], x1[0]) → COND_96_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 (113_0_descend_Load(x1[1]) →^* 215_0_descend_Return∧x0[1] →^* x0[2]∧x1[1] →^* x1[2])

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

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

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

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

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

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

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

The set Q consists of the following terms:
113_0_descend_Load(x0)
210_0_descend_LE(x0)
Cond_210_0_descend_LE(TRUE, x0)
229_1_descend_InvokeMethod(215_0_descend_Return, x0)
111_1_rec_InvokeMethod(215_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:
113_0_descend_Load(x0) → 210_0_descend_LE(x0)
210_0_descend_LE(0) → 215_0_descend_Return
210_0_descend_LE(x0) → Cond_210_0_descend_LE(x0 > 0, x0)
Cond_210_0_descend_LE(TRUE, x0) → 229_1_descend_InvokeMethod(210_0_descend_LE(x0 - 1), x0 - 1)
229_1_descend_InvokeMethod(215_0_descend_Return, 0) → 215_0_descend_Return
229_1_descend_InvokeMethod(215_0_descend_Return, x0) → 215_0_descend_Return

The integer pair graph contains the following rules and edges:
(10): COND_387_1_TEST_INVOKEMETHOD(TRUE, 215_0_descend_Return, x0[10], x1[10]) → 96_0_REC_GE(x0[10], x1[10] + 1)
(9): 387_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[9], x1[9]) → COND_387_1_TEST_INVOKEMETHOD(x1[9] > 0, 215_0_descend_Return, x0[9], x1[9])
(8): 370_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[8], x1[8]) → 387_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[8]), x0[8], x1[8])
(7): 353_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[7], x1[7]) → 370_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[7]), x0[7], x1[7])
(6): 336_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[6], x1[6]) → 353_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[6]), x0[6], x1[6])
(5): 319_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[5], x1[5]) → 336_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[5]), x0[5], x1[5])
(4): 301_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[4], x1[4]) → 319_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[4]), x0[4], x1[4])
(3): 270_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[3], x1[3]) → 301_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[3]), x0[3], x1[3])
(2): 113_1_TEST_INVOKEMETHOD(215_0_descend_Return, x0[2], x1[2]) → 270_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[2]), x0[2], x1[2])
(1): COND_96_0_REC_GE(TRUE, x0[1], x1[1]) → 113_1_TEST_INVOKEMETHOD(113_0_descend_Load(x1[1]), x0[1], x1[1])

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

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

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

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

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

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

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

(8) -> (9), if (113_0_descend_Load(x1[8]) →^* 215_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:
113_0_descend_Load(x0)
210_0_descend_LE(x0)
Cond_210_0_descend_LE(TRUE, x0)
229_1_descend_InvokeMethod(215_0_descend_Return, x0)
111_1_rec_InvokeMethod(215_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