Termination proof of /tmp/tmpJj9TrK/Avg.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 180 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 JBCTerminationSCC

↳5 SCCToIDPv1Proof (⇒, 510 ms)

↳6 IDP

↳7 IDPNonInfProof (⇒, 160 ms)

↳8 AND

    ↳9 IDP

        ↳10 IDependencyGraphProof (⇔, 0 ms)

        ↳11 IDP

        ↳12 UsableRulesProof (⇔, 0 ms)

        ↳13 IDP

        ↳14 IDPNonInfProof (⇒, 0 ms)

        ↳15 AND

            ↳16 IDP

                ↳17 IDependencyGraphProof (⇔, 0 ms)

                ↳18 TRUE

            ↳19 IDP

                ↳20 IDependencyGraphProof (⇔, 0 ms)

                ↳21 TRUE

    ↳22 IDP

        ↳23 IDependencyGraphProof (⇔, 0 ms)

        ↳24 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_22 (Sun Microsystems Inc.) Main-Class: Avg

public class Avg {
	public static void main(String[] args) {
		int x, y;
		x = args[0].length();
		y = args[1].length();
		average(x,y);
	}

	public static int average(int x, int y) {
		if (x > 0) {
			return average(x-1, y+1);
		} else if (y > 2) {
			return 1 + average(x+1, y-2);
		} else {
			return 1;
		}
	}
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

Avg.average(II)I: Graph of 64 nodes with 0 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 1 SCCs.

(4) Obligation:

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

(5) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 28 rules for P and 46 rules for R.

P rules:
251_0_average_LE(EOS(STATIC_251), matching1, i37, matching2) → 257_0_average_LE(EOS(STATIC_257), 0, i37, 0) | &&(=(matching1, 0), =(matching2, 0))
251_0_average_LE(EOS(STATIC_251), i44, i37, i44) → 258_0_average_LE(EOS(STATIC_258), i44, i37, i44)
257_0_average_LE(EOS(STATIC_257), matching1, i37, matching2) → 262_0_average_Load(EOS(STATIC_262), 0, i37) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
262_0_average_Load(EOS(STATIC_262), matching1, i37) → 272_0_average_ConstantStackPush(EOS(STATIC_272), 0, i37, i37) | =(matching1, 0)
272_0_average_ConstantStackPush(EOS(STATIC_272), matching1, i37, i37) → 286_0_average_LE(EOS(STATIC_286), 0, i37, i37, 2) | =(matching1, 0)
286_0_average_LE(EOS(STATIC_286), matching1, i49, i49, matching2) → 299_0_average_LE(EOS(STATIC_299), 0, i49, i49, 2) | &&(=(matching1, 0), =(matching2, 2))
299_0_average_LE(EOS(STATIC_299), matching1, i49, i49, matching2) → 311_0_average_ConstantStackPush(EOS(STATIC_311), 0, i49) | &&(&&(>(i49, 2), =(matching1, 0)), =(matching2, 2))
311_0_average_ConstantStackPush(EOS(STATIC_311), matching1, i49) → 326_0_average_Load(EOS(STATIC_326), 0, i49, 1) | =(matching1, 0)
326_0_average_Load(EOS(STATIC_326), matching1, i49, matching2) → 339_0_average_ConstantStackPush(EOS(STATIC_339), i49, 1, 0) | &&(=(matching1, 0), =(matching2, 1))
339_0_average_ConstantStackPush(EOS(STATIC_339), i49, matching1, matching2) → 359_0_average_IntArithmetic(EOS(STATIC_359), i49, 1, 0, 1) | &&(=(matching1, 1), =(matching2, 0))
359_0_average_IntArithmetic(EOS(STATIC_359), i49, matching1, matching2, matching3) → 370_0_average_Load(EOS(STATIC_370), i49, 1, 1) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 1))
370_0_average_Load(EOS(STATIC_370), i49, matching1, matching2) → 382_0_average_ConstantStackPush(EOS(STATIC_382), 1, 1, i49) | &&(=(matching1, 1), =(matching2, 1))
382_0_average_ConstantStackPush(EOS(STATIC_382), matching1, matching2, i49) → 391_0_average_IntArithmetic(EOS(STATIC_391), 1, 1, i49, 2) | &&(=(matching1, 1), =(matching2, 1))
391_0_average_IntArithmetic(EOS(STATIC_391), matching1, matching2, i49, matching3) → 401_0_average_InvokeMethod(EOS(STATIC_401), 1, 1, -(i49, 2)) | &&(&&(&&(>(i49, 0), =(matching1, 1)), =(matching2, 1)), =(matching3, 2))
401_0_average_InvokeMethod(EOS(STATIC_401), matching1, matching2, i67) → 404_1_average_InvokeMethod(404_0_average_Load(EOS(STATIC_404), 1, i67), 1, 1, i67) | &&(=(matching1, 1), =(matching2, 1))
404_0_average_Load(EOS(STATIC_404), matching1, i67) → 408_0_average_Load(EOS(STATIC_408), 1, i67) | =(matching1, 1)
408_0_average_Load(EOS(STATIC_408), matching1, i67) → 242_0_average_Load(EOS(STATIC_242), 1, i67) | =(matching1, 1)
242_0_average_Load(EOS(STATIC_242), i13, i37) → 251_0_average_LE(EOS(STATIC_251), i13, i37, i13)
258_0_average_LE(EOS(STATIC_258), i44, i37, i44) → 263_0_average_Load(EOS(STATIC_263), i44, i37) | >(i44, 0)
263_0_average_Load(EOS(STATIC_263), i44, i37) → 274_0_average_ConstantStackPush(EOS(STATIC_274), i44, i37, i44)
274_0_average_ConstantStackPush(EOS(STATIC_274), i44, i37, i44) → 288_0_average_IntArithmetic(EOS(STATIC_288), i44, i37, i44, 1)
288_0_average_IntArithmetic(EOS(STATIC_288), i44, i37, i44, matching1) → 301_0_average_Load(EOS(STATIC_301), i44, i37, -(i44, 1)) | &&(>(i44, 0), =(matching1, 1))
301_0_average_Load(EOS(STATIC_301), i44, i37, i50) → 314_0_average_ConstantStackPush(EOS(STATIC_314), i44, i37, i50, i37)
314_0_average_ConstantStackPush(EOS(STATIC_314), i44, i37, i50, i37) → 328_0_average_IntArithmetic(EOS(STATIC_328), i44, i37, i50, i37, 1)
328_0_average_IntArithmetic(EOS(STATIC_328), i44, i37, i50, i37, matching1) → 342_0_average_InvokeMethod(EOS(STATIC_342), i44, i37, i50, +(i37, 1)) | &&(>=(i37, 0), =(matching1, 1))
342_0_average_InvokeMethod(EOS(STATIC_342), i44, i37, i50, i56) → 361_1_average_InvokeMethod(361_0_average_Load(EOS(STATIC_361), i50, i56), i44, i37, i50, i56)
361_0_average_Load(EOS(STATIC_361), i50, i56) → 372_0_average_Load(EOS(STATIC_372), i50, i56)
372_0_average_Load(EOS(STATIC_372), i50, i56) → 242_0_average_Load(EOS(STATIC_242), i50, i56)
R rules:
286_0_average_LE(EOS(STATIC_286), matching1, i48, i48, matching2) → 298_0_average_LE(EOS(STATIC_298), 0, i48, i48, 2) | &&(=(matching1, 0), =(matching2, 2))
298_0_average_LE(EOS(STATIC_298), matching1, i48, i48, matching2) → 309_0_average_ConstantStackPush(EOS(STATIC_309)) | &&(&&(<=(i48, 2), =(matching1, 0)), =(matching2, 2))
309_0_average_ConstantStackPush(EOS(STATIC_309)) → 323_0_average_Return(EOS(STATIC_323), 1)
361_1_average_InvokeMethod(323_0_average_Return(EOS(STATIC_323), matching1), i44, i37, matching2, i64) → 402_0_average_Return(EOS(STATIC_402), i44, i37, 0, i64, 1) | &&(=(matching1, 1), =(matching2, 0))
361_1_average_InvokeMethod(406_0_average_Return(EOS(STATIC_406), i73, i74, matching1), i44, i37, i73, i74) → 429_0_average_Return(EOS(STATIC_429), i44, i37, i73, i74, i73, i74, 1) | =(matching1, 1)
361_1_average_InvokeMethod(441_0_average_Return(EOS(STATIC_441), i87, i88, matching1), i44, i37, i87, i88) → 471_0_average_Return(EOS(STATIC_471), i44, i37, i87, i88, i87, i88, 1) | =(matching1, 1)
361_1_average_InvokeMethod(552_0_average_Return(EOS(STATIC_552), i147, i148, i121), i44, i37, i147, i148) → 581_0_average_Return(EOS(STATIC_581), i44, i37, i147, i148, i147, i148, i121)
361_1_average_InvokeMethod(674_0_average_Return(EOS(STATIC_674), i213, i214, i189), i44, i37, i213, i214) → 701_0_average_Return(EOS(STATIC_701), i44, i37, i213, i214, i213, i214, i189)
361_1_average_InvokeMethod(780_0_average_Return(EOS(STATIC_780), i282, i283, i259), i44, i37, i282, i283) → 805_0_average_Return(EOS(STATIC_805), i44, i37, i282, i283, i282, i283, i259)
361_1_average_InvokeMethod(787_0_average_Return(EOS(STATIC_787), i274), i44, i37, matching1, i294) → 826_0_average_Return(EOS(STATIC_826), i44, i37, 0, i294, i274) | =(matching1, 0)
361_1_average_InvokeMethod(836_0_average_Return(EOS(STATIC_836), i313, i314, i301), i44, i37, i313, i314) → 854_0_average_Return(EOS(STATIC_854), i44, i37, i313, i314, i313, i314, i301)
402_0_average_Return(EOS(STATIC_402), i44, i37, matching1, i64, matching2) → 406_0_average_Return(EOS(STATIC_406), i44, i37, 1) | &&(=(matching1, 0), =(matching2, 1))
404_1_average_InvokeMethod(406_0_average_Return(EOS(STATIC_406), matching1, i79, matching2), matching3, matching4, i79) → 432_0_average_Return(EOS(STATIC_432), 1, 1, i79, 1, i79, 1) | &&(&&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1)), =(matching4, 1))
404_1_average_InvokeMethod(441_0_average_Return(EOS(STATIC_441), matching1, i90, matching2), matching3, matching4, i90) → 474_0_average_Return(EOS(STATIC_474), 1, 1, i90, 1, i90, 1) | &&(&&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1)), =(matching4, 1))
404_1_average_InvokeMethod(552_0_average_Return(EOS(STATIC_552), matching1, i150, i121), matching2, matching3, i150) → 584_0_average_Return(EOS(STATIC_584), 1, 1, i150, 1, i150, i121) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
404_1_average_InvokeMethod(674_0_average_Return(EOS(STATIC_674), matching1, i216, i189), matching2, matching3, i216) → 704_0_average_Return(EOS(STATIC_704), 1, 1, i216, 1, i216, i189) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
404_1_average_InvokeMethod(780_0_average_Return(EOS(STATIC_780), matching1, i284, i259), matching2, matching3, i284) → 808_0_average_Return(EOS(STATIC_808), 1, 1, i284, 1, i284, i259) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
404_1_average_InvokeMethod(836_0_average_Return(EOS(STATIC_836), matching1, i316, i301), matching2, matching3, i316) → 857_0_average_Return(EOS(STATIC_857), 1, 1, i316, 1, i316, i301) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
406_0_average_Return(EOS(STATIC_406), i44, i37, matching1) → 441_0_average_Return(EOS(STATIC_441), i44, i37, 1) | =(matching1, 1)
429_0_average_Return(EOS(STATIC_429), i44, i37, i73, i74, i73, i74, matching1) → 531_0_average_Return(EOS(STATIC_531), i44, i37, i73, i74, i73, i74, 1) | =(matching1, 1)
432_0_average_Return(EOS(STATIC_432), matching1, matching2, i79, matching3, i79, matching4) → 539_0_average_Return(EOS(STATIC_539), 1, 1, i79, 1, i79, 1) | &&(&&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1)), =(matching4, 1))
441_0_average_Return(EOS(STATIC_441), i44, i37, matching1) → 552_0_average_Return(EOS(STATIC_552), i44, i37, 1) | =(matching1, 1)
471_0_average_Return(EOS(STATIC_471), i44, i37, i87, i88, i87, i88, matching1) → 429_0_average_Return(EOS(STATIC_429), i44, i37, i87, i88, i87, i88, 1) | =(matching1, 1)
474_0_average_Return(EOS(STATIC_474), matching1, matching2, i90, matching3, i90, matching4) → 432_0_average_Return(EOS(STATIC_432), 1, 1, i90, 1, i90, 1) | &&(&&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1)), =(matching4, 1))
531_0_average_Return(EOS(STATIC_531), i44, i37, i119, i120, i119, i120, i121) → 652_0_average_Return(EOS(STATIC_652), i44, i37, i119, i120, i119, i120, i121)
539_0_average_Return(EOS(STATIC_539), matching1, matching2, i129, matching3, i129, i130) → 662_0_average_Return(EOS(STATIC_662), 1, 1, i129, 1, i129, i130) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
552_0_average_Return(EOS(STATIC_552), i44, i37, i121) → 674_0_average_Return(EOS(STATIC_674), i44, i37, i121)
581_0_average_Return(EOS(STATIC_581), i44, i37, i147, i148, i147, i148, i121) → 531_0_average_Return(EOS(STATIC_531), i44, i37, i147, i148, i147, i148, i121)
584_0_average_Return(EOS(STATIC_584), matching1, matching2, i150, matching3, i150, i121) → 539_0_average_Return(EOS(STATIC_539), 1, 1, i150, 1, i150, i121) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
607_0_average_Return(EOS(STATIC_607), i44, i37, matching1, i166, i165) → 726_0_average_Return(EOS(STATIC_726), i44, i37, 0, i166, i165) | =(matching1, 0)
652_0_average_Return(EOS(STATIC_652), i44, i37, i187, i188, i187, i188, i189) → 764_0_average_Return(EOS(STATIC_764), i44, i37, i187, i188, i187, i188, i189)
662_0_average_Return(EOS(STATIC_662), matching1, matching2, i196, matching3, i196, i197) → 771_0_average_Return(EOS(STATIC_771), 1, 1, i196, 1, i196, i197) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
674_0_average_Return(EOS(STATIC_674), i44, i37, i189) → 780_0_average_Return(EOS(STATIC_780), i44, i37, i189)
701_0_average_Return(EOS(STATIC_701), i44, i37, i213, i214, i213, i214, i189) → 652_0_average_Return(EOS(STATIC_652), i44, i37, i213, i214, i213, i214, i189)
704_0_average_Return(EOS(STATIC_704), matching1, matching2, i216, matching3, i216, i189) → 662_0_average_Return(EOS(STATIC_662), 1, 1, i216, 1, i216, i189) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
726_0_average_Return(EOS(STATIC_726), i44, i37, matching1, i234, i233) → 827_0_average_Return(EOS(STATIC_827), i44, i37, 0, i234, i233) | =(matching1, 0)
764_0_average_Return(EOS(STATIC_764), i44, i37, i257, i258, i257, i258, i259) → 780_0_average_Return(EOS(STATIC_780), i44, i37, i259)
771_0_average_Return(EOS(STATIC_771), matching1, matching2, i265, matching3, i265, i266) → 782_0_average_IntArithmetic(EOS(STATIC_782), 1, i266) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
780_0_average_Return(EOS(STATIC_780), i44, i37, i259) → 836_0_average_Return(EOS(STATIC_836), i44, i37, i259)
782_0_average_IntArithmetic(EOS(STATIC_782), matching1, i266) → 787_0_average_Return(EOS(STATIC_787), +(1, i266)) | =(matching1, 1)
805_0_average_Return(EOS(STATIC_805), i44, i37, i282, i283, i282, i283, i259) → 764_0_average_Return(EOS(STATIC_764), i44, i37, i282, i283, i282, i283, i259)
808_0_average_Return(EOS(STATIC_808), matching1, matching2, i284, matching3, i284, i259) → 771_0_average_Return(EOS(STATIC_771), 1, 1, i284, 1, i284, i259) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
826_0_average_Return(EOS(STATIC_826), i44, i37, matching1, i294, i274) → 827_0_average_Return(EOS(STATIC_827), i44, i37, 0, i294, i274) | =(matching1, 0)
827_0_average_Return(EOS(STATIC_827), i44, i37, matching1, i302, i301) → 836_0_average_Return(EOS(STATIC_836), i44, i37, i301) | =(matching1, 0)
854_0_average_Return(EOS(STATIC_854), i44, i37, i313, i314, i313, i314, i301) → 764_0_average_Return(EOS(STATIC_764), i44, i37, i313, i314, i313, i314, i301)
857_0_average_Return(EOS(STATIC_857), matching1, matching2, i316, matching3, i316, i301) → 771_0_average_Return(EOS(STATIC_771), 1, 1, i316, 1, i316, i301) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))

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

