Termination proof of /tmp/tmpIPiGFh/AlternatingGrowReduceRec2.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 460 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 1020 ms)

        ↳7 IDP

        ↳8 IDPtoQDPProof (⇒, 70 ms)

        ↳9 QDP

        ↳10 UsableRulesProof (⇔, 0 ms)

        ↳11 QDP

        ↳12 QReductionProof (⇔, 0 ms)

        ↳13 QDP

        ↳14 QDPOrderProof (⇔, 0 ms)

        ↳15 QDP

        ↳16 DependencyGraphProof (⇔, 0 ms)

        ↳17 TRUE

    ↳18 JBCTerminationSCC

        ↳19 SCCToIDPv1Proof (⇒, 60 ms)

        ↳20 IDP

        ↳21 IDPNonInfProof (⇒, 110 ms)

        ↳22 AND

            ↳23 IDP

                ↳24 IDependencyGraphProof (⇔, 0 ms)

                ↳25 TRUE

            ↳26 IDP

                ↳27 IDependencyGraphProof (⇔, 0 ms)

                ↳28 TRUE

(0) Obligation:

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

package AlternatingGrowReduceRec2;

public class AlternatingGrowReduceRec2 {
	AlternatingGrowReduceRec2 next;

	public static void main(String[] argv) {
		Random.args = argv;
		AlternatingGrowReduceRec2 list = createList(Random.random());
		growReduce(0, list);
	}

	public static void growReduce(int mode, AlternatingGrowReduceRec2 list) {
		if (list == null) return;
		if (mode == 0) {
			list = list.next;
		} else if (mode == 1) {
			list = new AlternatingGrowReduceRec2(list);
		} else if (mode > 1) {
			list = list.next;
		}

		mode++;
		if (mode > 2) {
			growReduce(0, list);
		} else {
			growReduce(mode, list);
		}
	}

	public AlternatingGrowReduceRec2(AlternatingGrowReduceRec2 old) {
		this.next = old;
	}

	public static AlternatingGrowReduceRec2 createList(int length) {
		AlternatingGrowReduceRec2 res = new AlternatingGrowReduceRec2(null);
		if (length > 1) {
			res.next = createList(length - 1);
		}
		return res;
	}
}


package AlternatingGrowReduceRec2;

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

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

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

AlternatingGrowReduceRec2.AlternatingGrowReduceRec2.createList(I)LAlternatingGrowReduceRec2/AlternatingGrowReduceRec2;: Graph of 33 nodes with 0 SCCs.

AlternatingGrowReduceRec2.AlternatingGrowReduceRec2.growReduce(ILAlternatingGrowReduceRec2/AlternatingGrowReduceRec2;)V: Graph of 138 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: AlternatingGrowReduceRec2.AlternatingGrowReduceRec2.growReduce(ILAlternatingGrowReduceRec2/AlternatingGrowReduceRec2;)V
SCC calls the following helper methods: AlternatingGrowReduceRec2.AlternatingGrowReduceRec2.growReduce(ILAlternatingGrowReduceRec2/AlternatingGrowReduceRec2;)V
Performed SCC analyses: UsedFieldsAnalysis

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 97 rules for P and 46 rules for R.

P rules:
775_0_growReduce_NONNULL(EOS(STATIC_775), i84, java.lang.Object(o131sub), java.lang.Object(o131sub)) → 777_0_growReduce_NONNULL(EOS(STATIC_777), i84, java.lang.Object(o131sub), java.lang.Object(o131sub))
777_0_growReduce_NONNULL(EOS(STATIC_777), i84, java.lang.Object(o131sub), java.lang.Object(o131sub)) → 780_0_growReduce_Load(EOS(STATIC_780), i84, java.lang.Object(o131sub))
780_0_growReduce_Load(EOS(STATIC_780), i84, java.lang.Object(o131sub)) → 784_0_growReduce_NE(EOS(STATIC_784), i84, java.lang.Object(o131sub), i84)
784_0_growReduce_NE(EOS(STATIC_784), i86, java.lang.Object(o131sub), i86) → 788_0_growReduce_NE(EOS(STATIC_788), i86, java.lang.Object(o131sub), i86)
784_0_growReduce_NE(EOS(STATIC_784), matching1, java.lang.Object(o131sub), matching2) → 789_0_growReduce_NE(EOS(STATIC_789), 0, java.lang.Object(o131sub), 0) | &&(=(matching1, 0), =(matching2, 0))
788_0_growReduce_NE(EOS(STATIC_788), i86, java.lang.Object(o131sub), i86) → 792_0_growReduce_Load(EOS(STATIC_792), i86, java.lang.Object(o131sub)) | >(i86, 0)
792_0_growReduce_Load(EOS(STATIC_792), i86, java.lang.Object(o131sub)) → 797_0_growReduce_ConstantStackPush(EOS(STATIC_797), i86, java.lang.Object(o131sub), i86)
797_0_growReduce_ConstantStackPush(EOS(STATIC_797), i86, java.lang.Object(o131sub), i86) → 805_0_growReduce_NE(EOS(STATIC_805), i86, java.lang.Object(o131sub), i86, 1)
805_0_growReduce_NE(EOS(STATIC_805), matching1, java.lang.Object(o131sub), matching2, matching3) → 810_0_growReduce_NE(EOS(STATIC_810), 1, java.lang.Object(o131sub), 1, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
805_0_growReduce_NE(EOS(STATIC_805), matching1, java.lang.Object(o131sub), matching2, matching3) → 811_0_growReduce_NE(EOS(STATIC_811), 2, java.lang.Object(o131sub), 2, 1) | &&(&&(=(matching1, 2), =(matching2, 2)), =(matching3, 1))
810_0_growReduce_NE(EOS(STATIC_810), matching1, java.lang.Object(o131sub), matching2, matching3) → 817_0_growReduce_New(EOS(STATIC_817), 1, java.lang.Object(o131sub)) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
817_0_growReduce_New(EOS(STATIC_817), matching1, java.lang.Object(o131sub)) → 826_0_growReduce_Duplicate(EOS(STATIC_826), 1, java.lang.Object(o131sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 1)
826_0_growReduce_Duplicate(EOS(STATIC_826), matching1, java.lang.Object(o131sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 834_0_growReduce_Load(EOS(STATIC_834), 1, java.lang.Object(o131sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 1)
834_0_growReduce_Load(EOS(STATIC_834), matching1, java.lang.Object(o131sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 842_0_growReduce_InvokeMethod(EOS(STATIC_842), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o131sub)) | =(matching1, 1)
842_0_growReduce_InvokeMethod(EOS(STATIC_842), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o131sub)) → 850_0_<init>_Load(EOS(STATIC_850), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o131sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o131sub)) | =(matching1, 1)
850_0_<init>_Load(EOS(STATIC_850), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o131sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o131sub)) → 868_0_<init>_InvokeMethod(EOS(STATIC_868), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o131sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o131sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 1)
868_0_<init>_InvokeMethod(EOS(STATIC_868), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o131sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o131sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 877_0_<init>_Load(EOS(STATIC_877), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o131sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o131sub)) | =(matching1, 1)
877_0_<init>_Load(EOS(STATIC_877), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o131sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o131sub)) → 888_0_<init>_Load(EOS(STATIC_888), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o131sub), java.lang.Object(o131sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 1)
888_0_<init>_Load(EOS(STATIC_888), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o131sub), java.lang.Object(o131sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 896_0_<init>_FieldAccess(EOS(STATIC_896), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o131sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o131sub)) | =(matching1, 1)
896_0_<init>_FieldAccess(EOS(STATIC_896), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o131sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o131sub)) → 906_0_<init>_Return(EOS(STATIC_906), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub))), java.lang.Object(o131sub)) | =(matching1, 1)
906_0_<init>_Return(EOS(STATIC_906), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub))), java.lang.Object(o131sub)) → 917_0_growReduce_Store(EOS(STATIC_917), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub)))) | =(matching1, 1)
917_0_growReduce_Store(EOS(STATIC_917), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub)))) → 925_0_growReduce_JMP(EOS(STATIC_925), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub)))) | =(matching1, 1)
925_0_growReduce_JMP(EOS(STATIC_925), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub)))) → 942_0_growReduce_Inc(EOS(STATIC_942), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub)))) | =(matching1, 1)
942_0_growReduce_Inc(EOS(STATIC_942), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub)))) → 957_0_growReduce_Load(EOS(STATIC_957), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub)))) | =(matching1, 1)
957_0_growReduce_Load(EOS(STATIC_957), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub)))) → 967_0_growReduce_ConstantStackPush(EOS(STATIC_967), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub))), 2) | =(matching1, 2)
967_0_growReduce_ConstantStackPush(EOS(STATIC_967), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub))), matching2) → 978_0_growReduce_LE(EOS(STATIC_978), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub))), 2, 2) | &&(=(matching1, 2), =(matching2, 2))
978_0_growReduce_LE(EOS(STATIC_978), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub))), matching2, matching3) → 991_0_growReduce_Load(EOS(STATIC_991), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub)))) | &&(&&(=(matching1, 2), =(matching2, 2)), =(matching3, 2))
991_0_growReduce_Load(EOS(STATIC_991), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub)))) → 1007_0_growReduce_Load(EOS(STATIC_1007), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub))), 2) | =(matching1, 2)
1007_0_growReduce_Load(EOS(STATIC_1007), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub))), matching1) → 1037_0_growReduce_InvokeMethod(EOS(STATIC_1037), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub)))) | =(matching1, 2)
1037_0_growReduce_InvokeMethod(EOS(STATIC_1037), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub)))) → 1065_1_growReduce_InvokeMethod(1065_0_growReduce_Load(EOS(STATIC_1065), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub)))), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub)))) | =(matching1, 2)
1065_0_growReduce_Load(EOS(STATIC_1065), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub)))) → 1077_0_growReduce_Load(EOS(STATIC_1077), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub)))) | =(matching1, 2)
1077_0_growReduce_Load(EOS(STATIC_1077), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub)))) → 1097_0_growReduce_Load(EOS(STATIC_1097), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o131sub)))) | =(matching1, 2)
1097_0_growReduce_Load(EOS(STATIC_1097), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o128))) → 769_0_growReduce_Load(EOS(STATIC_769), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o128))) | =(matching1, 2)
769_0_growReduce_Load(EOS(STATIC_769), i84, o127) → 775_0_growReduce_NONNULL(EOS(STATIC_775), i84, o127, o127)
811_0_growReduce_NE(EOS(STATIC_811), matching1, java.lang.Object(o131sub), matching2, matching3) → 819_0_growReduce_Load(EOS(STATIC_819), 2, java.lang.Object(o131sub)) | &&(&&(=(matching1, 2), =(matching2, 2)), =(matching3, 1))
819_0_growReduce_Load(EOS(STATIC_819), matching1, java.lang.Object(o131sub)) → 827_0_growReduce_ConstantStackPush(EOS(STATIC_827), 2, java.lang.Object(o131sub), 2) | =(matching1, 2)
827_0_growReduce_ConstantStackPush(EOS(STATIC_827), matching1, java.lang.Object(o131sub), matching2) → 836_0_growReduce_LE(EOS(STATIC_836), 2, java.lang.Object(o131sub), 2, 1) | &&(=(matching1, 2), =(matching2, 2))
836_0_growReduce_LE(EOS(STATIC_836), matching1, java.lang.Object(o131sub), matching2, matching3) → 844_0_growReduce_Load(EOS(STATIC_844), 2, java.lang.Object(o131sub)) | &&(&&(=(matching1, 2), =(matching2, 2)), =(matching3, 1))
844_0_growReduce_Load(EOS(STATIC_844), matching1, java.lang.Object(o131sub)) → 853_0_growReduce_FieldAccess(EOS(STATIC_853), 2, java.lang.Object(o131sub)) | =(matching1, 2)
853_0_growReduce_FieldAccess(EOS(STATIC_853), matching1, java.lang.Object(o131sub)) → 861_0_growReduce_FieldAccess(EOS(STATIC_861), 2, java.lang.Object(o131sub)) | =(matching1, 2)
853_0_growReduce_FieldAccess(EOS(STATIC_853), matching1, java.lang.Object(o131sub)) → 862_0_growReduce_FieldAccess(EOS(STATIC_862), 2, java.lang.Object(o131sub)) | =(matching1, 2)
861_0_growReduce_FieldAccess(EOS(STATIC_861), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o163))) → 869_0_growReduce_FieldAccess(EOS(STATIC_869), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o163))) | =(matching1, 2)
869_0_growReduce_FieldAccess(EOS(STATIC_869), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o163))) → 879_0_growReduce_Store(EOS(STATIC_879), 2, o163) | =(matching1, 2)
879_0_growReduce_Store(EOS(STATIC_879), matching1, o163) → 889_0_growReduce_Inc(EOS(STATIC_889), 2, o163) | =(matching1, 2)
889_0_growReduce_Inc(EOS(STATIC_889), matching1, o163) → 898_0_growReduce_Load(EOS(STATIC_898), o163) | =(matching1, 2)
898_0_growReduce_Load(EOS(STATIC_898), o163) → 908_0_growReduce_ConstantStackPush(EOS(STATIC_908), o163)
908_0_growReduce_ConstantStackPush(EOS(STATIC_908), o163) → 919_0_growReduce_LE(EOS(STATIC_919), o163, 2)
919_0_growReduce_LE(EOS(STATIC_919), o163, matching1) → 927_0_growReduce_ConstantStackPush(EOS(STATIC_927), o163) | =(matching1, 2)
927_0_growReduce_ConstantStackPush(EOS(STATIC_927), o163) → 944_0_growReduce_Load(EOS(STATIC_944), o163, 0)
944_0_growReduce_Load(EOS(STATIC_944), o163, matching1) → 959_0_growReduce_InvokeMethod(EOS(STATIC_959), 0, o163) | =(matching1, 0)
959_0_growReduce_InvokeMethod(EOS(STATIC_959), matching1, o163) → 969_1_growReduce_InvokeMethod(969_0_growReduce_Load(EOS(STATIC_969), 0, o163), 0, o163) | =(matching1, 0)
969_0_growReduce_Load(EOS(STATIC_969), matching1, o163) → 980_0_growReduce_Load(EOS(STATIC_980), 0, o163) | =(matching1, 0)
980_0_growReduce_Load(EOS(STATIC_980), matching1, o163) → 769_0_growReduce_Load(EOS(STATIC_769), 0, o163) | =(matching1, 0)
862_0_growReduce_FieldAccess(EOS(STATIC_862), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o165))) → 870_0_growReduce_FieldAccess(EOS(STATIC_870), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o165))) | =(matching1, 2)
870_0_growReduce_FieldAccess(EOS(STATIC_870), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o165))) → 881_0_growReduce_Store(EOS(STATIC_881), 2, o165) | =(matching1, 2)
881_0_growReduce_Store(EOS(STATIC_881), matching1, o165) → 890_0_growReduce_Inc(EOS(STATIC_890), 2, o165) | =(matching1, 2)
890_0_growReduce_Inc(EOS(STATIC_890), matching1, o165) → 901_0_growReduce_Load(EOS(STATIC_901), o165) | =(matching1, 2)
901_0_growReduce_Load(EOS(STATIC_901), o165) → 911_0_growReduce_ConstantStackPush(EOS(STATIC_911), o165)
911_0_growReduce_ConstantStackPush(EOS(STATIC_911), o165) → 923_0_growReduce_LE(EOS(STATIC_923), o165, 2)
923_0_growReduce_LE(EOS(STATIC_923), o165, matching1) → 930_0_growReduce_ConstantStackPush(EOS(STATIC_930), o165) | =(matching1, 2)
930_0_growReduce_ConstantStackPush(EOS(STATIC_930), o165) → 947_0_growReduce_Load(EOS(STATIC_947), o165, 0)
947_0_growReduce_Load(EOS(STATIC_947), o165, matching1) → 962_0_growReduce_InvokeMethod(EOS(STATIC_962), 0, o165) | =(matching1, 0)
962_0_growReduce_InvokeMethod(EOS(STATIC_962), matching1, o165) → 970_1_growReduce_InvokeMethod(970_0_growReduce_Load(EOS(STATIC_970), 0, o165), 0, o165) | =(matching1, 0)
970_0_growReduce_Load(EOS(STATIC_970), matching1, o165) → 981_0_growReduce_Load(EOS(STATIC_981), 0, o165) | =(matching1, 0)
981_0_growReduce_Load(EOS(STATIC_981), matching1, o165) → 1029_0_growReduce_Load(EOS(STATIC_1029), 0, o165) | =(matching1, 0)
1029_0_growReduce_Load(EOS(STATIC_1029), matching1, o165) → 769_0_growReduce_Load(EOS(STATIC_769), 0, o165) | =(matching1, 0)
789_0_growReduce_NE(EOS(STATIC_789), matching1, java.lang.Object(o131sub), matching2) → 794_0_growReduce_Load(EOS(STATIC_794), 0, java.lang.Object(o131sub)) | &&(=(matching1, 0), =(matching2, 0))
794_0_growReduce_Load(EOS(STATIC_794), matching1, java.lang.Object(o131sub)) → 802_0_growReduce_FieldAccess(EOS(STATIC_802), 0, java.lang.Object(o131sub)) | =(matching1, 0)
802_0_growReduce_FieldAccess(EOS(STATIC_802), matching1, java.lang.Object(o131sub)) → 807_0_growReduce_FieldAccess(EOS(STATIC_807), 0, java.lang.Object(o131sub)) | =(matching1, 0)
802_0_growReduce_FieldAccess(EOS(STATIC_802), matching1, java.lang.Object(o131sub)) → 808_0_growReduce_FieldAccess(EOS(STATIC_808), 0, java.lang.Object(o131sub)) | =(matching1, 0)
807_0_growReduce_FieldAccess(EOS(STATIC_807), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o134))) → 813_0_growReduce_FieldAccess(EOS(STATIC_813), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o134))) | =(matching1, 0)
813_0_growReduce_FieldAccess(EOS(STATIC_813), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o134))) → 821_0_growReduce_Store(EOS(STATIC_821), 0, o134) | =(matching1, 0)
821_0_growReduce_Store(EOS(STATIC_821), matching1, o134) → 829_0_growReduce_JMP(EOS(STATIC_829), 0, o134) | =(matching1, 0)
829_0_growReduce_JMP(EOS(STATIC_829), matching1, o134) → 837_0_growReduce_Inc(EOS(STATIC_837), 0, o134) | =(matching1, 0)
837_0_growReduce_Inc(EOS(STATIC_837), matching1, o134) → 846_0_growReduce_Load(EOS(STATIC_846), 1, o134) | =(matching1, 0)
846_0_growReduce_Load(EOS(STATIC_846), matching1, o134) → 855_0_growReduce_ConstantStackPush(EOS(STATIC_855), 1, o134, 1) | =(matching1, 1)
855_0_growReduce_ConstantStackPush(EOS(STATIC_855), matching1, o134, matching2) → 863_0_growReduce_LE(EOS(STATIC_863), 1, o134, 1) | &&(=(matching1, 1), =(matching2, 1))
863_0_growReduce_LE(EOS(STATIC_863), matching1, o134, matching2) → 872_0_growReduce_Load(EOS(STATIC_872), 1, o134) | &&(=(matching1, 1), =(matching2, 1))
872_0_growReduce_Load(EOS(STATIC_872), matching1, o134) → 883_0_growReduce_Load(EOS(STATIC_883), o134, 1) | =(matching1, 1)
883_0_growReduce_Load(EOS(STATIC_883), o134, matching1) → 891_0_growReduce_InvokeMethod(EOS(STATIC_891), 1, o134) | =(matching1, 1)
891_0_growReduce_InvokeMethod(EOS(STATIC_891), matching1, o134) → 903_1_growReduce_InvokeMethod(903_0_growReduce_Load(EOS(STATIC_903), 1, o134), 1, o134) | =(matching1, 1)
903_0_growReduce_Load(EOS(STATIC_903), matching1, o134) → 913_0_growReduce_Load(EOS(STATIC_913), 1, o134) | =(matching1, 1)
913_0_growReduce_Load(EOS(STATIC_913), matching1, o134) → 769_0_growReduce_Load(EOS(STATIC_769), 1, o134) | =(matching1, 1)
808_0_growReduce_FieldAccess(EOS(STATIC_808), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o136))) → 815_0_growReduce_FieldAccess(EOS(STATIC_815), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o136))) | =(matching1, 0)
815_0_growReduce_FieldAccess(EOS(STATIC_815), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o136))) → 824_0_growReduce_Store(EOS(STATIC_824), 0, o136) | =(matching1, 0)
824_0_growReduce_Store(EOS(STATIC_824), matching1, o136) → 832_0_growReduce_JMP(EOS(STATIC_832), 0, o136) | =(matching1, 0)
832_0_growReduce_JMP(EOS(STATIC_832), matching1, o136) → 840_0_growReduce_Inc(EOS(STATIC_840), 0, o136) | =(matching1, 0)
840_0_growReduce_Inc(EOS(STATIC_840), matching1, o136) → 848_0_growReduce_Load(EOS(STATIC_848), 1, o136) | =(matching1, 0)
848_0_growReduce_Load(EOS(STATIC_848), matching1, o136) → 858_0_growReduce_ConstantStackPush(EOS(STATIC_858), 1, o136, 1) | =(matching1, 1)
858_0_growReduce_ConstantStackPush(EOS(STATIC_858), matching1, o136, matching2) → 866_0_growReduce_LE(EOS(STATIC_866), 1, o136, 1) | &&(=(matching1, 1), =(matching2, 1))
866_0_growReduce_LE(EOS(STATIC_866), matching1, o136, matching2) → 875_0_growReduce_Load(EOS(STATIC_875), 1, o136) | &&(=(matching1, 1), =(matching2, 1))
875_0_growReduce_Load(EOS(STATIC_875), matching1, o136) → 886_0_growReduce_Load(EOS(STATIC_886), o136, 1) | =(matching1, 1)
886_0_growReduce_Load(EOS(STATIC_886), o136, matching1) → 894_0_growReduce_InvokeMethod(EOS(STATIC_894), 1, o136) | =(matching1, 1)
894_0_growReduce_InvokeMethod(EOS(STATIC_894), matching1, o136) → 905_1_growReduce_InvokeMethod(905_0_growReduce_Load(EOS(STATIC_905), 1, o136), 1, o136) | =(matching1, 1)
905_0_growReduce_Load(EOS(STATIC_905), matching1, o136) → 915_0_growReduce_Load(EOS(STATIC_915), 1, o136) | =(matching1, 1)
915_0_growReduce_Load(EOS(STATIC_915), matching1, o136) → 940_0_growReduce_Load(EOS(STATIC_940), 1, o136) | =(matching1, 1)
940_0_growReduce_Load(EOS(STATIC_940), matching1, o136) → 769_0_growReduce_Load(EOS(STATIC_769), 1, o136) | =(matching1, 1)
R rules:
775_0_growReduce_NONNULL(EOS(STATIC_775), i84, NULL, NULL) → 778_0_growReduce_NONNULL(EOS(STATIC_778), i84, NULL, NULL)
778_0_growReduce_NONNULL(EOS(STATIC_778), i84, NULL, NULL) → 782_0_growReduce_Return(EOS(STATIC_782), i84, NULL)
903_1_growReduce_InvokeMethod(782_0_growReduce_Return(EOS(STATIC_782), matching1, NULL), matching2, NULL) → 948_0_growReduce_Return(EOS(STATIC_948), 1, NULL, 1, NULL) | &&(=(matching1, 1), =(matching2, 1))
903_1_growReduce_InvokeMethod(1342_0_growReduce_Return(EOS(STATIC_1342)), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o578))) → 1363_0_growReduce_Return(EOS(STATIC_1363), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o578))) | =(matching1, 1)
905_1_growReduce_InvokeMethod(782_0_growReduce_Return(EOS(STATIC_782), matching1, NULL), matching2, NULL) → 965_0_growReduce_Return(EOS(STATIC_965), 1, NULL, 1, NULL) | &&(=(matching1, 1), =(matching2, 1))
905_1_growReduce_InvokeMethod(1342_0_growReduce_Return(EOS(STATIC_1342)), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o582))) → 1370_0_growReduce_Return(EOS(STATIC_1370), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o582))) | =(matching1, 1)
948_0_growReduce_Return(EOS(STATIC_948), matching1, NULL, matching2, NULL) → 963_0_growReduce_Return(EOS(STATIC_963)) | &&(=(matching1, 1), =(matching2, 1))
963_0_growReduce_Return(EOS(STATIC_963)) → 975_0_growReduce_Return(EOS(STATIC_975))
965_0_growReduce_Return(EOS(STATIC_965), matching1, NULL, matching2, NULL) → 975_0_growReduce_Return(EOS(STATIC_975)) | &&(=(matching1, 1), =(matching2, 1))
969_1_growReduce_InvokeMethod(782_0_growReduce_Return(EOS(STATIC_782), matching1, NULL), matching2, NULL) → 1038_0_growReduce_Return(EOS(STATIC_1038), 0, NULL, 0, NULL) | &&(=(matching1, 0), =(matching2, 0))
969_1_growReduce_InvokeMethod(963_0_growReduce_Return(EOS(STATIC_963)), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1039_0_growReduce_Return(EOS(STATIC_1039), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 0)
969_1_growReduce_InvokeMethod(975_0_growReduce_Return(EOS(STATIC_975)), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1047_0_growReduce_Return(EOS(STATIC_1047), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 0)
969_1_growReduce_InvokeMethod(1378_0_growReduce_Return(EOS(STATIC_1378)), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o660))))) → 1425_0_growReduce_Return(EOS(STATIC_1425), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o660))))) | =(matching1, 0)
969_1_growReduce_InvokeMethod(1382_0_growReduce_Return(EOS(STATIC_1382)), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o673))))) → 1436_0_growReduce_Return(EOS(STATIC_1436), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o673))))) | =(matching1, 0)
970_1_growReduce_InvokeMethod(782_0_growReduce_Return(EOS(STATIC_782), matching1, NULL), matching2, NULL) → 1070_0_growReduce_Return(EOS(STATIC_1070), 0, NULL, 0, NULL) | &&(=(matching1, 0), =(matching2, 0))
970_1_growReduce_InvokeMethod(963_0_growReduce_Return(EOS(STATIC_963)), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1071_0_growReduce_Return(EOS(STATIC_1071), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 0)
970_1_growReduce_InvokeMethod(975_0_growReduce_Return(EOS(STATIC_975)), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1075_0_growReduce_Return(EOS(STATIC_1075), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 0)
970_1_growReduce_InvokeMethod(1378_0_growReduce_Return(EOS(STATIC_1378)), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o665))))) → 1428_0_growReduce_Return(EOS(STATIC_1428), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o665))))) | =(matching1, 0)
970_1_growReduce_InvokeMethod(1382_0_growReduce_Return(EOS(STATIC_1382)), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o678))))) → 1439_0_growReduce_Return(EOS(STATIC_1439), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o678))))) | =(matching1, 0)
1038_0_growReduce_Return(EOS(STATIC_1038), matching1, NULL, matching2, NULL) → 1067_0_growReduce_JMP(EOS(STATIC_1067)) | &&(=(matching1, 0), =(matching2, 0))
1039_0_growReduce_Return(EOS(STATIC_1039), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1048_0_growReduce_Return(EOS(STATIC_1048), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 0)
1047_0_growReduce_Return(EOS(STATIC_1047), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1048_0_growReduce_Return(EOS(STATIC_1048), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 0)
1048_0_growReduce_Return(EOS(STATIC_1048), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1261_0_growReduce_Return(EOS(STATIC_1261), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 0)
1065_1_growReduce_InvokeMethod(1292_0_growReduce_Return(EOS(STATIC_1292)), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o544))))) → 1328_0_growReduce_Return(EOS(STATIC_1328), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o544))))) | =(matching1, 2)
1065_1_growReduce_InvokeMethod(1296_0_growReduce_Return(EOS(STATIC_1296)), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o549))))) → 1338_0_growReduce_Return(EOS(STATIC_1338), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o549))))) | =(matching1, 2)
1067_0_growReduce_JMP(EOS(STATIC_1067)) → 1084_0_growReduce_JMP(EOS(STATIC_1084))
1070_0_growReduce_Return(EOS(STATIC_1070), matching1, NULL, matching2, NULL) → 1084_0_growReduce_JMP(EOS(STATIC_1084)) | &&(=(matching1, 0), =(matching2, 0))
1071_0_growReduce_Return(EOS(STATIC_1071), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1270_0_growReduce_Return(EOS(STATIC_1270), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 0)
1075_0_growReduce_Return(EOS(STATIC_1075), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1071_0_growReduce_Return(EOS(STATIC_1071), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 0)
1084_0_growReduce_JMP(EOS(STATIC_1084)) → 1087_0_growReduce_Return(EOS(STATIC_1087))
1156_0_growReduce_Return(EOS(STATIC_1156), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))))) → 1329_0_growReduce_Return(EOS(STATIC_1329), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))))) | =(matching1, 2)
1261_0_growReduce_Return(EOS(STATIC_1261), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o437))) → 1284_0_growReduce_JMP(EOS(STATIC_1284)) | =(matching1, 0)
1270_0_growReduce_Return(EOS(STATIC_1270), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o468))) → 1287_0_growReduce_JMP(EOS(STATIC_1287)) | =(matching1, 0)
1284_0_growReduce_JMP(EOS(STATIC_1284)) → 1292_0_growReduce_Return(EOS(STATIC_1292))
1287_0_growReduce_JMP(EOS(STATIC_1287)) → 1296_0_growReduce_Return(EOS(STATIC_1296))
1328_0_growReduce_Return(EOS(STATIC_1328), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o544))))) → 1329_0_growReduce_Return(EOS(STATIC_1329), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o544))))) | =(matching1, 2)
1329_0_growReduce_Return(EOS(STATIC_1329), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o553))))) → 1342_0_growReduce_Return(EOS(STATIC_1342)) | =(matching1, 2)
1338_0_growReduce_Return(EOS(STATIC_1338), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o549))))) → 1329_0_growReduce_Return(EOS(STATIC_1329), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o549))))) | =(matching1, 2)
1363_0_growReduce_Return(EOS(STATIC_1363), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o578))) → 1364_0_growReduce_Return(EOS(STATIC_1364), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o578))) | =(matching1, 1)
1364_0_growReduce_Return(EOS(STATIC_1364), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o587))) → 1378_0_growReduce_Return(EOS(STATIC_1378)) | =(matching1, 1)
1370_0_growReduce_Return(EOS(STATIC_1370), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o582))) → 1371_0_growReduce_Return(EOS(STATIC_1371), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o582))) | =(matching1, 1)
1371_0_growReduce_Return(EOS(STATIC_1371), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o607))) → 1382_0_growReduce_Return(EOS(STATIC_1382)) | =(matching1, 1)
1425_0_growReduce_Return(EOS(STATIC_1425), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o660))))) → 1261_0_growReduce_Return(EOS(STATIC_1261), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o660))))) | =(matching1, 0)
1428_0_growReduce_Return(EOS(STATIC_1428), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o665))))) → 1270_0_growReduce_Return(EOS(STATIC_1270), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o665))))) | =(matching1, 0)
1436_0_growReduce_Return(EOS(STATIC_1436), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o673))))) → 1261_0_growReduce_Return(EOS(STATIC_1261), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o673))))) | =(matching1, 0)
1439_0_growReduce_Return(EOS(STATIC_1439), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o678))))) → 1270_0_growReduce_Return(EOS(STATIC_1270), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o678))))) | =(matching1, 0)