P rules:
251_0_average_LE(EOS(STATIC_251), 0, x1, 0) → 404_1_average_InvokeMethod(251_0_average_LE(EOS(STATIC_251), 1, -(x1, 2), 1), 1, 1, -(x1, 2)) | >(x1, 2)
251_0_average_LE(EOS(STATIC_251), x0, x1, x0) → 361_1_average_InvokeMethod(251_0_average_LE(EOS(STATIC_251), -(x0, 1), +(x1, 1), -(x0, 1)), x0, x1, -(x0, 1), +(x1, 1)) | &&(>(+(x1, 1), 0), >(x0, 0))
R rules:
361_1_average_InvokeMethod(323_0_average_Return(EOS(STATIC_323), 1), x1, x2, 0, x4) → 836_0_average_Return(EOS(STATIC_836), x1, x2, 1)
361_1_average_InvokeMethod(780_0_average_Return(EOS(STATIC_780), x0, x1, x2), x3, x4, x0, x1) → 836_0_average_Return(EOS(STATIC_836), x3, x4, x2)
361_1_average_InvokeMethod(836_0_average_Return(EOS(STATIC_836), x0, x1, x2), x3, x4, x0, x1) → 836_0_average_Return(EOS(STATIC_836), x3, x4, x2)
361_1_average_InvokeMethod(674_0_average_Return(EOS(STATIC_674), x0, x1, x2), x3, x4, x0, x1) → 836_0_average_Return(EOS(STATIC_836), x3, x4, x2)
361_1_average_InvokeMethod(406_0_average_Return(EOS(STATIC_406), x0, x1, 1), x3, x4, x0, x1) → 836_0_average_Return(EOS(STATIC_836), x3, x4, 1)
361_1_average_InvokeMethod(441_0_average_Return(EOS(STATIC_441), x0, x1, 1), x3, x4, x0, x1) → 836_0_average_Return(EOS(STATIC_836), x3, x4, 1)
361_1_average_InvokeMethod(552_0_average_Return(EOS(STATIC_552), x0, x1, x2), x3, x4, x0, x1) → 836_0_average_Return(EOS(STATIC_836), x3, x4, x2)
361_1_average_InvokeMethod(787_0_average_Return(EOS(STATIC_787), x0), x1, x2, 0, x4) → 836_0_average_Return(EOS(STATIC_836), x1, x2, x0)
404_1_average_InvokeMethod(780_0_average_Return(EOS(STATIC_780), 1, x1, x2), 1, 1, x1) → 787_0_average_Return(EOS(STATIC_787), +(1, x2))
404_1_average_InvokeMethod(836_0_average_Return(EOS(STATIC_836), 1, x1, x2), 1, 1, x1) → 787_0_average_Return(EOS(STATIC_787), +(1, x2))
404_1_average_InvokeMethod(674_0_average_Return(EOS(STATIC_674), 1, x1, x2), 1, 1, x1) → 787_0_average_Return(EOS(STATIC_787), +(1, x2))
404_1_average_InvokeMethod(406_0_average_Return(EOS(STATIC_406), 1, x1, 1), 1, 1, x1) → 787_0_average_Return(EOS(STATIC_787), 2)
404_1_average_InvokeMethod(441_0_average_Return(EOS(STATIC_441), 1, x1, 1), 1, 1, x1) → 787_0_average_Return(EOS(STATIC_787), 2)
404_1_average_InvokeMethod(552_0_average_Return(EOS(STATIC_552), 1, x1, x2), 1, 1, x1) → 787_0_average_Return(EOS(STATIC_787), +(1, x2))

Filtered ground terms:

251_0_average_LE(x1, x2, x3, x4) → 251_0_average_LE(x2, x3, x4)
Cond_251_0_average_LE1(x1, x2, x3, x4, x5) → Cond_251_0_average_LE1(x1, x3, x4, x5)
404_1_average_InvokeMethod(x1, x2, x3, x4) → 404_1_average_InvokeMethod(x1, x4)
Cond_251_0_average_LE(x1, x2, x3, x4, x5) → Cond_251_0_average_LE(x1, x4)
787_0_average_Return(x1, x2) → 787_0_average_Return(x2)
552_0_average_Return(x1, x2, x3, x4) → 552_0_average_Return(x2, x3, x4)
441_0_average_Return(x1, x2, x3, x4) → 441_0_average_Return(x2, x3)
406_0_average_Return(x1, x2, x3, x4) → 406_0_average_Return(x2, x3)
674_0_average_Return(x1, x2, x3, x4) → 674_0_average_Return(x2, x3, x4)
836_0_average_Return(x1, x2, x3, x4) → 836_0_average_Return(x2, x3, x4)
780_0_average_Return(x1, x2, x3, x4) → 780_0_average_Return(x2, x3, x4)
323_0_average_Return(x1, x2) → 323_0_average_Return

Filtered duplicate args:

251_0_average_LE(x1, x2, x3) → 251_0_average_LE(x2, x3)
404_1_average_InvokeMethod(x1, x2) → 404_1_average_InvokeMethod(x1)
Cond_251_0_average_LE1(x1, x2, x3, x4) → Cond_251_0_average_LE1(x1, x3, x4)

Filtered unneeded arguments:

361_1_average_InvokeMethod(x1, x2, x3, x4, x5) → 361_1_average_InvokeMethod(x1, x2, x4)
780_0_average_Return(x1, x2, x3) → 780_0_average_Return(x1)
836_0_average_Return(x1, x2, x3) → 836_0_average_Return(x1)
674_0_average_Return(x1, x2, x3) → 674_0_average_Return(x1)
406_0_average_Return(x1, x2) → 406_0_average_Return(x1)
441_0_average_Return(x1, x2) → 441_0_average_Return(x1)
552_0_average_Return(x1, x2, x3) → 552_0_average_Return(x1)

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

P rules:
251_0_average_LE(x1, 0) → 404_1_average_InvokeMethod(251_0_average_LE(-(x1, 2), 1)) | >(x1, 2)
251_0_average_LE(x1, x0) → 361_1_average_InvokeMethod(251_0_average_LE(+(x1, 1), -(x0, 1)), x0, -(x0, 1)) | &&(>(x1, -1), >(x0, 0))
R rules:
361_1_average_InvokeMethod(323_0_average_Return, x1, 0) → 836_0_average_Return(x1)
361_1_average_InvokeMethod(780_0_average_Return(x0), x3, x0) → 836_0_average_Return(x3)
361_1_average_InvokeMethod(836_0_average_Return(x0), x3, x0) → 836_0_average_Return(x3)
361_1_average_InvokeMethod(674_0_average_Return(x0), x3, x0) → 836_0_average_Return(x3)
361_1_average_InvokeMethod(406_0_average_Return(x0), x3, x0) → 836_0_average_Return(x3)
361_1_average_InvokeMethod(441_0_average_Return(x0), x3, x0) → 836_0_average_Return(x3)
361_1_average_InvokeMethod(552_0_average_Return(x0), x3, x0) → 836_0_average_Return(x3)
361_1_average_InvokeMethod(787_0_average_Return(x0), x1, 0) → 836_0_average_Return(x1)
404_1_average_InvokeMethod(780_0_average_Return(1)) → 787_0_average_Return(+(1, x2))
404_1_average_InvokeMethod(836_0_average_Return(1)) → 787_0_average_Return(+(1, x2))
404_1_average_InvokeMethod(674_0_average_Return(1)) → 787_0_average_Return(+(1, x2))
404_1_average_InvokeMethod(406_0_average_Return(1)) → 787_0_average_Return(2)
404_1_average_InvokeMethod(441_0_average_Return(1)) → 787_0_average_Return(2)
404_1_average_InvokeMethod(552_0_average_Return(1)) → 787_0_average_Return(+(1, x2))

Performed bisimulation on rules. Used the following equivalence classes: {[836_0_average_Return_1, 780_0_average_Return_1, 674_0_average_Return_1, 406_0_average_Return_1, 441_0_average_Return_1, 552_0_average_Return_1]=836_0_average_Return_1}