Combined rules. Obtained 5 conditional rules for P and 17 conditional rules for R.

P rules:
775_0_growReduce_NONNULL(EOS(STATIC_775), 1, java.lang.Object(x1), java.lang.Object(x1)) → 1065_1_growReduce_InvokeMethod(775_0_growReduce_NONNULL(EOS(STATIC_775), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1)))), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1))))
775_0_growReduce_NONNULL(EOS(STATIC_775), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))) → 969_1_growReduce_InvokeMethod(775_0_growReduce_NONNULL(EOS(STATIC_775), 0, x1, x1), 0, x1)
775_0_growReduce_NONNULL(EOS(STATIC_775), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))) → 970_1_growReduce_InvokeMethod(775_0_growReduce_NONNULL(EOS(STATIC_775), 0, x1, x1), 0, x1)
775_0_growReduce_NONNULL(EOS(STATIC_775), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))) → 903_1_growReduce_InvokeMethod(775_0_growReduce_NONNULL(EOS(STATIC_775), 1, x1, x1), 1, x1)
775_0_growReduce_NONNULL(EOS(STATIC_775), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))) → 905_1_growReduce_InvokeMethod(775_0_growReduce_NONNULL(EOS(STATIC_775), 1, x1, x1), 1, x1)
R rules:
775_0_growReduce_NONNULL(EOS(STATIC_775), x0, NULL, NULL) → 782_0_growReduce_Return(EOS(STATIC_782), x0, NULL)
905_1_growReduce_InvokeMethod(782_0_growReduce_Return(EOS(STATIC_782), 1, NULL), 1, NULL) → 975_0_growReduce_Return(EOS(STATIC_975))
903_1_growReduce_InvokeMethod(782_0_growReduce_Return(EOS(STATIC_782), 1, NULL), 1, NULL) → 975_0_growReduce_Return(EOS(STATIC_975))
970_1_growReduce_InvokeMethod(782_0_growReduce_Return(EOS(STATIC_782), 0, NULL), 0, NULL) → 1087_0_growReduce_Return(EOS(STATIC_1087))
969_1_growReduce_InvokeMethod(782_0_growReduce_Return(EOS(STATIC_782), 0, NULL), 0, NULL) → 1087_0_growReduce_Return(EOS(STATIC_1087))
1065_1_growReduce_InvokeMethod(1292_0_growReduce_Return(EOS(STATIC_1292)), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))))) → 1342_0_growReduce_Return(EOS(STATIC_1342))
1065_1_growReduce_InvokeMethod(1296_0_growReduce_Return(EOS(STATIC_1296)), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))))) → 1342_0_growReduce_Return(EOS(STATIC_1342))
969_1_growReduce_InvokeMethod(1378_0_growReduce_Return(EOS(STATIC_1378)), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))))) → 1292_0_growReduce_Return(EOS(STATIC_1292))
969_1_growReduce_InvokeMethod(1382_0_growReduce_Return(EOS(STATIC_1382)), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))))) → 1292_0_growReduce_Return(EOS(STATIC_1292))
969_1_growReduce_InvokeMethod(963_0_growReduce_Return(EOS(STATIC_963)), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1292_0_growReduce_Return(EOS(STATIC_1292))
969_1_growReduce_InvokeMethod(975_0_growReduce_Return(EOS(STATIC_975)), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1292_0_growReduce_Return(EOS(STATIC_1292))
970_1_growReduce_InvokeMethod(963_0_growReduce_Return(EOS(STATIC_963)), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1296_0_growReduce_Return(EOS(STATIC_1296))
970_1_growReduce_InvokeMethod(975_0_growReduce_Return(EOS(STATIC_975)), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1296_0_growReduce_Return(EOS(STATIC_1296))
970_1_growReduce_InvokeMethod(1378_0_growReduce_Return(EOS(STATIC_1378)), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))))) → 1296_0_growReduce_Return(EOS(STATIC_1296))
970_1_growReduce_InvokeMethod(1382_0_growReduce_Return(EOS(STATIC_1382)), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))))) → 1296_0_growReduce_Return(EOS(STATIC_1296))
903_1_growReduce_InvokeMethod(1342_0_growReduce_Return(EOS(STATIC_1342)), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))) → 1378_0_growReduce_Return(EOS(STATIC_1378))
905_1_growReduce_InvokeMethod(1342_0_growReduce_Return(EOS(STATIC_1342)), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))) → 1382_0_growReduce_Return(EOS(STATIC_1382))