Finished conversion. Obtained 4 rules for P and 5 rules for R. System has predefined symbols.

P rules:
251_0_AVERAGE_LE(x1, 0) → COND_251_0_AVERAGE_LE(>(x1, 2), x1, 0)
COND_251_0_AVERAGE_LE(TRUE, x1, 0) → 251_0_AVERAGE_LE(-(x1, 2), 1)
251_0_AVERAGE_LE(x1, x0) → COND_251_0_AVERAGE_LE1(&&(>(x1, -1), >(x0, 0)), x1, x0)
COND_251_0_AVERAGE_LE1(TRUE, x1, x0) → 251_0_AVERAGE_LE(+(x1, 1), -(x0, 1))
R rules:
361_1_average_InvokeMethod(323_0_average_Return, x1, 0) → 836_0_average_Return(x1)
361_1_average_InvokeMethod(836_0_average_Return(x0), x3, x0) → 836_0_average_Return(x3)
361_1_average_InvokeMethod(787_0_average_Return(x0), x1, 0) → 836_0_average_Return(x1)
404_1_average_InvokeMethod(836_0_average_Return(1)) → 787_0_average_Return(+(1, x2))
404_1_average_InvokeMethod(836_0_average_Return(1)) → 787_0_average_Return(2)

(6) Obligation:

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

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

The following domains are used:

Integer, Boolean

The ITRS R consists of the following rules:
361_1_average_InvokeMethod(323_0_average_Return, x1, 0) → 836_0_average_Return(x1)
361_1_average_InvokeMethod(836_0_average_Return(x0), x3, x0) → 836_0_average_Return(x3)
361_1_average_InvokeMethod(787_0_average_Return(x0), x1, 0) → 836_0_average_Return(x1)
404_1_average_InvokeMethod(836_0_average_Return(1)) → 787_0_average_Return(1 + x2)
404_1_average_InvokeMethod(836_0_average_Return(1)) → 787_0_average_Return(2)

The integer pair graph contains the following rules and edges:
(0): 251_0_AVERAGE_LE(x1[0], 0) → COND_251_0_AVERAGE_LE(x1[0] > 2, x1[0], 0)
(1): COND_251_0_AVERAGE_LE(TRUE, x1[1], 0) → 251_0_AVERAGE_LE(x1[1] - 2, 1)
(2): 251_0_AVERAGE_LE(x1[2], x0[2]) → COND_251_0_AVERAGE_LE1(x1[2] > -1 && x0[2] > 0, x1[2], x0[2])
(3): COND_251_0_AVERAGE_LE1(TRUE, x1[3], x0[3]) → 251_0_AVERAGE_LE(x1[3] + 1, x0[3] - 1)

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

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

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

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

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

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

The set Q consists of the following terms:
361_1_average_InvokeMethod(323_0_average_Return, x0, 0)
361_1_average_InvokeMethod(836_0_average_Return(x0), x1, x0)
361_1_average_InvokeMethod(787_0_average_Return(x0), x1, 0)
404_1_average_InvokeMethod(836_0_average_Return(1))

(7) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@64c0d2d3 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 251_0_AVERAGE_LE(x1, 0) → COND_251_0_AVERAGE_LE(>(x1, 2), x1, 0) the following chains were created:

We consider the chain 251_0_AVERAGE_LE(x1[0], 0) → COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0), COND_251_0_AVERAGE_LE(TRUE, x1[1], 0) → 251_0_AVERAGE_LE(-(x1[1], 2), 1) which results in the following constraint:
(1)    (>(x1[0], 2)=TRUE∧x1[0]=x1[1] ⇒ 251_0_AVERAGE_LE(x1[0], 0)≥NonInfC∧251_0_AVERAGE_LE(x1[0], 0)≥COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0)∧(U^Increasing(COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0)), ≥))

We simplified constraint (1) using rule (IV) which results in the following new constraint:
(2)    (>(x1[0], 2)=TRUE ⇒ 251_0_AVERAGE_LE(x1[0], 0)≥NonInfC∧251_0_AVERAGE_LE(x1[0], 0)≥COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0)∧(U^Increasing(COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0)), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x1[0] + [-3] ≥ 0 ⇒ (U^Increasing(COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0)), ≥)∧[(-1)bni_15 + (-1)Bound*bni_15] + [bni_15]x1[0] ≥ 0∧[(-1)bso_16] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x1[0] + [-3] ≥ 0 ⇒ (U^Increasing(COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0)), ≥)∧[(-1)bni_15 + (-1)Bound*bni_15] + [bni_15]x1[0] ≥ 0∧[(-1)bso_16] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x1[0] + [-3] ≥ 0 ⇒ (U^Increasing(COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0)), ≥)∧[(-1)bni_15 + (-1)Bound*bni_15] + [bni_15]x1[0] ≥ 0∧[(-1)bso_16] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x1[0] ≥ 0 ⇒ (U^Increasing(COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0)), ≥)∧[(2)bni_15 + (-1)Bound*bni_15] + [bni_15]x1[0] ≥ 0∧[(-1)bso_16] ≥ 0)

For Pair COND_251_0_AVERAGE_LE(TRUE, x1, 0) → 251_0_AVERAGE_LE(-(x1, 2), 1) the following chains were created:

We consider the chain COND_251_0_AVERAGE_LE(TRUE, x1[1], 0) → 251_0_AVERAGE_LE(-(x1[1], 2), 1) which results in the following constraint:
(7)    (COND_251_0_AVERAGE_LE(TRUE, x1[1], 0)≥NonInfC∧COND_251_0_AVERAGE_LE(TRUE, x1[1], 0)≥251_0_AVERAGE_LE(-(x1[1], 2), 1)∧(U^Increasing(251_0_AVERAGE_LE(-(x1[1], 2), 1)), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    ((U^Increasing(251_0_AVERAGE_LE(-(x1[1], 2), 1)), ≥)∧[bni_17] = 0∧[(-1)bso_18] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    ((U^Increasing(251_0_AVERAGE_LE(-(x1[1], 2), 1)), ≥)∧[bni_17] = 0∧[(-1)bso_18] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    ((U^Increasing(251_0_AVERAGE_LE(-(x1[1], 2), 1)), ≥)∧[bni_17] = 0∧[(-1)bso_18] ≥ 0)

We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(11)    ((U^Increasing(251_0_AVERAGE_LE(-(x1[1], 2), 1)), ≥)∧[bni_17] = 0∧0 = 0∧[(-1)bso_18] ≥ 0)

For Pair 251_0_AVERAGE_LE(x1, x0) → COND_251_0_AVERAGE_LE1(&&(>(x1, -1), >(x0, 0)), x1, x0) the following chains were created:

We consider the chain 251_0_AVERAGE_LE(x1[2], x0[2]) → COND_251_0_AVERAGE_LE1(&&(>(x1[2], -1), >(x0[2], 0)), x1[2], x0[2]), COND_251_0_AVERAGE_LE1(TRUE, x1[3], x0[3]) → 251_0_AVERAGE_LE(+(x1[3], 1), -(x0[3], 1)) which results in the following constraint:
(12)    (&&(>(x1[2], -1), >(x0[2], 0))=TRUE∧x1[2]=x1[3]∧x0[2]=x0[3] ⇒ 251_0_AVERAGE_LE(x1[2], x0[2])≥NonInfC∧251_0_AVERAGE_LE(x1[2], x0[2])≥COND_251_0_AVERAGE_LE1(&&(>(x1[2], -1), >(x0[2], 0)), x1[2], x0[2])∧(U^Increasing(COND_251_0_AVERAGE_LE1(&&(>(x1[2], -1), >(x0[2], 0)), x1[2], x0[2])), ≥))

We simplified constraint (12) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
(13)    (>(x1[2], -1)=TRUE∧>(x0[2], 0)=TRUE ⇒ 251_0_AVERAGE_LE(x1[2], x0[2])≥NonInfC∧251_0_AVERAGE_LE(x1[2], x0[2])≥COND_251_0_AVERAGE_LE1(&&(>(x1[2], -1), >(x0[2], 0)), x1[2], x0[2])∧(U^Increasing(COND_251_0_AVERAGE_LE1(&&(>(x1[2], -1), >(x0[2], 0)), x1[2], x0[2])), ≥))

We simplified constraint (13) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(14)    (x1[2] ≥ 0∧x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_251_0_AVERAGE_LE1(&&(>(x1[2], -1), >(x0[2], 0)), x1[2], x0[2])), ≥)∧[(-1)bni_19 + (-1)Bound*bni_19] + [(2)bni_19]x0[2] + [bni_19]x1[2] ≥ 0∧[(-1)bso_20] ≥ 0)

We simplified constraint (14) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(15)    (x1[2] ≥ 0∧x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_251_0_AVERAGE_LE1(&&(>(x1[2], -1), >(x0[2], 0)), x1[2], x0[2])), ≥)∧[(-1)bni_19 + (-1)Bound*bni_19] + [(2)bni_19]x0[2] + [bni_19]x1[2] ≥ 0∧[(-1)bso_20] ≥ 0)

We simplified constraint (15) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(16)    (x1[2] ≥ 0∧x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_251_0_AVERAGE_LE1(&&(>(x1[2], -1), >(x0[2], 0)), x1[2], x0[2])), ≥)∧[(-1)bni_19 + (-1)Bound*bni_19] + [(2)bni_19]x0[2] + [bni_19]x1[2] ≥ 0∧[(-1)bso_20] ≥ 0)

We simplified constraint (16) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(17)    (x1[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(COND_251_0_AVERAGE_LE1(&&(>(x1[2], -1), >(x0[2], 0)), x1[2], x0[2])), ≥)∧[bni_19 + (-1)Bound*bni_19] + [(2)bni_19]x0[2] + [bni_19]x1[2] ≥ 0∧[(-1)bso_20] ≥ 0)

For Pair COND_251_0_AVERAGE_LE1(TRUE, x1, x0) → 251_0_AVERAGE_LE(+(x1, 1), -(x0, 1)) the following chains were created:

We consider the chain COND_251_0_AVERAGE_LE1(TRUE, x1[3], x0[3]) → 251_0_AVERAGE_LE(+(x1[3], 1), -(x0[3], 1)) which results in the following constraint:
(18)    (COND_251_0_AVERAGE_LE1(TRUE, x1[3], x0[3])≥NonInfC∧COND_251_0_AVERAGE_LE1(TRUE, x1[3], x0[3])≥251_0_AVERAGE_LE(+(x1[3], 1), -(x0[3], 1))∧(U^Increasing(251_0_AVERAGE_LE(+(x1[3], 1), -(x0[3], 1))), ≥))

We simplified constraint (18) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(19)    ((U^Increasing(251_0_AVERAGE_LE(+(x1[3], 1), -(x0[3], 1))), ≥)∧[bni_21] = 0∧[1 + (-1)bso_22] ≥ 0)

We simplified constraint (19) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(20)    ((U^Increasing(251_0_AVERAGE_LE(+(x1[3], 1), -(x0[3], 1))), ≥)∧[bni_21] = 0∧[1 + (-1)bso_22] ≥ 0)

We simplified constraint (20) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(21)    ((U^Increasing(251_0_AVERAGE_LE(+(x1[3], 1), -(x0[3], 1))), ≥)∧[bni_21] = 0∧[1 + (-1)bso_22] ≥ 0)

We simplified constraint (21) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(22)    ((U^Increasing(251_0_AVERAGE_LE(+(x1[3], 1), -(x0[3], 1))), ≥)∧[bni_21] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)

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