Filtered ground terms:

905_1_growReduce_InvokeMethod(x1, x2, x3) → 905_1_growReduce_InvokeMethod(x1, x3)
775_0_growReduce_NONNULL(x1, x2, x3, x4) → 775_0_growReduce_NONNULL(x2, x3, x4)
AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1, x2) → AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x2)
903_1_growReduce_InvokeMethod(x1, x2, x3) → 903_1_growReduce_InvokeMethod(x1, x3)
970_1_growReduce_InvokeMethod(x1, x2, x3) → 970_1_growReduce_InvokeMethod(x1, x3)
969_1_growReduce_InvokeMethod(x1, x2, x3) → 969_1_growReduce_InvokeMethod(x1, x3)
1065_1_growReduce_InvokeMethod(x1, x2, x3) → 1065_1_growReduce_InvokeMethod(x1, x3)
1382_0_growReduce_Return(x1) → 1382_0_growReduce_Return
1342_0_growReduce_Return(x1) → 1342_0_growReduce_Return
1378_0_growReduce_Return(x1) → 1378_0_growReduce_Return
1296_0_growReduce_Return(x1) → 1296_0_growReduce_Return
975_0_growReduce_Return(x1) → 975_0_growReduce_Return
963_0_growReduce_Return(x1) → 963_0_growReduce_Return
1292_0_growReduce_Return(x1) → 1292_0_growReduce_Return
1087_0_growReduce_Return(x1) → 1087_0_growReduce_Return
782_0_growReduce_Return(x1, x2, x3) → 782_0_growReduce_Return(x2)

Filtered duplicate args:

775_0_growReduce_NONNULL(x1, x2, x3) → 775_0_growReduce_NONNULL(x1, x3)

Combined rules. Obtained 5 conditional rules for P and 17 conditional rules for R.

P rules:
775_0_growReduce_NONNULL(1, java.lang.Object(x1)) → 1065_1_growReduce_InvokeMethod(775_0_growReduce_NONNULL(2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1)))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1))))
775_0_growReduce_NONNULL(2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → 969_1_growReduce_InvokeMethod(775_0_growReduce_NONNULL(0, x1), x1)
775_0_growReduce_NONNULL(2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → 970_1_growReduce_InvokeMethod(775_0_growReduce_NONNULL(0, x1), x1)
775_0_growReduce_NONNULL(0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → 903_1_growReduce_InvokeMethod(775_0_growReduce_NONNULL(1, x1), x1)
775_0_growReduce_NONNULL(0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → 905_1_growReduce_InvokeMethod(775_0_growReduce_NONNULL(1, x1), x1)
R rules:
775_0_growReduce_NONNULL(x0, NULL) → 782_0_growReduce_Return(x0)
905_1_growReduce_InvokeMethod(782_0_growReduce_Return(1), NULL) → 975_0_growReduce_Return
903_1_growReduce_InvokeMethod(782_0_growReduce_Return(1), NULL) → 975_0_growReduce_Return
970_1_growReduce_InvokeMethod(782_0_growReduce_Return(0), NULL) → 1087_0_growReduce_Return
969_1_growReduce_InvokeMethod(782_0_growReduce_Return(0), NULL) → 1087_0_growReduce_Return
1065_1_growReduce_InvokeMethod(1292_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))))) → 1342_0_growReduce_Return
1065_1_growReduce_InvokeMethod(1296_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))))) → 1342_0_growReduce_Return
969_1_growReduce_InvokeMethod(1378_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))))) → 1292_0_growReduce_Return
969_1_growReduce_InvokeMethod(1382_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))))) → 1292_0_growReduce_Return
969_1_growReduce_InvokeMethod(963_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(NULL))) → 1292_0_growReduce_Return
969_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(NULL))) → 1292_0_growReduce_Return
970_1_growReduce_InvokeMethod(963_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(NULL))) → 1296_0_growReduce_Return
970_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(NULL))) → 1296_0_growReduce_Return
970_1_growReduce_InvokeMethod(1378_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))))) → 1296_0_growReduce_Return
970_1_growReduce_InvokeMethod(1382_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))))) → 1296_0_growReduce_Return
903_1_growReduce_InvokeMethod(1342_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → 1378_0_growReduce_Return
905_1_growReduce_InvokeMethod(1342_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → 1382_0_growReduce_Return

Performed bisimulation on rules. Used the following equivalence classes: {[970_1_growReduce_InvokeMethod_2, 969_1_growReduce_InvokeMethod_2]=970_1_growReduce_InvokeMethod_2, [905_1_growReduce_InvokeMethod_2, 903_1_growReduce_InvokeMethod_2]=905_1_growReduce_InvokeMethod_2, [975_0_growReduce_Return, 1087_0_growReduce_Return, 1292_0_growReduce_Return, 1342_0_growReduce_Return, 1296_0_growReduce_Return, 1378_0_growReduce_Return, 1382_0_growReduce_Return, 963_0_growReduce_Return]=975_0_growReduce_Return}

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

P rules:
775_0_GROWREDUCE_NONNULL(1, java.lang.Object(x1)) → 775_0_GROWREDUCE_NONNULL(2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1))))
775_0_GROWREDUCE_NONNULL(2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → 775_0_GROWREDUCE_NONNULL(0, x1)
775_0_GROWREDUCE_NONNULL(0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → 775_0_GROWREDUCE_NONNULL(1, x1)
R rules:
775_0_growReduce_NONNULL(x0, NULL) → 782_0_growReduce_Return(x0)
905_1_growReduce_InvokeMethod(782_0_growReduce_Return(1), NULL) → 975_0_growReduce_Return
970_1_growReduce_InvokeMethod(782_0_growReduce_Return(0), NULL) → 975_0_growReduce_Return
1065_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))))) → 975_0_growReduce_Return
970_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))))) → 975_0_growReduce_Return
970_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(NULL))) → 975_0_growReduce_Return
905_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → 975_0_growReduce_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:
none