251_0_AVERAGE_LE(x1, 0) → COND_251_0_AVERAGE_LE(>(x1, 2), x1, 0)
- (x1[0] ≥ 0 ⇒ (U^Increasing(COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0)), ≥)∧[(2)bni_15 + (-1)Bound*bni_15] + [bni_15]x1[0] ≥ 0∧[(-1)bso_16] ≥ 0)
COND_251_0_AVERAGE_LE(TRUE, x1, 0) → 251_0_AVERAGE_LE(-(x1, 2), 1)
- ((U^Increasing(251_0_AVERAGE_LE(-(x1[1], 2), 1)), ≥)∧[bni_17] = 0∧0 = 0∧[(-1)bso_18] ≥ 0)
251_0_AVERAGE_LE(x1, x0) → COND_251_0_AVERAGE_LE1(&&(>(x1, -1), >(x0, 0)), x1, x0)
- (x1[2] ≥ 0∧x0[2] ≥ 0 ⇒ (U^Increasing(COND_251_0_AVERAGE_LE1(&&(>(x1[2], -1), >(x0[2], 0)), x1[2], x0[2])), ≥)∧[bni_19 + (-1)Bound*bni_19] + [(2)bni_19]x0[2] + [bni_19]x1[2] ≥ 0∧[(-1)bso_20] ≥ 0)
COND_251_0_AVERAGE_LE1(TRUE, x1, x0) → 251_0_AVERAGE_LE(+(x1, 1), -(x0, 1))
- ((U^Increasing(251_0_AVERAGE_LE(+(x1[3], 1), -(x0[3], 1))), ≥)∧[bni_21] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_22] ≥ 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(361_1_average_InvokeMethod(x₁, x₂, x₃)) = [-1]
POL(323_0_average_Return) = [-1]
POL(0) = 0
POL(836_0_average_Return(x₁)) = [-1]
POL(787_0_average_Return(x₁)) = x₁
POL(404_1_average_InvokeMethod(x₁)) = [-1]
POL(1) = [1]
POL(+(x₁, x₂)) = x₁ + x₂
POL(2) = [2]
POL(251_0_AVERAGE_LE(x₁, x₂)) = [-1] + [2]x₂ + x₁
POL(COND_251_0_AVERAGE_LE(x₁, x₂, x₃)) = [-1] + x₂
POL(>(x₁, x₂)) = [-1]
POL(-(x₁, x₂)) = x₁ + [-1]x₂
POL(COND_251_0_AVERAGE_LE1(x₁, x₂, x₃)) = [-1] + [2]x₃ + x₂
POL(&&(x₁, x₂)) = [-1]
POL(-1) = [-1]

The following pairs are in P_>:

COND_251_0_AVERAGE_LE1(TRUE, x1[3], x0[3]) → 251_0_AVERAGE_LE(+(x1[3], 1), -(x0[3], 1))

The following pairs are in P_bound:

251_0_AVERAGE_LE(x1[0], 0) → COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0)
251_0_AVERAGE_LE(x1[2], x0[2]) → COND_251_0_AVERAGE_LE1(&&(>(x1[2], -1), >(x0[2], 0)), x1[2], x0[2])

The following pairs are in P_≥:

251_0_AVERAGE_LE(x1[0], 0) → COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0)
COND_251_0_AVERAGE_LE(TRUE, x1[1], 0) → 251_0_AVERAGE_LE(-(x1[1], 2), 1)
251_0_AVERAGE_LE(x1[2], x0[2]) → COND_251_0_AVERAGE_LE1(&&(>(x1[2], -1), >(x0[2], 0)), x1[2], x0[2])

There are no usable rules.

(8) Complex Obligation (AND)

(9) 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

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

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

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

(10) IDependencyGraphProof (EQUIVALENT transformation)

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

(11) 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:
361_1_average_InvokeMethod(323_0_average_Return, x1, 0) → 836_0_average_Return(x1)
361_1_average_InvokeMethod(836_0_average_Return(x0), x3, x0) → 836_0_average_Return(x3)
361_1_average_InvokeMethod(787_0_average_Return(x0), x1, 0) → 836_0_average_Return(x1)
404_1_average_InvokeMethod(836_0_average_Return(1)) → 787_0_average_Return(1 + x2)
404_1_average_InvokeMethod(836_0_average_Return(1)) → 787_0_average_Return(2)

The integer pair graph contains the following rules and edges:
(1): COND_251_0_AVERAGE_LE(TRUE, x1[1], 0) → 251_0_AVERAGE_LE(x1[1] - 2, 1)
(0): 251_0_AVERAGE_LE(x1[0], 0) → COND_251_0_AVERAGE_LE(x1[0] > 2, x1[0], 0)

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

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

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

(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

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_251_0_AVERAGE_LE(TRUE, x1[1], 0) → 251_0_AVERAGE_LE(x1[1] - 2, 1)
(0): 251_0_AVERAGE_LE(x1[0], 0) → COND_251_0_AVERAGE_LE(x1[0] > 2, x1[0], 0)

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

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

(14) 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@64c0d2d3 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_251_0_AVERAGE_LE(TRUE, x1[1], 0) → 251_0_AVERAGE_LE(-(x1[1], 2), 1) the following chains were created:

We consider the chain COND_251_0_AVERAGE_LE(TRUE, x1[1], 0) → 251_0_AVERAGE_LE(-(x1[1], 2), 1) which results in the following constraint:
(1)    (COND_251_0_AVERAGE_LE(TRUE, x1[1], 0)≥NonInfC∧COND_251_0_AVERAGE_LE(TRUE, x1[1], 0)≥251_0_AVERAGE_LE(-(x1[1], 2), 1)∧(U^Increasing(251_0_AVERAGE_LE(-(x1[1], 2), 1)), ≥))

We simplified constraint (1) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(2)    ((U^Increasing(251_0_AVERAGE_LE(-(x1[1], 2), 1)), ≥)∧[bni_6] = 0∧[2 + (-1)bso_7] ≥ 0)

We simplified constraint (2) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(3)    ((U^Increasing(251_0_AVERAGE_LE(-(x1[1], 2), 1)), ≥)∧[bni_6] = 0∧[2 + (-1)bso_7] ≥ 0)

We simplified constraint (3) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(4)    ((U^Increasing(251_0_AVERAGE_LE(-(x1[1], 2), 1)), ≥)∧[bni_6] = 0∧[2 + (-1)bso_7] ≥ 0)

We simplified constraint (4) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(5)    ((U^Increasing(251_0_AVERAGE_LE(-(x1[1], 2), 1)), ≥)∧[bni_6] = 0∧0 = 0∧[2 + (-1)bso_7] ≥ 0)

For Pair 251_0_AVERAGE_LE(x1[0], 0) → COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0) the following chains were created:

We consider the chain 251_0_AVERAGE_LE(x1[0], 0) → COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0), COND_251_0_AVERAGE_LE(TRUE, x1[1], 0) → 251_0_AVERAGE_LE(-(x1[1], 2), 1) which results in the following constraint:
(6)    (>(x1[0], 2)=TRUE∧x1[0]=x1[1] ⇒ 251_0_AVERAGE_LE(x1[0], 0)≥NonInfC∧251_0_AVERAGE_LE(x1[0], 0)≥COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0)∧(U^Increasing(COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0)), ≥))