The ITRS R consists of the following rules:
775_0_growReduce_NONNULL(x0, NULL) → 782_0_growReduce_Return(x0)
905_1_growReduce_InvokeMethod(782_0_growReduce_Return(1), NULL) → 975_0_growReduce_Return
970_1_growReduce_InvokeMethod(782_0_growReduce_Return(0), NULL) → 975_0_growReduce_Return
1065_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))))) → 975_0_growReduce_Return
970_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))))) → 975_0_growReduce_Return
970_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(NULL))) → 975_0_growReduce_Return
905_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → 975_0_growReduce_Return

The integer pair graph contains the following rules and edges:
(0): 775_0_GROWREDUCE_NONNULL(1, java.lang.Object(x1[0])) → 775_0_GROWREDUCE_NONNULL(2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[0]))))
(1): 775_0_GROWREDUCE_NONNULL(2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[1]))) → 775_0_GROWREDUCE_NONNULL(0, x1[1])
(2): 775_0_GROWREDUCE_NONNULL(0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[2]))) → 775_0_GROWREDUCE_NONNULL(1, x1[2])

(0) -> (0), if (2 →^* 1∧java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[0]))) →^* java.lang.Object(x1[0]'))

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

(0) -> (2), if (2 →^* 0∧java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[0]))) →^* java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[2])))

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

(1) -> (1), if (0 →^* 2∧x1[1] →^* java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[1]')))

(1) -> (2), if x1[1] →^* java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[2]))

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

(2) -> (1), if (1 →^* 2∧x1[2] →^* java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[1])))

(2) -> (2), if (1 →^* 0∧x1[2] →^* java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[2]')))

The set Q consists of the following terms:
775_0_growReduce_NONNULL(x0, NULL)
905_1_growReduce_InvokeMethod(782_0_growReduce_Return(1), NULL)
970_1_growReduce_InvokeMethod(782_0_growReduce_Return(0), NULL)
1065_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x0)))))
970_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x0)))))
970_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(NULL)))
905_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x0)))

(8) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(9) Obligation:

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

775_0_GROWREDUCE_NONNULL(pos(s(01)), java.lang.Object(x1[0])) → 775_0_GROWREDUCE_NONNULL(pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[0]))))
775_0_GROWREDUCE_NONNULL(pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[1]))) → 775_0_GROWREDUCE_NONNULL(pos(01), x1[1])
775_0_GROWREDUCE_NONNULL(pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[2]))) → 775_0_GROWREDUCE_NONNULL(pos(s(01)), x1[2])

The TRS R consists of the following rules:

775_0_growReduce_NONNULL(x0, NULL) → 782_0_growReduce_Return(x0)
905_1_growReduce_InvokeMethod(782_0_growReduce_Return(pos(s(01))), NULL) → 975_0_growReduce_Return
970_1_growReduce_InvokeMethod(782_0_growReduce_Return(pos(01)), NULL) → 975_0_growReduce_Return
1065_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))))) → 975_0_growReduce_Return
970_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))))) → 975_0_growReduce_Return
970_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(NULL))) → 975_0_growReduce_Return
905_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → 975_0_growReduce_Return

The set Q consists of the following terms:

775_0_growReduce_NONNULL(x0, NULL)
905_1_growReduce_InvokeMethod(782_0_growReduce_Return(pos(s(01))), NULL)
970_1_growReduce_InvokeMethod(782_0_growReduce_Return(pos(01)), NULL)
1065_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x0)))))
970_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x0)))))
970_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(NULL)))
905_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x0)))

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

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) Obligation:

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

775_0_GROWREDUCE_NONNULL(pos(s(01)), java.lang.Object(x1[0])) → 775_0_GROWREDUCE_NONNULL(pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[0]))))
775_0_GROWREDUCE_NONNULL(pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[1]))) → 775_0_GROWREDUCE_NONNULL(pos(01), x1[1])
775_0_GROWREDUCE_NONNULL(pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[2]))) → 775_0_GROWREDUCE_NONNULL(pos(s(01)), x1[2])

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

775_0_growReduce_NONNULL(x0, NULL)
905_1_growReduce_InvokeMethod(782_0_growReduce_Return(pos(s(01))), NULL)
970_1_growReduce_InvokeMethod(782_0_growReduce_Return(pos(01)), NULL)
1065_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x0)))))
970_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x0)))))
970_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(NULL)))
905_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x0)))

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

(12) QReductionProof (EQUIVALENT transformation)

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

775_0_growReduce_NONNULL(x0, NULL)
905_1_growReduce_InvokeMethod(782_0_growReduce_Return(pos(s(01))), NULL)
970_1_growReduce_InvokeMethod(782_0_growReduce_Return(pos(01)), NULL)
1065_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x0)))))
970_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x0)))))
970_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(NULL)))
905_1_growReduce_InvokeMethod(975_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x0)))

(13) Obligation:

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

775_0_GROWREDUCE_NONNULL(pos(s(01)), java.lang.Object(x1[0])) → 775_0_GROWREDUCE_NONNULL(pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[0]))))
775_0_GROWREDUCE_NONNULL(pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[1]))) → 775_0_GROWREDUCE_NONNULL(pos(01), x1[1])
775_0_GROWREDUCE_NONNULL(pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[2]))) → 775_0_GROWREDUCE_NONNULL(pos(s(01)), x1[2])

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

(14) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

775_0_GROWREDUCE_NONNULL(pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[1]))) → 775_0_GROWREDUCE_NONNULL(pos(01), x1[1])

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :

POL(775_0_GROWREDUCE_NONNULL(x₁, x₂)) = 0 +
[ 1, 1 ]

· x₁ +
[ 1, 0 ]

· x₂

POL(pos(x₁)) =
/ 1 \

\ 1 /

+
/ 0 1 \

\ 0 0 /

· x₁

POL(s(x₁)) =
/ 0 \

\ 1 /

+
/ 0 0 \

\ 1 0 /

· x₁

POL(01) =
/ 1 \

\ 1 /

POL(java.lang.Object(x₁)) =
/ 0 \

\ 0 /

+
/ 0 1 \

\ 0 0 /

· x₁

POL(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x₁)) =
/ 0 \

\ 1 /

+
/ 0 0 \

\ 1 0 /

· x₁

The following usable rules [FROCOS05] were oriented: none

(15) Obligation:

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

775_0_GROWREDUCE_NONNULL(pos(s(01)), java.lang.Object(x1[0])) → 775_0_GROWREDUCE_NONNULL(pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[0]))))
775_0_GROWREDUCE_NONNULL(pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[2]))) → 775_0_GROWREDUCE_NONNULL(pos(s(01)), x1[2])

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

(16) DependencyGraphProof (EQUIVALENT transformation)

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

(17) TRUE

(18) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: AlternatingGrowReduceRec2.AlternatingGrowReduceRec2.createList(I)LAlternatingGrowReduceRec2/AlternatingGrowReduceRec2;
SCC calls the following helper methods: AlternatingGrowReduceRec2.AlternatingGrowReduceRec2.createList(I)LAlternatingGrowReduceRec2/AlternatingGrowReduceRec2;
Performed SCC analyses: UsedFieldsAnalysis

(19) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 22 rules for P and 10 rules for R.

P rules:
159_0_createList_Duplicate(EOS(STATIC_159), i18) → 164_0_createList_ConstantStackPush(EOS(STATIC_164), i18)
164_0_createList_ConstantStackPush(EOS(STATIC_164), i18) → 170_0_createList_InvokeMethod(EOS(STATIC_170), i18)
170_0_createList_InvokeMethod(EOS(STATIC_170), i18) → 177_0_<init>_Load(EOS(STATIC_177), i18)
177_0_<init>_Load(EOS(STATIC_177), i18) → 186_0_<init>_InvokeMethod(EOS(STATIC_186), i18)
186_0_<init>_InvokeMethod(EOS(STATIC_186), i18) → 196_0_<init>_Load(EOS(STATIC_196), i18)
196_0_<init>_Load(EOS(STATIC_196), i18) → 203_0_<init>_Load(EOS(STATIC_203), i18)
203_0_<init>_Load(EOS(STATIC_203), i18) → 210_0_<init>_FieldAccess(EOS(STATIC_210), i18)
210_0_<init>_FieldAccess(EOS(STATIC_210), i18) → 216_0_<init>_Return(EOS(STATIC_216), i18)
216_0_<init>_Return(EOS(STATIC_216), i18) → 221_0_createList_Store(EOS(STATIC_221), i18)
221_0_createList_Store(EOS(STATIC_221), i18) → 226_0_createList_Load(EOS(STATIC_226), i18)
226_0_createList_Load(EOS(STATIC_226), i18) → 230_0_createList_ConstantStackPush(EOS(STATIC_230), i18, i18)
230_0_createList_ConstantStackPush(EOS(STATIC_230), i18, i18) → 233_0_createList_LE(EOS(STATIC_233), i18, i18, 1)
233_0_createList_LE(EOS(STATIC_233), i26, i26, matching1) → 238_0_createList_LE(EOS(STATIC_238), i26, i26, 1) | =(matching1, 1)
238_0_createList_LE(EOS(STATIC_238), i26, i26, matching1) → 242_0_createList_Load(EOS(STATIC_242), i26) | &&(>(i26, 1), =(matching1, 1))
242_0_createList_Load(EOS(STATIC_242), i26) → 244_0_createList_Load(EOS(STATIC_244), i26)
244_0_createList_Load(EOS(STATIC_244), i26) → 246_0_createList_ConstantStackPush(EOS(STATIC_246), i26)
246_0_createList_ConstantStackPush(EOS(STATIC_246), i26) → 256_0_createList_IntArithmetic(EOS(STATIC_256), i26, 1)
256_0_createList_IntArithmetic(EOS(STATIC_256), i26, matching1) → 260_0_createList_InvokeMethod(EOS(STATIC_260), -(i26, 1)) | &&(>(i26, 0), =(matching1, 1))
260_0_createList_InvokeMethod(EOS(STATIC_260), i30) → 263_1_createList_InvokeMethod(263_0_createList_New(EOS(STATIC_263), i30), i30)
263_0_createList_New(EOS(STATIC_263), i30) → 268_0_createList_New(EOS(STATIC_268), i30)
268_0_createList_New(EOS(STATIC_268), i30) → 153_0_createList_New(EOS(STATIC_153), i30)
153_0_createList_New(EOS(STATIC_153), i18) → 159_0_createList_Duplicate(EOS(STATIC_159), i18)
R rules:
233_0_createList_LE(EOS(STATIC_233), i25, i25, matching1) → 237_0_createList_LE(EOS(STATIC_237), i25, i25, 1) | =(matching1, 1)
237_0_createList_LE(EOS(STATIC_237), i25, i25, matching1) → 241_0_createList_Load(EOS(STATIC_241)) | &&(<=(i25, 1), =(matching1, 1))
241_0_createList_Load(EOS(STATIC_241)) → 243_0_createList_Return(EOS(STATIC_243))
263_1_createList_InvokeMethod(243_0_createList_Return(EOS(STATIC_243)), matching1) → 285_0_createList_Return(EOS(STATIC_285), 1) | =(matching1, 1)
263_1_createList_InvokeMethod(361_0_createList_Return(EOS(STATIC_361)), i53) → 393_0_createList_Return(EOS(STATIC_393), i53)
285_0_createList_Return(EOS(STATIC_285), matching1) → 340_0_createList_Return(EOS(STATIC_340), 1) | =(matching1, 1)
340_0_createList_Return(EOS(STATIC_340), i45) → 346_0_createList_FieldAccess(EOS(STATIC_346))
346_0_createList_FieldAccess(EOS(STATIC_346)) → 354_0_createList_Load(EOS(STATIC_354))
354_0_createList_Load(EOS(STATIC_354)) → 361_0_createList_Return(EOS(STATIC_361))
393_0_createList_Return(EOS(STATIC_393), i53) → 340_0_createList_Return(EOS(STATIC_340), i53)

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

P rules:
159_0_createList_Duplicate(EOS(STATIC_159), x0) → 263_1_createList_InvokeMethod(159_0_createList_Duplicate(EOS(STATIC_159), -(x0, 1)), -(x0, 1)) | >(x0, 1)
R rules:
263_1_createList_InvokeMethod(243_0_createList_Return(EOS(STATIC_243)), 1) → 361_0_createList_Return(EOS(STATIC_361))
263_1_createList_InvokeMethod(361_0_createList_Return(EOS(STATIC_361)), x0) → 361_0_createList_Return(EOS(STATIC_361))

Filtered ground terms:

159_0_createList_Duplicate(x1, x2) → 159_0_createList_Duplicate(x2)
Cond_159_0_createList_Duplicate(x1, x2, x3) → Cond_159_0_createList_Duplicate(x1, x3)
361_0_createList_Return(x1) → 361_0_createList_Return
243_0_createList_Return(x1) → 243_0_createList_Return

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

P rules:
159_0_createList_Duplicate(x0) → 263_1_createList_InvokeMethod(159_0_createList_Duplicate(-(x0, 1)), -(x0, 1)) | >(x0, 1)
R rules:
263_1_createList_InvokeMethod(243_0_createList_Return, 1) → 361_0_createList_Return
263_1_createList_InvokeMethod(361_0_createList_Return, x0) → 361_0_createList_Return

Performed bisimulation on rules. Used the following equivalence classes: {[243_0_createList_Return, 361_0_createList_Return]=243_0_createList_Return}

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

P rules:
159_0_CREATELIST_DUPLICATE(x0) → COND_159_0_CREATELIST_DUPLICATE(>(x0, 1), x0)
COND_159_0_CREATELIST_DUPLICATE(TRUE, x0) → 159_0_CREATELIST_DUPLICATE(-(x0, 1))
R rules:
263_1_createList_InvokeMethod(243_0_createList_Return, 1) → 243_0_createList_Return
263_1_createList_InvokeMethod(243_0_createList_Return, x0) → 243_0_createList_Return

(20) 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:
263_1_createList_InvokeMethod(243_0_createList_Return, 1) → 243_0_createList_Return
263_1_createList_InvokeMethod(243_0_createList_Return, x0) → 243_0_createList_Return