We simplified constraint (6) using rule (IV) which results in the following new constraint:
(7)    (>(x1[0], 2)=TRUE ⇒ 251_0_AVERAGE_LE(x1[0], 0)≥NonInfC∧251_0_AVERAGE_LE(x1[0], 0)≥COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0)∧(U^Increasing(COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0)), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    (x1[0] + [-3] ≥ 0 ⇒ (U^Increasing(COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0)), ≥)∧[(-1)bni_8 + (-1)Bound*bni_8] + [bni_8]x1[0] ≥ 0∧[(-1)bso_9] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    (x1[0] + [-3] ≥ 0 ⇒ (U^Increasing(COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0)), ≥)∧[(-1)bni_8 + (-1)Bound*bni_8] + [bni_8]x1[0] ≥ 0∧[(-1)bso_9] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    (x1[0] + [-3] ≥ 0 ⇒ (U^Increasing(COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0)), ≥)∧[(-1)bni_8 + (-1)Bound*bni_8] + [bni_8]x1[0] ≥ 0∧[(-1)bso_9] ≥ 0)

We simplified constraint (10) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(11)    (x1[0] ≥ 0 ⇒ (U^Increasing(COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0)), ≥)∧[(2)bni_8 + (-1)Bound*bni_8] + [bni_8]x1[0] ≥ 0∧[(-1)bso_9] ≥ 0)

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

COND_251_0_AVERAGE_LE(TRUE, x1[1], 0) → 251_0_AVERAGE_LE(-(x1[1], 2), 1)
- ((U^Increasing(251_0_AVERAGE_LE(-(x1[1], 2), 1)), ≥)∧[bni_6] = 0∧0 = 0∧[2 + (-1)bso_7] ≥ 0)
251_0_AVERAGE_LE(x1[0], 0) → COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0)
- (x1[0] ≥ 0 ⇒ (U^Increasing(COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0)), ≥)∧[(2)bni_8 + (-1)Bound*bni_8] + [bni_8]x1[0] ≥ 0∧[(-1)bso_9] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(COND_251_0_AVERAGE_LE(x₁, x₂, x₃)) = [-1] + x₂
POL(0) = 0
POL(251_0_AVERAGE_LE(x₁, x₂)) = [-1] + x₁
POL(-(x₁, x₂)) = x₁ + [-1]x₂
POL(2) = [2]
POL(1) = [1]
POL(>(x₁, x₂)) = [-1]

The following pairs are in P_>:

COND_251_0_AVERAGE_LE(TRUE, x1[1], 0) → 251_0_AVERAGE_LE(-(x1[1], 2), 1)

The following pairs are in P_bound:

251_0_AVERAGE_LE(x1[0], 0) → COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0)

The following pairs are in P_≥:

251_0_AVERAGE_LE(x1[0], 0) → COND_251_0_AVERAGE_LE(>(x1[0], 2), x1[0], 0)

There are no usable rules.

(15) Complex Obligation (AND)

(16) 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

R is empty.

The integer pair graph contains the following rules and edges:
(0): 251_0_AVERAGE_LE(x1[0], 0) → COND_251_0_AVERAGE_LE(x1[0] > 2, x1[0], 0)

The set Q consists of the following terms:
361_1_average_InvokeMethod(323_0_average_Return, x0, 0)
361_1_average_InvokeMethod(836_0_average_Return(x0), x1, x0)
361_1_average_InvokeMethod(787_0_average_Return(x0), x1, 0)
404_1_average_InvokeMethod(836_0_average_Return(1))

(17) IDependencyGraphProof (EQUIVALENT transformation)

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

(18) TRUE

(19) 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

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_251_0_AVERAGE_LE(TRUE, x1[1], 0) → 251_0_AVERAGE_LE(x1[1] - 2, 1)

The set Q consists of the following terms:
361_1_average_InvokeMethod(323_0_average_Return, x0, 0)
361_1_average_InvokeMethod(836_0_average_Return(x0), x1, x0)
361_1_average_InvokeMethod(787_0_average_Return(x0), x1, 0)
404_1_average_InvokeMethod(836_0_average_Return(1))

(20) IDependencyGraphProof (EQUIVALENT transformation)

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

(21) TRUE

(22) 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:
361_1_average_InvokeMethod(323_0_average_Return, x1, 0) → 836_0_average_Return(x1)
361_1_average_InvokeMethod(836_0_average_Return(x0), x3, x0) → 836_0_average_Return(x3)
361_1_average_InvokeMethod(787_0_average_Return(x0), x1, 0) → 836_0_average_Return(x1)
404_1_average_InvokeMethod(836_0_average_Return(1)) → 787_0_average_Return(1 + x2)
404_1_average_InvokeMethod(836_0_average_Return(1)) → 787_0_average_Return(2)

The integer pair graph contains the following rules and edges:
(1): COND_251_0_AVERAGE_LE(TRUE, x1[1], 0) → 251_0_AVERAGE_LE(x1[1] - 2, 1)
(3): COND_251_0_AVERAGE_LE1(TRUE, x1[3], x0[3]) → 251_0_AVERAGE_LE(x1[3] + 1, x0[3] - 1)

The set Q consists of the following terms:
361_1_average_InvokeMethod(323_0_average_Return, x0, 0)
361_1_average_InvokeMethod(836_0_average_Return(x0), x1, x0)
361_1_average_InvokeMethod(787_0_average_Return(x0), x1, 0)
404_1_average_InvokeMethod(836_0_average_Return(1))

(23) IDependencyGraphProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Obligation:

(5) SCCToIDPv1Proof (SOUND transformation)

(6) Obligation:

(7) IDPNonInfProof (SOUND transformation)

(8) Complex Obligation (AND)

(9) Obligation:

(10) IDependencyGraphProof (EQUIVALENT transformation)

(11) Obligation:

(12) UsableRulesProof (EQUIVALENT transformation)

(13) Obligation:

(14) IDPNonInfProof (SOUND transformation)

(15) Complex Obligation (AND)

(16) Obligation:

(17) IDependencyGraphProof (EQUIVALENT transformation)

(18) TRUE

(19) Obligation:

(20) IDependencyGraphProof (EQUIVALENT transformation)

(21) TRUE

(22) Obligation:

(23) IDependencyGraphProof (EQUIVALENT transformation)

(24) TRUE