The integer pair graph contains the following rules and edges:
(0): 159_0_CREATELIST_DUPLICATE(x0[0]) → COND_159_0_CREATELIST_DUPLICATE(x0[0] > 1, x0[0])
(1): COND_159_0_CREATELIST_DUPLICATE(TRUE, x0[1]) → 159_0_CREATELIST_DUPLICATE(x0[1] - 1)

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

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

The set Q consists of the following terms:
263_1_createList_InvokeMethod(243_0_createList_Return, x0)

(21) 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@4c0f73a3 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 159_0_CREATELIST_DUPLICATE(x0) → COND_159_0_CREATELIST_DUPLICATE(>(x0, 1), x0) the following chains were created:

We consider the chain 159_0_CREATELIST_DUPLICATE(x0[0]) → COND_159_0_CREATELIST_DUPLICATE(>(x0[0], 1), x0[0]), COND_159_0_CREATELIST_DUPLICATE(TRUE, x0[1]) → 159_0_CREATELIST_DUPLICATE(-(x0[1], 1)) which results in the following constraint:
(1)    (>(x0[0], 1)=TRUE∧x0[0]=x0[1] ⇒ 159_0_CREATELIST_DUPLICATE(x0[0])≥NonInfC∧159_0_CREATELIST_DUPLICATE(x0[0])≥COND_159_0_CREATELIST_DUPLICATE(>(x0[0], 1), x0[0])∧(U^Increasing(COND_159_0_CREATELIST_DUPLICATE(>(x0[0], 1), x0[0])), ≥))

We simplified constraint (1) using rule (IV) which results in the following new constraint:
(2)    (>(x0[0], 1)=TRUE ⇒ 159_0_CREATELIST_DUPLICATE(x0[0])≥NonInfC∧159_0_CREATELIST_DUPLICATE(x0[0])≥COND_159_0_CREATELIST_DUPLICATE(>(x0[0], 1), x0[0])∧(U^Increasing(COND_159_0_CREATELIST_DUPLICATE(>(x0[0], 1), x0[0])), ≥))

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

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

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x0[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_159_0_CREATELIST_DUPLICATE(>(x0[0], 1), x0[0])), ≥)∧[(-1)Bound*bni_10] + [(2)bni_10]x0[0] ≥ 0∧[(-1)bso_11] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x0[0] ≥ 0 ⇒ (U^Increasing(COND_159_0_CREATELIST_DUPLICATE(>(x0[0], 1), x0[0])), ≥)∧[(-1)Bound*bni_10 + (4)bni_10] + [(2)bni_10]x0[0] ≥ 0∧[(-1)bso_11] ≥ 0)

For Pair COND_159_0_CREATELIST_DUPLICATE(TRUE, x0) → 159_0_CREATELIST_DUPLICATE(-(x0, 1)) the following chains were created:

We consider the chain COND_159_0_CREATELIST_DUPLICATE(TRUE, x0[1]) → 159_0_CREATELIST_DUPLICATE(-(x0[1], 1)) which results in the following constraint:
(7)    (COND_159_0_CREATELIST_DUPLICATE(TRUE, x0[1])≥NonInfC∧COND_159_0_CREATELIST_DUPLICATE(TRUE, x0[1])≥159_0_CREATELIST_DUPLICATE(-(x0[1], 1))∧(U^Increasing(159_0_CREATELIST_DUPLICATE(-(x0[1], 1))), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    ((U^Increasing(159_0_CREATELIST_DUPLICATE(-(x0[1], 1))), ≥)∧[bni_12] = 0∧[2 + (-1)bso_13] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    ((U^Increasing(159_0_CREATELIST_DUPLICATE(-(x0[1], 1))), ≥)∧[bni_12] = 0∧[2 + (-1)bso_13] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    ((U^Increasing(159_0_CREATELIST_DUPLICATE(-(x0[1], 1))), ≥)∧[bni_12] = 0∧[2 + (-1)bso_13] ≥ 0)

We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(11)    ((U^Increasing(159_0_CREATELIST_DUPLICATE(-(x0[1], 1))), ≥)∧[bni_12] = 0∧0 = 0∧[2 + (-1)bso_13] ≥ 0)

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

159_0_CREATELIST_DUPLICATE(x0) → COND_159_0_CREATELIST_DUPLICATE(>(x0, 1), x0)
- (x0[0] ≥ 0 ⇒ (U^Increasing(COND_159_0_CREATELIST_DUPLICATE(>(x0[0], 1), x0[0])), ≥)∧[(-1)Bound*bni_10 + (4)bni_10] + [(2)bni_10]x0[0] ≥ 0∧[(-1)bso_11] ≥ 0)
COND_159_0_CREATELIST_DUPLICATE(TRUE, x0) → 159_0_CREATELIST_DUPLICATE(-(x0, 1))
- ((U^Increasing(159_0_CREATELIST_DUPLICATE(-(x0[1], 1))), ≥)∧[bni_12] = 0∧0 = 0∧[2 + (-1)bso_13] ≥ 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(263_1_createList_InvokeMethod(x₁, x₂)) = [-1]
POL(243_0_createList_Return) = [-1]
POL(1) = [1]
POL(159_0_CREATELIST_DUPLICATE(x₁)) = [2]x₁
POL(COND_159_0_CREATELIST_DUPLICATE(x₁, x₂)) = [2]x₂
POL(>(x₁, x₂)) = [-1]
POL(-(x₁, x₂)) = x₁ + [-1]x₂

The following pairs are in P_>:

COND_159_0_CREATELIST_DUPLICATE(TRUE, x0[1]) → 159_0_CREATELIST_DUPLICATE(-(x0[1], 1))

The following pairs are in P_bound:

159_0_CREATELIST_DUPLICATE(x0[0]) → COND_159_0_CREATELIST_DUPLICATE(>(x0[0], 1), x0[0])

The following pairs are in P_≥:

159_0_CREATELIST_DUPLICATE(x0[0]) → COND_159_0_CREATELIST_DUPLICATE(>(x0[0], 1), x0[0])

There are no usable rules.

(22) Complex Obligation (AND)

(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:
263_1_createList_InvokeMethod(243_0_createList_Return, 1) → 243_0_createList_Return
263_1_createList_InvokeMethod(243_0_createList_Return, x0) → 243_0_createList_Return

The integer pair graph contains the following rules and edges:
(0): 159_0_CREATELIST_DUPLICATE(x0[0]) → COND_159_0_CREATELIST_DUPLICATE(x0[0] > 1, x0[0])

The set Q consists of the following terms:
263_1_createList_InvokeMethod(243_0_createList_Return, x0)

(24) IDependencyGraphProof (EQUIVALENT transformation)

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

(25) TRUE

(26) 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:
263_1_createList_InvokeMethod(243_0_createList_Return, 1) → 243_0_createList_Return
263_1_createList_InvokeMethod(243_0_createList_Return, x0) → 243_0_createList_Return

The integer pair graph contains the following rules and edges:
(1): COND_159_0_CREATELIST_DUPLICATE(TRUE, x0[1]) → 159_0_CREATELIST_DUPLICATE(x0[1] - 1)

The set Q consists of the following terms:
263_1_createList_InvokeMethod(243_0_createList_Return, x0)

(27) IDependencyGraphProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIDPv1Proof (SOUND transformation)

(7) Obligation:

(8) IDPtoQDPProof (SOUND transformation)

(9) Obligation:

(10) UsableRulesProof (EQUIVALENT transformation)

(11) Obligation:

(12) QReductionProof (EQUIVALENT transformation)

(13) Obligation:

(14) QDPOrderProof (EQUIVALENT transformation)

(15) Obligation:

(16) DependencyGraphProof (EQUIVALENT transformation)

(17) TRUE

(18) Obligation:

(19) SCCToIDPv1Proof (SOUND transformation)

(20) Obligation:

(21) IDPNonInfProof (SOUND transformation)

(22) Complex Obligation (AND)

(23) Obligation:

(24) IDependencyGraphProof (EQUIVALENT transformation)

(25) TRUE

(26) Obligation:

(27) IDependencyGraphProof (EQUIVALENT transformation)

(28) TRUE